z3 为没有量词的断言产生未知数

Question

我有一些简单的约束，涉及 z3 中产生 unknown 的实数乘法。问题似乎是它们被包装在数据类型中，因为未包装的版本会产生 sat。

这是一个简化的案例:

(declare-datatypes () ((T (NUM (n Real)))))

(declare-const a T)
(declare-const b T)
(declare-const c T)

(assert (is-NUM a))
(assert (is-NUM b))
(assert (is-NUM c))

(assert (= c (NUM (* (n a) (n b)))))

(check-sat)
;unknown

并且没有数据类型:

(declare-const a Real)
(declare-const b Real)
(declare-const c Real)

(assert (= c (* a b)))

(check-sat)
;sat

我使用的是 z3 3.2，但这也可以在 Web 界面中重现。

Answer 1

是的，Z3 可以在无量词问题中返回 unknown。以下是主要原因:

• 时间或内存不足

• 无量词片段是不可判定的(例如，非线性整数算术)

• 无量词片段太昂贵，和/或在 Z3 中实现的过程不完整。

您的问题存在于可判定的片段中，而未知数是由于 Z3 中使用的非线性算术程序不完整。 Z3 4.0 具有完整的非线性实数运算程序，但仍未与其他理论相结合。所以，它对第一个问题没有帮助。

第一个和第二个查询的行为不同是由于每个查询使用的策略不同。 Z3 有一个用于定义自定义策略的新框架。您可以使用命令获取第一个查询的 sat

(check-sat-using (then simplify solve-eqs smt))

而不是

(check-sat)

第一个命令强制 Z3 通过求解等式来消除变量(即策略 solve-eqs)。它将消除相等性 (= c (NUM (* (n a) (n b))))。 Z3 3.x 中的第二个问题自动使用了这种策略。请注意，如果我们用 (>= c (NUM (* (n a) (n b)))) 替换等式，这种策略将无济于事。

此外，第二个问题只包含非线性算术。因此，在 Z3 4.0 中，将自动使用新的(完整的)非线性实数算术求解器。

您可以在 http://rise4fun.com/Z3/tutorial/strategies 了解新的战略框架, http://rise4fun.com/Z3Py/tutorial/strategies