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.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4bce6f0d2b5aede419e0e019ee2a1b7c52441e96..001a8bbc7c8d13903482b529f8a785d49846ea77 100644 (file)
--- 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 786cdcab2f3b0d50447c7e7356c116289bf6ea6f..e54f12fa5853b3863806dae405abcec071227e30 100644 (file)
--- 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 (file)
index 0000000..2a9cd28
--- /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 (file)
index 0000000..69aab76
--- /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