		Search-engine friendly clone of the ACL2 documentation.

Sfaiglist

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

Signature
(sfaiglist sexprs) → faigs
Arguments: sexprs — A list of 4v-sexprs.
Returns: faigs — A list of equivalent FAIGs, using numeric variables.

Definitions and Theorems

Function: sfaiglist

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

Theorem: len-of-sfaiglist

(defthm len-of-sfaiglist
  (equal (len (sfaiglist x)) (len x)))