mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

add trace statement

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-10 17:24:15 -10:00
parent a86d4b0675
commit eee8188abf
1 changed files with 19 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/math/lp/nla_intervals.cpp
View file

@ -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<lp::constraint_index> 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<lp::constraint_index> 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<lp::constraint_index> 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<lp::constraint_index> 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 {