title: Take out common variables using Z3
body: <p>I have a formlua in DNF form, say:</p>
  
  <pre><code>abcx + abcy + abz
  </code></pre>
  
  <p>Is there any way to take out the common variables, to get the follwing formula:</p>
  
  <pre><code>ab (cx + cy + z)
  </code></pre>
  
  <p>A followup question, can it be done recursively, like</p>
  
  <pre><code>ab ( c(x+y) + z) 
  </code></pre>