Z3是一种SMT Solver，用于在给定背景逻辑的情况下，求解改组理论解释下的公式可满足性。

下载安装

从下面链接中下载新的Z3版本：
https://github.com/Z3Prover/z3/releases

安装：
1.cd z3
2.python scripts/mk_make.py
3.cd build（切换到build文件夹）
4.make
看到Z3 was successfully built则表示安装成功

写一个Z3示例程序

安装成功后在命令行输入z3 -h查看帮助，使用z3 -in开始输入代码，如输入下面代码：

(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)

check-sat的结果为sat
退出输入状态使用“(exit)”命令。
这样一个完整的例子就写好了。

写一个Z3无法求解的约束

(declare-const a Int)
(assert (> (* a a) 3))
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) (* a 1000000)))
(check-sat)

上述check-sat的结果为unknow，因为对于非线性的实数运算的代价是非常大的，返回的结果可能是unknow或者loop。

参考资料：
z3 -h：官方自带的help文档，什么都不知道的情况可以查看，否则连怎么输入代码都不知道
Z3-guide：官方文档https://rise4fun.com/z3/tutorialcontent/guide#h24

SMT Solver-Z3入手教程相关推荐

JML使用基础——利用openjml和JMLunit联合操作——SMT solver验证
目录从DBC到JML SMT solver 使用 JML toolchain的可视化输出和我的测试结果规格的完善策略架构设计 debug情况心得体会一.从DBC到JML 契约式设计(Des ...
[github] github入手教程
[github] github入手教程简单的介绍一下Github的基本操作. 主页:https://github.com/ 首先自然是在GitHub注册一个帐号了.然后开始正文吧. Git基本介绍 ...
树莓派的系统安装（简单易入手教程！！！）
树莓派的系统安装(简单易入手教程!!!) 感谢一位幽默的大佬将这技术传授与我,接下来我将把我的理解一一还原,让大家也可以获取到这样一个很棒的技能,若文章中有什么错误或不足的地方,望大家包涵并指正,希 ...
GitLab 小白入手教程
GitLab 小白入手教程这里不讲概念性的东西,在看这个之前请先移步到廖雪峰的官方网站选择git教程!下载并安装Git,然后点击Git Bash Here ,进行全局配置 1 git config ...
绘图与可视化入手教程
绘图与可视化入手教程 Matplotlib 创建画布与创建子图创建画布 plt.figure()---在plt中绘制一张图片 plt.subplot--创建单个子图 plt.subplots--创建 ...
IDEA萌新快速入手教程
Intellij IDEA的大名相信不少人都听过,号称"最强大的JAVA开发工具".但是,仍然有大部分人依旧在使用Eclipse系列产品进行程序开发,本人也是一直使用Eclipse ...
6、Google TPU 入手教程
最近获得一块Google TPU ,简单介绍一下启动过程:具体参考手册: https://coral.withgoogle.com/resources/ https://www.mrtbc.com/3 ...
Z3 Solver中Tactic的使用
Z3求解器是微软开发的一款定理证明器.可以用来证明定理,也可以用于求解.其基本用法并不复杂,通过现有的教程,结合源码中提供的示例就可以理解.除了基础的用法以外,Z3还提供了一系列Tactic辅助计算和 ...
【z3 solver手动安装】
TSN领域有很多文章使用z3 solver求解约束可满足性问题.典型的工作包括Silviu S. Craciunas 等人的Scheduling Real-Time Communication in ...

SMT Solver-Z3入手教程

下载安装

写一个Z3示例程序

SMT Solver-Z3入手教程相关推荐

最新文章

热门文章