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.

13 files changed, 62 insertions, 63 deletions

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)"