CODEWITHSUNDEEP
z3smtsatsat-solverspysmt
Rituraj Singh
Rituraj Singh

Reputation: 639

Is there way to give input as normal expression to Z3 Solver?

The Z3 input format is an extension of the one defined by SMT-LIB 2.0 standard. The input expressions need to write in prefix form. As for example rise4fun,

x + (y * 2) = 20 needs to be given input in the form of " (= (+ x (* 2 y)) 20)) ".

Z3 supports JAVA API. As for example, let us consider the below code which evaluates and checks satisfiability expressions: x+y = 500 and x + (y * 2) = 20.

final Context ctx = new Context();
final Solver solver = ctx.mkSimpleSolver();

IntExpr x = ctx.mkIntConst("x");
IntExpr y = ctx.mkIntConst("y");
IntExpr th = ctx.mkInt(500); 
IntExpr th1 = ctx.mkInt(2);
IntExpr th2 = ctx.mkInt(20);
BoolExpr t1 = ctx.mkEq(ctx.mkAdd(x,y), th);
BoolExpr t2 = ctx.mkEq(ctx.mkAdd(x,ctx.mkMul(th1, y)), th2);
solver.add(t1);
solver.add(t2);
solver.check()

The problem is if an external user wants to give input to the solver, he cannot give it in the form of the general formula as " x+y = 500, x + (y * 2) = 20 ". The input needs to be parsed and then should be written manually using JAVA API in prefix form (Note BoolExpr t2 in above code) to give the final expressions to Solver.

Is there any parser/library/API (Preferably JAVA or in any other language) which parses the general expressions with arithmetic operators(+, -, <, >, =), propositional logic connectors (And, OR), Quantifiers(ForAll, Exists) and then gives input to the Z3 Solvers ?

Please suggest and help.

Upvotes: 3

Views: 790

Answers (1)

alias
alias

Reputation: 30428

This is precisely why people build high-level interfaces to SMT solvers. There are many choices here for z3:

The goal of these "wrappers" is to precisely save the end-user from all the details of intricate bindings, and provide something much easier and less-error prone to use. On the flip side, they require you to learn yet another library. In my experience, if the host language of your choice has such an implementation, it'd pay off nicely to use it. If not, you should build one!

Upvotes: 3

Related Questions