未找到作为z3属性的BitVecVal

Question

我正在尝试使用z3的pythonapi来创建一个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

你的程序没有问题。我在开头添加了打印版本，在结尾添加了打印语句：

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代码时处于正确的环境中

Answer 3

我在Pycharm IDE中也有同样的问题（当我仅从文件安装z3时->；设置->；项目解释器->；添加） 但是在我安装了z3解算器之后，这个问题就解决了