Export z3py to smtlib ?

[umangm]

Hi, I have a python script in which I have a solver and I add constraints to the solver, I push and I also pop. Is there a way to convert the script to SMTLib format ? I understand that I can use the function Z3_benchmark_to_smtlib_string, but as far as I can see, it does not export the push and pop commands. Is there a way I can do this ?

Below is a sample script

from z3 import *

def ctxToSMT2Benchmark(ctx, status="unknown", name="benchmark", logic=""):
  v = (Ast * 0)()
  return Z3_benchmark_to_smtlib_string(ctx, name, logic, status, "", 0, v, f.as_ast())

a = Int('a')
b = Int('b')
f = And(Or(a > If(b > 0, -b, b) + 1, a <= 0), b > 0)
s = Solver()
s.push()
s.add(f)
s.pop()
print(ctxToSMT2Benchmark(main_ctx().ref(), logic="QF_LIA"))

[NikolajBjorner]

Try the "sexpr()" method that comes with Solver and other objects.

from z3 import *

a = Int('a') b = Int('b') f = And(Or(a > If(b > 0, -b, b) + 1, a <= 0), b > 0) s = Solver() s.push() s.add(f) print(s.sexpr()) s.pop()

[wintersteiger]

No, Z3 does not keep a list of SMT2 commands, it only knows goals and solvers, which contain assertions. Push/pop as well as many other commands (e.g. set-options, tactics, etc) are executed immediately and not kept in any form of history.

Further, note that Z3_benchmark_to_smtlib_string has been removed. This function produced SMT version 1.0 files, which Z3 does not support anymore. (There's a separate function for SMT 2.x.)

[NikolajBjorner]

oh, I didn't read the question in detail. Right, Z3 does not print the commands. There is a low level log facility that can be used for debugging, but that's it.

[NikolajBjorner]

this is now implemented when setting the solver.smtlib2_log="filename.smt2" parameter.