我有一个映射（M：address-> value），它表示为Z3返回的模型中的lambda表达式（exp = Lambda（k！0，0））。我想扩展它并访问它们映射到的地址和值。我知道我可以使用（z3.set_param（'model_compress'，False））指示Z3不返回Lambda表达式，但这不是我想要的。这是通过设置此标志得到的输出：
[2148532227 -> 0,
2148532228 -> 0,
2148532230 -> 0,
2148532231 -> 0 ...]
我也知道我可以通过（exp.ast）访问此表达式的抽象语法树，但是我找不到任何Python API来遍历此Ast。
我传递给Z3的smt公式可通过以下链接访问。不幸的是，我可以举一个较小的例子。
链接：https://raw.githubusercontent.com/hnemati/hnemati.github.io/master/fm.smt。
谢谢，
通常，这是不可能的。要了解原因，请考虑以下程序：
from z3 import *
s = Solver()
a = Array('A', IntSort(), IntSort())
i = Int('i')
s.add(a == Lambda([i], i+1))
print s.check()
print s.model()
z3说：
sat
[A = Lambda(i, 1 + i)]
并且您会看到没有可以获取的“有限”值集。
当然，这是一个极端的例子，解释了为什么z3py不仅为您“提供”一种方法来执行此操作，也没有一种明显的方式让AST来获取这些值。 （如果您使用AST，则基本上会看到一个“ Lambda”节点。）但是，我希望您能看到为什么在所有情况下都无法做到这一点，而且通常也不容易做到这一点。
话虽如此，您的特定问题可能不会遇到相同的问题。特别是，您很可能会对域中“感兴趣”的值感兴趣，以便从模型的角度对“感兴趣”进行一些定义。如果您的域是有限的，那么您总是可以编写一个循环并查询所有内容，然后选择所需的域，尽管当然对于较大的域（例如64位位向量）来说，这可能并不实际。而且，如果您的域名是Int，则显然不起作用。
您还没有对您的原始问题发表任何言论，因此很难再发表意见。但是，当我过去看到此类问题时，几乎总是有另一种方法可以让您通过其他机制（通常是通过一些额外的建模代码）来跟踪域中“有趣”的元素。如果可以这样做，那么您可以在获取模型时自行查询数组（或lambda）中那些节点的值。
希望这可以帮助您入门。如果您发布有关问题细节的更具体的问题，则可能有其他方法可以解决该问题。如果是这样，请随时提出一个新问题！