		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-sweep-aux

Signature
(fraig-sweep-aux node aignet aignet2 copy strash fraig-ctrexes classes mark aignet-refcounts sat-lits ipasir fraig-stats config state) → (mv new-aignet2 new-copy new-strash new-fraig-ctrexes new-classes new-refcounts new-sat-lits new-ipasir new-fraig-stats new-state)
Arguments: node — Current node ID.
Guard (natp node).; aignet — Input aignet.; aignet2 — New aignet.; copy — Mapping from old to new aignet.; strash — strash for aignet2.; fraig-ctrexes — memory in which to simulate ctrexes.; classes — equiv classes data structure.; mark — Bit array marking nodes to simplify.; aignet-refcounts — refcounts for aignet2 for sat generation.; sat-lits — sat lit mapping for aignet2.; ipasir — sat solver on aignet2.; fraig-stats — statistics collection.; config — Guard (fraig-config-p config).

Definitions and Theorems

Function: fraig-sweep-aux

(defun fraig-sweep-aux
       (node aignet aignet2 copy strash fraig-ctrexes
             classes mark aignet-refcounts sat-lits
             ipasir fraig-stats config state)
 (declare
      (xargs :stobjs (aignet aignet2 copy strash fraig-ctrexes
                             classes mark aignet-refcounts
                             sat-lits ipasir fraig-stats state)))
 (declare (xargs :guard (and (natp node)
                             (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))
          (fraig-ctrexes-ok fraig-ctrexes)
          (equal (fraig-ctrex-data-rows fraig-ctrexes)
                 (num-fanins aignet))
          (equal (fraig-ctrex-in/reg-rows fraig-ctrexes)
                 (+ (num-ins aignet) (num-regs aignet)))
          (<= node (num-fanins aignet))
          (equal (num-ins aignet)
                 (num-ins aignet2))
          (equal (num-regs aignet)
                 (num-regs aignet2))
          (non-exec (and (not (eq (ipasir$a->status ipasir) :undef))
                         (not (ipasir$a->new-clause ipasir))
                         (not (ipasir$a->assumption ipasir))))
          (sat-lits-wfp sat-lits aignet2))))
 (let ((__function__ 'fraig-sweep-aux))
   (declare (ignorable __function__))
   (b*
    (((when (mbe :logic (zp (+ (num-fanins aignet) (- (nfix node))))
                 :exec (eql (num-fanins aignet) node)))
      (b* ((ipasir (ipasir-cancel-new-clause ipasir))
           (ipasir (ipasir-cancel-assumption ipasir))
           (ipasir (ipasir-input ipasir)))
        (mv aignet2 copy strash
            fraig-ctrexes classes aignet-refcounts
            sat-lits ipasir fraig-stats state)))
     ((mv aignet2 copy strash
          fraig-ctrexes classes aignet-refcounts
          sat-lits ipasir fraig-stats state)
      (fraig-sweep-node node
                        aignet aignet2 copy strash fraig-ctrexes
                        classes mark aignet-refcounts sat-lits
                        ipasir fraig-stats config state)))
    (fraig-sweep-aux (+ 1 (lnfix node))
                     aignet aignet2 copy strash fraig-ctrexes
                     classes mark aignet-refcounts sat-lits
                     ipasir fraig-stats config state))))

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

(defthm aignet-extension-p-of-fraig-sweep-aux
 (aignet-extension-p
   (mv-nth 0
           (fraig-sweep-aux node
                            aignet aignet2 copy strash fraig-ctrexes
                            classes mark aignet-refcounts sat-lits
                            ipasir fraig-stats config state))
   aignet2)
 :rule-classes :rewrite)

Theorem: ipasir-guard-of-fraig-sweep-aux

(defthm ipasir-guard-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
    (and (not (equal (ipasir$a->status new-ipasir)
                     :undef))
         (not (ipasir$a->new-clause new-ipasir))
         (not (ipasir$a->assumption new-ipasir)))))

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

(defthm classes-wellformed-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
    (implies (classes-wellformed classes)
             (classes-wellformed new-classes))))

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

(defthm classes-size-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
    (equal (classes-size new-classes)
           (classes-size classes))))

Theorem: fraig-ctrex-data-rows-of-fraig-sweep-aux

(defthm fraig-ctrex-data-rows-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
    (implies (equal (fraig-ctrex-data-rows fraig-ctrexes)
                    (num-fanins aignet))
             (equal (fraig-ctrex-data-rows new-fraig-ctrexes)
                    (num-fanins aignet)))))

Theorem: fraig-ctrex-in/reg-rows-of-fraig-sweep-aux

(defthm fraig-ctrex-in/reg-rows-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
    (implies (equal (fraig-ctrex-in/reg-rows fraig-ctrexes)
                    (+ (num-ins aignet2)
                       (num-regs aignet2)))
             (equal (fraig-ctrex-in/reg-rows new-fraig-ctrexes)
                    (+ (num-ins aignet2)
                       (num-regs aignet2))))))

Theorem: fraig-ctrex-ncols-of-fraig-sweep-aux

(defthm fraig-ctrex-ncols-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
    (equal (fraig-ctrex-ncols new-fraig-ctrexes)
           (fraig-ctrex-ncols fraig-ctrexes))))

Theorem: fraig-ctrexes-ok-of-fraig-sweep-aux

(defthm fraig-ctrexes-ok-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
    (implies (and (fraig-ctrexes-ok fraig-ctrexes)
                  (classes-wellformed classes)
                  (equal (classes-size classes)
                         (num-fanins aignet))
                  (equal (fraig-ctrex-data-rows fraig-ctrexes)
                         (num-fanins aignet))
                  (<= (nfix (fraig-ctrex-nbits fraig-ctrexes))
                      (* 32 (fraig-ctrex-ncols fraig-ctrexes)))
                  (equal (fraig-ctrex-in/reg-rows fraig-ctrexes)
                         (+ (num-ins aignet2)
                            (num-regs aignet2))))
             (fraig-ctrexes-ok new-fraig-ctrexes))))

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

(defthm stype-count-preserved-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats 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-aux

(defthm copy-len-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
    (implies (and (< (fanin-count aignet) (len copy))
                  (<= (nfix node) (fanin-count aignet)))
             (equal (len new-copy) (len copy)))))

Theorem: sat-lits-wfp-of-fraig-sweep-aux

(defthm sat-lits-wfp-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
    (implies (sat-lits-wfp sat-lits aignet2)
             (sat-lits-wfp new-sat-lits new-aignet2))))

Theorem: ipasir-formula-wfp-of-fraig-sweep-aux

(defthm ipasir-formula-wfp-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
    (implies (and (sat-lits-wfp sat-lits aignet2)
                  (aignet-copies-in-bounds copy aignet2)
                  (sat-lit-list-listp (ipasir$a->formula ipasir)
                                      sat-lits)
                  (<= (nfix node) (fanin-count aignet)))
             (sat-lit-list-listp (ipasir$a->formula new-ipasir)
                                 new-sat-lits))))

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

(defthm aignet-copies-ok-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
    (implies (and (aignet-copies-in-bounds copy aignet2)
                  (equal n (+ 1 (fanin-count aignet))))
             (aignet-copies-in-bounds new-copy new-aignet2))))

Theorem: cnf-for-aignet-of-fraig-sweep-aux

(defthm cnf-for-aignet-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
    (implies (and (cnf-for-aignet aignet2 (ipasir$a->formula ipasir)
                                  sat-lits)
                  (sat-lits-wfp sat-lits aignet2)
                  (aignet-copies-in-bounds copy aignet2)
                  (sat-lit-list-listp (ipasir$a->formula ipasir)
                                      sat-lits))
             (cnf-for-aignet new-aignet2
                             (ipasir$a->formula new-ipasir)
                             new-sat-lits))))

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

(defthm
    aignet-copy-is-comb-equivalent-for-non-gates-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats 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-aux

(defthm aignet-copy-is-comb-equivalent-of-fraig-sweep-aux
 (b* (((mv ?new-aignet2 ?new-copy ?new-strash
           ?new-fraig-ctrexes ?new-classes
           ?new-refcounts ?new-sat-lits
           ?new-ipasir ?new-fraig-stats ?new-state)
       (fraig-sweep-aux node
                        aignet aignet2 copy strash fraig-ctrexes
                        classes mark aignet-refcounts sat-lits
                        ipasir fraig-stats config state)))
  (implies
     (and (aignet-copy-is-comb-equivalent node aignet copy aignet2)
          (aignet-copy-is-comb-equivalent-for-non-gates
               (num-fanins aignet)
               aignet copy aignet2)
          (cnf-for-aignet aignet2 (ipasir$a->formula ipasir)
                          sat-lits)
          (sat-lits-wfp sat-lits aignet2)
          (aignet-copies-in-bounds copy aignet2)
          (sat-lit-list-listp (ipasir$a->formula ipasir)
                              sat-lits))
     (aignet-copy-is-comb-equivalent (+ 1 (fanin-count aignet))
                                     aignet new-copy new-aignet2))))

Theorem: w-state-of-fraig-sweep-aux

(defthm w-state-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
    (equal (w new-state) (w state))))

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

(defthm lit-copy-0-of-fraig-sweep-aux
  (b* (((mv ?new-aignet2 ?new-copy ?new-strash
            ?new-fraig-ctrexes ?new-classes
            ?new-refcounts ?new-sat-lits
            ?new-ipasir ?new-fraig-stats ?new-state)
        (fraig-sweep-aux node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
    (equal (lit-copy 0 new-copy)
           (lit-copy 0 copy))))

Theorem: fraig-sweep-aux-of-nfix-node

(defthm fraig-sweep-aux-of-nfix-node
  (equal (fraig-sweep-aux (nfix node)
                          aignet aignet2 copy strash fraig-ctrexes
                          classes mark aignet-refcounts sat-lits
                          ipasir fraig-stats config state)
         (fraig-sweep-aux node
                          aignet aignet2 copy strash fraig-ctrexes
                          classes mark aignet-refcounts sat-lits
                          ipasir fraig-stats config state)))

Theorem: fraig-sweep-aux-nat-equiv-congruence-on-node

(defthm fraig-sweep-aux-nat-equiv-congruence-on-node
 (implies
    (nat-equiv node node-equiv)
    (equal (fraig-sweep-aux node
                            aignet aignet2 copy strash fraig-ctrexes
                            classes mark aignet-refcounts sat-lits
                            ipasir fraig-stats config state)
           (fraig-sweep-aux node-equiv
                            aignet aignet2 copy strash fraig-ctrexes
                            classes mark aignet-refcounts sat-lits
                            ipasir fraig-stats config state)))
 :rule-classes :congruence)

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

(defthm fraig-sweep-aux-of-fraig-config-fix-config
  (equal (fraig-sweep-aux node aignet aignet2
                          copy strash fraig-ctrexes classes
                          mark aignet-refcounts sat-lits ipasir
                          fraig-stats (fraig-config-fix config)
                          state)
         (fraig-sweep-aux node
                          aignet aignet2 copy strash fraig-ctrexes
                          classes mark aignet-refcounts sat-lits
                          ipasir fraig-stats config state)))

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

(defthm fraig-sweep-aux-fraig-config-equiv-congruence-on-config
 (implies
    (fraig-config-equiv config config-equiv)
    (equal (fraig-sweep-aux node
                            aignet aignet2 copy strash fraig-ctrexes
                            classes mark aignet-refcounts sat-lits
                            ipasir fraig-stats config state)
           (fraig-sweep-aux node
                            aignet aignet2 copy strash fraig-ctrexes
                            classes mark aignet-refcounts sat-lits
                            ipasir fraig-stats config-equiv state)))
 :rule-classes :congruence)