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

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 1a4275d77592898cc6df3d0630e19c0fc0a39363..4a7a9e8a7309b0e2fc17583aac4db9d4c00e8fc7 100644 (file)
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -299,6 +299,8 @@ option sygusStream --sygus-stream bool :default false
 # CEGQI applied to general quantified formulas
 option cbqi --cbqi bool :read-write :default false
  turns on counterexample-based quantifier instantiation
+option cbqiFullEffort --cbqi-full bool :read-write :default false
+ turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation
 option recurseCbqi --cbqi-recurse bool :default true
  turns on recursive counterexample-based quantifier instantiation
 option cbqiSat --cbqi-sat bool :read-write :default true
@@ -339,13 +341,13 @@ option quantEprMatching --quant-epr-match bool :default true
  use matching heuristics for EPR instantiation
  
 # CEGQI for BV
-option cbqiBv --cbqi-bv bool :read-write :default false
+option cbqiBv --cbqi-bv bool :read-write :default true
   use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors
 option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :default false
   interleave model value instantiation with word-level inversion approach
-option cbqiBvIneqMode --cbqi-bv-ineq=MODE CVC4::theory::quantifiers::CbqiBvIneqMode :read-write :default CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_SLACK :include "options/quantifiers_modes.h" :handler stringToCbqiBvIneqMode
+option cbqiBvIneqMode --cbqi-bv-ineq=MODE CVC4::theory::quantifiers::CbqiBvIneqMode :read-write :default CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY :include "options/quantifiers_modes.h" :handler stringToCbqiBvIneqMode
  choose mode for handling bit-vector inequalities with counterexample-guided instantiation
-option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default false 
+option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default true 
   replaces extract terms with variables for counterexample-guided instantiation for bit-vectors
  
 ### local theory extensions options 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 65dae6b8f4c1dbbebe645e8ba95adc85bf9906e1..3a0cb297ed71576d66e6d8fc2fcfd55fcdd4856f 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1912,6 +1912,14 @@ void SmtEngine::setDefaults() {
     if( !options::cbqi.wasSetByUser() ){
       options::cbqi.set( true );
     }
+    // check whether we should apply full cbqi
+    if (d_logic.isPure(THEORY_BV))
+    {
+      if (!options::cbqiFullEffort.wasSetByUser())
+      {
+        options::cbqiFullEffort.set(true);
+      }
+    }
   }
   if( options::cbqi() ){
     //must rewrite divk
@@ -1931,8 +1939,11 @@ void SmtEngine::setDefaults() {
         options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
       }
     }else{
-      //only supported in pure arithmetic
-      options::cbqiNestedQE.set(false);
+      // only supported in pure arithmetic or pure BV
+      if (d_logic.isPure(THEORY_BV))
+      {
+        options::cbqiNestedQE.set(false);
+      }
     }
   }
   //implied options...

diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 15bfbe9f999764a5a343e4a6af32c9a28c5ba391..cf2c51ec1e2d79dc8ef417941d89d068d28f393f 100644 (file)
--- 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 ab9c7ea051e461d14edf9275034d08728d4296a5..126f0325ffd25b444f19799fe42c56decc058eea 100644 (file)
--- 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 674f7c17e2b1582a8371342d0c9bde1e2c585d5c..4570d03c32e88b1861c1b3f5c953fcca6acc9b5a 100644 (file)
--- 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 4fb954d4455f66e19a17bf384b09291b9e367fc1..c2864acc5817166dde015c93b143078b75714cac 100644 (file)
--- 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
   */