2

以下を含むファイルがあります。

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Real)
(declare-const e Real)
(assert (> a (+ b 2)))
(assert (= a (+ (* 2 c) 10)))
(assert (<= (+ c b) 1000))
(assert (>= d e))
(check-sat)
(get-model)

オンライン チュートリアルによると、このファイルに対して z3 を実行すると、次のように返されます。

sat
(model
    (define-fun c () Int
        (- 5))
    (define-fun a () Int
        0)
    (define-fun b () Int
        (- 3))
    (define-fun d ()
        Real 0.0)
    (define-fun e ()
        Real 0.0)
)

だから私はこれが正当な Z3 入力であることを知っています。ただし、「z3 [option]」を実行すると、選択したオプションに関係なく、エラーメッセージが表示されるだけです。エラーメッセージはありません。入力ファイルで Z3 を正しく呼び出す方法を教えてもらえますか?

よろしく。

4

1 に答える 1

5

Z3 は多くの入力フォーマットをサポートしています。ファイル拡張子を使用して、使用されるパーサーを推測します。拡張子が.smt2. SMT 2.0 パーサーを使用します。使用するパーサーを指定することもできます。このオプション-smt2は、Z3 に SMT 2.0 パーサーの使用を強制します。最後に、Z3 はデフォルトでモデル構築を有効にしません。したがって、オプションを使用するか、スクリプトの先頭にMODEL=trueコマンドを追加する必要があります。(set-option :produce-models true)

非常に古いバージョンの Z3 を使用する場合は、SMT 1.0 フォーマットを使用する必要があります。この形式については、http: //goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.30.pdfで説明されています。

そうは言っても、アップグレードすることを強くお勧めします。SMT 1.0 はあまりユーザーフレンドリーではなく、SMT のほとんどのドキュメント/チュートリアルは SMT 2.0 形式になっています。

この形式の例を次に示します。

(benchmark file
  :extrafuns ((a Int) (b Int) (c Int) (d Real) (e Real))
  :assumption (> a (+ b 2))
  :assumption (= a (+ (* 2 c) 10))
  :assumption (<= (+ c b) 1000)
  :assumption (>= d e)
  :formula true)
于 2012-01-22T03:08:25.403 に答える