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 26b1cfecb566bcfa8337a1af75ab65d0988b5869..ce6f2169d19f378633b39a5157459f09919336bc 100644 (file)
--- 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 4cb6dda1d9b488065d8ce53b95ad996edc9ed1a9..173a421ec6fb4c3fb2a5869fd78fa72aa534ce5f 100644 (file)
--- 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 a766dce674c9e7712f0cae8b48cc7ffe1ee6baa7..5eda4bb18f9031a2591f149948c8310027547ae1 100644 (file)
--- 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 05ea7f51273baab22bfc7d8117d6d0137eddce88..576dd41034f84b1a146157c16cbac684a759ab17 100644 (file)
--- 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 80dedfb70fdec5545c301b29ed6b3e9378aaf2d0..24f7fdb3995601bcae157e393211032d3b70c152 100644 (file)
--- 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 abb27ac9f7b7e158c7e5218deb608ca55b4486e8..5522257552d4861c61182e8c346d084698bee8f0 100644 (file)
--- 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 ecd0bcf95ddb743acd64de0debd63029f33dea1b..075ce6fa92c06d8f1a8fde3007fc2fe0d6a12e2d 100644 (file)
--- 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 aeff832b53c92267117b9c91f4c08363b0932c54..04b02e23ebdda5538fe485cecd61172f009a8127 100644 (file)
--- 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 f0875455fbfdede152c57ff4087efcbe7ea9f4f4..f0458793e4d98fc5e9dce686c08b4eca17643d5c 100644 (file)
--- 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 eda5ea963f7195db861a6ef0b22a2cb13bb763f7..229b6b05844925867962ee5b065363f38e49c6b2 100644 (file)
--- 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 4eb3511996a1d9d120b4a3a872d992328d774831..58632aafc88b23b6635421635a81e7e9eb9d4e0e 100644 (file)
--- 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 a97fe572fd6e9ce46a0ba0b56aa00f80cf7969a1..f7bd70a369b4c0fd2a5cbb122ea3f4142a008858 100644 (file)
--- 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 058d8be277c34cfc249e317a8fc56bdaa6316fc2..d90d8f69302fcbc18fe8770dc8bbefde3498055d 100644 (file)
--- 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)"