• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
      • Representation
      • Aignet-copy-init
      • Aignet-simplify-with-tracking
      • Aignet-simplify-marked-with-tracking
      • Aignet-cnf
      • Aignet-simplify-marked
      • Aignet-complete-copy
      • Aignet-transforms
        • Aignet-output-ranges
        • Aignet-comb-transforms
          • Fraig
            • Fraig-config
            • Fraig-sweep-node
            • Fraig-sweep-aux
            • Fraig-finish-copy-nonstrict
            • Fraig-core-aux
            • Fraig-output-type
            • Ipasir-check-aignet-equivalence
            • Fraig-store-ctrex-aux
            • Fraig-finish-copy-outs
            • Fraig-core
            • Fraig-ctrexes-maybe-resim
            • Fraig-sweep
            • Fraig-store-ctrex
            • S32v-row-repeat-bitcols
            • Fraig-ctrexes-resim-aux
            • Fraig-config-normalized-output-map
            • S32v-copy-cares
            • Ipasir-maybe-recycle
            • Fraig-ctrexes-ok
            • Fraig-add-equiv-class-outputs-aux-2
            • Fraig-add-equiv-class-outputs-aux-1
            • Fraig-ctrexes-resim
            • Fraig-create-aignet-node-mask
            • Fraig-classes-maybe-delete-class
            • Aignet-copy-outs-range
            • Fraig-record-sat-ctrex-rec
            • Fraig-ctrex-has-relevant-disagreement
            • S32v-bitcol-nth-set
            • Fraig-output-map-mark-non-simplified
            • Fraig-output-map-mark-simplified
            • Fraig-output-map-initial-equiv-start/count
            • Fraig-minimize-sat-ctrex-rec
            • Fraig-create-output-map
            • Bitarr-copy-cares-to-s32v-col
            • S32v-install-bit
            • S32v-bitcol-count-set
            • Fraig-ctrexes-init
            • Bitarr-or-cares-with-s32v-col
            • Fraig-ctrex-find-agreeable
            • S32v-repeat-bitcols
            • S32v-add-salt
            • Bitarr-remove-marked
            • Print-fraig-stats-noninitial
            • Fraig-ctrex-regvals->vecsim
            • Fraig-ctrex-invals->vecsim
            • Bitarr-to-s32v-col
            • Fraig-output-map-entry
            • Aignet-unmark-higher-levels
            • Aignet-mark-output-node-range
            • Fraig-initial-sim
            • Fraig-ctrexes-reinit
            • Fraig-add-equiv-class-outputs
            • Aignet-maybe-update-refs
            • S32v-randomize-rows
            • S32v-get-bit
            • Fraig-level-limit-ok
            • Aignet-vals->regvals-after-invals
            • Aignet-mark-fanout-cones-of-marked
            • Fraig-debug-output-ranges
            • S32v-zero-rows
            • Fraig-output-map-total-count
            • Fraig-output-map-has-multiple-initial-equivs
            • Fraig-output-map-has-initial-equivs
            • Fraig-output-type-map
            • Aignet-vals->in/regvals
            • Fraig-output-map
            • Fraig-total-checks
            • Fraig-stats-count-sat-call
            • Fraig-ctrex-ncols
            • Fraig-ctrex-data-rows
            • Fraig-stats-update-last-chance
            • Print-fraig-stats-initial
            • Print-classes-counts-with-mark
            • Fraig-stats-increment-forced-proved
            • Fraig-stats-increment-coincident-nodes
            • Print-classes-counts
            • Fraig-ctrex-in/reg-rows
          • Parametrize
          • Observability-fix
          • Constprop
          • Apply-m-assumption-n-output-output-transform-default
          • Balance
          • Apply-n-output-comb-transform-default
          • Apply-comb-transform-default
          • Obs-constprop
          • Rewrite
          • Comb-transform
          • Abc-comb-simplify
          • Prune
          • Rewrite!
          • M-assumption-n-output-comb-transform->name
          • N-output-comb-transform->name
          • Comb-transform->name
          • N-output-comb-transformlist
          • M-assumption-n-output-comb-transformlist
          • Comb-transformlist
          • Apply-comb-transform
        • Aignet-m-assumption-n-output-transforms
        • Aignet-n-output-comb-transforms
      • Aignet-eval
      • Semantics
      • Aignet-read-aiger
      • Aignet-write-aiger
      • Aignet-abc-interface
      • Utilities
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Fraig

Fraig-core-aux

Signature

(fraig-core-aux strict-count 
                aignet aignet2 config output-ranges 
                copy strash classes s32v mark state) 
 
  → 
(mv new-aignet2 
    new-copy new-strash new-classes new-s32v 
    new-mark 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-aux

(defun fraig-core-aux
       (strict-count aignet aignet2 config output-ranges
                     copy strash classes s32v mark state)
 (declare
      (xargs :stobjs (aignet aignet2
                             copy strash classes s32v mark state)))
 (declare
     (xargs :guard (and (acl2::maybe-natp strict-count)
                        (fraig-config-p config)
                        (aignet-output-range-map-p output-ranges))))
 (declare
  (xargs
      :guard (non-exec (and (or (not strict-count)
                                (<= strict-count (num-outs aignet)))
                            (equal strash (create-strash))
                            (equal s32v (create-s32v))
                            (equal classes (create-classes))
                            (equal mark (acl2::create-bitarr))))))
 (let ((__function__ 'fraig-core-aux))
  (declare (ignorable __function__))
  (b*
   (((fraig-config config))
    (- (fraig-debug-output-ranges output-ranges aignet))
    ((mv outmap output-ranges)
     (fraig-config-normalized-output-map
          config output-ranges aignet))
    (- (and config.random-seed-name
            (acl2::seed-random$ config.random-seed-name)))
    (classes (mbe :logic (non-exec (create-classes))
                  :exec classes))
    (classes
     (cond
      (config.outs-only (classes-init-outs classes aignet))
      (config.miters-only (classes-init-out-miters classes aignet))
      ((fraig-output-map-has-initial-equivs outmap)
       (b*
        (((mv offset count)
          (fraig-output-map-initial-equiv-start/count outmap 0))
         (classes
              (classes-init-n-outputs count offset classes aignet)))
        (classes-check-consistency (num-fanins aignet)
                                   classes)
        (print-classes-counts classes)
        classes))
      (t (classes-init (num-fanins aignet)
                       classes))))
    (mark (fraig-create-aignet-node-mask
               aignet outmap config.level-limit mark))
    (- (print-classes-counts-with-mark classes mark)
       (classes-check-consistency (num-fanins aignet)
                                  classes))
    (s32v (mbe :logic (non-exec (create-s32v))
               :exec s32v))
    (s32v (s32v-resize-cols config.initial-sim-words s32v))
    (s32v (s32v-resize-rows (classes-size classes)
                            s32v))
    ((mv classes s32v state)
     (fraig-initial-sim config.initial-sim-rounds
                        s32v classes aignet state))
    (strash (mbe :logic (non-exec '(nil))
                 :exec (strashtab-init (num-gates aignet)
                                       nil nil strash)))
    ((mv copy aignet2)
     (init-copy-comb aignet copy aignet2))
    ((mv aignet2 copy strash classes state)
     (fraig-sweep aignet aignet2
                  copy strash classes mark config state))
    ((mv output-ranges aignet2)
     (fraig-finish-copy-nonstrict strict-count output-ranges
                                  config.save-candidate-equivs-as
                                  config.remove-candidate-equivs
                                  classes aignet copy aignet2)))
   (mv aignet2 copy strash classes
       s32v mark output-ranges state))))

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

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

Theorem: num-ins-of-fraig-core-aux

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

Theorem: num-regs-of-fraig-core-aux

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

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

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

Theorem: num-outs-of-fraig-core-aux

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

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

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

Theorem: fraig-core-aux-comb-equivalent

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

Theorem: classes-wellformed-of-fraig-core-aux

(defthm classes-wellformed-of-fraig-core-aux
  (b* (((mv ?new-aignet2 ?new-copy
            ?new-strash ?new-classes ?new-s32v
            ?new-mark ?new-output-ranges ?new-state)
        (fraig-core-aux strict-count
                        aignet aignet2 config output-ranges
                        copy strash classes s32v mark state)))
    (classes-wellformed new-classes)))

Theorem: classes-size-of-fraig-core-aux

(defthm classes-size-of-fraig-core-aux
  (b* (((mv ?new-aignet2 ?new-copy
            ?new-strash ?new-classes ?new-s32v
            ?new-mark ?new-output-ranges ?new-state)
        (fraig-core-aux strict-count
                        aignet aignet2 config output-ranges
                        copy strash classes s32v mark state)))
    (equal (classes-size new-classes)
           (num-fanins aignet))))

Theorem: normalize-input-of-fraig-core-aux

(defthm normalize-input-of-fraig-core-aux
  (implies
       (syntaxp (not (and (equal aignet2 ''nil)
                          (equal copy ''nil)
                          (equal strash ''nil)
                          (equal classes ''nil)
                          (equal s32v ''nil)
                          (equal mark ''nil))))
       (equal (fraig-core-aux aignet strict-count
                              aignet2 config output-ranges
                              copy strash classes s32v mark state)
              (fraig-core-aux aignet
                              strict-count nil config output-ranges
                              nil nil nil nil nil state))))

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

(defthm output-eval-of-fraig-core-aux-when-nonstrict
  (b* (((mv ?new-aignet2 ?new-copy
            ?new-strash ?new-classes ?new-s32v
            ?new-mark ?new-output-ranges ?new-state)
        (fraig-core-aux strict-count
                        aignet aignet2 config output-ranges
                        copy strash classes s32v mark 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: w-state-of-fraig-core-aux

(defthm w-state-of-fraig-core-aux
  (b* (((mv ?new-aignet2 ?new-copy
            ?new-strash ?new-classes ?new-s32v
            ?new-mark ?new-output-ranges ?new-state)
        (fraig-core-aux strict-count
                        aignet aignet2 config output-ranges
                        copy strash classes s32v mark state)))
    (equal (w new-state) (w state))))

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

(defthm fraig-core-aux-of-maybe-natp-fix-strict-count
  (equal (fraig-core-aux (acl2::maybe-natp-fix strict-count)
                         aignet aignet2 config output-ranges
                         copy strash classes s32v mark state)
         (fraig-core-aux strict-count
                         aignet aignet2 config output-ranges
                         copy strash classes s32v mark state)))

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

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

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

(defthm fraig-core-aux-of-fraig-config-fix-config
  (equal (fraig-core-aux strict-count
                         aignet aignet2 (fraig-config-fix config)
                         output-ranges
                         copy strash classes s32v mark state)
         (fraig-core-aux strict-count
                         aignet aignet2 config output-ranges
                         copy strash classes s32v mark state)))

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

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

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

(defthm fraig-core-aux-of-aignet-output-range-map-fix-output-ranges
  (equal (fraig-core-aux strict-count aignet aignet2 config
                         (aignet-output-range-map-fix output-ranges)
                         copy strash classes s32v mark state)
         (fraig-core-aux strict-count
                         aignet aignet2 config output-ranges
                         copy strash classes s32v mark state)))

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

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