3

式を削除し、z3 を使用して最終結果を cnf に変換したいのですが、"(error "tactic failed: operator not supported, apply simplifier before invoking this strategy")" というエラーが発生します。スクリプトの問題は何ですか?

(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を前提としています。あなたの例では、問題は数式内にネストされた演算子の発生です。戦術を使用してそれを排除できます。更新されたスクリプトは次のとおりです。anddistinctand(! 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 に答える