z3py表达式简化

Question

我正在尝试使用z3py简化表达式，但找不到任何关于不同策略的文档。我找到的最好的资源是一个stack overflow question，它按名称列出了所有的战术。

有没有人能把我链接到关于可用战术的详细文档？在线python教程是不够的。

或者有人可以推荐一种更好的方法来实现这一点。

问题的一个例子是这样的表达式：

我希望这可以简化到x = 1。

在这个例子中，使用unit-subsume-simplify出现的策略是可行的。

但是，当我尝试更复杂的示例时，比如x > 1, x < 5, x != 3, x != 4，我得到的结果是x > 1, x < 5, x ≠ 3, x ≠ 4。当我喜欢x = 2的时候。

使用z3py实现这类简化的最佳方法是什么？

My current solution。

谢谢，马特

Answer 1

可能的解决方案：

x = Int('x')
s = Solver()
s.add(x < 5, x < 4, x < 3, x == 1)
print s.check()
m = s.model()
print m
s1 = Solver()
s1.add(x > 1, x < 5, x != 3, x != 4)
print s1.check()
m1 = s1.model()
print m1

输出：

sat
[x = 1]
sat
[x = 2]

联机运行此解决方案here

Answer 2

Reduce的Redlog示例。请让我知道你的想法。

​

​