(错误 "tactic failed: operator not supported, apply simplifier before invoking this strategy" ) 在 Z3 中

Question

我想消除表达式，并使用z3将最终结果转换为cnf，但是，出现了一个错误："（错误"策略失败：不支持运算符，在调用此策略之前应用simplefier"）"脚本中有什么问题？

(set-option :produce-models true)
(declare-var t Real)
(declare-var tc Real)
(declare-var t1 Real)
(declare-var t1c Real)
(assert
   (and 
      (not (and (and (<= 0.0 t)(<= 0.0 t1))(= t1c 2.0)(= tc 1.0)))
      (not (and (and (<= 0.0 t)(<= 0.0 t1))(< 2.0 t1c)(= tc 1.0)))
      (not (and (and (and (<= 0.0 t)(<= 0.0 t1))(< 1.0 tc)) (= t1c 2.0)))
      (not (and (and (and (<= 0.0 t)(<= 0.0 t1))(< 1.0 tc)) (< 2.0 t1c)))
      (or (and (and (and (<= 0.0 t)(<= 0.0 t1))(<= 0.0 t1c))(<= 0.0 tc)(< tc 1.0))
          (and (and (and (<= 0.0 t) (<= 0.0 t1))(<= 0.0 t1c))(< 1.0 tc)(< t1c 2.0))
          (and (and (and (<= 0.0 t)(<= 0.0 t1))(< 1.0 tc)) (= t1c 2.0))
          (and (and (and (<= 0.0 t) (<= 0.0 t1))(<= 0.0 t1c))
               (= tc 1.0)
               (or (and (and (and (<= 0.0 t) (<= 0.0 t1))(<= 0.0 t1c))
                        (< t1c  2.0)
                        (= tc 1.0)
                     )
                   (and (and (<= 0.0 t)(<= 0.0 t1))(= t1c 2.0)(= tc 1.0))
                )
           )
        )
   )
)
(apply (then  ctx-solver-simplify propagate-values  (par-then (repeat (or-else split-clause skip)) propagate-ineqs) tseitin-cnf))

Answer 1

一些策略（例如，tseitin-cnf）假设一些运算符（例如and、distinct…）已被消除。在您的示例中，问题是出现了嵌套在公式中的运算符and。你可以使用策略(! simplify :elim-and true)来消除它。这是更新后的脚本：

(apply (then (! simplify :elim-and true) ctx-solver-simplify propagate-values (par-then (repeat (or-else split-clause skip)) propagate-ineqs) tseitin-cnf))

也就是说，在下一个版本中，我们将使tseitin-cnf等策略更加"用户友好"。也就是说，它将在需要时自动应用所需的转换。