奇怪的语法错误答案

【问题标题】：Weird error with syntax奇怪的语法错误
【发布时间】：2014-04-14 12:57:06
【问题描述】：

只是尝试使用 smtlib。我没有看到以下内容有什么问题...

(set-logic BV)
(declare-fun var1 () (_ BitVec 32)) ; a is a constant
(declare-fun var2 () (_ BitVec 32)) ; a is a constant
(declare-fun var3 () (_ BitVec 32)) ; a is a constant

(assert(
    (= var1 var2)
    and
    (= var3 bvsub(var1 var2) )
    ))
(check-sat)
(get-model)

用 z3 运行它，错误是：（错误“第 7 行第 2 列：无效的限定/索引标识符，'_' 或 'as' 预期”）

【问题讨论】：

问题是 Z3 的输入语法是前缀表示法（en.wikipedia.org/wiki/Polish_notation），你有它的等式（例如，(= var1 var2)，但不是其他一些部分（例如，a and b )，您使用中缀表示法 (en.wikipedia.org/wiki/Infix_notation)。

标签： z3 smt satisfiability

【解决方案1】：

后来修改了2次，终于弄明白了：

(set-logic BV)
(declare-fun var1 () (_ BitVec 32)) ; a is a constant
(declare-fun var2 () (_ BitVec 32)) ; a is a constant
(declare-fun var3 () (_ BitVec 32)) ; a is a constant

(assert(
    and (= var1 var2) (= var3 (bvsub var1 var2))))
(check-sat)
(get-model)

【讨论】：