無法爲z3py提取Z3 EnumSort的值

Question

我正在嘗試將問題編碼到Z3中，並且我希望爲「三態」布爾值（即，帶有true,false和unknown的布爾值）建模。

這裏是我怎麼也仿照它：

#!/usr/bin/env python 

import z3 
from collections import OrderedDict 

TristateValues = ["True", "False", "Unknown"] 
Tristate, consts = z3.EnumSort("Tristate", TristateValues) 
TristateValues = OrderedDict(zip(TristateValues, consts)) 

s = z3.Solver() 
x = z3.Const("x", Tristate) 
s.add(x != TristateValues["Unknown"]) 
value = s.check() 
if value == z3.sat: 
    m = s.model() 
    print str(m.eval(x)) 
else: 
    print str(value) 

# EOF 

而且這個小例子，事情的工作很好，我得到的值，如True或False。

然而，在大規模的例子，我得到的結果，如：

• Tristate!val!0
• Tristate!val!1
• Tristate!val!2

很明顯，似乎有將它們之間的映射「三態「字符串和真實值，所以我寫了這樣的東西：

ModelToTristate = {} 

as_list = list(TristateValues.keys()) 
for idx in range(0, len(as_list)): 
    ModelToTristate["Tristate!val!{:d}".format(idx)] = as_list[idx] 

嘗試在值之間映射回（這就是爲什麼使用OrderedDict對於保持排序非常重要）。

而且，最初，它似乎工作。但是，我然後打一些，陌生的錯誤：

• 我最終得到查找錯誤到ModelToTristate它似乎確實我在得到正確的價值上的model.eval()結果調用str（即Z3會給True，False等，而不是比Tristate!val!*）
• 我會得到模型中的不一致性（例如，甚至斷言x == Tristate["False"]時，檢查查找會導致model.eval(x) == Tristate!val!1，其中Tristate!val!1映射到True）

對於這最後一個問題，我認爲有一個查找問題，而不是Z3給出不正確的值。

所以，我的問題是：是什麼原因造成Z3使用這些Tristate!val!*字符串，我可以「強制」 Z3使用正確的值（即True，False，Unknown）？

我正在使用Z3 4.5.0。

更新檢查後，似乎這個問題出現在我使用SolverFor("QF_ABV")時。

Answer 1

QF_ABV邏輯不知道代數數據類型。它會把它們當作未解釋的。你回來的模型就好像枚舉類是免費的。