summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/combination_engine.cpp4
-rw-r--r--src/theory/combination_engine.h7
-rw-r--r--src/theory/model_manager.cpp4
-rw-r--r--src/theory/model_manager.h5
-rw-r--r--src/theory/sort_inference.h10
-rw-r--r--src/theory/theory_engine.cpp4
-rw-r--r--src/theory/theory_engine.h8
-rw-r--r--src/theory/theory_model.cpp2
-rw-r--r--src/theory/theory_model.h5
-rw-r--r--src/theory/theory_model_builder.cpp2
-rw-r--r--src/theory/theory_model_builder.h6
-rw-r--r--src/theory/theory_state.cpp2
-rw-r--r--src/theory/theory_state.h5
13 files changed, 27 insertions, 37 deletions
diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index 609f8d9d6..9352ce95c 100644
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -32,8 +32,8 @@ CombinationEngine::CombinationEngine(TheoryEngine& te,
Env& env,
const std::vector<Theory*>& paraTheories,
ProofNodeManager* pnm)
- : d_te(te),
- d_env(env),
+ : EnvObj(env),
+ d_te(te),
d_valuation(&te),
d_pnm(pnm),
d_logicInfo(te.getLogicInfo()),
diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h
index 7f04ccd75..f7da01fac 100644
--- a/src/theory/combination_engine.h
+++ b/src/theory/combination_engine.h
@@ -18,9 +18,10 @@
#ifndef CVC5__THEORY__COMBINATION_ENGINE__H
#define CVC5__THEORY__COMBINATION_ENGINE__H
-#include <vector>
#include <memory>
+#include <vector>
+#include "smt/env_obj.h"
#include "theory/ee_manager.h"
#include "theory/valuation.h"
@@ -42,7 +43,7 @@ class SharedSolver;
* mode, and
* (2) Implementing the main combination method (combineTheories).
*/
-class CombinationEngine
+class CombinationEngine : protected EnvObj
{
public:
CombinationEngine(TheoryEngine& te,
@@ -107,8 +108,6 @@ class CombinationEngine
virtual eq::EqualityEngineNotify* getModelEqualityEngineNotify();
/** Reference to the theory engine */
TheoryEngine& d_te;
- /** Reference to the environment */
- Env& d_env;
/** Valuation for the engine */
Valuation d_valuation;
/** The proof node manager */
diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index 29c4bf169..2b746cba1 100644
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -28,8 +28,8 @@ namespace cvc5 {
namespace theory {
ModelManager::ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem)
- : d_te(te),
- d_env(env),
+ : EnvObj(env),
+ d_te(te),
d_eem(eem),
d_modelEqualityEngine(nullptr),
d_modelEqualityEngineAlloc(nullptr),
diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h
index fd8ca6e11..2a62c8be0 100644
--- a/src/theory/model_manager.h
+++ b/src/theory/model_manager.h
@@ -20,6 +20,7 @@
#include <memory>
+#include "smt/env_obj.h"
#include "theory/ee_manager.h"
#include "theory/logic_info.h"
@@ -40,7 +41,7 @@ class TheoryModel;
* method is a manager-specific way for setting up the equality engine of the
* model in preparation for model building.
*/
-class ModelManager
+class ModelManager : protected EnvObj
{
public:
ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem);
@@ -111,8 +112,6 @@ class ModelManager
/** Reference to the theory engine */
TheoryEngine& d_te;
- /** Reference to the environment */
- Env& d_env;
/** The equality engine manager */
EqEngineManager& d_eem;
/**
diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h
index 279be5e10..126c94749 100644
--- a/src/theory/sort_inference.h
+++ b/src/theory/sort_inference.h
@@ -23,6 +23,7 @@
#include "expr/node.h"
#include "expr/type_node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
@@ -38,8 +39,9 @@ namespace theory {
* "Sort it out with Monotonicity" Claessen 2011
* "Non-Cyclic Sorts for First-Order Satisfiability" Korovin 2013.
*/
-class SortInference {
-private:
+class SortInference : protected EnvObj
+{
+ private:
//all subsorts
std::vector< int > d_sub_sorts;
std::map< int, bool > d_non_monotonic_sorts;
@@ -66,8 +68,6 @@ public:
};
private:
- /** Reference to the env */
- Env& d_env;
/** the id count for all subsorts we have allocated */
int d_sortCount;
UnionFind d_type_union_find;
@@ -111,7 +111,7 @@ private:
void reset();
public:
- SortInference(Env& env) : d_env(env), d_sortCount(1) {}
+ SortInference(Env& env) : EnvObj(env), d_sortCount(1) {}
~SortInference(){}
/** initialize
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index cd9445bb0..72f3d78ac 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -219,8 +219,8 @@ context::UserContext* TheoryEngine::getUserContext() const
}
TheoryEngine::TheoryEngine(Env& env)
- : d_propEngine(nullptr),
- d_env(env),
+ : EnvObj(env),
+ d_propEngine(nullptr),
d_logicInfo(env.getLogicInfo()),
d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
: nullptr),
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 5c44f8968..496966149 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -26,6 +26,7 @@
#include "expr/node.h"
#include "options/theory_options.h"
#include "proof/trust_node.h"
+#include "smt/env_obj.h"
#include "theory/atom_requests.h"
#include "theory/engine_output_channel.h"
#include "theory/interrupted.h"
@@ -98,7 +99,7 @@ class PropEngine;
* T-solvers look like a single unit to the propositional part of
* cvc5.
*/
-class TheoryEngine
+class TheoryEngine : protected EnvObj
{
/** Shared terms database can use the internals notify the theories */
friend class SharedTermsDatabase;
@@ -529,11 +530,6 @@ class TheoryEngine
prop::PropEngine* d_propEngine;
/**
- * Reference to the environment.
- */
- Env& d_env;
-
- /**
* A table of from theory IDs to theory pointers. Never use this table
* directly, use theoryOf() instead.
*/
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 291cd1905..4cc25a887 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -33,7 +33,7 @@ namespace cvc5 {
namespace theory {
TheoryModel::TheoryModel(Env& env, std::string name, bool enableFuncModels)
- : d_env(env),
+ : EnvObj(env),
d_name(name),
d_equalityEngine(nullptr),
d_using_model_core(false),
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 6841a11d8..4a6492aaa 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -21,6 +21,7 @@
#include <unordered_map>
#include <unordered_set>
+#include "smt/env_obj.h"
#include "theory/ee_setup_info.h"
#include "theory/rep_set.h"
#include "theory/type_enumerator.h"
@@ -79,7 +80,7 @@ namespace theory {
* above functions such as getRepresentative() when assigning total
* interpretations for uninterpreted functions.
*/
-class TheoryModel
+class TheoryModel : protected EnvObj
{
friend class TheoryEngineModelBuilder;
@@ -357,8 +358,6 @@ class TheoryModel
std::string debugPrintModelEqc() const;
protected:
- /** Reference to the environmanet */
- Env& d_env;
/** Unique name of this model */
std::string d_name;
/** equality engine containing all known equalities/disequalities */
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 2acbe2388..23a76d273 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -32,7 +32,7 @@ using namespace cvc5::context;
namespace cvc5 {
namespace theory {
-TheoryEngineModelBuilder::TheoryEngineModelBuilder(Env& env) : d_env(env) {}
+TheoryEngineModelBuilder::TheoryEngineModelBuilder(Env& env) : EnvObj(env) {}
void TheoryEngineModelBuilder::Assigner::initialize(
TypeNode tn, TypeEnumeratorProperties* tep, const std::vector<Node>& aes)
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index 71458a913..dd11a3d2e 100644
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -21,6 +21,7 @@
#include <unordered_map>
#include <unordered_set>
+#include "smt/env_obj.h"
#include "theory/theory_model.h"
namespace cvc5 {
@@ -42,7 +43,7 @@ namespace theory {
* this will set up the data structures in TheoryModel to represent
* a model for the current set of assertions.
*/
-class TheoryEngineModelBuilder
+class TheoryEngineModelBuilder : protected EnvObj
{
typedef std::unordered_map<Node, Node> NodeMap;
typedef std::unordered_set<Node> NodeSet;
@@ -315,9 +316,6 @@ class TheoryEngineModelBuilder
Node v,
std::map<Node, bool>& visited);
//---------------------------------end for debugging finite model finding
- /** Reference to the env */
- Env& d_env;
-
}; /* class TheoryEngineModelBuilder */
} // namespace theory
diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp
index 72ab24a7e..e3655e3ab 100644
--- a/src/theory/theory_state.cpp
+++ b/src/theory/theory_state.cpp
@@ -21,7 +21,7 @@ namespace cvc5 {
namespace theory {
TheoryState::TheoryState(Env& env, Valuation val)
- : d_env(env),
+ : EnvObj(env),
d_valuation(val),
d_ee(nullptr),
d_conflict(d_env.getContext(), false)
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index cc58347bf..9162fdeb6 100644
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -21,6 +21,7 @@
#include "context/cdo.h"
#include "expr/node.h"
#include "smt/env.h"
+#include "smt/env_obj.h"
#include "theory/valuation.h"
namespace cvc5 {
@@ -30,7 +31,7 @@ namespace eq {
class EqualityEngine;
}
-class TheoryState
+class TheoryState : protected EnvObj
{
public:
TheoryState(Env& env,
@@ -117,8 +118,6 @@ class TheoryState
Valuation& getValuation();
protected:
- /** Reference to the environment. */
- Env& d_env;
/**
* The valuation proxy for the Theory to communicate back with the
* theory engine (and other theories).
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback