Disable solving non-linear BV literals by default (#2070)

4 files changed, 42 insertions, 8 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 107f3896f..69868ad8d 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1427,6 +1427,14 @@ header = "options/quantifiers_options.h"
   help       = "linearize adder chains for variables"
 
 [[option]]
+  name       = "cbqiBvSolveNl"
+  category   = "regular"
+  long       = "cbqi-bv-solve-nl"
+  type       = "bool"
+  default    = "false"
+  help       = "try to solve non-linear bv literals using model value projections"
+
+[[option]]
   name       = "cbqiBvConcInv"
   category   = "regular"
   long       = "cbqi-bv-concat-inv"
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index b0f7a2cb8..3ff27366b 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -175,8 +175,12 @@ Node BvInverter::getPathToPv(
   return Node::null();
 }
 
-Node BvInverter::getPathToPv(
-    Node lit, Node pv, Node sv, Node pvs, std::vector<unsigned>& path)
+Node BvInverter::getPathToPv(Node lit,
+                             Node pv,
+                             Node sv,
+                             Node pvs,
+                             std::vector<unsigned>& path,
+                             bool projectNl)
 {
   std::unordered_set<TNode, TNodeHashFunction> visited;
   Node slit = getPathToPv(lit, pv, sv, path, visited);
@@ -186,7 +190,14 @@ Node BvInverter::getPathToPv(
     // substitute pvs for the other occurrences of pv
     TNode tpv = pv;
     TNode tpvs = pvs;
+    Node prev_lit = slit;
     slit = slit.substitute(tpv, tpvs);
+    if (!projectNl && slit != prev_lit)
+    {
+      // found another occurrence of pv that was not on the solve path,
+      // hence lit is non-linear wrt pv and we return null.
+      return Node::null();
+    }
   }
   return slit;
 }
diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index 59dc543ae..2d9e04281 100644
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -59,9 +59,16 @@ class BvInverter
    * pvs (if pvs is non-null). If return value R is non-null, then :
    *   lit.path = pv R.path = sv
    *   R.path' = pvs for all lit.path' = pv, where path' != path
+   *
+   * If the flag projectNl is false, we return the null node if the
+   * literal lit is non-linear with respect to pv.
    */
-  Node getPathToPv(
-      Node lit, Node pv, Node sv, Node pvs, std::vector<unsigned>& path);
+  Node getPathToPv(Node lit,
+                   Node pv,
+                   Node sv,
+                   Node pvs,
+                   std::vector<unsigned>& path,
+                   bool projectNl);
 
   /**
    * Same as above, but does not linearize lit for pv.
@@ -69,7 +76,7 @@ class BvInverter
    */
   Node getPathToPv(Node lit, Node pv, std::vector<unsigned>& path)
   {
-    return getPathToPv(lit, pv, pv, Node::null(), path);
+    return getPathToPv(lit, pv, pv, Node::null(), path, false);
   }
 
   /** solveBvLit
diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
index 0274d45cd..cf09cfa55 100644
--- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
@@ -991,8 +991,9 @@ void BvInstantiator::processLiteral(CegInstantiator* ci,
   std::vector<unsigned> path;
   Node sv = d_inverter->getSolveVariable(pv.getType());
   Node pvs = ci->getModelValue(pv);
-  Trace("cegqi-bv") << "Get path to pv : " << lit << std::endl;
-  Node slit = d_inverter->getPathToPv(lit, pv, sv, pvs, path);
+  Trace("cegqi-bv") << "Get path to " << pv << " : " << lit << std::endl;
+  Node slit =
+      d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cbqiBvSolveNl());
   if (!slit.isNull())
   {
     CegInstantiatorBvInverterQuery m(ci);
@@ -1017,6 +1018,10 @@ void BvInstantiator::processLiteral(CegInstantiator* ci,
       Trace("cegqi-bv") << "...failed to solve." << std::endl;
     }
   }
+  else
+  {
+    Trace("cegqi-bv") << "...no path." << std::endl;
+  }
 }
 
 Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
@@ -1981,7 +1986,10 @@ void BvInstantiatorPreprocess::collectExtracts(
       {
         if (cur.getKind() == BITVECTOR_EXTRACT)
         {
-          extract_map[cur[0]].push_back(cur);
+          if (cur[0].getKind() == INST_CONSTANT)
+          {
+            extract_map[cur[0]].push_back(cur);
+          }
         }
 
         for (const Node& nc : cur)