Fix quantified bv variable elimination (#2039)

3 files changed, 27 insertions, 42 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index bb92cbaf7..c3dcdf6dc 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -926,56 +926,35 @@ Node QuantifiersRewriter::computeVariableElimLitBv(Node lit,
   Assert(lit.getKind() == EQUAL);
   // TODO (#1494) : linearize the literal using utility
 
-  // figure out if this literal is linear and invertible on path with args
-  std::map<TNode, bool> linear;
-  std::unordered_set<TNode, TNodeHashFunction> visited;
-  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
-  std::vector<TNode> visit;
-  TNode cur;
-  visit.push_back(lit);
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    if (std::find(args.begin(), args.end(), cur) != args.end())
-    {
-      bool lval = linear.find(cur) == linear.end();
-      linear[cur] = lval;
-    }
-    if (visited.find(cur) == visited.end())
-    {
-      visited.insert(cur);
-
-      for (const Node& cn : cur)
-      {
-        visit.push_back(cn);
-      }
-    }
-  } while (!visit.empty());
+  // compute a subset active_args of the bound variables args that occur in lit
+  std::vector<Node> active_args;
+  computeArgVec(args, active_args, lit);
 
   BvInverter binv;
-  for (std::pair<const TNode, bool>& lp : linear)
+  for (const Node& cvar : active_args)
   {
-    if (lp.second)
+    // solve for the variable on this path using the inverter
+    std::vector<unsigned> path;
+    Node slit = binv.getPathToPv(lit, cvar, path);
+    if (!slit.isNull())
     {
-      TNode cvar = lp.first;
-      Trace("quant-velim-bv") << "...linear wrt " << cvar << std::endl;
-      std::vector<unsigned> path;
-      Node slit = binv.getPathToPv(lit, cvar, path);
-      if (!slit.isNull())
+      Node slv = binv.solveBvLit(cvar, lit, path, nullptr);
+      Trace("quant-velim-bv") << "...solution : " << slv << std::endl;
+      if (!slv.isNull())
       {
-        Node slv = binv.solveBvLit(cvar, lit, path, nullptr);
-        Trace("quant-velim-bv") << "...solution : " << slv << std::endl;
-        if (!slv.isNull())
+        var = cvar;
+        // if this is a proper variable elimination, that is, var = slv where
+        // var is not in the free variables of slv, then we can return this
+        // as the variable elimination for lit.
+        if (isVariableElim(var, slv))
         {
-          var = cvar;
           return slv;
         }
       }
-      else
-      {
-        Trace("quant-velim-bv") << "...non-invertible path." << std::endl;
-      }
+    }
+    else
+    {
+      Trace("quant-velim-bv") << "...non-invertible path." << std::endl;
     }
   }
 
@@ -1130,10 +1109,11 @@ bool QuantifiersRewriter::computeVariableElimLit(
       std::vector<Node>::iterator ita =
           std::find(args.begin(), args.end(), var);
       Assert(ita != args.end());
-      Assert(isVariableElim(var, slv));
       Trace("var-elim-quant")
           << "Variable eliminate based on bit-vector inversion : " << var
           << " -> " << slv << std::endl;
+      Assert(!slv.hasSubterm(var));
+      Assert(slv.getType().isSubtypeOf(var.getType()));
       vars.push_back(var);
       subs.push_back(slv);
       args.erase(ita);
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index b40b28dae..d235f27d3 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -600,6 +600,7 @@ REG0_TESTS = \
 	regress0/quantifiers/floor.smt2 \
 	regress0/quantifiers/is-even-pred.smt2 \
 	regress0/quantifiers/is-int.smt2 \
+	regress0/quantifiers/issue2031-bv-var-elim.smt2 \
 	regress0/quantifiers/issue1805.smt2 \
 	regress0/quantifiers/lra-triv-gn.smt2 \
 	regress0/quantifiers/macros-int-real.smt2 \
diff --git a/test/regress/regress0/quantifiers/issue2031-bv-var-elim.smt2 b/test/regress/regress0/quantifiers/issue2031-bv-var-elim.smt2
new file mode 100644
index 000000000..0585c5d67
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue2031-bv-var-elim.smt2
@@ -0,0 +1,4 @@
+(set-logic BV)
+(set-info :status unsat)
+(assert (exists ((?y2 (_ BitVec 32))) (exists ((?y3 (_ BitVec 32))) (forall ((?y5 (_ BitVec 32))) (forall ((?y6 (_ BitVec 32))) (not (= (bvadd (bvadd (bvadd (bvadd (bvmul (bvneg (_ bv65 32)) ?y6) (bvmul (bvneg (_ bv93 32)) ?y5)) (_ bv0 32)) (_ bv0 32)) (_ bv0 32)) (_ bv69 32))))))))
+(check-sat)