		Search-engine friendly clone of the ACL2 documentation.

Solve-input-processing

Solve-process-method

Process the :method input.

Signature
(solve-process-method method method? ctx state) → (mv erp nothing state)
Arguments: method? — Guard (booleanp method?).
Returns: nothing — Type (null nothing).

Definitions and Theorems

Function: solve-process-method

(defun solve-process-method (method method? ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (booleanp method?)))
 (let ((__function__ 'solve-process-method))
  (declare (ignorable __function__))
  (cond
   ((eq method :acl2-rewriter)
    (if (function-symbolp *solve-call-acl2-rewriter* (w state))
        (value nil)
     (er-soft+
      ctx t nil
      "In order to use the ACL2 rewriter as the solving method ~
             it is necessary to include community book ~
             kestrel/apt/solve-method-acl2-rewriter.lisp.")))
   ((eq method :axe-rewriter)
    (if (function-symbolp *solve-call-axe-rewriter* (w state))
        (value nil)
     (er-soft+
      ctx t nil
      "In order to use the Axe rewriter as the solving method ~
             it is necessary to include community book ~
             kestrel/apt/solve-method-axe-rewriter.lisp.")))
   ((eq method :manual) (value nil))
   (method?
    (er-soft+
     ctx t nil
     "The :METHOD input must be ~
                    :ACL2-REWRITER, :AXE-REWRITER, or :MANUAL, ~
                    but it is ~x0 instead. ~
                    More methods will be supported in the future."
     method))
   (t (er-soft+ ctx t nil
                "The :METHOD input must be supplied.")))))

Theorem: null-of-solve-process-method.nothing

(defthm null-of-solve-process-method.nothing
  (b* (((mv ?erp ?nothing acl2::?state)
        (solve-process-method method method? ctx state)))
    (null nothing))
  :rule-classes :rewrite)