Cbqi multiple instantiation (#1289)

* Multi-instantiation heuristic for cbqi bv.

* New clang format.

* Minor

* Minor.

* Minor

1 files changed, 21 insertions, 1 deletions

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(); }