Minor improvements and changes to defaults for cbqi bv (#1406)

This 

makes it so that --cbqi-bv tries at most 2 instantiations per quantified formula (one based on inversions when applicable, one based on model values). This makes it so that we do not have exponential run time in the worst case. This helps significantly for psyco benchmarks which have many quantified variables.

Enables --cbqi-bv by default and changes the default inequality mode to eq-boundary (which is the best performer overall), also enables extract removal by default

Allows cbqiNestedQE to be used in the BV logic.

Adds an option --cbqi-full which indicates whether we should try model value instantiations for bit-vectors (by default, this is done only for the pure BV logic).

4 files changed, 32 insertions, 13 deletions

diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 15bfbe9f9..cf2c51ec1 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -460,11 +460,9 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
     }
 
     //[4] resort to using value in model. We do so if:
-    // - we are in a higher effort than CEG_INST_EFFORT_STANDARD,
-    // - if the variable is Boolean, or
-    // - if we are solving for a subfield of a datatype.
-    bool use_model_value = vinst->useModelValue(this, sf, pv, d_effort);
-    if ((d_effort > CEG_INST_EFFORT_STANDARD || use_model_value || is_cv)
+    // - if the instantiator uses model values at this effort, or
+    // - if we are solving for a subfield of a datatype (is_cv).
+    if ((vinst->useModelValue(this, sf, pv, d_effort) || is_cv)
         && vinst->allowModelValue(this, sf, pv, d_effort))
     {
 #ifdef CVC4_ASSERTIONS
@@ -478,7 +476,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
       Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
       d_curr_iphase[pv] = CEG_INST_PHASE_MVALUE;
       CegInstEffort prev = d_effort;
-      if (!use_model_value)
+      if (d_effort < CEG_INST_EFFORT_STANDARD_MV)
       {
         // update the effort level to indicate we have used a model value
         d_effort = CEG_INST_EFFORT_STANDARD_MV;
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index ab9c7ea05..126f0325f 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -691,7 +691,7 @@ public:
                              Node pv,
                              CegInstEffort effort)
   {
-    return false;
+    return effort > CEG_INST_EFFORT_STANDARD;
   }
   /** do we allow the model value as instantiation for pv? */
   virtual bool allowModelValue(CegInstantiator* ci,
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 674f7c17e..4570d03c3 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -934,8 +934,9 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery
   CegInstantiator * d_ci;
 };
 
-
-BvInstantiator::BvInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){
+BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn)
+    : Instantiator(qe, tn), d_tried_assertion_inst(false)
+{
   // get the global inverter utility
   // this must be global since we need to:
   // * process Skolem functions properly across multiple variables within the same quantifier
@@ -958,6 +959,7 @@ void BvInstantiator::reset(CegInstantiator* ci,
   d_inst_id_to_alit.clear();
   d_var_to_curr_inst_id.clear();
   d_alit_to_model_slack.clear();
+  d_tried_assertion_inst = false;
 }
 
 void BvInstantiator::processLiteral(CegInstantiator* ci,
@@ -1001,6 +1003,11 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
                                          Node lit,
                                          CegInstEffort effort)
 {
+  if (effort == CEG_INST_EFFORT_FULL)
+  {
+    // always use model values at full effort
+    return Node::null();
+  }
   Node atom = lit.getKind() == NOT ? lit[0] : lit;
   bool pol = lit.getKind() != NOT;
   Kind k = atom.getKind();
@@ -1113,6 +1120,15 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci,
   return false;
 }
 
+bool BvInstantiator::useModelValue(CegInstantiator* ci,
+                                   SolvedForm& sf,
+                                   Node pv,
+                                   CegInstEffort effort)
+{
+  return !d_tried_assertion_inst
+         && (effort < CEG_INST_EFFORT_FULL || options::cbqiFullEffort());
+}
+
 bool BvInstantiator::processAssertions(CegInstantiator* ci,
                                        SolvedForm& sf,
                                        Node pv,
@@ -1200,6 +1216,7 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci,
         Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term
                           << std::endl;
         d_var_to_curr_inst_id[pv] = inst_id;
+        d_tried_assertion_inst = true;
         if (ci->constructInstantiationInc(
                 pv, inst_term, pv_prop_bv, sf, revertOnSuccess))
         {
diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
index 4fb954d44..c2864acc5 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -214,13 +214,15 @@ class BvInstantiator : public Instantiator {
                                  SolvedForm& sf,
                                  Node pv,
                                  CegInstEffort effort) override;
+  /** use model value
+   *
+   * We allow model values if we have not already tried an assertion,
+   * and only at levels below full if cbqiFullEffort is false.
+   */
   virtual bool useModelValue(CegInstantiator* ci,
                              SolvedForm& sf,
                              Node pv,
-                             CegInstEffort effort) override
-  {
-    return true;
-  }
+                             CegInstEffort effort) override;
   virtual std::string identify() const { return "Bv"; }
  private:
   // point to the bv inverter class
@@ -235,6 +237,8 @@ class BvInstantiator : public Instantiator {
   std::unordered_map< Node, unsigned, NodeHashFunction > d_var_to_curr_inst_id;
   /** the amount of slack we added for asserted literals */
   std::unordered_map<Node, Node, NodeHashFunction> d_alit_to_model_slack;
+  /** whether we have tried an instantiation based on assertion in this round */
+  bool d_tried_assertion_inst;
   /** rewrite assertion for solve pv
   * returns a literal that is equivalent to lit that leads to best solved form for pv
   */