Improvements for CBQI BV (#1504)

3 files changed, 108 insertions, 114 deletions

diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 275d7238d..e617819d7 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -994,12 +994,15 @@ void BvInstantiator::processLiteral(CegInstantiator* ci,
     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++;
+      if (inst.isConst() || !ci->hasNestedQuantification())
+      {
+        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
     {
@@ -1022,90 +1025,80 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
   Node atom = lit.getKind() == NOT ? lit[0] : lit;
   bool pol = lit.getKind() != NOT;
   Kind k = atom.getKind();
-  if (pol && k == EQUAL)
+  if (k != EQUAL && k != BITVECTOR_ULT && k != BITVECTOR_SLT)
   {
-    // positively asserted equalities between bitvector terms we always leave
-    // unmodified
-    if (atom[0].getType().isBitVector()) {
-      return lit;
-    }
+    // others are unhandled
+    return Node::null();
+  }
+  else if (!atom[0].getType().isBitVector())
+  {
+    return Node::null();
+  }
+  else if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_KEEP
+           || (pol && k == EQUAL))
+  {
+    return lit;
   }
-  else if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_KEEP)
+  NodeManager* nm = NodeManager::currentNM();
+  Node s = atom[0];
+  Node t = atom[1];
+
+  Node sm = ci->getModelValue(s);
+  Node tm = ci->getModelValue(t);
+  Assert(!sm.isNull() && sm.isConst());
+  Assert(!tm.isNull() && tm.isConst());
+  Trace("cegqi-bv") << "Model value: " << std::endl;
+  Trace("cegqi-bv") << "   " << s << " " << k << " " << t << " is "
+                    << std::endl;
+  Trace("cegqi-bv") << "   " << sm << " <> " << tm << std::endl;
+
+  Node ret;
+  if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_EQ_SLACK)
   {
-    // if option is set, disequalities and inequalities we leave unmodified
-    if ((k == EQUAL && atom[0].getType().isBitVector()) || k == BITVECTOR_ULT
-        || k == BITVECTOR_SLT)
+    // if using slack, we convert constraints to a positive equality based on
+    // the current model M, e.g.:
+    //   (not) s ~ t  --->  s = t + ( s^M - t^M )
+    if (sm != tm)
+    {
+      Node slack = Rewriter::rewrite(nm->mkNode(BITVECTOR_SUB, sm, tm));
+      Assert(slack.isConst());
+      // remember the slack value for the asserted literal
+      d_alit_to_model_slack[lit] = slack;
+      ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_PLUS, t, slack));
+      Trace("cegqi-bv") << "Slack is " << slack << std::endl;
+    }
+    else
     {
-      return lit;
+      ret = s.eqNode(t);
     }
   } else {
-    bool useSlack = false;
-    if (k == EQUAL && atom[0].getType().isBitVector())
+    // turn disequality into an inequality
+    // e.g. s != t becomes s < t or t < s
+    if (k == EQUAL)
     {
-      // always use slack for disequalities
-      useSlack = true;
-    } else if (k == BITVECTOR_ULT || k == BITVECTOR_SLT) {
-      if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_EQ_SLACK)
+      if (Random::getRandom().pickWithProb(0.5))
       {
-        useSlack = true;
+        std::swap(s, t);
       }
-    } else {
-      // others are not unhandled
-      return Node::null();
+      pol = true;
     }
-    // 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 (useSlack) {
-      Node s = atom[0];
-      Node t = atom[1];
-      // only handle equalities between bitvectors
-      if (s.getType().isBitVector()) {
-        NodeManager* nm = NodeManager::currentNM();
-        Node sm = ci->getModelValue(s);
-        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;
-          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;
-        } else {
-          ret = s.eqNode(t);          
-          Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl;
-        }
-        return ret;
-      }
+    // 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.
+    if (!pol)
+    {
+      ret = s.eqNode(t);
     } 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;
+      Node bv_one = bv::utils::mkOne(bv::utils::getSize(s));
+      ret = nm->mkNode(BITVECTOR_PLUS, s, bv_one).eqNode(t);
     }
   }
-  return Node::null();
+  Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl;
+  return ret;
 }
 
 bool BvInstantiator::processAssertion(CegInstantiator* ci,
@@ -1126,7 +1119,10 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci,
         Trace("cegqi-bv") << "...rewritten to " << rlit << std::endl;
       }
     }
-    processLiteral(ci, sf, pv, rlit, alit, effort);
+    if (!rlit.isNull())
+    {
+      processLiteral(ci, sf, pv, rlit, alit, effort);
+    }
   }
   return false;
 }
@@ -1163,8 +1159,6 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci,
           Trace("cegqi-bv") << "  ...this is the first variable" << 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
@@ -1173,53 +1167,47 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci,
       // 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];
-
-        // 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;
-        }
+      if (Trace.isOn("cegqi-bv"))
+      {
+        for (unsigned j = 0, size = iti->second.size(); j < 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")) {
+          // debug printing
           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;
           }
+          Trace("cegqi-bv-debug") << "   ...from : " << alit << std::endl;
           Trace("cegqi-bv") << std::endl;
         }
-
-        // currently:
-        //   We select the first literal, and
-        //   for the first variable, we select all 
-        //   if cbqiMultiInst is enabled.
-        if (inst_ids_try.empty() || (firstVar && options::cbqiMultiInst()))
-        {
-          // 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 )<=1, otherwise worst-case performance
+      // Typically we try only one, otherwise worst-case performance
       // for constructing instantiations is exponential on the number of
       // variables in this quantifier prefix.
       bool ret = false;
-      bool revertOnSuccess = inst_ids_try.size() > 1;
-      for (unsigned j = 0; j < inst_ids_try.size(); j++) {
-        unsigned inst_id = inst_ids_try[j];
+      bool tryMultipleInst = firstVar && options::cbqiMultiInst();
+      bool revertOnSuccess = tryMultipleInst;
+      for (unsigned j = 0, size = iti->second.size(); j < 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];
         Node alit = d_inst_id_to_alit[inst_id];
@@ -1236,6 +1224,11 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci,
           ret = true;
         }
         ci->markSolved(alit, false);
+        // we are done unless we try multiple instances
+        if (!tryMultipleInst)
+        {
+          break;
+        }
       }
       if (ret)
       {
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 17214112b..472316cae 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -920,7 +920,8 @@ Node QuantifiersRewriter::computeVariableElimLitBv(Node lit,
     visit.pop_back();
     if (std::find(args.begin(), args.end(), cur) != args.end())
     {
-      linear[cur] = linear.find(cur) == linear.end();
+      bool lval = linear.find(cur) == linear.end();
+      linear[cur] = lval;
     }
     if (visited.find(cur) == visited.end())
     {
diff --git a/test/regress/regress0/sygus/Base16_1.sy b/test/regress/regress0/sygus/Base16_1.sy
index 5833751cb..b54c7688b 100644
--- a/test/regress/regress0/sygus/Base16_1.sy
+++ b/test/regress/regress0/sygus/Base16_1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE:  --sygus-qe-preproc --cbqi-bv-rm-extract --sygus-out=status --cbqi-bv --cegqi-si=all
+; COMMAND-LINE:  --sygus-qe-preproc --cbqi-full --sygus-out=status --cegqi-si=all
 (set-logic BV)
 
 (define-fun B ((h (BitVec 8)) (l (BitVec 8)) (v (BitVec 8))) (BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l))))