z3 - z3中 "simplify"和 "ctx-solver-simplify"有什么区别

Question

从当前版本开始，“ctx-solver-simplify”中存在一些问题，例如在示例http://rise4fun.com/Z3/CqRv z3中给出了错误的答案。我像http://rise4fun.com/Z3/x9X4一样将“ctx-solver-simplify”替换为“simplify”
我想知道，这两种策略“简化”和“ctx-求解器-简化”有什么区别？

Answer 1

战术simplify仅执行“本地简化”。对于每个术语t，我们都知道simplify(t)是一个等同于t的新术语。此外，simplify(t)的结果不取决于t发生的上下文。在上下文中，我的意思是断言F(发生t的地方)和所有其他断言。由于simplify是本地的，因此非常有效。该实现实质上基于简化规则的自下而上的应用。而且，由于simplify(t)的结果不依赖于上下文信息，因此我们可以对其进行缓存。因此，即使t在公式N中出现F次，我们也只需将其简化一次。 Z3中的所有内置求解器均采用这种简化方式。因此，诸如simplify之类的策略已被广泛测试。

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

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