Require argument description for non-{bool,void} options. (#2228)

Not adding the argument description for non-{bool,void} options is now an error.

Further, adds missing argument descriptions.

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index 1d679e47adabc5f9fe451211673c65f16972a524..c0946c86a3ded7c7fe8aabc193aa7ba8248cab33 100644 (file)
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -141,7 +141,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "maxCutsInContext"
   category   = "regular"
-  long       = "maxCutsInContext"
+  long       = "maxCutsInContext=N"
   type       = "unsigned"
   default    = "65535"
   read_only  = true
@@ -207,7 +207,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "maxApproxDepth"
   category   = "regular"
-  long       = "approx-branch-depth"
+  long       = "approx-branch-depth=N"
   type       = "int16_t"
   default    = "200"
   help       = "maximum branch depth the approximate solver is allowed to take"
@@ -231,7 +231,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "arithPropAsLemmaLength"
   category   = "regular"
-  long       = "arith-prop-clauses"
+  long       = "arith-prop-clauses=N"
   type       = "uint16_t"
   default    = "8"
   help       = "rows shorter than this are propagated as clauses"
@@ -273,7 +273,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "dioSolverTurns"
   category   = "regular"
-  long       = "dio-turns"
+  long       = "dio-turns=N"
   type       = "int"
   default    = "10"
   read_only  = true
@@ -282,7 +282,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "rrTurns"
   category   = "regular"
-  long       = "rr-turns"
+  long       = "rr-turns=N"
   type       = "int"
   default    = "3"
   read_only  = true
@@ -300,7 +300,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "replayEarlyCloseDepths"
   category   = "regular"
-  long       = "replay-early-close-depth"
+  long       = "replay-early-close-depth=N"
   type       = "int"
   default    = "1"
   read_only  = true
@@ -309,7 +309,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "replayFailurePenalty"
   category   = "regular"
-  long       = "replay-failure-penalty"
+  long       = "replay-failure-penalty=N"
   type       = "int"
   default    = "100"
   read_only  = true
@@ -318,7 +318,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "replayNumericFailurePenalty"
   category   = "regular"
-  long       = "replay-num-err-penalty"
+  long       = "replay-num-err-penalty=N"
   type       = "int"
   default    = "4194304"
   read_only  = true
@@ -327,7 +327,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "replayRejectCutSize"
   category   = "regular"
-  long       = "replay-reject-cut"
+  long       = "replay-reject-cut=N"
   type       = "unsigned"
   default    = "25500"
   read_only  = true
@@ -336,7 +336,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "lemmaRejectCutSize"
   category   = "regular"
-  long       = "replay-lemma-reject-cut"
+  long       = "replay-lemma-reject-cut=N"
   type       = "unsigned"
   default    = "25500"
   read_only  = true
@@ -345,7 +345,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "soiApproxMajorFailure"
   category   = "regular"
-  long       = "replay-soi-major-threshold"
+  long       = "replay-soi-major-threshold=T"
   type       = "double"
   default    = ".01"
   read_only  = true
@@ -354,7 +354,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "soiApproxMajorFailurePen"
   category   = "regular"
-  long       = "replay-soi-major-threshold-pen"
+  long       = "replay-soi-major-threshold-pen=N"
   type       = "int"
   default    = "50"
   read_only  = true
@@ -363,7 +363,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "soiApproxMinorFailure"
   category   = "regular"
-  long       = "replay-soi-minor-threshold"
+  long       = "replay-soi-minor-threshold=T"
   type       = "double"
   default    = ".0001"
   read_only  = true
@@ -372,7 +372,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "soiApproxMinorFailurePen"
   category   = "regular"
-  long       = "replay-soi-minor-threshold-pen"
+  long       = "replay-soi-minor-threshold-pen=N"
   type       = "int"
   default    = "10"
   read_only  = true
@@ -381,7 +381,7 @@ header = "options/arith_options.h"
 [[option]]
   name       = "ppAssertMaxSubSize"
   category   = "regular"
-  long       = "pp-assert-max-sub-size"
+  long       = "pp-assert-max-sub-size=N"
   type       = "unsigned"
   default    = "2"
   read_only  = true

diff --git a/src/options/arrays_options.toml b/src/options/arrays_options.toml
index c6021adb9ce68bdbc078db3f1d5aa02adf7a4063..8c82a7fb578f6edfaf9fbe2b9d210ea541af53e7 100644 (file)
--- a/src/options/arrays_options.toml
+++ b/src/options/arrays_options.toml
@@ -53,7 +53,7 @@ header = "options/arrays_options.h"
 [[option]]
   name       = "arraysConfig"
   category   = "regular"
-  long       = "arrays-config"
+  long       = "arrays-config=N"
   type       = "int"
   default    = "0"
   help       = "set different array option configurations - for developers only"
@@ -69,7 +69,7 @@ header = "options/arrays_options.h"
 [[option]]
   name       = "arraysPropagate"
   category   = "regular"
-  long       = "arrays-prop"
+  long       = "arrays-prop=N"
   type       = "int"
   default    = "2"
   help       = "propagation effort for arrays: 0 is none, 1 is some, 2 is full"

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index ed0bdce7a4bb7affe74969efcda7803b650feb2c..15a9047c7f854abcf3b9c01aa18f8089fb085904 100644 (file)
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -89,7 +89,7 @@ header = "options/bv_options.h"
 [[option]]
   name       = "bitvectorAlgebraicBudget"
   category   = "expert"
-  long       = "bv-algebraic-budget"
+  long       = "bv-algebraic-budget=N"
   type       = "unsigned"
   default    = "1500"
   links      = ["--bv-algebraic-solver"]
@@ -146,7 +146,7 @@ header = "options/bv_options.h"
 [[option]]
   name       = "bvNumFunc"
   category   = "expert"
-  long       = "bv-num-func=NUM"
+  long       = "bv-num-func=N"
   type       = "unsigned"
   default    = "1"
   read_only  = true

diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index 42453a92c966f6c1504a1d18a199896c6d9edbb1..9f75e9426e9ed11ade88c75f6867e737213d96ba 100644 (file)
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -47,7 +47,7 @@ header = "options/main_options.h"
   name       = "seed"
   category   = "common"
   short      = "s"
-  long       = "seed"
+  long       = "seed=N"
   type       = "uint64_t"
   default    = "0"
   read_only  = true

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index b2df2150143cc02e5a5dfb3c3da2d9aca0eda712..f3a045e02a05a0b4798f7efb8bf9506c51ccb54f 100755 (executable)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -485,6 +485,17 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
         else:
             specs.append(TPL_DECL_ASSIGN.format(name=option.name))
 
+        if option.long and option.type not in ['bool', 'void'] and \
+           '=' not in option.long:
+            die("module '{}': option '{}' with type '{}' needs an argument " \
+                "description ('{}=...')".format(
+                    module.id, option.long, option.type, option.long))
+        elif option.long and option.type in ['bool', 'void'] and \
+             '=' in option.long:
+            die("module '{}': option '{}' with type '{}' must not have an " \
+                "argument description".format(
+                    module.id, option.long, option.type))
+
         # Generate module inlines
         inls.append(TPL_IMPL_OP_PAR.format(name=option.name))
         inls.append(TPL_IMPL_OPTION_WAS_SET_BY_USER.format(name=option.name))

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index eb74592f9b292dbe5195e475a0ae9744a5b4f9f2..aac84e92c8936ed70b33dd28095c02a597101104 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -199,7 +199,7 @@ header = "options/quantifiers_options.h"
 [[option]]
   name       = "termDbMode"
   category   = "regular"
-  long       = "term-db-mode"
+  long       = "term-db-mode=MODE"
   type       = "CVC4::theory::quantifiers::TermDbMode"
   default    = "CVC4::theory::quantifiers::TERM_DB_ALL"
   handler    = "stringToTermDbMode"
@@ -331,7 +331,7 @@ header = "options/quantifiers_options.h"
 [[option]]
   name       = "triggerSelMode"
   category   = "regular"
-  long       = "trigger-sel"
+  long       = "trigger-sel=MODE"
   type       = "CVC4::theory::quantifiers::TriggerSelMode"
   default    = "CVC4::theory::quantifiers::TRIGGER_SEL_MIN"
   handler    = "stringToTriggerSelMode"
@@ -341,7 +341,7 @@ header = "options/quantifiers_options.h"
 [[option]]
   name       = "triggerActiveSelMode"
   category   = "regular"
-  long       = "trigger-active-sel"
+  long       = "trigger-active-sel=MODE"
   type       = "CVC4::theory::quantifiers::TriggerActiveSelMode"
   default    = "CVC4::theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL"
   handler    = "stringToTriggerActiveSelMode"
@@ -1278,7 +1278,7 @@ header = "options/quantifiers_options.h"
 [[option]]
   name       = "sygusRewSynthCheckTimeout"
   category   = "regular"
-  long       = "sygus-rr-synth-check-timeout"
+  long       = "sygus-rr-synth-check-timeout=N"
   type       = "unsigned long"
   help       = "timeout (in milliseconds) for the satisfiability check to verify correctness of candidate rewrites"
 

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index ce7b3eebadd12482fae350f5ce84341f658e0430..7301272b1128c6dff6d2f8ba2f53e617f03a00f1 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -345,7 +345,7 @@ header = "options/smt_options.h"
 [[option]]
   name       = "zombieHuntThreshold"
   category   = "regular"
-  long       = "simp-ite-hunt-zombies"
+  long       = "simp-ite-hunt-zombies=N"
   type       = "uint32_t"
   default    = "524288"
   read_only  = true
@@ -478,7 +478,7 @@ header = "options/smt_options.h"
 [[option]]
   name       = "rewriteStep"
   category   = "expert"
-  long       = "rewrite-step"
+  long       = "rewrite-step=N"
   type       = "unsigned"
   default    = "1"
   read_only  = true
@@ -487,7 +487,7 @@ header = "options/smt_options.h"
 [[option]]
   name       = "theoryCheckStep"
   category   = "expert"
-  long       = "theory-check-step"
+  long       = "theory-check-step=N"
   type       = "unsigned"
   default    = "1"
   read_only  = true
@@ -496,7 +496,7 @@ header = "options/smt_options.h"
 [[option]]
   name       = "decisionStep"
   category   = "expert"
-  long       = "decision-step"
+  long       = "decision-step=N"
   type       = "unsigned"
   default    = "1"
   read_only  = true
@@ -505,7 +505,7 @@ header = "options/smt_options.h"
 [[option]]
   name       = "bitblastStep"
   category   = "expert"
-  long       = "bitblast-step"
+  long       = "bitblast-step=N"
   type       = "unsigned"
   default    = "1"
   read_only  = true
@@ -514,7 +514,7 @@ header = "options/smt_options.h"
 [[option]]
   name       = "parseStep"
   category   = "expert"
-  long       = "parse-step"
+  long       = "parse-step=N"
   type       = "unsigned"
   default    = "1"
   read_only  = true
@@ -523,7 +523,7 @@ header = "options/smt_options.h"
 [[option]]
   name       = "lemmaStep"
   category   = "expert"
-  long       = "lemma-step"
+  long       = "lemma-step=N"
   type       = "unsigned"
   default    = "1"
   read_only  = true
@@ -532,7 +532,7 @@ header = "options/smt_options.h"
 [[option]]
   name       = "restartStep"
   category   = "expert"
-  long       = "restart-step"
+  long       = "restart-step=N"
   type       = "unsigned"
   default    = "1"
   read_only  = true
@@ -541,7 +541,7 @@ header = "options/smt_options.h"
 [[option]]
   name       = "cnfStep"
   category   = "expert"
-  long       = "cnf-step"
+  long       = "cnf-step=N"
   type       = "unsigned"
   default    = "1"
   read_only  = true
@@ -550,7 +550,7 @@ header = "options/smt_options.h"
 [[option]]
   name       = "preprocessStep"
   category   = "expert"
-  long       = "preprocess-step"
+  long       = "preprocess-step=N"
   type       = "unsigned"
   default    = "1"
   read_only  = true
@@ -559,7 +559,7 @@ header = "options/smt_options.h"
 [[option]]
   name       = "quantifierStep"
   category   = "expert"
-  long       = "quantifier-step"
+  long       = "quantifier-step=N"
   type       = "unsigned"
   default    = "1"
   read_only  = true
@@ -568,7 +568,7 @@ header = "options/smt_options.h"
 [[option]]
   name       = "satConflictStep"
   category   = "expert"
-  long       = "sat-conflict-step"
+  long       = "sat-conflict-step=N"
   type       = "unsigned"
   default    = "1"
   read_only  = true
@@ -577,7 +577,7 @@ header = "options/smt_options.h"
 [[option]]
   name       = "bvSatConflictStep"
   category   = "expert"
-  long       = "bv-sat-conflict-step"
+  long       = "bv-sat-conflict-step=N"
   type       = "unsigned"
   default    = "1"
   read_only  = true
@@ -625,7 +625,7 @@ header = "options/smt_options.h"
 [[option]]
   name       = "solveIntAsBV"
   category   = "undocumented"
-  long       = "solve-int-as-bv"
+  long       = "solve-int-as-bv=N"
   type       = "uint32_t"
   default    = "0"
   read_only  = true