• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
      • Faig-constructors
      • Faig-onoff-equiv
      • Faig-purebool-p
        • Faig-purebool-check
        • Faig-purebool-list-p
        • Faig-purebool-aig
      • Faig-alist-equiv
      • Faig-equiv
      • Faig-eval
      • Faig-restrict
      • Faig-fix
      • Faig-partial-eval
      • Faig-compose
      • Faig-compose-alist
      • Patbind-faig
      • Faig-constants
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Faig-purebool-p

Faig-purebool-aig

An AIG that captures exactly when the FAIG X is Boolean valued.

Signature

(faig-purebool-aig x) → aig

Arguments

x — A single FAIG.

This is useful mainly to implement faig-purebool-check.

Definitions and Theorems

Function: faig-purebool-aig

(defun faig-purebool-aig (x)
       (declare (xargs :guard t))
       (let ((__function__ 'faig-purebool-aig))
            (declare (ignorable __function__))
            (b* ((x (faig-fix x))
                 (onset (car x))
                 (offset (cdr x)))
                (aig-or (aig-and onset (aig-not offset))
                        (aig-and offset (aig-not onset))))))

Theorem: faig-purebool-p-as-aig-eval

(defthm faig-purebool-p-as-aig-eval
        (equal (faig-purebool-p x)
               (aig-eval (faig-purebool-aig x)
                         (faig-purebool-p-witness x))))

Theorem: faig-purebool-p-monotonicity

(defthm faig-purebool-p-monotonicity
        (implies (not (aig-eval (faig-purebool-aig x) env))
                 (not (aig-eval (faig-purebool-aig x)
                                (faig-purebool-p-witness x)))))