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

rebase

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-09-14 11:52:14 -07:00
parent e705e5a309
commit 5dee39721a
5 changed files with 17 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -17,10 +17,6 @@ const impq & bound_propagator::get_upper_bound(unsigned j) const {
} }
void bound_propagator::try_add_bound(mpq v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { void bound_propagator::try_add_bound(mpq v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) {
j = m_lar_solver.adjust_column_index_to_term_index(j); j = m_lar_solver.adjust_column_index_to_term_index(j);
if (m_lar_solver.is_term(j)) {
// lp treats terms as not having a free coefficient, restoring it below for the outside consumption
v += m_lar_solver.get_term(j).m_v;
}
lconstraint_kind kind = is_low? GE : LE; lconstraint_kind kind = is_low? GE : LE;
if (strict) if (strict)

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

@ -75,7 +75,7 @@ struct lar_term_constraint: public lar_base_constraint {
} }
unsigned size() const override { return m_term->size();} unsigned size() const override { return m_term->size();}
lar_term_constraint(const lar_term *t, lconstraint_kind kind, const mpq& right_side) : lar_base_constraint(kind, right_side), m_term(t) { } lar_term_constraint(const lar_term *t, lconstraint_kind kind, const mpq& right_side) : lar_base_constraint(kind, right_side), m_term(t) { }
mpq get_free_coeff_of_left_side() const override { return m_term->m_v;} mpq get_free_coeff_of_left_side() const override { return zero_of_type<mpq>();}
}; };

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

@ -137,7 +137,6 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be,
kind = static_cast<lconstraint_kind>(-kind); kind = static_cast<lconstraint_kind>(-kind);
} }
rs_of_evidence /= ratio; rs_of_evidence /= ratio;
rs_of_evidence += t->m_v * ratio;
} }
return kind == be.kind() && rs_of_evidence == be.m_bound; return kind == be.kind() && rs_of_evidence == be.m_bound;
@ -613,7 +612,6 @@ void lar_solver::substitute_terms_in_linear_expression(const vector<std::pair<mp
for (auto & p : term.coeffs()){ for (auto & p : term.coeffs()){
register_monoid_in_map(coeffs, t.first * p.second , p.first); register_monoid_in_map(coeffs, t.first * p.second , p.first);
} }
free_coeff += t.first * term.m_v;
} }
} }
@ -1117,7 +1115,7 @@ bool lar_solver::has_upper_bound(var_index var, constraint_index& ci, mpq& value
bool lar_solver::has_value(var_index var, mpq& value) const { bool lar_solver::has_value(var_index var, mpq& value) const {
if (is_term(var)) { if (is_term(var)) {
lar_term const& t = get_term(var); lar_term const& t = get_term(var);
value = t.m_v; value = zero_of_type<mpq>();
for (auto const& cv : t) { for (auto const& cv : t) {
impq const& r = get_column_value(cv.var()); impq const& r = get_column_value(cv.var());
if (!numeric_traits<mpq>::is_zero(r.y)) return false; if (!numeric_traits<mpq>::is_zero(r.y)) return false;
@ -1497,7 +1495,7 @@ bool lar_solver::term_is_int(const lar_term * t) const {
for (auto const & p : t->m_coeffs) for (auto const & p : t->m_coeffs)
if (! (column_is_int(p.first) && p.second.is_int())) if (! (column_is_int(p.first) && p.second.is_int()))
return false; return false;
return t->m_v.is_int(); return true;
} }
bool lar_solver::var_is_int(var_index v) const { bool lar_solver::var_is_int(var_index v) const {
@ -1598,9 +1596,8 @@ 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, var_index lar_solver::add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs) {
const mpq &m_v) { push_and_register_term(new lar_term(coeffs));
push_and_register_term(new lar_term(coeffs, m_v));
return m_terms_start_index + m_terms.size() - 1; return m_terms_start_index + m_terms.size() - 1;
} }
@ -1643,12 +1640,11 @@ void lar_solver::push_and_register_term(lar_term* t) {
} }
// terms // terms
var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs, var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs) {
const mpq &m_v) {
if (strategy_is_undecided()) if (strategy_is_undecided())
return add_term_undecided(coeffs, m_v); return add_term_undecided(coeffs);
push_and_register_term(new lar_term(coeffs, m_v)); push_and_register_term(new lar_term(coeffs));
unsigned adjusted_term_index = m_terms.size() - 1; unsigned adjusted_term_index = m_terms.size() - 1;
var_index ret = m_terms_start_index + adjusted_term_index; var_index ret = m_terms_start_index + adjusted_term_index;
if (use_tableau() && !coeffs.empty()) { if (use_tableau() && !coeffs.empty()) {
@ -1743,9 +1739,8 @@ void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_k
// lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int()); // lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int());
unsigned term_j; unsigned term_j;
if (m_var_register.external_is_used(j, term_j)) { if (m_var_register.external_is_used(j, term_j)) {
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)); 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); update_column_type_and_bound(term_j, kind, right_side, ci);
} }
else { else {
add_constraint_from_term_and_create_new_column_row(j, m_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);
@ -1756,7 +1751,7 @@ constraint_index lar_solver::add_constraint(const vector<std::pair<mpq, var_inde
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;
substitute_terms_in_linear_expression(left_side_with_terms, left_side, rs); substitute_terms_in_linear_expression(left_side_with_terms, left_side, rs);
unsigned term_index = add_term(left_side, zero_of_type<mpq>()); unsigned term_index = add_term(left_side);
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);
return ci; return ci;
@ -1767,7 +1762,7 @@ void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned ter
add_row_from_term_no_constraint(term, term_j); add_row_from_term_no_constraint(term, term_j);
unsigned j = A_r().column_count() - 1; unsigned j = A_r().column_count() - 1;
update_column_type_and_bound(j, kind, right_side - term->m_v, m_constraints.size()); update_column_type_and_bound(j, kind, right_side, m_constraints.size());
m_constraints.push_back(new lar_term_constraint(term, kind, right_side)); m_constraints.push_back(new lar_term_constraint(term, kind, right_side));
lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size());
} }

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

@ -164,13 +164,11 @@ public:
// terms // terms
var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs, var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs);
const mpq &m_v);
var_index add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs, var_index add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs);
const mpq &m_v);
bool term_coeffs_are_ok(const vector<std::pair<mpq, var_index>> & coeffs, const mpq& v); bool term_coeffs_are_ok(const vector<std::pair<mpq, var_index>> & coeffs);
void push_and_register_term(lar_term* t); void push_and_register_term(lar_term* t);
void add_row_for_term(const lar_term * term, unsigned term_ext_index); void add_row_for_term(const lar_term * term, unsigned term_ext_index);

9
src/util/lp/lar_term.h
View file

@ -23,7 +23,6 @@ namespace lp {
struct lar_term { struct lar_term {
// the term evaluates to sum of m_coeffs + m_v // the term evaluates to sum of m_coeffs + m_v
std::unordered_map<unsigned, mpq> m_coeffs; std::unordered_map<unsigned, mpq> m_coeffs;
mpq m_v;
lar_term() {} lar_term() {}
void add_monomial(const mpq& c, unsigned j) { void add_monomial(const mpq& c, unsigned j) {
auto it = m_coeffs.find(j); auto it = m_coeffs.find(j);
@ -37,7 +36,7 @@ struct lar_term {
} }
bool is_empty() const { bool is_empty() const {
return m_coeffs.size() == 0 && is_zero(m_v); return m_coeffs.size() == 0;
} }
unsigned size() const { return static_cast<unsigned>(m_coeffs.size()); } unsigned size() const { return static_cast<unsigned>(m_coeffs.size()); }
@ -46,8 +45,7 @@ struct lar_term {
return m_coeffs; return m_coeffs;
} }
lar_term(const vector<std::pair<mpq, unsigned>>& coeffs, lar_term(const vector<std::pair<mpq, unsigned>>& coeffs) {
const mpq & v) : m_v(v) {
for (const auto & p : coeffs) { for (const auto & p : coeffs) {
add_monomial(p.first, p.second); add_monomial(p.first, p.second);
} }
@ -87,7 +85,7 @@ struct lar_term {
template <typename T> template <typename T>
T apply(const vector<T>& x) const { T apply(const vector<T>& x) const {
T ret = T(m_v); T ret = zero_of_type<T>();
for (const auto & t : m_coeffs) { for (const auto & t : m_coeffs) {
ret += t.second * x[t.first]; ret += t.second * x[t.first];
} }
@ -96,7 +94,6 @@ struct lar_term {
void clear() { void clear() {
m_coeffs.clear(); m_coeffs.clear();
m_v = zero_of_type<mpq>();
} }
struct ival { struct ival {