SMT позволяет выражать область видимости - PullRequest
Новая
       9

SMT позволяет выражать область видимости

0 голосов
/ 21 мая 2019

Я использую простое выражение 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))
)

Я посмотрел документацию здесь , и неясно, действительно ли запрещено, чтобы привязки ссылались на другие (ранее определенные) привязки:

Вся конструкция let полностью эквивалентна замене каждого нового параметра его выражениемв целевом выражении, полностью исключая новые символы (...)

Я полагаю, это "мелкая" замена?

1 Ответ

2 голосов
/ 21 мая 2019

Из раздела 3.6.1 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf:

Пусть . Связыватель let вводит и определяет одну или несколько локальных переменных в параллели. Семантически, термин вида (let ((x1 t1) · · · (xn tn)) t) (3.3) эквивалентен термину t[t1/x1, . . . , tn/xn] получен из t одновременной заменой каждого свободного вхождения xi в t по ti, для каждого i = 1,. , , , п, возможно, после подходящего переименование связанных переменных t, чтобы избежать захвата любых переменных в t1,. , , , тн. Из-за параллельной семантики переменные x1,. , , xn в (3.3) должен быть попарно различен.

Примечание 3 (без последовательных версия пусть). Язык не имеет последовательной версии позволять. Его эффект достигается вложением let, как в (let ((x1 t1)) (let ((x2 t2)) t)).

Как указано в Замечание 3 , если вы хотите обратиться к более раннему определению, вы должны вложить выражения let.

...