diff options
author | Tim King <taking@google.com> | 2017-03-27 12:26:14 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2017-03-27 12:26:14 -0700 |
commit | f49ddf87046793972a7f6a1bdae15003709f08d2 (patch) | |
tree | b008e40a4e29be9455bc09a65bf2437588900104 /src/theory/theory.cpp | |
parent | 4930de53415ffbf614d6965af59b1f44e405451c (diff) |
Making the ExtTheory object a private member of Theory.
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r-- | src/theory/theory.cpp | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index ab72bf55f..3aa468e01 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -66,7 +66,7 @@ Theory::Theory(TheoryId id, context::Context* satContext, , d_sharedTermsIndex(satContext, 0) , d_careGraph(NULL) , d_quantEngine(NULL) - , d_extt(NULL) + , d_extTheory(NULL) , d_checkTime(getFullInstanceName() + "::checkTime") , d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime") , d_sharedTerms(satContext) @@ -81,6 +81,8 @@ Theory::Theory(TheoryId id, context::Context* satContext, Theory::~Theory() { smtStatisticsRegistry()->unregisterStat(&d_checkTime); smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime); + + delete d_extTheory; } TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { @@ -296,6 +298,11 @@ std::pair<bool, Node> Theory::entailmentCheck( return make_pair(false, Node::null()); } +ExtTheory* Theory::getExtTheory() { + Assert(d_extTheory != NULL); + return d_extTheory; +} + void Theory::addCarePair(TNode t1, TNode t2) { if (d_careGraph) { d_careGraph->insert(CarePair(t1, t2, d_id)); @@ -312,6 +319,18 @@ void Theory::getCareGraph(CareGraph* careGraph) { d_careGraph = NULL; } +void Theory::setQuantifiersEngine(QuantifiersEngine* qe) { + Assert(d_quantEngine == NULL); + Assert(qe != NULL); + d_quantEngine = qe; +} + +void Theory::setupExtTheory() { + Assert(d_extTheory == NULL); + d_extTheory = new ExtTheory(this); +} + + EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid) : d_tid(tid) { } |