		Search-engine friendly clone of the ACL2 documentation.

Solve-input-processing

Solve-process-solution-guard

Process the :solution-guard input.

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

Definitions and Theorems

Function: solve-process-solution-guard

(defun solve-process-solution-guard
       (solution-guard solution-guard?
                       x1...xn f-existsp ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp solution-guard?)
                             (symbol-listp x1...xn)
                             (booleanp f-existsp))))
 (let ((__function__ 'solve-process-solution-guard))
  (declare (ignorable __function__))
  (b*
   (((when (and solution-guard? f-existsp))
     (er-soft+
      ctx t nil
      "Since the :SOLUTION-NAME input ~
                   specifies an existing function, ~
                   the :SOLUTION-GUARD input must be absent."))
    ((er (list term stobjs-out))
     (ensure-value-is-untranslated-term$
          solution-guard
          "The :SOLUTION-GUARD input" t nil))
    (description (msg "The :SOLUTION-GUARD term ~x0"
                      solution-guard))
    ((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))))