base implementation for cardinality constraints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/ast.cpp

@@ -3356,8 +3356,8 @@ proof * ast_manager::mk_th_lemma(
     }
     pr = mk_app(get_family_name(tid), args.size(), args.data(), mk_proof_sort());
     args.reset();
-    args.push_back(pr.get());
     args.append(num_proofs, (expr**) proofs);
+    args.push_back(pr.get());
     args.push_back(fact);
     return mk_app(basic_family_id, PR_TH_LEMMA, parameters.size(), parameters.data(), args.size(), args.data());
 }

src/ast/ast.h

@@ -2328,7 +2328,7 @@ public:
     unsigned get_num_parents(proof const * p) const {
         SASSERT(is_proof(p));
         unsigned n = p->get_num_args();
-        return !has_fact(p) ? n : n - 1;
+        return p->get_decl()->get_decl_kind() == PR_TH_LEMMA ? n - 2 : !has_fact(p) ? n : n - 1;
     }
     proof * get_parent(proof const * p, unsigned idx) const { SASSERT(is_proof(p)); return to_app(p->get_arg(idx)); }
     proof * mk_true_proof();

src/ast/rewriter/finite_set_axioms.h

@@ -12,6 +12,7 @@ Abstract:
        
 --*/
 
+#pragma once
 #include "ast/rewriter/th_rewriter.h"
 
 struct theory_axiom {

src/smt/CMakeLists.txt

@@ -58,6 +58,7 @@ z3_add_component(smt
     theory_datatype.cpp
     theory_dense_diff_logic.cpp
     theory_finite_set.cpp
+    theory_finite_set_size.cpp
     theory_diff_logic.cpp
     theory_dl.cpp
     theory_dummy.cpp

src/smt/theory_finite_set.cpp

@@ -27,7 +27,8 @@ 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), m_find(*this)
+        m_axioms(m), m_find(*this),
+        m_cardinality_solver(*this)
     {
         // Setup the add_clause callback for axioms
         std::function<void(theory_axiom *)> add_clause_fn =
@@ -108,6 +109,10 @@ namespace smt {
         }
         else if (u.is_range(e)) {
             
+        }
+        else if (u.is_size(e)) {
+            auto f = to_app(e)->get_decl();
+            m_cardinality_solver.add_set_size(f);
         }
         return r;
     }
@@ -246,7 +251,13 @@ 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";);
-        m_find.merge(v1, v2); // triggers merge_eh, which triggers incremental generation of theory axioms
+        auto n1 = get_enode(v1);
+        auto n2 = get_enode(v2);
+        if (u.is_finite_set(n1->get_expr()) && u.is_finite_set(n2->get_expr())) {
+            m_eqs.push_back({v1, v2});
+            ctx.push_trail(push_back_vector(m_eqs));
+            m_find.merge(v1, v2);  // triggers merge_eh, which triggers incremental generation of theory axioms
+        }
     }
 
     /**
@@ -266,6 +277,8 @@ namespace smt {
                 return;
             if (are_forced_distinct(n1, n2))
                 return;
+            m_diseqs.push_back({v1, v2});
+            ctx.push_trail(push_back_vector(m_diseqs));
             m_axioms.extensionality_axiom(e1, e2);
         }
     }
@@ -301,8 +314,41 @@ namespace smt {
 
         if (assume_eqs())
             return FC_CONTINUE;
+
+        switch (m_cardinality_solver.final_check()) {
+        case l_true: break;
+        case l_false: return FC_CONTINUE;
+        case l_undef: return FC_GIVEUP;
+        }
         
-        return FC_DONE;
+        return is_fully_solved() ? FC_DONE : FC_GIVEUP;
+    }
+
+    /**
+    * Determine if the constraints are fully solved.
+    * They can be fully solved if:
+    * - the model that is going to be produced satisfies all constraints
+    * The model will always satisfy the constraints if:
+    * - there is no occurrence of set.map
+    * - there is not both set.size and set.filter
+    */
+    bool theory_finite_set::is_fully_solved() {
+        bool has_map = false, has_filter = false, has_size = false;
+        for (unsigned v = 0; v < get_num_vars(); ++v) {
+            auto n = get_enode(v);
+            auto e = n->get_expr();
+            if (u.is_filter(e))
+                has_filter = true;
+            if (u.is_map(e))
+                has_map = true;
+            if (u.is_size(e))
+                has_size = true;
+        }
+        if (has_map)
+            return false; // todo use more expensive model check here
+        if (has_filter && has_size)
+            return false; // tood use more expensive model check here
+        return true;
     }
 
 

src/smt/theory_finite_set.h

@@ -75,12 +75,6 @@ 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
@@ -92,12 +86,16 @@ theory_finite_set.cpp.
 #include "util/obj_pair_hashtable.h"
 #include "util/union_find.h"
 #include "smt/smt_theory.h"
+#include "smt/theory_finite_set_size.h"
 #include "model/finite_set_factory.h"
 
 namespace smt {
+    class context;
+
     class theory_finite_set : public theory {
         using th_union_find = union_find<theory_finite_set>;
         friend class theory_finite_set_test;
+        friend class theory_finite_set_size;
         friend struct finite_set_value_proc;
 
         struct var_data {
@@ -135,18 +133,16 @@ namespace smt {
             }
         };
 
-        struct range {
-            rational lo, hi;
-        };
-
         finite_set_util           u;
         finite_set_axioms         m_axioms;
         th_union_find             m_find;
         theory_clauses            m_clauses;
+        theory_finite_set_size m_cardinality_solver;
         finite_set_factory *m_factory = nullptr;
         obj_map<enode, obj_map<enode, bool> *> m_set_members;
         ptr_vector<func_decl> m_set_in_decls;
         ptr_vector<var_data> m_var_data;
+        svector<std::pair<theory_var, theory_var>> m_diseqs, m_eqs;
         stats m_stats;
                
     protected:
@@ -172,6 +168,13 @@ namespace smt {
         void collect_statistics(::statistics & st) const override {
             m_stats.collect_statistics(st);
         }
+        void add_theory_assumptions(expr_ref_vector& assumptions) override {
+            m_cardinality_solver.add_theory_assumptions(assumptions);
+        }
+
+        bool should_research(expr_ref_vector& unsat_core) override {
+            return m_cardinality_solver.should_research(unsat_core);
+        }
 
 
         void add_in_axioms(theory_var v1, theory_var v2);
@@ -189,6 +192,7 @@ namespace smt {
         bool assume_eqs();
         bool is_new_axiom(expr *a, expr *b);
         app *mk_union(unsigned num_elems, expr *const *elems, sort* set_sort);
+        bool is_fully_solved();
 
         // model construction
         void collect_members();

src/smt/theory_finite_set_size.cpp

@@ -0,0 +1,412 @@
+
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    theory_finite_set_size.cpp
+
+Abstract:
+
+    Theory solver for finite sets.
+    Implements axiom schemas for finite set operations.
+
+--*/
+
+#include "smt/theory_finite_set.h"
+#include "smt/theory_finite_set_size.h"
+#include "smt/smt_context.h"
+#include "smt/smt_model_generator.h"
+#include "smt/smt_arith_value.h"
+#include "ast/ast_pp.h"
+
+namespace smt {
+
+    theory_finite_set_size::theory_finite_set_size(theory_finite_set& th): 
+        m(th.m), ctx(th.ctx), th(th), u(m), m_assumption(m) {}
+
+    void theory_finite_set_size::add_set_size(func_decl* f) {
+        if (!m_set_size_decls.contains(f)) {
+            m_set_size_decls.push_back(f);
+            ctx.push_trail(push_back_trail(m_set_size_decls));
+        }
+    }
+
+    void theory_finite_set_size::initialize_solver() {
+        struct clear_solver : public trail {
+            theory_finite_set_size &s;
+        public:
+            clear_solver(theory_finite_set_size &s) : s(s) {}
+            void undo() override {
+                s.m_solver = nullptr;
+                s.n2b.reset();
+                s.m_assumptions.reset();
+            }
+        };
+        ctx.push_trail(clear_solver(*this));
+        m_solver = alloc(context, m, ctx.get_fparams(), ctx.get_params());
+        // collect all expressons that use cardinality constraints
+        // collect cone of influence of sets terminals used in cardinality constraints
+        // for every visited uninterpreted set variable add a Boolean variable
+        // for every visited set expression add definitions as constraints to m_cardinality solver
+        // introduce fresh variables for set membership constraints
+        // assume that distinct enodes in set memberships produce different sets
+        // assert added disequalities
+        // assert equalities based on union-find equalities
+        // assert set membership constraints by in
+
+        enode_vector ns;
+        collect_subexpressions(ns);
+        create_singleton_sets_from_membership(ns);
+        //
+        // we now got all subexpressions from equalities, disequalities, set.in
+        //        
+        // associate a Boolean variable with every set enode
+        expr_ref_vector bs(m);
+        for (auto n : ns) {
+            std::ostringstream strm;
+            strm << enode_pp(n, ctx);
+            symbol name = symbol(strm.str());
+            expr_ref b(m.mk_const(name, m.mk_bool_sort()), m);
+            bs.push_back(b);
+            n2b.insert(n, b);
+        }
+
+        add_def_axioms(ns);
+        add_singleton_axioms(ns); // (set.in x s) -> |{x}| = 1
+        add_diseq_axioms(ns);     // |x\y| > 0 or |y\x| > 0
+        add_eq_axioms(ns);
+
+        TRACE(finite_set, display(tout));
+    }
+
+    /**
+    * For every (supported) set expression ensure associated Boolean expressions follow semantics
+    */
+    void theory_finite_set_size::add_def_axioms(enode_vector const& ns) {
+        for (auto n : ns) {
+            expr *e = n->get_expr();
+            if (u.is_union(e)) {
+                auto a = n2b[n->get_arg(0)];
+                auto b = n2b[n->get_arg(1)];
+                m_solver->assert_expr(m.mk_iff(n2b[n], m.mk_or(a, b)));
+            }
+            else if (u.is_intersect(e)) {
+                auto a = n2b[n->get_arg(0)];
+                auto b = n2b[n->get_arg(1)];
+                m_solver->assert_expr(m.mk_iff(n2b[n], m.mk_and(a, b)));
+            }
+            else if (u.is_difference(e)) {
+                auto a = n2b[n->get_arg(0)];
+                auto not_b = m.mk_not(n2b[n->get_arg(1)]);
+                m_solver->assert_expr(m.mk_iff(n2b[n], m.mk_and(a, not_b)));
+            }
+        }
+    }
+
+    enode* theory_finite_set_size::mk_singleton(enode* n) {
+        expr_ref s(u.mk_singleton(n->get_expr()), m);
+        ctx.ensure_internalized(s);
+        ctx.mark_as_relevant(s.get());
+        return ctx.get_enode(s);
+    }
+
+    enode* theory_finite_set_size::mk_diff(enode* a, enode* b) {
+        expr_ref d(u.mk_difference(a->get_expr(), b->get_expr()), m);
+        ctx.ensure_internalized(d);
+        ctx.mark_as_relevant(d.get());
+        return ctx.get_enode(d);
+    }
+
+    /**
+     * For every set membership (set.in x s) add axiom for (set.subset (set.singleton x) s)
+     */
+
+    void theory_finite_set_size::add_singleton_axioms(enode_vector const &ns) {
+        for (auto n : ns) {
+            for (auto p : enode::parents(n)) {
+                if (!u.is_in(p->get_expr()))
+                    continue;
+                if (!ctx.is_relevant(p))
+                    continue;
+                auto v = ctx.get_assignment(p);
+                if (v == l_undef)
+                    continue;
+                auto e = p->get_arg(0)->get_root();
+                auto s = mk_singleton(e);
+                SASSERT(n2b.contains(e));
+                SASSERT(n2b.contains(s));
+                auto is_in = m.mk_implies(n2b[s], n2b[p->get_arg(1)]);
+                if (v == l_false)
+                    is_in = m.mk_not(is_in);
+                in lit(p, v == l_true);
+                expr* b = m.mk_const(symbol("set.in"), m.mk_bool_sort());
+                m_assumptions.insert(b, lit);
+                m_solver->assert_expr(is_in);
+            }
+        }
+    }
+
+    /**
+    * For every asserted equality ensure equivalence
+    */
+    void theory_finite_set_size::add_eq_axioms(enode_vector const &ns) {
+        for (auto [a, b] : th.m_eqs) {
+            auto x = th.get_enode(a);
+            auto y = th.get_enode(b);
+            if (n2b.contains(x) && n2b.contains(y)) {
+                eq e = {a, b};
+                auto t = m.mk_const(symbol("eq"), m.mk_bool_sort());
+                m_assumptions.insert(t, e);
+                m_solver->assert_expr(m.mk_implies(t, m.mk_iff(n2b[x], n2b[y])));
+            }
+        }
+    }
+
+    /*
+    * For every disequality include the assertions x = y or |x\y| >= 1 or |y\z| >= 1
+    * The expressions x\y and y\x are created when ns is created.
+    */
+    void theory_finite_set_size::add_diseq_axioms(enode_vector const &ns) {
+        for (auto [a, b] : th.m_diseqs) {
+            auto x = th.get_enode(a);
+            auto y = th.get_enode(b);
+            if (n2b.contains(x) && n2b.contains(y)) {
+                diseq d = {a, b};
+                auto b = m.mk_const(symbol("!="), m.mk_bool_sort());
+                m_assumptions.insert(b, d);
+                m_solver->assert_expr(m.mk_implies(b, m.mk_not(m.mk_iff(n2b[x], n2b[y]))));
+                arith_util a(m);
+                auto d1 = mk_diff(x, y);
+                auto d2 = mk_diff(y, x);
+                expr_ref sz1(u.mk_size(d1->get_expr()), m);
+                expr_ref sz2(u.mk_size(d2->get_expr()), m);
+                literal l_eq = th.mk_literal(m.mk_eq(x->get_expr(), y->get_expr()));
+                literal l1 = th.mk_literal(a.mk_ge(sz1, a.mk_int(1)));
+                literal l2 = th.mk_literal(a.mk_ge(sz2, a.mk_int(1)));
+                ctx.mk_th_axiom(th.get_id(), l_eq, l1, l2);
+            }
+        }
+    }
+
+    /**
+    * Walk the cone of influence of expresions that depend on ns
+    */
+    void theory_finite_set_size::collect_subexpressions(enode_vector& ns) {
+
+        // initialize disequality watch list
+        u_map<unsigned_vector> v2diseqs, v2eqs;
+        for (auto [a, b] : th.m_diseqs) {
+            v2diseqs.insert_if_not_there(a, unsigned_vector()).push_back(b);
+            v2diseqs.insert_if_not_there(b, unsigned_vector()).push_back(a);
+        }
+        for (auto [a, b] : th.m_eqs) {
+            v2eqs.insert_if_not_there(a, unsigned_vector()).push_back(b);
+            v2eqs.insert_if_not_there(b, unsigned_vector()).push_back(a);
+        }
+
+        auto add_expression = [&](enode *e) {
+            if (!ctx.is_relevant(e))
+                return;
+            if (e->is_marked())
+                return;
+            e->set_mark();
+            ns.push_back(e);
+        };
+
+        auto is_setop = [&](enode *n) {
+            auto e = n->get_expr();
+            return u.is_union(e) || u.is_intersect(e) || u.is_difference(e);
+        };
+
+        for (auto f : m_set_size_decls) {
+            for (auto n : ctx.enodes_of(f)) {
+                SASSERT(u.is_size(n->get_expr()));
+                add_expression(n->get_arg(0));
+            }
+        }
+        for (unsigned i = 0; i < ns.size(); ++i) {
+            auto n = ns[i];
+            // add children under set operations
+            if (is_setop(n))
+                for (auto arg : enode::args(n))
+                    add_expression(arg);
+            // add parents that are operations and use n
+            for (auto p : enode::parents(n))
+                if (is_setop(p) && any_of(enode::args(p), [n](auto a){
+                    return a == n;}))
+                    add_expression(p);
+            // add equalities and disequalities
+            auto v = th.get_th_var(n);
+            if (v2eqs.contains(v)) {
+                auto const &other = v2eqs[v];
+                for (auto w : other) 
+                    add_expression(th.get_enode(w));                
+            }
+            if (v2diseqs.contains(v)) {
+                auto const &other = v2diseqs[v];
+                for (auto w : other) {
+                    auto n2 = th.get_enode(w);
+                    add_expression(n2);
+                    add_expression(mk_diff(n, n2));
+                    add_expression(mk_diff(n2, n));
+                }
+            }
+        }
+        for (auto n : ns)
+            n->unset_mark();
+    }
+
+    void theory_finite_set_size::create_singleton_sets_from_membership(enode_vector& ns) {
+        unsigned sz = ns.size();
+        enode_vector to_unmark;
+        for (unsigned i = 0; i < sz; ++i) {
+            auto n = ns[i];
+            for (auto p : enode::parents(n)) {
+                if (!u.is_in(p->get_expr()))
+                    continue;
+                auto e = p->get_arg(0)->get_root();
+                if (e->is_marked())
+                    continue;
+                e->set_mark();
+                to_unmark.push_back(e);
+                ns.push_back(mk_singleton(e));
+            }
+        }
+        for (auto n : to_unmark)
+            n->unset_mark();
+    }
+
+    /**
+    * Base implementation:
+    *    Enumerate all satisfying assignments to m_solver for atoms based on |s|
+    *    Extract Core from enumeration
+    *    Assert Core => |s_i| = sum_ij n_ij for each |s_i| cardinality expression
+    *    NB. Soundness of using Core has not been rigorously established.    
+    * Incremental algorithm:
+    *    Enumerate N assignments at a time. 
+    *    Associate tracking literal C_i with current assignment.
+    *    Assume C_i
+    *    Assert !C_0, .. , !C_{i-1}, C_i => /\_i |s_i| = sum_j n_ij and /\ n_j >= 0
+    * Incremental algorithm with blocking clauses (sketch)
+    *    If /\_i |s_i| = sum_j n_ij and /\ n_j >= 0 is unsat
+    *    Then, instead of asserting sum constraint assert
+    *    C_i <=> \/_j core_j
+    *    where core_j come from covering of LRA conflict 
+    */
+    lbool theory_finite_set_size::run_solver() {
+        expr_ref_vector asms(m);
+        for (auto [k, v] : m_assumptions)
+            asms.push_back(k);
+
+        expr_ref_vector slack_exprs(m);
+        obj_map<expr, expr *> slack_sums;
+        arith_util a(m);
+        for (auto f : m_set_size_decls) {
+            for (auto n : ctx.enodes_of(f)) {
+                slack_sums.insert(n->get_expr(), a.mk_int(0));
+            }
+        }
+
+        while (true) {
+            lbool r = m_solver->check(asms.size(), asms.data());
+            if (r == l_false) {
+                auto const& core = m_solver->unsat_core();
+                literal_vector lits;
+                for (auto c : core) {
+                    auto exp = m_assumptions[c];
+                    if (std::holds_alternative<eq>(exp)) {
+                        auto [a, b] = *std::get_if<eq>(&exp);
+                        lits.push_back(~th.mk_literal(m.mk_eq(th.get_expr(a), th.get_expr(b))));
+                    }
+                    else if (std::holds_alternative<diseq>(exp)) {
+                        auto [a, b] = *std::get_if<diseq>(&exp);
+                        lits.push_back(th.mk_literal(m.mk_eq(th.get_expr(a), th.get_expr(b))));
+                    }
+                    else if (std::holds_alternative<in>(exp)) {
+                        auto [n, is_pos] = *std::get_if<in>(&exp);
+                        auto lit = th.mk_literal(n->get_expr());
+                        lits.push_back(is_pos ? ~lit : lit);
+                    }
+                }
+                for (auto f : m_set_size_decls) {
+                    for (auto n : ctx.enodes_of(f)) {
+                        expr_ref eq(m.mk_eq(n->get_expr(), slack_sums[n->get_expr()]), m);
+                        auto lit = th.mk_literal(eq);
+                        literal_vector lemma(lits);
+                        lemma.push_back(lit);
+                        ctx.mk_th_axiom(th.get_id(), lemma);
+                    }
+                }
+                ctx.push_trail(value_trail(m_solver_ran));
+                TRACE(finite_set, ctx.display(tout));
+                m_solver_ran = true;
+                return l_false;
+            }
+            if (r != l_true)
+                return r;
+
+            expr_ref slack(m.mk_fresh_const(symbol("slack"), a.mk_int()), m);
+            ctx.mk_th_axiom(th.get_id(), th.mk_literal(a.mk_ge(slack, a.mk_int(0))));  // slack is non-negative
+            model_ref mdl;
+            m_solver->get_model(mdl);
+            TRACE(finite_set, tout << *mdl);
+            expr_ref_vector props(m);
+            for (auto f : m_set_size_decls) {
+                for (auto n : ctx.enodes_of(f)) {
+                    auto arg = n->get_arg(0);
+                    auto b = n2b[arg];
+                    auto b_is_true = mdl->is_true(b);
+                    props.push_back(b_is_true ? b : m.mk_not(b));
+                    if (b_is_true) {
+                        auto s = slack_sums[n->get_expr()];
+                        s = a.mk_add(s, slack);
+                        slack_exprs.push_back(s);
+                        slack_sums.insert(n->get_expr(), s);
+                    }
+                }
+            }
+            m_solver->assert_expr(m.mk_not(m.mk_and(props)));           
+        }
+        return l_undef;
+    }
+
+    lbool theory_finite_set_size::final_check() {
+        if (m_set_size_decls.empty())
+            return l_true;
+        if (!m_solver) {
+            initialize_solver();
+            return l_false;
+        }
+        if (!m_solver_ran)
+            return run_solver();
+
+        // at this point we assume that 
+        // cardinality constraints are satisfied 
+        // by arithmetic solver.
+        // 
+        // a refinement checks if this is really necessary
+        //
+        return l_true;
+    }
+
+    /**
+    * Introduce an assumption literal to manage incremental search for solutions
+    */
+    void theory_finite_set_size::add_theory_assumptions(expr_ref_vector &assumptions) {
+        if (m_set_size_decls.empty())
+            return;
+        m_assumption = m.mk_fresh_const(symbol("set.size.solver"), m.mk_bool_sort());
+        assumptions.push_back(m_assumption);
+    }
+
+    bool theory_finite_set_size::should_research(expr_ref_vector& unsat_core) {
+        return unsat_core.contains(m_assumption);
+    }
+
+    std::ostream& theory_finite_set_size::display(std::ostream& out) {
+        if (m_solver)
+            m_solver->display(out);
+        return out;
+    }
+}  // namespace smt

src/smt/theory_finite_set_size.h

@@ -0,0 +1,73 @@
+
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    theory_finite_set_size.h
+
+Abstract:
+
+    sub-solver for cardinality constraints of finite sets
+
+--*/
+
+#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 "util/union_find.h"
+#include "smt/smt_theory.h"
+#include "model/finite_set_factory.h"
+
+namespace smt {
+    class context;
+    class theory_finite_set;
+
+    class theory_finite_set_size {
+        struct diseq {
+            theory_var x, y;
+        };
+        struct eq {
+            theory_var x, y;
+        };
+        struct in {
+            enode *n;
+            bool is_pos;
+        };
+        using tracking_literal = std::variant<diseq, eq, in>;
+        ast_manager          &m;
+        context             &ctx;
+        theory_finite_set   &th;
+        finite_set_util u;
+        scoped_ptr<context> m_solver;
+        bool m_solver_ran = false;
+        ptr_vector<func_decl> m_set_size_decls;
+        obj_map<enode, expr *> n2b;
+        obj_map<expr, tracking_literal> m_assumptions;
+        expr_ref m_assumption;
+
+        void collect_subexpressions(enode_vector& ns);
+        void create_singleton_sets_from_membership(enode_vector& ns);
+        void add_def_axioms(enode_vector const &ns);
+        void add_singleton_axioms(enode_vector const &ns);
+        void add_eq_axioms(enode_vector const &ns);
+        void add_diseq_axioms(enode_vector const &ns);
+        enode *mk_singleton(enode* n);
+        enode *mk_diff(enode *a, enode *b);
+        void initialize_solver();
+
+        lbool run_solver();
+
+    public:
+        theory_finite_set_size(theory_finite_set &th);
+        void add_set_size(func_decl *f);
+        void add_theory_assumptions(expr_ref_vector &assumptions); 
+        bool should_research(expr_ref_vector &unsat_core);
+        lbool final_check(); 
+        std::ostream &display(std::ostream &out);
+    };
+}