[SMT-LIB] Benchmark Conformance: log in AUFLIRA/nasa/
cok@frontiernet.net
cok at frontiernet.net
Wed Nov 3 03:21:47 EDT 2010
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
More information about the SMT-LIB
mailing list