解析器

>>> state = p.factory.entry_state() >>> one = state.solver.BVV(1,64) >>> one <BV64 0x1> >>> two = state.solver.BVV(100,64) >>> two <BV64 0x64> >>> three = state.solver.BVV(9,27)//生成位向量 >>> three <BV27 0x9> >>> two + one <BV64 0x65> >>> three.zero_extend(64-27)//修改位向量的长度，用零扩展位向量的高位 <BV64 0x9> >>> x = state.solver.BVS('x',64) >>> y = state.solver.BVS('y',64) >>> x <BV64 x_0_64> >>> y <BV64 y_1_64> >>> x.op//运算的属性 'BVS' >>> x.args//参与运算的操作数 ('x_0_64', None, None, None, False, False, None) >>> x + one <BV64 x_0_64 + 0x1> >>> (x + one) / 2 <BV64 (x_0_64 + 0x1) / 0x2> >>> x + one <BV64 x_0_64 + 0x1> >>> (x + one) / 2 <BV64 (x_0_64 + 0x1) / 0x2> >>> x == 1 <Bool x_0_64 == 0x1> >>> x + 1 <BV64 x_0_64 + 0x1> >>> x <BV64 x_0_64> >>> x > 5 <Bool x_0_64 > 0x5> >>> one > 5 <Bool False> >>> m = x > y >>> q = one == 1 >>> state.solver.add(x > y) [<Bool x_0_64 > y_1_64>] >>> state.solver.add(y > 10)//约束条件 [<Bool y_1_64 > 0xa>] >>> state.solver.eval(x)//eval方法将位向量转化为python的int类型 13L >>> state.solver.eval(y)//返回的值就在约束条件之间的随机值 12L >>> input = state.solver.BVS('input',64) >>> answer = input + 1 >>> output = 100 >>> state.solver.add(answer == output) [<Bool (input_0_64 + 0x1) == 0x64>] >>> state.solver.eval(input)//也可以用来找到一个产生指定输出的输入但是不同的方程要放不同的类 99L >>> state.satisfiable()//检查有无解，跟z3有点像 True

solver.eval(expression) 将会解出一个可行解 solver.eval_one(expression)将会给出一个表达式的可行解，若有多个可行解，则抛出异常。 solver.eval_upto(expression, n)将会给出最多n个可行解，如果不足n个就给出所有的可行解。 solver.eval_exact(expression, n)将会给出n个可行解，如果解的个数不等于n个，将会抛出异常。 solver.min(expression)将会给出最小可行解 solver.max(expression)将会给出最大可行解