title: Converting Z3 CNF formula into list-of-lists representation using Z3Py
body: <p>Given a Z3 formula in CNF, is it possible to convert it into a list-of-lists representation using Z3Py? I'd like to do this for easier access and manipulation of literals. If Python were a functional language, I might do something like</p>
  
  <pre><code>def cnf2list(fm) :
    match fm with
    | And(P,Q) -&gt; cnf2list(P) + cnf2list(Q)
    | P -&gt; clause2list(P)
  
  def clause2list(fm) :
    match fm with
    | Or(P,Q) -&gt; clause2list(P) + clause2list(Q)  
    | P -&gt; [P]
  </code></pre>
  
  <p>But I'm not sure I can do this in Python. Is it possible to perform pattern matching like above (or use some entirely different method) to obtain a list-of-lists representation of a Z3 CNF formula?</p>