[SMT-LIB] let vs. assumption construct

[Cesare Tinelli]

Hi Rémi and all,

I'd like to add to Clark's comments by stressing that there is nothing  
in the SMT-LIB standard per se that allows one to answer your  
questions. The issues you bring up are entirely solver dependent. In  
principle, with one SMT-solver it might be better to do it one way and  
with another solver the opposite way.
That said, most current SMT solvers are similar in this respect. Clark  
is referring to the current state of the art.

On 15 Jan 2010, at 13:37, Clark Barrett wrote:

> My opinion is that for efficiency reasons, it is preferable to use
> definitions (i.e. let) rather than assumptions.  The reason for this  
> is that
> assumptions introduce additional variables, and additional variables  
> often
> lead to more splitting, more overhead, etc.
>
> In SMT-LIB Version 1.2, "let" constructs are the only way to share  
> terms
> without introducing new variables.  In the upcoming Version 2.0, we  
> are
> adding a mechanism for global definitions, so there will be another  
> way to
> accomplish the same thing.
>
For the records, I think Clark means "free constants", not "variables"  
in the to paragraphs above. ("let" constructs do introduce new  
variables.)


> There are currently SMT-LIB benchmarks with many many nested "let"
> expressions - enough to overflow the stack if you try to process them
> recursively.  So, I think most solver implementers have implemented
> non-recursive parsing of "let" and this works fine.
>

In fact, the problem is general. There are SMT-LIB benchmarks with  
very deeply nested "and" operators that will cause recursive parsers  
to stack overflow.

Cheers,


Cesare



> -Clark
>
>
> On Thu, Jan 14, 2010 at 9:56 AM, Rémi Delmas <Remi.Delmas at onera.fr>  
> wrote:
>
>> Hi all and happy new year!
>>
>> which approach is preferable in SMT-lib between these two to  
>> express a
>> functional dependency between variables of a model (in the benchmark
>> library both approaches are used)?
>>
>> Using assumptions to encode variable definitions
>> declare a free symbol and constrain it to be equal to some  
>> expression of
>> other symbols :
>> :extrafun (x S)
>> ...
>> :assumption (= x <some S-sorted expression>)
>> :formula (<some formula of x>)
>>
>> Or the use let construct directly in the formula :
>> :formula (let (x <some S-sorted expression>) <some formula of x>)
>>
>> Is it possible to run into issues like parser stack overflow when
>> nesting lots of let constructs  (hundreds of thousands) ?
>>
>> Thanks,
>>
>> /Rémi
>>
>> _______________________________________________
>> 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