mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 21:33:39 +00:00
Code Activity

restore some class names by replacing u_set to int_set

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-25 09:36:07 -07:00
parent ab34ef9daf
commit 09467ba677
5 changed files with 38 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/math/lp/lar_constraints.h
View file

@ -96,7 +96,7 @@ public:
}; };
class constrau_set { class constraint_set {
region m_region; region m_region;
column_namer& m_namer; column_namer& m_namer;
vector<lar_base_constraint*> m_constraints; vector<lar_base_constraint*> m_constraints;
@ -139,10 +139,10 @@ class constrau_set {
} }
public: public:
constrau_set(column_namer& cn): constraint_set(column_namer& cn):
m_namer(cn) {} m_namer(cn) {}
~constrau_set() { ~constraint_set() {
for (auto* c : m_constraints) for (auto* c : m_constraints)
c->~lar_base_constraint(); c->~lar_base_constraint();
} }
@ -198,15 +198,15 @@ public:
bool valid_index(constraint_index ci) const { return ci < m_constraints.size(); } bool valid_index(constraint_index ci) const { return ci < m_constraints.size(); }
class active_constraints { class active_constraints {
friend class constrau_set; friend class constraint_set;
constrau_set const& cs; constraint_set const& cs;
public: public:
active_constraints(constrau_set const& cs): cs(cs) {} active_constraints(constraint_set const& cs): cs(cs) {}
class iterator { class iterator {
friend class constrau_set; friend class constraint_set;
constrau_set const& cs; constraint_set const& cs;
unsigned m_index; unsigned m_index;
iterator(constrau_set const& cs, unsigned idx): cs(cs), m_index(idx) { forward(); } iterator(constraint_set const& cs, unsigned idx): cs(cs), m_index(idx) { forward(); }
void next() { ++m_index; forward(); } void next() { ++m_index; forward(); }
void forward() { for (; m_index < cs.m_constraints.size() && !cs.is_active(m_index); m_index++) ; } void forward() { for (; m_index < cs.m_constraints.size() && !cs.is_active(m_index); m_index++) ; }
public: public:
@ -224,15 +224,15 @@ public:
active_constraints active() const { return active_constraints(*this); } active_constraints active() const { return active_constraints(*this); }
class active_indices { class active_indices {
friend class constrau_set; friend class constraint_set;
constrau_set const& cs; constraint_set const& cs;
public: public:
active_indices(constrau_set const& cs): cs(cs) {} active_indices(constraint_set const& cs): cs(cs) {}
class iterator { class iterator {
friend class constrau_set; friend class constraint_set;
constrau_set const& cs; constraint_set const& cs;
unsigned m_index; unsigned m_index;
iterator(constrau_set const& cs, unsigned idx): cs(cs), m_index(idx) { forward(); } iterator(constraint_set const& cs, unsigned idx): cs(cs), m_index(idx) { forward(); }
void next() { ++m_index; forward(); } void next() { ++m_index; forward(); }
void forward() { for (; m_index < cs.m_constraints.size() && !cs.is_active(m_index); m_index++) ; } void forward() { for (; m_index < cs.m_constraints.size() && !cs.is_active(m_index); m_index++) ; }
public: public:
@ -288,7 +288,7 @@ public:
}; };
inline std::ostream& operator<<(std::ostream& out, constrau_set const& cs) { inline std::ostream& operator<<(std::ostream& out, constraint_set const& cs) {
return cs.display(out); return cs.display(out);
} }

4
src/math/lp/lar_solver.h
View file

@ -93,7 +93,7 @@ public:
var_register m_var_register; var_register m_var_register;
var_register m_term_register; var_register m_term_register;
stacked_vector<ul_pair> m_columns_to_ul_pairs; stacked_vector<ul_pair> m_columns_to_ul_pairs;
constrau_set m_constraints; constraint_set m_constraints;
// the set of column indices j such that bounds have changed for j // the set of column indices j such that bounds have changed for j
u_set m_columns_with_changed_bound; u_set m_columns_with_changed_bound;
u_set m_rows_with_changed_bounds; u_set m_rows_with_changed_bounds;
@ -111,7 +111,7 @@ public:
const vector<lar_term*> & terms() const { return m_terms; } const vector<lar_term*> & terms() const { return m_terms; }
lar_term const& term(unsigned i) const { return *m_terms[i]; } lar_term const& term(unsigned i) const { return *m_terms[i]; }
constrau_set const& constraints() const { return m_constraints; } constraint_set const& constraints() const { return m_constraints; }
void set_int_solver(int_solver * int_slv) { m_int_solver = int_slv; } void set_int_solver(int_solver * int_slv) { m_int_solver = int_slv; }
int_solver * get_int_solver() { return m_int_solver; } int_solver * get_int_solver() { return m_int_solver; }

8
src/math/lp/lp_dual_core_solver.h
View file

@ -39,7 +39,7 @@ public:
T m_theta_P; T m_theta_P;
int m_q; int m_q;
// todo : replace by a vector later // todo : replace by a vector later
std::set<unsigned> m_breakpou_set; // it is F in "Progress in the dual simplex method ..." std::set<unsigned> m_breakpoint_set; // it is F in "Progress in the dual simplex method ..."
std::set<unsigned> m_flipped_boxed; std::set<unsigned> m_flipped_boxed;
std::set<unsigned> m_tight_set; // it is the set of all breakpoints that become tight when m_q becomes tight std::set<unsigned> m_tight_set; // it is the set of all breakpoints that become tight when m_q becomes tight
vector<T> m_a_wave; vector<T> m_a_wave;
@ -124,7 +124,7 @@ public:
bool can_be_breakpoint(unsigned j); bool can_be_breakpoint(unsigned j);
void fill_breakpou_set(); void fill_breakpoint_set();
void DSE_FTran(); void DSE_FTran();
T get_delta(); T get_delta();
@ -183,7 +183,7 @@ public:
bool tight_breakpoinst_are_all_boxed(); bool tight_breakpoinst_are_all_boxed();
T calculate_harris_delta_on_breakpou_set(); T calculate_harris_delta_on_breakpoint_set();
void fill_tight_set_on_harris_delta(const T & harris_delta ); void fill_tight_set_on_harris_delta(const T & harris_delta );
@ -191,7 +191,7 @@ public:
void find_q_and_tight_set(); void find_q_and_tight_set();
void erase_tight_breakpoints_and_q_from_breakpou_set(); void erase_tight_breakpoints_and_q_from_breakpoint_set();
bool ratio_test(); bool ratio_test();

30
src/math/lp/lp_dual_core_solver_def.h
View file

@ -285,11 +285,11 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::can_be_breakpo
} }
} }
template <typename T, typename X> void lp_dual_core_solver<T, X>::fill_breakpou_set() { template <typename T, typename X> void lp_dual_core_solver<T, X>::fill_breakpoint_set() {
m_breakpou_set.clear(); m_breakpoint_set.clear();
for (unsigned j : this->non_basis()) { for (unsigned j : this->non_basis()) {
if (can_be_breakpoint(j)) { if (can_be_breakpoint(j)) {
m_breakpou_set.insert(j); m_breakpoint_set.insert(j);
} }
} }
} }
@ -590,11 +590,11 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::tight_breakpoi
return true; return true;
} }
template <typename T, typename X> T lp_dual_core_solver<T, X>::calculate_harris_delta_on_breakpou_set() { template <typename T, typename X> T lp_dual_core_solver<T, X>::calculate_harris_delta_on_breakpoint_set() {
bool first_time = true; bool first_time = true;
T ret = zero_of_type<T>(); T ret = zero_of_type<T>();
lp_assert(m_breakpou_set.size() > 0); lp_assert(m_breakpoint_set.size() > 0);
for (auto j : m_breakpou_set) { for (auto j : m_breakpoint_set) {
T t; T t;
if (this->x_is_at_lower_bound(j)) { if (this->x_is_at_lower_bound(j)) {
t = abs((std::max(this->m_d[j], numeric_traits<T>::zero()) + m_harris_tolerance) / this->m_pivot_row[j]); t = abs((std::max(this->m_d[j], numeric_traits<T>::zero()) + m_harris_tolerance) / this->m_pivot_row[j]);
@ -613,7 +613,7 @@ template <typename T, typename X> T lp_dual_core_solver<T, X>::calculate_harris_
template <typename T, typename X> void lp_dual_core_solver<T, X>::fill_tight_set_on_harris_delta(const T & harris_delta ){ template <typename T, typename X> void lp_dual_core_solver<T, X>::fill_tight_set_on_harris_delta(const T & harris_delta ){
m_tight_set.clear(); m_tight_set.clear();
for (auto j : m_breakpou_set) { for (auto j : m_breakpoint_set) {
if (this->x_is_at_lower_bound(j)) { if (this->x_is_at_lower_bound(j)) {
if (abs(std::max(this->m_d[j], numeric_traits<T>::zero()) / this->m_pivot_row[j]) <= harris_delta){ if (abs(std::max(this->m_d[j], numeric_traits<T>::zero()) / this->m_pivot_row[j]) <= harris_delta){
m_tight_set.insert(j); m_tight_set.insert(j);
@ -646,26 +646,26 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::find_q_on_tigh
} }
template <typename T, typename X> void lp_dual_core_solver<T, X>::find_q_and_tight_set() { template <typename T, typename X> void lp_dual_core_solver<T, X>::find_q_and_tight_set() {
T harris_del = calculate_harris_delta_on_breakpou_set(); T harris_del = calculate_harris_delta_on_breakpoint_set();
fill_tight_set_on_harris_delta(harris_del); fill_tight_set_on_harris_delta(harris_del);
find_q_on_tight_set(); find_q_on_tight_set();
m_entering_boundary_position = this->get_non_basic_column_value_position(m_q); m_entering_boundary_position = this->get_non_basic_column_value_position(m_q);
} }
template <typename T, typename X> void lp_dual_core_solver<T, X>::erase_tight_breakpoints_and_q_from_breakpou_set() { template <typename T, typename X> void lp_dual_core_solver<T, X>::erase_tight_breakpoints_and_q_from_breakpoint_set() {
m_breakpou_set.erase(m_q); m_breakpoint_set.erase(m_q);
for (auto j : m_tight_set) { for (auto j : m_tight_set) {
m_breakpou_set.erase(j); m_breakpoint_set.erase(j);
} }
} }
template <typename T, typename X> bool lp_dual_core_solver<T, X>::ratio_test() { template <typename T, typename X> bool lp_dual_core_solver<T, X>::ratio_test() {
m_sign_of_alpha_r = define_sign_of_alpha_r(); m_sign_of_alpha_r = define_sign_of_alpha_r();
fill_breakpou_set(); fill_breakpoint_set();
m_flipped_boxed.clear(); m_flipped_boxed.clear();
int initial_delta_sign = m_delta >= numeric_traits<T>::zero()? 1: -1; int initial_delta_sign = m_delta >= numeric_traits<T>::zero()? 1: -1;
do { do {
if (m_breakpou_set.empty()) { if (m_breakpoint_set.empty()) {
set_status_to_tentative_dual_unbounded_or_dual_unbounded(); set_status_to_tentative_dual_unbounded_or_dual_unbounded();
return false; return false;
} }
@ -674,13 +674,13 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::ratio_test() {
if (!tight_breakpoinst_are_all_boxed()) break; if (!tight_breakpoinst_are_all_boxed()) break;
T del = m_delta - delta_lost_on_flips_of_tight_breakpoints() * initial_delta_sign; T del = m_delta - delta_lost_on_flips_of_tight_breakpoints() * initial_delta_sign;
if (!delta_keeps_the_sign(initial_delta_sign, del)) break; if (!delta_keeps_the_sign(initial_delta_sign, del)) break;
if (m_tight_set.size() + 1 == m_breakpou_set.size()) { if (m_tight_set.size() + 1 == m_breakpoint_set.size()) {
break; // deciding not to flip since we might get stuck without finding m_q, the column entering the basis break; // deciding not to flip since we might get stuck without finding m_q, the column entering the basis
} }
// we can flip m_q together with the tight set and look for another breakpoint candidate for m_q and another tight set // we can flip m_q together with the tight set and look for another breakpoint candidate for m_q and another tight set
add_tight_breakpoints_and_q_to_flipped_set(); add_tight_breakpoints_and_q_to_flipped_set();
m_delta = del; m_delta = del;
erase_tight_breakpoints_and_q_from_breakpou_set(); erase_tight_breakpoints_and_q_from_breakpoint_set();
} while (true); } while (true);
m_theta_D = this->m_d[m_q] / this->m_pivot_row[m_q]; m_theta_D = this->m_d[m_q] / this->m_pivot_row[m_q];
return true; return true;

2
src/math/lp/u_set.h
View file

@ -15,7 +15,7 @@ Author:
Revision History: Revision History:
TBD use indexed_uu_set from src/util/uu_set.h, TBD use indexed_uint_set from src/util/uu_set.h,
--*/ --*/
#pragma once #pragma once