In Z3 (Python), I found a way to see which are the models of a formula. See the post Z3: finding all satisfying models and a piece of code of it below:
a = Int('a')
b = Int('b')
s = Solver()
s.add(1 <= a)
s.add(a <= 20)
s.add(1 <= b)
s.add(b <= 20)
s.add(a >= 2*b)
while s.check() == sat:
print s.model()
s.add(Or(a != s.model()[a], b != s.model()[b]))
Now, I would like to count how many models are there. Of course, I could add a counter in the loop:
def count_models (s):
counter = 0
while s.check() == sat:
print s.model()
s.add(Or(a != s.model()[a], b != s.model()[b]))
counter = counter + 1
return counter
However, I would like to know whether there is any native function to do so. Something like s.count_models. Any help?
No. This is the only way as z3 stands today. The way to count models is to generate each one-by-one and add them up. Any internal method would essentially do the same.
Keep in mind that if you have an unbounded domain (such as unbounded integers as you have in your example), there might be infinite number of models; thus your loop is not always guaranteed to terminate.
Model counting in SAT and SMT are both research problems. Here're a couple of references for further reading:
In the SAT context, see: https://www.cs.cornell.edu/~sabhar/chapters/ModelCounting-SAT-Handbook-prelim.pdf.
In the SMT context, see: https://link.springer.com/article/10.1007/s00236-017-0297-2
Generating all models in z3 can be done faster than the algorithm you've used. See https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-blocking-evaluations for details. The idea is still to enumerate, but using better splits of the search-space instead of randomly walking it.