• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
      • Faig-constructors
        • T-aig-ite*
        • F-aig-ite*
        • T-aig-ite
        • F-aig-ite
        • T-aig-tristate
        • F-aig-zif
        • T-aig-xor
        • T-aig-or
        • T-aig-iff
        • T-aig-and
        • F-aig-and
        • F-aig-xor
        • F-aig-or
        • F-aig-iff
        • F-aig-res
        • F-aig-unfloat
        • T-aig-not
        • F-aig-pullup
        • F-aig-not
        • T-aig-xdet
        • F-aig-xdet
      • Faig-onoff-equiv
      • Faig-purebool-p
      • 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-constructors

F-aig-ite*

(f-aig-ite* c a b) constructs a (more conservative) FAIG representing (if c a b), assuming these input FAIGs cannot evaluate to Z.

Signature

(f-aig-ite* c a b) → *

This is a more-conservative version of f-aig-ite that emits X in the case that c is unknown, even when a = b. See 4v-ite for discussion related to this issue.

Definitions and Theorems

Function: f-aig-ite*

(defun f-aig-ite* (c a b)
  (declare (xargs :guard t))
  (let ((__function__ 'f-aig-ite*))
    (declare (ignorable __function__))
    (b* ((c (f-aig-unfloat c))
         (a (f-aig-unfloat a))
         (b (f-aig-unfloat b)))
      (t-aig-ite* c a b))))

Theorem: faig-eval-of-f-aig-ite*

(defthm faig-eval-of-f-aig-ite*
  (equal (faig-eval (f-aig-ite* c a b) env)
         (f-aig-ite* (faig-eval c env)
                     (faig-eval a env)
                     (faig-eval b env))))

Theorem: faig-fix-equiv-implies-equal-f-aig-ite*-1

(defthm faig-fix-equiv-implies-equal-f-aig-ite*-1
  (implies (faig-fix-equiv c c-equiv)
           (equal (f-aig-ite* c a b)
                  (f-aig-ite* c-equiv a b)))
  :rule-classes (:congruence))

Theorem: faig-fix-equiv-implies-equal-f-aig-ite*-2

(defthm faig-fix-equiv-implies-equal-f-aig-ite*-2
  (implies (faig-fix-equiv a a-equiv)
           (equal (f-aig-ite* c a b)
                  (f-aig-ite* c a-equiv b)))
  :rule-classes (:congruence))

Theorem: faig-fix-equiv-implies-equal-f-aig-ite*-3

(defthm faig-fix-equiv-implies-equal-f-aig-ite*-3
  (implies (faig-fix-equiv b b-equiv)
           (equal (f-aig-ite* c a b)
                  (f-aig-ite* c a b-equiv)))
  :rule-classes (:congruence))

Theorem: faig-equiv-implies-faig-equiv-f-aig-ite*-3

(defthm faig-equiv-implies-faig-equiv-f-aig-ite*-3
  (implies (faig-equiv b b-equiv)
           (faig-equiv (f-aig-ite* c a b)
                       (f-aig-ite* c a b-equiv)))
  :rule-classes (:congruence))

Theorem: faig-equiv-implies-faig-equiv-f-aig-ite*-2

(defthm faig-equiv-implies-faig-equiv-f-aig-ite*-2
  (implies (faig-equiv a a-equiv)
           (faig-equiv (f-aig-ite* c a b)
                       (f-aig-ite* c a-equiv b)))
  :rule-classes (:congruence))

Theorem: faig-equiv-implies-faig-equiv-f-aig-ite*-1

(defthm faig-equiv-implies-faig-equiv-f-aig-ite*-1
  (implies (faig-equiv c c-equiv)
           (faig-equiv (f-aig-ite* c a b)
                       (f-aig-ite* c-equiv a b)))
  :rule-classes (:congruence))