		Search-engine friendly clone of the ACL2 documentation.

Aignet-comb-transforms

Constprop

Simplify a single-output aignet by assuming inputs from a top-level conjunction to be true.

Signature
(constprop aignet aignet2 config) → new-aignet2
Arguments: aignet — Input aignet.; aignet2 — New aignet -- will be emptied.; config — Settings for the transform.
Guard (constprop-config-p config).

Note: This should only be run on a single-output combinational aignet. In the current implementation it will return a copy of the original aignet otherwise; if we did attempt to apply the transform to each combinational output in a network having more than one, we might increase the size of the network.

This transform searches the top-level AND or OR gate nest of the output formula for conjuncts/disjuncts that imply that combinational inputs are equivalent to one another or to constants. It computes canonical forms of each of the equivalence classes yielded by this process (where constant literals are always the canonical representatives of their equivalence classes). It then rephrases the formula as follows. Suppose F is the top-level formula and C is the conjunction of all the inputs/negations. Let FC denote the substitution into F of each canonical representative for all the literals of its class. Then F is equivalent to FC & C. This sometimes decreases the size of the formula because the conjuncts within C may have other occurrences not in the top-level conjunction of F.

Definitions and Theorems

Function: constprop

(defun constprop (aignet aignet2 config)
 (declare (xargs :stobjs (aignet aignet2)))
 (declare (xargs :guard (constprop-config-p config)))
 (let ((__function__ 'constprop))
   (declare (ignorable __function__))
   (b*
     (((local-stobjs aignet-tmp)
       (mv aignet2 aignet-tmp))
      (aignet-tmp (constprop-core aignet aignet-tmp config))
      (aignet2
           (aignet-prune-comb aignet-tmp aignet2
                              (constprop-config->gatesimp config))))
     (mv aignet2 aignet-tmp))))

Theorem: num-ins-of-constprop

(defthm num-ins-of-constprop
  (b* ((?new-aignet2 (constprop aignet aignet2 config)))
    (equal (stype-count :pi new-aignet2)
           (stype-count :pi aignet))))

Theorem: num-regs-of-constprop

(defthm num-regs-of-constprop
  (b* ((?new-aignet2 (constprop aignet aignet2 config)))
    (equal (stype-count :reg new-aignet2)
           (stype-count :reg aignet))))

Theorem: num-outs-of-constprop

(defthm num-outs-of-constprop
  (b* ((?new-aignet2 (constprop aignet aignet2 config)))
    (equal (stype-count :po new-aignet2)
           (stype-count :po aignet))))

Theorem: constprop-comb-equivalent

(defthm constprop-comb-equivalent
  (b* ((?new-aignet2 (constprop aignet aignet2 config)))
    (comb-equiv new-aignet2 aignet)))

Theorem: normalize-inputs-of-constprop

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

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

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

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

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

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

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

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

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

Theorem: constprop-of-constprop-config-fix-config

(defthm constprop-of-constprop-config-fix-config
  (equal (constprop aignet
                    aignet2 (constprop-config-fix config))
         (constprop aignet aignet2 config)))

Theorem: constprop-constprop-config-equiv-congruence-on-config

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

Subtopics

Aignet-constprop-sweep
Aignet-lit-constprop-init-and-sweep
Aignet-lit-constprop
Aignet-constprop-sweep-invar
Constprop-iter
Constprop-once
Constprop-core
Constprop!: Like constprop, but overwrites the original network instead of returning a new one.
Constprop-config: Configuration object for the constprop aignet transform.
Aignet-constprop-stats