diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 31 |
1 files changed, 25 insertions, 6 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index cf105803c..db22d8981 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -68,7 +68,9 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { d_engine->getSharedTermManager()->addEq(fact); } - if(Options::current()->theoryRegistration && !fact.getAttribute(RegisteredAttr())) { + if(Options::current()->theoryRegistration && + !fact.getAttribute(RegisteredAttr()) && + d_engine->d_needRegistration) { list<TNode> toReg; toReg.push_back(fact); @@ -137,6 +139,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt) : d_propEngine(NULL), d_context(ctxt), d_activeTheories(0), + d_needRegistration(false), d_theoryOut(this, ctxt), d_hasShutDown(false), d_incomplete(ctxt, false), @@ -272,7 +275,7 @@ bool TheoryEngine::check(theory::Theory::Effort effort) { // Do the checking try { - CVC4_FOR_EACH_THEORY + CVC4_FOR_EACH_THEORY; } catch(const theory::Interrupted&) { Debug("theory") << "TheoryEngine::check() => conflict" << std::endl; } @@ -291,7 +294,7 @@ void TheoryEngine::propagate() { } // Propagate for each theory using the statement above - CVC4_FOR_EACH_THEORY + CVC4_FOR_EACH_THEORY; } /* Our goal is to tease out any ITE's sitting under a theory operator. */ @@ -389,7 +392,7 @@ bool TheoryEngine::presolve() { } // Presolve for each theory using the statement above - CVC4_FOR_EACH_THEORY + CVC4_FOR_EACH_THEORY; } catch(const theory::Interrupted&) { Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl; } @@ -409,7 +412,7 @@ void TheoryEngine::notifyRestart() { } // notify each theory using the statement above - CVC4_FOR_EACH_THEORY + CVC4_FOR_EACH_THEORY; } void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) { @@ -429,7 +432,23 @@ void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) { } // static learning for each theory using the statement above - CVC4_FOR_EACH_THEORY + CVC4_FOR_EACH_THEORY; +} + +bool TheoryEngine::hasRegisterTerm(TheoryId th) const { + switch(th) { + // Definition of the statement that is to be run by every theory +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + case THEORY: \ + return theory::TheoryTraits<THEORY>::hasRegisterTerm; + + CVC4_FOR_EACH_THEORY + default: + Unhandled(th); + } } Node TheoryEngine::simplify(TNode in, theory::Substitutions& outSubstitutions) { |