mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

remove a too strict debug check and fix a bug in intervals on terms

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-02 19:47:17 -08:00
parent 6ec9f9112c
commit e56a5787dc
2 changed files with 26 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -77,7 +77,14 @@ bool intervals::check_nex(const nex* n, u_dependency* initial_deps) {
return false;
}
auto interv_wd = interval_of_expr<e_with_deps::with_deps>(n, 1);
TRACE("grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) <<"expr = " << *n << "\n, initial deps\n"; print_dependencies(initial_deps, tout););
TRACE("grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) <<"expr = " << *n << "\n, initial deps\n"; print_dependencies(initial_deps, tout);
tout << ", expressions vars = \n";
for(lpvar j: m_core->get_vars_of_expr_with_opening_terms(n)) {
m_core->print_var(j, tout);
}
tout << "\n";
);
std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
m_core->add_empty_lemma();
m_core->current_expl().add(e);
@ -268,6 +275,12 @@ bool intervals::interval_from_term(const nex& e, interval& i) {
lp::explanation exp;
if (m_core->explain_by_equiv(norm_t, exp)) {
set_zero_interval(i);
if (wd == e_with_deps::with_deps) {
for (auto p : exp) {
i.m_lower_dep = mk_join(i.m_lower_dep, mk_leaf(p.second));
}
i.m_upper_dep = i.m_lower_dep;
}
TRACE("nla_intervals", tout << "explain_by_equiv\n";);
return true;
}
@ -275,7 +288,7 @@ bool intervals::interval_from_term(const nex& e, interval& i) {
if (j + 1 == 0)
return false;
set_var_interval<e_with_deps::without_deps>(j, i);
set_var_interval<wd>(j, i);
interval bi;
m_dep_intervals.mul<wd>(a, i, bi);
m_dep_intervals.add(b, bi);

19
src/smt/theory_lra.cpp
View file

@ -3333,14 +3333,17 @@ public:
c.neg();
ctx().mark_as_relevant(c);
}
TRACE("arith", ctx().display_literals_verbose(tout, m_core) << "\n";);
DEBUG_CODE(
for (literal const& c : m_core) {
if (ctx().get_assignment(c) == l_true) {
TRACE("arith", ctx().display_literal_verbose(tout, c) << " is true\n";);
SASSERT(false);
}
});
// DEBUG_CODE(
// for (literal const& c : m_core) {
// if (ctx().get_assignment(c) == l_true) {
// TRACE("arith", ctx().display_literal_verbose(tout, c) << " is true\n";);
// SASSERT(false);
// }
// }); // TODO: this check seems to be too strict.
// The lemmas can come in batches
// and the same literal can appear in several lemmas in a batch: it becomes l_true
// in earlier processing, but it was not so when the lemma was produced
ctx().mk_th_axiom(get_id(), m_core.size(), m_core.c_ptr());
}
}