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 */