簡化在Z3的含義

Question

是否有可能使用Z3該表達式

簡化這一個

？如果是，我們應該如何實現它？

Answer 1

這兩個表達式不等價。特別地，第一公式意味着t_FC < 1. 可以使用一種稱爲策略CTX-求解器簡化，以簡化公式像你以利用上下文限制，例如t_FC < 1.

你的例子的編碼是於：http://rise4fun.com/Z3Py/xCN2

tFb, tFc, tFt = Reals('tFb tFc tFt') 

g = Goal() 
g.add(And([Not(tFb >= 1), 
    Implies(tFb <= 1, tFb + tFc <= 5), 
    Implies(tFb <= 1, tFb + tFc + tFt <= 5), 
    Implies(tFb <= 1, tFb + tFc + tFt <= 5), 
    ])) 

print g 
print Tactic('ctx-solver-simplify')(g) 

結果是：

¬(tFb ≥ 1), tFb + tFc ≤ 5, tFb ≤ 1 ⇒ tFb + tFc + tFt ≤ 5 

教程http://rise4fun.com/Z3Py/tutorial/strategies解釋了使用策略從Z3（在Python INT的上下文erface）