https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction

https://z3prover.github.io/papers/programmingz3.html

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/b
  • eq(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,如果失败则用 s
  • Repeat(t,n) 重复用 t 到没有被修改过或者超过 n 次了(可省略 n 参数)
  • TryFor(t, ms) 尝试 t,有个超时设定
  • With(t, params) 有指定参数

可以通过方法 .solver() 转化为一个求解器,之后和正常求解器一样使用

或者在交互式命令里也可以用 solve_using(bv_solver,...)