https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction
Solver() 命令创建一个通用求解器
add() 添加约束
check() 方法判断在当前约束下是否仍有可能情况满足，如果有则输出 sat，否则则是 unsat，也可能无法求解约束返回 unknown
pop 和 push 可以像栈一样管理约束
只能求解非线性多项式（x 不能在指数上之类的）
The command check returns sat when Z3 finds a solution for the set of asserted constraints. We say Z3 satisfied the set of constraints. We say the solution is a model for the set of asserted constraints. 当 Z3 找到一组断言约束的解时，命令 check 返回 sat 。我们称 Z3 满足这组约束。我们称该解是这组断言约束的模型 。
m = s.model()
for d in m.decls():
print("%s=%s"%(d.name(),m[d]))
# or
s = Solver()
s.add(soduku_c+instance_c)
if s.check() == sat:
m = s.model()
r = [[m.eval(X[i][j])for i in range(9)] for j in range(9)]
print_matrix(r)
else:
print("failed")如此得到 model 里的解
与 C、C++、C#、Java 等编程语言不同，Z3 中不区分有符号和无符号位向量作为数字的表示。相反，Z3 提供了特殊的算术运算有符号版本，这些运算会根据位向量被视为有符号还是无符号而产生不同结果。在 Z3Py 中，运算符 < 、 <= 、 > 、 >= 、 / 、 % 和 >>; 对应有符号版本。相应的无符号运算符为 ULT 、 ULE 、 UGT 、 UGE 、 UDiv 、 URem 和 LShR 。运算符 >> 表示算术右移，而 << 表示左移。逻辑右移的运算符是 LShR
z3 里的函数
x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())
solve(f(f(x)) == x, f(x) == y, x == 3+y)Sort 是类型的意思，需要指定输入和输出的类型。这里相当于是解出了抽象函数的一个实例
f=Function('f',IntSort(),RealSort(),BoolSort())
print(f.name())
print(f.range())
print(f.arity())
for i in range(f.arity()):
print(f"domain({i}):{f.domain(i)}")
print(f(x+1,x))
print(f(x+1,x).decl())
print(eq(f(x+1,x).decl(),f))可以这样理解：
f本身是一个定义了函数签名的声明，指定了函数的名称、参数类型和返回类型f(x+1,x)是使用声明f创建的具体表达式，带有具体的参数f(x+1,x).decl()是从这个具体表达式提取出它所基于的函数声明
最后一行 eq(f(x+1,x).decl(),f) 返回 True 就证明了这一点 - 函数应用表达式 f(x+1,x) 的声明与原始函数声明 f 是相同的。
另一种理解方式是：声明定义了符号的 ” 模板 “，而表达式是这个模板的具体实例。无论你用什么参数调用函数，得到的表达式都共享同一个基础声明。
替换
x, y = Ints('x y')
f = Function('f', IntSort(), IntSort(), IntSort())
g = Function('g', IntSort(), IntSort())
n = f(f(g(x), g(g(x))), g(g(y)))
print(n)
print(substitute(n, (g(g(x)), y), (g(y), x+1)))一些神奇的函数
Distinct每个参数保证不相等If如果 a，则 b ，否则 c。这里可以填 True 之类的东西来忽略某一项pp打印某个东西Implies如果 a 为真，b 一定为真，其他不保证Q有理数 a/beq(n1, n2)在 n1 和 n2 为同一 AST 时返回 True 。这是一个结构性的测试。model.check(bools)可以额外加入一定成立的 bool 值is_true()转换为 python 的 bool
数组
声明 Array('A',IntSort(),IntSort())
可以找下标 Select(A,x) 或者存储（返回一个新的数组结果）Store(A,x,y)==A
K(s, v) 表示全部 s 类型的一个数组，它所有元素的值都为 v
数据类型
Int(name) 和 Real(name) 分别是 Const(name, IntSort()) 和 Const(name, RealSort()) 的简写
Datatype('List') 声明了一个“占位符”，用于存放构造函数和访问器的声明
declare('cons', ('car', IntSort()), ('cdr', List)) 声明了名为 cons 的构造函数，该函数利用一个整数和一个 List 构建新的 List，同时它还声明了访问器 car 和 cdr 。访问器 car 提取 cons 单元的整数值，而 cdr 则提取 cons 单元的列表 V
其实按照现代程序的习惯，这就是指定了一个只能对每个成员赋值的一个构造函数，如上则是声明了 car 和 cdr 两个成员（通过
List.car访问），然后他们的类型是 Int 和 List（类本身），这个构造函数的名字叫 cons
List = Datatype('List')
List.declare('cons',
('car', IntSort()),
('cdr', List))
List.declare('nil')
List = List.create()
print(is_sort(List))
cons = List.cons
car = List.car
cdr = List.cdr
nil = List.nil
print(nil)
print(is_func_decl(cons))
print(is_expr(nil))
l1 = cons(10, cons(20, nil))
print(l1)
print(simplify(cdr(l1)))
print(simplify(car(l1)))
print(car(l1))
print(simplify(l1 == nil))z3 支持运算符重载
看到这里就感觉和 rust 的枚举差不多，下面还就真用枚举来描述了：有语法糖：
Color, (red, green, blue) = EnumSort('Color', ('red', 'green', 'blue'))
##
Color = Datatype('Color')
Color.declare('red')
Color.declare('green')
Color.declare('blue')
Color = Color.create()量词
f = ForAll([x, y], f(x, y) == 0)软约束
p1,p2,p3=Bools('p1 p2 p3')
x,y=Ints('x y')
s=Solver()
s.add(
Implies(p1,x>10),
Implies(p1,y>x),
Implies(p2,y<5),
Implies(p3,y>0),
)
print(s)
print(s.check(p1,p2,p3))
print(s.unsat_core())
print(s.check(p2,p3))
print(s.model())自定义求解策略
g = Goal()
g.add(x > 0, y > 0, x == y + 2)设定目标
Tactic('simplify')化简Tactic('solve-eqs')使用高斯消元消除变量Tactic('split-clause')拆分 子句
describe_tactics() 提供所有内置策略的描述 常用的 z3 策略
x, y = Reals('x y')
g = Goal()
g.add(x > 0, y > 0, x == y + 2)
print(g)
t1 = Tactic('simplify')
t2 = Tactic('solve-eqs')
t = Then(t1, t2)
print(t(g))如此应用策略
Then(t, s)首先用 t，然后对生成的每个子结果用 s 处理OrElse(t,s)首先用 t，如果失败则用 sRepeat(t,n)重复用 t 到没有被修改过或者超过 n 次了（可省略 n 参数）TryFor(t, ms)尝试 t，有个超时设定With(t, params)有指定参数
可以通过方法 .solver() 转化为一个求解器，之后和正常求解器一样使用
或者在交互式命令里也可以用 solve_using(bv_solver,...)