Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.

1 files changed, 0 insertions, 19 deletions

diff --git a/src/options/boolean_term_conversion_mode.h b/src/options/boolean_term_conversion_mode.h
index f2f4a51af..57e2ccaf4 100644
--- a/src/options/boolean_term_conversion_mode.h
+++ b/src/options/boolean_term_conversion_mode.h
@@ -26,28 +26,9 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-enum BooleanTermConversionMode {
-  /**
-   * Convert Boolean terms to bitvectors of size 1.
-   */
-  BOOLEAN_TERM_CONVERT_TO_BITVECTORS,
-  /**
-   * Convert Boolean terms to enumerations in the Datatypes theory.
-   */
-  BOOLEAN_TERM_CONVERT_TO_DATATYPES,
-  /**
-   * Convert Boolean terms to enumerations in the Datatypes theory IF
-   * used in a datatypes context, otherwise to a bitvector of size 1.
-   */
-  BOOLEAN_TERM_CONVERT_NATIVE
-
-};
-
 }/* CVC4::theory::booleans namespace */
 }/* CVC4::theory namespace */
 
-std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) CVC4_PUBLIC;
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */