		Search-engine friendly clone of the ACL2 documentation.

Sfaig

Sfaig-make-faigenv

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

Signature
(sfaig-make-faigenv sexpr env) → faig-env
Arguments: sexpr — A single 4v-sexpr.; env — A sexpr-env to evaluate it under.
Returns: faig-env — The corresponding faig environment.

Definitions and Theorems

Function: sfaig-make-faigenv

(defun sfaig-make-faigenv (sexpr env)
       (declare (xargs :guard t))
       (let ((__function__ 'sfaig-make-faigenv))
            (declare (ignorable __function__))
            (b* ((vars (4v-sexpr-vars-1pass sexpr))
                 (onoff (num-varmap vars 0))
                 (env (4v-sexpr-alist-extract vars env)))
                (sig-al-to-svar-al (4v-alist->faig-const-alist env)
                                   onoff))))

Theorem: faig-eval-of-sfaig-make-faigenv

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