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。請讓我知道你的想法。