		Search-engine friendly clone of the ACL2 documentation.

Constprop

Aignet-lit-constprop

Signature
(aignet-lit-constprop lit aignet gatesimp aignet2) → (mv new-lit new-aignet2)
Arguments: lit — Guard (litp lit).; gatesimp — Guard (gatesimp-p gatesimp).
Returns: new-lit — Type (litp new-lit).

Definitions and Theorems

Function: aignet-lit-constprop

(defun aignet-lit-constprop (lit aignet gatesimp aignet2)
  (declare (xargs :stobjs (aignet aignet2)))
  (declare (type (integer 0 *) lit))
  (declare (xargs :guard (and (litp lit) (gatesimp-p gatesimp))))
  (declare (xargs :split-types t
                  :guard (fanin-litp lit aignet)))
  (let ((__function__ 'aignet-lit-constprop))
    (declare (ignorable __function__))
    (b* (((local-stobjs copy strash)
          (mv new-lit aignet2 strash copy))
         ((mv constr-lit strash copy aignet2)
          (aignet-lit-constprop-init-and-sweep
               lit
               aignet gatesimp strash copy aignet2))
         ((acl2::hintcontext-bind ((sweep-aignet2 aignet2))))
         ((mv conj strash aignet2)
          (aignet-hash-and constr-lit (lit-copy (lit-abs lit) copy)
                           gatesimp strash aignet2))
         (result-lit (lit-negate-cond conj (lit->neg lit)))
         ((acl2::hintcontext :here)))
      (mv result-lit aignet2 strash copy))))

Theorem: litp-of-aignet-lit-constprop.new-lit

(defthm litp-of-aignet-lit-constprop.new-lit
  (b* (((mv ?new-lit ?new-aignet2)
        (aignet-lit-constprop lit aignet gatesimp aignet2)))
    (litp new-lit))
  :rule-classes :rewrite)

Theorem: stype-count-of-aignet-lit-constprop

(defthm stype-count-of-aignet-lit-constprop
  (b* (((mv ?new-lit ?new-aignet2)
        (aignet-lit-constprop lit aignet gatesimp aignet2)))
    (and (equal (stype-count :pi new-aignet2)
                (stype-count :pi aignet))
         (equal (stype-count :reg new-aignet2)
                (stype-count :reg aignet))
         (equal (stype-count :po new-aignet2) 0)
         (equal (stype-count :nxst new-aignet2)
                0)
         (equal (stype-count :const new-aignet2)
                0))))

Theorem: aignet-litp-of-aignet-lit-constprop

(defthm aignet-litp-of-aignet-lit-constprop
  (b* (((mv ?new-lit ?new-aignet2)
        (aignet-lit-constprop lit aignet gatesimp aignet2)))
    (implies (and (aignet-litp lit aignet))
             (aignet-litp new-lit new-aignet2))))

Theorem: aignet-lit-constprop-correct

(defthm aignet-lit-constprop-correct
  (b* (((mv ?new-lit ?new-aignet2)
        (aignet-lit-constprop lit aignet gatesimp aignet2)))
    (implies (aignet-litp lit aignet)
             (equal (lit-eval new-lit invals regvals new-aignet2)
                    (lit-eval lit invals regvals aignet)))))

Theorem: normalize-inputs-of-aignet-lit-constprop

(defthm normalize-inputs-of-aignet-lit-constprop
 (b* nil
  (implies
    (syntaxp (not (equal aignet2 ''nil)))
    (equal (aignet-lit-constprop lit aignet gatesimp aignet2)
           (let ((aignet2 nil))
             (aignet-lit-constprop lit aignet gatesimp aignet2))))))

Theorem: aignet-lit-constprop-of-lit-fix-lit

(defthm aignet-lit-constprop-of-lit-fix-lit
  (equal (aignet-lit-constprop (lit-fix lit)
                               aignet gatesimp aignet2)
         (aignet-lit-constprop lit aignet gatesimp aignet2)))

Theorem: aignet-lit-constprop-lit-equiv-congruence-on-lit

(defthm aignet-lit-constprop-lit-equiv-congruence-on-lit
 (implies
   (lit-equiv lit lit-equiv)
   (equal (aignet-lit-constprop lit aignet gatesimp aignet2)
          (aignet-lit-constprop lit-equiv aignet gatesimp aignet2)))
 :rule-classes :congruence)

Theorem: aignet-lit-constprop-of-node-list-fix-aignet

(defthm aignet-lit-constprop-of-node-list-fix-aignet
  (equal (aignet-lit-constprop lit (node-list-fix aignet)
                               gatesimp aignet2)
         (aignet-lit-constprop lit aignet gatesimp aignet2)))

Theorem: aignet-lit-constprop-node-list-equiv-congruence-on-aignet

(defthm aignet-lit-constprop-node-list-equiv-congruence-on-aignet
 (implies
   (node-list-equiv aignet aignet-equiv)
   (equal (aignet-lit-constprop lit aignet gatesimp aignet2)
          (aignet-lit-constprop lit aignet-equiv gatesimp aignet2)))
 :rule-classes :congruence)

Theorem: aignet-lit-constprop-of-gatesimp-fix-gatesimp

(defthm aignet-lit-constprop-of-gatesimp-fix-gatesimp
  (equal (aignet-lit-constprop lit aignet (gatesimp-fix gatesimp)
                               aignet2)
         (aignet-lit-constprop lit aignet gatesimp aignet2)))

Theorem: aignet-lit-constprop-gatesimp-equiv-congruence-on-gatesimp

(defthm aignet-lit-constprop-gatesimp-equiv-congruence-on-gatesimp
 (implies
   (gatesimp-equiv gatesimp gatesimp-equiv)
   (equal (aignet-lit-constprop lit aignet gatesimp aignet2)
          (aignet-lit-constprop lit aignet gatesimp-equiv aignet2)))
 :rule-classes :congruence)

Theorem: aignet-lit-constprop-of-node-list-fix-aignet2

(defthm aignet-lit-constprop-of-node-list-fix-aignet2
 (equal
      (aignet-lit-constprop lit
                            aignet gatesimp (node-list-fix aignet2))
      (aignet-lit-constprop lit aignet gatesimp aignet2)))

Theorem: aignet-lit-constprop-node-list-equiv-congruence-on-aignet2

(defthm aignet-lit-constprop-node-list-equiv-congruence-on-aignet2
 (implies
   (node-list-equiv aignet2 aignet2-equiv)
   (equal (aignet-lit-constprop lit aignet gatesimp aignet2)
          (aignet-lit-constprop lit aignet gatesimp aignet2-equiv)))
 :rule-classes :congruence)