		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation-tailrec-elimination

Atj-parallel-asg-depgraph

Calculate a dependency graph for a parallel assignment.

Signature
(atj-parallel-asg-depgraph vars exprs) → graph
Arguments: vars — Guard (string-listp vars).; exprs — Guard (jexpr-listp exprs).
Returns: graph — Type (alistp graph).

Since Java does not have parallel assignment, in order to assign the expressions exprs to the variables vars, we attempt to topologically order these assignments according to their dependencies. This function calculates the dependency graph, in a form suitable for this dependency graph library.

We go through the variables in order, and for each we construct an association pair for the graph represented as an alist. For each variable, we collect all the variables in the corresponding expression, but we exclude the variable itself and any variable not in the initial set. Thus, we use an auxiliary function that has the unchanging initial set as an additional argument.

Definitions and Theorems

Function: atj-parallel-asg-depgraph-aux

(defun atj-parallel-asg-depgraph-aux (vars exprs all-vars)
  (declare (xargs :guard (and (string-listp vars)
                              (jexpr-listp exprs)
                              (string-listp all-vars))))
  (declare (xargs :guard (= (len vars) (len exprs))))
  (let ((__function__ 'atj-parallel-asg-depgraph-aux))
    (declare (ignorable __function__))
    (b* (((when (endp vars)) nil)
         (var (car vars))
         (expr (car exprs))
         (deps (remove-equal var
                             (intersection-equal (jexpr-vars expr)
                                                 all-vars)))
         (rest-alist (atj-parallel-asg-depgraph-aux (cdr vars)
                                                    (cdr exprs)
                                                    all-vars)))
      (acons var deps rest-alist))))

Theorem: alistp-of-atj-parallel-asg-depgraph-aux

(defthm alistp-of-atj-parallel-asg-depgraph-aux
  (b* ((graph (atj-parallel-asg-depgraph-aux vars exprs all-vars)))
    (alistp graph))
  :rule-classes :rewrite)

Theorem: atj-parallel-asg-depgraph-aux-subsetp-vars

(defthm atj-parallel-asg-depgraph-aux-subsetp-vars
  (b* ((?graph (atj-parallel-asg-depgraph-aux vars exprs all-vars)))
    (subsetp-equal (alist-keys graph)
                   vars)))

Function: atj-parallel-asg-depgraph

(defun atj-parallel-asg-depgraph (vars exprs)
  (declare (xargs :guard (and (string-listp vars)
                              (jexpr-listp exprs))))
  (declare (xargs :guard (= (len vars) (len exprs))))
  (let ((__function__ 'atj-parallel-asg-depgraph))
    (declare (ignorable __function__))
    (atj-parallel-asg-depgraph-aux vars exprs vars)))

Theorem: alistp-of-atj-parallel-asg-depgraph

(defthm alistp-of-atj-parallel-asg-depgraph
  (b* ((graph (atj-parallel-asg-depgraph vars exprs)))
    (alistp graph))
  :rule-classes :rewrite)

Theorem: atj-parallel-asg-depgraph-subsetp-vars

(defthm atj-parallel-asg-depgraph-subsetp-vars
  (b* ((?graph (atj-parallel-asg-depgraph vars exprs)))
    (subsetp-equal (alist-keys graph)
                   vars)))