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.

6 files changed, 0 insertions, 80 deletions

diff --git a/src/options/boolean_term_conversion_mode.cpp b/src/options/boolean_term_conversion_mode.cpp
index 0673718bb..4fc9b1f8d 100644
--- a/src/options/boolean_term_conversion_mode.cpp
+++ b/src/options/boolean_term_conversion_mode.cpp
@@ -20,22 +20,5 @@
 
 namespace CVC4 {
 
-std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) {
-  switch(mode) {
-  case theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
-    out << "BOOLEAN_TERM_CONVERT_TO_BITVECTORS";
-    break;
-  case theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
-    out << "BOOLEAN_TERM_CONVERT_TO_DATATYPES";
-    break;
-  case theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE:
-    out << "BOOLEAN_TERM_CONVERT_NATIVE";
-    break;
-  default:
-    out << "BooleanTermConversionMode!UNKNOWN";
-  }
-
-  return out;
-}
 
 }/* CVC4 namespace */
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 */
diff --git a/src/options/booleans_options b/src/options/booleans_options
index a150c1d83..6143f4f67 100644
--- a/src/options/booleans_options
+++ b/src/options/booleans_options
@@ -5,7 +5,5 @@
 
 module BOOLEANS "options/booleans_options.h" Boolean theory
 
-option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "options/boolean_term_conversion_mode.h" :handler stringToBooleanTermConversionMode
- policy for converting Boolean terms
 
 endmodule
diff --git a/src/options/expr_options b/src/options/expr_options
index 75354a010..d6997b2dd 100644
--- a/src/options/expr_options
+++ b/src/options/expr_options
@@ -26,8 +26,5 @@ option earlyTypeChecking --eager-type-checking/--lazy-type-checking bool :defaul
 option typeChecking type-checking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking
  never type check expressions
 
-option biasedITERemoval --biased-ites bool :default false
- try the new remove ite pass that is biased against term ites appearing
-
 endmodule
 
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 0dac42362..c0aa67cd4 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1061,41 +1061,6 @@ void OptionsHandler::setBitblastAig(std::string option, bool arg) throw(OptionEx
   }
 }
 
-
-// theory/booleans/options_handlers.h
-const std::string OptionsHandler::s_booleanTermConversionModeHelp = "\
-Boolean term conversion modes currently supported by the\n\
---boolean-term-conversion-mode option:\n\
-\n\
-bitvectors [default]\n\
-+ Boolean terms are converted to bitvectors of size 1.\n\
-\n\
-datatypes\n\
-+ Boolean terms are converted to enumerations in the Datatype theory.\n\
-\n\
-native\n\
-+ Boolean terms are converted in a \"natural\" way depending on where they\n\
-  are used.  If in a datatype context, they are converted to an enumeration.\n\
-  Elsewhere, they are converted to a bitvector of size 1.\n\
-";
-
-theory::booleans::BooleanTermConversionMode OptionsHandler::stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException){
-  if(optarg ==  "bitvectors") {
-    return theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS;
-  } else if(optarg ==  "datatypes") {
-    return theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES;
-  } else if(optarg ==  "native") {
-    return theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE;
-  } else if(optarg ==  "help") {
-    puts(s_booleanTermConversionModeHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") +
-                          optarg + "'.  Try --boolean-term-conversion-mode help.");
-  }
-}
-
-
 // theory/uf/options_handlers.h
 const std::string OptionsHandler::s_ufssModeHelp = "\
 UF strong solver options currently supported by the --uf-ss option:\n\
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 45aea7b79..248f15c98 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -118,10 +118,6 @@ public:
 
   theory::bv::SatSolverMode stringToSatSolver(std::string option, std::string optarg) throw(OptionException);
     
-
-  // theory/booleans/options_handlers.h
-  theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException);
-
   // theory/uf/options_handlers.h
   theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg) throw(OptionException);