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, 7 deletions

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index d71b3635b..1309a05f9 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -18,10 +18,10 @@
 #include "expr/skolem_manager.h"
 #include "smt/env.h"
 #include "smt/term_formula_removal.h"
-#include "theory/evaluator.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory.h"
+#include "util/rational.h"
 
 using namespace cvc5::kind;
 
@@ -67,7 +67,7 @@ Node BuiltinProofRuleChecker::applySubstitutionRewrite(
     MethodId idr)
 {
   Node nks = applySubstitution(n, exp, ids, ida);
-  return d_env.getRewriter()->rewriteViaMethod(nks, idr);
+  return d_env.rewriteViaMethod(nks, idr);
 }
 
 bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp,
@@ -249,7 +249,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     {
       return Node::null();
     }
-    Node res = d_env.getRewriter()->rewriteViaMethod(args[0], idr);
+    Node res = d_env.rewriteViaMethod(args[0], idr);
     if (res.isNull())
     {
       return Node::null();
@@ -260,7 +260,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
   {
     Assert(children.empty());
     Assert(args.size() == 1);
-    Node res = d_env.getRewriter()->rewriteViaMethod(args[0], MethodId::RW_EVALUATE);
+    Node res = d_env.rewriteViaMethod(args[0], MethodId::RW_EVALUATE);
     if (res.isNull())
     {
       return Node::null();
@@ -302,7 +302,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
                              << SkolemManager::getOriginalForm(res) << std::endl;
     // **** NOTE: can rewrite the witness form here. This enables certain lemmas
     // to be provable, e.g. (= k t) where k is a purification Skolem for t.
-    res = Rewriter::rewrite(SkolemManager::getOriginalForm(res));
+    res = d_env.getRewriter()->rewrite(SkolemManager::getOriginalForm(res));
     if (!res.isConst() || !res.getConst<bool>())
     {
       Trace("builtin-pfcheck")
@@ -349,8 +349,8 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     if (res1 != res2)
     {
       // can rewrite the witness forms
-      res1 = Rewriter::rewrite(SkolemManager::getOriginalForm(res1));
-      res2 = Rewriter::rewrite(SkolemManager::getOriginalForm(res2));
+      res1 = d_env.getRewriter()->rewrite(SkolemManager::getOriginalForm(res1));
+      res2 = d_env.getRewriter()->rewrite(SkolemManager::getOriginalForm(res2));
       if (res1.isNull() || res1 != res2)
       {
         Trace("builtin-pfcheck") << "Failed to match results" << std::endl;