Z3Py Bool 变量在模型中转换为 Int答案

【问题标题】：Z3Py Bool variables cast to Int in the modelZ3Py Bool 变量在模型中转换为 Int
【发布时间】：2013-06-13 07:13:10
【问题描述】：

我正在使用适用于 Z3 的 python API 来构建我的研究工具。我有以下问题：我正在使用 Python 脚本生成一组 Z3 约束。由于集合可能不一致，我正在使用 assert_and_check 跟踪每个公式。例如，

s.assert_and_track(occWrites_1== True, 'p16')

当然，occWrites 被声明为布尔值：

occWrites_1 = Bool('occWrites_1')

但是，在模型中，Z3 将 occWrites 报告为整数。为什么会这样？模型中occWrites的值不应该是True还是False？

【问题讨论】：

请提供一个链接到rise4fun上托管的一个演示行为的最小示例。

标签： int boolean z3 z3py

【解决方案1】：

我无法重现您描述的问题。在以下示例中，occWrites_1 的值在 Z3 生成的模型中为 true。也可在线获取here。请注意，该值是 Z3 表达式，而不是 Python True 值。也许这就是混乱的根源。 sexpr() 方法漂亮地使用 Z3 内部格式打印值。

from z3 import *

s = Solver()
occWrites_1 = Bool('occWrites_1')
s.assert_and_track(occWrites_1 == True, 'p16')
print s.check()
m = s.model()
print m[occWrites_1]
print m[occWrites_1].sexpr()

产生的输出是：

sat
True
true

【讨论】：