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).

1 files changed, 4 insertions, 6 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;