1

我有一组可以满足的断言给 z3。当我调用时(check-sat)，z3 返回sat。然后我调用(get-model)并查看特定变量的定义%%P2_*_143。它看起来像这样：

(define-fun %%P2_*_143 () JS (NUM 2.0))

如果我采用这个定义，把它变成断言

(assert (= %%P2_*_143 (NUM 2.0)))

再次调用(check-sat)，z3 返回unsat. 此外，如果我再调用(get-unsat-core)， z3 会返回()。

我的理解是 z3 生成的模型对所有变量都给出了令人满意的赋值，因此断言赋值也应该是可满足的。这是不正确的，还是我在其他地方有错误？

整个断言集都在这个要点中：https ://gist.github.com/2966738 。添加的断言位于最底部。

我在 Mac OS X 10.7.4 上使用 Z3 版本 3.2。我还能够使用http://rise4fun.com/z3上的在线界面重现此行为。

4

1 回答 1

1

几天前报告了一个类似的错误。线性实数算术包中的模型构造存在错误。该错误已得到修复。Z3 使用无穷小来处理严格的不等式，详细信息在以下论文中进行了描述：http ://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf

请注意，该错误不会影响求解器的健全性。也就是说，sat/unsat 答案是正确的。但是，模型不是。您示例中的第二个查询未满足，因为模型不正确。如果你需要，我可以提供一个新的二进制文件来解决这个问题。同时，您可以通过在脚本中添加以下命令来解决该错误：

(declare-fun delta () Real)
(assert (< 0.0000001 delta))
(assert (< delta 0.0000002))
于 2012-06-21T18:23:23.993 回答