使用量词时从Z3模型中提取布尔项

Question

我试图使用Z3来探索两个谓词之间的差异，但是模型包含exist-表达式，我期望布尔常量。

我在smtlib中有以下程序:

(set-option :produce-models true)
(declare-fun a (Int) Bool)
(declare-const t1 Bool)
(declare-const t2 Bool)
(assert (= t1 (exists ((i Int)) (and (a i) (or (= i 10) (= i 11) )))))
(assert (= t2 (exists ((i Int)) (and (a i) (and (< i 13) (< 9 i))))))
(assert (distinct t1 t2))
(check-sat)
(get-value (a))
(get-value (t1 t2))

我试图找到t1和t2的值，当问题是可满足的。

Z3响应

sat
((a (store (store ((as const Array) true) 11 false) 10 false)))
((t1 (exists ((i Int)) (and (not (= i 10)) (not (= i 11)) (or (= i 10) (= i 11)))))
(t2 (exists ((i Int))
(and (not (= i 10)) (not (= i 11)) (not (<= 13 i)) (not (<= i 9))))))

t1和t2的模型没有给我布尔常数，而是表达式。我怎样才能说服Z3给出这些表达式的值呢?(我相信t1的模型实际上是一个矛盾，所以它总是假的。

我不需要通过smtlib来做这个，使用Z3 api就足够了。

Answer 1

您只能获得顶级值的值。一个简单的exist(即，一个没有嵌套的)相当于一个顶级声明。(也有一些方法可以通过skolemization来处理嵌套存在，但这不是重点。)因此，只需将这些存在的变量拉到顶部:

(set-option :produce-models true)
(declare-fun a (Int) Bool)
(declare-const t1 Bool)
(declare-const t2 Bool)
(declare-const i1 Int)
(declare-const i2 Int)
(assert (= t1 (and (a i1) (or (= i1 10) (= i1 11) ))))
(assert (= t2 (and (a i2) (and (< i2 13) (< 9 i2)))))
(assert (distinct t1 t2))
(check-sat)
(get-value (a))
(get-value (i1 i2))
(get-value (t1 t2))

这个打印:

sat
((a (store ((as const Array) true) 12 false)))
((i1 10)
(i2 12))
((t1 true)
(t2 false))

我相信这满足了您所有的约束，并为您提供了t1和t2的值，以及i1和i2，使它们根据要求不同。