Quantifier elimination for multilinear rational arithmetic in Z3

0
votes

As far as I understand, Z3, when encountering quantified linear real/rational arithmetic, applies a form of quantifier elimination described in Bjørner, IJCAR 2010 and more recent work by Bjørner and Monniaux (that's what qe_sat_tactic.cpp says, at least).

I was wondering

  1. Whether it still works if the formula is multilinear, in the sense that the "constants" are symbolic. E.g. ∀x, ax≤b ⇒ ax ≤ 0 can be dealt with by separating the cases a<0, a=0 and a>0. This is possible using Weispfenning's virtual substitution approach, but I don't know what ended up being implemented in Z3 (that is, whether it implements the general approach or the one restricted to constant coefficients).

  2. Whether it is possible, in Z3, to output the result of elimination instead of just solving for one model. There might be a Z3 tactic to do so but I don't know how this is supposed to be requested.

  3. Whether it is possible, in Z3, to perform elimination as described above, then use the new nonlinear solver to obtain a model. Again, a succession of tactics might do the trick, but I don't know how this is supposed to be requested.

Thanks.

1
z3smt
If I understand your correct, and read your name (+link) correct, you are actually asking some very specific question about an method you described yourself. Sorry we cant tell you what your work can and what not. Furter, the question seem not to be a specific programming questions. (In case I misunderstood you it is a hint for you to reformulate it). – flolo
David, flolo may have a point. We can/should discuss this issue by email, or use the discussion session in the Z3 website: z3.codeplex.com/discussions – Leonardo de Moura
fiolo, I just don't know what ended up being implemented in Z3; there is a big difference between describing an algorithm and knowing how it ended up in a system you did not design. ;-) I also don't know the proper sequence of requests to pass to Z3 to ask for linear quantifier elimination then general nonlinear solving. I also don't know if there is any way to request Z3 to output the result of quantifier elimination... – David Monniaux

1 Answers

0
votes

After long travels (including a travel where I met David at a conference), here is a short summary to answer the questions as they are posed.

  1. There is no specific support for multi-linear forms.
  2. The 'qe' tactic produces results of elimination, but may as a side-effect decide satisfiablity.
  3. This is a very interesting problem to investigate, but it is not supported out of the box.