z3py 表达式简化

Question

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

有人可以将我链接到有关可用策略的详细文档吗？ 网上的python教程还不够。

或者有人可以推荐一个更好的方法来完成这个。

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

x < 5, x < 4, x < 3, x = 1我希望将其简化为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

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