Add option --fmf-fun-rlv, remove deprecated option --axiom-inst.

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;