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

我無法重現您所描述的問題。 在以下示例中，由Z3生成的模型中occWrites_1的值爲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