SMT let expression binding scope

Question

I'm using a simple let expression to shorten my SMT formula. I want bindings to use previously defined bindings as follows, but if I remove the commented line and have n refer to s it doesn't work:

;;;;;;;;;;;;;;;;;;;;;
;                   ;
; This is our state ;
;                   ;
;;;;;;;;;;;;;;;;;;;;;
(declare-datatypes ((State 0))
    (((rec
        (myArray String)
        (index   Int))))
)

;;;;;;;;;;;;;;;;;;;;;;;;;;
;                        ;
; This is our function f ;
;                        ;
;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-fun f ((in State)) State
    (let (
          (s   (myArray in))
          (n   (str.len (myArray in))))
;;;;;;;;;;(n   (str.len s)))
     in
         (rec (str.substr s 1 n) 1733))
)

I looked at the documentation here, and it's not clear whether it's indeed forbidden to have bindings refer to other (previously defined) bindings:

The whole let construct is entirely equivalent to replacing each new parameter by its expression in the target expression, eliminating the new symbols completely (...)

I guess it's a "shallow" replacement?

Wouldn't it be possible to deal with this using a double-nested let? — Patrick Trentin

alias alias · Accepted Answer · 2019-05-21T14:30:56

From Section 3.6.1 of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf:

Let. The let binder introduces and defines one or more local variables in parallel. Semantically, 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.

Remark 3 (No sequential version of let). The language does not have a sequential version of let. Its effect is achieved by nesting lets, as in (let ((x1 t1)) (let ((x2 t2)) t)).

As indicated in Remark 3, if you want to refer to an earlier definition you have to nest the let-expressions.

SMT let expression binding scope

1 Answers