diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index d0dd0a9e2..ec9d51a01 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -1151,7 +1151,7 @@ namespace lp { } // c_g is not integral if (lra.stats().m_dio_calls % - lra.settings().dio_cut_from_proof_period() == + lra.settings().dio_branch_from_proof_period() == 0 && !has_fresh_var(ei)) prepare_lia_branch_report(ei, e, g, c_g); @@ -1414,7 +1414,7 @@ namespace lp { // term_to_lar_solver(remove_fresh_vars(create_term_from_ind_c()))) // enable_trace("dioph_eq"); - TRACE("dioph_eq_deb", tout << "after subs\n"; + TRACE("dioph_eq_deb_subs", tout << "after subs\n"; print_term_o(create_term_from_ind_c(), tout) << std::endl; tout << "term_to_tighten:"; print_lar_term_L(term_to_tighten, tout) << std::endl; @@ -1581,7 +1581,7 @@ namespace lp { while (progress) { if (!normalize_by_gcd()) { if (m_report_branch) { - lra.stats().m_dio_cut_from_proofs++; + lra.stats().m_dio_branch_from_proofs++; m_report_branch = false; return lia_move::branch; } else { @@ -1898,6 +1898,18 @@ namespace lp { return false; } if (it->second != p.second) { + TRACE("dioph_eq_deb", tout << "m_columns_to_terms[" << j << "] has to be "; + tout << "{"; + for(unsigned lll : p.second) { + tout << lll << ", "; + } + tout << "}, \nbut it is {"; + for (unsigned lll : it->second) { + tout << lll << ", "; + }; + tout << "}" << std::endl; + + ); return false; } } diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 421859ec0..d61de21f7 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -190,7 +190,7 @@ namespace lp { } bool should_gomory_cut() { - return !settings().dio_cuts() + return (!settings().dio_eqs() || settings().dio_enable_gomory_cuts()) && m_number_of_calls % settings().m_int_gomory_cut_period == 0; } @@ -199,7 +199,8 @@ namespace lp { } bool should_hnf_cut() { - return !settings().dio_cuts() && settings().enable_hnf() && m_number_of_calls % settings().hnf_cut_period() == 0; + return (!settings().dio_eqs() || settings().dio_enable_hnf_cuts()) + && settings().enable_hnf() && m_number_of_calls % settings().hnf_cut_period() == 0; } lia_move hnf_cut() { diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 7c65b9b15..7029af8ce 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -33,6 +33,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) { m_simplex_strategy = static_cast(p.arith_simplex_strategy()); m_nlsat_delay = p.arith_nl_delay(); m_dio_eqs = p.arith_lp_dio_eqs(); - m_dio_cuts = m_dio_eqs && p.arith_lp_dio_cuts(); - m_dio_cut_from_proof_period = p.arith_lp_dio_cut_from_proof_period(); + m_dio_branch_from_proof_period = p.arith_lp_dio_branch_from_proof_period(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index b7928e2cd..77e0871e8 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -133,7 +133,7 @@ struct statistics { unsigned m_dio_tighten_conflicts = 0; unsigned m_dio_branch_iterations= 0; unsigned m_dio_branching_depth = 0; - unsigned m_dio_cut_from_proofs = 0; + unsigned m_dio_branch_from_proofs = 0; unsigned m_dio_branching_infeasibles = 0; unsigned m_dio_rewrite_conflicts = 0; unsigned m_dio_branching_sats = 0; @@ -174,7 +174,7 @@ struct statistics { st.update("arith-dio-tighten-conflicts", m_dio_tighten_conflicts); st.update("arith-dio-branch-iterations", m_dio_branch_iterations); st.update("arith-dio-branch-depths", m_dio_branching_depth); - st.update("arith-dio-cut-from-proofs", m_dio_cut_from_proofs); + st.update("arith-dio-branch-from-proofs", m_dio_branch_from_proofs); st.update("arith-dio-branching-infeasibles", m_dio_branching_infeasibles); st.update("arith-dio-rewrite-conflicts", m_dio_rewrite_conflicts); st.update("arith-dio-branching-sats", m_dio_branching_sats); @@ -249,8 +249,9 @@ private: bool m_print_external_var_name = false; bool m_propagate_eqs = false; bool m_dio_eqs = false; - bool m_dio_cuts = false; - unsigned m_dio_cut_from_proof_period = 2; + bool m_dio_enable_gomory_cuts = true; + bool m_dio_enable_hnf_cuts = true; + unsigned m_dio_branch_from_proof_period = 100; // report rarely public: bool print_external_var_name() const { return m_print_external_var_name; } @@ -260,8 +261,9 @@ public: unsigned random_next() { return m_rand(); } unsigned random_next(unsigned u ) { return m_rand(u); } bool dio_eqs() { return m_dio_eqs; } - bool dio_cuts() { return m_dio_eqs && m_dio_cuts; } - unsigned dio_cut_from_proof_period() { return m_dio_cut_from_proof_period; } + bool dio_enable_gomory_cuts() { return m_dio_eqs && m_dio_enable_gomory_cuts; } + bool dio_enable_hnf_cuts() { return m_dio_eqs && m_dio_enable_hnf_cuts; } + unsigned dio_branch_from_proof_period() { return m_dio_branch_from_proof_period; } void set_random_seed(unsigned s) { m_rand.set_seed(s); } bool bound_progation() const { diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 8dc6b8574..4d8b4378f 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -58,8 +58,9 @@ def_module_params(module_name='smt', ('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.lp.dio_eqs', BOOL, True, 'use Diophantine equalities'), - ('arith.lp.dio_cut_from_proof_period', UINT, 3, 'Period of creating a cut from proof in dioph equations'), - ('arith.lp.dio_cuts', BOOL, True, 'use cuts from Diophantine equalities conflics instead of Gomory cuts, only works when dioph_eq is true'), + ('arith.lp.dio_branch_from_proof_period', UINT, 100, 'Period of creating a branch instead of a cut'), + ('arith.lp.dio_cuts_enable_gomory', BOOL, True, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'), + ('arith.lp.dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'), ('arith.nl.nra', BOOL, True, 'call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6'), ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),