mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

unused methods

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-23 19:28:07 -07:00
parent 5d36578684
commit 7f3bdea0d5
2 changed files with 45 additions and 200 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,21 +1,9 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Lev Nachmanson (levnach)
Revision History:
--*/
#pragma once
#include "util/vector.h"
@ -51,9 +39,9 @@ public:
stacked_vector<numeric_pair<mpq>> m_r_upper_bounds;
static_matrix<mpq, numeric_pair<mpq>> m_r_A;
stacked_vector<unsigned> m_r_pushed_basis;
vector<unsigned> m_r_basis;
vector<unsigned> m_r_nbasis;
vector<int> m_r_heading;
vector<unsigned> m_r_basis;
vector<unsigned> m_r_nbasis;
vector<int> m_r_heading;
stacked_vector<unsigned> m_r_columns_nz;
stacked_vector<unsigned> m_r_rows_nz;
@ -91,13 +79,6 @@ public:
column_type get_column_type(unsigned j) { return m_column_types[j];}
void init_costs(bool first_time);
void init_cost_for_column(unsigned j);
// returns m_sign_of_alpha_r
int column_is_out_of_bounds(unsigned j);
void calculate_pivot_row(unsigned i);
void print_pivot_row(std::ostream & out, unsigned row_index) const {
@ -112,8 +93,7 @@ public:
for (unsigned j : m_r_solver.m_pivot_row.m_index) {
m_r_solver.print_column_bound_info(j, out);
}
m_r_solver.print_column_bound_info(m_r_solver.m_basis[row_index], out);
m_r_solver.print_column_bound_info(m_r_solver.m_basis[row_index], out);
}
@ -131,28 +111,20 @@ public:
void prefix_d();
unsigned m_m() const {
return m_r_A.row_count();
}
unsigned m_m() const { return m_r_A.row_count(); }
unsigned m_n() const {
return m_r_A.column_count();
}
unsigned m_n() const { return m_r_A.column_count(); }
bool is_tiny() const { return this->m_m() < 10 && this->m_n() < 20; }
bool is_empty() const { return this->m_m() == 0 && this->m_n() == 0; }
template <typename L>
int get_sign(const L & v) {
return v > zero_of_type<L>() ? 1 : (v < zero_of_type<L>() ? -1 : 0);
}
int get_sign(const L & v) { return v > zero_of_type<L>() ? 1 : (v < zero_of_type<L>() ? -1 : 0); }
void fill_evidence(unsigned row);
unsigned get_number_of_non_ints() const;
unsigned get_number_of_non_ints() const;
void solve();

201
src/math/lp/lar_core_solver_def.h
View file

@ -1,33 +1,6 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Lev Nachmanson (levnach)
Revision History:
--*/
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Lev Nachmanson (levnach)
@ -42,137 +15,36 @@ Revision History:
#include "math/lp/lar_solution_signature.h"
namespace lp {
lar_core_solver::lar_core_solver(
lp_settings & settings,
const column_namer & column_names
):
lp_settings & settings,
const column_namer & column_names):
m_infeasible_sum_sign(0),
m_r_solver(m_r_A,
m_right_sides_dummy,
m_r_x,
m_r_basis,
m_r_nbasis,
m_r_heading,
m_costs_dummy,
m_column_types(),
m_r_lower_bounds(),
m_r_upper_bounds(),
settings,
m_right_sides_dummy,
m_r_x,
m_r_basis,
m_r_nbasis,
m_r_heading,
m_costs_dummy,
m_column_types(),
m_r_lower_bounds(),
m_r_upper_bounds(),
settings,
column_names),
m_d_solver(m_d_A,
m_d_right_sides_dummy,
m_d_x,
m_d_basis,
m_d_nbasis,
m_d_heading,
m_d_costs_dummy,
m_column_types(),
m_d_lower_bounds,
m_d_upper_bounds,
settings,
column_names){}
void lar_core_solver::init_costs(bool first_time) {
lp_assert(false); // should not be called
// lp_assert(this->m_x.size() >= this->m_n());
// lp_assert(this->m_column_types.size() >= this->m_n());
// if (first_time)
// this->m_costs.resize(this->m_n());
// X inf = this->m_infeasibility;
// this->m_infeasibility = zero_of_type<X>();
// for (unsigned j = this->m_n(); j--;)
// init_cost_for_column(j);
// if (!(first_time || inf >= this->m_infeasibility)) {
// LP_OUT(this->m_settings, "iter = " << this->total_iterations() << std::endl);
// LP_OUT(this->m_settings, "inf was " << T_to_string(inf) << " and now " << T_to_string(this->m_infeasibility) << std::endl);
// lp_assert(false);
// }
// if (inf == this->m_infeasibility)
// this->m_iters_with_no_cost_growing++;
}
void lar_core_solver::init_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
const numeric_pair<mpq> & x = this->m_x[j];
// set zero cost for each non-basis column
if (this->m_basis_heading[j] < 0) {
this->m_costs[j] = numeric_traits<T>::zero();
return;
}
// j is a basis column
switch (this->m_column_types[j]) {
case fixed:
case column_type::boxed:
if (x > this->m_upper_bounds[j]) {
this->m_costs[j] = 1;
this->m_infeasibility += x - this->m_upper_bounds[j];
} else if (x < this->m_lower_bounds[j]) {
this->m_infeasibility += this->m_lower_bounds[j] - x;
this->m_costs[j] = -1;
} else {
this->m_costs[j] = numeric_traits<T>::zero();
}
break;
case lower_bound:
if (x < this->m_lower_bounds[j]) {
this->m_costs[j] = -1;
this->m_infeasibility += this->m_lower_bounds[j] - x;
} else {
this->m_costs[j] = numeric_traits<T>::zero();
}
break;
case upper_bound:
if (x > this->m_upper_bounds[j]) {
this->m_costs[j] = 1;
this->m_infeasibility += x - this->m_upper_bounds[j];
} else {
this->m_costs[j] = numeric_traits<T>::zero();
}
break;
case free_column:
this->m_costs[j] = numeric_traits<T>::zero();
break;
default:
lp_assert(false);
break;
}*/
}
// returns m_sign_of_alpha_r
int lar_core_solver::column_is_out_of_bounds(unsigned j) {
/*
switch (this->m_column_type[j]) {
case fixed:
case column_type::boxed:
if (this->x_below_low_bound(j)) {
return -1;
}
if (this->x_above_upper_bound(j)) {
return 1;
}
return 0;
case lower_bound:
if (this->x_below_low_bound(j)) {
return -1;
}
return 0;
case upper_bound:
if (this->x_above_upper_bound(j)) {
return 1;
}
return 0;
default:
return 0;
break;
}*/
lp_assert(false);
return true;
}
m_d_right_sides_dummy,
m_d_x,
m_d_basis,
m_d_nbasis,
m_d_heading,
m_d_costs_dummy,
m_column_types(),
m_d_lower_bounds,
m_d_upper_bounds,
settings,
column_names) {
}
void lar_core_solver::calculate_pivot_row(unsigned i) {
m_r_solver.calculate_pivot_row(i);
@ -180,8 +52,8 @@ void lar_core_solver::calculate_pivot_row(unsigned i) {
void lar_core_solver::prefix_r() {
if (!m_r_solver.m_settings.use_tableau()) {
void lar_core_solver::prefix_r() {
if (!m_r_solver.m_settings.use_tableau()) {
m_r_solver.m_copy_of_xB.resize(m_r_solver.m_n());
m_r_solver.m_ed.resize(m_r_solver.m_m());
m_r_solver.m_pivot_row.resize(m_r_solver.m_n());
@ -203,7 +75,7 @@ void lar_core_solver::calculate_pivot_row(unsigned i) {
}
}
void lar_core_solver::prefix_d() {
void lar_core_solver::prefix_d() {
m_d_solver.m_b.resize(m_d_solver.m_m());
m_d_solver.m_breakpoint_indices_queue.resize(m_d_solver.m_n());
m_d_solver.m_copy_of_xB.resize(m_d_solver.m_n());
@ -256,12 +128,12 @@ void lar_core_solver::fill_not_improvable_zero_sum() {
}
unsigned lar_core_solver::get_number_of_non_ints() const {
unsigned n = 0;
for (auto & x : m_r_solver.m_x) {
if (x.is_int() == false)
n++;
}
return n;
unsigned n = 0;
for (auto & x : m_r_solver.m_x) {
if (x.is_int() == false)
n++;
}
return n;
}
void lar_core_solver::solve() {
@ -309,7 +181,8 @@ void lar_core_solver::solve() {
}
if (m_r_solver.get_status() == lp_status::INFEASIBLE) {
fill_not_improvable_zero_sum();
} else if (m_r_solver.get_status() != lp_status::UNBOUNDED) {
}
else if (m_r_solver.get_status() != lp_status::UNBOUNDED) {
m_r_solver.set_status(lp_status::OPTIMAL);
}
lp_assert(r_basis_is_OK());