1 files changed, 57 insertions, 0 deletions
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 */