Handle fmf.card as input from user, add support in SMT2 parser, as requested by Martin Brain. Fix two minor bugs : E-matching with datatypes, instantiation caching with incremental.

3 files changed, 13 insertions, 10 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 4a23f1c97..a74c51a9a 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -210,7 +210,7 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
     }
   }
   if( index==(int)f[0].getNumChildren() ){
-    return false;
+    return reset;
   }else{
     Node n = m[ index ];
     std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 738cfed60..8b62fc39b 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -83,14 +83,17 @@ void ModelEngine::check( Theory::Effort e ){
           Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
           //let the strong solver verify that the model is minimal
           //for debugging, this will if there are terms in the model that the strong solver was not notified of
-          ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm );
-          Trace("model-engine-debug") << "Check model..." << std::endl;
-          d_incomplete_check = false;
-          //print debug
-          Debug("fmf-model-complete") << std::endl;
-          debugPrint("fmf-model-complete");
-          //successfully built an acceptable model, now check it
-          addedLemmas += checkModel();
+          if( ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ) ){
+            Trace("model-engine-debug") << "Check model..." << std::endl;
+            d_incomplete_check = false;
+            //print debug
+            Debug("fmf-model-complete") << std::endl;
+            debugPrint("fmf-model-complete");
+            //successfully built an acceptable model, now check it
+            addedLemmas += checkModel();
+          }else{
+            addedLemmas++;
+          }
         }
       }
       if( addedLemmas==0 ){
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index ea1231e7a..c1b3b307d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -81,7 +81,7 @@ Node TermDb::getOperator( Node n ) {
     }
     d_par_op_map[op][tn1][tn2] = n;
     return n;
-  }else if( n.getKind()==APPLY_UF ){
+  }else if( n.hasOperator() ){
     return n.getOperator();
   }else{
     return Node::null();