From ece041baf842fe713381a74ea8ba247da40811b8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Feb 2020 10:32:49 -0800 Subject: [PATCH] randomize branch direction (outside of int_solver for now) Signed-off-by: Nikolaj Bjorner --- src/math/lp/gomory.cpp | 2 +- src/smt/theory_lra.cpp | 10 +++++++++- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 5a789a610..5148dedc0 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -22,7 +22,7 @@ #include "math/lp/lar_solver.h" #include "math/lp/lp_utils.h" -#define SMALL_CUTS 0 +#define SMALL_CUTS 1 namespace lp { class gomory::imp { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 432f7e11d..234b58b42 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2045,7 +2045,15 @@ public: case lp::lia_move::branch: { TRACE("arith", tout << "branch\n";); - app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); + app_ref b(m); + bool u = m_lia->is_upper(); + auto const & k = m_lia->get_offset(); + if (0 == ctx().get_random_value() % 2) { + b = mk_bound(m_lia->get_term(), k, !u); + } + else { + b = mk_bound(m_lia->get_term(), u ? k - 1 : k + 1, u); + } if (m.has_trace_stream()) { app_ref body(m); body = m.mk_or(b, m.mk_not(b));