如何以 smt2 格式示例获得 z3 求解器的多个解决方案? [英] how to get multiple solutions for z3 solver in smt2 format example?

问题描述

如何使用 smt2 格式的 z3 求解器为位向量公式生成多个模型?

How to generate multiple models for bit vector formula using z3 solver in smt2 format?

在为位向量实现 IDEA 代码时，它生成了一个模型.

While implementing IDEA Code for Bit Vector it is generating one model.

如果存在，如何为相同的模型生成所有可能的模型?

How to generate all possible models for the same if exists?

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)

推荐答案

通常的方法是添加一个排除第一个模型的新约束.在这个例子中，这看起来像这样:

The usual approach is to add a new constraint that excludes the first model. In this example, this would look like so:

(check-sat)

(assert (and (not (= k16 #x2c7d))  (not (= ... ))
(check-sat)

没有获取所有解决方案或解决方案数量的 SMT2 命令.如果某些事情取决于某些属性适用于所有解决方案的事实，我们可以使用量词对其进行编码，例如

There is no SMT2 command to get all solutions or the number of solutions. If something depends on the fact that some property holds for all solutions, we can encode that using quantifiers, e.g.

(assert (forall ((x (_ BitVec 16))) (... property depending on x ...))) 

然而，这些类型的问题当然更难解决，Z3 将在幕后使用不同的决策程序.

However, those types of problems are of course harder to solve and Z3 will use different decision procedures under the hood.

这篇关于如何以 smt2 格式示例获得 z3 求解器的多个解决方案?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！