【发布时间】：2014-02-11 18:53:21
【问题描述】：
将 Z3 中的量词消除应用于线性算术公式 h 后，我得到了一个 30 行左右的公式。事实证明这个公式等价于h2=And(n>2, i>=0, i<=n-2)，我更喜欢它作为输出。
我试过ctx-solver-simplify;我越来越：
And(Not(n <= 2), Or(Not(i >= 1), Not(n + -1*i <= 1)), i >= 0)
现在，Not(n<=2) 可以更简洁地表示为n>=3，Not(n + -1*i <= 1) 表示为n-i>=2，而在这个公式中，i >= 1 是不需要的。
Repeat(Then('nnf','ctx-solver-simplify')) 做得更好（通过摆脱 i>=1）。
有没有更好的简化策略？
同样，有没有一种策略可以将Or(x==0, x==1, x==2, x==3) 转换为And(x>=0,x<=3)？
【问题讨论】：
-
好问题，虽然我不认为内置方法可以做到这一点。 ctx-solver-simplify 方法是更激进的方法之一，它不知道您的意图是获得合取。也许一个想法是简化公式以一组模板为模。您可以提出从模板空间中提取的文字（从公式本身中提取的文字），然后提取连词。
-
不幸的是，预期的公式不一定是连词。在那个特定的例子中，我推测结果应该等同于公式
h2（h来自程序分析问题，我对最终结果应该有一些直觉），我用 Z3（h⇒h2和h2⇒h)，但通常公式可能更复杂。你的想法很有趣，我可以说，推测该公式仅包含几个析取项......
标签： z3