diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
commit | 0b2f9943d55152e0958369083649dd71340864c9 (patch) | |
tree | cd040f1dd12816c6af37548597bd674cafb45271 /src/printer/options_handlers.h | |
parent | 8ebd49cb903ba19f9330820d02af08e226c9b791 (diff) |
More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.
Diffstat (limited to 'src/printer/options_handlers.h')
-rw-r--r-- | src/printer/options_handlers.h | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/src/printer/options_handlers.h b/src/printer/options_handlers.h index 97d0e64c9..2a89a8d38 100644 --- a/src/printer/options_handlers.h +++ b/src/printer/options_handlers.h @@ -19,7 +19,7 @@ #ifndef __CVC4__PRINTER__OPTIONS_HANDLERS_H #define __CVC4__PRINTER__OPTIONS_HANDLERS_H -#include "printer/model_format_mode.h" +#include "printer/modes.h" namespace CVC4 { namespace printer { @@ -34,6 +34,16 @@ table\n\ + Print functional expressions over finite domains in a table format.\n\ "; +static const std::string instFormatHelp = "\ +Inst format modes currently supported by the --model-format option:\n\ +\n\ +default \n\ ++ Print instantiations as a list in the output language format.\n\ +\n\ +szs\n\ ++ Print instantiations as SZS compliant proof.\n\ +"; + inline ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "default") { return MODEL_FORMAT_MODE_DEFAULT; @@ -48,6 +58,19 @@ inline ModelFormatMode stringToModelFormatMode(std::string option, std::string o } } +inline InstFormatMode stringToInstFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "default") { + return INST_FORMAT_MODE_DEFAULT; + } else if(optarg == "szs") { + return INST_FORMAT_MODE_SZS; + } else if(optarg == "help") { + puts(instFormatHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --inst-format: `") + + optarg + "'. Try --inst-format help."); + } +} }/* CVC4::printer namespace */ }/* CVC4 namespace */ |