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

[Mohamed Iguernelala]

Hello,

Thanks for the link http://smtlib.cs.uiowa.edu/logics/AUFLIRA.smt2. I've 
never figured out that "Logics" in SMT-LIB's website "are clickable" ...

So, ok: there is an implicit cast in this case, but it is defined on the 
"logic level" not on the theory level.

Regards,
Mohamed.

-- 
Senior R&D Engineer, OCamlPro
Research Associate, VALS team, LRI.
http://www.iguer.info

Le 19/07/2014 09:48, Jochen Hoenicke a écrit :
> 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