stp：下划线的含义？

【问题标题】：SMTLIB / z3 / stp: Meaning of underscore?SMTLIB / z3 / stp：下划线的含义？
【发布时间】：2016-02-01 10:06:26
【问题描述】：

我不明白下划线的含义，例如在这些（不相关的）表达式中

(display (_ bv20 8))
(declare-const x (_ BitVec 64))

或者这个：

(declare-fun a () (Array (_ BitVec 32) (_ BitVec 7)))

“_”是什么意思？

【问题讨论】：

标签： z3 smt

【解决方案1】：

根据 SMTLIB 手册的 §3.3 Identifiers 部分，(_ <symbol> <index>+) 是一种定义索引标识符的方法。我认为这相当于在其他语言的标识符中编码信息，例如int_64，只是数据具有更明确的结构。

【讨论】：