[SMT-LIB] Issues with define-fun for Functions of Arity 0

[Cesare Tinelli]

Tjark

On 21 Apr 2016, at 13:27, Tjark Weber wrote:

> On Thu, 2016-04-21 at 15:48 +0200, Tjark Weber wrote:
>> Moreover, there are currently numerous SMT-LIB benchmarks in
>> *quantifier-free* logics that use define-fun to define functions of
>> arity 0.
>
> Further analysis of the 2015-06-01 SMT-LIB release also revealed
> numerous benchmarks that are classified as quantifier-free but use
> 'define-fun' to define functions of arity >= 1.
>
> Perhaps those benchmarks should be re-classified?
>
No, they should not. As I wrote in a recent post, the use of define-fun 
is explicitly allowed in benchmarks classified as quantifier-free 
because it can be processed without the use of quantifier reasoning.

As an aside, that is *not* going to be the case for the recently added 
define-fun-rec. In its general form, this command defines functions 
recursively. Such definitions do require an ability to reason about 
quantifiers. (That is the main reason we added a now command instead of 
just extending the syntax of define-fun.)

We do not have benchmarks with define-fun-rec yet, but when we add them 
they will go into quantified logics.


Cesare

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