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

[Tinelli, Cesare]

Hi Levent and all,

Equality is not treated any differently than the other operators in SMT-LIB.
It is parametric with type (or rank, in SMT-LIB parlance) alpha x alpha -> Bool. Notice that both arguments must be of the same sort.

As for the point you raised, I agree with you. At the same time, as Jochen correctly pointed out, the logics AUFLIRA and AUFNIRA allow one to omit applications of to_real in cases when it is easy to infer and insert it automatically. Note that the extension does *not* change the type of any operators, including equality.


This extension has been somewhat controversial. Those against it were afraid that it would be confusing to people, especially those who do not read the docs :)
There is evidence that those against the extension were right, but removing it now would be problematic because it would cause backward compatibility problems, something we try to avoid as much as possible.

That said, the whole mechanism for defining and naming logics will have to change soon because the proliferation of logics has become unmanageable (many more logics are on the way with the addition of a theory of floating points and the planned addition of sequences/strings, sets and algebraic data types).
This issue has been discussed both off-line and at SMT'14 the other day. If we revamp that mechanism, as we hope, a number of non-backward compatible changes to the logics will become necessary. 
That will be a good time to remove those extensions from the new versions of AUFLIRA and AUFNIRA if there is enough push from the community.


Cesare



On 19 Jul 2014, at 21:24, Levent Erkok <erkokl at gmail.com> wrote:

> 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
>> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib