如何将Z3求解器模型返回的Instance类型转为int类型？

我运行以下代码后，打印结果看起来是整数，但s.model()[a]或s.model()[b]的类型是<type 'instance'>，没办法直接在后续代码里当int用，请问怎么转成int类型？

代码如下：

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]

别担心，这是Z3使用中很常见的小问题，你可以用这几种简单方法把Z3的整数实例转成Python原生int类型：

方法1：直接用int()强制转换 #

Z3返回的IntNumRef实例（也就是你看到的<type 'instance'>）支持直接被Python的int()函数解析，直接套一层就能得到原生整数：

def test(): 
    s = Solver() 
    a = Int('x') 
    b = Int('y') 
    s.add(a*b==22) 
    print(s.check()) 
    model = s.model()
    # 转换为Python原生int
    x_val = int(model[a])
    y_val = int(model[b])
    return x_val, y_val

这样返回的x_val和y_val就是标准的<type 'int'>，后续代码里随便用都没问题。

方法2：使用Z3自带的as_long()方法 #

如果你的求解结果是32位以内的整数，也可以用Z3提供的as_long()方法转换：

x_val = model[a].as_long()
y_val = model[b].as_long()

不过要注意，要是数值超出了常规长整数范围（Python3里int已经支持任意精度，这个问题基本可以忽略），还是用int()的兼容性更好。

简单来说，Z3的模型返回的是它自己的数值类型实例，用来保留符号计算相关的信息，但当你确定结果是具体数值时，上面两种方法都能轻松帮你转成可以直接使用的原生整数。

内容的提问来源于stack exchange，提问作者user8877134