Enhancement: make the bool-to-bv pass more robust and targeted (#3021)

This pull request is an improvement to the bool-to-bv preprocessing pass. The existing pass is both too weak and too strong, depending on the circumstance. Throughout this description, "lower" refers to lowering a boolean to a bit-vector.

2 files changed, 318 insertions, 127 deletions

diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index 30b64fd74..b4d638595 100644
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -19,7 +19,6 @@
 
 #include "base/map_util.h"
 #include "expr/node.h"
-#include "options/bv_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
@@ -30,7 +29,10 @@ namespace passes {
 using namespace CVC4::theory;
 
 BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext)
-    : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics(){};
+    : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics()
+{
+  d_boolToBVMode = options::boolToBitvector();
+};
 
 PreprocessingPassResult BoolToBV::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
@@ -38,31 +40,73 @@ PreprocessingPassResult BoolToBV::applyInternal(
   NodeManager::currentResourceManager()->spendResource(
       ResourceManager::Resource::PreprocessStep);
 
-  unsigned size = assertionsToPreprocess->size();
-  for (unsigned i = 0; i < size; ++i)
+  size_t size = assertionsToPreprocess->size();
+
+  if (d_boolToBVMode == options::BoolToBVMode::ALL)
+  {
+    for (size_t i = 0; i < size; ++i)
+    {
+      Node newAssertion = lowerAssertion((*assertionsToPreprocess)[i], true);
+      assertionsToPreprocess->replace(i, Rewriter::rewrite(newAssertion));
+    }
+  }
+  else
   {
-    assertionsToPreprocess->replace(
-        i, Rewriter::rewrite(lowerAssertion((*assertionsToPreprocess)[i])));
+    Assert(d_boolToBVMode == options::BoolToBVMode::ITE);
+    for (size_t i = 0; i < size; ++i)
+    {
+      assertionsToPreprocess->replace(
+          i, Rewriter::rewrite(lowerIte((*assertionsToPreprocess)[i])));
+    }
   }
 
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+void BoolToBV::updateCache(TNode n, TNode rebuilt)
+{
+  // check more likely case first
+  if ((n.getKind() != kind::ITE) || !n[1].getType().isBitVector())
+  {
+    d_lowerCache[n] = rebuilt;
+  }
+  else
+  {
+    d_iteBVLowerCache[n] = rebuilt;
+  }
+}
+
 Node BoolToBV::fromCache(TNode n) const
 {
-  if (d_lowerCache.find(n) != d_lowerCache.end())
+  // check more likely case first
+  if (n.getKind() != kind::ITE)
   {
-    return d_lowerCache.find(n)->second;
+    if (d_lowerCache.find(n) != d_lowerCache.end())
+    {
+      return d_lowerCache.at(n);
+    }
+  }
+  else
+  {
+    if (d_iteBVLowerCache.find(n) != d_iteBVLowerCache.end())
+    {
+      return d_iteBVLowerCache.at(n);
+    }
   }
   return n;
 }
 
+inline bool BoolToBV::inCache(const Node& n) const
+{
+  return (ContainsKey(d_lowerCache, n) || ContainsKey(d_iteBVLowerCache, n));
+}
+
 bool BoolToBV::needToRebuild(TNode n) const
 {
   // check if any children were rebuilt
   for (const Node& nn : n)
   {
-    if (ContainsKey(d_lowerCache, nn))
+    if (inCache(nn))
     {
       return true;
     }
@@ -70,134 +114,82 @@ bool BoolToBV::needToRebuild(TNode n) const
   return false;
 }
 
-Node BoolToBV::lowerAssertion(const TNode& a)
+Node BoolToBV::lowerAssertion(const TNode& assertion, bool allowIteIntroduction)
 {
-  bool optionITE = options::boolToBitvector() == options::BoolToBVMode::ITE;
-  NodeManager* nm = NodeManager::currentNM();
-  std::vector<TNode> visit;
-  visit.push_back(a);
+  // first try to lower all the children
+  for (const Node& c : assertion)
+  {
+    lowerNode(c, allowIteIntroduction);
+  }
+
+  // now try lowering the assertion, but don't force it with an ITE (even in mode all)
+  lowerNode(assertion, false);
+  Node newAssertion = fromCache(assertion);
+  TypeNode newAssertionType = newAssertion.getType();
+  if (newAssertionType.isBitVector())
+  {
+    Assert(newAssertionType.getBitVectorSize() == 1);
+    newAssertion = NodeManager::currentNM()->mkNode(
+        kind::EQUAL, newAssertion, bv::utils::mkOne(1));
+    newAssertionType = newAssertion.getType();
+  }
+  Assert(newAssertionType.isBoolean());
+  return newAssertion;
+}
+
+Node BoolToBV::lowerNode(const TNode& node, bool allowIteIntroduction)
+{
+  std::vector<TNode> to_visit;
+  to_visit.push_back(node);
   std::unordered_set<TNode, TNodeHashFunction> visited;
-  // for ite mode, keeps track of whether you're in an ite condition
-  // for all mode, unused
-  std::unordered_set<TNode, TNodeHashFunction> ite_cond;
 
-  while (!visit.empty())
+  while (!to_visit.empty())
   {
-    TNode n = visit.back();
-    visit.pop_back();
+    TNode n = to_visit.back();
+    to_visit.pop_back();
 
-    int numChildren = n.getNumChildren();
-    Kind k = n.getKind();
-    Debug("bool-to-bv") << "BoolToBV::lowerAssertion Post-traversal with " << n
-                        << " and visited = " << ContainsKey(visited, n)
+    Debug("bool-to-bv") << "BoolToBV::lowerNode: Post-order traversal with "
+                        << n << " and visited = " << ContainsKey(visited, n)
                         << std::endl;
 
     // Mark as visited
-    /* Optimization: if it's a leaf, don't need to wait to do the work */
-    if (!ContainsKey(visited, n) && (numChildren > 0))
+    if (ContainsKey(visited, n))
+    {
+      visit(n, allowIteIntroduction);
+    }
+    else
     {
       visited.insert(n);
-      visit.push_back(n);
+      to_visit.push_back(n);
 
       // insert children in reverse order so that they're processed in order
-      //     important for rewriting which sorts by node id
-      for (int i = numChildren - 1; i >= 0; --i)
+      //    important for rewriting which sorts by node id
+      // NOTE: size_t is unsigned, so using underflow for termination condition
+      size_t numChildren = n.getNumChildren();
+      for (size_t i = numChildren - 1; i < numChildren; --i)
       {
-        visit.push_back(n[i]);
-      }
-
-      if (optionITE)
-      {
-        // check for ite-conditions
-        if (k == kind::ITE)
-        {
-          ite_cond.insert(n[0]);
-        }
-        else if (ContainsKey(ite_cond, n))
-        {
-          // being part of an ite condition is inherited from the parent
-          ite_cond.insert(n.begin(), n.end());
-        }
+        to_visit.push_back(n[i]);
       }
     }
-    /* Optimization for ite mode */
-    else if (optionITE && !ContainsKey(ite_cond, n) && !needToRebuild(n))
-    {
-      Debug("bool-to-bv")
-          << "BoolToBV::lowerAssertion Skipping because don't need to rebuild: "
-          << n << std::endl;
-      // in ite mode, if you've already visited the node but it's not
-      // in an ite condition and doesn't need to be rebuilt, then
-      // don't need to do anything
-      continue;
-    }
-    else
-    {
-      lowerNode(n);
-    }
   }
 
-  if (fromCache(a).getType().isBitVector())
-  {
-    return nm->mkNode(kind::EQUAL, fromCache(a), bv::utils::mkOne(1));
-  }
-  else
-  {
-    Assert(a == fromCache(a));
-    return a;
-  }
+  return fromCache(node);
 }
 
-void BoolToBV::lowerNode(const TNode& n)
+void BoolToBV::visit(const TNode& n, bool allowIteIntroduction)
 {
-  NodeManager* nm = NodeManager::currentNM();
   Kind k = n.getKind();
 
-  bool all_bv = true;
-  // check if it was able to convert all children to bitvectors
-  for (const Node& nn : n)
+  // easy case -- just replace boolean constant
+  if (k == kind::CONST_BOOLEAN)
   {
-    all_bv = all_bv && fromCache(nn).getType().isBitVector();
-    if (!all_bv)
-    {
-      break;
-    }
-  }
-
-  if (!all_bv || (n.getNumChildren() == 0))
-  {
-    if ((options::boolToBitvector() == options::BoolToBVMode::ALL)
-        && n.getType().isBoolean())
-    {
-      if (k == kind::CONST_BOOLEAN)
-      {
-        d_lowerCache[n] = (n == bv::utils::mkTrue()) ? bv::utils::mkOne(1)
-                                                     : bv::utils::mkZero(1);
-      }
-      else
-      {
-        d_lowerCache[n] =
-            nm->mkNode(kind::ITE, n, bv::utils::mkOne(1), bv::utils::mkZero(1));
-      }
-
-      Debug("bool-to-bv") << "BoolToBV::lowerNode " << n << " =>\n"
-                          << fromCache(n) << std::endl;
-      ++(d_statistics.d_numTermsForcedLowered);
-      return;
-    }
-    else
-    {
-      // invariant
-      // either one of the children is not a bit-vector or bool
-      //   i.e. something that can't be 'forced' to a bitvector
-      // or it's in 'ite' mode which will give up on bools that
-      //   can't be converted easily
-
-      Debug("bool-to-bv") << "BoolToBV::lowerNode skipping: " << n << std::endl;
-      return;
-    }
+    updateCache(n,
+                (n == bv::utils::mkTrue()) ? bv::utils::mkOne(1)
+                                           : bv::utils::mkZero(1));
+    return;
   }
 
+  NodeManager* nm = NodeManager::currentNM();
   Kind new_kind = k;
   switch (k)
   {
@@ -221,9 +213,154 @@ void BoolToBV::lowerNode(const TNode& n)
     default: break;
   }
 
+  // check if it's safe to lower or rebuild the node
+  // Note: might have to rebuild to keep changes to children, even if this node
+  // isn't being lowered
+
+  // it's safe to lower if all the children are bit-vectors
+  bool safe_to_lower =
+      (new_kind != k);  // don't need to lower at all if kind hasn't changed
+
+  // it's safe to rebuild if rebuilding doesn't change any of the types of the
+  // children
+  bool safe_to_rebuild = true;
+
+  for (const Node& nn : n)
+  {
+    safe_to_lower = safe_to_lower && fromCache(nn).getType().isBitVector();
+    safe_to_rebuild = safe_to_rebuild && (fromCache(nn).getType() == nn.getType());
+
+    // if it's already not safe to do either, stop checking
+    if (!safe_to_lower && !safe_to_rebuild)
+    {
+      break;
+    }
+  }
+
+  Debug("bool-to-bv") << "safe_to_lower = " << safe_to_lower
+                      << ", safe_to_rebuild = " << safe_to_rebuild << std::endl;
+
+  if (new_kind != k && safe_to_lower)
+  {
+    // lower to BV
+    rebuildNode(n, new_kind);
+    return;
+  }
+  else if (new_kind != k && allowIteIntroduction && fromCache(n).getType().isBoolean())
+  {
+    // lower to BV using an ITE
+
+    if (safe_to_rebuild && needToRebuild(n))
+    {
+      // need to rebuild to keep changes made to descendants
+      rebuildNode(n, k);
+    }
+
+    updateCache(n,
+                nm->mkNode(kind::ITE,
+                           fromCache(n),
+                           bv::utils::mkOne(1),
+                           bv::utils::mkZero(1)));
+    Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
+                        << " =>\n"
+                        << fromCache(n) << std::endl;
+    ++(d_statistics.d_numIntroducedItes);
+    return;
+  }
+  else if (safe_to_rebuild && needToRebuild(n))
+  {
+    // rebuild to incorporate changes to children
+    Assert(k == new_kind);
+    rebuildNode(n, k);
+  }
+  else if (allowIteIntroduction && fromCache(n).getType().isBoolean())
+  {
+    // force booleans (which haven't already been converted) to bit-vector
+    // needed to maintain the invariant that all boolean children
+    // have been converted (even constants and variables) when forcing
+    // with ITE introductions
+    updateCache(
+        n, nm->mkNode(kind::ITE, n, bv::utils::mkOne(1), bv::utils::mkZero(1)));
+    Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
+                        << " =>\n"
+                        << fromCache(n) << std::endl;
+    ++(d_statistics.d_numIntroducedItes);
+  }
+  else
+  {
+    // do nothing
+    Debug("bool-to-bv") << "BoolToBV::visit skipping: " << n
+                        << std::endl;
+  }
+}
+
+Node BoolToBV::lowerIte(const TNode& node)
+{
+  std::vector<TNode> visit;
+  visit.push_back(node);
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+
+  while (!visit.empty())
+  {
+    TNode n = visit.back();
+    visit.pop_back();
+
+    Debug("bool-to-bv") << "BoolToBV::lowerIte: Post-order traversal with " << n
+                        << " and visited = " << ContainsKey(visited, n)
+                        << std::endl;
+
+    // Look for ITEs and mark visited
+    if (!ContainsKey(visited, n))
+    {
+      if ((n.getKind() == kind::ITE) && n[1].getType().isBitVector())
+      {
+        Debug("bool-to-bv") << "BoolToBV::lowerIte: adding " << n[0]
+                            << " to set of ite conditions" << std::endl;
+        // don't force in this case -- forcing only introduces more ITEs
+        Node loweredNode = lowerNode(n, false);
+        // some of the lowered nodes might appear elsewhere but not in an ITE
+        // reset the cache to prevent lowering them
+        // the bit-vector ITEs are still tracked in d_iteBVLowerCache though
+        d_lowerCache.clear();
+      }
+      else
+      {
+        visit.push_back(n);
+        visited.insert(n);
+        // insert in reverse order so that they're processed in order
+        for (int i = n.getNumChildren() - 1; i >= 0; --i)
+        {
+          visit.push_back(n[i]);
+        }
+      }
+    }
+    else if (needToRebuild(n))
+    {
+      // Note: it's always safe to rebuild here, because we've only lowered
+      //       ITEs of type bit-vector to BITVECTOR_ITE
+      rebuildNode(n, n.getKind());
+    }
+    else
+    {
+      Debug("bool-to-bv")
+          << "BoolToBV::lowerIte Skipping because don't need to rebuild: " << n
+          << std::endl;
+    }
+  }
+  return fromCache(node);
+}
+
+void BoolToBV::rebuildNode(const TNode& n, Kind new_kind)
+{
+  Kind k = n.getKind();
+  NodeManager* nm = NodeManager::currentNM();
   NodeBuilder<> builder(new_kind);
-  if ((options::boolToBitvector() == options::BoolToBVMode::ALL)
-      && (new_kind != k))
+
+  Debug("bool-to-bv") << "BoolToBV::rebuildNode with " << n
+                      << " and new_kind = " << kindToString(new_kind)
+                      << std::endl;
+
+  if ((d_boolToBVMode == options::BoolToBVMode::ALL) && (new_kind != k))
   {
     ++(d_statistics.d_numTermsLowered);
   }
@@ -234,7 +371,7 @@ void BoolToBV::lowerNode(const TNode& n)
   }
 
   // special case IMPLIES because needs to be rewritten
-  if (k == kind::IMPLIES)
+  if ((k == kind::IMPLIES) && (new_kind != k))
   {
     builder << nm->mkNode(kind::BITVECTOR_NOT, fromCache(n[0]));
     builder << fromCache(n[1]);
@@ -247,16 +384,16 @@ void BoolToBV::lowerNode(const TNode& n)
     }
   }
 
-  Debug("bool-to-bv") << "BoolToBV::lowerNode " << n << " =>\n"
+  Debug("bool-to-bv") << "BoolToBV::rebuildNode " << n << " =>\n"
                       << builder << std::endl;
 
-  d_lowerCache[n] = builder.constructNode();
+  updateCache(n, builder.constructNode());
 }
 
 BoolToBV::Statistics::Statistics()
     : d_numIteToBvite("preprocessing::passes::BoolToBV::NumIteToBvite", 0),
       d_numTermsLowered("preprocessing::passes:BoolToBV::NumTermsLowered", 0),
-      d_numTermsForcedLowered(
+      d_numIntroducedItes(
           "preprocessing::passes::BoolToBV::NumTermsForcedLowered", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_numIteToBvite);
@@ -266,7 +403,7 @@ BoolToBV::Statistics::Statistics()
     // because it might discard rebuilt nodes if it fails to
     // convert a bool to width-one bit-vector (never forces)
     smtStatisticsRegistry()->registerStat(&d_numTermsLowered);
-    smtStatisticsRegistry()->registerStat(&d_numTermsForcedLowered);
+    smtStatisticsRegistry()->registerStat(&d_numIntroducedItes);
   }
 }
 
@@ -276,7 +413,7 @@ BoolToBV::Statistics::~Statistics()
   if (options::boolToBitvector() == options::BoolToBVMode::ALL)
   {
     smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered);
-    smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered);
+    smtStatisticsRegistry()->unregisterStat(&d_numIntroducedItes);
   }
 }
 
diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h
index 11cb551fa..6e6d368eb 100644
--- a/src/preprocessing/passes/bool_to_bv.h
+++ b/src/preprocessing/passes/bool_to_bv.h
@@ -18,6 +18,7 @@
 #ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
 #define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
 
+#include "options/bv_options.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "theory/bv/theory_bv_utils.h"
@@ -41,29 +42,82 @@ class BoolToBV : public PreprocessingPass
   {
     IntStat d_numIteToBvite;
     IntStat d_numTermsLowered;
-    IntStat d_numTermsForcedLowered;
+    IntStat d_numIntroducedItes;
     Statistics();
     ~Statistics();
   };
 
-  /* Takes an assertion and tries to create more bit-vector structure */
-  Node lowerAssertion(const TNode& a);
+  /** Takes an assertion and attempts to create more bit-vector structure
+      by replacing boolean operators with bit-vector operators.
 
-  /* Tries to lower one node to a width-one bit-vector */
-  void lowerNode(const TNode& n);
+      It passes the allowIteIntroduction argument down to lowerNode, however it
+      never allows ite introduction in the top-level assertion. There's no point
+      forcing the assertion to be a bit-vector when it will just be converted
+      back into a boolean.
+  */
+  Node lowerAssertion(const TNode& node, bool allowIteIntroduction = false);
+
+  /** Traverses subterms to turn booleans into bit-vectors using visit
+   *  Passes the allowIteIntroduction argument to visit
+   *  Returns the lowered node
+   */
+  Node lowerNode(const TNode& node, bool allowIteIntroduction = false);
+
+  /** Tries to lower one node to a width-one bit-vector
+   *  Caches the result if successful
+   *
+   *  allowIteIntroduction = true causes booleans to be converted to bit-vectors
+   *     using an ITE this is only used by mode ALL currently, but could
+   *     conceivably be used in new modes.
+   */
+  void visit(const TNode& n, bool allowIteIntroduction = false);
+
+  /* Traverses formula looking for ITEs to lower to BITVECTOR_ITE using
+   * lowerNode*/
+  Node lowerIte(const TNode& node);
+
+  /** Rebuilds node using the provided kind
+   *  Note: The provided kind is not necessarily different from the
+   *        existing one, but still might need to be rebuilt because
+   *        of subterms
+   */
+  void rebuildNode(const TNode& n, Kind new_kind);
+
+  /** Updates the cache, the cache is actually supported by two maps
+      one for ITEs and one for everything else
+
+      This is necessary so that when in ITE mode, the regular cache
+      can be cleared to prevent lowering boolean operators that are
+      not in an ITE
+   */
+  void updateCache(TNode n, TNode rebuilt);
 
   /* Returns cached node if it exists, otherwise returns the node */
   Node fromCache(TNode n) const;
 
-  /** Checks if any of the nodes children were rebuilt,
+  /* Checks both caches for membership */
+  bool inCache(const Node& n) const;
+
+  /** Checks if any of the node's children were rebuilt,
    *  in which case n needs to be rebuilt as well
    */
   bool needToRebuild(TNode n) const;
 
   Statistics d_statistics;
 
-  /* Keeps track of lowered nodes */
+  /** Keeps track of lowered ITEs
+      Note: it only keeps mappings for ITEs of type bit-vector.
+      Other ITEs will be in the d_lowerCache
+   */
+  std::unordered_map<Node, Node, NodeHashFunction> d_iteBVLowerCache;
+
+  /** Keeps track of other lowered nodes
+      -- will be cleared periodically in ITE mode
+  */
   std::unordered_map<Node, Node, NodeHashFunction> d_lowerCache;
+
+  /** Stores the bool-to-bv mode option */
+  options::BoolToBVMode d_boolToBVMode;
 };  // class BoolToBV
 
 }  // namespace passes