From 3fcd9e64c7343f2096b417a094699534c076dc61 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Oct 2019 20:18:21 -0700 Subject: [PATCH] logging Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_explain.cpp | 38 +++++++++++++++++++++++++++++-------- src/nlsat/nlsat_solver.cpp | 6 ++++-- 2 files changed, 34 insertions(+), 10 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 1e7b0f33451..97a789f0321 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -188,7 +188,7 @@ namespace nlsat { unsigned lidx = l.index(); if (m_already_added_literal.get(lidx, false)) return; - TRACE("nlsat_explain", tout << "adding literal: " << lidx << "\n"; m_solver.display(tout, l); tout << "\n";); + TRACE("nlsat_explain", tout << "adding literal: " << lidx << "\n"; m_solver.display(tout, l) << "\n";); m_already_added_literal.setx(lidx, true, false); m_result->push_back(l); } @@ -619,10 +619,15 @@ namespace nlsat { void psc(polynomial_ref & p, polynomial_ref & q, var x) { polynomial_ref_vector & S = m_psc_tmp; polynomial_ref s(m_pm); - TRACE("nlsat_explain", tout << "computing psc of\n"; display(tout, p); tout << "\n"; display(tout, q); tout << "\n";); psc_chain(p, q, x, S); unsigned sz = S.size(); + TRACE("nlsat_explain", tout << "computing psc of\n"; display(tout, p); tout << "\n"; display(tout, q); tout << "\n"; + for (unsigned i = 0; i < sz; ++i) { + s = S.get(i); + tout << "psc: " << s << "\n"; + }); + for (unsigned i = 0; i < sz; i++) { s = S.get(i); TRACE("nlsat_explain", tout << "processing psc(" << i << ")\n"; display(tout, s); tout << "\n";); @@ -634,7 +639,7 @@ namespace nlsat { TRACE("nlsat_explain", tout << "done, psc is a constant\n";); return; } - if (sign(s) == 0) { + if (sign(s) == polynomial::sign_zero) { TRACE("nlsat_explain", tout << "psc vanished, adding zero assumption\n";); add_zero_assumption(s); continue; @@ -825,6 +830,7 @@ namespace nlsat { #else int s = sign(p); if (!is_const(p)) { + TRACE("nlsat_explain", tout << p << "\n";); add_simple_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p); } return s; @@ -833,6 +839,11 @@ namespace nlsat { /** Auxiliary function to linear roots. + y > root[1](-2*y - z) + y > -z/2 + y + z/2 > 0 + 2y + z > 0 + */ void mk_linear_root(atom::kind k, var y, unsigned i, poly * p, bool mk_neg) { polynomial_ref p_prime(m_pm); @@ -898,8 +909,13 @@ namespace nlsat { m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots); unsigned num_roots = roots.size(); for (unsigned i = 0; i < num_roots; i++) { - TRACE("nlsat_explain", tout << "comparing root: "; m_am.display_decimal(tout, roots[i]); tout << "\n";); int s = m_am.compare(y_val, roots[i]); + TRACE("nlsat_explain", + m_am.display_decimal(tout << "comparing root: ", roots[i]); tout << "\n"; + m_am.display_decimal(tout << "with y_val:", y_val); + tout << "\nsign " << s << "\n"; + tout << "poly: " << p << "\n"; + ); if (s == 0) { // y_val == roots[i] // add literal @@ -931,11 +947,15 @@ namespace nlsat { } } } - - if (!lower_inf) + + if (!lower_inf) { + TRACE("nlsat_explain", tout << "lower_inf: " << lower_inf << " upper_inf: " << upper_inf << " " << p_lower << "\n";); add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, i_lower, p_lower); - if (!upper_inf) + } + if (!upper_inf) { + TRACE("nlsat_explain", tout << "lower_inf: " << lower_inf << " upper_inf: " << upper_inf << " " << p_upper << "\n";); add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, i_upper, p_upper); + } } /** @@ -1076,7 +1096,7 @@ namespace nlsat { new_lit = l; return; } - TRACE("nlsat_simplify_core", tout << "trying to simplify literal\n"; display(tout, l); tout << "\nusing equation\n"; + TRACE("nlsat_simplify_core", display(tout << "trying to simplify literal\n", l) << "\nusing equation\n"; m_pm.display(tout, info.m_eq, m_solver.display_proc()); tout << "\n";); int atom_sign = 1; bool modified_lit = false; @@ -1348,7 +1368,9 @@ namespace nlsat { var max_x = max_var(m_ps); TRACE("nlsat_explain", tout << "polynomials in the conflict:\n"; display(tout, m_ps); tout << "\n";); elim_vanishing(m_ps); + TRACE("nlsat_explain", tout << "elim vanishing\n"; display(tout, m_ps); tout << "\n";); project(m_ps, max_x); + TRACE("nlsat_explain", tout << "after projection\n"; display(tout, m_ps); tout << "\n";); } void process2(unsigned num, literal const * ls) { diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 2709da1e9d7..19e28333ff2 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -652,9 +652,11 @@ namespace nlsat { SASSERT(i > 0); SASSERT(x >= max_var(p)); SASSERT(k == atom::ROOT_LT || k == atom::ROOT_GT || k == atom::ROOT_EQ || k == atom::ROOT_LE || k == atom::ROOT_GE); - polynomial_ref p1(m_pm); + polynomial_ref p1(m_pm), uniq_p(m_pm); p1 = m_pm.flip_sign_if_lm_neg(p); // flipping the sign of the polynomial will not change its roots. - poly * uniq_p = m_cache.mk_unique(p1); + uniq_p = m_cache.mk_unique(p1); + TRACE("nlsat_solver", tout << p1 << " " << uniq_p << "\n";); + void * mem = m_allocator.allocate(sizeof(root_atom)); root_atom * new_atom = new (mem) root_atom(k, x, i, uniq_p); root_atom * old_atom = m_root_atoms.insert_if_not_there(new_atom);