diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-11-26 17:07:46 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-11-26 17:07:46 +0000 |
commit | 2a731b9164bb178f1232a9af0babc7dd84450cea (patch) | |
tree | 57d14d55f1bae93737dbee34c737771858572fad /src/theory/theory_engine.cpp | |
parent | 164163c9c8fd255947cf3e8d236a5b9da1a1fdab (diff) |
Adding support for a master equality engine. Each theory gets the master equality engine through the setMasterEqualityEngine method. This is a read-only equality engine, so nothing should be added to it directly. Instead each equality engine that is of interest should have the master equality engine attached to it. To set when to use the master equality engine see TheoryEngine::finishInit().
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 32 |
1 files changed, 17 insertions, 15 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 4b4316db1..cd3b34879 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -42,12 +42,26 @@ #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/uf/equality_engine.h" using namespace std; using namespace CVC4; using namespace CVC4::theory; +void TheoryEngine::finishInit() { + if (d_logicInfo.isQuantified()) { + Assert(d_masterEqualityEngine == 0); + d_masterEqualityEngine = new eq::EqualityEngine(getSatContext(), "theory::master"); + + for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { + if (d_theoryTable[theoryId]) { + d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine); + } + } + } +} + TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveITE& iteRemover, @@ -58,6 +72,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_userContext(userContext), d_logicInfo(logicInfo), d_sharedTerms(this, context), + d_masterEqualityEngine(NULL), d_quantEngine(NULL), d_curr_model(NULL), d_curr_model_builder(NULL), @@ -114,6 +129,8 @@ TheoryEngine::~TheoryEngine() { delete d_quantEngine; + delete d_masterEqualityEngine; + StatisticsRegistry::unregisterStat(&d_combineTheoriesTime); } @@ -229,21 +246,6 @@ void TheoryEngine::dumpAssertions(const char* tag) { } } - -template<typename T, bool doAssert> -class scoped_vector_clear { - vector<T>& d_v; -public: - scoped_vector_clear(vector<T>& v) - : d_v(v) { - Assert(!doAssert || d_v.empty()); - } - ~scoped_vector_clear() { - d_v.clear(); - } - -}; - /** * Check all (currently-active) theories for conflicts. * @param effort the effort level to use |