Towards standard usage of ExtendedRewriter (#7145)

This PR:

Adds extendedRewrite to EnvObj and Rewriter.
Eliminates static calls to Rewriter::rewrite from within the extended rewriter. Instead, the use of extended rewriter is always through Rewriter, which passes itself to the ExtendedRewriter.
Make most uses of extended rewriter non-static. I've added a placeholder method Rewriter::callExtendedRewrite for places in the code that call the extended rewriter are currently difficult to eliminate.

1 files changed, 3 insertions, 3 deletions

diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp
index a36388c26..7242be54c 100644
--- a/src/preprocessing/passes/extended_rewriter_pass.cpp
+++ b/src/preprocessing/passes/extended_rewriter_pass.cpp
@@ -20,7 +20,6 @@
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "theory/quantifiers/extended_rewrite.h"
 
 namespace cvc5 {
 namespace preprocessing {
@@ -32,11 +31,12 @@ ExtRewPre::ExtRewPre(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult ExtRewPre::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  theory::quantifiers::ExtendedRewriter extr(options::extRewPrepAgg());
   for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
     assertionsToPreprocess->replace(
-        i, extr.extendedRewrite((*assertionsToPreprocess)[i]));
+        i,
+        extendedRewrite((*assertionsToPreprocess)[i],
+                        options::extRewPrepAgg()));
   }
   return PreprocessingPassResult::NO_CONFLICT;
 }