From 4464ab943194711f1c1160c0e71546411d257884 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Oct 2025 18:18:46 +0100 Subject: [PATCH] fix empty set declaration, add axioms and rewrites Signed-off-by: Nikolaj Bjorner --- src/ast/finite_set_decl_plugin.cpp | 8 +- src/ast/finite_set_decl_plugin.h | 4 + src/ast/rewriter/finite_set_axioms.cpp | 164 +++++++++++++---------- src/ast/rewriter/finite_set_axioms.h | 25 +++- src/ast/rewriter/finite_set_rewriter.cpp | 97 ++++++++------ src/smt/theory_finite_set.cpp | 4 +- 6 files changed, 180 insertions(+), 122 deletions(-) diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index 88c04129f..e825dac30 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -27,7 +27,7 @@ Revision History: finite_set_decl_plugin::finite_set_decl_plugin(): m_init(false) { m_names.resize(LAST_FINITE_SET_OP, nullptr); - m_names[OP_FINITE_SET_EMPTY] = "set.empty "; + m_names[OP_FINITE_SET_EMPTY] = "set.empty"; m_names[OP_FINITE_SET_SINGLETON] = "set.singleton"; m_names[OP_FINITE_SET_UNION] = "set.union"; m_names[OP_FINITE_SET_INTERSECT] = "set.intersect"; @@ -39,6 +39,7 @@ finite_set_decl_plugin::finite_set_decl_plugin(): m_names[OP_FINITE_SET_FILTER] = "set.filter"; m_names[OP_FINITE_SET_RANGE] = "set.range"; m_names[OP_FINITE_SET_EXT] = "set.diff"; + m_names[OP_FINITE_SET_MAP_INVERSE] = "set.map.inverse"; } finite_set_decl_plugin::~finite_set_decl_plugin() { @@ -70,6 +71,7 @@ void finite_set_decl_plugin::init() { sort* arrABsetA[2] = { arrAB, setA }; sort* arrABoolsetA[2] = { arrABool, setA }; sort* intintT[2] = { intT, intT }; + sort *arrABsetBsetA[3] = {arrAB, setB, setA}; m_sigs.resize(LAST_FINITE_SET_OP); m_sigs[OP_FINITE_SET_EMPTY] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_EMPTY], 1, 0, nullptr, setA); @@ -84,7 +86,7 @@ void finite_set_decl_plugin::init() { m_sigs[OP_FINITE_SET_FILTER] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_FILTER], 1, 2, arrABoolsetA, setA); m_sigs[OP_FINITE_SET_RANGE] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_RANGE], 0, 2, intintT, setInt); m_sigs[OP_FINITE_SET_EXT] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_EXT], 1, 2, setAsetA, A); -// m_sigs[OP_FINITE_SET_MAP_INVERSE] = alloc(polymorphism::psig, m, "set.map_inverse", 2, 3, arrABsetBsetA, A); + m_sigs[OP_FINITE_SET_MAP_INVERSE] = alloc(polymorphism::psig, m, "set.map_inverse", 2, 3, arrABsetBsetA, A); } sort * finite_set_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { @@ -190,6 +192,7 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param case OP_FINITE_SET_SIZE: case OP_FINITE_SET_SUBSET: case OP_FINITE_SET_MAP: + case OP_FINITE_SET_MAP_INVERSE: case OP_FINITE_SET_FILTER: case OP_FINITE_SET_RANGE: case OP_FINITE_SET_EXT: @@ -322,3 +325,4 @@ func_decl *finite_set_util::mk_range_decl() { sort *domain[2] = {i, i}; return m_manager.mk_func_decl(m_fid, OP_FINITE_SET_RANGE, 0, nullptr, 2, domain, nullptr); } + diff --git a/src/ast/finite_set_decl_plugin.h b/src/ast/finite_set_decl_plugin.h index 9084648b6..8dd52c8b8 100644 --- a/src/ast/finite_set_decl_plugin.h +++ b/src/ast/finite_set_decl_plugin.h @@ -201,6 +201,10 @@ public: return m_manager.mk_app(m_fid, OP_FINITE_SET_MAP, arr, set); } + app *mk_map_inverse(expr *arr, expr *a, expr *b) { + return m_manager.mk_app(m_fid, OP_FINITE_SET_MAP_INVERSE, arr, b, a); + } + app * mk_filter(expr* arr, expr* set) { return m_manager.mk_app(m_fid, OP_FINITE_SET_FILTER, arr, set); } diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp index 7e3adc0ed..06c600aba 100644 --- a/src/ast/rewriter/finite_set_axioms.cpp +++ b/src/ast/rewriter/finite_set_axioms.cpp @@ -41,11 +41,8 @@ void finite_set_axioms::in_empty_axiom(expr *x) { sort* elem_sort = x->get_sort(); sort *set_sort = u.mk_finite_set_sort(elem_sort); expr_ref empty_set(u.mk_empty(set_sort), m); - expr_ref x_in_empty(u.mk_in(x, empty_set), m); - - theory_axiom* ax = alloc(theory_axiom, m, "in-empty", x); - ax->clause.push_back(m.mk_not(x_in_empty)); - m_add_clause(ax); + expr_ref x_in_empty(u.mk_in(x, empty_set), m); + add_unit("in-empty", x, m.mk_not(x_in_empty)); } // a := set.union(b, c) @@ -55,7 +52,6 @@ void finite_set_axioms::in_union_axiom(expr *x, expr *a) { if (!u.is_union(a, b, c)) return; - 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); @@ -151,10 +147,10 @@ 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", x, a); - if (x == b) { - // If x and b are syntactically identical, then (x in a) is always true + if (x == b) { + // If x and b are syntactically identical, then (x in a) is always true + theory_axiom* ax = alloc(theory_axiom, m, "in-singleton", x, a); ax->clause.push_back(x_in_a); m_add_clause(ax); return; @@ -163,35 +159,28 @@ void finite_set_axioms::in_singleton_axiom(expr *x, expr *a) { expr_ref x_eq_b(m.mk_eq(x, b), m); // (x in a) => (x == b) - 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", x, a); + add_binary("in-singleton", x, a, m.mk_not(x_in_a), x_eq_b); // (x == b) => (x in a) - ax->clause.push_back(m.mk_not(x_eq_b)); - ax->clause.push_back(x_in_a); - m_add_clause(ax); + add_binary("in-singleton", x, a, m.mk_not(x_eq_b), x_in_a); } void finite_set_axioms::in_singleton_axiom(expr* a) { expr *b = nullptr; if (!u.is_singleton(a, b)) - return; - - - - expr_ref b_in_a(u.mk_in(b, a), m); - - auto ax = alloc(theory_axiom, m, "in-singleton"); - ax->clause.push_back(b_in_a); - m_add_clause(ax); + return; + add_unit("in-singleton", a, u.mk_in(b, a)); } - - // a := set.range(lo, hi) // (x in a) <=> (lo <= x <= hi) +// we use the rewriter to simplify inequalitiess because the arithmetic solver +// makes some assumptions that inequalities are in normal form. +// this complicates proof checking. +// Options are to include a proof of the rewrite within the justification +// fix the arithmetic solver to use the inequalities without rewriting (it really should) +// the same issue applies to everywhere we apply rewriting when adding theory axioms. + void finite_set_axioms::in_range_axiom(expr *x, expr *a) { expr* lo = nullptr, *hi = nullptr; if (!u.is_range(a, lo, hi)) @@ -205,16 +194,10 @@ 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", x, a); - ax1->clause.push_back(m.mk_not(x_in_a)); - ax1->clause.push_back(lo_le_x); - m_add_clause(ax1); + add_binary("in-range", x, a, m.mk_not(x_in_a), lo_le_x); // (x in a) => (x <= hi) - 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); + add_binary("in-range", x, a, m.mk_not(x_in_a), x_le_hi); // (lo <= x) and (x <= hi) => (x in a) theory_axiom* ax3 = alloc(theory_axiom, m, "in-range", x, a); @@ -246,13 +229,8 @@ void finite_set_axioms::in_range_axiom(expr* r) { ax->clause.push_back(u.mk_in(hi, r)); m_add_clause(ax); - 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", r); - ax->clause.push_back(m.mk_not(u.mk_in(a.mk_add(lo, a.mk_int(-1)), r))); - m_add_clause(ax); + add_unit("range-bounds", r, m.mk_not(u.mk_in(a.mk_add(hi, a.mk_int(1)), r))); + add_unit("range-bounds", r, m.mk_not(u.mk_in(a.mk_add(lo, a.mk_int(-1)), r))); } // a := set.map(f, b) @@ -262,6 +240,11 @@ void finite_set_axioms::in_map_axiom(expr *x, expr *a) { if (!u.is_map(a, f, b)) return; + expr_ref inv(u.mk_map_inverse(x, f, b), m); + expr_ref f1(u.mk_in(x, a), m); + expr_ref f2(u.mk_in(inv, b), m); + add_binary("map-inverse", x, a, m.mk_not(f1), f2); + add_binary("map-inverse", x, b, f1, m.mk_not(f2)); // For now, we provide a placeholder implementation // The full implementation would require skolemization // to express the inverse relationship properly. @@ -281,12 +264,10 @@ void finite_set_axioms::in_map_image_axiom(expr *x, expr *a) { array_util autil(m); expr_ref fx(autil.mk_select(f, x), m); expr_ref fx_in_a(u.mk_in(fx, a), m); + m_rewriter(fx); // (x in b) => f(x) in a - 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); + add_binary("in-map", x, a, m.mk_not(x_in_b), fx_in_a); } // a := set.filter(p, b) @@ -304,16 +285,10 @@ 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", x, a); - ax1->clause.push_back(m.mk_not(x_in_a)); - ax1->clause.push_back(x_in_b); - m_add_clause(ax1); + add_binary("in-filter", x, a, m.mk_not(x_in_a), x_in_b); // (x in a) => p(x) - 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); + add_binary("in-filter", x, a, m.mk_not(x_in_a), px); // (x in b) and p(x) => (x in a) theory_axiom* ax3 = alloc(theory_axiom, m, "in-filter", x, a); @@ -323,23 +298,74 @@ void finite_set_axioms::in_filter_axiom(expr *x, expr *a) { m_add_clause(ax3); } -// a := set.singleton(b) -// set.size(a) = 1 -void finite_set_axioms::size_singleton_axiom(expr *a) { - expr* b = nullptr; - if (!u.is_singleton(a, b)) - return; - - arith_util arith(m); - expr_ref size_a(u.mk_size(a), m); - 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", a); - ax->clause.push_back(eq); +void finite_set_axioms::add_unit(char const* name, expr* e, expr* unit) { + theory_axiom *ax = alloc(theory_axiom, m, name, e); + ax->clause.push_back(unit); m_add_clause(ax); } +void finite_set_axioms::add_binary(char const* name, expr* x, expr* y, expr* f1, expr* f2) { + theory_axiom *ax = alloc(theory_axiom, m, name, x, y); + ax->clause.push_back(f1); + ax->clause.push_back(f2); + m_add_clause(ax); +} + +// Auxiliary algebraic axioms to ease reasoning about set.size +// The axioms are not required for completenss for the base fragment +// as they are handled by creating semi-linear sets. +void finite_set_axioms::size_ub_axiom(expr *e) { + expr *b = nullptr, *x = nullptr, *y = nullptr; + arith_util a(m); + expr_ref ineq(m); + + if (u.is_singleton(e, b)) + add_unit("size", e, m.mk_eq(u.mk_size(e), a.mk_int(1))); + else if (u.is_empty(e)) + add_unit("size", e, m.mk_eq(u.mk_size(e), a.mk_int(0))); + else if (u.is_union(e, x, y)) { + ineq = a.mk_le(u.mk_size(e), a.mk_add(u.mk_size(x), u.mk_size(y))); + m_rewriter(ineq); + add_unit("size", e, ineq); + } + else if (u.is_intersect(e, x, y)) { + ineq = a.mk_le(u.mk_size(e), u.mk_size(x)); + m_rewriter(ineq); + add_unit("size", e, ineq); + ineq = a.mk_le(u.mk_size(e), u.mk_size(y)); + m_rewriter(ineq); + add_unit("size", e, ineq); + } + else if (u.is_difference(e, x, y)) { + ineq = a.mk_le(u.mk_size(e), u.mk_size(x)); + m_rewriter(ineq); + add_unit("size", e, ineq); + } + else if (u.is_filter(e, x, y)) { + ineq = a.mk_le(u.mk_size(e), u.mk_size(y)); + m_rewriter(ineq); + add_unit("size", e, ineq); + } + else if (u.is_map(e, x, y)) { + ineq = a.mk_le(u.mk_size(e), u.mk_size(y)); + m_rewriter(ineq); + add_unit("size", e, ineq); + } + else if (u.is_range(e, x, y)) { + ineq = a.mk_eq(u.mk_size(e), m.mk_ite(a.mk_le(x, y), a.mk_add(a.mk_sub(y, x), a.mk_int(1)), a.mk_int(0))); + m_rewriter(ineq); + add_unit("size", e, ineq); + } +} + +void finite_set_axioms::size_lb_axiom(expr* e) { + arith_util a(m); + expr_ref ineq(m); + ineq = a.mk_le(a.mk_int(0), u.mk_size(e)); + m_rewriter(ineq); + add_unit("size-lb", e, ineq); +} + void finite_set_axioms::subset_axiom(expr* a) { expr *b = nullptr, *c = nullptr; if (!u.is_subset(a, b, c)) @@ -367,7 +393,7 @@ void finite_set_axioms::extensionality_axiom(expr *a, expr* b) { expr_ref diff_in_a(u.mk_in(diff_ab, a), m); expr_ref diff_in_b(u.mk_in(diff_ab, b), m); - // (a != b) => (x in diff_ab != x in diff_ba) + // (a != b) => (x in diff_ab != x in diff_ba) 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)); diff --git a/src/ast/rewriter/finite_set_axioms.h b/src/ast/rewriter/finite_set_axioms.h index c7f4d18c7..9f5d02263 100644 --- a/src/ast/rewriter/finite_set_axioms.h +++ b/src/ast/rewriter/finite_set_axioms.h @@ -46,6 +46,10 @@ class finite_set_axioms { std::function m_add_clause; + void add_unit(char const* name, expr* x, expr *e); + + void add_binary(char const *name, expr *x, expr *y, expr *f1, expr *f2); + public: finite_set_axioms(ast_manager &m) : m(m), u(m), m_rewriter(m) {} @@ -86,8 +90,8 @@ public: // a := set.range(lo, hi) // (not (set.in (- lo 1) a)) // (not (set.in (+ hi 1) a)) - // (set.in lo a) - // (set.in hi a) + // lo <= hi => (set.in lo a) + // lo <= hi => (set.in hi a) void in_range_axiom(expr *a); // a := set.map(f, b) @@ -106,9 +110,20 @@ public: // (a) <=> (set.intersect(b, c) = b) void subset_axiom(expr *a); - // a := set.singleton(b) - // set.size(a) = 1 - void size_singleton_axiom(expr *a); + + // set.size(empty) = 0 + // set.size(set.singleton(b)) = 1 + // set.size(a u b) <= set.size(a) + set.size(b) + // set.size(a n b) <= min(set.size(a), set.size(b)) + // set.size(a \ b) <= set.size(a) + // set.size(set.map(f, b)) <= set.size(b) + // set.size(set.filter(p, b)) <= set.size(b) + // set.size([l..u]) = if(l <= u, u - l + 1, 0) + void size_ub_axiom(expr *a); + + // 0 <= set.size(e) + void size_lb_axiom(expr *e); + // a != b => set.in (set.diff(a, b) a) != set.in (set.diff(a, b) b) void extensionality_axiom(expr *a, expr *b); diff --git a/src/ast/rewriter/finite_set_rewriter.cpp b/src/ast/rewriter/finite_set_rewriter.cpp index 9e2aaa3a6..b86f211f1 100644 --- a/src/ast/rewriter/finite_set_rewriter.cpp +++ b/src/ast/rewriter/finite_set_rewriter.cpp @@ -47,78 +47,87 @@ br_status finite_set_rewriter::mk_app_core(func_decl * f, unsigned num_args, exp } br_status finite_set_rewriter::mk_union(unsigned num_args, expr * const * args, expr_ref & result) { + VERIFY(num_args == 2); // Idempotency: set.union(x, x) -> x - if (num_args == 2 && args[0] == args[1]) { + if (args[0] == args[1]) { result = args[0]; return BR_DONE; } // Identity: set.union(x, empty) -> x or set.union(empty, x) -> x - if (num_args == 2) { - if (u.is_empty(args[0])) { - result = args[1]; - return BR_DONE; - } - if (u.is_empty(args[1])) { + if (u.is_empty(args[0])) { + result = args[1]; + return BR_DONE; + } + if (u.is_empty(args[1])) { + result = args[0]; + return BR_DONE; + } + + // Absorption: set.union(x, set.intersect(x, y)) -> x + expr *a1, *a2; + if (u.is_intersect(args[1], a1, a2)) { + if (args[0] == a1 || args[0] == a2) { result = args[0]; return BR_DONE; } - - // Absorption: set.union(x, set.intersect(x, y)) -> x - expr* a1, *a2; - if (u.is_intersect(args[1], a1, a2)) { - if (args[0] == a1 || args[0] == a2) { - result = args[0]; - return BR_DONE; - } - } - - // Absorption: set.union(set.intersect(x, y), x) -> x - if (u.is_intersect(args[0], a1, a2)) { - if (args[1] == a1 || args[1] == a2) { - result = args[1]; - return BR_DONE; - } + } + + // Absorption: set.union(set.intersect(x, y), x) -> x + if (u.is_intersect(args[0], a1, a2)) { + if (args[1] == a1 || args[1] == a2) { + result = args[1]; + return BR_DONE; } } + return BR_FAILED; } br_status finite_set_rewriter::mk_intersect(unsigned num_args, expr * const * args, expr_ref & result) { + if (num_args != 2) + return BR_FAILED; + // Idempotency: set.intersect(x, x) -> x - if (num_args == 2 && args[0] == args[1]) { + if (args[0] == args[1]) { result = args[0]; return BR_DONE; } // Annihilation: set.intersect(x, empty) -> empty or set.intersect(empty, x) -> empty - if (num_args == 2) { - if (u.is_empty(args[0])) { + if (u.is_empty(args[0])) { + result = args[0]; + return BR_DONE; + } + if (u.is_empty(args[1])) { + result = args[1]; + return BR_DONE; + } + + // Absorption: set.intersect(x, set.union(x, y)) -> x + expr *a1, *a2; + if (u.is_union(args[1], a1, a2)) { + if (args[0] == a1 || args[0] == a2) { result = args[0]; return BR_DONE; } - if (u.is_empty(args[1])) { + } + + // Absorption: set.intersect(set.union(x, y), x) -> x + if (u.is_union(args[0], a1, a2)) { + if (args[1] == a1 || args[1] == a2) { result = args[1]; return BR_DONE; } - - // Absorption: set.intersect(x, set.union(x, y)) -> x - expr* a1, *a2; - if (u.is_union(args[1], a1, a2)) { - if (args[0] == a1 || args[0] == a2) { - result = args[0]; - return BR_DONE; - } - } - - // Absorption: set.intersect(set.union(x, y), x) -> x - if (u.is_union(args[0], a1, a2)) { - if (args[1] == a1 || args[1] == a2) { - result = args[1]; - return BR_DONE; - } - } + } + expr *l1, *l2, *u1, *u2; + if (u.is_range(args[0], l1, u1) && u.is_range(args[1], l2, u2)) { + arith_util a(m); + auto max_l = m.mk_ite(a.mk_ge(l1, l2), l1, l2); + auto min_u = m.mk_ite(a.mk_ge(u1, u2), u2, u1); + result = u.mk_range(max_l, min_u); + return BR_REWRITE_FULL; } return BR_FAILED; diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index a234acdfd..6071226cf 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -122,12 +122,12 @@ namespace smt { } /* - * Merge the equivalence classes of two variables. + * Merge the equivalence classes of two variables. * parent_in := vector of (set.in x S) terms where S is in the equivalence class of r. * parent_setops := vector of (set.op S T) where S or T is in the equivalence class of r. * setops := vector of (set.op S T) where (set.op S T) is in the equivalence class of r. * - */ + */ void theory_finite_set::merge_eh(theory_var root, theory_var other, theory_var, theory_var) { // r is the new root TRACE(finite_set, tout << "merging v" << root << " v" << other << "\n"; display_var(tout, root);