[SMT-LIB] let vs. assumption construct

[Rhishikesh Limaye]

Equality assumptions and let expressions make a difference when reporting
models. With equality assumptions, there are the free constants (or
variables in colloquial terms), and I guess  all the solvers print out the
model values of all of them. This cannot be avoided, because a user is right
in expecting model values of all ":extrafuns" declaration done by him/her.
With let expressions, there is no such expectation, and a solver is free to
forget the let bindings after parsing. Thus, even if inlining/replacements
are done to simplify away equality assumptions, a solver would have to
expend a bit of memory to store the mappings for model reporting purpose.

Rhishi

2010/1/15 Johannes Waldmann <waldmann at imn.htwk-leipzig.de>

> Clark Barrett wrote:
>
> > My opinion is that for efficiency reasons, it is preferable to use
> > definitions (i.e. let) rather than assumptions. [...]
>
> This sounds a lot like a programming advice "you shouldn't
> use subprograms because they have implementation overhead"
> while compilers are fine at inlining.
>
> As a SMT user, I'd like to have more freedom in writing
> the constraint systems, and expect the solvers to do transformations
> for efficiency (e.g., replace equality assumptions by let).
>
> Best regards, Johannes Waldmann.
>
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
>