		Search-engine friendly clone of the ACL2 documentation.

Solve-input-processing

Solve-process-solution-guard-hints

Process the :solution-guard-hints input.

Signature
(solve-process-solution-guard-hints solution-guard-hints solution-guard-hints? f-existsp ctx state) → (mv erp nothing state)
Arguments: solution-guard-hints? — Guard (booleanp solution-guard-hints?).; f-existsp — Guard (booleanp f-existsp).
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-guard-hints

(defun solve-process-solution-guard-hints
       (solution-guard-hints solution-guard-hints?
                             f-existsp ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp solution-guard-hints?)
                             (booleanp f-existsp))))
 (let ((__function__ 'solve-process-solution-guard-hints))
  (declare (ignorable __function__))
  (if
   (and solution-guard-hints? f-existsp)
   (er-soft+
    ctx t nil
    "Since the :SOLUTION-NAME input ~
                 specifies an existing function, ~
                 the :SOLUTION-GUARD-HINTS input must be absent.")
   (ensure-value-is-true-list$ solution-guard-hints
                               "The :SOLUTION-GUARD-HINTS input"
                               t nil))))

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

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