是否存在Python-Z3到Z3/smt2的表达式转换工具？

我正在用Z3的Python API开发，虽然提升了开发效率，但有时需要把Python执行的结果转换成Z3/SMT2可读的输入格式，比如执行量词消去操作后就需要做这种转换。

手动转换简单表达式还算容易，但碰到下面这种复杂表达式就特别繁琐：

[[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))]]

我需要的是从Z3Py表达式到SMT-LIB2格式的转换工具：输入任意Z3Py公式（比如上面的复杂表达式），返回对应的等价SMT-LIB2格式字符串。

举个具体例子，执行以下Z3Py代码：

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)

得到的结果是phi_qe = [[Not(y <= x), Not(x + -1*y <= -2)]]，我希望通过类似parse(phi_qe)的工具，得到对应的SMT-LIB2格式：

(and (> y x) (> (+ x (- y)) -2))

注：我找到过一个接近的方案，但其中的parse_smt2_string功能和我的需求完全相反——它是把SMT-LIB2字符串转成Z3Py表达式，而我需要的是反向转换。

内容的提问来源于stack exchange，提问作者Theo Deep