Merge branch 'finite-sets' into copilot/add-rewrite-rules-finite-set-rewriter

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;

src/ast/rewriter/finite_set_rewriter.h

@@ -34,14 +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);
-    br_status mk_singleton(expr * arg, expr_ref & result);
-    br_status mk_in(expr * elem, expr * set, expr_ref & result);
-public:
+    public:
     finite_set_rewriter(ast_manager & m, params_ref const & p = params_ref()):
         m_util(m) {
     }
@@ -52,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);
+
 };
 

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

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);

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();

src/smt/theory_finite_set.cpp

@@ -0,0 +1,262 @@
+/*++
+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<void(expr_ref_vector const &)> add_clause_fn = 
+            [this](expr_ref_vector const& 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";);
+
+        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(m_elements, 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;
+        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());
+            }
+        }
+        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";);
+        
+        struct insert_obj_pair_table : public trail {
+            obj_pair_hashtable<expr, expr> &table;
+            expr *a, *b;
+            insert_obj_pair_table(obj_pair_hashtable<expr, expr> &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);
+        }
+        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");
+        ctx.push_trail(push_back_vector(m_lemmas));
+        m_lemmas.push_back(clause);        
+    }
+
+    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;
+    }
+
+    bool theory_finite_set::instantiate_false_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

src/smt/theory_finite_set.h

@@ -57,20 +57,75 @@ 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 "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 {
+    class theory_finite_set : public theory {
+        friend class theory_finite_set_test;
+        finite_set_util           u;
+        finite_set_axioms         m_axioms;
+        obj_hashtable<enode>      m_elements;             // set of all 'x' where there is an 'x in S' atom
+        vector<expr_ref_vector>   m_lemmas;
+        obj_pair_hashtable<expr, expr> m_lemma_exprs;
+        
+    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 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);
+        ~theory_finite_set() override {}
+    };
+
+}  // namespace smt 

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);

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")