• 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
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 4v-sexpr-to-faig

4v-sexpr-to-faig-plain

Non-optimized conversion from sexprs into faigs.

This is a straightforward, non-optimizing conversion where we just use the f- versions of the faig-constructors at each level.

Definitions and Theorems

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

(defun 4v-sexpr-to-faig-plain (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
        (4v-sexpr-to-faig-apply fn
                                (4v-sexpr-to-faig-plain-list (cdr x)
                                                             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))
             (args (4v-sexpr-to-faig-plain-list (cdr x)
                                                onoff))
             (arg1 (4v-first args))
             (arg2 (4v-second args))
             (arg3 (4v-third args)))
          (case fn
            (not (f-aig-not arg1))
            (and (f-aig-and arg1 arg2))
            (xor (f-aig-xor arg1 arg2))
            (iff (f-aig-iff arg1 arg2))
            (or (f-aig-or arg1 arg2))
            (ite* (f-aig-ite* arg1 arg2 arg3))
            (zif (f-aig-zif arg1 arg2 arg3))
            (buf (f-aig-unfloat arg1))
            (xdet (f-aig-xdet arg1))
            (res (f-aig-res arg1 arg2))
            (tristate (t-aig-tristate arg1 arg2))
            (ite (f-aig-ite arg1 arg2 arg3))
            (pullup (f-aig-pullup arg1))
            (id (faig-fix arg1))
            (otherwise (faig-x)))))))

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

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

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

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

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

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

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

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

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

(defthm faig-eval-4v-sexpr-to-faig-plain
  (let
    ((4v-env
          (faig-const-alist->4v-alist (faig-eval-alist onoff env))))
    (equal (faig-eval (4v-sexpr-to-faig-plain x onoff)
                      env)
           (4v->faig-const (4v-sexpr-eval x 4v-env)))))

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

(defthm faig-eval-4v-sexpr-to-faig-plain-list
 (let
   ((4v-env
         (faig-const-alist->4v-alist (faig-eval-alist onoff env))))
  (equal (faig-eval-list (4v-sexpr-to-faig-plain-list x onoff)
                         env)
         (4v-list->faig-const-list (4v-sexpr-eval-list x 4v-env)))))