[SMT-LIB] Mixing Integers and Reals in SMT2 formulas

[Levent Erkok]

Thanks for pointing that out Jochen. I wasn't aware of this extension.
Equality is typically treated quite differently then other operators
though, so I'm curious if Cesare et. al., meant "=" to be part of that or
not. It'd be great if that was clarified in the document.

-Levent.


On Sat, Jul 19, 2014 at 12:48 AM, Jochen Hoenicke <
hoenicke at informatik.uni-freiburg.de> wrote:

> Hello,
>
> 2014-07-19 8:22 GMT+02:00 Martin Brain <martin.brain at cs.ox.ac.uk>:
> > On Fri, 2014-07-18 at 11:16 -0700, Levent Erkok wrote:
> >> I think the point is that such queries should be rejected by compliant
> >> solvers. Or, contrapositively, any solver not rejecting such a query is
> >> non-compliant with the standard. This follows from the core theory
> >> definition in
> >> http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf,
> >> page 30; which requires equality to receive the same "sort" for its
> >> arguments.
> >
> > The problem with requiring all compliant solvers to reject non-compliant
> > input is that it prevents developers adding their own extensions.  As I
> > understand it, SMT-LIB is written to support authors in further
> > developing and extending the language.
>
> I just wanted to point out, that the syntax may be officially correct.
> There is an extension in AUFLIRA and AUFNIRA.
>
> From http://smtlib.cs.uiowa.edu/logics/AUFLIRA.smt2
>
>  "For every operator op with declaration (op Real Real s) for some sort s,
>   and every term t1, t2 of sort Int and t of sort Real, the expression
>   - (op t1 t) is syntactic sugar for (op (to_real t1) t)
>   - (op t t1) is syntactic sugar for (op t (to_real t1))
>   - (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_real t2))
>  "
>
> One can now argue whether the equality symbol is declared as (= Real
> Real Bool), since it is really a polymorphic operator. Of course, if
> the solver supports this extension, then it should also produce the
> right result, i.e., (= 0 0.5) is unsatisfiable.
>
> Our solver smtinterpol (which only supports the inofficial logic
> QF_AUFLIRA) has some code that is only used to support this extension.
>
> Regards,
>   Jochen
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>