		Search-engine friendly clone of the ACL2 documentation.

Solve-input-processing

Solve-process-solution-body

Process the :solution-body input.

Signature
(solve-process-solution-body solution-body solution-body? method x1...xn f-existsp ctx state) → (mv erp nothing state)
Arguments: solution-body? — Guard (booleanp solution-body?).; method — Guard (keywordp method).; x1...xn — Guard (symbol-listp x1...xn).; f-existsp — Guard (booleanp f-existsp).
Returns: nothing — Always nil.

Definitions and Theorems

Function: solve-process-solution-body

(defun solve-process-solution-body
       (solution-body solution-body?
                      method x1...xn f-existsp ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp solution-body?)
                             (keywordp method)
                             (symbol-listp x1...xn)
                             (booleanp f-existsp))))
 (let ((__function__ 'solve-process-solution-body))
  (declare (ignorable __function__))
  (if
   (eq method :manual)
   (if f-existsp
    (if solution-body?
     (er-soft+
      ctx t nil
      "Since the :SOLUTION-NAME input ~
                         specifies an existing function, ~
                         the :SOLUTION-BODY input must be absent, ~
                         but instead ~x0 has been supplied.")
     (value nil))
    (if
     (not solution-body?)
     (er-soft+
      ctx t nil
      "Since the :METHOD input is :MANUAL ~
                       and the :SOLUTION-NAME input specifies ~
                       the name of a function to be generated, ~
                       the :SOLUTION-BODY input must be supplied.")
     (b* (((er (list term stobjs-out))
           (ensure-value-is-untranslated-term$
                solution-body
                "The :SOLUTION-BODY input" t nil))
          (description (msg "The :SOLUTION-BODY term ~x0"
                            solution-body))
          ((er &)
           (ensure-function/lambda/term-number-of-results$
                stobjs-out 1 description t nil))
          ((er &)
           (ensure-term-free-vars-subset$
                term x1...xn description t nil)))
       (value nil))))
   (if solution-body?
    (er-soft+
     ctx t nil
     "Since the :METHOD input is not :MANUAL, ~
                   the :SOLUTION-BODY input must be absent, ~
                   but instead ~x0 has been supplied."
     solution-body)
    (value nil)))))