入力ファイルにZ3を起動する方法

Question

私が入ったファイルがあります：

(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を正しく呼び出す方法を教えてもらえますか？

よろしくお願いいたします。

Answer 1

多くの入力フォーマットに対応しています。ファイル拡張子を使用して、どのパーサーが使用されるかを推測します。拡張子が.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)