【发布时间】：2012-08-04 13:29:54
【问题描述】：
从当前版本开始，“ctx-solver-simplify”中存在一些问题，如示例中的http://rise4fun.com/Z3/CqRvz3 给出了错误的答案。我将“ctx-solver-simplify”替换为“simplify”，例如http://rise4fun.com/Z3/x9X4 我想知道，这两种策略“简化”和“ctx-solver-simplify”有什么区别？
【问题讨论】：
标签： z3
【发布时间】：2012-08-04 13:29:54
【问题描述】：
策略simplify 只执行“局部简化”。对于每个术语t，我们有simplify(t) 是等效于t 的新术语。此外，simplify(t) 的结果不依赖于t 出现的上下文。根据上下文，我的意思是F 出现t 的断言以及所有其他断言。因为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 的预发布版本
【讨论】：