z3求解器

----------------------持续更新-------------------------------2023.11.4

基于SMTLIB引用

安装：

sudo spt install z3

例：预定义的排序 Bool 是所有布尔命题表达式的排序（类型）。 Z3 支持常用的布尔运算符 and, or, xor, not, => (implication), ite (if-then-else)。双向蕴涵使用等式 = 来表示。以下示例说明如何证明如果 p 蕴含 q 且 q 蕴含 r，则 p 蕴含 r。我们通过证明否定是不可满足的来实现这一点。命令 define-fun 用于定义宏（又名别名）。在此示例中，猜想是我们要证明的猜想的别名。

(declare-const p Bool)

(declare-const q Bool)

(declare-const r Bool)

(define-fun conjecture () Bool

(=> (and (=> p q) (=> q r))

(=> p r)))

(assert (not conjecture))

(check-sat)

将此内容命名为example.smt2

z3 example.smt2

输出结果：unsat

python包引用

安装：

pip install z3-solver

例：

from z3 import *

x, y = Reals('x y')

solve(x-y 3, 3*x-8*y 4)

将此内容命名为test.py

python3 test.py

输出结果：

[y = 1, x = 4]