How to make quantifier elimination using Z3-Py?

Question

I am trying to obtain a quantifier-free formula using the following code:

S, E, I, R = Reals('S E I R')
b, n, s, g, m = Reals('b n s g m')
SS = Then('qe', 'smt').solver()
SS.add(Exists([S,E,I,R], And(m+g*R-m*S-b*I*S == 0,
   b*I*S-(m+s)*E==0, s*E-(n+m)*I==0, n*I-(m+g)*R==0,
   S > 0, I > 0, E > 0, R >0)))
SS.add(b > 0, n > 0, s >0 , g >0, m>0)
print SS
print SS.check()

but I am obtaining the output:

unknown

Please can you tell me what happens with my code? Many thanks.

Answer 1

Quantifier elimination works just for additive arithmetic. It does not eliminate quantifiers from formulas where variables are multiplied with other variables. This is why quantifier elimination does not produce a reduced formula for your problem.

Notice, however, that a formula Exists x . phi[x] is equi-satisfiable to a formula of the form phi[x], so it should not be required to put an existential quantifier on your formula. The nlsat strategy handles quantifier-free formulas over the reals with multiplication.