一、基本语法
Declare-const: 声明给定类型（type/ sort）的常量
declare-fun：声明一个函数
(declare-fun f (Int Bool) Int)：声明一个接收整型和布尔型两个参数的函数，返回int
(define-fun a () Int [val])：是解释。此处表明a的值是val
(define-fun conjecture () Bool
(=> (and (=> p q) (=> q r))
(=> p r)))
(assert (not conjecture)) 此处的define-fun是起到把后面bool表达式定义一个别名的作用
Reset：重置清空所有声明和断言
Simplify：简化表达式
Define-sort：给sort类型的表达式定义一个别名
Declare-sort：声明一种未解释的类型A
(declare-sort A)
(declare-const x A) 声明A类型的常量x
SMT公式的基本构建块我就是常量和函数，而常量实际就是没有参数的函数，所以其所有东西都可以看成一个函数。
(Declare-fun a () int) 等价于 （declare-const b int）<后者是前者的语法糖>
典型的一阶逻辑中，函数都没有副作用，都是定义在输入值上的，所以没有参数的函数实际就是常量
纯一阶逻辑中的函数和常量符号是未解释的或者说自由的，即没有先验解释附加之上。所以+号不一定代表加法，任何和其兼容的都可以
; defining my own division operator where x/0.0 == 0.0 for every x.
(define-fun mydiv ((x Real) (y Real)) Real
(if (not (= y 0.0))
(/ x y)
0.0))
二、 位向量
现代CPU和主流的编程语言都是基于固定大小的位向量实现的算法。位向量理论允许对无符号/有符号两类算术的语义进行精确建模。
位向量常量可能是二进制、十进制和十六进制。二进制格式的位向量#b010大小为3，十六进制格式位向量#x0a0大小是12。必须为十进制格式的位向量字面量指定大小，因为同一大小的十进制数用不同进制表示，位数可能不同，如下示例：
(display #b0100) //4
(display (_ bv20 8)) //大小为8，数值为20的十进制数，表示为是#x14
(display (_ bv20 7)) //大小为7，数值为20的十进制数，表示为是#b0010100
(display #b0100) （_bv4 4）
操作包括：加减乘除，模、求余、左右移（有无符号）、与或非、大小等于
数组：
(Select a i)返回数组a中处于位置i的数据；
(store a i v)返回位置i处值为v的数组a
(declare-const a1 (Array Int Int))：声明int类型的数组
将所有索引映射到某个固定值的数组可以在Z3中使用const构造来指定。它从数组的范围类型中获取一个值，然后创建一个数组。Z3不能仅通过检查实参类型来推断const构造函数必须返回哪种类型的数组。因此，必须使用限定标识符(如const(数组T1 T2))。下面的示例定义了一个只包含1的常量数组。
(declare-const all1 (Array Int Int))
(declare-const a Int)
(declare-const i Int)
(assert (= all1 ((as const (Array Int Int)) 1))) //all1数组中所有数的值为1
(assert (= a (select all1 i))) //SAT
Array的解释特别像函数的解释，都是 用define-fun的方式
三、 Tatics
Tatics是一系列z3内置的函数结合而成的，可以通过apply命令将多个内置的tatics结合在一起（比如simplify和solve-eqs）。前者用于简化表达式，后者采用高斯消去法来消去变量求解方程。
(apply (then simplify solve-eqs)) //连接器them将simplify应用于输入目标，然后solver-eqs简化simplify产生的每个子公式中的多余变量
split-clause：将约束分为多个子约束
(then t s) applies t to the input goal and s to every subgoal produced by t.
(par-then t s) applies t to the input goal and s to every subgoal produced by t in parallel.
(or-else t s) first applies t to the given goal, if it fails then returns the result of s applied to the given goal.
(par-or t s) applies t and s in parallel until one of them succeed. The tractic fails if t and s fails
(repeat t) Keep applying the given tactic until no subgoal is modified by it.
(repeat t n) Keep applying the given tactic until no subgoal is modified by it, or the num
ber of iterations is greater than n.
Check
-sat-using类似于check-sat，但其不利用z3自带的solver而是用tatics里提供的tatic
四、Sequence
本节描述Z3对字符串、序列和正则表达式的处理。
Z3仅使用一个不完整的启发式求解器解决字符串等式(尽管存在完整的过程)，长度和序列(以及正则表达式)的完整组合无论如何都是不可决定的。
string是变量中内在的名字 (declare a String)
(assert (= (str.++ b a) (str.++ "abc" b)))//是否存在连接到“ abc”和后跟b的字符串a和b。
字符串操作：
五、Optimization
该功能使用户可以直接使用Z3制定目标函数。 引擎盖下有用于解决SMT公式，MaxSMT及其组合的线性优化问题的方法组合。
算术优化》》
(Maximize t)：调用check-sat同时产生值最大的解释
(minimize t): 调用check-sat同时产生值最小的解释
无界对象：z3中的最大可以是无穷（00），最小可以使负无穷（-00）
六、题外话
1、若使用z3实现复杂的功能还是使用python或者Haskell, 这些语言提供了对z3更强大的API；
2、虽说C/C++可能执行的比python快，但C++使用z3有很大的局限性,也比较麻烦，所有类型都要声明。
3、当然可以选择C++与python结合，python写约束求解的脚本，C++调用python脚本
