Size of constraints in the Z3 Solver()

Question

Is there a way for us to get how many constraints were added into the solver? For example, we initialize a z3 solver s = Solver() and then adding constraints to it using s.add(). How can we get the number of constraints which were finally added to the solver?

It's customary to either "accept" answers or indicate why they don't work for you with a comment so other users have some feedback on whether the issue is resolved. — alias

alias alias · Accepted Answer · 2019-01-08T22:58:55

You can use the assertions method:

from z3 import *

s = Solver()

i = Int('i')
s.add (i > 1)
s.add (i < 12)

print s.assertions()
print len(s.assertions())

This prints:

[i > 1, i < 12]
2

Size of constraints in the Z3 Solver()

1 Answers