title: Z3py: Convert a Z3 formula to clauses used by picosat
body: <p>LINKS:<br>
  <a href="http://z3.codeplex.com/" rel="noreferrer">Z3 theorem prover</a><br>
  <a href="https://pypi.python.org/pypi/pycosat" rel="noreferrer">picosat with pyhton bindings</a>  </p>
  
  <p>I've used Z3 as a SAT-solver. For larger formulae there seem to be performance issues which is why I wanted to check out picosat to see whether it's a faster alternative.
  My existing python code generates a propositional formula in z3 syntax:</p>
  
  <pre><code>from z3 import *
  
  import pycosat
  from pycosat import solve, itersolve
  
  #
  #1 2  3  4  5  6  7   8  (variable names in picosat are numbers!)
  #
  C, G, M, P, R, S, SN, B = Bools('C G M P R S SN B')
  C = (And(*(S,Or(Not(S),P),Or(Not(P),S),Or(Not(P),B),Or(Not(C),P),Or(Not(G),P),Or(Not(M),P),Or(Not(R),P),Or(Not(SN),P),Or(Not(B),P),True,Not(False),Or(R,SN,B,G,M,C,True))))
  
  # formula in Z3:
  f = simplify(C)
  
  print f 
  </code></pre>
  
  <p><strong>OUTPUT / RESULT</strong></p>
  
  <pre><code>And(S,
      Or(Not(S), P),
      Or(Not(P), S),
      Or(Not(P), B),
  
      Or(Not(C), P),
      Or(Not(G), P),
      Or(Not(M), P),
      Or(Not(R), P),
      Or(Not(SN), P),
      Or(Not(B), P))
  </code></pre>
  
  <p>Picosat however uses lists/arrays of numbers, as shown in the following example ("clauses1": 6 refers to variable P, -6 means "not P" etc.):</p>
  
  <pre><code>import pycosat
  from pycosat import solve, itersolve
  #
  # use pico sat
  #
  nvars = 8
  clauses =[
      [6],
      [-6, 4],   ##  "Or(Not(S), P)" from OUPUT above
      [-4, 6],
      [-4, 8],
      [-1, 4],
      [-2, 4],
      [-3, 4],
      [-5, 4],
      [-7, 4],
      [-8, 4]]
  
  #
  # efficiently find all models of the formula
  #
  sols = list(itersolve(clauses, vars=nvars))
  print "result:"
  print sols
  print "\n\n====\n"
  </code></pre>
  
  <p>What do you recommend as a simple solution to convert a Z3 variable (like the varaible "f" from the code example) representing a formula in CNF into the forementioned format picosat uses to represent formulae in CNF? I really tried to use the python API of Z3, however the documentation was not sufficient to solve the problem by myself.</p>
  
  <p>(Please note the example above merely illustrates the concept. The formula represented by variable C would be dynamically generated and would be too complex to be processed efficiently by z3 directly)</p>