diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp index 0f020cbd1..dd25a54f1 100644 --- a/src/ast/rewriter/finite_set_axioms.cpp +++ b/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); diff --git a/src/ast/rewriter/finite_set_axioms.h b/src/ast/rewriter/finite_set_axioms.h index 46684373c..e9d304b41 100644 --- a/src/ast/rewriter/finite_set_axioms.h +++ 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); diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index 615ef1785..d9abb8756 100644 --- a/src/smt/theory_finite_set.cpp +++ b/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) - args.push_back(m.mk_const(p.get_symbol(), m.mk_proof_sort())); + for (auto const &p : ax->params) { + 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);