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

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

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

来源

2012-11-29 user1861926

不，这不是一个错误。战术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解算器。下面是一个使用这种战术（也可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)

关于humand可读性，执行任何战术的时候，这是从来没有一个进球。请告诉我们，上述策略是否不足以达到您的目的。

来源

2012-11-29 07:54:51

谢谢！如果我想生成一个公式的简洁易读的版本，并且计算时间不那么重要，那么我是否可以在Z3中调用API或策略来“更加努力”来简化表达式？或者我需要修改ctx_solver_simplify_tactic.cpp /写我自己的战术？ – user1861926

事实上，'propagate-values'对我有很大帮助 - 再次感谢！ – user1861926

我认为写一个自定义策略会更好，因为当你基本上要求正规性时，还有其他的折衷。 Z3没有任何将公式转换为规范形式的策略。所以，如果你想要的东西总是产生相同的答案公式是地面等值，你将不得不写一个新的规范，确保这一点。

在简化公式时，ctx_solver_simplify_tactic还会进行一些折衷：它避免了多次简化相同的子公式。如果是这样，它可能会显着增加结果公式的大小（按指数规律）。

来源

2012-11-29 16:18:24

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

回答

相关问题