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

[Nikolaj Bjorner]

Dear Cesare and all,

I would suggest not to have implicit conversions. They complicate parsing and it becomes tempting to resort to guesswork instead of consulting a the PDF specification.

At the very least the signature of a function should be determined uniquely by its name and the types of the arguments. 
The types of the arguments are determined bottom up.
This leaves room for the current overloading, but not for implicit coercions. 
It also entails that the type of an expression can be re-constructed bottom-up.

While I support the SMT-LIB2 format (see my shameless plug: http://rise4fun.com/z3 ), I see its main priority as a low-level mostly 
machine writeable/readable interchange format that as an added benefit is also human read/write-able.

Thanks,

Nikolaj



-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Cesare Tinelli
Sent: Tuesday, November 02, 2010 10:31 PM
To: smt-lib at cs.nyu.edu
Subject: Re: [SMT-LIB] Benchmark Conformance: log in AUFLIRA/nasa/

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


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