diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 127 |
1 files changed, 67 insertions, 60 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index dd130e28a..d1cc4dfc1 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -65,20 +65,20 @@ namespace theory { * Do not change this order. */ -#define CVC4_FOR_EACH_THEORY \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BUILTIN) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BOOL) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_UF) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_ARITH) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BV) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_FP) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_ARRAYS) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_DATATYPES) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_SEP) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_SETS) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BAGS) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_STRINGS) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_QUANTIFIERS) +#define CVC5_FOR_EACH_THEORY \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BUILTIN) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BOOL) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_UF) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_ARITH) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BV) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_FP) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_ARRAYS) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_DATATYPES) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_SEP) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_SETS) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BAGS) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_STRINGS) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_QUANTIFIERS) } // namespace theory @@ -128,12 +128,12 @@ void TheoryEngine::finishInit() { // NOTE: This seems to be required since // theory::TheoryTraits<THEORY>::isParametric cannot be accessed without - // using the CVC4_FOR_EACH_THEORY_STATEMENT macro. -AJR + // using the CVC5_FOR_EACH_THEORY_STATEMENT macro. -AJR std::vector<theory::Theory*> paraTheories; -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::isParametric \ && d_logicInfo.isTheoryEnabled(THEORY)) \ { \ @@ -141,7 +141,7 @@ void TheoryEngine::finishInit() } // Collect the parametric theories, which are given to the theory combination // manager below - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; // Initialize the theory combination architecture if (options::tcMode() == options::TcMode::CARE_GRAPH) @@ -411,10 +411,10 @@ void TheoryEngine::check(Theory::Effort effort) { // Reset the interrupt flag d_interrupted = false; -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasCheck \ && d_logicInfo.isTheoryEnabled(THEORY)) \ { \ @@ -471,7 +471,7 @@ void TheoryEngine::check(Theory::Effort effort) { d_factsAsserted = false; // Do the checking - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << endl; @@ -562,19 +562,21 @@ void TheoryEngine::propagate(Theory::Effort effort) d_interrupted = false; // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \ - theoryOf(THEORY)->propagate(effort); \ +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasPropagate \ + && d_logicInfo.isTheoryEnabled(THEORY)) \ + { \ + theoryOf(THEORY)->propagate(effort); \ } // Reset the interrupt flag d_interrupted = false; // Propagate for each theory using the statement above - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; } Node TheoryEngine::getNextDecisionRequest() @@ -665,19 +667,21 @@ bool TheoryEngine::presolve() { try { // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasPresolve) { \ - theoryOf(THEORY)->presolve(); \ - if(d_inConflict) { \ - return true; \ - } \ - } +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasPresolve) \ + { \ + theoryOf(THEORY)->presolve(); \ + if (d_inConflict) \ + { \ + return true; \ + } \ + } // Presolve for each theory using the statement above - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl; } @@ -690,14 +694,14 @@ void TheoryEngine::postsolve() { d_inSatMode = false; // Reset the interrupt flag d_interrupted = false; - bool CVC4_UNUSED wasInConflict = d_inConflict; + bool CVC5_UNUSED wasInConflict = d_inConflict; try { // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasPostsolve) \ { \ theoryOf(THEORY)->postsolve(); \ @@ -706,7 +710,7 @@ void TheoryEngine::postsolve() { } // Postsolve for each theory using the statement above - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::postsolve() => interrupted" << endl; } @@ -718,16 +722,18 @@ void TheoryEngine::notifyRestart() { d_interrupted = false; // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \ - theoryOf(THEORY)->notifyRestart(); \ +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasNotifyRestart \ + && d_logicInfo.isTheoryEnabled(THEORY)) \ + { \ + theoryOf(THEORY)->notifyRestart(); \ } // notify each theory using the statement above - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; } void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder& learned) @@ -736,16 +742,17 @@ void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder& learned) d_interrupted = false; // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) { \ - theoryOf(THEORY)->ppStaticLearn(in, learned); \ +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) \ + { \ + theoryOf(THEORY)->ppStaticLearn(in, learned); \ } // static learning for each theory using the statement above - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; } bool TheoryEngine::isRelevant(Node lit) const @@ -1089,14 +1096,14 @@ void TheoryEngine::declareSepHeap(TypeNode locT, TypeNode dataT) } // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ theoryOf(THEORY)->declareSepHeap(locT, dataT); // notify each theory using the statement above - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; // remember the types we have set d_sepLocType = locT; |