Cbqi multiple instantiation (#1289)

* Multi-instantiation heuristic for cbqi bv.

* New clang format.

* Minor

* Minor.

* Minor

4 files changed, 66 insertions, 17 deletions

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 0262012f6..ba7c8338a 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -303,6 +303,8 @@ option cbqiModel --cbqi-model bool :read-write :default true
  guide instantiations by model values for counterexample-based quantifier instantiation
 option cbqiAll --cbqi-all bool :read-write :default false
  apply counterexample-based instantiation to all quantified formulas
+option cbqiMultiInst --cbqi-multi-inst bool :read-write :default false
+ when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation
  
 # CEGQI for arithmetic
 option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false
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
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index 8d7a9b5c3..0808b5ed0 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -119,6 +119,8 @@ public:
       d_theta.pop_back();
     }
   }
+  // is this solved form empty?
+  bool empty() { return d_vars.empty(); }
 public:
   // theta values (for LIA, see Section 4 of Reynolds/King/Kuncak FMSD 2017)
   std::vector< Node > d_theta;
@@ -227,7 +229,25 @@ public:
 public:
   void pushStackVariable( Node v );
   void popStackVariable();
-  bool doAddInstantiationInc( Node pv, Node n, TermProperties& pv_prop, SolvedForm& sf, unsigned effort );
+  /** do add instantiation increment
+   *
+   * Adds the substitution { pv_prop.getModifiedTerm(pv) -> n } to the current
+   * instantiation, specified by sf.
+   *
+   * This function returns true if a call to
+   * QuantifiersEngine::addInstantiation(...)
+   * was successfully made in a recursive call.
+   *
+   * The solved form sf is reverted to its original state if
+   *   this function returns false, or
+   *   revertOnSuccess is true and this function returns true.
+   */
+  bool doAddInstantiationInc(Node pv,
+                             Node n,
+                             TermProperties& pv_prop,
+                             SolvedForm& sf,
+                             unsigned effort,
+                             bool revertOnSuccess = false);
   Node getModelValue( Node n );
 public:
   unsigned getNumCEAtoms() { return d_ce_atoms.size(); }
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index ad4c83919..60566da1b 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -1029,10 +1029,18 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
     Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl;
     // if interleaving, do not do inversion half the time
     if (!options::cbqiBvInterleaveValue() || rand() % 2 == 0) {
+      bool firstVar = sf.empty();
       // get inst id list
-      Trace("cegqi-bv") << "  " << iti->second.size()
-                        << " candidate instantiations for " << pv << " : "
-                        << std::endl;
+      if (Trace.isOn("cegqi-bv"))
+      {
+        Trace("cegqi-bv") << "  " << iti->second.size()
+                          << " candidate instantiations for " << pv << " : "
+                          << std::endl;
+        if (firstVar)
+        {
+          Trace("cegqi-bv") << "  ...this is the first variable" << std::endl;
+        }
+      }
       // the order of instantiation ids we will try
       std::vector<unsigned> inst_ids_try;
       // until we have a model-preserving selection function for BV, this must
@@ -1081,8 +1089,12 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
           Trace("cegqi-bv") << std::endl;
         }
 
-        // currently we select the first literal
-        if (inst_ids_try.empty()) {
+        // currently:
+        //   We select the first literal, and
+        //   for the first variable, we select all 
+        //   if cbqiMultiInst is enabled.
+        if (inst_ids_try.empty() || (firstVar && options::cbqiMultiInst()))
+        {
           // try the first one
           inst_ids_try.push_back(inst_id);
         } else {
@@ -1090,11 +1102,12 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
         }
       }
 
-      // now, try all instantiation ids we want to try
-      // typically size( inst_ids_try )=0, otherwise worst-case performance for
-      // constructing
-      // instantiations is exponential on the number of variables in this
-      // quantifier
+      // Now, try all instantiation ids we want to try
+      // Typically size( inst_ids_try )<=1, otherwise worst-case performance
+      // for constructing instantiations is exponential on the number of
+      // variables in this quantifier prefix.
+      bool ret = false;
+      bool revertOnSuccess = inst_ids_try.size() > 1;
       for (unsigned j = 0; j < inst_ids_try.size(); j++) {
         unsigned inst_id = iti->second[j];
         Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end());
@@ -1104,10 +1117,16 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
         Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term
                           << std::endl;
         d_var_to_curr_inst_id[pv] = inst_id;
-        if (ci->doAddInstantiationInc(pv, inst_term, pv_prop_bv, sf, effort)) {
-          return true;
+        if (ci->doAddInstantiationInc(
+                pv, inst_term, pv_prop_bv, sf, effort, revertOnSuccess))
+        {
+          ret = true;
         }
       }
+      if (ret)
+      {
+        return true;
+      }
       Trace("cegqi-bv") << "...failed to add instantiation for " << pv
                         << std::endl;
       d_var_to_curr_inst_id.erase(pv);