diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp index 6213e7cd3..8d6b6ad8e 100644 --- a/src/cmd_context/extra_cmds/proof_cmds.cpp +++ b/src/cmd_context/extra_cmds/proof_cmds.cpp @@ -15,28 +15,51 @@ Author: Notes: -- add theory hint bypass using proof checker plugins of SMT - - arith_proof_checker.h is currently -- could use m_drat for drup premises. +Proof checker for clauses created during search. +1. Clauses annotated by RUP (reverse unit propagation) + are checked to be inferrable using reverse unit propagation + based on previous clauses. +2. Clauses annotated by supported proof rules (proof hints) + are checked by custom proof checkers. There is a proof checker + for each proof rule. Main proof checkers just have a single step + but the framework allows to compose proof rules, each inference + is checked for correctness by a plugin. +3. When there are no supported plugin to justify the derived + clause, or a custom check fails, the fallback is to check that the + derived clause is a consequence of the input clauses using SMT. + The last approach is a bail-out and offers a weaker notion of + self-validation. It is often (but not always) sufficient for using proof + checking for debugging, as the root-cause for an unsound inference in z3 + does not necessarily manifest when checking the conclusion of the + inference. An external proof checker that uses such fallbacks could + use several solvers, or bootstrap from a solver that can generate certificates + when z3 does not. + + + --*/ #include "util/small_object_allocator.h" #include "ast/ast_util.h" -#include "cmd_context/cmd_context.h" #include "smt/smt_solver.h" #include "sat/sat_solver.h" #include "sat/sat_drat.h" #include "sat/smt/euf_proof_checker.h" +#include "cmd_context/cmd_context.h" #include class smt_checker { ast_manager& m; params_ref m_params; + + // for checking proof rules (hints) euf::proof_checker m_checker; + // for fallback SMT checker scoped_ptr m_solver; + // for RUP symbol m_rup; sat::solver m_sat_solver; sat::drat m_drat; @@ -63,11 +86,10 @@ public: m_rup = symbol("rup"); } - bool is_rup(expr* proof_hint) { + bool is_rup(app* proof_hint) { return proof_hint && - is_app(proof_hint) && - to_app(proof_hint)->get_name() == m_rup; + proof_hint->get_name() == m_rup; } void mk_clause(expr_ref_vector const& clause) { @@ -79,6 +101,14 @@ public: m_clause.push_back(sat::literal(e->get_id(), sign)); } } + + void mk_clause(expr* e) { + m_clause.reset(); + bool sign = false; + while (m.is_not(e, e)) + sign = !sign; + m_clause.push_back(sat::literal(e->get_id(), sign)); + } bool check_rup(expr_ref_vector const& clause) { add_units(); @@ -86,25 +116,38 @@ public: return m_drat.is_drup(m_clause.size(), m_clause.data(), m_units); } + bool check_rup(expr* u) { + add_units(); + mk_clause(u); + return m_drat.is_drup(m_clause.size(), m_clause.data(), m_units); + } + void add_clause(expr_ref_vector const& clause) { mk_clause(clause); m_drat.add(m_clause, sat::status::input()); } - void check(expr_ref_vector const& clause, expr* proof_hint) { - - + void check(expr_ref_vector& clause, app* proof_hint) { + if (is_rup(proof_hint) && check_rup(clause)) { std::cout << "(verified-rup)\n"; return; } - if (m_checker.check(clause, proof_hint)) { - if (is_app(proof_hint)) - std::cout << "(verified-" << to_app(proof_hint)->get_name() << ")\n"; - else - std::cout << "(verified-checker)\n"; - return; + expr_ref_vector units(m); + if (m_checker.check(clause, proof_hint, units)) { + bool units_are_rup = true; + for (expr* u : units) { + if (!check_rup(u)) { + std::cout << "unit " << mk_pp(u, m) << " is not rup\n"; + units_are_rup = false; + } + } + if (units_are_rup) { + std::cout << "(verified-" << proof_hint->get_name() << ")\n"; + add_clause(clause); + return; + } } m_solver->push(); @@ -123,7 +166,7 @@ public: } m_solver->pop(1); std::cout << "(verified-smt)\n"; - // assume(clause); + add_clause(clause); } void assume(expr_ref_vector const& clause) { @@ -135,14 +178,14 @@ public: class proof_cmds_imp : public proof_cmds { ast_manager& m; expr_ref_vector m_lits; - expr_ref m_proof_hint; + app_ref m_proof_hint; smt_checker m_checker; public: proof_cmds_imp(ast_manager& m): m(m), m_lits(m), m_proof_hint(m), m_checker(m) {} void add_literal(expr* e) override { if (m.is_proof(e)) - m_proof_hint = e; + m_proof_hint = to_app(e); else m_lits.push_back(e); } diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 93f4c2e91..17de0fe3b 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -416,6 +416,8 @@ namespace sat { void drat::verify(unsigned n, literal const* c) { if (!m_check_unsat) return; + if (m_inconsistent) + return; for (unsigned i = 0; i < n; ++i) declare(c[i]); if (is_drup(n, c)) { @@ -690,7 +692,7 @@ namespace sat { ++m_stats.m_num_add; if (m_check) { switch (sz) { - case 0: add(); break; + case 0: if (st.is_input()) m_inconsistent = true; else add(); break; case 1: append(lits[0], st); break; default: append(mk_clause(sz, lits, st.is_redundant()), st); break; } diff --git a/src/sat/smt/arith_proof_checker.h b/src/sat/smt/arith_proof_checker.h index d1d0c089c..d067303a5 100644 --- a/src/sat/smt/arith_proof_checker.h +++ b/src/sat/smt/arith_proof_checker.h @@ -140,11 +140,13 @@ namespace arith { SASSERT(m_todo.empty()); m_todo.push_back({ mul, e }); rational coeff1; - expr* e1, *e2; + expr* e1, *e2, *e3; for (unsigned i = 0; i < m_todo.size(); ++i) { auto [coeff, e] = m_todo[i]; if (a.is_mul(e, e1, e2) && a.is_numeral(e1, coeff1)) m_todo.push_back({coeff*coeff1, e2}); + else if (a.is_mul(e, e1, e2) && a.is_uminus(e1, e3) && a.is_numeral(e3, coeff1)) + m_todo.push_back({-coeff*coeff1, e2}); else if (a.is_mul(e, e1, e2) && a.is_numeral(e2, coeff1)) m_todo.push_back({coeff*coeff1, e1}); else if (a.is_add(e)) @@ -158,6 +160,8 @@ namespace arith { } else if (a.is_numeral(e, coeff1)) r.m_coeff += coeff*coeff1; + else if (a.is_uminus(e, e1) && a.is_numeral(e1, coeff1)) + r.m_coeff -= coeff*coeff1; else add(r, e, coeff); } @@ -361,8 +365,14 @@ namespace arith { return out; } - bool check(expr_ref_vector const& clause, app* jst) override { + bool check(expr_ref_vector const& clause, app* jst, expr_ref_vector& units) override { reset(); + expr_mark pos, neg; + for (expr* e : clause) + if (m.is_not(e, e)) + neg.mark(e, true); + else + pos.mark(e, true); if (jst->get_name() == symbol("farkas")) { bool even = true; @@ -387,13 +397,24 @@ namespace arith { } else return false; + + if (sign && !pos.is_marked(arg)) { + units.push_back(m.mk_not(arg)); + pos.mark(arg, false); + } + else if (!sign && !neg.is_marked(arg)) { + units.push_back(arg); + neg.mark(arg, false); + } + } even = !even; } - if (check_farkas()) + if (check_farkas()) { return true; + } - IF_VERBOSE(0, verbose_stream() << "did not check farkas\n" << mk_pp(jst, m) << "\n"); + IF_VERBOSE(0, verbose_stream() << "did not check farkas\n" << mk_pp(jst, m) << "\n"; display(verbose_stream()); ); return false; } diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp index 38ad62589..41f627914 100644 --- a/src/sat/smt/euf_proof_checker.cpp +++ b/src/sat/smt/euf_proof_checker.cpp @@ -35,13 +35,14 @@ namespace euf { m_map.insert(rule, p); } - bool proof_checker::check(expr_ref_vector const& clause, expr* e) { + bool proof_checker::check(expr_ref_vector const& clause, expr* e, expr_ref_vector& units) { if (!e || !is_app(e)) return false; + units.reset(); app* a = to_app(e); proof_checker_plugin* p = nullptr; if (m_map.find(a->get_decl()->get_name(), p)) - return p->check(clause, a); + return p->check(clause, a, units); return false; } diff --git a/src/sat/smt/euf_proof_checker.h b/src/sat/smt/euf_proof_checker.h index be1e8fa70..464d90559 100644 --- a/src/sat/smt/euf_proof_checker.h +++ b/src/sat/smt/euf_proof_checker.h @@ -27,7 +27,7 @@ namespace euf { class proof_checker_plugin { public: virtual ~proof_checker_plugin() {} - virtual bool check(expr_ref_vector const& clause, app* jst) = 0; + virtual bool check(expr_ref_vector const& clause, app* jst, expr_ref_vector& units) = 0; virtual void register_plugins(proof_checker& pc) = 0; }; @@ -39,7 +39,7 @@ namespace euf { proof_checker(ast_manager& m); ~proof_checker(); void register_plugin(symbol const& rule, proof_checker_plugin*); - bool check(expr_ref_vector const& clause, expr* e); + bool check(expr_ref_vector const& clause, expr* e, expr_ref_vector& units); }; } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 0224d5e96..72094f78a 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -255,9 +255,8 @@ namespace smt { return false; ptr_vector sorts(f->get_arity(), f->get_domain()); svector names; - for (unsigned i = 0; i < f->get_arity(); ++i) { + for (unsigned i = 0; i < f->get_arity(); ++i) names.push_back(symbol(i)); - } defined_names dn(m); body = replace_value_from_ctx(body); body = m.mk_lambda(sorts.size(), sorts.data(), names.data(), body); @@ -575,16 +574,16 @@ namespace smt { for (unsigned i = 0; i < n; ++i) { proof* pr = nullptr; expr* arg = args[i]; - if (m.proofs_enabled()) { + if (m.proofs_enabled()) pr = m.mk_def_intro(arg); - } m_context->internalize_assertion(arg, pr, gen); } } TRACE("model_checker_bug_detail", tout << "instantiating... q:\n" << mk_pp(q, m) << "\n"; tout << "inconsistent: " << m_context->inconsistent() << "\n"; - tout << "bindings:\n" << expr_ref_vector(m, num_decls, m_pinned_exprs.data() + offset) << "\n";); + tout << "bindings:\n" << expr_ref_vector(m, num_decls, m_pinned_exprs.data() + offset) << "\n"; + tout << "def " << mk_pp(inst.m_def, m) << "\n";); m_context->add_instance(q, nullptr, num_decls, bindings.data(), inst.m_def, gen, gen, gen, dummy); TRACE("model_checker_bug_detail", tout << "after instantiating, inconsistent: " << m_context->inconsistent() << "\n";); }