mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity

rm breakpoints

Browse source
This commit is contained in:
Lev Nachmanson 2023-03-06 09:59:32 -08:00
parent 73224adc48
commit 6201eda055
4 changed files with 1 additions and 267 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/math/lp/breakpoint.h
View file

@ -1,35 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Lev Nachmanson (levnach)
Revision History:
--*/
#pragma once
namespace lp {
enum breakpoint_type {
low_break, upper_break, fixed_break
};
template <typename X>
struct breakpoint {
unsigned m_j; // the basic column
breakpoint_type m_type;
X m_delta;
breakpoint(){}
breakpoint(unsigned j, X delta, breakpoint_type type):m_j(j), m_type(type), m_delta(delta) {}
};
}

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

@ -13,7 +13,6 @@ Author:
#include <algorithm>
#include "math/lp/indexed_vector.h"
#include "math/lp/binary_heap_priority_queue.h"
#include "math/lp/breakpoint.h"
#include "math/lp/lp_primal_core_solver.h"
#include "math/lp/stacked_vector.h"
#include "math/lp/lar_solution_signature.h"
@ -96,11 +95,6 @@ public:
m_r_solver.print_column_bound_info(m_r_solver.m_basis[row_index], out);
}
void advance_on_sorted_breakpoints(unsigned entering);
void change_slope_on_breakpoint(unsigned entering, breakpoint<numeric_pair<mpq>> * b, mpq & slope_at_entering);
bool row_is_infeasible(unsigned row);
bool row_is_evidence(unsigned row);

66
src/math/lp/lp_primal_core_solver.h
View file

@ -32,7 +32,6 @@ Revision History:
#include "math/lp/static_matrix.h"
#include "math/lp/core_solver_pretty_printer.h"
#include "math/lp/lp_core_solver_base.h"
#include "math/lp/breakpoint.h"
#include "math/lp/binary_heap_priority_queue.h"
#include "math/lp/u_set.h"
namespace lp {
@ -64,47 +63,7 @@ public:
int choose_entering_column(unsigned number_of_benefitial_columns_to_go_over);
int choose_entering_column_tableau();
int choose_entering_column_presize(unsigned number_of_benefitial_columns_to_go_over);
int find_leaving_and_t_with_breakpoints(unsigned entering, X & t);
// int find_inf_row() {
// // mimicing CLP : todo : use a heap
// int j = -1;
// for (unsigned k : this->m_inf_set.m_index) {
// if (k < static_cast<unsigned>(j))
// j = static_cast<int>(k);
// }
// if (j == -1)
// return -1;
// return this->m_basis_heading[j];
// #if 0
// vector<int> choices;
// unsigned len = 100000000;
// for (unsigned j : this->m_inf_set.m_index) {
// int i = this->m_basis_heading[j];
// lp_assert(i >= 0);
// unsigned row_len = this->m_A.m_rows[i].size();
// if (row_len < len) {
// choices.clear();
// choices.push_back(i);
// len = row_len;
// if (m_settings.random_next() % 10) break;
// } else if (row_len == len) {
// choices.push_back(i);
// if (m_settings.random_next() % 10) break;
// }
// }
// if (choices.size() == 0)
// return -1;
// if (choices.size() == 1)
// return choices[0];
// unsigned k = this->m_settings.random_next() % choices.size();
// return choices[k];
// #endif
// }
bool column_is_benefitial_for_entering_basis_on_sign_row_strategy(unsigned j, int sign) const {
// sign = 1 means the x of the basis column of the row has to grow to become feasible, when the coeff before j is neg, or x - has to diminish when the coeff is pos
// we have xbj = -aj * xj
@ -538,16 +497,7 @@ public:
if (this->current_x_is_feasible())
this->set_status(lp_status::OPTIMAL);
}
void fill_breakpoints_array(unsigned entering);
void try_add_breakpoint_in_row(unsigned i);
void change_slope_on_breakpoint(unsigned entering, breakpoint<X> * b, T & slope_at_entering);
void decide_on_status_when_cannot_find_entering() {
lp_assert(!need_to_switch_costs());
this->set_status(this->current_x_is_feasible()? lp_status::OPTIMAL: lp_status::INFEASIBLE);
@ -772,10 +722,6 @@ public:
bool column_is_benefitial_for_entering_basis(unsigned j) const;
bool column_is_benefitial_for_entering_basis_precise(unsigned j) const;
bool column_is_benefitial_for_entering_on_breakpoints(unsigned j) const;
bool can_enter_basis(unsigned j);
bool done();
void init_infeasibility_costs();
@ -785,26 +731,16 @@ public:
void init_infeasibility_costs_for_changed_basis_only();
void print_column(unsigned j, std::ostream & out);
void add_breakpoint(unsigned j, X delta, breakpoint_type type);
// j is the basic column, x is the value at x[j]
// d is the coefficient before m_entering in the row with j as the basis column
void try_add_breakpoint(unsigned j, const X & x, const T & d, breakpoint_type break_type, const X & break_value);
template <typename L>
bool same_sign_with_entering_delta(const L & a) {
return (a > zero_of_type<L>() && m_sign_of_entering_delta > 0) || (a < zero_of_type<L>() && m_sign_of_entering_delta < 0);
}
bool lower_bounds_are_set() const override { return true; }
int advance_on_sorted_breakpoints(unsigned entering, X & t);
std::string break_type_to_string(breakpoint_type type);
void print_breakpoint(const breakpoint<X> * b, std::ostream & out);
void print_bound_info_and_x(unsigned j, std::ostream & out);
void init_infeasibility_after_update_x_if_inf(unsigned leaving) {

161
src/math/lp/lp_primal_core_solver_def.h
View file

@ -75,39 +75,6 @@ void lp_primal_core_solver<T, X>::sort_non_basis() {
}
}
template <typename T, typename X>
bool lp_primal_core_solver<T, X>::column_is_benefitial_for_entering_on_breakpoints(unsigned j) const {
bool ret;
const T & d = this->m_d[j];
switch (this->m_column_types[j]) {
case column_type::lower_bound:
lp_assert(this->x_is_at_lower_bound(j));
ret = d < -m_epsilon_of_reduced_cost;
break;
case column_type::upper_bound:
lp_assert(this->x_is_at_upper_bound(j));
ret = d > m_epsilon_of_reduced_cost;
break;
case column_type::fixed:
ret = false;
break;
case column_type::boxed:
{
bool lower_bound = this->x_is_at_lower_bound(j);
lp_assert(lower_bound || this->x_is_at_upper_bound(j));
ret = (lower_bound && d < -m_epsilon_of_reduced_cost) || ((!lower_bound) && d > m_epsilon_of_reduced_cost);
}
break;
case column_type::free_column:
ret = d > m_epsilon_of_reduced_cost || d < - m_epsilon_of_reduced_cost;
break;
default:
lp_unreachable();
ret = false;
break;
}
return ret;
}
template <typename T, typename X>
bool lp_primal_core_solver<T, X>::column_is_benefitial_for_entering_basis(unsigned j) const {
if (numeric_traits<T>::precise())
@ -261,14 +228,6 @@ int lp_primal_core_solver<T, X>::choose_entering_column(unsigned number_of_benef
}
template <typename T, typename X> int
lp_primal_core_solver<T, X>::find_leaving_and_t_with_breakpoints(unsigned entering, X & t){
lp_assert(this->precise() == false);
fill_breakpoints_array(entering);
return advance_on_sorted_breakpoints(entering, t);
}
template <typename T, typename X> bool lp_primal_core_solver<T, X>::get_harris_theta(X & theta) {
lp_assert(this->m_ed.is_OK());
bool unlimited = true;
@ -799,19 +758,6 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::one_iteratio
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::fill_breakpoints_array(unsigned entering) {
for (unsigned i : this->m_ed.m_index)
try_add_breakpoint_in_row(i);
if (this->m_column_types[entering] == column_type::boxed) {
if (m_sign_of_entering_delta < 0)
add_breakpoint(entering, - this->bound_span(entering), low_break);
else
add_breakpoint(entering, this->bound_span(entering), upper_break);
}
}
template <typename T, typename X> bool lp_primal_core_solver<T, X>::done() {
if (this->get_status() == lp_status::OPTIMAL) return true;
@ -893,9 +839,6 @@ lp_primal_core_solver<T, X>::get_infeasibility_cost_for_column(unsigned j) const
template <typename T, typename X> void
lp_primal_core_solver<T, X>::init_infeasibility_cost_for_column(unsigned j) {
// If j is a breakpoint column, then we set the cost zero.
// When anylyzing an entering column candidate we update the cost of the breakpoints columns to get the left or the right derivative if the infeasibility function
// set zero cost for each non-basis column
if (this->m_basis_heading[j] < 0) {
this->m_costs[j] = numeric_traits<T>::zero();
this->remove_column_from_inf_set(j);
@ -966,110 +909,6 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::print_column
}
}
// j is the basic column, x is the value at x[j]
// d is the coefficient before m_entering in the row with j as the basis column
template <typename T, typename X> void lp_primal_core_solver<T, X>::try_add_breakpoint(unsigned j, const X & x, const T & d, breakpoint_type break_type, const X & break_value) {
X diff = x - break_value;
if (is_zero(diff)) {
switch (break_type) {
case low_break:
if (!same_sign_with_entering_delta(d))
return; // no breakpoint
break;
case upper_break:
if (same_sign_with_entering_delta(d))
return; // no breakpoint
break;
default: break;
}
add_breakpoint(j, zero_of_type<X>(), break_type);
return;
}
auto delta_j = diff / d;
if (same_sign_with_entering_delta(delta_j))
add_breakpoint(j, delta_j, break_type);
}
template <typename T, typename X> std::string lp_primal_core_solver<T, X>::break_type_to_string(breakpoint_type type) {
switch (type){
case low_break: return "low_break";
case upper_break: return "upper_break";
case fixed_break: return "fixed_break";
default:
lp_assert(false);
break;
}
return "type is not found";
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::print_breakpoint(const breakpoint<X> * b, std::ostream & out) {
out << "(" << this->column_name(b->m_j) << "," << break_type_to_string(b->m_type) << "," << T_to_string(b->m_delta) << ")" << std::endl;
print_bound_info_and_x(b->m_j, out);
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::change_slope_on_breakpoint(unsigned entering, breakpoint<X> * b, T & slope_at_entering) {
if (b->m_j == entering) {
lp_assert(b->m_type != fixed_break && (!is_zero(b->m_delta)));
slope_at_entering += m_sign_of_entering_delta;
return;
}
lp_assert(this->m_basis_heading[b->m_j] >= 0);
unsigned i_row = this->m_basis_heading[b->m_j];
const T & d = - this->m_ed[i_row];
if (numeric_traits<T>::is_zero(d)) return;
T delta = m_sign_of_entering_delta * abs(d);
switch (b->m_type) {
case fixed_break:
if (is_zero(b->m_delta)) {
slope_at_entering += delta;
} else {
slope_at_entering += 2 * delta;
}
break;
case low_break:
case upper_break:
slope_at_entering += delta;
break;
default:
lp_assert(false);
}
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::try_add_breakpoint_in_row(unsigned i) {
lp_assert(i < this->m_m());
const T & d = this->m_ed[i]; // the coefficient before m_entering in the i-th row
if (d == 0) return; // the change of x[m_entering] will not change the corresponding basis x
unsigned j = this->m_basis[i];
const X & x = this->m_x[j];
switch (this->m_column_types[j]) {
case column_type::fixed:
try_add_breakpoint(j, x, d, fixed_break, this->m_lower_bounds[j]);
break;
case column_type::boxed:
try_add_breakpoint(j, x, d, low_break, this->m_lower_bounds[j]);
try_add_breakpoint(j, x, d, upper_break, this->m_upper_bounds[j]);
break;
case column_type::lower_bound:
try_add_breakpoint(j, x, d, low_break, this->m_lower_bounds[j]);
break;
case column_type::upper_bound:
try_add_breakpoint(j, x, d, upper_break, this->m_upper_bounds[j]);
break;
case column_type::free_column:
break;
default:
lp_assert(false);
break;
}
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::print_bound_info_and_x(unsigned j, std::ostream & out) {
out << "type of " << this->column_name(j) << " is " << column_type_to_string(this->m_column_types[j]) << std::endl;
out << "x[" << this->column_name(j) << "] = " << this->m_x[j] << std::endl;