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 | |
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')
-rw-r--r-- | src/options/arith_options.toml | 9 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 39 |
2 files changed, 40 insertions, 8 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" diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 4e2a5bba1..bed59baf5 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -3943,15 +3943,38 @@ Node TheoryArithPrivate::branchIntegerVariable(ArithVar x) const { TNode var = d_partialModel.asNode(x); Integer floor_d = d.floor(); - //Node eq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, var, mkRationalNode(floor_d+1))); - //Node diseq = eq.notNode(); - - Node ub = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d))); - Node lb = ub.notNode(); - + Node lem; + NodeManager* nm = NodeManager::currentNM(); + if (options::brabTest()) + { + Trace("integers") << "branch-round-and-bound enabled" << endl; + Integer ceil_d = d.ceiling(); + Rational f = r - floor_d; + // Multiply by -1 to get abs value. + Rational c = (r - ceil_d) * (-1); + Integer nearest = (c > f) ? floor_d : ceil_d; + + // Prioritize trying a simple rounding of the real solution first, + // it that fails, fall back on original branch and bound strategy. + Node ub = Rewriter::rewrite( + nm->mkNode(kind::LEQ, var, mkRationalNode(nearest - 1))); + Node lb = Rewriter::rewrite( + nm->mkNode(kind::GEQ, var, mkRationalNode(nearest + 1))); + lem = nm->mkNode(kind::OR, ub, lb); + Node eq = Rewriter::rewrite( + nm->mkNode(kind::EQUAL, var, mkRationalNode(nearest))); + Node literal = d_containing.getValuation().ensureLiteral(eq); + d_containing.getOutputChannel().requirePhase(literal, true); + lem = nm->mkNode(kind::OR, literal, lem); + } + else + { + Node ub = + Rewriter::rewrite(nm->mkNode(kind::LEQ, var, mkRationalNode(floor_d))); + Node lb = ub.notNode(); + lem = nm->mkNode(kind::OR, ub, lb); + } - //Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, diseq); - Node lem = NodeManager::currentNM()->mkNode(kind::OR, ub, lb); Trace("integers") << "integers: branch & bound: " << lem << endl; if(isSatLiteral(lem[0])) { Debug("integers") << " " << lem[0] << " == " << getSatValue(lem[0]) << endl; |