		Search-engine friendly clone of the ACL2 documentation.

Solve-input-processing

Solve-process-solution-hints

Process the :solution-hints input.

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

For now we just check that this is a true list, which may be enough to catch simple mistakes. We may extend this input processor with more validity checks.

Definitions and Theorems

Function: solve-process-solution-hints

(defun solve-process-solution-hints
       (solution-hints solution-hints? method ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp solution-hints?)
                             (keywordp method))))
 (let ((__function__ 'solve-process-solution-hints))
  (declare (ignorable __function__))
  (if (eq method :manual)
      (ensure-value-is-true-list$ solution-hints
                                  "The :SOLUTION-HINTS input" t nil)
   (if solution-hints?
    (er-soft+
     ctx t nil
     "Since the :METHOD input is not :MANUAL, ~
                   the :SOLUTION-HINTS input must be absent, ~
                   but instead ~x0 has been supplied."
     solution-hints)
    (value nil)))))

Theorem: null-of-solve-process-solution-hints.nothing

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