diff options
Diffstat (limited to 'src/smt/options_handlers.h')
| -rw-r--r-- | src/smt/options_handlers.h | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index 2af826d24..43d53ee4c 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -154,16 +154,6 @@ none\n\ + do not perform nonclausal simplification\n\ "; -static const std::string modelFormatHelp = "\ -Model format modes currently supported by the --model-format option:\n\ -\n\ -default \n\ -+ Print model as expressions in the output language format.\n\ -\n\ -table\n\ -+ Print functional expressions over finite domains in a table format.\n\ -"; - inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) { #ifdef CVC4_DUMPING char* optargPtr = strdup(optarg.c_str()); @@ -271,20 +261,6 @@ inline SimplificationMode stringToSimplificationMode(std::string option, std::st } } -inline ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default") { - return MODEL_FORMAT_MODE_DEFAULT; - } else if(optarg == "table") { - return MODEL_FORMAT_MODE_TABLE; - } else if(optarg == "help") { - puts(modelFormatHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --model-format: `") + - optarg + "'. Try --model-format help."); - } -} - // ensure we haven't started search yet inline void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(ModalException) { if(smt != NULL && smt->d_fullyInited) { |