1

Z3 4.1 を使用しており、プログラムで smt lib2 形式の入力を解析したいと考えています。

Z3_parse_smtlib2_fileそのため、最初に Z3 で提供されている例 (フォルダー Z3-4.1/examples/smtlib の下にあります) を解析するために使用を試みます。しかし、多くの解析エラーが見つかり、プログラムがすぐに終了します。入力形式は正しいはずだと思います。次のコードを使用して Z3.2.smt2 を解析しようとしました。

(set-option :auto-config true)
(set-option :produce-models true)

(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)

結果は次のとおりです。

smt2parser_example
(error "line 1 column 26: error setting ':auto-config', option value cannot be modified after initialization")
Error code: 4
BUG: incorrect use of Z3.

API は次のように呼び出されます。

fs = Z3_parse_smtlib2_file(ctx, fname, 0, 0, 0, 0, 0, 0);

問題はどこだ ？入力ファイルは問題ないはずです。問題は Z3_parse_smtlib2_file の引数にありますか?

4

1 に答える 1

1

エラー メッセージで示されているように、Z3 コンテキストが初期化されると、auto-config オプションは変更できません。いくつかのオプションのみが変更可能で、コンテキストが作成された後に変更でき、auto-config はその中にありません。行が

(set-option :auto-config true)

入力ファイルから削除され、正しく解析されます。アプリケーションでオプションを設定する必要がある場合は、config(C++ の場合) またはZ3_config(C の場合) オブジェクトをコンテキスト コンストラクターに渡すなどして、それらをコンテキスト コンストラクターに直接渡すのが最善です。

于 2012-09-27T18:26:04.257 に答える