BitVecVal не найден в качестве атрибута для z3

Question

Я пытаюсь использовать Python API z3, одного из наиболее популярных SMT-решателей, для создания экземпляра SMT. Для начала я хотел бы создать четыре битовых вектора с двумя битами и значениями от нуля до трех. Мой код инициализации в Python следующий:

import z3

NONE = z3.BitVecVal(0, 2)
A    = z3.BitVecVal(1, 2)
B    = z3.BitVecVal(2, 2)
C    = z3.BitVecVal(3, 2)

Но я столкнулся с этой ошибкой при запуске файла Python: AttributeError: module 'z3' has no attribute 'BitVecVal'. Я посмотрел BitVecVal, и это действительный экземпляр z3, показанный здесь . Есть идеи как это исправить?

Answer 1

В вашей программе нет ничего плохого. Я добавил версию для печати в начале и инструкцию для печати в конце:

import z3

print z3.get_version_string()

NONE = z3.BitVecVal(0, 2)
A    = z3.BitVecVal(1, 2)
B    = z3.BitVecVal(2, 2)
C    = z3.BitVecVal(3, 2)

print  NONE, A, B, C

И я получаю:

4.8.8
0 1 2 3

Это говорит о том, что ваша установка каким-то образом нарушена. Лучшим вариантом может быть переустановка с нуля.

Answer 2

Пакет z3, вероятно, импортирован неправильно. Убедитесь, что вы находитесь в правильной среде при выполнении кода Python.