z3 - 假设 'check-sat'不支持 bool 函数吗？

Question

在下面的示例中，我尝试使用未解释的 bool 函数，例如“(declare-const p (Int) Bool)”，而不是针对每个假设使用单个 bool 常量。但它不起作用(它给出了编译错误)。

(set-option :produce-unsat-cores true)
(set-option :produce-models true)

(declare-fun p (Int) Bool) 
             ;(declare-const p1 Bool) 
             ;(declare-const p2 Bool)
             ; (declare-const p3 Bool)

;; We assert (=> p C) to track C using p
(declare-const x Int)
(declare-const y Int)
(assert (=> (p 1) (> x 10)))
;; An Boolean constant may track more than one formula
(assert (=> (p 1) (> y x)))

(assert (=> (p 2) (< y 5)))
(assert (=> (p 3) (> y 0)))

(check-sat (p 1) (p 2) (p 3))
(get-unsat-core)

输出

Z3(18, 16): ERROR: invalid check-sat command, 'not' expected, assumptions must be Boolean literals
Z3(19, 19): ERROR: unsat core is not available

我了解无法(不支持)使用 bool 函数。这背后有什么原因吗？有什么不同的方法吗？

Answer 1

我们有这个限制是因为 Z3 在解决问题之前应用了许多简化。他们中的一些人会重写公式和术语。 Z3 实际解决的问题往往与输入问题大不相同。我们会把简化的假设追溯到原始假设，或者引入辅助变量。限制为 bool 文字避免了这个问题，并使界面非常干净。请注意，此限制并不限制表达能力。如果您认为声明许多 bool 变量来跟踪不同的断言太烦人。我建议您看一下 Z3 的新 Python 前端，称为 Z3Py。使用起来比SMT 2.0方便多了。这是您在 Z3Py 中的示例:http://rise4fun.com/Z3Py/cL在这个例子中，不是创建一个未解释的谓词 p，而是创建一个“向量”(实际上，它是一个 Python 列表)o bool 常量。

Z3Py online tutorial包含许多示例。

也可以在 Z3Py 中实现创建辅助变量的方法。这是执行此操作的脚本。我定义了一个函数 check_ext 来完成所有的管道工作。 http://rise4fun.com/Z3Py/B4