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, 15 insertions, 0 deletions

diff --git a/src/smt/env_obj.cpp b/src/smt/env_obj.cpp
index fcbcc92d2..b9aebbe83 100644
--- a/src/smt/env_obj.cpp
+++ b/src/smt/env_obj.cpp
@@ -33,6 +33,21 @@ Node EnvObj::extendedRewrite(TNode node, bool aggr) const
 {
   return d_env.getRewriter()->extendedRewrite(node, aggr);
 }
+Node EnvObj::evaluate(TNode n,
+                      const std::vector<Node>& args,
+                      const std::vector<Node>& vals,
+                      bool useRewriter) const
+{
+  return d_env.evaluate(n, args, vals, useRewriter);
+}
+Node EnvObj::evaluate(TNode n,
+                      const std::vector<Node>& args,
+                      const std::vector<Node>& vals,
+                      const std::unordered_map<Node, Node>& visited,
+                      bool useRewriter) const
+{
+  return d_env.evaluate(n, args, vals, visited, useRewriter);
+}
 
 const LogicInfo& EnvObj::logicInfo() const { return d_env.getLogicInfo(); }