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>

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index ab8164130b9ff2be5b0c44a634bd8623a1cf15dc..1c0351bcbbd12217194d112d6a6b336c14dab8a2 100644 (file)
--- 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 4e2a5bba19b1ecd6857cc5616dfb1e5cd731a607..bed59baf57a4607531438dfeffa2eb3e6d60d2f9 100644 (file)
--- 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 47006622dd2b6a3a5755d5135fdb4b4a4448752e..c540ecbe5514ea2acff12fbc7217a9f612e9299f 100644 (file)
--- 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 (file)
index 0000000..7856ae0
--- /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)
+