diff options
Diffstat (limited to 'src/theory/quantifiers/options_handlers.h')
-rw-r--r-- | src/theory/quantifiers/options_handlers.h | 34 |
1 files changed, 0 insertions, 34 deletions
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index e5e484625..f27b98a3d 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -60,24 +60,6 @@ predicate\n\ Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\ \n\ "; - -static const std::string axiomInstModeHelp = "\ -Axiom instantiation modes currently supported by the --axiom-inst option:\n\ -\n\ -default \n\ -+ Treat axioms the same as usual quantifiers, i.e. use all available methods for\n\ - instantiating axioms.\n\ -\n\ -trust \n\ -+ Treat axioms only using heuristic instantiation. Return unknown if in the case\n\ - that no instantiations are produced.\n\ -\n\ -priority \n\ -+ Treat axioms only using heuristic instantiation. Resort to using all methods\n\ - in the case that no instantiations are produced.\n\ -\n\ -"; - static const std::string mbqiModeHelp = "\ Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ \n\ @@ -292,22 +274,6 @@ inline void checkLiteralMatchMode(std::string option, LiteralMatchMode mode, Smt } } -inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default") { - return AXIOM_INST_MODE_DEFAULT; - } else if(optarg == "trust") { - return AXIOM_INST_MODE_TRUST; - } else if(optarg == "priority") { - return AXIOM_INST_MODE_PRIORITY; - } else if(optarg == "help") { - puts(axiomInstModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --axiom-inst: `") + - optarg + "'. Try --axiom-inst help."); - } -} - inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "gen-ev") { return MBQI_GEN_EVAL; |