z3 - z3 中的简化含义

Question

是否可以使用 z3 来简化这个表达式

对这个

? 如果是，我们应该如何实现它？

Answer 1

这两个表达式不等价。特别是第一个公式意味着 t_FC < 1。您可以使用称为 ctx-solver-simplify 的策略来简化像您这样的公式，以利用 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 接口的上下文中）