diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index f5e936939..4c5703b0b 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -3338,15 +3338,25 @@ proof * ast_manager::mk_th_lemma( if (proofs_disabled()) return nullptr; + proof_ref pr(*this); ptr_buffer args; - vector parameters; - parameters.push_back(parameter(get_family_name(tid))); for (unsigned i = 0; i < num_params; ++i) { - parameters.push_back(params[i]); + auto const &p = params[i]; + if (p.is_symbol()) + args.push_back(mk_app(p.get_symbol(), 0, nullptr, mk_proof_sort())); + else if (p.is_ast() && is_expr(p.get_ast())) + args.push_back(to_expr(p.get_ast())); + else if (p.is_rational()) { + arith_util autil(*this); + args.push_back(autil.mk_real(p.get_rational())); + } } + pr = mk_app(get_family_name(tid), args.size(), args.data(), mk_proof_sort()); + args.reset(); + args.push_back(pr.get()); args.append(num_proofs, (expr**) proofs); args.push_back(fact); - return mk_app(basic_family_id, PR_TH_LEMMA, num_params+1, parameters.data(), args.size(), args.data()); + return mk_app(basic_family_id, PR_TH_LEMMA, 0, nullptr, args.size(), args.data()); } proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl, diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp index 5231849bf..e8a309ed0 100644 --- a/src/ast/rewriter/finite_set_axioms.cpp +++ b/src/ast/rewriter/finite_set_axioms.cpp @@ -38,7 +38,7 @@ void finite_set_axioms::in_empty_axiom(expr *x) { expr_ref empty_set(u.mk_empty(elem_sort), m); expr_ref x_in_empty(u.mk_in(x, empty_set), m); - theory_axiom ax(m, "finite-set", "in-empty"); + theory_axiom ax(m, "in-empty"); ax.clause.push_back(m.mk_not(x_in_empty)); m_add_clause(ax); } @@ -50,7 +50,7 @@ void finite_set_axioms::in_union_axiom(expr *x, expr *a) { if (!u.is_union(a, b, c)) return; - theory_axiom ax(m, "finite-set", "in-union"); + theory_axiom ax(m, "in-union"); expr_ref x_in_a(u.mk_in(x, a), m); expr_ref x_in_b(u.mk_in(x, b), m); expr_ref x_in_c(u.mk_in(x, c), m); @@ -62,13 +62,13 @@ void finite_set_axioms::in_union_axiom(expr *x, expr *a) { m_add_clause(ax); // (x in b) => (x in a) - theory_axiom ax2(m, "finite-set", "in-union"); + theory_axiom ax2(m, "in-union"); ax2.clause.push_back(m.mk_not(x_in_b)); ax2.clause.push_back(x_in_a); m_add_clause(ax2); // (x in c) => (x in a) - theory_axiom ax3(m, "finite-set", "in-union"); + theory_axiom ax3(m, "in-union"); ax3.clause.push_back(m.mk_not(x_in_c)); ax3.clause.push_back(x_in_a); m_add_clause(ax3); @@ -86,19 +86,19 @@ void finite_set_axioms::in_intersect_axiom(expr *x, expr *a) { expr_ref x_in_c(u.mk_in(x, c), m); // (x in a) => (x in b) - theory_axiom ax1(m, "finite-set", "in-intersect"); + theory_axiom ax1(m, "in-intersect"); ax1.clause.push_back(m.mk_not(x_in_a)); ax1.clause.push_back(x_in_b); m_add_clause(ax1); // (x in a) => (x in c) - theory_axiom ax2(m, "finite-set", "in-intersect"); + theory_axiom ax2(m, "in-intersect"); ax2.clause.push_back(m.mk_not(x_in_a)); ax2.clause.push_back(x_in_c); m_add_clause(ax2); // (x in b) and (x in c) => (x in a) - theory_axiom ax3(m, "finite-set", "in-intersect"); + theory_axiom ax3(m, "in-intersect"); ax3.clause.push_back(m.mk_not(x_in_b)); ax3.clause.push_back(m.mk_not(x_in_c)); ax3.clause.push_back(x_in_a); @@ -117,19 +117,19 @@ void finite_set_axioms::in_difference_axiom(expr *x, expr *a) { expr_ref x_in_c(u.mk_in(x, c), m); // (x in a) => (x in b) - theory_axiom ax1(m, "finite-set", "in-difference"); + theory_axiom ax1(m, "in-difference"); ax1.clause.push_back(m.mk_not(x_in_a)); ax1.clause.push_back(x_in_b); m_add_clause(ax1); // (x in a) => not (x in c) - theory_axiom ax2(m, "finite-set", "in-difference"); + theory_axiom ax2(m, "in-difference"); ax2.clause.push_back(m.mk_not(x_in_a)); ax2.clause.push_back(m.mk_not(x_in_c)); m_add_clause(ax2); // (x in b) and not (x in c) => (x in a) - theory_axiom ax3(m, "finite-set", "in-difference"); + theory_axiom ax3(m, "in-difference"); ax3.clause.push_back(m.mk_not(x_in_b)); ax3.clause.push_back(x_in_c); ax3.clause.push_back(x_in_a); @@ -145,7 +145,7 @@ void finite_set_axioms::in_singleton_axiom(expr *x, expr *a) { expr_ref x_in_a(u.mk_in(x, a), m); - theory_axiom ax(m, "finite-set", "in-singleton"); + theory_axiom ax(m, "in-singleton"); if (x == b) { // If x and b are syntactically identical, then (x in a) is always true @@ -181,19 +181,19 @@ void finite_set_axioms::in_range_axiom(expr *x, expr *a) { expr_ref x_le_hi(arith.mk_le(x, hi), m); // (x in a) => (lo <= x) - theory_axiom ax1(m, "finite-set", "in-range"); + theory_axiom ax1(m, "in-range"); ax1.clause.push_back(m.mk_not(x_in_a)); ax1.clause.push_back(lo_le_x); m_add_clause(ax1); // (x in a) => (x <= hi) - theory_axiom ax2(m, "finite-set", "in-range"); + theory_axiom ax2(m, "in-range"); ax2.clause.push_back(m.mk_not(x_in_a)); ax2.clause.push_back(x_le_hi); m_add_clause(ax2); // (lo <= x) and (x <= hi) => (x in a) - theory_axiom ax3(m, "finite-set", "in-range"); + theory_axiom ax3(m, "in-range"); ax3.clause.push_back(m.mk_not(lo_le_x)); ax3.clause.push_back(m.mk_not(x_le_hi)); ax3.clause.push_back(x_in_a); @@ -228,7 +228,7 @@ void finite_set_axioms::in_map_image_axiom(expr *x, expr *a) { expr_ref fx_in_a(u.mk_in(fx, a), m); // (x in b) => f(x) in a - theory_axiom ax(m, "finite-set", "in-map-image"); + theory_axiom ax(m, "in-map-image"); ax.clause.push_back(m.mk_not(x_in_b)); ax.clause.push_back(fx_in_a); m_add_clause(ax); @@ -249,19 +249,19 @@ void finite_set_axioms::in_filter_axiom(expr *x, expr *a) { expr_ref px(autil.mk_select(p, x), m); // (x in a) => (x in b) - theory_axiom ax1(m, "finite-set", "in-filter"); + theory_axiom ax1(m, "in-filter"); ax1.clause.push_back(m.mk_not(x_in_a)); ax1.clause.push_back(x_in_b); m_add_clause(ax1); // (x in a) => p(x) - theory_axiom ax2(m, "finite-set", "in-filter"); + theory_axiom ax2(m, "in-filter"); ax2.clause.push_back(m.mk_not(x_in_a)); ax2.clause.push_back(px); m_add_clause(ax2); // (x in b) and p(x) => (x in a) - theory_axiom ax3(m, "finite-set", "in-filter"); + theory_axiom ax3(m, "in-filter"); ax3.clause.push_back(m.mk_not(x_in_b)); ax3.clause.push_back(m.mk_not(px)); ax3.clause.push_back(x_in_a); @@ -280,7 +280,7 @@ void finite_set_axioms::size_singleton_axiom(expr *a) { expr_ref one(arith.mk_int(1), m); expr_ref eq(m.mk_eq(size_a, one), m); - theory_axiom ax(m, "finite-set", "size-singleton"); + theory_axiom ax(m, "size-singleton"); ax.clause.push_back(eq); m_add_clause(ax); } @@ -293,12 +293,12 @@ void finite_set_axioms::subset_axiom(expr* a) { expr_ref intersect_bc(u.mk_intersect(b, c), m); expr_ref eq(m.mk_eq(intersect_bc, b), m); - theory_axiom ax1(m, "finite-set", "subset"); + theory_axiom ax1(m, "subset"); ax1.clause.push_back(m.mk_not(a)); ax1.clause.push_back(eq); m_add_clause(ax1); - theory_axiom ax2(m, "finite-set", "subset"); + theory_axiom ax2(m, "subset"); ax2.clause.push_back(a); ax2.clause.push_back(m.mk_not(eq)); m_add_clause(ax2); @@ -313,13 +313,13 @@ void finite_set_axioms::extensionality_axiom(expr *a, expr* b) { expr_ref diff_in_b(u.mk_in(diff_ab, b), m); // (a != b) => (x in diff_ab != x in diff_ba) - theory_axiom ax(m, "finite-set", "extensionality"); + theory_axiom ax(m, "extensionality"); ax.clause.push_back(a_eq_b); ax.clause.push_back(m.mk_not(diff_in_a)); ax.clause.push_back(m.mk_not(diff_in_b)); m_add_clause(ax); - theory_axiom ax2(m, "finite-set", "extensionality"); + theory_axiom ax2(m, "extensionality"); ax2.clause.push_back(m.mk_not(a_eq_b)); ax2.clause.push_back(diff_in_a); ax2.clause.push_back(diff_in_b); diff --git a/src/ast/rewriter/finite_set_axioms.h b/src/ast/rewriter/finite_set_axioms.h index d2d17c49c..85b192cdd 100644 --- a/src/ast/rewriter/finite_set_axioms.h +++ b/src/ast/rewriter/finite_set_axioms.h @@ -19,12 +19,7 @@ struct theory_axiom { theory_axiom(ast_manager& m, symbol const& th): clause(m) { params.push_back(parameter(th)); } - theory_axiom(ast_manager &m, symbol const &th, symbol const& rule) : clause(m) { - params.push_back(parameter(th)); - params.push_back(parameter(rule)); - } - theory_axiom(ast_manager &m, char const *th, char const *rule) : clause(m) { - params.push_back(parameter(symbol(th))); + theory_axiom(ast_manager &m, char const* rule) : clause(m) { params.push_back(parameter(symbol(rule))); } theory_axiom(ast_manager &m) : clause(m) { diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp index 99085455f..324674a99 100644 --- a/src/smt/smt_clause_proof.cpp +++ b/src/smt/smt_clause_proof.cpp @@ -151,7 +151,7 @@ namespace smt { update(st, m_lits, pr); } - void clause_proof::propagate(literal lit, justification const& jst, literal_vector const& ante) { + void clause_proof::propagate(literal lit, justification * jst, literal_vector const& ante) { if (!is_enabled()) return; m_lits.reset(); @@ -159,8 +159,7 @@ namespace smt { m_lits.push_back(ctx.literal2expr(~l)); m_lits.push_back(ctx.literal2expr(lit)); auto st = clause_proof::status::th_lemma; - auto pr = justification2proof(st, &const_cast(jst)); - // proof_ref pr(m.mk_app(symbol("smt"), 0, nullptr, m.mk_proof_sort()), m); + auto pr = justification2proof(st, jst); update(st, m_lits, pr); } diff --git a/src/smt/smt_clause_proof.h b/src/smt/smt_clause_proof.h index d7cc421cf..28191cfa2 100644 --- a/src/smt/smt_clause_proof.h +++ b/src/smt/smt_clause_proof.h @@ -82,7 +82,7 @@ namespace smt { void add(literal lit1, literal lit2, clause_kind k, justification* j, literal_buffer const* simp_lits = nullptr); void add(clause& c, literal_buffer const* simp_lits = nullptr); void add(unsigned n, literal const* lits, clause_kind k, justification* j); - void propagate(literal lit, justification const& j, literal_vector const& ante); + void propagate(literal lit, justification* j, literal_vector const& ante); void del(clause& c); proof_ref get_proof(bool inconsistent); bool is_enabled() const { return m_enabled; } diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index e85137028..6118024b1 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -347,7 +347,7 @@ namespace smt { literal_vector & antecedents = m_tmp_literal_vector; antecedents.reset(); justification2literals_core(js, antecedents); - m_ctx.get_clause_proof().propagate(consequent, *js, antecedents); + m_ctx.get_clause_proof().propagate(consequent, js, antecedents); for (literal l : antecedents) process_antecedent(l, num_marks); (void)consequent; diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index 2713c55fb..7badc1c99 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -724,13 +724,16 @@ namespace smt { auto bjust = ctx.mk_justification(just); if (ctx.clause_proof_active()) { // assume all justifications is a non-empty list of symbol parameters + // proof logging is basically broken: it doesn't log propagations, but instead + // only propagations that are processed by conflict resolution. + // this misses conflicts at base level. proof_ref pr(m); expr_ref_vector args(m); - for (unsigned i = 1; i < ax.params.size(); ++i) - args.push_back(m.mk_app(ax.params[i].get_symbol(), 0, nullptr, m.mk_proof_sort())); - pr = m.mk_app(ax.params[0].get_symbol(), args.size(), args.data(), m.mk_proof_sort()); + for (auto const& p : ax.params) + args.push_back(m.mk_const(p.get_symbol(), m.mk_proof_sort())); + pr = m.mk_app(m.get_family_name(get_family_id()), args.size(), args.data(), m.mk_proof_sort()); justification_proof_wrapper jp(ctx, pr.get(), false); - ctx.get_clause_proof().propagate(lit, jp, antecedent); + ctx.get_clause_proof().propagate(lit, &jp, antecedent); jp.del_eh(m); } ctx.assign(lit, bjust);