extend proof logging

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

src/ast/rewriter/finite_set_axioms.cpp

@@ -39,7 +39,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 = alloc(theory_axiom, m, "in-empty");
+    theory_axiom* ax = alloc(theory_axiom, m, "in-empty", x);
     ax->clause.push_back(m.mk_not(x_in_empty));
     m_add_clause(ax);
 }
@@ -57,20 +57,20 @@ void finite_set_axioms::in_union_axiom(expr *x, expr *a) {
     expr_ref x_in_c(u.mk_in(x, c), m);
     
     // (x in a) => (x in b) or (x in c)
-    theory_axiom *ax1 = alloc(theory_axiom, m, "in-union");
+    theory_axiom *ax1 = alloc(theory_axiom, m, "in-union", x, a);
     ax1->clause.push_back(m.mk_not(x_in_a));
     ax1->clause.push_back(x_in_b);
     ax1->clause.push_back(x_in_c);
     m_add_clause(ax1);
 
     // (x in b) => (x in a)
-    theory_axiom* ax2 = alloc(theory_axiom, m, "in-union");
+    theory_axiom* ax2 = alloc(theory_axiom, m, "in-union", x, a);
     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 = alloc(theory_axiom, m, "in-union");
+    theory_axiom* ax3 = alloc(theory_axiom, m, "in-union", x, a);
     ax3->clause.push_back(m.mk_not(x_in_c));
     ax3->clause.push_back(x_in_a);
     m_add_clause(ax3);
@@ -88,19 +88,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 = alloc(theory_axiom, m, "in-intersect");
+    theory_axiom* ax1 = alloc(theory_axiom, m, "in-intersect", x, a);
     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 = alloc(theory_axiom, m, "in-intersect");
+    theory_axiom* ax2 = alloc(theory_axiom, m, "in-intersect", x, a);
     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 = alloc(theory_axiom, m, "in-intersect");
+    theory_axiom* ax3 = alloc(theory_axiom, m, "in-intersect", x, a);
     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);
@@ -119,19 +119,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 = alloc(theory_axiom, m, "in-difference");
+    theory_axiom* ax1 = alloc(theory_axiom, m, "in-difference", x, a);
     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 = alloc(theory_axiom, m, "in-difference");
+    theory_axiom* ax2 = alloc(theory_axiom, m, "in-difference", x, a);
     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 = alloc(theory_axiom, m, "in-difference");
+    theory_axiom* ax3 = alloc(theory_axiom, m, "in-difference", x, a);
     ax3->clause.push_back(m.mk_not(x_in_b));
     ax3->clause.push_back(x_in_c);
     ax3->clause.push_back(x_in_a);
@@ -147,7 +147,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 = alloc(theory_axiom, m, "in-singleton");
+    theory_axiom* ax = alloc(theory_axiom, m, "in-singleton", x, a);
     if (x == b) {
         // If x and b are syntactically identical, then (x in a) is always true
 
@@ -162,7 +162,7 @@ void finite_set_axioms::in_singleton_axiom(expr *x, expr *a) {
     ax->clause.push_back(m.mk_not(x_in_a));
     ax->clause.push_back(x_eq_b);
     m_add_clause(ax);
-    ax = alloc(theory_axiom, m, "in-singleton");
+    ax = alloc(theory_axiom, m, "in-singleton", x, a);
 
     // (x == b) => (x in a)
     ax->clause.push_back(m.mk_not(x_eq_b));
@@ -201,19 +201,19 @@ void finite_set_axioms::in_range_axiom(expr *x, expr *a) {
     m_rewriter(x_le_hi);
     
     // (x in a) => (lo <= x)
-    theory_axiom* ax1 = alloc(theory_axiom, m, "in-range");
+    theory_axiom* ax1 = alloc(theory_axiom, m, "in-range", x, a);
     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 = alloc(theory_axiom, m, "in-range");
+    theory_axiom* ax2 = alloc(theory_axiom, m, "in-range", x, a);
     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 = alloc(theory_axiom, m, "in-range");
+    theory_axiom* ax3 = alloc(theory_axiom, m, "in-range", x, a);
     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);
@@ -233,16 +233,16 @@ void finite_set_axioms::in_range_axiom(expr* r) {
     ax->clause.push_back(u.mk_in(lo, r));
     m_add_clause(ax);
 
-    ax = alloc(theory_axiom, m, "range-bounds");
+    ax = alloc(theory_axiom, m, "range-bounds", r);
     ax->clause.push_back(u.mk_in(hi, r));
     m_add_clause(ax);
 
     arith_util a(m);
-    ax = alloc(theory_axiom, m, "range-bounds");
+    ax = alloc(theory_axiom, m, "range-bounds", r);
     ax->clause.push_back(m.mk_not(u.mk_in(a.mk_add(hi, a.mk_int(1)), r)));
     m_add_clause(ax);
 
-    ax = alloc(theory_axiom, m, "range-bounds");
+    ax = alloc(theory_axiom, m, "range-bounds", r);
     ax->clause.push_back(m.mk_not(u.mk_in(a.mk_add(lo, a.mk_int(-1)), r)));
     m_add_clause(ax);
 }
@@ -275,7 +275,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 = alloc(theory_axiom, m, "in-map-image");
+    theory_axiom* ax = alloc(theory_axiom, m, "in-map-image", x, a);
     ax->clause.push_back(m.mk_not(x_in_b));
     ax->clause.push_back(fx_in_a);
     m_add_clause(ax);
@@ -296,19 +296,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 = alloc(theory_axiom, m, "in-filter");
+    theory_axiom* ax1 = alloc(theory_axiom, m, "in-filter", x, a);
     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 = alloc(theory_axiom, m, "in-filter");
+    theory_axiom* ax2 = alloc(theory_axiom, m, "in-filter", x, a);
     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 = alloc(theory_axiom, m, "in-filter");
+    theory_axiom* ax3 = alloc(theory_axiom, m, "in-filter", x, a);
     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);
@@ -327,7 +327,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 = alloc(theory_axiom, m, "size-singleton");
+    theory_axiom* ax = alloc(theory_axiom, m, "size-singleton", a);
     ax->clause.push_back(eq);
     m_add_clause(ax);
 }
@@ -340,12 +340,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 = alloc(theory_axiom, m,  "subset");
+    theory_axiom* ax1 = alloc(theory_axiom, m,  "subset", a);
     ax1->clause.push_back(m.mk_not(a));
     ax1->clause.push_back(eq);
     m_add_clause(ax1);
 
-    theory_axiom* ax2 = alloc(theory_axiom, m,  "subset");
+    theory_axiom* ax2 = alloc(theory_axiom, m,  "subset", a);
     ax2->clause.push_back(a);
     ax2->clause.push_back(m.mk_not(eq));
     m_add_clause(ax2);
@@ -360,13 +360,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 = alloc(theory_axiom, m, "extensionality");
+    theory_axiom* ax = alloc(theory_axiom, m, "extensionality", a, b);
     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 = alloc(theory_axiom, m, "extensionality");
+    theory_axiom* ax2 = alloc(theory_axiom, m, "extensionality", a, b);
     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

@@ -26,6 +26,13 @@ struct theory_axiom {
     }
     theory_axiom(ast_manager &m) : clause(m) {
     }
+
+    theory_axiom(ast_manager &m, char const *rule, expr* x, expr* y = nullptr) : clause(m) {
+        params.push_back(parameter(symbol(rule)));
+        params.push_back(parameter(x));
+        if (y)
+            params.push_back(parameter(y));
+    }
 };
 
 std::ostream &operator<<(std::ostream &out, theory_axiom const &ax);

src/smt/theory_finite_set.cpp

@@ -891,8 +891,13 @@ namespace smt {
                 // this misses conflicts at base level.
                 proof_ref pr(m);
                 expr_ref_vector args(m);
-                for (auto const& p : ax->params)
+                for (auto const &p : ax->params) {
-                    args.push_back(m.mk_const(p.get_symbol(), m.mk_proof_sort()));
+                    if (p.is_ast())
+                        args.push_back(to_expr(p.get_ast()));
+                    else
+                        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);