mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 09:28:45 +00:00
Code Activity

add option branch_flip to lp_settings

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-02-22 21:30:09 -08:00
parent b9bfa950f6
commit ab92c20106
5 changed files with 11 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/int_branch.cpp
View file

@ -34,6 +34,7 @@ namespace lp {
return j != -1 ? j : find_inf_int_nbasis_column(); return j != -1 ? j : find_inf_int_nbasis_column();
} }
lia_move int_branch::create_branch_on_column(int j) { lia_move int_branch::create_branch_on_column(int j) {
TRACE("check_main_int", tout << "branching" << std::endl;); TRACE("check_main_int", tout << "branching" << std::endl;);
lp_assert(lia.m_t.is_empty()); lp_assert(lia.m_t.is_empty());
@ -44,7 +45,7 @@ namespace lp {
lia.m_k = mpq(0); lia.m_k = mpq(0);
} }
else { 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)); lia.m_k = lia.m_upper? floor(lia.get_value(j)) : ceil(lia.get_value(j));
} }

6
src/math/lp/lp_settings.h
View file

@ -200,6 +200,7 @@ public:
unsigned limit_on_columns_for_hnf_cutter; unsigned limit_on_columns_for_hnf_cutter;
bool m_enable_hnf; bool m_enable_hnf;
bool m_print_external_var_name; bool m_print_external_var_name;
bool m_branch_flip;
#ifdef Z3DEBUG #ifdef Z3DEBUG
unsigned m_counter_for_debug; unsigned m_counter_for_debug;
#endif #endif
@ -270,12 +271,15 @@ public:
limit_on_rows_for_hnf_cutter(75), limit_on_rows_for_hnf_cutter(75),
limit_on_columns_for_hnf_cutter(150), limit_on_columns_for_hnf_cutter(150),
m_enable_hnf(true), m_enable_hnf(true),
m_print_external_var_name(false) m_print_external_var_name(false),
m_branch_flip(false)
#ifdef Z3DEBUG #ifdef Z3DEBUG
, m_counter_for_debug(0) , m_counter_for_debug(0)
#endif #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; } void set_resource_limit(lp_resource_limit& lim) { m_resource_limit = &lim; }
bool get_cancel_flag() const { return m_resource_limit->get_cancel_flag(); } bool get_cancel_flag() const { return m_resource_limit->get_cancel_flag(); }

1
src/smt/params/smt_params_helper.pyg
View file

@ -62,6 +62,7 @@ def_module_params(module_name='smt',
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'), ('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.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.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
('arith.ignore_int', BOOL, False, 'treat integer variables as real'), ('arith.ignore_int', BOOL, False, 'treat integer variables as real'),

1
src/smt/theory_array.cpp
View file

@ -296,7 +296,6 @@ namespace smt {
} }
void theory_array::apply_sort_cnstr(enode * n, sort * s) { void theory_array::apply_sort_cnstr(enode * n, sort * s) {
return;
SASSERT(is_array_sort(s)); SASSERT(is_array_sort(s));
if (!is_attached_to_var(n)) if (!is_attached_to_var(n))
mk_var(n); mk_var(n);

10
src/smt/theory_lra.cpp
View file

@ -393,9 +393,10 @@ class theory_lra::imp {
lp().settings().print_statistics = lpar.arith_print_stats(); lp().settings().print_statistics = lpar.arith_print_stats();
// todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts // 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; unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;
lp().set_cut_strategy(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().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test;
lp().settings().set_random_seed(ctx().get_fparams().m_random_seed); lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
m_switcher.m_use_nla = lpar.arith_nla(); m_switcher.m_use_nla = lpar.arith_nla();
@ -2079,12 +2080,7 @@ public:
app_ref b(m); app_ref b(m);
bool u = m_lia->is_upper(); bool u = m_lia->is_upper();
auto const & k = m_lia->get_offset(); auto const & k = m_lia->get_offset();
if (0 == ctx().get_random_value() % 2) { b = mk_bound(m_lia->get_term(), k, !u);
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));