diff options
| author | Amalee <amalee@cs.stanford.edu> | 2020-03-26 16:32:51 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-26 16:32:51 -0700 |
| commit | 479584c063e01e8a5f79ab039c4fb7003e244bbd (patch) | |
| tree | 4614195a2edddf45892dde38eab351427ba50a07 /src/options/arith_options.toml | |
| parent | ea8937689b097d41c70060ed17495feed5d6b95b (diff) | |
Added unit-cube-like test for branch and bound (#3922)
* unit-cude test wip
* test for wip unit cube test
* fixed simple rounding
* wip
* Passing tests except for sat vs unknown ones
* added flag for cube test
* put example back to normal
* Fixed for style guidelines.
* fixed rewrite bug
* removed extra comments
* unit-cude test wip
* test for wip unit cube test
* fixed simple rounding
* wip
* Passing tests except for sat vs unknown ones
* added flag for cube test
* put example back to normal
* Fixed for style guidelines.
* fixed rewrite bug
* removed extra comments
* Small fixes based on PR feedback
* replace NodeManager::currentNM with nm and clang formatted
* renamed test
* Added a regression test that triggers branch and bound
* Added ; COMMAND-LINE: --arith-brab
* Updated arith-brab test
* arith-brab enabled by default
* Added --nl-ext-tplanes to regress0/nl/ext-rew-aggr-test.smt2
Co-authored-by: Amalee Wilson <amalee@cis.uab.edu>
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Diffstat (limited to 'src/options/arith_options.toml')
| -rw-r--r-- | src/options/arith_options.toml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index ab8164130..1c0351bcb 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -551,3 +551,12 @@ header = "options/arith_options.h" default = "true" read_only = true help = "whether to increment the precision for irrational function constraints" + +[[option]] + name = "brabTest" + category = "regular" + long = "arith-brab" + type = "bool" + default = "true" + read_only = true + help = "whether to use simple rounding, similar to a unit-cube test, for integers" |