src/options/arith_options.toml

   1 id     = "ARITH"
   2 name   = "Arithmetic Theory"
   3
   4 [[option]]
   5   name       = "arithUnateLemmaMode"
   6   category   = "regular"
   7   long       = "unate-lemmas=MODE"
   8   type       = "ArithUnateLemmaMode"
   9   default    = "ALL"
  10   help       = "determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)"
  11   help_mode  = "Unate lemmas are generated before SAT search begins using the relationship of constant terms and polynomials."
  12 [[option.mode.ALL]]
  13   name = "all"
  14   help = "A combination of inequalities and equalities."
  15 [[option.mode.EQUALITY]]
  16   name = "eqs"
  17   help = "Outputs lemmas of the general forms (= p c) implies (<= p d) for c < d, or (= p c) implies (not (= p d)) for c != d."
  18 [[option.mode.INEQUALITY]]
  19   name = "ineqs"
  20   help  = "Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d."
  21 [[option.mode.NO]]
  22   name = "none"
  23
  24 [[option]]
  25   name       = "arithPropagationMode"
  26   category   = "regular"
  27   long       = "arith-prop=MODE"
  28   type       = "ArithPropagationMode"
  29   default    = "BOTH_PROP"
  30   help       = "turns on arithmetic propagation (default is 'old', see --arith-prop=help)"
  31   help_mode  = "This decides on kind of propagation arithmetic attempts to do during the search."
  32 [[option.mode.NO_PROP]]
  33   name = "none"
  34 [[option.mode.UNATE_PROP]]
  35   name = "unate"
  36   help = "Use constraints to do unate propagation."
  37 [[option.mode.BOUND_INFERENCE_PROP]]
  38   name = "bi"
  39   help  = "(Bounds Inference) infers bounds on basic variables using the upper and lower bounds of the non-basic variables in the tableau."
  40 [[option.mode.BOTH_PROP]]
  41   name = "both"
  42   help = "Use bounds inference and unate."
  43
  44
  45
  46 # The maximum number of difference pivots to do per invocation of simplex.
  47 # If this is negative, the number of pivots done is the number of variables.
  48 # If this is not set by the user, different logics are free to chose different
  49 # defaults.
  50 [[option]]
  51   name       = "arithHeuristicPivots"
  52   category   = "regular"
  53   long       = "heuristic-pivots=N"
  54   type       = "int64_t"
  55   default    = "0"
  56   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"
  57
  58
  59 # The maximum number of variable order pivots to do per invocation of simplex.
  60 # If this is negative, the number of pivots done is unlimited.
  61 # If this is not set by the user, different logics are free to chose different
  62 # defaults.
  63 [[option]]
  64   name       = "arithStandardCheckVarOrderPivots"
  65   category   = "expert"
  66   long       = "standard-effort-variable-order-pivots=N"
  67   type       = "int64_t"
  68   default    = "-1"
  69   help       = "limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule"
  70
  71 [[option]]
  72   name       = "arithErrorSelectionRule"
  73   category   = "regular"
  74   long       = "error-selection-rule=RULE"
  75   type       = "ErrorSelectionRule"
  76   default    = "MINIMUM_AMOUNT"
  77   help       = "change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)"
  78   help_mode  = "This decides on the rule used by simplex during heuristic rounds for deciding the next basic variable to select."
  79 [[option.mode.MINIMUM_AMOUNT]]
  80   name = "min"
  81   help = "The minimum abs() value of the variable's violation of its bound."
  82 [[option.mode.VAR_ORDER]]
  83   name = "varord"
  84   help = "The variable order."
  85 [[option.mode.MAXIMUM_AMOUNT]]
  86   name = "max"
  87   help = "The maximum violation the bound."
  88 [[option.mode.SUM_METRIC]]
  89   name = "sum"
  90
  91 # The number of pivots before simplex rechecks every basic variable for a conflict
  92 [[option]]
  93   name       = "arithSimplexCheckPeriod"
  94   category   = "regular"
  95   long       = "simplex-check-period=N"
  96   type       = "uint64_t"
  97   default    = "200"
  98   help       = "the number of pivots to do in simplex before rechecking for a conflict on all variables"
  99
 100 # This is the pivots per basic variable that can be done using heuristic choices
 101 # before variable order must be used.
 102 # If this is not set by the user, different logics are free to chose different
 103 # defaults.
 104 [[option]]
 105   name       = "arithPivotThreshold"
 106   category   = "regular"
 107   long       = "pivot-threshold=N"
 108   type       = "uint64_t"
 109   default    = "2"
 110   help       = "sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order"
 111
 112 [[option]]
 113   name       = "arithPropagateMaxLength"
 114   category   = "regular"
 115   long       = "prop-row-length=N"
 116   type       = "uint64_t"
 117   default    = "16"
 118   help       = "sets the maximum row length to be used in propagation"
 119
 120 [[option]]
 121   name       = "arithDioSolver"
 122   category   = "regular"
 123   long       = "dio-solver"
 124   type       = "bool"
 125   default    = "true"
 126   help       = "turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)"
 127
 128 # Whether to split (= x y) into (and (<= x y) (>= x y)) in
 129 # arithmetic preprocessing.
 130 [[option]]
 131   name       = "arithRewriteEq"
 132   category   = "regular"
 133   long       = "arith-rewrite-equalities"
 134   type       = "bool"
 135   default    = "false"
 136   help       = "turns on the preprocessing rewrite turning equalities into a conjunction of inequalities"
 137
 138 [[option]]
 139   name       = "arithMLTrick"
 140   category   = "regular"
 141   long       = "miplib-trick"
 142   type       = "bool"
 143   default    = "false"
 144   help       = "turns on the preprocessing step of attempting to infer bounds on miplib problems"
 145
 146 [[option]]
 147   name       = "arithMLTrickSubstitutions"
 148   category   = "regular"
 149   long       = "miplib-trick-subs=N"
 150   type       = "uint64_t"
 151   default    = "1"
 152   help       = "do substitution for miplib 'tmp' vars if defined in <= N eliminated vars"
 153
 154 [[option]]
 155   name       = "doCutAllBounded"
 156   category   = "regular"
 157   long       = "cut-all-bounded"
 158   type       = "bool"
 159   default    = "false"
 160   help       = "turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds"
 161
 162 [[option]]
 163   name       = "maxCutsInContext"
 164   category   = "regular"
 165   long       = "maxCutsInContext=N"
 166   type       = "uint64_t"
 167   default    = "65535"
 168   help       = "maximum cuts in a given context before signalling a restart"
 169
 170 [[option]]
 171   name       = "revertArithModels"
 172   category   = "regular"
 173   long       = "revert-arith-models-on-unsat"
 174   type       = "bool"
 175   default    = "false"
 176   help       = "revert the arithmetic model to a known safe model on unsat if one is cached"
 177
 178 [[option]]
 179   name       = "havePenalties"
 180   category   = "regular"
 181   long       = "fc-penalties"
 182   type       = "bool"
 183   default    = "false"
 184   help       = "turns on degenerate pivot penalties"
 185
 186 [[option]]
 187   name       = "useFC"
 188   category   = "regular"
 189   long       = "use-fcsimplex"
 190   type       = "bool"
 191   default    = "false"
 192   help       = "use focusing and converging simplex (FMCAD 2013 submission)"
 193
 194 [[option]]
 195   name       = "useSOI"
 196   category   = "regular"
 197   long       = "use-soi"
 198   type       = "bool"
 199   default    = "false"
 200   help       = "use sum of infeasibility simplex (FMCAD 2013 submission)"
 201
 202 [[option]]
 203   name       = "restrictedPivots"
 204   category   = "regular"
 205   long       = "restrict-pivots"
 206   type       = "bool"
 207   default    = "true"
 208   help       = "have a pivot cap for simplex at effort levels below fullEffort"
 209
 210 [[option]]
 211   name       = "collectPivots"
 212   category   = "regular"
 213   long       = "collect-pivot-stats"
 214   type       = "bool"
 215   default    = "false"
 216   help       = "collect the pivot history"
 217
 218 [[option]]
 219   name       = "useApprox"
 220   category   = "regular"
 221   long       = "use-approx"
 222   type       = "bool"
 223   default    = "false"
 224   help       = "attempt to use an approximate solver"
 225
 226 [[option]]
 227   name       = "maxApproxDepth"
 228   category   = "regular"
 229   long       = "approx-branch-depth=N"
 230   type       = "int64_t"
 231   default    = "200"
 232   help       = "maximum branch depth the approximate solver is allowed to take"
 233
 234 [[option]]
 235   name       = "exportDioDecompositions"
 236   category   = "regular"
 237   long       = "dio-decomps"
 238   type       = "bool"
 239   default    = "false"
 240   help       = "let skolem variables for integer divisibility constraints leak from the dio solver"
 241
 242 [[option]]
 243   name       = "newProp"
 244   category   = "regular"
 245   long       = "new-prop"
 246   type       = "bool"
 247   default    = "true"
 248   help       = "use the new row propagation system"
 249
 250 [[option]]
 251   name       = "arithPropAsLemmaLength"
 252   category   = "regular"
 253   long       = "arith-prop-clauses=N"
 254   type       = "uint64_t"
 255   default    = "8"
 256   help       = "rows shorter than this are propagated as clauses"
 257
 258 [[option]]
 259   name       = "soiQuickExplain"
 260   category   = "regular"
 261   long       = "soi-qe"
 262   type       = "bool"
 263   default    = "false"
 264   help       = "use quick explain to minimize the sum of infeasibility conflicts"
 265
 266 [[option]]
 267   name       = "trySolveIntStandardEffort"
 268   category   = "regular"
 269   long       = "se-solve-int"
 270   type       = "bool"
 271   default    = "false"
 272   help       = "attempt to use the approximate solve integer method on standard effort"
 273
 274 [[option]]
 275   name       = "replayFailureLemma"
 276   category   = "regular"
 277   long       = "lemmas-on-replay-failure"
 278   type       = "bool"
 279   default    = "false"
 280   help       = "attempt to use external lemmas if approximate solve integer failed"
 281
 282 [[option]]
 283   name       = "dioSolverTurns"
 284   category   = "regular"
 285   long       = "dio-turns=N"
 286   type       = "int64_t"
 287   default    = "10"
 288   help       = "turns in a row dio solver cutting gets"
 289
 290 [[option]]
 291   name       = "rrTurns"
 292   category   = "regular"
 293   long       = "rr-turns=N"
 294   type       = "int64_t"
 295   default    = "3"
 296   help       = "round robin turn"
 297
 298 [[option]]
 299   name       = "replayEarlyCloseDepths"
 300   category   = "regular"
 301   long       = "replay-early-close-depth=N"
 302   type       = "int64_t"
 303   default    = "1"
 304   help       = "multiples of the depths to try to close the approx log eagerly"
 305
 306 [[option]]
 307   name       = "replayNumericFailurePenalty"
 308   category   = "regular"
 309   long       = "replay-num-err-penalty=N"
 310   type       = "int64_t"
 311   default    = "4194304"
 312   help       = "number of solve integer attempts to skips after a numeric failure"
 313
 314 [[option]]
 315   name       = "replayRejectCutSize"
 316   category   = "regular"
 317   long       = "replay-reject-cut=N"
 318   type       = "uint64_t"
 319   default    = "25500"
 320   help       = "maximum complexity of any coefficient while replaying cuts"
 321
 322 [[option]]
 323   name       = "lemmaRejectCutSize"
 324   category   = "regular"
 325   long       = "replay-lemma-reject-cut=N"
 326   type       = "uint64_t"
 327   default    = "25500"
 328   help       = "maximum complexity of any coefficient while outputting replaying cut lemmas"
 329
 330 [[option]]
 331   name       = "ppAssertMaxSubSize"
 332   category   = "regular"
 333   long       = "pp-assert-max-sub-size=N"
 334   type       = "uint64_t"
 335   default    = "2"
 336   help       = "threshold for substituting an equality in ppAssert"
 337
 338 [[option]]
 339   name       = "arithNoPartialFun"
 340   category   = "regular"
 341   long       = "arith-no-partial-fun"
 342   type       = "bool"
 343   default    = "false"
 344   help       = "do not use partial function semantics for arithmetic (not SMT LIB compliant)"
 345
 346 [[option]]
 347   name       = "pbRewrites"
 348   category   = "regular"
 349   long       = "pb-rewrites"
 350   type       = "bool"
 351   default    = "false"
 352   help       = "apply pseudo boolean rewrites"
 353
 354 [[option]]
 355   name       = "nlExt"
 356   category   = "regular"
 357   long       = "nl-ext=MODE"
 358   type       = "NlExtMode"
 359   default    = "FULL"
 360   help       = "incremental linearization approach to non-linear"
 361   help_mode  = "Modes for the non-linear linearization"
 362 [[option.mode.NONE]]
 363   name = "none"
 364   help = "Disable linearization approach"
 365 [[option.mode.LIGHT]]
 366   name = "light"
 367   help = "Only use a few light-weight lemma schemes"
 368 [[option.mode.FULL]]
 369   name = "full"
 370   help = "Use all lemma schemes"
 371
 372 [[option]]
 373   name       = "nlRlvAssertBounds"
 374   category   = "regular"
 375   long       = "nl-rlv-assert-bounds"
 376   type       = "bool"
 377   default    = "false"
 378   help       = "use bound inference utility to prune when an assertion is entailed by another"
 379
 380 [[option]]
 381   name       = "nlExtResBound"
 382   category   = "regular"
 383   long       = "nl-ext-rbound"
 384   type       = "bool"
 385   default    = "false"
 386   help       = "use resolution-style inference for inferring new bounds in non-linear incremental linearization solver"
 387
 388 [[option]]
 389   name       = "nlExtFactor"
 390   category   = "regular"
 391   long       = "nl-ext-factor"
 392   type       = "bool"
 393   default    = "true"
 394   help       = "use factoring inference in non-linear incremental linearization solver"
 395
 396 [[option]]
 397   name       = "nlExtTangentPlanes"
 398   category   = "regular"
 399   long       = "nl-ext-tplanes"
 400   type       = "bool"
 401   default    = "false"
 402   help       = "use non-terminating tangent plane strategy for non-linear incremental linearization solver"
 403
 404 [[option]]
 405   name       = "nlExtTangentPlanesInterleave"
 406   category   = "regular"
 407   long       = "nl-ext-tplanes-interleave"
 408   type       = "bool"
 409   default    = "false"
 410   help       = "interleave tangent plane strategy for non-linear incremental linearization solver"
 411
 412 [[option]]
 413   name       = "nlExtTfTangentPlanes"
 414   category   = "regular"
 415   long       = "nl-ext-tf-tplanes"
 416   type       = "bool"
 417   default    = "true"
 418   help       = "use non-terminating tangent plane strategy for transcendental functions for non-linear incremental linearization solver"
 419
 420 [[option]]
 421   name       = "nlExtEntailConflicts"
 422   category   = "regular"
 423   long       = "nl-ext-ent-conf"
 424   type       = "bool"
 425   default    = "false"
 426   help       = "check for entailed conflicts in non-linear solver"
 427
 428 [[option]]
 429   name       = "nlExtRewrites"
 430   category   = "regular"
 431   long       = "nl-ext-rewrite"
 432   type       = "bool"
 433   default    = "true"
 434   help       = "do context-dependent simplification based on rewrites in non-linear solver"
 435
 436 [[option]]
 437   name       = "nlExtPurify"
 438   category   = "regular"
 439   long       = "nl-ext-purify"
 440   type       = "bool"
 441   default    = "false"
 442   help       = "purify non-linear terms at preprocess"
 443
 444 [[option]]
 445   name       = "nlExtSplitZero"
 446   category   = "regular"
 447   long       = "nl-ext-split-zero"
 448   type       = "bool"
 449   default    = "false"
 450   help       = "initial splits on zero for all variables"
 451
 452 [[option]]
 453   name       = "nlExtTfTaylorDegree"
 454   category   = "regular"
 455   long       = "nl-ext-tf-taylor-deg=N"
 456   type       = "int64_t"
 457   default    = "4"
 458   help       = "initial degree of polynomials for Taylor approximation"
 459
 460 [[option]]
 461   name       = "nlExtIncPrecision"
 462   category   = "regular"
 463   long       = "nl-ext-inc-prec"
 464   type       = "bool"
 465   default    = "true"
 466   help       = "whether to increment the precision for irrational function constraints"
 467
 468 [[option]]
 469   name       = "nlRlvMode"
 470   category   = "regular"
 471   long       = "nl-rlv=MODE"
 472   type       = "NlRlvMode"
 473   default    = "NONE"
 474   help       = "choose mode for using relevance of assertions in non-linear arithmetic"
 475   help_mode  = "Modes for using relevance of assertions in non-linear arithmetic."
 476 [[option.mode.NONE]]
 477   name = "none"
 478   help = "Do not use relevance."
 479 [[option.mode.INTERLEAVE]]
 480   name = "interleave"
 481   help = "Alternate rounds using relevance."
 482 [[option.mode.ALWAYS]]
 483   name = "always"
 484   help = "Always use relevance."
 485
 486 [[option]]
 487   name       = "brabTest"
 488   category   = "regular"
 489   long       = "arith-brab"
 490   type       = "bool"
 491   default    = "true"
 492   help       = "whether to use simple rounding, similar to a unit-cube test, for integers"
 493
 494 [[option]]
 495   name       = "nlCad"
 496   category   = "regular"
 497   long       = "nl-cad"
 498   type       = "bool"
 499   default    = "false"
 500   help       = "whether to use the cylindrical algebraic coverings solver for non-linear arithmetic"
 501
 502 [[option]]
 503   name       = "nlCadVarElim"
 504   category   = "regular"
 505   long       = "nl-cad-var-elim"
 506   type       = "bool"
 507   default    = "false"
 508   help       = "whether to eliminate variables using equalities before going into the cylindrical algebraic coverings solver"
 509
 510 [[option]]
 511   name       = "nlCadPrune"
 512   category   = "regular"
 513   long       = "nl-cad-prune"
 514   type       = "bool"
 515   default    = "false"
 516   help       = "whether to prune intervals more agressively"
 517
 518 [[option]]
 519   name       = "nlCadLinearModel"
 520   category   = "regular"
 521   long       = "nl-cad-linear-model=MODE"
 522   type       = "NlCadLinearModelMode"
 523   default    = "NONE"
 524   help       = "whether to use the linear model as initial guess for the cylindrical algebraic coverings solver"
 525   help_mode  = "Modes for the usage of the linear model in non-linear arithmetic."
 526 [[option.mode.NONE]]
 527   name       = "none"
 528   help       = "Do not use linear model to seed nonlinear model"
 529 [[option.mode.INITIAL]]
 530   name       = "initial"
 531   help       = "Use linear model to seed nonlinear model initially, discard it when it does not work"
 532 [[option.mode.PERSISTENT]]
 533   name       = "persistent"
 534   help       = "Use linear model to seed nonlinear model whenever possible"
 535
 536 [[option]]
 537   name       = "nlCadProjection"
 538   category   = "expert"
 539   long       = "nl-cad-proj=MODE"
 540   type       = "NlCadProjectionMode"
 541   default    = "MCCALLUM"
 542   help       = "choose the CAD projection operator"
 543   help_mode  = "Modes for the CAD projection operator in non-linear arithmetic."
 544 [[option.mode.MCCALLUM]]
 545   name = "mccallum"
 546   help = "McCallum's projection operator."
 547 [[option.mode.LAZARD]]
 548   name = "lazard"
 549   help = "Lazard's projection operator."
 550 [[option.mode.LAZARDMOD]]
 551   name = "lazard-mod"
 552   help = "A modification of Lazard's projection operator."
 553
 554 [[option]]
 555   name       = "nlCadLifting"
 556   category   = "expert"
 557   long       = "nl-cad-lift=MODE"
 558   type       = "NlCadLiftingMode"
 559   default    = "REGULAR"
 560   help       = "choose the CAD lifting mode"
 561   help_mode  = "Modes for the CAD lifting in non-linear arithmetic."
 562 [[option.mode.REGULAR]]
 563   name = "regular"
 564   help = "Regular lifting."
 565 [[option.mode.LAZARD]]
 566   name = "lazard"
 567   help = "Lazard's lifting scheme."
 568
 569 [[option]]
 570   name       = "nlICP"
 571   category   = "regular"
 572   long       = "nl-icp"
 573   type       = "bool"
 574   default    = "false"
 575   help       = "whether to use ICP-style propagations for non-linear arithmetic"
 576
 577 [[option]]
 578   name       = "arithEqSolver"
 579   category   = "regular"
 580   long       = "arith-eq-solver"
 581   type       = "bool"
 582   default    = "false"
 583   help       = "whether to use the equality solver in the theory of arithmetic"
 584
 585 [[option]]
 586   name       = "arithCongMan"
 587   category   = "regular"
 588   long       = "arith-cong-man"
 589   type       = "bool"
 590   default    = "true"
 591   help       = "(experimental) whether to use the congruence manager when the equality solver is enabled"