From 479584c063e01e8a5f79ab039c4fb7003e244bbd Mon Sep 17 00:00:00 2001 From: Amalee Date: Thu, 26 Mar 2020 16:32:51 -0700 Subject: [PATCH] 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 Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> Co-authored-by: Andrew Reynolds --- src/options/arith_options.toml | 9 +++++ src/theory/arith/theory_arith_private.cpp | 39 +++++++++++++++---- .../regress0/nl/ext-rew-aggr-test.smt2 | 2 +- .../regress1/arith/arith-brab-test.smt2 | 23 +++++++++++ 4 files changed, 64 insertions(+), 9 deletions(-) create mode 100644 test/regress/regress1/arith/arith-brab-test.smt2 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; diff --git a/test/regress/regress0/nl/ext-rew-aggr-test.smt2 b/test/regress/regress0/nl/ext-rew-aggr-test.smt2 index 47006622d..c540ecbe5 100644 --- a/test/regress/regress0/nl/ext-rew-aggr-test.smt2 +++ b/test/regress/regress0/nl/ext-rew-aggr-test.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg --no-new-prop +; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg --no-new-prop --nl-ext-tplanes ; EXPECT: sat (set-info :smt-lib-version 2.6) (set-logic QF_NIA) 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) + -- 2.30.2