Filtering...

select

books/acl2s/cgen/select
other
(in-package "CGEN")
other
(include-book "basis")
other
(include-book "simple-graph-array")
other
(include-book "cgen-state")
other
(include-book "type")
other
(defttag t)
other
(set-register-invariant-risk nil)
other
(defttag nil)
other
(def separate-const/simple-hyps.
  (ts wrld hc. hs. ho.)
  (decl :sig ((pseudo-term-list plist-world
       pseudo-term-list
       pseudo-term-list
       pseudo-term-list) ->
      (mv pseudo-term-list
        pseudo-term-list
        pseudo-term-list))
    :doc "given a list of hyps, separate constant hyps, simple defdata-type hyps and others")
  (f* ((add-others-and-recurse... nil
       (separate-const/simple-hyps. rst
         wrld
         hc.
         hs.
         (cons hyp ho.))) (add-constant-and-recurse (h)
        (separate-const/simple-hyps. rst
          wrld
          (cons h hc.)
          hs.
          ho.)))
    (if (endp ts)
      (mv hc. hs. ho.)
      (b* (((cons hyp rst) ts))
        (case-match hyp
          ((p t1) (declare (ignore p t1))
            (b* (((list p t1) (expand-lambda hyp)))
              (if (and (symbolp t1)
                  (is-type-predicate p wrld))
                (separate-const/simple-hyps. rst
                  wrld
                  hc.
                  (cons hyp hs.)
                  ho.)
                (add-others-and-recurse...))))
          ((r t1 t2) (if (equivalence-relationp r wrld)
              (cond ((and (symbolp t1) (quotep t2)) (add-constant-and-recurse (list r t1 t2)))
                ((and (quotep t1) (symbolp t2)) (add-constant-and-recurse (list r t2 t1)))
                (t (add-others-and-recurse...)))
              (add-others-and-recurse...)))
          (& (add-others-and-recurse...)))))))
other
(mutual-recursion (defun possible-constant-value-expressionp-lst
    (expr-lst)
    (declare (xargs :guard t))
    (if (atom expr-lst)
      t
      (and (possible-constant-value-expressionp (car expr-lst))
        (possible-constant-value-expressionp-lst (cdr expr-lst)))))
  (defun possible-constant-value-expressionp
    (expr)
    (declare (xargs :guard t))
    (cond ((null expr) t)
      ((possible-constant-value-p expr) t)
      ((atom expr) (possible-constant-value-p expr))
      ((not (symbolp (car expr))) nil)
      (t (possible-constant-value-expressionp-lst (cdr expr))))))
constant-hyp?function
(defun constant-hyp?
  (hyp)
  (declare (xargs :guard t))
  (and (equiv-term? hyp)
    (or (and (proper-symbolp (second hyp))
        (possible-constant-value-expressionp (third hyp)))
      (and (proper-symbolp (third hyp))
        (possible-constant-value-expressionp (second hyp))))))
mget-term-varfunction
(defun mget-term-var
  (term recordp)
  (declare (xargs :guard t))
  (and (true-listp term)
    (= (len term) 3)
    (member-equal (car term) '(mget g g))
    (quotep (cadr term))
    (true-listp (cadr term))
    (implies recordp
      (keywordp (unquote (cadr term))))
    (proper-symbolp (third term))
    (third term)))
mget-hyp-varfunction
(defun mget-hyp-var
  (hyp recordp)
  (declare (xargs :guard t))
  (or (mget-term-var hyp recordp)
    (and (equiv-term? hyp)
      (or (mget-term-var (second hyp) recordp)
        (mget-term-var (third hyp) recordp)))))
destruct-simple-hypfunction
(defun destruct-simple-hyp
  (chyp)
  (declare (xargs :guard (>= (len chyp) 3)))
  (if (proper-symbolp (second chyp))
    (mv (second chyp) (third chyp))
    (mv (third chyp) (second chyp))))
simple-var-hyp?function
(defun simple-var-hyp?
  (hyp var-quotient-alst list-dest-fns)
  (and (not (constant-hyp? hyp))
    (not (equiv-hyp? hyp))
    (= 3 (len hyp))
    (member-eq (car hyp) '(equal = eq eql))
    (or (proper-symbolp (second hyp))
      (proper-symbolp (third hyp)))
    (mv-let (var expr)
      (destruct-simple-hyp hyp)
      (and (let* ((vquotient (get-val var var-quotient-alst)) (dvars (get-free-vars1 expr nil))
            (dquotients (get-val-lst dvars var-quotient-alst)))
          (not (member-equal vquotient dquotients)))
        (not (member-eq (car expr) list-dest-fns))))))
directed-2-rel?function
(defun directed-2-rel?
  (hyp)
  (and (= (len hyp) 3)
    (b* (((mv t2 t3) (if (proper-symbolp (second hyp))
           (mv (second hyp) (third hyp))
           (mv (third hyp) (second hyp)))))
      (and (proper-symbolp t2)
        (consp t3)
        (not (member-eq (car t3)
            '(mget g g nth car cdr)))))))
undirected-2-rel?function
(defun undirected-2-rel?
  (hyp)
  (and (= (len hyp) 3)
    (let* ((t2 (second hyp)) (t3 (third hyp)))
      (and (proper-symbolp t2)
        (proper-symbolp t3)
        (member-eq (first hyp)
          '(subset-equal subset-eq
            subset-eql
            <
            <=
            >
            >=))))))
put-interdependency-edges-in-alstfunction
(defun put-interdependency-edges-in-alst
  (term-lst all-terms alst)
  (if (endp term-lst)
    alst
    (let* ((term (car term-lst)) (vars (get-free-vars1 term nil))
        (rest-terms (remove-equal term all-terms))
        (rest-vars (get-free-vars1-lst rest-terms nil)))
      (put-interdependency-edges-in-alst (cdr term-lst)
        all-terms
        (union-entries-in-adj-list vars
          (set-difference-eq rest-vars vars)
          alst)))))
build-vdependency-graphfunction
(defun build-vdependency-graph
  (hyp-lst alst alst-c incoming)
  (declare (ignorable incoming))
  (declare (xargs :verify-guards nil
      :guard (and (pseudo-term-listp hyp-lst)
        (symbol-alistp alst)
        (symbol-alistp alst-c)
        (symbol-alistp incoming))))
  "return the dependency graph in alst, when all hypotheses have been 
processed, the annotation of edges is also returned"
  (if (endp hyp-lst)
    (append alst alst-c)
    (let ((hyp (car hyp-lst)))
      (cond ((constant-hyp? hyp) (b* (((mv var &) (destruct-simple-hyp hyp)))
            (build-vdependency-graph (cdr hyp-lst)
              (remove-entry var alst)
              (put-assoc-equal var nil alst-c)
              incoming)))
        ((or (atom hyp)
           (quotep hyp)
           (and (equal (len hyp) 2)
             (equal (len (get-free-vars1 (cadr hyp) nil))
               1))) (build-vdependency-graph (cdr hyp-lst)
            alst
            alst-c
            incoming))
        ((undirected-2-rel? hyp) (build-vdependency-graph (cdr hyp-lst)
            alst
            alst-c
            incoming))
        ((directed-2-rel? hyp) (b* (((mv var term) (destruct-simple-hyp hyp)) (fvars (remove-equal var
                  (get-free-vars1 term nil))))
            (build-vdependency-graph (cdr hyp-lst)
              (union-entry-in-adj-list var
                fvars
                alst)
              alst-c
              incoming)))
        ((and (equal (len hyp) 3)
           (member-eq (car hyp)
             '(member-eq member
               member-eql
               member-equal
               in
               in))
           (proper-symbolp (second hyp))) (b* ((var (second hyp)) (term (third hyp))
              (fvars (remove-equal var
                  (get-free-vars1 term nil))))
            (build-vdependency-graph (cdr hyp-lst)
              (union-entry-in-adj-list var
                fvars
                alst)
              alst-c
              incoming)))
        (t (build-vdependency-graph (cdr hyp-lst)
            alst
            alst-c
            incoming))))))
build-variable-dependency-graphfunction
(defun build-variable-dependency-graph
  (hyps vars)
  (build-vdependency-graph hyps
    (make-empty-adj-list vars)
    nil
    nil))
other
(def vars-in-dependency-order
  (hyps concl vl wrld)
  (decl :sig ((pseudo-term-list pseudo-term
       fixnum
       plist-world) ->
      symbol-list)
    :doc "return the free variables ordered according to the notion of
  dependency that treats equality relation specially. See FMCAD paper for
  details, but I have not completely implemented the improvements in the
  paper. This is where I can use better heuristics. But with no hard examples
  to work on, I am doing a naive job for now.")
  (b* ((cterms (cons (cgen-dumb-negate-lit concl) hyps)) (vars (all-vars-lst cterms))
      ((mv hc hs ho) (separate-const/simple-hyps. cterms
          wrld
          'nil
          'nil
          'nil))
      (dgraph (build-variable-dependency-graph ho vars))
      (ord-vs (reverse (approximate-topological-sort dgraph
            (system-debug-flag vl))))
      (cvars (all-vars-lst hc))
      (svars (all-vars-lst hs))
      (ord-vs (union-eq svars ord-vs))
      (ord-vs (union-eq cvars
          (set-difference-eq ord-vs cvars)))
      (ord-vs (set-difference-eq ord-vs '(t nil))))
    ord-vs))
other
(program)
other
(mutual-recursion (defun can-reach1
    (v g seen ans)
    (if (member-equal v seen)
      ans
      (b* ((xs (cdr (assoc-equal v g))) (seen (cons v seen)))
        (can-reach1-lst xs
          g
          seen
          (union-equal xs ans)))))
  (defun can-reach1-lst
    (vs g seen ans)
    (if (endp vs)
      ans
      (b* ((ans1 (can-reach1 (car vs)
             g
             seen
             ans)))
        (can-reach1-lst (cdr vs)
          g
          seen
          (union-equal ans1 ans))))))
can-reachfunction
(defun can-reach
  (v g)
  (can-reach1 v g 'nil 'nil))
pick-sink-with-max-faninfunction
(defun pick-sink-with-max-fanin
  (sinks g ans)
  (if (endp sinks)
    ans
    (if (> (len (can-reach (car sinks) g))
        (len (can-reach ans g)))
      (pick-sink-with-max-fanin (cdr sinks)
        g
        (car sinks))
      (pick-sink-with-max-fanin (cdr sinks)
        g
        ans))))
add-edgefunction
(defun add-edge
  (u v g)
  (put-assoc-equal u
    (add-to-set-equal v
      (cdr (assoc-equal u g)))
    g))
add-edges1function
(defun add-edges1
  (us v g)
  (if (endp us)
    g
    (add-edges1 (cdr us)
      v
      (add-edge (car us) v g))))
transform-to-incoming-edge-alst1function
(defun transform-to-incoming-edge-alst1
  (g g-in)
  (if (endp g)
    g-in
    (b* (((cons u v-lst) (car g)) (g-in (add-edges1 v-lst u g-in)))
      (transform-to-incoming-edge-alst1 (cdr g)
        g-in))))
transform-to-incoming-edge-alstfunction
(defun transform-to-incoming-edge-alst
  (g)
  (transform-to-incoming-edge-alst1 g
    (pairlis$ (strip-cars g) nil)))
dumb-get-all-sinksfunction
(defun dumb-get-all-sinks
  (g)
  (if (endp g)
    'nil
    (if (null (cdr (car g)))
      (cons (caar g)
        (dumb-get-all-sinks (cdr g)))
      (dumb-get-all-sinks (cdr g)))))
other
(mutual-recursion (defun var-depth-in-term
    (x t2)
    (if (equal x t2)
      0
      (if (or (atom t2) (quotep t2))
        -1
        (let ((d (max-var-depth-in-terms x (cdr t2) -1)))
          (if (natp d)
            (1+ d)
            d)))))
  (defun max-var-depth-in-terms
    (x terms ans)
    (if (endp terms)
      ans
      (b* ((d1 (var-depth-in-term x (car terms))))
        (max-var-depth-in-terms x
          (cdr terms)
          (max d1 ans))))))
pick-sink-with-max-depthfunction
(defun pick-sink-with-max-depth
  (sinks terms ans)
  (if (endp sinks)
    ans
    (if (> (max-var-depth-in-terms (car sinks)
          terms
          -1)
        (max-var-depth-in-terms ans terms -1))
      (pick-sink-with-max-depth (cdr sinks)
        terms
        (car sinks))
      (pick-sink-with-max-depth (cdr sinks)
        terms
        ans))))
filter-combinator-type-sinksfunction
(defun filter-combinator-type-sinks
  (sinks vt-alist wrld)
  (if (endp sinks)
    'nil
    (b* ((sink (car sinks)) ((cons & types) (assoc-equal sink vt-alist))
        (type (car types))
        (type-metadata (get1 type
            (type-metadata-table wrld))))
      (if (or (consp (get1 :prettyified-def type-metadata))
          (member-eq (car (get1 :prettyified-def type-metadata))
            '(record)))
        (cons sink
          (filter-combinator-type-sinks (cdr sinks)
            vt-alist
            wrld))
        (filter-combinator-type-sinks (cdr sinks)
          vt-alist
          wrld)))))
pick-sink-heuristicfunction
(defun pick-sink-heuristic
  (sinks terms
    vt-alist
    wrld
    ans)
  (b* ((c-sinks (filter-combinator-type-sinks sinks
         vt-alist
         wrld)))
    (if (consp c-sinks)
      (pick-sink-with-max-depth (cdr c-sinks)
        terms
        (car c-sinks))
      (pick-sink-with-max-depth sinks
        terms
        ans))))
pick-constant-hyp-varfunction
(defun pick-constant-hyp-var
  (terms)
  (if (endp terms)
    nil
    (if (constant-hyp? (car terms))
      (b* (((mv var &) (destruct-simple-hyp (car terms))))
        var)
      (pick-constant-hyp-var (cdr terms)))))
other
(defloop filter-terms-with-arity->
  (terms n)
  (for ((term in terms))
    (append (and (> (len term) (1+ n))
        (list term)))))
other
(def select
  (terms vl wrld)
  (decl :sig ((pseudo-term-list fixnum plist-world) ->
      symbol)
    :mode :program :doc "choose the variable with least dependency. Build a dependency
  graph, topologically sort it and return the first sink we find.")
  (b* ((vars (all-vars-lst terms)) (cvar (pick-constant-hyp-var terms))
      ((when (proper-symbolp cvar)) cvar)
      (g (build-variable-dependency-graph terms
          vars))
      (var1 (car (last (approximate-topological-sort g
              (debug-flag vl)))))
      (sinks (dumb-get-all-sinks g))
      (terms/binary-or-more (filter-terms-with-arity-> terms 1))
      (dumb-type-alist (dumb-type-alist-infer terms
          vars
          vl
          wrld))
      (var (pick-sink-heuristic sinks
          terms/binary-or-more
          dumb-type-alist
          wrld
          var1))
      (- (cw? (verbose-stats-flag vl)
          "~| Cgen/Incremental-search: Select var: ~x0~%"
          var)))
    var))