		Search-engine friendly clone of the ACL2 documentation.

Solve-event-generation

Solve-gen-solution-ACL2-rewriter

Attempt to generate a solution using the ACL2 rewriter.

Signature
(solve-gen-solution-acl2-rewriter old ?f x1...xn matrix method-rules f solution-enable solution-guard solution-guard-hints verify-guards print names-to-avoid ctx state) → (mv erp result state)
Arguments: old — Guard (symbolp old).; ?f — Guard (symbolp ?f).; x1...xn — Guard (symbol-listp x1...xn).; matrix — Guard (pseudo-termp matrix).; method-rules — Guard (symbol-listp method-rules).; f — Guard (symbolp f).; solution-enable — Guard (booleanp solution-enable).; solution-guard — An untranslated term.; solution-guard-hints — Guard (true-listp solution-guard-hints).; verify-guards — Guard (booleanp verify-guards).; print — Guard (evmac-input-print-p print).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: result — (tuple (local-events pseudo-event-form-listp) (exported-events pseudo-event-form-listp) (solution-theorem symbolp) (old-instance symbolp) (updated-names-to-avoid symbol-listp) result).

We reflectively call a function that calls the ACL2 rewriter. This function is in a separate file, which can be included, along with its dependency on rewrite$, only if desired. The input validation performed by this transformation ensures that we call the function only if its file is included.

If the call is successful, we attempt to extract a solution, i.e. the body to use for the function f to generate.

We generate the rewriting theorem and the solution theorem, along with the solution function.

We return all the events, the name of the solution theorem, and the name of the instance of old in the theorem.

Definitions and Theorems

Function: solve-gen-solution-acl2-rewriter

(defun solve-gen-solution-acl2-rewriter
       (old ?f x1...xn matrix method-rules
            f solution-enable solution-guard
            solution-guard-hints verify-guards
            print names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old)
                             (symbolp ?f)
                             (symbol-listp x1...xn)
                             (pseudo-termp matrix)
                             (symbol-listp method-rules)
                             (symbolp f)
                             (booleanp solution-enable)
                             (true-listp solution-guard-hints)
                             (booleanp verify-guards)
                             (evmac-input-print-p print)
                             (symbol-listp names-to-avoid))))
 (let ((__function__ 'solve-gen-solution-acl2-rewriter))
   (declare (ignorable __function__))
   (b*
     (((er (list rewritten-term used-rules))
       (trans-eval-error-triple
            (cons *solve-call-acl2-rewriter*
                  (append (kwote-lst (list matrix method-rules ctx))
                          '(state)))
            ctx state))
      ((er f-body)
       (solve-gen-solution-from-rewritten-term
            matrix
            rewritten-term ?f x1...xn ctx state))
      ((mv rewriting-theorem-event
           rewriting-theorem names-to-avoid)
       (solve-gen-acl2-rewriter-theorem
            matrix rewritten-term
            used-rules names-to-avoid (w state)))
      ((mv f-local-event f-exported-event)
       (solve-gen-f f x1...xn f-body solution-guard
                    solution-guard-hints solution-enable
                    verify-guards (w state)))
      ((mv solution-theorem-events solution-theorem
           old-instance names-to-avoid)
       (solve-gen-solution-theorem-from-rewriting-theorem
            old x1...xn ?f f rewriting-theorem
            print names-to-avoid (w state))))
     (value (list (list* rewriting-theorem-event
                         f-local-event solution-theorem-events)
                  (list f-exported-event)
                  solution-theorem
                  old-instance names-to-avoid)))))