SMT let 表达式绑定作用域

Question

我正在使用一个简单的 let 表达式来缩短我的 SMT 公式。我希望绑定使用以前定义的绑定，如下所示，但是如果我删除注释行并让 n 引用 s 它不起作用：

;;;;;;;;;;;;;;;;;;;;;
;                   ;
; 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))
)

我查看了文档here，并不清楚是否确实禁止绑定引用其他（先前定义的）绑定：

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

我想这是 "shallow" 的替代品？

Answer 1

来自 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 的第 3.6.1 节：

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)).

如 备注 3 所示，如果您想引用较早的定义，则必须嵌套 let-expressions.

SMT let 表达式绑定作用域

SMT let expression binding scope

smt

z3