		Search-engine friendly clone of the ACL2 documentation.

Solve-implementation

Solve-call-ACL2-rewriter

Call the ACL2 rewriter on the matrix of old.

Signature
(solve-call-acl2-rewriter matrix method-rules ctx state) → (mv erp result state)
Arguments: matrix — Guard (pseudo-termp matrix).; method-rules — Guard (symbol-listp method-rules).
Returns: result — A tuple (rewritten-term used-rules) satisfying (typed-tuplep pseudo-termp symbol-listp result).

Definitions and Theorems

Function: solve-call-acl2-rewriter

(defun solve-call-acl2-rewriter (matrix method-rules ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp matrix)
                             (symbol-listp method-rules))))
 (let ((__function__ 'solve-call-acl2-rewriter))
  (declare (ignorable __function__))
  (b*
   (((er (list* rewritten-term used-rules pairs))
     (rewrite$ matrix
               :ctx ctx
               :in-theory (cons 'enable method-rules)))
    ((unless (null pairs))
     (value
      (raise
       "Internal error: ~
                       REWRITE$ returned non-NIL pairs ~x0 ~
                       even though it was called without forced assumptions."
       pairs))))
   (value (list rewritten-term used-rules)))))