3

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

(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))
4

1 回答 1

2

一些策略（例如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更“用户友好”之类的策略。也就是说，它会在需要时自动应用所需的转换。

于 2012-08-04T17:32:54.200 回答