2

我从https://git01.codeplex.com/z3 (89c1785b)ctx-solver-simplify的 master 分支中看到了相当令人惊讶的行为，其中 z3.And() 的参数顺序似乎很重要：

#!/usr/bin/python
import z3

a, b = z3.Bools('a b')
p = z3.Not(a)
q = z3.Or(a, b)
for e in z3.And(p, q), z3.And(q, p):
  print e, '->', z3.Tactic('ctx-solver-simplify')(e)

产生：

And(Not(a), Or(a, b)) -> [[Not(a), Or(a, b)]]
And(Or(a, b), Not(a)) -> [[b, Not(a)]]

这是Z3的错误吗？

4

2 回答 2

2

不，这不是错误。这种策略ctx-solver-simplify非常昂贵并且本质上是不对称的。也就是说，访问子公式的顺序会影响最终结果。这个策略在文件中实现src/smt/tactic/ctx_solver_simplify_tactic.cpp。代码可读性很强。请注意，它使用“SMT”求解器 ( )，并在遍历输入公式时m_solver进行多次调用。m_solver.check()这些调用中的每一个都可能非常昂贵。对于特定的问题域，我们可以实施这种策略的一个版本，它甚至更昂贵，并避免您的问题中描述的不对称性。

编辑：

你也可以考虑战术ctx-simplify，它比 便宜ctx-solver-simplify，但它是对称的。该策略ctx-simplify基本上将应用以下规则：

A \/ F[A] ==> A \/ F[false]
x != c \/ F[x] ==> F[c]

哪里F[A]是一个可能包含的公式A。它比它更便宜，ctx-solver-simplify因为它在遍历公式时不调用 SMT 求解器。这是使用此策略的示例（也可在线获得）：

a, b = Bools('a b')
p = Not(a)
q = Or(a, b)
c = Bool('c')
t = Then('simplify', 'propagate-values', 'ctx-simplify')
for e in Or(c, And(p, q)), Or(c, And(q, p)):
  print e, '->', t(e)

关于人类可读性，在实施任何策略时，这从来都不是目标。请告诉我们上述策略是否不足以满足您的目的。

于 2012-11-29T07:54:51.197 回答
2

我认为编写自定义策略会更好，因为当您本质上要求规范性时还有其他权衡。Z3 没有任何将公式转换为规范形式的策略。因此，如果您想要始终为等效的公式产生相同答案的东西，则必须编写一个新的规范化器来确保这一点。

The ctx_solver_simplify_tactic furthermore makes some tradeoffs when simplifying formulas: it avoids simplifying the same sub-formula multiple times. If it did, it could increase the size of the resulting formula significantly (exponentially).

于 2012-11-29T16:18:24.983 回答