求解器Z3（未完，更新中）_z3求解器中文手册

定义a、b，条件a>b,b>1。那么它就会告诉你有解，a=3，b=2是一个解。

定义a、b，条件a>b,b>a。那么它就会告诉你无解。

当然，实际工作中用到的条件会复杂得多，人们不可能通过人脑完成判断，这时需要用计算机的求解器完成。

---

目前求解器有yices，Z3等，都符合SMT-LIB standard标准。

先来一个简单的例子：

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

第一行定义了一个int类型的a。

第二行定义了一个参数为int和Bool的返回值为int的函数f。

第三行给定条件a>10。

第四行给定条件f(a,true)<100。

第五行检查是否有解。

第六行得到一个解的模型，或者说特解。