summaryrefslogtreecommitdiff
path: root/src/options/boolean_term_conversion_mode.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/boolean_term_conversion_mode.h')
-rw-r--r--src/options/boolean_term_conversion_mode.h19
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback