Bug fixes related to parametric datatypes + theory combination + quantifiers. Add regression.

3 files changed, 11 insertions, 6 deletions

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index bb514f41b..8c67eb95e 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -691,10 +691,13 @@ bool FullSaturation::process( Node f, bool fullEffort ){
                 if( max_zero[i] ){
                   //no terms available, will report incomplete instantiation
                   terms.push_back( Node::null() );
+                  Trace("inst-alg-rd") << "  null" << std::endl;
                 }else if( r==0 ){
                   terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
+                  Trace("inst-alg-rd") << "  " << rd->getRDomain( f, i )->d_terms[childIndex[i]] << std::endl;
                 }else{
                   terms.push_back( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) );
+                  Trace("inst-alg-rd") << "  " << d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) << std::endl;
                 }
               }
               if( d_quantEngine->addInstantiation( f, terms, false ) ){
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 1cbfbd99b..c796333b3 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -508,9 +508,9 @@ bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRe
       if( it!=d_var_rel_dom.end() ){
         for( std::map< TNode, std::vector< unsigned > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
           for( unsigned j=0; j<it2->second.size(); j++ ){
-            Debug("qcf-match-debug2") << n << " in relevant domain " <<  it2->second << "." << it2->second[j] << "?" << std::endl;
+            Debug("qcf-match-debug2") << n << " in relevant domain " <<  it2->first << "." << it2->second[j] << "?" << std::endl;
             if( !p->getTermDatabase()->inRelevantDomain( it2->first, it2->second[j], n ) ){
-              Debug("qcf-match-debug") << "  -> fail, since " << n << " is not in relevant domain of " << it2->second << "." << it2->second[j] << std::endl;
+              Debug("qcf-match-debug") << "  -> fail, since " << n << " is not in relevant domain of " << it2->first << "." << it2->second[j] << std::endl;
               return false;
             }
           }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index ef301c2cf..51c72d7bb 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -126,9 +126,10 @@ Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) {
 }
 
 Node TermDb::getMatchOperator( Node n ) {
-  //return n.getOperator();
   Kind k = n.getKind();
-  if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ){
+  //datatype operators may be parametric, always assume they are
+  if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || 
+      k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ){
     //since it is parametric, use a particular one as op
     TypeNode tn = n[0].getType();
     Node op = n.getOperator();
@@ -241,10 +242,11 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQ
   if( itv != visited.end() ){
     return itv->second;
   }
-  Assert( n.getKind()!=BOUND_VARIABLE );
   Trace("term-db-eval") << "evaluate term : " << n << std::endl;
   Node ret;
-  if( !qy->hasTerm( n ) ){
+  if( n.getKind()==BOUND_VARIABLE ){
+    return n;
+  }else if( !qy->hasTerm( n ) ){
     //term is not known to be equal to a representative in equality engine, evaluate it
     if( n.getKind()==FORALL ){
       ret = Node::null();