z3py：从z3公式中检索分支条件

Question

假设我有一个像这样的z3py程序：

import z3


a = z3.Int("a")
input_0 = z3.Int("input_0")
output = z3.Int("output")

some_formula = z3.If(a < input_0, 1, z3.If(a > 1, 4, 2))

s = z3.Solver()

s.add(output == some_formula)

s.check()
m = s.model()
print(m)

我是否有一种优雅的方法可以从some_formula中检索分支条件？因此，获取诸如[a < input_0, a > 1]的列表。它适用于if表达式的任意深度嵌套。

我知道有一些使用多维数据集的方法，但是我不能检索两个以上的多维数据集表达式。我不确定如何配置求解器。

Answer 1

您可以使用以下命令打印多维数据集：

for cube in s.cube():
    print cube

但是这不会真正帮助您。对于您的示例，它打印：

[If(a + -1*input_0 >= 0, If(a <= 1, 2, 4), 1) == 1]
[Not(If(a + -1*input_0 >= 0, If(a <= 1, 2, 4), 1) == 1)]

这与您所寻找的不完全相同。

解决问题的最简单方法是直接自己走公式的AST，并在遍历表达式时抓住条件。当然，Z3 AST是一个多毛的对象（双关语！），因此这将需要大量编程。但是，通读此文件中的构造函数（If，Var等）可以使您入门：https://z3prover.github.io/api/html/z3py_8py_source.html