diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-12-01 15:13:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-12-01 15:13:58 +0000 |
commit | e820acb9e220389e9a7e23bcffd97f1d0354f612 (patch) | |
tree | 2c968d847c87ec363cf6add1ac3cf8cfbf4902a1 /src/theory/theory.cpp | |
parent | ec29471e427bf25034a93c182b424730d439a90a (diff) |
remove instantiator framework
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r-- | src/theory/theory.cpp | 72 |
1 files changed, 0 insertions, 72 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index ea3902d59..f513b0d78 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -48,11 +48,6 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ }/* ostream& operator<<(ostream&, Theory::Effort) */ Theory::~Theory() { - if(d_inst != NULL) { - delete d_inst; - d_inst = NULL; - } - StatisticsRegistry::unregisterStat(&d_computeCareGraphTime); } @@ -174,73 +169,6 @@ void Theory::debugPrintFacts() const{ 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]->processResetInstantiationRound(effort); - } - } - processResetInstantiationRound(effort); - */ -} - -int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) { - /* - if( getQuantifierActive(f) ) { - 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]->process( 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; - } - } - } - return status; - } else { - Debug("inst-engine-inst") << "We have no constraints from this quantifier." << endl; - return InstStrategy::STATUS_SAT; - } - */ - return 0; -} - -//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 ); -// } -// } -// } -// } -//} - std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{ std::hash_set<TNode, TNodeHashFunction> currentlyShared; for(shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i){ |