[SOLVED] Is there a parser from Python-Z3 to Z3/smt2?

Is there a parser from Python-Z3 to Z3/smt2?

I am working with the Python API of Z3, because of convenience, but sometimes I need to convert my Python results into readable input for Z3/smt2. For instance, whenever I perform quantifier eliminations, I need to input the result into the other format.

Often it is easy to do it by hand, but sometimes I get large expressions like:

[[Not(y <= x),
  Not(And(x +
          -1*If(y + -1*ext >= 0, y + -1*ext, -1*y + ext) +
          -1*ext <=
          -2,
          Or(If(y + -1*ext >= 0, y + -1*ext, -1*y + ext) >=
             1,
             And(If(y + -1*ext >= 0, y + -1*ext, -1*y + ext) <=
                 0,
                 If(y + -1*ext >= 0, y + -1*ext, -1*y + ext) >=
                 1)))),
  Not(And(x + -1*ext <= -2,
          If(y + -1*ext >= 0, y + -1*ext, -1*y + ext) >= 2))]]

... whereas I would need something like (And(Not...)).

Is there a parser from Python-PY to Z3? I mean: it takes the large solution above (or any other formula) and returns the Z3/smt2 equivalent. As for an example, I want to execute this:

x, y, z = Ints('x y z')

l_1 = (y > x)
l_2 = (z > x)
l_3 = (z >= y)

f_1 = l_1
f_2 = Implies(l_2,l_3)

phi = And([f_1, f_2])


t = Tactic("qe")
phi_s = Goal()
phi_s.add(ForAll([z], phi))
phi_qe = t(phi_s)
print(phi_qe)

... which produces phi_qe = [[Not(y <= x), Not(x + -1*y <= -2)]].

Then, use some parse(phi_qe) (which is what I ask for) and get this: (and (> y x) (> (+ x (- y)) -2)))))

PS: The closest solution I found is Z3Py: Parsing expressions using eval or z3.parse_smt2_string, where they use a function parse_smt2_string for the exact opposite of what I want.

Solution

As mentioned in the comments by @sepp2k, sexpr() is the way to go.

However, I think mixing/matching SMTLib/Z3-Python like this sounds like a bad idea. Unless it's for purely presentation reasons, this'll no doubt create friction between different layers of programming.

Based on your other question I gather these are skolem functions generated by some other mechanism. Perhaps it'd be best to tweak that system to spit out Python? Or, if the generated functions are simple enough, you might want to write a program to do that yourself. That would be a program that can be written any language, that takes these strings and generate simple Python snippets. Skolem functions generated by z3 tend to be simple enough in structure, so this might be a viable alternative.