From: Gereon Kremer <gkremer@stanford.edu>
Date: Tue, 14 Dec 2021 21:14:48 +0000 (-0800)
Subject: Make some undocumented options regular/expert (#7805)
X-Git-Tag: cvc5-1.0.0~665
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9ef7cc3520344901a704bda018cd1783ebc18d06;p=cvc5.git

Make some undocumented options regular/expert (#7805)

We have some options that are currently "undocumented" for no good reason.
This PR makes them regular or expert options.
---

diff --git a/src/options/README.md b/src/options/README.md
index c3e018215..2f89f04ee 100644
--- a/src/options/README.md
+++ b/src/options/README.md
@@ -26,7 +26,7 @@ Specifying Options
 Options can be defined within a module file with the `[[option]]` tag, the
 required attributes for an option are:
 
-* `category` (string): one of `common`, `expert`, `regular`, or `undocumented`
+* `category` (string): one of `common`, `regular`, `expert`, or `undocumented`
 * `type` (string): the C++ type of the option value, see below for more details.
 
 Optional attributes are:
@@ -59,6 +59,16 @@ Optional attributes are:
   given)
 
 
+Option categories
+-----------------
+
+Every option has one of the following categories that influences where and how an option is visible:
+
+* `common`: Used for the most common options. All `common` options are shown at the very top in both the online documentation and the output of `--help` on the command line.
+* `regular`: This should be used for most options.
+* `expert`: This is for options that should be used with care only. A warning is shown in both the online documentation and the command line help.
+* `undocumented`: Such an option is skipped entirely in both the online documentation and the command line help. This should only be used when users don't have a (reasonable) use case for this option (e.g., because it stores data that is added via another option like for `output` and `outputTagHolder`).
+
 Option types
 ------------
 
diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 042fd6b8a..415dbf9f3 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -3,27 +3,30 @@ name   = "Base"
 
 [[option]]
   name       = "err"
-  category   = "undocumented"
+  category   = "regular"
   long       = "err=erroutput"
   type       = "ManagedErr"
   alias      = ["diagnostic-output-channel"]
   predicates = ["setErrStream"]
   includes   = ["<iostream>", "options/managed_streams.h"]
+  help       = "Set the error (or diagnostic) output channel. Writes to stderr for \"stderr\" or \"--\", stdout for \"stdout\" or the given filename otherwise."
 
 [[option]]
   name       = "in"
-  category   = "undocumented"
+  category   = "regular"
   long       = "in=input"
   type       = "ManagedIn"
   includes   = ["<iostream>", "options/managed_streams.h"]
+  help       = "Set the error (or diagnostic) output channel. Reads from stdin for \"stdin\" or \"--\" and the given filename otherwise."
 
 [[option]]
   name       = "out"
-  category   = "undocumented"
+  category   = "regular"
   long       = "out=output"
   type       = "ManagedOut"
   alias      = ["regular-output-channel"]
   includes   = ["<iostream>", "options/managed_streams.h"]
+  help       = "Set the error (or diagnostic) output channel. Writes to stdout for \"stdout\" or \"--\", stderr for \"stderr\" or the given filename otherwise."
 
 [[option]]
   name       = "inputLanguage"
diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml
index 6fc683368..5552a677d 100644
--- a/src/options/parser_options.toml
+++ b/src/options/parser_options.toml
@@ -45,10 +45,11 @@ name   = "Parser"
 # overwrite an existing file with malicious content.
 [[option]]
   name       = "filesystemAccess"
-  category   = "undocumented"
+  category   = "expert"
   long       = "filesystem-access"
   type       = "bool"
   default    = "true"
+  help       = "limits the file system access if set to false"
 
 [[option]]
   name       = "forceLogicString"
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 026c8f494..1e55f63d0 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -377,7 +377,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "solveBVAsInt"
-  category   = "undocumented"
+  category   = "expert"
   long       = "solve-bv-as-int=MODE"
   type       = "SolveBVAsIntMode"
   default    = "OFF"
@@ -401,7 +401,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "BVAndIntegerGranularity"
-  category   = "undocumented"
+  category   = "expert"
   long       = "bvand-integer-granularity=N"
   type       = "uint64_t"
   default    = "1"
@@ -409,7 +409,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "iandMode"
-  category   = "undocumented"
+  category   = "expert"
   long       = "iand-mode=mode"
   type       = "IandMode"
   default    = "VALUE"
@@ -427,7 +427,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "solveIntAsBV"
-  category   = "undocumented"
+  category   = "expert"
   long       = "solve-int-as-bv=N"
   type       = "uint64_t"
   default    = "0"
@@ -435,7 +435,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "solveRealAsInt"
-  category   = "undocumented"
+  category   = "expert"
   long       = "solve-real-as-int"
   type       = "bool"
   default    = "false"
@@ -443,7 +443,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "produceInterpols"
-  category   = "undocumented"
+  category   = "regular"
   long       = "produce-interpols=MODE"
   type       = "ProduceInterpols"
   default    = "NONE"
@@ -470,7 +470,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "produceAbducts"
-  category   = "undocumented"
+  category   = "regular"
   long       = "produce-abducts"
   type       = "bool"
   default    = "false"