• Top
  • Documentation
  • Books
  • 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
  • Math
  • Testing-utilities

• 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)))))