Let-binding

[bruderj15]

This can be done equivalently to quantifiers.

Do the solvers use it to share terms?

Standard does not make it sound like:

Let. The let binder introduces and defines one or more local variables in parallel. Semanti- cally, a term of the form (let ((x1 t1) · · · (xn tn)) t) (3.3) is equivalent to the term t[t1/x1, . . . , tn/xn] obtained from t by simultaneously replacing each free occurrence of xi in t by ti, for each i = 1, . . . , n, possibly after a suitable renaming of t’s bound variables to avoid capturing any variables in t1, . . . , tn. Because of the parallel semantics, the variables x1, . . . , xn in (3.3) must be pairwise distinct.

But what do the solvers do?

[bruderj15]

Z3 just expands it as they share terms before anyways: https://github.com/Z3Prover/z3/issues/6732#issuecomment-1560704954

[bruderj15]

As of above implementation in https://github.com/bruderj15/Hasmtlib/commit/d28c2319fb76590de8db3f4cce7e56e70e0d6ee3 we now need to traverse the entire formula on every assert.

Previously we just had to do that if logic was with quantifiers (not starting with QF). As we handle the let identical to the quantifiers by creating a scoped var before asserting, we now need to traverse every formula.

Significant (5x) ghc-runtime increase on a bigger instance of mine. There is no other way than that if we want to remain pure.

That runtime increase does not seem worth it for a in my opinion useless let-binding.

[bruderj15]

Reverted in: https://github.com/bruderj15/Hasmtlib/commit/9605d116122c9c7ea9e43a39dc29c7c8a177d634

[bruderj15]

Let is sugar only: https://github.com/usi-verification-and-security/opensmt/discussions/773#discussioncomment-10704269