[SMT-LIB] Benchmark Conformance: log in AUFLIRA/nasa/

[Cesare Tinelli]

Hi Tjark and all,

On 13 Oct 2010, at 08:55, Tjark Weber wrote:

> On Wed, 2010-10-13 at 13:24 +0100, Tjark Weber wrote:
>> As far as I can tell, this is not valid.  Logic AUFLIRA is based on
>> theory Reals_Ints, which declares NUMERALs to be of sort Int (while
>> DECIMALs are of sort Real).  The :extensions in AUFLIRA permit implicit
>> conversion from Int to Real only for binary operators; they do not apply
>> to the unary function log.  Hence, (log 330) is ill-typed.
> 
> A related issue affects a number of benchmarks in AUFLIRA/nasa and
> AUFNIRA/nasa.  In these benchmarks, the array update function (store)
> and a user-declared function divide of type ((Real Real) Real) are
> applied to numerals.  Again, AUFLIRA/AUFNIRA do not admit implicit
> conversions from Int to Real (because store is ternary, and because
> divide is passed two Int arguments, which would both need to be
> converted).
> 
Perhaps we should extend the AUFLIRA and AUFNIRA logics further to allow implicit conversions for *any user-defined* function symbol.

The current extension is meant for the symbols in Reals_Ints (although admittedly that is not spelled out). Its limitation to binary symbols is justified by the fact that several symbols in Reals_Ints are overloaded. In particular, (unary) minus has two ranks: (Int Int) and (Real Real). During parsing then, there is no way to tell that in the term (- 3), say, the term 3 is meant to be a Real. In contrast, it is possible, and easy, during parsing to recognize (+ 4 3.5), say, as a shorthand for (+ (to_real 4) 3.5).

That said, user-defined symbols cannot be overloaded, so there is no problem in principle in allowing Int terms in place of Real arguments. For instance, in the log case above, log has (only) rank (Real Real). So (log 330) can be easily converted into (log (to_real 330)) during parsing. (Note that this does not apply to the theory symbol store.)

On the other hand, one could make a case in the completely opposite direction and argue for not allowing any implicit conversions at all, even those currently there, since they complicate parsing a bit nonetheless.

Personally, I'm neutral on this and I'd be happy to modify the declarations of AUFLIRA and AUFNIRA in either direction. Before proceeding then, it'd be good to hear from this community.

Any comments?


Cesare




> Regards,
> Tjark
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib