Call the ACL2 rewriter on the matrix of
(solve-call-acl2-rewriter matrix method-rules ctx state) → (mv erp result state)
Function:
(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)))))