Make quantifiers strategies exit immediately when in conflict (#2099)

5 files changed, 65 insertions, 18 deletions

diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index eb3f6232d..78fb987f1 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -426,6 +426,7 @@ int InstMatchGenerator::getNextMatch(Node f,
   Node t = d_curr_first_candidate;
   do{
     Trace("matching-debug2") << "Matching candidate : " << t << std::endl;
+    Assert(!qe->inConflict());
     //if t not null, try to fit it into match m
     if( !t.isNull() ){
       if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
@@ -439,7 +440,7 @@ int InstMatchGenerator::getNextMatch(Node f,
       }
       //get the next candidate term t
       if( success<0 ){
-        t = d_cg->getNextCandidate();
+        t = qe->inConflict() ? Node::null() : d_cg->getNextCandidate();
       }else{
         d_curr_first_candidate = d_cg->getNextCandidate();
       }
@@ -1029,10 +1030,11 @@ int InstMatchGeneratorSimple::addInstantiations(Node q,
     if( d_pol ){
       tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op );
     }else{
-      Node r = qe->getEqualityQuery()->getRepresentative( d_eqc );
       //iterate over all classes except r
       tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op );
-      if( tat ){
+      if (tat && !qe->inConflict())
+      {
+        Node r = qe->getEqualityQuery()->getRepresentative(d_eqc);
         for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
           if( it->first!=r ){
             InstMatch m( q );
@@ -1042,12 +1044,13 @@ int InstMatchGeneratorSimple::addInstantiations(Node q,
             }
           }
         }
-        tat = NULL;
       }
+      tat = nullptr;
     }
   }
   Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl;
-  if( tat ){
+  if (tat && !qe->inConflict())
+  {
     InstMatch m( q );
     addInstantiations( m, qe, addedLemmas, 0, tat );
   }
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 02c9aedf5..92a355348 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -268,7 +268,10 @@ bool QuantInfo::reset_round( QuantConflictFind * p ) {
   
   d_mg->reset_round( p );
   for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){
-    it->second->reset_round( p );
+    if (!it->second->reset_round(p))
+    {
+      return false;
+    }
   }
   //now, reset for matching
   d_mg->reset( p, false, this );
@@ -1178,11 +1181,14 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars
   }
 }
 
-
-void MatchGen::reset_round( QuantConflictFind * p ) {
+bool MatchGen::reset_round(QuantConflictFind* p)
+{
   d_wasSet = false;
   for( unsigned i=0; i<d_children.size(); i++ ){
-    d_children[i].reset_round( p );
+    if (!d_children[i].reset_round(p))
+    {
+      return false;
+    }
   }
   for( std::map< int, TNode >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){
     d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );
@@ -1194,18 +1200,31 @@ void MatchGen::reset_round( QuantConflictFind * p ) {
     //}else if( e==-1 ){
     //  d_ground_eval[0] = p->d_false;
     //}
-    //modified 
-    for( unsigned i=0; i<2; i++ ){ 
-      if( p->getTermDatabase()->isEntailed( d_n, i==0 ) ){
+    //modified
+    TermDb* tdb = p->getTermDatabase();
+    QuantifiersEngine* qe = p->getQuantifiersEngine();
+    for( unsigned i=0; i<2; i++ ){
+      if (tdb->isEntailed(d_n, i == 0))
+      {
         d_ground_eval[0] = i==0 ? p->d_true : p->d_false;
       }
+      if (qe->inConflict())
+      {
+        return false;
+      }
     }
   }else if( d_type==typ_eq ){
-    for (unsigned i = 0; i < d_n.getNumChildren(); i++)
+    TermDb* tdb = p->getTermDatabase();
+    QuantifiersEngine* qe = p->getQuantifiersEngine();
+    for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++)
     {
       if (!expr::hasBoundVar(d_n[i]))
       {
-        TNode t = p->getTermDatabase()->getEntailedTerm(d_n[i]);
+        TNode t = tdb->getEntailedTerm(d_n[i]);        
+        if (qe->inConflict())
+        {
+          return false;
+        }
         if (t.isNull())
         {
           d_ground_eval[i] = d_n[i];
@@ -1220,6 +1239,7 @@ void MatchGen::reset_round( QuantConflictFind * p ) {
   d_qni_bound_cons.clear();
   d_qni_bound_cons_var.clear();
   d_qni_bound.clear();
+  return true;
 }
 
 void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
@@ -2038,9 +2058,10 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
                   }
                 }
                 Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl;
-                if( d_conflict || d_quantEngine->inConflict() ){
-                  break;
-                }
+              }
+              if (d_conflict || d_quantEngine->inConflict())
+              {
+                break;
               }
             }
           }
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index d76495b52..0469e958b 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -90,7 +90,13 @@ public:
   std::vector< MatchGen > d_children;
   short d_type;
   bool d_type_not;
-  void reset_round( QuantConflictFind * p );
+  /** reset round
+   *
+   * Called once at the beginning of each full/last-call effort, prior to
+   * processing this match generator. This method returns false if the reset
+   * failed, e.g. if a conflict was encountered during term indexing.
+   */
+  bool reset_round(QuantConflictFind* p);
   void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi );
   bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );
   bool isValid() { return d_type!=typ_invalid; }
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 63593c662..ca9b88ecf 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -621,6 +621,7 @@ REG0_TESTS = \
 	regress0/quantifiers/issue1805.smt2 \
 	regress0/quantifiers/issue2031-bv-var-elim.smt2 \
 	regress0/quantifiers/issue2033-macro-arith.smt2 \
+	regress0/quantifiers/issue2035.smt2 \
 	regress0/quantifiers/lra-triv-gn.smt2 \
 	regress0/quantifiers/macros-int-real.smt2 \
 	regress0/quantifiers/macros-real-arg.smt2 \
diff --git a/test/regress/regress0/quantifiers/issue2035.smt2 b/test/regress/regress0/quantifiers/issue2035.smt2
new file mode 100644
index 000000000..4c677d352
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue2035.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --inst-when=full --full-saturate-quant
+; EXPECT: unsat
+(set-logic AUFLIA)
+(set-info :status unsat)
+(declare-fun _substvar_37_ () Int)
+(declare-fun _substvar_33_ () Int)
+(declare-fun _substvar_32_ () Int)
+(declare-sort A 0)
+(declare-sort PZA 0)
+(declare-fun MS (Int A PZA) Bool)
+(declare-fun length (PZA Int) Bool)
+(declare-fun p () PZA)
+(assert (! (exists ((n55 Int)) (and true true (forall ((x862 Int) (x863 A) (x864 A)) (=> (and (MS x862 x863 p) (MS x862 x864 p)) (= x863 x864))) true)) :named hyp30))
+(assert (! (exists ((x1298 A) (x1299 A) (x1300 Int)) (exists ((x1302 Int)) (length p 0))) :named hyp42))
+(assert (! (not (exists ((n67 Int)) (and true true (forall ((x1308 Int) (x1309 A) (x1310 A)) (=> (and (exists ((i114 Int)) (and true true (= _substvar_32_ _substvar_33_) (exists ((x1312 Int)) (and (forall ((x1313 Int)) (=> (length p 0) (= x1312 (+ (- 0 _substvar_33_) 1)))) (MS x1312 x1309 p))))) (exists ((i115 Int)) (and true true (= _substvar_32_ _substvar_37_) (exists ((x1315 Int)) (and (forall ((x1316 Int)) (=> (length p 0) (= x1315 (+ (- 0 _substvar_37_) 1)))) (MS x1315 x1310 p)))))) (= x1309 x1310))) true))) :named goal))
+(check-sat)