		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-sweep-node

Signature
(fraig-sweep-node 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 — options.
Guard (fraig-config-p config).

Definitions and Theorems

Function: fraig-sweep-node

(defun fraig-sweep-node
       (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)))
          (id-existsp node 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-node))
  (declare (ignorable __function__))
  (b* ((n (lnfix node))
       (slot0 (id->slot n 0 aignet))
       (type (snode->type slot0))
       (ipasir (ipasir-cancel-new-clause ipasir))
       (ipasir (ipasir-cancel-assumption ipasir))
       (ipasir (ipasir-input ipasir)))
   (aignet-case
    type :in
    (mv aignet2 copy strash
        fraig-ctrexes classes aignet-refcounts
        sat-lits ipasir fraig-stats state)
    :out
    (mv aignet2 copy strash
        fraig-ctrexes classes aignet-refcounts
        sat-lits ipasir fraig-stats state)
    :const
    (mv aignet2 copy strash
        fraig-ctrexes classes aignet-refcounts
        sat-lits ipasir fraig-stats state)
    :gate
    (b*
     ((fraig-stats (update-fraig-gates-processed
                        (+ 1 (fraig-gates-processed fraig-stats))
                        fraig-stats))
      ((mv forced-refinedp
           classes fraig-ctrexes fraig-stats state)
       (fraig-ctrexes-maybe-resim n config aignet fraig-ctrexes
                                  classes fraig-stats state))
      (lit0 (snode->fanin slot0))
      (slot1 (id->slot n 1 aignet))
      (lit1 (snode->fanin slot1))
      (lit0-copy (lit-copy lit0 copy))
      (lit1-copy (lit-copy lit1 copy))
      (prev-count (num-fanins aignet2))
      ((fraig-config config))
      ((mv and-lit strash aignet2)
       (if (eql 1 (snode->regp slot1))
           (aignet-hash-xor lit0-copy lit1-copy
                            config.gatesimp strash aignet2)
         (aignet-hash-and lit0-copy lit1-copy
                          config.gatesimp strash aignet2)))
      (aignet-refcounts (aignet-maybe-update-refs
                             prev-count aignet-refcounts aignet2))
      (copy (set-lit n and-lit copy))
      ((when (eql 0 (get-bit n mark)))
       (mv aignet2 copy strash
           fraig-ctrexes classes aignet-refcounts
           sat-lits ipasir fraig-stats state))
      (equiv-node (node-head n classes))
      ((when (>= equiv-node n))
       (mv aignet2 copy strash
           fraig-ctrexes classes aignet-refcounts
           sat-lits ipasir fraig-stats state))
      (equiv-lit (make-lit equiv-node
                           (b-xor (id->phase equiv-node aignet)
                                  (snode->phase slot1))))
      (equiv-copy (lit-copy equiv-lit copy))
      ((when (eql equiv-copy and-lit))
       (b*
        ((fraig-stats
              (fraig-stats-increment-coincident-nodes fraig-stats)))
        (mv aignet2 copy strash
            fraig-ctrexes classes aignet-refcounts
            sat-lits ipasir fraig-stats state)))
      (- (and (eql 0
                   (logand 255 (fraig-total-checks fraig-stats)))
              (print-fraig-stats-noninitial
                   classes ipasir fraig-stats mark
                   :start-node n)))
      (-
       (and
        (eql (lit-id equiv-copy)
             (lit-id and-lit))
        (raise
         "Programming error -- node and equivalence candidate were the same ID but negated")))
      ((mv status sat-lits ipasir fraig-stats)
       (ipasir-check-aignet-equivalence
            and-lit equiv-copy
            config aignet2 aignet-refcounts
            sat-lits ipasir fraig-stats))
      ((when (eq status :failed))
       (b* (((mv classes fraig-stats)
             (fraig-classes-maybe-delete-class
                  config.delete-class-on-fail
                  n classes fraig-stats)))
         (mv aignet2 copy strash
             fraig-ctrexes classes aignet-refcounts
             sat-lits ipasir fraig-stats state)))
      ((when (eq status :unsat))
       (b* ((fraig-stats (fraig-stats-increment-forced-proved
                              forced-refinedp fraig-stats))
            (copy (set-lit n equiv-copy copy)))
         (mv aignet2 copy strash
             fraig-ctrexes classes aignet-refcounts
             sat-lits ipasir fraig-stats state)))
      ((mv fraig-ctrexes state)
       (fraig-store-ctrex and-lit equiv-copy equiv-node aignet2
                          sat-lits ipasir fraig-ctrexes state)))
     (mv aignet2 copy strash
         fraig-ctrexes classes aignet-refcounts
         sat-lits ipasir fraig-stats state))))))

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

(defthm aignet-extension-p-of-fraig-sweep-node
 (aignet-extension-p
  (mv-nth 0
          (fraig-sweep-node 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-node

(defthm ipasir-guard-of-fraig-sweep-node
  (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-node 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-node

(defthm classes-wellformed-of-fraig-sweep-node
  (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-node 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-node

(defthm classes-size-of-fraig-sweep-node
  (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-node 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-node

(defthm fraig-ctrex-data-rows-of-fraig-sweep-node
  (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-node 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-node

(defthm fraig-ctrex-in/reg-rows-of-fraig-sweep-node
  (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-node 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-node

(defthm fraig-ctrex-ncols-of-fraig-sweep-node
  (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-node 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-node

(defthm fraig-ctrexes-ok-of-fraig-sweep-node
  (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-node 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))
                  (<= (nfix node) (fanin-count 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-node

(defthm stype-count-preserved-of-fraig-sweep-node
  (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-node 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-node

(defthm copy-len-of-fraig-sweep-node
  (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-node 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-node

(defthm sat-lits-wfp-of-fraig-sweep-node
  (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-node 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-node

(defthm ipasir-formula-wfp-of-fraig-sweep-node
  (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-node 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-node

(defthm aignet-copies-ok-of-fraig-sweep-node
  (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-node 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)))
                  (<= (nfix node) (fanin-count aignet)))
             (aignet-copies-in-bounds new-copy new-aignet2))))

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

(defthm cnf-for-aignet-of-fraig-sweep-node
  (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-node 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-node

(defthm
   aignet-copy-is-comb-equivalent-for-non-gates-of-fraig-sweep-node
  (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-node 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-node

(defthm aignet-copy-is-comb-equivalent-of-fraig-sweep-node
 (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-node node
                         aignet aignet2 copy strash fraig-ctrexes
                         classes mark aignet-refcounts sat-lits
                         ipasir fraig-stats config state)))
  (implies
     (and (nat-equiv node1 node)
          (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)
          (< (nfix node) (num-fanins aignet)))
     (aignet-copy-is-comb-equivalent (+ 1 node1)
                                     aignet new-copy new-aignet2))))

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

(defthm w-state-of-fraig-sweep-node
  (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-node 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-node

(defthm lit-copy-0-of-fraig-sweep-node
  (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-node 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-node-of-nfix-node

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

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

(defthm fraig-sweep-node-nat-equiv-congruence-on-node
 (implies
   (nat-equiv node node-equiv)
   (equal (fraig-sweep-node node
                            aignet aignet2 copy strash fraig-ctrexes
                            classes mark aignet-refcounts sat-lits
                            ipasir fraig-stats config state)
          (fraig-sweep-node 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-node-of-fraig-config-fix-config

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

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

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