		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-store-ctrex-aux

Signature
(fraig-store-ctrex-aux lit1 lit2 aignet2 sat-lits ipasir ctrex-count packed-vals packed-relevants state) → (mv new-ctrex-count new-packed-vals new-packed-relevants new-state)
Arguments: lit1 — Guard (litp lit1).; lit2 — Guard (litp lit2).; ctrex-count — Guard (natp ctrex-count).
Returns: new-ctrex-count — Type (natp new-ctrex-count).

Definitions and Theorems

Function: fraig-store-ctrex-aux

(defun fraig-store-ctrex-aux
       (lit1 lit2 aignet2 sat-lits ipasir ctrex-count
             packed-vals packed-relevants state)
 (declare
      (xargs :stobjs (aignet2 sat-lits ipasir
                              packed-vals packed-relevants state)))
 (declare (xargs :guard (and (litp lit1)
                             (litp lit2)
                             (natp ctrex-count))))
 (declare
  (xargs :guard (and (fanin-litp lit1 aignet2)
                     (fanin-litp lit2 aignet2)
                     (non-exec (eq (ipasir$a->status ipasir) :sat))
                     (sat-lits-wfp sat-lits aignet2)
                     (equal (+ (num-ins aignet2) (num-regs aignet2))
                            (s32v-nrows packed-relevants))
                     (equal (s32v-nrows packed-relevants)
                            (s32v-nrows packed-vals))
                     (< ctrex-count
                        (* 32 (s32v-ncols packed-relevants)))
                     (equal (s32v-ncols packed-relevants)
                            (s32v-ncols packed-vals)))))
 (let ((__function__ 'fraig-store-ctrex-aux))
  (declare (ignorable __function__))
  (b*
   (((local-stobjs mark ctrex-eval ctrex-relevant
                   in/reg-vals in/reg-relevants)
     (mv mark
         ctrex-eval ctrex-relevant in/reg-vals
         in/reg-relevants new-ctrex-count
         packed-vals packed-relevants state))
    (ctrex-eval (resize-bits (num-fanins aignet2)
                             ctrex-eval))
    (ctrex-relevant (resize-bits (num-fanins aignet2)
                                 ctrex-relevant))
    (mark (resize-bits (num-fanins aignet2) mark))
    ((mv mark ctrex-eval)
     (fraig-record-sat-ctrex-rec
          (lit-id lit1)
          mark
          aignet2 sat-lits ipasir ctrex-eval))
    ((mv mark ctrex-eval)
     (fraig-record-sat-ctrex-rec
          (lit-id lit2)
          mark
          aignet2 sat-lits ipasir ctrex-eval))
    ((mv ctrex-relevant state)
     (fraig-minimize-sat-ctrex-rec (lit-id lit1)
                                   ctrex-relevant
                                   aignet2 ctrex-eval state))
    ((mv ctrex-relevant state)
     (fraig-minimize-sat-ctrex-rec (lit-id lit2)
                                   ctrex-relevant
                                   aignet2 ctrex-eval state))
    (in/reg-vals
         (resize-bits (+ (num-ins aignet2) (num-regs aignet2))
                      in/reg-vals))
    (in/reg-relevants
         (resize-bits (+ (num-ins aignet2) (num-regs aignet2))
                      in/reg-relevants))
    (in/reg-vals
         (aignet-vals->in/regvals ctrex-eval in/reg-vals aignet2))
    (in/reg-relevants
         (aignet-vals->in/regvals ctrex-relevant
                                  in/reg-relevants aignet2))
    (agreeable-bitcol (fraig-ctrex-find-agreeable
                           ctrex-count in/reg-vals in/reg-relevants
                           packed-vals packed-relevants))
    ((mv bitcol ctrex-count)
     (if agreeable-bitcol (mv agreeable-bitcol (lnfix ctrex-count))
       (mv ctrex-count (+ 1 (lnfix ctrex-count)))))
    (packed-vals
       (bitarr-copy-cares-to-s32v-col 0 bitcol in/reg-vals
                                      in/reg-relevants packed-vals))
    (packed-relevants (bitarr-or-cares-with-s32v-col
                           0 bitcol
                           in/reg-relevants packed-relevants)))
   (mv mark ctrex-eval ctrex-relevant
       in/reg-vals in/reg-relevants ctrex-count
       packed-vals packed-relevants state))))

Theorem: natp-of-fraig-store-ctrex-aux.new-ctrex-count

(defthm natp-of-fraig-store-ctrex-aux.new-ctrex-count
  (b*
   (((mv ?new-ctrex-count ?new-packed-vals
         ?new-packed-relevants ?new-state)
     (fraig-store-ctrex-aux lit1
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)))
   (natp new-ctrex-count))
  :rule-classes :type-prescription)

Theorem: packed-vals-nrows-of-fraig-store-ctrex-aux

(defthm packed-vals-nrows-of-fraig-store-ctrex-aux
  (b*
   (((mv ?new-ctrex-count ?new-packed-vals
         ?new-packed-relevants ?new-state)
     (fraig-store-ctrex-aux lit1
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)))
   (implies (equal (s32v-nrows packed-vals)
                   (+ (num-ins aignet2)
                      (num-regs aignet2)))
            (equal (len (stobjs::2darr->rows new-packed-vals))
                   (+ (num-ins aignet2)
                      (num-regs aignet2))))))

Theorem: packed-relevants-nrows-of-fraig-store-ctrex-aux

(defthm packed-relevants-nrows-of-fraig-store-ctrex-aux
  (b*
   (((mv ?new-ctrex-count ?new-packed-vals
         ?new-packed-relevants ?new-state)
     (fraig-store-ctrex-aux lit1
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)))
   (implies (equal (s32v-nrows packed-relevants)
                   (+ (num-ins aignet2)
                      (num-regs aignet2)))
            (equal (len (stobjs::2darr->rows new-packed-relevants))
                   (+ (num-ins aignet2)
                      (num-regs aignet2))))))

Theorem: packed-vals-ncols-of-fraig-store-ctrex-aux

(defthm packed-vals-ncols-of-fraig-store-ctrex-aux
  (b*
   (((mv ?new-ctrex-count ?new-packed-vals
         ?new-packed-relevants ?new-state)
     (fraig-store-ctrex-aux lit1
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)))
   (equal (stobjs::2darr->ncols new-packed-vals)
          (stobjs::2darr->ncols packed-vals))))

Theorem: packed-relevants-ncols-of-fraig-store-ctrex-aux

(defthm packed-relevants-ncols-of-fraig-store-ctrex-aux
  (b*
   (((mv ?new-ctrex-count ?new-packed-vals
         ?new-packed-relevants ?new-state)
     (fraig-store-ctrex-aux lit1
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)))
   (equal (stobjs::2darr->ncols new-packed-relevants)
          (stobjs::2darr->ncols packed-relevants))))

Theorem: ctrex-count-bound-of-fraig-store-ctrex-aux

(defthm ctrex-count-bound-of-fraig-store-ctrex-aux
  (b*
   (((mv ?new-ctrex-count ?new-packed-vals
         ?new-packed-relevants ?new-state)
     (fraig-store-ctrex-aux lit1
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)))
   (implies (< (nfix ctrex-count)
               (* 32 (s32v-ncols packed-relevants)))
            (<= new-ctrex-count
                (* 32 (s32v-ncols packed-relevants)))))
  :rule-classes :linear)

Theorem: w-state-of-fraig-store-ctrex-aux

(defthm w-state-of-fraig-store-ctrex-aux
  (b*
   (((mv ?new-ctrex-count ?new-packed-vals
         ?new-packed-relevants ?new-state)
     (fraig-store-ctrex-aux lit1
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)))
   (equal (w new-state) (w state))))

Theorem: fraig-store-ctrex-aux-of-lit-fix-lit1

(defthm fraig-store-ctrex-aux-of-lit-fix-lit1
 (equal
     (fraig-store-ctrex-aux (lit-fix lit1)
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)
     (fraig-store-ctrex-aux lit1
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)))

Theorem: fraig-store-ctrex-aux-lit-equiv-congruence-on-lit1

(defthm fraig-store-ctrex-aux-lit-equiv-congruence-on-lit1
 (implies
  (lit-equiv lit1 lit1-equiv)
  (equal
     (fraig-store-ctrex-aux lit1
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)
     (fraig-store-ctrex-aux lit1-equiv
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)))
 :rule-classes :congruence)

Theorem: fraig-store-ctrex-aux-of-lit-fix-lit2

(defthm fraig-store-ctrex-aux-of-lit-fix-lit2
 (equal
     (fraig-store-ctrex-aux lit1 (lit-fix lit2)
                            aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)
     (fraig-store-ctrex-aux lit1
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)))

Theorem: fraig-store-ctrex-aux-lit-equiv-congruence-on-lit2

(defthm fraig-store-ctrex-aux-lit-equiv-congruence-on-lit2
 (implies
  (lit-equiv lit2 lit2-equiv)
  (equal
     (fraig-store-ctrex-aux lit1
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)
     (fraig-store-ctrex-aux lit1 lit2-equiv
                            aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)))
 :rule-classes :congruence)

Theorem: fraig-store-ctrex-aux-of-nfix-ctrex-count

(defthm fraig-store-ctrex-aux-of-nfix-ctrex-count
 (equal
     (fraig-store-ctrex-aux lit1 lit2 aignet2
                            sat-lits ipasir (nfix ctrex-count)
                            packed-vals packed-relevants state)
     (fraig-store-ctrex-aux lit1
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)))

Theorem: fraig-store-ctrex-aux-nat-equiv-congruence-on-ctrex-count

(defthm fraig-store-ctrex-aux-nat-equiv-congruence-on-ctrex-count
 (implies
  (nat-equiv ctrex-count ctrex-count-equiv)
  (equal
     (fraig-store-ctrex-aux lit1
                            lit2 aignet2 sat-lits ipasir ctrex-count
                            packed-vals packed-relevants state)
     (fraig-store-ctrex-aux lit1 lit2 aignet2
                            sat-lits ipasir ctrex-count-equiv
                            packed-vals packed-relevants state)))
 :rule-classes :congruence)