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.

5 files changed, 0 insertions, 91 deletions

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 15ace0869..43060bc54 100644
--- 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 3791da714..d70765d69 100644
--- 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 f373e9836..ccbe1a956 100644
--- 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 71074d420..72c7b51a0 100644
--- 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 c813e1900..a0e3014b0 100644
--- 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"