Reasoning with Finite Sets and Cardinality Constraints in SMT

TL;DR

This paper introduces a novel, efficient calculus for deciding satisfiability in the theory of finite sets with cardinality constraints, enhancing SMT solver capabilities for reasoning about set properties.

Contribution

It presents a new incremental approach using a graph to track overlapping set regions, improving scalability and efficiency over previous methods.

Findings

The new technique is competitive with existing methods.

It scales better on certain problem classes.

The calculus is suitable for implementation in SMT solvers.

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.

Tables

Table 1. 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

Equations

$${\mathcal{M}}^{\ast }=$$

$${\mathcal{S}}^{\ast }=$$

$$\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\}$$

$$\mathcal{C}◃(l)=\{\begin{array}{ll}\mathcal{C}& \text{if }l\in {\mathcal{C}}^{\ast }\\ \mathcal{C}\cup \{l\}& \text{otherwise}\end{array}$$

$$\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\}.$$

$$\mathsf{card}(T)$$

$$\mathsf{card}(T\bigsqcup U)$$

$$\mathsf{card}(U)$$

$$\mathcal{L}(n)=\left\{n^{\prime }\in \mathrm{Leaves}(n)|n^{\prime }\approx \varnothing \notin {\mathcal{S}}^{\ast }\right\},$$

$$V({\mathcal{G}}^{\prime })$$

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

$$\left\{c_s\approx \sum _{t\in \mathcal{L}(s)}{c}_t|s\in V(\mathcal{G})\right\}$$

$$\left\{c_s\text{>=}0|s\in V(\mathcal{G})\right\}$$

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

$$\left\{c_s\approx 0|s\in V(\mathcal{G}),s=\varnothing \right\}$$

$$\mathcal{S}$$

$$\mathcal{A}$$

$$\left(f_1(\sigma ),\dots ,f_9(\sigma )\right){>}_{\text{lex}}^9\left(f_1({\sigma }^{\prime }),\dots ,f_9({\sigma }^{\prime })\right)$$

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

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

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

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

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

$$e\in \mathrm{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}^{*}$$

$$y\approx x\in {\mathcal{M}}^{\ast }$$

$$y^{\mathfrak{S}}=x^{\mathfrak{S}}$$

$$e\in \left\{x^{\mathfrak{S}}\right\}$$

$$e\in \mathrm{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}^{*}$$

$$\displaystyle x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathcal{S}^{*}\text{ and }x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}$$

$$x^{\mathfrak{S}}\in \mathrm{Elements}(t)\text{ and }{x}^{\mathfrak{S}}\in \mathrm{Elements}(u)$$

$$x^{\mathfrak{S}}\in t^{\mathfrak{S}}\text{ and }{x}^{\mathfrak{S}}\in u^{\mathfrak{S}}$$

$$e\in t^{\mathfrak{S}}\cap u^{\mathfrak{S}}$$

$$e\in t^{\mathfrak{S}}\text{ and }e\in u^{\mathfrak{S}}$$

$$e\in \mathrm{Elements}(t)\text{ and }e\in \mathrm{Elements}(u)$$

$$\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$$

$$\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}^{*}$$

$$\displaystyle x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathcal{S}^{*}\text{ and }x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathcal{S}^{*}$$

Full text

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 \thethm.

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}$.

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$:

[TABLE]

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,

[TABLE]

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.

{exa}

Let

[TABLE]

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.

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$:

[TABLE]

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,

[TABLE]

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})$.

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)$:

[TABLE]

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:

[TABLE] 2. (2)

Each cardinality is non-negative:

[TABLE] 3. (3)

Every singleton set has cardinality $1$:

[TABLE] 4. (4)

The empty set has cardinality [math]:

[TABLE]

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

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$.

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.

{exa}

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

[TABLE]

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.

{defi}

[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

[TABLE]

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,

[TABLE]

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:

[TABLE]

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

[TABLE]

For any set term $s$, define

[TABLE]

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}$:

[TABLE]

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:

[TABLE]

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:

[TABLE]

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

[TABLE]

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

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

[TABLE]

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

[TABLE]

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

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

[TABLE]

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

[TABLE]

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.

[TABLE]

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.

[TABLE] 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:

[TABLE]

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

[TABLE]

then

[TABLE]

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:

[TABLE]

Property 6 follows from:

[TABLE]

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$:

[TABLE]

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

[TABLE]

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,

[TABLE]

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

[TABLE]

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

[TABLE]

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

[TABLE]

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:

[TABLE]

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$,

[TABLE]

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:

[TABLE]

From Proposition 5, it follows that:

[TABLE]

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

[TABLE]

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.

[TABLE] 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:

[TABLE]

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

[TABLE]

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,

[TABLE]

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,

[TABLE] 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,

[TABLE]

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

[TABLE]

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,

[TABLE] 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,

[TABLE]

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

[TABLE]

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,

[TABLE] 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)$:

[TABLE]

and also,

[TABLE]

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:

[TABLE]

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

[TABLE]

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

[TABLE]

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,

[TABLE]

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:

[TABLE]

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.

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].