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

[Cesare Tinelli]

Hi Nikolaj,

On 3 Nov 2010, at 00:53, Nikolaj Bjorner 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.
> 
Yes, that is indeed the main designing principle of the standard. 
I tend to agree with you and the others who have voiced their opinion so far that we should disallow implicit coercions then. 
I'd be interested in seeing if there is any support for them.


As for your "shameless plug" at  http://rise4fun.com/z3, it is great that you have something like that on-line, but let me say that your relaxed adherence to the SMT-LIB2 format (as pointed out by David Cok in another message) could actually harm the cause, in my option. It will only introduce confusion unless you state explicitly that Z3's accepts as *SMT-LIB2-like* format.

Put more clearly, while I certainly do not intend to tell you, the Z3 developers, how to define your tool's input language, I'd like to urge you not to present it, explicitly or implicitly, as the SMT-LIB2 language when it is not.

Best,


Cesare
 





> 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
>