1–LABEL:LastPageFeb. 22, 2017Nov. 01, 2018 final

This article extends [BRBT16] with additional calculus rules and a full proof
of correctness.

# Reasoning with finite sets and
cardinality constraints in SMT

Kshitij Bansala  aGoogle, Inc<EMAIL_ADDRESS>,  Clark Barrettb  bDepartment
of Computer Science, Stanford University<EMAIL_ADDRESS>,  Andrew
Reynoldsc  cDepartment of Computer Science, The University of Iowa  andrew-
<EMAIL_ADDRESS>and  Cesare Tinellic<EMAIL_ADDRESS>
###### Abstract.

We consider the problem of deciding the satisfiability of quantifier-free
formulas in the theory of finite sets with cardinality constraints. Sets are a
common high-level data structure used in programming; thus, such a theory is
useful for modeling program constructs directly. More importantly, sets are a
basic construct of mathematics and thus natural to use when formalizing the
properties of computational systems. We develop a calculus describing a
modular combination of a procedure for reasoning about membership constraints
with a procedure for reasoning about cardinality constraints. Cardinality
reasoning involves tracking how different sets overlap. For efficiency, we
avoid considering Venn regions directly, as done in previous work. Instead, we
develop a novel technique wherein potentially overlapping regions are
considered incrementally as needed, using a graph to track the interaction
among the different regions. The calculus has been designed to facilitate its
implementation within SMT solvers based on the DPLL($T$) architecture. Our
experimental results demonstrate that the new techniques are competitive with
previous techniques and can scale much better on certain classes of problems.

###### Key words and phrases:

Satisfiability modulo theories, Finite sets, Decision procedures

###### 1991 Mathematics Subject Classification:

Theory of computation: Automated reasoning

This work was partially supported by NSF grants 1228765, 1228768, and 1320583.
The first author was at New York University when this work was completed.

##  1\. Introduction

Satisfiability modulo theories (SMT) solvers are at the heart of many formal
methods tools. One of the reasons for their popularity is that fast, dedicated
decision procedures for fragments of first-order logic that SMT solvers
implement are extremely useful for reasoning about constructs common in
hardware and software verification. In particular, they provide a good balance
between speed and expressiveness. Common fragments include theories such as
bitvectors, arithmetic, and arrays, which are useful for modeling basic
constructs as well as for performing general reasoning.

As the use of SMT solvers has spread, there has been a corresponding demand
for SMT solvers to support additional useful theories. Although it is possible
to encode finitely axiomatizable theories using quantifiers, the performance
and robustness gap between a custom decision procedure and an encoding using
quantifiers can be quite significant.

In this paper, we present a new decision procedure for a fragment of finite
set theory. Our main motivation is that sets are a common abstraction used in
programming. As with other general-purpose SMT theories such as the theories
of arrays and bitvectors, the theory of finite sets is useful for modeling a
variety of program constructs. Sets are also used directly in high-level
programming languages such as SETL [SDSD86] and in specification languages
such as Alloy [Jac12], B [AA05] and Z [ASM80]. More generally, sets are a
basic construct in mathematics and come up quite naturally when trying to
express properties of systems.

While the full language of set theory is undecidable, many interesting
fragments are known to be decidable. We present a calculus for the theory of
finite sets which can handle basic set operations, such as membership, union,
intersection, and difference, and which can also reason efficiently about set
cardinalities and linear constraints involving them. The calculus is
explicitly designed for easy integration into the DPLL($T$) framework [NOT06].
We briefly describe our implementation in the DPLL($T$)-based SMT solver cvc4
and an initial experimental evaluation of this implementation.

###  1.1. Related work

In the SMT community, the desire to support a theory of finite sets with
cardinality goes at least as far back as a proposal by Kröning et al. [KRW09].
That article focuses on formalizing the semantics and representation of the
theory within the context of the SMT-LIB standard, rather than on a decision
procedure for deciding it.

There is a stream of research on exploring decidable fragments of set theory
(often referred to in the literature as syllogistics) [COP01]. One such
subfragment is MLSS, more precisely, the ground set-theoretic fragment with
basic Boolean set operators (union, intersection, set difference), singleton
operator and membership predicate. A tableau-based procedure for this fragment
was introduced by Cantone and Zarba [CZ98]. The part of our calculus covering
this fragment builds on their work. De Moura and Bjørner presented an
extension of the theory of arrays [DMB09] that can be used to encode the MLSS
fragment. However, this approach cannot be used to encode cardinality
constraints.

In this paper, we consider an extension of the MLSS fragment with set
cardinality operations, whose decidability was established by Zarba [Zar02,
Zar05]. The decision procedure described by Zarba involves making an upfront
guess that is exponential in the number of set variables, making it non-
incremental and highly impractical. That said, the focus of that work is on
establishing decidability and not on providing an efficient procedure.

Another closely related logical fragment is the Boolean Algebra and Presburger
Arithmetic (BAPA) fragment, for which several algorithms have been proposed
[KNR06, KR07, SSK11]. Though BAPA does not have the membership predicate or
the singleton operator in its language, Suter et al. [SSK11, Section 4] show
how one can generalize their algorithm for such reasoning. Intuitively,
singleton sets can be simulated by imposing a cardinality constraint
$\mathsf{card}(X)=1$. Similarly, membership constraints of the form
$x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}S$ can be encoded as $X\sqsubseteq S$
by introducing a singleton subset $X$. This reduction can lead to significant
inefficiencies, however. Consider the following simple example:
$x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}S_{1}\sqcup\left(S_{2}\sqcup\left(\ldots\sqcup\left(S_{99}\sqcup
S_{100}\right)\right)\right)$. In our calculus, a straightforward repeated
application of one of the rules for set unions can determine the
satisfiability of this constraint. In contrast, in a reduction to BAPA,
membership reasoning is reduced to reasoning about cardinalities of different
sets. For example, the algorithm in [SSK11] will reduce the problem to an
arithmetic problem involving variables for $2^{101}$ Venn regions derived from
$S_{1}$, $S_{2}$, $\ldots$, $S_{100}$, and the singleton set introduced for
$x$.

The broader point is that reasoning about the cardinalities of Venn regions is
the main bottleneck for this fragment. As we show in our calculus, it is
possible to avoid using Venn regions for membership predicates by instead
reasoning about them directly. For explicit cardinality constraints, our
calculus minimizes the number of Venn regions that need to be considered by
reasoning about only a limited number of relevant regions introduced lazily.

A procedure for cardinality constraints over multisets is considered in
[PK08]. A recent procedure for reasoning about sets and measure functions is
given by Bender et al [BS17], which also relies on a reduction from set
reasoning to arithmetic reasoning. Reasoning about sets with cardinality
constraints in the context of invariant checking for bounded model checking is
considered by Alberti et al. [AGP16], and in the context of invariant
synthesis by von Gleissenthall et el. [vGBR16]. These works too rely on
reductions to arithmetic and do not involve the use of dedicated decision
procedures for sets in SMT solvers. Other procedures for reasoning about sets
include a unification-based approach by Cristiá et al. [CR16].

The theory we consider in this paper can be seen as the combination of
Presburger arithmetic with the theory of finite sets, with the cardinality
operator acting as a _bridging function_ between the two theories. Decision
procedures for non-disjoint combinations of theories with bridging functions
have been studied by Sofronie-Stokkermans [SS09] and Chocron et al. [CFR15].
Their main contribution is the identification of restrictions on the theories
and the development of combination methods that allow one to construct a
decision procedure for the combined theory as a modular combination of the
decision procedures for the component theories. That work is mostly limited to
cases of bridging functions from the theory of algebraic datatypes to other
theories, where the bridging function is definable by recursion over
constructor terms. It does not apply to our setting because neither our source
theory nor the bridging function match those requirements. Our approach is
similar though in that it tries to separate as much as possible the reasoning
about sets proper from the reasoning about their cardinality, so as to
leverage off-the-shelf linear integer arithmetic solvers in order to reason
about cardinalities.

###  1.2. Formal Preliminaries

We work in the context of many-sorted first-order logic with equality. We
assume the reader is familiar with the following notions: signature, term,
literal, formula, free variable, interpretation, and satisfiability of a
formula in an interpretation (see, e.g., [BSST09] for more details). Let
$\Sigma$ be a many-sorted signature. We use $\approx$ as the (infix) logical
symbol for equality for all sorts in $\Sigma$ and always interpret it as the
identity relation. If $e$ is a term or a formula, we denote by
$\mathcal{V}(e)$ the set of $e$’s free variables, extending the notation to
tuples and sets of terms or formulas as expected.

If $\varphi$ is a $\Sigma$-formula and $\mathcal{I}$ a
$\Sigma$-interpretation, we write $\mathcal{I}\models\varphi$ if $\mathcal{I}$
satisfies $\varphi$. If $t$ is a term, we denote by $t^{\mathcal{I}}$ the
value of $t$ in $\mathcal{I}$. A theory is a pair $T=(\Sigma,\mathbf{I})$,
where $\Sigma$ is a signature and $\mathbf{I}$ is a class of
$\Sigma$-interpretations that is closed under variable reassignment (i.e.,
every $\Sigma$-interpretation that differs from one in $\mathbf{I}$ only in
how it interprets the variables is also in $\mathbf{I}$). We refer to
$\mathbf{I}$ as the models of $T$. A $\Sigma$-formula $\varphi$ is satisfiable
(resp., unsatisfiable) in $T$ if it is satisfied by some (resp., no)
interpretation in $\mathbf{I}$. A set $\Gamma$ of $\Sigma$-formulas entails in
$T$ a $\Sigma$-formula $\varphi$, written $\Gamma\models_{T}\varphi$, if every
interpretation in $\mathbf{I}$ that satisfies all formulas in $\Gamma$
satisfies $\varphi$ as well. We write $\models_{T}\varphi$ as an abbreviation
for $\emptyset\models_{T}\varphi$. We write $\Gamma\models\varphi$ to denote
that $\Gamma$ entails $\varphi$ in the class of all $\Sigma$-interpretations.
The set $\Gamma$ is satisfiable in $T$ if $\Gamma\not\models_{T}\bot$ where
$\bot$ is the universally false atom. Two $\Sigma$-formulas are
equisatisfiable in $T$ if for every model $\mathcal{I}$ of $T$ that satisfies
one, there is a model of $T$ that satisfies the other and differs from
$\mathcal{I}$ at most over the free variables not shared by the two formulas.
When convenient, we will tacitly treat a finite set of formulas as the
conjunction of its elements and vice versa.

##  2\. A Theory of Finite Sets with Cardinality

We are interested in a typed theory ${\mathfrak{T}_{S}}$ of finite sets with
cardinality. In a more general logical setting, this theory would be equipped
with a parametric set type, with a type parameter for the set’s elements, and
a corresponding collection of polymorphic set operations.111In fact, this is
the setting supported in our implementation in cvc4. For simplicity here, we
will describe instead a many-sorted theory of sets of sort $\mathsf{Set}$
whose elements are all of sort $\mathsf{Element}$. The theory
${\mathfrak{T}_{S}}$ can be combined with any other theory $\mathfrak{T}$ in a
standard way, i.e., Nelson-Oppen-style, by identifying the $\mathsf{Element}$
sort with a sort in $\mathfrak{T}$ but with the restriction that the sort must
be interpreted in $\mathfrak{T}$ as an infinite set.222An extension that
allows the sort to be interpreted as finite by relying on polite combination
[JB10] is left to future work. Note that the many-sorted setting limits us to
sets of elements of the same type (so sets such as
$\\{1,\,\\{2,3\\},\,\\{\\{5\\}\\}\\}$ are not representable). Also, we limit
our language to consider only _flat_ sets (i.e., no sets of sets of integers,
say) although this restriction can be lifted by combining $\mathfrak{T}$ with
(copies of) itself using Nelson-Oppen combination. More generally, an input
having set constraints over multiple element types $T_{1},\ldots,T_{n}$ can be
handled by invoking $n$ copies of our procedure for these sorts and combining
them in the standard way. The theory ${\mathfrak{T}_{S}}$ has also a sort
$\mathsf{Card}$ for terms denoting set cardinalities. Since we consider only
finite sets, all cardinalities will be natural numbers.

Atomic formulas in ${\mathfrak{T}_{S}}$ are built over a signature with these
three sorts, and an infinite set of variables for each sort. Modulo
isomorphism, ${\mathfrak{T}_{S}}$ is the theory of a single many-sorted
structure, and its models differ in essence only on how they interpret the
variables. Each model of ${\mathfrak{T}_{S}}$ interprets $\mathsf{Element}$ as
some _countably infinite_ set $E$, $\mathsf{Set}$ as the set of _finite_
subsets of $E$, and $\mathsf{Card}$ as $\mathbb{N}$. The signature of
${\mathfrak{T}_{S}}$ has the following predicate and function symbols,
summarized in Figure LABEL:fig:symbols: the usual symbols of _linear_ integer
arithmetic, the usual set composition operators, an empty set ($\emptyset$)
and a singleton set ($\left\\{\cdot\right\\}$) constructor,333We will use
$\emptyset$, $\\{$, and $\\}$ also to denote sets at the meta level. The
difference between their two uses should be clear from context.  and a
cardinality operator ($\mathsf{card}(\cdot)$), all interpreted as expected.
The signature includes also symbols for the cardinality comparison
($\operatorname{\texttt{<}\,},\operatorname{\texttt{>=}\,}$), subset
($\sqsubseteq$) and membership ($\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}$)
predicates.

We call set term any term of sort $\mathsf{Set}$, and cardinality term any
term of sort $\mathsf{Card}$ with no occurrences of $\mathsf{card}(\cdot)$. A
set constraint is an atomic formula of the form $s\approx t$, $s\sqsubseteq
t$, $e\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s$ or their negation, with $s$
and $t$ set terms or of the form $\mathsf{card}(s)$, and $e$ a term of sort
$\mathsf{Element}$. A cardinality constraint is a [dis]equality
$[\lnot]c\approx d$ or an inequality $c\operatorname{\texttt{<}\,}d$ or
$c\operatorname{\texttt{>=}\,}d$ where $c$ and $d$ are cardinality terms. An
element constraint is a [dis]equality $[\lnot]x\approx y$ where $x$ and $y$
are variables of sort $\mathsf{Element}$. A ${\mathfrak{T}_{S}}$-constraint is
a set, cardinality or element constraint. We write $u\not\approx v$ and
$e\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t$ respectively as an
abbreviation of $\lnot u\approx v$ and $\lnot
e\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t$.

We use $x$, $y$ for variables of sort $\mathsf{Element}$; $S$, $T$, $U$ for
variables of sort $\mathsf{Set}$; $s$, $t$, $u$, $v$ for terms of sort
$\mathsf{Set}$; and $c$ with subscripts for variables of sort $\mathsf{Card}$.
Given $\mathcal{C}$, a set of constraints,
$\operatorname{Vars}{(}\mathcal{C})$ (respectively,
$\operatorname{Terms}(\mathcal{C})$) denotes the set of variables
(respectively, terms) in $\mathcal{C}$. For notational convenience, we fix an
injective mapping from terms of sort $\mathsf{Set}$ to variables of sort
$\mathsf{Card}$ that allows us to associate to each set term $s$ a unique
cardinality variable $c_{s}$.

We are interested in checking the satisfiability in ${\mathfrak{T}_{S}}$ of
conjunctions of ${\mathfrak{T}_{S}}$-constraints. While this problem is
decidable, it has high worst-case time complexity [Zar02]. So our efforts are
in the direction of producing a solver for ${\mathfrak{T}_{S}}$-constraints
that is efficient in practice, in addition to being correct and terminating.
Our solver relies on the modular combination of a solver for set constraints
and an off-the-shelf solver for linear integer arithmetic, which handles
arithmetic reasoning over set cardinalities.

##  3\. A Calculus for the Theory

In this section, we describe a tableaux-style calculus capturing the essence
of our combined solver for ${\mathfrak{T}_{S}}$. As we describe in the next
section, that calculus admits a proof procedure that decides the
satisfiability of ${\mathfrak{T}_{S}}$-constraints.

######  Restriction .

For simplicity, we consider as input to the calculus only finite sets
$\mathcal{C}$ of constraints whose set constraints are in flat form. The
latter are (well-sorted) set constraints of the form $S\approx T$,
$S\not\approx T$, $S\approx\emptyset$, $S\approx\left\\{x\right\\}$, $S\approx
T\sqcup U$, $S\approx T\sqcap U$, $S\approx T\setminus U$,
$x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}S$,
$x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}S$, or
$c_{S}\approx\mathsf{card}(S)$, where $S$, $T$, $U$, $c_{S}$, and $x$ are
variables of the expected sort. We also assume that any set variable $S$ of
$\mathcal{C}$ appears in at most one union, intersection or set difference
term. Thanks to common equisatisfiability-preserving transformations all of
these assumptions can be made without loss of generality [COP01, Chapter 10].
These transformations include intermediate steps that replace constraints of
the form $s\sqsubseteq t$ with $s\approx(s\sqcap t)$. They also include steps
that replace each occurrence $i$ of the same term $t$ in union, intersection
or set difference terms by a fresh variable $T_{i}$ while adding the equality
constraint $T_{i}\approx t$.

The calculus is described as a set of derivation rules which modify a state
data structure. A state is either the special state $\mathsf{unsat}$ or a
tuple of the form
$\langle\mathcal{S},\mathcal{M},\mathcal{A},\mathcal{G}\rangle$, where

  * •

$\mathcal{S}$ is a set of set constraints,

  * •

$\mathcal{M}$ is a set of element constraints,

  * •

$\mathcal{A}$ is a set of cardinality constraints, and

  * •

$\mathcal{G}$ is a directed graph over set terms with nodes $V(\mathcal{G})$
and edges $E(\mathcal{G})$.

Initial states have the form
$\langle\mathcal{S}_{0},\mathcal{M}_{0},\mathcal{A}_{0},\mathcal{G}_{0}\rangle$
where $\mathcal{G}_{0}$ is the empty graph and
$(\mathcal{S}_{0},\mathcal{M}_{0},\mathcal{A}_{0})$ is a partition of a given
set of constraints $\mathcal{C}$ satisfying Restriction 3.

Since cardinality constraints can be processed by a standard arithmetic
solver, and element constraints by a simple equality solver,444 Recall that
${\mathfrak{T}_{S}}$ has no terms of sort $\mathsf{Element}$ besides
variables.  we present and discuss only rules that deal with set constraints.

The derivation rules are provided in Figures 2 through 9 in guarded assignment
form. In such form, the premises of a rule refer to the current state and the
conclusion describes how each state component is changed, if at all, by the
rule’s application. A derivation rule applies to a state $\sigma$ if all the
conditions in the rule’s premises hold for $\sigma$ _and_ the resulting state
is different from $\sigma$. In the rules, we write $S,t$ as an abbreviation
for $S\cup\\{t\\}$. Rules with two or more conclusions separated by the symbol
$\parallel$ are non-deterministic branching rules.

The rules are such that it is possible to generate a closed tableau (or
derivation tree) from an initial state
$\langle\mathcal{S}_{0},\mathcal{M}_{0},\mathcal{A}_{0},\mathcal{G}_{0}\rangle$,
where $\mathcal{S}_{0}$, $\mathcal{M}_{0}$, and $\mathcal{A}_{0}$ satisfy
Restriction 3 and $\mathcal{G}_{0}$ is an empty graph, if and only if
$\mathcal{S}_{0}\cup\mathcal{M}_{0}\cup\mathcal{A}_{0}$ is unsatisfiable in
${\mathfrak{T}_{S}}$. Broadly speaking, the derivation rules can be divided
into three categories. First are those that reason about membership
constraints (of form $x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}S$). These rules
only update the components $\mathcal{S}$ and $\mathcal{M}$ of the current
state, although their premises may depend on other parts of the state, in
particular, the nodes of the graph $\mathcal{G}$. Second are rules that handle
constraints of the form $c_{S}\approx\mathsf{card}(S)$. The graph
incrementally built by the calculus is central to satisfying these
constraints. Third are rules for propagating element and cardinality
constraints, respectively to $\mathcal{M}$ and $\mathcal{A}$.

Union Down I $\displaystyle\displaystyle{\hbox{\hskip
36.4902pt\vbox{\hbox{\hskip-36.49019pt\hbox{\hbox{$\displaystyle\displaystyle{x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\sqcup
t\in\mathcal{S}^{*}}$}}}\vbox{}}}\over\hbox{\hskip
66.86453pt\vbox{\vbox{}\hbox{\hskip-66.86452pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s)\triangleleft(x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t)}$}}}}}}$
Union Down II $\displaystyle\displaystyle{\hbox{\hskip
110.33585pt\vbox{\hbox{\hskip-110.33583pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\sqcup
t\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\\{u,v\\}=\\{s,t\\}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}u\in\mathcal{S}^{*}}$}}}}}\vbox{}}}\over\hbox{\hskip
35.07176pt\vbox{\vbox{}\hbox{\hskip-35.07175pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}v)}$}}}}}}$
---
Union Up I $\displaystyle\displaystyle{\hbox{\hskip
95.75822pt\vbox{\hbox{\hskip-95.75822pt\hbox{\hbox{$\displaystyle\displaystyle{x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{s\sqcup
t\in\mathcal{T}}$}}}}}\vbox{}}}\over\hbox{\hskip
45.92357pt\vbox{\vbox{}\hbox{\hskip-45.92357pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\sqcup
t)}$}}}}}}$ Union Up II $\displaystyle\displaystyle{\hbox{\hskip
82.89185pt\vbox{\hbox{\hskip-82.89185pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}u\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{u\in\\{s,t\\}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{s\sqcup
t\in\mathcal{T}}$}}}}}\vbox{}}}\over\hbox{\hskip
42.17357pt\vbox{\vbox{}\hbox{\hskip-42.17357pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\sqcup
t)}$}}}}}}$
Inter Down I $\displaystyle\displaystyle{\hbox{\hskip
32.7402pt\vbox{\hbox{\hskip-32.74019pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\sqcap
t\in\mathcal{S}^{*}}$}}}\vbox{}}}\over\hbox{\hskip
59.36453pt\vbox{\vbox{}\hbox{\hskip-59.36452pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s)\triangleleft(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t)}$}}}}}}$
Inter Down II $\displaystyle\displaystyle{\hbox{\hskip
110.33585pt\vbox{\hbox{\hskip-110.33583pt\hbox{\hbox{$\displaystyle\displaystyle{x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\sqcap
t\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\\{u,v\\}=\\{s,t\\}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}u\in\mathcal{S}^{*}}$}}}}}\vbox{}}}\over\hbox{\hskip
38.82176pt\vbox{\vbox{}\hbox{\hskip-38.82175pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}v)}$}}}}}}$
Inter Up I $\displaystyle\displaystyle{\hbox{\hskip
88.25822pt\vbox{\hbox{\hskip-88.25822pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{s\sqcap
t\in\mathcal{T}}$}}}}}\vbox{}}}\over\hbox{\hskip
42.17357pt\vbox{\vbox{}\hbox{\hskip-42.17357pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\sqcap
t)}$}}}}}}$ Inter Up II $\displaystyle\displaystyle{\hbox{\hskip
86.64185pt\vbox{\hbox{\hskip-86.64185pt\hbox{\hbox{$\displaystyle\displaystyle{x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}u\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{u\in\\{s,t\\}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{s\sqcap
t\in\mathcal{T}}$}}}}}\vbox{}}}\over\hbox{\hskip
45.92357pt\vbox{\vbox{}\hbox{\hskip-45.92357pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\sqcap
t)}$}}}}}}$
Union split $\displaystyle\displaystyle{\hbox{\hskip
90.0325pt\vbox{\hbox{\hskip-90.03249pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\sqcup
t\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s,x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t\not\in\mathcal{S}^{*}}$}}}}\vbox{}}}\over\hbox{\hskip
78.80899pt\vbox{\vbox{}\hbox{\hskip-78.80898pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s)\
\parallel\
\mathcal{S}:=\mathcal{S}\triangleleft(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t)}$}}}}}}$
Inter split $\displaystyle\displaystyle{\hbox{\hskip
153.98277pt\vbox{\hbox{\hskip-153.98277pt\hbox{\hbox{$\displaystyle\displaystyle{s\sqcap
t\in\mathcal{T}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\\{u,v\\}=\\{s,t\\}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}u\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}v,x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}v\not\in\mathcal{S}^{*}}$}}}}}}\vbox{}}}\over\hbox{\hskip
83.61569pt\vbox{\vbox{}\hbox{\hskip-83.61568pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}v)\
\parallel\
\mathcal{S}:=\mathcal{S}\triangleleft(x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}v)}$}}}}}}$
Set difference Down 1 $\displaystyle\displaystyle{\hbox{\hskip
33.29576pt\vbox{\hbox{\hskip-33.29575pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\setminus
t\in\mathcal{S}^{*}}$}}}\vbox{}}}\over\hbox{\hskip
63.11453pt\vbox{\vbox{}\hbox{\hskip-63.11452pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s)\triangleleft(x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t)}$}}}}}}$
Set difference Down 2 $\displaystyle\displaystyle{\hbox{\hskip
72.4249pt\vbox{\hbox{\hskip-72.4249pt\hbox{\hbox{$\displaystyle\displaystyle{x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\setminus
t\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\in\mathcal{S}^{*}}$}}}}\vbox{}}}\over\hbox{\hskip
34.2743pt\vbox{\vbox{}\hbox{\hskip-34.2743pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t)}$}}}}}}$
Set difference Down 3 $\displaystyle\displaystyle{\hbox{\hskip
75.6367pt\vbox{\hbox{\hskip-75.6367pt\hbox{\hbox{$\displaystyle\displaystyle{x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\setminus
t\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t\in\mathcal{S}^{*}}$}}}}\vbox{}}}\over\hbox{\hskip
38.5625pt\vbox{\vbox{}\hbox{\hskip-38.5625pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s)}$}}}}}}$
Set difference Up 1 $\displaystyle\displaystyle{\hbox{\hskip
92.56378pt\vbox{\hbox{\hskip-92.56378pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{s\setminus
t\in\mathcal{T}}$}}}}}\vbox{}}}\over\hbox{\hskip
42.72913pt\vbox{\vbox{}\hbox{\hskip-42.72913pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\setminus
t)}$}}}}}}$
Set difference Up 2 $\displaystyle\displaystyle{\hbox{\hskip
57.72284pt\vbox{\hbox{\hskip-57.72282pt\hbox{\hbox{$\displaystyle\displaystyle{x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{s\setminus
t\in\mathcal{T}}$}}}}\vbox{}}}\over\hbox{\hskip
46.47913pt\vbox{\vbox{}\hbox{\hskip-46.47913pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\setminus
t)}$}}}}}}$ Set difference Up 3 $\displaystyle\displaystyle{\hbox{\hskip
53.43465pt\vbox{\hbox{\hskip-53.43463pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{s\setminus
t\in\mathcal{T}}$}}}}\vbox{}}}\over\hbox{\hskip
46.47913pt\vbox{\vbox{}\hbox{\hskip-46.47913pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\setminus
t)}$}}}}}}$
Set difference split $\displaystyle\displaystyle{\hbox{\hskip
134.90474pt\vbox{\hbox{\hskip-134.90472pt\hbox{\hbox{$\displaystyle\displaystyle{s\setminus
t\in\mathcal{T}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t\not\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t\not\in\mathcal{S}^{*}}$}}}}}}\vbox{}}}\over\hbox{\hskip
82.0208pt\vbox{\vbox{}\hbox{\hskip-82.02078pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t)\
\parallel\
\mathcal{S}:=\mathcal{S}\triangleleft(x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t)}$}}}}}}$
Figure 2. Union, intersection, and set difference rules.

###  3.1. Set reasoning rules

Figures 2 and 3 focus on sets without cardinality. They are based on the MLSS
decision procedure by Cantone and Zarba [CZ98], though with some key
differences. First, the rules operate over a set $\mathcal{T}$ of terms with
sort $\mathsf{Set}$ which may be larger than just the terms in $\mathcal{S}$.
This generalization is required because of additional terms that may be
introduced when reasoning about cardinalities. Second, the reasoning is done
modulo equality. A final, technical difference is that we work with sets of
ur-elements rather than untyped sets.

These rules rely on the following additional notation. For any set
$\mathcal{C}$ of constraints, let $\operatorname{Terms}_{\sigma}(\mathcal{C})$
refer to terms of sort $\sigma$ in $\mathcal{C}$, with
$\operatorname{Terms}(\mathcal{C})$ denoting all terms in $\mathcal{C}$. We
define the binary relation $\approx_{\mathcal{C}}^{*}\
\subseteq\operatorname{Terms}(\mathcal{C})\times\operatorname{Terms}(\mathcal{C})$
to be the reflexive, symmetric, and transitive closure of the relation on
terms induced by the equality constraints in $\mathcal{C}$. Now, we define the
following closures on the components $\mathcal{M}$ and $\mathcal{S}$ of a
state $\langle\mathcal{S},\mathcal{M},\mathcal{A},\mathcal{G}\rangle$:

$\displaystyle\mathcal{M}^{*}=$ $\displaystyle\left\\{x\approx y\ \middle|\
x\approx_{\mathcal{M}}^{*}y\right\\}\cup\left\\{x\not\approx y\ \middle|\
\exists
x^{\prime},y^{\prime}.~{}x\approx_{\mathcal{M}}^{*}x^{\prime},~{}y\approx_{\mathcal{M}}^{*}y^{\prime},~{}x^{\prime}\not\approx
y^{\prime}\in\mathcal{M}\right\\}$ $\displaystyle\mathcal{S}^{*}=$
$\displaystyle~{}\mathcal{S}\cup\left\\{x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\
\middle|\ \exists
x^{\prime},s^{\prime}.~{}x\approx_{\mathcal{M}}^{*}x^{\prime},~{}s\approx_{\mathcal{S}}^{*}s^{\prime},~{}x^{\prime}\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s^{\prime}\in\mathcal{S}\right\\}$
$\displaystyle\phantom{~{}\mathcal{S}}\cup\left\\{x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\
\middle|\ \exists
x^{\prime},s^{\prime}.~{}x\approx_{\mathcal{M}}^{*}x^{\prime},~{}s\approx_{\mathcal{S}}^{*}s^{\prime},~{}x^{\prime}\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s^{\prime}\in\mathcal{S}\right\\}$

where $x$, $y$, $x^{\prime}$, $y^{\prime}$ in
$\operatorname{Terms}_{\mathsf{Element}}(\mathcal{M}\cup\mathcal{S})$, and
$s$, $s^{\prime}$ in $\operatorname{Terms}_{\mathsf{Set}}(\mathcal{S})$. Next,
we define a left-associative binary operator $\triangleleft$ that takes as
input a set $\mathcal{C}$ of constraints and a single constraint $l$.
Intuitively, $\mathcal{C}\triangleleft(l)$ adds $l$ to $\mathcal{C}$ only if
$l$ is not in $\mathcal{C}$’s closure. More precisely,

$\mathcal{C}\triangleleft(l)=\begin{cases}\mathcal{C}&\text{if
}l\in\mathcal{C}^{*}\\\ \mathcal{C}\cup\\{l\\}&\text{otherwise}\end{cases}$
(1)

The set of relevant terms, denoted by $\mathcal{T}$, for a state
$\langle\mathcal{S},\mathcal{M},\mathcal{A},\mathcal{G}\rangle$ consists of
all terms from $\mathcal{S}$ and $\mathcal{G}$, namely:
$\operatorname{Terms}(\mathcal{S})\cup V(\mathcal{G})$.

Figure 2 shows the rules for reasoning about membership in unions,
intersections, and differences. Each rule covers one case in which a new
membership (or non-membership) constraint can be deduced. The justification
for these rules is straightforward based on the semantics of the set
operations. The restriction $\\{u,v\\}=\\{s,t\\}$ in the premise of some of
the rules cover all the various cases where $s$, say, is the same as $t$,
different from $t$, the same as $u$, and the same as $v$. Figure 3 shows rules
for singletons, disequalities, and contradictions. Note in particular that the
Set Disequality rule introduces a fresh variable $y$, denoting an element that
is in one set but not in the other.

Singleton $\displaystyle\displaystyle{\hbox{\hskip
14.80211pt\vbox{\hbox{\hskip-14.80211pt\hbox{\hbox{$\displaystyle\displaystyle{\left\\{x\right\\}\in\mathcal{T}}$}}}\vbox{}}}\over\hbox{\hskip
40.3264pt\vbox{\vbox{}\hbox{\hskip-40.3264pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}\left\\{x\right\\})}$}}}}}}$
Single Member $\displaystyle\displaystyle{\hbox{\hskip
29.27734pt\vbox{\hbox{\hskip-29.27733pt\hbox{\hbox{$\displaystyle\displaystyle{x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}\left\\{y\right\\}\in\mathcal{S}^{*}}$}}}\vbox{}}}\over\hbox{\hskip
34.09952pt\vbox{\vbox{}\hbox{\hskip-34.09952pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{M}:=\mathcal{M}\triangleleft(x\approx
y)}$}}}}}}$ Single Non-member $\displaystyle\displaystyle{\hbox{\hskip
33.02734pt\vbox{\hbox{\hskip-33.02733pt\hbox{\hbox{$\displaystyle\displaystyle{x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}\left\\{y\right\\}\in\mathcal{S}^{*}}$}}}\vbox{}}}\over\hbox{\hskip
37.84952pt\vbox{\vbox{}\hbox{\hskip-37.84952pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{M}:=\mathcal{M}\triangleleft(x\not\approx
y)}$}}}}}}$
---
Set Disequality $\displaystyle\displaystyle{\hbox{\hskip
197.36574pt\vbox{\hbox{\hskip-197.36574pt\hbox{\hbox{$\displaystyle\displaystyle{s\not\approx
t\in\mathcal{S}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\left\\{x\in\mathcal{T}\
\middle|\
x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s,x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t\in\mathcal{S}^{*}\right\\}=\emptyset}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\left\\{x\in\mathcal{T}\
\middle|\
x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s,x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t\in\mathcal{S}^{*}\right\\}=\emptyset}$}}}}}\vbox{}}}\over\hbox{\hskip
140.0439pt\vbox{\vbox{}\hbox{\hskip-140.04388pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(y\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s)\triangleleft(y\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t)\quad\parallel\quad\mathcal{S}:=\mathcal{S}\triangleleft(y\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s)\triangleleft(y\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}t)}$}}}}}}$
Eq Unsat $\displaystyle\displaystyle{\hbox{\hskip
30.72633pt\vbox{\hbox{\hskip-30.72632pt\hbox{\hbox{$\displaystyle\displaystyle{(x\not\approx
x)\in\mathcal{M}^{*}}$}}}\vbox{}}}\over\hbox{\hskip
11.97226pt\vbox{\vbox{}\hbox{\hskip-11.97224pt\hbox{\hbox{$\displaystyle\displaystyle{\mathsf{unsat}}$}}}}}}$
Set Unsat $\displaystyle\displaystyle{\hbox{\hskip
72.28607pt\vbox{\hbox{\hskip-72.28607pt\hbox{\hbox{$\displaystyle\displaystyle{(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s)\in\mathcal{S}^{*}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{(x\not\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s)\in\mathcal{S}^{*}}$}}}}\vbox{}}}\over\hbox{\hskip
11.97226pt\vbox{\vbox{}\hbox{\hskip-11.97224pt\hbox{\hbox{$\displaystyle\displaystyle{\mathsf{unsat}}$}}}}}}$
Empty Unsat $\displaystyle\displaystyle{\hbox{\hskip
29.42429pt\vbox{\hbox{\hskip-29.42429pt\hbox{\hbox{$\displaystyle\displaystyle{(x\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}\emptyset)\in\mathcal{S}^{*}}$}}}\vbox{}}}\over\hbox{\hskip
11.97226pt\vbox{\vbox{}\hbox{\hskip-11.97224pt\hbox{\hbox{$\displaystyle\displaystyle{\mathsf{unsat}}$}}}}}}$
Figure 3. Singleton, disequality and contradiction rules. Here, $y$ is a fresh
variable.

Let

$\mathcal{S}=\\{S\approx A\sqcup B,\,S\approx
C\sqcap{D},\,x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}C,\,x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}D,\,y\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}S,\,y\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}D\\}.$

Using the rules in Figure 2, we can directly deduce the additional
constraints: $x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}C\sqcap{D}$ (by
Inter Up II), $x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}A$,
$x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}B$,
$y\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}A$,
$y\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}B$ (by Union Down I), and
$y\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}C$ (by Inter Down II). This gives
a complete picture, modulo equality, of exactly which sets contain $x$ and
$y$. ∎

###  3.2. Cardinality of sets

The next set of rules, described in Figure 6 and Figure 7, operate on the
graph component of the current state. Their purpose is to modify the graph so
as to capture the mutual dependencies between set and cardinality constraints.
They are based on the observation that $(i)$ the cardinality of two sets, and
that of their union, intersection and set difference are interrelated; and
$(ii)$ if two set terms are asserted to be equal, their cardinalities must
match.

$T$$U$$T\setminus U$$T\sqcap U$$U\setminus T$$T\sqcup U$ Figure 4. Venn
regions for $T$ and $U$.

$T$$T\sqcup U$$U$$T\setminus U$$T\sqcap U$$U\setminus T$ Figure 5. The same
structure as a graph.

Figure 5 shows the Venn regions for two sets, $T$ and $U$. The fact that
$T\setminus U$, $T\sqcap U$ and $U\setminus T$ are disjoint imposes the
following relationships between their cardinalities and those of $T$, $U$ and
$T\sqcup U$:

$\displaystyle\mathsf{card}(T)$
$\displaystyle\,\approx\,\mathsf{card}(T\setminus
U)\>\operatorname{\texttt{+}\,}\>\mathsf{card}(T\sqcap U)$
$\displaystyle\mathsf{card}(T\sqcup U)$
$\displaystyle\,\approx\,\mathsf{card}(T\setminus
U)\>\operatorname{\texttt{+}\,}\>\mathsf{card}(T\sqcap
U)\>\operatorname{\texttt{+}\,}\>\mathsf{card}(U\setminus T)$
$\displaystyle\mathsf{card}(U)$
$\displaystyle\,\approx\,\mathsf{card}(U\setminus
T)\>\operatorname{\texttt{+}\,}\>\mathsf{card}(T\sqcap U)\ .$

We can represent these same relationships using the graph in Figure 5. The
nodes of the graph are set terms, and each node has the property of being the
disjoint union of its children in the graph. Our calculus incrementally
constructs a similar graph containing all nodes whose cardinality is
implicitly or explicitly constrained by the current state. Set terms with
implicit cardinality constraints include $(i)$ union, intersection, and set
difference terms appearing in $\mathcal{S}$, for which one of the operands is
already in the graph; and $(ii)$ terms occurring in an equality whose other
member is already in the graph. A careful analysis555See completeness proof in
[Ban16, Chapter 2] for further details. reveals that we can actually avoid
adding intersection terms $t\sqcap u$ unless both $t$ and $u$ are already in
the graph, and set difference terms $t\setminus u$ unless $t$ is already in
the graph.

The rules in Figure 6 make use of a function $\operatorname{add}$ which takes
a graph $\mathcal{G}$ and a term $s$ and returns the graph
$\mathcal{G}^{\prime}$ defined as follows:

  1. (1)

For $s=T$ or $s=\emptyset$ or $s=\left\\{x\right\\}$:

     * $V(\mathcal{G}^{\prime})=V(\mathcal{G})\cup\\{s\\}$

     * $E(\mathcal{G}^{\prime})=E(\mathcal{G})$

  2. (2)

For $s=T\sqcap U$ or $s=T\setminus U$:

     * $V(\mathcal{G}^{\prime})=V_{2}=V(\mathcal{G})\cup\\{T,U,T\setminus U,T\sqcap U,U\setminus T\\}$

     * $E(\mathcal{G}^{\prime})=E_{2}=E(\mathcal{G})\cup\\{(T,T\setminus U),(T,T\sqcap U)$, $(U,T\sqcap U)$, $(U,U\setminus T)\\}$

  3. (3)

For $s=T\sqcup U$ and $V_{2}$ and $E_{2}$ as above:

     * $V(\mathcal{G}^{\prime})=V_{2}\cup\\{T\sqcup U\\}$

     * $E(\mathcal{G}^{\prime})=E_{2}\cup\\{(T\sqcup U,T\setminus U),(T\sqcup U,T\sqcap U),(T\sqcup U,U\setminus T)\\}$

Recall that, by assumption, each set variable participates in at most one
union, intersection, or set difference in the input set of constraints. It is
not difficult to see that this property is preserved by every rule. This
ensures that edges from a set variable node are added to the graph only once,
maintaining the invariant that its children in the graph are disjoint. The
only other rule which adds edges to the graph is the Merge Equality IIrule,
but it only adds nodes from the leaves of the graph, creating a new set of
disjoint leaves.

Terms with explicit constraints on their cardinality are added to the graph by
rule Introduce Card. Terms that have implicit constraints on their
cardinality, specifically, singletons and the empty set, are added by rules
Introduce Singleton and Introduce Empty Set.

If two nodes $s$ and $t$ in the graph are explicitly asserted to be equal
(that is, $s\approx t\in\mathcal{S}$ or $t\approx s\in\mathcal{S}$), we can
ensure they have the same cardinality by systematically modifying the graph as
follows. Let $\mathcal{L}(n)$ denote the set of leaf nodes for the subtree
rooted at node $n$ which are not known to be empty. Formally,

$\mathcal{L}(n)=\left\\{n^{\prime}\in\operatorname{Leaves}{(n)}\ \middle|\
n^{\prime}\approx\emptyset\not\in\mathcal{S}^{*}\right\\},$ (2)

where $\operatorname{Leaves}{(v)}=\left\\{w\in V(\mathcal{G})\ \middle|\
C(w)=\emptyset,w\text{ is reachable from }v\right\\}$ and $C(w)$ denotes the
children of $w$. We call two nodes $n$ and $n^{\prime}$ merged if they have
the same set of nonempty leaves, that is if
$\mathcal{L}(n)=\mathcal{L}(n^{\prime})$.

Introduce Eq Right $\displaystyle\displaystyle{\hbox{\hskip
84.13875pt\vbox{\hbox{\hskip-84.13875pt\hbox{\hbox{$\displaystyle\displaystyle{S\approx
t\in\mathcal{S}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{S\in V(\mathcal{G})}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{t\not\in
V(\mathcal{G})}$}}}}}\vbox{}}}\over\hbox{\hskip
29.09727pt\vbox{\vbox{}\hbox{\hskip-29.09726pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{G}:=\operatorname{add}(\mathcal{G},t)}$}}}}}}$
Introduce Eq Left $\displaystyle\displaystyle{\hbox{\hskip
82.7499pt\vbox{\hbox{\hskip-82.7499pt\hbox{\hbox{$\displaystyle\displaystyle{S\approx
t\in\mathcal{S}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{S\not\in
V(\mathcal{G})}$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{t\in
V(\mathcal{G})}$}}}}}\vbox{}}}\over\hbox{\hskip
30.64587pt\vbox{\vbox{}\hbox{\hskip-30.64586pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{G}:=\operatorname{add}(\mathcal{G},S)}$}}}}}}$
---
Introduce Union $\displaystyle\displaystyle{\hbox{\hskip
136.75354pt\vbox{\hbox{\hskip-136.75354pt\hbox{\hbox{$\displaystyle\displaystyle{S\approx
T\sqcup U\in\mathcal{S}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{T\sqcup U\not\in
V(\mathcal{G})}$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{T\in
V(\mathcal{G})\text{ or }U\in V(\mathcal{G})}$}}}}}\vbox{}}}\over\hbox{\hskip
40.42256pt\vbox{\vbox{}\hbox{\hskip-40.42256pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{G}:=\operatorname{add}(\mathcal{G},T\sqcup
U)}$}}}}}}$
Introduce Inter $\displaystyle\displaystyle{\hbox{\hskip
138.96188pt\vbox{\hbox{\hskip-138.96188pt\hbox{\hbox{$\displaystyle\displaystyle{S\approx
T\sqcap U\in\mathcal{S}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{T\sqcap U\not\in
V(\mathcal{G})}$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{T\in
V(\mathcal{G})}$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{U\in
V(\mathcal{G})}$}}}}}}\vbox{}}}\over\hbox{\hskip
40.42256pt\vbox{\vbox{}\hbox{\hskip-40.42256pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{G}:=\operatorname{add}(\mathcal{G},T\sqcap
U)}$}}}}}}$
Introduce Set difference $\displaystyle\displaystyle{\hbox{\hskip
106.77377pt\vbox{\hbox{\hskip-106.77376pt\hbox{\hbox{$\displaystyle\displaystyle{S\approx
T\setminus U\in\mathcal{S}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{T\in V(\mathcal{G})}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{T\setminus U\not\in
V(\mathcal{G})}$}}}}}\vbox{}}}\over\hbox{\hskip
40.97812pt\vbox{\vbox{}\hbox{\hskip-40.97812pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{G}:=\operatorname{add}(\mathcal{G},T\setminus
U)}$}}}}}}$
Introduce Card $\displaystyle\displaystyle{\hbox{\hskip
31.56657pt\vbox{\hbox{\hskip-31.56657pt\hbox{\hbox{$\displaystyle\displaystyle{c_{s}\approx\mathsf{card}(S)\in\mathcal{S}}$}}}\vbox{}}}\over\hbox{\hskip
30.64587pt\vbox{\vbox{}\hbox{\hskip-30.64586pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{G}:=\operatorname{add}(\mathcal{G},S)}$}}}}}}$
Introduce Singleton $\displaystyle\displaystyle{\hbox{\hskip
31.37158pt\vbox{\hbox{\hskip-31.37158pt\hbox{\hbox{$\displaystyle\displaystyle{\left\\{x\right\\}\in\operatorname{Terms}(\mathcal{S})}$}}}\vbox{}}}\over\hbox{\hskip
34.31606pt\vbox{\vbox{}\hbox{\hskip-34.31604pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{G}:=\operatorname{add}(\mathcal{G},\left\\{x\right\\})}$}}}}}}$
Introduce Empty Set $\displaystyle\displaystyle{\hbox{\hskip
5.00002pt\vbox{\hbox{\hskip-5.0pt\hbox{\hbox{$\displaystyle\displaystyle{\quad}$}}}\vbox{}}}\over\hbox{\hskip
29.79172pt\vbox{\vbox{}\hbox{\hskip-29.79172pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{G}:=\operatorname{add}(\mathcal{G},\emptyset)}$}}}}}}$
Figure 6. Graph extension rules. Merge Equality I
$\displaystyle\displaystyle{\hbox{\hskip
130.07983pt\vbox{\hbox{\hskip-130.07983pt\hbox{\hbox{$\displaystyle\displaystyle{s\approx
t\in\mathcal{S}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{s,t,\emptyset\in
V(\mathcal{G})}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\\{u,v\\}=\\{s,t\\}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L}(u)\subsetneq\mathcal{L}(v)}$}}}}}}\vbox{}}}\over\hbox{\hskip
67.38731pt\vbox{\vbox{}\hbox{\hskip-67.38731pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\left\\{s^{\prime}\approx\emptyset\
\middle|\
s^{\prime}\in\mathcal{L}(v)\setminus\mathcal{L}(u)\right\\}\cup\mathcal{S}}$}}}}}}$
---
Merge Equality II $\displaystyle\displaystyle{\hbox{\hskip
119.54857pt\vbox{\hbox{\hskip-119.54857pt\hbox{\hbox{$\displaystyle\displaystyle{s\approx
t\in\mathcal{S}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{s,t\in
V(\mathcal{G})}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L}(s)\nsubseteq\mathcal{L}(t)}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L}(t)\nsubseteq\mathcal{L}(s)}$}}}}}}\vbox{}}}\over\hbox{\hskip
38.67711pt\vbox{\vbox{}\hbox{\hskip-38.67711pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{G}:=\operatorname{merge}(\mathcal{G},s,t)}$}}}}}}$
Figure 7. Merge rules.

The rules in Figure 7 ensure that for all equalities over set terms, the
corresponding nodes in the graph are merged. Consider an equality $s\approx
t$. Rule Merge Equality I handles the case when either $\mathcal{L}(s)$ or
$\mathcal{L}(t)$ is a proper subset of the other by constraining the extra
leaves in the superset to be empty. Rule Merge Equality II handles the
remaining case where neither is a subset of the other. The graph
$\mathcal{G}^{\prime}=\operatorname{merge}(\mathcal{G},s,t)$ is defined as
follows, where $L_{1}=\mathcal{L}(s)\setminus\mathcal{L}(t)$ and
$L_{2}=\mathcal{L}(t)\setminus\mathcal{L}(s)$:

$\displaystyle V(\mathcal{G}^{\prime})$ $\displaystyle=$ $\displaystyle
V(\mathcal{G})\cup\left\\{l_{1}\sqcap l_{2}\ \middle|\ l_{1}\in L_{1},l_{2}\in
L_{2}\right\\}$ $\displaystyle E(\mathcal{G}^{\prime})$ $\displaystyle=$
$\displaystyle E(\mathcal{G})\cup\left\\{(l_{1},l_{1}\sqcap
l_{2}),(l_{2},l_{1}\sqcap l_{2})\ \middle|\ l_{1}\in L_{1},l_{2}\in
L_{2}\right\\}$

Merge Equality II introduces a quadratic number of leaves
($\left|L_{1}\right|\cdot\left|L_{2}\right|$). To reduce the impact of merge
operations, a useful rule to apply early on is the (optional) Guess Empty Set
rule in Figure 8. It guesses if a leaf node is equal to the empty set or not.
The use of this rule is illustrated in Example 3.3. Here and in Figure 9,
$\operatorname{Leaves}{(\mathcal{G})}=\\{v\in V(\mathcal{G})\ |\
C(v)=\emptyset\\}$.

In Figure 8 we denote by $\hat{\mathcal{G}}$ the collection of all of the
following cardinality constraints imposed by graph $\mathcal{G}$:

  1. (1)

For each set term $s\in V(\mathcal{G})$, its cardinality (denoted by its
corresponding cardinality variable $c_{s}$) is the sum of the cardinalities of
its non-empty leaf nodes:

$\left\\{c_{s}\approx\sum_{t\in\mathcal{L}(s)}c_{t}\ \middle|\ s\in
V(\mathcal{G})\right\\}$

  2. (2)

Each cardinality is non-negative:

$\left\\{c_{s}\operatorname{\texttt{>=}\,}0\ \middle|\ s\in
V(\mathcal{G})\right\\}$

  3. (3)

Every singleton set has cardinality $1$:

$\left\\{c_{s}\approx 1\ \middle|\ s\in
V(\mathcal{G}),~{}s=\left\\{x\right\\}\right\\}$

  4. (4)

The empty set has cardinality $0$:

$\left\\{c_{s}\approx 0\ \middle|\ s\in
V(\mathcal{G}),~{}s=\emptyset\right\\}$

Rule Arithmetic contradiction relies on the arithmetic solver to check whether
the constraints in $\hat{\mathcal{G}}$ are inconsistent with the input
cardinality constraints.

Arithmetic contradiction $\displaystyle\displaystyle{\hbox{\hskip
20.72226pt\vbox{\hbox{\hskip-20.72226pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{A}\cup\hat{\mathcal{G}}\models_{{\mathfrak{T}_{A}}}\bot}$}}}\vbox{}}}\over\hbox{\hskip
11.97226pt\vbox{\vbox{}\hbox{\hskip-11.97224pt\hbox{\hbox{$\displaystyle\displaystyle{\mathsf{unsat}}$}}}}}}$
Guess Empty Set $\displaystyle\displaystyle{\hbox{\hskip
28.74307pt\vbox{\hbox{\hskip-28.74306pt\hbox{\hbox{$\displaystyle\displaystyle{t\in\operatorname{Leaves}{(\mathcal{G})}}$}}}\vbox{}}}\over\hbox{\hskip
77.08327pt\vbox{\vbox{}\hbox{\hskip-77.08325pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{S}:=\mathcal{S}\triangleleft(t\approx\emptyset)\quad\parallel\quad\mathcal{S}:=\mathcal{S}\triangleleft(t\not\approx\emptyset)}$}}}}}}$
---
Figure 8. Additional graph rules.

###  3.3. Cardinality and membership interaction

The rules in Figure 9 propagate consequences of set membership constraints to
the state components $\mathcal{M}$ and $\mathcal{A}$. Let $\mathcal{E}$ denote
the set of equalities in $\mathcal{M}$, and let $\left[x\right]_{\mathcal{E}}$
denote the equivalence class of $x$ with respect to $\mathcal{E}$. In the
rules, for term $t$ of sort $\mathsf{Set}$, $t_{\mathcal{S}}$ denotes the set
$\left\\{\left[x\right]_{\mathcal{E}}\ \middle|\
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathcal{S}^{*}\right\\}$ of
equivalence classes of elements known to be in $t$. The notation
$\mathcal{A}\Rrightarrow c_{t}\geq n$ means that
$c_{t}\operatorname{\texttt{>=}\,}k\in\mathcal{A}$ for some concrete constant
$k\geq n$.

Members Arrangement $\displaystyle\displaystyle{\hbox{\hskip
150.51659pt\vbox{\hbox{\hskip-150.51657pt\hbox{\hbox{$\displaystyle\displaystyle{t\in\operatorname{Leaves}{(\mathcal{G})}\quad\mathcal{A}\not\Rrightarrow
c_{t}\geq\left|t_{\mathcal{S}}\right|\quad\left[x\right]_{\mathcal{E}},\left[y\right]_{\mathcal{E}}\in
t_{\mathcal{S}}\quad\left[x\right]_{\mathcal{E}}\neq\left[y\right]_{\mathcal{E}}\quad
x\not\approx y\not\in\mathcal{M}^{*}}$}}}\vbox{}}}\over\hbox{\hskip
86.67123pt\vbox{\vbox{}\hbox{\hskip-86.67122pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{M}:=\mathcal{M}\triangleleft(x\approx
y)\quad\parallel\quad\mathcal{M}:=\mathcal{M}\triangleleft(x\not\approx
y)}$}}}}}}$
---
Guess Lower Bound $\displaystyle\displaystyle{\hbox{\hskip
103.48174pt\vbox{\hbox{\hskip-103.48174pt\hbox{\hbox{$\displaystyle\displaystyle{t\in\operatorname{Leaves}{(\mathcal{G})}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{A}\not\Rrightarrow
c_{t}\geq\left|t_{\mathcal{S}}\right|}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{c_{t}\operatorname{\texttt{<}\,}\left|t_{\mathcal{S}}\right|\not\in\mathcal{A}}$}}}}}\vbox{}}}\over\hbox{\hskip
77.79424pt\vbox{\vbox{}\hbox{\hskip-77.79422pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{A}:=c_{t}\operatorname{\texttt{>=}\,}\left|t_{\mathcal{S}}\right|,\mathcal{A}\quad\parallel\quad\mathcal{A}:=c_{t}\operatorname{\texttt{<}\,}\left|t_{\mathcal{S}}\right|,\mathcal{A}}$}}}}}}$
Propagate Minsize $\displaystyle\displaystyle{\hbox{\hskip
167.89227pt\vbox{\hbox{\hskip-167.89227pt\hbox{\hbox{$\displaystyle\displaystyle{x_{1}\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s,\ldots,x_{n}\mathrel{\ooalign{$\displaystyle\sqsubset$\cr{$\displaystyle-$}}}s\in\mathcal{S}^{*}\quad\mathcal{A}\not\Rrightarrow
c_{s}\geq n}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{x_{i}\not\approx
x_{j}\in\mathcal{M}^{*}\text{ for all }1\leq i<j\leq
n}$}}}}\vbox{}}}\over\hbox{\hskip
30.64413pt\vbox{\vbox{}\hbox{\hskip-30.64412pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{A}:=c_{s}\operatorname{\texttt{>=}\,}n,\mathcal{A}}$}}}}}}$
Figure 9.  Cardinality and membership interaction rules.

Rule Members Arrangement is used to decide which element variables constrained
to be in the same set $t$ should be identified and which should not. Once
applied to completion, Rule Propagate Minsize can then be used to determine a
lower bound for the cardinality of that set. The (optional) rule Guess Lower
Bound can be used to short-circuit this process by guessing a conservative
lower bound based on the number of distinct equivalence classes of elements
known to be members of a set. If this does not lead to a contradiction, a
model can be found without resorting to an extensive use of Members
Arrangement.

Consider again the constraints from Example 3.1, but now augmented with
cardinality constraints:

$\displaystyle\mathcal{S}$ $\displaystyle=$ $\displaystyle\\{S\approx A\sqcup
B,\,S\approx
C\sqcap{D},\,x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}C,\,x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}D,\,y\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}S,\,y\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}D\\}$
$\displaystyle\mathcal{A}$ $\displaystyle=$
$\displaystyle\\{c_{S}\approx\mathsf{card}(S),\,c_{C}\approx\mathsf{card}(C),\,c_{D}\approx\mathsf{card}(D),\,c_{S}\operatorname{\texttt{>=}\,}4,\,c_{C}+c_{D}\operatorname{\texttt{<}\,}10\\}$

Using the rules in Figure 6, the following nodes get added to the graph: $S$,
$C$, $D$ (by Introduce Card), $A\sqcup B$, $C\sqcap D$ (by Introduce Eq
Right). Node $A\sqcup B$ is added with children $A\setminus B$, $A\sqcap B$,
and $B\setminus A$; and by adding $C\sqcap D$, we also get $C\setminus D$ and
$D\setminus C$, with the corresponding edges from $C$ and $D$. Now, using two
applications of Merge Equality II, we force the sets $S$, $A\sqcup B$ and
$C\sqcap D$ to have the same set of 3 leaves, labeled $S\sqcap(A\setminus
B)\sqcap(C\sqcap D)$, $S\sqcap(A\sqcap B)\sqcap(C\sqcap D)$, and
$S\sqcap(B\setminus A)\sqcap(C\sqcap D)$. Let us call the latter nodes
respectively $l_{1}$, $l_{2}$, and $l_{3}$, for convenience. Let us also
designate $l_{4}=C\setminus D$ and $l_{5}=D\setminus C$. Notice that the
induced cardinality constraints now include $c_{S}\approx
c_{l_{1}}\operatorname{\texttt{+}\,}c_{l_{2}}\operatorname{\texttt{+}\,}c_{l_{3}}$,
$c_{C}\approx
c_{l_{1}}\operatorname{\texttt{+}\,}c_{l_{2}}\operatorname{\texttt{+}\,}c_{l_{3}}\operatorname{\texttt{+}\,}c_{l_{4}}$,
and $c_{D}\approx
c_{l_{1}}\operatorname{\texttt{+}\,}c_{l_{2}}\operatorname{\texttt{+}\,}c_{l_{3}}\operatorname{\texttt{+}\,}c_{l_{5}}$.
With the addition of $C\setminus D$ and $D\setminus C$ to the graph, these are
also added to $\mathcal{T}$. We can then deduce
$x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}C\setminus D$ and
$y\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}D\setminus C$ using the rules for set
difference. Finally, we can use Propagate Minsize to deduce
$c_{l_{4}}\operatorname{\texttt{>=}\,}1$ and
$c_{l_{5}}\operatorname{\texttt{>=}\,}1$. It is now not hard to see that using
pure arithmetic reasoning, we can deduce that
$c_{C}\operatorname{\texttt{+}\,}c_{D}\operatorname{\texttt{>=}\,}10$ which
leads to $\mathsf{unsat}$ using Arithmetic contradiction. ∎

##  4\. Calculus Correctness

Our calculus is terminating and sound for any derivation strategy, that is,
regardless of how the rules are applied. It is also refutation complete for
any fair strategy, defined as a strategy that does not delay indefinitely the
application of an applicable derivation rule.

To prove these properties it is convenient to partition the derivation rules
of the calculus in the following subsets.

  * $\mathcal{R}_{1}$, membership predicate reasoning rules, from Figures 2 and 3.

  * $\mathcal{R}_{2}$, graph rules to reason about cardinality, from Figures 6, 7 and 8.

  * $\mathcal{R}_{3}$, rules from Figure 9 other than Rule Guess Lower Bound.

  * $\mathcal{R}_{4}$, rule Guess Lower Bound.

The rules are used to construct derivation trees. A derivation tree is a tree
over states, with a root of the form
$\langle\mathcal{S}_{0},\mathcal{M}_{0},\mathcal{A}_{0},(\emptyset,\emptyset)\rangle$
where $\mathcal{S}_{0}\cup\mathcal{M}_{0}\cup\mathcal{A}_{0}$ satisfies
Restriction 3 and the children of each non-root node are obtained by applying
one of the derivation rules of the calculus to that node. Let $\mathcal{R}$ be
a subset of the derivation rules of the calculus. A state is saturated with
respect to $\mathcal{R}$ if no rules in $\mathcal{R}$ apply to it. A branch of
a derivation tree is closed if it ends with $\mathsf{unsat}$; it is saturated
with respect to $\mathcal{R}$ if so is its leaf. A derivation tree is closed
if all of its branches are closed. A derivation tree derives from a derivation
tree $T$ if it is obtained from $T$ by the application of exactly one of the
derivation rules to one of $T$’s leaves.

[Derivations]Let $\mathcal{C}$ be a set of ${\mathfrak{T}_{S}}$-constraints. A
derivation (of $\mathcal{C}$) is a sequence $(T_{i})_{0\leq i\leq\kappa}$ of
derivation trees, with $\kappa$ finite or countably infinite, such that
$T_{i+1}$ derives from $T_{i}$ for all $i$, and $T_{0}$ is a one-node tree
whose root is a state
$\langle\mathcal{S}_{0},\mathcal{M}_{0},\mathcal{A}_{0},(\emptyset,\emptyset)\rangle$
where $\mathcal{S}_{0}\cup\mathcal{M}_{0}\cup\mathcal{A}_{0}=\mathcal{C}$. A
refutation (of $\mathcal{C}$) is a (finite) derivation of $\mathcal{C}$ that
ends with a closed tree.

######  Remark 1.

In the proofs below we implicitly rely on the fact that, for every state
$\langle\mathcal{S},\mathcal{M},\mathcal{A},\mathcal{G}\rangle$ in a
derivation tree, the constraints in
$\mathcal{S}\cup\mathcal{M}\cup\mathcal{A}$ satisfy Restriction 3. This is the
case because the restriction is imposed on root states and is preserved by all
of its rules, as one can easily verify.

###  4.1. Termination

######  Proposition 2 (Termination).

Let $\mathcal{R}$ collect all rules in our calculus except for (the optional)
rule Guess Lower Bound. Every derivation using only rules from $\mathcal{R}$
is finite.

######  Proof 4.1.

Let
$\langle\mathcal{S}_{0},\mathcal{M}_{0},\mathcal{A}_{0},(\emptyset,\emptyset)\rangle$
be the initial state of the derivation. We first define a well-founded
relation $\succ$ over states. Next, we show that application of any rule in
$\mathcal{R}$ to a leaf of a derivation tree gives smaller states with respect
to this relation. As the relation is well-founded, it will follow that the
derivation cannot be infinite.

In order to define $\succ$, we define $f_{i}$ for $i\in\\{1,2,\ldots,9\\}$,
each of which maps a state
$\sigma=\langle\mathcal{S},\mathcal{M},\mathcal{A},\mathcal{G}\rangle$ to a
natural number (non-negative integer). We denote the set of natural numbers by
$\mathbb{N}$.

  * •

$f_{1}(\sigma)$: number of equalities $t_{1}\approx t_{2}$ in $\mathcal{S}$
such that either $t_{1}\not\in V(\mathcal{G})$, $t_{2}\not\in V(\mathcal{G})$,
or $\mathcal{L}(t_{1})\neq\mathcal{L}(t_{2})$.

  * •

$f_{2}(\sigma)$: size of
$(\operatorname{Terms}_{\mathsf{Set}}(\mathcal{S})\cup\\{\emptyset\\})\setminus
V(\mathcal{G})$.

  * •

$f_{3}(\sigma)$: size of $\left\\{t\in\operatorname{Leaves}{(\mathcal{G})}\
\middle|\
t\approx\emptyset\not\in\mathcal{S}^{*},t\not\approx\emptyset\not\in\mathcal{S}^{*}\right\\}$.

  * •

$f_{4}(\sigma)$: number of disequalities $t_{1}\not\approx t_{2}$ in
$\mathcal{S}$ such that the premise of Set Disequality holds.

  * •

$f_{5}(\sigma)$: size of
$\operatorname{Terms}_{\mathsf{Set}}(\mathcal{S})\cup\\{\emptyset\\}\cup
V(\mathcal{G})$.

  * •

$f_{6}(\sigma)$: size of
$\operatorname{Terms}_{\mathsf{Element}}(\mathcal{S}\cup\mathcal{M})$.

  * •

$f_{7}(\sigma)$: size of $\mathcal{M}^{*}$ subtracted from
$2\cdot\left(f_{6}(\sigma)\right)^{2}$. As all constraints in
$\mathcal{M}^{*}$ are either $x\approx y$ or $x\not\approx y$ with $x$ and $y$
in $\operatorname{Terms}_{\mathsf{Element}}(\mathcal{S}\cup\mathcal{M})$, the
size of $\mathcal{M}^{*}$ can be at most
$2\cdot\left(f_{6}(\sigma)\right)^{2}$. Thus, $f_{7}(\cdot)$ is well-defined
as a map into $\mathbb{N}$.

  * •

$f_{8}(\sigma)$: size of $\mathcal{S}^{*}$ subtracted from
$2\cdot\left(f_{5}(\sigma)\right)^{2}+2\cdot f_{5}(\sigma)\cdot
f_{6}(\sigma)$. There are at most $2\cdot\left(f_{5}(\sigma)\right)^{2}$
constraints of the form $s\approx t$ or $s\not\approx t$ in $\mathcal{S}^{*}$
as $s$ and $t$ are in
$\operatorname{Terms}_{\mathsf{Set}}(\mathcal{S})\cup\\{\emptyset\\}\cup
V(\mathcal{G})$. There are at most $2\cdot f_{5}(\sigma)\cdot f_{6}(\sigma)$
constraints of the form $x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s$ or
$x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s$ in $\mathcal{S}^{*}$ as $x$
and $s$ are in
$\operatorname{Terms}_{\mathsf{Element}}(\mathcal{S}\cup\mathcal{M})$ and
$\operatorname{Terms}_{\mathsf{Set}}(\mathcal{S})\cup\\{\emptyset\\}\cup
V(\mathcal{G})$ respectively. Thus, $f_{8}(\cdot)$ is well-defined as a map
into $\mathbb{N}$.

  * •

$f_{9}(\sigma)$: size of
$\left(\operatorname{Terms}_{\mathsf{Set}}(\mathcal{S})\cup\\{\emptyset\\}\cup
V(\mathcal{G})\right)\setminus\left\\{t\in\operatorname{Leaves}{(\mathcal{G})}\
\middle|\ \mathcal{A}\not\Rrightarrow
c_{t}\geq\mathsf{card}(t_{\mathcal{S}})\right\\}$.

Then, we define the order $\succ$ over states as follows:

  * •

$\sigma\succ\sigma^{\prime}$ if $\sigma\neq\mathsf{unsat}$ and
$\sigma^{\prime}=\mathsf{unsat}$.

  * •

$\sigma\succ\sigma^{\prime}$ if $\sigma\neq\mathsf{unsat}$,
$\sigma^{\prime}\neq\mathsf{unsat}$, and

$\left(f_{1}(\sigma),\ldots,f_{9}(\sigma)\right)>^{9}_{\textsf{lex}}\left(f_{1}(\sigma^{\prime}),\ldots,f_{9}(\sigma^{\prime})\right)$

where $\left(\mathbb{N}^{9},>^{9}_{\textsf{lex}}\right)$ is the $9$-fold
lexicographic product of ordering over natural numbers
$\left(\mathbb{N},>\right)$.

  * •

$\sigma\not\succ\sigma^{\prime}$ otherwise.

The well-foundedness of $\succ$ over states follows from the well-foundedness
of $\left(\mathbb{N}^{9},>^{9}_{\textsf{lex}}\right)$ [BN98, Section 2.4].

Let $r\in\mathcal{R}$ be a rule applicable at state $\sigma$, and let
$\sigma^{\prime}$ be the state after the application of the rule (if there are
multiple conclusions, denote the state on first branch as
$\sigma_{1}^{\prime}$, second branch as $\sigma_{2}^{\prime}$ and so on). We
note below for each rule $r\in\mathcal{R}$ the relation between
$f_{1}(\sigma)$, $\ldots$, $f_{9}(\sigma)$ and $f_{1}(\sigma^{\prime})$,
$\ldots$, $f_{9}(\sigma^{\prime})$ which establishes that
$\sigma\succ\sigma^{\prime}$.

  * •

First, we consider Rules for intersection (Figure 2), union (Figure 2), set
difference (Figure 2) and Rule Singleton for singleton. None of these rules
introduce equalities of set terms, nor do they affect the graph $\mathcal{G}$;
thus $f_{1}(\sigma)\geq f_{1}(\sigma^{\prime})$. The only terms introduced to
$\mathcal{S}$ are from $V(\mathcal{G})$, thus
$f_{2}(\sigma)=f_{2}(\sigma^{\prime})$. None of these rules update
$\mathcal{G}$ or introduce equalities or disequalities of set terms, thus
$f_{3}(\sigma)=f_{3}(\sigma^{\prime})$. None of these rules introduce
disequalities between set terms, thus $f_{4}(\sigma)\geq
f_{4}(\sigma^{\prime})$. None of these rules introduce set terms not already
in $\mathcal{S}$ or $V(\mathcal{G})$, thus
$f_{5}(\sigma)=f_{5}(\sigma^{\prime})$. None of the rules introduce
$\mathsf{Element}$ variables not already in $\mathcal{S}$ or $\mathcal{M}$,
thus $f_{6}(\sigma)=f_{6}(\sigma^{\prime})$. None of these rules update
$\mathcal{M}$, thus $f_{7}(\sigma)=f_{7}(\sigma^{\prime})$.

Each of these rules updates $\mathcal{S}$. Recall that for a rule to be
applicable at $\sigma$, the resulting state must be different from $\sigma$.
From the definition of $\triangleleft$, we can conclude that the size of
$\mathcal{S}^{*}$ has increased. As $f_{5}(\sigma)=f_{5}(\sigma^{\prime})$ and
$f_{6}(\sigma)=f_{6}(\sigma^{\prime})$, it follows that
$f_{8}(\sigma)>f_{8}(\sigma^{\prime})$.

  * •

Next, we consider Rules Single Member, Single Non-member and Members
Arrangement. None of these rules introduce equalities of set terms, thus
$f_{1}(\sigma)\geq f_{1}(\sigma^{\prime})$. None of these rules introduce set
terms to $\mathcal{S}$ or $V(\mathcal{G})$, thus
$f_{2}(\sigma)=f_{2}(\sigma^{\prime})$. None of these rules update
$\mathcal{G}$ or introduce equalities or disequality of set terms, thus
$f_{3}(\sigma)=f_{3}(\sigma^{\prime})$. None of these rules introduce
disequalities of set terms, thus $f_{4}(\sigma)\geq f_{4}(\sigma^{\prime})$.
None of these rules introduce set terms to $\mathcal{S}$ or $V(\mathcal{G})$,
thus $f_{5}(\sigma)=f_{5}(\sigma^{\prime})$. None of the rules introduce
$\mathsf{Element}$ variables not already in $\mathcal{S}$ or $\mathcal{M}$,
thus $f_{6}(\sigma)=f_{6}(\sigma^{\prime})$.

Each of these rules updates $\mathcal{M}$. From the definition of
$\triangleleft$, we can conclude that the size of $\mathcal{M}^{*}$ has
increased. As $f_{6}(\sigma)=f_{6}(\sigma^{\prime})$, we can conclude that
$f_{7}(\sigma)>f_{7}(\sigma^{\prime})$.

  * •

Next, we consider Rule Set Disequality. The rule does not introduce any
equality of set terms, thus $f_{1}(\sigma)\geq f_{1}(\sigma_{i}^{\prime})$ for
$i\in\\{1,2\\}$. The rule does not introduce set terms to $\mathcal{S}$ or
$V(\mathcal{G})$, thus $f_{2}(\sigma)=f_{2}(\sigma_{i}^{\prime})$ for
$i\in\\{1,2\\}$. The rule does not update $\mathcal{G}$, thus
$f_{3}(\sigma)\geq f_{3}(\sigma_{i}^{\prime})$ for $i\in\\{1,2\\}$. The
premise of the rule does not hold after application of the rule on either of
the branches. It follows that $f_{4}(\sigma)>f_{4}(\sigma_{i}^{\prime})$ for
$i\in\\{1,2\\}$.

  * •

Next, we consider Introduce Rules (Figure 6). Note that none of these rules
introduce equalities of set terms. Also note that if $t_{1}\in
V(\mathcal{G})$, $t_{2}\in V(\mathcal{G})$ and $t_{1}\approx t_{2}$ in
$\mathcal{S}$ then $\mathcal{L}(t_{1})=\mathcal{L}(t_{2})$ (see Proposition 5,
property 1). Thus, $f_{1}(\sigma)\geq f_{1}(\sigma^{\prime})$.

Each of the rules adds at least one new node to $\mathcal{G}$ which is in
$\operatorname{Terms}_{\mathsf{Set}}(\mathcal{S})\cup\\{\emptyset\\}$. At the
same time, $\mathcal{S}$ is unchanged. It follows that
$f_{2}(\sigma)>f_{2}(\sigma^{\prime})$.

  * •

Rules Merge Equality I and Merge Equality II. Though these rules add
equalities of the form $u\approx\emptyset$ to $\mathcal{S}$, the equalities
are such that $u\in V(\mathcal{G})$, $\emptyset\in V(\mathcal{G})$ and
$\mathcal{L}(u)=\emptyset=\mathcal{L}(\emptyset)$. It follows that
$f_{1}(\sigma)\geq f_{1}(\sigma^{\prime})$.

Now, observe that for Rule Merge Equality I or Rule Merge Equality II to be
applicable, there must exist $s\approx t\in\mathcal{S}$ such that
$\mathcal{L}(s)\neq\mathcal{L}(t)$. After the application of the rule,
$\mathcal{L}(s)=\mathcal{L}(t)$. This shows that
$f_{1}(\sigma)>f_{1}(\sigma^{\prime})$.

  * •

Rule Merge Equality III. For the rule to be applicable, there must exist
$s\approx t\in\mathcal{S}$ such that $\mathcal{L}(s)\neq\mathcal{L}(t)$. After
the application of the rule, $\mathcal{L}(s)=\mathcal{L}(t)$. Thus,
necessarily $f_{1}(\sigma)>f_{1}(\sigma^{\prime})$.

  * •

Rule Guess Empty Set. Note that though this rule may add an equality of the
form $t\approx\emptyset$ on the first branch, using the same reasoning as for
Rules Merge Equality I and Merge Equality II above, we can conclude that
$f_{1}(\sigma)\geq f_{1}(\sigma_{1}^{\prime})$. On the second branch, as no
disequality is added, we get that $f_{1}(\sigma)\geq
f_{1}(\sigma_{2}^{\prime})$. Only terms introduced to $\mathcal{S}$ are from
$V(\mathcal{G})$, thus $f_{2}(\sigma)=f_{2}(\sigma_{1}^{\prime})$ for
$i\in\\{1,2\\}$.

In order to apply the rule, we pick a $t\in\operatorname{Leaves}{(G)}$ such
that $t\approx\emptyset\not\in\mathcal{S}^{*}$ and
$t\not\approx\emptyset\not\in\mathcal{S}^{*}$. On the first branch,
$t\approx\emptyset\in\mathcal{S}^{*}$, thus
$f_{3}(\sigma)>f_{3}(\sigma_{1}^{\prime})$. On the second branch,
$t\not\approx\emptyset\in\mathcal{S}^{*}$, thus
$f_{3}(\sigma)>f_{3}(\sigma_{2}^{\prime})$.

  * •

Rule Propagate Minsize. The rule does not update $\mathcal{S}$, $\mathcal{M}$,
or $\mathcal{G}$, thus $f_{1}(\sigma)=f_{1}(\sigma^{\prime})$,
$f_{2}(\sigma)=f_{2}(\sigma^{\prime})$,
$f_{3}(\sigma)=f_{3}(\sigma^{\prime})$,
$f_{4}(\sigma)=f_{4}(\sigma^{\prime})$,
$f_{5}(\sigma)=f_{5}(\sigma^{\prime})$,
$f_{6}(\sigma)=f_{6}(\sigma^{\prime})$,
$f_{7}(\sigma)=f_{7}(\sigma^{\prime})$, and
$f_{8}(\sigma)=f_{8}(\sigma^{\prime})$. But,
$f_{9}(\sigma)>f_{9}(\sigma^{\prime})$.

  * •

Rules Eq Unsat, Set Unsat, Empty Unsat, and Arithmetic contradiction. For each
of these rules to be applicable, $\sigma\neq\mathsf{unsat}$. On the other
hand, $\sigma^{\prime}=\mathsf{unsat}$ after the application of the rule. By
definition, $\sigma\succ\sigma^{\prime}$.

######  Remark 3.

It is easy to extend the termination proof above to include the optional rule
Guess Lower Bound. It would involve tracking sizes of additional objects—a
strategy similar to the one adopted for Rule Guess Empty Set in our proof
would suffice.

###  4.2. Completeness

We prove properties about different subsets of rules, developing the
completeness proof in stages. We start with a proposition about rule set
$\mathcal{R}_{1}$.

######  Proposition 4.

Let $\langle\mathcal{S},\mathcal{M},\mathcal{A},\mathcal{G}\rangle$ be a
derivation tree leaf that is saturated with respect to $\mathcal{R}_{1}$.
There is a model $\mathfrak{S}$ of ${\mathfrak{T}_{S}}$ that satisfies the
constraints $\mathcal{S}$ and $\mathcal{M}$ and has the following properties.

  1. (1)

For all
$x,y\in\operatorname{Vars}{(}\mathcal{M})\cup\operatorname{Vars}{(}\mathcal{S})$
of sort $\mathsf{Element}$,
$x^{\mathfrak{S}}=y^{\mathfrak{S}}$ if and only if $x\approx
y\in\mathcal{M}^{*}$.

  2. (2)

For all $S\in\operatorname{Vars}{(}\mathcal{S})$ of sort $\mathsf{Set}$,
$S^{\mathfrak{S}}=\left\\{x^{\mathfrak{S}}\ \middle|\
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}S\in\mathcal{S}^{*}\right\\}$.

  3. (3)

For all $c_{S}\in\operatorname{Vars}{(}\mathcal{S})$ of sort $\mathsf{Card}$,
$c_{S}^{\mathfrak{S}}=\left|S^{\mathfrak{S}}\right|$.

######  Proof 4.2.

Since the models of ${\mathfrak{T}_{S}}$ are closed under variable
reassignment, we pick an arbitrary model $\mathfrak{S}$ of
${\mathfrak{T}_{S}}$ and show that we can change its interpretation of the
variables of $\mathcal{S}\cup\mathcal{M}$ to satisfy the properties above.

We start by interpreting all variables of $\mathsf{Element}$ sort in
$\mathcal{S}\cup\mathcal{M}$ so that, for all $x$ and $y$ in
$\operatorname{Vars}{(}\mathcal{M})\cup\operatorname{Vars}{(}\mathcal{S})$ of
$\mathsf{Element}$ sort,

$x^{\mathfrak{S}}=y^{\mathfrak{S}}\text{ if and only }x\approx
y\in\mathcal{M}^{*}\ \text{.}$

It follows that $\mathfrak{S}$ satisfies $\mathcal{M}$. Next, let
$\mathfrak{S}$ interpret each variable $S$ of $\mathsf{Set}$ sort in
$\operatorname{Vars}{(}\mathcal{S})$ as:

$S^{\mathfrak{S}}=\left\\{x^{\mathfrak{S}}\ \middle|\
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}S\in\mathcal{S}^{*}\right\\}$

and each variable $c_{S}$ of $\mathsf{Card}$ sort in
$\operatorname{Vars}{(}\mathcal{S})$ as:

$c_{S}^{\mathfrak{S}}=\left|S^{\mathfrak{S}}\right|\ \text{.}$

For any set term $s$, define

$\operatorname{Elements}(s)=\left\\{x^{\mathfrak{S}}\ \middle|\
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\in\mathcal{S}^{*}\right\\}\ .$ (4)

Let $\mathcal{T}$ be an arbitrary set of set terms which includes all set
terms in $\mathcal{S}$. Using the assumption that the given state is
saturated, we show by structural induction on set terms that for any set term
$s\in\mathcal{T}$:

$\operatorname{Elements}(s)=s^{\mathfrak{S}}$ (5)

######  Case 1 ($s$ is a variable).

The definition of $\operatorname{Elements}(s)$ is identical to that of
$s^{\mathfrak{S}}$.

######  Case 2 ($s$ is $\emptyset$).

Rule Empty Unsat would apply to the state if there was a constraint of the
form $x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}\emptyset$ in $\mathcal{S}^{*}$.
It follows that $\operatorname{Elements}(\emptyset)=\emptyset$.

######  Case 3 ($s$ is $\left\\{x\right\\}$).

As $s^{\mathfrak{S}}=\left\\{x^{\mathfrak{S}}\right\\}$, it is sufficient to
show that $\operatorname{Elements}(s)=\left\\{x^{\mathfrak{S}}\right\\}$.
Since rule Singleton is not applicable, we can conclude that
$x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\in\mathcal{S}^{*}$. It follows that
$\left\\{x^{\mathfrak{S}}\right\\}\subseteq\operatorname{Elements}(s)$. The
other direction,
$\operatorname{Elements}(s)\subseteq\left\\{x^{\mathfrak{S}}\right\\}$,
follows because of saturation with respect to rule Single Member:

$\displaystyle e\in\operatorname{Elements}(\left\\{x\right\\})$ $\displaystyle
e=y^{\mathfrak{S}}\text{ for some }y\text{ with
}y\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}\left\\{x\right\\}\in\mathcal{S}^{*}$
(definition) $\displaystyle y\approx x\in\mathcal{M}^{*}$ Rule Single Member
$\displaystyle y^{\mathfrak{S}}=x^{\mathfrak{S}}$ ($\mathfrak{S}$ satisfies
$\mathcal{M}$) $\displaystyle e\in\left\\{x^{\mathfrak{S}}\right\\}$
($e=y^{\mathfrak{S}}$)

######  Case 4 ($s$ is $t\sqcap u$).

We need to show $\operatorname{Elements}(t\sqcap u)=t^{\mathfrak{S}}\cap
u^{\mathfrak{S}}$. The proof of the left-to-right inclusion depends on rule
Inter Down I:

$\displaystyle e\in\operatorname{Elements}(t\sqcap u)$ $\displaystyle
e=x^{\mathfrak{S}}\text{ for some }x\text{ with
}x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\sqcap u\in\mathcal{S}^{*}$
(definition) $\displaystyle
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathcal{S}^{*}\text{ and
}x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}$ (Rule Inter Down
I) $\displaystyle x^{\mathfrak{S}}\in\operatorname{Elements}(t)\text{ and
}x^{\mathfrak{S}}\in\operatorname{Elements}(u)$ (definition) $\displaystyle
x^{\mathfrak{S}}\in t^{\mathfrak{S}}\text{ and }x^{\mathfrak{S}}\in
u^{\mathfrak{S}}$ (induction) $\displaystyle e\in t^{\mathfrak{S}}\cap
u^{\mathfrak{S}}$

For the other direction, $t^{\mathfrak{S}}\cap
u^{\mathfrak{S}}\subseteq\operatorname{Elements}(t\sqcap u)$, we rely on rule
Inter Up I:

$\displaystyle e\in t^{\mathfrak{S}}\cap u^{\mathfrak{S}}$ $\displaystyle e\in
t^{\mathfrak{S}}\text{ and }e\in u^{\mathfrak{S}}$ $\displaystyle
e\in\operatorname{Elements}(t)\text{ and }e\in\operatorname{Elements}(u)$
(induction) $\displaystyle
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathcal{S}^{*}\text{ and
}y\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}\text{ with
}x^{\mathfrak{I}}=y^{\mathfrak{I}}=e$ (definition) $\displaystyle
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathcal{S}^{*}\text{ and
}y\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}\text{ with
}x\approx y\in\mathcal{M}^{*}$ (by construction) $\displaystyle
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathcal{S}^{*}\text{ and
}x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}$ $\displaystyle
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\sqcap u\in\mathcal{S}^{*}$ ($t\sqcap
u\in\mathcal{T}$, Rule Inter Up I) $\displaystyle
e\in\operatorname{Elements}(t\sqcap u)$

######  Case 5 ($s$ is $t\sqcup u$).

First we show that $\operatorname{Elements}(t\sqcup u)\subseteq
t^{\mathfrak{S}}\cap u^{\mathfrak{S}}$:

$\displaystyle e\in\operatorname{Elements}(t\sqcup u)$ $\displaystyle
e=x^{\mathfrak{S}}\text{ for some }x\text{ with
}x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\sqcup u\in\mathcal{S}^{*}$
(definition) $\displaystyle
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathcal{S}^{*}\text{ or
}x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}$ (Rule Union
split) $\displaystyle x^{\mathfrak{S}}\in\operatorname{Elements}(t)\text{ or
}x^{\mathfrak{S}}\in\operatorname{Elements}(u)$ (definition) $\displaystyle
x^{\mathfrak{S}}\in t^{\mathfrak{S}}\text{ or }x^{\mathfrak{S}}\in
u^{\mathfrak{S}}$ (induction) $\displaystyle e\in t^{\mathfrak{S}}\cup
u^{\mathfrak{S}}$

Then we show that $t^{\mathfrak{S}}\cup
u^{\mathfrak{S}}\subseteq\operatorname{Elements}(t\sqcup u)$:

$\displaystyle e\in t^{\mathfrak{S}}\cup u^{\mathfrak{S}}$ $\displaystyle e\in
t^{\mathfrak{S}}\text{ or }e\in u^{\mathfrak{S}}$ $\displaystyle
e\in\operatorname{Elements}(t)\text{ or }e\in\operatorname{Elements}(u)$
(induction) $\displaystyle
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathcal{S}^{*}\text{ or
}x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}\text{ where
}x^{\mathfrak{I}}=e$ (definition) $\displaystyle
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\sqcup u\in\mathcal{S}^{*}$ ($t\sqcup
u\in\mathcal{T}$, Rule Union Up II) $\displaystyle
e\in\operatorname{Elements}(t\sqcap u)$

######  Case 6 ($s$ is $t\setminus u$).

First we show that $\operatorname{Elements}(t\setminus u)\subseteq
t^{\mathfrak{S}}\setminus u^{\mathfrak{S}}$:

$\displaystyle e\in\operatorname{Elements}(t\setminus u)$ $\displaystyle
e=x^{\mathfrak{S}}\text{ for some }x\text{ with
}x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\setminus u\in\mathcal{S}^{*}$
(definition) $\displaystyle
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathcal{S}^{*}\text{ and
}x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}$ (Rule Set
difference Down 1) From
$x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}$ we can
conclude that $x^{\mathfrak{S}}\in\operatorname{Elements}(u)$. In fact, if we
assume otherwise, we have that
$y\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}$ for some $y$
with $x^{\mathfrak{S}}=y^{\mathfrak{S}}$. But then $x\approx
y\in\mathcal{M}^{*}$ which implies that
$x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}$. This, however,
make rules Set Unsat applicable. Then we have: $\displaystyle
x^{\mathfrak{S}}\in\operatorname{Elements}(t)\text{ and
}x^{\mathfrak{S}}\not\in\operatorname{Elements}(u)$ $\displaystyle
x^{\mathfrak{S}}\in t^{\mathfrak{S}}\text{ and }x^{\mathfrak{S}}\not\in
u^{\mathfrak{S}}$ (induction) $\displaystyle e\in t^{\mathfrak{S}}\setminus
u^{\mathfrak{S}}$

We now show that $t^{\mathfrak{S}}\setminus
u^{\mathfrak{S}}\subseteq\operatorname{Elements}(t\setminus u)$:

$\displaystyle e\in t^{\mathfrak{S}}\setminus u^{\mathfrak{S}}$ $\displaystyle
e\in t^{\mathfrak{S}}\text{ and }e\not\in u^{\mathfrak{S}}$ $\displaystyle
e\in\operatorname{Elements}(t)\text{ and }e\not\in\operatorname{Elements}(u)$
(induction) $\displaystyle
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathcal{S}^{*}\text{ and
}x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\not\in\mathcal{S}^{*}\text{ for
some }x\text{ with }x^{\mathfrak{I}}=e$ (definition)

We show by contradiction that
$x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}$. Assume the
otherwise. Since
$x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\not\in\mathcal{S}^{*}$ and
$t\setminus u\in\mathcal{T}$, the premise of rule Set difference split is
satisfied. As we had neither
$x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}$ nor
$x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}$, we get a
contradiction.

$\displaystyle
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathcal{S}^{*}\text{ and
}x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}$ (Rule Set
difference split) $\displaystyle
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\setminus u\in\mathcal{S}^{*}$
($t\setminus u\in\mathcal{T}$, Rule Set difference Up 1) $\displaystyle
e\in\operatorname{Elements}(t\setminus u)$

Having established the property of $\operatorname{Elements}(\cdot)$, showing
that each constraint in $\mathcal{S}$ is satisfied by $\mathfrak{S}$ is
straightforward:

  1. (1)

Let $x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\in\mathcal{S}$. Then,
$x^{\mathfrak{S}}\in\operatorname{Elements}(s)$ by (4) and
$x^{\mathfrak{S}}\in s^{\mathfrak{S}}$ by (5).

  2. (2)

Let $x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\in\mathcal{S}$. We show
$x^{\mathfrak{S}}\not\in s^{\mathfrak{S}}$ by contradiction.

$\displaystyle x^{\mathfrak{S}}\in s^{\mathfrak{S}}$ (assume) $\displaystyle
x^{\mathfrak{S}}\in\operatorname{Elements}(s)$ (proved above) $\displaystyle
x^{\mathfrak{S}}=y^{\mathfrak{S}}\text{ for some }y\text{ with
}y\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\in\mathcal{S}^{*}$ (definition)
$\displaystyle x\approx y\in\mathcal{M}^{*}$
($x^{\mathfrak{S}}=y^{\mathfrak{S}}$ iff $x\approx y\in\mathcal{M}^{*}$)
$\displaystyle x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\in\mathcal{S}^{*}$
(definition of $\mathcal{S}^{*}$) Tableau is closed, contradiction. (Rule Set
Unsat)

  3. (3)

Let $s\approx t\in\mathcal{S}$. From the definition of $\mathcal{S}^{*}$ it
follows that $\operatorname{Elements}(s)=\operatorname{Elements}(t)$. Since
$s^{\mathfrak{S}}=\operatorname{Elements}(s)$ and
$t^{\mathfrak{S}}=\operatorname{Elements}(t)$, it follows that
$s^{\mathfrak{S}}=t^{\mathfrak{S}}$.

  4. (4)

Let $s\not\approx t\in\mathcal{S}$. From rule Set Disequality, it follows that
there exists $x$ such that either
$x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\in\mathcal{S}^{*}$ and
$x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathcal{S}^{*}$, or
$x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\in\mathcal{S}^{*}$ and
$x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathcal{S}^{*}$. It follows that
either $x^{\mathfrak{S}}\in s^{\mathfrak{S}}$ and $x^{\mathfrak{S}}\not\in
t^{\mathfrak{S}}$, or $x^{\mathfrak{S}}\not\in s^{\mathfrak{S}}$ and
$x^{\mathfrak{S}}\in t^{\mathfrak{S}}$. In either case, we can conclude that
$s^{\mathfrak{S}}\neq t^{\mathfrak{S}}$.

  5. (5)

Let $c_{S}\approx\mathsf{card}(S)\in\mathcal{S}$. By definition, both
$c_{S}^{\mathfrak{S}}=\left|S^{\mathfrak{S}}\right|=\mathsf{card}(S)^{\mathfrak{S}}$.

For the next two results, let
$\langle\mathcal{S},\mathcal{M},\mathcal{A},\mathcal{G}\rangle$ be a
derivation tree leaf saturated with respect to rules
$\mathcal{R}_{1}\cup\mathcal{R}_{2}\cup\mathcal{R}_{3}$ in a derivation tree.
The first result is about the effects of the rules in $\mathcal{R}_{2}$. The
second is about the rules in $\mathcal{R}_{3}$.

######  Proposition 5.

For every $s\in V(\mathcal{G})$ the following holds.

  1. (1)

If $s\approx t\in\mathcal{S}$ or $t\approx s\in\mathcal{S}$ for some $t$, then
$\mathcal{L}(s)=\mathcal{L}(t)$.

  2. (2)

If $s=T\sqcup U$, then $\mathcal{L}(T\sqcup
U)=\mathcal{L}(T)\cup\mathcal{L}(U)$.

  3. (3)

If $s=T\sqcap U$, then $\mathcal{L}(T\sqcap
U)=\mathcal{L}(T)\cap\mathcal{L}(U)$.

  4. (4)

If $s=T\setminus U$, then $\mathcal{L}(T\setminus
U)=\mathcal{L}(T)\setminus\mathcal{L}(U)$.

  5. (5)

For all distinct $t,u\in\operatorname{Leaves}{(s)}$,
$\models_{\mathfrak{T}_{S}}t\sqcap u\approx\emptyset$.

  6. (6)

$\left\\{t\approx u\ \middle|\ t\approx
u\in\mathcal{S}^{*}\right\\}\models_{\mathfrak{T}_{S}}s\approx\bigsqcup_{t\in\mathcal{L}(s)}t.$666Technically,
$\bigsqcup_{\ldots}$ is ambiguous. However, since $\sqcup$ is associative in
${\mathfrak{T}_{S}}$, bracketing does not matter in this context.

######  Proof 4.3 (Proof (Proposition 5, property 1)).

Let $s\approx t\in\mathcal{S}$, with $s\in V(\mathcal{G})$ or $t\in
V(\mathcal{G})$. From rule Introduce Eq Right and rule Introduce Eq Left it
follows that both $s\in V(\mathcal{G})$ and $t\in V(\mathcal{G})$. For each of
the Rules Merge Equality I, Merge Equality II, and Merge Equality III; we show
that after the application of the rule, $\mathcal{L}(s)$ and $\mathcal{L}(t)$
are equal.

Consider rule Merge Equality I. Let $L_{s}$ and $L_{t}$ denote
$\mathcal{L}(s)$ and $\mathcal{L}(t)$ respectively before application of the
rule. Let $L^{\prime}_{s}$ and $L^{\prime}_{t}$ denote $\mathcal{L}(s)$ and
$\mathcal{L}(t)$ after application of the rule. For the rule to be applicable
$L_{s}\subsetneq L_{t}$. The rule adds constraints to $\mathcal{S}$ so that
$L^{\prime}_{t}=L_{t}\setminus(L_{t}\setminus L_{s})$. Equivalently,
$L^{\prime}_{t}=L_{t}\cap L_{s}=L_{s}$. Since $L^{\prime}_{s}=L_{s}$, we get
$L^{\prime}_{s}=L_{s}=L^{\prime}_{t}$.

The case for rule Merge Equality II is analogous to rule Merge Equality I.

Consider rule Merge Equality III. Let $L_{s}$ and $L_{t}$ denote
$\mathcal{L}(s)$ and $\mathcal{L}(t)$ respectively before application of the
rule. Let $L^{\prime}_{s}$ and $L^{\prime}_{t}$ denote $\mathcal{L}(s)$ and
$\mathcal{L}(t)$ after application of the rule. Let $n\in L^{\prime}_{s}$.
Note that the $\operatorname{merge}$ operation only adds nodes and vertices.
Thus, $n$ is one of the following:

  * •

$l_{1}\sqcap l_{2}$ with $l_{1}\in L_{s}$ and $l_{2}\in L_{t}$: Since
$(l_{1},l_{1}\sqcap l_{2})$ as well as $(l_{2},l_{1}\sqcap l_{2})$ is an edge,
it follows that $n\in L^{\prime}_{t}$.

  * •

$l_{1}\in L_{s}$. Since nodes in $L_{s}\setminus L_{t}$ have an outgoing edge,
it must be the case that $l_{1}\in L_{s}\cap L_{t}$. It follows that $n\in
L^{\prime}_{t}$.

This shows that $L^{\prime}_{s}\subseteq L^{\prime}_{t}$. The reasoning for
$L^{\prime}_{t}\subseteq L^{\prime}_{s}$ is symmetrical.

As $s\approx t$, $s\in V(\mathcal{G})$, and $t\in V(\mathcal{G})$, the premise
of at least once of the rules (Merge Equality I), (Merge Equality II), and
(Merge Equality III) must be satisfied whenever
$\mathcal{L}(s)\neq\mathcal{L}(t)$. As the branch is saturated,
$\mathcal{L}(s)=\mathcal{L}(t)$ follows.

######  Proof 4.4 (Proof (Proposition 5, properties 2, 3, 4)).

As $\mathcal{D}$ is obtained from a derivation starting with a state with an
empty graph, it is sufficient to show the properties hold for the empty graph,
and that they are preserved each time the graph is modified by one of the
rules.

The properties hold trivially for the empty graph. The interesting cases are
when edges are added to the graph: i) $\operatorname{add}$ of a union,
intersection, or set minus term, and ii) $\operatorname{merge}$ operation.

Observe that when we introduce $T\sqcup U$, $T\sqcap U$, and $T\setminus U$ to
the graph, the following holds:

  * •

$\operatorname{Leaves}{(T)}=\\{T\setminus U,T\sqcap U\\}$,

  * •

$\operatorname{Leaves}{(U)}=\\{T\sqcap U,U\setminus T\\}$,

  * •

$\operatorname{Leaves}{(T\sqcup U)}=\\{T\setminus U,T\sqcap U,U\setminus
T\\}$,

  * •

$\operatorname{Leaves}{(T\sqcap U)}=\\{T\sqcap U\\}$,

  * •

$\operatorname{Leaves}{(T\setminus U)}=\\{T\setminus U\\}$, and

  * •

$\operatorname{Leaves}{(U\setminus T)}=\\{U\setminus T\\}$.

We conclude that:

  * •

$\operatorname{Leaves}{(T\sqcup
U)}=\operatorname{Leaves}{(T)}\cup\operatorname{Leaves}{(U)}$

  * •

$\operatorname{Leaves}{(T\sqcap
U)}=\operatorname{Leaves}{(T)}\cap\operatorname{Leaves}{(U)}$

  * •

$\operatorname{Leaves}{(T\setminus
U)}=\operatorname{Leaves}{(T)}\setminus\operatorname{Leaves}{(U)}$

  * •

$\operatorname{Leaves}{(U\setminus
T)}=\operatorname{Leaves}{(U)}\setminus\operatorname{Leaves}{(T)}$

when an introduce rule is applied. Note that the merge operation only adds
edges from existing leaf nodes, ensuring that the property is maintained by
any application of $\operatorname{merge}$.

$\mathcal{L}(\cdot)$, as defined in (2), can also be defined as:

$\mathcal{L}(n)=\operatorname{Leaves}{(n)}\setminus E$ (6)

where $E=\left\\{n^{\prime}\in V(\mathcal{G})\ \middle|\
n^{\prime}\approx\emptyset\in\mathcal{S}^{*}\right\\}$ does not depend on $n$.
The properties in the proposition about $\mathcal{L}(\cdot)$ follow from the
corresponding property of $\operatorname{Leaves}{(\cdot)}$ just established,
and above formulation of $\mathcal{L}(\cdot)$.

######  Proof 4.5 (Proof (Proposition 5, properties 5,6)).

The properties holds trivially for the empty graph.

Let $\mathcal{G}$ be the graph constraints. Let $s\in V(\mathcal{G})$. Let
$s^{\prime}\approx\emptyset$ be a new constraint such that
$s^{\prime}\in\mathcal{L}(s)$. Then, this modifies $\mathcal{L}(s)$, and we
need to verify the Property 6 still holds. Note that for any structure in
${\mathfrak{T}_{S}}$, if $s^{\prime}$ is interpreted as empty set, the
interpretation of $\bigsqcup_{t\in\mathcal{L}(s)\setminus\\{s^{\prime}\\}}t$
will be same as $\bigsqcup_{t\in\mathcal{L}(s)}t$. Thus, if
$s^{\prime}\in\mathcal{L}(s)$ and

$\models_{\mathfrak{T}_{S}}\left(\bigwedge_{P\in
E}P\right)\Rightarrow\left(s\approx\bigsqcup_{t\in\mathcal{L}(s)}t\right)\quad\text{,}$

then

$\models_{\mathfrak{T}_{S}}\left(s^{\prime}\approx\emptyset\wedge\bigwedge_{P\in
E}P\right)\Rightarrow\left(s\approx\bigsqcup_{t\in\mathcal{L}(s)\setminus\\{s^{\prime}\\}}t\right)\quad\text{.}$

It follows if $s^{\prime}\approx\emptyset$ is added to $\mathcal{S}^{*}$ by a
rule, the property 6 continue to hold. Also note that an equality is not
removed by any rule (if there was such a rule, we would need to check the
property continues to hold when the left side of the implication is weakened).

The only other rules which affect the properties are those which modify the
graph directly, i.e. the $\operatorname{add}$ and $\operatorname{merge}$
operations.

We show that if $\mathcal{G}$ satisfies the properties, then so does
$\operatorname{add}(\mathcal{G},s)$:

  * •

$s$ is $\emptyset$, $S$ or $\left\\{x\right\\}$: trivially, as no edges are
added.

  * •

$s$ is $T\sqcap U$: Note that because of the assumptions on the normal form,
either $T\sqcap U$ already in the graph and $\operatorname{add}$ operation
does not modify the graph, or it will add the nodes $T$, $U$, $T\setminus U$,
$T\sqcap U$, and $U\setminus T$ to the graph, and edges between them. It is
easy to see that the property 5 follows from:

$\displaystyle\models_{\mathfrak{T}_{S}}\left(\left(T\setminus
U\right)\sqcap\left(T\sqcap U\right)\right)\approx\emptyset$
$\displaystyle\models_{\mathfrak{T}_{S}}\left(\left(U\setminus
T\right)\sqcap\left(T\sqcap U\right)\right)\approx\emptyset$

Property 6 follows from:

$\displaystyle\models_{\mathfrak{T}_{S}}T\approx\left(\left(T\setminus
U\right)\sqcup\left(T\sqcap U\right)\right)$
$\displaystyle\models_{\mathfrak{T}_{S}}U\approx\left(\left(U\setminus
T\right)\sqcup\left(T\sqcap U\right)\right)$
$\displaystyle\models_{\mathfrak{T}_{S}}\left(T\sqcap
U\right)\approx\left(T\sqcap U\right)$
$\displaystyle\models_{\mathfrak{T}_{S}}\left(U\setminus
T\right)\approx\left(U\setminus T\right)$
$\displaystyle\models_{\mathfrak{T}_{S}}\left(T\setminus
U\right)\approx\left(T\setminus U\right)$

and reasoning as earlier that any constraint of the form
$s^{\prime}\approx\emptyset$ does not affect the property.

  * •

$s$ is $T\setminus U$ or $U\setminus T$: reasoning same as for $T\sqcap U$.

  * •

$s$ is $T\sqcup U$. If not already present, $T$, $U$, $T\setminus U$, $T\sqcap
U$ are added to the graph as for $T\sqcap U$. In addition,
$\operatorname{add}$ for union also adds $T\sqcup U$, and three edges. The
properties follows from the following tautologies in ${\mathfrak{T}_{S}}$ in
addition to those listed in analysis for $T\sqcap U$:

$\displaystyle\models_{\mathfrak{T}_{S}}\left(\left(T\setminus
U\right)\sqcap\left(\left(U\setminus T\right)\right)\right)\approx\emptyset$
$\displaystyle\models_{\mathfrak{T}_{S}}\left(T\sqcup
U\right)\approx\left(\left(T\setminus U\right)\sqcup\left(T\sqcap
U\right)\sqcup\left(U\setminus T\right)\right)$

Finally, we show that if $\mathcal{G}$ satisfies the properties, then so does
$\operatorname{merge}(\mathcal{G},s,t)$ if $s\in V(\mathcal{G})$, $t\in
V(\mathcal{G})$, $\mathcal{L}(s)\nsubseteq\mathcal{L}(t)$ and
$\mathcal{L}(t)\nsubseteq\mathcal{L}(s)$.

Let $L_{s}$ denote $\mathcal{L}(s)$ in $\mathcal{G}$, and $L^{\prime}_{s}$
denote $\mathcal{L}(s)$ in
$\operatorname{merge}(\mathcal{G},s^{\prime},t^{\prime})$ (likewise for $t$,
$u$ etc.).

In order to show property 5 holds, let $s^{\prime}\in V(\mathcal{G})$,
$t^{\prime}\in L^{\prime}_{s^{\prime}}$ and $u^{\prime}\in
L^{\prime}_{s^{\prime}}$. We need to show:
$\models_{\mathfrak{T}_{S}}t^{\prime}\sqcap u^{\prime}\approx\emptyset$.

  * •

Let $t^{\prime}\in L_{s^{\prime}}$ and $u^{\prime}\in L_{s^{\prime}}$, i.e.
both are also leaf nodes in $\mathcal{G}$. Then, the property for
$\operatorname{merge}(\mathcal{G},s,t)$ follows from that of $\mathcal{G}$.

  * •

Let $t^{\prime}$ be one of the newly introduced leaf nodes and $u^{\prime}\in
L_{s^{\prime}}$ a leaf node in $\mathcal{G}$. Without loss of generality, let
$t^{\prime}$ be $t_{1}\sqcap t_{2}$ with $t_{1}\in L_{s}\setminus L_{t}$ and
$t_{2}\in L_{t}\setminus L_{s}$. For $t^{\prime}$ to be in
$L^{\prime}_{s^{\prime}}$, given the way the edges are added, either $t_{1}\in
L_{s^{\prime}}$ or $t_{2}\in L_{s^{\prime}}$. Thus, we know that either
$\models_{\mathfrak{T}_{S}}t_{1}\sqcap u^{\prime}\approx\emptyset$ or
$\models_{\mathfrak{T}_{S}}t_{2}\sqcap u^{\prime}\approx\emptyset$. In either
case, it follows that $\models_{\mathfrak{T}_{S}}\left(t_{1}\sqcap
t_{2}\right)\sqcap u^{\prime}\approx\emptyset$, i.e.
$\models_{\mathfrak{T}_{S}}t^{\prime}\sqcap u^{\prime}\approx\emptyset$.

  * •

The analysis for the case where both are newly introduced leaf nodes is
similar.

To show property 6 holds, the main observation is that each node no longer a
leaf node, say $s^{\prime}\in L_{s}\setminus L^{\prime}_{s}$, is union of a
new set of leaf nodes in $L^{\prime}_{s}$ (assuming the equalities).

$\displaystyle s^{\prime}$ $\displaystyle\approx s^{\prime}\sqcap s$
($s^{\prime}\in L_{s}$, $s\approx\bigsqcup_{s^{\prime\prime}\in
L_{s}}s^{\prime\prime}$) $\displaystyle\approx s^{\prime}\sqcap t$ ($s\approx
t\in E$) $\displaystyle\approx s^{\prime}\sqcap\left(\bigsqcup_{t^{\prime}\in
L_{t}}t^{\prime}\right)$ ($t\approx\bigsqcup_{t^{\prime}\in L_{t}}t^{\prime}$)
$\displaystyle\approx\bigsqcup_{t^{\prime}\in L_{t}}s^{\prime}\sqcap
t^{\prime}$ (distribute) But by property 5, $s^{\prime}\sqcap
t^{\prime}\approx\emptyset$ for $s^{\prime},t^{\prime}\in L_{s}$. Thus,
$\displaystyle s^{\prime}$ $\displaystyle\approx\bigsqcup_{t^{\prime}\in
L_{t}\setminus L_{s}}s^{\prime}\sqcap t^{\prime}$

Note that $\left\\{s^{\prime}\sqcap t^{\prime}\ \middle|\ t^{\prime}\in
L_{t}\setminus L_{s}\right\\}$ are precisely the nodes in $L^{\prime}_{s}$ to
which edges are added from $s^{\prime}$. The proof for a node in $L_{t}$ but
not in $L^{\prime}_{t}$ is similar.

Since all the new leaf nodes are of the form $s^{\prime}\sqcap t^{\prime}$
with $s^{\prime}\in L_{s}\setminus L_{t}$ and $t^{\prime}\in L_{t}\setminus
L_{s}$, it follows that property 6 holds for
$\operatorname{merge}(\mathcal{G},s,t)$ if it holds for $\mathcal{G}$ assuming
$s\approx t\in E$.

######  Proposition 6.

Let $\langle\mathcal{S},\mathcal{M},\mathcal{A},\mathcal{G}\rangle$ be a state
such that none of the rules in our calculus are applicable. Let $\mathfrak{S}$
be an interpretation defined in Proposition 4 satisfying constraints in
$\mathcal{S}$ and $\mathcal{M}$. To recall, for $x$ and $y$ of
$\mathsf{Element}$ sort,

$x^{\mathfrak{S}}=y^{\mathfrak{S}}\text{ if and only if }x\approx
y\in\mathcal{M}^{*}$

and for $s$ of $\mathsf{Set}$ sort,

$s^{\mathfrak{S}}=\left\\{x^{\mathfrak{S}}\ \middle|\
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\in\mathcal{S}^{*}\right\\}\text{.}$

Let $\mathfrak{A}$ be an interpretation satisfying $\mathcal{A}$. Then, for
all $t\in\mathcal{L}(\mathcal{G})$,

$c_{t}^{\mathfrak{A}}\geq\left|t^{\mathfrak{S}}\right|\text{.}$

######  Proof 4.6.

Let $t\in\mathcal{L}(\mathcal{G})$. First we show that if
$\mathcal{A}\Rightarrow c_{t}\geq\left|t_{\mathcal{S}}\right|$, then the
proposition follows. That is there exists $n\geq\left|t_{\mathcal{S}}\right|$
such that $c_{t}\operatorname{\texttt{>=}\,}n\in\mathcal{A}$. Let
$\operatorname{Elements}(\cdot)$ be as in (4).

$\displaystyle c_{t}^{\mathfrak{A}}$ $\displaystyle\geq n^{\mathfrak{A}}$
($c_{t}\operatorname{\texttt{>=}\,}n\in\mathcal{A}$) $\displaystyle=n$
(constant symbol) $\displaystyle\geq\left|t_{\mathcal{S}}\right|$ (definition)
$\displaystyle=\left|\operatorname{Elements}(t)\right|$
($x^{\mathfrak{S}}=y^{\mathfrak{S}}$ iff $x\approx y\in\mathcal{M}^{*}$)
$\displaystyle=\left|t^{\mathfrak{S}}\right|$ (using (5))

It remains to show that $\mathcal{A}\Rightarrow
c_{t}\geq\left|t_{\mathcal{S}}\right|$. Because of rule Members Arrangement,
either $\mathcal{A}\Rightarrow c_{t}\geq\left|t_{\mathcal{S}}\right|$ or Rule
Members Arrangement is applicable until the premise of rule Propagate Minsize
holds. If Rule Propagate Minsize is applicable,
$c_{t}\operatorname{\texttt{>=}\,}\left|t_{\mathcal{S}}\right|$ must have been
added to $\mathcal{A}$. In either case, $\mathcal{A}\Rightarrow
c_{t}\geq\left|t_{\mathcal{S}}\right|$.

Completeness is a direct consequence of the following result.

######  Proposition 7.

Let $\mathcal{S}_{0},\mathcal{M}_{0},\mathcal{A}_{0}$ be set, element and
cardinality constraints respectively, satisfying Restriction 3. Let
$\mathbf{D}$ be a derivation with respect to rules
$\mathcal{R}_{1}\cup\mathcal{R}_{2}\cup\mathcal{R}_{3}$ from state
$\langle\mathcal{S}_{0},$ $\mathcal{M}_{0},$ $\mathcal{A}_{0},$
$(\emptyset,\emptyset)\rangle$. If $\mathbf{D}$ is finite, and the final
derivation tree, say $\mathcal{D}$, in $\mathbf{D}$ is open and saturated with
respect to the rules $\mathcal{R}_{1}\cup\mathcal{R}_{2}\cup\mathcal{R}_{3}$;
then there exists an interpretation $\mathfrak{I}$ that satisfies
$\mathcal{S}_{0}$, $\mathcal{M}_{0}$ and $\mathcal{A}_{0}$.

######  Proof 4.7.

Proof outline: We build a model of the leaf nodes in the graph by modifying as
needed the model obtained from Proposition 4. We add additional elements to
these sets to make the cardinalities match the model satisfying the
cardinality constraints and the constraints induced by the graph. Propositions
5 and 6 ensure that it is always possible to do so without violating the set
constraints.

As $\mathcal{D}$ is open, there exists a branch that does not end in the state
unsat. Let $\langle\mathcal{S},\mathcal{M},\mathcal{A},\mathcal{G}\rangle$ be
the final state on such a branch.

Let $\mathcal{A}\cup\hat{\mathcal{G}}$ be the cardinality constraints, and the
cardinality constraints induced by the graph. These constraints fall in the
theory ${\mathfrak{T}_{A}}$. Let $\mathfrak{A}$ be the structure satisfying
these constraints. Such a structure exists because rule Arithmetic
contradiction would have closed the branch if the constraints were
inconsistent. From Proposition 4, we obtain a structure $\mathfrak{S}$
satisfying $\mathcal{S}$ and $\mathcal{M}$. Without loss of generality, assume
that $\mathsf{Element}^{\mathfrak{S}}$ is infinite.

The $\mathfrak{I}$ we build satisfying
$\mathcal{S}_{0}\cup\mathcal{M}_{0}\cup\mathcal{A}_{0}$ will be as follows. It
coincides with the structure $\mathfrak{S}$ on terms of $\mathsf{Element}$
sort. It coincides with the structure $\mathfrak{A}$ on terms of
$\mathsf{Card}$ sort. In order to define the value of set variables, for each
leaf node $t\in\operatorname{Leaves}{(\mathcal{G})}$ we create the following
sets:

$B_{t}=\\{e_{t,1},e_{t,2}\ldots
e_{t,c_{t}^{\mathfrak{I}}-\left|t^{\mathfrak{S}}\right|}\\}$

where $e_{t,i}\in\mathsf{Element}^{\mathfrak{S}}$ are distinct from each other
and from any $e$ such that $e=x^{\mathfrak{S}}$ for $x$ in $\mathcal{S}$ or
$\mathcal{M}$. From Proposition 6, we know that
$c_{t}^{\mathfrak{I}}\geq\left|t^{\mathfrak{S}}\right|$. Thus, for a leaf node
$t$,

$\left|t^{\mathfrak{S}}\right|+\left|B_{t}\right|=c_{t}^{\mathfrak{I}}\text{.}$
(7)

For a set variable not in the graph, $S\not\in V(\mathcal{G})$, define
$S^{\mathfrak{I}}=S^{\mathfrak{S}}$. For a set variable in the graph, $S\in
V(\mathcal{G})$, define:

$S^{\mathfrak{I}}=\bigcup_{t\in\mathcal{L}(S)}(t^{\mathfrak{S}}\cup B_{t})$
(8)

From Proposition 5, it follows that:

$\bigcup_{t\in\mathcal{L}(S)}t^{\mathfrak{S}}=S^{\mathfrak{S}}$ (9)

So an equivalent way to define $S^{\mathfrak{I}}$ is as follows:

$S^{\mathfrak{I}}=S^{\mathfrak{S}}\cup\bigcup_{t\in\mathcal{L}(S)}B_{t}$ (10)

We verify that each constraint in $\mathcal{S}_{0}$ is satisfied:

  1. (1)

$S\approx T$, $S\not\approx T$.

For $S\approx T$, we need to show $S^{\mathfrak{I}}=T^{\mathfrak{I}}$. If
neither $S\in V(\mathcal{G})$ nor $T\in V(\mathcal{G})$, then this follows
from Proposition 4. If either $S\in V(\mathcal{G})$ or $T\in V(\mathcal{G})$,
then due to rule Introduce Eq Right and rule Introduce Eq Left both $S\in
V(\mathcal{G})$ and $T\in V(\mathcal{G})$. From Proposition 5, property 1, we
know that $\mathcal{L}(S)=\mathcal{L}(T)$. From the definition of
$S^{\mathfrak{I}}$ and $T^{\mathfrak{I}}$ in (8), it follows that
$S^{\mathfrak{I}}=T^{\mathfrak{I}}$.

For $S\not\approx T$, we need to show $S^{\mathfrak{I}}\neq T^{\mathfrak{I}}$.
Let us write $S^{\mathfrak{I}}=S^{\mathfrak{S}}\cup B_{S}$, where
$B_{S}=\emptyset$ if $S\not\in V(\mathcal{G})$, otherwise let
$B_{S}=\bigcup_{t\in\mathcal{L}(S)}B_{t}$ (from (10)). Similarly we may write
$T^{\mathfrak{I}}=T^{\mathfrak{S}}\cup B_{T}$. From Proposition 4 we know that
$S^{\mathfrak{S}}\neq T^{\mathfrak{S}}$. Without loss of generality assume
$e\in S^{\mathfrak{S}}$ and $e\not\in T^{\mathfrak{S}}$. By definition,
$B_{T}$ is disjoint from $S^{\mathfrak{S}}$, thus $e\not\in B_{T}$. Thus,
$e\in S^{\mathfrak{I}}$ and $e\not\in T^{\mathfrak{I}}$. $S^{\mathfrak{I}}\neq
T^{\mathfrak{I}}$ follows.

  2. (2)

$S\approx\emptyset$.

We need to show $S^{\mathfrak{I}}=\emptyset^{\mathfrak{I}}=\emptyset$. It will
follow from rule Introduce Empty Set and rule Introduce Eq Left.

$\displaystyle\emptyset\in V(\mathcal{G})\text{ and }S\in V(\mathcal{G})$
(Rules Introduce Empty Set, Introduce Eq Left)
$\displaystyle\mathcal{L}(S)=\mathcal{L}(\emptyset)$ (Proposition 5, property
1) $\displaystyle\mathcal{L}(S)=\emptyset$
($\mathcal{L}(\emptyset)=\emptyset$) $\displaystyle
S^{\mathfrak{I}}=\emptyset$ ($S\in V(\mathcal{G})$, (8))

  3. (3)

$S\approx\left\\{x\right\\}$.

We need to show that $S^{\mathfrak{I}}=\left\\{x^{\mathfrak{I}}\right\\}$.
From rule Introduce Singleton we conclude that $\left\\{x\right\\}\in
V(\mathcal{G})$ Then, from rule Introduce Eq Left, $S\in V(\mathcal{G})$.

From $\hat{\mathcal{G}}$, we know that:

$\displaystyle c_{S}^{\mathfrak{I}}$
$\displaystyle=\sum_{t\in\mathcal{L}(S)}c_{t}^{\mathfrak{I}}$ (constraint in
$\hat{\mathcal{G}}$ for $c_{S}$)
$\displaystyle=\sum_{t\in\mathcal{L}(\left\\{x\right\\})}c_{t}^{\mathfrak{I}}$
(Proposition 5, property 1)
$\displaystyle=c_{\left\\{x\right\\}}^{\mathfrak{I}}$ (constraint in
$\hat{\mathcal{G}}$ for $c_{\left\\{x\right\\}}$) $\displaystyle=1$
(constraint in $\hat{\mathcal{G}}$ for singletons)

We can conclude that $\left|S^{\mathfrak{I}}\right|=1$ as
$\left|S^{\mathfrak{I}}\right|=c^{\mathfrak{I}}_{S}$ (for proof of
$\left|S^{\mathfrak{I}}\right|=c^{\mathfrak{I}}_{S}$, see reasoning later in
this proof for $\left|S\right|\approx c_{S}$ – the same reasoning works for
all nodes $S\in V(\mathcal{G})$)

From, Singleton, we know $x^{\mathfrak{S}}\in S^{\mathfrak{S}}$. By
Proposition 4, $x^{\mathfrak{S}}\in S^{\mathfrak{S}}$. As

$S^{\mathfrak{I}}=S^{\mathfrak{S}}\cup\bigcup_{t\in\mathcal{L}(S)}B_{t}$

and $\left|S^{\mathfrak{I}}\right|=1$, we conclude that
$S^{\mathfrak{I}}=\left\\{x^{\mathfrak{S}}\right\\}=\left\\{x^{\mathfrak{I}}\right\\}$.

  4. (4)

$S\approx T\sqcup U$. We need to show $S^{\mathfrak{I}}=T^{\mathfrak{I}}\cup
U^{\mathfrak{I}}$.

Let $S\not\in V(\mathcal{G})$, $T\not\in V(\mathcal{G})$, and $U\not\in
V(\mathcal{G})$. Then,

$\displaystyle S^{\mathfrak{I}}$ $\displaystyle=S^{\mathfrak{S}}$ ($S\not\in
V(\mathcal{G})$) $\displaystyle=T^{\mathfrak{S}}\cup U^{\mathfrak{S}}$
(Proposition 4) $\displaystyle=T^{\mathfrak{I}}\cup U^{\mathfrak{I}}$
($T\not\in V(\mathcal{G})$, $U\not\in V(\mathcal{G})$)

Otherwise, let $S\in V(\mathcal{G})$, or $T\in V(\mathcal{G})$, or $U\in
V(\mathcal{G})$. Then, from Rules Introduce Eq Right, Introduce Eq Left,
Introduce Union and definition of $\operatorname{add}$, we know $S$, $T$,
_and_ $U$ in $V(\mathcal{G})$. Then,

$\displaystyle S^{\mathfrak{I}}$
$\displaystyle=\bigcup_{t\in\mathcal{L}(S)}(t^{\mathfrak{S}}\cup B_{t})$
($S\in V(\mathcal{G})$) $\displaystyle=\bigcup_{t\in\mathcal{L}(T\sqcup
U)}(t^{\mathfrak{S}}\cup B_{t})$ (Proposition 5)
$\displaystyle=\left(\bigcup_{t\in\mathcal{L}(T)}(t^{\mathfrak{S}}\cup
B_{t})\right)\cup\left(\bigcup_{t\in\mathcal{L}(U)}(t^{\mathfrak{S}}\cup
B_{t})\right)$ (Proposition 5) $\displaystyle=T^{\mathfrak{I}}\cup
U^{\mathfrak{I}}$ ($T\in V(\mathcal{G})$, $U\in V(\mathcal{G})$)

  5. (5)

$S\approx T\sqcap U$. We need to show $S^{\mathfrak{I}}=T^{\mathfrak{I}}\cap
U^{\mathfrak{I}}$.

Let $S\not\in V(\mathcal{G})$, $T\not\in V(\mathcal{G})$, and $U\not\in
V(\mathcal{G})$. Then,

$\displaystyle S^{\mathfrak{I}}$ $\displaystyle=S^{\mathfrak{S}}$ ($S\not\in
V(\mathcal{G})$) $\displaystyle=T^{\mathfrak{S}}\cap U^{\mathfrak{S}}$
(Proposition 4) $\displaystyle=T^{\mathfrak{I}}\cap U^{\mathfrak{I}}$
($T\not\in V(\mathcal{G})$, $U\not\in V(\mathcal{G})$)

Let $S\not\in V(\mathcal{G})$ and $T\not\in V(\mathcal{G})$, but $U\in
V(\mathcal{G})$. Then,

$\displaystyle T^{\mathfrak{I}}\cap U^{\mathfrak{I}}$
$\displaystyle=T^{\mathfrak{S}}\cap U^{\mathfrak{I}}$ ($T\not\in
V(\mathcal{G})$)
$\displaystyle=T^{\mathfrak{S}}\cap\left(U^{\mathfrak{S}}\cup\bigcup_{t\in\mathcal{L}(U)}B_{t}\right)$
($U\in V(\mathcal{G})$) $\displaystyle=T^{\mathfrak{S}}\cap U^{\mathfrak{S}}$
($T^{\mathfrak{S}}\cap B_{t}=\emptyset$) $\displaystyle=S^{\mathfrak{S}}$
(Proposition 4) $\displaystyle=S^{\mathfrak{I}}$ ($S\not\in V(\mathcal{G})$)

If $S\not\in V(\mathcal{G})$ and $U\not\in V(\mathcal{G})$, but $T\in
V(\mathcal{G})$; the reasoning is same as above.

Otherwise, either $S\in V(\mathcal{G})$ or both $T\in V(\mathcal{G})$ and
$U\in V(\mathcal{G})$. Then, from Rules Introduce Eq Right, Introduce Eq Left,
Introduce Inter and definition of $\operatorname{add}$, we know $S$, $T$,
_and_ $U$ in $V(\mathcal{G})$. Then,

$\displaystyle T^{\mathfrak{I}}\cap U^{\mathfrak{I}}$
$\displaystyle=\left(T^{\mathfrak{S}}\cup\bigcup_{t\in\mathcal{L}(T)}B_{t}\right)\cap\left(U^{\mathfrak{S}}\cup\bigcup_{t\in\mathcal{L}(U)}B_{t}\right)$
($T$, $U$ in $V(\mathcal{G})$) As each $B_{t}$ is disjoint from all other
sets, the above expression simplifies to:
$\displaystyle=\left(T^{\mathfrak{S}}\cap
U^{\mathfrak{S}}\right)\cup\bigcup_{t\in\mathcal{L}(T)\cap\mathcal{L}(U)}B_{t}$
$\displaystyle=S^{\mathfrak{S}}\cup\bigcup_{t\in\mathcal{L}(S)}B_{t}$
(Propositions 4 and 5) $\displaystyle=S^{\mathfrak{I}}$ ($S\in
V(\mathcal{G})$)

  6. (6)

$S\approx T\setminus U$. We need to show
$S^{\mathfrak{I}}=T^{\mathfrak{I}}\setminus U^{\mathfrak{I}}$.

Let $S\not\in V(\mathcal{G})$, $T\not\in V(\mathcal{G})$, and $U\not\in
V(\mathcal{G})$. Then,

$\displaystyle S^{\mathfrak{I}}$ $\displaystyle=S^{\mathfrak{S}}$ ($S\not\in
V(\mathcal{G})$) $\displaystyle=T^{\mathfrak{S}}\setminus U^{\mathfrak{S}}$
(Proposition 4) $\displaystyle=T^{\mathfrak{I}}\setminus U^{\mathfrak{I}}$
($T\not\in V(\mathcal{G})$, $U\not\in V(\mathcal{G})$)

Let $S\not\in V(\mathcal{G})$ and $T\not\in V(\mathcal{G})$, but $U\in
V(\mathcal{G})$. Then,

$\displaystyle T^{\mathfrak{I}}\setminus U^{\mathfrak{I}}$
$\displaystyle=T^{\mathfrak{S}}\setminus U^{\mathfrak{I}}$ ($T\not\in
V(\mathcal{G})$)
$\displaystyle=T^{\mathfrak{S}}\setminus\left(U^{\mathfrak{S}}\cup\bigcup_{t\in\mathcal{L}(U)}B_{t}\right)$
($U\in V(\mathcal{G})$) $\displaystyle=T^{\mathfrak{S}}\setminus
U^{\mathfrak{S}}$ ($T^{\mathfrak{S}}\setminus B_{t}=T^{\mathfrak{S}}$)
$\displaystyle=S^{\mathfrak{S}}$ (Proposition 4)
$\displaystyle=S^{\mathfrak{I}}$ ($S\not\in V(\mathcal{G})$)

Note that in contrast to intersection, if $S\not\in V(\mathcal{G})$, $T\in
V(\mathcal{G})$, and $U\not\in V(\mathcal{G})$, the above analysis does not
apply. We do need to introduce and reason about the equality in the graph.

Let $S\in V(\mathcal{G})$ or $T\in V(\mathcal{G})$. From Rules Introduce Eq
Right, Introduce Eq Left, Introduce Set difference and definition of
$\operatorname{add}$ we know $S$, $T$, _and_ $U$ in $V(\mathcal{G})$. Then,

$\displaystyle T^{\mathfrak{I}}\setminus U^{\mathfrak{I}}$
$\displaystyle=\left(T^{\mathfrak{S}}\cup\bigcup_{t\in\mathcal{L}(T)}B_{t}\right)\setminus\left(U^{\mathfrak{S}}\cup\bigcup_{t\in\mathcal{L}(U)}B_{t}\right)$
($T$, $U$ in $V(\mathcal{G})$) As each $B_{t}$ is disjoint from all other
sets, the above expression simplifies to:
$\displaystyle=\left(T^{\mathfrak{S}}\setminus
U^{\mathfrak{S}}\right)\cup\bigcup_{t\in\mathcal{L}(T)\setminus\mathcal{L}(U)}B_{t}$
$\displaystyle=S^{\mathfrak{S}}\cup\bigcup_{t\in\mathcal{L}(S)}B_{t}$
(Propositions 4 and 5) $\displaystyle=S^{\mathfrak{I}}$ ($S\not\in
V(\mathcal{G})$)

  7. (7)

$x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}S$,
$x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}S$.

Note that irrespective of whether $S\in V(\mathcal{G})$ or $S\not\in
V(\mathcal{G})$, $S^{\mathfrak{S}}\subseteq S^{\mathfrak{I}}$. Thus, from
Proposition 4, $x^{\mathfrak{I}}\in S^{\mathfrak{I}}$ if
$x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}S$ is a constraint.

It remains to show that if $x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}S$ is
a constraint then $x^{\mathfrak{I}}\not\in S^{\mathfrak{I}}$. If $S\not\in
V(\mathcal{G})$, then again $x^{\mathfrak{I}}\not\in S^{\mathfrak{I}}$ follows
from Proposition 4. If $S\in V(\mathcal{G})$, then observe that
$S^{\mathfrak{I}}$ is $S^{\mathfrak{S}}\cup\bigcup_{t\in\mathcal{L}(U)}B_{t}$.
We already know $x^{\mathfrak{I}}\not\in S^{\mathfrak{S}}$. It remains to show
that $x^{\mathfrak{I}}\not\in\bigcup_{t\in\mathcal{L}(U)}B_{t}$. This follows
from the definition of $B_{t}$.

  8. (8)

$c_{S}\approx\mathsf{card}(S)$.

From Proposition 5, we know that for $t,u$ in $\mathcal{L}(S)$:

$\models_{\mathfrak{T}_{S}}t\sqcap u\approx\emptyset$

and also,

$\models_{\mathfrak{T}_{S}}\left(\bigwedge_{t\in
E}t\approx\emptyset\right)\Rightarrow\left(S\approx\bigsqcup_{t\in\mathcal{L}(S)}t\right)$

where $E=\left\\{t\in V(\mathcal{G})\ \middle|\
t\approx\emptyset\in\mathcal{S}^{*}\right\\}$.

In $\mathfrak{I}$, as for each $t\in E$, $t^{\mathfrak{I}}=\emptyset$, it
follows that:

$S^{\mathfrak{I}}=\bigcup_{t\in\mathcal{L}(S)}t^{\mathfrak{I}}\text{\quad.}$

Also, for $t,u$ in $\mathcal{L}(S)$:

$t^{\mathfrak{I}}\cap u^{\mathfrak{I}}=\emptyset\text{\quad.}$

In other words, $S^{\mathfrak{I}}$ is a disjoint union of $t^{\mathfrak{I}}$
where $t\in\mathcal{L}(S)$. It follows that,

$\left|S^{\mathfrak{I}}\right|=\sum_{t\in\mathcal{L}(S)}\left|t^{\mathfrak{I}}\right|$

For a leaf node $t\in\mathcal{L}(S)$, from (7) we know that
$\left|t^{\mathfrak{I}}\right|=\left|t^{\mathfrak{S}}\right|+\left|B_{t}\right|=c_{t}^{\mathfrak{I}}$.
We may thus conclude,

$\left|S^{\mathfrak{I}}\right|=\sum_{t\in\mathcal{L}(S)}c_{t}^{\mathfrak{I}}$

From the constraint on cardinality for $S$ induced by the graph, i.e the
constraint on $c_{S}$ in $\hat{\mathcal{G}}$, we know that
$c_{S}^{\mathfrak{I}}=\sum_{t\in\mathcal{L}(S)}c_{t}^{\mathfrak{I}}$. The
result follows:

$\left|S^{\mathfrak{I}}\right|=c_{S}^{\mathfrak{I}}$

######  Proposition 8 (Completeness).

Under any fair derivation strategy, every derivation of a set $\mathcal{C}$ of
${\mathfrak{T}_{S}}$-unsatisfiable constraints extends to a refutation.

######  Proof 4.8.

Contrapositively, suppose that $\mathcal{C}$ has a derivation $\mathbf{D}$
that cannot be extended to a refutation. By Proposition 2, $\mathbf{D}$ must
be extensible to one that ends with a tree with a saturated branch. By
Proposition 7, $\mathcal{C}$ is satisfiable in ${\mathfrak{T}_{S}}$.

###  4.3. Soundness

We start by showing that every rule preserves constraint satisfiability.

######  Lemma 9.

For every rule of the calculus, the premise state is satisfied by a model
$\mathfrak{I}_{p}$ of ${\mathfrak{T}_{S}}$ iff one of its conclusion
configurations is satisfied by a model $\mathfrak{I}_{c}$ of
${\mathfrak{T}_{S}}$ where $\mathfrak{I}_{p}$ and $\mathfrak{I}_{c}$ agree on
the variables shared by the two states.

######  Proof 4.9 (Sketch).

Soundness of the rules in Figure 2 and Figure 3 follows trivially from the
semantics of set operators and the definition of $\mathcal{S}^{*}$. Soundness
of Merge Equality I follows from properties of the graph (see Proposition 5,
in particular the property that leaf terms are disjoint). The rules in Figure
6 and rule Merge Equality II do not modify the constraints, but we need them
to establish properties of the graph. Soundness of the induced graph
constraints in Arithmetic contradiction follows from Proposition 5 (in
particular properties 5 and 6). Soundness of Propagate Minsize follows from
the semantics of cardinality. Soundness of Guess Empty Set, Members
Arrangement and Guess Lower Bound is trivial.

######  Proposition 10 (Soundness).

Every set of ${\mathfrak{T}_{S}}$-constraints that has a refutation is
${\mathfrak{T}_{S}}$-unsatisfiable.

######  Proof 4.10 (Sketch).

Given Lemma 9, one can show by structural induction on derivation trees that
the root of any closed derivation tree is ${\mathfrak{T}_{S}}$-unsatisfiable.
The claim then follows from the fact that every refutation of a set
$\mathcal{C}$ of ${\mathfrak{T}_{S}}$-constraints starts with a state
${\mathfrak{T}_{S}}$-equisatisfiable with $\mathcal{C}$.

##  5\. Evaluation

We have implemented a decision procedure based on the calculus above in the
SMT solver cvc4 [BCD+11]. We describe a high-level, non-deterministic version
of it here, followed by an experimental evaluation on benchmarks from program
analysis.

###  5.1. Derivation strategy

The decision procedure can be thought of as a specific strategy for applying
the rules given in Section 3, divided into the sets $\mathcal{R}_{1}$, …,
$\mathcal{R}_{4}$ introduced in Section 4.

Our derivation strategy can be summarized as follows. We start the derivation
from the initial state
$\langle\mathcal{S}_{0},\mathcal{M}_{0},\mathcal{A}_{0},\mathcal{G}_{0}\rangle$
with $\mathcal{G}_{0}$ the empty graph, as described in Section 3, and apply
the steps listed below, in the given order. The steps are described as rules
being applied to a _current_ branch of the derivation tree being constructed.
Initially, the current branch is the only branch in the tree. On application
of a rule with more than one conclusion, we select one of the branches (say,
the left branch) as the current branch.

  1. (1)

If a rule that derives unsat is applicable to the current branch, we apply one
and close the branch. We then pick another open branch as the current branch
and repeat Step 1. If no open branch exists, we stop and output unsat.

  2. (2)

If a _propagation_ rule (those with one conclusion) in $\mathcal{R}_{1}$ is
applicable, apply one and go to Step 1.

  3. (3)

If a _split_ rule (those with more than one conclusion) in $\mathcal{R}_{1}$
is applicable, apply one and go to Step 1.

  4. (4)

If Guess Empty Set rule is applicable, apply it and go to Step 1.

  5. (5)

If an introduce or merge rule in $\mathcal{R}_{2}$ is applicable, apply it and
go to Step 1.

  6. (6)

If any of the remaining rules are applicable, apply one and go to Step 1.

  7. (7)

At this point, the current branch is saturated. Stop and output sat.

Note that if there are no constraints involving the cardinality operator, then
steps 1 to 3 above are sufficient for completeness.

Table 1. Performance of our calculus on benchmarks derived from verification of programs file | output | time (s.) | # vertices | # leaves
---|---|---|---|---
cade07-vc1.smt2 | unsat | 0.00 | 3 | 3
cade07-vc2a.smt2 | unsat | 0.00 | 6 | 3
cade07-vc2b.smt2 | sat | 0.01 | 15 | 5
cade07-vc2.smt2 | unsat | 0.01 | 6 | 3
cade07-vc3a.smt2 | unsat | 0.00 | 6 | 0
cade07-vc3b.smt2 | sat | 0.02 | 15 | 6
cade07-vc3.smt2 | unsat | 0.01 | 6 | 0
cade07-vc4b.smt2 | sat | 0.16 | 44 | 12
cade07-vc4.smt2 | unsat | 0.17 | 51 | 16
cade07-vc5b.smt2 | sat | 0.39 | 63 | 21
cade07-vc5.smt2 | unsat | 0.38 | 77 | 25
cade07-vc6a.smt2 | unsat | 0.02 | 32 | 12
cade07-vc6b.smt2 | sat | 0.04 | 32 | 12
cade07-vc6c.smt2 | sat | 0.06 | 32 | 12
cade07-vc6.smt2 | unsat | 0.32 | 36 | 16
cvc4-card.scala-10.smt2 | 2 sat/2 unsat | 0.10 | 48 | 19
cvc4-card.scala-12.smt2 | 1 sat/3 unsat | 0.03 | 0 | 0
cvc4-card.scala-14.smt2 | 2 sat/2 unsat | 0.09 | 25 | 11
cvc4-card.scala-15.smt2 | 1 sat/3 unsat | 0.01 | 0 | 0
cvc4-card.scala-16.smt2 | 2 sat/4 unsat | 0.26 | 39 | 18
cvc4-card.scala-17.smt2 | 1 sat/3 unsat | 0.02 | 19 | 8
cvc4-card.scala-18.smt2 | 2 sat/2 unsat | 0.10 | 39 | 20
cvc4-card.scala-21.smt2 | 2 sat/2 unsat | 1.69 | 134 | 35
cvc4-card.scala-6.smt2 | 1 sat/4 unsat | 0.02 | 8 | 5
cvc4-card.scala-8.smt2 | 1 sat/3 unsat | 0.06 | 21 | 12

###  5.2. Experimental evaluation

We evaluated our procedure on benchmarks obtained from a software verification
applications. The experiments were run on a machine with 3.40GHz Intel i7 CPU
with a memory limit of 3 GB and timeout of 300 seconds. We used a development
version of cvc4 for this
evaluation.777https://github.com/kbansal/CVC4/tree/37f6117 Benchmarks are
available on the cvc4 website.888http://cvc4.cs.stanford.edu/papers/LMCS-2018/

The first set of benchmarks consists of single query benchmarks obtained from
verifying programs manipulating pointer-based data structures. These were
generated by the Jahob system, and have been used to evaluate earlier work on
decision procedures for finite sets and cardinality [KNR06, KR07, SSK11]. The
results from running cvc4 on these benchmarks are provided in the top half of
Table 1. The output reported by cvc4 is in the second column. The third column
shows the solving time. The fourth and fifth columns give the maximum number
of vertices (# V) and leaves999The # L statistic is updated only when
explicitly computed, so the numbers are approximate. For the same reason, # L
is 0 on certain benchmarks even though # V is not. This is because cvc4 was
able to report unsat before the need for computing the set of leaves arose. (#
L) in the graph at any point during the run of the algorithm. Keeping the
number of leaves low is important to avoid a blowup from the Merge Equality II
rule.

Although we have not rerun the systems described in [KNR06, KR07, SSK11], we
report here the experimental results as stated in the respective
papers.101010One reason we were unable to do a more thorough comparison with
previous work is that those implementations are no longer being maintained.
Since the experiments were run on different machines the comparison is only
indicative, but it does suggest that our solver has comparable performance.

In [KR07], the procedure from [KNR06] is reported to solve 12 of the 15
benchmarks with a timeout of 100 seconds, while the novel procedure in [KR07]
is reported to solve 11 of the 15 benchmarks with the same timeout. The best-
performing previous procedure ([SSK11]) can solve all 15 benchmarks in under a
second.111111 [SSK11] includes a second set of benchmarks, but we were unable
to evaluate our procedure on these, as they were only made available in a non-
standard format and were missing crucial datatype declarations. As another
point of comparison, we tested the procedure from [SSK11] on a benchmark of
the type mentioned in Section 1.1: a single constraint of the form
$x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}A_{1}\sqcup\ldots\sqcup A_{21}$. As
expected, the solver failed (it ran out of memory after 85 seconds). In
contrast, cvc4 solves this problem instantaneously.

Finally, another important difference compared to earlier work is that our
implementation is completely integrated in an actively developed and
maintained solver, cvc4.

To highlight the usefulness of an implementation in a full-featured SMT
solver, we did a second evaluation on a set of incremental (i.e., multiple-
query) benchmarks obtained from the Leon verification system [BKKS13]. These
contain a mix of membership and cardinality constraints combined with
constraints over the theories of datatypes and bitvectors. The results of this
evaluation are shown in the bottom half of Table 1. The output column reports
the number of sat and unsat queries in each benchmark. cvc4 successfully
solves all of the queries in these benchmarks in under one second. To the best
of our knowledge, no other SMT solver can handle this combination of theories.

##  6\. Conclusion

We presented a new decision procedure for deciding finite sets with
cardinality constraints and proved its correctness. A novel feature of the
procedure is that it can reason directly and efficiently about both membership
constraints and cardinality constraints. We have implemented the procedure in
the SMT solver cvc4, and demonstrated the feasibility as well as some
advantages of our approach. We hope this work will enable the use of sets and
cardinality constraints in many new applications that rely on SMT solvers. We
also expect to use it to drive the development of a standard theory of sets
under the SMT-LIB initiative [BFT].

We expect to pursue several directions of future work. We will investigate
relaxing Restriction 3.1 by doing more reasoning modulo equality. We will also
experiment with different strategies to attempt to find the most efficient
ones. We will also look into efficient means of combining sets with other
theories and investigate extensions to relations and relational operators.

## Acknowledgement

The authors wish to acknowledge fruitful discussions with Viktor Kuncak and
Etienne Kneuss and for providing the Leon benchmarks. We thank Philippe Suter
for his help running the algorithm from [SSK11].

## References

  * [AA05] Jean-Raymond Abrial and Jean-Raymond Abrial.  The B-book: assigning programs to meanings.  Cambridge University Press, 2005.
  * [AGP16] Francesco Alberti, Silvio Ghilardi, and Elena Pagani.  Counting constraints in flat array fragments.  In Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, pages 65–81, 2016.
  * [ASM80] Jean-Raymond Abrial, Stephen A. Schuman, and Bertrand Meyer.  Specification language.  In On the Construction of Programs, pages 343–410. Cambridge University Press, 1980.
  * [Ban16] Kshitij Bansal.  Decision Procedures for Finite Sets with Cardinality and Local Theory Extensions.  PhD thesis, New York University, January 2016.
  * [BCD+11] Clark Barrett, Christopher Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli.  CVC4.  In 23rd International Conference on Computer Aided Verification (CAV’11), volume 6806 of Lecture Notes in Computer Science, pages 171–177. Springer, 2011.