		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-core

Signature
(fraig-core strict-count aignet aignet2 config output-ranges state) → (mv new-aignet2 new-output-ranges new-state)
Arguments: strict-count — Number of initial outputs that must be combinationally preserved, or NIL meaning all.
Guard (acl2::maybe-natp strict-count).; aignet — Input aignet.; aignet2 — New aignet -- will be emptied.; config — Guard (fraig-config-p config).; output-ranges — Guard (aignet-output-range-map-p output-ranges).
Returns: new-output-ranges — Type (aignet-output-range-map-p new-output-ranges).

Definitions and Theorems

Function: fraig-core

(defun fraig-core (strict-count aignet
                                aignet2 config output-ranges state)
 (declare (xargs :stobjs (aignet aignet2 state)))
 (declare
     (xargs :guard (and (acl2::maybe-natp strict-count)
                        (fraig-config-p config)
                        (aignet-output-range-map-p output-ranges))))
 (declare (xargs :guard (or (not strict-count)
                            (<= strict-count (num-outs aignet)))))
 (let ((__function__ 'fraig-core))
   (declare (ignorable __function__))
   (b* (((local-stobjs copy strash classes s32v mark)
         (mv aignet2 copy strash
             classes s32v mark output-ranges state)))
     (fraig-core-aux strict-count
                     aignet aignet2 config output-ranges
                     copy strash classes s32v mark state))))

Theorem: aignet-output-range-map-p-of-fraig-core.new-output-ranges

(defthm aignet-output-range-map-p-of-fraig-core.new-output-ranges
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (fraig-core strict-count aignet
                    aignet2 config output-ranges state)))
    (aignet-output-range-map-p new-output-ranges))
  :rule-classes :rewrite)

Theorem: num-ins-of-fraig-core

(defthm num-ins-of-fraig-core
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (fraig-core strict-count aignet
                    aignet2 config output-ranges state)))
    (equal (stype-count :pi new-aignet2)
           (stype-count :pi aignet))))

Theorem: num-regs-of-fraig-core

(defthm num-regs-of-fraig-core
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (fraig-core strict-count aignet
                    aignet2 config output-ranges state)))
    (equal (stype-count :reg new-aignet2)
           (stype-count :reg aignet))))

Theorem: output-range-map-length-of-fraig-core

(defthm output-range-map-length-of-fraig-core
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (fraig-core strict-count aignet
                    aignet2 config output-ranges state)))
    (equal (aignet-output-range-map-length new-output-ranges)
           (stype-count :po new-aignet2))))

Theorem: num-outs-of-fraig-core

(defthm num-outs-of-fraig-core
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (fraig-core strict-count aignet
                    aignet2 config output-ranges state)))
    (implies (not strict-count)
             (equal (stype-count :po new-aignet2)
                    (stype-count :po aignet)))))

Theorem: num-outs-lower-bound-of-fraig-core-nonstrict

(defthm num-outs-lower-bound-of-fraig-core-nonstrict
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (fraig-core strict-count aignet
                    aignet2 config output-ranges state)))
    (implies strict-count
             (<= (nfix strict-count)
                 (stype-count :po new-aignet2))))
  :rule-classes :linear)

Theorem: fraig-core-comb-equivalent

(defthm fraig-core-comb-equivalent
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (fraig-core strict-count aignet
                    aignet2 config output-ranges state)))
    (implies (not strict-count)
             (comb-equiv new-aignet2 aignet))))

Theorem: output-eval-of-fraig-core-when-nonstrict

(defthm output-eval-of-fraig-core-when-nonstrict
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (fraig-core strict-count aignet
                    aignet2 config output-ranges state)))
    (implies (and strict-count
                  (< (nfix i) (nfix strict-count)))
             (equal (output-eval i invals regvals new-aignet2)
                    (output-eval i invals regvals aignet)))))

Theorem: normalize-input-of-fraig-core

(defthm normalize-input-of-fraig-core
  (implies (syntaxp (not (equal aignet2 ''nil)))
           (equal (fraig-core strict-count aignet
                              aignet2 config output-ranges state)
                  (fraig-core strict-count aignet
                              nil config output-ranges state))))

Theorem: w-state-of-fraig-core

(defthm w-state-of-fraig-core
  (b* (((mv ?new-aignet2
            ?new-output-ranges ?new-state)
        (fraig-core strict-count aignet
                    aignet2 config output-ranges state)))
    (equal (w new-state) (w state))))

Theorem: fraig-core-of-maybe-natp-fix-strict-count

(defthm fraig-core-of-maybe-natp-fix-strict-count
  (equal (fraig-core (acl2::maybe-natp-fix strict-count)
                     aignet
                     aignet2 config output-ranges state)
         (fraig-core strict-count aignet
                     aignet2 config output-ranges state)))

Theorem: fraig-core-maybe-nat-equiv-congruence-on-strict-count

(defthm fraig-core-maybe-nat-equiv-congruence-on-strict-count
  (implies (acl2::maybe-nat-equiv strict-count strict-count-equiv)
           (equal (fraig-core strict-count aignet
                              aignet2 config output-ranges state)
                  (fraig-core strict-count-equiv aignet
                              aignet2 config output-ranges state)))
  :rule-classes :congruence)

Theorem: fraig-core-of-fraig-config-fix-config

(defthm fraig-core-of-fraig-config-fix-config
  (equal (fraig-core strict-count
                     aignet aignet2 (fraig-config-fix config)
                     output-ranges state)
         (fraig-core strict-count aignet
                     aignet2 config output-ranges state)))

Theorem: fraig-core-fraig-config-equiv-congruence-on-config

(defthm fraig-core-fraig-config-equiv-congruence-on-config
  (implies (fraig-config-equiv config config-equiv)
           (equal (fraig-core strict-count aignet
                              aignet2 config output-ranges state)
                  (fraig-core strict-count aignet aignet2
                              config-equiv output-ranges state)))
  :rule-classes :congruence)

Theorem: fraig-core-of-aignet-output-range-map-fix-output-ranges

(defthm fraig-core-of-aignet-output-range-map-fix-output-ranges
  (equal (fraig-core strict-count aignet aignet2 config
                     (aignet-output-range-map-fix output-ranges)
                     state)
         (fraig-core strict-count aignet
                     aignet2 config output-ranges state)))

Theorem: fraig-core-aignet-output-range-map-equiv-congruence-on-output-ranges

(defthm
 fraig-core-aignet-output-range-map-equiv-congruence-on-output-ranges
 (implies
   (aignet-output-range-map-equiv output-ranges output-ranges-equiv)
   (equal (fraig-core strict-count aignet
                      aignet2 config output-ranges state)
          (fraig-core strict-count aignet aignet2
                      config output-ranges-equiv state)))
 :rule-classes :congruence)