z3 - 如何使用z3消除表达式中的“not”？

Question

我尝试使用代码来删除表达式中的 not：

(declare-const t Int)

(assert (and (or (>= t 2) (>= t 1)) (not (= t 1))))

(apply ctx-solver-simplify)

我想得到如下结果： t >= 2 但是，结果是：

(goals
(goal
  (>= t 1)
  (not (= t 1))
  :precision precise :depth 1)
)

有人会帮我怎么做吗？

Answer 1

战术simplify有一个选项:eq2ineq。启用后，它将等式t1 = t2转换为t1 <= t2 and t1 >= t2. 应用此策略后，该策略propagate-ineqs将更加有效。

这是一个可以解决问题的脚本： http ://rise4fun.com/Z3/JWit

请注意，这不是通用解决方案。没有任何内置策略完全符合您的要求。