From: Andres Noetzli Date: Thu, 2 Apr 2020 18:59:34 +0000 (-0700) Subject: Remove undocumented/uncommon aliases (#4177) X-Git-Tag: cvc5-1.0.0~3411 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e24e6f3620996ee9e5010d30fefc51247cc55fdc;p=cvc5.git 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 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" diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index da9434d79..ce1a23655 100644 --- 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 e4a0dbb36..5aafaeaa2 100644 --- 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]);