由于当前版本，“ctx-solver-simplify”中存在一些问题，如示例http://rise4fun.com/Z3/CqRv z3 给出了错误的答案。我将“ctx-solver-simplify”替换为“simplify”，如http://rise4fun.com/Z3/x9X4 我想知道，这两种策略“simplify”和“ctx-solver-simplify”有什么区别？
user1487718
问问题
2029 次
1 回答
7
该策略simplify仅执行“局部简化”。对于每个术语t，我们都有simplify(t)一个新术语，相当于t。此外，结果simplify(t)不取决于t发生的上下文。就上下文而言，我指的是发生位置的断言F和t所有其他断言。由于simplify是本地的，因此非常有效。该实现基本上基于简化规则的自下而上应用。此外，由于结果simplify(t)不依赖于上下文信息，我们可以缓存它。因此，即使公式中t出现多次，我们也只需简化一次。Z3 中的所有内置求解器都应用了这种简化。因此，诸如NFsimplify已经过广泛的测试。
该策略ctx-solver-simplify使用t发生的上下文来应用简化。F基本思想是通过使用求解器遍历公式来简化公式S。求解器S本质上包含“上下文”。每当S.check()返回时unsat，我们知道当前上下文不一致，那么我们可以将当前公式替换为false。ctx-solver-simplify贵很多。首先，它对S.check(). 这些调用中的每一个都可能非常昂贵。缓存中间结果也更加困难。Z3 可能不得不t多次简化子公式，因为它出现在不同的上下文中。
您在问题中报告的错误已得到修复。该修复程序将在下一个版本（4.1 版）中提供。如果您需要，我们可以为您提供 Z3 4.1 的预发布版本
于 2012-08-04T17:54:38.403 回答