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,...)