ccg

(in-package "ACL2")

(defttag :ccg)

(progn+all-ttags-allowed (include-book "hacking/all" :dir :system :ttags :all))

(subsume-ttags-since-defttag)

(add-acl2-defaults-table-key :termination-method (member-eq val '(:measure :ccg)))

(verify-guards get-termination-method)

(rewrite-table-guard acl2-defaults-table
  (:carpat %body%
    :vars %body%
    :repl (if (eq key :ccg-hierarchy)
      (non-empty-hlevel-listp val)
      %body%)))

(set-state-ok t)

(program)

(add-acl2-defaults-table-key :ccg-time-limit (or (null val) (and (rationalp val) (< 0 val))))

(logic)

(set-state-ok nil)

(verify-guards get-ccg-time-limit)

(program)

(set-state-ok t)

(defstruct-raw funct
  (fn nil :type symbol)
  (formals nil :type list)
  (ccms nil :type sequence))

(defstruct-raw context
  (ruler nil)
  (call nil)
  (parent-funct (make-funct) :type funct)
  (call-funct (make-funct) :type funct)
  num)

(defmacro-raw context-fn
  (c)
  `(funct-fn (context-parent-funct ,C)))

(defmacro-raw context-formals
  (c)
  `(funct-formals (context-parent-funct ,C)))

(defmacro-raw context-callfn
  (c)
  `(funct-fn (context-call-funct ,C)))

(defmacro-raw context-callformals
  (c)
  `(funct-formals (context-call-funct ,C)))

(defmacro-raw context-ccms
  (c)
  `(funct-ccms (context-parent-funct ,C)))

(defstruct-raw ccmf-node
  (>-edges nil :type list)
  (>=-edges nil :type list))

(defstruct-raw ccmf
  (firstsite 0 :type fixnum)
  (lastsite 0 :type fixnum)
  (fc-num (list 0) :type (cons fixnum list))
  (lc-num (list 0) :type (cons fixnum list))
  (graph nil :type (array ccmf-node))
  (in-sizes 0 :type fixnum)
  (out-sizes 0 :type fixnum)
  (steps 1 :type fixnum))

(defstruct-raw accg-edge
  (tail -1 :type fixnum)
  (head -1 :type fixnum)
  (ccmf nil :type (or null ccmf)))

(defstruct-raw accg-node
  (context (make-context) :type context)
  (fwd-edges nil :type list)
  (bwd-edges nil :type list)
  (num 0 :type fixnum))

(defmacro-raw accg-node-ruler
  (accg)
  `(context-ruler (accg-node-context ,ACCG)))

(defmacro-raw accg-node-call
  (accg)
  `(context-call (accg-node-context ,ACCG)))

(defmacro-raw accg-node-parent-funct
  (accg)
  `(context-parent-funct (accg-node-context ,ACCG)))

(defmacro-raw accg-node-call-funct
  (accg)
  `(context-call-funct (accg-node-context ,ACCG)))

(defmacro-raw accg-node-fn
  (accg)
  `(context-fn (accg-node-context ,ACCG)))

(defmacro-raw accg-node-formals
  (accg)
  `(context-formals (accg-node-context ,ACCG)))

(defmacro-raw accg-node-callformals
  (accg)
  `(context-callformals (accg-node-context ,ACCG)))

(defmacro-raw accg-node-callfn
  (accg)
  `(context-callfn (accg-node-context ,ACCG)))

(defmacro-raw accg-node-context-num
  (accg)
  `(context-num (accg-node-context ,ACCG)))

(defmacro-raw accg-node-ccms
  (accg)
  `(context-ccms (accg-node-context ,ACCG)))

(defstruct-raw srg-edge
  (tail 0 :type fixnum)
  (head 0 :type fixnum)
  (ccmf (make-ccmf) :type ccmf)
  (label 'none :type symbol))

(defstruct-raw srg-node
  (node 0 :type fixnum)
  (ccm 0 :type fixnum)
  (fwd-edges nil :type list)
  (bwd-edges nil :type list))

(defstruct-raw memoization
  (proved nil :type list)
  (unproved (make-array 0 :initial-element nil :element-type 'list)
    :type (vector list)))

(defun-raw create-memoization
  (max-ind)
  (make-memoization :unproved (make-array (1+ max-ind)
      :initial-element nil
      :element-type 'list)))

(defun-raw ccg-simplify-hyps-no-split
  (hyps ctx ens wrld state)
  (declare (ignore ctx))
  (mv-let (nhyps ttree)
    (normalize-lst hyps
      t
      nil
      ens
      wrld
      nil
      (backchain-limit wrld :ts))
    (er-progn (accumulate-ttree-and-step-limit-into-state ttree
        :skip state)
      (value (flatten-ands-in-lit-lst nhyps)))))

(defrec query-spec-var
  ((wrld . ens) (ctx . otf-flg) (stop-time . mem))
  t)

(defun-raw print-funct-ccms
  (functs wrld state)
  (if (endp functs)
    state
    (pprogn (fms "The CCM~#1~[~/s~] for ~x0 ~#1~[is~/are~] ~&1.~|"
        `((#\0 . ,(FUNCT-FN (CAR FUNCTS))) (#\1 . ,(UNTRANSLATE-LST
  (MAPCAR #'DE-PROPAGATE (COERCE (FUNCT-CCMS (CAR FUNCTS)) 'LIST)) NIL WRLD)))
        *standard-co*
        state
        nil)
      (print-funct-ccms (cdr functs) wrld state))))

(defun-raw prettify-ccms
  (ccm-array vars vals wrld)
  (let ((fn (if vars
         (function (lambda (x)
             (untranslate (subcor-var vars vals (de-propagate x))
               nil
               wrld)))
         (function (lambda (x) (untranslate (de-propagate x) nil wrld))))))
    (map 'vector fn ccm-array)))

(defmacro-raw ce-defun-fn (defun) `(cadr ,DEFUN))

(defmacro-raw ce-defun-formals (defun) `(caddr ,DEFUN))

(defmacro-raw ce-defun-body (defun) `(cadddr ,DEFUN))

(defmacro-raw ce-defun-test
  (defun)
  `(let ((body (ce-defun-body ,DEFUN)))
    (if (eq (fn-symb body) 'if)
      (cadr body)
      t)))

(defmacro-raw ce-defun-call
  (defun)
  `(let ((body (ce-defun-body ,DEFUN)))
    (if (eq (fn-symb body) 'if)
      (caddr body)
      body)))

(defun-raw ccmf-graph-no-edges?
  (ccmf-graph)
  (loop for
    node
    across
    ccmf-graph
    when
    (or (consp (ccmf-node->-edges node))
      (consp (ccmf-node->=-edges node)))
    return
    nil
    finally
    (return t)))

(defun-raw ccmf-graph-term
  (i graph ccms0 ccms1 acc)
  (if (< i 0)
    (cond ((endp acc) acc)
      ((endp (cdr acc)) (car acc))
      (t (cons 'and acc)))
    (let* ((node (aref graph i)) (>=-edges (ccmf-node->=-edges node))
        (>-edges (ccmf-node->-edges node))
        (ccm (de-propagate (aref ccms0 i))))
      (ccmf-graph-term (1- i)
        graph
        ccms0
        ccms1
        (append (mapcar (function (lambda (x) `(> ,CCM ,(DE-PROPAGATE (AREF CCMS1 X)))))
            >-edges)
          (mapcar (function (lambda (x) `(>= ,CCM ,(DE-PROPAGATE (AREF CCMS1 X)))))
            >=-edges)
          acc)))))

(defun-raw print-ccmfs1
  (defuns defun0 defun1 ccmfs flst funct0 col wrld state)
  (if (endp defuns)
    state
    (let* ((graph (ccmf-graph (car ccmfs))) (ne? (ccmf-graph-no-edges? graph))
        (f0 (car defuns))
        (f1 (if (consp (cdr defuns))
            (cadr defuns)
            defun0))
        (f2 (cond ((endp (cdr defuns)) defun1)
            ((endp (cddr defuns)) defun0)
            (t (caddr defuns))))
        (fn0 (ce-defun-fn f0))
        (fn1 (ce-defun-fn f1))
        (fn2 (ce-defun-fn f2))
        (formals (ce-defun-formals f1))
        (actuals (fargs (ce-defun-call f0)))
        (ccms0 (prettify-ccms (funct-ccms (car flst)) nil nil wrld))
        (ccms0-lst (coerce ccms0 'list))
        (ccms1 (prettify-ccms (funct-ccms (if (endp (cdr flst))
                funct0
                (cadr flst)))
            formals
            actuals
            wrld))
        (ccms1-lst (coerce ccms1 'list)))
      (pprogn (fms "When execution moves from the recursive call in ~x0 of ~x1 to ~
             ~#2~[itself~/the recursive call in ~x1 of ~x3~], we need to know ~
             how the measures of ~x0 compare with the result of substituting ~
             the formals of ~x1 with the actuals of the call to ~x1 in the ~
             measures of ~x1. The measure~#4~[~/s~] for ~x0 ~
             ~#4~[is~/are~]:~|~%~*6~%The result~#5~[~/s~] of applying the ~
             substitution to the measures of ~x1 ~#5~[is~/are~]:~|~%~*7~%We ~
             know ~#8~[nothing about how the values of these CCMs ~
             relate.~/the following about these CCMs:~%~%~Y9A~]~|~%If you can ~
             show that any of the terms in the first list is always either ~
             strictly greater than, or greater than or equal to some term in ~
             the second list, this could be helpful for proving termination.~|"
          (list (cons #\0 fn0)
            (cons #\1 fn1)
            (cons #\2
              (if (eq fn0 fn1)
                0
                1))
            (cons #\3 fn2)
            (cons #\4 ccms0-lst)
            (cons #\5 ccms1-lst)
            (cons #\6 `("" "~x*.~|" "~x*~|" "~x*~|" ,CCMS0-LST))
            (cons #\7 `("" "~x*.~|" "~x*~|" "~x*~|" ,CCMS1-LST))
            (cons #\8
              (if ne?
                0
                1))
            (cons #\9
              (ccmf-graph-term (1- (array-dimension graph 0))
                graph
                ccms0
                ccms1
                nil))
            (cons #\A (term-evisc-tuple nil state)))
          *standard-co*
          state
          nil)
        (print-ccmfs1 (cdr defuns)
          defun0
          defun1
          (cdr ccmfs)
          (cdr flst)
          funct0
          col
          wrld
          state)))))

(defun-raw print-ccmfs
  (defuns ccmfs flst col wrld state)
  (if (endp defuns)
    state
    (print-ccmfs1 defuns
      (car defuns)
      (if (endp (cdr defuns))
        (car defuns)
        (cadr defuns))
      ccmfs
      flst
      (car flst)
      col
      wrld
      state)))

(defun-raw print-ccms
  (defuns functs col wrld state)
  (if (endp defuns)
    (mv-let (col state)
      (fmt1 "~|" nil col *standard-co* state nil)
      (declare (ignore col))
      state)
    (mv-let (col state)
      (fmt1 "The CCM~#1~[~/s~] for ~x0 ~#1~[is~/are~] ~&1. "
        (list (cons #\0 (cadar defuns))
          (cons #\1
            (untranslate-lst (mapcar (function de-propagate)
                (coerce (funct-ccms (car functs)) 'list))
              nil
              wrld)))
        col
        *standard-co*
        state
        nil)
      (print-ccms (cdr defuns) (cdr functs) col wrld state))))

(defun-raw produce-counter-example1
  (ccmfs context-array alist wrld)
  (if (endp ccmfs)
    (mv nil nil nil)
    (let* ((context (aref context-array (car (ccmf-fc-num (car ccmfs))))) (funct (context-parent-funct context))
        (fn (funct-fn funct)))
      (mv-let (name i)
        (ccg-counter-example-fn-name fn
          (assoc-eq-value fn 0 alist)
          wrld)
        (mv-let (contexts functs names)
          (produce-counter-example1 (cdr ccmfs)
            context-array
            (assoc-set-eq fn (1+ i) alist)
            wrld)
          (mv (cons context contexts)
            (cons funct functs)
            (cons name names)))))))

(defun-raw produce-counter-example2
  (contexts names name0 ctx ens wrld state)
  (if (endp contexts)
    (value nil)
    (let* ((context (car contexts)) (funct (context-parent-funct context))
        (call (cons (if (endp (cdr names))
              name0
              (cadr names))
            (fargs (context-call context)))))
      (er-let* ((ruler (state-global-let* ((inhibit-output-lst *valid-output-names*))
             (simp-hyps0 (context-ruler context)
               ctx
               ens
               wrld
               state
               nil
               t
               nil
               :term-order))) (body (value (if (endp ruler)
                call
                `(if ,(IF (ENDP (CDR RULER))
     (CAR RULER)
     `(AND ,@RULER))
                  ,CALL
                  (list ,@(FUNCT-FORMALS FUNCT))))))
          (rst (produce-counter-example2 (cdr contexts)
              (cdr names)
              name0
              ctx
              ens
              wrld
              state)))
        (value (cons `(defun ,(CAR NAMES) ,(FUNCT-FORMALS FUNCT) ,BODY)
            rst))))))

(defun-raw accg-find-ccmf
  (accg i j)
  (loop for
    edge
    in
    (accg-node-fwd-edges (aref accg i))
    when
    (= j (accg-edge-head edge))
    return
    (accg-edge-ccmf edge)))

(defun-raw produce-counter-example
  (path accg context-array ctx ens wrld state)
  (let* ((ccmfs (loop for
         p
         on
         path
         when
         (and (consp p) (consp (cdr p)))
         collect
         (accg-find-ccmf accg (car p) (cadr p)))))
    (pprogn (fms "Producing counter-example, including simplifying rulers in order to ~
           maximize the readability of the counter-example."
        nil
        *standard-co*
        state
        nil)
      (mv-let (contexts functs names)
        (produce-counter-example1 ccmfs context-array nil wrld)
        (er-let* ((defuns (produce-counter-example2 contexts
               names
               (car names)
               ctx
               ens
               wrld
               state)))
          (value (list* ccmfs functs defuns)))))))

(defun-raw print-counter-example
  (accg ce contexts ctx ens wrld state)
  (er-let* ((triple (produce-counter-example (cdr ce)
         accg
         contexts
         ctx
         ens
         wrld
         state)) (ccmfs (value (car triple)))
      (functs (value (cadr triple)))
      (defuns (value (cddr triple))))
    (pprogn (fms "The following function definitions correspond to an actual loop in ~
          your function definitions for which the CCG analysis was unable to ~
          prove termination in all cases: ~%~%~Y01~%"
        (list (cons #\0
            (untranslate (if (endp (cdr defuns))
                (car defuns)
                (cons 'mutual-recursion defuns))
              nil
              wrld))
          (cons #\1 (term-evisc-tuple nil state)))
        *standard-co*
        state
        nil)
      (print-ccmfs defuns ccmfs functs 0 wrld state)
      (let* ((loop-graph (car ce)) (ne? (ccmf-graph-no-edges? loop-graph))
          (ccms (funct-ccms (car functs))))
        (fms "As it stands, we do not have enough information to show that this ~
            loop terminates. ~#0~[When we put it all together, we find that ~
            when we loop from ~x1 to itself, we know ~#2~[nothing about how ~
            the values of the CCMs change. ~/the following about how values ~
            change from one iteration to the loop to the next (measures are ~
            presented without substitution):~%~%~Y34~]~/~]~|~%Note that under ~
            this abstraction, the loop is idempotent (i.e. going through the ~
            loop again will result in the same information about ~
            non-increasing and decreasing values as we have just stated), and ~
            that there is no CCM that decreases to itself across the loop. ~
            There are therefore three possibilities: ~|~%(1) We did not guess ~
            the CCMs needed for proving termination. If this is the case, you ~
            could provide them for us using a :CONSIDER-CCMS or ~
            :CONSIDER-ONLY-CCMS hint (see :DOC CCG-XARGS). If you are truly ~
            desperate, you can resort to proving termination using ACL2's ~
            measure-based termination method (do this globally by using ~
            SET-TERMINATION-METHOD or just once by using the ~
            :TERMINATION-METHOD xarg; see :DOC CCG-XARGS).~|~%(2) We guessed ~
            the proper CCMs, but were unable to prove some necessary ~
            theorem(s) about how these values change from step to step in the ~
            loop. In this case, we suggest that you look at the ~
            counter-example we generated and use it to determine what ~
            additional lemmas are needed for CCG analysis to successfully ~
            prove termination.~|~%(3) The loop really is non-terminating for ~
            some inputs. In this case, you should alter the definition of the ~
            function so that it will terminate on all inputs.~%~%"
          (list (cons #\0
              (if (consp (cdr defuns))
                0
                1))
            (cons #\1 (cadar defuns))
            (cons #\2
              (if ne?
                0
                1))
            (cons #\3
              (untranslate (ccmf-graph-term (1- (array-dimension loop-graph 0))
                  loop-graph
                  ccms
                  ccms
                  nil)
                nil
                wrld))
            (cons #\4 (term-evisc-tuple nil state)))
          *standard-co*
          state
          nil)))))

(defun-raw print-ccmf-changes
  (col changes state)
  (if (endp changes)
    state
    (let ((change (car changes)))
      (mv-let (col state)
        (fmt1 "When execution moves ~@0, the following ~
             always holds:~|~%~x1.~|~%"
          `((#\0 . ,(IF (CONSP (CAR CHANGE))
     `("from context ~x0 to context ~x1" (#\0 . ,(CAAR CHANGE))
       (#\1 . ,(CDAR CHANGE)))
     `("across context ~x0" (#\0 . ,(CAR CHANGE))))) (#\1 . ,(CDR CHANGE)))
          col
          *standard-co*
          state
          nil)
        (print-ccmf-changes col (cdr changes) state)))))

(defun-raw p<
  (p1 p2)
  (or (< (car p1) (car p2))
    (and (= (car p1) (car p2)) (< (cdr p1) (cdr p2)))))

(defun-raw construct-accg-changes-printout
  (changes)
  (if (endp changes)
    nil
    (cons `("the edge from context ~x0 to context ~x1" (#\0 . ,(CAAR CHANGES))
        (#\1 . ,(CDAR CHANGES)))
      (construct-accg-changes-printout (cdr changes)))))

(defun-raw print-accg-changes
  (changes state)
  (if (endp changes)
    (fms "~|" nil *standard-co* state nil)
    (pprogn (fms "~x0 -> ~x1"
        `((#\0 . ,(CAAR CHANGES)) (#\1 . ,(CDAR CHANGES)))
        *standard-co*
        state
        nil)
      (print-accg-changes (cdr changes) state))))

(defun-raw print-changes
  (col changes state)
  (if (and (endp (car changes)) (endp (cdr changes)))
    (mv-let (col state)
      (fmt1 "We discovered nothing new about the CCG.~|"
        nil
        col
        *standard-co*
        state
        nil)
      (declare (ignore col))
      state)
    (mv-let (col state)
      (fmt1 "We discovered the following about the CCG.~|~%"
        nil
        col
        *standard-co*
        state
        nil)
      (mv-let (col state)
        (if (endp (car changes))
          (mv col state)
          (mv-let (col state)
            (fmt1 "We can safely omit the following edges from the CCG:~|"
              nil
              col
              *standard-co*
              state
              nil)
            (declare (ignore col))
            (mv 0 (print-accg-changes (car changes) state))))
        (print-ccmf-changes col
          (sort (copy-list (cdr changes))
            (if (consp (caadr changes))
              (function p<)
              (function <))
            :key (function car))
          state)))))

(defun-raw print-context-array1
  (i names context-array state)
  (if (>= i (array-dimension context-array 0))
    state
    (pprogn (let ((context (aref context-array i)))
        (fms "CALLING CONTEXT ~x0~#1~[~/ in the body of ~x2~]:~|rulers: ~
             ~x3~|call: ~x4~|"
          `((#\0 . ,I) (#\1 . ,NAMES)
            (#\2 . ,(CONTEXT-FN CONTEXT))
            (#\3 . ,(CONTEXT-RULER CONTEXT))
            (#\4 . ,(CONTEXT-CALL CONTEXT)))
          *standard-co*
          state
          nil))
      (print-context-array1 (1+ i) names context-array state))))

(defun-raw print-context-array
  (names context-array state)
  (pprogn (fms "The calling contexts for ~#0~[this definition~/these definitions~] ~
         are:~|"
      `((#\0 . ,NAMES))
      *standard-co*
      state
      nil)
    (print-context-array1 0 names context-array state)))

(defun-raw print-accg-edges3
  (edges accg state)
  (if (endp edges)
    state
    (pprogn (let ((pair (accg-edge-context-pair (car edges) accg)))
        (fms "~x0 -> ~x1"
          `((#\0 . ,(CAR PAIR)) (#\1 . ,(CDR PAIR)))
          *standard-co*
          state
          nil))
      (print-accg-edges3 (cdr edges) accg state))))

(defun-raw print-accg-edges2
  (i n accg state)
  (if (>= i n)
    state
    (pprogn (print-accg-edges3 (accg-node-fwd-edges (aref accg i))
        accg
        state)
      (print-accg-edges2 (1+ i) n accg state))))

(defun-raw print-accg-edges1
  (accgs state)
  (if (endp accgs)
    (fms "~|" nil *standard-co* state nil)
    (pprogn (print-accg-edges2 0
        (array-dimension (car accgs) 0)
        (car accgs)
        state)
      (print-accg-edges1 (cdr accgs) state))))

(defun-raw print-accg-edges
  (col accgs state)
  (if (endp accgs)
    state
    (mv-let (col state)
      (fmt1 "The Calling Context Graph has the following edges:~|"
        nil
        col
        *standard-co*
        state
        nil)
      (declare (ignore col))
      (print-accg-edges1 accgs state))))

(defun-raw ccg-negate
  (exp)
  (if (and (consp exp) (eq (first exp) 'not))
    (second exp)
    `(not ,EXP)))

(defun-raw ccg-addlist
  (lst)
  (cond ((endp lst) 0)
    ((endp (cdr lst)) (car lst))
    (t `(binary-+ ,(CAR LST) ,(CCG-ADDLIST (CDR LST))))))

(defun-raw ccg-count-contexts
  (tms)
  (let ((i 0))
    (dolist (tm tms i) (setf i (+ i (len tm))))))

(defun-raw subsumed-by-proved-clause
  (cl proved)
  (and (consp proved)
    (or (eq t (subsumes *init-subsumes-count* (car proved) cl nil))
      (subsumed-by-proved-clause cl (cdr proved)))))

(defun-raw eliminate-subsumed-tail
  (cl cl-set acc)
  (if (endp cl-set)
    acc
    (eliminate-subsumed-tail cl
      (cdr cl-set)
      (if (subsumes *init-subsumes-count* cl (car cl-set) nil)
        acc
        (cons (car cl-set) acc)))))

(defun-raw add-proved-clause
  (cl proved)
  (cons cl (eliminate-subsumed-tail cl proved nil)))

(defun-raw equals-unproved-clause1
  (cl unproved)
  (and (consp unproved)
    (or (let ((cl-unproved (car unproved)))
        (and (eq t (subsumes *init-subsumes-count* cl cl-unproved nil))
          (eq t (subsumes *init-subsumes-count* cl-unproved cl nil))))
      (equals-unproved-clause1 cl (cdr unproved)))))

(defun-raw equals-unproved-clause
  (cl unproved i)
  (and (< i (array-dimension unproved 0))
    (or (equals-unproved-clause1 cl (aref unproved i))
      (equals-unproved-clause cl unproved (1+ i)))))

(defmacro-raw time-er
  (ctx)
  `(er soft
    ,CTX
    "CCG analysis has exceeded the specified time ~
        limit. If you did not expect a time-limit, check the global ~
         time-limit setting (see :DOC set-ccg-time-limit and the ~
         discussion of the :time-limit flag in :DOC CCG) to find out ~
         more. At this point you have several options:~|~% ~
         * Set the :don't-guess-ccms flag to t. Sometimes CCG analysis ~
           guesses too many CCMs which leads to excessive prover ~
           queries. This will eliminate *all* CCMs other than the ~
           acl2s-size of each formal.~|~%~
         * Do you see a variable that you don't think is relevant to the ~
           termination proof? In that case, us the :ignore-formals flag ~
           to tell the CCG analysis to throw out CCMs that contain that ~
           formal. This may also cut down on CCMs and therefore prover ~
           queries.~|~%~
         * Finally, if you are willing to wait some more, you ~
           could try increasing the time limit, or eliminating it by ~
           setting it to nil."))

(defun-raw time-left
  (stop-time ctx state)
  (let ((now (get-internal-run-time)))
    (if (< now stop-time)
      (value (rationalize (/ (- stop-time now)
            (coerce internal-time-units-per-second 'float))))
      (time-er ctx))))

(defun-raw time-check
  (stop-time ctx state)
  (if (and (posp stop-time)
      (<= stop-time (get-internal-run-time)))
    (time-er ctx)
    (value nil)))

(defmacro-raw maybe-prover-before-stop-time
  (stop-time ctx state body)
  `(let ((stop-time ,STOP-TIME))
    (if (null stop-time)
      ,BODY
      (er-let* ((time-limit (time-left stop-time ,CTX ,STATE)))
        (with-prover-time-limit time-limit ,BODY)))))

(defun-raw query
  (hyps concl pt qspv state)
  (let* ((stop-time (access query-spec-var qspv :stop-time)) (mem (access query-spec-var qspv :mem))
      (otf-flg (access query-spec-var qspv :otf-flg))
      (ens (access query-spec-var qspv :ens))
      (ctx (access query-spec-var qspv :ctx))
      (wrld (access query-spec-var qspv :wrld))
      (clause (add-literal concl (dumb-negate-lit-lst hyps) t))
      (bic-onlyp (equal pt :built-in-clauses))
      (ind-limit (if bic-onlyp
          -1
          (cadr pt)))
      (displayed-goal (prettyify-clause-set (list clause)
          (let*-abstractionp state)
          wrld)))
    (pprogn (ccg-io? query
        nil
        state
        (bic-onlyp ind-limit clause wrld)
        (fms "We now make the following query, using ~
                           proof-technique ~x0 (see :DOC ~
                           CCG-hierarchy)~#1~[~/ and with the otf-flg set to ~
                           ~x2~]:~|~%GOAL~%~Y34."
          `((#\0 . ,PT) (#\1 . ,(IF BIC-ONLYP
     0
     1))
            (#\2 . ,OTF-FLG)
            (#\3 . ,DISPLAYED-GOAL)
            (#\4 . ,(TERM-EVISC-TUPLE NIL STATE)))
          (proofs-co state)
          state
          nil))
      (er-let* ((pair (cond (bic-onlyp (mv-let (built-in-clausep ttree)
                 (built-in-clausep 'query
                   clause
                   ens
                   (match-free-override wrld)
                   wrld
                   state)
                 (value (if built-in-clausep
                     (cons t ttree)
                     (cons nil nil)))))
             ((subsumed-by-proved-clause clause (memoization-proved mem)) (pprogn (ccg-io? query
                   nil
                   state
                   nil
                   (fms "But we see that this query is already ~
                                      subsumed by another query that was ~
                                      previously proven.~%~%"
                     nil
                     (proofs-co state)
                     state
                     nil))
                 (value (cons t nil))))
             ((equals-unproved-clause clause
                (memoization-unproved mem)
                ind-limit) (pprogn (ccg-io? query
                   nil
                   state
                   nil
                   (fms "But we see that we already tried and ~
                                      failed to prove an equivalent query ~
                                      using the same restrictions on the ~
                                      theorem prover.~%~%"
                     nil
                     (proofs-co state)
                     state
                     nil))
                 (value (cons nil nil))))
             (t (er-let* ((pair (let ((hints (translated-limit-induction-hint ind-limit)))
                      (maybe-prover-before-stop-time stop-time
                        ctx
                        state
                        (prove-no-er (termify-clause-set (list clause))
                          (make-pspv ens
                            wrld
                            state
                            :displayed-goal displayed-goal
                            :otf-flg otf-flg)
                          hints
                          ens
                          wrld
                          ctx
                          state)))))
                 (progn (if (car pair)
                     (setf (memoization-proved mem)
                       (add-proved-clause clause (memoization-proved mem)))
                     (setf (aref (memoization-unproved mem) ind-limit)
                       (cons clause (aref (memoization-unproved mem) ind-limit))))
                   (value pair)))))))
        (pprogn (ccg-io? query
            nil
            state
            nil
            (fms "ACL2 has ~#0~[SUCCEEDED in proving this ~
                             query~/FAILED to prove this query~].~|"
              (list (cons #\0
                  (if (car pair)
                    0
                    1)))
              (proofs-co state)
              state
              nil))
          (er-progn (time-check stop-time ctx state)
            (if (car pair)
              (accumulate-ttree-and-step-limit-into-state (cdr pair)
                :skip state)
              (pprogn (pprogn (f-put-global 'gag-state-saved
                    (f-get-global 'gag-state state)
                    state)
                  (f-put-global 'gag-state nil state))
                (value nil)))
            (value (car pair))))))))

(defun-raw ccg-generic-dfs-visit
  (u graph f color time node-fwd-edges edge-head)
  (setf (aref color u) 'grey)
  (dolist (vn (funcall node-fwd-edges (aref graph u)))
    (let ((v (funcall edge-head vn)))
      (when (eq (aref color v) 'white)
        (setf time
          (ccg-generic-dfs-visit v
            graph
            f
            color
            time
            node-fwd-edges
            edge-head)))))
  (setf (aref color u) 'black)
  (setf (aref f time) u)
  (incf time))

(defun-raw ccg-generic-dfs
  (graph node-fwd-edges edge-head)
  (let* ((size (array-total-size graph)) (f (make-array size :element-type 'fixnum))
      (time 0)
      (color (make-array size
          :element-type '(member white grey black)
          :initial-element 'white)))
    (dotimes (i size f)
      (when (eq (aref color i) 'white)
        (setf time
          (ccg-generic-dfs-visit i
            graph
            f
            color
            time
            node-fwd-edges
            edge-head))))))

(defun-raw ccg-generic-scc-aux
  (u graph
    scc
    scc-array
    scc-num
    color
    node-bwd-edges
    edge-tail)
  (let ((scc scc))
    (setf (aref color u) 'grey)
    (dolist (vn (funcall node-bwd-edges (aref graph u)))
      (let ((v (funcall edge-tail vn)))
        (when (eq (aref color v) 'white)
          (setf scc
            (ccg-generic-scc-aux v
              graph
              scc
              scc-array
              scc-num
              color
              node-bwd-edges
              edge-tail)))))
    (setf (aref color u) 'black)
    (setf (aref scc-array u) scc-num)
    (cons u scc)))

(defun-raw ccg-generic-scc
  (graph node-fwd-edges node-bwd-edges edge-tail edge-head)
  (let ((scc-num -1))
    (loop with
      f
      =
      (ccg-generic-dfs graph node-fwd-edges edge-head)
      with
      size
      =
      (array-dimension graph 0)
      with
      color
      =
      (make-array size
        :element-type '(member black grey white)
        :initial-element 'white)
      with
      scc-array
      =
      (make-array size :element-type 'fixnum :initial-element 0)
      for
      i
      from
      (1- size)
      downto
      0
      for
      u
      =
      (aref f i)
      when
      (eq (aref color u) 'white)
      collect
      (ccg-generic-scc-aux u
        graph
        nil
        scc-array
        (incf scc-num)
        color
        node-bwd-edges
        edge-tail)
      into
      sccs
      finally
      (return (values sccs scc-array)))))

(defun-raw accg-can-omit-edge?
  (node1 node2 hlevel qspv state)
  (if (hlevel-ccmfs-per-nodep hlevel)
    (value nil)
    (query (append (accg-node-ruler node1)
        (subcor-var-lst (accg-node-formals node2)
          (fargs (accg-node-call node1))
          (accg-node-ruler node2)))
      nil
      (hlevel-proof-technique hlevel)
      qspv
      state)))

(defun-raw accg-fill-in-edges
  (accg name-node-alist)
  (loop for
    i
    from
    0
    below
    (array-dimension accg 0)
    for
    node1
    =
    (aref accg i)
    for
    successors
    =
    (cdr (assoc (accg-node-callfn node1) name-node-alist))
    do
    (setf (accg-node-fwd-edges node1)
      (loop for
        node2
        in
        successors
        for
        j
        =
        (accg-node-num node2)
        for
        edge
        =
        (make-accg-edge :tail i :head j)
        do
        (setf (accg-node-bwd-edges node2)
          (cons edge (accg-node-bwd-edges node2)))
        collect
        edge))))

(defun-raw context-to-accg-node-lst
  (contexts total)
  (if (endp contexts)
    (mv nil total)
    (mv-let (nodes ntotal)
      (context-to-accg-node-lst (cdr contexts) total)
      (let ((node (make-accg-node :context (car contexts))))
        (mv (cons node nodes) (cons node ntotal))))))

(defun-raw ccg-build-accg0
  (names contexts)
  (if (endp names)
    (mv nil nil)
    (let ((name (car names)) (context-list (car contexts)))
      (mv-let (alist total)
        (ccg-build-accg0 (cdr names) (cdr contexts))
        (mv-let (nodes ntotal)
          (context-to-accg-node-lst context-list total)
          (mv (acons name nodes alist) ntotal))))))

(defun-raw ccg-build-accg
  (names contexts)
  (mv-let (name-node-alist accg-node-lst)
    (ccg-build-accg0 names contexts)
    (let ((accg (coerce accg-node-lst 'vector)))
      (progn (loop for
          i
          from
          0
          below
          (array-dimension accg 0)
          do
          (setf (accg-node-num (aref accg i)) i))
        (accg-fill-in-edges accg name-node-alist)
        accg))))

(defun-raw simplify-contexts1
  (context-lst ens wrld ctx state)
  (if (endp context-lst)
    state
    (mv-let (erp value state)
      (ccg-simplify-hyps-no-split (context-ruler (car context-lst))
        ctx
        ens
        wrld
        state)
      (progn (unless erp (setf (context-ruler (car context-lst)) value))
        (simplify-contexts1 (cdr context-lst) ens wrld ctx state)))))

(defun-raw simplify-contexts
  (contexts ens wrld ctx state)
  (if (endp contexts)
    state
    (pprogn (simplify-contexts1 (car contexts) ens wrld ctx state)
      (simplify-contexts (cdr contexts) ens wrld ctx state))))

(defun-raw ccg-formal-sizes
  (formals)
  (loop for
    x
    in
    formals
    collect
    `(acl2s-size ,X)))

(defun-raw ccg-add-zp-ccm
  (r formals ccms)
  (cond ((atom r) ccms)
    ((and (eq (ffn-symb r) 'not)
       (consp (fargn r 1))
       (eq (ffn-symb (fargn r 1)) 'zp)
       (not (member-eq (fargn (fargn r 1) 1) formals))) (cons (fargn (fargn r 1) 1) ccms))
    (t ccms)))

(defun-raw ccg-add-<-ccm
  (r formals ccms)
  (declare (ignore formals))
  (cond ((atom r) ccms)
    ((or (eq (car r) '<)
       (and (eq (car r) 'not)
         (consp (second r))
         (eq (car (second r)) '<))) (let* ((not? (eq (car r) 'not)) (r0 (if (eq (car r) '<)
              r
              (second r)))
          (rarg1 (second r0))
          (rarg2 (third r0))
          (p (term-order (second r0) (third r0)))
          (arg1 (if p
              (second r0)
              (third r0)))
          (arg2 (if p
              (third r0)
              (second r0))))
        (cond ((and (quotep arg1) (quotep arg2)) ccms)
          ((not (or (quotep arg1) (quotep arg2))) (if not?
              (cons `(acl2s-size (binary-+ '1 (binary-+ ,RARG1 (unary-- ,RARG2))))
                ccms)
              (cons `(acl2s-size (binary-+ '1 (binary-+ ,RARG2 (unary-- ,RARG1))))
                ccms)))
          ((and (quotep arg1) (acl2-numberp (unquote arg1))) (if (and (or (eql (unquote arg1) 0) (eql (unquote arg1) 1))
                (variablep arg2))
              ccms
              (cons `(acl2s-size (binary-+ ',(- 1 (UNQUOTE ARG1)) ,ARG2))
                ccms)))
          ((and (quotep arg2) (acl2-numberp (unquote arg2))) (if (and (or (eql (unquote arg2) 0) (eql (unquote arg2) 1))
                (variablep arg1))
              ccms
              (cons `(acl2s-size (binary-+ ',(- 1 (UNQUOTE ARG2)) ,ARG1))
                ccms)))
          (t ccms))))
    (t ccms)))

(defun-raw ccg-add-dec-ccm
  (arg ccms)
  (if (and (consp arg) (eq (car arg) 'dec))
    (cons arg ccms)
    ccms))

(defun-raw accg-guess-ccms-for-node
  (node)
  (let ((ccms nil) (rulers (accg-node-ruler node))
      (formals (accg-node-formals node)))
    (dolist (r rulers ccms)
      (setf ccms (ccg-add-<-ccm r formals ccms))
      (setf ccms (ccg-add-zp-ccm r formals ccms)))))

(defun-raw ccg-remove-duplicate-ccms-in-functs
  (functs)
  (dolist (funct functs functs)
    (setf (funct-ccms funct)
      (remove-duplicates (funct-ccms funct)
        :test (function equal)
        :key (function de-propagate)))))

(defun-raw ccg-remove-duplicate-ccms
  (ccms)
  (let ((n (array-dimension ccms 0)))
    (dotimes (i n ccms)
      (setf (aref ccms i)
        (remove-duplicates (aref ccms i)
          :test (function equal)
          :key (function de-propagate))))))

(defun-raw accg-propagate-ccm
  (ccm accg n consider-onlyp)
  (let* ((size (array-dimension accg 0)) (queued (make-array size
          :element-type 'boolean
          :initial-element nil))
      (successor (make-array size :element-type 'integer :initial-element 0))
      (ccms (make-array size :initial-element nil))
      (queue (make-array size :element-type 'integer :initial-element -1))
      (c (accg-node-context-num (aref accg n)))
      (i 0)
      (queue-preds (lambda (m)
          (loop for
            edge
            in
            (accg-node-bwd-edges (aref accg m))
            for
            pred
            =
            (accg-edge-tail edge)
            unless
            (or (aref queued pred) (aref consider-onlyp pred))
            do
            (setf (aref queued pred) t)
            and
            do
            (setf (aref queue (incf i)) pred)
            and
            do
            (setf (aref successor pred) m)))))
    (let ((node (aref accg n)))
      (setf (accg-node-ccms node)
        (cons ccm (accg-node-ccms node)))
      (setf (aref ccms n) ccm))
    (setf (aref queued n) t)
    (funcall queue-preds n)
    (loop for
      j
      from
      1
      below
      size
      for
      k
      =
      (aref queue j)
      when
      (= k -1)
      return
      nil
      do
      (let* ((succ (aref successor k)) (node (aref accg k))
          (nccm (subcor-var (accg-node-callformals node)
              (fargs (accg-node-call node))
              (aref ccms succ))))
        (setf (aref ccms k) nccm))
      do
      (funcall queue-preds k))
    (loop for
      j
      from
      1
      below
      size
      for
      k
      =
      (aref queue j)
      when
      (= k -1)
      return
      nil
      do
      (let ((node (aref accg k)))
        (setf (accg-node-ccms node)
          (cons `(ccg-propagate ,C ,(AREF CCMS K))
            (accg-node-ccms node)))))))

(defun-raw accg-propagate-ccms
  (ccms accg consider-onlyp)
  (loop with
    size
    =
    (array-dimension ccms 0)
    for
    i
    from
    0
    below
    size
    do
    (loop for
      ccm
      in
      (aref ccms i)
      do
      (accg-propagate-ccm ccm accg i consider-onlyp))))

(defun-raw accg-partition-ccms-by-function
  (ccms nodes)
  (loop for
    i
    from
    0
    below
    (array-dimension ccms 0)
    for
    funct
    =
    (accg-node-parent-funct (aref nodes i))
    do
    (setf (funct-ccms funct)
      (append (aref ccms i) (funct-ccms funct)))))

(defun-raw accg-guess-ccms
  (accg functs ccm-hints-alist)
  (let* ((size (array-dimension accg 0)) (ccms (make-array size :element-type 'list :initial-element nil))
      (consider-onlyp (make-array size
          :element-type 'boolean
          :initial-element nil)))
    (loop for
      i
      from
      0
      below
      size
      for
      entry
      =
      (assoc (accg-node-fn (aref accg i)) ccm-hints-alist)
      do
      (setf (aref consider-onlyp i) (cadr entry))
      unless
      (eq (cddr entry) *0*)
      do
      (setf (aref ccms i) (cddr entry)))
    (loop for
      i
      from
      0
      below
      size
      for
      node
      =
      (aref accg i)
      unless
      (or (aref consider-onlyp i)
        (endp (accg-node-fwd-edges (aref accg i))))
      do
      (setf (aref ccms i)
        (append (accg-guess-ccms-for-node node) (aref ccms i))))
    (accg-propagate-ccms (ccg-remove-duplicate-ccms ccms)
      accg
      consider-onlyp)
    (ccg-remove-duplicate-ccms-in-functs functs)
    (loop for
      funct
      in
      functs
      for
      fn-sccms
      in
      ccm-hints-alist
      for
      fsizes
      =
      (ccg-formal-sizes (funct-formals funct))
      unless
      (cadr fn-sccms)
      do
      (setf (funct-ccms funct)
        (append fsizes
          (if (length-exceedsp fsizes 1)
            (cons (ccg-addlist fsizes) (funct-ccms funct))
            (funct-ccms funct))))
      finally
      (ccg-remove-duplicate-ccms-in-functs functs))
    (loop for
      funct
      in
      functs
      do
      (setf (funct-ccms funct)
        (coerce (funct-ccms funct) 'vector)))))

(defun-raw ccmf->-value?
  (ruler e1 e2 pt qspv state)
  (query ruler
    `(o< ,(DE-PROPAGATE E2) ,(DE-PROPAGATE E1))
    pt
    qspv
    state))

(defun-raw ccmf->=-value?
  (ruler e1 e2 pt qspv state)
  (query ruler
    `(not (o< ,(DE-PROPAGATE E1) ,(DE-PROPAGATE E2)))
    pt
    qspv
    state))

(defun-raw ccmf-skip-edge
  (f1 n1 c1 e1 f2 n2 e2 hlevel)
  (or (null hlevel)
    (eq (fn-symb e1) 'ccg-propagated)
    (and (eq (fn-symb e2) 'ccg-propagated)
      (not (equal (fargn e2 1) c1)))
    (and (let ((v1 (all-vars e1)) (v2 (all-vars e2)))
        (and (not (and (eq f1 f2) (= n1 n2)))
          (case (hlevel-ccm-comparison-scheme hlevel)
            (:equal (not (and (subsetp v1 v2) (subsetp v2 v1))))
            (:all (or (subsetp v2 v1) (not (subsetp v1 v2))))
            (:some (or (subsetp v1 v2) (not (intersectp-eq v1 v2))))
            (:none (intersectp-eq v1 v2))))))))

(defun-raw accg-copy-ccmf-graph
  (graph &key (size nil))
  (let* ((n (array-dimension graph 0)) (ngraph (make-array (if size
            (max n size)
            n)
          :element-type 'ccmf-node
          :initial-element (make-ccmf-node))))
    (loop for
      i
      from
      0
      below
      n
      for
      node
      =
      (aref graph i)
      do
      (setf (aref ngraph i)
        (make-ccmf-node :>-edges (copy-list (ccmf-node->-edges node))
          :>=-edges (copy-list (ccmf-node->=-edges node)))))
    ngraph))

(defun-raw accg-add-ccmfs
  (accg)
  (loop for
    node1
    across
    accg
    for
    in-sizes
    =
    (array-dimension (accg-node-ccms node1) 0)
    do
    (loop for
      edge
      in
      (accg-node-fwd-edges node1)
      for
      head
      =
      (accg-edge-head edge)
      for
      node2
      =
      (aref accg head)
      for
      graph
      =
      (make-array in-sizes)
      do
      (loop for
        i
        from
        0
        below
        in-sizes
        do
        (setf (aref graph i) (make-ccmf-node)))
      do
      (setf (accg-edge-ccmf edge)
        (make-ccmf :firstsite (accg-edge-tail edge)
          :lastsite head
          :fc-num (accg-node-context-num node1)
          :lc-num (accg-node-context-num node2)
          :in-sizes in-sizes
          :out-sizes (array-dimension (accg-node-ccms node2) 0)
          :graph graph)))))

(defun-raw accg-scc
  (graph)
  (ccg-generic-scc graph
    (function accg-node-fwd-edges)
    (function accg-node-bwd-edges)
    (function accg-edge-tail)
    (function accg-edge-head)))

(defun-raw accg-edge-context-pair
  (edge accg)
  (cons (car (accg-node-context-num (aref accg (accg-edge-tail edge))))
    (car (accg-node-context-num (aref accg (accg-edge-head edge))))))

(defun-raw accg-delete-non-scc-edges1
  (edges accg scc scc-array)
  (if (endp edges)
    (mv nil nil)
    (mv-let (changes nedges)
      (accg-delete-non-scc-edges1 (cdr edges) accg scc scc-array)
      (if (= scc (aref scc-array (accg-edge-head (car edges))))
        (mv changes (cons (car edges) nedges))
        (mv (cons (accg-edge-context-pair (car edges) accg) changes)
          nedges)))))

(defun-raw accg-delete-non-scc-edges
  (accg scc-array)
  (loop with
    changes
    =
    nil
    for
    i
    from
    0
    below
    (array-dimension accg 0)
    for
    nodei
    =
    (aref accg i)
    for
    scci
    =
    (aref scc-array i)
    do
    (mv-let (nchanges nedges)
      (accg-delete-non-scc-edges1 (accg-node-fwd-edges nodei)
        accg
        scci
        scc-array)
      (progn (setf (accg-node-fwd-edges nodei) nedges)
        (setf changes (append nchanges changes))))
    do
    (setf (accg-node-bwd-edges nodei)
      (delete-if-not (function (lambda (x) (= scci (aref scc-array (accg-edge-tail x)))))
        (accg-node-bwd-edges nodei)))
    finally
    (return changes)))

(defun-raw accg-separate-sccs0
  (accg sccs scc-array &key (ccmfp nil))
  (if (endp (cdr sccs))
    (mv nil (list accg))
    (let* ((m (array-dimension accg 0)) (n (len sccs))
        (count (make-array n :element-type 'fixnum :initial-element 0))
        (mapping (make-array m :element-type 'fixnum :initial-element 0))
        (changes nil))
      (loop for
        i
        from
        0
        below
        m
        for
        j
        =
        (aref scc-array i)
        do
        (setf (aref mapping i) (aref count j))
        do
        (incf (aref count j)))
      (let ((naccgs (make-array n)))
        (loop for
          i
          from
          0
          below
          n
          do
          (setf (aref naccgs i) (make-array (aref count i))))
        (loop for
          i
          from
          0
          below
          m
          for
          sccn
          =
          (aref scc-array i)
          for
          noden
          =
          (aref mapping i)
          for
          node
          =
          (aref accg i)
          do
          (setf (aref (aref naccgs sccn) noden) node)
          do
          (setf (accg-node-num node) noden)
          do
          (setf (accg-node-bwd-edges node) nil))
        (loop for
          i
          from
          0
          below
          n
          for
          naccg
          =
          (aref naccgs i)
          do
          (loop for
            j
            from
            0
            below
            (aref count i)
            for
            node
            =
            (aref naccg j)
            do
            (setf (accg-node-fwd-edges node)
              (loop for
                e
                in
                (accg-node-fwd-edges node)
                for
                head
                =
                (accg-edge-head e)
                for
                nhead
                =
                (aref mapping head)
                for
                ccmf
                =
                (accg-edge-ccmf e)
                if
                (= (aref scc-array head) i)
                do
                (setf (accg-edge-head e) nhead)
                and
                do
                (setf (accg-edge-tail e) j)
                and
                do
                (let ((hnode (aref naccg nhead)))
                  (setf (accg-node-bwd-edges hnode)
                    (cons e (accg-node-bwd-edges hnode))))
                and
                collect
                e
                and
                when
                ccmfp
                do
                (setf (ccmf-firstsite ccmf) j)
                and
                do
                (setf (ccmf-lastsite ccmf) nhead)
                else
                do
                (setf changes
                  (cons (accg-edge-context-pair e accg) changes))))))
        (mv changes
          (loop for
            i
            from
            0
            below
            n
            for
            naccg
            =
            (aref naccgs i)
            unless
            (and (= (aref count i) 1)
              (not (accg-node-fwd-edges (aref naccg 0))))
            collect
            naccg))))))

(defun-raw accg-separate-sccs
  (accg &key (ccmfp nil))
  (multiple-value-bind (sccs scc-array)
    (accg-scc accg)
    (accg-separate-sccs0 accg sccs scc-array :ccmfp ccmfp)))

(defun-raw build-and-annotate-accgs
  (names functs contexts ccm-hints-alist)
  (let ((accg (ccg-build-accg names contexts)))
    (multiple-value-bind (sccs scc-array)
      (accg-scc accg)
      (progn (accg-delete-non-scc-edges accg scc-array)
        (accg-guess-ccms accg functs ccm-hints-alist)
        (accg-add-ccmfs accg)
        (mv-let (changes0 naccgs)
          (accg-separate-sccs0 accg sccs scc-array :ccmfp t)
          (declare (ignore changes0))
          naccgs)))))

(defun-raw weaker-proof-techniquesp
  (h1 h2)
  (or (null h1)
    (not (null h2))
    (let ((pt1 (car h1)) (pt2 (car h2)))
      (if (equal pt1 :built-in-clauses)
        (not (equal pt2 :built-in-clauses))
        (and (consp pt2) (< (cadr pt1) (cadr pt2)))))))

(defun-raw accg-ccmf-adj-matrix
  (ccmf)
  (loop with
    n1
    =
    (ccmf-in-sizes ccmf)
    with
    n2
    =
    (ccmf-out-sizes ccmf)
    with
    graph
    =
    (ccmf-graph ccmf)
    with
    matrix
    =
    (make-array `(,N1 ,N2)
      :initial-element nil
      :element-type '(member nil '>= '>))
    for
    i
    from
    0
    below
    n1
    for
    node
    =
    (aref graph i)
    do
    (loop for
      j
      in
      (ccmf-node->-edges node)
      do
      (setf (aref matrix i j) '>))
    do
    (loop for
      j
      in
      (ccmf-node->=-edges node)
      do
      (setf (aref matrix i j) '>=))
    finally
    (return matrix)))

(defun-raw accg-refine-ccmf2
  (i j
    matrix
    node
    e1
    hyps
    f1
    c1
    f2
    ccms2
    cformals
    args
    redop
    changes
    old-hlevel
    hlevel
    qspv
    state)
  (let ((wrld (access query-spec-var qspv :wrld)))
    (if (< j 0)
      (value changes)
      (let* ((o2 (aref ccms2 j)) (e2 (subcor-var cformals args o2))
          (u1 (untranslate e1 nil wrld))
          (u2 (untranslate o2 nil wrld))
          (skipp (or (ccmf-skip-edge f1 i c1 e1 f2 j e2 hlevel)
              (not (or redop (ccmf-skip-edge f1 i c1 e1 f2 j e2 old-hlevel)))))
          (label (aref matrix i j))
          (pt (hlevel-proof-technique hlevel)))
        (er-let* ((nlabel (cond (skipp (value label))
               ((eq label '>) (value '>))
               ((equal (de-propagate e1) (de-propagate e2)) (value '>=))
               (t (er-let* ((result (pprogn (increment-timer 'other-time state)
                        (ccg-io? build/refine
                          nil
                          state
                          (u1 u2)
                          (fms "We attempt to prove that, under the given ~
                                   conditions, it is the case that the ~
                                   context measure ~x0 is always greater than ~
                                   ~x1.~|"
                            `((#\0 . ,U1) (#\1 . ,U2))
                            *standard-co*
                            state
                            nil))
                        (increment-timer 'print-time state)
                        (ccmf->-value? hyps e1 e2 pt qspv state))))
                   (cond (result (value '>))
                     ((eq label '>=) (value '>=))
                     (t (er-let* ((result (pprogn (increment-timer 'other-time state)
                              (ccg-io? build/refine
                                nil
                                state
                                (u1 u2)
                                (fms "Since the previous query failed, ~
                                           we attempt to prove that, under ~
                                           the given conditions,  it is the ~
                                           case that the context measure ~x0 ~
                                           is never less than ~x1.~|"
                                  `((#\0 . ,U1) (#\1 . ,U2))
                                  *standard-co*
                                  state
                                  nil))
                              (increment-timer 'print-time state)
                              (ccmf->=-value? hyps e1 e2 pt qspv state))))
                         (value (if result
                             '>=
                             nil))))))))))
          (progn (case nlabel
              (> (setf (ccmf-node->-edges node)
                  (cons j (ccmf-node->-edges node))))
              (>= (setf (ccmf-node->=-edges node)
                  (cons j (ccmf-node->=-edges node)))))
            (accg-refine-ccmf2 i
              (1- j)
              matrix
              node
              e1
              hyps
              f1
              c1
              f2
              ccms2
              cformals
              args
              redop
              (if (eq nlabel label)
                changes
                (cons `(,NLABEL ,U1 ,U2) changes))
              old-hlevel
              hlevel
              qspv
              state)))))))

(defun-raw accg-refine-ccmf1
  (i matrix
    ccmf
    hyps
    f1
    ccms1
    c1
    f2
    ccms2
    cformals
    args
    redop
    changes
    old-hlevel
    hlevel
    qspv
    state)
  (if (< i 0)
    (value (cond ((endp changes) changes)
        ((endp (cdr changes)) (car changes))
        (t (cons 'and changes))))
    (er-let* ((changes0 (accg-refine-ccmf2 i
           (1- (ccmf-out-sizes ccmf))
           matrix
           (aref (ccmf-graph ccmf) i)
           (aref ccms1 i)
           hyps
           f1
           c1
           f2
           ccms2
           cformals
           args
           redop
           changes
           old-hlevel
           hlevel
           qspv
           state)))
      (accg-refine-ccmf1 (1- i)
        matrix
        ccmf
        hyps
        f1
        ccms1
        c1
        f2
        ccms2
        cformals
        args
        redop
        changes0
        old-hlevel
        hlevel
        qspv
        state))))

(defun-raw accg-refine-ccmf
  (ccmf hyps
    f1
    ccms1
    c1
    f2
    ccms2
    cformals
    args
    redop
    old-hlevel
    hlevel
    qspv
    state)
  (let ((matrix (accg-ccmf-adj-matrix ccmf)))
    (loop for
      node
      across
      (ccmf-graph ccmf)
      do
      (setf (ccmf-node->-edges node) nil)
      do
      (setf (ccmf-node->=-edges node) nil))
    (accg-refine-ccmf1 (1- (ccmf-in-sizes ccmf))
      matrix
      ccmf
      hyps
      f1
      ccms1
      c1
      f2
      ccms2
      cformals
      args
      redop
      nil
      old-hlevel
      hlevel
      qspv
      state)))

(defun-raw accg-node-refine-ccmfs-per-edge
  (edges node1
    accg
    ccms1
    c1
    ruler1
    cformals
    args
    stronger-proofsp
    changes
    old-hlevel
    hlevel
    qspv
    state)
  (if (endp edges)
    (value changes)
    (let* ((edge (car edges)) (node2 (aref accg (accg-edge-head edge)))
        (ccms2 (accg-node-ccms node2))
        (ruler2 (subcor-var-lst cformals args (accg-node-ruler node2)))
        (wrld (access query-spec-var qspv :wrld)))
      (pprogn (increment-timer 'other-time state)
        (ccg-io? build/refine
          nil
          state
          (node1 ruler1 wrld node2)
          (fms "We use theorem prover queries to discen how the context ~
                      measures change when execution moves from call ~x0 in ~
                      function ~x1 under the ruler ~x2 to call ~x3 in ~
                      function ~x4 under the ruler ~x5.~|"
            `((#\0 . ,(ACCG-NODE-CALL NODE1)) (#\1 . ,(ACCG-NODE-FN NODE1))
              (#\2 . ,(UNTRANSLATE-LST RULER1 NIL WRLD))
              (#\3 . ,(ACCG-NODE-CALL NODE2))
              (#\4 . ,(ACCG-NODE-FN NODE2))
              (#\5 . ,(UNTRANSLATE-LST (ACCG-NODE-RULER NODE2) NIL WRLD)))
            *standard-co*
            state
            nil))
        (increment-timer 'print-time state)
        (er-let* ((nchanges (accg-refine-ccmf (accg-edge-ccmf edge)
               (append ruler1 ruler2)
               (accg-node-fn node1)
               ccms1
               c1
               (accg-node-fn node2)
               ccms2
               cformals
               args
               stronger-proofsp
               old-hlevel
               hlevel
               qspv
               state)))
          (accg-node-refine-ccmfs-per-edge (cdr edges)
            node1
            accg
            ccms1
            c1
            ruler1
            cformals
            args
            stronger-proofsp
            (if (null nchanges)
              changes
              (acons (cons (car (accg-node-context-num node1))
                  (car (accg-node-context-num node2)))
                nchanges
                changes))
            old-hlevel
            hlevel
            qspv
            state))))))

(defun-raw accg-refine-ccmfs1
  (i accg
    stronger-proofsp
    changes
    old-hlevel
    hlevel
    qspv
    state)
  (if (< i 0)
    (value changes)
    (let* ((node1 (aref accg i)) (ccms1 (accg-node-ccms node1))
        (c1 (accg-node-context-num node1))
        (ruler1 (accg-node-ruler node1))
        (cformals (accg-node-callformals node1))
        (args (fargs (accg-node-call node1)))
        (wrld (access query-spec-var qspv :wrld)))
      (er-let* ((changes0 (if (hlevel-ccmfs-per-nodep hlevel)
             (pprogn (ccg-io? build/refine
                 nil
                 state
                 (c1 ruler1 wrld)
                 (fms "We use theorem prover queries to discern how our ~
                             context mesaures change when execution moves ~
                             across call ~x0 in function ~x1 under the ruler ~
                             ~x2.~|"
                   `((#\0 . ,(ACCG-NODE-CALL NODE1)) (#\1 . ,(ACCG-NODE-FN NODE1))
                     (#\2 . ,(UNTRANSLATE-LST RULER1 NIL WRLD)))
                   *standard-co*
                   state
                   nil))
               (er-let* ((edge1 (value (car (accg-node-fwd-edges node1)))) (node2 (value (aref accg (accg-edge-head edge1))))
                   (ccmf (value (accg-edge-ccmf (car (accg-node-fwd-edges node1)))))
                   (nchanges (accg-refine-ccmf ccmf
                       ruler1
                       (accg-node-fn node1)
                       ccms1
                       c1
                       (accg-node-fn node2)
                       (accg-node-ccms node2)
                       cformals
                       args
                       stronger-proofsp
                       old-hlevel
                       hlevel
                       qspv
                       state))
                   (ngraph (value (ccmf-graph ccmf))))
                 (loop for
                   edge
                   in
                   (cdr (accg-node-fwd-edges node1))
                   for
                   occmf
                   =
                   (accg-edge-ccmf edge)
                   do
                   (setf (ccmf-graph occmf) (accg-copy-ccmf-graph ngraph))
                   finally
                   (return (value (if (null nchanges)
                         changes
                         (acons (car (accg-node-context-num node1)) nchanges changes)))))))
             (accg-node-refine-ccmfs-per-edge (accg-node-fwd-edges node1)
               node1
               accg
               ccms1
               c1
               ruler1
               cformals
               args
               stronger-proofsp
               changes
               old-hlevel
               hlevel
               qspv
               state))))
        (accg-refine-ccmfs1 (1- i)
          accg
          stronger-proofsp
          changes0
          old-hlevel
          hlevel
          qspv
          state)))))

(defun-raw accg-refine-ccmfs
  (accg stronger-proofsp old-hlevel hlevel qspv state)
  (accg-refine-ccmfs1 (1- (array-dimension accg 0))
    accg
    stronger-proofsp
    nil
    old-hlevel
    hlevel
    qspv
    state))

(defun-raw accg-refine-ccmfs-lst1
  (accgs caccgs
    uaccgs
    changes
    stronger-proofsp
    old-hlevel
    hlevel
    qspv
    state)
  (if (endp accgs)
    (value (list* changes caccgs uaccgs))
    (er-let* ((accg (value (car accgs))) (nchanges (accg-refine-ccmfs accg
            stronger-proofsp
            old-hlevel
            hlevel
            qspv
            state)))
      (accg-refine-ccmfs-lst1 (cdr accgs)
        (if (consp nchanges)
          (cons accg caccgs)
          caccgs)
        (if (consp nchanges)
          uaccgs
          (cons accg uaccgs))
        (append nchanges changes)
        stronger-proofsp
        old-hlevel
        hlevel
        qspv
        state))))

(defun-raw accg-refine-ccmfs-lst
  (accgs stronger-proofsp old-hlevel hlevel qspv state)
  (accg-refine-ccmfs-lst1 accgs
    nil
    nil
    nil
    stronger-proofsp
    old-hlevel
    hlevel
    qspv
    state))

(defun-raw prune-accg-node
  (node1 edges accg changes hlevel qspv state)
  (if (endp edges)
    (value changes)
    (let* ((edge (car edges)) (node2 (aref accg (accg-edge-head edge))))
      (er-let* ((result (pprogn (increment-timer 'other-time state)
             (ccg-io? build/refine
               nil
               state
               (node1 node2)
               (fms "We attempt to prove that it is not possible for ~
                         execution to move from context ~x0 to context ~x1.~|"
                 `((#\0 . ,(CAR (ACCG-NODE-CONTEXT-NUM NODE1))) (#\1 . ,(CAR (ACCG-NODE-CONTEXT-NUM NODE2))))
                 *standard-co*
                 state
                 nil))
             (increment-timer 'print-time state)
             (accg-can-omit-edge? node1 node2 hlevel qspv state))))
        (progn (unless result
            (setf (accg-node-fwd-edges node1)
              (cons edge (accg-node-fwd-edges node1)))
            (setf (accg-node-bwd-edges node2)
              (cons edge (accg-node-bwd-edges node2))))
          (prune-accg-node node1
            (cdr edges)
            accg
            (if result
              (acons (car (accg-node-context-num node1))
                (car (accg-node-context-num node2))
                changes)
              changes)
            hlevel
            qspv
            state))))))

(defun-raw prune-accg1
  (i accg changes hlevel qspv state)
  (if (< i 0)
    (value changes)
    (let* ((node (aref accg i)) (edges (accg-node-fwd-edges node)))
      (setf (accg-node-fwd-edges node) nil)
      (er-let* ((nchanges (prune-accg-node node edges accg changes hlevel qspv state)))
        (prune-accg1 (1- i) accg nchanges hlevel qspv state)))))

(defun-raw prune-accg
  (accg hlevel qspv state)
  (loop for
    node
    across
    accg
    do
    (setf (accg-node-bwd-edges node) nil))
  (pprogn (ccg-io? build/refine
      nil
      state
      nil
      (fms "We attempt to prune the CCG by using theorem prover queries ~
                  to determine if the rulers of adjacent calling contexts are ~
                  incompatible.~|"
        nil
        *standard-co*
        state
        nil))
    (prune-accg1 (1- (array-dimension accg 0))
      accg
      nil
      hlevel
      qspv
      state)))

(defun-raw accg-refine-accg
  (accg stronger-proofsp old-hlevel hlevel qspv state)
  (er-let* ((accg-changes0 (if (and stronger-proofsp (not (hlevel-ccmfs-per-nodep hlevel)))
         (prune-accg accg hlevel qspv state)
         (value nil))))
    (if (consp accg-changes0)
      (mv-let (accg-changes1 naccgs)
        (accg-separate-sccs accg :ccmfp t)
        (er-let* ((triple (accg-refine-ccmfs-lst naccgs
               stronger-proofsp
               old-hlevel
               hlevel
               qspv
               state)))
          (value (cons (cons (append accg-changes0 accg-changes1) (car triple))
              naccgs))))
      (er-let* ((changes0 (accg-refine-ccmfs accg
             stronger-proofsp
             old-hlevel
             hlevel
             qspv
             state)))
        (value (cons (cons nil changes0) (list accg)))))))

(defun-raw accg-refine-accgs1
  (accgs ces
    changes
    caccgs
    uaccgs
    uces
    stronger-proofsp
    old-hlevel
    new-hlevel
    qspv
    state)
  (if (endp accgs)
    (value (list* changes caccgs uaccgs uces))
    (er-let* ((pair (accg-refine-accg (car accgs)
           stronger-proofsp
           old-hlevel
           new-hlevel
           qspv
           state)))
      (if (or (consp (caar pair)) (consp (cdar pair)))
        (accg-refine-accgs1 (cdr accgs)
          (cdr ces)
          (cons (append (caar pair) (car changes))
            (append (cdar pair) (cdr changes)))
          (append (cdr pair) caccgs)
          uaccgs
          uces
          stronger-proofsp
          old-hlevel
          new-hlevel
          qspv
          state)
        (accg-refine-accgs1 (cdr accgs)
          (cdr ces)
          changes
          caccgs
          (append (cdr pair) uaccgs)
          (cons (car ces) uces)
          stronger-proofsp
          old-hlevel
          new-hlevel
          qspv
          state)))))

(defun-raw accg-refine-accgs
  (accgs ces old-hlevel new-hlevel qspv state)
  (pprogn (ccg-io? basics
      nil
      state
      (new-hlevel accgs)
      (fms "We now move to the ~x0 level of the hierarchy ~
                  (see :DOC CCG-hierarchy) in order to refine the remaining ~
                  SCC~#1~[~/s~] of our anotated CCG.~|"
        `((#\0 . ,NEW-HLEVEL) (#\1 . ,ACCGS))
        *standard-co*
        state
        nil))
    (er-let* ((tuple (accg-refine-accgs1 accgs
           ces
           nil
           nil
           nil
           nil
           (weaker-proof-techniquesp old-hlevel new-hlevel)
           old-hlevel
           new-hlevel
           qspv
           state)) (changes (value (car tuple)))
        (caccgs (value (cadr tuple)))
        (uaccgs (value (caddr tuple)))
        (uces (value (cdddr tuple))))
      (pprogn (ccg-io? basics
          nil
          state
          (changes state)
          (mv-let (col state)
            (fmt "We have completed CCG refinement. "
              nil
              *standard-co*
              state
              nil)
            (print-changes col changes state)))
        (value (list* caccgs uaccgs uces))))))

(defun-raw srg-scc
  (graph)
  (ccg-generic-scc graph
    (function srg-node-fwd-edges)
    (function srg-node-bwd-edges)
    (function srg-edge-tail)
    (function srg-edge-head)))

(defun-raw srg-scc-has->-edgep
  (scc scc-array srg)
  (let ((scc-num (aref scc-array (car scc))))
    (dolist (p scc nil)
      (let ((x (aref srg p)))
        (when (dolist (e (srg-node-fwd-edges x) nil)
            (when (and (eq (srg-edge-label e) '>)
                (= scc-num (aref scc-array (srg-edge-head e))))
              (return t)))
          (return t))))))

(defun-raw ccmf-remove-ccms
  (ccmf first-del-array last-del-array)
  (loop with
    graph
    =
    (ccmf-graph ccmf)
    for
    i
    from
    0
    below
    (ccmf-in-sizes ccmf)
    for
    node
    =
    (aref graph i)
    for
    f
    =
    (lambda (x) (aref last-del-array x))
    if
    (aref first-del-array i)
    do
    (setf (aref graph i) (make-ccmf-node))
    else
    do
    (setf (aref graph i)
      (make-ccmf-node :>-edges (delete-if f (ccmf-node->-edges node))
        :>=-edges (delete-if f (ccmf-node->=-edges node))))))

(defun-raw ccmf-remove-ccms-list
  (ccmfs deletep-array)
  (dolist (ccmf ccmfs nil)
    (ccmf-remove-ccms ccmf
      (aref deletep-array (ccmf-firstsite ccmf))
      (aref deletep-array (ccmf-lastsite ccmf)))))

(defun-raw srg-restrict
  (srg ccms)
  (let* ((n (length ccms)) (rsrg (make-array n))
      (a (make-array (array-dimension srg 0)
          :element-type 'fixnum
          :initial-element -1)))
    (loop for
      p
      in
      ccms
      for
      i
      from
      0
      for
      node
      =
      (aref srg p)
      do
      (setf (aref a p) i)
      do
      (setf (aref rsrg i)
        (make-srg-node :node (srg-node-node node)
          :ccm (srg-node-ccm node))))
    (loop for
      p
      in
      ccms
      for
      i
      from
      0
      for
      node
      =
      (aref srg p)
      for
      nnode
      =
      (aref rsrg i)
      do
      (loop for
        e
        in
        (srg-node-fwd-edges node)
        unless
        (= (aref a (srg-edge-head e)) -1)
        do
        (let* ((head (aref a (srg-edge-head e))) (hnode (aref rsrg head))
            (ne (make-srg-edge :head head
                :tail i
                :ccmf (srg-edge-ccmf e)
                :label (srg-edge-label e))))
          (setf (srg-node-fwd-edges nnode)
            (cons ne (srg-node-fwd-edges nnode)))
          (setf (srg-node-bwd-edges hnode)
            (cons ne (srg-node-bwd-edges hnode))))))
    rsrg))

(defun-raw srg-scc-for-node-aux
  (srg nn visited node-fwd-edges edge-head)
  (setf (aref visited nn) t)
  (loop for
    edge
    in
    (funcall node-fwd-edges (aref srg nn))
    for
    head
    =
    (funcall edge-head edge)
    unless
    (aref visited head)
    do
    (srg-scc-for-node-aux srg
      head
      visited
      node-fwd-edges
      edge-head)))

(defun-raw srg-scc-for-node
  (srg nn)
  (let* ((n (array-dimension srg 0)) (in-scc-array (make-array n
          :element-type '(member t nil :ignore)
          :initial-element nil)))
    (let* ((n (array-dimension in-scc-array 0)))
      (srg-scc-for-node-aux srg
        nn
        in-scc-array
        (function srg-node-fwd-edges)
        (function srg-edge-head))
      (loop for
        i
        from
        0
        below
        n
        if
        (aref in-scc-array i)
        do
        (setf (aref in-scc-array i) nil)
        else
        do
        (setf (aref in-scc-array i) :ignore))
      (srg-scc-for-node-aux srg
        nn
        in-scc-array
        (function srg-node-bwd-edges)
        (function srg-edge-tail))
      (loop for
        i
        from
        0
        below
        n
        when
        (eq (aref in-scc-array i) :ignore)
        do
        (setf (aref in-scc-array i) nil))
      in-scc-array)))

(defun-raw srg-add-scc-for-node
  (srg nn in-scc-array)
  (if (aref in-scc-array nn)
    in-scc-array
    (let ((new-in-scc-array (srg-scc-for-node srg nn)))
      (loop for
        i
        from
        0
        below
        (length in-scc-array)
        when
        (and (not (aref in-scc-array i)) (aref new-in-scc-array i))
        do
        (setf (aref in-scc-array i) t))
      in-scc-array)))

(defun-raw mtp
  (srg ccmfs
    num-contexts
    fwd-edges
    bwd-edges
    edge-head
    edge-tail)
  (let* ((n (array-dimension srg 0)) (count (make-array `(,N ,NUM-CONTEXTS)
          :element-type 'fixnum
          :initial-element 0))
      (accg-matrix (make-array `(,NUM-CONTEXTS ,NUM-CONTEXTS)
          :element-type 'boolean
          :initial-element nil))
      (marked (make-array n :element-type 'boolean :initial-element nil))
      (worklist nil))
    (dolist (ccmf ccmfs)
      (setf (aref accg-matrix
          (ccmf-firstsite ccmf)
          (ccmf-lastsite ccmf))
        t))
    (dotimes (i n)
      (let ((node (aref srg i)))
        (dolist (e (funcall fwd-edges node))
          (incf (aref count
              i
              (srg-node-node (aref srg (funcall edge-head e))))))
        (dotimes (j num-contexts)
          (when (and (aref accg-matrix (srg-node-node node) j)
              (= (aref count i j) 0))
            (setf worklist (cons i worklist))
            (setf (aref marked i) t)))))
    (loop while
      (consp worklist)
      for
      cw
      =
      (car worklist)
      for
      j
      =
      (srg-node-node (aref srg cw))
      do
      (setf worklist (cdr worklist))
      do
      (dolist (e (funcall bwd-edges (aref srg cw)))
        (let ((i (funcall edge-tail e)))
          (unless (aref marked i)
            (decf (aref count i j))
            (when (= (aref count i j) 0)
              (setf (aref marked i) t)
              (setf worklist (cons i worklist))))))
      finally
      (return (loop for
          i
          from
          0
          below
          n
          unless
          (aref marked i)
          collect
          i)))))

(defun-raw mtp-fwd
  (srg ccmfs num-contexts)
  (mtp srg
    ccmfs
    num-contexts
    (function srg-node-fwd-edges)
    (function srg-node-bwd-edges)
    (function srg-edge-head)
    (function srg-edge-tail)))

(defun-raw mtp-bwd
  (srg ccmfs num-contexts)
  (mtp srg
    ccmfs
    num-contexts
    (function srg-node-bwd-edges)
    (function srg-node-fwd-edges)
    (function srg-edge-tail)
    (function srg-edge-head)))

(defun-raw fan-free
  (srg edge-list other-node num-contexts)
  (loop with
    n
    =
    (array-dimension srg 0)
    with
    seen
    =
    (make-array num-contexts
      :element-type 'boolean
      :initial-element nil)
    for
    i
    from
    0
    below
    n
    unless
    (loop for
      e
      in
      (funcall edge-list (aref srg i))
      for
      j
      =
      (funcall other-node e)
      for
      context
      =
      (srg-node-node (aref srg j))
      if
      (aref seen context)
      return
      nil
      else
      do
      (setf (aref seen context) t)
      finally
      (return t))
    return
    nil
    do
    (loop for
      i
      from
      0
      below
      num-contexts
      do
      (setf (aref seen i) nil))
    finally
    (return t)))

(defun-raw fan-in-free
  (srg num-contexts)
  (fan-free srg
    (function srg-node-bwd-edges)
    (function srg-edge-tail)
    num-contexts))

(defun-raw fan-out-free
  (srg num-contexts)
  (fan-free srg
    (function srg-node-fwd-edges)
    (function srg-edge-head)
    num-contexts))

(defun-raw mtp-to-anchor
  (srg ahash)
  (loop for
    i
    from
    0
    below
    (array-dimension srg 0)
    do
    (loop for
      e
      in
      (srg-node-fwd-edges (aref srg i))
      when
      (and (eq (srg-edge-label e) '>)
        (not (gethash (srg-edge-ccmf e) ahash)))
      do
      (setf (gethash (srg-edge-ccmf e) ahash) t))
    finally
    (return ahash)))

(defun-raw simple-anchors
  (srg ahash ccmfs num-contexts)
  (let ((srgp (srg-restrict srg (mtp-fwd srg ccmfs num-contexts))))
    (if (fan-in-free srgp num-contexts)
      (mtp-to-anchor srgp ahash)
      (let ((srgq (srg-restrict srg (mtp-bwd srg ccmfs num-contexts))))
        (if (fan-out-free srgq num-contexts)
          (mtp-to-anchor srgq ahash)
          nil)))))

(defun-raw srg-restrict-edges
  (srg pred)
  (loop with
    n
    =
    (array-dimension srg 0)
    with
    rsrg
    =
    (make-array n)
    for
    i
    from
    0
    below
    n
    for
    node
    =
    (aref srg i)
    do
    (setf (aref rsrg i)
      (make-srg-node :node (srg-node-node node)
        :ccm (srg-node-ccm node)
        :fwd-edges (remove-if-not pred (srg-node-fwd-edges node))
        :bwd-edges (remove-if-not pred (srg-node-bwd-edges node))))
    finally
    (return rsrg)))

(defun-raw ndg
  (srg)
  (srg-restrict-edges srg
    (lambda (e) (eq (srg-edge-label e) '>=))))

(defun-raw srg-interior
  (srg)
  (multiple-value-bind (scc scc-array)
    (srg-scc srg)
    (declare (ignore scc))
    (srg-restrict-edges srg
      (lambda (e)
        (eq (aref scc-array (srg-edge-tail e))
          (aref scc-array (srg-edge-head e)))))))

(defun-raw srg-to-matrix
  (srg)
  (loop with
    n
    =
    (array-dimension srg 0)
    with
    matrix
    =
    (make-array (list n n)
      :element-type 'boolean
      :initial-element nil)
    for
    i
    from
    0
    below
    n
    do
    (loop for
      e
      in
      (srg-node-fwd-edges (aref srg i))
      do
      (setf (aref matrix i (srg-edge-head e)) t))
    finally
    (return matrix)))

(defun-raw ccmf-to-ccmfdown-in-srg
  (srg ccmf ndgi-matrix)
  (srg-restrict-edges srg
    (lambda (e)
      (not (and (eq (srg-node-node (aref srg (srg-edge-tail e)))
            (ccmf-firstsite ccmf))
          (eq (srg-node-node (aref srg (srg-edge-head e)))
            (ccmf-lastsite ccmf))
          (aref ndgi-matrix (srg-edge-tail e) (srg-edge-head e)))))))

(defun-raw anchor-find
  (srg ccmfs num-contexts)
  (let ((ahash (make-hash-table :rehash-size 2
         :rehash-threshold (float 3/4))))
    (multiple-value-bind (sccs scc-array)
      (srg-scc srg)
      (declare (ignore scc-array))
      (dolist (scc sccs)
        (simple-anchors (srg-restrict srg scc)
          ahash
          ccmfs
          num-contexts))
      (let ((anchors (loop for
             k
             being
             the
             hash-keys
             of
             ahash
             using
             (hash-value v)
             when
             v
             collect
             k)))
        (if anchors
          anchors
          (loop with
            ndgi-matrix
            =
            (srg-to-matrix (srg-interior (ndg srg)))
            for
            ccmf
            in
            ccmfs
            for
            h
            =
            (ccmf-to-ccmfdown-in-srg srg ccmf ndgi-matrix)
            when
            (or (mtp-fwd h ccmfs num-contexts)
              (mtp-bwd h ccmfs num-contexts))
            return
            (list ccmf)))))))

(defun-raw copy-a-ccmf
  (ccmf)
  (make-ccmf :firstsite (ccmf-firstsite ccmf)
    :lastsite (ccmf-lastsite ccmf)
    :fc-num (ccmf-fc-num ccmf)
    :lc-num (ccmf-lc-num ccmf)
    :graph (accg-copy-ccmf-graph (ccmf-graph ccmf))
    :in-sizes (ccmf-in-sizes ccmf)
    :out-sizes (ccmf-out-sizes ccmf)
    :steps (ccmf-steps ccmf)))

(defun-raw copy-ccmfs
  (ccmfs)
  (loop for
    ccmf
    in
    ccmfs
    collect
    (copy-a-ccmf ccmf)))

(defun-raw copy-accg
  (accg)
  (let* ((n (array-dimension accg 0)) (naccg (make-array n)))
    (loop for
      i
      from
      0
      below
      n
      for
      node
      =
      (aref accg i)
      do
      (setf (aref naccg i)
        (make-accg-node :context (accg-node-context node) :num i)))
    (loop for
      node
      across
      accg
      for
      nnode
      across
      naccg
      do
      (setf (accg-node-fwd-edges nnode)
        (loop for
          edge
          in
          (accg-node-fwd-edges node)
          for
          head
          =
          (accg-edge-head edge)
          for
          hnode
          =
          (aref naccg head)
          for
          nedge
          =
          (make-accg-edge :tail (accg-edge-tail edge)
            :head head
            :ccmf (copy-a-ccmf (accg-edge-ccmf edge)))
          do
          (setf (accg-node-bwd-edges hnode)
            (cons nedge (accg-node-bwd-edges hnode)))
          collect
          nedge)))
    naccg))

(defun-raw accg-ccmfs
  (accg)
  (loop for
    node
    across
    accg
    append
    (mapcar (function accg-edge-ccmf) (accg-node-fwd-edges node))))

(defun-raw accg-contexts
  (accg)
  (map 'vector (lambda (x) (accg-node-context x)) accg))

(defun-raw accg-srg-add-edge
  (tailnode headnode tailnum headnum ccmf label)
  (let ((edge (make-srg-edge :tail tailnum
         :head headnum
         :ccmf ccmf
         :label label)))
    (setf (srg-node-fwd-edges tailnode)
      (cons edge (srg-node-fwd-edges tailnode)))
    (setf (srg-node-bwd-edges headnode)
      (cons edge (srg-node-bwd-edges headnode)))
    nil))

(defun-raw accg-remove-edges-corresponding-to-ccmfs
  (accg ccmfs)
  (loop for
    ccmf
    in
    ccmfs
    do
    (setf (ccmf-firstsite ccmf) -1))
  (loop with
    pred
    =
    (lambda (edge)
      (= (ccmf-firstsite (accg-edge-ccmf edge)) -1))
    for
    node
    across
    accg
    do
    (setf (accg-node-fwd-edges node)
      (delete-if pred (accg-node-fwd-edges node)))
    do
    (setf (accg-node-bwd-edges node)
      (delete-if pred (accg-node-bwd-edges node))))
  accg)

(defun-raw accg-construct-srg
  (accg)
  (let* ((n (array-dimension accg 0)) (node-offset (make-array n :element-type 'fixnum :initial-element 0))
      (c 0))
    (dotimes (i n)
      (setf (aref node-offset i) c)
      (incf c (array-dimension (accg-node-ccms (aref accg i)) 0)))
    (let ((srg (make-array c
           :element-type 'srg-node
           :initial-element (make-srg-node))))
      (loop for
        i
        from
        1
        below
        c
        do
        (setf (aref srg i) (make-srg-node)))
      (loop for
        i
        from
        0
        below
        n
        do
        (loop for
          edge
          in
          (accg-node-fwd-edges (aref accg i))
          for
          ccmf
          =
          (accg-edge-ccmf edge)
          for
          offset1
          =
          (aref node-offset i)
          for
          offset2
          =
          (aref node-offset (accg-edge-head edge))
          for
          cg
          =
          (ccmf-graph ccmf)
          do
          (loop for
            j
            from
            0
            below
            (array-dimension cg 0)
            for
            a
            from
            offset1
            for
            nodea
            =
            (aref srg a)
            do
            (setf (srg-node-node nodea) i)
            do
            (setf (srg-node-ccm nodea) j)
            do
            (loop for
              x
              in
              (ccmf-node->-edges (aref cg j))
              for
              b
              =
              (+ offset2 x)
              do
              (accg-srg-add-edge nodea (aref srg b) a b ccmf '>))
            do
            (loop for
              x
              in
              (ccmf-node->=-edges (aref cg j))
              for
              b
              =
              (+ offset2 x)
              do
              (accg-srg-add-edge nodea (aref srg b) a b ccmf '>=))))
        finally
        (return srg)))))

(defun-raw cln-accg
  (accg)
  (let* ((srg (accg-construct-srg accg)) (n (array-dimension accg 0))
      (deletep-array (make-array n)))
    (dotimes (i n)
      (setf (aref deletep-array i)
        (make-array (array-dimension (accg-node-ccms (aref accg i)) 0)
          :element-type 'boolean
          :initial-element nil)))
    (multiple-value-bind (sccs scc-array)
      (srg-scc srg)
      (loop for
        scc
        in
        sccs
        unless
        (srg-scc-has->-edgep scc scc-array srg)
        do
        (loop for
          v
          in
          scc
          for
          node
          =
          (aref srg v)
          for
          context
          =
          (srg-node-node node)
          for
          ccm
          =
          (srg-node-ccm node)
          do
          (setf (aref (aref deletep-array context) ccm) t))))
    (progn (ccmf-remove-ccms-list (accg-ccmfs accg) deletep-array)
      accg)))

(defun-raw scp
  (accg)
  (when accg
    (let* ((n (array-dimension accg 0)) (anchors (anchor-find (accg-construct-srg accg) (accg-ccmfs accg) n)))
      (when anchors
        (mv-let (changes sccs)
          (accg-separate-sccs (accg-remove-edges-corresponding-to-ccmfs accg anchors))
          (declare (ignore changes))
          (loop for
            scc
            in
            sccs
            unless
            (scp (cln-accg scc))
            return
            nil
            finally
            (return t)))))))

(defstruct-raw scg-path
  (start 0 :type fixnum)
  (end 0 :type fixnum)
  (length 0 :type fixnum)
  (interior nil :type (or null fixnum cons)))

(defun-raw new-scg-path
  (start end)
  (make-scg-path :start start
    :end end
    :length 2
    :interior nil))

(defun-raw compose-scg-paths
  (p1 p2)
  (make-scg-path :start (scg-path-start p1)
    :end (scg-path-end p2)
    :length (1- (+ (scg-path-length p1) (scg-path-length p2)))
    :interior (let ((x (if (null (scg-path-interior p2))
           (scg-path-start p2)
           (cons (scg-path-start p2) (scg-path-interior p2)))))
      (if (null (scg-path-interior p1))
        x
        (cons (scg-path-interior p1) x)))))

(defun-raw flatten-scg-interior
  (interior acc)
  (cond ((null interior) acc)
    ((atom interior) (cons interior acc))
    (t (flatten-scg-interior (car interior)
        (flatten-scg-interior (cdr interior) acc)))))

(defun-raw flatten-scg-path
  (path)
  (cons (scg-path-start path)
    (flatten-scg-interior (scg-path-interior path)
      (list (scg-path-end path)))))

(defun-raw scg-path-equal
  (p1 p2)
  (and (= (scg-path-start p1) (scg-path-start p2))
    (= (scg-path-end p1) (scg-path-end p2))))

(defun-raw path<
  (p1 p2)
  (or (< (scg-path-start p1) (scg-path-start p2))
    (and (= (scg-path-start p1) (scg-path-start p2))
      (< (scg-path-end p1) (scg-path-end p2)))))

(defun-raw shortest-scg-path
  (p1 p2)
  (if (<= (scg-path-length p1) (scg-path-length p2))
    p1
    p2))

(defstruct-raw scg
  (paths nil :type list)
  (newest-paths nil :type list)
  (new-newest-paths nil :type list)
  (num 0 :type fixnum)
  (graph nil))

(defun-raw sorted-set-union1
  (lst1 lst2 key1 key2 predicate combine key test)
  (cond ((funcall test key1 key2) (cons (car lst1)
        (sorted-set-union (cdr lst1)
          (cdr lst2)
          predicate
          :key key
          :combine combine
          :test test)))
    ((funcall predicate key1 key2) (cons (car lst1)
        (if (endp (cdr lst1))
          lst2
          (sorted-set-union1 (cdr lst1)
            lst2
            (funcall key (cadr lst1))
            key2
            predicate
            combine
            key
            test))))
    (t (cons (car lst2)
        (if (endp (cdr lst2))
          lst1
          (sorted-set-union1 lst1
            (cdr lst2)
            key1
            (funcall key (cadr lst2))
            predicate
            combine
            key
            test))))))

(defun-raw sorted-set-union
  (lst1 lst2
    predicate
    &key
    (key (function identity))
    (combine (function (lambda (x y) (declare (ignore y)) x)))
    (test (function equal)))
  (cond ((endp lst1) lst2)
    ((endp lst2) lst1)
    (t (sorted-set-union1 lst1
        lst2
        (funcall key (car lst1))
        (funcall key (car lst2))
        predicate
        combine
        key
        test))))

(defun-raw sorted-set-difference1
  (lst1 lst2 key1 key2 predicate key test)
  (cond ((funcall test key1 key2) (sorted-set-difference (cdr lst1)
        (cdr lst2)
        predicate
        :key key
        :test test))
    ((funcall predicate key1 key2) (cons (car lst1)
        (if (endp (cdr lst1))
          nil
          (sorted-set-difference1 (cdr lst1)
            lst2
            (funcall key (cadr lst1))
            key2
            predicate
            key
            test))))
    (t (if (endp (cdr lst2))
        lst1
        (sorted-set-difference1 lst1
          (cdr lst2)
          key1
          (funcall key (cadr lst2))
          predicate
          key
          test)))))

(defun-raw sorted-set-difference
  (lst1 lst2 predicate &key (key (function identity)) (test (function equal)))
  (cond ((endp lst1) nil)
    ((endp lst2) lst1)
    (t (sorted-set-difference1 lst1
        lst2
        (funcall key (car lst1))
        (funcall key (car lst2))
        predicate
        key
        test))))

(defun-raw sorted-union/difference1
  (lst1 lst2 key1 key2 predicate combine key test)
  (cond ((funcall test key1 key2) (mv-let (union difference)
        (sorted-union/difference (cdr lst1)
          (cdr lst2)
          predicate
          :combine combine
          :key key
          :test test)
        (mv (cons (funcall combine (car lst1) (car lst2)) union)
          difference)))
    ((funcall predicate key1 key2) (mv-let (union difference)
        (if (endp (cdr lst1))
          (mv lst2 nil)
          (sorted-union/difference1 (cdr lst1)
            lst2
            (funcall key (cadr lst1))
            key2
            predicate
            combine
            key
            test))
        (mv (cons (car lst1) union) (cons (car lst1) difference))))
    (t (mv-let (union difference)
        (if (endp (cdr lst2))
          (mv lst1 lst1)
          (sorted-union/difference1 lst1
            (cdr lst2)
            key1
            (funcall key (cadr lst2))
            predicate
            combine
            key
            test))
        (mv (cons (car lst2) union) difference)))))

(defun-raw sorted-union/difference
  (lst1 lst2
    predicate
    &key
    (key (function identity))
    (combine (function (lambda (x y) (declare (ignore y)) x)))
    (test (function equal)))
  (cond ((endp lst1) (mv lst2 nil))
    ((endp lst2) (mv lst1 lst1))
    (t (sorted-union/difference1 lst1
        lst2
        (funcall key (car lst1))
        (funcall key (car lst2))
        predicate
        combine
        key
        test))))

(defun-raw sorted-adjoin
  (element set
    predicate
    &key
    (key (function identity))
    (combine (function (lambda (x y) (declare (ignore y)) x)))
    (test (function equal)))
  (sorted-set-union (list element)
    set
    predicate
    :key key
    :combine combine
    :test test))

(defun-raw sorted-remove-duplicates1
  (lst carkey key combine test)
  (if (endp (cdr lst))
    lst
    (let ((cadrkey (funcall key (cadr lst))))
      (if (funcall test carkey cadrkey)
        (let ((comb (funcall combine (car lst) (cadr lst))))
          (sorted-remove-duplicates1 (cons comb (cddr lst))
            (funcall key comb)
            key
            combine
            test))
        (cons (car lst)
          (sorted-remove-duplicates1 (cdr lst)
            cadrkey
            key
            combine
            test))))))

(defun-raw sorted-remove-duplicates
  (lst &key
    (key (function identity))
    (combine (function (lambda (x y) (declare (ignore y)) x)))
    (test (function equal)))
  (cond ((endp lst) nil)
    ((endp (cdr lst)) lst)
    (t (sorted-remove-duplicates1 lst
        (funcall key (car lst))
        key
        combine
        test))))

(defun-raw list-to-sorted-set
  (lst predicate
    &key
    (key (function identity))
    (combine (function (lambda (x y) (declare (ignore y)) x)))
    (test (function equal)))
  (sorted-remove-duplicates (sort lst predicate :key key)
    :key key
    :combine combine
    :test test))

(defun-raw scg-graph-key (graph) graph)

(defun-raw update-scg-paths
  (graph paths i graph-hash)
  (let* ((key (scg-graph-key graph)) (scg (gethash key graph-hash)))
    (if scg
      (let* ((new-newest-paths (scg-new-newest-paths scg)) (npaths (sorted-set-difference (sorted-set-difference paths
                (scg-paths scg)
                (function path<)
                :test (function scg-path-equal))
              (scg-newest-paths scg)
              (function path<)
              :test (function scg-path-equal))))
        (mv-let (union difference)
          (sorted-union/difference npaths
            new-newest-paths
            (function path<)
            :test (function scg-path-equal)
            :combine (function shortest-scg-path))
          (progn (setf (scg-new-newest-paths scg) union)
            (mv i (endp new-newest-paths) difference scg))))
      (let ((nscg (make-scg :graph graph :num i :new-newest-paths paths)))
        (setf (gethash key graph-hash) nscg)
        (mv (1+ i) t paths nscg)))))

(defun-raw age-scgs
  (lst)
  (loop for
    scg
    in
    lst
    do
    (setf (scg-paths scg)
      (sorted-set-union (scg-paths scg)
        (scg-newest-paths scg)
        (function path<)
        :combine (function shortest-scg-path)
        :test (function scg-path-equal)))
    do
    (setf (scg-newest-paths scg) (scg-new-newest-paths scg))
    do
    (setf (scg-new-newest-paths scg) nil)
    finally
    (return lst)))

(defun-raw ccmfs-to-scgs1
  (ccmfs graph-hash i acc)
  (if (endp ccmfs)
    (mv i (sort acc (function <) :key (function scg-num)))
    (let ((ccmf (car ccmfs)))
      (mv-let (ni new? diff scg)
        (update-scg-paths (ccmf-graph ccmf)
          (list (new-scg-path (ccmf-firstsite ccmf) (ccmf-lastsite ccmf)))
          i
          graph-hash)
        (ccmfs-to-scgs1 (cdr ccmfs)
          graph-hash
          ni
          (if (and new? (consp diff))
            (cons scg acc)
            acc))))))

(defun-raw ccmfs-to-scgs
  (ccmfs graph-hash)
  (ccmfs-to-scgs1 ccmfs graph-hash 0 nil))

(defun-raw compose-scg-graphs
  (g h)
  (loop with
    n
    =
    (array-dimension g 0)
    with
    gh
    =
    (make-array (array-dimension g 0)
      :element-type 'ccmf-node
      :initial-element (make-ccmf-node))
    for
    i
    below
    n
    for
    nodei
    =
    (aref g i)
    for
    >-edges
    =
    nil
    for
    >=-edges
    =
    nil
    do
    (loop for
      j
      in
      (ccmf-node->-edges nodei)
      for
      nodej
      =
      (aref h j)
      do
      (loop for
        k
        in
        (ccmf-node->-edges nodej)
        do
        (setf >-edges (cons k >-edges)))
      do
      (loop for
        k
        in
        (ccmf-node->=-edges nodej)
        do
        (setf >-edges (cons k >-edges))))
    do
    (loop for
      j
      in
      (ccmf-node->=-edges nodei)
      for
      nodej
      =
      (aref h j)
      do
      (loop for
        k
        in
        (ccmf-node->-edges nodej)
        do
        (setf >-edges (cons k >-edges)))
      do
      (loop for
        k
        in
        (ccmf-node->=-edges nodej)
        do
        (setf >=-edges (cons k >=-edges))))
    do
    (let* ((sorted->-edges (list-to-sorted-set >-edges (function <))))
      (setf (aref gh i)
        (make-ccmf-node :>-edges sorted->-edges
          :>=-edges (sorted-set-difference (list-to-sorted-set >=-edges (function <))
            sorted->-edges
            (function <)))))
    finally
    (return gh)))

(defun-raw compose-scg-path-lsts1
  (gpath hpaths acc)
  (if (or (endp hpaths)
      (not (= (scg-path-start (car hpaths)) (scg-path-end gpath))))
    acc
    (compose-scg-path-lsts1 gpath
      (cdr hpaths)
      (cons (compose-scg-paths gpath (car hpaths)) acc))))

(defun-raw compose-scg-path-lsts
  (gpaths hpaths acc)
  (cond ((or (endp gpaths) (endp hpaths)) (list-to-sorted-set acc
        (function path<)
        :test (function scg-path-equal)
        :combine (function shortest-scg-path)))
    ((< (scg-path-end (car gpaths))
       (scg-path-start (car hpaths))) (compose-scg-path-lsts (cdr gpaths) hpaths acc))
    ((> (scg-path-end (car gpaths))
       (scg-path-start (car hpaths))) (compose-scg-path-lsts gpaths (cdr hpaths) acc))
    (t (compose-scg-path-lsts (cdr gpaths)
        hpaths
        (compose-scg-path-lsts1 (car gpaths) hpaths acc)))))

(defun-raw scg-counter-example?
  (scg diff)
  (and (loop for
      path
      in
      diff
      when
      (= (scg-path-start path) (scg-path-end path))
      return
      t
      finally
      (return nil))
    (loop for
      path
      in
      (append (scg-paths scg)
        (scg-newest-paths scg)
        (sorted-set-difference (scg-new-newest-paths scg)
          diff
          (function path<)
          :test (function scg-path-equal)))
      when
      (= (scg-path-start path) (scg-path-end path))
      return
      nil
      finally
      (return t))
    (loop with
      graph
      =
      (scg-graph scg)
      for
      i
      from
      0
      below
      (array-dimension graph 0)
      when
      (member i (ccmf-node->-edges (aref graph i)))
      return
      nil
      finally
      (return t))
    (let ((graph (scg-graph scg)))
      (equalp (compose-scg-graphs graph graph) graph))))

(defun-raw shortest-self-loop
  (paths path)
  (cond ((endp paths) path)
    ((= (scg-path-start (car paths)) (scg-path-end (car paths))) (shortest-self-loop (cdr paths)
        (if (or (null path)
            (< (scg-path-length (car paths)) (scg-path-length path)))
          (car paths)
          path)))
    (t (shortest-self-loop (cdr paths) path))))

(defun-raw compose-scgs
  (g h i graph-hash)
  (let ((ghgraph (compose-scg-graphs (scg-graph g) (scg-graph h))) (ghpaths (compose-scg-path-lsts (sort (copy-list (scg-newest-paths g))
            (function <)
            :key (function scg-path-end))
          (scg-newest-paths h)
          nil)))
    (mv-let (ni new? diff gh)
      (update-scg-paths ghgraph ghpaths i graph-hash)
      (if (scg-counter-example? gh diff)
        (mv t
          ni
          (cons (scg-graph gh)
            (flatten-scg-path (shortest-self-loop diff nil))))
        (mv nil
          ni
          (if (and new? (consp diff))
            gh
            nil))))))

(defun-raw scg-predecessors
  (scg)
  (sorted-remove-duplicates (mapcar (function scg-path-start) (scg-newest-paths scg))))

(defun-raw scg-successors
  (scg)
  (list-to-sorted-set (mapcar (function scg-path-end) (scg-newest-paths scg))
    (function <)))

(defun-raw organize-scgs-by-preds1
  (scgs array)
  (if (endp scgs)
    nil
    (let ((scg (car scgs)))
      (organize-scgs-by-preds1 (cdr scgs) array)
      (loop for
        i
        in
        (scg-predecessors scg)
        do
        (setf (aref array i) (cons scg (aref array i)))))))

(defun-raw organize-scgs-by-preds
  (scgs numsites)
  (let ((array (make-array numsites
         :initial-element nil
         :element-type 'list)))
    (organize-scgs-by-preds1 scgs array)
    array))

(defun-raw union-scgs
  (scg-array indices)
  (loop for
    i
    in
    indices
    append
    (aref scg-array i)
    into
    union
    finally
    (return (list-to-sorted-set union (function <) :key (function scg-num)))))

(defun-raw copy-scgs
  (scgs)
  (loop for
    scg
    in
    scgs
    collect
    (make-scg :graph (scg-graph scg)
      :num (scg-num scg)
      :paths (scg-paths scg)
      :newest-paths (scg-newest-paths scg)
      :new-newest-paths (scg-new-newest-paths scg))))

(defun-raw print-sct-total-report
  (success? comps graph-hash start-time state)
  (mv-let (col state)
    (ccg-io? size-change
      nil
      (mv col state)
      (success?)
      (fmt "~%SCT has found ~#0~[no~/a~] counter-example to ~
                  termination. "
        (list (cons #\0
            (if success?
              0
              1)))
        *standard-co*
        state
        nil)
      :default-bindings ((col 0)))
    (mv-let (col state)
      (ccg-io? performance
        nil
        (mv col state)
        (comps graph-hash start-time internal-time-units-per-second)
        (fmt1 "In the process, ~x0 total ~#1~[compositions ~
                    were~/composition was~] performed and ~x2 unique ~
                    ~#3~[graphs were~/graph was~] created. Total time taken ~
                    was ~x4 seconds.~|"
          (list (cons #\0 comps)
            (cons #\1
              (if (= comps 1)
                1
                0))
            (cons #\2 (hash-table-count graph-hash))
            (cons #\3
              (if (= (hash-table-count graph-hash) 1)
                1
                0))
            (cons #\4
              (/ (- (get-internal-run-time) start-time)
                (coerce internal-time-units-per-second 'float))))
          col
          *standard-co*
          state
          nil)
        :default-bindings ((col 0)))
      (mv-let (col state)
        (ccg-io? size-change
          nil
          (mv col state)
          nil
          (fmt1 "~|" nil col *standard-co* state nil))
        (declare (ignore col))
        state))))

(defun-raw sct
  (ccmfs numsites state)
  (let ((graph-hash (make-hash-table :test 'equalp)) (start-time (get-internal-run-time)))
    (mv-let (i newest)
      (ccmfs-to-scgs ccmfs graph-hash)
      (progn (loop for
          scg
          in
          newest
          for
          nnp
          =
          (scg-new-newest-paths scg)
          when
          (scg-counter-example? scg nnp)
          do
          (return-from sct
            (value (cons (scg-graph scg)
                (flatten-scg-path (shortest-self-loop nnp nil))))))
        (age-scgs newest)
        (loop with
          total-comps
          =
          0
          with
          generators
          =
          (organize-scgs-by-preds (copy-scgs newest) numsites)
          until
          (endp newest)
          for
          iteration
          from
          0
          for
          new-newest
          =
          nil
          for
          comps
          =
          0
          do
          (loop for
            g
            in
            newest
            for
            gsucc
            =
            (scg-successors g)
            do
            (loop for
              h
              in
              (union-scgs generators gsucc)
              do
              (mv-let (counter-example? ni gh)
                (compose-scgs g h i graph-hash)
                (progn (incf comps)
                  (incf total-comps)
                  (setf i ni)
                  (cond (counter-example? (pprogn (increment-timer 'other-time state)
                        (print-sct-loop-report iteration comps state)
                        (print-sct-total-report nil
                          total-comps
                          graph-hash
                          start-time
                          state)
                        (increment-timer 'print-time state)
                        (return-from sct (value gh))))
                    (gh (setf new-newest (cons gh new-newest))))))))
          do
          (age-scgs (list-to-sorted-set (append newest (copy-list new-newest))
              (function <)
              :key (function scg-num)))
          do
          (setf newest new-newest)
          do
          (pprogn (increment-timer 'other-time state)
            (print-sct-loop-report iteration comps state)
            (increment-timer 'print-time state))
          finally
          (pprogn (increment-timer 'other-time state)
            (print-sct-total-report t
              total-comps
              graph-hash
              start-time
              state)
            (increment-timer 'print-time state)
            (return (value nil))))))))

(defun-raw find-funct
  (fn functs)
  (cond ((endp functs) (make-funct :fn fn))
    ((eq fn (funct-fn (car functs))) (car functs))
    (t (find-funct fn (cdr functs)))))

(defun-raw t-machine-to-contexts
  (t-machine parent-funct functs)
  (if (endp t-machine)
    nil
    (let* ((tac (car t-machine)) (call (access tests-and-call tac :call)))
      (cons (make-context :ruler (access tests-and-call tac :tests)
          :call call
          :parent-funct parent-funct
          :call-funct (find-funct (ffn-symb call) functs))
        (t-machine-to-contexts (cdr t-machine) parent-funct functs)))))

(defun-raw t-machines-to-contexts1
  (t-machines functs all-functs)
  (if (endp t-machines)
    nil
    (cons (t-machine-to-contexts (car t-machines)
        (car functs)
        all-functs)
      (t-machines-to-contexts1 (cdr t-machines)
        (cdr functs)
        all-functs))))

(defun-raw t-machines-to-contexts
  (t-machines functs)
  (t-machines-to-contexts1 t-machines functs functs))

(defun-raw make-funct-structs
  (names arglists)
  (if (endp names)
    nil
    (cons (make-funct :fn (car names) :formals (car arglists))
      (make-funct-structs (cdr names) (cdr arglists)))))

(defun-raw context-array
  (contexts)
  (let ((carray (coerce (loop for
           cs
           in
           contexts
           append
           cs)
         'vector)))
    (loop for
      i
      from
      0
      below
      (length carray)
      do
      (setf (context-num (aref carray i)) (list i)))
    carray))

(defun-raw accg-scp-list
  (lst proved unproved)
  (if (endp lst)
    (mv proved unproved)
    (let* ((accg (cln-accg (copy-accg (car lst)))))
      (cond ((scp (copy-accg accg)) (accg-scp-list (cdr lst) (cons accg proved) unproved))
        (t (accg-scp-list (cdr lst) proved (cons (car lst) unproved)))))))

(defun-raw accg-sct-list1
  (lst i n proved unproved ces state)
  (if (endp lst)
    (pprogn (let ((plen (len proved)))
        (ccg-io? basics
          nil
          state
          (plen unproved)
          (fms "Size-change analysis has proven ~x0 out of ~x1 SCCs of ~
                       the CCG terminating.~|"
            `((#\0 . ,PLEN) (#\1 . ,(+ PLEN (LEN UNPROVED))))
            *standard-co*
            state
            nil)))
      (value (list* proved unproved ces)))
    (pprogn (increment-timer 'other-time state)
      (ccg-io? size-change
        nil
        state
        nil
        (fms "We now begin size change analysis on the ~n0 SCC out of ~
                    ~n1."
          (list (cons #\0 `(,I)) (cons #\1 n))
          *standard-co*
          state
          nil))
      (increment-timer 'print-time state)
      (let* ((accg (cln-accg (copy-accg (car lst)))))
        (if (null accg)
          (pprogn (increment-timer 'other-time state)
            (ccg-io? size-change
              nil
              state
              nil
              (fms "A trivial analysis has revealed that this SCC is ~
                           potentially non-terminating. We will set it aside ~
                           for further refinement.~|"
                nil
                *standard-co*
                state
                nil))
            (increment-timer 'print-time state)
            (accg-sct-list1 (cdr lst)
              (1+ i)
              n
              proved
              (cons (car lst) unproved)
              (cons nil ces)
              state))
          (er-let* ((ce (sct (accg-ccmfs accg) (array-dimension accg 0) state)))
            (if (null ce)
              (pprogn (increment-timer 'other-time state)
                (ccg-io? size-change
                  nil
                  state
                  nil
                  (fms "We have shown this SCC to be terminating, so we ~
                              do not need to refine it any further.~|"
                    nil
                    *standard-co*
                    state
                    nil))
                (increment-timer 'print-time state)
                (accg-sct-list1 (cdr lst)
                  (1+ i)
                  n
                  (cons accg proved)
                  unproved
                  ces
                  state))
              (pprogn (increment-timer 'other-time state)
                (ccg-io? size-change
                  nil
                  state
                  nil
                  (fms "This SCC is potentially non-terminating. We will ~
                            set it aside for further refinement.~|"
                    nil
                    *standard-co*
                    state
                    nil))
                (increment-timer 'print-time state)
                (accg-sct-list1 (cdr lst)
                  (1+ i)
                  n
                  proved
                  (cons (car lst) unproved)
                  (cons ce ces)
                  state)))))))))

(defun-raw accg-sct-list
  (lst proved unproved ces state)
  (accg-sct-list1 lst 1 (len lst) proved unproved ces state))

(defun-raw aref-lst
  (array lst)
  (mapcar (function (lambda (x) (aref array x))) lst))

(defun-raw alist-add-eq
  (alist key val)
  (cond ((endp alist) (acons key (list val) nil))
    ((eq (caar alist) key) (acons key (cons val (cdar alist)) (cdr alist)))
    (t (cons (car alist) (alist-add-eq (cdr alist) key val)))))

(defun-raw order-names-arglists
  (names arglists rv-alist)
  (let* ((na-arrays (coerce (mapcar (lambda (x y) (coerce (cons x y) 'vector))
           names
           arglists)
         'vector)) (maxsize (loop for
          v
          across
          na-arrays
          maximize
          (array-dimension v 0))))
    (loop for
      i
      from
      1
      below
      maxsize
      append
      (loop for
        array
        across
        na-arrays
        when
        (and (< i (array-dimension array 0))
          (not (member-eq (aref array i)
              (cdr (assoc (aref array 0) rv-alist)))))
        collect
        (cons (aref array 0) (aref array i))))))

(defmacro-raw ccmf-tail-fn
  (ccmf contexts)
  `(context-fn (aref ,CONTEXTS (car (ccmf-fc-num ,CCMF)))))

(defmacro-raw ccmf-head-fn
  (ccmf contexts)
  `(context-fn (aref ,CONTEXTS (car (ccmf-lc-num ,CCMF)))))

(defun-raw restrict-ccmf
  (ccmf ccmr1 ccmr2)
  (let* ((graph (ccmf-graph ccmf)) (n (array-dimension graph 0))
      (ngraph (make-array n
          :element-type 'ccmf-node
          :initial-element (make-ccmf-node)))
      (nccmf (make-ccmf :firstsite (ccmf-firstsite ccmf)
          :lastsite (ccmf-lastsite ccmf)
          :fc-num (ccmf-fc-num ccmf)
          :lc-num (ccmf-lc-num ccmf)
          :in-sizes (ccmf-in-sizes ccmf)
          :out-sizes (ccmf-out-sizes ccmf)
          :graph ngraph))
      (f (lambda (x) (aref ccmr2 x))))
    (loop for
      i
      from
      0
      below
      n
      for
      node
      =
      (aref graph i)
      if
      (aref ccmr1 i)
      do
      (setf (aref ngraph i)
        (make-ccmf-node :>-edges (remove-if-not f (ccmf-node->-edges node))
          :>=-edges (remove-if-not f (ccmf-node->=-edges node))))
      else
      do
      (setf (aref ngraph i) (make-ccmf-node)))
    (loop for
      node
      across
      ngraph
      when
      (or (consp (ccmf-node->-edges node))
        (consp (ccmf-node->=-edges node)))
      return
      nccmf
      finally
      (return nil))))

(defun-raw can-solve-restricted-accgs?
  (accgs ccmrs scp? state)
  (loop for
    accg
    in
    accgs
    for
    n
    =
    (array-dimension accg 0)
    for
    naccg
    =
    (make-array n)
    do
    (loop for
      i
      from
      0
      below
      n
      for
      node
      =
      (aref accg i)
      do
      (setf (aref naccg i)
        (make-accg-node :context (accg-node-context node) :num i)))
    do
    (loop for
      i
      from
      0
      below
      n
      for
      node
      =
      (aref accg i)
      for
      nnode1
      =
      (aref naccg i)
      for
      ccmr1
      =
      (aref ccmrs (car (accg-node-context-num node)))
      do
      (loop for
        edge
        in
        (accg-node-fwd-edges node)
        for
        ccmf
        =
        (accg-edge-ccmf edge)
        for
        ccmr2
        =
        (aref ccmrs (accg-edge-head edge))
        for
        nnode2
        =
        (aref naccg (accg-edge-head edge))
        for
        nccmf
        =
        (restrict-ccmf ccmf ccmr1 ccmr2)
        if
        nccmf
        do
        (let ((nedge (make-accg-edge :head (accg-edge-head edge)
               :tail (accg-edge-tail edge)
               :ccmf nccmf)))
          (setf (accg-node-fwd-edges nnode1)
            (cons nedge (accg-node-fwd-edges nnode1)))
          (setf (accg-node-bwd-edges nnode2)
            (cons nedge (accg-node-bwd-edges nnode2))))
        else
        do
        (return-from can-solve-restricted-accgs? (value nil))))
    do
    (if scp?
      (unless (scp (cln-accg naccg)) (return (value nil)))
      (er-let* ((caccg (value (cln-accg naccg))) (ce (if (null caccg)
              (value t)
              (sct (accg-ccmfs caccg) n state))))
        (unless (null ce) (return (value nil)))))
    finally
    (return (value t))))

(defun-raw create-ccm-restrictions
  (contexts av-alist)
  (loop with
    n
    =
    (array-dimension contexts 0)
    with
    ccmrs
    =
    (make-array n)
    for
    i
    from
    0
    below
    n
    for
    context
    =
    (aref contexts i)
    for
    ccms
    =
    (context-ccms context)
    for
    vars
    =
    (cdr (assoc (context-fn context) av-alist))
    for
    m
    =
    (array-dimension ccms 0)
    for
    ccmri
    =
    (make-array m :element-type 'boolean :initial-element nil)
    do
    (setf (aref ccmrs i) ccmri)
    do
    (loop for
      j
      from
      0
      below
      m
      do
      (setf (aref ccmri j)
        (subsetp (all-vars (aref ccms j)) vars)))
    finally
    (return ccmrs)))

(defun-raw ruler-vars
  (names contexts)
  (loop with
    rv-alist
    =
    (pairlis$ names nil)
    for
    context
    across
    contexts
    for
    fn
    =
    (context-fn context)
    for
    vars
    =
    (all-vars1-lst (context-ruler context) nil)
    for
    pair
    =
    (assoc fn rv-alist)
    do
    (setf (cdr pair) (union-eq vars (cdr pair)))
    finally
    (return rv-alist)))

(defun-raw cgma-aux
  (nalist proved-scp proved-sct contexts av-alist i state)
  (cond ((zp i) (let ((ccmrs (create-ccm-restrictions contexts av-alist)))
        (er-let* ((p1 (can-solve-restricted-accgs? proved-scp ccmrs t state)) (p2 (if p1
                (can-solve-restricted-accgs? proved-sct ccmrs nil state)
                (value nil))))
          (if p2
            (value av-alist)
            (value nil)))))
    ((endp nalist) (value nil))
    (t (er-let* ((nav-alist (cgma-aux (cdr nalist)
             proved-scp
             proved-sct
             contexts
             (alist-add-eq av-alist (caar nalist) (cdar nalist))
             (1- i)
             state)))
        (if nav-alist
          (value nav-alist)
          (cgma-aux (cdr nalist)
            proved-scp
            proved-sct
            contexts
            av-alist
            i
            state))))))

(defun-raw ccg-generate-measure-alist1
  (i nalist proved-scp proved-sct contexts rv-alist state)
  (er-let* ((av-alist (cgma-aux nalist
         proved-scp
         proved-sct
         contexts
         rv-alist
         i
         state)))
    (if av-alist
      (value (mapcar (lambda (x) (cons (car x) (cons :? (cdr x))))
          av-alist))
      (ccg-generate-measure-alist1 (1+ i)
        nalist
        proved-scp
        proved-sct
        contexts
        rv-alist
        state))))

(defun-raw ccg-generate-measure-alist
  (proved-scp proved-sct names arglists contexts cpn state)
  (let* ((rv-alist (if cpn
         (pairlis$ names nil)
         (ruler-vars names contexts))) (nalist (order-names-arglists names arglists rv-alist)))
    (ccg-generate-measure-alist1 0
      nalist
      proved-scp
      proved-sct
      contexts
      rv-alist
      state)))

(defun-raw name-var-pairs1
  (name arglist rst)
  (if (endp arglist)
    rst
    (acons name
      (car arglist)
      (name-var-pairs1 name (cdr arglist) rst))))

(defun-raw name-var-pairs
  (functs rv-alist)
  (if (endp functs)
    (mv nil nil)
    (mv-let (free fixed)
      (name-var-pairs (cdr functs) rv-alist)
      (let* ((funct (car functs)) (fn (funct-fn funct))
          (rv (cdr (assoc fn rv-alist))))
        (mv (name-var-pairs1 fn
            (set-difference-eq (funct-formals funct) rv)
            free)
          (name-var-pairs1 fn rv fixed))))))

(defun-raw get-ccm-vars1
  (i ccms ccm-vars)
  (cond ((< i 0) ccm-vars)
    (t (setf (aref ccm-vars i) (all-vars (aref ccms i)))
      (get-ccm-vars1 (1- i) ccms ccm-vars))))

(defun-raw get-ccm-vars
  (ccms)
  (let ((len (array-dimension ccms 0)))
    (get-ccm-vars1 (1- len)
      ccms
      (make-array len :element-type 'list :initial-element nil))))

(defun-raw fn-ccm-vars-alist
  (functs)
  (if (endp functs)
    nil
    (let ((funct (car functs)))
      (acons (funct-fn funct)
        (get-ccm-vars (funct-ccms funct))
        (fn-ccm-vars-alist (cdr functs))))))

(defun-raw gather-relevant-ccms1
  (i var ccm-vars indices)
  (if (< i 0)
    indices
    (gather-relevant-ccms1 (1- i)
      var
      ccm-vars
      (if (member-eq var (aref ccm-vars i))
        (cons i indices)
        indices))))

(defun-raw gather-relevant-ccms
  (var ccm-vars)
  (gather-relevant-ccms1 (1- (array-dimension ccm-vars 0))
    var
    ccm-vars
    nil))

(defun-raw gather-all-relevant-ccms1
  (avars alist)
  (if (endp avars)
    nil
    (let* ((avar (car avars)) (fn (car avar)) (var (cdr avar)))
      (cons (gather-relevant-ccms var (cdr (assoc fn alist)))
        (gather-all-relevant-ccms1 (cdr avars) alist)))))

(defun-raw gather-all-relevant-ccms
  (avars functs)
  (gather-all-relevant-ccms1 avars (fn-ccm-vars-alist functs)))

(defun-raw ccmf-remove-relevant-edges1
  (i graph relevant-ccms1 relevant-ccms2 edges-alist)
  (cond ((<= (array-dimension graph 0) i) edges-alist)
    ((and (consp relevant-ccms1) (= i (car relevant-ccms1))) (let* ((node (aref graph i)) (>-edges-i (ccmf-node->-edges node))
          (>=-edges-i (ccmf-node->=-edges node)))
        (setf (ccmf-node->-edges node) nil)
        (setf (ccmf-node->=-edges node) nil)
        (ccmf-remove-relevant-edges1 (1+ i)
          graph
          (cdr relevant-ccms1)
          relevant-ccms2
          (if (and (endp >-edges-i) (endp >=-edges-i))
            edges-alist
            (acons i (cons >-edges-i >=-edges-i) edges-alist)))))
    ((consp relevant-ccms2) (let* ((node (aref graph i)) (>-edges-i (ccmf-node->-edges node))
          (>=-edges-i (ccmf-node->=-edges node)))
        (mv-let (>-diff >-intersect)
          (set-difference-and-intersection >-edges-i relevant-ccms2)
          (mv-let (>=-diff >=-intersect)
            (set-difference-and-intersection >=-edges-i relevant-ccms2)
            (progn (when (consp >-intersect)
                (setf (ccmf-node->-edges node) >-diff))
              (when (consp >=-intersect)
                (setf (ccmf-node->=-edges node) >=-diff))
              (ccmf-remove-relevant-edges1 (1+ i)
                graph
                relevant-ccms1
                relevant-ccms2
                (if (and (endp >-intersect) (endp >=-intersect))
                  edges-alist
                  (acons i (cons >-intersect >=-intersect) edges-alist))))))))
    (t (ccmf-remove-relevant-edges1 (1+ i)
        graph
        relevant-ccms1
        relevant-ccms2
        edges-alist))))

(defun-raw ccmf-remove-relevant-edges
  (ccmf relevant-ccms1 relevant-ccms2)
  (let ((graph (ccmf-graph ccmf)))
    (cons ccmf
      (ccmf-remove-relevant-edges1 0
        graph
        relevant-ccms1
        relevant-ccms2
        nil))))

(defun-raw ccmf-remove-relevant-edges-lst
  (ccmfs contexts fn relevant-ccms acc)
  (if (endp ccmfs)
    acc
    (let* ((ccmf (car ccmfs)) (tcontext (aref contexts (car (ccmf-fc-num ccmf))))
        (relevant-ccms1 (if (eq (context-fn tcontext) fn)
            relevant-ccms
            nil))
        (hcontext (aref contexts (car (ccmf-lc-num ccmf))))
        (relevant-ccms2 (if (eq (context-fn hcontext) fn)
            relevant-ccms
            nil)))
      (ccmf-remove-relevant-edges-lst (cdr ccmfs)
        contexts
        fn
        relevant-ccms
        (cons (ccmf-remove-relevant-edges ccmf
            relevant-ccms1
            relevant-ccms2)
          acc)))))

(defun-raw accg-remove-relevant-ccmf-edges1
  (i accg contexts fn relevant-ccms acc)
  (if (< i 0)
    acc
    (let* ((node (aref accg i)))
      (accg-remove-relevant-ccmf-edges1 (1- i)
        accg
        contexts
        fn
        relevant-ccms
        (if (eq (accg-node-fn node) fn)
          (let ((pred (lambda (edge)
                 (equal (accg-node-fn (aref accg (accg-edge-tail edge))) fn))))
            (ccmf-remove-relevant-edges-lst (append (mapcar (function accg-edge-ccmf) (accg-node-fwd-edges node))
                (mapcar (function accg-edge-ccmf)
                  (remove-if pred (accg-node-bwd-edges node))))
              contexts
              fn
              relevant-ccms
              acc))
          acc)))))

(defun-raw accg-remove-relevant-ccmf-edges
  (accg contexts fn relevant-ccms)
  (accg-remove-relevant-ccmf-edges1 (1- (array-dimension accg 0))
    accg
    contexts
    fn
    relevant-ccms
    nil))

(defun-raw accg-remove-relevant-ccmf-edges-lst-tail
  (accgs contexts fn relevant-ccms acc)
  (if (endp accgs)
    acc
    (accg-remove-relevant-ccmf-edges-lst-tail (cdr accgs)
      contexts
      fn
      relevant-ccms
      (accg-remove-relevant-ccmf-edges1 (1- (array-dimension (car accgs) 0))
        (car accgs)
        contexts
        fn
        relevant-ccms
        acc))))

(defun-raw accg-remove-relevant-ccmf-edges-lst
  (accgs contexts fn relevant-ccms)
  (accg-remove-relevant-ccmf-edges-lst-tail accgs
    contexts
    fn
    relevant-ccms
    nil))

(defun-raw restore-edges1
  (ccmf alist)
  (if (endp alist)
    nil
    (let* ((entry (car alist)) (i (car entry))
        (>-edges (cadr entry))
        (>=-edges (cddr entry))
        (node (aref (ccmf-graph ccmf) i)))
      (setf (ccmf-node->-edges node)
        (merge 'list >-edges (ccmf-node->-edges node) (function <)))
      (setf (ccmf-node->=-edges node)
        (merge 'list >=-edges (ccmf-node->=-edges node) (function <)))
      (restore-edges1 ccmf (cdr alist)))))

(defun-raw restore-edges
  (alist)
  (if (endp alist)
    nil
    (progn (restore-edges1 (caar alist) (cdar alist))
      (restore-edges (cdr alist)))))

(defun-raw can-scp-lstp
  (accgs)
  (or (endp accgs)
    (and (scp (cln-accg (copy-accg (car accgs))))
      (can-scp-lstp (cdr accgs)))))

(defun-raw can-sct-lstp
  (accgs state)
  (if (endp accgs)
    (value t)
    (let ((naccg (cln-accg (copy-accg (car accgs)))))
      (if (null naccg)
        (value nil)
        (er-let* ((ce (sct (accg-ccmfs naccg) (array-dimension naccg 0) state)))
          (if (null ce)
            (can-sct-lstp (cdr accgs) state)
            (value nil)))))))

(defun-raw all-termination1
  (proved-scp proved-sct
    contexts
    avars
    relevant-edges
    subsets
    state)
  (cond ((member-equal 'nil subsets) (value 'nil))
    ((endp avars) (value '(nil)))
    (t (let* ((avar (car avars)) (fn (car avar))
          (re-info (accg-remove-relevant-ccmf-edges-lst-tail proved-sct
              contexts
              fn
              (car relevant-edges)
              (accg-remove-relevant-ccmf-edges-lst proved-scp
                contexts
                fn
                (car relevant-edges)))))
        (er-let* ((p (can-sct-lstp proved-sct state)) (nsubsets (if (and p (can-scp-lstp proved-scp))
                (all-termination1 proved-scp
                  proved-sct
                  contexts
                  (cdr avars)
                  (cdr relevant-edges)
                  (remove-covered-subsets avar subsets)
                  state)
                (value 'nil))))
          (progn (restore-edges re-info)
            (er-let* ((nnsubsets (all-termination1 proved-scp
                   proved-sct
                   contexts
                   (cdr avars)
                   (cdr relevant-edges)
                   (append nsubsets (remove-avar-from-subsets avar subsets))
                   state)))
              (value (append nsubsets (add-avar-to-subsets avar nnsubsets))))))))))

(defun-raw funct-fns-lst
  (functs)
  (if (endp functs)
    nil
    (cons (funct-fn (car functs)) (cdr functs))))

(defun-raw all-termination
  (proved-scp proved-sct contexts functs cpn state)
  (if (and (endp proved-scp) (endp proved-sct))
    (value '(nil))
    (let ((names (funct-fns-lst functs)))
      (mv-let (free fixed)
        (name-var-pairs functs
          (if cpn
            (pairlis$ names nil)
            (ruler-vars names contexts)))
        (let ((relevant-ccms (gather-all-relevant-ccms free functs)))
          (er-let* ((at1 (all-termination1 proved-scp
                 proved-sct
                 contexts
                 free
                 relevant-ccms
                 nil
                 state)))
            (value (append-to-all fixed at1))))))))

(defun-raw ccm-o-p-clauses2
  (contexts term clauses)
  (if (endp contexts)
    clauses
    (ccm-o-p-clauses2 (cdr contexts)
      term
      (conjoin-clause-to-clause-set (add-literal term
          (dumb-negate-lit-lst (context-ruler (car contexts)))
          t)
        clauses))))

(defun-raw ccm-o-p-clauses1
  (contexts ccm-list clauses)
  (if (endp ccm-list)
    clauses
    (ccm-o-p-clauses1 contexts
      (cdr ccm-list)
      (ccm-o-p-clauses2 contexts
        (mcons-term* 'o-p (car ccm-list))
        clauses))))

(defun-raw ccm-o-p-clauses0
  (contexts ccm-list clauses)
  (cond ((endp contexts) clauses)
    ((eq (car ccm-list) *0*) (ccm-o-p-clauses0 (cdr contexts) (cdr ccm-list) clauses))
    (t (ccm-o-p-clauses0 (cdr contexts)
        (cdr ccm-list)
        (ccm-o-p-clauses1 (car contexts) (car ccm-list) clauses)))))

(defun-raw ccm-o-p-clauses
  (contexts ccm-list)
  (ccm-o-p-clauses0 contexts ccm-list nil))

(defun-raw ccg-intermediate-step
  (accgs ces new-hlevel old-hlevel proved qspv state)
  (er-let* ((triple (accg-refine-accgs accgs
         ces
         old-hlevel
         new-hlevel
         qspv
         state)) (caccgs (value (car triple)))
      (uaccgs (value (cadr triple)))
      (uces (value (cddr triple))))
    (cond ((endp caccgs) (pprogn (ccg-io? basics
            nil
            state
            nil
            (fms "Since we have no new information, we skip size ~
                           change analysis and attempt to further refine the ~
                           SCCs.~|"
              nil
              *standard-co*
              state
              nil))
          (value (list* proved uaccgs uces))))
      (t (pprogn (let ((clen (len caccgs)))
            (ccg-io? basics
              nil
              state
              (uaccgs clen caccgs)
              (fms "~@0 of the CCG ~#3~[was~/were~] altered. We ~
                              analyze ~#3~[it~/each of these~] with the size ~
                              change termination analysis.~@4~|"
                `((#\0 . ,(IF (CONSP UACCGS)
     "~N1 of the ~n2 SCCs"
     "~#3~[The sole SCC~/All the SCCs~]")) (#\1 . ,CLEN)
                  (#\2 . ,(+ CLEN (LEN UACCGS)))
                  (#\3 . ,CACCGS)
                  (#\4 . ,(IF (ENDP UACCGS)
     ""
     " The others will be set aside ~
                                               for further refinement.")))
                *standard-co*
                state
                nil)))
          (accg-sct-list caccgs proved uaccgs uces state))))))

(defun-raw ccg-measure-step
  (hlevel names
    t-machines
    measure-alist
    mp
    rel
    bodies
    verbose
    qspv
    state)
  (if (consp measure-alist)
    (let ((ctx (access query-spec-var qspv :ctx)) (wrld (access query-spec-var qspv :wrld))
        (ens (access query-spec-var qspv :ens))
        (stop-time (access query-spec-var qspv :stop-time))
        (otf-flg (access query-spec-var qspv :otf-flg))
        (pt (cadr hlevel)))
      (pprogn (ccg-io? basics
          nil
          state
          (hlevel)
          (fms "The current level of the CCG hierarchy is ~x0. We ~
                      therefore attempt a measure proof.~|"
            `((#\0 . hlevel))
            *standard-co*
            state
            nil))
        (mv-let (erp pair state)
          (er-let* ((hints (if (equal pt :built-in-clauses)
                 (translate-hints "Measure Built-in-clauses Hint"
                   '(("goal" :do-not '(eliminate-destructors eliminate-irrelevance
                        generalize
                        fertilize)
                      :in-theory (theory 'minimal-theory)
                      :do-not-induct :otf-flg-override))
                   ctx
                   wrld
                   state)
                 (value (translated-limit-induction-hint (cadr pt))))))
            (state-global-let* ((inhibit-output-lst (if verbose
                   (@ inhibit-output-lst)
                   (list* 'event 'error (@ inhibit-output-lst)))))
              (maybe-prover-before-stop-time stop-time
                ctx
                state
                (prove-termination names
                  t-machines
                  measure-alist
                  mp
                  rel
                  hints
                  otf-flg
                  bodies
                  nil
                  ctx
                  ens
                  wrld
                  state
                  (f-get-global 'accumulated-ttree state)))))
          (if erp
            (er-progn (time-check stop-time ctx state)
              (pprogn (ccg-io? basics
                  nil
                  state
                  nil
                  (fms "Since ACL2 has failed to prove the measure ~
                             conjecture, we continue with the hierarchical ~
                             analysis.~|"
                    nil
                    *standard-co*
                    state
                    nil))
                (value nil)))
            (pprogn (ccg-io? basics
                nil
                state
                nil
                (fms "ACL2 has succeeded in proving the measure ~
                          conjecture, thereby proving termination."
                  nil
                  *standard-co*
                  state
                  nil))
              (value (list* :measure (car pair) measure-alist (cdr pair))))))))
    (pprogn (ccg-io? basics
        nil
        state
        (hlevel)
        (fms "Skipping level ~x0 of the hierarchy due to previously ~
                    mentioned error when guessing measures."
          `((#\0 . hlevel))
          *standard-co*
          state
          nil))
      (value nil))))

(defun-raw ccg
  (accgs ces
    last-ccg-hlevel
    hierarchy
    proved
    context-array
    names
    arglists
    t-machines
    measure-alist
    mp
    rel
    bodies
    verbose
    qspv
    state)
  (cond ((endp accgs) (pprogn (increment-timer 'other-time state)
        (ccg-io? basics
          nil
          state
          nil
          (fms "We have successfully proven termination! We now weed ~
                         out irrelevant CCMs so that we can minimize the ~
                         measured-subset. This may require running the size ~
                         change analysis several more times.~|"
            nil
            *standard-co*
            state
            nil))
        (increment-timer 'print-time state)
        (er-let* ((ms (ccg-generate-measure-alist nil
               proved
               names
               arglists
               context-array
               (hlevel-ccmfs-per-nodep last-ccg-hlevel)
               state)))
          (pprogn (mv-let (col state)
              (io? event
                nil
                (mv col state)
                (names ms)
                (fmt "CCG analysis has succeeded in proving termination of ~
                        ~&0 using CCMs over the following variables~#0~[~/, ~
                        respectively~]: ~&1. Thus, we admit ~#0~[this ~
                        function~/these ~ functions~] under the principle of ~
                        definition."
                  (list (cons #\0 names) (cons #\1 (strip-cddrs ms)))
                  *standard-co*
                  state
                  nil)
                :default-bindings ((col 0)))
              (value (list* :ccg col ms (f-get-global 'accumulated-ttree state))))))))
    ((endp hierarchy) (pprogn (ccg-io? basics
          nil
          state
          nil
          (fms "We have completed all levels of the hierarchy, but ~
                         have failed to prove termination."
            nil
            *standard-co*
            state
            nil))
        (if (null (car ces))
          state
          (ccg-io? counter-example
            nil
            state
            nil
            (print-counter-example (car accgs)
              (car ces)
              context-array
              (access query-spec-var qspv :ctx)
              (access query-spec-var qspv :ens)
              (access query-spec-var qspv :wrld)
              state)))
        (mv t nil state)))
    ((eq (caar hierarchy) :measure) (er-let* ((tuple (ccg-measure-step (car hierarchy)
             names
             t-machines
             measure-alist
             mp
             rel
             bodies
             verbose
             qspv
             state)))
        (if tuple
          (value tuple)
          (ccg accgs
            ces
            last-ccg-hlevel
            (cdr hierarchy)
            proved
            context-array
            names
            arglists
            t-machines
            measure-alist
            mp
            rel
            bodies
            verbose
            qspv
            state))))
    (t (er-let* ((tuple (state-global-let* ((inhibit-output-lst (if verbose
                  (@ inhibit-output-lst)
                  (list* 'prove 'proof-tree (@ inhibit-output-lst)))))
             (ccg-intermediate-step accgs
               ces
               (car hierarchy)
               last-ccg-hlevel
               proved
               qspv
               state))) (nproved (value (car tuple)))
          (naccgs (value (cadr tuple)))
          (nces (value (cddr tuple))))
        (ccg naccgs
          nces
          (car hierarchy)
          (cdr hierarchy)
          nproved
          context-array
          names
          arglists
          t-machines
          measure-alist
          mp
          rel
          bodies
          verbose
          qspv
          state)))))

(defun-raw build-accgs
  (names contexts functs ccm-hints wrld state)
  (let* ((context-array (context-array contexts)) (accgs (build-and-annotate-accgs names
          functs
          contexts
          (pairlis$ names ccm-hints))))
    (pprogn (increment-timer 'other-time state)
      (ccg-io? basics
        nil
        state
        (names context-array accgs)
        (pprogn (fms "We begin with the Calling Context Graph (CCG), ~
                     containing the following contexts (if the output doesn't ~
                     make sense, see :DOC CCG and also the paper referenced ~
                     above):~|"
            nil
            *standard-co*
            state
            nil)
          (print-context-array1 0 names context-array state)
          (fms "and the following edges:~|"
            nil
            *standard-co*
            state
            nil)
          (print-accg-edges1 accgs state)
          (fms "We have annotated the CCG with the following calling ~
                     context measures (CCMs):~|"
            nil
            *standard-co*
            state
            nil)
          (print-funct-ccms functs wrld state)))
      (increment-timer 'print-time state)
      (pprogn (ccg-io? basics
          nil
          state
          nil
          (fms "Before we begin the hierarchical analysis, we run our ~
                     size-change analysis so we have a baseline for refinement."
            nil
            *standard-co*
            state
            nil))
        (er-let* ((tuple (accg-sct-list accgs nil nil nil state)))
          (value (cons context-array tuple)))))))

(defun-raw prove-termination-with-ccg
  (names functs
    contexts
    ruler-extenders-lst
    ccm-hints
    hierarchy
    verbose
    time-limit
    arglists
    measures
    t-machines
    mp
    rel
    otf-flg
    bodies
    ctx
    ens
    wrld
    state
    ttree)
  (let* ((ccms (mapcar (function cdr) ccm-hints)) (entry (find-?-ccm names ccms))
      (stop-time (if time-limit
          (+ (get-internal-run-time)
            (* internal-time-units-per-second time-limit))
          nil))
      (qspv (make query-spec-var
          :stop-time stop-time
          :mem (create-memoization (max-induction-depth hierarchy))
          :otf-flg otf-flg
          :ens ens
          :ctx ctx
          :wrld wrld)))
    (cond ((and entry (not (ld-skip-proofsp state))) (let ((fn (car entry)) (ccm (cdr entry)))
          (er soft
            ctx
            "A CCM of the form (:? v1 ... vk) is only legal when the defun is ~
             redundant (see :DOC redundant-events) or when skipping proofs ~
             (see :DOC ld-skip-proofsp).  The CCM ~x0 supplied for function ~
             symbol ~x1 is thus illegal."
            ccm
            fn)))
      ((null contexts) (mv-let (col state)
          (io? event
            nil
            (mv col state)
            (names)
            (fmt "Since ~&0 is non-recursive, its admission is trivial.  "
              (list (cons #\0 names))
              (proofs-co state)
              state
              nil)
            :default-bindings ((col 0)))
          (value (list* :ccg (or col 0) nil nil))))
      ((ld-skip-proofsp state) (let ((fns (fns-without-consider-only-ccms-hints names ccms)))
          (if (consp fns)
            (er soft
              ctx
              "Proofs cannot be skipped on a CCG termination proof unless ~
                 CCMs are defined for every function. You did not supply CCMs ~
                 for function~#0~[~/s~] ~&0. Therefore, proofs cannot be skipped."
              fns)
            (value (list* :ccg 0
                (pairlis$ names
                  (mapcar (lambda (x) `(:? ,@(ALL-VARS1-LST (CDR X) NIL)))
                    ccms))
                nil)))))
      (t (pprogn (ccg-io? basics
            nil
            state
            (names ruler-extenders-lst)
            (fms "Attempting to prove termination using Calling Context Graph ~
              (CCG) analysis. There are various ways in which users can ~
              control CCG analysis. See the :DOC CCG for details. This ~
              analysis is described in a 2006 CAV paper by Manolios and ~
              Vroon.~|~%The ruler-extenders for each function are as follows: ~
              ~*0~|"
              `((#\0 . ,(RULER-EXTENDER-PRINTOUT NAMES RULER-EXTENDERS-LST)))
              *standard-co*
              state
              nil))
          (simplify-contexts contexts ens wrld ctx state)
          (mv-let (o-p-clauses ttree)
            (clean-up-clause-set (ccm-o-p-clauses contexts ccms)
              ens
              wrld
              ttree
              state)
            (er-let* ((ttree (accumulate-ttree-and-step-limit-into-state ttree
                   :skip state)))
              (pprogn (increment-timer 'other-time state)
                (er-let* ((displayed-goal (value (prettyify-clause-set o-p-clauses
                         (let*-abstractionp state)
                         wrld))) (simp-phrase (value (tilde-*-simp-phrase ttree)))
                    (ttree1 (if o-p-clauses
                        (pprogn (io? event
                            nil
                            state
                            (ttree displayed-goal simp-phrase)
                            (fms "You have told us to consider CCMs that are not ~
                             trivially proved to be ordinals. ~
                             Therefore, the conjecture that we must prove ~
                             before we can continue with the CCG ~
                             analysis~#0~[~/, given ~*1,~] is ~
                             ~@2~%~%Goal~%~Q34."
                              `((#\0 . ,(IF (NTH 4 SIMP-PHRASE)
     1
     0)) (#\1 . ,SIMP-PHRASE)
                                (#\2 . ,(IF (TAGGED-OBJECTSP 'SR-LIMIT TTREE)
     " as follows (where the ~
                                           subsumption/replacement limit ~
                                           affected this analysis; see :DOC ~
                                           case-split-limitations)."
     ""))
                                (#\3 . ,DISPLAYED-GOAL)
                                (#\4 . ,(TERM-EVISC-TUPLE NIL STATE)))
                              (proofs-co state)
                              state
                              nil))
                          (increment-timer 'print-time state)
                          (prove (termify-clause-set o-p-clauses)
                            (make-pspv ens
                              wrld
                              state
                              :displayed-goal displayed-goal
                              :otf-flg otf-flg)
                            nil
                            ens
                            wrld
                            ctx
                            state))
                        (value ttree))))
                  (mv-let (has-ccgp has-measurep)
                    (ccg-hierarchy-kinds-of-levels hierarchy nil nil)
                    (er-let* ((ba-tuple (if has-ccgp
                           (build-accgs names contexts functs ccm-hints wrld state)
                           (list* (make-array 0
                               :initial-element (make-context)
                               :element-type 'context)
                             `(,(MAKE-ARRAY 0 :INITIAL-ELEMENT (MAKE-ACCG-NODE) :ELEMENT-TYPE 'ACCG-NODE))
                             `(,(MAKE-ARRAY 0 :INITIAL-ELEMENT (MAKE-ACCG-NODE) :ELEMENT-TYPE 'ACCG-NODE))
                             `(nil)))) (context-array (value (car ba-tuple)))
                        (proved-accgs (value (cadr ba-tuple)))
                        (accgs (value (caddr ba-tuple)))
                        (ces (value (cdddr ba-tuple)))
                        (measure-alist (if (not has-measurep)
                            (value nil)
                            (mv-let (erp ma state)
                              (guess-measure-alist names
                                arglists
                                measures
                                t-machines
                                ctx
                                wrld
                                state)
                              (if (not erp)
                                (value ma)
                                (pprogn (ccg-io? basics
                                    nil
                                    state
                                    (names)
                                    (fms "Since there was an error guessing the ~
                                   measure~#0~[~/s~], we will skip all levels ~
                                   of the hierarchy of the form (:MEASURE ~
                                   PT).~|"
                                      `((#\0 . ,NAMES))
                                      *standard-co*
                                      state
                                      nil))
                                  (value nil)))))))
                      (er-let* ((quadruple (ccg accgs
                             ces
                             nil
                             hierarchy
                             proved-accgs
                             context-array
                             names
                             arglists
                             t-machines
                             measure-alist
                             mp
                             rel
                             bodies
                             verbose
                             qspv
                             state)))
                        (let* ((term-method (car quadruple)) (col (cadr quadruple))
                            (measure-alist (caddr quadruple))
                            (ttree-new (cdddr quadruple)))
                          (prog2$ nil
                            (value (list* term-method
                                col
                                measure-alist
                                (cons-tag-trees ttree-new ttree1)))))))))))))))))

(defun-raw ccg-prove-termination-recursive
  (names arglists
    measures
    ccm-hints
    ruler-extenders-lst
    t-machines
    mp
    rel
    verbose
    time-limit
    hierarchy
    otf-flg
    bodies
    ctx
    ens
    wrld
    state)
  (let ((functs (make-funct-structs names arglists)))
    (prove-termination-with-ccg names
      functs
      (t-machines-to-contexts t-machines functs)
      ruler-extenders-lst
      ccm-hints
      hierarchy
      verbose
      time-limit
      arglists
      measures
      t-machines
      mp
      rel
      otf-flg
      bodies
      ctx
      ens
      wrld
      state
      nil)))

(defun-raw ccg-put-induction-info
  (names arglists
    term-method
    measures
    ccms
    ruler-extenders-lst
    bodies
    mp
    rel
    verbose
    time-limit
    hierarchy
    hints
    otf-flg
    big-mutrec
    measure-debug
    ctx
    ens
    wrld
    state)
  (prog2$ (choke-on-loop$-recursion nil
      names
      (car bodies)
      'ccg-put-induction-info)
    (let ((wrld1 (putprop-recursivep-lst nil nil names bodies wrld)))
      (cond ((and (null (cdr names))
           (null (getprop (car names)
               'recursivep
               nil
               'current-acl2-world
               wrld1))) (er-let* ((tuple (prove-termination-non-recursive names
                 bodies
                 mp
                 rel
                 hints
                 otf-flg
                 big-mutrec
                 ctx
                 ens
                 wrld1
                 state)))
            (value (cons nil tuple))))
        (t (let ((t-machines (termination-machines nil
                 nil
                 names
                 nil
                 bodies
                 ruler-extenders-lst)))
            (er-let* ((wrld1 (update-w t wrld1)) (quadruple (if (eq term-method :measure)
                    (er-let* ((triple (prove-termination-recursive names
                           arglists
                           measures
                           t-machines
                           mp
                           rel
                           hints
                           otf-flg
                           bodies
                           measure-debug
                           ctx
                           ens
                           wrld1
                           state)))
                      (value (cons :measure triple)))
                    (ccg-prove-termination-recursive names
                      arglists
                      measures
                      ccms
                      ruler-extenders-lst
                      t-machines
                      mp
                      rel
                      verbose
                      time-limit
                      hierarchy
                      otf-flg
                      bodies
                      ctx
                      ens
                      wrld1
                      state))))
              (let* ((term-method (car quadruple)) (col (cadr quadruple))
                  (measure-alist (caddr quadruple))
                  (ttree (cdddr quadruple)))
                (er-let* ((tuple (put-induction-info-recursive nil
                       names
                       arglists
                       col
                       ttree
                       measure-alist
                       t-machines
                       ruler-extenders-lst
                       bodies
                       mp
                       rel
                       wrld1
                       state)))
                  (value (cons term-method tuple)))))))))))

(defun-raw ccg-defuns-fn0
  (names arglists
    docs
    pairs
    guards
    term-method
    measures
    ccms
    ruler-extenders-lst
    mp
    rel
    verbose
    time-limit
    hierarchy
    hints
    guard-hints
    std-hints
    otf-flg
    guard-debug
    guard-simplify
    measure-debug
    bodies
    symbol-class
    normalizeps
    split-types-terms
    new-lambda$-alist-pairs
    non-executablep
    type-prescription-lst
    ctx
    wrld
    state)
  (cond ((eq symbol-class :program) (defuns-fn-short-cut nil
        nil
        names
        docs
        pairs
        guards
        measures
        split-types-terms
        bodies
        non-executablep
        ctx
        wrld
        state))
    (t (let ((ens (ens state)) (big-mutrec (big-mutrec names)))
        (er-let* ((tuple (ccg-put-induction-info names
               arglists
               term-method
               measures
               ccms
               ruler-extenders-lst
               bodies
               mp
               rel
               verbose
               time-limit
               hierarchy
               hints
               otf-flg
               big-mutrec
               measure-debug
               ctx
               ens
               wrld
               state)))
          (defuns-fn1 (cdr tuple)
            ens
            big-mutrec
            names
            arglists
            docs
            pairs
            guards
            guard-hints
            std-hints
            otf-flg
            guard-debug
            guard-simplify
            bodies
            symbol-class
            normalizeps
            split-types-terms
            new-lambda$-alist-pairs
            non-executablep
            type-prescription-lst
            ctx
            state))))))

(defun-bridge ccg-defuns-fn
  (def-lst state event-form)
  :program (value nil)
  :raw (with-ctx-summarized (defun-ctx def-lst)
    (let ((wrld (w state)) (def-lst0 def-lst)
        (event-form (or event-form (list 'defuns def-lst))))
      (revert-world-on-error (er-let* ((tuple (ccg-chk-acceptable-defuns def-lst ctx wrld state)) (fives (chk-defuns-tuples def-lst nil ctx wrld state)))
          (cond ((eq (car tuple) 'redundant) (stop-redundant-event ctx
                state
                :name (caar def-lst)
                :defun-mode (cdr tuple)
                :def-lst def-lst0))
            (t (enforce-redundancy event-form
                ctx
                wrld
                (let ((term-method (nth 1 tuple)) (names (nth 2 tuple))
                    (arglists (nth 3 tuple))
                    (docs (nth 4 tuple))
                    (pairs (nth 5 tuple))
                    (guards (nth 6 tuple))
                    (measures (nth 7 tuple))
                    (ruler-extenders-lst (nth 8 tuple))
                    (mp (nth 9 tuple))
                    (rel (nth 10 tuple))
                    (hints (nth 11 tuple))
                    (guard-hints (nth 12 tuple))
                    (std-hints (nth 13 tuple))
                    (otf-flg (nth 14 tuple))
                    (bodies (nth 15 tuple))
                    (symbol-class (nth 16 tuple))
                    (normalizeps (nth 17 tuple))
                    (reclassifyingp (nth 18 tuple))
                    (wrld (nth 19 tuple))
                    (non-executablep (nth 20 tuple))
                    (guard-debug (nth 21 tuple))
                    (measure-debug (nth 22 tuple))
                    (split-types-terms (nth 23 tuple))
                    (new-lambda$-alist-pairs (nth 24 tuple))
                    (guard-simplify (nth 25 tuple))
                    (type-prescription-lst (nth 26 tuple))
                    (ccms (nth 27 tuple))
                    (verbose (nth 28 tuple))
                    (time-limit (nth 29 tuple))
                    (hierarchy (nth 30 tuple)))
                  (er-let* ((pair (ccg-defuns-fn0 names
                         arglists
                         docs
                         pairs
                         guards
                         term-method
                         measures
                         ccms
                         ruler-extenders-lst
                         mp
                         rel
                         verbose
                         time-limit
                         hierarchy
                         hints
                         guard-hints
                         std-hints
                         otf-flg
                         guard-debug
                         guard-simplify
                         measure-debug
                         bodies
                         symbol-class
                         normalizeps
                         split-types-terms
                         new-lambda$-alist-pairs
                         non-executablep
                         type-prescription-lst
                         ctx
                         wrld
                         state)))
                    (er-progn (chk-assumption-free-ttree nil ctx state)
                      (install-event-defuns names
                        event-form
                        def-lst0
                        symbol-class
                        reclassifyingp
                        non-executablep
                        pair
                        ctx
                        wrld
                        state)
                      (if (or (eq symbol-class :program)
                          (ld-skip-proofsp state)
                          (and (null (cdr names))
                            (null (getprop (car names)
                                'recursivep
                                nil
                                'current-acl2-world
                                (w state)))))
                        (value (cond ((null (cdr names)) (car names)) (t names)))
                        (defun-make-event names
                          fives
                          symbol-class
                          term-method
                          (car pair)
                          event-form
                          state)))))))))))))

(logic)

(program)

(redefun defuns-fn
  (def-lst state event-form)
  (ccg-defuns-fn def-lst state event-form))

(progn+touchable :all (redefun+rewrite defstobj-fn
    (:carpat (process-embedded-events %1%
        %2%
        %3%
        %4%
        %5%
        (append . %app-cdr%) . %pee-cdr%)
      :repl (process-embedded-events %1%
        %2%
        %3%
        %4%
        %5%
        (append '((set-termination-method :measure)) . %app-cdr%) . %pee-cdr%)
      :vars (%1% %2% %3% %4% %5% %app-cdr% %pee-cdr%)
      :mult 1)))

(defxdoc ccg
  :parents (acl2-sedan proof-automation)
  :short "A powerful automated termination prover for ACL2"
  :long "<p>In order to see how the CCG analysis works, consider the following
 definition of Ackermann's function from exercise 6.15 in the ACL2
 textbook:</p>

 @({
  (defun ack (x y)
     (if (zp x)
         1
       (if (zp y)
           (if (equal x 1) 2 (+ x 2))
         (ack (ack (1- x) y) (1- y)))))

 })

 <p>ACL2 cannot automatically prove the termination of @('ack') using its
  measure-based termination proof. In order to admit the function, the user
  must supply a measure. An example measure is @('(make-ord 1 (1+ (acl2s-size
  y)) (acl2s-size x))'), which is equivalent to the ordinal @('w * (1+
  (acl2s-size y)) + (acl2s-size x)'), where @('w') is the first infinite
  ordinal.</p>

 <p>The CCG analysis, on the other hand, automatically proves termination as
 follows. Note that there are two recursive calls. These calls, along with
 their rulers (i.e. the conditions under which the recursive call is reached)
 are called <i>calling contexts</i>, or sometimes just <i>contexts</i> (for
 more on rulers, see @(see ruler-extenders)). For @('ack'), these are:</p>

 @({
  1. (ack (1- x) y) with ruler ((not (zp x)) (not (zp y))).
  2. (ack (ack (1- x) y) (1- y)) with ruler ((not (zp x)) (not (zp y))).
 })

 <p>These calling contexts are used to build a <i>calling context graph
 (CCG)</i>, from which our analysis derives its name. This graph has an edge
 from context @('c1') to context @('c2') when it is possible that execution can
 move from context @('c1') to context @('c2') in one ``step'' (i.e. without
 visiting any other contexts). For our example, we get the complete graph, with
 edges from each context to both contexts.</p>

 <p>The analysis next attempts to guess <i>calling context measures (CCMs)</i>,
 or just <i>measures</i>, for each function. These are similar to ACL2
 measures, in that they are ACL2 terms that must provably be able to evaluate
 to an ordinal value (unlike ACL2 measures, CCG currently ignores the current
 well-founded relation setting). However, functions may have multiple CCMs,
 instead of one, like ACL2, and the CCG analysis has some more sophisticated
 heuristics for guessing appropriate measures. However, there is a mechanism
 for supplying measures to the CCG analysis if you need to see @(see
 CCG-XARGS). In our example, the CCG analysis will guess the measures
 @('(acl2s-size x)'), @('(acl2s-size y)'), and @('(+ (acl2s-size x) (acl2s-size
 y))'). This last one turns out to be unimportant for the termination
 proof. However, note that the first two of these measures are components of
 the ordinal measure that we gave ACL2 to prove termination earlier. As one
 might guess, these are important for the success of our CCG analysis.</p>

 <p>Like ACL2's measure analysis, we are concerned with what happens to these
 values when a recursive call is made. However, we are concerned not just with
 decreasing measures, but also non-increasing measures. Thus, we construct
 <i>Calling Context Measure Functions (CCMFs)</i>, which tell us how one
 measure compares to another across recursive calls.</p>

 <p>In our example, note that when the recursive call of the context 1 is made,
 the new value of @('(acl2s-size x)') is less than the original value of
 @('(acl2s-size x)'). More formally, we can prove the following:</p>

 @({
  (implies (and (not (zp x))
                (not (zp y)))
           (o< (acl2s-size (1- x))
               (acl2s-size x)))
 })

 <p>For those of you that are familiar with measure-based termination proofs in
 ACL2, this should look familiar, as it has the same structure as such a
 termination proof. However, we also note the following trivial
 observation:</p>

 @({
  (implies (and (not (zp x))
                (not (zp y)))
           (o<= (acl2s-size y)
                (acl2s-size y)))
 })

 <p>That is, @('y') stays the same across this recursive call. For the other
 context, we similarly note that @('(acl2s-size y)') is decreasing. However, we
 can say nothing about the value of @('(acl2s-size x)'). The CCG algorithm does
 this analysis using queries to the theorem prover that are carefully
 restricted to limit prover time.</p>

 <p>Finally, the CCG analysis uses this local information to do a global
 analysis of what happens to values. This analysis asks the question, for every
 infinite path through our CCG, @('c_1'), @('c_2'), @('c_3'), ..., is there a
 natural number @('N') such that there is an infinite sequence of measures
 @('m_N'), @('m_(N+1)'), @('m_(N+2)'), ... such that each @('m_i') is a measure
 for the context @('c_i') (i.e. a measure for the function containing @('ci')),
 we have proven that the @('m_(i+1)') is never larger than @('m_i'), and for
 infinitely many @('i'), it is the case that we have proven that @('m_i') is
 always larger than @('m_(i+)'). That's a bit of a mouthful, but what we are
 essentially saying is that, for every possible infinite sequence of recursions
 it is the case that after some finite number of steps, we can start picking
 out measures such that they never increase and infinitely often they
 decrease. Since these measures return ordinal values, we then know that there
 can be no infinite recursions, and we are done.</p>

 <p>For our example, consider two kinds of infinite paths through our CCG:
 those that visit context 2 infinitely often, and those that don't. In the
 first case, we know that @('(acl2s-size y)') is never increasing, since a
 visit to context 1 does not change the value of @('y'), and a visit to context
 2 decreases the value of @('(acl2s-size y)'). Furthermore, since we visit
 context 2 infinitely often, we know that @('(acl2s-size y)') is infinitely
 decreasing along this path. Therefore, we have met the criteria for proving no
 such path is a valid computation. In the case in which we do not visit context
 2 infinitely often, there must be a value @('N') such that we do not visit
 context 2 any more after the @('N')th context in the path. After this, we must
 only visit context 1, which always decreases the value of @('(acl2s-size
 x)'). Therefore, no such path can be a valid computation. Since all infinite
 paths through our CCG either visit context 2 infinitely often or not, we have
 proven termination. This analysis of the local data in the global context is
 done automatically by a decision procedure.</p>

 <p>That is a brief overview of the CCG analysis. Note that, can it prove many
 functions terminating that ACL2 cannot. It also does so using simpler
 measures. In the @('ack') example, we did not require any infinite ordinal
 measures to prove termination using CCG. Intuitively, CCG is in a way putting
 together the measures for you so you don't have to think about the ordinal
 structure. Thus, even when the CCG analysis to prove termination, it is often
 easier to give it multiple simple measures and allow it to put together the
 global termination argument than to give ACL2 the entire measure so it can
 prove that it decreases every single step.</p>

 <p>To find out more about interacting and controlling the CCG analysis, see
 the topics included in this section.</p>")

(defxdoc ccg-xargs
  :parents (ccg)
  :short "Giving hints to CCG analysis via See @(see xargs)"
  :long "<p>In addition to the @(tsee xargs) provided by ACL2 for passing @(see
 hints) to function definitions, the CCG analysis enables several others for
 guiding the CCG termination analysis for a given function definition. The
 following example is nonsensical but illustrates all of these xargs:</p>

 @({
  (declare (xargs :termination-method :ccg
                  :consider-ccms ((foo x) (bar y z))
                  :consider-only-ccms ((foo x) (bar y z))
                  :ccg-print-proofs nil
                  :time-limit 120
                  :ccg-hierarchy *ccg-hierarchy-hybrid*))

  General Form:
  (xargs :key1 val1 ... :keyn valn)
 })

 <p>Where the keywords and their respective values are as shown below.</p>

 <p>Note that the :TERMINATION-METHOD @('xarg') is always valid, but the other
 @('xargs') listed above are only valid if the termination method being used
 for the given function is :CCG.</p>

 <p>@(':TERMINATION-METHOD value')<br></br>

 @('Value') here is either @(':CCG') or @(':MEASURE'). For details on the
 meaning of these settings, see the documentation for @(tsee
 set-termination-method). If this @('xarg') is given, it overrides the global
 setting for the current definition. If the current definition is part of a
 @(tsee mutual-recursion), and a @(':termination-method') is provided, it must
 match that provided by all other functions in the @('mutual-recursion').</p>

 <p>@(':CONSIDER-CCMS value') or @(':CONSIDER-ONLY-CCMS value')<br></br>

 @('Value') is a list of terms involving only the formals of the function being
 defined. Both suggest measures for the current function to the CCG
 analysis. ACL2 must be able to prove that each of these terms always evaluate
 to an ordinal see @(see ordinals). ACL2 will attempt to prove this before
 beginning the CCG analysis. The difference between @(':consider-ccms') and
 @(':consider-only-ccms') is that if @(':consider-ccms') is used, the CCG
 analysis will attempt to guess additional measures that it thinks might be
 useful for proving termination, whereas if @(':consider-only-ccms') is used,
 only the measures given will be used for the given function in the CCG
 analysis. These two @('xargs') may not be used together, and attempting to do
 so will result in an error.</p>

 <p>@(':CCG-PRINT-PROOFS value')<br></br>

 @('Value') is either @('t') or @('nil'). This is a local override of the
 @(tsee set-ccg-print-proofs) setting. See this documentation topic for
 details.</p>

 <p>@(':TIME-LIMIT value')<br></br>

 @('Value') is either a positive rational number or nil. This is a local
 override of the @(tsee set-ccg-time-limit) setting. See this documentation
 topic for details.</p>

 <p>@(':CCG-HIERARCHY value')<br></br>

 @('Value') is a CCG hierarchy. This is a local override of the @(tsee
 set-ccg-hierarchy) setting. See this documentation topic for details.</p>")

(defxdoc get-ccg-inhibit-output-lst
  :parents (ccg)
  :short "Returns the list of ``kinds'' of output that will be inhibited during CCG
analysis"
  :long "@({
  Examples:
  (get-ccg-inhibit-output-lst)
  :get-ccg-inhibit-output-lst
 })

 <p>See See @(see set-ccg-inhibit-output-lst).</p>")

(defxdoc get-ccg-print-proofs
  :parents (ccg)
  :short "Returns the setting that controls whether proof attempts are printed during
CCG analysis"
  :long "@({
  Examples:
  (get-ccg-print-proofs)
  :get-ccg-print-proofs
 })

 <p>See See @(see set-ccg-print-proofs) for details.</p>")

(defxdoc get-ccg-time-limit
  :parents (ccg)
  :short "Returns the current default ccg-time-limit setting."
  :long "@({
  Examples:
  (get-ccg-time-limit (w state))
 })

 <p>This will return the time-limit as specified by the current world.</p>

 @({
  General Form:
  (get-time-limit wrld)
 })

 <p>where @('wrld') is a @(see world). For information on the settings and
 their meaning, see @(see set-termination-method).</p>")

(defxdoc get-termination-method
  :parents (ccg)
  :short "Returns the current default termination method."
  :long "@({
  Examples:
  (get-termination-method (w state))
 })

 <p>This will return the termination-method as specified by the current
 world.</p>

 @({
  General Form:
  (get-termination-method wrld)
 })

 <p>where @('wrld') is a @(see world). For information on the settings and
 their meaning, see @(see set-termination-method).</p>")

(defxdoc set-ccg-hierarchy
  :parents (ccg)
  :short "Set the default hierarchy of techniques for CCG-based termination
analysis."
  :long "@({
  (set-ccg-hierarchy ((:built-in-clauses :equal t)
                      (:measure (:induction-depth 1))
                      ((:induction-depth 0) :EQUAL t)
                      ((:induction-depth 1) :EQUAL t)
                      ((:induction-depth 1) :ALL   t)
                      ((:induction-depth 1) :SOME  t)
                      ((:induction-depth 1) :NONE  t)
                      ((:induction-depth 1) :EQUAL nil)
                      ((:induction-depth 1) :ALL   nil)
                      ((:induction-depth 1) :SOME  nil)
                      ((:induction-depth 1) :NONE  nil)))
  :set-ccg-hierarchy ((:built-in-clauses :equal t)
                      ((:induction-depth 0) :EQUAL t)
                      ((:induction-depth 1) :EQUAL t)
                      ((:induction-depth 1) :ALL   t)
                      ((:induction-depth 1) :SOME  t)
                      ((:induction-depth 1) :NONE  t))

  General Form:
  (set-ccg-hierarchy v)
 })

 <p>where @('v') is @(':CCG-ONLY'), @(':CCG-ONLY-CPN'), @(':HYBRID'),
 @(':HYBRID-CPN'), or a non-empty list of hierarchy levels, which either have
 the form @('(pt ccm-cs cpn)') or the form @('(:measure pt)'), where @('pt') is
 either @(':built-in-clauses') or @('(:induction-depth n)') for some natural
 number @('n'), @('ccm-cs') is one of @(':EQUAL'), @(':ALL'), @(':SOME'), or
 @(':NONE'), and @('cpn') is @('t') or @('nil').</p>

 <p>Each level of the hierarchy describes techniques used to prove
 termination. Termination proofs performed after admitting this event will use
 the specified techniques in the order in which they are listed.</p>

 <p>Basically, the CCG analysis as described and illustrated at a high level in
 the documentation for @(see CCG) can potentially be very expensive. In order
 to make the analysis as efficient as possible, we use less expensive (and less
 powerful) techniques first, and resort to more powerful and expensive
 techniques only when these fail.</p>

 <p>There are three ways of varying the CCG analysis, which are represented by
 each of the three elements in a hierarchy level (levels of the form
 @('(:measure pt)') will be explained later).</p>

 <p>@('Pt') tells the CCG analysis how to limit proof attempts. The idea behind
 this is that ACL2 is designed to prove statements that the user thinks are
 true. It therefore does everything it can to prove the conjecture. As ACL2
 useres already know, this can lead to very long, or even non-terminating proof
 attempts. The CCG analysis, on the other hand, sends multiple queries to the
 theorem prover that may or may not be true, in order to improve the accuracy
 of the analysis. It is therefore necessary to reign in ACL2's proof attempts
 to keep them from taking too long. Of course, the trade-off is that, the more
 we limit ACL2's prover, the less powerful it becomes.</p>

 <p>@('Pt') can be @(':built-in-clauses'), which tells ACL2 to use only @(see
 built-in-clause)s analysis. This is a very fast, and surprisingly powerful
 proof technique. For example, the definition of Ackermann's function given in
 the documentation for @(see CCG) is solved using only this proof
 technique.</p>

 <p>@('Pt') can also be of the form @('(:induction-depth n)'), where @('n') is
 a natural number. This uses the full theorem prover, but limits it in two
 ways. First, it stops proof attempts if ACL2 has been working on a subgoal
 with no case splitting or induction for 20 steps (that is, at a goal of the
 form 1.5'20'). It also limits the <i>induction depth</i>, which describes how
 many times we allow induction goals to lead to further induction goals. For
 example, @('(:induction-depth 0)') allows no induction, while
 @('(:induction-depth 1)') allows goals of the form @('*1') or @('*2'), but
 stops if it creates a goal such as @('*1.1') or @('*2.1').</p>

 <p>@('Ccm-cs') limits which CCMs are compared using the theorem
 prover. Consider again the @('ack') example in the documentation for @(see
 CCG). All we needed was to compare the value of @('(acl2s-size x)') before and
 after the recursive call and the value of @('(acl2s-size y)') before and after
 the recursive call. We would learn nothing, and waste time with the theorem
 prover if we compared @('(acl2s-size x)') to @('(acl2s-size y)'). However,
 other times, it is important to compare CCMs with each other, for example,
 when arguments are permuted, or we are dealing with a mutual recursion.</p>

 <p>@('Ccm-cs') can be one of @(':EQUAL'), @(':ALL'), @(':SOME'), or
 @(':NONE'). These limit which CCMs we compare based on the variables they
 mention. Let @('c') be a recursive call in the body of function @('f') that
 calls function @('g'). Let @('m1') be a CCM for @('f') and @('m2') be a CCM
 for @('g'). Let @('v1') be the formals mentioned in @('m1') and @('v2') be the
 formals mentioned in @('m2'') where @('m2'') is derived from @('m2') by
 substituting the formals of @('g') with the actuals of @('c'). For example,
 consider following function:</p>

 @({
  (defun f (x)
    (if (endp x)
        0
      (1+ (f (cdr x)))))
 })

 <p>Now consider the case where @('m1') and @('m2') are both the measure
 @('(acl2s-size x)'). Then if we look at the recursive call @('(f (cdr x))') in
 the body of @('f'), then @('m2'') is the result of replacing @('x') with
 @('(cdr x)') in @('m2'), i.e., @('(acl2s-size (cdr x))').</p>

 <p>If @('ccm-cs') is @(':EQUAL') we will compare @('m1') to @('m2') if @('v1')
 and @('v2') are equal. If @('value') is @(':ALL') we will compare @('m1') to
 @('m2'') if @('v2') is a subset of @('v1'). If @('value') is @(':SOME') we
 will compare @('m1') to @('m2'') if @('v1') and @('v2') intersect. If
 @('value') is @(':NONE') we will compare @('m1') to @('m2') no matter
 what.</p>

 <p>There is one caveat to what was just said: if @('m1') and @('m2') are
 syntactically equal, then regardless of the value of @('ccm-cs') we will
 construct a CCMF that will indicate that @('(o>= m1 m2)').</p>

 <p>@('Cpn') tells us how much ruler information we will use to compare CCMs.
 Unlike ACL2's measure-based termination analysis, CCG has the ability to use
 the rulers from both the current recursive call the next recursive call when
 constructing the CCMFs. That is, instead of asking ``What happens when I make
 recursive call A?'', we can ask, ``What happens when execution moves from
 recursive call A to recursive call B?''. Using this information potentially
 strengthens the termination analysis. For a brief example, consider the
 following code:</p>

 @({
  (defun half (x)
     (if (zp x)
         0
       (1+ (half (- x 2)))))
 })

 <p>Clearly this is terminating. If we choose a measure of @('(nfix x)') we
 know that if @('x') is a positive integer, @('(nfix (- x 2))') is less than
 @('(nfix x)'). But consider the measure @('(acl2s-size x)'). The strange thing
 here is that if @('x') is 1, then @('(acl2s-size (- x 2))') is @('(acl2s-size
 -1)'), which is 1, i.e. the @('acl2s-size') of @('x'). So, the fact that we
 know that @('x') is a positive integer is not enough to show that this measure
 decreases. But notice that if @('x') is 1, we will recur just one more
 time. So, if we consider what happens when we move from the recursive call
 back to itself. In this case we know @('(and (not (zp x)) (not (zp (- x
 2))))').  Under these conditions, it is trivial for ACL2 to prove that
 @('(acl2s-size (- x 2))') is always less than @('(acl2s-size x)').

 However, this can make the CCG analysis much more expensive, since information
 about how values change from step to step are done on a per-edge, rather than
 a per-node basis in the CCG (where the nodes are the recursive calls and the
 edges indicate that execution can move from one call to another in one
 step). Thus, calculating CCMFs (how values change across recursive calls) on a
 per-edge basis rather than a per-node basis can require n^2 instead of n
 prover queries.</p>

 <p>If @('cpn') is @('t'), we will use only the ruler of the current recursive
 call to compute our CCMFs. If it is @('nil'), we will use the much more
 expensive technique of using the rulers of the current and next call.</p>

 <p>Levels of the hierarchy of the form @('(:measure pt)') specify that the CCG
 analysis is to be set aside for a step, and the traditional measure-based
 termination proof is to be attempted. Here, @('pt') has the same meaning as it
 does in a CCG hierarchy level. That is, it limits the measure proof in order
 to avoid prohibitively long termination analyses.</p>

 <p>The user may specify their own hierarchy in the form given above. The main
 restriction is that no level may be subsumed by an earlier level. That is, it
 should be the case at each level of the hierarchy, that it is possible to
 discover new information about the CCG that could help lead to a termination
 proof.</p>

 <p>In addition to constructing his or her own CCG hierarchy, the user may use
 several preset hierarchies:</p>

 @({
  :CCG-ONLY
  ((:built-in-clauses :equal t)
   ((:induction-depth 0) :EQUAL t)
   ((:induction-depth 1) :EQUAL t)
   ((:induction-depth 1) :ALL   t)
   ((:induction-depth 1) :SOME  t)
   ((:induction-depth 1) :NONE  t)
   ((:induction-depth 1) :EQUAL nil)
   ((:induction-depth 1) :ALL   nil)
   ((:induction-depth 1) :SOME  nil)
   ((:induction-depth 1) :NONE  nil))

  :CCG-ONLY-CPN
  ((:built-in-clauses :equal t)
   ((:induction-depth 0) :EQUAL t)
   ((:induction-depth 1) :EQUAL t)
   ((:induction-depth 1) :ALL   t)
   ((:induction-depth 1) :SOME  t)
   ((:induction-depth 1) :NONE  t))

  :HYBRID
  ((:built-in-clauses :equal t)
   (:measure (:induction-depth 1))
   ((:induction-depth 0) :EQUAL t)
   ((:induction-depth 1) :EQUAL t)
   ((:induction-depth 1) :ALL   t)
   ((:induction-depth 1) :SOME  t)
   ((:induction-depth 1) :NONE  t)
   ((:induction-depth 1) :EQUAL nil)
   ((:induction-depth 1) :ALL   nil)
   ((:induction-depth 1) :SOME  nil)
   ((:induction-depth 1) :NONE  nil))

  :HYBRID-CPN
  ((:built-in-clauses :equal t)
   (:measure (:induction-depth 1))
   ((:induction-depth 0) :EQUAL t)
   ((:induction-depth 1) :EQUAL t)
   ((:induction-depth 1) :ALL   t)
   ((:induction-depth 1) :SOME  t)
   ((:induction-depth 1) :NONE  t))
 })

 <p>The default hierarchy for CCG termination analysis is :CCG-ONLY.</p>")

(defxdoc set-ccg-inhibit-output-lst
  :parents (ccg)
  :short "Control output during CCG termination analysis"
  :long "@({
  Examples:
  (set-ccg-inhibit-output-lst '(query))
  (set-ccg-inhibit-output-lst '(build/refine size-change))
  (set-ccg-inhibit-output-lst *ccg-valid-output-names*) ; inhibit all ccg output
  :set-ccg-inhibit-output-lst (build/refine size-change)

  General Form:
  (set-ccg-inhibit-output-lst lst)
 })

 <p>where @('lst') is a form (which may mention @(tsee state)) that evaluates
 to a list of names, each of which is the name of one of the following
 ``kinds'' of output produced by the CCG termination analysis.</p>

 <code> query prints the goal, restrictions, and results of each prover
   query (for a discussion on displaying actual proofs, see
   @('set-ccg-display-proofs')(yet to be documented).  basics the basic CCG
   output, enough to follow along, but concise enough to keep from drowning in
   output performance performance information for the size change analysis
   build/refine the details of CCG construction and refinement size-change the
   details of size change analysis counter-example prints out a counter-example
   that can be useful for debugging failed termination proof attempts.  </code>

 <p>It is possible to inhibit each kind of output by putting the corresponding
 name into @('lst').  For example, if @(''query') is included in (the value of)
 @('lst'), then no information about individual queries is printed during CCG
 analysis.</p>

 <p>The default setting is @(''(query performance build/refine size-change)').
 That is, by default only the basic CCG information and counter-example (in the
 case of a failed proof attempt) are printed. This should hopefully be adequate
 for most users.</p>")

(defxdoc set-ccg-print-proofs
  :parents (ccg)
  :short "Controls whether proof attempts are printed during CCG analysis"
  :long "@({
  Examples:
  (set-ccg-print-proofs t)
  (set-ccg-print-proofs nil)
  :set-ccg-print-proofs t

  General Form:
  (set-ccg-print-proofs v)
 })

 <p>If @('v') is @('nil'), no proof attempts will be printed during CCG
 analysis. This is the default. If @('v') is anything but @('nil'), proofs will
 be displayed. Fair warning: there is potentially a large amount of prover
 output that might be displayed. It is probably better to use See @(see
 set-ccg-inhibit-output-lst) to un-inhibit @(''query') output to figure out
 what lemmas might be needed to get a given query to go through.</p>")

(defxdoc set-ccg-time-limit
  :parents (ccg)
  :short "Set a global time limit for CCG-based termination proofs."
  :long "@({
  Examples:
  (set-ccg-time-limit 120)  ; limits termination proofs to 120 seconds.
  (set-ccg-time-limit 53/2) ; limits termination proofs to 53/2 seconds.
  (set-ccg-time-limit nil)  ; removes any time limit for termination proofs.
 })

 <p>Introduced by the CCG analysis book, this macro sets a global time limit
 for the completion of the CCG analysis. The time limit is given as a rational
 number, signifying the number of seconds to which the CCG analysis should be
 limited, or nil, signifying that there should be no such time limit. If CCG
 has not completed its attempt to prove termination in the number of seconds
 specified, it will immediately throw an error and the definition attempt will
 fail. Note: This is an event!  It does not print the usual event summary but
 nevertheless changes the ACL2 logical @(see world) and is so recorded.</p>

 @({
   General Form:
  (set-ccg-time-limit tl)
 })

 <p>where @('tl') is a positive rational number or nil. The default is nil. If
 the time limit is nil, the CCG analysis will work as long as it needs to in
 order to complete the analysis. If the @('tl') is a positive rational number,
 all CCG analyses will be limited to @('tl') seconds.</p>

 <p>To see what the current time limit is, see @(tsee
 get-ccg-time-limit).</p>")

(defxdoc set-termination-method
  :parents (ccg)
  :short "Set the default means of proving termination."
  :long "@({
  Examples:
  (set-termination-method :ccg)
  (set-termination-method :measure)
 })

 <p>Introduced by the CCG analysis book, this macro sets the default means by
 which ACL2 will prove termination. Note: This is an event!  It does not print
 the usual event summary but nevertheless changes the ACL2 logical @(see world)
 and is so recorded.</p>

 @({
   General Form:
  (set-termination-method tm)
 })

 <p>where @('tm') is @(':CCG') or @(':MEASURE'). The default is @(':MEASURE')
 (chosen to assure compatibility with books created without CCG). The
 recommended setting is @(':CCG'). This macro is equivalent to @('(table
 acl2-defaults-table :termination-method 'tm)'), and hence is @(tsee local) to
 any @(see books) and @(tsee encapsulate) @(see events) in which it occurs; see
 @(see acl2-defaults-table).</p>

 <p>When the termination-method is set to @(':CCG'), a termination proof is
 attempted using the the hierarchical CCG algorithm <a
 href='CCG-hierarchy'>CCG-hierarchy</a>.</p>

 <p>When the termination-method is set to @(':MEASURE'), ACL2 attempts to prove
 termination using its default measure-based method. Thus, in this setting,
 ACL2's behavior is identical to that when the CCG book is not included at
 all.</p>

 <p>To see what the current termination method setting is, use @(tsee
 get-termination-method).</p>")