other
(in-package "AIGNET")
other
(include-book "litp")
other
(include-book "centaur/misc/arrays" :dir :system)
other
(include-book "std/stobjs/bitarr" :dir :system)
other
(include-book "misc/definline" :dir :system)
other
(include-book "std/lists/equiv" :dir :system)
other
(include-book "std/stobjs/clone" :dir :system)
other
(local (include-book "data-structures/list-defthms" :dir :system))
other
(local (include-book "arithmetic/top-with-meta" :dir :system))
other
(deflist bit-list :pred bit-listp :elt-type bit :true-listp t)
other
(defthm bitarr$ap-is-bit-listp (equal (bitarr$ap x) (bit-listp x)))
other
(defsection nth-lit
(defund nth-lit
(n x)
(lit-fix (nth n x)))
(local (in-theory (enable nth-lit)))
(defcong nat-equiv
equal
(nth-lit n x)
1)
(defthm litp-of-nth-lit
(litp (nth-lit n x)))
(defthm nth-lit-of-resize-list
(implies (<= (len lst) (nfix m))
(equal (nth-lit n
(resize-list lst m 0))
(nth-lit n lst)))
:hints (("Goal" :in-theory (enable nth-with-large-index
nth-of-resize-list-split))))
(defund update-nth-lit
(n v x)
(update-nth n
(lit-fix v)
x))
(local (in-theory (enable update-nth-lit)))
(defcong nat-equiv
equal
(update-nth-lit n v x)
1)
(defcong lit-equiv
equal
(update-nth-lit n v x)
2)
(defthm nth-lit-of-update-nth-lit-same
(equal (nth-lit n
(update-nth-lit n v x))
(lit-fix v)))
(defthm nth-lit-of-update-nth-lit-diff
(implies (not (equal (nfix n) (nfix m)))
(equal (nth-lit m
(update-nth-lit n v x))
(nth-lit m x))))
(defthm nth-lit-of-update-nth-lit-split
(equal (nth-lit m
(update-nth-lit n v x))
(if (equal (nfix n) (nfix m))
(lit-fix v)
(nth-lit m x))))
(defthm len-update-nth-lit-not-smaller
(<= (len x)
(len (update-nth-lit n v x)))
:rule-classes (:rewrite :linear))
(defthm len-update-nth-lit-at-least-n+1
(<= (+ 1 (nfix n))
(len (update-nth-lit n v x)))
:rule-classes ((:linear :trigger-terms ((len (update-nth-lit n v x))))))
(defthm len-of-update-nth-lit
(implies (< (nfix n) (len x))
(equal (len (update-nth-lit n val x))
(len x)))
:hints (("Goal" :in-theory (enable update-nth-lit))))
(defthm update-nth-lit-same
(equal (update-nth-lit n
v1
(update-nth-lit n v2 arr))
(update-nth-lit n v1 arr)))
(defthmd update-nth-lit-switch
(implies (not (equal (nfix n1) (nfix n2)))
(equal (update-nth-lit n2
v2
(update-nth-lit n1 v1 l))
(update-nth-lit n1
v1
(update-nth-lit n2 v2 l))))
:rule-classes ((:rewrite :loop-stopper ((n2 n1))))))
other
(defsection bitarr (local (in-theory (enable resize-list))) (definline bitarr-clear (bitarr) (declare (xargs :stobjs bitarr :guard-hints ('(:expand ((len bitarr) (len (cdr bitarr))) :in-theory (e/d (nth update-nth)))))) (mbe :logic (non-exec nil) :exec (resize-bits 0 bitarr))))
other
(defsection litarr
(def-1d-arr litarr
:slotname lit
:pred litp
:fix lit-fix$inline
:type-decl (unsigned-byte 32)
:default-val 0
:rename ((get-lit . get-lit_) (set-lit . set-lit_)))
(definline get-lit
(n litarr)
(declare (xargs :stobjs litarr
:guard (and (natp n)
(< n (lits-length litarr)))
:guard-hints ('(:in-theory (enable nth-lit)))))
(mbe :logic (non-exec (nth-lit n litarr))
:exec (get-lit_ n litarr)))
(definline set-lit
(n v litarr)
(declare (xargs :stobjs litarr
:guard (and (natp n)
(< n (lits-length litarr))
(litp v))
:guard-hints ('(:in-theory (enable update-nth-lit)))))
(mbe :logic (non-exec (update-nth-lit n
(lit-fix v)
litarr))
:exec (if (< (the (integer 0 *) v) (expt 2 32))
(set-lit_ n v litarr)
(ec-call (set-lit_ n v litarr)))))
(local (in-theory (enable resize-list)))
(definline litarr-clear
(litarr)
(declare (xargs :stobjs litarr
:guard-hints ('(:expand ((len litarr) (len (cdr litarr)))
:in-theory (enable nth update-nth)))))
(mbe :logic (non-exec nil)
:exec (resize-lits 0 litarr)))
(def-universal-equiv lits-equiv
:qvars (i)
:equiv-terms ((lit-equiv (nth i x))))
(defcong lits-equiv
lit-equiv
(nth i x)
2
:hints ('(:use ((:instance lits-equiv-necc (y x-equiv))))))
(defcong lits-equiv
lits-equiv
(update-nth i v x)
3
:hints ((and stable-under-simplificationp
`(:expand (,(CAR (LAST AIGNET::CLAUSE)))
:in-theory (enable lits-equiv-necc)))))
(defcong lit-equiv
lits-equiv
(update-nth i v x)
2
:hints ((and stable-under-simplificationp
`(:expand (,(CAR (LAST AIGNET::CLAUSE)))
:in-theory (enable lits-equiv-necc)))))
(local (in-theory (enable nth-lit update-nth-lit)))
(defcong lits-equiv
lit-equiv
(nth-lit i x)
2)
(defcong lits-equiv
lits-equiv
(update-nth-lit i v x)
3)
(defcong lit-equiv
lits-equiv
(update-nth-lit i v x)
2))
other
(defsection u32arr
(def-1d-arr u32arr
:slotname u32
:pred natp
:fix nfix
:type-decl (unsigned-byte 32)
:default-val 0
:rename ((set-u32 . set-u32_) (u32s-length . u32-length)
(resize-u32s . resize-u32)))
(defun set-u32-ec-call
(n v u32arr)
(declare (xargs :stobjs u32arr :guard t))
(ec-call (set-u32_ n v u32arr)))
(definline set-u32
(n v u32arr)
(declare (xargs :stobjs u32arr
:guard (and (natp n)
(< n (u32-length u32arr))
(natp v))))
(mbe :logic (set-u32_ n
(nfix v)
u32arr)
:exec (if (< (the (integer 0 *) v) (expt 2 32))
(set-u32_ n v u32arr)
(set-u32-ec-call n v u32arr)))))
other
(defstobj-clone mark bitarr :suffix "-MARK")
other
(defstobj-clone mark2 bitarr :suffix "-MARK2")
other
(defstobj-clone copy litarr :prefix "COPY-")
other
(defstobj-clone copy2 litarr :prefix "COPY2-")
other
(defstobj-clone vals bitarr :prefix "VALS-")
other
(defstobj-clone vals2 bitarr :prefix "VALS2-")