title: Z3Py example from checking beliefs in dynamic networks
body: <p>For a better understanding of Z3 (or more specific of Z3Py) I wanted to implement the straight forward example from the Paper <a href="https://www.usenix.org/node/189019" rel="nofollow noreferrer">Checking Beliefs in dynamic Networks</a>. </p>
  
  <p>Here is my working code:</p>
  
  <pre><code>from z3 import *
  
  fp = Fixedpoint()
  
  dst = BitVec('dst', 3)
  src = BitVec('src', 3)
  dst_next = BitVec('dst_next', 3)
  src_next = BitVec('src_next', 3)
  
  fp.declare_var(dst, src, dst_next, src_next)
  
  rels = {}
  
  for c in ['A', 'R1', 'R2', 'R3', 'B', 'D']:
      f = Function(c, BitVecSort(3), BitVecSort(3), BoolSort())
      rels[c] = f
      fp.register_relation(f)
      fp.set_predicate_representation(f, 'doc')
  
  # Guards
  g12 = And(Extract(2, 1, dst) == 0b10, Extract(2, 1, dst) == 0b01)
  g13 = And(Not(g12), Extract(2, 2, dst) == 0b1)
  g2b = Extract(2, 1, dst) == 0b10
  g3d = Extract(2, 2, src) == 0b1
  g32 = And(Not(g3d), Extract(2, 2, dst) == 0b1)
  ld = And(src_next == src, dst_next == dst)
  set0 = And(src_next == src, dst_next == dst &amp; 0b101)
  
  # Relations
  fp.rule(rels['R1'](dst_next, src_next), And(rels['R2'](dst, src), g12, ld))
  fp.rule(rels['R1'](dst_next, src_next), And(rels['R3'](dst, src), g13, ld))
  fp.rule(rels['R2'](dst_next, src_next), And(rels['B'](dst, src), g2b, ld))
  fp.rule(rels['R3'](dst_next, src_next), And(rels['D'](dst, src), g3d, ld))
  fp.rule(rels['R3'](dst_next, src_next), And(rels['R2'](dst, src), g32, set0))
  fp.rule(rels['A'](dst, src), rels['R1'](dst, src))
  
  fp.fact(rels['B'](dst, src))
  
  #print(fp)
  print(fp.query(rels['A'](dst, src)))
  print(fp.get_answer())
  </code></pre>
  
  <p>This prints the correct Answer:</p>
  
  <pre><code>sat
  Or(And(Var(0) == 5, Var(1) == 2),
     And(Var(0) == 4, Var(1) == 2),
     And(Var(0) == 4, Var(1) == 3),
     And(Var(0) == 5, Var(1) == 1),
     And(Var(0) == 4, Var(1) == 0),
     And(Var(0) == 5, Var(1) == 3),
     And(Var(0) == 5, Var(1) == 0),
     And(Var(0) == 4, Var(1) == 1))
  </code></pre>
  
  <p>So my question is now can Z3Py do some Bitvector "compression" of the result and print something like <code>And(Var(0) == 10*, Var(1) == 0**</code> ? And if I wanted to get all packets from B to A over R3 can I simply <code>fp.query(rels['A'](dst, src), rels['R3'](dst, src))</code> or do I have to remove the relation R2 to R1?</p>
  
  <p>Thanks!</p>