From 4d352cb642ef943215711411db7f6f16522b3688 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Fri, 27 Jul 2018 14:54:06 -0700 Subject: [PATCH] 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. --- src/options/arith_options.toml | 30 ++++++++++++++-------------- src/options/arrays_options.toml | 4 ++-- src/options/bv_options.toml | 4 ++-- src/options/main_options.toml | 2 +- src/options/mkoptions.py | 11 ++++++++++ src/options/quantifiers_options.toml | 8 ++++---- src/options/smt_options.toml | 28 +++++++++++++------------- 7 files changed, 49 insertions(+), 38 deletions(-) diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 1d679e47a..c0946c86a 100644 --- 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 c6021adb9..8c82a7fb5 100644 --- 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 ed0bdce7a..15a9047c7 100644 --- 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 42453a92c..9f75e9426 100644 --- 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 b2df21501..f3a045e02 100755 --- 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 eb74592f9..aac84e92c 100644 --- 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 ce7b3eeba..7301272b1 100644 --- 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 -- 2.30.2