From f674d22ec817f03253e236d4558312f2c7e8ab38 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Oct 2025 08:54:00 +0200 Subject: [PATCH 1/7] update description for signature of the theory solver Signed-off-by: Nikolaj Bjorner --- src/smt/theory_finite_set.h | 36 +++++++++++++++++++++++++++++------- 1 file changed, 29 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index 982876a33..4666dd988 100644 --- a/src/smt/theory_finite_set.h +++ b/src/smt/theory_finite_set.h @@ -57,20 +57,42 @@ Abstract: ----------------------------------------------- x in v3 <=> p(x) and x in v4 +Rules are encoded in src/ast/rewriter/finite_set_axioms.cpp as clauses. + The central claim is that the above rules are sufficient to -decide satisfiability of finite set constraints. +decide satisfiability of finite set constraints for a subset +of operations, namely union, intersection, difference, singleton, membership. Model construction proceeds by selecting every set.in(x_i, v) for a congruence root v. Then the set of elements { x_i | set.in(x_i, v) } is the interpretation. -This approach, however, does not work with ranges, or is impractical. -For ranges, we are going to extract an interpretation for set variable v -directly from a set of range expressions. -Inductively, the interpretation of a range expression is given by the -range itself. It proceeds by taking unions, intersections and differences of range -interpretations. +This approach for model-construction, however, does not work with ranges, or is impractical. +For ranges we can adapt a different model construction approach. + +When introducing select and map, decidability can be lost. For Boolean lattice constraints given by equality, subset, strict subset and union, intersections, the theory solver uses a stand-alone satisfiability checker for Boolean algebras to close branches. +Instructions for copilot: + +1. Override relevant methods for smt::theory. Add them to the signature and add stubs or implementations in +theory_finite_set.cpp. +2. In final_check_eh add instantiation of theory axioms following the outline in the inference rules above. + An example of how to instantiate axioms is in theory_arrays_base.cpp and theroy_datatypes.cpp and other theory files. --*/ + +#pragma once + +#include "ast/ast.h" +#include "ast/ast_pp.h" +#include "smt/smt_theory.h" + +namespace smt { + class theory_finite_set : public theory { + public: + theory_finite_set(ast_manager & m); + ~theory_finite_set() override {} + }; + +} // namespace smt \ No newline at end of file From b24aec3c4cf6dfb5b2b0e63d8cf40cc8875649dd Mon Sep 17 00:00:00 2001 From: kper Date: Wed, 15 Oct 2025 14:03:00 +0200 Subject: [PATCH 2/7] Fixed tests by making methods public for finite sets (#7977) --- src/ast/rewriter/finite_set_rewriter.h | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/finite_set_rewriter.h b/src/ast/rewriter/finite_set_rewriter.h index cc028d3ff..ebffbbd44 100644 --- a/src/ast/rewriter/finite_set_rewriter.h +++ b/src/ast/rewriter/finite_set_rewriter.h @@ -34,12 +34,7 @@ where the signature is defined in finite_set_decl_plugin.h. */ class finite_set_rewriter { finite_set_util m_util; - // Rewrite rules for set operations - br_status mk_union(unsigned num_args, expr * const * args, expr_ref & result); - br_status mk_intersect(unsigned num_args, expr * const * args, expr_ref & result); - br_status mk_difference(expr * arg1, expr * arg2, expr_ref & result); - br_status mk_subset(expr * arg1, expr * arg2, expr_ref & result); -public: + public: finite_set_rewriter(ast_manager & m, params_ref const & p = params_ref()): m_util(m) { } @@ -50,5 +45,11 @@ public: br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); + // Rewrite rules for set operations + br_status mk_union(unsigned num_args, expr * const * args, expr_ref & result); + br_status mk_intersect(unsigned num_args, expr * const * args, expr_ref & result); + br_status mk_difference(expr * arg1, expr * arg2, expr_ref & result); + br_status mk_subset(expr * arg1, expr * arg2, expr_ref & result); + }; From 7446112fbec0e67f4935ce57834d91d0d4ad5612 Mon Sep 17 00:00:00 2001 From: kper Date: Wed, 15 Oct 2025 14:35:57 +0200 Subject: [PATCH 3/7] Implement more cases for `finite_set_decl_plugin::are_distinct` (#7978) * Implement more cases for finite_set_decl_plugin::are_distinct * Adapted distinctive checks for finite sets --- src/ast/finite_set_decl_plugin.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index 3a3a96bce..002887905 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -204,6 +204,9 @@ bool finite_set_decl_plugin::are_distinct(app* e1, app* e2) const { return true; if (r.is_singleton(e1) && r.is_empty(e2)) return true; + if(r.is_singleton(e1) && r.is_singleton(e2)) + return m_manager->are_distinct(e1, e2); + // TODO: could be extended to cases where we can prove the sets are different by containing one element // that the other doesn't contain. Such as (union (singleton a) (singleton b)) and (singleton c) where c is different from a, b. return false; From b4d41ffe815f5102ddb7e4e675d5e268a1bc82fb Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 15 Oct 2025 14:55:08 +0200 Subject: [PATCH 4/7] Complete theory_finite_set.h header and implement finite set theory solver (#7976) * Initial plan * Implement theory_finite_set header and implementation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add theory registration to smt_setup Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Update theory_finite_set.cpp * Refactor membership_atoms and add elements list Renamed membership_atoms to membership_elements and added elements list. * Change membership elements to use enode type * Update theory_finite_set.cpp * Fix typo in internalize_atom function * Update theory_finite_set.cpp * Refactor final_check_eh by removing comments Removed redundant comments and cleaned up code. * Add m_lemmas member to theory_finite_set class * Improve clause management and instantiation logic Refactor clause handling and instantiate logic in finite set theory. * Add friend class declaration for testing * Add placeholder methods for lemma instantiation Added placeholder methods for lemma instantiation. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/smt/CMakeLists.txt | 1 + src/smt/smt_setup.cpp | 6 + src/smt/smt_setup.h | 1 + src/smt/theory_finite_set.cpp | 209 ++++++++++++++++++++++++++++++++++ src/smt/theory_finite_set.h | 33 +++++- 5 files changed, 248 insertions(+), 2 deletions(-) create mode 100644 src/smt/theory_finite_set.cpp diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 01e3a9254..6d0e86b77 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -57,6 +57,7 @@ z3_add_component(smt theory_char.cpp theory_datatype.cpp theory_dense_diff_logic.cpp + theory_finite_set.cpp theory_diff_logic.cpp theory_dl.cpp theory_dummy.cpp diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index d655316ed..926818d78 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -40,6 +40,7 @@ Revision History: #include "smt/theory_pb.h" #include "smt/theory_fpa.h" #include "smt/theory_polymorphism.h" +#include "smt/theory_finite_set.h" namespace smt { @@ -784,6 +785,10 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_char, m_context)); } + void setup::setup_finite_set() { + m_context.register_plugin(alloc(smt::theory_finite_set, m_context)); + } + void setup::setup_special_relations() { m_context.register_plugin(alloc(smt::theory_special_relations, m_context, m_manager)); } @@ -807,6 +812,7 @@ namespace smt { setup_dl(); setup_seq_str(st); setup_fpa(); + setup_finite_set(); setup_special_relations(); setup_polymorphism(); setup_relevancy(st); diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index 3d2bf47f3..897755ef7 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -102,6 +102,7 @@ namespace smt { void setup_seq_str(static_features const & st); void setup_seq(); void setup_char(); + void setup_finite_set(); void setup_card(); void setup_sls(); void setup_i_arith(); diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp new file mode 100644 index 000000000..72b25d16a --- /dev/null +++ b/src/smt/theory_finite_set.cpp @@ -0,0 +1,209 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + theory_finite_set.cpp + +Abstract: + + Theory solver for finite sets. + Implements axiom schemas for finite set operations. + +Author: + + GitHub Copilot Agent 2025 + +Revision History: + +--*/ + +#include "smt/theory_finite_set.h" +#include "smt/smt_context.h" +#include "smt/smt_model_generator.h" +#include "ast/ast_pp.h" + +namespace smt { + + theory_finite_set::theory_finite_set(context& ctx): + theory(ctx, ctx.get_manager().mk_family_id("finite_set")), + u(m), + m_axioms(m) + { + // Setup the add_clause callback for axioms + std::function add_clause_fn = + [this](expr_ref_vector const& clause) { + this->m_lemmas.push_back(clause); + }; + m_axioms.set_add_clause(add_clause_fn); + } + + bool theory_finite_set::internalize_atom(app * atom, bool gate_ctx) { + TRACE("finite_set", tout << "internalize_atom: " << mk_pp(atom, m) << "\n";); + + internalize_term(atom); + + // Track membership elements (set.in) + expr* elem = nullptr, *set = nullptr; + if (u.is_in(atom, elem, set)) { + auto n = ctx.get_enode(elem); + if (!m_elements.contains(n)) { + m_elements.insert(n); + ctx.push_trail(insert_obj_trail(n)); + } + } + + return true; + } + + bool theory_finite_set::internalize_term(app * term) { + TRACE("finite_set", tout << "internalize_term: " << mk_pp(term, m) << "\n";); + + // Internalize all arguments first + for (expr* arg : *term) + ctx.internalize(arg, false); + + // Create boolean variable for Boolean terms + if (m.is_bool(term) && !ctx.b_internalized(term)) { + bool_var bv = ctx.mk_bool_var(term); + ctx.set_var_theory(bv, get_id()); + } + + // Create enode for the term if needed + enode* e = nullptr; + if (ctx.e_internalized(term)) + e = ctx.get_enode(term); + else + e = ctx.mk_enode(term, false, m.is_bool(term), true); + + // Attach theory variable if this is a set + if (!is_attached_to_var(e)) + ctx.attach_th_var(e, this, mk_var(e)); + + return true; + } + + void theory_finite_set::new_eq_eh(theory_var v1, theory_var v2) { + TRACE("finite_set", tout << "new_eq_eh: v" << v1 << " = v" << v2 << "\n";); + // When two sets are equal, propagate membership constraints + // This is handled by congruence closure, so no additional work needed here + } + + 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 + } + + final_check_status theory_finite_set::final_check_eh() { + TRACE("finite_set", tout << "final_check_eh\n";); + + // walk all parents of elem in congruence table. + // if a parent is of the form elem' in S u T, or similar. + // create clauses for elem in S u T. + + expr* elem1 = nullptr, *set1 = nullptr; + m_lemmas.reset(); + for (auto elem : m_elements) { + for (auto p : enode::parents(elem)) { + if (!u.is_in(p->get_expr(), elem1, set1)) + continue; + if (elem->get_root() != p->get_arg(0)->get_root()) + continue; // elem is then equal to set1 but not elem1. This is a different case. + for (auto sib : *p->get_arg(1)) + instantiate_axioms(elem->get_expr(), sib->get_expr()); + } + } + if (instantiate_false_lemma()) + return FC_CONTINUE; + if (instantiate_unit_propagation()) + return FC_CONTINUE; + if (instantiate_free_lemma()) + return FC_CONTINUE; + + return FC_DONE; + } + + void theory_finite_set::instantiate_axioms(expr* elem, expr* set) { + TRACE("finite_set", tout << "instantiate_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";); + + // Instantiate appropriate axiom based on set structure + 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_select(set)) { + m_axioms.in_select_axiom(elem, set); + } + + // Instantiate size axioms for singleton sets + // TODO, such axioms don't belong here + if (u.is_singleton(set)) { + m_axioms.size_singleton_axiom(set); + } + } + + void theory_finite_set::add_clause(expr_ref_vector const& clause) { + TRACE("finite_set", + tout << "add_clause: " << clause << "\n"); + + // Convert expressions to literals and assert the clause + literal_vector lits; + for (expr* e : clause) { + ctx.internalize(e, false); + literal lit = ctx.get_literal(lit_expr); + lits.push_back(lit); + } + + if (!lits.empty()) { + scoped_trace_stream _sts(*this, lits); + ctx.mk_th_axiom(get_id(), lits); + } + } + + theory * theory_finite_set::mk_fresh(context * new_ctx) { + return alloc(theory_finite_set, *new_ctx); + } + + void theory_finite_set::display(std::ostream & out) const { + out << "theory_finite_set:\n"; + } + + void theory_finite_set::init_model(model_generator & mg) { + TRACE("finite_set", tout << "init_model\n";); + // Model generation will use default interpretation for sets + // The model will be constructed based on the membership literals that are true + } + + model_value_proc * theory_finite_set::mk_value(enode * n, model_generator & mg) { + TRACE("finite_set", tout << "mk_value: " << mk_pp(n->get_expr(), m) << "\n";); + + // For now, return nullptr to use default model construction + // A complete implementation would construct explicit set values + // based on true membership literals + return nullptr; + } + + void theory_finite_set::instantiate_false_lemma() {} + void theory_finite_set::instantiate_unit_propagation() {} + void theory_finite_set::instantiate_free_lemma() {} + +} // namespace smt diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index 4666dd988..59a8651a7 100644 --- a/src/smt/theory_finite_set.h +++ b/src/smt/theory_finite_set.h @@ -86,13 +86,42 @@ theory_finite_set.cpp. #include "ast/ast.h" #include "ast/ast_pp.h" +#include "ast/finite_set_decl_plugin.h" +#include "ast/rewriter/finite_set_axioms.h" #include "smt/smt_theory.h" namespace smt { class theory_finite_set : public theory { + friend class theory_finite_set_test; + finite_set_util u; + finite_set_axioms m_axioms; + obj_hashtable m_elements; // set of all 'x' where there is an 'x in S' atom + vector m_lemmas; + + protected: + // Override relevant methods from smt::theory + bool internalize_atom(app * atom, bool gate_ctx) override; + bool internalize_term(app * term) override; + void new_eq_eh(theory_var v1, theory_var v2) override; + void new_diseq_eh(theory_var v1, theory_var v2) override; + final_check_status final_check_eh() override; + + theory * mk_fresh(context * new_ctx) override; + char const * get_name() const override { return "finite_set"; } + void display(std::ostream & out) const override; + void init_model(model_generator & mg) override; + model_value_proc * mk_value(enode * n, model_generator & mg) override; + + // Helper methods for axiom instantiation + void instantiate_axioms(expr* elem, expr* set); + void add_clause(expr_ref_vector const& clause); + void instantiate_false_lemma(); + void instantiate_unit_propagation(); + void instantiate_free_lemma(); + public: - theory_finite_set(ast_manager & m); + theory_finite_set(context& ctx); ~theory_finite_set() override {} }; -} // namespace smt \ No newline at end of file +} // namespace smt From 54980a38d4e05376e3a87d9713d3de5d04236188 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Oct 2025 15:02:58 +0200 Subject: [PATCH 5/7] fixup theory_finite_set Signed-off-by: Nikolaj Bjorner --- src/smt/theory_finite_set.cpp | 39 +++++++++++++++++++++-------------- src/smt/theory_finite_set.h | 6 +++--- 2 files changed, 27 insertions(+), 18 deletions(-) diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index 72b25d16a..fc279a5d2 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -39,7 +39,7 @@ namespace smt { } bool theory_finite_set::internalize_atom(app * atom, bool gate_ctx) { - TRACE("finite_set", tout << "internalize_atom: " << mk_pp(atom, m) << "\n";); + // TRACE(finite_set, tout << "internalize_atom: " << mk_pp(atom, m) << "\n";); internalize_term(atom); @@ -49,7 +49,7 @@ namespace smt { auto n = ctx.get_enode(elem); if (!m_elements.contains(n)) { m_elements.insert(n); - ctx.push_trail(insert_obj_trail(n)); + ctx.push_trail(insert_obj_trail(m_elements, n)); } } @@ -57,7 +57,7 @@ namespace smt { } bool theory_finite_set::internalize_term(app * term) { - TRACE("finite_set", tout << "internalize_term: " << mk_pp(term, m) << "\n";); + // TRACE("finite_set", tout << "internalize_term: " << mk_pp(term, m) << "\n";); // Internalize all arguments first for (expr* arg : *term) @@ -84,19 +84,19 @@ namespace smt { } void theory_finite_set::new_eq_eh(theory_var v1, theory_var v2) { - TRACE("finite_set", tout << "new_eq_eh: v" << v1 << " = v" << v2 << "\n";); + // TRACE("finite_set", tout << "new_eq_eh: v" << v1 << " = v" << v2 << "\n";); // When two sets are equal, propagate membership constraints // This is handled by congruence closure, so no additional work needed here } 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";); + // 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 } final_check_status theory_finite_set::final_check_eh() { - TRACE("finite_set", tout << "final_check_eh\n";); + // TRACE("finite_set", tout << "final_check_eh\n";); // walk all parents of elem in congruence table. // if a parent is of the form elem' in S u T, or similar. @@ -125,7 +125,7 @@ namespace smt { } void theory_finite_set::instantiate_axioms(expr* elem, expr* set) { - TRACE("finite_set", tout << "instantiate_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";); + // TRACE("finite_set", tout << "instantiate_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";); // Instantiate appropriate axiom based on set structure if (u.is_empty(set)) { @@ -162,14 +162,14 @@ namespace smt { } void theory_finite_set::add_clause(expr_ref_vector const& clause) { - TRACE("finite_set", - tout << "add_clause: " << clause << "\n"); + //TRACE("finite_set", + // tout << "add_clause: " << clause << "\n"); // Convert expressions to literals and assert the clause literal_vector lits; for (expr* e : clause) { ctx.internalize(e, false); - literal lit = ctx.get_literal(lit_expr); + literal lit = ctx.get_literal(e); lits.push_back(lit); } @@ -188,13 +188,13 @@ namespace smt { } void theory_finite_set::init_model(model_generator & mg) { - TRACE("finite_set", tout << "init_model\n";); + // TRACE("finite_set", tout << "init_model\n";); // Model generation will use default interpretation for sets // The model will be constructed based on the membership literals that are true } model_value_proc * theory_finite_set::mk_value(enode * n, model_generator & mg) { - TRACE("finite_set", tout << "mk_value: " << mk_pp(n->get_expr(), m) << "\n";); + // TRACE("finite_set", tout << "mk_value: " << mk_pp(n->get_expr(), m) << "\n";); // For now, return nullptr to use default model construction // A complete implementation would construct explicit set values @@ -202,8 +202,17 @@ namespace smt { return nullptr; } - void theory_finite_set::instantiate_false_lemma() {} - void theory_finite_set::instantiate_unit_propagation() {} - void theory_finite_set::instantiate_free_lemma() {} + bool theory_finite_set::instantiate_false_lemma() { + // Implementation for instantiating false lemma + return false; + } + bool theory_finite_set::instantiate_unit_propagation() { + // Implementation for instantiating unit propagation + return false; + } + bool theory_finite_set::instantiate_free_lemma() { + // Implementation for instantiating free lemma + return false; + } } // namespace smt diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index 59a8651a7..62506ac4c 100644 --- a/src/smt/theory_finite_set.h +++ b/src/smt/theory_finite_set.h @@ -115,9 +115,9 @@ namespace smt { // Helper methods for axiom instantiation void instantiate_axioms(expr* elem, expr* set); void add_clause(expr_ref_vector const& clause); - void instantiate_false_lemma(); - void instantiate_unit_propagation(); - void instantiate_free_lemma(); + bool instantiate_false_lemma(); + bool instantiate_unit_propagation(); + bool instantiate_free_lemma(); public: theory_finite_set(context& ctx); From 30878541c82a4d2e12383cb214c159eb50c82354 Mon Sep 17 00:00:00 2001 From: kper Date: Wed, 15 Oct 2025 17:03:46 +0200 Subject: [PATCH 6/7] Changed sort of mk_empty to fix test (#7979) --- src/test/finite_set.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/test/finite_set.cpp b/src/test/finite_set.cpp index b7b07f074..ca6ae35bb 100644 --- a/src/test/finite_set.cpp +++ b/src/test/finite_set.cpp @@ -37,16 +37,16 @@ static void tst_finite_set_basic() { ENSURE(fsets.is_finite_set(finite_set_int.get())); // Test creating empty set - app_ref empty_set(fsets.mk_empty(int_sort), m); + app_ref empty_set(fsets.mk_empty(finite_set_int), m); ENSURE(fsets.is_empty(empty_set.get())); ENSURE(empty_set->get_sort() == finite_set_int.get()); - + // Test set.singleton expr_ref five(arith.mk_int(5), m); app_ref singleton_set(fsets.mk_singleton(five), m); ENSURE(fsets.is_singleton(singleton_set.get())); ENSURE(singleton_set->get_sort() == finite_set_int.get()); - + // Test set.range expr_ref zero(arith.mk_int(0), m); expr_ref ten(arith.mk_int(10), m); From 4225f1a0f1f22bcbf636564810695f9273bbb768 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Oct 2025 18:33:22 +0200 Subject: [PATCH 7/7] prove your first finite set theorem Signed-off-by: Nikolaj Bjorner --- src/smt/theory_finite_set.cpp | 112 +++++++++++++++++++++++----------- src/smt/theory_finite_set.h | 4 ++ src/util/trace_tags.def | 2 + 3 files changed, 84 insertions(+), 34 deletions(-) diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index fc279a5d2..ae0cafad2 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -33,13 +33,13 @@ namespace smt { // Setup the add_clause callback for axioms std::function add_clause_fn = [this](expr_ref_vector const& clause) { - this->m_lemmas.push_back(clause); + this->add_clause(clause); }; m_axioms.set_add_clause(add_clause_fn); } bool theory_finite_set::internalize_atom(app * atom, bool gate_ctx) { - // TRACE(finite_set, tout << "internalize_atom: " << mk_pp(atom, m) << "\n";); + TRACE(finite_set, tout << "internalize_atom: " << mk_pp(atom, m) << "\n";); internalize_term(atom); @@ -57,7 +57,7 @@ namespace smt { } bool theory_finite_set::internalize_term(app * term) { - // TRACE("finite_set", tout << "internalize_term: " << mk_pp(term, m) << "\n";); + TRACE(finite_set, tout << "internalize_term: " << mk_pp(term, m) << "\n";); // Internalize all arguments first for (expr* arg : *term) @@ -84,32 +84,35 @@ namespace smt { } void theory_finite_set::new_eq_eh(theory_var v1, theory_var v2) { - // TRACE("finite_set", tout << "new_eq_eh: v" << v1 << " = v" << v2 << "\n";); + TRACE(finite_set, tout << "new_eq_eh: v" << v1 << " = v" << v2 << "\n";); // When two sets are equal, propagate membership constraints // This is handled by congruence closure, so no additional work needed here } 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";); + 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 } final_check_status theory_finite_set::final_check_eh() { - // TRACE("finite_set", tout << "final_check_eh\n";); + TRACE(finite_set, tout << "final_check_eh\n";); // walk all parents of elem in congruence table. // if a parent is of the form elem' in S u T, or similar. // create clauses for elem in S u T. expr* elem1 = nullptr, *set1 = nullptr; - m_lemmas.reset(); for (auto elem : m_elements) { + if (!ctx.is_relevant(elem)) + continue; for (auto p : enode::parents(elem)) { if (!u.is_in(p->get_expr(), elem1, set1)) continue; if (elem->get_root() != p->get_arg(0)->get_root()) continue; // elem is then equal to set1 but not elem1. This is a different case. + if (!ctx.is_relevant(p)) + continue; for (auto sib : *p->get_arg(1)) instantiate_axioms(elem->get_expr(), sib->get_expr()); } @@ -125,8 +128,21 @@ namespace smt { } void theory_finite_set::instantiate_axioms(expr* elem, expr* set) { - // TRACE("finite_set", tout << "instantiate_axioms: " << mk_pp(elem, m) << " in " << mk_pp(set, m) << "\n";); + TRACE(finite_set, tout << "instantiate_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})) + 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); @@ -162,21 +178,9 @@ namespace smt { } void theory_finite_set::add_clause(expr_ref_vector const& clause) { - //TRACE("finite_set", - // tout << "add_clause: " << clause << "\n"); - - // Convert expressions to literals and assert the clause - literal_vector lits; - for (expr* e : clause) { - ctx.internalize(e, false); - literal lit = ctx.get_literal(e); - lits.push_back(lit); - } - - if (!lits.empty()) { - scoped_trace_stream _sts(*this, lits); - ctx.mk_th_axiom(get_id(), lits); - } + TRACE(finite_set, tout << "add_clause: " << clause << "\n"); + ctx.push_trail(push_back_vector(m_lemmas)); + m_lemmas.push_back(clause); } theory * theory_finite_set::mk_fresh(context * new_ctx) { @@ -188,13 +192,13 @@ namespace smt { } void theory_finite_set::init_model(model_generator & mg) { - // TRACE("finite_set", tout << "init_model\n";); + TRACE(finite_set, tout << "init_model\n";); // Model generation will use default interpretation for sets // The model will be constructed based on the membership literals that are true } model_value_proc * theory_finite_set::mk_value(enode * n, model_generator & mg) { - // TRACE("finite_set", tout << "mk_value: " << mk_pp(n->get_expr(), m) << "\n";); + TRACE(finite_set, tout << "mk_value: " << mk_pp(n->get_expr(), m) << "\n";); // For now, return nullptr to use default model construction // A complete implementation would construct explicit set values @@ -203,16 +207,56 @@ namespace smt { } bool theory_finite_set::instantiate_false_lemma() { - // Implementation for instantiating false lemma - return false; - } - bool theory_finite_set::instantiate_unit_propagation() { - // Implementation for instantiating unit propagation - return false; - } - bool theory_finite_set::instantiate_free_lemma() { - // Implementation for instantiating free lemma + for (auto const& clause : m_lemmas) { + bool all_false = all_of(clause, [&](expr *e) { return ctx.find_assignment(e) == l_false; }); + if (!all_false) + continue; + assert_clause(clause); + return true; + } return false; } + bool theory_finite_set::instantiate_unit_propagation() { + for (auto const &clause : m_lemmas) { + expr *undef = nullptr; + bool is_unit_propagating = true; + for (auto e : clause) { + switch (ctx.find_assignment(e)) { + case l_false: continue; + case l_true: is_unit_propagating = false; break; + case l_undef: + if (undef != nullptr) + is_unit_propagating = false; + undef = e; + break; + } + if (!is_unit_propagating) + break; + } + if (!is_unit_propagating || undef == nullptr) + continue; + assert_clause(clause); + return true; + } + return false; + } + + bool theory_finite_set::instantiate_free_lemma() { + for (auto const& clause : m_lemmas) { + if (any_of(clause, [&](expr *e) { return ctx.find_assignment(e) == l_true; })) + continue; + assert_clause(clause); + return true; + } + return false; + } + + void theory_finite_set::assert_clause(expr_ref_vector const &clause) { + literal_vector lclause; + for (auto e : clause) + lclause.push_back(mk_literal(e)); + ctx.mk_th_axiom(get_id(), lclause); + } + } // namespace smt diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index 62506ac4c..418384252 100644 --- a/src/smt/theory_finite_set.h +++ b/src/smt/theory_finite_set.h @@ -88,6 +88,7 @@ theory_finite_set.cpp. #include "ast/ast_pp.h" #include "ast/finite_set_decl_plugin.h" #include "ast/rewriter/finite_set_axioms.h" +#include "util/obj_pair_hashtable.h" #include "smt/smt_theory.h" namespace smt { @@ -97,6 +98,7 @@ namespace smt { finite_set_axioms m_axioms; obj_hashtable m_elements; // set of all 'x' where there is an 'x in S' atom vector m_lemmas; + obj_pair_hashtable m_lemma_exprs; protected: // Override relevant methods from smt::theory @@ -115,9 +117,11 @@ namespace smt { // Helper methods for axiom instantiation void instantiate_axioms(expr* elem, expr* set); void add_clause(expr_ref_vector const& clause); + void assert_clause(expr_ref_vector const &clause); bool instantiate_false_lemma(); bool instantiate_unit_propagation(); bool instantiate_free_lemma(); + lbool truth_value(expr *e); public: theory_finite_set(context& ctx); diff --git a/src/util/trace_tags.def b/src/util/trace_tags.def index ffa631d7a..545c903e4 100644 --- a/src/util/trace_tags.def +++ b/src/util/trace_tags.def @@ -70,6 +70,8 @@ X(eq_der, top_sort, "top sort") X(expr_substitution_simplifier, expr_substitution_simplifier, "expr substitution simplifier") X(expr_substitution_simplifier, propagate_values, "propagate values") +X(finite_set, finite_set, "finite set") + X(fm_model_converter, fm_model_converter, "fm model converter") X(fm_model_converter, fm_mc, "fm mc")