• Top
  • Documentation
  • Books
  • 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-and-faig-operations-commute
          • 4v-sexpr-to-faig-plain
          • 4v-sexpr-to-faig-opt
          • Sfaig
          • 4v->faig-const
          • 4v-sexpr-to-faig-list
          • Faig-const-fix
          • Faig-const->4v
          • 4v-sexpr-to-faig-alist
          • Faig-const-<=
          • Faig-const-p
        • 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
        • 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
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 4v-sexpr-to-faig

4v-sexpr-to-faig-opt

Optimized conversion from sexprs into faigs.

Definitions and Theorems

Function: 4v-sexpr-to-faig-opt

(defun 4v-sexpr-to-faig-opt (x onoff)
 (declare (xargs :guard t))
 (b* (((when (atom x))
       (if x (let ((look (hons-get x onoff)))
               (if (consp (cdr look))
                   (cdr look)
                 (faig-x)))
         (faig-x)))
      (fn (car x)))
  (mbe
    :logic
    (let ((sargs (cdr x)))
      (4v-sexpr-to-faig-opt-apply
           fn sargs
           (4v-sexpr-to-faig-opt-list sargs onoff)))
    :exec
    (b*
      (((when (eq fn (4vt))) (faig-t))
       ((when (eq fn (4vf))) (faig-f))
       ((when (eq fn (4vz))) (faig-z))
       ((when (eq fn (4vx))) (faig-x))
       (sargs (cdr x))
       (args (4v-sexpr-to-faig-opt-list sargs onoff))
       ((when (eq fn 'id))
        (faig-fix (4v-first args)))
       ((when (eq fn 'res))
        (f-aig-res (4v-first args)
                   (4v-second args)))
       ((when (eq fn 'tristate))
        (t-aig-tristate (4v-first args)
                        (4v-second args)))
       ((when (eq fn 'pullup))
        (f-aig-pullup (4v-first args)))
       ((when (eq fn 'zif))
        (t-aig-ite* (maybe-f-aig-unfloat
                         (mbe :logic (first sargs)
                              :exec (and (consp sargs) (car sargs)))
                         (4v-first args))
                    (4v-second args)
                    (4v-third args)))
       (args (maybe-f-aig-unfloat-list sargs args))
       (arg1 (4v-first args))
       (arg2 (4v-second args))
       (arg3 (4v-third args)))
      (case fn
        (not (t-aig-not arg1))
        (and (t-aig-and arg1 arg2))
        (xor (t-aig-xor arg1 arg2))
        (iff (t-aig-iff arg1 arg2))
        (ite* (t-aig-ite* arg1 arg2 arg3))
        (or (t-aig-or arg1 arg2))
        (buf (faig-fix arg1))
        (xdet (t-aig-xdet arg1))
        (ite (t-aig-ite arg1 arg2 arg3))
        (otherwise (faig-x)))))))

Function: 4v-sexpr-to-faig-opt-list

(defun 4v-sexpr-to-faig-opt-list (x onoff)
  (declare (xargs :guard t))
  (if (atom x)
      nil
    (cons (4v-sexpr-to-faig-opt (car x) onoff)
          (4v-sexpr-to-faig-opt-list (cdr x)
                                     onoff))))

Theorem: len-4v-sexpr-to-faig-opt-list

(defthm len-4v-sexpr-to-faig-opt-list
  (equal (len (4v-sexpr-to-faig-opt-list x onoff))
         (len x)))

Theorem: consp-4v-sexpr-to-faig-opt

(defthm consp-4v-sexpr-to-faig-opt
  (consp (4v-sexpr-to-faig-opt x al))
  :rule-classes :type-prescription)

Theorem: alistp-4v-sexpr-to-faig-opt-list

(defthm alistp-4v-sexpr-to-faig-opt-list
  (alistp (4v-sexpr-to-faig-opt-list x al)))

Function: 4v-sexpr-to-faig-opt-memoize-condition

(defun 4v-sexpr-to-faig-opt-memoize-condition (x onoff)
  (declare (ignorable x onoff)
           (xargs :guard 't))
  (and (consp x) (consp (cdr x))))

Theorem: faig-eval-4v-sexpr-to-faig-opt

(defthm faig-eval-4v-sexpr-to-faig-opt
  (equal (faig-eval (4v-sexpr-to-faig-opt x al)
                    env)
         (faig-eval (4v-sexpr-to-faig-plain x al)
                    env)))

Theorem: faig-eval-4v-sexpr-to-faig-opt-list

(defthm faig-eval-4v-sexpr-to-faig-opt-list
  (equal (faig-eval-list (4v-sexpr-to-faig-opt-list x al)
                         env)
         (faig-eval-list (4v-sexpr-to-faig-plain-list x al)
                         env)))