diff options
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r-- | src/theory/theory.cpp | 64 |
1 files changed, 27 insertions, 37 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 1dd0a1209..1301da653 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -78,21 +78,21 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { break; case THEORY_OF_TERM_BASED: // Variables - if (node.getMetaKind() == kind::metakind::VARIABLE) { - if (theoryOf(node.getType()) != theory::THEORY_BOOL) { + if (node.getMetaKind() == kind::metakind::VARIABLE) { + if (theoryOf(node.getType()) != theory::THEORY_BOOL) { // We treat the varibables as uninterpreted return s_uninterpretedSortOwner; } else { // Except for the Boolean ones, which we just ignore anyhow return theory::THEORY_BOOL; } - } + } // Constants if (node.getMetaKind() == kind::metakind::CONSTANT) { - // Constants go to the theory of the type + // Constants go to the theory of the type return theoryOf(node.getType()); - } - // Equality + } + // Equality if (node.getKind() == kind::EQUAL) { // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow if (node[0].getKind() == kind::ITE) { @@ -100,7 +100,7 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { } if (node[1].getKind() == kind::ITE) { return theoryOf(node[1].getType()); - } + } // If both sides belong to the same theory the choice is easy TheoryId T1 = theoryOf(node[0]); TheoryId T2 = theoryOf(node[1]); @@ -108,12 +108,12 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { return T1; } TheoryId T3 = theoryOf(node[0].getType()); - // This is a case of + // This is a case of // * x*y = f(z) -> UF // * x = c -> UF // * f(x) = read(a, y) -> either UF or ARRAY // at least one of the theories has to be parametric, i.e. theory of the type is different - // from the theory of the term + // from the theory of the term if (T1 == T3) { return T2; } @@ -122,13 +122,13 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { } // If both are parametric, we take the smaller one (arbitraty) return T1 < T2 ? T1 : T2; - } + } // Regular nodes are owned by the kind - return kindToTheoryId(node.getKind()); - break; + return kindToTheoryId(node.getKind()); + break; default: Unreachable(); - } + } } void Theory::addSharedTermInternal(TNode n) { @@ -194,31 +194,21 @@ void Instantiator::resetInstantiationRound(Theory::Effort effort) { processResetInstantiationRound(effort); } -int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e, int limitInst) { +int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) { if(hasConstraintsFrom(f)) { - int origLemmas = d_quantEngine->getNumLemmasWaiting(); - int status = process(f, effort, e, limitInst); - if(limitInst <= 0 || (d_quantEngine->getNumLemmasWaiting()-origLemmas) < limitInst) { - if(d_instStrategies.empty()) { - Debug("inst-engine-inst") << "There are no instantiation strategies allocated." << endl; - } else { - for(int i = 0; i < (int) d_instStrategies.size(); ++i) { - if(isActiveStrategy(d_instStrategies[i])) { - Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " process " << effort << endl; - //call the instantiation strategy's process method - int s_limitInst = limitInst > 0 ? limitInst - (d_quantEngine->getNumLemmasWaiting() - origLemmas) : 0; - int s_status = d_instStrategies[i]->doInstantiation(f, effort, e, s_limitInst); - Debug("inst-engine-inst") << " -> status is " << s_status << endl; - if(limitInst > 0 && (d_quantEngine->getNumLemmasWaiting() - origLemmas) >= limitInst) { - Assert( (d_quantEngine->getNumLemmasWaiting() - origLemmas) == limitInst ); - i = (int) d_instStrategies.size(); - status = InstStrategy::STATUS_UNKNOWN; - } else { - InstStrategy::updateStatus(status, s_status); - } - } else { - Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " is not active." << endl; - } + int status = process(f, effort, e ); + if(d_instStrategies.empty()) { + Debug("inst-engine-inst") << "There are no instantiation strategies allocated." << endl; + } else { + for(int i = 0; i < (int) d_instStrategies.size(); ++i) { + if(isActiveStrategy(d_instStrategies[i])) { + Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " process " << effort << endl; + //call the instantiation strategy's process method + int s_status = d_instStrategies[i]->doInstantiation( f, effort, e ); + Debug("inst-engine-inst") << " -> status is " << s_status << endl; + InstStrategy::updateStatus(status, s_status); + } else { + Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " is not active." << endl; } } } |