From 107981f099f478cb278d5b4c2c9181515e8c6769 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 28 Sep 2022 10:40:43 -0700 Subject: [PATCH] update proof formats for new core - update proof format for quantifier instantiation to track original literals - update proof replay tools with ability to extract proof object The formats and features are subject to heavy revisions. Example ``` (set-option :sat.euf true) (set-option :sat.smt.proof eufproof.smt2) (declare-fun f (Int) Int) (declare-const x Int) (assert (or (= (f (f (f x))) x) (= (f (f x)) x))) (assert (not (= (f (f (f (f (f (f x)))))) x))) (check-sat) ``` eufproof.smt2 is: ``` (declare-fun x () Int) (declare-fun f (Int) Int) (define-const $24 Int (f x)) (define-const $25 Int (f $24)) (define-const $26 Int (f $25)) (define-const $27 Bool (= $26 x)) (define-const $28 Bool (= $25 x)) (assume $27 $28) (define-const $30 Int (f $26)) (define-const $31 Int (f $30)) (define-const $32 Int (f $31)) (define-const $33 Bool (= $32 x)) (assume (not $33)) (declare-fun rup () Proof) (infer (not $33) rup) (declare-fun euf (Bool Bool Proof Proof Proof Proof) Proof) (declare-fun cc (Bool) Proof) (define-const $42 Bool (= $32 $30)) (define-const $43 Proof (cc $42)) (define-const $40 Bool (= $31 $24)) (define-const $41 Proof (cc $40)) (define-const $38 Bool (= $30 $25)) (define-const $39 Proof (cc $38)) (define-const $36 Bool (= $24 $26)) (define-const $37 Proof (cc $36)) (define-const $34 Bool (not $33)) (define-const $44 Proof (euf $34 $28 $37 $39 $41 $43)) (infer (not $28) $33 $44) (infer (not $28) rup) (infer $27 rup) (declare-fun euf (Bool Bool Proof Proof Proof) Proof) (define-const $49 Bool (= $32 $26)) (define-const $50 Proof (cc $49)) (define-const $47 Bool (= $31 $25)) (define-const $48 Proof (cc $47)) (define-const $45 Bool (= $24 $30)) (define-const $46 Proof (cc $45)) (define-const $51 Proof (euf $34 $27 $46 $48 $50)) (infer $33 $51) (infer rup) ``` Example of inspecting proof from Python: ``` from z3 import * def parse(file): s = Solver() set_option("solver.proof.save", True) set_option("solver.proof.check", False) s.from_file(file) for step in s.proof().children(): print(step) parse("../eufproof.smt2") ``` Proof checking (self-validation) is on by default. Proof saving is off by default. You can use the proof logs and the proof terms to retrieve quantifier instantiations from the new core. The self-checker contains a few built-in tuned checkers but falls back to self-checking inferred clauses using SMT. --- src/api/api_parsers.cpp | 4 + src/api/api_solver.cpp | 10 ++- src/ast/ast.cpp | 10 +-- src/cmd_context/basic_cmds.cpp | 4 +- src/cmd_context/cmd_context.cpp | 2 + src/cmd_context/cmd_context.h | 5 +- src/cmd_context/extra_cmds/proof_cmds.cpp | 83 ++++++++++++++++--- src/muz/spacer/spacer_iuc_solver.h | 5 +- src/opt/opt_context.cpp | 2 +- src/opt/opt_context.h | 3 +- src/opt/opt_solver.cpp | 2 +- src/opt/opt_solver.h | 2 +- src/params/solver_params.pyg | 2 + src/sat/sat_solver/inc_sat_solver.cpp | 5 +- src/sat/smt/arith_axioms.cpp | 47 ++++++----- src/sat/smt/arith_diagnostics.cpp | 10 +++ src/sat/smt/arith_proof_checker.h | 10 +-- src/sat/smt/arith_solver.h | 2 + src/sat/smt/euf_proof.cpp | 26 +++--- src/sat/smt/euf_proof_checker.cpp | 44 ++++++++-- src/sat/smt/euf_solver.h | 2 +- src/sat/smt/q_ematch.cpp | 2 +- src/sat/smt/q_mbi.cpp | 17 +--- src/sat/smt/q_solver.cpp | 45 ++++++---- src/sat/smt/q_solver.h | 19 +++-- src/sat/smt/sat_th.cpp | 15 ++-- src/sat/smt/sat_th.h | 5 +- src/smt/smt_solver.cpp | 2 +- src/solver/check_sat_result.cpp | 13 ++- src/solver/check_sat_result.h | 18 ++-- src/solver/combined_solver.cpp | 9 +- src/solver/solver.h | 2 +- src/solver/solver_na2as.cpp | 2 +- src/solver/solver_na2as.h | 1 - src/solver/solver_pool.cpp | 4 +- src/solver/tactic2solver.cpp | 6 +- .../fd_solver/bounded_int2bv_solver.cpp | 2 +- src/tactic/fd_solver/enum2bv_solver.cpp | 2 +- src/tactic/fd_solver/pb2bv_solver.cpp | 2 +- src/tactic/fd_solver/smtfd_solver.cpp | 2 +- 40 files changed, 295 insertions(+), 153 deletions(-) diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 31ae28f47..00fe1cd8b 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -27,6 +27,7 @@ Revision History: #include "solver/solver_na2as.h" #include "muz/fp/dl_cmds.h" #include "opt/opt_cmds.h" +#include "cmd_context/extra_cmds/proof_cmds.h" @@ -42,6 +43,7 @@ extern "C" { ast_manager& m = c.m(); ctx = alloc(cmd_context, false, &(m)); install_dl_cmds(*ctx.get()); + install_proof_cmds(*ctx.get()); install_opt_cmds(*ctx.get()); install_smt2_extra_cmds(*ctx.get()); ctx->register_plist(); @@ -175,6 +177,7 @@ extern "C" { ast_manager& m = mk_c(c)->m(); scoped_ptr ctx = alloc(cmd_context, false, &(m)); install_dl_cmds(*ctx.get()); + install_proof_cmds(*ctx.get()); install_opt_cmds(*ctx.get()); install_smt2_extra_cmds(*ctx.get()); ctx->register_plist(); @@ -233,6 +236,7 @@ extern "C" { auto* ctx = alloc(cmd_context, false, &(mk_c(c)->m())); mk_c(c)->cmd() = ctx; install_dl_cmds(*ctx); + install_proof_cmds(*ctx); install_opt_cmds(*ctx); install_smt2_extra_cmds(*ctx); ctx->register_plist(); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index a56ca3d3c..5048f39fe 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -43,6 +43,7 @@ Revision History: #include "sat/sat_solver.h" #include "sat/tactic/goal2sat.h" #include "sat/tactic/sat2goal.h" +#include "cmd_context/extra_cmds/proof_cmds.h" extern "C" { @@ -257,8 +258,10 @@ extern "C" { void solver_from_stream(Z3_context c, Z3_solver s, std::istream& is) { auto& solver = *to_solver(s); - if (!solver.m_cmd_context) + if (!solver.m_cmd_context) { solver.m_cmd_context = alloc(cmd_context, false, &(mk_c(c)->m())); + install_proof_cmds(*solver.m_cmd_context); + } auto& ctx = solver.m_cmd_context; ctx->set_ignore_check(true); std::stringstream errstrm; @@ -270,6 +273,7 @@ extern "C" { return; } + bool initialized = to_solver(s)->m_solver.get() != nullptr; if (!initialized) init_solver(c, s); @@ -277,6 +281,10 @@ extern "C" { to_solver(s)->assert_expr(e); ctx->reset_tracked_assertions(); to_solver_ref(s)->set_model_converter(ctx->get_model_converter()); + auto* ctx_s = ctx->get_solver(); + if (ctx_s && ctx_s->get_proof()) + to_solver_ref(s)->set_proof(ctx_s->get_proof()); + } static void solver_from_dimacs_stream(Z3_context c, Z3_solver s, std::istream& is) { diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 38f4dcf05..f9bdc3414 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -856,11 +856,11 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren case PR_MODUS_PONENS_OEQ: return mk_proof_decl("mp~", k, 2, m_mp_oeq_decl); case PR_TH_LEMMA: return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_decls); case PR_HYPER_RESOLVE: return mk_proof_decl("hyper-res", k, num_parents, m_hyper_res_decl0); - case PR_ASSUMPTION_ADD: return mk_proof_decl("add-assume", k, num_parents, m_assumption_add_decl); - case PR_LEMMA_ADD: return mk_proof_decl("add-lemma", k, num_parents, m_lemma_add_decl); - case PR_TH_ASSUMPTION_ADD: return mk_proof_decl("add-th-assume", k, num_parents, m_th_assumption_add_decl); - case PR_TH_LEMMA_ADD: return mk_proof_decl("add-th-lemma", k, num_parents, m_th_lemma_add_decl); - case PR_REDUNDANT_DEL: return mk_proof_decl("del-redundant", k, num_parents, m_redundant_del_decl); + case PR_ASSUMPTION_ADD: return mk_proof_decl("assume", k, num_parents, m_assumption_add_decl); + case PR_LEMMA_ADD: return mk_proof_decl("infer", k, num_parents, m_lemma_add_decl); + case PR_TH_ASSUMPTION_ADD: return mk_proof_decl("th-assume", k, num_parents, m_th_assumption_add_decl); + case PR_TH_LEMMA_ADD: return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_add_decl); + case PR_REDUNDANT_DEL: return mk_proof_decl("del", k, num_parents, m_redundant_del_decl); case PR_CLAUSE_TRAIL: return mk_proof_decl("proof-trail", k, num_parents, false); default: UNREACHABLE(); diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index b17bc3641..a2757d955 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -177,10 +177,10 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", { if (!ctx.has_manager()) throw cmd_exception("proof is not available"); - if (ctx.ignore_check()) - return; expr_ref pr(ctx.m()); auto* chsr = ctx.get_check_sat_result(); + if (!chsr && ctx.ignore_check()) + return; if (!chsr) throw cmd_exception("proof is not available"); pr = chsr->get_proof(); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 97ae0fbc1..0c38f2e4a 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -604,6 +604,8 @@ void cmd_context::global_params_updated() { if (m_opt) { get_opt()->updt_params(gparams::get_module("opt")); } + if (m_proof_cmds) + m_proof_cmds->updt_params(gparams::get_module("solver")); } void cmd_context::set_produce_models(bool f) { diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 512e367ef..61e3b2ecc 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -96,8 +96,9 @@ public: virtual ~proof_cmds() {} virtual void add_literal(expr* e) = 0; virtual void end_assumption() = 0; - virtual void end_learned() = 0; + virtual void end_infer() = 0; virtual void end_deleted() = 0; + virtual void updt_params(params_ref const& p) = 0; }; @@ -159,6 +160,7 @@ struct builtin_decl { class opt_wrapper : public check_sat_result { public: + opt_wrapper(ast_manager& m): check_sat_result(m) {} virtual bool empty() = 0; virtual void push() = 0; virtual void pop(unsigned n) = 0; @@ -411,6 +413,7 @@ public: sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; } proof_cmds* get_proof_cmds() { return m_proof_cmds.get(); } + solver* get_solver() { return m_solver.get(); } void set_proof_cmds(proof_cmds* pc) { m_proof_cmds = pc; } void set_solver_factory(solver_factory * s); diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp index 505b0a5ed..03cb3f95c 100644 --- a/src/cmd_context/extra_cmds/proof_cmds.cpp +++ b/src/cmd_context/extra_cmds/proof_cmds.cpp @@ -47,6 +47,7 @@ Proof checker for clauses created during search. #include "sat/sat_drat.h" #include "sat/smt/euf_proof_checker.h" #include "cmd_context/cmd_context.h" +#include "params/solver_params.hpp" #include class smt_checker { @@ -166,8 +167,6 @@ public: } m_solver->pop(1); std::cout << "(verified-smt)\n"; - if (proof_hint) - std::cout << "(missed-hint " << mk_pp(proof_hint, m) << ")\n"; add_clause(clause); } @@ -175,15 +174,59 @@ public: add_clause(clause); m_solver->assert_expr(mk_or(clause)); } + + void del(expr_ref_vector const& clause) { + + } + +}; + + +class proof_saver { + cmd_context& ctx; + ast_manager& m; +public: + proof_saver(cmd_context& ctx):ctx(ctx), m(ctx.m()) { + auto* s = ctx.get_solver(); + if (!s) + ctx.set_solver_factory(mk_smt_strategic_solver_factory()); + if (!ctx.get_check_sat_result()) + ctx.set_check_sat_result(ctx.get_solver()); + } + + void assume(expr_ref_vector const& clause) { + ctx.get_solver()->log_inference(m.mk_assumption_add(nullptr, mk_or(clause))); + } + + void del(expr_ref_vector const& clause) { + ctx.get_solver()->log_inference(m.mk_redundant_del(mk_or(clause))); + } + + void infer(expr_ref_vector const& clause, app* hint) { + ctx.get_solver()->log_inference(m.mk_lemma_add(hint, mk_or(clause))); + } + }; class proof_cmds_imp : public proof_cmds { + cmd_context& ctx; ast_manager& m; expr_ref_vector m_lits; app_ref m_proof_hint; - smt_checker m_checker; + bool m_check = true; + bool m_save = false; + bool m_trim = false; + scoped_ptr m_checker; + scoped_ptr m_saver; + + smt_checker& checker() { if (!m_checker) m_checker = alloc(smt_checker, m); return *m_checker; } + proof_saver& saver() { if (!m_saver) m_saver = alloc(proof_saver, ctx); return *m_saver; } + + public: - proof_cmds_imp(ast_manager& m): m(m), m_lits(m), m_proof_hint(m), m_checker(m) {} + proof_cmds_imp(cmd_context& ctx): ctx(ctx), m(ctx.m()), m_lits(m), m_proof_hint(m) { + updt_params(gparams::get_module("solver")); + } void add_literal(expr* e) override { if (m.is_proof(e)) @@ -193,27 +236,43 @@ public: } void end_assumption() override { - m_checker.assume(m_lits); + if (m_check) + checker().assume(m_lits); + if (m_save) + saver().assume(m_lits); m_lits.reset(); m_proof_hint.reset(); } - void end_learned() override { - m_checker.check(m_lits, m_proof_hint); + void end_infer() override { + if (m_check) + checker().check(m_lits, m_proof_hint); + if (m_save) + saver().infer(m_lits, m_proof_hint); m_lits.reset(); m_proof_hint.reset(); } void end_deleted() override { + if (m_check) + checker().del(m_lits); + if (m_save) + saver().del(m_lits); m_lits.reset(); m_proof_hint.reset(); } + + void updt_params(params_ref const& p) { + solver_params sp(p); + m_check = sp.proof_check(); + m_save = sp.proof_save(); + } }; static proof_cmds& get(cmd_context& ctx) { if (!ctx.get_proof_cmds()) - ctx.set_proof_cmds(alloc(proof_cmds_imp, ctx.m())); + ctx.set_proof_cmds(alloc(proof_cmds_imp, ctx)); return *ctx.get_proof_cmds(); } @@ -248,9 +307,9 @@ public: }; // learned/redundant clause -class learn_cmd : public cmd { +class infer_cmd : public cmd { public: - learn_cmd():cmd("learn") {} + infer_cmd():cmd("infer") {} char const* get_usage() const override { return "+"; } char const* get_descr(cmd_context& ctx) const override { return "proof command for learned (redundant) clauses"; } unsigned get_arity() const override { return VAR_ARITY; } @@ -259,11 +318,11 @@ public: void failure_cleanup(cmd_context & ctx) override {} cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { return CPK_EXPR; } void set_next_arg(cmd_context & ctx, expr * arg) override { get(ctx).add_literal(arg); } - void execute(cmd_context& ctx) override { get(ctx).end_learned(); } + void execute(cmd_context& ctx) override { get(ctx).end_infer(); } }; void install_proof_cmds(cmd_context & ctx) { ctx.insert(alloc(del_cmd)); - ctx.insert(alloc(learn_cmd)); + ctx.insert(alloc(infer_cmd)); ctx.insert(alloc(assume_cmd)); } diff --git a/src/muz/spacer/spacer_iuc_solver.h b/src/muz/spacer/spacer_iuc_solver.h index 8b75adf88..be1a3879b 100644 --- a/src/muz/spacer/spacer_iuc_solver.h +++ b/src/muz/spacer/spacer_iuc_solver.h @@ -42,7 +42,6 @@ private: }; friend struct def_manager; - ast_manager& m; solver& m_solver; app_ref_vector m_proxies; unsigned m_num_proxies; @@ -72,7 +71,7 @@ public: iuc_solver(solver &solver, unsigned iuc, unsigned iuc_arith, bool print_farkas_stats, bool old_hyp_reducer, bool split_literals = false) : - m(solver.get_manager()), + solver(m), m_solver(solver), m_proxies(m), m_num_proxies(0), @@ -150,7 +149,7 @@ public: void get_unsat_core(expr_ref_vector &r) override; void get_model_core(model_ref &m) override {m_solver.get_model(m);} - proof *get_proof() override {return m_solver.get_proof();} + proof *get_proof_core() override {return m_solver.get_proof_core();} std::string reason_unknown() const override { return m_solver.reason_unknown(); } void set_reason_unknown(char const* msg) override { m_solver.set_reason_unknown(msg); } void get_labels(svector &r) override { m_solver.get_labels(r); } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index bc41e0c6d..ba31d74cf 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -124,7 +124,7 @@ namespace opt { } context::context(ast_manager& m): - m(m), + opt_wrapper(m), m_arith(m), m_bv(m), m_hard_constraints(m), diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 8b0e8eab1..a93400592 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -164,7 +164,6 @@ namespace opt { unsigned get_index(symbol const& id) { return m_indices[id]; } }; - ast_manager& m; on_model_t m_on_model_ctx; std::function m_on_model_eh; bool m_calling_on_model = false; @@ -226,7 +225,7 @@ namespace opt { void get_box_model(model_ref& _m, unsigned index) override; void fix_model(model_ref& _m) override; void collect_statistics(statistics& stats) const override; - proof* get_proof() override { return nullptr; } + proof* get_proof_core() override { return nullptr; } void get_labels(svector & r) override; void get_unsat_core(expr_ref_vector & r) override; std::string reason_unknown() const override; diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 01975464a..64bf389bf 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -365,7 +365,7 @@ namespace opt { m = m_last_model.get(); } - proof * opt_solver::get_proof() { + proof * opt_solver::get_proof_core() { return m_context.get_proof(); } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index e71287400..bd83f06c8 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -97,7 +97,7 @@ namespace opt { lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override; void get_unsat_core(expr_ref_vector & r) override; void get_model_core(model_ref & _m) override; - proof * get_proof() override; + proof * get_proof_core() override; std::string reason_unknown() const override; void set_reason_unknown(char const* msg) override; void get_labels(svector & r) override; diff --git a/src/params/solver_params.pyg b/src/params/solver_params.pyg index b475d368d..6e33ca6d7 100644 --- a/src/params/solver_params.pyg +++ b/src/params/solver_params.pyg @@ -8,5 +8,7 @@ def_module_params('solver', ('lemmas2console', BOOL, False, 'print lemmas during search'), ('instantiations2console', BOOL, False, 'print quantifier instantiations to the console'), ('axioms2files', BOOL, False, 'print negated theory axioms to separate files during search'), + ('proof.check', BOOL, True, 'check proof logs'), + ('proof.save', BOOL, False, 'save proof log into a proof object that can be extracted using (get-proof)'), )) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 981d91072..5c1859258 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -48,7 +48,6 @@ Notes: // incremental SAT solver. class inc_sat_solver : public solver { - ast_manager& m; mutable sat::solver m_solver; stacked_value m_has_uninterpreted; goal2sat m_goal2sat; @@ -87,7 +86,7 @@ class inc_sat_solver : public solver { bool is_internalized() const { return m_fmls_head == m_fmls.size(); } public: inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_mode): - m(m), + solver(m), m_solver(p, m.limit()), m_has_uninterpreted(false), m_fmls(m), @@ -405,7 +404,7 @@ public: return result; } - proof * get_proof() override { + proof * get_proof_core() override { return nullptr; } diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index 4d1afb4cc..2b02015e0 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -251,6 +251,17 @@ namespace arith { if (hi_sup != end) mk_bound_axiom(b, *hi_sup); } + void solver::add_farkas_clause(sat::literal l1, sat::literal l2) { + arith_proof_hint* bound_params = nullptr; + if (ctx.use_drat()) { + m_arith_hint.set_type(ctx, hint_type::farkas_h); + m_arith_hint.add_lit(rational(1), ~l1); + m_arith_hint.add_lit(rational(1), ~l2); + bound_params = m_arith_hint.mk(ctx); + } + add_clause(l1, l2, bound_params); + } + void solver::mk_bound_axiom(api_bound& b1, api_bound& b2) { literal l1(b1.get_lit()); literal l2(b2.get_lit()); @@ -263,55 +274,45 @@ namespace arith { if (k1 == k2 && kind1 == kind2) return; SASSERT(k1 != k2 || kind1 != kind2); - auto bin_clause = [&](sat::literal l1, sat::literal l2) { - arith_proof_hint* bound_params = nullptr; - if (ctx.use_drat()) { - m_arith_hint.set_type(ctx, hint_type::farkas_h); - m_arith_hint.add_lit(rational(1), ~l1); - m_arith_hint.add_lit(rational(1), ~l2); - bound_params = m_arith_hint.mk(ctx); - } - add_clause(l1, l2, bound_params); - }; if (kind1 == lp_api::lower_t) { if (kind2 == lp_api::lower_t) { if (k2 <= k1) - bin_clause(~l1, l2); + add_farkas_clause(~l1, l2); else - bin_clause(l1, ~l2); + add_farkas_clause(l1, ~l2); } else if (k1 <= k2) // k1 <= k2, k1 <= x or x <= k2 - bin_clause(l1, l2); + add_farkas_clause(l1, l2); else { // k1 > hi_inf, k1 <= x => ~(x <= hi_inf) - bin_clause(~l1, ~l2); + add_farkas_clause(~l1, ~l2); if (v_is_int && k1 == k2 + rational(1)) // k1 <= x or x <= k1-1 - bin_clause(l1, l2); + add_farkas_clause(l1, l2); } } else if (kind2 == lp_api::lower_t) { if (k1 >= k2) // k1 >= lo_inf, k1 >= x or lo_inf <= x - bin_clause(l1, l2); + add_farkas_clause(l1, l2); else { // k1 < k2, k2 <= x => ~(x <= k1) - bin_clause(~l1, ~l2); + add_farkas_clause(~l1, ~l2); if (v_is_int && k1 == k2 - rational(1)) // x <= k1 or k1+l <= x - bin_clause(l1, l2); + add_farkas_clause(l1, l2); } } else { // kind1 == A_UPPER, kind2 == A_UPPER if (k1 >= k2) // k1 >= k2, x <= k2 => x <= k1 - bin_clause(l1, ~l2); + add_farkas_clause(l1, ~l2); else // k1 <= hi_sup , x <= k1 => x <= hi_sup - bin_clause(~l1, l2); + add_farkas_clause(~l1, l2); } } @@ -421,9 +422,9 @@ namespace arith { ge = mk_literal(a.mk_ge(diff, zero)); } ++m_stats.m_assert_diseq; - add_clause(~eq, le); - add_clause(~eq, ge); - add_clause(~le, ~ge, eq); + add_farkas_clause(~eq, le); + add_farkas_clause(~eq, ge); + add_clause(~le, ~ge, eq, explain_triangle_eq(le, ge, eq)); } diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp index 3c3235df1..cba691319 100644 --- a/src/sat/smt/arith_diagnostics.cpp +++ b/src/sat/smt/arith_diagnostics.cpp @@ -133,6 +133,16 @@ namespace arith { return m_arith_hint.mk(ctx); } + arith_proof_hint const* solver::explain_triangle_eq(sat::literal le, sat::literal ge, sat::literal eq) { + if (!ctx.use_drat()) + return nullptr; + m_arith_hint.set_type(ctx, hint_type::implied_eq_h); + m_arith_hint.add_lit(rational(1), le); + m_arith_hint.add_lit(rational(1), ge); + m_arith_hint.add_lit(rational(1), ~eq); + return m_arith_hint.mk(ctx); + } + expr* arith_proof_hint::get_hint(euf::solver& s) const { ast_manager& m = s.get_manager(); family_id fid = m.get_family_id("arith"); diff --git a/src/sat/smt/arith_proof_checker.h b/src/sat/smt/arith_proof_checker.h index 1a8a8df27..56e4cf1f8 100644 --- a/src/sat/smt/arith_proof_checker.h +++ b/src/sat/smt/arith_proof_checker.h @@ -383,14 +383,13 @@ namespace arith { neg.mark(e, true); else pos.mark(e, true); - - if (jst->get_name() != m_farkas && - jst->get_name() != m_bound && - jst->get_name() != m_implied_eq) { + bool is_bound = jst->get_name() == m_bound; + bool is_implied_eq = jst->get_name() == m_implied_eq; + bool is_farkas = jst->get_name() == m_farkas; + if (!is_farkas && !is_bound && !is_implied_eq) { IF_VERBOSE(0, verbose_stream() << "unhandled inference " << mk_pp(jst, m) << "\n"); return false; } - bool is_bound = jst->get_name() == m_bound; bool even = true; rational coeff; expr* x, * y; @@ -436,7 +435,6 @@ namespace arith { if (check()) return true; - IF_VERBOSE(0, verbose_stream() << "did not check condition\n" << mk_pp(jst, m) << "\n"; display(verbose_stream()); ); return false; } diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index 83c91ac05..2142874d5 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -322,6 +322,7 @@ namespace arith { void mk_bound_axiom(api_bound& b1, api_bound& b2); void mk_power0_axioms(app* t, app* n); void flush_bound_axioms(); + void add_farkas_clause(sat::literal l1, sat::literal l2); // bounds struct compare_bounds { @@ -473,6 +474,7 @@ namespace arith { arith_proof_hint const* explain(hint_type ty, sat::literal lit = sat::null_literal); arith_proof_hint const* explain_implied_eq(euf::enode* a, euf::enode* b); + arith_proof_hint const* explain_triangle_eq(sat::literal le, sat::literal ge, sat::literal eq); void explain_assumptions(); diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index bf8aad44b..99bc99d48 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -92,16 +92,20 @@ namespace euf { expr* eq_proof_hint::get_hint(euf::solver& s) const { ast_manager& m = s.get_manager(); - func_decl_ref cc(m); + func_decl_ref cc(m), cc_comm(m); sort* proof = m.mk_proof_sort(); ptr_buffer sorts; expr_ref_vector args(m); if (m_cc_head < m_cc_tail) { - sort* sorts[2] = { m.mk_bool_sort(), m.mk_bool_sort() }; - cc = m.mk_func_decl(symbol("cc"), 2, sorts, proof); + sort* sorts[1] = { m.mk_bool_sort() }; + cc_comm = m.mk_func_decl(symbol("comm"), 1, sorts, proof); + cc = m.mk_func_decl(symbol("cc"), 1, sorts, proof); } auto cc_proof = [&](bool comm, expr* eq) { - return m.mk_app(cc, m.mk_bool_val(comm), eq); + if (comm) + return m.mk_app(cc_comm, eq); + else + return m.mk_app(cc, eq); }; auto compare_ts = [](cc_justification_record const& a, cc_justification_record const& b) { @@ -168,11 +172,11 @@ namespace euf { if (!visit_clause(out, n, lits)) return; if (st.is_asserted()) - display_redundant(out, n, lits, status2proof_hint(st)); + display_inferred(out, n, lits, status2proof_hint(st)); else if (st.is_deleted()) display_deleted(out, n, lits); else if (st.is_redundant()) - display_redundant(out, n, lits, status2proof_hint(st)); + display_inferred(out, n, lits, status2proof_hint(st)); else if (st.is_input()) display_assume(out, n, lits); else @@ -228,10 +232,12 @@ namespace euf { display_literals(out << "(assume", n, lits) << ")\n"; } - void solver::display_redundant(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint) { - if (proof_hint) - visit_expr(out, proof_hint); - display_hint(display_literals(out << "(learn", n, lits), proof_hint) << ")\n"; + 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()); + visit_expr(out, hint); + display_hint(display_literals(out << "(infer", n, lits), hint) << ")\n"; } void solver::display_deleted(std::ostream& out, unsigned n, literal const* lits) { diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp index 3ddafd00b..d0a4e4ab1 100644 --- a/src/sat/smt/euf_proof_checker.cpp +++ b/src/sat/smt/euf_proof_checker.cpp @@ -20,6 +20,7 @@ Author: #include "ast/ast_ll_pp.h" #include "sat/smt/euf_proof_checker.h" #include "sat/smt/arith_proof_checker.h" +#include namespace euf { @@ -57,6 +58,7 @@ namespace euf { ast_manager& m; basic_union_find m_uf; svector> m_expr2id; + ptr_vector m_id2expr; svector> m_diseqs; unsigned m_ts = 0; @@ -108,10 +110,10 @@ namespace euf { if (ts != m_ts) { id = m_uf.mk_var(); m_expr2id.setx(e->get_id(), {m_ts, id}, {0,0}); + m_id2expr.setx(id, e, nullptr); } return id; - } - + } public: eq_proof_checker(ast_manager& m): m(m) {} @@ -149,15 +151,17 @@ namespace euf { if (!is_app(arg)) return false; app* a = to_app(arg); - if (a->get_num_args() != 2) + if (a->get_num_args() != 1) return false; - if (a->get_name() != symbol("cc")) + if (!m.is_eq(a->get_arg(0), x, y)) return false; - if (!m.is_eq(a->get_arg(1), x, y)) + bool is_cc = a->get_name() == symbol("cc"); + bool is_comm = a->get_name() == symbol("comm"); + if (!is_cc && !is_comm) return false; if (!is_app(x) || !is_app(y)) return false; - if (!congruence(m.is_true(a->get_arg(0)), to_app(x), to_app(y))) { + if (!congruence(!is_cc, to_app(x), to_app(y))) { IF_VERBOSE(0, verbose_stream() << "not congruent " << mk_pp(a, m) << "\n"); return false; } @@ -167,9 +171,27 @@ namespace euf { return false; } } + // check if a disequality is violated. for (auto const& [a, b] : m_diseqs) if (are_equal(a, b)) - return true; + return true; + + // check if some equivalence class contains two distinct values. + for (unsigned v = 0; v < m_uf.get_num_vars(); ++v) { + if (v != m_uf.find(v)) + continue; + unsigned r = v; + expr* val = nullptr; + do { + expr* e = m_id2expr[v]; + if (val && m.are_distinct(e, val)) + return true; + if (m.is_value(e)) + val = e; + v = m_uf.next(v); + } + while (r != v); + } return false; } @@ -201,8 +223,12 @@ namespace euf { 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, units); + if (!m_map.find(a->get_decl()->get_name(), p)) + return false; + if (p->check(clause, a, units)) + return true; + + std::cout << "(missed-hint " << mk_pp(e, m) << ")\n"; return false; } diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index f4867d841..b5d65205c 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -197,7 +197,7 @@ namespace euf { void on_proof(unsigned n, literal const* lits, sat::status st); std::ostream& display_literals(std::ostream& out, unsigned n, sat::literal const* lits); void display_assume(std::ostream& out, unsigned n, literal const* lits); - void display_redundant(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint); + void display_inferred(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint); void display_deleted(std::ostream& out, unsigned n, literal const* lits); std::ostream& display_hint(std::ostream& out, expr* proof_hint); expr_ref status2proof_hint(sat::status st); diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index a4093cdb7..4a834d355 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -387,7 +387,7 @@ namespace q { m_qs.log_instantiation(lits, &j); euf::th_proof_hint* ph = nullptr; if (ctx.use_drat()) - ph = q_proof_hint::mk(ctx, j.m_clause.size(), j.m_binding); + ph = q_proof_hint::mk(ctx, lits, j.m_clause.size(), j.m_binding); m_qs.add_clause(lits, ph); } diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 8be75f03c..0802f71c9 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -70,19 +70,10 @@ namespace q { m_max_cex += ctx.get_config().m_mbqi_max_cexs; for (auto const& [qlit, fml, inst, generation] : m_instantiations) { euf::solver::scoped_generation sg(ctx, generation + 1); - sat::literal lit = ctx.mk_literal(fml); - euf::th_proof_hint* ph = nullptr; - if (!inst.empty()) { - ph = q_proof_hint::mk(ctx, inst.size(), inst.data()); - sat::literal_vector lits; - lits.push_back(~qlit); - lits.push_back(~lit); - m_qs.add_clause(lits, ph); - } - else { - m_qs.add_clause(~qlit, ~lit); - } - m_qs.log_instantiation(~qlit, ~lit); + sat::literal lit = ~ctx.mk_literal(fml); + auto* ph = q_proof_hint::mk(ctx, ~qlit, lit, inst.size(), inst.data()); + m_qs.add_clause(~qlit, lit, ph); + m_qs.log_instantiation(~qlit, lit); } m_instantiations.reset(); if (result != l_true) diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 0a8ca5085..c99311f4e 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -364,36 +364,49 @@ namespace q { } } - q_proof_hint* q_proof_hint::mk(euf::solver& s, unsigned n, euf::enode* const* bindings) { - auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n)); - q_proof_hint* ph = new (mem) q_proof_hint(); - ph->m_num_bindings = n; + q_proof_hint* q_proof_hint::mk(euf::solver& s, sat::literal_vector const& lits, unsigned n, euf::enode* const* bindings) { + auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n, lits.size())); + q_proof_hint* ph = new (mem) q_proof_hint(n, lits.size()); for (unsigned i = 0; i < n; ++i) ph->m_bindings[i] = bindings[i]->get_expr(); + for (unsigned i = 0; i < lits.size(); ++i) + ph->m_literals[i] = lits[i]; return ph; } - q_proof_hint* q_proof_hint::mk(euf::solver& s, unsigned n, expr* const* bindings) { - auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n)); - q_proof_hint* ph = new (mem) q_proof_hint(); - ph->m_num_bindings = n; + q_proof_hint* q_proof_hint::mk(euf::solver& s, sat::literal l1, sat::literal l2, unsigned n, expr* const* bindings) { + auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n, 2)); + q_proof_hint* ph = new (mem) q_proof_hint(n, 2); for (unsigned i = 0; i < n; ++i) ph->m_bindings[i] = bindings[i]; + ph->m_literals[0] = l1; + ph->m_literals[1] = l2; return ph; } expr* q_proof_hint::get_hint(euf::solver& s) const { ast_manager& m = s.get_manager(); expr_ref_vector args(m); - sort_ref_vector sorts(m); - for (unsigned i = 0; i < m_num_bindings; ++i) { - args.push_back(m_bindings[i]); - sorts.push_back(args.back()->get_sort()); - } + ptr_buffer sorts; + expr_ref binding(m); sort* range = m.mk_proof_sort(); - func_decl* d = m.mk_func_decl(symbol("inst"), args.size(), sorts.data(), range); - expr* r = m.mk_app(d, args); - return r; + func_decl* d; + for (unsigned i = 0; i < m_num_bindings; ++i) + args.push_back(m_bindings[i]); + for (expr* arg : args) + sorts.push_back(arg->get_sort()); + d = m.mk_func_decl(symbol("bind"), args.size(), sorts.data(), range); + binding = m.mk_app(d, args); + args.reset(); + sorts.reset(); + for (unsigned i = 0; i < m_num_literals; ++i) + args.push_back(s.literal2expr(~m_literals[i])); + args.push_back(binding); + for (expr* arg : args) + sorts.push_back(arg->get_sort()); + + d = m.mk_func_decl(symbol("inst"), args.size(), sorts.data(), range); + return m.mk_app(d, args); } } diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h index ee2e47111..3a95a00be 100644 --- a/src/sat/smt/q_solver.h +++ b/src/sat/smt/q_solver.h @@ -30,12 +30,19 @@ namespace euf { namespace q { struct q_proof_hint : public euf::th_proof_hint { - unsigned m_num_bindings; - expr* m_bindings[0]; - q_proof_hint() {} - static size_t get_obj_size(unsigned num_bindings) { return sizeof(q_proof_hint) + num_bindings*sizeof(expr*); } - static q_proof_hint* mk(euf::solver& s, unsigned n, euf::enode* const* bindings); - static q_proof_hint* mk(euf::solver& s, unsigned n, expr* const* bindings); + unsigned m_num_bindings; + unsigned m_num_literals; + sat::literal* m_literals; + expr* m_bindings[0]; + + q_proof_hint(unsigned b, unsigned l) { + m_num_bindings = b; + m_num_literals = l; + m_literals = reinterpret_cast(m_bindings + m_num_bindings); + } + static size_t get_obj_size(unsigned num_bindings, unsigned num_lits) { return sizeof(q_proof_hint) + num_bindings*sizeof(expr*) + num_lits*sizeof(sat::literal); } + static q_proof_hint* mk(euf::solver& s, sat::literal_vector const& lits, unsigned n, euf::enode* const* bindings); + static q_proof_hint* mk(euf::solver& s, sat::literal l1, sat::literal l2, unsigned n, expr* const* bindings); expr* get_hint(euf::solver& s) const override; }; diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 3267f0940..00a23d903 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -143,20 +143,16 @@ namespace euf { is_new = true; return is_new; } - - bool th_euf_solver::add_clause(sat::literal a, sat::literal b) { - sat::literal lits[2] = { a, b }; - return add_clause(2, lits); - } - - bool th_euf_solver::add_clause(sat::literal a, sat::literal b, th_proof_hint const* ps) { + + bool th_euf_solver::add_clause(sat::literal a, sat::literal b, th_proof_hint const* ps) { + SASSERT(ps); sat::literal lits[2] = { a, b }; return add_clause(2, lits, ps); } - bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c) { + bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, th_proof_hint const* ps) { sat::literal lits[3] = { a, b, c }; - return add_clause(3, lits); + return add_clause(3, lits, ps); } bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d) { @@ -165,6 +161,7 @@ namespace euf { } bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps) { + //SASSERT(!ctx.use_drat() || ps); - very far from true, and isn't a requirement bool was_true = false; for (unsigned i = 0; i < n; ++i) was_true |= is_true(lits[i]); diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 8289418fc..a76b86cfd 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -160,9 +160,8 @@ namespace euf { bool add_unit(sat::literal lit); bool add_units(sat::literal_vector const& lits); bool add_clause(sat::literal lit) { return add_unit(lit); } - bool add_clause(sat::literal a, sat::literal b); - bool add_clause(sat::literal a, sat::literal b, th_proof_hint const* ps); - bool add_clause(sat::literal a, sat::literal b, sat::literal c); + 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_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); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 5064ed7ef..61c6de377 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -289,7 +289,7 @@ namespace { m_context.get_model(m); } - proof * get_proof() override { + proof * get_proof_core() override { return m_context.get_proof(); } diff --git a/src/solver/check_sat_result.cpp b/src/solver/check_sat_result.cpp index d29e0f2bd..e946dd430 100644 --- a/src/solver/check_sat_result.cpp +++ b/src/solver/check_sat_result.cpp @@ -39,8 +39,19 @@ void check_sat_result::set_reason_unknown(event_handler& eh) { } } +proof* check_sat_result::get_proof() { + if (!m_log.empty() && !m_proof) { + app* last = m_log.back(); + m_log.push_back(to_app(m.get_fact(last))); + m_proof = m.mk_clause_trail(m_log.size(), m_log.data()); + } + if (m_proof) + return m_proof.get(); + return get_proof_core(); +} simple_check_sat_result::simple_check_sat_result(ast_manager & m): + check_sat_result(m), m_core(m), m_proof(m) { } @@ -66,7 +77,7 @@ void simple_check_sat_result::get_model_core(model_ref & m) { m = nullptr; } -proof * simple_check_sat_result::get_proof() { +proof * simple_check_sat_result::get_proof_core() { return m_proof; } diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h index 86941f590..e00b53cc9 100644 --- a/src/solver/check_sat_result.h +++ b/src/solver/check_sat_result.h @@ -39,12 +39,15 @@ Notes: */ class check_sat_result { protected: - unsigned m_ref_count; - lbool m_status; + ast_manager& m; + proof_ref_vector m_log; + proof_ref m_proof; + unsigned m_ref_count = 0; + lbool m_status = l_undef; model_converter_ref m_mc0; - double m_time; + double m_time = 0; public: - check_sat_result():m_ref_count(0), m_status(l_undef), m_time(0) {} + check_sat_result(ast_manager& m): m(m), m_log(m), m_proof(m) {} virtual ~check_sat_result() = default; void inc_ref() { m_ref_count++; } void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); } @@ -59,7 +62,10 @@ public: get_model_core(m); if (m && mc0()) (*mc0())(m); } - virtual proof * get_proof() = 0; + void log_inference(proof* p) { m_log.push_back(p); } + void set_proof(proof* p) { m_proof = p; } + proof* get_proof(); + virtual proof * get_proof_core() = 0; virtual std::string reason_unknown() const = 0; virtual void set_reason_unknown(char const* msg) = 0; void set_reason_unknown(event_handler& eh); @@ -97,7 +103,7 @@ struct simple_check_sat_result : public check_sat_result { void collect_statistics(statistics & st) const override; void get_unsat_core(expr_ref_vector & r) override; void get_model_core(model_ref & m) override; - proof * get_proof() override; + proof * get_proof_core() override; std::string reason_unknown() const override; void get_labels(svector & r) override; void set_reason_unknown(char const* msg) override { m_unknown = msg; } diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 6e414816f..76e6138ab 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -115,7 +115,8 @@ private: } public: - combined_solver(solver * s1, solver * s2, params_ref const & p) { + combined_solver(solver * s1, solver * s2, params_ref const & p): + solver(s1->get_manager()) { m_solver1 = s1; m_solver2 = s2; updt_local_params(p); @@ -318,11 +319,11 @@ public: return m_solver2->get_trail(max_level); } - proof * get_proof() override { + proof * get_proof_core() override { if (m_use_solver1_results) - return m_solver1->get_proof(); + return m_solver1->get_proof_core(); else - return m_solver2->get_proof(); + return m_solver2->get_proof_core(); } std::string reason_unknown() const override { diff --git a/src/solver/solver.h b/src/solver/solver.h index 8b7d56a8c..8a4bec538 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -52,7 +52,7 @@ class solver : public check_sat_result, public user_propagator::core { params_ref m_params; symbol m_cancel_backup_file; public: - solver() {} + solver(ast_manager& m): check_sat_result(m) {} /** \brief Creates a clone of the solver. diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index 4951f8833..605a32ae1 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -24,7 +24,7 @@ Notes: solver_na2as::solver_na2as(ast_manager & m): - m(m), + solver(m), m_assumptions(m) { } diff --git a/src/solver/solver_na2as.h b/src/solver/solver_na2as.h index c8340bd6e..81a58fb39 100644 --- a/src/solver/solver_na2as.h +++ b/src/solver/solver_na2as.h @@ -25,7 +25,6 @@ Notes: class solver_na2as : public solver { protected: - ast_manager & m; expr_ref_vector m_assumptions; unsigned_vector m_scopes; void restore_assumptions(unsigned old_sz); diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index bbc46c9c8..f5760bde3 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -102,10 +102,10 @@ public: } - proof * get_proof() override { + proof * get_proof_core() override { scoped_watch _t_(m_pool.m_proof_watch); if (!m_proof.get()) { - m_proof = m_base->get_proof(); + m_proof = m_base->get_proof_core(); if (m_proof) { elim_aux_assertions pc(m_pred); pc(m, m_proof, m_proof); diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index b178929bd..6e34758e6 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -70,7 +70,7 @@ public: void collect_statistics(statistics & st) const override; void get_unsat_core(expr_ref_vector & r) override; void get_model_core(model_ref & m) override; - proof * get_proof() override; + proof * get_proof_core() override; std::string reason_unknown() const override; void set_reason_unknown(char const* msg) override; void get_labels(svector & r) override {} @@ -311,9 +311,9 @@ void tactic2solver::get_model_core(model_ref & m) { } } -proof * tactic2solver::get_proof() { +proof * tactic2solver::get_proof_core() { if (m_result.get()) - return m_result->get_proof(); + return m_result->get_proof_core(); else return nullptr; } diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp index bc05a3328..f7974671e 100644 --- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp +++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp @@ -195,7 +195,7 @@ public: mc = concat(mc.get(), m_solver->get_model_converter().get()); return mc; } - proof * get_proof() override { return m_solver->get_proof(); } + proof * get_proof_core() override { return m_solver->get_proof_core(); } std::string reason_unknown() const override { return m_solver->reason_unknown(); } void set_reason_unknown(char const* msg) override { m_solver->set_reason_unknown(msg); } void get_labels(svector & r) override { m_solver->get_labels(r); } diff --git a/src/tactic/fd_solver/enum2bv_solver.cpp b/src/tactic/fd_solver/enum2bv_solver.cpp index 5322b523d..5e05fdf31 100644 --- a/src/tactic/fd_solver/enum2bv_solver.cpp +++ b/src/tactic/fd_solver/enum2bv_solver.cpp @@ -120,7 +120,7 @@ public: mc = concat(mc.get(), m_solver->get_model_converter().get()); return mc; } - proof * get_proof() override { return m_solver->get_proof(); } + proof * get_proof_core() override { return m_solver->get_proof_core(); } std::string reason_unknown() const override { return m_solver->reason_unknown(); } void set_reason_unknown(char const* msg) override { m_solver->set_reason_unknown(msg); } void get_labels(svector & r) override { m_solver->get_labels(r); } diff --git a/src/tactic/fd_solver/pb2bv_solver.cpp b/src/tactic/fd_solver/pb2bv_solver.cpp index ee4a03d31..609ed173d 100644 --- a/src/tactic/fd_solver/pb2bv_solver.cpp +++ b/src/tactic/fd_solver/pb2bv_solver.cpp @@ -116,7 +116,7 @@ public: mc = concat(mc.get(), m_solver->get_model_converter().get()); return mc; } - proof * get_proof() override { return m_solver->get_proof(); } + proof * get_proof_core() override { return m_solver->get_proof_core(); } std::string reason_unknown() const override { return m_solver->reason_unknown(); } void set_reason_unknown(char const* msg) override { m_solver->set_reason_unknown(msg); } void get_labels(svector & r) override { m_solver->get_labels(r); } diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index f653e22e2..3729a2ad1 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -2075,7 +2075,7 @@ namespace smtfd { return m_fd_sat_solver->get_model_converter(); } - proof * get_proof() override { return nullptr; } + proof * get_proof_core() override { return nullptr; } std::string reason_unknown() const override { return m_reason_unknown; } void set_reason_unknown(char const* msg) override { m_reason_unknown = msg; } void get_labels(svector & r) override { }