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 /test/regress/regress1 | |
| 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 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/arith/arith-brab-test.smt2 | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test/regress/regress1/arith/arith-brab-test.smt2 b/test/regress/regress1/arith/arith-brab-test.smt2 new file mode 100644 index 000000000..7856ae0e6 --- /dev/null +++ b/test/regress/regress1/arith/arith-brab-test.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --arith-brab +; COMMAND-LINE: --no-arith-brab +; EXPECT: sat +(set-logic ALL) + +(declare-fun x1 () Real) +(declare-fun y1 () Real) +(declare-fun m1 () Real) +(declare-fun b1 () Real) + +(declare-fun x () Int) +(declare-fun y () Int) + +(assert (= y1 (+ b1 (* m1 x1)))) +(assert (= x1 (/ m1 (- y1 b1)))) +(assert (= b1 1.25)) +(assert (= m1 (/ 1 3))) + +(assert (and (> x x1) (> y y1))) + +(check-sat) +(exit) + |