simple-graph-array

other

(in-package "CGEN")

other

(include-book "utilities")

make-n-upto-listfunction

(defun make-n-upto-list
  (size ans)
  (declare (xargs :guard (and (natp size) (nat-listp ans))))
  (if (zp size)
    ans
    (make-n-upto-list (1- size)
      (cons (1- size) ans))))

other

(set-verify-guards-eagerness 0)

inmacro

(defmacro in
  (a x)
  `(member-equal ,CGEN::A ,CGEN::X))

vertex-indexesfunction

(defun vertex-indexes
  (vs sym-lst)
  (declare (xargs :guard (and (symbol-listp vs)
        (symbol-listp sym-lst)
        (subsetp vs sym-lst))))
  (if (endp vs)
    nil
    (cons (position (car vs) sym-lst)
      (vertex-indexes (cdr vs) sym-lst))))

other

(defstobj g$
  (adj-list-array :type (array t (0))
    :initially nil
    :resizable t)
  :renaming ((adj-list-arrayi ai) (update-adj-list-arrayi ui))
  :inline t)

other

(defrec vinfo%
  (name adj seen cc)
  nil)

make-g$-array-valuemacro

(defmacro make-g$-array-value
  (name &key adj seen cc)
  `(make vinfo%
    :name ,CGEN::NAME
    :adj ,CGEN::ADJ
    :seen ,CGEN::SEEN
    :cc ,(OR CGEN::CC 0)))

symbol-alst->g$1function

(defun symbol-alst->g$1
  (alst vs g$)
  (declare (xargs :stobjs (g$)
      :guard (and (symbol-alistp alst)
        (symbol-listp vs)
        (g$p g$))))
  (if (endp alst)
    g$
    (b* (((cons v adj-vs) (car alst)) ((list i) (vertex-indexes (list v) vs))
        (adj-is (vertex-indexes adj-vs vs))
        (g$ (ui i
            (make-g$-array-value v :adj adj-is)
            g$)))
      (symbol-alst->g$1 (cdr alst) vs g$))))

init-g$1function

(defun init-g$1
  (i vs g$)
  (declare (xargs :stobjs (g$)
      :guard (and (symbol-listp vs) (g$p g$))))
  (if (endp vs)
    g$
    (let ((g$ (ui i
           (make-g$-array-value (car vs))
           g$)))
      (init-g$1 (1+ i) (cdr vs) g$))))

init-g$function

(defun init-g$
  (vs size g$)
  ";intializes/resets a g$ to a graph with no edges"
  (declare (xargs :stobjs (g$)
      :guard (and (symbol-listp vs)
        (= (len vs) size)
        (g$p g$))))
  (let ((g$ (resize-adj-list-array size g$)))
    (init-g$1 0 vs g$)))

symbol-alist->g$function

(defun symbol-alist->g$
  (alst g$)
  "top-level call to populate g$ with adj-list information obtained
from alst. Assumption: (len alst) = number of vertices in graph and
[strip-cars alst] has distinct vertices"
  (declare (xargs :stobjs (g$)
      :guard (and (symbol-alistp alst) (g$p g$))))
  (b* ((vs (strip-cars alst)) (size (len alst))
      (g$ (init-g$ vs size g$)))
    (symbol-alst->g$1 alst vs g$)))

other

(set-well-founded-relation l<)

dfs-visit1function

(defun dfs-visit1
  (g$ v n fin flag)
  "explore the graph g$ (adj-list array) starting at v.
n is the number of vertices of g$ not seen,
initially it is just the total number of vertices.
fin is the list of finished vertices, with the
(car fin) being the last finished vertice, i.e
the vertice with the maximum post time."
  (declare (xargs :stobjs (g$)
      :guard (and (g$p g$)
        (or (natp v) (nat-listp v))
        (nat-listp fin)
        (natp n))
      :measure (list (nfix n) (acl2-count v))))
  (if (zp n)
    (mv g$ fin)
    (if (equal 'dfs-visit flag)
      (b* ((v-entry (ai v g$)) (adj-vs (access vinfo% v-entry :adj))
          (g$ (ui v
              (change vinfo% v-entry :seen t)
              g$))
          ((mv g$ fin!) (dfs-visit1 g$
              adj-vs
              (1- n)
              fin
              'dfs-visit-lst)))
        (mv g$ (cons v fin!)))
      (if (endp v)
        (mv g$ fin)
        (b* ((v-entry (ai (car v) g$)))
          (if (access vinfo% v-entry :seen)
            (dfs-visit1 g$
              (cdr v)
              n
              fin
              'dfs-visit-lst)
            (b* (((mv g$ fin!) (dfs-visit1 g$
                   (car v)
                   n
                   fin
                   'dfs-visit)))
              (dfs-visit1 g$
                (cdr v)
                n
                fin!
                'dfs-visit-lst))))))))

dfs-all-verticesfunction

(defun dfs-all-vertices
  (g$ vs n fin cnum)
  "Do DFS over all vertices in vs"
  (declare (xargs :stobjs (g$)
      :guard (and (g$p g$)
        (nat-listp vs)
        (nat-listp fin)
        (natp cnum)
        (natp n))))
  (if (endp vs)
    (mv g$ fin)
    (b* ((v-entry (ai (car vs) g$)))
      (if (access vinfo% v-entry :seen)
        (dfs-all-vertices g$
          (cdr vs)
          n
          fin
          cnum)
        (b* ((g$ (ui (car vs)
               (change vinfo% v-entry :cc cnum)
               g$)) ((mv g$ fin!) (dfs-visit1 g$
                (car vs)
                n
                fin
                'dfs-visit)))
          (dfs-all-vertices g$
            (cdr vs)
            n
            fin!
            (1+ cnum)))))))

dfs1function

(defun dfs1
  (g$ vs)
  (declare (xargs :stobjs (g$)
      :guard (and (nat-listp vs) (g$p g$))))
  (dfs-all-vertices g$
    vs
    (adj-list-array-length g$)
    nil
    0))

adjacency-list1pfunction

(defun adjacency-list1p
  (v)
  (if (null v)
    t
    (if (atom v)
      nil
      (let ((entry (car v)))
        (and (symbolp (car entry))
          (symbol-listp (cdr entry))
          (no-duplicatesp (cdr entry))
          (adjacency-list1p (cdr v)))))))

adjacency-listpfunction

(defun adjacency-listp
  (v)
  (and (adjacency-list1p v)
    (no-duplicatesp (strip-cars v))))

make-empty-adj-listfunction

(defun make-empty-adj-list
  (vars)
  (declare (xargs :guard (and (symbol-listp vars)
        (no-duplicatesp vars))))
  (if (endp vars)
    nil
    (cons (cons (car vars) nil)
      (make-empty-adj-list (cdr vars)))))

union-entry-in-adj-listfunction

(defun union-entry-in-adj-list
  (var fvars alst)
  (declare (xargs :guard (and (adjacency-listp alst)
        (true-listp fvars))))
  (if (endp alst)
    nil
    (if (eq var (caar alst))
      (cons (cons var
          (union-equal fvars (cdar alst)))
        (cdr alst))
      (cons (car alst)
        (union-entry-in-adj-list var
          fvars
          (cdr alst))))))

union-entries-in-adj-listfunction

(defun union-entries-in-adj-list
  (is fis alst)
  (declare (xargs :guard (and (adjacency-listp alst)
        (true-listp is)
        (true-listp fis))))
  (if (endp is)
    alst
    (union-entries-in-adj-list (cdr is)
      fis
      (union-entry-in-adj-list (car is)
        fis
        alst))))

transpose-alst1function

(defun transpose-alst1
  (alst ans)
  (declare (xargs :guard (and (adjacency-listp alst)
        (adjacency-listp ans))))
  (if (endp alst)
    ans
    (b* (((cons v vs) (car alst)))
      (transpose-alst1 (cdr alst)
        (union-entries-in-adj-list vs
          (list v)
          ans)))))

transpose-alstfunction

(defun transpose-alst
  (alst)
  (declare (xargs :guard (adjacency-listp alst)))
  (transpose-alst1 alst
    (make-empty-adj-list (strip-cars alst))))

scc1function

(defun scc1
  (alst g$)
  (declare (xargs :stobjs (g$)
      :guard (and (symbol-alistp alst)
        (adjacency-listp alst)
        (g$p g$))))
  (b* ((r-alst (transpose-alst alst)) (g$ (symbol-alist->g$ r-alst g$))
      (n (adj-list-array-length g$))
      ((mv g$ fin) (dfs1 g$ (make-n-upto-list n nil)))
      (g$ (symbol-alist->g$ alst g$))
      ((mv g$ fin!) (dfs1 g$ fin)))
    (mv g$ fin!)))

g$->var-quotient-alst1function

(defun g$->var-quotient-alst1
  (g$ i size ans)
  "Given graph g$, where g$[v]=(record name adj-is seenBit ccnum), we will
return, symbol alist, which maps each vertex (name), to its component
number (ccnum). This is used in simple-var-hyp? for finding cycles."
  (declare (xargs :stobjs (g$)
      :measure (nfix (- size i))
      :guard (and (natp i)
        (natp size)
        (<= i size))))
  (if (zp (- size i))
    ans
    (let ((v-entry (ai i g$)))
      (g$->var-quotient-alst1 g$
        (1+ i)
        size
        (acons (access vinfo% v-entry :name)
          (access vinfo% v-entry :cc)
          ans)))))

g$->var-quotient-alstfunction

(defun g$->var-quotient-alst
  (g$)
  (declare (xargs :stobjs (g$)))
  (g$->var-quotient-alst1 g$
    0
    (adj-list-array-length g$)
    nil))

vertex-namesfunction

(defun vertex-names
  (is g$)
  (declare (xargs :stobjs (g$)
      :guard (nat-listp is)))
  (if (endp is)
    nil
    (cons (access vinfo%
        (ai (car is) g$)
        :name)
      (vertex-names (cdr is) g$))))

g$->alst1function

(defun g$->alst1
  (g$ i size ans)
  (declare (xargs :stobjs (g$)
      :measure (nfix (- size i))
      :guard (and (natp i)
        (natp size)
        (<= i size))))
  (if (zp (- size i))
    ans
    (let ((v-entry (ai i g$)))
      (g$->alst1 g$
        (1+ i)
        size
        (acons (access vinfo% v-entry :name)
          (vertex-names (access vinfo% v-entry :adj)
            g$)
          ans)))))

g$->symbol-alistfunction

(defun g$->symbol-alist
  (g$)
  (declare (xargs :stobjs (g$)))
  (g$->alst1 g$
    0
    (adj-list-array-length g$)
    nil))

scc0function

(defun scc0
  (alst g$)
  (declare (xargs :stobjs (g$)
      :guard (symbol-alistp alst)))
  (mv-let (g$ fin)
    (scc1 alst g$)
    (mv (g$->var-quotient-alst g$)
      (vertex-names fin g$)
      (g$->symbol-alist g$)
      g$)))

union-lstsfunction

(defun union-lsts
  (lsts)
  (declare (xargs :mode :logic :guard (true-list-listp lsts)))
  (if (endp lsts)
    nil
    (union-equal (car lsts)
      (union-lsts (cdr lsts)))))

fix-adjacency-listfunction

(defun fix-adjacency-list
  (alst)
  (declare (xargs :guard (adjacency-listp alst)))
  "Fix an adjacency list to have in it keys all the vertices."
  (b* ((adj-v-lst-lst (strip-cdrs alst)) (vs (strip-cars alst))
      (adj-vs (union-lsts adj-v-lst-lst))
      (missing-vs (set-difference-eq adj-vs vs))
      (missing-alst (pairlis$ missing-vs nil)))
    (append alst missing-alst)))

strongly-connected-componentsfunction

(defun strongly-connected-components
  (alst debug-flag)
  "Strongly Connected Components of adj list graph alst.
Gives (mv map-ccnum finished-vertex-list) as result, where
map-ccnum, maps each vertex to its component number.
finished-vertex-list gives the list of vertexes in decreasing
post times."
  (declare (xargs :guard (adjacency-listp alst)))
  (b* ((alst! (fix-adjacency-list alst)) (- (cw? (and (not (equal alst alst!)) debug-flag)
          "CEgen/Note: SCC: Got Adjacency list : ~x0 Fixed to : ~x1~%"
          alst
          alst!)))
    (with-local-stobj g$
      (mv-let (var-ccnum-alst decreasing-post-times-vertex-lst
          adj-alst
          g$)
        (scc0 alst! g$)
        (mv var-ccnum-alst
          decreasing-post-times-vertex-lst
          adj-alst)))))

approximate-topological-sortfunction

(defun approximate-topological-sort
  (alst debug-flag)
  (declare (xargs :guard (adjacency-listp alst)))
  (b* (((mv & fin-vs &) (strongly-connected-components alst
         debug-flag)))
    fin-vs))