我有涉及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界面可重复性。
是的，Z3可以返回unknown自由量词问题。 以下是主要的原因：
运行时间或内存不足
自由量词片段是不可判定（例如，非线性整数算术）
自由量词片段是太昂贵，和/或在实施Z3的程序是不完整的。
你的问题是在判定片断，和未知是因为在Z3采用非线性算法不完整的过程。 Z3 4.0具有非线性真正的算术一个完整的过程，但它仍然无法与其他理论整合。 因此，它不会在第一个问题有所帮助。
在第一和第二查询行为不同是由于用于每个查询不同的策略。 Z3具有定义自定义策略的新框架。 你可以得到sat用命令的第一个查询
(check-sat-using (then simplify solve-eqs smt))
代替
(check-sat)
第一个命令部队Z3消除通过求解等式（即战术变量solve-eqs ）。 这将消除平等(= c (NUM (* (na) (nb)))) 这个战术在Z3 3.x中的第二个问题自动使用 需要注意的是，如果我们将其替换平等这一战术也无济于事(>= c (NUM (* (na) (nb))))
此外，在第二个问题中只包含非线性算法。 所以，在Z3 4.0，新的（和完整）求解非线性真正的算术将被自动使用。
您可以了解新的战略框架http://rise4fun.com/Z3/tutorial/strategies ， http://rise4fun.com/Z3Py/tutorial/strategies
你的例子是非线性的算术。 Z3 4.0能够解决，只有非线性的算术断言的问题，但不能与未解释的功能和其他理论一起。 这就解释了为什么它会产生unknown的第一个例子。 这种限制很可能在Z3的未来版本中得到解决。
