如何使用smt2格式的z3解算器生成位向量公式的多个模型?在
在实现位向量的IDEA代码时,它正在生成一个模型。在
如果存在,如何为相同的模型生成所有可能的模型?在
ex.smt2
文件
(set-logic QF_BV)
(set-info :smt-lib-version 2.0)
(declare-const A0 (_ BitVec 16))
(declare-const A1 (_ BitVec 16))
(declare-const A2 (_ BitVec 16))
(declare-const B0 (_ BitVec 16))
(declare-const B1 (_ BitVec 16))
(declare-const B2 (_ BitVec 16))
(declare-const C0 (_ BitVec 16))
(declare-const C1 (_ BitVec 16))
(declare-const C2 (_ BitVec 16))
(declare-const D0 (_ BitVec 16))
(declare-const D1 (_ BitVec 16))
(declare-const D2 (_ BitVec 16))
(declare-const k11 (_ BitVec 16))
(declare-const k12 (_ BitVec 16))
(declare-const k13 (_ BitVec 16))
(declare-const k14 (_ BitVec 16))
(declare-const k15 (_ BitVec 16))
(declare-const k16 (_ BitVec 16))
(declare-const k21 (_ BitVec 16))
(declare-const k22 (_ BitVec 16))
(declare-const k23 (_ BitVec 16))
(declare-const k24 (_ BitVec 16))
(declare-const k25 (_ BitVec 16))
(declare-const k26 (_ BitVec 16))
(declare-const E11 (_ BitVec 16))
(declare-const E12 (_ BitVec 16))
(declare-const E13 (_ BitVec 16))
(declare-const E21 (_ BitVec 16))
(declare-const E22 (_ BitVec 16))
(declare-const E23 (_ BitVec 16))
(declare-const F11 (_ BitVec 16))
(declare-const F12 (_ BitVec 16))
(declare-const F13 (_ BitVec 16))
(declare-const F21 (_ BitVec 16))
(declare-const F22 (_ BitVec 16))
(declare-const F23 (_ BitVec 16))
(declare-const t11 (_ BitVec 16))
(declare-const t12 (_ BitVec 16))
(declare-const t13 (_ BitVec 16))
(declare-const t14 (_ BitVec 16))
(declare-const t15 (_ BitVec 16))
(declare-const t16 (_ BitVec 16))
(declare-const t21 (_ BitVec 16))
(declare-const t22 (_ BitVec 16))
(declare-const t23 (_ BitVec 16))
(declare-const t24 (_ BitVec 16))
(declare-const t25 (_ BitVec 16))
(declare-const t26 (_ BitVec 16))
;round------ 1 -------
(assert (= t11 (bvmul A0 k11)))
(assert (= t12 (bvadd B0 k12)))
(assert (= t13 (bvadd C0 k13)))
(assert (= t14 (bvmul D0 k14)))
(assert (= E11 (bvxor t11 t13)))
(assert (= F11 (bvxor t12 t14)))
(assert (= E12 (bvmul E11 k15)))
(assert (= F12 (bvadd F11 E12)))
(assert (= E13 (bvadd E12 F13)))
(assert (= F13 (bvmul F12 k16)))
(assert (= A1 (bvxor t11 F13)))
(assert (= t15 (bvxor t12 E13)))
(assert (= B1 t16))
(assert (= t16 (bvxor t13 F13)))
(assert (= C1 t15))
(assert (= D1 (bvxor t14 E13)))
;round------ 2 -------
(assert (= t21 (bvmul A1 k21)))
(assert (= t22 (bvadd B1 k22)))
(assert (= t23 (bvadd C1 k23)))
(assert (= t24 (bvmul D1 k24)))
(assert (= E12 (bvxor t21 t23)))
(assert (= F12 (bvxor t22 t24)))
(assert (= E13 (bvmul E12 k25)))
(assert (= F13 (bvadd F12 E13)))
(assert (= E21 (bvadd E13 F21)))
(assert (= F21 (bvmul F13 k26)))
(assert (= A2 (bvxor t21 F21)))
(assert (= t25 (bvxor t22 E21)))
(assert (= B2 t26))
(assert (= t26 (bvxor t23 F21)))
(assert (= C2 t25))
(assert (= D2 (bvxor t24 E21)))
(assert (= A0 #xb621))
(assert (= B0 #xdf47))
(assert (= C0 #xa779))
(assert (= D0 #xac41))
(check-sat)
(get-value (k11))
(get-value (k12))
(get-value (k13))
(get-value (k14))
(get-value (k15))
(get-value (k16))
(get-value (k21))
(get-value (k22))
(get-value (k23))
(get-value (k24))
(get-value (k25))
(get-value (k26))
(exit)
通常的方法是添加排除第一个模型的新约束。在本例中,如下所示:
没有SMT2命令来获取所有解决方案或解决方案的数量。如果某些东西依赖于某个属性对所有解都有效的事实,我们可以使用量词对其进行编码,例如
^{pr2}$然而,这些类型的问题当然更难解决,Z3将在幕后使用不同的决策程序。在
相关问题 更多 >
编程相关推荐