z3pyでZ3 EnumSortの値を抽出できません

Question

現在、問題をZ3にエンコードしようとしています。「tristate」ブール型（つまり、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

を、「これらの間のマッピングが存在することになるようですトライステート "の文字列と実際の値は、このように書いています。

値の間で戻って試してみてください（これはOrderedDictの使用が順序を保持するために重要です）。

そして、当初、これはうまくいくように見えました。しかし、私はその後、いくつかのより多くの、見知らぬ人のエラーヒット：

• を私は最終的に私が実際に（すなわち、Z3は与えるだろうmodel.eval()の結果にstrを呼び出すための正しい値を得ていたようだModelToTristateにルックアップエラーを取得したいです私は、モデル内の矛盾を取得したいTrue、FalseなどではなくTristate!val!*より）
• （Tristate!val!1がTrueにマップどこ例えば、x == Tristate["False"]を主張しても、ルックアップをチェックすると、model.eval(x) == Tristate!val!1につながる）

この最後の問題では、誤った値を与えるZ3ではなく、ルックアップの問題があると思います。

だから、私の質問は：Z3はこれらTristate!val!*文字列を使用するために引き起こしているものを、と私は正しい値（すなわち、True、False、Unknown）を使用するようにZ3を「強制」することができますか？

私はZ3 4.5.0を使用しています。

更新を確認した後、SolverFor("QF_ABV")を使用するとこの問題が発生するようです。

Answer 1

QF_ABVロジックは、代数データ型については認識していません。それは未解釈のものとして扱われます。あなたが元に戻すモデルは列挙型が自由であるかのようです。