• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
          • Sfaiglist-recover-4venv
          • Sfaiglist-make-faigenv
          • Sfaiglist
          • Sfaig-recover-4venv
          • Sfaig-make-faigenv
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

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