BoolToBV modes (off, ite, all) (#2530)

diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index c711567ab13c4f7922c4116e72e3b5fca653e60d..b86db8d00dc626421dc4b6fdab614c4394c5f5ca 100644 (file)
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -9,6 +9,8 @@ libcvc4_add_sources(
   arith_unate_lemma_mode.cpp
   arith_unate_lemma_mode.h
   base_handlers.h
+  bool_to_bv_mode.cpp
+  bool_to_bv_mode.h
   bv_bitblast_mode.cpp
   bv_bitblast_mode.h
   datatypes_modes.h

diff --git a/src/options/bool_to_bv_mode.cpp b/src/options/bool_to_bv_mode.cpp
new file mode 100644 (file)
index 0000000..670e154
--- /dev/null
+++ b/src/options/bool_to_bv_mode.cpp
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file bool_to_bv_mode.cpp
+** \verbatim
+** Top contributors (to current version):
+**   Makai Mann
+** This file is part of the CVC4 project.
+** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+** in the top-level source directory) and their institutional affiliations.
+** All rights reserved.  See the file COPYING in the top-level source
+** directory for licensing information.\endverbatim
+**
+** \brief Modes for bool-to-bv preprocessing pass
+**
+** Modes for bool-to-bv preprocessing pass which tries to lower booleans
+**       to bit-vectors of width 1 at various levels of aggressiveness.
+**/
+
+#include "options/bool_to_bv_mode.h"
+
+#include <iostream>
+
+
+namespace CVC4
+{
+  std::ostream& operator<<(std::ostream& out, preprocessing::passes::BoolToBVMode mode) {
+    switch(mode) {
+    case preprocessing::passes::BOOL_TO_BV_OFF:
+      out << "BOOL_TO_BV_OFF";
+      break;
+    case preprocessing::passes::BOOL_TO_BV_ITE:
+      out << "BOOL_TO_BV_ITE";
+      break;
+    case preprocessing::passes::BOOL_TO_BV_ALL:
+      out << "BOOL_TO_BV_ALL";
+      break;
+    default:
+      out << "BoolToBVMode:UNKNOWN![" << unsigned(mode) << "]";
+    }
+
+    return out;
+  }
+} // namespace CVC4

diff --git a/src/options/bool_to_bv_mode.h b/src/options/bool_to_bv_mode.h
new file mode 100644 (file)
index 0000000..f2911c3
--- /dev/null
+++ b/src/options/bool_to_bv_mode.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file bool_to_bv_mode.h
+** \verbatim
+** Top contributors (to current version):
+**   Makai Mann
+** This file is part of the CVC4 project.
+** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+** in the top-level source directory) and their institutional affiliations.
+** All rights reserved.  See the file COPYING in the top-level source
+** directory for licensing information.\endverbatim
+**
+** \brief Modes for bool-to-bv preprocessing pass
+**
+** Modes for bool-to-bv preprocessing pass which tries to lower booleans
+**       to bit-vectors of width 1 at various levels of aggressiveness.
+**/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H
+#define __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H
+
+#include <iosfwd>
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+/** Enumeration of bool-to-bv modes */
+enum BoolToBVMode
+{
+  /**
+   * No bool-to-bv pass
+   */
+  BOOL_TO_BV_OFF,
+
+  /**
+   * Only lower bools in condition of ITEs
+   * Tries to give more info to bit-vector solver
+   * by using bit-vector-ITEs when possible
+   */
+  BOOL_TO_BV_ITE,
+
+  /**
+   * Lower every bool beneath the top layer to be a
+   * bit-vector
+   */
+  BOOL_TO_BV_ALL
+};
+}
+}
+
+std::ostream& operator<<(std::ostream& out, preprocessing::passes::BoolToBVMode mode);
+
+}
+
+#endif /* __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H */

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 15a9047c7f854abcf3b9c01aa18f8089fb085904..00290da7d5fe8e242d38946c8b360a122cac763d 100644 (file)
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -105,11 +105,22 @@ header = "options/bv_options.h"
 
 [[option]]
   name       = "boolToBitvector"
+  smt_name   = "bool-to-bv"
   category   = "regular"
-  long       = "bool-to-bv"
+  long       = "bool-to-bv=MODE"
+  type       = "CVC4::preprocessing::passes::BoolToBVMode"
+  default    = "CVC4::preprocessing::passes::BOOL_TO_BV_OFF"
+  handler    = "stringToBoolToBVMode"
+  includes   = ["options/bool_to_bv_mode.h"]
+  help       = "convert booleans to bit-vectors of size 1 at various levels of aggressiveness, see --bool-to-bv=help"
+
+[[option]]
+  name       = "bitwiseEq"
+  category   = "regular"
+  long       = "bitwise-eq"
   type       = "bool"
-  default    = "false"
-  help       = "convert booleans to bit-vectors of size 1 when possible"
+  default    = "true"
+  help       = "lift equivalence with one-bit bit-vectors to be boolean operations"
 
 [[option]]
   name       = "bitvectorDivByZeroConst"

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index a808ecd3cea7bb9bc030c91900a38b82f32df5a5..4203964520bb695a061af694ed11cb984da58df0 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1301,6 +1301,50 @@ theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode(
   }
 }
 
+const std::string OptionsHandler::s_boolToBVModeHelp =
+    "\
+BoolToBV pass modes supported by the --bool-to-bv option:\n\
+\n\
+off (default)\n\
++ Don't push any booleans to width one bit-vectors\n\
+\n\
+ite\n\
++ Try to turn ITEs into BITVECTOR_ITE when possible. It can fail per-formula \n\
+  if not all sub-formulas can be turned to bit-vectors\n\
+\n\
+all\n\
++ Force all booleans to be bit-vectors of width one except at the top level.\n\
+  Most aggressive mode\n\
+";
+
+preprocessing::passes::BoolToBVMode OptionsHandler::stringToBoolToBVMode(
+    std::string option, std::string optarg)
+{
+  if (optarg == "off")
+  {
+    return preprocessing::passes::BOOL_TO_BV_OFF;
+  }
+  else if (optarg == "ite")
+  {
+    return preprocessing::passes::BOOL_TO_BV_ITE;
+  }
+  else if (optarg == "all")
+  {
+    return preprocessing::passes::BOOL_TO_BV_ALL;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_boolToBVModeHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(std::string("unknown option for --bool-to-bv: `")
+                          + optarg
+                          + "'. Try --bool-to-bv=help");
+  }
+}
+
 void OptionsHandler::setBitblastAig(std::string option, bool arg)
 {
   if(arg) {

diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 53e31789587918c09bdc1db0916d0806733fe65b..f9663269671e0f2bb5e3cf8c380070de1dc0b6eb 100644 (file)
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -27,6 +27,7 @@
 #include "options/arith_propagation_mode.h"
 #include "options/arith_unate_lemma_mode.h"
 #include "options/base_handlers.h"
+#include "options/bool_to_bv_mode.h"
 #include "options/bv_bitblast_mode.h"
 #include "options/datatypes_modes.h"
 #include "options/decision_mode.h"
@@ -137,6 +138,8 @@ public:
                                                 std::string optarg);
   theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option,
                                                 std::string optarg);
+  preprocessing::passes::BoolToBVMode stringToBoolToBVMode(std::string option,
+                                                           std::string optarg);
   void setBitblastAig(std::string option, bool arg);
 
   theory::bv::SatSolverMode stringToSatSolver(std::string option,
@@ -229,6 +232,7 @@ public:
   static const std::string s_bvSatSolverHelp;
   static const std::string s_booleanTermConversionModeHelp;
   static const std::string s_bvSlicerModeHelp;
+  static const std::string s_boolToBVModeHelp;
   static const std::string s_cegqiFairModeHelp;
   static const std::string s_decisionModeHelp;
   static const std::string s_instFormatHelp ;

diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index c8a59bdc453a59bca8bb18f36c5246ff66a8c977..252ab941c909bd7581116b16634bd975a85d698e 100644 (file)
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -9,17 +9,17 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief The BoolToBv preprocessing pass
+ ** \brief The BoolToBV preprocessing pass
  **
  **/
 
 #include "preprocessing/passes/bool_to_bv.h"
 
 #include <string>
-#include <unordered_map>
-#include <vector>
 
+#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,183 +30,253 @@ namespace passes {
 using namespace CVC4::theory;
 
 BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext)
-    : PreprocessingPass(preprocContext, "bool-to-bv"),
-      d_lowerCache(),
-      d_one(bv::utils::mkOne(1)),
-      d_zero(bv::utils::mkZero(1)),
-      d_statistics(){};
+    : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics(){};
 
 PreprocessingPassResult BoolToBV::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
   NodeManager::currentResourceManager()->spendResource(
       options::preprocessStep());
-  std::vector<Node> new_assertions;
-  lowerBoolToBv(assertionsToPreprocess->ref(), new_assertions);
-  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
+
+  unsigned size = assertionsToPreprocess->size();
+  for (unsigned i = 0; i < size; ++i)
   {
-    assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i]));
+    assertionsToPreprocess->replace(
+        i, Rewriter::rewrite(lowerAssertion((*assertionsToPreprocess)[i])));
   }
-  return PreprocessingPassResult::NO_CONFLICT;
-}
 
-void BoolToBV::addToLowerCache(TNode term, Node new_term)
-{
-  Assert(new_term != Node());
-  Assert(!hasLowerCache(term));
-  d_lowerCache[term] = new_term;
+  return PreprocessingPassResult::NO_CONFLICT;
 }
 
-Node BoolToBV::getLowerCache(TNode term) const
+Node BoolToBV::fromCache(TNode n) const
 {
-  Assert(hasLowerCache(term));
-  return d_lowerCache.find(term)->second;
+  if (d_lowerCache.find(n) != d_lowerCache.end())
+  {
+    return d_lowerCache.find(n)->second;
+  }
+  return n;
 }
 
-bool BoolToBV::hasLowerCache(TNode term) const
+bool BoolToBV::needToRebuild(TNode n) const
 {
-  return d_lowerCache.find(term) != d_lowerCache.end();
+  // check if any children were rebuilt
+  for (const Node& nn : n)
+  {
+    if (ContainsKey(d_lowerCache, nn))
+    {
+      return true;
+    }
+  }
+  return false;
 }
 
-Node BoolToBV::lowerNode(TNode current, bool topLevel)
+Node BoolToBV::lowerAssertion(const TNode& a)
 {
-  Node result;
+  bool optionITE = options::boolToBitvector() == BOOL_TO_BV_ITE;
   NodeManager* nm = NodeManager::currentNM();
-  if (hasLowerCache(current))
-  {
-    result = getLowerCache(current);
-  }
-  else
+  std::vector<TNode> visit;
+  visit.push_back(a);
+  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())
   {
-    if (current.getNumChildren() == 0)
+    TNode n = visit.back();
+    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)
+                        << 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 (current.getKind() == kind::CONST_BOOLEAN)
+      visited.insert(n);
+      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)
       {
-        result = (current == bv::utils::mkTrue()) ? d_one : d_zero;
+        visit.push_back(n[i]);
       }
-      else
+
+      if (optionITE)
       {
-        result = current;
+        // 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());
+        }
       }
     }
+    /* 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
     {
-      Kind kind = current.getKind();
-      Kind new_kind = kind;
-      switch (kind)
-      {
-        case kind::EQUAL:
-          if (current[0].getType().isBitVector()
-              || current[0].getType().isBoolean())
-          {
-            new_kind = kind::BITVECTOR_COMP;
-          }
-          break;
-        case kind::AND: new_kind = kind::BITVECTOR_AND; break;
-        case kind::OR: new_kind = kind::BITVECTOR_OR; break;
-        case kind::NOT: new_kind = kind::BITVECTOR_NOT; break;
-        case kind::XOR: new_kind = kind::BITVECTOR_XOR; break;
-        case kind::IMPLIES: new_kind = kind::BITVECTOR_OR; break;
-        case kind::ITE:
-          if (current.getType().isBitVector() || current.getType().isBoolean())
-          {
-            new_kind = kind::BITVECTOR_ITE;
-          }
-          break;
-        case kind::BITVECTOR_ULT: new_kind = kind::BITVECTOR_ULTBV; break;
-        case kind::BITVECTOR_SLT: new_kind = kind::BITVECTOR_SLTBV; break;
-        case kind::BITVECTOR_ULE:
-        case kind::BITVECTOR_UGT:
-        case kind::BITVECTOR_UGE:
-        case kind::BITVECTOR_SLE:
-        case kind::BITVECTOR_SGT:
-        case kind::BITVECTOR_SGE:
-          // Should have been removed by rewriting.
-          Unreachable();
-        default: break;
-      }
-      NodeBuilder<> builder(new_kind);
-      if (kind != new_kind)
-      {
-        ++(d_statistics.d_numTermsLowered);
-      }
-      if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
-      {
-        builder << current.getOperator();
-      }
-      Node converted;
-      if (new_kind == kind::ITE)
+      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;
+  }
+}
+
+void BoolToBV::lowerNode(const TNode& n)
+{
+  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)
+  {
+    all_bv = all_bv && fromCache(nn).getType().isBitVector();
+    if (!all_bv)
+    {
+      break;
+    }
+  }
+
+  if (!all_bv || (n.getNumChildren() == 0))
+  {
+    if ((options::boolToBitvector() == BOOL_TO_BV_ALL)
+        && n.getType().isBoolean())
+    {
+      if (k == kind::CONST_BOOLEAN)
       {
-        // Special-case ITE because need condition to be Boolean.
-        converted = lowerNode(current[0], true);
-        builder << converted;
-        converted = lowerNode(current[1]);
-        builder << converted;
-        converted = lowerNode(current[2]);
-        builder << converted;
-      }
-      else if (kind == kind::IMPLIES) {
-        // Special-case IMPLIES because needs to be rewritten.
-        converted = lowerNode(current[0]);
-        builder << nm->mkNode(kind::BITVECTOR_NOT, converted);
-        converted = lowerNode(current[1]);
-        builder << converted;
+        d_lowerCache[n] = (n == bv::utils::mkTrue()) ? bv::utils::mkOne(1)
+                                                     : bv::utils::mkZero(1);
       }
       else
       {
-        for (unsigned i = 0; i < current.getNumChildren(); ++i)
-        {
-          converted = lowerNode(current[i]);
-          builder << converted;
-        }
+        d_lowerCache[n] =
+            nm->mkNode(kind::ITE, n, bv::utils::mkOne(1), bv::utils::mkZero(1));
       }
-      result = builder;
+
+      Debug("bool-to-bv") << "BoolToBV::lowerNode " << n << " =>\n"
+                          << fromCache(n) << std::endl;
+      ++(d_statistics.d_numTermsForcedLowered);
+      return;
     }
-    if (result.getType().isBoolean())
+    else
     {
-      ++(d_statistics.d_numTermsForcedLowered);
-      result = nm->mkNode(kind::ITE, result, d_one, d_zero);
+      // 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;
     }
-    addToLowerCache(current, result);
   }
-  if (topLevel)
+
+  Kind new_kind = k;
+  switch (k)
   {
-    result = nm->mkNode(kind::EQUAL, result, d_one);
+    case kind::EQUAL: new_kind = kind::BITVECTOR_COMP; break;
+    case kind::AND: new_kind = kind::BITVECTOR_AND; break;
+    case kind::OR: new_kind = kind::BITVECTOR_OR; break;
+    case kind::NOT: new_kind = kind::BITVECTOR_NOT; break;
+    case kind::XOR: new_kind = kind::BITVECTOR_XOR; break;
+    case kind::IMPLIES: new_kind = kind::BITVECTOR_OR; break;
+    case kind::ITE: new_kind = kind::BITVECTOR_ITE; break;
+    case kind::BITVECTOR_ULT: new_kind = kind::BITVECTOR_ULTBV; break;
+    case kind::BITVECTOR_SLT: new_kind = kind::BITVECTOR_SLTBV; break;
+    case kind::BITVECTOR_ULE:
+    case kind::BITVECTOR_UGT:
+    case kind::BITVECTOR_UGE:
+    case kind::BITVECTOR_SLE:
+    case kind::BITVECTOR_SGT:
+    case kind::BITVECTOR_SGE:
+      // Should have been removed by rewriting.
+      Unreachable();
+    default: break;
   }
-  Assert(result != Node());
-  Debug("bool-to-bv") << "BoolToBV::lowerNode " << current << " => \n"
-                      << result << "\n";
-  return result;
-}
 
-void BoolToBV::lowerBoolToBv(const std::vector<Node>& assertions,
-                             std::vector<Node>& new_assertions)
-{
-  for (unsigned i = 0; i < assertions.size(); ++i)
+  NodeBuilder<> builder(new_kind);
+  if ((options::boolToBitvector() == BOOL_TO_BV_ALL) && (new_kind != k))
+  {
+    ++(d_statistics.d_numTermsLowered);
+  }
+
+  if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
+  {
+    builder << n.getOperator();
+  }
+
+  // special case IMPLIES because needs to be rewritten
+  if (k == kind::IMPLIES)
+  {
+    builder << nm->mkNode(kind::BITVECTOR_NOT, fromCache(n[0]));
+    builder << fromCache(n[1]);
+  }
+  else
   {
-    Node new_assertion = lowerNode(assertions[i], true);
-    new_assertions.push_back(new_assertion);
-    Trace("bool-to-bv") << "  " << assertions[i] << " => " << new_assertions[i]
-                        << "\n";
+    for (const Node& nn : n)
+    {
+      builder << fromCache(nn);
+    }
   }
+
+  Debug("bool-to-bv") << "BoolToBV::lowerNode " << n << " =>\n"
+                      << builder << std::endl;
+
+  d_lowerCache[n] = builder.constructNode();
 }
 
 BoolToBV::Statistics::Statistics()
-    : d_numTermsLowered("preprocessing::passes::BoolToBV::NumTermsLowered", 0),
-      d_numAtomsLowered("preprocessing::passes::BoolToBV::NumAtomsLowered", 0),
+    : d_numIteToBvite("preprocessing::passes::BoolToBV::NumIteToBvite", 0),
+      d_numTermsLowered("preprocessing::passes:BoolToBV::NumTermsLowered", 0),
       d_numTermsForcedLowered(
           "preprocessing::passes::BoolToBV::NumTermsForcedLowered", 0)
 {
-  smtStatisticsRegistry()->registerStat(&d_numTermsLowered);
-  smtStatisticsRegistry()->registerStat(&d_numAtomsLowered);
-  smtStatisticsRegistry()->registerStat(&d_numTermsForcedLowered);
+  smtStatisticsRegistry()->registerStat(&d_numIteToBvite);
+  if (options::boolToBitvector() == BOOL_TO_BV_ALL)
+  {
+    // these statistics wouldn't be correct in the ITE mode,
+    // 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);
+  }
 }
 
 BoolToBV::Statistics::~Statistics()
 {
-  smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered);
-  smtStatisticsRegistry()->unregisterStat(&d_numAtomsLowered);
-  smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered);
+  smtStatisticsRegistry()->unregisterStat(&d_numIteToBvite);
+  if (options::boolToBitvector() == BOOL_TO_BV_ALL)
+  {
+    smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered);
+    smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered);
+  }
 }
 
 

diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h
index 49c9dc944f593864ea2b7192f80cc5306fdb2bb5..da99d3c84ce64ccf11409cc0860c96b5f37b4c9b 100644 (file)
--- a/src/preprocessing/passes/bool_to_bv.h
+++ b/src/preprocessing/passes/bool_to_bv.h
@@ -2,14 +2,14 @@
 /*! \file bool_to_bv.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Yoni Zohar
+ **   Makai Mann, Yoni Zohar
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief The BoolToBv preprocessing pass
+ ** \brief The BoolToBV preprocessing pass
  **
  **/
 
@@ -18,9 +18,9 @@
 #ifndef __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
 #define __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
 
-#include "preprocessing/passes/bv_to_bool.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
+#include "theory/bv/theory_bv_utils.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -39,24 +39,33 @@ class BoolToBV : public PreprocessingPass
  private:
   struct Statistics
   {
+    IntStat d_numIteToBvite;
     IntStat d_numTermsLowered;
-    IntStat d_numAtomsLowered;
     IntStat d_numTermsForcedLowered;
     Statistics();
     ~Statistics();
   };
 
-  void lowerBoolToBv(const std::vector<Node>& assertions,
-                     std::vector<Node>& new_assertions);
-  void addToLowerCache(TNode term, Node new_term);
-  Node getLowerCache(TNode term) const;
-  bool hasLowerCache(TNode term) const;
-  Node lowerNode(TNode current, bool topLevel = false);
-  NodeNodeMap d_lowerCache;
-  Node d_one;
-  Node d_zero;
+  /* Takes an assertion and tries to create more bit-vector structure */
+  Node lowerAssertion(const TNode& a);
+
+  /* Tries to lower one node to a width-one bit-vector */
+  void lowerNode(const TNode& n);
+
+  /* Returns cached node if it exists, otherwise returns the node */
+  Node fromCache(TNode n) const;
+
+  /** Checks if any of the nodes children were rebuilt,
+   *  in which case n needs to be rebuilt as well
+   */
+  bool needToRebuild(TNode n) const;
+
   Statistics d_statistics;
-};  // class
+
+  /* Keeps track of lowered nodes */
+  std::unordered_map<Node, Node, NodeHashFunction> d_lowerCache;
+};  // class BoolToBV
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6814ad5310bc4c2685236774510365a696294cf9..7abfd82733efdc934a9ec7ee55e99c3ab5c7a0b4 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1379,17 +1379,17 @@ void SmtEngine::setDefaults() {
       options::bitvectorToBool.set(false);
     }
 
-    if (options::boolToBitvector())
+    if (options::boolToBitvector() != preprocessing::passes::BOOL_TO_BV_OFF)
     {
       if (options::boolToBitvector.wasSetByUser())
       {
         throw OptionException(
-            "bool-to-bv not supported with unsat cores/proofs");
+            "bool-to-bv != off not supported with unsat cores/proofs");
       }
-      Notice() << "SmtEngine: turning off bool-to-bitvector to support unsat "
+      Notice() << "SmtEngine: turning off bool-to-bv to support unsat "
                   "cores/proofs"
                << endl;
-      options::boolToBitvector.set(false);
+      setOption("boolToBitvector", SExpr("off"));
     }
 
     if (options::bvIntroducePow2())
@@ -1449,13 +1449,18 @@ void SmtEngine::setDefaults() {
 
   if (options::cbqiBv() && d_logic.isQuantified())
   {
-    if(options::boolToBitvector.wasSetByUser()) {
-      throw OptionException(
-          "bool-to-bv not supported with CBQI BV for quantified logics");
+    if (options::boolToBitvector() != preprocessing::passes::BOOL_TO_BV_OFF)
+    {
+      if (options::boolToBitvector.wasSetByUser())
+      {
+        throw OptionException(
+            "bool-to-bv != off not supported with CBQI BV for quantified "
+            "logics");
+      }
+      Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
+               << endl;
+      setOption("boolToBitvector", SExpr("off"));
     }
-    Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
-             << endl;
-    options::boolToBitvector.set(false);
   }
 
   // cases where we need produce models
@@ -1617,6 +1622,19 @@ void SmtEngine::setDefaults() {
     }
   }
 
+  if (options::boolToBitvector() == preprocessing::passes::BOOL_TO_BV_ALL
+      && !d_logic.isTheoryEnabled(THEORY_BV))
+  {
+    if (options::boolToBitvector.wasSetByUser())
+    {
+      throw OptionException(
+          "bool-to-bv=all not supported for non-bitvector logics.");
+    }
+    Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: "
+             << d_logic.getLogicString() << std::endl;
+    setOption("boolToBitvector", SExpr("off"));
+  }
+
   if (! options::bvEagerExplanations.wasSetByUser() &&
       d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
       d_logic.isTheoryEnabled(THEORY_BV)) {

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index e60d604569f135c8dda64aa93117e336cdbe5698..949a3d7381accb61f36570d0810f9cb66b2926fc 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -740,7 +740,7 @@ Node TheoryBV::ppRewrite(TNode t)
 {
   Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n";
   Node res = t;
-  if (RewriteRule<BitwiseEq>::applies(t)) {
+  if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t)) {
     Node result = RewriteRule<BitwiseEq>::run<false>(t);
     res = Rewriter::rewrite(result);
   } else if (d_isCoreTheory && t.getKind() == kind::EQUAL) {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f22796929256b1b46550ca161110612a76e546da..9e942aae1f6685f60c83287bf728b8907aa2e4d3 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -159,7 +159,8 @@ set(regress_0_tests
   regress0/bv/ackermann2.smt2
   regress0/bv/ackermann3.smt2
   regress0/bv/ackermann4.smt2
-  regress0/bv/bool-to-bv.smt2
+  regress0/bv/bool-to-bv-all.smt2
+  regress0/bv/bool-to-bv-ite.smt2
   regress0/bv/bug260a.smt
   regress0/bv/bug260b.smt
   regress0/bv/bug440.smt

diff --git a/test/regress/regress0/bv/bool-to-bv-all.smt2 b/test/regress/regress0/bv/bool-to-bv-all.smt2
new file mode 100644 (file)
index 0000000..5947699
--- /dev/null
+++ b/test/regress/regress0/bv/bool-to-bv-all.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --bool-to-bv=all
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun x2 () (_ BitVec 3))
+(declare-fun x1 () (_ BitVec 3))
+(declare-fun x0 () (_ BitVec 3))
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
+(declare-fun b3 () Bool)
+(assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1)))
+(assert (not (bvslt (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1)))
+(assert (= #b000 x2))
+(assert (=> b1 b2))
+(assert (and b1 b2))
+(assert (or b1 b2))
+(assert (xor b1 b3))
+(assert (not (xor b2 b2)))
+(assert (ite b2 b2 b1))
+(check-sat)

diff --git a/test/regress/regress0/bv/bool-to-bv-ite.smt2 b/test/regress/regress0/bv/bool-to-bv-ite.smt2
new file mode 100644 (file)
index 0000000..e1be3ea
--- /dev/null
+++ b/test/regress/regress0/bv/bool-to-bv-ite.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --bool-to-bv=ite
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun x2 () (_ BitVec 3))
+(declare-fun x1 () (_ BitVec 3))
+(declare-fun x0 () (_ BitVec 3))
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
+(assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1)))
+(assert (= #b000 x2))
+(assert (=> b1 b2))
+(assert (= x2 (ite (bvugt x0 x1) (bvadd x0 (_ bv1 3)) (bvadd x1 (_ bv1 3)))))
+(check-sat)

diff --git a/test/regress/regress0/bv/bool-to-bv.smt2 b/test/regress/regress0/bv/bool-to-bv.smt2
deleted file mode 100644 (file)
index 8706c51..0000000
--- a/test/regress/regress0/bv/bool-to-bv.smt2
+++ /dev/null
@@ -1,19 +0,0 @@
-; COMMAND-LINE: --bool-to-bv
-; EXPECT: sat
-(set-logic QF_BV)
-(declare-fun x2 () (_ BitVec 3))
-(declare-fun x1 () (_ BitVec 3))
-(declare-fun x0 () (_ BitVec 3))
-(declare-fun b1 () Bool)
-(declare-fun b2 () Bool)
-(declare-fun b3 () Bool)
-(assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1)))
-(assert (not (bvslt (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1)))
-(assert (= #b000 x2))
-(assert (=> b1 b2))
-(assert (and b1 b2))
-(assert (or b1 b2))
-(assert (xor b1 b3))
-(assert (not (xor b2 b2)))
-(assert (ite b2 b2 b1))
-(check-sat)