FOSSIL 2.0移植指导书
发表于 2026/05/27
0
1 软件介绍
FOSSIL 是一款用于声效和自动合成李雅普诺夫类函数的软件工具，目的是验证以微分方程建模的连续时间动力系统的稳定性或安全性。该工具采用基于CEGIS的架构;Verision 1.0 工具在对应的工具论文中有详细描述（同样见下文）。
2 环境配置
环境信息
|
服务器 |
TaiShan 200 |
|---|---|
|
处理器 |
2*KunPeng 920 7280Z |
|
内存 |
16*32G，2933MHz，DDR4 |
|
系统版本 |
openEuler 22.03-LTS-SP4 |
|
FOSSIL |
2.0 |
3 系统配置
3.1 关闭防火墙
步骤 1 关闭防火墙。
systemctl stop firewalld.service
步骤 2 关闭防火墙服务自启。
systemctl disable firewalld.service
3.2 修改SELINUX为disabled
步骤 1 关闭selinux，立即生效。
setenforce 0
步骤 2 (永久）关闭selinux，重启生效。
sed -i 's/SELINUX=enforcing/SELINUX=disabled/g' /etc/sysconfig/selinux
----结束
3.3 安装依赖包
步骤 1 安装依赖包
yum install -y git gcc-c++ make cmake python3 python3-pip python3-devel boost-devel blas-devel lapack-devel gmp-devel mpfr-devel libmpc-devel zlib-devel openssl-devel wget curl tar unzip
3.4 Python 环境配置
步骤 1 python版本
python3 --version步骤 2 创建虚拟环境
python3 -m venv fossil-env
source /opt/fossil-env/bin/activate步骤 3 升级pip并安装依赖
pip install --upgrade pip -i https://pypi.tuna.tsinghua.edu.cn/simple --trusted-host pypi.tuna.tsinghua.edu.cn
pip install pytest numpy scipy antlr4-python3-runtime psutil -i https://pypi.tuna.tsinghua.edu.cn/simple --trusted-host pypi.tuna.tsinghua.edu.cn
3.5 安装python依赖
步骤 1 下载源码
cd /opt
git clone https://github.com/oxford-oxcav/fossil.git步骤 2 安装z3
cd /opt/fossil
pip3 install z3-solver==4.12.2.0步骤 3 安装其他依赖
在/opt/fossil下执行
pip3 install .
4 软件安装
在编译dreal前，需要安装前置依赖nlopt、bazel构建工具、ibex。
4.1 安装nlopt
dreal依赖nlopt。
cd /opt
git clone https://github.com/stevengj/nlopt.git
cd nlopt
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=/usr/local -DBUILD_SHARED_LIBS=ON ..
make
make install安装后，建立符号链接：
# 1. 确保目标目录存在
mkdir -p /usr/lib64/pkgconfig
# 2. 建立硬链接（比软链接更稳，防止沙箱隔离导致找不到符号链接指向的文件）
ln -f /usr/local/lib64/pkgconfig/nlopt.pc /usr/lib64/pkgconfig/nlopt.pc
# 3. 告诉系统库文件在哪里（防止编译通过但运行报错）
echo "/usr/local/lib64" > /etc/ld.so.conf.d/nlopt.conf
ldconfig
export PKG_CONFIG_PATH=/usr/lib64/pkgconfig:/usr/local/share/pkgconfig:$PKG_CONFIG_PATH4.2 安装bazel构建工具
安装bazel构建工具
cd /opt/fossil/dreal4
git clone https://github.com/dreal/dreal4.git
cd dreal4
wget https://github.com/bazelbuild/bazel/releases/download/6.4.0/bazel-6.4.0-linux-arm64 -O /usr/local/bin/bazel
chmod +x /usr/local/bin/bazel4.3 安装Coin-OR CLP
步骤 1 下载 coinbrew 脚本
# 下载脚本
wget https://raw.githubusercontent.com/coin-or/coinbrew/master/coinbrew
chmod +x coinbrew步骤 2 下载并编译 CLP
# 下载 CLP 及其依赖源码（如 CoinUtils, Osi, Sample 等）
./coinbrew fetch Clp@master
#开始编译
# --prefix 指定安装目录
./coinbrew build Clp@master --prefix=/usr/local步骤 3 安装并刷新环境
# 安装到 /usr/local
./coinbrew install Clp@master
# 刷新动态链接库缓存
echo "/usr/local/lib" | sudo tee /etc/ld.so.conf.d/coinor.conf
sudo ldconfig步骤 4 建立软链接
sudo ln -s /usr/local/include/coin /usr/local/include/coin-or4.4 安装ibex
步骤 1 获取IBEX源码
git clone https://github.com/ibex-team/ibex-lib.git -b ibex-2.8.3
cd ibex-lib步骤 2 配置编译
# 赋予执行权限
chmod +x waf
export
PKG_CONFIG_PATH=/usr/local/lib/pkgconfig:$PKG_CONFIG_PATH
LDFLAGS="-lCoinUtils -lOsi -lpthread -lz" CXXFLAGS="-fPIC" ./waf configure --with-optim --lp-lib=clp --clp-path=/usr/local --interval-lib=direct --prefix=/usr/local --enable-shared步骤 3 编译安装
./waf build
sudo ./waf install
# 检查 ibex 库文件是否在 /usr/local/lib 或 /usr/local/lib64
ls -l /usr/local/lib/libibex*
# 然后将其加入动态库缓存
echo "/usr/local/lib" > /etc/ld.so.conf.d/ibex.conf
echo "/usr/local/lib64" >> /etc/ld.so.conf.d/ibex.conf
ldconfig步骤 4 完成链接
ln -sf /usr/local/share/pkgconfig/ibex.pc /usr/lib64/pkgconfig/ibex.pc4.5 安装dreal4
1. 下载依赖包
这里统一使用本地下载引入，防止编译中因网络情况报错。保存地址以~/bazel_deps为例。
表格 4.1
|
文件名 |
下载链接 |
|
json-b2306145e1789368e6f261680e8dc007e91cc986.tar.gz |
https://codeload.github.com/nlohmann/json/tar.gz/b2306145e1789368e6f261680e8dc007e91cc986 |
|
picosat-ee542566ca89717af1b4558b0b3f226eb3b6b42d.tar.gz |
https://codeload.github.com/dreal-deps/picosat/tar.gz/ee542566ca89717af1b4558b0b3f226eb3b6b42d |
|
ezoptionparser-5bb9214fc26bf14cea071411216e23799cabd0da.tar.gz |
https://codeload.github.com/dreal-deps/ezoptionparser/tar.gz/5bb9214fc26bf14cea071411216e23799cabd0da |
|
rules_cc-0.0.2.tar.gz |
https://release-assets.githubusercontent.com/github-production-release-asset/161776641/8c31b75a-1df3-43a7-be94-47a0de556700?sp=r&sv=2018-11-09&sr=b&spr=https&se=2026-04-18T08%3A35%3A58Z&rscd=attachment%3B+filename%3Drules_cc-0.0.2.tar.gz&rsct=application%2Foctet-stream&skoid=96c2d410-5711-43a1-aedd-ab1947aa7ab0&sktid=398a6654-997b-47e9-b12b-9515b896b4de&skt=2026-04-18T07%3A35%3A40Z&ske=2026-04-18T08%3A35%3A58Z&sks=b&skv=2018-11-09&sig=UlcKuMOT3z7gNvyWMOT52Dl1gcTmmi%2FgT5dNbrnrti8%3D&jwt=eyJ0eXAiOiJKV1QiLCJhbGciOiJIUzI1NiJ9.eyJpc3MiOiJnaXRodWIuY29tIiwiYXVkIjoicmVsZWFzZS1hc3NldHMuZ2l0aHVidXNlcmNvbnRlbnQuY29tIiwia2V5Ijoia2V5MSIsImV4cCI6MTc3NjQ5ODg2MCwibmJmIjoxNzc2NDk4NTYwLCJwYXRoIjoicmVsZWFzZWFzc2V0cHJvZHVjdGlvbi5ibG9iLmNvcmUud2luZG93cy5uZXQifQ.7hM2N5LFqCMuv1qk0SGv2U5os1uhCocnEsRIBYdeiPk&response-content-disposition=attachment%3B%20filename%3Drules_cc-0.0.2.tar.gz&response-content-type=application%2Foctet-stream |
|
libcds-2.3.3.tar.gz |
https://codeload.github.com/khizmax/libcds/tar.gz/refs/tags/v2.3.3 |
|
pybind11-2.10.2.tar.gz |
https://codeload.github.com/pybind/pybind11/tar.gz/refs/tags/v2.10.2 |
|
rules_license-0.0.4.tar.gz |
https://release-assets.githubusercontent.com/github-production-release-asset/256319745/edb16a60-5498-4532-84fd-b071e67d9d1f?sp=r&sv=2018-11-09&sr=b&spr=https&se=2026-04-18T07%3A58%3A34Z&rscd=attachment%3B+filename%3Drules_license-0.0.4.tar.gz&rsct=application%2Foctet-stream&skoid=96c2d410-5711-43a1-aedd-ab1947aa7ab0&sktid=398a6654-997b-47e9-b12b-9515b896b4de&skt=2026-04-18T06%3A57%3A52Z&ske=2026-04-18T07%3A58%3A34Z&sks=b&skv=2018-11-09&sig=o09%2FGdNpFoSJxg14kixTpvSVyFeeiHPxtlSGVJVc49I%3D&jwt=eyJ0eXAiOiJKV1QiLCJhbGciOiJIUzI1NiJ9.eyJpc3MiOiJnaXRodWIuY29tIiwiYXVkIjoicmVsZWFzZS1hc3NldHMuZ2l0aHVidXNlcmNvbnRlbnQuY29tIiwia2V5Ijoia2V5MSIsImV4cCI6MTc3NjQ5NjE0NSwibmJmIjoxNzc2NDk1ODQ1LCJwYXRoIjoicmVsZWFzZWFzc2V0cHJvZHVjdGlvbi5ibG9iLmNvcmUud2luZG93cy5uZXQifQ.dhwjtZPjXHX-JkvnBzkCsERr5siV-Zp7xCv8gWMfE5A&response-content-disposition=attachment%3B%20filename%3Drules_license-0.0.4.tar.gz&response-content-type=application%2Foctet-stream |
|
spdlog-1.11.0.tar.gz |
https://codeload.github.com/gabime/spdlog/tar.gz/refs/tags/v1.11.0 |
|
fmt-9.1.0.tar.gz |
https://codeload.github.com/fmtlib/fmt/tar.gz/refs/tags/9.1.0 |
|
abseil-cpp-20230125.1.tar.gz |
https://codeload.github.com/abseil/abseil-cpp/tar.gz/refs/tags/20230125.1 |
|
rules_python-0.17.3.tar.gz |
https://codeload.github.com/bazel-contrib/rules_python/tar.gz/refs/tags/0.17.3 |
|
pycodestyle-2.10.0.tar.gz |
https://codeload.github.com/PyCQA/pycodestyle/tar.gz/refs/tags/2.10.0 |
|
cpplint-1.6.1.tar.gz |
https://codeload.github.com/cpplint/cpplint/tar.gz/refs/tags/1.6.1 |
|
googletest-release-1.12.1.tar.gz |
https://codeload.github.com/google/googletest/tar.gz/refs/tags/release-1.12.1 |
|
rules_java-5.5.1.tar.gz |
https://release-assets.githubusercontent.com/github-production-release-asset/189174211/c0c66883-571a-4c2b-8da3-47fc51ee1c5f?sp=r&sv=2018-11-09&sr=b&spr=https&se=2026-04-17T08%3A23%3A26Z&rscd=attachment%3B+filename%3Drules_java-5.5.1.tar.gz&rsct=application%2Foctet-stream&skoid=96c2d410-5711-43a1-aedd-ab1947aa7ab0&sktid=398a6654-997b-47e9-b12b-9515b896b4de&skt=2026-04-17T07%3A23%3A06Z&ske=2026-04-17T08%3A23%3A26Z&sks=b&skv=2018-11-09&sig=rr0N%2F1y50muhzfLxHYOoPaSLQq5tDeeFZUCWv%2B%2BOUGo%3D&jwt=eyJ0eXAiOiJKV1QiLCJhbGciOiJIUzI1NiJ9.eyJpc3MiOiJnaXRodWIuY29tIiwiYXVkIjoicmVsZWFzZS1hc3NldHMuZ2l0aHVidXNlcmNvbnRlbnQuY29tIiwia2V5Ijoia2V5MSIsImV4cCI6MTc3NjQxMjE0OCwibmJmIjoxNzc2NDExODQ4LCJwYXRoIjoicmVsZWFzZWFzc2V0cHJvZHVjdGlvbi5ibG9iLmNvcmUud2luZG93cy5uZXQifQ.D7Qr8wox7F-Tt8Z6dJrBnoGESYLyxa1EZz9xrpkdNgA&response-content-disposition=attachment%3B%20filename%3Drules_java-5.5.1.tar.gz&response-content-type=application%2Foctet-stream |
|
bazel-skylib-1.4.0.tar.gz |
https://codeload.github.com/bazelbuild/bazel-skylib/tar.gz/refs/tags/1.4.0 |
|
rules_pkg-0.8.0.tar.gz |
https://mirror.bazel.build/github.com/bazelbuild/rules_pkg/releases/download/0.8.0/rules_pkg-0.8.0.tar.gz |
2. 修改配置文件
红色字体(-)表示删除该行，绿色字体(+)表示新增该行。
步骤 1 修改WORKSPACE文件
-load(
- "//third_party/com_github_robotlocomotion_drake:tools/workspace/github.bzl",
- "github_archive",
-)步骤 2 修改WORKSPACE中bazel_skylib部分
-github_archive(
- name = "bazel_skylib", # Apache-2.0
- commit = "1.4.0",
- repository = "bazelbuild/bazel-skylib",
+# 1. bazel_skylib
+http_archive(
+ name = "bazel_skylib",
+ urls = ["file:///root/bazel_deps/bazel-skylib-1.4.0.tar.gz"],
sha256 = "4dd05f44200db3b78f72f56ebd8b102d5bcdc17c0299955d4eb20c38c6f07cd7",
+ strip_prefix = "bazel-skylib-1.4.0",
)步骤 3 修改WORKSPACE中google_styleguide部分
-github_archive(
- name = "google_styleguide", # BSD-3
+# 2. google_styleguide
+http_archive(
+ name = "google_styleguide",
build_file = "//tools:google_styleguide.BUILD.bazel",
- commit = "1.6.1",
- repository = "cpplint/cpplint",
+ urls = ["file:///root/bazel_deps/cpplint-1.6.1.tar.gz"],
sha256 = "7be47998c4bd590e229cf94f3312c46563d3ee35ea037b4ed389720f510029d6",
+ strip_prefix = "cpplint-1.6.1",
)
步骤 4 修改WORKSPACE中pycodestyle部分
-github_archive(
- name = "pycodestyle", # Expat
+# 3. pycodestyle
+http_archive(
+ name = "pycodestyle",
build_file = "//tools:pycodestyle.BUILD.bazel",
- commit = "2.10.0",
- repository = "PyCQA/pycodestyle",
+ urls = ["file:///root/bazel_deps/pycodestyle-2.10.0.tar.gz"],
sha256 = "a7306561f1ddf7bc00419b9f0d698d312a8eaa173b834e7c8e4ff32db5efd27f",
+ strip_prefix = "pycodestyle-2.10.0",
)步骤 5 修改WORKSPACE中ezoptionparser部分
-github_archive(
- name = "ezoptionparser", # MIT
+# 4. ezoptionparser
+http_archive(
+ name = "ezoptionparser",
build_file = "//tools:ezoptionparser.BUILD.bazel",
- commit = "5bb9214fc26bf14cea071411216e23799cabd0da",
- repository = "dreal-deps/ezoptionparser",
+ urls = ["file:///root/bazel_deps/ezoptionparser-5bb9214fc26bf14cea071411216e23799cabd0da.tar.gz"],
sha256 = "7349f3091bd05a675a61b61350536f32da77578d3bfb629e2ed5bc31b7a4fa2c",
+ strip_prefix = "ezoptionparser-5bb9214fc26bf14cea071411216e23799cabd0da",
)
步骤 6 修改WORKSPACE中googletest部分
-github_archive(
- name = "com_google_googletest", # GOOGLE
- commit = "release-1.12.1",
- repository = "google/googletest",
+# 5. googletest
+http_archive(
+ name = "com_google_googletest",
+ urls = ["file:///root/bazel_deps/googletest-release-1.12.1.tar.gz"],
sha256 = "81964fe578e9bd7c94dfdb09c8e4d6e6759e19967e397dbea48d1c10e45d0df2",
+ strip_prefix = "googletest-release-1.12.1",
)步骤 7 修改WORKSPACE中rules_python部分
-# Note: Dependency of rules_pkg in dreal/workspace.bzl
+# 6. rules_python
http_archive(
- name = "rules_python", # Apache-2.0
+ name = "rules_python",
+ urls = ["file:///root/bazel_deps/rules_python-0.17.3.tar.gz"],
sha256 = "8c15896f6686beb5c631a4459a3aa8392daccaab805ea899c9d14215074b60ef",
strip_prefix = "rules_python-0.17.3",
- url = "https://github.com/bazelbuild/rules_python/archive/refs/tags/0.17.3.tar.gz",
)步骤 8 修改dreal/workspace.bzl中rules_license部分
http_archive(
name = "rules_license",
sha256 = "6157e1e68378532d0241ecd15d3c45f6e5cfd98fc10846045509fb2a7cc9e381",
- urls = [
- "https://mirror.bazel.build/github.com/bazelbuild/rules_license/releases/download/0.0.4/rules_license-0.0.4.tar.gz",
- ],
+ urls = ["file:///root/bazel_deps/rules_license-0.0.4.tar.gz"],
)步骤 9 修改dreal/workspace.bzl中rules_pkg部分
http_archive(
name = "rules_pkg",
sha256 = "eea0f59c28a9241156a47d7a8e32db9122f3d50b505fae0f33de6ce4d9b61834",
- urls = [
- "https://mirror.bazel.build/github.com/bazelbuild/rules_pkg/releases/download/0.8.0/rules_pkg-0.8.0.tar.gz",
- "https://github.com/bazelbuild/rules_pkg/releases/download/0.8.0/rules_pkg-0.8.0.tar.gz",
- ],
+ urls = ["file:///root/bazel_deps/rules_pkg-0.8.0.tar.gz"],
)步骤 10 修改dreal/workspace.bzl中spdlog部分
- github_archive(
+ http_archive(
name = "spdlog", # MIT
build_file = str(Label("//tools:spdlog.BUILD.bazel")),
- commit = "v1.11.0",
- repository = "gabime/spdlog",
sha256 = "ca5cae8d6cac15dae0ec63b21d6ad3530070650f68076f3a4a862ca293a858bb",
+ urls = ["file:///root/bazel_deps/spdlog-1.11.0.tar.gz"],
+ strip_prefix = "spdlog-1.11.0",
)
步骤 11 修改dreal/workspace.bzl中fmt部分
- github_archive(
+ http_archive(
name = "fmt", # MIT
build_file = str(Label("//tools:fmt.BUILD.bazel")),
- commit = "9.1.0",
- repository = "fmtlib/fmt",
sha256 = "5dea48d1fcddc3ec571ce2058e13910a0d4a6bab4cc09a809d8b1dd1c88ae6f2",
+ urls = ["file:///root/bazel_deps/fmt-9.1.0.tar.gz"],
+ strip_prefix = "fmt-9.1.0",
)步骤 12 修改dreal/workspace.bzl中picosat部分
- github_archive(
+ http_archive(
name = "picosat", # MIT
build_file = str(Label("//tools:picosat.BUILD.bazel")),
- commit = "ee542566ca89717af1b4558b0b3f226eb3b6b42d", # v965 + custom fix
- repository = "dreal-deps/picosat",
sha256 = "9a047b7ba3ac1075a2288d35045585e2e3c24961f078f30ad97a313b8e539eb2",
+ urls = ["file:///root/bazel_deps/picosat-ee542566ca89717af1b4558b0b3f226eb3b6b42d.tar.gz"],
+ strip_prefix = "picosat-ee542566ca89717af1b4558b0b3f226eb3b6b42d",
)步骤 13 修改dreal/workspace.bzl中pybind11部分
- github_archive(
+ http_archive(
name = "pybind11", # BSD
build_file = str(Label("//tools:pybind11.BUILD.bazel")),
- commit = "v2.10.2",
- repository = "pybind/pybind11",
sha256 = "93bd1e625e43e03028a3ea7389bba5d3f9f2596abc074b068e70f4ef9b1314ae",
+ urls = ["file:///root/bazel_deps/pybind11-2.10.2.tar.gz"],
+ strip_prefix = "pybind11-2.10.2",
)
步骤 14 修改dreal/workspace.bzl中com_google_absl部分
- github_archive(
+ http_archive(
name = "com_google_absl", # BSD
- commit = "20230125.1",
- repository = "abseil/abseil-cpp",
sha256 = "81311c17599b3712069ded20cca09a62ab0bf2a89dfa16993786c8782b7ed145",
+ urls = ["file:///root/bazel_deps/abseil-cpp-20230125.1.tar.gz"],
+ strip_prefix = "abseil-cpp-20230125.1",
)步骤 15 修改dreal/workspace.bzl中cds部分
- github_archive(
+ http_archive(
name = "cds", # BSL 1.0
build_file = str(Label("//tools:cds.BUILD.bazel")),
- commit = "v2.3.3",
- repository = "khizmax/libcds",
sha256 = "f090380ecd6b63a3c2b2f0bdb27260de2ccb22486ef7f47cc1175b70c6e4e388",
+ urls = ["file:///root/bazel_deps/libcds-2.3.3.tar.gz"],
+ strip_prefix = "libcds-2.3.3",
)
步骤 16 修改dreal/workspace.bzl中json部分
- github_archive(
+ http_archive(
name = "json", # MIT
- commit = "b2306145e1789368e6f261680e8dc007e91cc986", # 20230131
- repository = "nlohmann/json",
sha256 = "dfb6ec5af1feeb9ce7efa1554676335ca9dde5f60424642c8ac2f9e0a66da909",
+ urls = ["file:///root/bazel_deps/json-b2306145e1789368e6f261680e8dc007e91cc986.tar.gz"],
+ strip_prefix = "json-b2306145e1789368e6f261680e8dc007e91cc986",
)
3. 修改Setup.py
def _build_dreal():
new_env = os.environ.copy()
new_env["PYTHON_BIN_PATH"] = sys.executable
- if subprocess.call([
- 'bazel', 'build', '//dreal:_dreal_py.so',
- '--cxxopt=-DDREAL_CHECK_INTERRUPT', '--python_path={}'.format(
- sys.executable),
- ],
- env=new_env) != 0:
- raise LibError("Unable to build dReal.\n" +
- "Please visit https://pypi.org/project/dreal and " +
- " the instructions to install the prerequisites.")
-
+
+ bazel_command = [
+ 'bazel', 'build',
+ '//dreal:_dreal_py.so',
+ '//:dreal_shared_library', # 同时构建这两个目标
+ '--distdir=/root/bazel_deps',
+ '--cxxopt=-I/usr/local/include/coin-or',
+ '--cxxopt=-DDREAL_CHECK_INTERRUPT',
+ '--linkopt=-Wl,--whole-archive',
+ '--linkopt=-libex',
+ '--linkopt=-Wl,--no-whole-archive',
+ '--linkopt=-L/usr/local/lib64',
+ '--linkopt=-lClp',
+ '--linkopt=-lCoinUtils',
+ '--jobs=64',
+ '--python_path={}'.format(sys.executable),
+ ]
+
+ if subprocess.call(bazel_command, env=new_env) != 0:
+ raise LibError("Unable to build dReal with Bazel.")
def _copy_bins():
- shutil.copy(os.path.join(SRC_DIR, 'bazel-bin', 'dreal', '_dreal_py.so'),
- os.path.join(ROOT_DIR, 'dreal'))
- os.chmod(os.path.join(ROOT_DIR, 'dreal', '_dreal_py.so'), 436)
- shutil.copy(os.path.join(SRC_DIR, 'bazel-bin', 'libdreal_.so'),
- os.path.join(ROOT_DIR, 'dreal'))
- os.chmod(os.path.join(ROOT_DIR, 'dreal', 'libdreal_.so'), 436)
- if sys.platform == 'darwin':
- dst_full = os.path.join(ROOT_DIR, 'dreal', '_dreal_py.so')
- subprocess.check_call(
- ["install_name_tool",
- "-id",
- os.path.join('@rpath', "_dreal_py.so"),
- dst_full])
- file_output = subprocess.check_output(["otool",
- "-L",
- dst_full]).decode("utf-8")
- for line in file_output.splitlines():
- # keep only file path, remove version information.
- relative_path = line.split(' (')[0].strip()
- # If path is relative, it needs to be replaced by absolute path.
- if "@loader_path" not in relative_path:
- continue
- if "libdreal_.so" in relative_path:
- subprocess.check_call(
- ["install_name_tool",
- "-change", relative_path,
- os.path.join('@loader_path', "libdreal_.so"),
- dst_full])
-
+ src_py_so = os.path.join(SRC_DIR, 'bazel-bin', 'dreal', '_dreal_py.so')
+ src_lib_so = os.path.join(SRC_DIR, 'bazel-bin', 'libdreal_.so')
+
+ # 如果 libdreal_.so 在 dreal 子目录下，请改为：
+ # src_lib_so = os.path.join(SRC_DIR, 'bazel-bin', 'dreal', 'libdreal_.so')
+
+ target_dir = os.path.join(ROOT_DIR, 'dreal')
+ if not os.path.exists(target_dir):
+ os.makedirs(target_dir)
+
+ print(f"Copying {src_py_so} to {target_dir}")
+ shutil.copy(src_py_so, target_dir)
+
+ print(f"Copying {src_lib_so} to {target_dir}")
+ shutil.copy(src_lib_so, target_dir)
+
+ # 设置权限
+ os.chmod(os.path.join(target_dir, '_dreal_py.so'), 0o755)
+ os.chmod(os.path.join(target_dir, 'libdreal_.so'), 0o755)4. 编译dreal及python代码示例
运行setup.py脚本打包wheel包。
python3 setup.py build
生成文件dist/dreal-4.21.6.2-cp39-none-manylinux1_aarch64.whl。
ls dist
dreal-4.21.6.2-cp39-none-manylinux1_aarch64.whl生成该wheel文件后即可安装在python中。
python3 -m pip install dreal-4.21.6.2-cp39-none-manylinux1_aarch64.whl
5. 编译dreal二进制
bazel build //dreal:dreal --distdir=/root/bazel_deps --cxxopt="-I/usr/local/include/coin-or" --linkopt="-Wl,--whole-archive" --linkopt="-libex" --linkopt="-Wl,--no-whole-archive" --linkopt="-L/usr/local/lib64" --linkopt="-lClp" --linkopt="-lCoinUtils" --jobs=64编译后会生成二进制文件bazel-bin/dreal/dreal。
运行如下：
2
6. 编译dreal：c++代码示例
以官方测试方程求解为例，，test.cpp内容如下：
#include <iostream>
#include <vector>
#include "dreal/dreal.h"
using namespace dreal;
int main() {
// 1. 定义变量
const Variable x{"x", Variable::Type::CONTINUOUS};
const Variable y{"y", Variable::Type::CONTINUOUS};
const Variable z{"z", Variable::Type::CONTINUOUS};
// 2. 构建约束公式 (等价于 Python 的 And)
// 注意：C++ 中使用 && 连接 Formula
Formula f_sat = (0 <= x) && (x <= 10) &&
(0 <= y) && (y <= 10) &&
(0 <= z) && (z <= 10) &&
(sin(x) + cos(y) == z);
std::cout << "Checking complex formula in C++..." << std::endl;
// 3. 求解 (精度设为 0.001)
Config config;
config.mutable_precision() = 0.001;
// CheckSatisfiability 返回一个 optional<Box>
auto result = CheckSatisfiability(f_sat, config);
// 4. 输出结果
if (result) {
std::cout << "SAT: " << *result << std::endl;
} else {
std::cout << "UNSAT" << std::endl;
}
return 0;
}编译test_dreal
g++ -std=c++17 test.cpp -o test_dreal \
-I/root/work/dreal4 \
-I/root/work/dreal4/bazel-bin \
-I/root/work/dreal4/third_party/com_github_pinam45_dynamic_bitset \
-I/root/work/dreal4/third_party/com_github_robotlocomotion_drake \
-I/root/work/dreal4/third_party/com_github_speadot_optional \
-I/root/work/dreal4/third_party/com_github_tartanllama_optional \
-I/usr/local/include \
-I/usr/local/include/ibex \
-I/usr/local/include/ibex/3rd \
-I/usr/local/include/coin-or \
-L/root/work/dreal4/bazel-bin \
-L/usr/local/lib \
-L/usr/local/lib64 \
-ldreal_ -libex -lClp -lCoinUtils -lnlopt \
-Wl,-rpath=/root/work/dreal4/bazel-bin:/usr/local/lib:/usr/local/lib64运行test_dreal
chmod +x test_dreal
./test_dreal
4.6 安装Fossil
安装完上述依赖后，进入fossil文件目录：
python3 -m pip install .
即完成安装。
验证fossil版本：
pip show fossil
5 运行验证
5.1 运行验证
1. 执行example.py
Fossil源码下提供了example.py来简单验证Fossil功能。下面做两点修改来加速迭代和打印出运行过程。
步骤 1 修改test_lnn.py规模
@@ -53,9 +63,10 @@ def test_lnn():
}
# define NN parameters
- activations = [fossil.ActivationType.SIGMOID, fossil.ActivationType.SIGMOID]
- n_hidden_neurons = [10] * len(activations)
-
+ #activations = [fossil.ActivationType.SIGMOID, fossil.ActivationType.SIGMOID]
+ #n_hidden_neurons = [10] * len(activations)
+ activations = [fossil.ActivationType.RELU, fossil.ActivationType.RELU]
+ n_hidden_neurons = [8, 8] # 规模也稍微缩小，确保首跑成功步骤 2 修改test_lnn.py输出方式
@@ -68,17 +79,23 @@ def test_lnn():
N_HIDDEN_NEURONS=n_hidden_neurons,
SYMMETRIC_BELT=False,
CEGIS_MAX_ITERS=25,
- VERBOSE=0,
+ VERBOSE=1,
SEED=167,
+ PRECISION=0.1
)
result = fossil.synthesise(
opts,
)
- D = opts.DOMAINS.pop(fossil.XD)
- plotting.benchmark(
- result.f, result.cert, domains=opts.DOMAINS, xrange=[-3, 2.5], yrange=[-2, 1]
- )
+ result = fossil.synthesise(opts)
+ print("\n" + "="*50)
+ print("🎊 Fossil AArch64 适配成功
🎊")
+ print(f"解合成状态: {result}")
+ print("="*50)
+ #D = opts.DOMAINS.pop(fossil.XD)
+ #plotting.benchmark(
+ # result.f, result.cert, domains=opts.DOMAINS, xrange=[-3, 2.5], yrange=[-2, 1]
+ #)修改完成后执行python3 example.py 预期得到以下内容：
Iteration:xx表示计算时的迭代次数，最终输出解。
6 FAQ
6.1 编译python包时报错：CheckSatisfiability 导致段错误退出
使用gdb调试，bt输出如下：
(gdb) run test.py
Starting program: /usr/bin/python3 test.py
[Thread debugging using libthread_db enabled]
Using host libthread_db library
"/usr/lib64/libthread_db.so.1".
Program received signal SIGSEGV, Segmentation
fault.
0x0000fffff63d0c14 in
ibex::next_generated_name(char const*, int) () from
/root/work/dreal4/bazel-bin/libdreal_.so
(gdb) bt
#0 0x0000fffff63d0c14 in ibex::next_generated_name(char const*, int) () from /root/work/dreal4/bazel-bin/libdreal_.so
#1 0x0000fffff634f944 in ibex::Function::init(ibex::Array<ibex::ExprSymbol
const> const&, ibex::ExprNode const&, char const*) () from
/root/work/dreal4/bazel-bin/libdreal_.so
#2 0x0000fffff6351ce8 in
ibex::Function::Function(ibex::Array<ibex::ExprSymbol const> const&,
ibex::ExprNode const&, char const*) () from
/root/work/dreal4/bazel-bin/libdreal_.so
#3 0x0000fffff62ccec8 in
dreal::ContractorIbexFwdbwd::ContractorIbexFwdbwd(dreal::drake::symbolic::Formula,
dreal::Box const&, dreal::Config const&) ()
from
/root/work/dreal4/bazel-bin/libdreal_.so
#4 0x0000fffff62c9dc0 in dreal::make_contractor_ibex_fwdbwd(dreal::drake::symbolic::Formula,
dreal::Box const&, dreal::Config const&) ()
from
/root/work/dreal4/bazel-bin/libdreal_.so
#5 0x0000fffff62ac844 in
dreal::TheorySolver::BuildContractor(std::vector<dreal::drake::symbolic::Formula,
std::allocator<dreal::drake::symbolic::Formula> > const&,
dreal::ContractorStatus*) () from /root/work/dreal4/bazel-bin/libdreal_.so
#6 0x0000fffff62ad89c in dreal::TheorySolver::CheckSat(dreal::Box
const&, std::vector<dreal::drake::symbolic::Formula,
std::allocator<dreal::drake::symbolic::Formula> > const&)
() from
/root/work/dreal4/bazel-bin/libdreal_.so
#7 0x0000fffff6286d6c in
dreal::Context::Impl::CheckSatCore(dreal::ScopedVector<dreal::drake::symbolic::Formula>
const&, dreal::Box, dreal::SatSolver*) ()
from
/root/work/dreal4/bazel-bin/libdreal_.so
#8 0x0000fffff628783c in dreal::Context::Impl::CheckSat() () from
/root/work/dreal4/bazel-bin/libdreal_.so
#9 0x0000fffff6265448 in dreal::Context::CheckSat() () from
/root/work/dreal4/bazel-bin/libdreal_.so
#10 0x0000fffff626036c in dreal::CheckSatisfiability(dreal::drake::symbolic::Formula
const&, dreal::Config) () from /root/work/dreal4/bazel-bin/libdreal_.so
#11 0x0000fffff626052c in
dreal::CheckSatisfiability(dreal::drake::symbolic::Formula const&, double)
() from /root/work/dreal4/bazel-bin/libdreal_.so
#12 0x0000fffff6506a68 in
pybind11::cpp_function::initialize<dreal::pybind11_init__dreal_py(pybind11::module_&)::{lambda(dreal::drake::symbolic::Formula
const&, double)#124}, tl::optional<dreal::Box>,
dreal::drake::symbolic::Formula const&, double, pybind11::name,
pybind11::scope,
pybind11::sibling>(dreal::pybind11_init__dreal_py(pybind11::module_&)::{lambda(dreal::drake::symbolic::Formula
const&, double)#124}&&, tl::optional<dreal::Box> (*)(dreal::drake::symbolic::Formula
const&, double), pybind11::name const&, pybind11::scope const&,
pybind11::sibling
const&)::{lambda(pybind11::detail::function_call&)#3}::operator()(pybind11::detail::function_call&)
const [clone .constprop.0] ()
from
/root/work/dreal4/dreal/_dreal_py.so
#13 0x0000fffff64f7d14 in
pybind11::cpp_function::dispatcher(_object*, _object*, _object*) () from
/root/work/dreal4/dreal/_dreal_py.so
#14 0x0000fffff7d06844 in ?? () from
/usr/lib64/libpython3.9.so.1.0
#15 0x0000fffff7cc93a8 in _PyObject_MakeTpCall ()
from /usr/lib64/libpython3.9.so.1.0
#16 0x0000fffff7c8dac8 in _PyEval_EvalFrameDefault
() from /usr/lib64/libpython3.9.so.1.0
#17 0x0000fffff7d8f954 in ?? () from
/usr/lib64/libpython3.9.so.1.0
#18 0x0000fffff7d8fdb4 in _PyEval_EvalCodeWithName
() from /usr/lib64/libpython3.9.so.1.0
#19 0x0000fffff7d8fe00 in PyEval_EvalCodeEx () from
/usr/lib64/libpython3.9.so.1.0
#20 0x0000fffff7d8fe3c in PyEval_EvalCode () from
/usr/lib64/libpython3.9.so.1.0
#21 0x0000fffff7dcb12c in ?? () from
/usr/lib64/libpython3.9.so.1.0
#22 0x0000fffff7dcb344 in ?? () from
/usr/lib64/libpython3.9.so.1.0
#23 0x0000fffff7dcde40 in ?? () from
/usr/lib64/libpython3.9.so.1.0
#24 0x0000fffff7dcdff4 in PyRun_SimpleFileExFlags
() from /usr/lib64/libpython3.9.so.1.0
#25 0x0000fffff7de8b90 in Py_RunMain () from
/usr/lib64/libpython3.9.so.1.0
#26 0x0000fffff7de9080 in Py_BytesMain () from
/usr/lib64/libpython3.9.so.1.0
#27 0x0000fffff798b000 in ?? () from
/usr/lib64/libc.so.6第10帧表明python代码中运行至CheckSatisfiability时报错，符合报错。第2帧表明底层在引用ibex时报错。检查ibex路径，发现ibex默认为静态二进制包，可能不满足动态链接需求。
步骤 1 清理旧环境：
步骤 1由于 Ibex 的 Waf 构建系统会缓存架构信息，必须彻底清理：
./waf distclean
步骤 2 配置与编译 Ibex：
显式开启 -fPIC（位置无关代码）和共享库支持。
# 使用环境变量传递 CXXFLAGS
CXXFLAGS="-fPIC" ./waf configure --prefix=/usr/local --enable-shared
./waf build
./waf install6.2 _dreal_py.so报错：undefined symbol
undefined
symbol: PyProperty_Type (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: _Py_NoneStruct (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: PyExc_RuntimeError (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: PyExc_TypeError (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: PyExc_ValueError (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: PyExc_StopIteration (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: PyInstanceMethod_Type (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: PyType_Type (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: _Py_TrueStruct (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: _Py_FalseStruct (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: PyByteArray_Type (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: _PyObject_NextNotImplemented (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: PyExc_OverflowError (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: PyExc_IndexError (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: PyExc_MemoryError (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: PyFloat_Type (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: PyCapsule_Type (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: PyMethod_Type (bazel-bin/dreal/_dreal_py.so)
undefined
symbol: PyDict_Type (bazel-bin/dreal/_dreal_py.so)修改问题6.1后，编译python共享库遇到大量undefined symbol错误。这是典型的符号不可见问题。在编译参数中引入 -Wl,--whole-archive 指令。链接ibex后添加--linkopt="-Wl,--whole-archive"提取全部符号，并在链接后关闭提取全部符号。
最终的编译参数为：
# setup.py
def _build_dreal():
new_env =
os.environ.copy()
new_env["PYTHON_BIN_PATH"] = sys.executable
bazel_command = [
'bazel', 'build',
'//dreal:_dreal_py.so',
'//:dreal_shared_library', # 同时构建这两个目标
'--distdir=/root/bazel_deps',
'--cxxopt=-I/usr/local/include/coin-or',
'--cxxopt=-DDREAL_CHECK_INTERRUPT',
'--linkopt=-Wl,--whole-archive',
'--linkopt=-libex',
'--linkopt=-Wl,--no-whole-archive',
'--linkopt=-L/usr/local/lib64',
'--linkopt=-lClp',
'--linkopt=-lCoinUtils',
'--jobs=64',
'--python_path={}'.format(sys.executable),
]
if
subprocess.call(bazel_command, env=new_env) != 0:
raise
LibError("Unable to build dReal with Bazel.")其中
'--linkopt=-Wl,--whole-archive',
'--linkopt=-libex',
'--linkopt=-Wl,--no-whole-archive',表明
步骤 1 引入 -Wl,--whole-archive 指令
步骤 2 强制链接器将 libex 中的所有对象文件（Object Files）全部包含在最终生成的 _dreal_py.so 中
步骤 3 通过 -Wl,--no-whole-archive 及时恢复默认链接行为