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

[Cesare Tinelli]

Hi Tjark,

On 3 Nov 2010, at 05:30, Tjark Weber wrote:

> Dear Cesare,
> 
> On Wed, 2010-11-03 at 00:31 -0500, Cesare Tinelli wrote:
>> 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?
> 
> I am inclined to agree with Nikolaj and David that there should be no
> implicit conversions.  They complicate parsing; the present conformance
> issue proves that the details are easy to get wrong; and their benefits
> seem marginal, considering that SMT-LIB is generated and read by
> automated tools more often than by human beings.
> 
Yep.

> Instead of (log (to_real 330)), one could simply write (log 330.0).
> 
Sure, that was just an example. If instead of 330 you had an Int constant there you would need to_real.


Cesare



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