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

6 files changed, 163 insertions, 3 deletions

diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index c711567ab..b86db8d00 100644
--- 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
index 000000000..670e15419
--- /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
index 000000000..f2911c339
--- /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 15a9047c7..00290da7d 100644
--- 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 a808ecd3c..420396452 100644
--- 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 53e317895..f96632696 100644
--- 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 ;