From 2f06bcc73159191c199b98b8d0330d4de2e91612 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Oct 2025 20:34:13 +0100 Subject: [PATCH] add finite_set to quantifieed theories in smt_setup, fix type signature for map-inverse axioms Signed-off-by: Nikolaj Bjorner --- src/ast/finite_set_decl_plugin.cpp | 4 +- src/ast/finite_set_decl_plugin.h | 4 +- src/ast/rewriter/finite_set_axioms.cpp | 41 +++++++++------ src/smt/smt_setup.cpp | 1 + src/smt/theory_finite_set.cpp | 72 ++++++++++++-------------- 5 files changed, 65 insertions(+), 57 deletions(-) diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index e825dac30..0d322b683 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -71,7 +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}; + sort *arrABBsetA[3] = {arrAB, B, 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); @@ -86,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, m_names[OP_FINITE_SET_MAP_INVERSE], 2, 3, arrABBsetA, A); } sort * finite_set_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { diff --git a/src/ast/finite_set_decl_plugin.h b/src/ast/finite_set_decl_plugin.h index 8dd52c8b8..df851472e 100644 --- a/src/ast/finite_set_decl_plugin.h +++ b/src/ast/finite_set_decl_plugin.h @@ -201,8 +201,8 @@ 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_map_inverse(expr *f, expr *x, expr *b) { + return m_manager.mk_app(m_fid, OP_FINITE_SET_MAP_INVERSE, f, x, b); } app * mk_filter(expr* arr, expr* set) { diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp index 4848f6e71..411fc6d8a 100644 --- a/src/ast/rewriter/finite_set_axioms.cpp +++ b/src/ast/rewriter/finite_set_axioms.cpp @@ -206,11 +206,15 @@ void finite_set_axioms::in_range_axiom(expr* r) { // a := set.map(f, b) // (x in a) <=> set.map_inverse(f, x, b) in b void finite_set_axioms::in_map_axiom(expr *x, expr *a) { - expr* f = nullptr, *b = nullptr; + expr *f = nullptr, *b = nullptr; + sort *elem_sort = nullptr; + VERIFY(u.is_finite_set(a->get_sort(), elem_sort)); + if (x->get_sort() != elem_sort) + return; if (!u.is_map(a, f, b)) return; - expr_ref inv(u.mk_map_inverse(x, f, b), m); + expr_ref inv(u.mk_map_inverse(f, x, 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); @@ -221,8 +225,12 @@ void finite_set_axioms::in_map_axiom(expr *x, expr *a) { // (x in b) => f(x) in a void finite_set_axioms::in_map_image_axiom(expr *x, expr *a) { expr* f = nullptr, *b = nullptr; + sort *elem_sort = nullptr; if (!u.is_map(a, f, b)) return; + VERIFY(u.is_finite_set(b->get_sort(), elem_sort)); + if (x->get_sort() != elem_sort) + return; expr_ref x_in_b(u.mk_in(x, b), m); @@ -286,56 +294,59 @@ void finite_set_axioms::add_ternary(char const *name, expr *p1, expr *p2, expr * // 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; +void finite_set_axioms::size_ub_axiom(expr *sz) { + expr *b = nullptr, *e = nullptr, *x = nullptr, *y = nullptr; + if (!u.is_size(sz, e)) + return; 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))); + add_unit("size", e, m.mk_eq(sz, 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))); + add_unit("size", e, m.mk_eq(sz, 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))); + ineq = a.mk_le(sz, 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)); + ineq = a.mk_le(sz, u.mk_size(x)); m_rewriter(ineq); add_unit("size", e, ineq); - ineq = a.mk_le(u.mk_size(e), u.mk_size(y)); + ineq = a.mk_le(sz, 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)); + ineq = a.mk_le(sz, 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)); + ineq = a.mk_le(sz, 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)); + ineq = a.mk_le(sz, 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))); + ineq = a.mk_eq(sz, 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) { + VERIFY(u.is_size(e)); arith_util a(m); expr_ref ineq(m); - ineq = a.mk_le(a.mk_int(0), u.mk_size(e)); + ineq = a.mk_le(a.mk_int(0), e); m_rewriter(ineq); - add_unit("size-lb", e, ineq); + add_unit("size", e, ineq); } void finite_set_axioms::subset_axiom(expr* a) { diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 926818d78..c1affcf1a 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -845,6 +845,7 @@ namespace smt { setup_bv(); setup_dl(); setup_seq_str(st); + setup_finite_set(); setup_fpa(); setup_recfuns(); setup_special_relations(); diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index 6071226cf..fd4715470 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -66,6 +66,7 @@ namespace smt { * (set.in (f x) (set.map f S)) */ theory_var theory_finite_set::mk_var(enode *n) { + TRACE(finite_set, tout << "mk_var: " << enode_pp(n, ctx) << "\n"); theory_var r = theory::mk_var(n); VERIFY(r == static_cast(m_find.mk_var())); SASSERT(r == static_cast(m_var_data.size())); @@ -88,7 +89,7 @@ namespace smt { } else if (u.is_union(e) || u.is_intersect(e) || u.is_difference(e) || u.is_singleton(e) || - u.is_empty(e) || u.is_range(e)) { + u.is_empty(e) || u.is_range(e) || u.is_filter(e) || u.is_map(e)) { m_var_data[r]->m_setops.push_back(n); ctx.push_trail(push_back_trail(m_var_data[r]->m_setops)); for (auto arg : enode::args(n)) { @@ -104,9 +105,6 @@ namespace smt { ctx.push_trail(push_back_trail(m_var_data[v]->m_parent_setops)); } } - else if (u.is_map(e) || u.is_filter(e)) { - NOT_IMPLEMENTED_YET(); - } else if (u.is_range(e)) { } @@ -362,9 +360,7 @@ namespace smt { * - (set.range lo hi) -> lo-1,hi+1 not in range, lo, hi in range if lo <= hi * * * Other axioms: - * - (set.singleton x) -> (set.size (set.singleton x)) = 1 - * - (set.empty) -> (set.size (set.empty)) = 0 - + * - (set.size s) -> 0 <= (set.size s) <= upper-bound(s) */ void theory_finite_set::add_immediate_axioms(app* term) { expr *elem = nullptr, *set = nullptr; @@ -390,6 +386,10 @@ namespace smt { range_local.push_back(a.mk_add(lo, a.mk_int(-1))); range_local.push_back(a.mk_add(hi, a.mk_int(1))); } + else if (u.is_size(term)) { + m_axioms.size_lb_axiom(term); + m_axioms.size_ub_axiom(term); + } // Assert all new lemmas as clauses for (unsigned i = sz; i < m_clauses.axioms.size(); ++i) { @@ -631,38 +631,34 @@ namespace smt { void theory_finite_set::add_membership_axioms(expr *elem, expr *set) { TRACE(finite_set, tout << "add_membership_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";); - try { // Instantiate appropriate axiom based on set structure - if (!is_new_axiom(elem, set)) - ; - else if (u.is_empty(set)) { - m_axioms.in_empty_axiom(elem); - } - else if (u.is_singleton(set)) { - m_axioms.in_singleton_axiom(elem, set); - } - else if (u.is_union(set)) { - m_axioms.in_union_axiom(elem, set); - } - else if (u.is_intersect(set)) { - m_axioms.in_intersect_axiom(elem, set); - } - else if (u.is_difference(set)) { - m_axioms.in_difference_axiom(elem, set); - } - else if (u.is_range(set)) { - m_axioms.in_range_axiom(elem, set); - } - else if (u.is_map(set)) { - m_axioms.in_map_axiom(elem, set); - m_axioms.in_map_image_axiom(elem, set); - } - else if (u.is_filter(set)) { - m_axioms.in_filter_axiom(elem, set); - } - } catch (...) { - TRACE(finite_set, tout << "exception\n"); - throw; + if (!is_new_axiom(elem, set)) + ; + else if (u.is_empty(set)) { + m_axioms.in_empty_axiom(elem); + } + else if (u.is_singleton(set)) { + m_axioms.in_singleton_axiom(elem, set); + } + else if (u.is_union(set)) { + m_axioms.in_union_axiom(elem, set); + } + else if (u.is_intersect(set)) { + m_axioms.in_intersect_axiom(elem, set); + } + else if (u.is_difference(set)) { + m_axioms.in_difference_axiom(elem, set); + } + else if (u.is_range(set)) { + m_axioms.in_range_axiom(elem, set); + } + else if (u.is_map(set)) { + // TODO type of elem could be from the pre-image + m_axioms.in_map_axiom(elem, set); + m_axioms.in_map_image_axiom(elem, set); + } + else if (u.is_filter(set)) { + m_axioms.in_filter_axiom(elem, set); } TRACE(finite_set, tout << "after add_membership_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";); }