ctx-solver-simplify中的非对称行为

Question

我看到了来自ctx-solver-simplify的相当令人惊讶的行为，其中Z3和()的参数顺序似乎很重要，使用来自https://git01.codeplex.com/z3主分支的最新版本的Z3 (89c1785b)：

#!/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中的错误吗？

Answer 1

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

编辑：

你也可以考虑策略ctx-simplify，它比ctx-solver-simplify便宜，但它是对称的。such ctx-simplify实质上将应用如下规则：

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

其中，F[A]是可能包含A的公式。它比ctx-solver-simplify更便宜，因为它在遍历公式时不会调用SMT求解器。下面是一个使用此策略的示例(也可以使用online)：

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)

关于人的可读性，这从来不是实现任何策略时的目标。如果上面的策略对你的目的不够好，请告诉我们。

Answer 2

我认为编写一个自定义的策略会更好，因为当你本质上要求规范时，还有其他的权衡。Z3没有任何将公式转换为规范形式的策略。因此，如果你想要对基本等价的公式总是产生相同的答案，你必须编写一个新的规范化程序来确保这一点。

此外，ctx_solver_simplify_tactic在简化公式时进行了一些权衡:它避免多次简化相同的子公式。如果是这样的话，它可能会显著增加结果公式的大小(指数级)。