int - Z3Py Bool 变量在模型中转换为 Int

Question

我正在使用用于 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？

Answer 1

我无法重现您描述的问题。在以下示例中，occWrites_1 的值true在 Z3 生成的模型中。它也可以在这里在线获得。请注意，该值是 Z3 表达式，而不是 PythonTrue值。也许这就是混乱的根源。该方法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