5 z3
从当前版本开始,"ctx-solver-simplified"中存在一些问题,例如http://rise4fun.com/Z3/CqRv中的 z3给出了错误的答案.我将"ctx-solver-simplified"替换为"简化",如http://rise4fun.com/Z3/x9X4 我想知道,这两种策略"简化"和"ctx-solver-simplified"之间有什么区别？
该策略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的预发布版本