从 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]) 或 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()