mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-02 10:58:47 +00:00
Code Activity

create hnf cuts too, when gomory_cut_period is 2

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-07-07 16:18:42 -07:00 • committed by Lev
parent c518ddac6f
commit 5c712d471f
4 changed files with 13 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -40,7 +40,7 @@ def_module_params(module_name='smt',
('bv.reflect', BOOL, True, 'create enode for every bit-vector term'), ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'), ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'),
('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false'), ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false'),
('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'), ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),

2
src/util/lp/int_solver.cpp
View file

@ -599,7 +599,7 @@ lia_move int_solver::make_hnf_cut() {
} }
lia_move int_solver::hnf_cut() { lia_move int_solver::hnf_cut() {
if ((m_number_of_calls) % settings().m_hnf_cut_period == 0) { if ((m_number_of_calls) % settings().hnf_cut_period() == 0) {
return make_hnf_cut(); return make_hnf_cut();
} }
return lia_move::undef; return lia_move::undef;

12
src/util/lp/lar_solver.cpp
View file

@ -2263,16 +2263,16 @@ bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term
} }
void lar_solver::set_cut_strategy(unsigned cut_frequency) { void lar_solver::set_cut_strategy(unsigned cut_frequency) {
if (cut_frequency < 4) { // enable only gomory cut if (cut_frequency < 4) {
settings().m_int_gomory_cut_period = 2; settings().m_int_gomory_cut_period = 2; // do it often
settings().m_hnf_cut_period = 100000000; settings().set_hnf_cut_period(4); // also create hnf cuts
} else if (cut_frequency == 4) { // enable all cuts and cube equally } else if (cut_frequency == 4) { // enable all cuts and cube equally
settings().m_int_gomory_cut_period = 4; settings().m_int_gomory_cut_period = 4;
settings().m_hnf_cut_period = 4; settings().set_hnf_cut_period(4);
} else { } else {
// disable all heuristics // disable all heuristics except cube
settings().m_int_gomory_cut_period = 10000000; settings().m_int_gomory_cut_period = 10000000;
settings().m_hnf_cut_period = 100000000; settings().set_hnf_cut_period(100000000);
} }
} }

5
src/util/lp/lp_settings.h
View file

@ -189,13 +189,18 @@ public:
unsigned column_number_threshold_for_using_lu_in_lar_solver; unsigned column_number_threshold_for_using_lu_in_lar_solver;
unsigned m_int_gomory_cut_period; unsigned m_int_gomory_cut_period;
unsigned m_int_find_cube_period; unsigned m_int_find_cube_period;
private:
unsigned m_hnf_cut_period; unsigned m_hnf_cut_period;
public:
bool m_int_run_gcd_test; bool m_int_run_gcd_test;
bool m_int_pivot_fixed_vars_from_basis; bool m_int_pivot_fixed_vars_from_basis;
bool m_int_patch_only_integer_values; bool m_int_patch_only_integer_values;
unsigned limit_on_rows_for_hnf_cutter; unsigned limit_on_rows_for_hnf_cutter;
unsigned limit_on_columns_for_hnf_cutter; unsigned limit_on_columns_for_hnf_cutter;
unsigned hnf_cut_period() const { return m_hnf_cut_period; }
void set_hnf_cut_period(unsigned period) { m_hnf_cut_period = period; }
unsigned random_next() { return m_rand(); } unsigned random_next() { return m_rand(); }
void set_random_seed(unsigned s) { m_rand.set_seed(s); } void set_random_seed(unsigned s) { m_rand.set_seed(s); }