[SMT-LIB] overloading

[Cesare Tinelli]

Hi David,

On 15 Nov 2010, at 12:39, cok at frontiernet.net wrote:

> Cesare et al.
> 
> This bullet on page 11 regards overloading:
> 
> Theory function symbols can now be overloaded arbitrarily, although in ambiguous
> cases their occurrences within a term must be annotated with a return sort. (User-defined function symbols cannot overload any already defined symbol.)
> 
Yes.

> I understood that to mean that the user cannot add definitions of theory functions, even with a different signature.
> 
Yes.

> The benchmark AUFLIRA/nasa/fol_simplify/cl5_nebula_array_0001.fof.smt2 (among others)
> includes as a user-definition
> 
> (declare-fun abs (Real) Real)
> 
> But the logic also includes the Reals_Ints theory, which defines 'abs' for an Int argument,
> but not for a Real argument.
> 
> Can you clarify whether the benchmark is incorrect or whether the statement about user-defined overloading needs elaboration?
> 
The benchmark is incorrect. Thanks for spotting that.

It should use another name for abs. Alternatively, we could add the function (abs Real Real) to Reals_Ints, but then the entire declaration above would have be removed from the offending benchmarks and the benchmarks' logic would have to be changed to AUFNIRA (because AUFLIRA does not allow abs as a theory symbol).  

I'll consult with Clark and Morgan to see which of the two alternatives is most reasonable from their point of view (as maintainers of the the repository).


Thanks,


Cesare

 

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