• 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
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Bed-from-aig

Match-aig-var-ite

Signature

(match-aig-var-ite x) → (mv okp var a b)

Arguments

x — AIG to pattern match.

Returns

okp — Whether x matches (if var a b).

var — On success, var from the match.
    Type (atom var).

a — On success, a from the match.

b — On success, b from the match.

Definitions and Theorems

Function: match-aig-var-ite

(defun match-aig-var-ite (x)
  (declare (xargs :guard t))
  (let ((__function__ 'match-aig-var-ite))
    (declare (ignorable __function__))
    (b* (((mv okp left right) (match-aig-or x))
         ((unless okp) (mv nil nil nil nil))
         ((mv okp a1 a2) (match-aig-and left))
         ((unless okp) (mv nil nil nil nil))
         ((mv okp b1 b2) (match-aig-and right))
         ((unless okp) (mv nil nil nil nil))
         ((mv okp var a b)
          (match-aig-var-ite-aux a1 a1 a2 b1 b2 x))
         ((when okp) (mv t var a b))
         ((mv okp var a b)
          (match-aig-var-ite-aux a2 a1 a2 b1 b2 x))
         ((when okp) (mv t var a b))
         ((mv okp var a b)
          (match-aig-var-ite-aux b1 a1 a2 b1 b2 x))
         ((when okp) (mv t var a b))
         ((mv okp var a b)
          (match-aig-var-ite-aux b2 a1 a2 b1 b2 x))
         ((when okp) (mv t var a b)))
      (mv nil nil nil nil))))

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

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

Theorem: match-aig-var-ite-correct

(defthm match-aig-var-ite-correct
  (b* (((mv okp var a b)
        (match-aig-var-ite x)))
    (implies okp
             (equal (aig-eval x env)
                    (if (aig-eval var env)
                        (aig-eval a env)
                      (aig-eval b env))))))

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

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

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

(defthm acl2-count-of-match-aig-var-ite-weak-1
  (b* (((mv ?okp ?var ?a ?b)
        (match-aig-var-ite x)))
    (<= (acl2-count var) (acl2-count x)))
  :rule-classes ((:rewrite) (:linear)))

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

(defthm acl2-count-of-match-aig-var-ite-weak-2
  (b* (((mv ?okp ?var ?a ?b)
        (match-aig-var-ite x)))
    (<= (acl2-count a) (acl2-count x)))
  :rule-classes ((:rewrite) (:linear)))

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

(defthm acl2-count-of-match-aig-var-ite-weak-3
  (b* (((mv ?okp ?var ?a ?b)
        (match-aig-var-ite x)))
    (<= (acl2-count b) (acl2-count x)))
  :rule-classes ((:rewrite) (:linear)))

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

(defthm acl2-count-of-match-aig-var-ite-strong-1
  (b* (((mv ?okp ?var ?a ?b)
        (match-aig-var-ite x)))
    (implies okp
             (< (acl2-count var) (acl2-count x))))
  :rule-classes ((:rewrite) (:linear)))

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

(defthm acl2-count-of-match-aig-var-ite-strong-2
  (b* (((mv ?okp ?var ?a ?b)
        (match-aig-var-ite x)))
    (implies okp (< (acl2-count a) (acl2-count x))))
  :rule-classes ((:rewrite) (:linear)))

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

(defthm acl2-count-of-match-aig-var-ite-strong-3
  (b* (((mv ?okp ?var ?a ?b)
        (match-aig-var-ite x)))
    (implies okp (< (acl2-count b) (acl2-count x))))
  :rule-classes ((:rewrite) (:linear)))