如何获取Z3公式中声明的高阶自由变量列表？

Z3内置的变量提取方法（比如get_vars()）只能返回原始声明的符号变量（如示例中的P1、x、y），因为A1、A2并不是自由变量，而是由原始变量组合而成的布尔表达式节点，Z3不会将其标记为“变量”来追踪。

要获取你需要的{P1, A1, A2}集合，最直接的方式是手动维护自定义表达式的集合，在定义这些表达式时就将其存入集合中：

from z3 import *

# 声明原始符号变量
P1 = Bool('P1')
x, y = Ints('x y')

# 初始化集合，用于存储需要追踪的表达式
target_exprs = set()

# 定义表达式时同时加入集合
A1 = (x + y > 1)
target_exprs.add(A1)
A2 = (x <= 0)
target_exprs.add(A2)
target_exprs.add(P1)

# 构建最终公式
f = And(Implies(P1, A1), Implies(Not(P1), A2))

# 此时target_exprs就是你需要的集合
print(target_exprs)

后续需要生成And(f, Not(A1))这类公式时，直接使用之前定义的A1变量即可，无需从f中反向提取——因为f的结构是由表达式树组成的，Z3不会保留你最初定义A1、A2时的命名关联。

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