2

のような制約が(t>=0 or t>=1)あり(t<=2 or t>=2)ます。実際、制約は " t>=0"に簡略化できます。z3を使用して、z3を使用してCNF形式で簡略化された結果を取得するにはどうすればよいですか？

(declare-const t Int)                                                                                  
(assert (and 
            (or
               (>= t 0)
               (>= t 1)
            )
            (or
                (>= t 2)
                 (<= t 2)
            )
            (>= t 0)
            (<= t 1)
        )
)                                                                                         
(apply (par-then (! simplify :elim-and true) tseitin-cnf))

ただし、スクリプトは機能しません。

4

1 に答える 1

3

このsimplifyタクティックは「局所的な単純化」のみを実行します。つまり、式 を簡略化する場合t、 のコンテキストは無視されますt。たとえば、 に簡略化できますが、 には簡略化a + 1 - aできませ1ん。コンテキストの単純化はコストがかかりますが、戦術は効率的かつ単純であることを意図しています。他の戦術を使用して、目的を達成することができます。a != 0 or b = a + 1a != 0 or b = 1simplify

戦術propagate-ineqsは不平等を広めます。ただし、式にネストされた項は処理されません。この戦術split-clauseを使用して、ケース\ゴールの式を破ることができます。タクティックpropagate-valuesはアサーションの値を伝播します。例:a = 0 and b >= aは に簡略化されa = 0 and b >= 0ます。

このコマンド(help-tactic)は、利用可能なすべての戦術を表示します。

これは、例を に単純化するための戦略ですt >= 0 and t <= 1。

(apply (then simplify propagate-values split-clause propagate-ineqs))

par-thenコンビネータは、多くのサブゴールを生成する戦術を組み合わせる場合にのみ役立つ ことに注意してください。は入力ゴールに適用(par-then t1 t2)され、 によって生成されたすべてのサブゴールに (並行して)適用されます。この戦術は、複数のサブゴールを生成します。次に（より大きな例の場合）使用する方が効率的かもしれません：t1t2t1split-clause

(apply (then simplify propagate-values (par-then split-clause propagate-ineqs)))
于 2012-07-15T16:54:36.683 に答える