From d4564028163571557dfd5d2b597f7795ec8fb7f3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Mar 2020 19:14:04 -0700 Subject: [PATCH] fix #3183 - change relevancy propagation to ensure that div/mod axioms are picked up Signed-off-by: Nikolaj Bjorner --- src/smt/smt_theory.cpp | 4 +- src/smt/smt_theory.h | 14 ++++ src/smt/theory_lra.cpp | 143 ++++++++++++----------------------------- 3 files changed, 58 insertions(+), 103 deletions(-) diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp index 147453d5443..ee317818f90 100644 --- a/src/smt/smt_theory.cpp +++ b/src/smt/smt_theory.cpp @@ -141,6 +141,7 @@ namespace smt { void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, app * const * bindings, unsigned pattern_id, const vector> & used_enodes) { ast_manager & m = get_manager(); + app_ref _r(r, m); std::ostream& out = m.trace_stream(); symbol const & family_name = m.get_family_name(get_family_id()); if (pattern_id == UINT_MAX) { @@ -158,7 +159,8 @@ namespace smt { out << " #" << substituted->get_owner_id(); } } - } else { + } + else { SASSERT(axiom_id != UINT_MAX); obj_hashtable already_visited; for (auto n : used_enodes) { diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index 810e21fc5f8..6213c438184 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -114,6 +114,15 @@ namespace smt { } }; + struct if_trace_stream { + ast_manager& m; + + if_trace_stream(ast_manager& m, std::function& fn): m(m) { + if (m.has_trace_stream()) { + fn(); + } + } + }; protected: /** @@ -418,6 +427,11 @@ namespace smt { log_axiom_instantiation(r, UINT_MAX, 0, nullptr, UINT_MAX, used_enodes); } + void log_axiom_unit(app* r) { + log_axiom_instantiation(r); + m_manager->trace_stream() << "[end-of-instance]\n"; + } + public: /** \brief Assume eqs between variable that are equal with respect to the given table. diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 76221695b9e..20c67ecabf5 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1340,59 +1340,35 @@ class theory_lra::imp { context& c = ctx(); if (!k.is_zero()) { - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())); - th.log_axiom_instantiation(body); - } mk_axiom(eq); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var())); - th.log_axiom_instantiation(body); - } mk_axiom(mod_ge_0); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_le(mod, upper)); - th.log_axiom_instantiation(body); + mk_axiom(mk_literal(a.mk_le(mod, upper))); + { + std::function log = [&,this]() { + th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()))); + th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var()))); + th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_le(mod, upper))); + }; + if_trace_stream _ts(m, log); } - expr_ref le(a.mk_le(mod, upper), m); - mk_axiom(mk_literal(le)); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (k.is_pos()) { - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())); - th.log_axiom_instantiation(body); - } - mk_axiom(~p_ge_0, div_ge_0); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())); - th.log_axiom_instantiation(body); - } + mk_axiom(~p_ge_0, div_ge_0); mk_axiom(~p_le_0, div_le_0); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + std::function log = [&,this]() { + th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var()))); + th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var()))); + }; + if_trace_stream _ts(m, log); } else { - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())); - th.log_axiom_instantiation(body); - } mk_axiom(~p_ge_0, div_le_0); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())); - th.log_axiom_instantiation(body); - } mk_axiom(~p_le_0, div_ge_0); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + std::function log = [&,this]() { + th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var()))); + th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var()))); + }; + if_trace_stream _ts(m, log); } } else { @@ -1404,64 +1380,29 @@ class theory_lra::imp { // q >= 0 or (p mod q) < -q literal q_ge_0 = mk_literal(a.mk_ge(q, zero)); literal q_le_0 = mk_literal(a.mk_le(q, zero)); - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())); - th.log_axiom_instantiation(body); - } + mk_axiom(q_ge_0, eq); mk_axiom(q_le_0, eq); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var())); - th.log_axiom_instantiation(body); - } mk_axiom(q_ge_0, mod_ge_0); mk_axiom(q_le_0, mod_ge_0); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero)); - th.log_axiom_instantiation(body); - } - mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero))); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero)); - th.log_axiom_instantiation(body); - } + mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero))); mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero))); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())); - th.log_axiom_instantiation(body); - } mk_axiom(q_le_0, ~p_ge_0, div_ge_0); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())); - th.log_axiom_instantiation(body); - } mk_axiom(q_le_0, ~p_le_0, div_le_0); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())); - th.log_axiom_instantiation(body); - } - mk_axiom(q_ge_0, ~p_ge_0, div_le_0); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())); - th.log_axiom_instantiation(body); - } - mk_axiom(q_ge_0, ~p_le_0, div_ge_0); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + mk_axiom(q_ge_0, ~p_ge_0, div_le_0); + mk_axiom(q_ge_0, ~p_le_0, div_ge_0); + + std::function log = [&,this]() { + th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()))); + th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var()))); + th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero))); + th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero))); + th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var()))); + th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var()))); + th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var()))); + th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var()))); + }; + if_trace_stream _ts(m, log); } if (m_arith_params.m_arith_enum_const_mod && k.is_pos() && k < rational(8)) { unsigned _k = k.get_unsigned(); @@ -1484,10 +1425,10 @@ class theory_lra::imp { } void mk_axiom(literal l) { - ctx().mk_th_axiom(get_id(), false_literal, l); if (ctx().relevancy()) { ctx().mark_as_relevant(l); } + ctx().mk_th_axiom(get_id(), false_literal, l); } void mk_axiom(literal l1, literal l2) { @@ -1498,7 +1439,7 @@ class theory_lra::imp { ctx().mk_th_axiom(get_id(), l1, l2); if (ctx().relevancy()) { ctx().mark_as_relevant(l1); - ctx().add_rel_watch(~l1, ctx().bool_var2expr(l2.var())); + ctx().mark_as_relevant(l2); } } @@ -1506,8 +1447,8 @@ class theory_lra::imp { ctx().mk_th_axiom(get_id(), l1, l2, l3); if (ctx().relevancy()) { ctx().mark_as_relevant(l1); - ctx().add_rel_watch(~l1, ctx().bool_var2expr(l2.var())); - ctx().add_rel_watch(~l2, ctx().bool_var2expr(l3.var())); + ctx().mark_as_relevant(l2); + ctx().mark_as_relevant(l3); } } @@ -1566,7 +1507,6 @@ class theory_lra::imp { rational get_value(theory_var v) const { if (v == null_theory_var || !lp().external_is_used(v)) { - TRACE("arith", tout << "Variable v" << v << " not internalized\n";); return rational::zero(); } @@ -1575,7 +1515,6 @@ class theory_lra::imp { return m_variable_values[vi]; if (!lp().is_term(vi)) { - TRACE("arith", tout << "not a term v" << v << "\n";); return rational::zero(); } @@ -3801,7 +3740,7 @@ class theory_lra::imp { lp().print_terms(out); // the tableau auto pp = lp ::core_solver_pretty_printer( - lp().m_mpq_lar_core_solver.m_r_solver, out); + lp().m_mpq_lar_core_solver.m_r_solver, out); pp.print(); for (unsigned j = 0; j < lp().number_of_vars(); j++) { lp().m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);