mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 21:33:39 +00:00
Code Activity

randomize branch direction (outside of int_solver for now)

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-01 10:32:49 -08:00
parent 1e92165690
commit ece041baf8
2 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/gomory.cpp
View file

@ -22,7 +22,7 @@
#include "math/lp/lar_solver.h" #include "math/lp/lar_solver.h"
#include "math/lp/lp_utils.h" #include "math/lp/lp_utils.h"
#define SMALL_CUTS 0 #define SMALL_CUTS 1
namespace lp { namespace lp {
class gomory::imp { class gomory::imp {

10
src/smt/theory_lra.cpp
View file

@ -2045,7 +2045,15 @@ public:
case lp::lia_move::branch: { case lp::lia_move::branch: {
TRACE("arith", tout << "branch\n";); 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()) { if (m.has_trace_stream()) {
app_ref body(m); app_ref body(m);
body = m.mk_or(b, m.mk_not(b)); body = m.mk_or(b, m.mk_not(b));