0

Java で開発したセキュリティ ツールに Z3 を統合したいと考えています。現在、式を出力してファイルにチェックインし、Z3 を呼び出しています。Java API の安定性についてお尋ねしてもよろしいですか?

Z3で配布しているJava APIの例を見ると、数式を解くには2つの方法があるようです。1 つ目は、ソルバーを作成することです。

Solver solver = ctx.MkSolver();

for (BoolExpr a : g.Formulas())
    solver.Assert(a);

if (solver.Check() != Status.SATISFIABLE)
    throw new TestFailedException();

別の方法は、戦術を使用することです。タクティック「simplify」と「smt」での使用例があります

ApplyResult ar = ApplyTactic(ctx, ctx.MkTactic("simplify"), g);
if (ar.NumSubgoals() == 1
        && (ar.Subgoals()[0].IsDecidedSat() || ar.Subgoals()[0]
                .IsDecidedUnsat()))
    throw new TestFailedException();

私の質問は次のとおりです: z3 を呼び出すより効率的な方法はどれですか? 最初または2番目のもの。そして、どの戦術がどの問題に適していますか? タクティック "smt" は SMT-LIB1 または SMT-LIB2 用ですか?

ありがとう。

4

1 に答える 1

1

Z3 Java API は、次のリリースまで関数/構造体の名前を変更しないという意味で安定しています。もちろん、バグ修正や追加機能があるかもしれません。

ソルバーと戦術のどちらを使用するのがより理にかなっているのかは、アプリケーションによって異なります。ただし、現在ファイルベースのインターフェースを使用しているため、ソルバーベースのインターフェースを使用するだけで十分である可能性があります。これを使用すると、solver.Check() はデフォルトの戦術 (使用されるロジックに依存する場合があります) を使用して問題を解決します。

戦術の詳細については、SMT-LIB ファイル ベースのインターフェイスから目標と戦術を使用する方法を示す戦略チュートリアルを参照してください。同じことが Java API にも当てはまり、タクティックの名前は同じです。「smt」タクティックは、タクティックにラップされた SMT ソルバーです。これは入力言語 (SMT1 または SMT2) に依存せず、ctx.MkSolver() によって構築されたデフォルトの Solver オブジェクトを使用するのと本質的に同じです。

于 2013-10-28T12:44:03.810 に答える