3

我有一些简单的约束，涉及 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 界面中重现。

4

2 回答 2

8

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

  • 时间或内存不足

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

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

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

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

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

代替

(check-sat)

第一个命令强制 Z3 通过求解等式（即 tactic 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 了解新的策略框架

于 2012-06-25T21:19:29.633 回答
2

你的例子是非线性算术。Z3 4.0 只能解决非线性算术断言的问题，但不能解决未解释的函数和其他理论。这就解释了为什么它unknown在第一个示例中产生。这个限制可能会在 Z3 的未来版本中得到解决。

于 2012-06-25T21:19:27.453 回答