安装

数据类型

from z3 import *
  • integer 整型

    x = Int('x')
    x, y = Ints('x y')
  • Real 实数

    x = Real('x')
    x, y = Reals('x y')
    • ```python
      x = Real(‘x’)
      sovle(3*x == 1)

      输出

      [x = 1/3]


      - ```python
      x = Real('x')
      # 启用精度
      set_option(rational_to_decimal=True)
      solve(3*x == 1)
      # 输出
      # [x = 0.3333333333?]
    • ```python
      x = Real(‘x’)

      设置精度

      set_option(precision=30)
      solve(3*x==1)

      输出

      [x = 0.333333333333333333333333333333?]


      过程set_option用于设置z3的执行环境。它用于设置全局配置选项, 如以何种方式来显示结果, 选项precision=30, 设置十进制显示结果中的小数位数。0.3333333333?中的?标志输出被截断。

      - Bool 布尔值

      ```python
      p = Bool('p')
      p, q = Bools('p q')

    z3支持布尔运算符:And, Or, Not, Implies(蕴涵), If(if-then-else)。等价使用==来表示。

    # 以下例子显示了如何求解简单的布尔条件约束
    p = Bool('p')
    q = Bool('q')
    r = Bool('r')
    solve(Implies(p, q), r == Not(q), Or(Not(p), r))
    # 输出
    # [q = False, p = False, r = True]

    # python布尔常量True和False可以创建z3的布尔表达式
    p = Bool('p')
    q = Bool('q')
    print And(p, q, True)
    print simplify(And(p, q, True))
    print simplify(And(p, False))
    # 输出
    # And(p, q, True)
    # And(p, q)
    # False

    # 以下例子结合了多项式和布尔约束
    p = Bool('p')
    x = Real('x')
    solve(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))
    # 输出
    # [x = -1.4142135623?, p = False]

Simplify

Z3公式/表达式简化器

  • 输入:
x = Int('x')
x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
  • 输出:
3 + 3*x + y
Not(y <= -2)
And(x >= 2, 2*x**2 + y**2 >= 3)

表达式分析

z3提供遍历表达式的函数

  • 输入:

    x = Int('x')
    y = Int('y')
    n = x + y >= 3
    print "num args: ", n.num_args()
    print "children: ", n.children()
    print "1st child:", n.arg(0)
    print "2nd child:", n.arg(1)
    print "operator: ", n.decl()
    print "op name: ", n.decl().name() # str
  • 输出

    num args:  2
    children: [x + y, 3]
    1st child: x + y
    2nd child: 3
    operator: >=
    op name: >=

整理解

a1 = IntVector('x', 32)

if s.check() == sat:
m = s.model()
res = ""
for i in range(32):
res += chr(m[a1[i]].as_long())

print(res)

更加优雅的写法(python3.6以后支持f-string)

m = s.model()
s = ''
for i in range(10):
v = m[x[i]].as_long()
s += f'{v:x}'
print(s)