mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

Fixed bug reported by Yan Peng from UBC

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-12 13:04:54 -08:00
parent ed1f67f1f1
commit a934c6813a
2 changed files with 39 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/nlsat/nlsat_explain.cpp
View file

@ -981,6 +981,14 @@ namespace nlsat {
bool atom_val = a->get_kind() == atom::EQ;
bool lit_val = l.sign() ? !atom_val : atom_val;
new_lit = lit_val ? true_literal : false_literal;
if (!info.m_lc_const) {
// We have essentially shown the current factor must be zero If the leading coefficient is not zero.
// Note that, if the current factor is zero, then the whole polynomial is zero.
// The atom is true if it is an equality, and false otherwise.
// The sign of the leading coefficient (info.m_lc) of info.m_eq doesn't matter.
// However, we have to store the fact it is not zero.
info.add_lc_diseq();
}
return;
}
else if (s == -1 && !is_even) {
@ -1341,3 +1349,32 @@ namespace nlsat {
}
};
#ifdef Z3DEBUG
void pp(nlsat::explain::imp & ex, unsigned num, nlsat::literal const * ls) {
ex.display(std::cout, num, ls);
}
void pp(nlsat::explain::imp & ex, nlsat::scoped_literal_vector & ls) {
ex.display(std::cout, ls);
}
void pp(nlsat::explain::imp & ex, polynomial_ref const & p) {
ex.display(std::cout, p);
std::cout << std::endl;
}
void pp(nlsat::explain::imp & ex, polynomial::polynomial * p) {
polynomial_ref _p(p, ex.m_pm);
ex.display(std::cout, _p);
std::cout << std::endl;
}
void pp(nlsat::explain::imp & ex, polynomial_ref_vector const & ps) {
ex.display(std::cout, ps);
}
void pp_var(nlsat::explain::imp & ex, nlsat::var x) {
ex.display(std::cout, x);
std::cout << std::endl;
}
void pp_lit(nlsat::explain::imp & ex, nlsat::literal l) {
ex.display(std::cout, l);
std::cout << std::endl;
}
#endif

2
src/nlsat/nlsat_explain.h
View file

@ -27,7 +27,9 @@ namespace nlsat {
class evaluator;
class explain {
public:
struct imp;
private:
imp * m_imp;
public:
explain(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq,