我有一些简单的约束,涉及生成的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,但这也可以在网络界面中重现.
是的,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