从 Z3 中的实例获取整数值

Question

我的代码是

def test():
    s = Solver()
    a = Int('x')
    b = Int('y')
    s.add(a*b==22)
    print s.check()
    return s.model()[a], s.model()[b]

这将打印数字，但是当你看到type(s.model()[a])or时type(s.model()[b])，它会给出<type 'instance'>. 如何以它会返回的方式投射它<type 'int'>？我无法在我的代码中进一步使用返回类型，因为它返回实例，即使它print s.model()[a]看起来像一个整数，但事实并非如此。

Answer 1

只需使用as_long方法即可。也就是说，将函数中的最后一行替换为：

   return s.model()[a].as_long(), s.model()[b].as_long()