diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/theory.cpp | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r-- | src/theory/theory.cpp | 114 |
1 files changed, 108 insertions, 6 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 1ed1f99ff..7555282d8 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -18,6 +18,8 @@ #include "theory/theory.h" #include "util/Assert.h" +#include "theory/quantifiers_engine.h" +#include "theory/instantiator_default.h" #include <vector> @@ -37,21 +39,32 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ os << "EFFORT_FULL"; break; case Theory::EFFORT_COMBINATION: os << "EFFORT_COMBINATION"; break; + case Theory::EFFORT_LAST_CALL: + os << "EFFORT_LAST_CALL"; break; default: Unreachable(); } return os; }/* ostream& operator<<(ostream&, Theory::Effort) */ +Theory::~Theory() { + if(d_inst != NULL) { + delete d_inst; + d_inst = NULL; + } + + StatisticsRegistry::unregisterStat(&d_computeCareGraphTime); +} + void Theory::addSharedTermInternal(TNode n) { - Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl; - Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl; + Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl; + Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl; d_sharedTerms.push_back(n); addSharedTerm(n); } void Theory::computeCareGraph() { - Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << std::endl; + Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl; for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) { TNode a = d_sharedTerms[i]; TypeNode aType = a.getType(); @@ -71,7 +84,7 @@ void Theory::computeCareGraph() { addCarePair(a, b); break; } - } + } } } @@ -85,8 +98,97 @@ void Theory::printFacts(std::ostream& os) const { } void Theory::debugPrintFacts() const{ - cout << "Theory::debugPrintFacts()" << endl; - printFacts(cout); + DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl; + printFacts(DebugChannel.getStream()); +} + +Instantiator::Instantiator(context::Context* c, QuantifiersEngine* qe, Theory* th) : + d_quantEngine(qe), + d_th(th) { +} + +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); + } + } + processResetInstantiationRound(effort); +} + +int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e, int limitInst) { + 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; + } + } + } + } + return status; + } else { + Debug("inst-engine-inst") << "We have no constraints from this quantifier." << endl; + return InstStrategy::STATUS_SAT; + } +} + +//void Instantiator::doInstantiation(int effort) { +// d_status = InstStrategy::STATUS_SAT; +// for( int q = 0; q < d_quantEngine->getNumQuantifiers(); ++q ) { +// Node f = d_quantEngine->getQuantifier(q); +// if( d_quantEngine->getActive(f) && hasConstraintsFrom(f) ) { +// int d_quantStatus = process( f, effort ); +// InstStrategy::updateStatus( d_status, d_quantStatus ); +// 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 +// d_quantStatus = d_instStrategies[i]->process( f, effort ); +// Debug("inst-engine-inst") << " -> status is " << d_quantStatus << endl; +// InstStrategy::updateStatus( d_status, d_quantStatus ); +// } +// } +// } +// } +//} + +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 */ |