CBQI BV choice expressions (#1296)

* Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently.

* Minor

* Make unique bound variables for choice functions in BvInstantor, clean up.

* Incorporate missing optimizations

* Clang format

* Unused field.

* Minor

* Fix, add regression.

* Fix regression.

* Fix bug that led to incorrect cleanup of instantiations.

* Add missing regression

* Improve handling of choice rewriting.

* Fix

* Clang format

* Use canonical variables for choice functions in cbqi bv.

* Add regression

* Clang format.

* Address review.

* Clang format

1 files changed, 46 insertions, 176 deletions

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 957385a14..d777dc4f8 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -52,21 +52,7 @@ Node BvInverter::getSolveVariable(TypeNode tn)
   std::map<TypeNode, Node>::iterator its = d_solve_var.find(tn);
   if (its == d_solve_var.end())
   {
-    std::stringstream ss;
-    if (tn.isFunction())
-    {
-      Assert(tn.getNumChildren() == 2);
-      Assert(tn[0].isBoolean());
-      ss << "slv_f";
-    }
-    else
-    {
-      ss << "slv";
-    }
-    Node k = NodeManager::currentNM()->mkSkolem(ss.str(), tn);
-    // marked as a virtual term (it is eligible for instantiation)
-    VirtualTermSkolemAttribute vtsa;
-    k.setAttribute(vtsa, true);
+    Node k = NodeManager::currentNM()->mkSkolem("slv", tn);
     d_solve_var[tn] = k;
     return k;
   }
@@ -76,75 +62,50 @@ Node BvInverter::getSolveVariable(TypeNode tn)
   }
 }
 
-Node BvInverter::getInversionSkolemFor(Node cond, TypeNode tn)
+Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m)
 {
   // condition should be rewritten
-  Assert(Rewriter::rewrite(cond) == cond);
-  std::unordered_map<Node, Node, NodeHashFunction>::iterator it =
-      d_inversion_skolem_cache.find(cond);
-  if (it == d_inversion_skolem_cache.end())
+  Node new_cond = Rewriter::rewrite(cond);
+  if (new_cond != cond)
   {
-    Node skv;
-    if (cond.getKind() == EQUAL)
+    Trace("cegqi-bv-skvinv-debug") << "Condition " << cond
+                                   << " was rewritten to " << new_cond
+                                   << std::endl;
+  }
+  Node c;
+  // optimization : if condition is ( x = v ) should just return v and not
+  // introduce a Skolem this can happen when we ask for the multiplicative
+  // inversion with bv1
+  TNode solve_var = getSolveVariable(tn);
+  if (new_cond.getKind() == EQUAL)
+  {
+    for (unsigned i = 0; i < 2; i++)
     {
-      // optimization : if condition is ( x = v ) should just return v and not
-      // introduce a Skolem this can happen when we ask for the multiplicative
-      // inversion with bv1
-      Node x = getSolveVariable(tn);
-      for (unsigned i = 0; i < 2; i++)
+      if (new_cond[i] == solve_var)
       {
-        if (cond[i] == x)
-        {
-          skv = cond[1 - i];
-          Trace("cegqi-bv-skvinv")
-              << "SKVINV : " << skv << " is trivially associated with conditon "
-              << cond << std::endl;
-          break;
-        }
+        c = new_cond[1 - i];
+        Trace("cegqi-bv-skvinv") << "SKVINV : " << c
+                                 << " is trivially associated with conditon "
+                                 << new_cond << std::endl;
+        break;
       }
     }
-    if (skv.isNull())
-    {
-      // TODO : compute the value if the condition is deterministic, e.g. calc
-      // multiplicative inverse of 2 constants
-      skv = NodeManager::currentNM()->mkSkolem(
-          "skvinv", tn, "created for BvInverter");
-      Trace("cegqi-bv-skvinv")
-          << "SKVINV : " << skv << " is the skolem associated with conditon "
-          << cond << std::endl;
-      // marked as a virtual term (it is eligible for instantiation)
-      VirtualTermSkolemAttribute vtsa;
-      skv.setAttribute(vtsa, true);
-    }
-    d_inversion_skolem_cache[cond] = skv;
-    return skv;
-  }
-  else
-  {
-    Assert(it->second.getType() == tn);
-    return it->second;
   }
-}
-
-Node BvInverter::getInversionSkolemFunctionFor(TypeNode tn)
-{
-  NodeManager* nm = NodeManager::currentNM();
-  // function maps conditions to skolems
-  TypeNode ftn = nm->mkFunctionType(nm->booleanType(), tn);
-  return getSolveVariable(ftn);
-}
-
-Node BvInverter::getInversionNode(Node cond, TypeNode tn)
-{
-  // condition should be rewritten
-  Node new_cond = Rewriter::rewrite(cond);
-  if (new_cond != cond)
+  // TODO : compute the value if the condition is deterministic, e.g. calc
+  // multiplicative inverse of 2 constants
+  if (c.isNull())
   {
-    Trace("bv-invert-debug") << "Condition " << cond << " was rewritten to "
-                             << new_cond << std::endl;
+    NodeManager* nm = NodeManager::currentNM();
+    Node x = m->getBoundVariable(tn);
+    Node ccond = new_cond.substitute(solve_var, x);
+    c = nm->mkNode(kind::CHOICE, nm->mkNode(BOUND_VAR_LIST, x), ccond);
+    Trace("cegqi-bv-skvinv") << "SKVINV : Make " << c << " for " << new_cond
+                             << std::endl;
   }
-  Node f = getInversionSkolemFunctionFor(tn);
-  return NodeManager::currentNM()->mkNode(kind::APPLY_UF, f, new_cond);
+  // currently shouldn't cache since
+  // the return value depends on the
+  // state of m (which bound variable is returned).
+  return c;
 }
 
 bool BvInverter::isInvertible(Kind k, unsigned index)
@@ -219,97 +180,6 @@ Node BvInverter::getPathToPv(
   return Node::null();
 }
 
-Node BvInverter::eliminateSkolemFunctions(TNode n,
-                                          std::vector<Node>& side_conditions)
-{
-  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
-  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
-  std::stack<TNode> visit;
-  TNode cur;
-
-  visit.push(n);
-  do
-  {
-    cur = visit.top();
-    visit.pop();
-    it = visited.find(cur);
-
-    if (it == visited.end())
-    {
-      visited[cur] = Node::null();
-      visit.push(cur);
-      for (unsigned i = 0; i < cur.getNumChildren(); i++)
-      {
-        visit.push(cur[i]);
-      }
-    }
-    else if (it->second.isNull())
-    {
-      Trace("bv-invert-debug")
-          << "eliminateSkolemFunctions from " << cur << "..." << std::endl;
-
-      Node ret = cur;
-      bool childChanged = false;
-      std::vector<Node> children;
-      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
-      {
-        children.push_back(cur.getOperator());
-      }
-      for (unsigned i = 0; i < cur.getNumChildren(); i++)
-      {
-        it = visited.find(cur[i]);
-        Assert(it != visited.end());
-        Assert(!it->second.isNull());
-        childChanged = childChanged || cur[i] != it->second;
-        children.push_back(it->second);
-      }
-      if (childChanged)
-      {
-        ret = NodeManager::currentNM()->mkNode(cur.getKind(), children);
-      }
-      // now, check if it is a skolem function
-      if (ret.getKind() == APPLY_UF)
-      {
-        Node op = ret.getOperator();
-        TypeNode tnp = op.getType();
-        // is this a skolem function?
-        std::map<TypeNode, Node>::iterator its = d_solve_var.find(tnp);
-        if (its != d_solve_var.end() && its->second == op)
-        {
-          Assert(ret.getNumChildren() == 1);
-          Assert(ret[0].getType().isBoolean());
-
-          Node cond = ret[0];
-          // must rewrite now to ensure we lookup the correct skolem
-          cond = Rewriter::rewrite(cond);
-
-          // if so, we replace by the (finalized) skolem variable
-          // Notice that since we are post-rewriting, skolem functions are
-          // already eliminated from cond
-          ret = getInversionSkolemFor(cond, ret.getType());
-
-          // also must add (substituted) side condition to vector
-          // substitute ( solve variable -> inversion skolem )
-          TNode solve_var = getSolveVariable(ret.getType());
-          TNode tret = ret;
-          cond = cond.substitute(solve_var, tret);
-          if (std::find(side_conditions.begin(), side_conditions.end(), cond)
-              == side_conditions.end())
-          {
-            side_conditions.push_back(cond);
-          }
-        }
-      }
-      Trace("bv-invert-debug") << "eliminateSkolemFunctions from " << cur
-                               << " returned " << ret << std::endl;
-      visited[cur] = ret;
-    }
-  } while (!visit.empty());
-  Assert(visited.find(n) != visited.end());
-  Assert(!visited.find(n)->second.isNull());
-  return visited[n];
-}
-
 Node BvInverter::getPathToPv(
     Node lit, Node pv, Node sv, Node pvs, std::vector<unsigned>& path)
 {
@@ -329,7 +199,7 @@ Node BvInverter::getPathToPv(
 Node BvInverter::solve_bv_lit(Node sv,
                               Node lit,
                               std::vector<unsigned>& path,
-                              BvInverterModelQuery* m,
+                              BvInverterQuery* m,
                               BvInverterStatus& status)
 {
   Assert(!path.empty());
@@ -413,7 +283,7 @@ Node BvInverter::solve_bv_lit(Node sv,
       }
       status.d_conds.push_back(sc);
       /* t = skv (fresh skolem constant)  */
-      Node skv = getInversionNode(sc, solve_tn);
+      Node skv = getInversionNode(sc, solve_tn, m);
       t = skv;
       if (!path.empty())
       {
@@ -469,7 +339,7 @@ Node BvInverter::solve_bv_lit(Node sv,
       }
       status.d_conds.push_back(sc);
       /* t = skv (fresh skolem constant)  */
-      Node skv = getInversionNode(sc, solve_tn);
+      Node skv = getInversionNode(sc, solve_tn, m);
       t = skv;
       if (!path.empty())
       {
@@ -502,7 +372,7 @@ Node BvInverter::solve_bv_lit(Node sv,
         Node sc = nm->mkNode(IMPLIES, scl, scr);
         status.d_conds.push_back(sc);
         /* t = skv (fresh skolem constant)  */
-        Node skv = getInversionNode(sc, solve_tn);
+        Node skv = getInversionNode(sc, solve_tn, m);
         t = skv;
         if (!path.empty())
         {
@@ -599,7 +469,7 @@ Node BvInverter::solve_bv_lit(Node sv,
 
           /* t = skv (fresh skolem constant)
            * get the skolem node for this side condition  */
-          Node skv = getInversionNode(sc, solve_tn);
+          Node skv = getInversionNode(sc, solve_tn, m);
           /* now solving with the skolem node as the RHS  */
           t = skv;
           break;
@@ -641,7 +511,7 @@ Node BvInverter::solve_bv_lit(Node sv,
           }
           Node sc = nm->mkNode(IMPLIES, scl, scr);
           status.d_conds.push_back(sc);
-          Node skv = getInversionNode(sc, solve_tn);
+          Node skv = getInversionNode(sc, solve_tn, m);
           t = skv;
           break;
         }
@@ -694,7 +564,7 @@ Node BvInverter::solve_bv_lit(Node sv,
 
           /* t = skv (fresh skolem constant)
            * get the skolem node for this side condition */
-          Node skv = getInversionNode(sc, solve_tn);
+          Node skv = getInversionNode(sc, solve_tn, m);
           /* now solving with the skolem node as the RHS */
           t = skv;
           break;
@@ -713,7 +583,7 @@ Node BvInverter::solve_bv_lit(Node sv,
           Node sc = nm->mkNode(IMPLIES, scl, scr);
           status.d_conds.push_back(sc);
           /* t = skv (fresh skolem constant)  */
-          Node skv = getInversionNode(sc, solve_tn);
+          Node skv = getInversionNode(sc, solve_tn, m);
           t = skv;
           break;
         }
@@ -749,7 +619,7 @@ Node BvInverter::solve_bv_lit(Node sv,
             Node sc = nm->mkNode(IMPLIES, scl, scr);
             status.d_conds.push_back(sc);
             /* t = skv (fresh skolem constant)  */
-            Node skv = getInversionNode(sc, solve_tn);
+            Node skv = getInversionNode(sc, solve_tn, m);
             t = skv;
           }
           else
@@ -793,7 +663,7 @@ Node BvInverter::solve_bv_lit(Node sv,
             Node sc = nm->mkNode(IMPLIES, scl, scr);
             status.d_conds.push_back(sc);
             /* t = skv (fresh skolem constant)  */
-            Node skv = getInversionNode(sc, solve_tn);
+            Node skv = getInversionNode(sc, solve_tn, m);
             t = skv;
           }
           else
@@ -863,7 +733,7 @@ Node BvInverter::solve_bv_lit(Node sv,
 
           /* t = skv (fresh skolem constant)
            * get the skolem node for this side condition */
-          Node skv = getInversionNode(sc, solve_tn);
+          Node skv = getInversionNode(sc, solve_tn, m);
           /* now solving with the skolem node as the RHS */
           t = skv;
           break;