Невозможно извлечь значение для Z3 EnumSort в z3py

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

Очевидно, что между этими строками "Tristate" и реальными значениями должно быть отображение, поэтому я написал что-то вроде этого:

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 где, кажется, я действительно получаю правильное значение для вызова str на результат model.eval() (т.е. 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 не знает об алгебраических типах данных. Это будет относиться к ним как к непонятным. Тогда модель, которую вы получаете, выглядит так, как будто сортировка перечисления свободна.