1

I want to know if Z3 can show equivalent formulas after Quantifier Elimination.

Example (exists k) (i x k) = 1 and k > 5 is equivalent to

i > 0 and 5 i - 1 < 0.

Here, quantifier k has been eliminated.

Is this possible?

Thanks, Kaustubh.

Kaustubh Nimkar
  • 159
  • 1
  • 6

2 Answers2

2

Yes, Z3 can check whether two formulas are equivalent. To check whether p and q are equivalent. We must check whether (not (iff p q)) is unsatisfiable.

Your example uses nonlinear arithmetic i*k. The quantifier elimination module in Z3 has limited support for nonlinear real arithmetic. It is based on virtual term substitution, which is not complete. However, it is sufficient for your example. We must enable the quantifier elimination module in Z3, and the nonlinear extensions (i.e., virtual term substitution).

Here is how we can encode your example in Z3: http://rise4fun.com/Z3/rXfi

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
1

In general, the result of eliminating quantifiers can be obtained. For instance by entering the following into rise4fun:

(declare-const i Real)
(assert (exists ((k Real)) (and (= (* i k) 1.0) (> k 5.0))))
(apply qe)

This case involves non-linear arithmetic, and Z3 does not eliminate the quantifier.

Josh Berdine
  • 326
  • 1
  • 1
  • The support for nonlinear arithmetic is not enabled by default in the quantifier elimination module. That is why Z3 does not eliminate the quantifier in the script above. Here is the same example, with nonlinear support enabled: http://rise4fun.com/Z3/qrW1 – Leonardo de Moura May 01 '12 at 17:38
  • I see, my mistake. For reference, I tried using set-option, but that didn't work: http://rise4fun.com/Z3/vm7M. – Josh Berdine May 01 '12 at 17:47
  • Many thanks Josh and Leonardo. I have few more questions, I am asking them separately as a new thread. – Kaustubh Nimkar May 03 '12 at 17:46