		Search-engine friendly clone of the ACL2 documentation.

Solve-implementation

Solve-fn

Check redundancy, process the inputs, and generate the event.

Signature
(solve-fn old method method? method-rules solution-name solution-enable solution-enable? solution-guard solution-guard? solution-guard-hints solution-guard-hints? solution-body solution-body? solution-hints solution-hints? new-name new-enable old-if-new-name old-if-new-name? old-if-new-enable old-if-new-enable? verify-guards print show-only call ctx state) → (mv erp event state)
Arguments: method? — Guard (booleanp method?).; solution-enable? — Guard (booleanp solution-enable?).; solution-guard? — Guard (booleanp solution-guard?).; solution-guard-hints? — Guard (booleanp solution-guard-hints?).; solution-body? — Guard (booleanp solution-body?).; solution-hints? — Guard (booleanp solution-hints?).; old-if-new-name? — Guard (booleanp old-if-new-name?).; old-if-new-enable? — Guard (booleanp old-if-new-enable?).; call — Guard (pseudo-event-formp call).
Returns: event — A pseudo-event-formp.

Definitions and Theorems

Function: solve-fn

(defun solve-fn (old method method? method-rules
                     solution-name solution-enable
                     solution-enable? solution-guard
                     solution-guard? solution-guard-hints
                     solution-guard-hints?
                     solution-body solution-body?
                     solution-hints solution-hints?
                     new-name new-enable old-if-new-name
                     old-if-new-name? old-if-new-enable
                     old-if-new-enable? verify-guards
                     print show-only call ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp method?)
                             (booleanp solution-enable?)
                             (booleanp solution-guard?)
                             (booleanp solution-guard-hints?)
                             (booleanp solution-body?)
                             (booleanp solution-hints?)
                             (booleanp old-if-new-name?)
                             (booleanp old-if-new-enable?)
                             (pseudo-event-formp call))))
 (let ((__function__ 'solve-fn))
   (declare (ignorable __function__))
   (b*
    ((encapsulate?
          (previous-transformation-expansion call (w state)))
     ((when encapsulate?)
      (b* (((run-when show-only)
            (cw "~x0~|" encapsulate?)))
        (cw "~%The transformation ~x0 is redundant.~%"
            call)
        (value '(value-triple :invisible))))
     ((er (list old ??f x1...xn matrix f f-existsp new
                new-enable old-if-new old-if-new-enable
                verify-guards names-to-avoid))
      (solve-process-inputs old method method? method-rules
                            solution-name solution-enable
                            solution-enable? solution-guard
                            solution-guard? solution-guard-hints
                            solution-guard-hints?
                            solution-body solution-body?
                            solution-hints solution-hints?
                            new-name new-enable old-if-new-name
                            old-if-new-name? old-if-new-enable
                            old-if-new-enable? verify-guards
                            print show-only ctx state))
     ((er event)
      (solve-gen-everything old ?f x1...xn matrix method
                            method-rules f f-existsp solution-enable
                            solution-guard solution-guard-hints
                            solution-body solution-hints new
                            new-enable old-if-new old-if-new-enable
                            verify-guards print show-only
                            call names-to-avoid ctx state)))
    (value event))))