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

fix add_constraint and substitute_terms_in_linear_expression

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-05-18 10:56:50 -07:00
parent e9d9354885
commit b92f0acae3
3 changed files with 7 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/test/lp/lp.cpp
View file

@ -2705,9 +2705,16 @@ void test_term() {
ls.push_back(std::pair<mpq, var_index>((int)1, z)); ls.push_back(std::pair<mpq, var_index>((int)1, z));
solver.add_constraint(ls, lconstraint_kind::EQ, mpq(0)); solver.add_constraint(ls, lconstraint_kind::EQ, mpq(0));
ls.clear();
ls.push_back(std::pair<mpq, var_index>((int)1, x));
solver.add_constraint(ls, lconstraint_kind::LT, mpq(0));
ls.push_back(std::pair<mpq, var_index>((int)2, y));
solver.add_constraint(ls, lconstraint_kind::GT, mpq(0));
auto status = solver.solve(); auto status = solver.solve();
std::cout << lp_status_to_string(status) << std::endl; std::cout << lp_status_to_string(status) << std::endl;
std::unordered_map<var_index, mpq> model; std::unordered_map<var_index, mpq> model;
if (status != OPTIMAL)
return;
solver.get_model(model); solver.get_model(model);
for (auto & t : model) { for (auto & t : model) {

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

@ -204,24 +204,12 @@ void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_k
} }
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) { 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; vector<std::pair<mpq, var_index>> left_side;
mpq rs = - right_side_parm; mpq rs = - right_side_parm;
std::cout << "before rs = " << rs << std::endl;
substitute_terms_in_linear_expression(left_side_with_terms, left_side, rs); 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>()); unsigned term_index = add_term(left_side, zero_of_type<mpq>());
constraint_index ci = m_constraints.size(); constraint_index ci = m_constraints.size();
add_var_bound_on_constraint_for_term(term_index, kind_par, -rs, ci); 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; return ci;
} }

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

@ -557,9 +557,6 @@ void lar_solver::substitute_terms_in_linear_expression(const vector<std::pair<mp
register_one_coeff_in_map(coeffs, t.first, j); register_one_coeff_in_map(coeffs, t.first, j);
} else { } else {
const lar_term & term = * m_terms[adjust_term_index(t.second)]; const lar_term & term = * m_terms[adjust_term_index(t.second)];
std::cout << "term = ";
print_term(term, std::cout);
std::cout << std::endl;
for (auto & p : term.coeffs()){ for (auto & p : term.coeffs()){
register_one_coeff_in_map(coeffs, t.first * p.second , p.first); register_one_coeff_in_map(coeffs, t.first * p.second , p.first);
} }