[SMT-LIB] let vs. assumption construct

Johannes Waldmann waldmann at imn.htwk-leipzig.de
Fri Jan 15 15:05:50 EST 2010


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


More information about the SMT-LIB mailing list