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.

1 files changed, 18 insertions, 18 deletions

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"