mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix a bug in nla_expr

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-05 14:35:40 -07:00
parent 1e625db84b
commit 87cc5c8d96
6 changed files with 48 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -25,6 +25,10 @@ class explanation {
vector<std::pair<mpq, constraint_index>> m_explanation;
std::unordered_set<unsigned> m_set_of_ci;
public:
explanation() {}
template <typename T>
explanation(const T& t) { for ( unsigned c : t) add(c); }
void clear() { m_explanation.clear(); m_set_of_ci.clear(); }
vector<std::pair<mpq, constraint_index>>::const_iterator begin() const { return m_explanation.begin(); }
vector<std::pair<mpq, constraint_index>>::const_iterator end() const { return m_explanation.end(); }

16
src/math/lp/lar_solver.cpp
View file

@ -1361,6 +1361,16 @@ std::ostream& lar_solver::print_constraint_indices_only(constraint_index ci, std
return print_constraint_indices_only(m_constraints[ci], out);
}
std::ostream& lar_solver::print_constraint_indices_only_customized(constraint_index ci, std::function<std::string (unsigned)> var_str, std::ostream & out) const {
if (ci >= m_constraints.size()) {
out << "constraint " << T_to_string(ci) << " is not found";
out << std::endl;
return out;
}
return print_constraint_indices_only_customized(m_constraints[ci], var_str, out);
}
std::ostream& lar_solver::print_constraints(std::ostream& out) const {
out << "number of constraints = " << m_constraints.size() << std::endl;
for (auto c : m_constraints) {
@ -1443,6 +1453,12 @@ std::ostream& lar_solver::print_constraint_indices_only(const lar_base_constrain
return out << " " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side << std::endl;
}
std::ostream& lar_solver::print_constraint_indices_only_customized(const lar_base_constraint * c,
std::function<std::string (unsigned)> var_str, std::ostream & out) const {
print_linear_combination_customized(c->coeffs(), var_str, out);
return out << " " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side << std::endl;
}
void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector<unsigned>& column_list) {
for (unsigned i = 0; i < sz; i++) {
var_index var = vars[i];

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

@ -505,6 +505,10 @@ public:
std::ostream& print_constraint_indices_only(constraint_index ci, std::ostream & out) const;
std::ostream& print_constraint_indices_only_customized(constraint_index ci, std::function<std::string (unsigned)> var_str, std::ostream & out) const;
std::ostream& print_constraint_indices_only_customized(const lar_base_constraint * c, std::function<std::string (unsigned)> var_str, std::ostream & out) const;
std::ostream& print_terms(std::ostream& out) const;
std::ostream& print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out) const;

15
src/math/lp/nla_core.cpp
View file

@ -277,7 +277,9 @@ std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream&
out << "expl: ";
for (auto &p : exp) {
out << "(" << p.second << ")";
m_lar_solver.print_constraint_indices_only(p.second, out);
m_lar_solver.print_constraint_indices_only_customized(p.second,
[this](lpvar j) { return var_str(j);},
out);
out << " ";
}
out << "\n";
@ -1397,13 +1399,16 @@ std::ostream& core::print_terms(std::ostream& out) const {
}
return out;
}
std::string core::var_str(lpvar j) const {
return is_monomial_var(j)?
(product_indices_str(m_emons[j].vars()) + (check_monomial(m_emons[j])? "": "_")) : (std::string("v") + lp::T_to_string(j));
}
std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const {
return lp::print_linear_combination_customized(
t.coeffs_as_vector(),
[this](lpvar j) {
return is_monomial_var(j)?
(product_indices_str(m_emons[j].vars()) + (check_monomial(m_emons[j])? "": "_")) : (std::string("v") + lp::T_to_string(j));
},
[this](lpvar j) { return var_str(j); },
out);
}
} // end of nla

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

@ -172,6 +172,8 @@ public:
std::ostream& print_product(const T & m, std::ostream& out) const;
template <typename T>
std::string product_indices_str(const T & m) const;
std::string var_str(lpvar) const;
std::ostream & print_factor(const factor& f, std::ostream& out) const;
std::ostream & print_factor_with_vars(const factor& f, std::ostream& out) const;
std::ostream& print_monomial(const monomial& m, std::ostream& out) const;
@ -187,7 +189,7 @@ public:
void print_monomial_stats(const monomial& m, std::ostream& out);
void print_stats(std::ostream& out);
std::ostream& print_lemma(std::ostream& out) const;
void print_specific_lemma(const lemma& l, std::ostream& out) const;

26
src/math/lp/nla_intervals.cpp
View file

@ -126,17 +126,19 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const {
}
svector<lp::constraint_index> expl;
m_dep_manager.linearize(i.m_lower_dep, expl);
out << "\nlower constraints (\n";
for (lp::constraint_index c: expl)
m_core->m_lar_solver.print_constraint_indices_only(c, out);
out << ")\n";
expl.clear();
{
lp::explanation e(expl);
out << "\nlower constraints\n";
m_core->print_explanation(e, out);
expl.clear();
}
m_dep_manager.linearize(i.m_upper_dep, expl);
out << "upper constraints (\n";
for (lp::constraint_index c: expl)
m_core->m_lar_solver.print_constraint_indices_only(c, out);
{
lp::explanation e(expl);
out << "\n)\nupper constraints (\n";
m_core->print_explanation(e, out);
}
out << ")\n";
return out;
}
@ -144,12 +146,6 @@ lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; }
const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; }
std::ostream& intervals::print_explanations(const svector<lp::constraint_index> &expl , std::ostream& out) const {
out << "interv expl:\n ";
for (auto ci : expl)
m_core->m_lar_solver.print_constraint_indices_only(ci, out);
return out;
}
} // end of nla namespace