From 9f48eb94a7a72338283492169a0d494fcdc57034 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 1 Sep 2021 19:10:42 -0700
Subject: [PATCH] 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.
---
 src/CMakeLists.txt  |  2 ++
 src/smt/env.h       |  2 +-
 src/smt/env_obj.cpp | 29 +++++++++++++++++++++++++
 src/smt/env_obj.h   | 53 +++++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 85 insertions(+), 1 deletion(-)
 create mode 100644 src/smt/env_obj.cpp
 create mode 100644 src/smt/env_obj.h

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
-- 
2.30.2