z3 为没有量词的断言产生未知数 [英] z3 produces unknown for assertions without quantifiers

问题描述

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

I have some simple constraints involving multiplication of reals in z3 that are producing unknown. The problem seems to be that they are wrapped in a datatype, as the unwrapped version produces 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 界面中重现.

I'm using z3 3.2, but this also is reproducible in the web interface.

推荐答案

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

Yes, Z3 can return unknown in quantifier-free problems. Here are the main reasons:

• 时间或内存不足

• Run out of time or memory

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

The quantifier-free fragment is undecidable (e.g., nonlinear integer arithmetic)

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

The quantifier-free fragment is too expensive, and/or the procedure implemented in Z3 is incomplete.

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

Your problems are in a decidable fragment, and the unknown is due to the incomplete procedure for nonlinear arithmetic used in Z3. Z3 4.0 has a complete procedure for nonlinear real arithmetic, but it is still not integrated with the other theories. So, it will not help in the first problem.

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

The different in behavior in the first and second queries is due to different strategies used for each query. Z3 has a new framework for defining custom strategies. You can get sat for the first query by using the command

(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))))，这种策略将无济于事.

The first command forces Z3 to eliminate variables by solving equalities (i.e., tactic solve-eqs). It will eliminate the equality (= c (NUM (* (n a) (n b)))). This tactic is automatically used in the second problem in Z3 3.x. Note that this tactic will not help if we replace the equality with (>= c (NUM (* (n a) (n b)))).

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

Moreover, the second problem contains only nonlinear arithmetic. So, in Z3 4.0, the new (and complete) solver for nonlinear real arithmetic will be automatically used.

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

这篇关于z3 为没有量词的断言产生未知数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！