如何在Z3模型评估中计算量化表达式？

Question

考虑以下内容，它创建了一个简单的模型，其中字符串等于特定的值：

from z3 import *

s = Solver()
x = String('x')
s.add(x == StringVal('foo'))
s.check()

然后，我想问是否存在一个等于x的模型值的字符串：

y = String('y')
expr = Exists(y, y == x)
print(s.model().evaluate(expr))

我希望这将返回一个布尔值，但是输出本身就是一个表达式：

Exists(y, y == "foo")

如何使这个表达式在evaluate方法中得到实际计算，而不是返回？我假设evaluate不喜欢我引入了一个新的未绑定变量，但是肯定将该变量放入一个Exists (或者就这个问题来说，一个ForAll)就足够计算表达式了吗？有没有一种方法可以在不引入新的无约束变量的情况下编写量化方法？

Answer 1

结果表明，量化略微超出了Z3在evaluate方法中所支持的范围(这是有意义的)。解决方法是，如果s.check()返回QuantifierRef，则重新运行QuantifierRef。

result = s.model().evaluate(expr)
print(result)
if isinstance(result, QuantifierRef):
  s.push()
  s.add(result)
  print(s.check())
  s.pop()

当然，您还可以问一问，为什么还要使用evaluate调用，而不只是在调用check之前将expr作为附加约束。