CBQI BV quick heuristics (#1239)

Adds two heuristics for cbqi-bv, both disabled by default.

The first optimistically solves for boundary points of inequalities.
The second randomly interleaves inversion and value instantiations.
Adds some newly solved regressions from SMT LIB.

2 files changed, 128 insertions, 70 deletions

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 2e765ce6b..d3f8c9f6a 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -334,7 +334,11 @@ option quantEprMatching --quant-epr-match bool :default true
  
 # CEGQI for BV
 option cbqiBv --cbqi-bv bool :read-write :default false
- use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors
+  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 cbqiBvSlackIneq --cbqi-bv-slack-ineq bool :read-write :default true
+  use model slack values when solving inequalities with word-level inversion approach
  
 ### local theory extensions options 
 
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 91c29c6de..ad99f1135 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -897,12 +897,15 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, SolvedForm& sf,
     unsigned iid = d_inst_id_counter;
     Node inst = d_inverter->solve_bv_lit( sv, slit, true, path, &m, d_inst_id_to_status[iid] );
     if( !inst.isNull() ){
+      inst = Rewriter::rewrite(inst);
+      Trace("cegqi-bv") << "...solved form is " << inst << std::endl;
       // store information for id and increment
       d_var_to_inst_id[pv].push_back( iid );
       d_inst_id_to_term[iid] = inst;
       d_inst_id_to_alit[iid] = alit;
       d_inst_id_counter++;
     }else{
+      Trace("cegqi-bv") << "...failed to solve." << std::endl;
       // cleanup information if we failed to solve
       d_inst_id_to_status.erase( iid );
     }
@@ -920,11 +923,23 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf,
       return lit;
     }
   } else {
+    bool useSlack = false;
+    if (k == EQUAL) {
+      // always use slack for disequalities
+      useSlack = true;
+    } else if (k == BITVECTOR_ULT || k == BITVECTOR_SLT) {
+      if (options::cbqiBvSlackIneq()) {
+        useSlack = true;
+      }
+    } else {
+      // others should be rewritten
+      Assert(false);
+      return Node::null();
+    }
     // for all other predicates, we convert them to a positive equality based on
     // the current model M, e.g.:
     //   (not) s ~ t  --->  s = t + ( s^M - t^M )
-    if (k == EQUAL || k == BITVECTOR_ULT || k == BITVECTOR_ULE ||
-        k == BITVECTOR_SLT || k == BITVECTOR_SLE) {
+    if (useSlack) {
       Node s = atom[0];
       Node t = atom[1];
       // only handle equalities between bitvectors
@@ -934,19 +949,43 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf,
         Assert(!sm.isNull() && sm.isConst());
         Node tm = ci->getModelValue(t);
         Assert(!tm.isNull() && tm.isConst());
+        Node ret;
         if (sm != tm) {
           Node slack =
               Rewriter::rewrite(nm->mkNode(kind::BITVECTOR_SUB, sm, tm));
           Assert(slack.isConst());
           // remember the slack value for the asserted literal
           d_alit_to_model_slack[lit] = slack;
-          Node ret = nm->mkNode(kind::EQUAL, s,
-                                nm->mkNode(kind::BITVECTOR_PLUS, t, slack));
+          ret = nm->mkNode(kind::EQUAL, s,
+                           nm->mkNode(kind::BITVECTOR_PLUS, t, slack));
           Trace("cegqi-bv") << "Process " << lit << " as " << ret
                             << ", slack is " << slack << std::endl;
-          return ret;
+        }else{
+          ret = s.eqNode(t);          
+          Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl;
         }
+        return ret;
+      }
+    } else {
+      // otherwise, we optimistically solve for the boundary point of an inequality
+      // for example
+      //   for s < t, we solve s+1 = t
+      //   for ~( s < t ), we solve s = t
+      // notice that this equality does not necessarily hold in the model, and
+      // hence the corresponding instantiation strategy is not guaranteed to be
+      // monotonic.
+      Node ret;
+      if (!pol) {
+        ret = atom[0].eqNode(atom[1]);
+      } else {
+        unsigned one = 1;
+        BitVector bval(atom[0].getType().getConst<BitVectorSize>(), one);
+        Node bv_one = NodeManager::currentNM()->mkConst<BitVector>(bval);
+        ret = NodeManager::currentNM()
+                  ->mkNode(kind::BITVECTOR_PLUS, atom[0], bv_one)
+                  .eqNode(atom[1]);
       }
+      return ret;
     }
   }
   return Node::null();
@@ -976,79 +1015,94 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
   std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction >::iterator iti = d_var_to_inst_id.find( pv );
   if( iti!=d_var_to_inst_id.end() ){
     Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl;
-    // get inst id list
-    Trace("cegqi-bv") << "  " << iti->second.size() << " candidate instantiations for " << pv << " : " << 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 be heuristic (we only pick one literal)
-    // hence we randomize the list
-    // this helps robustness, since picking the same literal every time may be lead to a stream of value instantiations
-    std::random_shuffle( iti->second.begin(), iti->second.end() );
+    // if interleaving, do not do inversion half the time
+    if (!options::cbqiBvInterleaveValue() || rand() % 2 == 0) {
+      // get inst id list
+      Trace("cegqi-bv") << "  " << iti->second.size()
+                        << " candidate instantiations for " << pv << " : "
+                        << 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
+      // be heuristic (we only pick one literal)
+      // hence we randomize the list
+      // this helps robustness, since picking the same literal every time may
+      // lead to a stream of value instantiations, whereas with randomization
+      // we may find an invertible literal that leads to a useful instantiation.
+      std::random_shuffle(iti->second.begin(), iti->second.end());
 
-    for( unsigned j=0; j<iti->second.size(); j++ ){
-      unsigned inst_id = iti->second[j];
-      Assert( d_inst_id_to_term.find(inst_id)!=d_inst_id_to_term.end() );
-      Node inst_term = d_inst_id_to_term[inst_id];
-      Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end());
-      Node alit = d_inst_id_to_alit[inst_id];
+      for (unsigned j = 0; j < iti->second.size(); j++) {
+        unsigned inst_id = iti->second[j];
+        Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end());
+        Node inst_term = d_inst_id_to_term[inst_id];
+        Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end());
+        Node alit = d_inst_id_to_alit[inst_id];
 
-      // get the slack value introduced for the asserted literal
-      Node curr_slack_val;
-      std::unordered_map<Node, Node, NodeHashFunction>::iterator itms =
-          d_alit_to_model_slack.find(alit);
-      if (itms != d_alit_to_model_slack.end()) {
-        curr_slack_val = itms->second;
-      }
-
-      // debug printing
-      if( Trace.isOn("cegqi-bv") ){
-        Trace("cegqi-bv") << "   [" << j << "] : ";
-        Trace("cegqi-bv") << inst_term << std::endl;
-        if (!curr_slack_val.isNull()) {
-          Trace("cegqi-bv") << "   ...with slack value : " << curr_slack_val
-                            << std::endl;
+        // get the slack value introduced for the asserted literal
+        Node curr_slack_val;
+        std::unordered_map<Node, Node, NodeHashFunction>::iterator itms =
+            d_alit_to_model_slack.find(alit);
+        if (itms != d_alit_to_model_slack.end()) {
+          curr_slack_val = itms->second;
         }
-        // process information about solved status
-        std::unordered_map< unsigned, BvInverterStatus >::iterator its = d_inst_id_to_status.find( inst_id );
-        Assert( its!=d_inst_id_to_status.end() );
-        if( !(*its).second.d_conds.empty() ){
-          Trace("cegqi-bv") << "   ...with " << (*its).second.d_conds.size() << " side conditions : " << std::endl;
-          for( unsigned k=0; k<(*its).second.d_conds.size(); k++ ){
-            Node cond = (*its).second.d_conds[k];
-            Trace("cegqi-bv") << "       " << cond << std::endl;
+
+        // debug printing
+        if (Trace.isOn("cegqi-bv")) {
+          Trace("cegqi-bv") << "   [" << j << "] : ";
+          Trace("cegqi-bv") << inst_term << std::endl;
+          if (!curr_slack_val.isNull()) {
+            Trace("cegqi-bv") << "   ...with slack value : " << curr_slack_val
+                              << std::endl;
+          }
+          // process information about solved status
+          std::unordered_map<unsigned, BvInverterStatus>::iterator its =
+              d_inst_id_to_status.find(inst_id);
+          Assert(its != d_inst_id_to_status.end());
+          if (!its->second.d_conds.empty()) {
+            Trace("cegqi-bv") << "   ...with " << its->second.d_conds.size()
+                              << " side conditions : " << std::endl;
+            for (unsigned k = 0; k < its->second.d_conds.size(); k++) {
+              Node cond = its->second.d_conds[k];
+              Trace("cegqi-bv") << "       " << cond << std::endl;
+            }
           }
+          Trace("cegqi-bv") << std::endl;
         }
-        Trace("cegqi-bv") << std::endl;
-      }
-
-      // currently we take select the first literal
-      if( inst_ids_try.empty() ){
-        // try the first one
-        inst_ids_try.push_back( inst_id );
-      } else {
-        // selection criteria across multiple literals goes here
-
 
+        // currently we select the first literal
+        if (inst_ids_try.empty()) {
+          // try the first one
+          inst_ids_try.push_back(inst_id);
+        } else {
+          // selection criteria across multiple literals goes here
+        }
       }
-    }
-    
-    // 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
-    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() );
-      Node inst_term = d_inst_id_to_term[inst_id];
-      // try instantiation pv -> inst_term
-      TermProperties pv_prop_bv;
-      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;
+
+      // 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
+      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());
+        Node inst_term = d_inst_id_to_term[inst_id];
+        // try instantiation pv -> inst_term
+        TermProperties pv_prop_bv;
+        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;
+        }
       }
+      Trace("cegqi-bv") << "...failed to add instantiation for " << pv
+                        << std::endl;
+      d_var_to_curr_inst_id.erase(pv);
+    } else {
+      Trace("cegqi-bv") << "...do not do instantiation for " << pv
+                        << " (skip, based on heuristic)" << std::endl;
     }
-    Trace("cegqi-bv") << "...failed to add instantiation for " << pv << std::endl;
-    d_var_to_curr_inst_id.erase( pv );
   }
 
   return false;