Anything is Nothing

前几个月科研用到z3-solver，学习了下，主要注释写在源码上进行学习和试验，现在记下相关的学习资源方便自己日后查用。

• github仓库相关官方资料论文资料汇总：（大部分都不需要着急看,进阶按需查找才需要）
  https://github.com/Z3Prover/z3/wiki#background

• 官方的document汇总
  https://github.com/Z3Prover/z3/wiki/Documentation

通常使用方式：z3是一个底层的工具，它最好是作为一个组件应用到其它需要求解逻辑公式的工具中，例如KLEE。为了方便使用，z3提供了很多的API，这些api支持的语言有C, .NET, and OCaml。当然，z3也可以通过命令行的方式来执行。

- 汇总多语言api入口 目前支持的语言：

语言	API链接
C语言	http://z3prover.github.io/api/html/group__capi.html
C++	http://z3prover.github.io/api/html/namespacez3.html
.NET	http://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html
Java	http://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html
Python	http://z3prover.github.io/api/html/namespacez3py.html
在线运行	https://rise4fun.com/z3/tutorial
OCaml (ML)	http://z3prover.github.io/api/html/ml/index.html
F# Ocaml	https://github.com/sishtiaq/compose-z3-tutorial

Z3完整的API文档在这：感觉python迭代勤快更好用，墙裂推荐使用python调用z3 https://z3prover.github.io/api/html/namespacez3py.html
z3 pydoc格式的api文档 http://z3prover.github.io/api/html/z3.html
python api https://z3prover.github.io/api/html/namespacez3py.html 比如 api 命名空间 https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.htm。

更快cpp

Cpp-API接口：https://z3prover.github.io/api/html/group__cppapi.html 这里更新一篇C++的较完整教程example.cpp ：http://www.cs.utah.edu/~vinu/research/formal/tools/notes/z3-notes.html 官方example.cpp文档：https://github.com/Z3Prover/z3/blob/master/examples/c%2B%2B/example.cpp 第二个入门教程也非常不错，里面包含了环境的搭建，例子的说明（其实就是C++的较完整教程example.cpp的说明） cpp项目中如果要使用z3则在install之后要在文件中包含z3++.h头文件，而且在编译参数上要加上-lz3

---

Less is More

私以为，看下面前两个官方教程及其github仓库源码就完全够用了。

• 先过一遍python官方F4(狗头) doc-z3 项目下html的几个网页版本教程其中Basic就是这里这页 http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/guide-examples.htm 中文翻译第一页Basic 及其对应代码仓库https://github.com/TysonSir/z3-solver 。然后剩下来的是符号推理策略strategies-examples,fixedpoint engine主要功能是基本的Datalog引擎，具有关系代数的引擎和基于属性定向可达性算法通用化的引擎,微软F4之4进阶主题
• 微软研究院写的教程入门python全面programmingZ3全场最佳触及本质元认知 https://theory.stanford.edu/~nikolaj/programmingz3.html 本教程提供了一个程序员’满意度模理论求解器Z3的介绍。它描述了如何通过Python脚本语言提供的脚本使用Z3，并描述了Z3内部决策过程的几种算法。它旨在广泛涵盖Z3的几乎所有可用功能以及基础算法的本质。
• smt-lib2.0在线运行官方教程简短教程，其中介绍了Z3的基础功能和简单的SMT-LIB语法。https://rise4fun.com/z3/tutorialcontent/guide 中文翻译 1 中文翻译 2
• 实例中学习，多看几个仓库高玩骚操作：案例PKHG/doc z3-playground ，包括github相关仓库多种实例。

简短的github gist记录下面这些cpp smt2接口用法，smt-lib2.0在线运行官方教程简短教程,F4-4进阶主题,和programmingz3.mdk了解z3py相关概念汇总精要，所需要知道的元认知和结构概览，结合源码本地修改注释，当遇到困惑点Stackoverflow、github issuses搜一下就行。

SMT

• 电子书《SAT/SMT by Example》 使用Z3的python接口精心设计并激发示例的优秀资源 https://sat-smt.codes/main.html 主页，前面官方链接给出下面两张图：

• SATCore：

• SMTCore：
  

前文微软F4教程(狗头)给了下面两张架构图：

符号主义old but fashion的AI ，Z3Overall：

SystemDiagrams：

z3 classes

Z3packages：

• 只需要2个API：z3py命名空间查出现或者需要的函数源码用法结构，比如issubclass()等。
• 类关系看祖先节点网络图往下选继承对象的说明就行,有疑惑就print(type(想了解的对象))进入文档查看。

然后vscode停留看源码，ctrl点进去细细研究就行，python多半只是接口，实际函数实现都封装在底层，最好还是看github源码仓库，其实根据需要Doxygen生成文档也很简单。

更加详细类关系鸟瞰整体结构可以浏览器打开看我之前用pyreverse从源码生成的类UML关联图svg的Z3classes.svg—pip install z3-solver 4.8.10.0版 类图。

logic programming Reasoning符号推理策略strategies

Z3 implements a methodology for orchestrating reasoning engines where “big” symbolic reasoning steps are represented as functions known as tactics大的符号推理步骤写成函数, and tactics are composed using combinators known as tacticals组成成分. Tactics process sets of formulas called Goals被处理的公式集.

符号推理策略strategies-examples,

Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used.

Z3, we say a clause is any constraint of the form Or(f_1, ..., f_n). The tactic split-clause will select a clause Or(f_1, ..., f_n) in the input goal, and split it n subgoals. One for each subformula f_i.

Fixed-point关系代数datalog程序分析验证

fixedpoint engine,主要功能是基本的Datalog引擎，具有关系代数(数据库的代数语义)的引擎和基于属性定向可达性算法通用化的引擎。有些静态语言分析会用到这种就像是prolog查询般的语言，在做符号执行属实是相当神奇的一群人。

---

一般对我而言，入门=知悉相关术语框架，重要概念，遇到问题知道去哪儿找答案，能明白最基本的原理demo是基于什么实现的，有需要的时候可以快速定位找到答案或者源码可供参考部分实现，更多内容看文档API。

妙就妙在"SAT是个筐，什么问题都往里装！"，CSP约束可满足编程问题，妙哉。

因为在做规划类的问题，z3就是一阶语言，构造代数数据结构和Coq，Haskell也没太大差别的样子。面向约束可满足问题的通用规划，进而实现自动程序设计。就像c-like语言盛行靠近底层，很多时候为了效率规划问题求解都是用自动机，多叉树启发式搜索来做的固化，譬如PRP,MyND,但是FOND-SAT的确走的是old but fashion的AI符号演算路子，MiniSAT可以，z3也不是不行。