		Search-engine friendly clone of the ACL2 documentation.

Sfaig

Sfaiglist-recover-4venv

For use with sfaiglist, translates faig environments back into equivalent sexpr environments.

Signature
(sfaiglist-recover-4venv sexprs faig-env) → sexpr-env
Arguments: sexprs — The list of 4v-sexprs.; faig-env — A faig-env to evaluate the corresponding faigs.
Returns: sexpr-env — The corresponding sexpr environment.

Definitions and Theorems

Function: sfaiglist-recover-4venv

(defun sfaiglist-recover-4venv (sexprs faig-env)
 (declare (xargs :guard t))
 (let ((__function__ 'sfaiglist-recover-4venv))
  (declare (ignorable __function__))
  (b* ((vars (4v-sexpr-vars-1pass-list sexprs))
       (onoff (num-varmap vars 0)))
    (faig-const-alist->4v-alist (faig-eval-alist onoff faig-env)))))

Theorem: 4v-sexpr-eval-list-of-sfaiglist-recover-4venv

(defthm 4v-sexpr-eval-list-of-sfaiglist-recover-4venv
 (b* ((faigs (sfaiglist sexprs))
      (sexpr-env (sfaiglist-recover-4venv sexprs faig-env)))
  (equal
       (4v-sexpr-eval-list sexprs sexpr-env)
       (faig-const-list->4v-list (faig-eval-list faigs faig-env)))))