[SMT-LIB] let vs. assumption construct

[Johannes Waldmann]

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.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 260 bytes
Desc: OpenPGP digital signature
Url : /pipermail/smt-lib/attachments/20100115/83c82f72/signature-0001.bin