Cbqi multiple instantiation (#1289)

* Multi-instantiation heuristic for cbqi bv.

* New clang format.

* Minor

* Minor.

* Minor

1 files changed, 12 insertions, 4 deletions

diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 02b2d3a1b..57bfb2d14 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -362,7 +362,13 @@ void CegInstantiator::popStackVariable() {
   d_stack_vars.pop_back();
 }
 
-bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv_prop, SolvedForm& sf, unsigned effort ) {
+bool CegInstantiator::doAddInstantiationInc(Node pv,
+                                            Node n,
+                                            TermProperties& pv_prop,
+                                            SolvedForm& sf,
+                                            unsigned effort,
+                                            bool revertOnSuccess)
+{
   Node cnode = pv_prop.getCacheNode();
   if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){
     d_curr_subs_proc[pv][n][cnode] = true;
@@ -453,12 +459,14 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv
       Trace("cbqi-inst-debug2") << "Recurse..." << std::endl;
       unsigned i = d_curr_index[pv];
       success = doAddInstantiation( sf, d_stack_vars.empty() ? i+1 : i, effort );
-      if( !success ){
+      if (!success || revertOnSuccess)
+      {
         Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl;
         sf.pop_back( pv, n, pv_prop );
       }
     }
-    if( success ){
+    if (success && !revertOnSuccess)
+    {
       return true;
     }else{
       Trace("cbqi-inst-debug2") << "Revert substitutions..." << std::endl;
@@ -472,7 +480,7 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv
       for( unsigned i=0; i<new_non_basic.size(); i++ ){
         sf.d_non_basic.pop_back();
       }
-      return false;
+      return success;
     }
   }else{
     //already tried this substitution