		Search-engine friendly clone of the ACL2 documentation.

Solve-event-generation

Solve-gen-solution-axe-rewriter

Attempt to generate a solution using the Axe rewriter.

Signature
(solve-gen-solution-axe-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-form-listp) (exported-events pseudo-form-listp) (solution-theorem symbolp) (old-instance symbolp) (updated-names-to-avoid symbol-listp) result).

This is analogous to solve-gen-solution-ACL2-rewriter. See that function for more details.

Definitions and Theorems

Function: solve-gen-solution-axe-rewriter

(defun solve-gen-solution-axe-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-axe-rewriter))
   (declare (ignorable __function__))
   (b*
     (((er rewritten-term)
       (trans-eval-error-triple
            (cons *solve-call-axe-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-axe-rewriter-theorem
            matrix rewritten-term
            method-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)))))