z3中的"simplify“和"ctx-solver-simplify”有什么区别？

Question

从当前版本开始，在“ctx-solver-simplify”中存在一些问题，例如http://rise4fun.com/Z3/CqRv z3给出了错误的答案。我把"ctx-solver-simplify“换成了"simplify”，就像http://rise4fun.com/Z3/x9X4一样我在想，这两种策略"simplify“和"ctx-solver-simplify”有什么区别？

Answer 1

策略simplify只执行“局部简化”。对于每个术语t，我们都认为simplify(t)是一个新术语，等同于t。此外，simplify(t)的结果不依赖于发生t的上下文。通过上下文，我指的是发生t的断言F和所有其他断言。因为，simplify是本地的，所以它非常高效。实现本质上是基于自下而上的简化规则的应用。此外，由于simplify(t)的结果不依赖于上下文信息，因此我们可以缓存它。因此，即使t在公式F中出现N次，我们也只需要简化它一次。Z3中的所有内置求解器都应用了这种简化。因此，像simplify这样的策略已经经过了广泛的测试。

策略ctx-solver-simplify使用t发生的上下文来应用简化。基本思想是通过使用求解器S遍历公式求解器来简化公式F。求解器上下文实际上包含“S”。只要S.check()返回unsat，我们就知道当前的上下文不一致，那么我们就可以用false替换当前的公式。ctx-solver-simplify的价格要贵得多。首先，它执行许多对S.check()的调用。这些调用中的每一个都可能非常昂贵。缓存中间结果也要困难得多。Z3可能需要多次简化子公式t，因为它出现在不同的上下文中。

您在问题中报告的错误已修复。该修复将在下一个版本(4.1版)中提供。如果您需要，我们可以为您提供Z3 4.1的预发布版本