		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-sweep

Signature
(fraig-sweep aignet aignet2 copy strash classes mark config state) → (mv new-aignet2 new-copy new-strash new-classes new-state)
Arguments: aignet — Input aignet.; aignet2 — New aignet.; copy — Mapping from old to new aignet.; strash — strash for aignet2.; classes — equiv classes data structure.; mark — bitarr marking nodes to be simplified.; config — Guard (fraig-config-p config).

Definitions and Theorems

Function: fraig-sweep

(defun fraig-sweep (aignet aignet2
                           copy strash classes mark config state)
 (declare (xargs :stobjs (aignet aignet2
                                 copy strash classes mark state)))
 (declare (xargs :guard (fraig-config-p config)))
 (declare (xargs :guard (and (<= (num-fanins aignet)
                                 (lits-length copy))
                             (<= (num-fanins aignet)
                                 (bits-length mark))
                             (aignet-copies-in-bounds copy aignet2)
                             (classes-wellformed classes)
                             (equal (classes-size classes)
                                    (num-fanins aignet))
                             (equal (num-ins aignet)
                                    (num-ins aignet2))
                             (equal (num-regs aignet)
                                    (num-regs aignet2)))))
 (let ((__function__ 'fraig-sweep))
  (declare (ignorable __function__))
  (b*
   (((local-stobjs fraig-ctrexes
                   sat-lits aignet-refcounts fraig-stats)
     (mv aignet2 copy strash
         fraig-ctrexes classes aignet-refcounts
         sat-lits fraig-stats state))
    ((ipasir::local-ipasir ipasir)
     (mv aignet2 copy strash
         fraig-ctrexes classes aignet-refcounts
         sat-lits ipasir fraig-stats state))
    ((fraig-config config))
    (ipasir (ipasir-set-limit ipasir config.ipasir-limit))
    (fraig-ctrexes
         (fraig-ctrexes-init config.sim-words fraig-ctrexes aignet))
    (sat-lits (resize-aignet->sat (ash (num-fanins aignet) -1)
                                  sat-lits))
    ((mv nclasses nconst-lits nclass-lits)
     (classes-counts-with-mark classes mark))
    (fraig-stats
         (update-fraig-initial-nclasses nclasses fraig-stats))
    (fraig-stats
         (update-fraig-initial-nconst-lits nconst-lits fraig-stats))
    (fraig-stats
         (update-fraig-initial-nclass-lits nclass-lits fraig-stats))
    (- (print-fraig-stats-initial fraig-stats))
    ((mv aignet2 copy strash
         fraig-ctrexes classes aignet-refcounts
         sat-lits ipasir fraig-stats state)
     (fraig-sweep-aux 0
                      aignet aignet2 copy strash fraig-ctrexes
                      classes mark aignet-refcounts sat-lits
                      ipasir fraig-stats config state))
    ((mv classes fraig-ctrexes fraig-stats state)
     (if
      (and config.final-force-resim
           (not (eql 0 (fraig-ctrex-nbits fraig-ctrexes))))
      (fraig-ctrexes-resim aignet
                           fraig-ctrexes classes fraig-stats state)
      (mv classes
          fraig-ctrexes fraig-stats state)))
    (- (print-aignet-stats "Tmp" aignet2))
    (- (print-fraig-stats-noninitial
            classes ipasir fraig-stats mark)))
   (mv aignet2 copy strash
       fraig-ctrexes classes aignet-refcounts
       sat-lits ipasir fraig-stats state))))

Theorem: aignet-extension-p-of-fraig-sweep

(defthm aignet-extension-p-of-fraig-sweep
  (aignet-extension-p
       (mv-nth 0
               (fraig-sweep aignet aignet2
                            copy strash classes mark config state))
       aignet2)
  :rule-classes :rewrite)

Theorem: classes-wellformed-of-fraig-sweep

(defthm classes-wellformed-of-fraig-sweep
  (b* (((mv ?new-aignet2 ?new-copy
            ?new-strash ?new-classes ?new-state)
        (fraig-sweep aignet aignet2
                     copy strash classes mark config state)))
    (implies (classes-wellformed classes)
             (classes-wellformed new-classes))))

Theorem: classes-size-of-fraig-sweep

(defthm classes-size-of-fraig-sweep
  (b* (((mv ?new-aignet2 ?new-copy
            ?new-strash ?new-classes ?new-state)
        (fraig-sweep aignet aignet2
                     copy strash classes mark config state)))
    (equal (classes-size new-classes)
           (classes-size classes))))

Theorem: stype-count-preserved-of-fraig-sweep

(defthm stype-count-preserved-of-fraig-sweep
  (b* (((mv ?new-aignet2 ?new-copy
            ?new-strash ?new-classes ?new-state)
        (fraig-sweep aignet aignet2
                     copy strash classes mark config state)))
    (implies (and (not (eq (stype-fix stype) (and-stype)))
                  (not (eq (stype-fix stype) (xor-stype))))
             (equal (stype-count stype new-aignet2)
                    (stype-count stype aignet2)))))

Theorem: copy-len-of-fraig-sweep

(defthm copy-len-of-fraig-sweep
  (b* (((mv ?new-aignet2 ?new-copy
            ?new-strash ?new-classes ?new-state)
        (fraig-sweep aignet aignet2
                     copy strash classes mark config state)))
    (implies (< (fanin-count aignet) (len copy))
             (equal (len new-copy) (len copy)))))

Theorem: aignet-copies-ok-of-fraig-sweep

(defthm aignet-copies-ok-of-fraig-sweep
  (b* (((mv ?new-aignet2 ?new-copy
            ?new-strash ?new-classes ?new-state)
        (fraig-sweep aignet aignet2
                     copy strash classes mark config state)))
    (implies (aignet-copies-in-bounds copy aignet2)
             (aignet-copies-in-bounds new-copy new-aignet2))))

Theorem: aignet-copy-is-comb-equivalent-for-non-gates-of-fraig-sweep

(defthm aignet-copy-is-comb-equivalent-for-non-gates-of-fraig-sweep
  (b* (((mv ?new-aignet2 ?new-copy
            ?new-strash ?new-classes ?new-state)
        (fraig-sweep aignet aignet2
                     copy strash classes mark config state)))
    (implies (and (aignet-copy-is-comb-equivalent-for-non-gates
                       (num-fanins aignet)
                       aignet copy aignet2)
                  (aignet-copies-in-bounds copy aignet2))
             (aignet-copy-is-comb-equivalent-for-non-gates
                  (+ 1 (fanin-count aignet))
                  aignet new-copy new-aignet2))))

Theorem: aignet-copy-is-comb-equivalent-of-fraig-sweep

(defthm aignet-copy-is-comb-equivalent-of-fraig-sweep
 (b* (((mv ?new-aignet2 ?new-copy
           ?new-strash ?new-classes ?new-state)
       (fraig-sweep aignet aignet2
                    copy strash classes mark config state)))
  (implies
     (and (aignet-copy-is-comb-equivalent-for-non-gates
               (num-fanins aignet)
               aignet copy aignet2)
          (aignet-copies-in-bounds copy aignet2))
     (aignet-copy-is-comb-equivalent (+ 1 (fanin-count aignet))
                                     aignet new-copy new-aignet2))))

Theorem: w-state-of-fraig-sweep

(defthm w-state-of-fraig-sweep
  (b* (((mv ?new-aignet2 ?new-copy
            ?new-strash ?new-classes ?new-state)
        (fraig-sweep aignet aignet2
                     copy strash classes mark config state)))
    (equal (w new-state) (w state))))

Theorem: lit-copy-0-of-fraig-sweep

(defthm lit-copy-0-of-fraig-sweep
  (b* (((mv ?new-aignet2 ?new-copy
            ?new-strash ?new-classes ?new-state)
        (fraig-sweep aignet aignet2
                     copy strash classes mark config state)))
    (equal (lit-copy 0 new-copy)
           (lit-copy 0 copy))))

Theorem: fraig-sweep-of-fraig-config-fix-config

(defthm fraig-sweep-of-fraig-config-fix-config
  (equal (fraig-sweep aignet aignet2 copy strash
                      classes mark (fraig-config-fix config)
                      state)
         (fraig-sweep aignet aignet2
                      copy strash classes mark config state)))

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

(defthm fraig-sweep-fraig-config-equiv-congruence-on-config
 (implies (fraig-config-equiv config config-equiv)
          (equal (fraig-sweep aignet aignet2
                              copy strash classes mark config state)
                 (fraig-sweep aignet aignet2 copy strash
                              classes mark config-equiv state)))
 :rule-classes :congruence)