Minor fixes for inst match generators. Updates to qip.google

5 files changed, 69 insertions, 21 deletions

diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 29754d3e6..791e36ce4 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -307,9 +307,6 @@ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
 }
 
 bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
-  if( qe->inConflict() ){
-    return false;
-  }
   if( d_needsReset ){
     Trace("matching") << "Reset not done yet, must do the reset..." << std::endl;
     reset( d_eq_class, qe );
@@ -348,9 +345,15 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif
       m.add( baseMatch );
       if( qe->addInstantiation( f, m, false ) ){
         addedLemmas++;
+        if( qe->inConflict() ){
+          break;
+        }
       }
     }else{
       addedLemmas++;
+      if( qe->inConflict() ){
+        break;
+      }
     }
     m.clear();
   }
@@ -368,7 +371,7 @@ int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
       }
     }
   }else{
-    for( int i=0; i<(int)d_children.size(); i++ ){
+    for( unsigned i=0; i<d_children.size(); i++ ){
       d_children[i]->addTerm( f, t, qe );
     }
   }
@@ -530,14 +533,14 @@ d_f( q ){
 
 /** reset instantiation round (call this whenever equivalence classes have changed) */
 void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){
-  for( int i=0; i<(int)d_children.size(); i++ ){
+  for( unsigned i=0; i<d_children.size(); i++ ){
     d_children[i]->resetInstantiationRound( qe );
   }
 }
 
 /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
-  for( int i=0; i<(int)d_children.size(); i++ ){
+  for( unsigned i=0; i<d_children.size(); i++ ){
     d_children[i]->reset( eqc, qe );
   }
 }
@@ -545,7 +548,7 @@ void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
 int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){
   int addedLemmas = 0;
   Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl;
-  for( int i=0; i<(int)d_children.size(); i++ ){
+  for( unsigned i=0; i<d_children.size(); i++ ){
     Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;
     std::vector< InstMatch > newMatches;
     InstMatch m( q );
@@ -555,8 +558,11 @@ int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, Qu
       m.clear();
     }
     Debug("smart-multi-trigger") << "Made " << newMatches.size() << " new matches for index " << i << std::endl;
-    for( int j=0; j<(int)newMatches.size(); j++ ){
+    for( unsigned j=0; j<newMatches.size(); j++ ){
       processNewMatch( qe, newMatches[j], i, addedLemmas );
+      if( qe->inConflict() ){
+        return addedLemmas;
+      }
     }
   }
   return addedLemmas;
@@ -579,6 +585,7 @@ void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch&
 void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
                                                         std::vector< IndexedTrie >& unique_var_tries,
                                                         int trieIndex, int childIndex, int endChildIndex, bool modEq ){
+  Assert( !qe->inConflict() );
   if( childIndex==endChildIndex ){
     //now, process unique variables
     processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 );
@@ -600,6 +607,9 @@ void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, I
           mn.setValue( curr_index, it->first);
           processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries,
                                     trieIndex+1, childIndex, endChildIndex, modEq );
+          if( qe->inConflict() ){
+            break;
+          }
         }
       //}
     }else{
@@ -621,6 +631,9 @@ void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, I
               if( itc!=tr->d_data.end() ){
                 processNewInstantiations( qe, m, addedLemmas, &(itc->second), unique_var_tries,
                                           trieIndex+1, childIndex, endChildIndex, modEq );
+                if( qe->inConflict() ){
+                  break;
+                }
               }
             }
             ++eqc;
@@ -652,6 +665,9 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe,
         InstMatch mn( &m );
         mn.setValue( curr_index, it->first);
         processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 );
+        if( qe->inConflict() ){
+          break;
+        }
       }
     }else{
       processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 );
@@ -727,6 +743,9 @@ int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, Q
           InstMatch m( q );
           m.add( baseMatch );
           addInstantiations( m, qe, addedLemmas, 0, &(it->second) );
+          if( qe->inConflict() ){
+            break;
+          }
         }
       }
       tat = NULL;
@@ -736,10 +755,8 @@ int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, Q
     InstMatch m( q );
     m.add( baseMatch );
     addInstantiations( m, qe, addedLemmas, 0, tat );
-    return addedLemmas;
-  }else{
-    return 0;
   }
+  return addedLemmas;
 }
 
 void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){
@@ -777,13 +794,12 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
         }
         return;
       }
+      //inst constant from another quantified formula, treat as ground term  TODO: remove this?
     }
-    if( !qe->inConflict() ){
-      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_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 863914567..c6f4affc5 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -156,8 +156,15 @@ bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >&
   if( areDisequal( a, b ) ){
     return true;
   }else{
-    //TODO?
-    return false;
+    //Assert( getRepresentative( a )==a );
+    //Assert( getRepresentative( b )==b );
+    std::map< Node, std::vector< Node > >::iterator itd = d_diseq_list[a].find( b );
+    if( itd!=d_diseq_list[a].end() ){
+      exp.insert( exp.end(), itd->second.begin(), itd->second.end() );
+      return true;
+    }else{
+      return false;
+    }
   }
 }
 
@@ -283,9 +290,27 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
       Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl;
       a = ar;
       b = br;
+      
+      //carry disequality list
+      std::map< Node, std::map< Node, std::vector< Node > > >::iterator itd = d_diseq_list.find( ar );
+      if( itd!=d_diseq_list.end() ){
+        for( std::map< Node, std::vector< Node > >::iterator itdd = itd->second.begin(); itdd != itd->second.end(); ++itdd ){
+          Node d = itdd->first;
+          if( d_diseq_list[br].find( d )==d_diseq_list[br].end() ){
+            merge_exp( d_diseq_list[br][d], itdd->second );
+            merge_exp( d_diseq_list[br][d], d_uf_exp[ar] );
+          }
+        }
+      }
+      
       return status;
     }else{
-      //TODO?
+      Trace("qip-eq") << "EqualityQueryInstProp::setEqual : disequal " << ar << " <> " << br << std::endl;
+      Assert( d_diseq_list[ar].find( br )==d_diseq_list[ar].end() );
+      Assert( d_diseq_list[br].find( ar )==d_diseq_list[br].end() );
+      
+      merge_exp( d_diseq_list[ar][br], reason );
+      merge_exp( d_diseq_list[br][ar], reason );
       return STATUS_NONE;
     }
   }
@@ -556,6 +581,7 @@ bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, st
     Trace("qip-prop") << "...finished notify instantiation." << std::endl;
     return !d_conflict;
   }else{
+    Assert( false );
     return true;
   }
 }
@@ -688,14 +714,18 @@ void InstPropagator::conflict( std::vector< Node >& exp ) {
   addRelevantInstances( exp, "qip-propagate" );
 
   //now, inform quantifiers engine which instances should be retracted
+  Trace("qip-prop-debug") << "...remove instantiation ids : ";
   for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){
     if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){
       if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){
         Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl;
         Assert( false );
+      }else{
+        Trace("qip-prop-debug") << it->first << " ";
       }
     }
   }
+  Trace("qip-prop-debug") << std::endl;
   //will interupt the quantifiers engine
   Trace("quant-engine-conflict") << "-----> InstPropagator::conflict with " << exp.size() << " instances." << std::endl;
 }
diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index a6f76ef44..0c02c7f95 100644
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -72,7 +72,7 @@ private:
   std::map< Node, std::vector< Node > > d_uf_exp;
   Node getUfRepresentative( Node a, std::vector< Node >& exp );
   /** disequality list, stores explanations */
-  std::map< Node, std::map< Node, Node > > d_diseq_list;
+  std::map< Node, std::map< Node, std::vector< Node > > > d_diseq_list;
   /** add arg */
   void addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol );
 public:
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index f98a3fd75..4b95c75ed 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1101,6 +1101,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
           Trace("inst-add-debug") << "...we are in conflict." << std::endl;
           d_conflict = true;
           Assert( !d_lemmas_waiting.empty() );
+          break;
         }
       }
     }
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 91e0c37d4..575aa4159 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -38,6 +38,7 @@ TESTS =	\
 	lst-no-self-rev-exp.smt2 \
 	fib-core.smt2 \
 	fore19-exp2-core.smt2 \
+	with-ind-104-core.smt2 \
 	syn002-si-real-int.smt2 \
 	krs-sat.smt2 \
 	forall_unit_data2.smt2 \