diff options
author | makaimann <makaim@stanford.edu> | 2018-12-10 08:37:11 -0800 |
---|---|---|
committer | Mathias Preiner <mathias.preiner@gmail.com> | 2018-12-10 08:37:11 -0800 |
commit | e1dc39321cd4ab29b436025badfb05714f5649b3 (patch) | |
tree | c2f02cd7370157fbea51ec6602ad174b149cd850 /src/options/options_handler.cpp | |
parent | 7270b2a800c45fa87ef4cdcad8fc353ccb8cd471 (diff) |
BoolToBV modes (off, ite, all) (#2530)
Diffstat (limited to 'src/options/options_handler.cpp')
-rw-r--r-- | src/options/options_handler.cpp | 44 |
1 files changed, 44 insertions, 0 deletions
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) { |