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]