		Search-engine friendly clone of the ACL2 documentation.

Sfaig

Sfaig-recover-4venv

For use with sfaig, translates faig environments into equivalent sexpr environments.

Signature
(sfaig-recover-4venv sexpr faig-env) → sexpr-env
Arguments: sexpr — A single 4v-sexpr.; faig-env — A faig-env to evaluate the corresponding faig.
Returns: sexpr-env — The corresponding sexpr environment.

Definitions and Theorems

Function: sfaig-recover-4venv

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

Theorem: sexpr-eval-of-sfaig-recover-4venv

(defthm sexpr-eval-of-sfaig-recover-4venv
  (b* ((faig (sfaig sexpr))
       (sexpr-env (sfaig-recover-4venv sexpr faig-env)))
    (equal (4v-sexpr-eval sexpr sexpr-env)
           (faig-const->4v (faig-eval faig faig-env)))))