0x17 Z3模块的学习

Author Avatar
张Mini Nov 28, 2018
  • Read this article on other devices

Z3模块的学习

  • Solver()命令创建一个通用求解器,可以使用add函数添加约束条件

  • check()函数解决声明的约束条件,sat表示找个某个合适的解,unsat表示无解

  • model()列出求解结果

  • 可以使用’Int’,’Real’,’BitVec’等声明一个整数或实数变量,也可以申明一个变量数组
    如:

    >>> message=[Int('flag%d' %i)for i in range(0,10)]
    >>> message
    [flag0, flag1, flag2, flag3, flag4, flag5, flag6, flag7, flag8, flag9]
    
  • 当需要进行二进制数据有关的运算时,需要用到BitVec类型,比如只有BitVec变量可以进行异或运算,BitVec是无符号数,Int是有符号数。Int类型无法表示过大的数,使用BitVec(‘x’,64)表示可以声明在64bit之内的变量。还有Real型变量,可以解出所有有理数