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