找不到BitVecVal作为z3的属性

Question

我正在尝试使用z3的Python API（一种更流行的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的有效实例，显示为here。任何想法如何解决此问题？

Answer 1

z3程序包可能未正确导入。执行Python代码时，请确保您处于正确的环境中。

Answer 2

您的程序没有错。我在开头添加了打印版本，并在结尾添加了打印语句：

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

这表明您的安装已被终止。您最好的选择是从头开始重新安装。