• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
      • Bed-op-p
      • Bed-from-aig
        • Match-aig-var-ite
        • Match-aig-var-ite-aux
        • Match-aig-xor-1
        • Match-aig-iff-2
        • Match-aig-xor-2
        • Match-aig-iff-1
        • Bed-from-aig-aux
        • Match-aig-nor
        • Match-aig-andc2
        • Match-aig-andc1
        • Match-aig-xor
        • Match-aig-or
        • Match-aig-iff
        • Match-aig-and
        • Match-aig-not
      • Bed-mk1
      • Bed-eval
      • Up
      • Aig-translation
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Bed-from-aig

Match-aig-var-ite-aux

We have been given the AIG (OR (AND A1 A2) (OR B1 B2)). We want to pattern match it against (IF VAR A B)?

Signature

(match-aig-var-ite-aux var a1 a2 b1 b2 x) → (mv okp var a b)

Returns

var — Type (atom var).

Definitions and Theorems

Function: match-aig-var-ite-aux

(defun match-aig-var-ite-aux (var a1 a2 b1 b2 x)
  (declare (ignore x))
  (declare (xargs :guard t))
  (let ((__function__ 'match-aig-var-ite-aux))
    (declare (ignorable __function__))
    (b* (((unless (and (atom var) (not (booleanp var))))
          (mv nil nil nil nil))
         ((when (equal var a1))
          (b* (((mv okp b1-guts) (match-aig-not b1))
               ((when (and okp (equal b1-guts var)))
                (mv t var a2 b2))
               ((mv okp b2-guts) (match-aig-not b2))
               ((when (and okp (equal b2-guts var)))
                (mv t var a2 b1)))
            (mv nil nil nil nil)))
         ((when (equal var a2))
          (b* (((mv okp b1-guts) (match-aig-not b1))
               ((when (and okp (equal b1-guts var)))
                (mv t var a1 b2))
               ((mv okp b2-guts) (match-aig-not b2))
               ((when (and okp (equal b2-guts var)))
                (mv t var a1 b1)))
            (mv nil nil nil nil)))
         ((when (equal var b1))
          (b* (((mv okp a1-guts) (match-aig-not a1))
               ((when (and okp (equal a1-guts var)))
                (mv t var b2 a2))
               ((mv okp a2-guts) (match-aig-not a2))
               ((when (and okp (equal a2-guts var)))
                (mv t var b2 a1)))
            (mv nil nil nil nil)))
         ((when (equal var b2))
          (b* (((mv okp a1-guts) (match-aig-not a1))
               ((when (and okp (equal a1-guts var)))
                (mv t var b1 a2))
               ((mv okp a2-guts) (match-aig-not a2))
               ((when (and okp (equal a2-guts var)))
                (mv t var b1 a1)))
            (mv nil nil nil nil))))
      (mv nil nil nil nil))))

Theorem: atom-of-match-aig-var-ite-aux.var

(defthm atom-of-match-aig-var-ite-aux.var
  (b* (((mv ?okp ?var ?a ?b)
        (match-aig-var-ite-aux var a1 a2 b1 b2 x)))
    (atom var))
  :rule-classes :type-prescription)

Theorem: not-booleanp-of-match-aig-var-ite-aux

(defthm not-booleanp-of-match-aig-var-ite-aux
  (b* (((mv okp var & &)
        (match-aig-var-ite-aux var a1 a2 b1 b2 x)))
    (implies okp
             (and (atom var)
                  (not (equal var t))
                  (not (equal var nil)))))
  :rule-classes :type-prescription)

Theorem: match-aig-var-ite-aux-correct

(defthm match-aig-var-ite-aux-correct
  (b* (((mv okp1 left right) (match-aig-or x))
       ((mv okp2 a1 a2) (match-aig-and left))
       ((mv okp3 b1 b2) (match-aig-and right))
       ((mv okp4 var a b)
        (match-aig-var-ite-aux var a1 a2 b1 b2 x)))
    (implies (and okp1 okp2 okp3 okp4)
             (equal (aig-eval x env)
                    (if (aig-eval var env)
                        (aig-eval a env)
                      (aig-eval b env))))))

Theorem: acl2-count-of-match-aig-var-ite-aux-weak

(defthm acl2-count-of-match-aig-var-ite-aux-weak
  (b* (((mv okp1 left right) (match-aig-or x))
       ((mv okp2 a1 a2) (match-aig-and left))
       ((mv okp3 b1 b2) (match-aig-and right))
       ((mv ?okp var a b)
        (match-aig-var-ite-aux var a1 a2 b1 b2 x)))
    (implies (and okp1 okp2 okp3)
             (and (<= (acl2-count var) (acl2-count x))
                  (<= (acl2-count a) (acl2-count x))
                  (<= (acl2-count b) (acl2-count x))))))

Theorem: acl2-count-of-match-aig-var-ite-aux-strong

(defthm acl2-count-of-match-aig-var-ite-aux-strong
  (b* (((mv okp1 left right) (match-aig-or x))
       ((mv okp2 a1 a2) (match-aig-and left))
       ((mv okp3 b1 b2) (match-aig-and right))
       ((mv okp4 var a b)
        (match-aig-var-ite-aux var a1 a2 b1 b2 x)))
    (implies (and okp1 okp2 okp3 okp4)
             (and (< (acl2-count var) (acl2-count x))
                  (< (acl2-count a) (acl2-count x))
                  (< (acl2-count b) (acl2-count x))))))