mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix in hnf for the lower bounds

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-07-11 12:29:09 -07:00
parent 2dfb8f53b6
commit e0e893b791
5 changed files with 21 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/util/lp/general_matrix.h
View file

@ -105,12 +105,12 @@ public:
} }
template <typename T> template <typename T>
void init_row_from_container(int i, const T & c, std::function<unsigned (unsigned)> column_fix) { void init_row_from_container(int i, const T & c, std::function<unsigned (unsigned)> column_fix, const mpq& sign) {
auto & row = m_data[adjust_row(i)]; auto & row = m_data[adjust_row(i)];
lp_assert(row_is_initialized_correctly(row)); lp_assert(row_is_initialized_correctly(row));
for (const auto & p : c) { for (const auto & p : c) {
unsigned j = adjust_column(column_fix(p.var())); unsigned j = adjust_column(column_fix(p.var()));
row[j] = p.coeff(); row[j] = sign * p.coeff();
} }
} }

15
src/util/lp/hnf_cutter.h
View file

@ -29,6 +29,7 @@ class hnf_cutter {
var_register m_var_register; var_register m_var_register;
general_matrix m_A; general_matrix m_A;
vector<const lar_term*> m_terms; vector<const lar_term*> m_terms;
vector<bool> m_terms_upper;
svector<constraint_index> m_constraints_for_explanation; svector<constraint_index> m_constraints_for_explanation;
vector<mpq> m_right_sides; vector<mpq> m_right_sides;
lp_settings & m_settings; lp_settings & m_settings;
@ -54,15 +55,22 @@ public:
// m_A will be filled from scratch in init_matrix_A // m_A will be filled from scratch in init_matrix_A
m_var_register.clear(); m_var_register.clear();
m_terms.clear(); m_terms.clear();
m_terms_upper.clear();
m_constraints_for_explanation.clear(); m_constraints_for_explanation.clear();
m_right_sides.clear(); m_right_sides.clear();
m_abs_max = zero_of_type<mpq>(); m_abs_max = zero_of_type<mpq>();
m_overflow = false; m_overflow = false;
} }
void add_term(const lar_term* t, const mpq &rs, constraint_index ci) { void add_term(const lar_term* t, const mpq &rs, constraint_index ci, bool upper_bound) {
m_terms.push_back(t); m_terms.push_back(t);
m_right_sides.push_back(rs); m_terms_upper.push_back(upper_bound);
if (upper_bound)
m_right_sides.push_back(rs);
else
m_right_sides.push_back(-rs);
m_constraints_for_explanation.push_back(ci); m_constraints_for_explanation.push_back(ci);
for (const auto &p : *t) { for (const auto &p : *t) {
m_var_register.add_var(p.var()); m_var_register.add_var(p.var());
mpq t = abs(ceil(p.coeff())); mpq t = abs(ceil(p.coeff()));
@ -76,7 +84,8 @@ public:
} }
void initialize_row(unsigned i) { void initialize_row(unsigned i) {
m_A.init_row_from_container(i, * m_terms[i], [this](unsigned j) { return m_var_register.add_var(j);}); mpq sign = m_terms_upper[i]? one_of_type<mpq>(): - one_of_type<mpq>();
m_A.init_row_from_container(i, * m_terms[i], [this](unsigned j) { return m_var_register.add_var(j);}, sign);
} }
void init_matrix_A() { void init_matrix_A() {

5
src/util/lp/int_solver.cpp
View file

@ -537,8 +537,9 @@ void int_solver::try_add_term_to_A_for_hnf(unsigned i) {
mpq rs; mpq rs;
const lar_term* t = m_lar_solver->terms()[i]; const lar_term* t = m_lar_solver->terms()[i];
constraint_index ci; constraint_index ci;
if (!hnf_cutter_is_full() && m_lar_solver->get_equality_and_right_side_for_term_on_current_x(i, rs, ci)) { bool upper_bound;
m_hnf_cutter.add_term(t, rs, ci); if (!hnf_cutter_is_full() && m_lar_solver->get_equality_and_right_side_for_term_on_current_x(i, rs, ci, upper_bound)) {
m_hnf_cutter.add_term(t, rs, ci, upper_bound);
} }
} }

4
src/util/lp/lar_solver.cpp
View file

@ -2239,7 +2239,7 @@ bool lar_solver::sum_first_coords(const lar_term& t, mpq & val) const {
return true; return true;
} }
bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term_index, mpq & rs, constraint_index& ci) const { bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term_index, mpq & rs, constraint_index& ci, bool &upper_bound) const {
unsigned tj = term_index + m_terms_start_index; unsigned tj = term_index + m_terms_start_index;
unsigned j; unsigned j;
bool is_int; bool is_int;
@ -2257,6 +2257,7 @@ bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term
return false; return false;
rs_is_calculated = true; rs_is_calculated = true;
if (rs == b) { if (rs == b) {
upper_bound = true;
return true; return true;
} }
} }
@ -2268,6 +2269,7 @@ bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term
lp_assert(b.is_int()); lp_assert(b.is_int());
if (rs == b) { if (rs == b) {
upper_bound = false;
return true; return true;
} }
} }

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

@ -573,7 +573,7 @@ public:
unsigned column_count() const { return A_r().column_count(); } unsigned column_count() const { return A_r().column_count(); }
const vector<unsigned> & r_basis() const { return m_mpq_lar_core_solver.r_basis(); } const vector<unsigned> & r_basis() const { return m_mpq_lar_core_solver.r_basis(); }
const vector<unsigned> & r_nbasis() const { return m_mpq_lar_core_solver.r_nbasis(); } const vector<unsigned> & r_nbasis() const { return m_mpq_lar_core_solver.r_nbasis(); }
bool get_equality_and_right_side_for_term_on_current_x(unsigned i, mpq &rs, constraint_index& ci) const; bool get_equality_and_right_side_for_term_on_current_x(unsigned i, mpq &rs, constraint_index& ci, bool &upper_bound) const;
bool remove_from_basis(unsigned); bool remove_from_basis(unsigned);
lar_term get_term_to_maximize(unsigned ext_j) const; lar_term get_term_to_maximize(unsigned ext_j) const;
void set_cut_strategy(unsigned cut_frequency); void set_cut_strategy(unsigned cut_frequency);