		Search-engine friendly clone of the ACL2 documentation.

Sfaig

A simplified version of 4v-sexpr-to-faig that constructs its own onoff list out of the variables of the sexpr.

Signature
(sfaig sexpr) → faig
Arguments: sexpr — A single 4v-sexpr.
Returns: faig — An equivalent FAIG, using numeric variables.

Definitions and Theorems

Function: sfaig

(defun sfaig (sexpr)
  (declare (xargs :guard t))
  (let ((__function__ 'sfaig))
    (declare (ignorable __function__))
    (b* ((vars (4v-sexpr-vars-1pass sexpr))
         (onoff (num-varmap vars 0)))
      (4v-sexpr-to-faig sexpr onoff))))

Subtopics

Sfaiglist-recover-4venv: For use with sfaiglist, translates faig environments back into equivalent sexpr environments.
Sfaiglist-make-faigenv: For use with sfaiglist, translates sexpr environments into equivalent faig environments.
Sfaiglist: A simplified version of 4v-sexpr-to-faig-list that constructs its own onoff list out of the variables of the sexprs.
Sfaig-recover-4venv: For use with sfaig, translates faig environments into equivalent sexpr environments.
Sfaig-make-faigenv: For use with sfaig, translates sexpr environments into equivalent faig environments.