From 31d4ba000954c4e6c458de30ae2d7e4bc0103134 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Jan 2025 13:54:56 -0800 Subject: [PATCH] re-introduce option to dump arithmetic lemmas to std-out --- src/smt/params/theory_arith_params.cpp | 2 ++ src/smt/params/theory_arith_params.h | 1 + src/smt/smt_context.h | 2 +- src/smt/smt_context_pp.cpp | 7 +++++- src/smt/theory_lra.cpp | 33 +++++++++++++++++++++----- 5 files changed, 37 insertions(+), 8 deletions(-) diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index fef7508f4..5d973a63e 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -37,6 +37,7 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_arith_eager_eq_axioms = p.arith_eager_eq_axioms(); m_arith_auto_config_simplex = p.arith_auto_config_simplex(); m_arith_validate = p.arith_validate(); + m_arith_dump_lemmas = p.arith_dump_lemmas(); m_nl_arith_propagate_linear_monomials = p.arith_nl_propagate_linear_monomials(); m_nl_arith_optimize_bounds = p.arith_nl_optimize_bounds(); m_nl_arith_cross_nested = p.arith_nl_cross_nested(); @@ -97,4 +98,5 @@ void theory_arith_params::display(std::ostream & out) const { DISPLAY_PARAM(m_nl_arith_optimize_bounds); DISPLAY_PARAM(m_nl_arith_cross_nested); DISPLAY_PARAM(m_arith_validate); + DISPLAY_PARAM(m_arith_dump_lemmas); } diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 0a6b9edca..26dadef58 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -83,6 +83,7 @@ struct theory_arith_params { unsigned m_arith_propagation_threshold = UINT_MAX; bool m_arith_validate = false; + bool m_arith_dump_lemmas = false; arith_pivot_strategy m_arith_pivot_strategy = arith_pivot_strategy::ARITH_PIVOT_SMALLEST; // used in diff-logic diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 9ab1db60a..a7b3ce124 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1469,7 +1469,7 @@ namespace smt { unsigned display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, symbol const& logic = symbol::null) const; void display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs, - literal consequent = false_literal, symbol const& logic = symbol::null) const; + literal consequent = false_literal, symbol const& logic = symbol::null, enode* x = nullptr, enode* y = nullptr) const; unsigned display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs, diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index a160b5f59..a91a437a2 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -456,6 +456,7 @@ namespace smt { literal2expr(~consequent, n); fmls.push_back(std::move(n)); } + if (logic != symbol::null) out << "(set-logic " << logic << ")\n"; visitor.collect(fmls); visitor.display_decls(out); @@ -475,7 +476,7 @@ namespace smt { void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, unsigned num_eq_antecedents, enode_pair const * eq_antecedents, - literal consequent, symbol const& logic) const { + literal consequent, symbol const& logic, enode* x, enode* y) const { ast_pp_util visitor(m); expr_ref_vector fmls(m); visitor.collect(fmls); @@ -490,6 +491,10 @@ namespace smt { n = m.mk_eq(p.first->get_expr(), p.second->get_expr()); fmls.push_back(n); } + if (x && y) { + expr_ref eq(m.mk_eq(x->get_expr(), y->get_expr()), m); + fmls.push_back(m.mk_not(eq)); + } if (consequent != false_literal) { literal2expr(~consequent, n); fmls.push_back(n); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 3d1103c4e..8a29515dd 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2396,7 +2396,9 @@ public: void assign(literal lit, literal_vector const& core, svector const& eqs, vector const& ps) { if (params().m_arith_validate) - VERIFY(validate_assign(lit, core, eqs)); + VERIFY(validate_assign(lit)); + if (params().m_arith_dump_lemmas) + dump_assign_lemma(lit); if (core.size() < small_lemma_size() && eqs.empty()) { m_core2.reset(); for (auto const& c : core) { @@ -3433,7 +3435,9 @@ public: if (params().m_arith_validate) - VERIFY(validate_conflict(m_core, m_eqs)); + VERIFY(validate_conflict()); + if (params().m_arith_dump_lemmas) + dump_conflict(); if (is_conflict) { ctx().set_conflict( ctx().mk_justification( @@ -3747,8 +3751,25 @@ public: } }; + void dump_assign_lemma(literal lit) { + m_core.push_back(~lit); + ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), lit); + m_core.pop_back(); + std::cout << "(reset)\n"; + } - bool validate_conflict(literal_vector const& core, svector const& eqs) { + void dump_conflict() { + ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data()); + std::cout << "(reset)\n"; + } + + void dump_eq(enode* x, enode* y) { + ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), false_literal, symbol::null, x, y); + std::cout << "(reset)\n"; + } + + + bool validate_conflict() { if (params().m_arith_mode != arith_solver_id::AS_NEW_ARITH) return true; VERIFY(!m_core.empty() || !m_eqs.empty()); @@ -3758,11 +3779,11 @@ public: cancel_eh eh(m.limit()); scoped_timer timer(1000, &eh); bool result = l_true != nctx.check(); - CTRACE("arith", !result, ctx().display_lemma_as_smt_problem(tout, core.size(), core.data(), eqs.size(), eqs.data(), false_literal);); + CTRACE("arith", !result, ctx().display_lemma_as_smt_problem(tout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), false_literal);); return result; } - bool validate_assign(literal lit, literal_vector const& core, svector const& eqs) { + bool validate_assign(literal lit) { if (params().m_arith_mode != arith_solver_id::AS_NEW_ARITH) return true; scoped_arith_mode _sa(ctx().get_fparams()); context nctx(m, ctx().get_fparams(), ctx().get_params()); @@ -3772,7 +3793,7 @@ public: cancel_eh eh(m.limit()); scoped_timer timer(1000, &eh); bool result = l_true != nctx.check(); - CTRACE("arith", !result, ctx().display_lemma_as_smt_problem(tout, core.size(), core.data(), eqs.size(), eqs.data(), lit); + CTRACE("arith", !result, ctx().display_lemma_as_smt_problem(tout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), lit); display(tout);); return result; }