未找到作为 z3 属性的 BitVecVal

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

这表明您的安装以某种方式被破坏了。您最好的选择可能是从头开始重新安装。

Answer 3

我在 Pycharm IDE 中遇到了同样的问题（当我只从 file->setting-> Project Interpreter -> add 安装 z3 时）但是我安装了z3-solver之后，这个问题就解决了。

未找到作为 z3 属性的 BitVecVal

BitVecVal not found as an attribute to z3

python

smt

z3

z3py