Towards standard usage of evaluator (#7189)

This makes the evaluator accessible via EnvObj through the Rewriter. It furthermore removes Rewriter::rewrite from inside the evaluator itself.

Construction of Evaluator utilities is now discouraged.

The include dependencies were cleaned slightly in this PR, leading to more precise includes throughout.

This is work towards having a configurable cardinality for strings, as well as eliminating SmtEngineScope.

1 files changed, 7 insertions, 13 deletions

diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index d87043a67..697253e03 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -18,22 +18,24 @@
 #pragma once
 
 #include "expr/node.h"
-#include "proof/method_id.h"
 #include "theory/theory_rewriter.h"
 
 namespace cvc5 {
 
+class Env;
 class TConvProofGenerator;
 class ProofNodeManager;
 class TrustNode;
 
 namespace theory {
 
+class Evaluator;
+
 /**
  * The main rewriter class.
  */
 class Rewriter {
-
+  friend class cvc5::Env;  // to initialize the evaluators of this class
  public:
   Rewriter();
 
@@ -62,6 +64,9 @@ class Rewriter {
   Node rewriteEqualityExt(TNode node);
 
   /**
+   * !!! Temporary until static access to rewriter is eliminated. This method
+   * should be moved to same place as evaluate (currently in Env).
+   *
    * Extended rewrite of the given node. This method is implemented by a
    * custom ExtendRewriter class that wraps this class to perform custom
    * rewrites (usually those that are not useful for solving, but e.g. useful
@@ -103,17 +108,6 @@ class Rewriter {
   /** Get the theory rewriter for the given id */
   TheoryRewriter* getTheoryRewriter(theory::TheoryId theoryId);
 
-  /**
-   * Apply rewrite on n via the rewrite method identifier idr (see method_id.h).
-   * This encapsulates the exact behavior of a REWRITE step in a proof.
-   *
-   * @param n The node to rewrite,
-   * @param idr The method identifier of the rewriter, by default RW_REWRITE
-   * specifying a call to rewrite.
-   * @return The rewritten form of n.
-   */
-  Node rewriteViaMethod(TNode n, MethodId idr = MethodId::RW_REWRITE);
-
  private:
   /**
    * Get the rewriter associated with the SmtEngine in scope.