From df62e5e9e616434b138f7832d1b7ea32b1438cf1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Oct 2025 09:37:11 +0200 Subject: [PATCH] add assume-eqs and extensionality Signed-off-by: Nikolaj Bjorner --- src/ast/finite_set_decl_plugin.cpp | 3 + src/ast/finite_set_decl_plugin.h | 3 + src/ast/rewriter/finite_set_axioms.cpp | 15 +++++ src/ast/rewriter/finite_set_axioms.h | 3 + src/smt/theory_finite_set.cpp | 93 ++++++++++++++++++++------ src/smt/theory_finite_set.h | 3 +- 6 files changed, 98 insertions(+), 22 deletions(-) diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index b91e4af3a..0f46fc123 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -70,6 +70,8 @@ void finite_set_decl_plugin::init() { m_sigs[OP_FINITE_SET_MAP] = alloc(polymorphism::psig, m, "set.map", 2, 2, arrABsetA, setB); m_sigs[OP_FINITE_SET_SELECT] = alloc(polymorphism::psig, m, "set.select", 1, 2, arrABoolsetA, setA); m_sigs[OP_FINITE_SET_RANGE] = alloc(polymorphism::psig, m, "set.range", 0, 2, intintT, setInt); + m_sigs[OP_FINITE_SET_DIFF] = alloc(polymorphism::psig, m, "set.diff", 1, 2, setAsetA, 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) { @@ -152,6 +154,7 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param case OP_FINITE_SET_MAP: case OP_FINITE_SET_SELECT: case OP_FINITE_SET_RANGE: + case OP_FINITE_SET_DIFF: return mk_finite_set_op(k, arity, domain, range); default: return nullptr; diff --git a/src/ast/finite_set_decl_plugin.h b/src/ast/finite_set_decl_plugin.h index c17b3f517..384217667 100644 --- a/src/ast/finite_set_decl_plugin.h +++ b/src/ast/finite_set_decl_plugin.h @@ -23,6 +23,7 @@ Operators: set.map : (S -> T) (FiniteSet S) -> (FiniteSet T) set.select : (S -> Bool) (FiniteSet S) -> (FiniteSet S) set.range : Int Int -> (FiniteSet Int) + set.diff : (FiniteSet S) (FiniteSet S) -> S --*/ #pragma once @@ -46,6 +47,8 @@ enum finite_set_op_kind { OP_FINITE_SET_MAP, OP_FINITE_SET_SELECT, OP_FINITE_SET_RANGE, + OP_FINITE_SET_DIFF, + OP_FINITE_SET_MAP_INVERSE, LAST_FINITE_SET_OP }; diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp index a0117ca6d..f16d619e8 100644 --- a/src/ast/rewriter/finite_set_axioms.cpp +++ b/src/ast/rewriter/finite_set_axioms.cpp @@ -298,4 +298,19 @@ void finite_set_axioms::subset_axiom(expr* a) { clause2.push_back(a); clause2.push_back(m.mk_not(eq)); m_add_clause(clause2); +} + +void finite_set_axioms::extensionality_axiom(expr *a, expr* b) { + // a != b => set.in (set.diff(a, b) a) != set.in (set.diff(a, b) b) + expr_ref diff_ab(u.mk_difference(a, b), m); + + expr_ref a_eq_b(m.mk_eq(a, b), m); + 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) + expr_ref_vector clause(m); + clause.push_back(a_eq_b); + clause.push_back(m.mk_not(m.mk_iff(diff_in_a, diff_in_b))); + m_add_clause(clause); } \ No newline at end of file diff --git a/src/ast/rewriter/finite_set_axioms.h b/src/ast/rewriter/finite_set_axioms.h index fad785cb4..250179911 100644 --- a/src/ast/rewriter/finite_set_axioms.h +++ b/src/ast/rewriter/finite_set_axioms.h @@ -69,4 +69,7 @@ public: // set.size(a) = 1 void size_singleton_axiom(expr *a); + // a != b => set.in (set.diff(a, b) a) != set.in (set.diff(a, b) b) + void extensionality_axiom(expr *a, expr *b); + }; \ No newline at end of file diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index abfe11503..13b6617eb 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -131,9 +131,18 @@ namespace smt { } void theory_finite_set::new_diseq_eh(theory_var v1, theory_var v2) { - TRACE(finite_set, tout << "new_diseq_eh: v" << v1 << " != v" << v2 << "\n";); - // Disequalities could trigger extensionality axioms - // For now, we rely on the final_check to handle this + TRACE(finite_set, tout << "new_diseq_eh: v" << v1 << " != v" << v2 << "\n"); + auto n1 = get_enode(v1); + auto n2 = get_enode(v2); + auto e1 = n1->get_expr(); + auto e2 = n2->get_expr(); + if (u.is_finite_set(e1) && u.is_finite_set(e2)) { + if (e1->get_id() > e2->get_id()) + std::swap(e1, e2); + if (!is_new_axiom(e1, e2)) + return; + m_axioms.extensionality_axiom(e1, e2); + } } /** @@ -143,7 +152,7 @@ namespace smt { * * It ensures saturation with respect to the theory axioms: * - membership axioms - * - extensionality axioms + * - assume eqs axioms */ final_check_status theory_finite_set::final_check_eh() { TRACE(finite_set, tout << "final_check_eh\n";); @@ -151,7 +160,7 @@ namespace smt { if (add_membership_axioms()) return FC_CONTINUE; - if (add_extensionality_axioms()) + if (assume_eqs()) return FC_CONTINUE; return FC_DONE; @@ -219,32 +228,76 @@ namespace smt { } /** - * Saturate with respect to extensionality: + * Saturate with respect to equality sharing: * - Sets corresponding to shared variables having the same interpretation should also be congruent */ - bool theory_finite_set::add_extensionality_axioms() { + bool theory_finite_set::assume_eqs() { + collect_members(); + expr_ref_vector trail(m); // make sure reference counts to union expressions are valid in this scope + obj_map set_reprs; + + auto start = ctx.get_random_value(); + auto sz = get_num_vars(); + for (unsigned w = 0; w < sz; ++w) { + auto v = (w + start) % sz; + enode* n = get_enode(v); + if (!u.is_finite_set(n->get_expr())) + continue; + if (!is_relevant_and_shared(n)) + continue; + auto r = n->get_root(); + // Create a union expression that is canonical (sorted) + auto& set = *m_set_members[r]; + ptr_vector elems; + for (auto e : set) + elems.push_back(e->get_expr()); + std::sort(elems.begin(), elems.end(), [](expr *a, expr *b) { return a->get_id() < b->get_id(); }); + expr* s = nullptr; + for (auto v : elems) + s = s ? u.mk_union(s, v) : v; + trail.push_back(s); + enode *n2 = nullptr; + if (!set_reprs.find(s, n2)) { + set_reprs.insert(s, n2); + continue; + } + if (n2->get_root() == r) + continue; + if (is_new_axiom(n->get_expr(), n2->get_expr()) && assume_eq(n, n2)) { + TRACE(finite_set, + tout << "assume " << mk_pp(n->get_expr(), m) << " = " << mk_pp(n2->get_expr(), m) << "\n";); + return true; + } + } return false; } + + bool theory_finite_set::is_new_axiom(expr* a, expr* b) { + struct insert_obj_pair_table : public trail { + obj_pair_hashtable &table; + expr *a, *b; + insert_obj_pair_table(obj_pair_hashtable &t, expr *a, expr *b) : table(t), a(a), b(b) {} + void undo() override { + table.erase({a, b}); + } + }; + if (m_lemma_exprs.contains({a, b})) + return false; + m_lemma_exprs.insert({a, b}); + ctx.push_trail(insert_obj_pair_table(m_lemma_exprs, a, b)); + return true; + } + /** * Instantiate axioms for a given element in a set. */ 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";); - struct insert_obj_pair_table : public trail { - obj_pair_hashtable &table; - expr *a, *b; - insert_obj_pair_table(obj_pair_hashtable &t, expr *a, expr *b) : - table(t), a(a), b(b) {} - void undo() override { - table.erase({a, b}); - } - }; - if (m_lemma_exprs.contains({elem, set})) + if (!is_new_axiom(elem, set)) return; - m_lemma_exprs.insert({elem, set}); - ctx.push_trail(insert_obj_pair_table(m_lemma_exprs, elem, set)); + // Instantiate appropriate axiom based on set structure if (u.is_empty(set)) { m_axioms.in_empty_axiom(elem); @@ -296,8 +349,6 @@ namespace smt { collect_members(); } - - void theory_finite_set::collect_members() { // This method can be used to collect all elements that are members of sets // and ensure that the model factory has values for them. diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index d017bb416..e32cb507d 100644 --- a/src/smt/theory_finite_set.h +++ b/src/smt/theory_finite_set.h @@ -128,7 +128,8 @@ namespace smt { lbool truth_value(expr *e); void add_immediate_axioms(app *atom); bool add_membership_axioms(); - bool add_extensionality_axioms(); + bool assume_eqs(); + bool is_new_axiom(expr *a, expr *b); // model construction void collect_members();