merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.

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;
         }
       }
     }