Add class EnvObj. (#7113)

This class will serve as base class for classes that need access to the
environment. This does not yet have classes derive from this base class.

Will update #7110 and #7112 to use this after this is in.

4 files changed, 85 insertions, 1 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4bce6f0d2..001a8bbc7 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -294,6 +294,8 @@ libcvc5_add_sources(
   smt/dump_manager.h
   smt/env.cpp
   smt/env.h
+  smt/env_obj.cpp
+  smt/env_obj.h
   smt/expand_definitions.cpp
   smt/expand_definitions.h
   smt/listeners.cpp
diff --git a/src/smt/env.h b/src/smt/env.h
index 786cdcab2..e54f12fa5 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -14,7 +14,7 @@
  * internal code
  */
 
-#include "cvc5_public.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__SMT__ENV_H
 #define CVC5__SMT__ENV_H
diff --git a/src/smt/env_obj.cpp b/src/smt/env_obj.cpp
new file mode 100644
index 000000000..2a9cd285f
--- /dev/null
+++ b/src/smt/env_obj.cpp
@@ -0,0 +1,29 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The base class for everything that nees access to the environment (Env)
+ * instance, which gives access to global utilities available to internal code.
+ */
+
+#include "smt/env_obj.h"
+
+#include "options/options.h"
+#include "smt/env.h"
+#include "theory/rewriter.h"
+
+namespace cvc5 {
+
+EnvObj::EnvObj(Env& env) : d_env(env) {}
+
+Node EnvObj::rewrite(TNode node) { return d_env.getRewriter()->rewrite(node); }
+
+}  // namespace cvc5
diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h
new file mode 100644
index 000000000..69aab7647
--- /dev/null
+++ b/src/smt/env_obj.h
@@ -0,0 +1,53 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The base class for everything that nees access to the environment (Env)
+ * instance, which gives access to global utilities available to internal code.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__SMT__ENV_OBJ_H
+#define CVC5__SMT__ENV_OBJ_H
+
+#include <memory>
+
+#include "expr/node.h"
+
+namespace cvc5 {
+
+class Env;
+class NodeManager;
+class Options;
+
+class EnvObj
+{
+ public:
+  /** Constructor. */
+  EnvObj(Env& env);
+  EnvObj() = delete;
+  /** Destructor.  */
+  ~EnvObj() {}
+
+  /**
+   * Rewrite a node.
+   * This is a wrapper around theory::Rewriter::rewrite via Env.
+   */
+  Node rewrite(TNode node);
+
+ protected:
+  /** The associated environment. */
+  Env& d_env;
+};
+
+}  // namespace cvc5
+#endif