在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
