[SMT-LIB] let vs. assumption construct

[Clark Barrett]

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.

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.

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