		Search-engine friendly clone of the ACL2 documentation.

Solve-event-generation

Solve-gen-solution

Attempt to generate the events that provide the solution.

Signature
(solve-gen-solution old ?f x1...xn matrix method method-rules f f-existsp solution-enable solution-guard solution-guard-hints solution-body solution-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 — Guard (keywordp method).; method-rules — Guard (symbol-listp method-rules).; f — Guard (symbolp f).; f-existsp — Guard (booleanp f-existsp).; solution-enable — Guard (booleanp solution-enable).; solution-guard — An untranslated term.; solution-guard-hints — Guard (true-listp solution-guard-hints).; solution-body — An untranslated term.; solution-hints — Guard (true-listp solution-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).

These are events that depend on the solving method. In contrast, the events for new and old-if-new are the same for every method.

Definitions and Theorems

Function: solve-gen-solution

(defun solve-gen-solution
       (old ?f x1...xn matrix method method-rules f
            f-existsp solution-enable solution-guard
            solution-guard-hints solution-body
            solution-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)
                              (keywordp method)
                              (symbol-listp method-rules)
                              (symbolp f)
                              (booleanp f-existsp)
                              (booleanp solution-enable)
                              (true-listp solution-guard-hints)
                              (true-listp solution-hints)
                              (booleanp verify-guards)
                              (evmac-input-print-p print)
                              (symbol-listp names-to-avoid))))
  (let ((__function__ 'solve-gen-solution))
    (declare (ignorable __function__))
    (case method
      (:acl2-rewriter (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))
      (:axe-rewriter (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))
      (:manual (solve-gen-solution-manual
                    old ?f x1...xn matrix f
                    f-existsp solution-enable solution-guard
                    solution-guard-hints solution-body
                    solution-hints verify-guards
                    print names-to-avoid state))
      (t (value (raise "Internal error: unknown method ~x0."
                       method))))))