default-hint - ACL2 Book

other

(in-package "ACL2")

other

(verify-termination observation1-cw
  (declare (xargs :verify-guards t)))

nonlinearp-default-hintfunction

(defun nonlinearp-default-hint
  (stable-under-simplificationp hist 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 (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)))