title: How to determine the number of solutions of a given instance using Mathsat
body: <p>Mathsat supports the command <code>check-allsat</code> and Z3 does not support it.  Please consider the following example:</p>
  
  <pre><code>(declare-fun m () Bool)
  (declare-fun p () Bool)
  (declare-fun b () Bool)
  (declare-fun c () Bool)
  (declare-fun r () Bool)
  (declare-fun al () Bool)
  (declare-fun all () Bool)
  (declare-fun la () Bool)
  (declare-fun lal () Bool)
  (declare-fun g () Bool)
  (declare-fun a () Bool)
  (define-fun conjecture () Bool
  (and (= (and (not r) c) m) (= p m) (= b m) (= c (not g)) (= (and (not al) (not all)) r)
  (=(and la b) al) 
  (= (and al la lal) all) (= (and (not g) p a) la) (= (and (not g) (or la a)) lal)))
  (assert conjecture)
  (check-allsat (m p b c r al all la lal g a))
  </code></pre>
  
  <p>Executing this code with mathsat all the consistent assignments are obtained.  The question is how to determine the number of such consistent assignments using Mathsat?</p>