		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-initial-sim

Signature
(fraig-initial-sim count s32v classes aignet state) → (mv new-classes new-s32v new-state)
Arguments: count — Guard (natp count).

Definitions and Theorems

Function: fraig-initial-sim

(defun fraig-initial-sim (count s32v classes aignet state)
  (declare (xargs :stobjs (s32v classes aignet state)))
  (declare (xargs :guard (natp count)))
  (declare (xargs :guard (and (classes-wellformed classes)
                              (<= (classes-size classes)
                                  (num-fanins aignet))
                              (<= (num-fanins aignet)
                                  (classes-size classes))
                              (equal (classes-size classes)
                                     (s32v-nrows s32v)))))
  (let ((__function__ 'fraig-initial-sim))
    (declare (ignorable __function__))
    (b* (((when (zp count))
          (mv classes s32v state))
         ((mv s32v state)
          (s32v-randomize-inputs 0 s32v aignet state))
         ((mv s32v state)
          (s32v-randomize-regs 0 s32v aignet state))
         (s32v (aignet-vecsim-top s32v aignet))
         ((mv classes & & &)
          (classes-refine s32v classes aignet)))
      (fraig-initial-sim (1- count)
                         s32v classes aignet state))))

Theorem: classes-wellformed-of-fraig-initial-sim

(defthm classes-wellformed-of-fraig-initial-sim
  (b* (((mv ?new-classes ?new-s32v ?new-state)
        (fraig-initial-sim count s32v classes aignet state)))
    (implies (classes-wellformed classes)
             (classes-wellformed new-classes))))

Theorem: classes-size-of-fraig-initial-sim

(defthm classes-size-of-fraig-initial-sim
  (b* (((mv ?new-classes ?new-s32v ?new-state)
        (fraig-initial-sim count s32v classes aignet state)))
    (equal (classes-size new-classes)
           (classes-size classes))))

Theorem: w-state-of-fraig-initial-sim

(defthm w-state-of-fraig-initial-sim
  (b* (((mv ?new-classes ?new-s32v ?new-state)
        (fraig-initial-sim count s32v classes aignet state)))
    (equal (w new-state) (w state))))

Theorem: fraig-initial-sim-of-nfix-count

(defthm fraig-initial-sim-of-nfix-count
  (equal (fraig-initial-sim (nfix count)
                            s32v classes aignet state)
         (fraig-initial-sim count s32v classes aignet state)))

Theorem: fraig-initial-sim-nat-equiv-congruence-on-count

(defthm fraig-initial-sim-nat-equiv-congruence-on-count
 (implies
  (nat-equiv count count-equiv)
  (equal (fraig-initial-sim count s32v classes aignet state)
         (fraig-initial-sim count-equiv s32v classes aignet state)))
 :rule-classes :congruence)