z3-solver模板

 1 z3-solver
 2 from z3 import *
 3 Group= [BitVec('solveL%d'%i,8) for i in range(0,2)]
 4 //Group=['solveL1','solveL2','solveL3'……]
 5 #a,b=Ints('a b')//Real()
 6 #''内的为求解出的解的名字，=前的为py代码里的名字，一般相同即可
 7 solve=Solver()
 8 solve.add()
 9 if solve.check()==sat:
10     print solve.model()
11 //
12 //多解的写法
13 while solve.check()==sat:
14     m=solve.model()
15     print m
16     solve.add(Or(T[0]!=m[T[0]],T[1]!=m[T[1]]))
17 //注意递归解题

标签：Group,solver,add,solve,sat,check,模板,z3
来源： https://www.cnblogs.com/yiye-0x11/p/15086764.html