* Clean up some options documentation

* Remove defunct --no-theory-registration option
* Point people to Wiki tutorial
* Modernize the cut-release script
* Misc cleanup, documentation

(this commit was certified error- and warning-free by the test-and-commit script.)

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) {