Remove undocumented/uncommon aliases (#4177)

This commit removes aliases that are either undocumented or associated
with uncommon options.

Note: The removal of --statistics, --language, and --output-language may be controversial. The options were undocumented previously and I am in favor of simplifying the options as much as possible, however. Please let me know what you think.

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 15ace0869dc64c4d847ba97be17c1fa7b84a7003..43060bc5493213702f9bea4bdafbdabaeba1ea67 100644 (file)
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -56,16 +56,6 @@ header = "options/base_options.h"
   category   = "undocumented"
   type       = "bool"
 
-[[alias]]
-  category   = "undocumented"
-  long       = "language=L"
-  links      = ["--lang=L"]
-
-[[alias]]
-  category   = "undocumented"
-  long       = "output-language=L"
-  links      = ["--output-lang=L"]
-
 [[option]]
   name       = "verbosity"
   smt_name   = "verbosity"
@@ -103,16 +93,6 @@ header = "options/base_options.h"
   read_only  = true
   help       = "give statistics on exit"
 
-[[alias]]
-  category   = "undocumented"
-  long       = "statistics"
-  links      = ["--stats"]
-
-[[alias]]
-  category   = "undocumented"
-  long       = "no-statistics"
-  links      = ["--no-stats"]
-
 [[option]]
   name       = "statsEveryQuery"
   category   = "regular"
@@ -123,16 +103,6 @@ header = "options/base_options.h"
   read_only  = true
   help       = "in incremental mode, print stats after every satisfiability or validity query"
 
-[[alias]]
-  category   = "undocumented"
-  long       = "statistics-every-query"
-  links      = ["--stats-every-query"]
-
-[[alias]]
-  category   = "undocumented"
-  long       = "no-statistics-every-query"
-  links      = ["--no-stats-every-query"]
-
 [[option]]
   name       = "statsHideZeros"
   category   = "regular"
@@ -142,21 +112,6 @@ header = "options/base_options.h"
   read_only  = true
   help       = "hide statistics which are zero"
 
-[[alias]]
-  category   = "undocumented"
-  long       = "stats-show-zeros"
-  links      = ["--no-stats-hide-zeros"]
-
-[[alias]]
-  category   = "undocumented"
-  long       = "hide-zero-stats"
-  links      = ["--stats-hide-zeros"]
-
-[[alias]]
-  category   = "undocumented"
-  long       = "show-zero-stats"
-  links      = ["--stats-show-zeros"]
-
 [[option]]
   name       = "parseOnly"
   category   = "regular"

diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml
index 3791da7141be41fb811aa4213f6dd573ab58f075..d70765d69ef0dcb91e1f4b8f6f015cf79c1653b4 100644 (file)
--- a/src/options/expr_options.toml
+++ b/src/options/expr_options.toml
@@ -13,11 +13,6 @@ header = "options/expr_options.h"
   read_only  = true
   help       = "print exprs to depth N (0 == default, -1 == no limit)"
 
-[[alias]]
-  category   = "undocumented"
-  long       = "expr-depth=N"
-  links      = ["--default-expr-depth=N"]
-
 [[option]]
   name       = "defaultDagThresh"
   smt_name   = "default-dag-thresh"
@@ -30,16 +25,6 @@ header = "options/expr_options.h"
   read_only  = true
   help       = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)"
 
-[[alias]]
-  category   = "undocumented"
-  long       = "dag-thresh=N"
-  links      = ["--default-dag-thresh=N"]
-
-[[alias]]
-  category   = "undocumented"
-  long       = "dag-threshold=N"
-  links      = ["--default-dag-thresh=N"]
-
 [[option]]
   name       = "printExprTypes"
   category   = "regular"
@@ -67,8 +52,3 @@ header = "options/expr_options.h"
   default    = "DO_SEMANTIC_CHECKS_BY_DEFAULT"
   read_only  = true
   help       = "never type check expressions"
-
-[[alias]]
-  category   = "undocumented"
-  long       = "no-type-checking"
-  links      = ["--no-eager-type-checking"]

diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index f373e9836451b5441ac42c2f4f1999fca9886746..ccbe1a95695bb4d6adba63d0e25f306b7981824d 100644 (file)
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -12,11 +12,6 @@ header = "options/main_options.h"
   alternate  = false
   help       = "identify this CVC4 binary"
 
-[[alias]]
-  category   = "undocumented"
-  long       = "license"
-  links      = ["--version"]
-
 [[option]]
   name       = "help"
   category   = "common"
@@ -103,11 +98,6 @@ header = "options/main_options.h"
   read_only  = true
   help       = "spin on segfault/other crash waiting for gdb"
 
-[[alias]]
-  category   = "undocumented"
-  long       = "segv-nospin"
-  links      = ["--no-segv-spin"]
-
 [[option]]
   name       = "tearDownIncremental"
   category   = "expert"

diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml
index 71074d4208f75c846bd5c0adf29d85b2334f3478..72c7b51a05d51dfaffa61037dadc4421d5d20c71 100644 (file)
--- a/src/options/parser_options.toml
+++ b/src/options/parser_options.toml
@@ -27,11 +27,6 @@ header = "options/parser_options.h"
   read_only  = true
   help       = "disable ALL semantic checks, including type checks"
 
-[[alias]]
-  category   = "undocumented"
-  long       = "no-checking"
-  links      = ["--no-type-checking"]
-
 [[option]]
   name       = "globalDeclarations"
   smt_name   = "global-declarations"
@@ -61,11 +56,6 @@ header = "options/parser_options.h"
   default    = "true"
   read_only  = true
 
-[[alias]]
-  category   = "undocumented"
-  long       = "no-include-file"
-  links      = ["--no-filesystem-access"]
-
 [[option]]
   name       = "forceLogicString"
   smt_name   = "force-logic"

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index c813e190019811083c5e9b59994ee0cf4172b465..a0e3014b0e13d7e34b2f44351cfe9f4f56f9db5f 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -46,12 +46,6 @@ header = "options/smt_options.h"
   name = "batch"
   help = "Save up all ASSERTions; run nonclausal simplification and clausal (MiniSat) propagation for all of them only after reaching a querying command (CHECKSAT or QUERY or predicate SUBTYPE declaration)."
 
-[[alias]]
-  category   = "regular"
-  long       = "no-simplification"
-  links      = ["--simplification=none"]
-  help       = "turn off all simplification (same as --simplification=none)"
-
 [[option]]
   name       = "doStaticLearning"
   category   = "regular"

diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index da9434d7953b3810176ef1f7a535dafe4f755c63..ce1a236556093658f6cb1b7923a7d6be46cd34ac 100644 (file)
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -57,7 +57,7 @@ private:
     {
       char* argv[2];
       argv[0] = strdup("");
-      argv[1] = strdup("--output-language=ast");
+      argv[1] = strdup("--output-lang=ast");
       Options::parseOptions(&opts, 2, argv);
       free(argv[0]);
       free(argv[1]);

diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index e4a0dbb367ffb11260421151d7cf507e902c278c..5aafaeaa2e073df9c02cd1931378b05cf222e4fa 100644 (file)
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -61,7 +61,7 @@ class NodeBlack : public CxxTest::TestSuite {
   {
     char* argv[2];
     argv[0] = strdup("");
-    argv[1] = strdup("--output-language=ast");
+    argv[1] = strdup("--output-lang=ast");
     Options::parseOptions(&opts, 2, argv);
     free(argv[0]);
     free(argv[1]);