如何在z3python中从FuncInterp获得具体的值？

Question

我使用Z3解算器来检查一些查询并得到模型。 但是模型中的一些变量是FuncInterp，显示为Lambda函数。你知道吗

[v0 = Lambda(k!0, If(k!0 == 1, 4, 0)),
 v1 = Lambda(k!0,
                  If(k!0 == 1,
                     1,
                     If(k!0 == 3,
                        128,
                        If(k!0 == 2, 113, 0)))),
 v2 = Lambda(k!0, If(k!0 == 1, 1, 0)),
 v3 = Lambda(k!0,
                  If(k!0 == 1,
                     244,
                     If(k!0 == 3,
                        216,
                        If(k!0 == 2, 214, 198)))),
 v4 = Lambda(k!0,
                  If(k!0 == 3,
                     198,
                     If(k!0 == 1,
                        214,
                        If(k!0 == 2, 244, 215)))),
 v5 = K(BitVec(32), 80),
 v6 = K(BitVec(32), 194),
 v7 = K(BitVec(32), 80),
 v8 = K(BitVec(32), 80)]

甚至我也尝试使用How get a a value from a Lambda expression?中建议的z3.set_param('model_compress', False) 它们仍然像：

[v0 = [0 -> 0, 1 -> 4, else -> 0],
 v1 = [0 -> 0,
       2 -> 113,
       3 -> 128,
       1 -> 1,
       else -> 0],
 v2 = [2 -> 0,
       0 -> 0,
       3 -> 0,
       1 -> 1,
       else -> 0],
 v3 = [0 -> 198,
       2 -> 214,
       3 -> 216,
       1 -> 244,
       else -> 198],
 v4 = [0 -> 215,
       2 -> 244,
       1 -> 214,
       3 -> 198,
       else -> 215],
 v5 = K(BitVec(32), 80),
 v6 = K(BitVec(32), 194),
 v7 = K(BitVec(32), 80),
 v8 = K(BitVec(32), 80),
 k!7 = [2 -> 0, 0 -> 0, 3 -> 0, 1 -> 1, else -> 0],
 k!4 = [0 -> 0, 1 -> 4, else -> 0],
 k!8 = [0 -> 215, 2 -> 244, 1 -> 214, 3 -> 198, else -> 215],
 k!5 = [0 -> 0, 2 -> 113, 3 -> 128, 1 -> 1, else -> 0],
 k!6 = [0 -> 198, 2 -> 214, 3 -> 216, 1 -> 244, else -> 198]]

我的问题是，如何获得这些函数的常量/具体值？你知道吗

非常感谢