		Search-engine friendly clone of the ACL2 documentation.

Network

Aignet-extension-p

(aignet-extension-p new old) determines if the aignet new is the result of building some new nodes onto another aignet old.

Signature
(aignet-extension-p new old) → bool
Arguments: new — Perhaps an extension of old.
Guard (node-listp new).; old — Original aignet that new may extend.
Guard (node-listp old).

Another way of looking at this is that the aignet new is an extension of old if old is some suffix of new.

This is a transitive, reflexive relation. This is a useful concept because every aignet-modifying function that doesn't reinitialize the AIG produces an extension of its input, and this relation implies many useful things.

In particular, any ID of the original aignet is an ID of the new aignet, and the node of that ID (and its entire suffix) is the same in both aignets. This implies, for example, that the evaluations of nodes existing in the first are the same as their evaluations in the second.

Definitions and Theorems

Function: aignet-extension-p

(defun aignet-extension-p (new old)
  (declare (xargs :guard (and (node-listp new)
                              (node-listp old))))
  (let ((__function__ 'aignet-extension-p))
    (declare (ignorable __function__))
    (or (node-list-equiv old new)
        (and (consp new)
             (aignet-extension-p (cdr new) old)))))

Theorem: aignet-extension-p-of-node-list-fix-new

(defthm acl2::aignet-extension-p-of-node-list-fix-new
  (equal (aignet-extension-p (node-list-fix new)
                             old)
         (aignet-extension-p new old)))

Theorem: aignet-extension-p-node-list-equiv-congruence-on-new

(defthm acl2::aignet-extension-p-node-list-equiv-congruence-on-new
  (implies (node-list-equiv new acl2::new-equiv)
           (equal (aignet-extension-p new old)
                  (aignet-extension-p acl2::new-equiv old)))
  :rule-classes :congruence)

Theorem: aignet-extension-p-of-node-list-fix-old

(defthm acl2::aignet-extension-p-of-node-list-fix-old
  (equal (aignet-extension-p new (node-list-fix old))
         (aignet-extension-p new old)))

Theorem: aignet-extension-p-node-list-equiv-congruence-on-old

(defthm acl2::aignet-extension-p-node-list-equiv-congruence-on-old
  (implies (node-list-equiv old acl2::old-equiv)
           (equal (aignet-extension-p new old)
                  (aignet-extension-p new acl2::old-equiv)))
  :rule-classes :congruence)

Theorem: fanin-count-when-aignet-extension

(defthm fanin-count-when-aignet-extension
  (implies (aignet-extension-p y x)
           (<= (fanin-count x) (fanin-count y)))
  :rule-classes ((:linear :trigger-terms ((fanin-count x)))))

Theorem: stype-count-when-aignet-extension

(defthm stype-count-when-aignet-extension
  (implies (aignet-extension-p y x)
           (<= (stype-count k x)
               (stype-count k y)))
  :rule-classes ((:linear :trigger-terms ((stype-count k x)))))

Theorem: fanin-count-cdr-when-aignet-extension-strong

(defthm fanin-count-cdr-when-aignet-extension-strong
  (implies (and (aignet-extension-p y x)
                (consp x)
                (fanin-node-p (car x)))
           (< (fanin-count (cdr x))
              (fanin-count y)))
  :rule-classes ((:linear :trigger-terms ((fanin-count (cdr x))))))

Theorem: stype-count-cdr-when-aignet-extension-p

(defthm stype-count-cdr-when-aignet-extension-p
  (implies (and (aignet-extension-p y x)
                (equal type (stype (car x)))
                (or (not (equal (stype-fix type) (const-stype)))
                    (consp x)))
           (< (stype-count type (cdr x))
              (stype-count type y)))
  :rule-classes
  ((:linear :trigger-terms ((stype-count type (cdr x))))))

Theorem: aignet-extension-p-transitive

(defthm aignet-extension-p-transitive
  (implies (and (aignet-extension-p x y)
                (aignet-extension-p y z))
           (aignet-extension-p x z))
  :rule-classes ((:rewrite :match-free :all)))

Theorem: aignet-extension-p-self

(defthm aignet-extension-p-self
  (aignet-extension-p x x))

Theorem: aignet-extension-p-cons

(defthm aignet-extension-p-cons
  (aignet-extension-p (cons x y) y))

Theorem: aignet-extension-p-cons-more

(defthm aignet-extension-p-cons-more
  (implies (aignet-extension-p y z)
           (aignet-extension-p (cons x y) z)))

Theorem: aignet-extension-p-cdr

(defthm aignet-extension-p-cdr
  (implies (and (aignet-extension-p y z) (consp z))
           (aignet-extension-p y (cdr z))))

Subtopics

Aignet-extension-bind-inverse: Find an appropriate free variable binding that is an aignet-extension of a bound variable.
Aignet-extension-binding: A strategy for making use of aignet-extension-p in rewrite rules.