From f6595c161f73309aeb4df9cc078d21d4909b38db Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Oct 2022 17:43:56 -0700 Subject: [PATCH] add examples with proof replay Signed-off-by: Nikolaj Bjorner --- examples/python/proofreplay.py | 113 ++++++++++++++++++++++ src/api/api_solver.cpp | 8 ++ src/cmd_context/cmd_context.h | 1 + src/cmd_context/extra_cmds/proof_cmds.cpp | 39 +++++++- src/cmd_context/extra_cmds/proof_cmds.h | 2 +- src/sat/sat_config.cpp | 3 +- src/sat/sat_config.h | 1 + src/sat/smt/euf_proof.cpp | 3 +- src/sat/smt/euf_proof_checker.cpp | 1 + 9 files changed, 166 insertions(+), 5 deletions(-) create mode 100644 examples/python/proofreplay.py diff --git a/examples/python/proofreplay.py b/examples/python/proofreplay.py new file mode 100644 index 000000000..c8c9ff47e --- /dev/null +++ b/examples/python/proofreplay.py @@ -0,0 +1,113 @@ +# This script illustrates uses of proof replay and proof logs over the Python interface. + +from z3 import * + +example1 = """ +(declare-sort T) + +(declare-fun subtype (T T) Bool) + +;; subtype is reflexive +(assert (forall ((x T)) (subtype x x))) + +;; subtype is antisymmetric +(assert (forall ((x T) (y T)) (=> (and (subtype x y) + (subtype y x)) + (= x y)))) +;; subtype is transitive +(assert (forall ((x T) (y T) (z T)) (=> (and (subtype x y) + (subtype y z)) + (subtype x z)))) +;; subtype has the tree-property +(assert (forall ((x T) (y T) (z T)) (=> (and (subtype x z) + (subtype y z)) + (or (subtype x y) + (subtype y x))))) + +;; now we define a simple example using the axiomatization above. +(declare-const obj-type T) +(declare-const int-type T) +(declare-const real-type T) +(declare-const complex-type T) +(declare-const string-type T) + +;; we have an additional axiom: every type is a subtype of obj-type +(assert (forall ((x T)) (subtype x obj-type))) + +(assert (subtype int-type real-type)) +(assert (subtype real-type complex-type)) +(assert (not (subtype string-type real-type))) +(declare-const root-type T) +(assert (subtype obj-type root-type)) +""" + +if __name__ == "__main__": + print("Solve and log inferences") + print("--------------------------------------------------------") + + # inference logging, replay, and checking is supported for + # the core enabled by setting sat.euf = true. + # setting the default tactic to 'sat' bypasses other tactics that could + # end up using different solvers. + set_param("sat.euf", True) + set_param("tactic.default_tactic", "sat") + + # Set a log file to trace inferences + set_param("sat.smt.proof", "proof_log.smt2") + s = Solver() + s.from_string(example1) + print(s.check()) + print(s.statistics()) + print("Parse the logged inferences and replay them") + print("--------------------------------------------------------") + + # Reset the log file to an invalid (empty) file name. + set_param("sat.smt.proof", "") + + # Turn off proof checking. It is on by default when parsing proof logs. + set_param("solver.proof.check", False) + s = Solver() + onc = OnClause(s, lambda pr, clause : print(pr, clause)) + s.from_file("proof_log.smt2") + + + print("Parse the logged inferences and check them") + print("--------------------------------------------------------") + s = Solver() + + # Now turn on proof checking. It invokes the self-validator. + # The self-validator produces log lines of the form: + # (proofs +tseitin 60 +alldiff 8 +euf 3 +rup 5 +inst 6 -quant 3 -inst 2) + # (verified-smt + # (inst (forall (vars (x T) (y T) (z T)) (or (subtype (:var 2) (:var 1)) ... + # The 'proofs' line summarizes inferences that were self-validated. + # The pair +tseitin 60 indicates that 60 inferences were validated as Tseitin + # encodings. + # The pair -inst 2 indicates that two quantifier instantiations were not self-validated + # They were instead validated using a call to SMT solving. A log for an smt invocation + # is exemplified in the next line. + # Note that the pair +inst 6 indicates that 6 quantifier instantations were validated + # using a syntactic (cheap) check. Some quantifier instantiations based on quantifier elimination + # are not simple substitutions and therefore a simple syntactic check does not suffice. + set_param("solver.proof.check", True) + s.from_file("proof_log.smt2") + + print("Verify and self-validate on the fly") + print("--------------------------------------------------------") + set_param("sat.smt.proof.check", True) + s = Solver() + s.from_string(example1) + print(s.check()) + print(s.statistics()) + + print("Verify and self-validate on the fly, but don't check rup") + print("--------------------------------------------------------") + set_param("sat.smt.proof.check", True) + set_param("sat.smt.proof.check_rup", False) + s = Solver() + s.from_string(example1) + print(s.check()) + print(s.statistics()) + + + diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index ab285be06..2f0780d58 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -931,6 +931,14 @@ extern "C" { on_clause_eh(user_ctx, of_expr(pr.get()), of_ast_vector(literals)); }; to_solver_ref(s)->register_on_clause(user_context, _on_clause); + auto& solver = *to_solver(s); + + if (!solver.m_cmd_context) { + solver.m_cmd_context = alloc(cmd_context, false, &(mk_c(c)->m())); + install_proof_cmds(*solver.m_cmd_context); + init_proof_cmds(*solver.m_cmd_context); + } + solver.m_cmd_context->get_proof_cmds()->register_on_clause(user_context, _on_clause); Z3_CATCH; } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 61e3b2ecc..15b5df0d1 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -99,6 +99,7 @@ public: virtual void end_infer() = 0; virtual void end_deleted() = 0; virtual void updt_params(params_ref const& p) = 0; + virtual void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) = 0; }; diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp index e544d353b..bf12157c1 100644 --- a/src/cmd_context/extra_cmds/proof_cmds.cpp +++ b/src/cmd_context/extra_cmds/proof_cmds.cpp @@ -227,13 +227,34 @@ class proof_cmds_imp : public proof_cmds { scoped_ptr m_checker; scoped_ptr m_saver; scoped_ptr m_trimmer; + user_propagator::on_clause_eh_t m_on_clause_eh; + void* m_on_clause_ctx = nullptr; + expr_ref m_assumption, m_del; euf::smt_proof_checker& checker() { params_ref p; if (!m_checker) m_checker = alloc(euf::smt_proof_checker, m, p); return *m_checker; } proof_saver& saver() { if (!m_saver) m_saver = alloc(proof_saver, ctx); return *m_saver; } proof_trim& trim() { if (!m_trimmer) m_trimmer = alloc(proof_trim, ctx); return *m_trimmer; } + + expr_ref assumption() { + if (!m_assumption) + m_assumption = m.mk_app(symbol("assumption"), 0, nullptr, m.mk_proof_sort()); + return m_assumption; + } + + expr_ref del() { + if (!m_del) + m_del = m.mk_app(symbol("del"), 0, nullptr, m.mk_proof_sort()); + return m_del; + } public: - proof_cmds_imp(cmd_context& ctx): ctx(ctx), m(ctx.m()), m_lits(m), m_proof_hint(m) { + proof_cmds_imp(cmd_context& ctx): + ctx(ctx), + m(ctx.m()), + m_lits(m), + m_proof_hint(m), + m_assumption(m), + m_del(m) { updt_params(gparams::get_module("solver")); } @@ -251,6 +272,8 @@ public: saver().assume(m_lits); if (m_trim) trim().assume(m_lits); + if (m_on_clause_eh) + m_on_clause_eh(m_on_clause_ctx, assumption(), m_lits.size(), m_lits.data()); m_lits.reset(); m_proof_hint.reset(); } @@ -262,6 +285,8 @@ public: saver().infer(m_lits, m_proof_hint); if (m_trim) trim().infer(m_lits, m_proof_hint); + if (m_on_clause_eh) + m_on_clause_eh(m_on_clause_ctx, m_proof_hint, m_lits.size(), m_lits.data()); m_lits.reset(); m_proof_hint.reset(); } @@ -273,6 +298,8 @@ public: saver().del(m_lits); if (m_trim) trim().del(m_lits); + if (m_on_clause_eh) + m_on_clause_eh(m_on_clause_ctx, del(), m_lits.size(), m_lits.data()); m_lits.reset(); m_proof_hint.reset(); } @@ -285,6 +312,12 @@ public: if (m_trim) trim().updt_params(p); } + + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause_eh) override { + m_on_clause_ctx = ctx; + m_on_clause_eh = on_clause_eh; + } + }; @@ -344,3 +377,7 @@ void install_proof_cmds(cmd_context & ctx) { ctx.insert(alloc(infer_cmd)); ctx.insert(alloc(assume_cmd)); } + +void init_proof_cmds(cmd_context& ctx) { + get(ctx); +} diff --git a/src/cmd_context/extra_cmds/proof_cmds.h b/src/cmd_context/extra_cmds/proof_cmds.h index 9625e93ad..bc2c84d47 100644 --- a/src/cmd_context/extra_cmds/proof_cmds.h +++ b/src/cmd_context/extra_cmds/proof_cmds.h @@ -33,4 +33,4 @@ Notes: class cmd_context; void install_proof_cmds(cmd_context & ctx); - +void init_proof_cmds(cmd_context& ctx); diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 2330fe401..32d764658 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -200,8 +200,9 @@ namespace sat { m_smt_proof = p.smt_proof(); m_smt_proof_check = p.smt_proof_check(); m_smt_proof_check_rup = p.smt_proof_check_rup(); + m_drat_disable = p.drat_disable(); m_drat = - !p.drat_disable() && p.threads() == 1 && + !m_drat_disable && p.threads() == 1 && (sp.lemmas2console() || m_drat_check_unsat || m_drat_file.is_non_empty_string() || diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 2d609b1bc..ae19c63ea 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -175,6 +175,7 @@ namespace sat { // drat proofs bool m_drat; + bool m_drat_disable; bool m_drat_binary; symbol m_drat_file; symbol m_smt_proof; diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 906e6e068..742e00cd7 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -25,7 +25,7 @@ namespace euf { if (m_proof_initialized) return; - if (m_on_clause) + if (m_on_clause && !s().get_config().m_drat_disable) s().set_drat(true); if (!s().get_config().m_drat) @@ -39,7 +39,6 @@ namespace euf { get_drat().add_theory(get_id(), symbol("euf")); get_drat().add_theory(m.get_basic_family_id(), symbol("bool")); - 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); diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp index 79f7e6880..2d4f67cd2 100644 --- a/src/sat/smt/euf_proof_checker.cpp +++ b/src/sat/smt/euf_proof_checker.cpp @@ -372,6 +372,7 @@ namespace euf { 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("quant"), this); pc.register_plugin(symbol("fpa"), this); }