Z3求解器学习（一）_z3无法求解的约束

引言

---

安装成功后在命令行输入z3 -h可以查看帮助学习如何使用，下面用几个简单的例子熟悉Z3求解器的基本命令（这里我们例子都使用z3 -in的输入形式从标准输入读取表达式）：

例子1：首先写一个简单的可满足条件的例子

(declare-const a Int)
(assert (> a 10))
(check-sat)
(get-model)

declare-const申明一个给定类型的常量（Int型的a)；

assert将一个公式添加到Z3内部堆栈中（a > 10);

check-sat判断堆栈中的公式是否满足。若满足，为返回sat，并且可以通过get-model命令给出一个使得所有公式为真的解释模型；若不满足，则返回unsat。

运行结果为：

sat
(model
  (define-fun a () Int
    11)
)

表示找到一个满足公式的解释a为11。具体格式为：

(define-fun a () Int [val])

表示模型中的a值为[val]。

例子2：一个约束不满足的例子

(declare-const a Int)
(assert (> a 10))
(assert (< a 10))
(check-sat)

运行结果为：

unsat

例子3：一个约束无法求解的例子

(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)

 

unknow

因为对于非线性的实数运算的代价是非常大的，返回的结果可能是unknow或者loop。（疑问：这个在官方给出的在线运行中结果为unknow，但是在我装的z3中给出了sat的结果）。