		Search-engine friendly clone of the ACL2 documentation.

Aignet-extension-p

Aignet-extension-bind-inverse

Find an appropriate free variable binding that is an aignet-extension of a bound variable.

An example rule using this utility:

(defthm lookup-id-in-extension-inverse
    (implies (and (aignet-extension-bind-inverse :orig orig :new new)
                  (<= (nfix id) (fanin-count orig)))
             (equal (lookup-id id orig)
                    (lookup-id id new))))

Suppose this rule matches on the term (lookup-id id (lookup-reg->nxst n aignet)). Therefore, orig is bound to (lookup-reg->nxst n aignet). The invocation of aignet-extension-bind-inverse knows that the second argument of lookup-reg->nxst is an aignet that is (likely) an extension of the lookup (because the lookup finds some suffix of that argument). So it binds new to aignet, in this case. Thus, this rule can be used instead of a whole series of rules about individual functions that look up some suffix of an aignet, such as:

(implies (<= (nfix id) (fanin-count (lookup-reg->nxst n aignet))))
         (equal (lookup-id id (lookup-reg->nxst n aignet))
                (lookup-id id aignet)))

(implies (<= (nfix id) (fanin-count (lookup-stype n stype aignet))))
         (equal (lookup-id id (lookup-stype n stype aignet))
                (lookup-id id aignet)))

etc.

See also aignet-extension-binding for a similar macro that finds a binding for a suffix aignet from a term giving some extension.

Definitions and Theorems

Function: aignet-extension-bind-scan-lookups

(defun aignet-extension-bind-scan-lookups (term var table)
  (b* (((when (atom table)) nil)
       ((mv ok subst)
        (acl2::simple-one-way-unify (caar table)
                                    term nil))
       ((unless ok)
        (aignet-extension-bind-scan-lookups term var (cdr table)))
       (new (acl2::substitute-into-term (cdar table)
                                        subst)))
    (cons (cons var new) 'nil)))

Function: aignet-extension-bind-inverse-fn

(defun aignet-extension-bind-inverse-fn (x var mfc state)
 (declare (xargs :stobjs state)
          (ignorable mfc))
 (aignet-extension-bind-scan-lookups x var
                                     (table-alist 'aignet-lookup-fns
                                                  (w state))))

Theorem: fanin-count-when-aignet-extension-bind-inverse

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

Theorem: stype-count-when-aignet-extension-bind-inverse

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

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

(defthm fanin-count-cdr-when-aignet-extension-inverse
  (implies (and (aignet-extension-bind-inverse :orig x
                                               :new y)
                (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-inverse

(defthm stype-count-cdr-when-aignet-extension-inverse
  (implies (and (aignet-extension-bind-inverse :orig x
                                               :new y)
                (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))))))