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

add_constraint has got a body

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-05-17 19:00:33 -07:00
parent d28b8b33b4
commit e9d9354885
3 changed files with 1359 additions and 1350 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/util/lp/init_lar_solver.cpp
View file

@ -95,7 +95,6 @@ void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) {
var_index lar_solver::add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs,
const mpq &m_v) {
m_terms.push_back(new lar_term(coeffs, m_v));
m_orig_terms.push_back(new lar_term(coeffs, m_v));
return m_terms_start_index + m_terms.size() - 1;
}
@ -106,11 +105,10 @@ var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs,
return add_term_undecided(coeffs, m_v);
m_terms.push_back(new lar_term(coeffs, m_v));
m_orig_terms.push_back(new lar_term(coeffs, m_v));
unsigned adjusted_term_index = m_terms.size() - 1;
var_index ret = m_terms_start_index + adjusted_term_index;
if (use_tableau() && !coeffs.empty()) {
add_row_for_term(m_orig_terms.back(), ret);
add_row_for_term(m_terms.back(), ret);
if (m_settings.bound_propagation())
m_rows_with_changed_bounds.insert(A_r().row_count() - 1);
}
@ -196,15 +194,36 @@ void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_k
auto it = m_ext_vars_to_columns.find(j);
if (it != m_ext_vars_to_columns.end()) {
unsigned term_j = it->second.ext_j();
mpq rs = right_side - m_orig_terms[adjusted_term_index]->m_v;
m_constraints.push_back(new lar_term_constraint(m_orig_terms[adjusted_term_index], kind, right_side));
mpq rs = right_side - m_terms[adjusted_term_index]->m_v;
m_constraints.push_back(new lar_term_constraint(m_terms[adjusted_term_index], kind, right_side));
update_column_type_and_bound(term_j, kind, rs, ci);
}
else {
add_constraint_from_term_and_create_new_column_row(j, m_orig_terms[adjusted_term_index], kind, right_side);
add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side);
}
}
constraint_index lar_solver::add_constraint(const vector<std::pair<mpq, var_index>>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) {
this->print_linear_combination_of_column_indices(left_side_with_terms, std::cout);
std::cout << std::endl;
vector<std::pair<mpq, var_index>> left_side;
mpq rs = - right_side_parm;
std::cout << "before rs = " << rs << std::endl;
substitute_terms_in_linear_expression(left_side_with_terms, left_side, rs);
std::cout << "after rs = " << rs << std::endl;
this->print_linear_combination_of_column_indices(left_side, std::cout);
std::cout << std::endl;
unsigned term_index = add_term(left_side, zero_of_type<mpq>());
constraint_index ci = m_constraints.size();
add_var_bound_on_constraint_for_term(term_index, kind_par, -rs, ci);
std::cout << "constraint = ";
print_constraint(ci, std::cout);
std::cout << std::endl;
return ci;
}
void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term,
lconstraint_kind kind, const mpq & right_side) {

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

@ -43,8 +43,6 @@ const lar_base_constraint& lar_solver::get_constraint(unsigned ci) const {
delete c;
for (auto t : m_terms)
delete t;
for (auto t : m_orig_terms)
delete t;
}
numeric_pair<mpq> const& lar_solver::get_value(var_index vi) const { return m_mpq_lar_core_solver.m_r_x[vi]; }
@ -75,7 +73,7 @@ const lar_base_constraint& lar_solver::get_constraint(unsigned ci) const {
unsigned v = be.m_j;
if (is_term(v)) {
out << "it is a term number " << be.m_j << std::endl;
print_term(*m_orig_terms[be.m_j - m_terms_start_index], out);
print_term(*m_terms[be.m_j - m_terms_start_index], out);
}
else {
out << get_column_name(v);
@ -123,7 +121,7 @@ const lar_base_constraint& lar_solver::get_constraint(unsigned ci) const {
}
rs_of_evidence /= ratio;
} else {
const lar_term * t = m_orig_terms[adjust_term_index(be.m_j)];
const lar_term * t = m_terms[adjust_term_index(be.m_j)];
const auto first_coeff = *t->m_coeffs.begin();
unsigned j = first_coeff.first;
auto it = coeff_map.find(j);
@ -266,8 +264,7 @@ const lar_base_constraint& lar_solver::get_constraint(unsigned ci) const {
// goes over touched rows and tries to induce bounds
void lar_solver::propagate_bounds_for_touched_rows(bound_propagator & bp) {
if (!use_tableau())
return; // ! todo : enable bound propagaion here. The current bug is that after the pop
// the changed terms become incorrect!
return; // todo: consider to remove the restriction
for (unsigned i : m_rows_with_changed_bounds.m_index) {
calculate_implied_bounds_for_row(i, bp);
@ -383,10 +380,8 @@ const lar_base_constraint& lar_solver::get_constraint(unsigned ci) const {
m_term_count.pop(k);
for (unsigned i = m_term_count; i < m_terms.size(); i++) {
delete m_terms[i];
delete m_orig_terms[i];
}
m_terms.resize(m_term_count);
m_orig_terms.resize(m_term_count);
m_simplex_strategy.pop(k);
m_settings.simplex_strategy() = m_simplex_strategy;
lean_assert(sizes_are_correct());
@ -543,20 +538,37 @@ const lar_base_constraint& lar_solver::get_constraint(unsigned ci) const {
m_vars_to_ul_pairs[j] = ul;
}
void lar_solver::register_one_coeff_in_map(std::unordered_map<var_index, mpq> & coeffs, const mpq & a, unsigned j) {
auto it = coeffs.find(j);
if (it == coeffs.end()) {
coeffs[j] = a;
} else {
it->second += a;
}
}
void lar_solver::substitute_terms(const mpq & mult,
const vector<std::pair<mpq, var_index>>& left_side_with_terms,
void lar_solver::substitute_terms_in_linear_expression(const vector<std::pair<mpq, var_index>>& left_side_with_terms,
vector<std::pair<mpq, var_index>> &left_side, mpq & right_side) const {
std::unordered_map<var_index, mpq> coeffs;
for (auto & t : left_side_with_terms) {
if (t.second < m_terms_start_index) {
lean_assert(t.second < A_r().column_count());
left_side.push_back(std::pair<mpq, var_index>(mult * t.first, t.second));
unsigned j = t.second;
if (!is_term(j)) {
register_one_coeff_in_map(coeffs, t.first, j);
} else {
const lar_term & term = * m_terms[adjust_term_index(t.second)];
substitute_terms(mult * t.first, left_side_with_terms, left_side, right_side);
right_side -= mult * term.m_v;
std::cout << "term = ";
print_term(term, std::cout);
std::cout << std::endl;
for (auto & p : term.coeffs()){
register_one_coeff_in_map(coeffs, t.first * p.second , p.first);
}
right_side += t.first * term.m_v;
}
}
for (auto & p : coeffs)
left_side.push_back(std::make_pair(p.second, p.first));
}
@ -878,29 +890,6 @@ const lar_base_constraint& lar_solver::get_constraint(unsigned ci) const {
return true;
}
constraint_index lar_solver::add_constraint(const vector<std::pair<mpq, var_index>>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) {
/*
mpq rs = right_side_parm;
vector<std::pair<mpq, var_index>> left_side;
substitute_terms(one_of_type<mpq>(), left_side_with_terms, left_side, rs);
lean_assert(left_side.size() > 0);
lean_assert(all_constrained_variables_are_registered(left_side));
lar_constraint original_constr(left_side, kind_par, rs);
unsigned j; // j is the index of the basic variables corresponding to the left side
canonic_left_side ls = create_or_fetch_canonic_left_side(left_side, j);
mpq ratio = find_ratio_of_original_constraint_to_normalized(ls, original_constr);
auto kind = ratio.is_neg() ? flip_kind(kind_par) : kind_par;
rs/= ratio;
lar_normalized_constraint normalized_constraint(ls, ratio, kind, rs, original_constr);
m_constraints.push_back(normalized_constraint);
constraint_index constr_ind = m_constraints.size() - 1;
update_column_type_and_bound(j, kind, rs, constr_ind);
return constr_ind;
*/
lean_assert(false); // not implemented
return 0;
}
bool lar_solver::all_constraints_hold() const {
if (m_settings.get_cancel_flag())
return true;

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

@ -60,7 +60,6 @@ class lar_solver : public column_namer {
stacked_value<int> m_infeasible_column_index; // such can be found at the initialization step
stacked_value<unsigned> m_term_count;
vector<lar_term*> m_terms;
vector<lar_term*> m_orig_terms;
const var_index m_terms_start_index;
indexed_vector<mpq> m_column_buffer;
std::function<column_type (unsigned)> m_column_type_function;
@ -255,8 +254,7 @@ public:
void set_low_bound_witness(var_index j, constraint_index ci);
void substitute_terms(const mpq & mult,
const vector<std::pair<mpq, var_index>>& left_side_with_terms,
void substitute_terms_in_linear_expression( const vector<std::pair<mpq, var_index>>& left_side_with_terms,
vector<std::pair<mpq, var_index>> &left_side, mpq & right_side) const;
@ -337,6 +335,9 @@ public:
bool the_relations_are_of_same_type(const vector<std::pair<mpq, unsigned>> & evidence, lconstraint_kind & the_kind_of_sum) const;
static void register_in_map(std::unordered_map<var_index, mpq> & coeffs, const lar_base_constraint & cn, const mpq & a);
static void register_one_coeff_in_map(std::unordered_map<var_index, mpq> & coeffs, const mpq & a, unsigned j);
bool the_left_sides_sum_to_zero(const vector<std::pair<mpq, unsigned>> & evidence) const;
bool the_right_sides_do_not_sum_to_zero(const vector<std::pair<mpq, unsigned>> & evidence);