From 1fc77c8c004521867f1a78368f3c956c3ecfdbb8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 18 Oct 2022 09:02:50 -0700 Subject: [PATCH] wip - proof checking fixes to smt_theory_checker. Generalize it to apply to arrays and fpa. Missing: bv --- src/sat/smt/euf_proof.cpp | 32 +++++++++++++++++-------------- src/sat/smt/euf_proof_checker.cpp | 19 +++++++++--------- src/sat/smt/euf_proof_checker.h | 6 ++---- src/sat/smt/euf_solver.cpp | 2 ++ src/sat/smt/euf_solver.h | 5 ++++- 5 files changed, 35 insertions(+), 29 deletions(-) diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 3e42d130e..bfda8aad6 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -22,19 +22,22 @@ Author: namespace euf { void solver::init_proof() { - if (!m_proof_initialized) { - get_drat().add_theory(get_id(), symbol("euf")); - get_drat().add_theory(m.get_basic_family_id(), symbol("bool")); - } - if (!m_proof_out && s().get_config().m_drat && + if (m_proof_initialized) + return; + + if (s().get_config().m_drat && (get_config().m_lemmas2console || s().get_config().m_smt_proof_check || s().get_config().m_smt_proof.is_non_empty_string())) { + + get_drat().add_theory(get_id(), symbol("euf")); + get_drat().add_theory(m.get_basic_family_id(), symbol("bool")); TRACE("euf", tout << "init-proof " << s().get_config().m_smt_proof << "\n"); - m_proof_out = alloc(std::ofstream, s().get_config().m_smt_proof.str(), std::ios_base::out); + if (s().get_config().m_smt_proof.is_non_empty_string()) + m_proof_out = alloc(std::ofstream, s().get_config().m_smt_proof.str(), std::ios_base::out); get_drat().set_clause_eh(*this); + m_proof_initialized = true; } - m_proof_initialized = true; } /** @@ -133,7 +136,8 @@ namespace euf { func_decl_ref cc(m), cc_comm(m); sort* proof = m.mk_proof_sort(); ptr_buffer sorts; - expr_ref_vector args(m); + expr_ref_vector& args = s.m_expr_args; + args.reset(); if (m_cc_head < m_cc_tail) { sort* sorts[1] = { m.mk_bool_sort() }; cc_comm = m.mk_func_decl(symbol("comm"), 1, sorts, proof); @@ -325,16 +329,16 @@ namespace euf { void solver::on_check(unsigned n, literal const* lits, sat::status st) { if (!s().get_config().m_smt_proof_check) return; - expr_ref_vector clause(m); + m_clause.reset(); for (unsigned i = 0; i < n; ++i) - clause.push_back(literal2expr(lits[i])); + m_clause.push_back(literal2expr(lits[i])); auto hint = status2proof_hint(st); if (st.is_asserted() || st.is_redundant()) - m_smt_proof_checker.infer(clause, hint); + m_smt_proof_checker.infer(m_clause, hint); else if (st.is_deleted()) - m_smt_proof_checker.del(clause); + m_smt_proof_checker.del(m_clause); else if (st.is_input()) - m_smt_proof_checker.assume(clause); + m_smt_proof_checker.assume(m_clause); } void solver::on_lemma(unsigned n, literal const* lits, sat::status st) { @@ -391,7 +395,7 @@ namespace euf { void solver::display_inferred(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint) { expr_ref hint(proof_hint, m); if (!hint) - hint = m.mk_const(symbol("smt"), m.mk_proof_sort()); + hint = m.mk_const(m_smt, m.mk_proof_sort()); visit_expr(out, hint); display_hint(display_literals(out << "(infer", n, lits), hint) << ")\n"; } diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp index ff2803cb8..097bc7b61 100644 --- a/src/sat/smt/euf_proof_checker.cpp +++ b/src/sat/smt/euf_proof_checker.cpp @@ -214,6 +214,7 @@ namespace euf { void register_plugins(theory_checker& pc) override { pc.register_plugin(symbol("euf"), this); + pc.register_plugin(symbol("smt"), this); } }; @@ -289,13 +290,11 @@ namespace euf { add_plugin(alloc(res_checker, m, *this)); add_plugin(alloc(q::theory_checker, m)); add_plugin(alloc(distinct::theory_checker, m)); - add_plugin(alloc(smt_theory_checker_plugin, m, symbol("datatype"))); // no-op datatype proof checker + add_plugin(alloc(smt_theory_checker_plugin, m)); add_plugin(alloc(tseitin::theory_checker, m)); } theory_checker::~theory_checker() { - for (auto& [k, v] : m_checked_clauses) - dealloc(v); } void theory_checker::add_plugin(theory_checker_plugin* p) { @@ -310,20 +309,14 @@ namespace euf { bool theory_checker::check(expr* e) { if (!e || !is_app(e)) return false; - if (m_checked_clauses.contains(e)) - return true; app* a = to_app(e); theory_checker_plugin* p = nullptr; return m_map.find(a->get_decl()->get_name(), p) && p->check(a); } expr_ref_vector theory_checker::clause(expr* e) { - expr_ref_vector* rr; - if (m_checked_clauses.find(e, rr)) - return *rr; SASSERT(is_app(e) && m_map.contains(to_app(e)->get_name())); expr_ref_vector r = m_map[to_app(e)->get_name()]->clause(to_app(e)); - m_checked_clauses.insert(e, alloc(expr_ref_vector, r)); return r; } @@ -365,12 +358,16 @@ namespace euf { expr_ref_vector smt_theory_checker_plugin::clause(app* jst) { expr_ref_vector result(m); - SASSERT(jst->get_name() == m_rule); for (expr* arg : *jst) result.push_back(mk_not(m, arg)); return result; } + void smt_theory_checker_plugin::register_plugins(theory_checker& pc) { + pc.register_plugin(symbol("datatype"), this); + pc.register_plugin(symbol("array"), this); + pc.register_plugin(symbol("fpa"), this); + } smt_proof_checker::smt_proof_checker(ast_manager& m, params_ref const& p): m(m), @@ -469,6 +466,7 @@ namespace euf { lbool is_sat = m_solver->check_sat(); if (is_sat != l_false) { std::cout << "did not verify: " << is_sat << " " << clause << "\n"; + std::cout << "vc:\n" << vc << "\n"; if (proof_hint) std::cout << "hint: " << mk_bounded_pp(proof_hint, m, 4) << "\n"; m_solver->display(std::cout); @@ -486,6 +484,7 @@ namespace euf { for (expr* arg : clause) std::cout << "\n " << mk_bounded_pp(arg, m); std::cout << ")\n"; + if (is_rup(proof_hint)) diagnose_rup_failure(clause); diff --git a/src/sat/smt/euf_proof_checker.h b/src/sat/smt/euf_proof_checker.h index ae8b9a407..17a867104 100644 --- a/src/sat/smt/euf_proof_checker.h +++ b/src/sat/smt/euf_proof_checker.h @@ -42,7 +42,6 @@ namespace euf { ast_manager& m; scoped_ptr_vector m_plugins; // plugins of proof checkers map m_map; // symbol table of proof checkers - obj_map m_checked_clauses; // cache of previously checked proofs and their clauses. void add_plugin(theory_checker_plugin* p); public: theory_checker(ast_manager& m); @@ -62,12 +61,11 @@ namespace euf { */ class smt_theory_checker_plugin : public theory_checker_plugin { ast_manager& m; - symbol m_rule; public: - smt_theory_checker_plugin(ast_manager& m, symbol const& n): m(m), m_rule(n) {} + smt_theory_checker_plugin(ast_manager& m): m(m) {} bool check(app* jst) override { return false; } expr_ref_vector clause(app* jst) override; - void register_plugins(theory_checker& pc) override { pc.register_plugin(m_rule, this); } + void register_plugins(theory_checker& pc) override; }; diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index b462998a2..128f6ecc9 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -50,6 +50,8 @@ namespace euf { m_to_m(&m), m_to_si(&si), m_values(m), + m_clause(m), + m_expr_args(m), m_clause_visitor(m), m_smt_proof_checker(m, p) { diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index b423b1768..720053d7d 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -200,11 +200,14 @@ namespace euf { typedef std::pair expr_pair; literal_vector m_proof_literals; - svector m_proof_eqs, m_proof_deqs, m_expr_pairs; + svector m_proof_eqs, m_proof_deqs, m_expr_pairs; unsigned m_lit_head = 0, m_lit_tail = 0, m_cc_head = 0, m_cc_tail = 0; unsigned m_eq_head = 0, m_eq_tail = 0, m_deq_head = 0, m_deq_tail = 0; symbol m_euf = symbol("euf"); symbol m_smt = symbol("smt"); + expr_ref_vector m_clause; + expr_ref_vector m_expr_args; + eq_proof_hint* mk_hint(symbol const& th, literal lit, literal_vector const& r);