diff options
Diffstat (limited to 'src/options/options_handler.cpp')
-rw-r--r-- | src/options/options_handler.cpp | 47 |
1 files changed, 45 insertions, 2 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index be2d7883d..46663ce7c 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -42,8 +42,6 @@ #include "options/language.h" #include "options/option_exception.h" #include "options/printer_modes.h" -#include "options/quantifiers_modes.h" -#include "options/simplification_mode.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "options/theoryof_mode.h" @@ -1472,6 +1470,51 @@ SimplificationMode OptionsHandler::stringToSimplificationMode( } } +const std::string OptionsHandler::s_modelCoresHelp = + "\ +Model cores modes currently supported by the --simplification option:\n\ +\n\ +none (default) \n\ ++ do not compute model cores\n\ +\n\ +simple\n\ ++ only include a subset of variables whose values are sufficient to show the\n\ +input formula is satisfied by the given model\n\ +\n\ +non-implied\n\ ++ only include a subset of variables whose values, in addition to the values\n\ +of variables whose values are implied, are sufficient to show the input\n\ +formula is satisfied by the given model\n\ +\n\ +"; + +ModelCoresMode OptionsHandler::stringToModelCoresMode(std::string option, + std::string optarg) +{ + if (optarg == "none") + { + return MODEL_CORES_NONE; + } + else if (optarg == "simple") + { + return MODEL_CORES_SIMPLE; + } + else if (optarg == "non-implied") + { + return MODEL_CORES_NON_IMPLIED; + } + else if (optarg == "help") + { + puts(s_modelCoresHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --model-cores: `") + + optarg + "'. Try --model-cores help."); + } +} + const std::string OptionsHandler::s_sygusSolutionOutModeHelp = "\ Modes for finite model finding bound minimization, supported by --sygus-out:\n\ |