default-hint

(defun nonlinearp-default-hint
  (stable-under-simplificationp hist pspv)
  (declare (xargs :guard (and (consp pspv)
        (consp (car pspv))
        (consp (car (car pspv)))
        (consp (car (car (car pspv))))
        (consp (car (car (car (car pspv)))))
        (consp (cdr (car (car (car (car pspv)))))))))
  (cond (stable-under-simplificationp (if (not (access rewrite-constant
            (access prove-spec-var pspv :rewrite-constant)
            :nonlinearp))
        (prog2$ (observation-cw 'nonlinearp-default-hint
            "We now enable non-linear arithmetic.")
          '(:computed-hint-replacement t :nonlinearp t))
        nil))
    ((access rewrite-constant
       (access prove-spec-var pspv :rewrite-constant)
       :nonlinearp) (if (and (consp hist)
          (consp (car hist))
          (not (equal (caar hist) 'settled-down-clause)))
        (prog2$ (observation-cw 'nonlinearp-default-hint
            "We now disable non-linear arithmetic.")
          '(:computed-hint-replacement t :nonlinearp nil))
        nil))
    (t nil)))

(defun arithmetic-default-hint
  (stable-under-simplificationp hist last-hint-used)
  (declare (xargs :mode :program))
  (cond (stable-under-simplificationp (cond ((equal last-hint-used nil) (prog2$ (observation-cw 'arithmetic-default-hint
              "We now enable prefer-positive-exponents.")
            (let ((e/d '(((:rewrite prefer-positive-exponents-scatter-exponents-equal) (:rewrite prefer-positive-exponents-scatter-exponents-<)
                    (:rewrite prefer-positive-exponents-scatter-exponents-<-2)
                    (:rewrite |(expt x (+ m n))|)
                    (:rewrite |(expt x (+ m n)) non-zero (+ m n)|)
                    (:rewrite |(expt x (+ m n)) non-zero x|)
                    (:rewrite normalize-factors-scatter-exponents)
                    (:rewrite simplify-products-scatter-exponents-equal)
                    (:rewrite simplify-products-scatter-exponents-<)) ((:rewrite normalize-factors-gather-exponents) (:rewrite simplify-products-gather-exponents-equal)
                     (:rewrite simplify-products-gather-exponents-<)))))
              `(:computed-hint-replacement ((arithmetic-default-hint stable-under-simplificationp
                   hist
                   'prefer-positive-addends))
                :dynamic-e/d ,E/D
                :nonlinearp nil))))
        ((equal last-hint-used 'prefer-positive-addends) (prog2$ (observation-cw 'arithmetic-default-hint
              "We now enable non-linear arithmetic.")
            `(:computed-hint-replacement ((arithmetic-default-hint stable-under-simplificationp
                 hist
                 'non-linear-arithmetic))
              :nonlinearp t)))
        (t nil)))
    ((and (equal last-hint-used 'non-linear-arithmetic)
       (consp hist)
       (consp (car hist))
       (not (equal (caar hist) 'settled-down-clause))) (prog2$ (observation-cw 'arithmetic-default-hint
          "We now disable non-linear arithmetic and return to the earlier ~
            enabled theory.")
        (let ((e/d '(((:rewrite normalize-factors-gather-exponents) (:rewrite simplify-products-gather-exponents-equal)
                (:rewrite simplify-products-gather-exponents-<)) ((:rewrite prefer-positive-exponents-scatter-exponents-equal) (:rewrite prefer-positive-exponents-scatter-exponents-<)
                 (:rewrite prefer-positive-exponents-scatter-exponents-<-2)
                 (:rewrite |(expt x (+ m n))|)
                 (:rewrite |(expt x (+ m n)) non-zero (+ m n)|)
                 (:rewrite |(expt x (+ m n)) non-zero x|)
                 (:rewrite normalize-factors-scatter-exponents)
                 (:rewrite simplify-products-scatter-exponents-equal)
                 (:rewrite simplify-products-scatter-exponents-<)))))
          `(:computed-hint-replacement ((arithmetic-default-hint stable-under-simplificationp
               hist
               nil))
            :dynamic-e/d ,E/D
            :nonlinearp nil))))
    (t nil)))

(defun first-inductive-subgoal-p
  (id)
  (declare (xargs :guard (and (consp id) (consp (cdr id)))))
  (and (< 1 (len (car id)))
    (equal 1 (len (cadr id)))
    (equal 0 (cddr id))))

(defun branch-taken1
  (x ans)
  (declare (xargs :guard (true-listp x)))
  (cond ((endp x) ans)
    ((equal (car x) 'd1) (branch-taken1 (cdr x) 1))
    ((equal (car x) 'd2) (branch-taken1 (cdr x) 2))
    (t (branch-taken1 (cdr x) ans))))

(defun branch-taken
  (id)
  (declare (xargs :guard (and (consp id) (consp (cdr id)) (true-listp (cadr id)))))
  (branch-taken1 (cadr id) nil))

(defun nonlinearp-default-hint++
  (id stable-under-simplificationp hist last-hint-used)
  (declare (xargs :mode :program))
  (cond (stable-under-simplificationp (cond ((equal last-hint-used nil) (prog2$ (observation-cw 'nonlinearp-default-hint++ "Branch.")
            (let ((e/d '(((:rewrite prefer-positive-exponents-scatter-exponents-equal) (:rewrite prefer-positive-exponents-scatter-exponents-<)
                    (:rewrite prefer-positive-exponents-scatter-exponents-<-2)
                    (:rewrite |(expt x (+ m n))|)
                    (:rewrite |(expt x (+ m n)) non-zero (+ m n)|)
                    (:rewrite |(expt x (+ m n)) non-zero x|)
                    (:rewrite normalize-factors-scatter-exponents)
                    (:rewrite simplify-products-scatter-exponents-equal)
                    (:rewrite simplify-products-scatter-exponents-<)) ((:rewrite normalize-factors-gather-exponents) (:rewrite simplify-products-gather-exponents-equal)
                     (:rewrite simplify-products-gather-exponents-<)))))
              `(:computed-hint-replacement ((nonlinearp-default-hint++ id
                   stable-under-simplificationp
                   hist
                   'check-branch-taken))
                :or ((:dynamic-e/d ,E/D :nonlinearp nil) (:nonlinearp t))))))
        ((equal last-hint-used 'prefer-positive-exponents) (prog2$ (observation-cw 'nonlinearp-default-hint++
              "Prefer-positive-exponents.")
            `(:computed-hint-replacement ((nonlinearp-default-hint++ id
                 stable-under-simplificationp
                 hist
                 'non-linear-arithmetic))
              :nonlinearp t)))
        ((equal last-hint-used 'recycle) (prog2$ (observation-cw 'nonlinearp-default-hint++ "Recycle.")
            `(:computed-hint-replacement ((nonlinearp-default-hint++ id
                 stable-under-simplificationp
                 hist
                 'non-linear-arithmetic))
              :nonlinearp t)))
        (t nil)))
    ((equal last-hint-used 'check-branch-taken) (let ((branch-taken (branch-taken id)))
        (cond ((equal branch-taken 2) (prog2$ (observation-cw 'nonlinearp-default-hint++
                "Check-branch-taken prefer-positive-exponents.")
              `(:computed-hint-replacement ((nonlinearp-default-hint++ id
                   stable-under-simplificationp
                   hist
                   'prefer-positive-exponents))
                :no-op t)))
          ((equal branch-taken 1) (prog2$ (observation-cw 'nonlinearp-default-hint++
                "Check-branch-taken non-linear-arithmetic.")
              `(:computed-hint-replacement ((nonlinearp-default-hint++ id
                   stable-under-simplificationp
                   hist
                   'recycle))
                :nonlinearp nil)))
          (t (cw "~%~%~ [Note: Computed hint error --- seemingly impossible ~
                  case reached in nonlinearp-default-hint++.  Perhaps there ~
                  are two or more :OR hints interacting in unexpected ways.  ~
                  We do not know what to do here, and so are defaulting to ~
                  doing nothing.~%~%")))))
    ((and (equal last-hint-used 'non-linear-arithmetic)
       (consp hist)
       (consp (car hist))
       (not (equal (caar hist) 'settled-down-clause))) (prog2$ (observation-cw 'nonlinearp-default-hint++
          "Non-linear-arithmetic.")
        `(:computed-hint-replacement ((nonlinearp-default-hint++ id
             stable-under-simplificationp
             hist
             'recycle))
          :nonlinearp nil)))
    (t nil)))