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

[cok@frontiernet.net]

I would agree with avoiding any implicit conversions and with keeping the parsing and typechecking task simple.  In addition:

- We should however keep what can be done in a theory consistent with what can be done in other commands.  The fact that overloading (with different ranks) can happen in one place and not the other is a nuisance in parsing and inconvenient for the user.
- The overloading on return type with the 'as' construct appears to have limited utility and also complicates the bottom up typechecking.

David

----- "Nikolaj Bjorner" <nbjorner at microsoft.com> wrote:

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