运行Boolector二进制程序时执行SMT-LIB代码遇问题求助

嘿，我来帮你搞定这段在Boolector里运行的SMT-LIB代码问题。你提到的代码来自《如何以十六进制格式打印输出》，但目前给出的片段不完整（最后卡在(ass...），我先帮你补全逻辑，再说明怎么让它正常运行并输出十六进制结果。

补全后的完整SMT-LIB代码 #

从你给出的片段来看，代码是用来验证16位乘法和32位乘法截断结果的一致性，我把逻辑补全并添加十六进制打印的配置：

(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))

; 定义16位直接乘法结果
(assert (= gen_mul (bvmul val1 val2)))
; 将16位操作数零扩展为32位
(assert (= eval1 (zero_extend val1 (_ BitVec 16))))
(assert (= eval2 (zero_extend val2 (_ BitVec 16))))
; 计算32位乘法结果
(assert (= org_mul (bvmul eval1 eval2)))
; 截取32位结果的低16位
(assert (= rem17 (bvand org_mul #x0000FFFF)))
(assert (= res (extract 15 0 rem17)))
; 断言两种方式得到的16位结果一致
(assert (= gen_mul res))

; 开启十六进制打印模式
(set-option :pp-hex true)
; 检查可满足性并输出模型
(check-sat)
(get-model)

运行Boolector的正确命令 #

把上面的代码保存为mul_test.smt2，然后在终端执行以下命令：

boolector -m mul_test.smt2

• -m参数是告诉Boolector输出模型结果，这样你就能看到各个变量的十六进制值了。

关键注意事项 #

• 代码完整性：之前的片段截断会导致Boolector解析失败，必须确保所有断言和指令都完整闭合。
• 十六进制打印开关：(set-option :pp-hex true)是Boolector特有的选项，开启后所有位向量类型的变量值都会以十六进制格式输出，这正是你需要的功能。
• 自定义测试值：如果需要测试具体的乘法案例，可以添加比如(assert (= val1 #x1A2B))、(assert (= val2 #x3C4D))这样的断言，替换成你想要的十六进制数值。

内容的提问来源于stack exchange，提问作者lightning