Fix quantified bv variable elimination (#2039)

1 files changed, 22 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);