• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
      • Aig-constructors
      • Aig-vars
      • Aig-sat
      • Bddify
      • Aig-substitution
      • Aig-other
      • Aig-semantics
        • Aig-eval
        • Aig-alist-equiv
        • Aig-env-equiv
        • Aig-equiv
        • Aig-eval-alist
        • Aig-eval-list
        • Aig-eval-alists
      • Aig-and-count
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Aig-semantics

Aig-alist-equiv

We say the AIG Alists X and Y are equivalent when they bind the same keys to equivalent AIGs, in the sense of aig-equiv.

This is a universal equivalence, introduced using def-universal-equiv.

Function: aig-alist-equiv

(defun aig-alist-equiv (x y)
  (declare (xargs :non-executable t))
  (declare (xargs :guard t))
  (prog2$ (throw-nonexec-error 'aig-alist-equiv
                               (list x y))
          (let ((k (aig-alist-equiv-witness x y)))
            (and (iff (hons-assoc-equal k x)
                      (hons-assoc-equal k y))
                 (aig-equiv (cdr (hons-assoc-equal k x))
                            (cdr (hons-assoc-equal k y)))))))

Definitions and Theorems

Theorem: aig-alist-equiv-necc

(defthm aig-alist-equiv-necc
  (implies (not (and (iff (hons-assoc-equal k x)
                          (hons-assoc-equal k y))
                     (aig-equiv (cdr (hons-assoc-equal k x))
                                (cdr (hons-assoc-equal k y)))))
           (not (aig-alist-equiv x y))))

Theorem: aig-alist-equiv-witnessing-witness-rule-correct

(defthm aig-alist-equiv-witnessing-witness-rule-correct
  (implies (not ((lambda (k y x)
                   (not (if (iff (hons-assoc-equal k x)
                                 (hons-assoc-equal k y))
                            (aig-equiv (cdr (hons-assoc-equal k x))
                                       (cdr (hons-assoc-equal k y)))
                          'nil)))
                 (aig-alist-equiv-witness x y)
                 y x))
           (aig-alist-equiv x y))
  :rule-classes nil)

Theorem: aig-alist-equiv-instancing-instance-rule-correct

(defthm aig-alist-equiv-instancing-instance-rule-correct
  (implies (not (if (iff (hons-assoc-equal k x)
                         (hons-assoc-equal k y))
                    (aig-equiv (cdr (hons-assoc-equal k x))
                               (cdr (hons-assoc-equal k y)))
                  'nil))
           (not (aig-alist-equiv x y)))
  :rule-classes nil)

Theorem: aig-alist-equiv-is-an-equivalence

(defthm aig-alist-equiv-is-an-equivalence
  (and (booleanp (aig-alist-equiv x y))
       (aig-alist-equiv x x)
       (implies (aig-alist-equiv x y)
                (aig-alist-equiv y x))
       (implies (and (aig-alist-equiv x y)
                     (aig-alist-equiv y z))
                (aig-alist-equiv x z)))
  :rule-classes (:equivalence))

Theorem: alist-equiv-refines-aig-alist-equiv

(defthm alist-equiv-refines-aig-alist-equiv
  (implies (alist-equiv x y)
           (aig-alist-equiv x y))
  :rule-classes (:refinement))