diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-16 21:59:50 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-16 21:59:50 +0000 |
commit | d9d71e0d7885d32ef44fbd08d47b3cccd35ff6f7 (patch) | |
tree | f730bb17eba9412258c47617f144510d722d6006 /src/theory/theory.cpp | |
parent | bbcfb5208c6c0f343d1a63b129c54914f66b2701 (diff) |
more cleanup of quantifiers code
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r-- | src/theory/theory.cpp | 22 |
1 files changed, 3 insertions, 19 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 63a493b07..cdad1e19c 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -186,14 +186,14 @@ Instantiator::~Instantiator() { void Instantiator::resetInstantiationRound(Theory::Effort effort) { for(int i = 0; i < (int) d_instStrategies.size(); ++i) { if(isActiveStrategy(d_instStrategies[i])) { - d_instStrategies[i]->resetInstantiationRound(effort); + d_instStrategies[i]->processResetInstantiationRound(effort); } } processResetInstantiationRound(effort); } int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) { - if(hasConstraintsFrom(f)) { + if( getQuantifierActive(f) ) { int status = process(f, effort, e ); if(d_instStrategies.empty()) { Debug("inst-engine-inst") << "There are no instantiation strategies allocated." << endl; @@ -202,7 +202,7 @@ int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) { 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 ); + int s_status = d_instStrategies[i]->process( f, effort, e ); Debug("inst-engine-inst") << " -> status is " << s_status << endl; InstStrategy::updateStatus(status, s_status); } else { @@ -237,22 +237,6 @@ int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) { // } //} -void Instantiator::setHasConstraintsFrom(Node f) { - d_hasConstraints[f] = true; - if(! d_quantEngine->hasOwner(f)) { - d_quantEngine->setOwner(f, getTheory()); - } else if(d_quantEngine->getOwner(f) != getTheory()) { - d_quantEngine->setOwner(f, NULL); - } -} - -bool Instantiator::hasConstraintsFrom(Node f) { - return d_hasConstraints.find(f) != d_hasConstraints.end() && d_hasConstraints[f]; -} - -bool Instantiator::isOwnerOf(Node f) { - return d_quantEngine->hasOwner(f) && d_quantEngine->getOwner(f) == getTheory(); -} }/* CVC4::theory namespace */ }/* CVC4 namespace */ |