From: Gereon Kremer Date: Tue, 3 Aug 2021 21:44:35 +0000 (-0700) Subject: Use int64_t, uint64_t or double for all numeric options. (#6970) X-Git-Tag: cvc5-1.0.0~1417 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1cb1934d76f25e9f42f51b2eead733b3e9e12236;p=cvc5.git Use int64_t, uint64_t or double for all numeric options. (#6970) This PR further simplifies the option setup by only using int64_t or uint64_t for integer options. --- diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 26b1cfecb..ce6f2169d 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -51,7 +51,7 @@ name = "Arithmetic Theory" name = "arithHeuristicPivots" category = "regular" long = "heuristic-pivots=N" - type = "int16_t" + type = "int64_t" default = "0" help = "the number of times to apply the heuristic pivot rule; if N < 0, this defaults to the number of variables; if this is unset, this is tuned by the logic selection" @@ -64,7 +64,7 @@ name = "Arithmetic Theory" name = "arithStandardCheckVarOrderPivots" category = "expert" long = "standard-effort-variable-order-pivots=N" - type = "int16_t" + type = "int64_t" default = "-1" help = "limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule" @@ -93,7 +93,7 @@ name = "Arithmetic Theory" name = "arithSimplexCheckPeriod" category = "regular" long = "simplex-check-period=N" - type = "uint16_t" + type = "uint64_t" default = "200" help = "the number of pivots to do in simplex before rechecking for a conflict on all variables" @@ -105,7 +105,7 @@ name = "Arithmetic Theory" name = "arithPivotThreshold" category = "regular" long = "pivot-threshold=N" - type = "uint16_t" + type = "uint64_t" default = "2" help = "sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order" @@ -113,7 +113,7 @@ name = "Arithmetic Theory" name = "arithPropagateMaxLength" category = "regular" long = "prop-row-length=N" - type = "uint16_t" + type = "uint64_t" default = "16" help = "sets the maximum row length to be used in propagation" @@ -147,7 +147,7 @@ name = "Arithmetic Theory" name = "arithMLTrickSubstitutions" category = "regular" long = "miplib-trick-subs=N" - type = "unsigned" + type = "uint64_t" default = "1" help = "do substitution for miplib 'tmp' vars if defined in <= N eliminated vars" @@ -163,7 +163,7 @@ name = "Arithmetic Theory" name = "maxCutsInContext" category = "regular" long = "maxCutsInContext=N" - type = "unsigned" + type = "uint64_t" default = "65535" help = "maximum cuts in a given context before signalling a restart" @@ -227,7 +227,7 @@ name = "Arithmetic Theory" name = "maxApproxDepth" category = "regular" long = "approx-branch-depth=N" - type = "int16_t" + type = "int64_t" default = "200" help = "maximum branch depth the approximate solver is allowed to take" @@ -251,7 +251,7 @@ name = "Arithmetic Theory" name = "arithPropAsLemmaLength" category = "regular" long = "arith-prop-clauses=N" - type = "uint16_t" + type = "uint64_t" default = "8" help = "rows shorter than this are propagated as clauses" @@ -283,7 +283,7 @@ name = "Arithmetic Theory" name = "dioSolverTurns" category = "regular" long = "dio-turns=N" - type = "int" + type = "int64_t" default = "10" help = "turns in a row dio solver cutting gets" @@ -291,7 +291,7 @@ name = "Arithmetic Theory" name = "rrTurns" category = "regular" long = "rr-turns=N" - type = "int" + type = "int64_t" default = "3" help = "round robin turn" @@ -307,7 +307,7 @@ name = "Arithmetic Theory" name = "replayEarlyCloseDepths" category = "regular" long = "replay-early-close-depth=N" - type = "int" + type = "int64_t" default = "1" help = "multiples of the depths to try to close the approx log eagerly" @@ -315,7 +315,7 @@ name = "Arithmetic Theory" name = "replayFailurePenalty" category = "regular" long = "replay-failure-penalty=N" - type = "int" + type = "int64_t" default = "100" help = "number of solve integer attempts to skips after a numeric failure" @@ -323,7 +323,7 @@ name = "Arithmetic Theory" name = "replayNumericFailurePenalty" category = "regular" long = "replay-num-err-penalty=N" - type = "int" + type = "int64_t" default = "4194304" help = "number of solve integer attempts to skips after a numeric failure" @@ -331,7 +331,7 @@ name = "Arithmetic Theory" name = "replayRejectCutSize" category = "regular" long = "replay-reject-cut=N" - type = "unsigned" + type = "uint64_t" default = "25500" help = "maximum complexity of any coefficient while replaying cuts" @@ -339,7 +339,7 @@ name = "Arithmetic Theory" name = "lemmaRejectCutSize" category = "regular" long = "replay-lemma-reject-cut=N" - type = "unsigned" + type = "uint64_t" default = "25500" help = "maximum complexity of any coefficient while outputting replaying cut lemmas" @@ -355,7 +355,7 @@ name = "Arithmetic Theory" name = "soiApproxMajorFailurePen" category = "regular" long = "replay-soi-major-threshold-pen=N" - type = "int" + type = "int64_t" default = "50" help = "threshold for a major tolerance failure by the approximate solver" @@ -371,7 +371,7 @@ name = "Arithmetic Theory" name = "soiApproxMinorFailurePen" category = "regular" long = "replay-soi-minor-threshold-pen=N" - type = "int" + type = "int64_t" default = "10" help = "threshold for a minor tolerance failure by the approximate solver" @@ -379,7 +379,7 @@ name = "Arithmetic Theory" name = "ppAssertMaxSubSize" category = "regular" long = "pp-assert-max-sub-size=N" - type = "unsigned" + type = "uint64_t" default = "2" help = "threshold for substituting an equality in ppAssert" @@ -493,7 +493,7 @@ name = "Arithmetic Theory" name = "nlExtTfTaylorDegree" category = "regular" long = "nl-ext-tf-taylor-deg=N" - type = "int16_t" + type = "int64_t" default = "4" help = "initial degree of polynomials for Taylor approximation" diff --git a/src/options/arrays_options.toml b/src/options/arrays_options.toml index 4cb6dda1d..173a421ec 100644 --- a/src/options/arrays_options.toml +++ b/src/options/arrays_options.toml @@ -45,7 +45,7 @@ name = "Arrays Theory" name = "arraysConfig" category = "regular" long = "arrays-config=N" - type = "int" + type = "int64_t" default = "0" help = "set different array option configurations - for developers only" @@ -61,7 +61,7 @@ name = "Arrays Theory" name = "arraysPropagate" category = "regular" long = "arrays-prop=N" - type = "int" + type = "int64_t" default = "2" help = "propagation effort for arrays: 0 is none, 1 is some, 2 is full" diff --git a/src/options/base_options.toml b/src/options/base_options.toml index a766dce67..5eda4bb18 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -55,7 +55,7 @@ public = true name = "verbosity" long = "verbosity=N" category = "regular" - type = "int" + type = "int64_t" default = "0" predicates = ["setVerbosity"] help = "the verbosity level of cvc5" diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 05ea7f512..576dd4103 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -88,7 +88,7 @@ name = "Bitvector Theory" name = "bitvectorAlgebraicBudget" category = "expert" long = "bv-algebraic-budget=N" - type = "unsigned" + type = "uint64_t" default = "1500" help = "the budget allowed for the algebraic solver in number of SAT conflicts" @@ -154,7 +154,7 @@ name = "Bitvector Theory" name = "bvNumFunc" category = "expert" long = "bv-num-func=N" - type = "unsigned" + type = "uint64_t" default = "1" help = "number of function symbols in conflicts that are generalized" diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index 80dedfb70..24f7fdb39 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -169,6 +169,6 @@ name = "Datatypes Theory" name = "sygusAbortSize" category = "regular" long = "sygus-abort-size=N" - type = "int" + type = "int64_t" default = "-1" help = "tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)" diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml index abb27ac9f..552225755 100644 --- a/src/options/decision_options.toml +++ b/src/options/decision_options.toml @@ -48,7 +48,7 @@ name = "Decision Heuristics" name = "decisionRandomWeight" category = "expert" long = "decision-random-weight=N" - type = "int" + type = "int64_t" default = "0" help = "assign random weights to nodes between 0 and N-1 (0: disable)" diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml index ecd0bcf95..075ce6fa9 100644 --- a/src/options/expr_options.toml +++ b/src/options/expr_options.toml @@ -5,7 +5,7 @@ name = "Expression" name = "defaultExprDepth" category = "regular" long = "expr-depth=N" - type = "int" + type = "int64_t" default = "0" predicates = ["setDefaultExprDepthPredicate"] help = "print exprs to depth N (0 == default, -1 == no limit)" @@ -14,7 +14,7 @@ name = "Expression" name = "defaultDagThresh" category = "regular" long = "dag-thresh=N" - type = "int" + type = "int64_t" default = "1" predicates = ["setDefaultDagThreshPredicate"] help = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)" diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index aeff832b5..04b02e23e 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -61,7 +61,6 @@ OPTION_ATTR_ALL = OPTION_ATTR_REQ + [ ] CATEGORY_VALUES = ['common', 'expert', 'regular', 'undocumented'] -SUPPORTED_CTYPES = ['int', 'unsigned', 'unsigned long', 'double'] ### Other globals @@ -249,12 +248,16 @@ def get_getall(module, option): if option.type == 'bool': return 'res.push_back({{"{}", opts.{}.{} ? "true" : "false"}});'.format( option.long_name, module.id, option.name) + elif option.type == 'std::string': + return 'res.push_back({{"{}", opts.{}.{}}});'.format( + option.long_name, module.id, option.name) elif is_numeric_cpp_type(option.type): return 'res.push_back({{"{}", std::to_string(opts.{}.{})}});'.format( option.long_name, module.id, option.name) else: - return '{{ std::stringstream ss; ss << opts.{}.{}; res.push_back({{"{}", ss.str()}}); }}'.format( - module.id, option.name, option.long_name) + return '{{ std::stringstream ss; ss << opts.{}.{}; res.push_back({{"{}", ss.str()}}); }}'.format(module.id, + option.name, option.long_name) + class Module(object): """Options module. @@ -459,11 +462,7 @@ def is_numeric_cpp_type(ctype): Check if given type is a numeric C++ type (this should cover the most common cases). """ - if ctype in SUPPORTED_CTYPES: - return True - elif re.match('u?int[0-9]+_t', ctype): - return True - return False + return ctype in ['int64_t', 'uint64_t', 'double'] def format_include(include): diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index f0875455f..f0458793e 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -31,7 +31,7 @@ name = "Proof" name = "proofPedantic" category = "regular" long = "proof-pedantic=N" - type = "uint32_t" + type = "uint64_t" default = "0" help = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof" diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml index eda5ea963..229b6b058 100644 --- a/src/options/prop_options.toml +++ b/src/options/prop_options.toml @@ -15,7 +15,7 @@ name = "SAT Layer" name = "satRandomSeed" category = "regular" long = "random-seed=S" - type = "uint32_t" + type = "uint64_t" default = "0" help = "sets the random seed for the sat solver" @@ -39,7 +39,7 @@ name = "SAT Layer" name = "satRestartFirst" category = "regular" long = "restart-int-base=N" - type = "unsigned" + type = "uint64_t" default = "25" help = "sets the base restart interval for the sat solver (N=25 by default)" diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 4eb351199..58632aafc 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -446,7 +446,7 @@ name = "Quantifiers" name = "instWhenPhase" category = "regular" long = "inst-when-phase=N" - type = "int" + type = "int64_t" default = "2" help = "instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen" @@ -462,7 +462,7 @@ name = "Quantifiers" name = "instMaxLevel" category = "regular" long = "inst-max-level=N" - type = "int" + type = "int64_t" default = "-1" help = "maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)" @@ -478,7 +478,7 @@ name = "Quantifiers" name = "instMaxRounds" category = "regular" long = "inst-max-rounds=N" - type = "int" + type = "int64_t" default = "-1" help = "maximum number of instantiation rounds (-1 == no limit, default)" @@ -520,7 +520,7 @@ name = "Quantifiers" name = "fullSaturateLimit" category = "regular" long = "full-saturate-quant-limit=N" - type = "int" + type = "int64_t" default = "-1" help = "maximum number of rounds of enumerative instantiation to apply (-1 means no limit)" @@ -697,7 +697,7 @@ name = "Quantifiers" name = "fmfTypeCompletionThresh" category = "regular" long = "fmf-type-completion-thresh=N" - type = "int" + type = "int64_t" default = "1000" help = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted" @@ -850,7 +850,7 @@ name = "Quantifiers" name = "conjectureGenPerRound" category = "regular" long = "conjecture-gen-per-round=N" - type = "int" + type = "int64_t" default = "1" help = "number of conjectures to generate per instantiation round" @@ -890,7 +890,7 @@ name = "Quantifiers" name = "conjectureGenGtEnum" category = "regular" long = "conjecture-gen-gt-enum=N" - type = "int" + type = "int64_t" default = "50" help = "number of ground terms to generate for model filtering" @@ -906,7 +906,7 @@ name = "Quantifiers" name = "conjectureGenMaxDepth" category = "regular" long = "conjecture-gen-max-depth=N" - type = "int" + type = "int64_t" default = "3" help = "maximum depth of terms to consider for conjectures" @@ -985,7 +985,7 @@ name = "Quantifiers" name = "cegqiSingleInvReconstructLimit" category = "regular" long = "sygus-si-rcons-limit=N" - type = "int" + type = "int64_t" default = "10000" help = "number of rounds of enumeration to use during solution reconstruction (negative means unlimited)" @@ -1089,7 +1089,7 @@ name = "Quantifiers" name = "sygusRepairConstTimeout" category = "regular" long = "sygus-repair-const-timeout=N" - type = "unsigned long" + type = "uint64_t" help = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions" [[option]] @@ -1120,7 +1120,7 @@ name = "Quantifiers" name = "sygusActiveGenEnumConsts" category = "regular" long = "sygus-active-gen-cfactor=N" - type = "unsigned long" + type = "uint64_t" default = "5" help = "the branching factor for the number of interpreted constants to consider for each size when using --sygus-active-gen=enum" @@ -1231,7 +1231,7 @@ name = "Quantifiers" name = "sygusPbeMultiFairDiff" category = "regular" long = "sygus-pbe-multi-fair-diff=N" - type = "int" + type = "int64_t" default = "0" help = "when using multiple enumerators, ensure that we only register values of minimial term size plus this value (default 0)" @@ -1313,7 +1313,7 @@ name = "Quantifiers" name = "sygusRecFunEvalLimit" category = "regular" long = "sygus-rec-fun-eval-limit=N" - type = "unsigned" + type = "uint64_t" default = "1000" help = "use a hard limit for how many times in a given evaluator call a recursive function can be evaluated (so infinite loops can be avoided)" @@ -1321,7 +1321,7 @@ name = "Quantifiers" name = "sygusVerifyInstMaxRounds" category = "regular" long = "sygus-verify-inst-max-rounds=N" - type = "int" + type = "int64_t" default = "3" help = "maximum number of instantiation rounds for sygus verification calls (-1 == no limit, default is 3)" @@ -1395,7 +1395,7 @@ name = "Quantifiers" name = "sygusSamples" category = "regular" long = "sygus-samples=N" - type = "int" + type = "int64_t" default = "1000" help = "number of points to consider when doing sygus rewriter sample testing" @@ -1443,7 +1443,7 @@ name = "Quantifiers" name = "sygusRewSynthInputNVars" category = "regular" long = "sygus-rr-synth-input-nvars=N" - type = "int" + type = "int64_t" default = "3" help = "the maximum number of variables per type that appear in rewrites from sygus-rr-synth-input" @@ -1459,7 +1459,7 @@ name = "Quantifiers" name = "sygusExprMinerCheckTimeout" category = "regular" long = "sygus-expr-miner-check-timeout=N" - type = "unsigned long" + type = "uint64_t" help = "timeout (in milliseconds) for satisfiability checks in expression miners" [[option]] @@ -1482,7 +1482,7 @@ name = "Quantifiers" name = "sygusQueryGenThresh" category = "regular" long = "sygus-query-gen-thresh=N" - type = "unsigned" + type = "uint64_t" default = "5" help = "number of points that we allow to be equal for enumerating satisfiable queries with sygus-query-gen" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index a97fe572f..f7bd70a36 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -323,7 +323,7 @@ name = "SMT Layer" name = "zombieHuntThreshold" category = "regular" long = "simp-ite-hunt-zombies=N" - type = "uint32_t" + type = "uint64_t" default = "524288" help = "post ite compression enables zombie removal while the number of nodes is above this threshold" @@ -421,7 +421,7 @@ name = "SMT Layer" name = "BVAndIntegerGranularity" category = "undocumented" long = "bvand-integer-granularity=N" - type = "uint32_t" + type = "uint64_t" default = "1" help = "granularity to use in --solve-bv-as-int mode and for iand operator (experimental)" @@ -447,7 +447,7 @@ name = "SMT Layer" name = "solveIntAsBV" category = "undocumented" long = "solve-int-as-bv=N" - type = "uint32_t" + type = "uint64_t" default = "0" help = "attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)" diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml index 058d8be27..d90d8f693 100644 --- a/src/options/uf_options.toml +++ b/src/options/uf_options.toml @@ -14,7 +14,7 @@ name = "Uninterpreted Functions Theory" name = "ufssTotalityLimited" category = "regular" long = "uf-ss-totality-limited=N" - type = "int" + type = "int64_t" default = "-1" help = "apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)" @@ -30,7 +30,7 @@ name = "Uninterpreted Functions Theory" name = "ufssAbortCardinality" category = "regular" long = "uf-ss-abort-card=N" - type = "int" + type = "int64_t" default = "-1" help = "tells the uf with cardinality to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)"