Make conflict-based instantiation abort if a ground conflict is found in the master equality engine during term indexing, fixes bug 801.

4 files changed, 65 insertions, 53 deletions

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 420a3d2f7..008514dcc 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2079,70 +2079,76 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                 //try to make a matches making the body false
                 Trace("qcf-check-debug") << "Get next match..." << std::endl;
                 while( qi->getNextMatch( this ) ){
-                  Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;
-                  qi->debugPrintMatch("qcf-inst");
-                  Trace("qcf-inst") << std::endl;
-                  if( !qi->isMatchSpurious( this ) ){
-                    std::vector< int > assigned;
-                    if( qi->completeMatch( this, assigned ) ){
-                      std::vector< Node > terms;
-                      qi->getMatch( terms );
-                      bool tcs = qi->isTConstraintSpurious( this, terms );
-                      if( !tcs ){
-                        //for debugging
-                        if( Debug.isOn("qcf-check-inst") ){
-                          Node inst = d_quantEngine->getInstantiation( q, terms );
-                          Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
-                          Assert( !getTermDatabase()->isEntailed( inst, true ) );
-                          Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict );
-                        }
-                        if( d_quantEngine->addInstantiation( q, terms ) ){
-                          Trace("qcf-check") << "   ... Added instantiation" << std::endl;
-                          Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
-                          qi->debugPrintMatch("qcf-inst");
-                          Trace("qcf-inst") << std::endl;
-                          ++addedLemmas;
-                          if( e==effort_conflict ){
-                            d_quantEngine->markRelevant( q );
-                            ++(d_quantEngine->d_statistics.d_instantiations_qcf);
-                            if( options::qcfAllConflict() ){
-                              isConflict = true;
-                            }else{
-                              d_conflict.set( true );
+                  if( d_quantEngine->inConflict() ){
+                    Trace("qcf-check") << "   ... Quantifiers engine discovered conflict, ";
+                    Trace("qcf-check") << "probably related to disequal congruent terms in master equality engine" << std::endl;
+                    break;
+                  }else{
+                    Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;
+                    qi->debugPrintMatch("qcf-inst");
+                    Trace("qcf-inst") << std::endl;
+                    if( !qi->isMatchSpurious( this ) ){
+                      std::vector< int > assigned;
+                      if( qi->completeMatch( this, assigned ) ){
+                        std::vector< Node > terms;
+                        qi->getMatch( terms );
+                        bool tcs = qi->isTConstraintSpurious( this, terms );
+                        if( !tcs ){
+                          //for debugging
+                          if( Debug.isOn("qcf-check-inst") ){
+                            Node inst = d_quantEngine->getInstantiation( q, terms );
+                            Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
+                            Assert( !getTermDatabase()->isEntailed( inst, true ) );
+                            Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict );
+                          }
+                          if( d_quantEngine->addInstantiation( q, terms ) ){
+                            Trace("qcf-check") << "   ... Added instantiation" << std::endl;
+                            Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
+                            qi->debugPrintMatch("qcf-inst");
+                            Trace("qcf-inst") << std::endl;
+                            ++addedLemmas;
+                            if( e==effort_conflict ){
+                              d_quantEngine->markRelevant( q );
+                              ++(d_quantEngine->d_statistics.d_instantiations_qcf);
+                              if( options::qcfAllConflict() ){
+                                isConflict = true;
+                              }else{
+                                d_conflict.set( true );
+                              }
+                              break;
+                            }else if( e==effort_prop_eq ){
+                              d_quantEngine->markRelevant( q );
+                              ++(d_quantEngine->d_statistics.d_instantiations_qcf);
                             }
+                          }else{
+                            Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;
+                            //this should only happen if the algorithm generates the same propagating instance twice this round
+                            //in this case, break to avoid exponential behavior
                             break;
-                          }else if( e==effort_prop_eq ){
-                            d_quantEngine->markRelevant( q );
-                            ++(d_quantEngine->d_statistics.d_instantiations_qcf);
                           }
                         }else{
-                          Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;
-                          //this should only happen if the algorithm generates the same propagating instance twice this round
-                          //in this case, break to avoid exponential behavior
-                          break;
+                          Trace("qcf-inst") << "   ... Spurious instantiation (match is T-inconsistent)" << std::endl;
                         }
+                        //clean up assigned
+                        qi->revertMatch( this, assigned );
+                        d_tempCache.clear();
                       }else{
-                        Trace("qcf-inst") << "   ... Spurious instantiation (match is T-inconsistent)" << std::endl;
+                        Trace("qcf-inst") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
                       }
-                      //clean up assigned
-                      qi->revertMatch( this, assigned );
-                      d_tempCache.clear();
                     }else{
-                      Trace("qcf-inst") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
+                      Trace("qcf-inst") << "   ... Spurious instantiation (match is inconsistent)" << std::endl;
                     }
-                  }else{
-                    Trace("qcf-inst") << "   ... Spurious instantiation (match is inconsistent)" << std::endl;
                   }
                 }
                 Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl;
-                if( d_conflict ){
+                if( d_conflict || d_quantEngine->inConflict() ){
                   break;
                 }
               }
             }
           }
         }
-        if( addedLemmas>0 ){
+        if( addedLemmas>0 || d_quantEngine->inConflict() ){
           break;
         }
       }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5ac5ae0cc..30b17d42c 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -278,10 +278,12 @@ void TermDb::computeUfTerms( TNode f ) {
                   Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl;
                   if( !d_quantEngine->getTheoryEngine()->needCheck() ){
                     Trace("term-db-lemma") << "  all theories passed with no lemmas." << std::endl;
+                    // we should be a full effort check, prior to theory combination
                   }
                   Trace("term-db-lemma") << "  add lemma : " << lem << std::endl;
                 }
                 d_quantEngine->addLemma( lem );
+                d_quantEngine->setConflict();
                 d_consistent_ee = false;
                 return;
               }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index db0efd988..55b1af83c 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -80,6 +80,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   d_util.push_back( d_term_db );
 
   if( options::instPropagate() ){
+    // notice that this option is incompatible with options::qcfAllConflict()
     d_inst_prop = new quantifiers::InstPropagator( this );
     d_util.push_back( d_inst_prop );
     d_inst_notify.push_back( d_inst_prop->getInstantiationNotify() );
@@ -1250,8 +1251,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
       for( unsigned j=0; j<d_inst_notify.size(); j++ ){
         if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){
           Trace("inst-add-debug") << "...we are in conflict." << std::endl;
-          d_conflict = true;
-          d_conflict_c = true;
+          setConflict();
           Assert( !d_lemmas_waiting.empty() );
           break;
         }
@@ -1319,6 +1319,11 @@ void QuantifiersEngine::markRelevant( Node q ) {
   d_model->markRelevant( q );
 }
 
+void QuantifiersEngine::setConflict() { 
+  d_conflict = true; 
+  d_conflict_c = true; 
+}
+
 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
   //determine if we should perform check, based on instWhenMode
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index bb38e5e4a..7405241b7 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -39,11 +39,6 @@ namespace theory {
 
 class QuantifiersEngine;
 
-namespace quantifiers {
-  class TermDb;
-  class TermDbSygus;
-}
-
 class InstantiationNotify {
 public:
   InstantiationNotify(){}
@@ -53,6 +48,8 @@ public:
 };
 
 namespace quantifiers {
+  class TermDb;
+  class TermDbSygus;
   class FirstOrderModel;
   //modules
   class InstantiationEngine;
@@ -343,6 +340,8 @@ public:
   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
   /** is in conflict */
   bool inConflict() { return d_conflict; }
+  /** set conflict */
+  void setConflict();
   /** get number of waiting lemmas */
   unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
   /** get needs check */