fixup proof log annotations of rules

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<expr> args;
-    vector<parameter> 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,

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);

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) {
+    theory_axiom(ast_manager &m, char 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)));
         params.push_back(parameter(symbol(rule)));
     }
     theory_axiom(ast_manager &m) : clause(m) {

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<justification &>(jst));
+        auto pr = justification2proof(st, jst);
-        // proof_ref pr(m.mk_app(symbol("smt"), 0, nullptr, m.mk_proof_sort()), m);
         update(st, m_lits, pr);
     }
 

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; }

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;

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) 
+                for (auto const& p : ax.params)
-                    args.push_back(m.mk_app(ax.params[i].get_symbol(), 0, nullptr, m.mk_proof_sort()));                    
+                    args.push_back(m.mk_const(p.get_symbol(), m.mk_proof_sort()));                  
-                pr = m.mk_app(ax.params[0].get_symbol(), args.size(), args.data(), 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);