		Search-engine friendly clone of the ACL2 documentation.

Solve-event-generation

Solve-gen-solution-manual

Attempt to generate the events that provide the solution, when using the manual method.

Signature
(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) → (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).; 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).

Definitions and Theorems

Function: solve-gen-solution-manual

(defun 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)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old)
                             (symbolp ?f)
                             (symbol-listp x1...xn)
                             (pseudo-termp matrix)
                             (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-manual))
  (declare (ignorable __function__))
  (b*
    ((wrld (w state))
     ((mv appcond names-to-avoid)
      (fresh-logical-name-with-$s-suffix 'appcond
                                         nil names-to-avoid wrld))
     ((mv old-instance names-to-avoid)
      (fresh-logical-name-with-$s-suffix 'old-instance
                                         'function
                                         names-to-avoid wrld))
     ((mv solution-theorem names-to-avoid)
      (fresh-logical-name-with-$s-suffix 'solution-theorem
                                         nil names-to-avoid wrld)))
   (if f-existsp
    (b*
     ((appcond-event
       (cons
        'local
        (cons (cons 'defthmd
                    (cons appcond
                          (cons (sublis-fn-simple (list (cons ?f f))
                                                  matrix)
                                (cons ':hints
                                      (cons solution-hints 'nil)))))
              'nil)))
      (old-instance-event
       (cons
        'local
        (cons
            (cons 'soft::defun-inst
                  (cons old-instance
                        (cons (cons old (cons (cons ?f f) 'nil))
                              (cons ':print
                                    (cons (and (eq print :all) :all)
                                          'nil)))))
            'nil)))
      (solution-theorem-event
       (cons
        'local
        (cons
         (cons
          'defthm
          (cons
           solution-theorem
           (cons
            (cons old-instance 'nil)
            (cons
             ':hints
             (cons
              (cons
               (cons
                '"Goal"
                (cons
                 ':in-theory
                 (cons
                  (cons
                       'quote
                       (cons (cons old-instance (cons appcond 'nil))
                             'nil))
                  'nil)))
               'nil)
              'nil)))))
         'nil))))
     (value (list (list appcond-event old-instance-event
                        solution-theorem-event)
                  nil solution-theorem names-to-avoid)))
    (b*
     ((f-body solution-body)
      ((mv & matrix-instance)
       (acl2::fsublis-fn-rec
            (list (cons ?f (make-lambda x1...xn solution-body)))
            matrix nil nil))
      (appcond-event
       (cons
        'local
        (cons (cons 'defthmd
                    (cons appcond
                          (cons matrix-instance
                                (cons ':hints
                                      (cons solution-hints 'nil)))))
              'nil)))
      ((mv f-local-event f-exported-event)
       (solve-gen-f f x1...xn f-body
                    solution-guard solution-guard-hints
                    solution-enable verify-guards wrld))
      (old-instance-event
       (cons
        'local
        (cons
            (cons 'soft::defun-inst
                  (cons old-instance
                        (cons (cons old (cons (cons ?f f) 'nil))
                              (cons ':print
                                    (cons (and (eq print :all) :all)
                                          'nil)))))
            'nil)))
      (solution-theorem-event
       (cons
        'local
        (cons
         (cons
          'defthm
          (cons
           solution-theorem
           (cons
            (cons old-instance 'nil)
            (cons
             ':hints
             (cons
              (cons
               (cons
                '"Goal"
                (cons
                 ':in-theory
                 (cons
                     (cons 'quote
                           (cons (cons old-instance
                                       (cons f (cons appcond 'nil)))
                                 'nil))
                     'nil)))
               'nil)
              'nil)))))
         'nil))))
     (value (list (list appcond-event
                        f-local-event old-instance-event
                        solution-theorem-event)
                  (list f-exported-event)
                  solution-theorem
                  old-instance names-to-avoid)))))))