aig-vars-ext - ACL2 Book

Included Books

aig-base bstar sbitsets hons-extra alist-defs numlist ihsext-basics quotient-remainder-lemmas top-with-meta

other

(in-package "ACL2")

include-book

(include-book "aig-base")

include-book

(include-book "std/util/bstar" :dir :system)

include-book

(include-book "std/bitsets/sbitsets" :dir :system)

include-book

(include-book "centaur/misc/hons-extra" :dir :system)

include-book

(include-book "centaur/misc/alist-defs" :dir :system)

include-book

(include-book "centaur/misc/numlist" :dir :system)

local

(local (include-book "centaur/bitops/ihsext-basics" :dir :system))

local

(local (include-book "ihs/quotient-remainder-lemmas" :dir :system))

local

(local (include-book "arithmetic/top-with-meta" :dir :system))

atom<function

(defun atom<
  (x y)
  (declare (xargs :guard (and (atom x) (atom y))))
  (mbe :logic (not (alphorder (and (atom y) y) (and (atom x) x)))
    :exec (not (fast-alphorder y x))))

other

(defsort alphorder-sort
  :prefix alphorder
  :comparablep (lambda (x) (not (consp x)))
  :compare< atom<
  :comparable-listp atom-listp
  :true-listp t
  :weak t)

accumulate-aig-varsfunction

(defun accumulate-aig-vars
  (x nodetable acc)
  (declare (xargs :guard t))
  (b* (((when (aig-atom-p x)) (if (or (booleanp x) (hons-get x nodetable))
         (mv nodetable acc)
         (mv (hons-acons x t nodetable) (cons x acc)))) ((when (eq (cdr x) nil)) (accumulate-aig-vars (car x) nodetable acc))
      ((when (hons-get x nodetable)) (mv nodetable acc))
      (nodetable (hons-acons x t nodetable))
      ((mv nodetable acc) (accumulate-aig-vars (car x) nodetable acc)))
    (accumulate-aig-vars (cdr x) nodetable acc)))

accumulate-aig-vars-listfunction

(defun accumulate-aig-vars-list
  (x nodetable acc)
  (declare (xargs :guard t))
  (b* (((when (atom x)) (mv nodetable acc)) ((mv nodetable acc) (accumulate-aig-vars (car x) nodetable acc)))
    (accumulate-aig-vars-list (cdr x) nodetable acc)))

aig-vars-unorderedfunction

(defun aig-vars-unordered
  (x)
  (declare (xargs :guard t))
  (b* (((mv nodetable acc) (accumulate-aig-vars x nil nil)))
    (fast-alist-free nodetable)
    acc))

aig-vars-unordered-listfunction

(defun aig-vars-unordered-list
  (x)
  (declare (xargs :guard t))
  (b* (((mv nodetable acc) (accumulate-aig-vars-list x nil nil)))
    (fast-alist-free nodetable)
    acc))

aigtab-collect-vars1function

(defun aigtab-collect-vars1
  (queue aigtab nodetable seen)
  (declare (xargs :guard t :mode :program))
  (b* (((when (atom queue)) (fast-alist-free nodetable) seen) (seen (cons (car queue) seen))
      (aig (cdr (hons-get (car queue) aigtab)))
      ((mv nodetable queue) (accumulate-aig-vars aig nodetable (cdr queue))))
    (aigtab-collect-vars1 queue aigtab nodetable seen)))

aigtab-collect-varsfunction

(defun aigtab-collect-vars
  (queue aigtab)
  (declare (xargs :guard t :mode :program))
  (aigtab-collect-vars1 queue
    aigtab
    (make-fast-alist (pairlis$ queue nil))
    nil))

other

(defsection aig-vars-1pass
  :parents (aig-vars)
  :short "Faster, raw Lisp implementation of @(see aig-vars)."
  :long "<p>Logically this is just @(see aig-vars).</p>"
  (defun aig-vars-1pass
    (x)
    (declare (xargs :guard t))
    (aig-vars x)))

other

(defsection aig-vars-fast
  :parents (aig-vars)
  :short "Faster, raw Lisp implementation of @(see aig-vars), with
under-the-hood memoization; kind of nasty."
  (defun aig-vars-fast
    (x)
    (declare (xargs :guard t))
    (aig-vars x)))

aig-vars-dfsorder-aux2function

(defun aig-vars-dfsorder-aux2
  (x seen vars)
  (declare (xargs :guard t))
  (b* (((when (atom x)) (if (or (booleanp x) (hons-get x vars))
         (mv seen vars)
         (mv seen (hons-acons x nil vars)))) ((when (hons-get x seen)) (mv seen vars))
      (seen (hons-acons x nil seen))
      ((unless (cdr x)) (aig-vars-dfsorder-aux2 (car x) seen vars))
      ((mv seen vars) (aig-vars-dfsorder-aux2 (car x) seen vars)))
    (aig-vars-dfsorder-aux2 (cdr x) seen vars)))

aig-vars-dfsorder-aux2-listfunction

(defun aig-vars-dfsorder-aux2-list
  (x seen vars)
  (declare (xargs :guard t))
  (b* (((when (atom x)) (mv seen vars)) ((mv seen vars) (aig-vars-dfsorder-aux2 (car x) seen vars)))
    (aig-vars-dfsorder-aux2-list (cdr x) seen vars)))

sbitset-alistpfunction

(defun sbitset-alistp
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    t
    (and (consp (car x))
      (sbitsetp (cdar x))
      (sbitset-alistp (cdr x)))))

sbitsetp-of-lookup-in-sbitset-alistptheorem

(defthm sbitsetp-of-lookup-in-sbitset-alistp
  (implies (and (sbitset-alistp x) (hons-assoc-equal k x))
    (sbitsetp (cdr (hons-assoc-equal k x)))))

local

(local (defun max-nat-list
    (x)
    (declare (xargs :guard (nat-listp x)))
    (if (atom x)
      0
      (max (lnfix (car x)) (max-nat-list (cdr x))))))

aig-vars-sparse/trans-auxfunction

(defun aig-vars-sparse/trans-aux
  (x memo-table nalist)
  (declare (xargs :guard (sbitset-alistp memo-table)
      :verify-guards nil))
  (b* (((when (atom x)) (mv (if (booleanp x)
           nil
           (sbitset-singleton (nfix (cdr (hons-get x nalist)))))
         memo-table)) ((unless (cdr x)) (aig-vars-sparse/trans-aux (car x) memo-table nalist))
      (look (hons-get x memo-table))
      ((when look) (mv (cdr look) memo-table))
      ((mv car-vars memo-table) (aig-vars-sparse/trans-aux (car x) memo-table nalist))
      ((mv cdr-vars memo-table) (aig-vars-sparse/trans-aux (cdr x) memo-table nalist))
      (all-vars (sbitset-union car-vars cdr-vars))
      (memo-table (hons-acons x all-vars memo-table)))
    (mv all-vars memo-table)))

sbitsetp-of-aig-vars-sparse-trans-auxtheorem

(defthm sbitsetp-of-aig-vars-sparse-trans-aux
  (implies (sbitset-alistp memo-table)
    (and (sbitsetp (mv-nth 0 (aig-vars-sparse/trans-aux x memo-table nalist)))
      (sbitset-alistp (mv-nth 1 (aig-vars-sparse/trans-aux x memo-table nalist))))))

other

(verify-guards aig-vars-sparse/trans-aux)

map-aig-vars-sparse/transfunction

(defun map-aig-vars-sparse/trans
  (x memo-table nalist)
  (declare (xargs :guard (sbitset-alistp memo-table)))
  (b* (((when (atom x)) (fast-alist-free memo-table) nil) ((mv vars1 memo-table) (aig-vars-sparse/trans-aux (car x) memo-table nalist)))
    (cons vars1
      (map-aig-vars-sparse/trans (cdr x) memo-table nalist))))

sbitset-listpfunction

(defun sbitset-listp
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (eq x nil)
    (and (sbitsetp (car x)) (sbitset-listp (cdr x)))))

sbitset-listp-of-map-aig-vars-sparse-transtheorem

(defthm sbitset-listp-of-map-aig-vars-sparse-trans
  (implies (sbitset-alistp memo-table)
    (sbitset-listp (map-aig-vars-sparse/trans x memo-table nalist))))

maybe-add-translated-sbitmacro

(defmacro maybe-add-translated-sbit
  (bit x offset acc tbl)
  `(if (logbitp ,BIT ,X)
    (cons (aref1 'map-aig-vars-fast-array ,TBL (+ ,BIT ,OFFSET))
      ,ACC)
    ,ACC))

60bits-0-7-transfunction

(defund 60bits-0-7-trans
  (offset x acc tbl)
  (declare (xargs :guard (and (natp offset)
        (array1p 'map-aig-vars-fast-array tbl)
        (<= (+ 8 offset)
          (car (dimensions 'map-aig-vars-fast-array tbl)))))
    (type (unsigned-byte 60) x))
  (b* ((acc (maybe-add-translated-sbit 7 x offset acc tbl)) (acc (maybe-add-translated-sbit 6 x offset acc tbl))
      (acc (maybe-add-translated-sbit 5 x offset acc tbl))
      (acc (maybe-add-translated-sbit 4 x offset acc tbl))
      (acc (maybe-add-translated-sbit 3 x offset acc tbl))
      (acc (maybe-add-translated-sbit 2 x offset acc tbl))
      (acc (maybe-add-translated-sbit 1 x offset acc tbl))
      (acc (maybe-add-translated-sbit 0 x offset acc tbl)))
    acc))

60bits-0-3-transfunction

(defund 60bits-0-3-trans
  (offset x acc tbl)
  (declare (xargs :guard (and (natp offset)
        (array1p 'map-aig-vars-fast-array tbl)
        (<= (+ 4 offset)
          (car (dimensions 'map-aig-vars-fast-array tbl)))))
    (type (unsigned-byte 60) x))
  (b* ((acc (maybe-add-translated-sbit 3 x offset acc tbl)) (acc (maybe-add-translated-sbit 2 x offset acc tbl))
      (acc (maybe-add-translated-sbit 1 x offset acc tbl))
      (acc (maybe-add-translated-sbit 0 x offset acc tbl)))
    acc))

60bits-0-59-transfunction

(defund 60bits-0-59-trans
  (offset x acc tbl)
  (declare (xargs :guard (and (natp offset)
        (array1p 'map-aig-vars-fast-array tbl)
        (<= (+ 60 offset)
          (car (dimensions 'map-aig-vars-fast-array tbl)))))
    (type (unsigned-byte 60) x))
  (b* ((acc (60bits-0-3-trans (+ offset 56)
         (the (unsigned-byte 60) (ash x -56))
         acc
         tbl)) (acc (60bits-0-7-trans (+ offset 48)
          (the (unsigned-byte 60) (ash x -48))
          acc
          tbl))
      (acc (60bits-0-7-trans (+ offset 40)
          (the (unsigned-byte 60) (ash x -40))
          acc
          tbl))
      (acc (60bits-0-7-trans (+ offset 32)
          (the (unsigned-byte 60) (ash x -32))
          acc
          tbl))
      (acc (60bits-0-7-trans (+ offset 24)
          (the (unsigned-byte 60) (ash x -24))
          acc
          tbl))
      (acc (60bits-0-7-trans (+ offset 16)
          (the (unsigned-byte 60) (ash x -16))
          acc
          tbl))
      (acc (60bits-0-7-trans (+ offset 8)
          (the (unsigned-byte 60) (ash x -8))
          acc
          tbl)))
    (60bits-0-7-trans offset x acc tbl)))

sbitset-max-offsetfunction

(defun sbitset-max-offset
  (x)
  (declare (xargs :guard (sbitsetp x)))
  (if (atom x)
    0
    (max (lnfix (sbitset-pair-offset (car x)))
      (sbitset-max-offset (cdr x)))))

sbitset-members-exec-transfunction

(defun sbitset-members-exec-trans
  (x acc tbl)
  (declare (xargs :guard (and (sbitsetp x)
        (array1p 'map-aig-vars-fast-array tbl)
        (<= (+ 60 (* 60 (sbitset-max-offset x)))
          (car (dimensions 'map-aig-vars-fast-array tbl))))))
  (if (atom x)
    acc
    (let* ((pair1 (car x)) (offset1 (sbitset-pair-offset pair1))
        (block1 (sbitset-pair-block pair1)))
      (60bits-0-59-trans (* offset1 60)
        block1
        (sbitset-members-exec-trans (cdr x) acc tbl)
        tbl))))

sbitset-members-transfunction

(defun sbitset-members-trans
  (x tbl)
  (declare (xargs :guard (and (sbitsetp x)
        (array1p 'map-aig-vars-fast-array tbl)
        (<= (+ 60 (* 60 (sbitset-max-offset x)))
          (car (dimensions 'map-aig-vars-fast-array tbl))))))
  (sbitset-members-exec-trans x nil tbl))

other

(memoize 'sbitset-members-trans)

max-sbitset-max-offsetfunction

(defun max-sbitset-max-offset
  (x)
  (declare (xargs :guard (sbitset-listp x)))
  (if (atom x)
    0
    (max (sbitset-max-offset (car x))
      (max-sbitset-max-offset (cdr x)))))

map-sbitset-members-transfunction

(defun map-sbitset-members-trans
  (x tbl)
  (declare (xargs :guard (and (sbitset-listp x)
        (array1p 'map-aig-vars-fast-array tbl)
        (<= (+ 60 (* 60 (max-sbitset-max-offset x)))
          (car (dimensions 'map-aig-vars-fast-array tbl))))))
  (if (atom x)
    nil
    (cons (sbitset-members-trans (car x) tbl)
      (map-sbitset-members-trans (cdr x) tbl))))

local

(local (defthm consp-assoc-equal-when-alistp
    (implies (alistp x) (iff (consp (assoc k x)) (assoc k x)))))

local

(local (defthm consp-assoc-equal-when-key
    (implies k (iff (consp (assoc k x)) (assoc k x)))))

local

(local (defthm car-of-assoc-equal-when-key
    (implies (and key (assoc key x))
      (equal (car (assoc key x)) key))))

local

(local (defthm bounded-integer-alistp-of-compress11
    (implies (and (natp bound) (natp i))
      (bounded-integer-alistp (compress11 name x i bound default)
        bound))))

local

(local (defthm alistp-of-compress11
    (implies i (alistp (compress11 name x i bound default)))))

finish-map-aig-vars-fastfunction

(defun finish-map-aig-vars-fast
  (array-len valist ndeps)
  (declare (xargs :guard (and (posp array-len)
        (< array-len (array-maximum-length-bound))
        (bounded-integer-alistp valist array-len)
        (sbitset-listp ndeps)
        (<= (+ 60 (* 60 (max-sbitset-max-offset ndeps))) array-len))
      :guard-hints (("Goal" :in-theory (enable array-order)))))
  (b* ((varr (compress1 'map-aig-vars-fast-array
         (cons (list :header :dimensions (list array-len)
             :maximum-length (+ array-len 1)
             :default 0
             :name 'map-aig-vars-fast-array)
           valist))) (nlists (map-sbitset-members-trans ndeps varr)))
    (flush-compress 'map-aig-vars-fast-array)
    nlists))

sbitset-max-offset-of-sbitset-union-exectheorem

(defthm sbitset-max-offset-of-sbitset-union-exec
  (implies (and (sbitsetp x) (sbitsetp y))
    (equal (sbitset-max-offset (sbitset-union-exec x y))
      (max (sbitset-max-offset x) (sbitset-max-offset y))))
  :hints (("Goal" :in-theory (enable sbitset-union-exec))))

sbitset-max-offset-of-sbitset-uniontheorem

(defthm sbitset-max-offset-of-sbitset-union
  (implies (and (sbitsetp x) (sbitsetp y))
    (equal (sbitset-max-offset (sbitset-union x y))
      (max (sbitset-max-offset x) (sbitset-max-offset y))))
  :hints (("Goal" :in-theory (enable sbitset-union))))

sbitset-max-offset-of-sbitset-singletontheorem

(defthm sbitset-max-offset-of-sbitset-singleton
  (equal (sbitset-max-offset (sbitset-singleton n))
    (floor (nfix n) *sbitset-block-size*))
  :hints (("Goal" :in-theory (enable sbitset-singleton sbitset-singleton-pair))))

sbitset-max-offset-of-lookuptheorem

(defthm sbitset-max-offset-of-lookup
  (<= (sbitset-max-offset (cdr (hons-assoc-equal x memo-table)))
    (max-sbitset-max-offset (alist-vals memo-table)))
  :hints (("Goal" :in-theory (enable alist-vals)))
  :rule-classes :linear)

local

(local (progn (defthm floor-of-lookup-when-max-nat-list
      (<= (floor (nfix (cdr (hons-assoc-equal x nalist))) 60)
        (floor (max-nat-list (alist-vals nalist)) 60))
      :hints (("Goal" :in-theory (enable alist-vals))))
    (defthm sbitset-max-offset-of-aig-vars-sparse/trans-aux
      (implies (and (sbitset-alistp memo-table)
          (<= (max-sbitset-max-offset (alist-vals memo-table))
            (floor (max-nat-list (alist-vals nalist)) 60)))
        (mv-let (bitset memo-table)
          (aig-vars-sparse/trans-aux x memo-table nalist)
          (and (<= (max-sbitset-max-offset (alist-vals memo-table))
              (floor (max-nat-list (alist-vals nalist)) 60))
            (<= (sbitset-max-offset bitset)
              (floor (max-nat-list (alist-vals nalist)) 60)))))
      :hints (("Goal" :in-theory (enable alist-vals)))
      :rule-classes (:rewrite :linear))
    (defthm max-sbitset-max-offset-of-map-aig-vars-sparse/trans
      (implies (and (sbitset-alistp memo-table)
          (<= (max-sbitset-max-offset (alist-vals memo-table))
            (floor (max-nat-list (alist-vals nalist)) 60)))
        (<= (max-sbitset-max-offset (map-aig-vars-sparse/trans x memo-table nalist))
          (floor (max-nat-list (alist-vals nalist)) 60)))
      :hints (("Goal" :in-theory (disable aig-vars-sparse/trans-aux)))
      :rule-classes (:rewrite :linear))
    (defthm alist-vals-of-pairlis
      (implies (equal (len x) (len y))
        (equal (alist-vals (pairlis$ x y)) (list-fix y)))
      :hints (("Goal" :in-theory (enable list-fix alist-vals))))
    (defthm max-nat-list-of-numlist
      (implies (and (natp start) (natp by))
        (equal (max-nat-list (numlist start by n))
          (if (zp n)
            0
            (+ start (* (+ -1 n) by))))))
    (defthm max-sbitset-max-offset-of-map-aig-vars-sparse/trans-start
      (implies (atom memo-table)
        (<= (max-sbitset-max-offset (map-aig-vars-sparse/trans x memo-table nalist))
          (floor (max-nat-list (alist-vals nalist)) 60)))
      :hints (("goal" :use max-sbitset-max-offset-of-map-aig-vars-sparse/trans
         :in-theory (e/d (alist-vals)
           (max-sbitset-max-offset-of-map-aig-vars-sparse/trans))))
      :rule-classes (:rewrite :linear))
    (defthm nat-listp-of-numlist
      (implies (and (natp start) (natp by))
        (nat-listp (numlist start by n))))
    (defthm bounded-integer-alistp-of-pairlis
      (implies (and (natp bound)
          (nat-listp keys)
          (force (< (max-nat-list keys) bound)))
        (bounded-integer-alistp (pairlis$ keys vals) bound)))))

map-aig-vars-fastfunction

(defun map-aig-vars-fast
  (aigs)
  (declare (xargs :guard t
      :guard-hints ('(:cases ((< 0
            (len (alist-keys (mv-nth 1 (aig-vars-dfsorder-aux2-list aigs nil nil))))))))))
  (b* (((mv seen vars) (aig-vars-dfsorder-aux2-list aigs nil nil)) (nseen (fast-alist-len seen))
      (- (fast-alist-free seen))
      (- (fast-alist-free vars))
      (all-vars (alist-keys vars))
      (len (len all-vars))
      (numlist (numlist 0 1 len))
      (nalist (pairlis$ all-vars numlist))
      (valist (pairlis$ numlist all-vars))
      ((with-fast nalist))
      (ndeps (map-aig-vars-sparse/trans aigs nseen nalist))
      (array-len (* 60 (+ 1 (floor len 60)))))
    (mbe :logic (finish-map-aig-vars-fast array-len valist ndeps)
      :exec (if (<= (array-maximum-length-bound) array-len)
        (prog2$ (er hard?
            'map-aig-vars-fast
            "Array length out of bounds: ~x0"
            array-len)
          (non-exec (finish-map-aig-vars-fast array-len valist ndeps)))
        (finish-map-aig-vars-fast array-len valist ndeps)))))