diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp index 6c4490d42..d792637ea 100644 --- a/src/cmd_context/extra_cmds/proof_cmds.cpp +++ b/src/cmd_context/extra_cmds/proof_cmds.cpp @@ -152,6 +152,14 @@ public: } } + // extract a simplified verification condition in case proof validation does not work. + // quantifier instantiation can be validated as follows: + // If quantifier instantiation claims that (forall x . phi(x)) => psi using instantiation x -> t + // then check the simplified VC: phi(t) => psi. + // in case psi is the literal instantiation, then the clause is a propositional tautology. + // The VC function is a no-op if the proof hint does not have an associated vc generator. + m_checker.vc(proof_hint, clause); + m_solver->push(); for (expr* lit : clause) m_solver->assert_expr(m.mk_not(lit)); diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp index 8e3c14f94..0554eae1d 100644 --- a/src/sat/sat_proof_trim.cpp +++ b/src/sat/sat_proof_trim.cpp @@ -40,10 +40,10 @@ namespace sat { revive(cl, clp); continue; } - IF_VERBOSE(0, s.display(verbose_stream())); + IF_VERBOSE(10, s.display(verbose_stream())); prune_trail(cl, clp); - IF_VERBOSE(0, verbose_stream() << cl << " " << in_core(cl, clp) << ": "; for (auto const& c : m_core_literals) verbose_stream() << "{" << c << "} "); - IF_VERBOSE(0, s.display(verbose_stream() << "\n")); + IF_VERBOSE(10, verbose_stream() << cl << " " << in_core(cl, clp) << ": "; for (auto const& c : m_core_literals) verbose_stream() << "{" << c << "} "); + IF_VERBOSE(10, s.display(verbose_stream() << "\n")); del(cl, clp); if (!in_core(cl, clp)) continue; diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index 51bd8bdd7..26bd835cc 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -36,6 +36,7 @@ z3_add_component(sat_smt q_mam.cpp q_mbi.cpp q_model_fixer.cpp + q_proof_checker.cpp q_queue.cpp q_solver.cpp recfun_solver.cpp diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index 751c43210..f2ce8803f 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -103,14 +103,18 @@ namespace dt { */ void solver::assert_eq_axiom(enode* n1, expr* e2, literal antecedent) { expr* e1 = n1->get_expr(); + euf::th_proof_hint* ph = nullptr; + if (ctx.use_drat()) { + // todo + } if (antecedent == sat::null_literal) - add_unit(eq_internalize(e1, e2)); + add_unit(eq_internalize(e1, e2), ph); else if (s().value(antecedent) == l_true) { euf::enode* n2 = e_internalize(e2); - ctx.propagate(n1, n2, euf::th_explain::propagate(*this, antecedent, n1, n2)); + ctx.propagate(n1, n2, euf::th_explain::propagate(*this, antecedent, n1, n2, ph)); } else - add_clause(~antecedent, eq_internalize(e1, e2)); + add_clause(~antecedent, eq_internalize(e1, e2), ph); } /** diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp index 158b850a5..fc9c80b75 100644 --- a/src/sat/smt/euf_proof_checker.cpp +++ b/src/sat/smt/euf_proof_checker.cpp @@ -21,6 +21,7 @@ Author: #include "ast/ast_ll_pp.h" #include "sat/smt/euf_proof_checker.h" #include "sat/smt/arith_proof_checker.h" +#include "sat/smt/q_proof_checker.h" #include namespace euf { @@ -240,7 +241,7 @@ namespace euf { return false; return pc.check(proof1) && pc.check(proof2); } - + expr_ref_vector clause(app* jst) override { expr_ref_vector result(m); auto x = jst->args3(); @@ -272,6 +273,7 @@ namespace euf { add_plugin(alloc(arith::proof_checker, m)); add_plugin(alloc(eq_proof_checker, m)); add_plugin(alloc(res_proof_checker, m, *this)); + add_plugin(alloc(q::proof_checker, m)); } proof_checker::~proof_checker() { @@ -290,8 +292,7 @@ namespace euf { bool proof_checker::check(expr* e) { if (m_checked_clauses.contains(e)) - return true; - + return true; if (!e || !is_app(e)) return false; app* a = to_app(e); @@ -309,12 +310,17 @@ namespace euf { expr_ref_vector* rr; if (m_checked_clauses.find(e, rr)) return *rr; - SASSERT(is_app(e) && m_map.contains(to_app(e)->get_decl()->get_name())); - expr_ref_vector r = m_map[to_app(e)->get_decl()->get_name()]->clause(to_app(e)); + 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; } + void proof_checker::vc(expr* e, expr_ref_vector& clause) { + SASSERT(is_app(e) && m_map.contains(to_app(e)->get_name())); + m_map[to_app(e)->get_name()]->vc(to_app(e), clause); + } + bool proof_checker::check(expr_ref_vector const& clause1, expr* e, expr_ref_vector & units) { if (!check(e)) return false; diff --git a/src/sat/smt/euf_proof_checker.h b/src/sat/smt/euf_proof_checker.h index 023bfae48..443d23186 100644 --- a/src/sat/smt/euf_proof_checker.h +++ b/src/sat/smt/euf_proof_checker.h @@ -30,6 +30,7 @@ namespace euf { virtual bool check(app* jst) = 0; virtual expr_ref_vector clause(app* jst) = 0; virtual void register_plugins(proof_checker& pc) = 0; + virtual void vc(app* jst, expr_ref_vector& clause) { } }; class proof_checker { @@ -44,6 +45,7 @@ namespace euf { void register_plugin(symbol const& rule, proof_checker_plugin*); bool check(expr* jst); expr_ref_vector clause(expr* jst); + void vc(expr* jst, expr_ref_vector& clause); bool check(expr_ref_vector const& clause, expr* e, expr_ref_vector& units); }; diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 00a23d903..7fc54f7cd 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -129,9 +129,9 @@ namespace euf { return sat::status::th(m_is_redundant, get_id(), ps); } - bool th_euf_solver::add_unit(sat::literal lit) { + bool th_euf_solver::add_unit(sat::literal lit, th_proof_hint const* ps) { bool was_true = is_true(lit); - ctx.s().add_clause(1, &lit, mk_status()); + ctx.s().add_clause(1, &lit, mk_status(ps)); ctx.add_root(lit); return !was_true; } @@ -155,9 +155,9 @@ namespace euf { return add_clause(3, lits, ps); } - bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d) { + bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d, th_proof_hint const* ps) { sat::literal lits[4] = { a, b, c, d }; - return add_clause(4, lits); + return add_clause(4, lits, ps); } bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps) { @@ -251,46 +251,46 @@ namespace euf { return new (sat::constraint_base::ptr2mem(mem)) th_explain(n_lits, lits, n_eqs, eqs, c, enode_pair(x, y), pma); } - th_explain* th_explain::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent, th_proof_hint const* pma) { - return mk(th, lits.size(), lits.data(), eqs.size(), eqs.data(), consequent, nullptr, nullptr, pma); + th_explain* th_explain::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent, th_proof_hint const* ph) { + return mk(th, lits.size(), lits.data(), eqs.size(), eqs.data(), consequent, nullptr, nullptr, ph); } - th_explain* th_explain::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* pma) { - return mk(th, lits.size(), lits.data(), eqs.size(), eqs.data(), sat::null_literal, x, y, pma); + th_explain* th_explain::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* ph) { + return mk(th, lits.size(), lits.data(), eqs.size(), eqs.data(), sat::null_literal, x, y, ph); } - th_explain* th_explain::propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* pma) { - return mk(th, 0, nullptr, eqs.size(), eqs.data(), sat::null_literal, x, y, pma); + th_explain* th_explain::propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* ph) { + return mk(th, 0, nullptr, eqs.size(), eqs.data(), sat::null_literal, x, y, ph); } - th_explain* th_explain::propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y) { - return mk(th, 1, &lit, 0, nullptr, sat::null_literal, x, y); + th_explain* th_explain::propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y, th_proof_hint const* ph) { + return mk(th, 1, &lit, 0, nullptr, sat::null_literal, x, y, ph); } - th_explain* th_explain::conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs) { - return conflict(th, lits.size(), lits.data(), eqs.size(), eqs.data()); + th_explain* th_explain::conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, th_proof_hint const* ph) { + return conflict(th, lits.size(), lits.data(), eqs.size(), eqs.data(), ph); } - th_explain* th_explain::conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs) { - return mk(th, n_lits, lits, n_eqs, eqs, sat::null_literal, nullptr, nullptr); + th_explain* th_explain::conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, th_proof_hint const* ph) { + return mk(th, n_lits, lits, n_eqs, eqs, sat::null_literal, nullptr, nullptr, ph); } - th_explain* th_explain::conflict(th_euf_solver& th, enode_pair_vector const& eqs) { - return conflict(th, 0, nullptr, eqs.size(), eqs.data()); + th_explain* th_explain::conflict(th_euf_solver& th, enode_pair_vector const& eqs, th_proof_hint const* ph) { + return conflict(th, 0, nullptr, eqs.size(), eqs.data(), ph); } - th_explain* th_explain::conflict(th_euf_solver& th, sat::literal lit) { - return conflict(th, 1, &lit, 0, nullptr); + th_explain* th_explain::conflict(th_euf_solver& th, sat::literal lit, th_proof_hint const* ph) { + return conflict(th, 1, &lit, 0, nullptr, ph); } - th_explain* th_explain::conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y) { + th_explain* th_explain::conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y, th_proof_hint const* ph) { enode_pair eq(x, y); - return conflict(th, 1, &lit, 1, &eq); + return conflict(th, 1, &lit, 1, &eq, ph); } - th_explain* th_explain::conflict(th_euf_solver& th, euf::enode* x, euf::enode* y) { + th_explain* th_explain::conflict(th_euf_solver& th, euf::enode* x, euf::enode* y, th_proof_hint const* ph) { enode_pair eq(x, y); - return conflict(th, 0, nullptr, 1, &eq); + return conflict(th, 0, nullptr, 1, &eq, ph); } std::ostream& th_explain::display(std::ostream& out) const { diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index a76b86cfd..cf645d21b 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -157,12 +157,12 @@ namespace euf { sat::status mk_status(th_proof_hint const* ps = nullptr); - bool add_unit(sat::literal lit); + bool add_unit(sat::literal lit, th_proof_hint const* ps = nullptr); bool add_units(sat::literal_vector const& lits); - bool add_clause(sat::literal lit) { return add_unit(lit); } + bool add_clause(sat::literal lit, th_proof_hint const* ps = nullptr) { return add_unit(lit, ps); } bool add_clause(sat::literal a, sat::literal b, th_proof_hint const* ps = nullptr); bool add_clause(sat::literal a, sat::literal b, sat::literal c, th_proof_hint const* ps = nullptr); - bool add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d); + bool add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d, th_proof_hint const* ps = nullptr); bool add_clause(sat::literal_vector const& lits, th_proof_hint const* ps = nullptr) { return add_clause(lits.size(), lits.data(), ps); } bool add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps = nullptr); void add_equiv(sat::literal a, sat::literal b); @@ -233,21 +233,21 @@ namespace euf { sat::literal* m_literals; enode_pair* m_eqs; static size_t get_obj_size(unsigned num_lits, unsigned num_eqs); - th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& eq, th_proof_hint const* pma = nullptr); - static th_explain* mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y, th_proof_hint const* pma = nullptr); + th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& eq, th_proof_hint const* ph = nullptr); + static th_explain* mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y, th_proof_hint const* ph = nullptr); public: - static th_explain* conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs); + static th_explain* conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, th_proof_hint const* ph = nullptr); static th_explain* conflict(th_euf_solver& th, sat::literal_vector const& lits) { return conflict(th, lits.size(), lits.data(), 0, nullptr); } - static th_explain* conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs); - static th_explain* conflict(th_euf_solver& th, enode_pair_vector const& eqs); - static th_explain* conflict(th_euf_solver& th, sat::literal lit); - static th_explain* conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y); - static th_explain* conflict(th_euf_solver& th, euf::enode* x, euf::enode* y); - static th_explain* propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y); - static th_explain* propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* pma = nullptr); - static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent, th_proof_hint const* pma = nullptr); - static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* pma = nullptr); + static th_explain* conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, th_proof_hint const* ph = nullptr); + static th_explain* conflict(th_euf_solver& th, enode_pair_vector const& eqs, th_proof_hint const* ph = nullptr); + static th_explain* conflict(th_euf_solver& th, sat::literal lit, th_proof_hint const* ph = nullptr); + static th_explain* conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y, th_proof_hint const* ph = nullptr); + static th_explain* conflict(th_euf_solver& th, euf::enode* x, euf::enode* y, th_proof_hint const* ph = nullptr); + static th_explain* propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y, th_proof_hint const* ph = nullptr); + static th_explain* propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* ph = nullptr); + static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent, th_proof_hint const* ph = nullptr); + static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* ph = nullptr); sat::ext_constraint_idx to_index() const { return sat::constraint_base::mem2base(this);