From ab92c201064614354565707724f0297f2ef8a8d1 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 22 Feb 2020 21:30:09 -0800 Subject: [PATCH] add option branch_flip to lp_settings Signed-off-by: Lev Nachmanson --- src/math/lp/int_branch.cpp | 3 ++- src/math/lp/lp_settings.h | 6 +++++- src/smt/params/smt_params_helper.pyg | 1 + src/smt/theory_array.cpp | 1 - src/smt/theory_lra.cpp | 10 +++------- 5 files changed, 11 insertions(+), 10 deletions(-) diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp index eb670dedd..d840888e5 100644 --- a/src/math/lp/int_branch.cpp +++ b/src/math/lp/int_branch.cpp @@ -34,6 +34,7 @@ namespace lp { return j != -1 ? j : find_inf_int_nbasis_column(); } + lia_move int_branch::create_branch_on_column(int j) { TRACE("check_main_int", tout << "branching" << std::endl;); lp_assert(lia.m_t.is_empty()); @@ -44,7 +45,7 @@ namespace lp { lia.m_k = mpq(0); } else { - lia.m_upper = left_branch_is_more_narrow_than_right(j); + lia.m_upper = lra.settings().branch_flip()? lia.random() % 2 : left_branch_is_more_narrow_than_right(j); lia.m_k = lia.m_upper? floor(lia.get_value(j)) : ceil(lia.get_value(j)); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index a7d7e9b86..099920035 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -200,6 +200,7 @@ public: unsigned limit_on_columns_for_hnf_cutter; bool m_enable_hnf; bool m_print_external_var_name; + bool m_branch_flip; #ifdef Z3DEBUG unsigned m_counter_for_debug; #endif @@ -270,12 +271,15 @@ public: limit_on_rows_for_hnf_cutter(75), limit_on_columns_for_hnf_cutter(150), m_enable_hnf(true), - m_print_external_var_name(false) + m_print_external_var_name(false), + m_branch_flip(false) #ifdef Z3DEBUG , m_counter_for_debug(0) #endif {} + bool branch_flip() const { return m_branch_flip; } + void set_branch_flip(bool f) { m_branch_flip = f; } void set_resource_limit(lp_resource_limit& lim) { m_resource_limit = &lim; } bool get_cancel_flag() const { return m_resource_limit->get_cancel_flag(); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 52131b9dc..092c0adbc 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -62,6 +62,7 @@ def_module_params(module_name='smt', ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'), ('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'), + ('arith.branch_flip', BOOL, False, 'flip branches randomly'), ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), ('arith.ignore_int', BOOL, False, 'treat integer variables as real'), diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index 703423f8f..9e341bb78 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -296,7 +296,6 @@ namespace smt { } void theory_array::apply_sort_cnstr(enode * n, sort * s) { - return; SASSERT(is_array_sort(s)); if (!is_attached_to_var(n)) mk_var(n); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c28cd7f89..4508511b1 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -393,9 +393,10 @@ class theory_lra::imp { lp().settings().print_statistics = lpar.arith_print_stats(); // todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts + lp().settings().set_branch_flip(lpar.arith_branch_flip()); unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio; lp().set_cut_strategy(branch_cut_ratio); - + lp().settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test; lp().settings().set_random_seed(ctx().get_fparams().m_random_seed); m_switcher.m_use_nla = lpar.arith_nla(); @@ -2079,12 +2080,7 @@ public: 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); - } + b = mk_bound(m_lia->get_term(), k, !u); if (m.has_trace_stream()) { app_ref body(m); body = m.mk_or(b, m.mk_not(b));