src/options/arith_options.toml

   1 id     = "ARITH"
   2 name   = "Arithmetic theory"
   3 header = "options/arith_options.h"
   4
   5 [[option]]
   6   name       = "arithUnateLemmaMode"
   7   category   = "regular"
   8   long       = "unate-lemmas=MODE"
   9   type       = "ArithUnateLemmaMode"
  10   default    = "ALL_PRESOLVE_LEMMAS"
  11   handler    = "stringToArithUnateLemmaMode"
  12   includes   = ["options/arith_unate_lemma_mode.h"]
  13   read_only  = true
  14   help       = "determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)"
  15
  16 [[option]]
  17   name       = "arithPropagationMode"
  18   category   = "regular"
  19   long       = "arith-prop=MODE"
  20   type       = "ArithPropagationMode"
  21   default    = "BOTH_PROP"
  22   handler    = "stringToArithPropagationMode"
  23   includes   = ["options/arith_propagation_mode.h"]
  24   read_only  = true
  25   help       = "turns on arithmetic propagation (default is 'old', see --arith-prop=help)"
  26
  27 # The maximum number of difference pivots to do per invocation of simplex.
  28 # If this is negative, the number of pivots done is the number of variables.
  29 # If this is not set by the user, different logics are free to chose different
  30 # defaults.
  31 [[option]]
  32   name       = "arithHeuristicPivots"
  33   category   = "regular"
  34   long       = "heuristic-pivots=N"
  35   type       = "int16_t"
  36   default    = "0"
  37   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"
  38
  39
  40 # The maximum number of variable order pivots to do per invocation of simplex.
  41 # If this is negative, the number of pivots done is unlimited.
  42 # If this is not set by the user, different logics are free to chose different
  43 # defaults.
  44 [[option]]
  45   name       = "arithStandardCheckVarOrderPivots"
  46   category   = "expert"
  47   long       = "standard-effort-variable-order-pivots=N"
  48   type       = "int16_t"
  49   default    = "-1"
  50   help       = "limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule"
  51
  52 [[option]]
  53   name       = "arithErrorSelectionRule"
  54   category   = "regular"
  55   long       = "error-selection-rule=RULE"
  56   type       = "ErrorSelectionRule"
  57   default    = "MINIMUM_AMOUNT"
  58   handler    = "stringToErrorSelectionRule"
  59   includes   = ["options/arith_heuristic_pivot_rule.h"]
  60   read_only  = true
  61   help       = "change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)"
  62
  63 # The number of pivots before simplex rechecks every basic variable for a conflict
  64 [[option]]
  65   name       = "arithSimplexCheckPeriod"
  66   category   = "regular"
  67   long       = "simplex-check-period=N"
  68   type       = "uint16_t"
  69   default    = "200"
  70   read_only  = true
  71   help       = "the number of pivots to do in simplex before rechecking for a conflict on all variables"
  72
  73 # This is the pivots per basic variable that can be done using heuristic choices
  74 # before variable order must be used.
  75 # If this is not set by the user, different logics are free to chose different
  76 # defaults.
  77 [[option]]
  78   name       = "arithPivotThreshold"
  79   category   = "regular"
  80   long       = "pivot-threshold=N"
  81   type       = "uint16_t"
  82   default    = "2"
  83   help       = "sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order"
  84
  85 [[option]]
  86   name       = "arithPropagateMaxLength"
  87   category   = "regular"
  88   long       = "prop-row-length=N"
  89   type       = "uint16_t"
  90   default    = "16"
  91   read_only  = true
  92   help       = "sets the maximum row length to be used in propagation"
  93
  94 [[option]]
  95   name       = "arithDioSolver"
  96   category   = "regular"
  97   long       = "dio-solver"
  98   type       = "bool"
  99   default    = "true"
 100   read_only  = true
 101   help       = "turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)"
 102
 103 # Whether to split (= x y) into (and (<= x y) (>= x y)) in
 104 # arithmetic preprocessing.
 105 [[option]]
 106   name       = "arithRewriteEq"
 107   category   = "regular"
 108   long       = "arith-rewrite-equalities"
 109   type       = "bool"
 110   default    = "false"
 111   help       = "turns on the preprocessing rewrite turning equalities into a conjunction of inequalities"
 112
 113 [[option]]
 114   name       = "arithMLTrick"
 115   smt_name   = "miplib-trick"
 116   category   = "regular"
 117   long       = "miplib-trick"
 118   type       = "bool"
 119   default    = "false"
 120   read_only  = true
 121   help       = "turns on the preprocessing step of attempting to infer bounds on miplib problems"
 122
 123 [[option]]
 124   name       = "arithMLTrickSubstitutions"
 125   smt_name   = "miplib-trick-subs"
 126   category   = "regular"
 127   long       = "miplib-trick-subs=N"
 128   type       = "unsigned"
 129   default    = "1"
 130   read_only  = true
 131   help       = "do substitution for miplib 'tmp' vars if defined in <= N eliminated vars"
 132
 133 [[option]]
 134   name       = "doCutAllBounded"
 135   category   = "regular"
 136   long       = "cut-all-bounded"
 137   type       = "bool"
 138   default    = "false"
 139   help       = "turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds"
 140
 141 [[option]]
 142   name       = "maxCutsInContext"
 143   category   = "regular"
 144   long       = "maxCutsInContext"
 145   type       = "unsigned"
 146   default    = "65535"
 147   read_only  = true
 148   help       = "maximum cuts in a given context before signalling a restart"
 149
 150 [[option]]
 151   name       = "revertArithModels"
 152   category   = "regular"
 153   long       = "revert-arith-models-on-unsat"
 154   type       = "bool"
 155   default    = "false"
 156   read_only  = true
 157   help       = "revert the arithmetic model to a known safe model on unsat if one is cached"
 158
 159 [[option]]
 160   name       = "havePenalties"
 161   category   = "regular"
 162   long       = "fc-penalties"
 163   type       = "bool"
 164   default    = "false"
 165   help       = "turns on degenerate pivot penalties"
 166
 167 [[option]]
 168   name       = "useFC"
 169   category   = "regular"
 170   long       = "use-fcsimplex"
 171   type       = "bool"
 172   default    = "false"
 173   help       = "use focusing and converging simplex (FMCAD 2013 submission)"
 174
 175 [[option]]
 176   name       = "useSOI"
 177   category   = "regular"
 178   long       = "use-soi"
 179   type       = "bool"
 180   default    = "false"
 181   help       = "use sum of infeasibility simplex (FMCAD 2013 submission)"
 182
 183 [[option]]
 184   name       = "restrictedPivots"
 185   category   = "regular"
 186   long       = "restrict-pivots"
 187   type       = "bool"
 188   default    = "true"
 189   help       = "have a pivot cap for simplex at effort levels below fullEffort"
 190
 191 [[option]]
 192   name       = "collectPivots"
 193   category   = "regular"
 194   long       = "collect-pivot-stats"
 195   type       = "bool"
 196   default    = "false"
 197   help       = "collect the pivot history"
 198
 199 [[option]]
 200   name       = "useApprox"
 201   category   = "regular"
 202   long       = "use-approx"
 203   type       = "bool"
 204   default    = "false"
 205   help       = "attempt to use an approximate solver"
 206
 207 [[option]]
 208   name       = "maxApproxDepth"
 209   category   = "regular"
 210   long       = "approx-branch-depth"
 211   type       = "int16_t"
 212   default    = "200"
 213   help       = "maximum branch depth the approximate solver is allowed to take"
 214
 215 [[option]]
 216   name       = "exportDioDecompositions"
 217   category   = "regular"
 218   long       = "dio-decomps"
 219   type       = "bool"
 220   default    = "false"
 221   help       = "let skolem variables for integer divisibility constraints leak from the dio solver"
 222
 223 [[option]]
 224   name       = "newProp"
 225   category   = "regular"
 226   long       = "new-prop"
 227   type       = "bool"
 228   default    = "false"
 229   help       = "use the new row propagation system"
 230
 231 [[option]]
 232   name       = "arithPropAsLemmaLength"
 233   category   = "regular"
 234   long       = "arith-prop-clauses"
 235   type       = "uint16_t"
 236   default    = "8"
 237   help       = "rows shorter than this are propagated as clauses"
 238
 239 [[option]]
 240   name       = "soiQuickExplain"
 241   category   = "regular"
 242   long       = "soi-qe"
 243   type       = "bool"
 244   default    = "false"
 245   help       = "use quick explain to minimize the sum of infeasibility conflicts"
 246
 247 [[option]]
 248   name       = "rewriteDivk"
 249   category   = "regular"
 250   long       = "rewrite-divk"
 251   type       = "bool"
 252   default    = "false"
 253   help       = "rewrite division and mod when by a constant into linear terms"
 254
 255 [[option]]
 256   name       = "trySolveIntStandardEffort"
 257   category   = "regular"
 258   long       = "se-solve-int"
 259   type       = "bool"
 260   default    = "false"
 261   read_only  = true
 262   help       = "attempt to use the approximate solve integer method on standard effort"
 263
 264 [[option]]
 265   name       = "replayFailureLemma"
 266   category   = "regular"
 267   long       = "lemmas-on-replay-failure"
 268   type       = "bool"
 269   default    = "false"
 270   read_only  = true
 271   help       = "attempt to use external lemmas if approximate solve integer failed"
 272
 273 [[option]]
 274   name       = "dioSolverTurns"
 275   category   = "regular"
 276   long       = "dio-turns"
 277   type       = "int"
 278   default    = "10"
 279   read_only  = true
 280   help       = "turns in a row dio solver cutting gets"
 281
 282 [[option]]
 283   name       = "rrTurns"
 284   category   = "regular"
 285   long       = "rr-turns"
 286   type       = "int"
 287   default    = "3"
 288   read_only  = true
 289   help       = "round robin turn"
 290
 291 [[option]]
 292   name       = "dioRepeat"
 293   category   = "regular"
 294   long       = "dio-repeat"
 295   type       = "bool"
 296   default    = "false"
 297   read_only  = true
 298   help       = "handle dio solver constraints in mass or one at a time"
 299
 300 [[option]]
 301   name       = "replayEarlyCloseDepths"
 302   category   = "regular"
 303   long       = "replay-early-close-depth"
 304   type       = "int"
 305   default    = "1"
 306   read_only  = true
 307   help       = "multiples of the depths to try to close the approx log eagerly"
 308
 309 [[option]]
 310   name       = "replayFailurePenalty"
 311   category   = "regular"
 312   long       = "replay-failure-penalty"
 313   type       = "int"
 314   default    = "100"
 315   read_only  = true
 316   help       = "number of solve integer attempts to skips after a numeric failure"
 317
 318 [[option]]
 319   name       = "replayNumericFailurePenalty"
 320   category   = "regular"
 321   long       = "replay-num-err-penalty"
 322   type       = "int"
 323   default    = "4194304"
 324   read_only  = true
 325   help       = "number of solve integer attempts to skips after a numeric failure"
 326
 327 [[option]]
 328   name       = "replayRejectCutSize"
 329   category   = "regular"
 330   long       = "replay-reject-cut"
 331   type       = "unsigned"
 332   default    = "25500"
 333   read_only  = true
 334   help       = "maximum complexity of any coefficient while replaying cuts"
 335
 336 [[option]]
 337   name       = "lemmaRejectCutSize"
 338   category   = "regular"
 339   long       = "replay-lemma-reject-cut"
 340   type       = "unsigned"
 341   default    = "25500"
 342   read_only  = true
 343   help       = "maximum complexity of any coefficient while outputting replaying cut lemmas"
 344
 345 [[option]]
 346   name       = "soiApproxMajorFailure"
 347   category   = "regular"
 348   long       = "replay-soi-major-threshold"
 349   type       = "double"
 350   default    = ".01"
 351   read_only  = true
 352   help       = "threshold for a major tolerance failure by the approximate solver"
 353
 354 [[option]]
 355   name       = "soiApproxMajorFailurePen"
 356   category   = "regular"
 357   long       = "replay-soi-major-threshold-pen"
 358   type       = "int"
 359   default    = "50"
 360   read_only  = true
 361   help       = "threshold for a major tolerance failure by the approximate solver"
 362
 363 [[option]]
 364   name       = "soiApproxMinorFailure"
 365   category   = "regular"
 366   long       = "replay-soi-minor-threshold"
 367   type       = "double"
 368   default    = ".0001"
 369   read_only  = true
 370   help       = "threshold for a minor tolerance failure by the approximate solver"
 371
 372 [[option]]
 373   name       = "soiApproxMinorFailurePen"
 374   category   = "regular"
 375   long       = "replay-soi-minor-threshold-pen"
 376   type       = "int"
 377   default    = "10"
 378   read_only  = true
 379   help       = "threshold for a minor tolerance failure by the approximate solver"
 380
 381 [[option]]
 382   name       = "ppAssertMaxSubSize"
 383   category   = "regular"
 384   long       = "pp-assert-max-sub-size"
 385   type       = "unsigned"
 386   default    = "2"
 387   read_only  = true
 388   help       = "threshold for substituting an equality in ppAssert"
 389
 390 [[option]]
 391   name       = "arithNoPartialFun"
 392   category   = "regular"
 393   long       = "arith-no-partial-fun"
 394   type       = "bool"
 395   default    = "false"
 396   read_only  = true
 397   help       = "do not use partial function semantics for arithmetic (not SMT LIB compliant)"
 398
 399 [[option]]
 400   name       = "pbRewrites"
 401   category   = "regular"
 402   long       = "pb-rewrites"
 403   type       = "bool"
 404   default    = "false"
 405   read_only  = true
 406   help       = "apply pseudo boolean rewrites"
 407
 408 [[option]]
 409   name       = "sNormInferEq"
 410   category   = "regular"
 411   long       = "snorm-infer-eq"
 412   type       = "bool"
 413   default    = "false"
 414   read_only  = true
 415   help       = "infer equalities based on Shostak normalization"
 416
 417 [[option]]
 418   name       = "nlExt"
 419   category   = "regular"
 420   long       = "nl-ext"
 421   type       = "bool"
 422   default    = "true"
 423   read_only  = true
 424   help       = "extended approach to non-linear"
 425
 426 [[option]]
 427   name       = "nlExtResBound"
 428   category   = "regular"
 429   long       = "nl-ext-rbound"
 430   type       = "bool"
 431   default    = "false"
 432   read_only  = true
 433   help       = "use resolution-style inference for inferring new bounds"
 434
 435 [[option]]
 436   name       = "nlExtFactor"
 437   category   = "regular"
 438   long       = "nl-ext-factor"
 439   type       = "bool"
 440   default    = "true"
 441   read_only  = true
 442   help       = "use factoring inference in non-linear solver"
 443
 444 [[option]]
 445   name       = "nlExtTangentPlanes"
 446   category   = "regular"
 447   long       = "nl-ext-tplanes"
 448   type       = "bool"
 449   default    = "false"
 450   read_only  = true
 451   help       = "use non-terminating tangent plane strategy for non-linear"
 452
 453 [[option]]
 454   name       = "nlExtTfTangentPlanes"
 455   category   = "regular"
 456   long       = "nl-ext-tf-tplanes"
 457   type       = "bool"
 458   default    = "false"
 459   read_only  = true
 460   help       = "use non-terminating tangent plane strategy for transcendental functions for non-linear"
 461
 462 [[option]]
 463   name       = "nlExtEntailConflicts"
 464   category   = "regular"
 465   long       = "nl-ext-ent-conf"
 466   type       = "bool"
 467   default    = "false"
 468   read_only  = true
 469   help       = "check for entailed conflicts in non-linear solver"
 470
 471 [[option]]
 472   name       = "nlExtRewrites"
 473   category   = "regular"
 474   long       = "nl-ext-rewrite"
 475   type       = "bool"
 476   default    = "true"
 477   read_only  = true
 478   help       = "do rewrites in non-linear solver"
 479
 480 [[option]]
 481   name       = "nlExtPurify"
 482   category   = "regular"
 483   long       = "nl-ext-purify"
 484   type       = "bool"
 485   default    = "false"
 486   read_only  = true
 487   help       = "purify non-linear terms at preprocess"
 488
 489 [[option]]
 490   name       = "nlExtSplitZero"
 491   category   = "regular"
 492   long       = "nl-ext-split-zero"
 493   type       = "bool"
 494   default    = "false"
 495   read_only  = true
 496   help       = "intial splits on zero for all variables"
 497
 498 [[option]]
 499   name       = "nlExtTfTaylorDegree"
 500   category   = "regular"
 501   long       = "nl-ext-tf-taylor-deg=N"
 502   type       = "int16_t"
 503   default    = "4"
 504   help       = "initial degree of polynomials for Taylor approximation"
 505
 506 [[option]]
 507   name       = "nlExtTfIncPrecision"
 508   category   = "regular"
 509   long       = "nl-ext-tf-inc-prec"
 510   type       = "bool"
 511   default    = "true"
 512   read_only  = true
 513   help       = "whether to increment the precision for transcendental function constraints"