deemetree/z3-fork

Z3定理证明器Docker镜像

本镜像提供Z3定理证明器的Docker化部署方案，无需本地安装即可通过容器运行Z3，适用于逻辑验证、数学证明等场景。

镜像概述

该镜像源码与上游Z3（https://github.com/Z3Prover/z3%EF%BC%89%E4%BF%9D%E6%8C%81%E5%90%8C%E6%AD%A5%EF%BC%8C%E6%AF%8F%E5%91%A8%E8%87%AA%E5%8A%A8%E6%89%A7%E8%A1%8C%E6%9E%84%E5%BB%BA%EF%BC%88%E8%AF%A6%E8%A7%81https://github.com/deemetree/z3-fork/blob/main/.github/workflows/publish-docker.yml%EF%BC%89%EF%BC%8C%E9%95%9C%E5%83%8F%E5%AD%98%E5%82%A8%E4%BA%8EDockerHub%EF%BC%9Ahttps://hub.docker.com/r/deemetree/z3-fork%E3%80%82

核心功能

• 支持SMT2、Datalog等输入格式
• 可通过管道输入或卷映射处理本地文件
• 提供多种标签版本（基于不同基础OS、Z3类型及构建类型）

标签模式

标签遵循以下格式：
<基础OS（如ubuntu-20.04）>-<Z3类型（如bare-z3/python-z3）>-<构建类型（如edge/sha-xyz/tag）>
完整标签列表见https://hub.docker.com/r/deemetree/z3-fork/tags?page=1&ordering=last_updated%E3%80%82
注意：edge及每周构建的镜像基于最新源码，可能存在不稳定性，建议参考https://github.com/Z3Prover/z3/releases%E3%80%82

使用场景

• 逻辑公式的可满足性验证
• 程序正确性证明
• 数学问题求解
• 形式化方法相关研究与开发

配置与使用示例

1. 拉取镜像

bash
docker pull deemetree/z3-fork:ubuntu-20.04-bare-z3-edge

2. 查看帮助

bash
docker run --rm deemetree/z3-fork:ubuntu-20.04-bare-z3-edge -h

3. 通过卷映射运行Z3

bash
# 假设本地有examples/task1.smt2文件
docker run --rm -v $(pwd):/.z3-wb/ deemetree/z3-fork:ubuntu-20.04-bare-z3-edge -smt2 /.z3-wb/examples/task1.smt2

4. 通过管道输入运行Z3

bash
cat examples/task1.smt2 | docker run --rm -i deemetree/z3-fork:ubuntu-20.04-bare-z3-edge -in -smt2

更多信息

Z3的详细使用说明见上游仓库：https://github.com/Z3Prover/z3/blob/master/README.md%E3%80%82

备注

• Python、Java及.NET绑定的支持正在规划中
• 欢迎提交PR以添加更多Z3镜像版本