CODEWITHSUNDEEP
javaz3
sean
sean

Reputation: 1832

How to call Z3 properly from Java program?

I want to integrate Z3 to my security tool developed in Java. At the moment, I'm outputting the formula to check into a file, and then call Z3. May I ask how stable the Java API is?

When I look at the Java API example distributed with Z3, it seems there are two ways to solve a formula. The first one is to create a solver:

Solver solver = ctx.MkSolver();

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

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

Another way is to use Tactic. There are examples of using with tactic "simplify" and "smt"

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

My question is: which is the more efficient way to call z3? the first or the second one. And which tactic is good for which problem? And the tactic "smt" is for SMT-LIB1 or SMT-LIB2?

Thanks.

Upvotes: 0

Views: 2039

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

The Z3 Java API is stable in the sense that it will not change any function/structure names until the next release. There may of course be bugfixes and perhaps some added functionality.

Whether it makes more sense to use solvers or tactics entirely depends on the application. However, since you currently use the file-based interface, using the solver-based interface is likely to be sufficient. When this is used, solver.Check() will use a default tactic (which may depend on the logic used) to solve problems.

For more information about tactics, please see the strategies tutorial, which shows how to use goals and tactics from the SMT-LIB file based interface. The same applies for the Java API, and the names of tactics are the same. The "smt" tactic is the SMT solver wrapped in a tactic; this is independent of the input language (SMT1 or SMT2), and is essentially the same as using the default Solver object constructed via ctx.MkSolver().

Upvotes: 1

Related Questions