1

.NETAPIで作成された既存のZ34.1コンテキストがあり、多くの関数宣言、ソート宣言、仮定がアサートされています。

このコンテキストで既存のすべての宣言を使用してSMT-LIB2文字列を解析する最もクリーンな方法は何ですか？具体的には、コンテキスト内のすべての宣言を繰り返す方法はありますか？宣言にアクセスできるようにするメソッドがContextに表示されませんでした。

現在、私は次のことを行っています。

Context z3 = new Context();

// ... declare sorts, add declarations (parsing other input files), add assertions, to z3 context

List<FuncDecl> decls = new List<FuncDecl>();
List<Symbol> names = new List<Symbol>();
string pstr; // smtlib2 string to be parsed populated elsewhere

// ... populate decls and names by iterating over my internal data structures with references to these declarations

BoolExpr prop = z3.ParseSMTLIB2String(pstr, null, null, names.ToArray(), decls.ToArray());

これらすべての宣言とシンボル名をz3コンテキスト自体から取得する方法はありますか？それらはすべて、z3オブジェクトですでに宣言されています。内部データ構造を反復処理するよりも、この方法で実行したいと思います。

私はそれを見逃したかもしれませんが、APIでこれを行うことができるものは何も見つかりませんでした。Solver.Assertionsを介して利用できるアサートされた数式の配列に似たものをイメージしています。

4

1 に答える 1

1

あなたのソリューションは正しいようです。宣言と名前は、呼び出しごとに再構築するのではなく、最初に発生したときに収集できます。これにより、呼び出しごとに内部データ構造を反復する必要がなくなります。Z3 に対して多くの呼び出しを行っている場合、SMT パーサーの使用は最も効率的な解決策ではない可能性があることに注意してください。可能であれば、文字列の代わりに Z3 式を直接作成することをお勧めします (この場合、シンボルのテーブルも必要になる可能性があります)。

于 2012-10-26T10:19:25.330 に答える