		Search-engine friendly clone of the ACL2 documentation.

Aignet-comb-transforms

Obs-constprop

Combine constprop and observability-fix for a transform that is sometimes somewhat better than simply running both in sequence.

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

Definitions and Theorems

Function: obs-constprop

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

Theorem: num-ins-of-obs-constprop

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

Theorem: num-regs-of-obs-constprop

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

Theorem: num-outs-of-obs-constprop

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

Theorem: obs-constprop-comb-equivalent

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

Theorem: normalize-inputs-of-obs-constprop

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

Theorem: w-state-of-obs-constprop

(defthm w-state-of-obs-constprop
  (b* (((mv ?new-aignet2 ?new-state)
        (obs-constprop aignet aignet2 config state)))
    (equal (w new-state) (w state))))

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

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

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

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

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

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

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

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

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

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

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

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

Subtopics

Obs-constprop-config: Configuration object for the obs-constprop aignet transform.
Obs-constprop!: Like obs-constprop, but overwrites the original network instead of returning a new one.