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