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

fix bugs related to emons

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-25 12:00:44 -07:00
parent f78a2058fc
commit 8303d8c9ae
5 changed files with 9 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/util/lp/emonomials.cpp
View file

@ -143,7 +143,7 @@ namespace nla {
} }
} }
unsigned idx = m_monomials.size(); unsigned idx = m_monomials.size();
m_monomials.push_back(monomial(v, vars.size(), vars.c_ptr(), idx)); m_monomials.push_back(monomial(v, vars, idx));
m_var2index.setx(v, idx, UINT_MAX); m_var2index.setx(v, idx, UINT_MAX);
do_canonize(m_monomials[idx]); do_canonize(m_monomials[idx]);
monomial const* result = nullptr; monomial const* result = nullptr;

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

@ -104,7 +104,7 @@ struct const_iterator_mon {
}; };
struct factorization_factory { struct factorization_factory {
const svector<lpvar>& m_vars; const svector<lpvar> m_vars;
const monomial* m_monomial; const monomial* m_monomial;
// returns true if found // returns true if found
virtual bool find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned& i) const = 0; virtual bool find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned& i) const = 0;

2
src/util/lp/nla_basics_lemmas.cpp
View file

@ -740,7 +740,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(co
explain(f); explain(f);
TRACE("nla_solver", TRACE("nla_solver",
c().print_lemma(tout); c().print_lemma(tout);
tout << "rm = " << rm; tout << "rm = " << pp_rmon(c(), rm);
); );
return true; return true;
} }

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

@ -173,8 +173,7 @@ std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out)
print_var(f.var(), out); print_var(f.var(), out);
} }
else { else {
out << " RM = " << m_emons[f.var()]; out << " RM = " << pp_rmon(*this, m_emons[f.var()]);
out << "\n orig mon = " << m_emons[f.var()];
} }
return out; return out;
} }
@ -1447,8 +1446,8 @@ void core::trace_print_ol(const monomial& ac,
const monomial& bc, const monomial& bc,
const factor& b, const factor& b,
std::ostream& out) { std::ostream& out) {
out << "ac = " << ac << "\n"; out << "ac = " << pp_mon(*this, ac) << "\n";
out << "bc = " << bc << "\n"; out << "bc = " << pp_mon(*this, bc) << "\n";
out << "a = "; out << "a = ";
print_factor_with_vars(a, out); print_factor_with_vars(a, out);
out << ", \nb = "; out << ", \nb = ";
@ -1585,7 +1584,7 @@ bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const monomial*
j = rm.var(); j = rm.var();
sign = rm.rsign(); sign = rm.rsign();
TRACE("nla_solver", tout << "found bf"; TRACE("nla_solver", tout << "found bf";
tout << ":rm:" << rm << "\n"; tout << ":rm:" << pp_rmon(*this, rm) << "\n";
tout << "bf:"; print_bfc(bf, tout); tout << "bf:"; print_bfc(bf, tout);
tout << ", product = " << val(rm) << ", but should be =" << val(bf.m_x)*val(bf.m_y); tout << ", product = " << val(rm) << ", but should be =" << val(bf.m_x)*val(bf.m_y);
tout << ", j == "; print_var(j, tout) << "\n";); tout << ", j == "; print_var(j, tout) << "\n";);

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

@ -187,8 +187,8 @@ bool order::order_lemma_on_ac_and_bc(const monomial& rm_ac,
bool k, bool k,
const monomial& rm_bd) { const monomial& rm_bd) {
TRACE("nla_solver", TRACE("nla_solver",
tout << "rm_ac = " << rm_ac << "\n"; tout << "rm_ac = " << pp_rmon(_(), rm_ac) << "\n";
tout << "rm_bd = " << rm_bd << "\n"; tout << "rm_bd = " << pp_rmon(_(), rm_bd) << "\n";
tout << "ac_f[k] = "; tout << "ac_f[k] = ";
c().print_factor_with_vars(ac_f[k], tout);); c().print_factor_with_vars(ac_f[k], tout););
factor b; factor b;