如何获取添加到求解器中任何约束的所有变量？答案

【问题标题】：How to get all the variables that were added to any constraint in a Solver?如何获取添加到求解器中任何约束的所有变量？
【发布时间】：2014-09-10 13:50:19
【问题描述】：

我正在使用 Z3py 并尝试在 Solver 的任何约束中获取所有变量的集合。例如，我可以调用Solver.assertions() 来获取ASTVector，然后循环该向量并获取BoolRef 类型的对象，但后来我被卡住了。我如何递归地迭代一个断言，例如 BoolRef 实例，以获取各个变量？

【问题讨论】：

这组变量/声明存在于 Solver 中，虽然我上次检查过，但它在 C/C++ API 之外是不可见的（例如：stackoverflow.com/questions/13054054/…）。除非改变了，否则另一种方法是跟踪您自己使用的所有变量/声明，然后您将拥有所有可用的变量/声明。如果你想走递归路线，有一些方法可以走 AST：stackoverflow.com/questions/15236450/…

标签： z3 z3py

【解决方案1】：

感谢泰勒的回答。我认为第二个链接解决了这个问题。更详细地说，Leo 在上一个答案中添加的 python 脚本会遍历 AST，AstMap 确保共享的子表达式只遍历一次。

【讨论】：