		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-store-ctrex

Signature
(fraig-store-ctrex lit1 lit2 class-head aignet2 sat-lits ipasir fraig-ctrexes state) → (mv new-fraig-ctrexes new-state)
Arguments: lit1 — Guard (litp lit1).; lit2 — Guard (litp lit2).; class-head — Guard (natp class-head).

Definitions and Theorems

Function: fraig-store-ctrex

(defun fraig-store-ctrex (lit1 lit2 class-head aignet2
                               sat-lits ipasir fraig-ctrexes state)
 (declare
      (xargs :stobjs (aignet2 sat-lits ipasir fraig-ctrexes state)))
 (declare (xargs :guard (and (litp lit1)
                             (litp lit2)
                             (natp class-head))))
 (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))
                            (fraig-ctrex-in/reg-rows fraig-ctrexes))
                     (fraig-ctrexes-ok fraig-ctrexes)
                     (< (nfix (fraig-ctrex-nbits fraig-ctrexes))
                        (* 32 (fraig-ctrex-ncols fraig-ctrexes)))
                     (< class-head
                        (fraig-ctrex-data-rows fraig-ctrexes)))))
 (let ((__function__ 'fraig-store-ctrex))
   (declare (ignorable __function__))
   (b* ((count (fraig-ctrex-nbits fraig-ctrexes))
        ((acl2::stobj-get new-count packed-vals
                          packed-relevants bitarr state)
         ((packed-vals (fraig-ctrex-in/reg-vals fraig-ctrexes))
          (packed-relevants
               (fraig-ctrex-in/reg-relevants fraig-ctrexes))
          (bitarr (fraig-ctrex-resim-classes fraig-ctrexes)))
         (b* (((mv new-count
                   packed-vals packed-relevants state)
               (fraig-store-ctrex-aux
                    lit1 lit2 aignet2 sat-lits ipasir count
                    packed-vals packed-relevants state))
              (bitarr (set-bit class-head 1 bitarr)))
           (mv new-count packed-vals
               packed-relevants bitarr state)))
        (fraig-ctrexes
             (update-fraig-ctrex-nbits new-count fraig-ctrexes))
        (fraig-ctrexes (update-fraig-ctrex-count
                            (+ 1 (fraig-ctrex-count fraig-ctrexes))
                            fraig-ctrexes)))
     (mv fraig-ctrexes state))))

Theorem: fraig-ctrexes-ok-of-fraig-store-ctrex

(defthm fraig-ctrexes-ok-of-fraig-store-ctrex
  (b* (((mv ?new-fraig-ctrexes ?new-state)
        (fraig-store-ctrex lit1 lit2 class-head aignet2
                           sat-lits ipasir fraig-ctrexes state)))
    (implies (and (fraig-ctrexes-ok fraig-ctrexes)
                  (< (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)))
                  (< (nfix class-head)
                     (fraig-ctrex-data-rows fraig-ctrexes)))
             (fraig-ctrexes-ok new-fraig-ctrexes))))

Theorem: fraig-ctrex-data-rows-of-fraig-store-ctrex

(defthm fraig-ctrex-data-rows-of-fraig-store-ctrex
  (b* (((mv ?new-fraig-ctrexes ?new-state)
        (fraig-store-ctrex lit1 lit2 class-head aignet2
                           sat-lits ipasir fraig-ctrexes state)))
    (equal (fraig-ctrex-data-rows new-fraig-ctrexes)
           (fraig-ctrex-data-rows fraig-ctrexes))))

Theorem: fraig-ctrex-ncols-of-fraig-store-ctrex

(defthm fraig-ctrex-ncols-of-fraig-store-ctrex
  (b* (((mv ?new-fraig-ctrexes ?new-state)
        (fraig-store-ctrex lit1 lit2 class-head aignet2
                           sat-lits ipasir fraig-ctrexes state)))
    (equal (fraig-ctrex-ncols new-fraig-ctrexes)
           (fraig-ctrex-ncols fraig-ctrexes))))

Theorem: fraig-ctrex-in/reg-rows-of-fraig-store-ctrex

(defthm fraig-ctrex-in/reg-rows-of-fraig-store-ctrex
  (b* (((mv ?new-fraig-ctrexes ?new-state)
        (fraig-store-ctrex lit1 lit2 class-head aignet2
                           sat-lits ipasir fraig-ctrexes 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: w-state-of-fraig-store-ctrex

(defthm w-state-of-fraig-store-ctrex
  (b* (((mv ?new-fraig-ctrexes ?new-state)
        (fraig-store-ctrex lit1 lit2 class-head aignet2
                           sat-lits ipasir fraig-ctrexes state)))
    (equal (w new-state) (w state))))

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

(defthm fraig-store-ctrex-of-lit-fix-lit1
  (equal (fraig-store-ctrex (lit-fix lit1)
                            lit2 class-head aignet2
                            sat-lits ipasir fraig-ctrexes state)
         (fraig-store-ctrex lit1 lit2 class-head aignet2
                            sat-lits ipasir fraig-ctrexes state)))

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

(defthm fraig-store-ctrex-lit-equiv-congruence-on-lit1
 (implies
    (lit-equiv lit1 lit1-equiv)
    (equal (fraig-store-ctrex lit1 lit2 class-head aignet2
                              sat-lits ipasir fraig-ctrexes state)
           (fraig-store-ctrex lit1-equiv lit2 class-head aignet2
                              sat-lits ipasir fraig-ctrexes state)))
 :rule-classes :congruence)

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

(defthm fraig-store-ctrex-of-lit-fix-lit2
  (equal (fraig-store-ctrex lit1 (lit-fix lit2)
                            class-head aignet2
                            sat-lits ipasir fraig-ctrexes state)
         (fraig-store-ctrex lit1 lit2 class-head aignet2
                            sat-lits ipasir fraig-ctrexes state)))

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

(defthm fraig-store-ctrex-lit-equiv-congruence-on-lit2
 (implies
    (lit-equiv lit2 lit2-equiv)
    (equal (fraig-store-ctrex lit1 lit2 class-head aignet2
                              sat-lits ipasir fraig-ctrexes state)
           (fraig-store-ctrex lit1 lit2-equiv class-head aignet2
                              sat-lits ipasir fraig-ctrexes state)))
 :rule-classes :congruence)

Theorem: fraig-store-ctrex-of-nfix-class-head

(defthm fraig-store-ctrex-of-nfix-class-head
  (equal (fraig-store-ctrex lit1 lit2 (nfix class-head)
                            aignet2
                            sat-lits ipasir fraig-ctrexes state)
         (fraig-store-ctrex lit1 lit2 class-head aignet2
                            sat-lits ipasir fraig-ctrexes state)))

Theorem: fraig-store-ctrex-nat-equiv-congruence-on-class-head

(defthm fraig-store-ctrex-nat-equiv-congruence-on-class-head
 (implies
    (nat-equiv class-head class-head-equiv)
    (equal (fraig-store-ctrex lit1 lit2 class-head aignet2
                              sat-lits ipasir fraig-ctrexes state)
           (fraig-store-ctrex lit1 lit2 class-head-equiv aignet2
                              sat-lits ipasir fraig-ctrexes state)))
 :rule-classes :congruence)