mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 03:12:03 +00:00
Code Activity

debug new monomials on order lemmas

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-24 10:14:05 -07:00
parent 02379417a6
commit 150d3769fb
3 changed files with 33 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/util/lp/nla_core.cpp
View file

@ -199,14 +199,12 @@ std::ostream& core::print_bfc(const bfc& m, std::ostream& out) const {
return out << "( x = "; print_factor(m.m_x, out); out << ", y = "; print_factor(m.m_y, out); out << ")"; return out << "( x = "; print_factor(m.m_x, out); out << ", y = "; print_factor(m.m_y, out); out << ")";
} }
std::ostream& core::print_monomial_with_vars(lpvar v, std::ostream& out) const { std::ostream& core::print_monomial_with_vars(lpvar v, std::ostream& out) const {
return print_monomial_with_vars(m_emons[v], out); return print_monomial_with_vars(m_emons[v], out);
} }
template <typename T> template <typename T>
std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const { std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const {
print_product(m.vars(), out) << "\n"; print_product(m, out) << "\n";
for (unsigned k = 0; k < m.size(); k++) { for (unsigned k = 0; k < m.size(); k++) {
print_var(m[k], out); print_var(m[k], out);
} }
@ -215,9 +213,9 @@ std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const
std::ostream& core::print_monomial_with_vars(const monomial& m, std::ostream& out) const { std::ostream& core::print_monomial_with_vars(const monomial& m, std::ostream& out) const {
out << "["; print_var(m.var(), out) << "]\n"; out << "["; print_var(m.var(), out) << "]\n";
for (lpvar j: m.vars()) out << "vars:"; print_product_with_vars(m.vars(), out) << "\n";
print_var(j, out); out << "rvars:"; print_product_with_vars(m.rvars(), out) << "\n";
out << ")\n"; out << "rsign:" << m.rsign() << "\n";
return out; return out;
} }

46
src/util/lp/nla_core.h
View file

@ -338,30 +338,36 @@ public:
lbool test_check(vector<lemma>& l); lbool test_check(vector<lemma>& l);
}; // end of core }; // end of core
struct pp_mon { struct pp_mon {
core const& c; core const& c;
monomial const& m; monomial const& m;
pp_mon(core const& c, monomial const& m): c(c), m(m) {} pp_mon(core const& c, monomial const& m): c(c), m(m) {}
pp_mon(core const& c, lpvar v): c(c), m(c.m_emons[v]) {} pp_mon(core const& c, lpvar v): c(c), m(c.m_emons[v]) {}
}; };
struct pp_rmon {
core const& c;
monomial const& m;
pp_rmon(core const& c, monomial const& m): c(c), m(m) {}
pp_rmon(core const& c, lpvar v): c(c), m(c.m_emons[v]) {}
};
inline std::ostream& operator<<(std::ostream& out, pp_mon const& p) { return p.c.print_monomial(p.m, out); }
inline std::ostream& operator<<(std::ostream& out, pp_rmon const& p) { return p.c.print_monomial_with_vars(p.m, out); }
inline std::ostream& operator<<(std::ostream& out, pp_mon const& p) { return p.c.print_monomial(p.m, out); } struct pp_fac {
core const& c;
factor const& f;
pp_fac(core const& c, factor const& f): c(c), f(f) {}
};
struct pp_fac { inline std::ostream& operator<<(std::ostream& out, pp_fac const& f) { return f.c.print_factor(f.f, out); }
core const& c;
factor const& f;
pp_fac(core const& c, factor const& f): c(c), f(f) {}
};
inline std::ostream& operator<<(std::ostream& out, pp_fac const& f) { return f.c.print_factor(f.f, out); } struct pp_var {
core const& c;
lpvar v;
pp_var(core const& c, lpvar v): c(c), v(v) {}
};
struct pp_var { inline std::ostream& operator<<(std::ostream& out, pp_var const& v) { return v.c.print_var(v.v, out); }
core const& c;
lpvar v;
pp_var(core const& c, lpvar v): c(c), v(v) {}
};
inline std::ostream& operator<<(std::ostream& out, pp_var const& v) { return v.c.print_var(v.v, out); }
} // end of namespace nla } // end of namespace nla

6
src/util/lp/nla_order_lemmas.cpp
View file

@ -61,10 +61,10 @@ void order::order_lemma_on_rmonomial(const monomial& m) {
// a > b && c > 0 => ac > bc, // a > b && c > 0 => ac > bc,
// with either variable of ac playing the role of c // with either variable of ac playing the role of c
void order::order_lemma_on_binomial(const monomial& ac) { void order::order_lemma_on_binomial(const monomial& ac) {
TRACE("nla_solver", tout << pp_mon(c(), ac);); TRACE("nla_solver", tout << pp_rmon(c(), ac););
SASSERT(!check_monomial(ac) && ac.size() == 2); SASSERT(!check_monomial(ac) && ac.size() == 2);
const rational mult_val = val(ac.vars()[0]) * val(ac.vars()[1]); const rational mult_val = val(ac.rvars()[0]) * val(ac.rvars()[1]);
const rational acv = val(ac); const rational acv = val(ac)*ac.rsign();
bool gt = acv > mult_val; bool gt = acv > mult_val;
bool k = false; bool k = false;
do { do {