Fixes related to cbqi + E-matching.

4 files changed, 54 insertions, 36 deletions

diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index de8e45a84..941eaf89b 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -40,6 +40,7 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){
   d_match_pattern_type = pat.getType();
   d_next = NULL;
   d_matchPolicy = MATCH_GEN_DEFAULT;
+  d_eq_class_rel = false;
 }
 
 InstMatchGenerator::InstMatchGenerator() {
@@ -56,7 +57,7 @@ void InstMatchGenerator::setActiveAdd(bool val){
   }
 }
 
-void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ){
+void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ){
   if( !d_pattern.isNull() ){
     Debug("inst-match-gen") << "Pattern term is " << d_pattern << std::endl;
     if( d_match_pattern.getKind()==NOT ){
@@ -103,16 +104,21 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
     //now, collect children of d_match_pattern
     //int childMatchPolicy = MATCH_GEN_DEFAULT;
     for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
-      if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){
-        InstMatchGenerator * cimg = Trigger::getInstMatchGenerator( d_match_pattern[i] );
+      Node qa = quantifiers::TermDb::getInstConstAttr(d_match_pattern[i]);
+      if( !qa.isNull() ){
+        InstMatchGenerator * cimg = Trigger::getInstMatchGenerator( q, d_match_pattern[i] );
         if( cimg ){
           d_children.push_back( cimg );
           d_children_index.push_back( i );
           gens.push_back( cimg );
           d_children_types.push_back( 1 );
         }else{
-          d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
-          d_children_types.push_back( 0 );
+          if( d_match_pattern[i].getKind()==INST_CONSTANT && qa==q ){
+            d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
+            d_children_types.push_back( 0 );
+          }else{
+            d_children_types.push_back( -1 );
+          }
         }
       }else{
         d_children_types.push_back( -1 );
@@ -157,6 +163,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
         //store the equivalence class that we will call d_cg->reset( ... ) on
         d_eq_class = d_pattern[1];
       }
+      d_eq_class_rel = true;
       Assert( Trigger::isAtomicTrigger( d_match_pattern ) );
       //we are matching only in a particular equivalence class
       d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern_op );
@@ -191,6 +198,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
     Assert( d_match_pattern.getKind()==INST_CONSTANT || t.getKind()==d_match_pattern.getKind() );
     Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );
     //first, check if ground arguments are not equal, or a match is in conflict
+    Trace("matching-debug2") << "Setting immediate matches..." << std::endl;
     for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
       if( d_children_types[i]==0 ){
         Trace("matching-debug2") << "Setting " << d_var_num[i] << " to " << t[i] << "..." << std::endl;
@@ -213,6 +221,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
         }
       }
     }
+    Trace("matching-debug2") << "Done setting immediate matches, success = " << success << "." << std::endl;
     //for variable matching
     if( d_match_pattern.getKind()==INST_CONSTANT ){
       bool addToPrev = m.get( d_var_num[0] ).isNull();
@@ -224,7 +233,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
         }
       }
     //for relational matching
-    }else if( !d_eq_class.isNull() && d_eq_class.getKind()==INST_CONSTANT ){
+    }else if( d_eq_class_rel && d_eq_class.getKind()==INST_CONSTANT ){
       int v = d_eq_class.getAttribute(InstVarNumAttribute());
       //also must fit match to equivalence class
       bool pol = d_pattern.getKind()!=NOT;
@@ -260,11 +269,13 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
       }
     }
     if( success ){
+      Trace("matching-debug2") << "Reset children..." << std::endl;
       //now, fit children into match
       //we will be requesting candidates for matching terms for each child
       for( int i=0; i<(int)d_children.size(); i++ ){
         d_children[i]->reset( t[ d_children_index[i] ], qe );
       }
+      Trace("matching-debug2") << "Continue next " << d_next << std::endl;
       success = continueNextMatch( f, m, qe );
     }
     if( !success ){
@@ -312,14 +323,14 @@ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
   //we have a specific equivalence class in mind
   //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
   //just look in equivalence class of the RHS
-  d_cg->reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class );
+  d_cg->reset( d_eq_class_rel ? Node::null() : d_eq_class );
   d_needsReset = false;
 }
 
 bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
   if( d_needsReset ){
     Trace("matching") << "Reset not done yet, must do the reset..." << std::endl;
-    reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class, qe );
+    reset( d_eq_class_rel ? Node::null() : d_eq_class, qe );
   }
   m.d_matched = Node::null();
   Trace("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << std::endl;
@@ -338,7 +349,7 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine*
   if( !success ){
     Trace("matching") << this << " failed, reset " << d_eq_class << std::endl;
     //we failed, must reset
-    reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class, qe );
+    reset( d_eq_class_rel ? Node::null() : d_eq_class, qe );
   }
   return success;
 }
@@ -382,13 +393,13 @@ int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
 }
 
 
-InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node pat, QuantifiersEngine* qe ) {
+InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe ) {
   std::vector< Node > pats;
   pats.push_back( pat );
-  return mkInstMatchGenerator( pats, qe );
+  return mkInstMatchGenerator( q, pats, qe );
 }
 
-InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe ) {
+InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) {
   size_t pCounter = 0;
   InstMatchGenerator* prev = NULL;
   InstMatchGenerator* oinit = NULL;
@@ -406,7 +417,7 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( std::vector< Node
       if( prev ){
         prev->d_next = curr;
       }
-      curr->initialize(qe, gens);
+      curr->initialize(q, qe, gens);
       prev = curr;
       counter++;
     }
@@ -488,7 +499,7 @@ d_f( f ){
   for( int i=0; i<(int)pats.size(); i++ ){
     Node n = pats[i];
     //make the match generator
-    d_children.push_back( InstMatchGenerator::mkInstMatchGenerator( n, qe ) );
+    d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(f, n, qe ) );
     //compute unique/shared variables
     std::vector< int > unique_vars;
     std::map< int, bool > shared_vars;
@@ -688,7 +699,11 @@ int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){
 InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ) {
   for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
     if( d_match_pattern[i].getKind()==INST_CONSTANT ){
-      d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
+      if( !options::cbqi() || quantifiers::TermDb::getInstConstAttr(d_match_pattern[i])==f ){
+        d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
+      }else{
+        d_var_num[i] = -1;
+      }
     }
     d_match_pattern_arg_types.push_back( d_match_pattern[i].getType() );
   }
@@ -725,22 +740,24 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
   }else{
     if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){
       int v = d_var_num[argIndex];
-      for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
-        Node t = it->first;
-        Node prev = m.get( v );
-        //using representatives, just check if equal
-        if( ( prev.isNull() || prev==t ) && t.getType().isSubtypeOf( d_match_pattern_arg_types[argIndex] ) ){
-          m.setValue( v, t);
-          addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
-          m.setValue( v, prev);
+      if( v!=-1 ){
+        for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
+          Node t = it->first;
+          Node prev = m.get( v );
+          //using representatives, just check if equal
+          if( ( prev.isNull() || prev==t ) && t.getType().isSubtypeOf( d_match_pattern_arg_types[argIndex] ) ){
+            m.setValue( v, t);
+            addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
+            m.setValue( v, prev);
+          }
         }
+        return;
       }
-    }else{
-      Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
-      std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
-      if( it!=tat->d_data.end() ){
-        addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
-      }
+    }
+    Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
+    std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
+    if( it!=tat->d_data.end() ){
+      addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
     }
   }
 }
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index f9853ef54..aae6d4e73 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -64,10 +64,11 @@ protected:
   InstMatchGenerator* d_next;
   /** eq class */
   Node d_eq_class;
+  bool d_eq_class_rel;
   /** variable numbers */
   std::map< int, int > d_var_num;
   /** initialize pattern */
-  void initialize( QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens );
+  void initialize( Node q, QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens );
   /** children types 0 : variable, 1 : child term, -1 : ground term */
   std::vector< int > d_children_types;
   /** continue */
@@ -116,8 +117,8 @@ public:
   bool d_active_add;
   void setActiveAdd( bool val );
 
-  static InstMatchGenerator* mkInstMatchGenerator( Node pat, QuantifiersEngine* qe );
-  static InstMatchGenerator* mkInstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe );
+  static InstMatchGenerator* mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe );
+  static InstMatchGenerator* mkInstMatchGenerator( Node q, std::vector< Node >& pats, QuantifiersEngine* qe );
 };/* class InstMatchGenerator */
 
 //match generator for boolean term ITEs
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index e9ce29468..c55ed27ea 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -43,7 +43,7 @@ d_quantEngine( qe ), d_f( f ){
       if( isSimpleTrigger( d_nodes[0] ) ){
         d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] );
       }else{
-        d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes[0], qe );
+        d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe );
         d_mg->setActiveAdd(true);
       }
     }else{
@@ -52,7 +52,7 @@ d_quantEngine( qe ), d_f( f ){
       //d_mg->setActiveAdd();
     }
   }else{
-    d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe );
+    d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes, qe );
     d_mg->setActiveAdd(true);
   }
   if( d_nodes.size()==1 ){
@@ -553,7 +553,7 @@ Node Trigger::getInversion( Node n, Node x ) {
   return Node::null();
 }
 
-InstMatchGenerator* Trigger::getInstMatchGenerator( Node n ) {
+InstMatchGenerator* Trigger::getInstMatchGenerator( Node q, Node n ) {
   if( n.getKind()==INST_CONSTANT ){
     return NULL;
   }else{
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 28da9f959..60e268a4f 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -113,7 +113,7 @@ public:
   static bool isPureTheoryTrigger( Node n );
   static bool isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms );
   /** return data structure for producing matches for this trigger. */
-  static InstMatchGenerator* getInstMatchGenerator( Node n );
+  static InstMatchGenerator* getInstMatchGenerator( Node q, Node n );
   static Node getInversionVariable( Node n );
   static Node getInversion( Node n, Node x );