运行布尔值二进制答案

【问题标题】：Running boolector binary运行布尔值二进制
【发布时间】：2018-03-20 17:41:47
【问题描述】：

我尝试运行下面的代码（直接取自how to print output in hexadecimal format，声称它有效）：

(set-logic QF_BV)
(set-info :smt-lib-version 2.0)

(declare-const val1  (_ BitVec 16))
(declare-const val2  (_ BitVec 16))

(declare-const gen_mul  (_ BitVec 16))
(declare-const eval1  (_ BitVec 32))
(declare-const eval2  (_ BitVec 32))
(declare-const org_mul  (_ BitVec 32))
(declare-const rem17 (_ BitVec 32))
(declare-const res (_ BitVec 16))

(assert (= gen_mul (bvmul val1 val2)))
(assert (= eval1 (concat #x0000 val1)))
(assert (= eval2 (concat #x0000 val2)))
(assert (= org_mul (bvmul eval1 eval2)))
(assert (= rem17 (bvurem org_mul #x00010001)))
(assert (= res ((_ extract 15 0) rem17)))
(assert (= val1 #xb621))
(assert (= val2 #xd620))
(check-sat)

(get-value (val1))
(get-value (val2))
(get-value (org_mul))
(get-value (gen_mul))
(get-value (eval1))
(get-value (eval2))
(get-value (org_mul))
(get-value (rem17))
(get-value (res))
(exit)

我尝试运行 ./boolector ex.smt2，得到以下错误： boolector: ex.smt2:4:2: 'declare-const' 处的预期命令

有人知道这是怎么回事吗？

【问题讨论】：

标签： smt sat

【解决方案1】：

Boolector 似乎不支持declare-const。而是使用declare-fun。也就是说，而不是写：

(declare-const val1  (_ BitVec 16))

写：

(declare-fun val1 () (_ BitVec 16))

请注意名称后面的额外括号。您需要为每个declare-const 执行此操作，否则无需进行其他更改。

严格来说，这是一个 boolector 缺陷，因为 declare-const 是 SMTLib 规范的一部分。请参阅http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 的第 4.2.3 节。通知他们可能是个好主意。

【讨论】：