2

Z3バージョン2.18を使用して、次のような式を単純化しようとしています。

  • （および（>（-（-x 1）1）0）（> x 0））
  • （または（>（-（-x 1）1）0）（> x 0））

（> x 2）および（> x 0）のようなものを取得したいと考えています。

次の入力ファイルを使用してZ3を実行しています。ここで、Fは上記の式の1つです。

(set-option set-param "STRONG_CONTEXT_SIMPLIFIER" "true")
(declare-const x Int)
(simplify F)

これは、次の出力が得られる論理和でうまく機能します。

(let (($x35 (<= x 0)))
(not $x35))

ただし、接続詞を使用すると、次のようになります。

(not (or (<= x 0) (<= x 2)))

Z3に上記の式をさらに単純化するように強制する方法はありますか？取得できるといいのですが(not (<= x 2))。

PS：Z3にその出力をインライン化させる方法はありますか（つまり、(not (<= x 0))の代わりに持つ(let (($x35 (<= x 0))) (not $x35))）

ありがとう、ガス

4

1 に答える 1

1

いいえ、Z32.xではそれを行うことはできません。

Z3 3.xには、新しい（完全に準拠した）SMT2.0フロントエンドがあります。Z3 3.xには、戦術と戦術に基づく「戦略仕様言語」などのいくつかの新機能があります。それが進行中であるので、私はまだそれを「宣伝」していません。基本的な考え方は、このスライドデッキで説明されています。この言語は、あなたがやりたいことをするために使うことができます。あなたはただ書く必要があります：

(declare-const x Int)
(assert (not (or (<= x 0) (<= x 2))))
(apply (and-then simplify propagate-bounds))

次のコマンドを使用して、使用可能なすべての戦術を見つけることができます。

(help-strategy)
(help apply)
(help check-sat-using)
于 2011-09-26T14:41:38.217 に答える