From d367c9f9b299a15fb970d62df04d3df22b7ca08d Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 4 Sep 2018 14:34:21 -0500
Subject: Make quantifiers strategies exit immediately when in conflict (#2099)

---
 src/theory/quantifiers/quant_conflict_find.cpp | 45 +++++++++++++++++++-------
 1 file changed, 33 insertions(+), 12 deletions(-)

(limited to 'src/theory/quantifiers/quant_conflict_find.cpp')

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;
               }
             }
           }
-- 
cgit v1.2.3