From eee8188abf9a4fc9dc450ab0cd9389aef855e769 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 10 Dec 2019 17:24:15 -1000 Subject: [PATCH] add trace statement Signed-off-by: Lev Nachmanson --- src/math/lp/nla_intervals.cpp | 35 +++++++++++++++++++---------------- 1 file changed, 19 insertions(+), 16 deletions(-) diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index fffab5637..dd447925d 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -579,26 +579,29 @@ bool intervals::check_interval_for_conflict_on_zero_upper( ci_dependency* dep) { if (!separated_from_zero_on_upper(i)) return false; - - m_core->add_empty_lemma(); - svector expl; - dep = m_dep_manager.mk_join(dep, i.m_upper_dep); - m_dep_manager.linearize(dep, expl); - m_core->current_expl().add_expl(expl); - TRACE("nla_solver", m_core->print_lemma(tout);); - return true; + + TRACE("grobner", display(tout, i);); + m_core->add_empty_lemma(); + svector expl; + dep = m_dep_manager.mk_join(dep, i.m_upper_dep); + m_dep_manager.linearize(dep, expl); + m_core->current_expl().add_expl(expl); + TRACE("nla_solver", m_core->print_lemma(tout);); + return true; } bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, ci_dependency* dep) { - if (!separated_from_zero_on_lower(i)) + if (!separated_from_zero_on_lower(i)) { return false; - m_core->add_empty_lemma(); - svector expl; - dep = m_dep_manager.mk_join(dep, i.m_lower_dep); - m_dep_manager.linearize(dep, expl); - m_core->current_expl().add_expl(expl); - TRACE("nla_solver", m_core->print_lemma(tout);); - return true; + } + TRACE("grobner", display(tout, i);); + m_core->add_empty_lemma(); + svector expl; + dep = m_dep_manager.mk_join(dep, i.m_lower_dep); + m_dep_manager.linearize(dep, expl); + m_core->current_expl().add_expl(expl); + TRACE("nla_solver", m_core->print_lemma(tout);); + return true; } common::ci_dependency *intervals::mk_dep(lp::constraint_index ci) const {