有从Python-Z3到Z3/smt2的解析器吗？

Question

为了方便起见，我正在使用 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))]]

...而我需要类似

(And(Not...))

的东西。

有从Python-PY到Z3的解析器吗？我的意思是：它采用上面的大解决方案（或任何其他公式）并返回 Z3/smt2 等效值。举个例子，我想执行这个：

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)

（这就是我所要求的）并得到这个：

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

PS：我找到的最接近的解决方案是Z3Py：使用 eval 或 z3.parse_smt2_string 解析表达式，其中他们使用函数

parse_smt2_string

与我想要的完全相反。

Answer 1

正如@sepp2k 的评论中提到的，

sexpr()

是正确的选择。

但是，我认为像这样混合/匹配 SMTLib/Z3-Python 听起来是个坏主意。除非纯粹是出于演示原因，否则这无疑会在不同编程层之间产生摩擦。

根据您的其他问题，我收集这些是由其他机制生成的 skolem 函数；也许最好调整该系统以输出 Python？或者，如果生成的函数足够简单，您可能想自己编写一个程序来执行此操作。这将是一个可以用任何语言编写的程序，它接受这些字符串并生成简单的 Python 片段。 z3 生成的 Skolem 函数在结构上往往足够简单，因此这可能是一个可行的替代方案。