mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

hook up more lp_params

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-05-19 03:47:45 -07:00
parent c96c37e878
commit be5170fc3b
4 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_lra.cpp
View file

@ -384,6 +384,8 @@ class theory_lra::imp {
lp().settings().bound_propagation() = BP_NONE != propagation_mode();
lp().settings().m_enable_hnf = lpar.enable_hnf();
lp().set_track_pivoted_rows(lpar.bprop_on_pivoted_rows());
lp().settings().report_frequency = lpar.rep_freq();
lp().settings().print_statistics = lpar.print_stats();
// todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts
unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;

2
src/util/lp/lp_dual_core_solver_def.h
View file

@ -738,7 +738,7 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::solve() { // s
lp_assert(d_is_correct());
lp_assert(problem_is_dual_feasible());
lp_assert(this->basis_heading_is_correct());
this->set_total_iterations(0);
//this->set_total_iterations(0);
this->iters_with_no_cost_growing() = 0;
do {
if (this->print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over("", *this->m_settings.get_message_ostream())){

2
src/util/lp/lp_primal_core_solver_def.h
View file

@ -643,7 +643,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::backup_an
template <typename T, typename X> void lp_primal_core_solver<T, X>::init_run() {
this->m_basis_sort_counter = 0; // to initiate the sort of the basis
this->set_total_iterations(0);
// this->set_total_iterations(0);
this->iters_with_no_cost_growing() = 0;
init_inf_set();
if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)

2
src/util/lp/lp_primal_core_solver_tableau_def.h
View file

@ -327,7 +327,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::init_run_tab
CASSERT("A_off", this->A_mult_x_is_off() == false);
lp_assert(basis_columns_are_set_correctly());
this->m_basis_sort_counter = 0; // to initiate the sort of the basis
this->set_total_iterations(0);
// this->set_total_iterations(0);
this->iters_with_no_cost_growing() = 0;
lp_assert(this->inf_set_is_correct());
if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)