Model counting in Z3Py

Question

I am trying to count the number of satisfying assignments by Z3. I am wondering if Z3 provides such information. If so, how can I count models in Z3 and particularly in Z3Py?

Answer 1

While Taylor's answer will give you the number of satisfying assignments, it will iterate over all of them. In principle, it is possible to do it without such an expensive iteration, but Z3 does not offer it.

There are efficient model counters for propositional logic, the same language used in SAT (search for sharpSAT to find such a system), but as far as I know there is no available model counter modulo theories.

Answer 2

No, such information is not available by default. However, you could easily implement this (assuming finite number of models) in any of the APIs by combining the model generation capability with adding assertions to prevent future assignments from being assigned the same values as past models. See the following answer for a Z3py script accomplishing this:

Z3: finding all satisfying models

To count the models, simply add a counter to the loop until it becomes unsat, and this will give you the number of models.