[SMT-LIB] Linear arithmetic and quantifiers

[Michal Moskal]

On Thu, Dec 10, 2009 at 08:07, Paul Jackson <pbj at inf.ed.ac.uk> wrote:
>
> Hi,
>
> with linear quantified sublogics such as AUFLIA and AUFLIRA, would be it
> be possible to allow non-linear arithmetic within quantified
> expressions?
>
> There are common situations when this would increase the utility of
> solvers that at heart only handle linear arithmetic, because many
> instantiations of interest would all be linear.
>
> For example, I have quite a few examples of benchmarks with axioms
> concerning division such as:
>
>  All x,y:Int. 0 <= x & 0 < y   =>     y * (x div y) <= x
>
> and instances of div of form
>
>  a div k
>
> where k is an natural number literal.


I think the current practice was to put them as non-linear (there is
the UFNIA division now).

For quantified queries solvers are going to be incomplete anyhow, so
there is really nothing to prevent use of a linear solver on a
potentially non-linear problems.

I was also tempted to think that this "essentially linear" fragment
would need some special treatment, but it now seems sort of arbitrary.

   Michał