在Linux系统中安装STP(一个用于约束求解的SMT求解器,常用于程序分析和符号执行)需要从源码编译安装,以下是详细步骤,覆盖常见发行版(如Ubuntu/Debian、CentOS/Fedora):
安装依赖项
STP依赖C/C++编译环境、CMake、Python及数学库,根据发行版选择命令:
Ubuntu/Debian
sudo apt update sudo apt install -y git cmake build-essential cmake libboost-all-dev python3-minimal flex bison
CentOS/Fedora
sudo yum install git cmake3 boost-devel python3 flex bison # Fedora sudo dnf groupinstall "Development Tools" sudo dnf install git cmake boost-devel python3 flex bison
关键依赖说明:
boost-devel
:STP核心算法依赖Boost库。flex
和bison
:解析器生成工具,用于处理STP的输入语言。cmake
:管理编译流程。
克隆STP源码
git clone https://github.com/stp/stp.git cd stp git checkout master # 使用稳定分支
配置与编译
通过CMake生成构建配置并编译:
mkdir build && cd build cmake .. -DBUILD_SHARED_LIBS=OFF -DENABLE_PYTHON_INTERFACE=ON # 禁用动态库(避免冲突),启用Python接口 make -j$(nproc) # 使用多核加速编译
参数解释:
-DBUILD_SHARED_LIBS=OFF
:静态链接提高兼容性。-DENABLE_PYTHON_INTERFACE=ON
:启用Python API(如需)。
安装与验证
sudo make install # 默认安装到 /usr/local/bin ldconfig # 更新库链接
验证安装:
stp --version # 输出版本信息(如 "STP version 2.3.3")
运行测试用例(可选):
./test/run_tests.sh # 在build目录内执行
常见问题解决
-
错误:找不到libboost_python
创建符号链接(以Ubuntu为例):sudo ln -s /usr/lib/x86_64-linux-gnu/libboost_python38.so /usr/lib/libboost_python.so
-
CMake报错:缺少依赖
根据错误提示安装对应包(如zlib
、openssl
)。 -
Python接口无法导入
确保编译时启用-DENABLE_PYTHON_INTERFACE=ON
,并安装Python开发包(python3-dev
)。
卸载STP
进入源码的build
目录执行:
sudo make uninstall rm -rf /usr/local/lib/libstp.a # 手动清理残留
引用说明
- STP官方GitHub仓库:https://github.com/stp/stp
- 编译指南参考:STP官方文档
- Boost库文档:https://www.boost.org/
提示:建议定期更新源码(
git pull
)以获取修复,遇到问题优先查阅GitHub Issues。
原创文章,发布者:酷番叔,转转请注明出处:https://cloud.kd.cn/ask/5999.html