paper report 11institutetext:  The University of Iowa 22institutetext:
Stanford University

# Verifying SQL Queries
using Theories of Tables and Relations

Mudathir Mohamed 11 Andrew Reynolds 11 Cesare Tinelli 11 Clark Barrett 22

###### Abstract

We present a number of first- and second-order extensions to SMT theories
specifically aimed at representing and analyzing SQL queries with join,
projection, and selection operations. We support reasoning about SQL queries
with either bag or set semantics for database tables. We provide the former
via an extension of a theory of finite bags and the latter via an extension of
the theory of finite relations. Furthermore, we add the ability to reason
about tables with null values by introducing a theory of nullable sorts based
on an extension of the theory of algebraic datatypes. We implemented solvers
for these theories in the SMT solver cvc5 and evaluated them on a set of
benchmarks derived from public sets of SQL equivalence problems.

##  0.1 Introduction

The structured query language (SQL) is the dominant declarative query language
in relational databases. Two queries are equivalent in SQL if and only if they
return the same table for every database instance of the same schema. Query
equivalence problems are undecidable in general [1]. For _conjunctive_
queries, the problem is NP-complete under set semantics [5] and
$\prod_{2}^{p}$-hard under bag semantics [6]. SQL query equivalence problems
have many applications in databases and software development, including query
optimization and sharing sub-queries in cloud databases. There is a financial
incentive to reduce the cost of these subqueries, since cloud databases charge
for data storage, network usage, and computation.

Recently, these problems got some attention from researchers in formal
verification who have developed software tools to prove query equivalence in
some SQL fragments. To our knowledge, the state of the art of these tools is
currently represented by SQLSolver [9] which supports a large subset of SQL,
and SPES, an earlier tool that was used to verify queries from cloud-scale
applications [24].

We present an alternative solution for the analysis of SQL queries based on a
reduction to constraints in a new SMT theory of tables with bag (i.e.,
multiset) semantics. This work includes the definition of the theory and the
development of a specialized subsolver for it within the cvc5 SMT solver. We
have extended a previous theory of finite bags [16] with map and filter
operators which are needed to support SQL select and where clauses,
respectively. We represent table rows as tuples and define tables as bags of
tuples. We also support the product operator over tables. While multiset
semantics captures faithfully the way tables are treated in relational
database management systems, there is a lot of work in the database literature
that is based on set semantics. We provide set semantics as an alternative
encoding based on a theory of finite relations by Meng et al. [17], extended
in this case too to accommodate SQL operations.

An initial experimental comparison of our implementation with SQLSolver and
SPES places it between the two in terms of performance and supported features.
While there are several opportunities for further performance improvements,
our solution has two main advantages with respect to previous work: $(i)$ it
is not limited to SQL equivalence problems, and $(ii)$ it comes fully
integrated in a state-of-the-art SMT solver with a rich set of background
theories. Additionally, it could be further extended to provide support for
SQL queries combining set and bag-set semantics [8]. This opens up the door to
other kinds of SQL query analyses (including, for instance, query containment
and query emptiness problems) over a large set of types for query columns
(various types of numerical values, strings, enumerations, and so on).

#### Specific Contributions

We introduce a theory of finite tables by extending a theory of bags with
support for product, filter and map operators. We also extend a theory of
finite relations with map, filter, and inner join operators. We introduce a
theory of nullable sorts as an extension of a theory of algebraic datatypes.
These new theories enable the encoding in SMT of a large fragment of SQL under
either multiset or set semantics and the automated analysis of problems such
as query equivalence. We extend the cvc5 SMT solver [3] with support for
quantifier-free constraints over any combination of the theories above and
those already defined in cvc5. We discuss an initial experimental evaluation
on query equivalence benchmarks.

Our contribution does not include support for aggregations in SQL yet but we
plan to add that in future work.

###  0.1.1 Related work

A decision procedure for quantifier-free formulas in the theory of bags (QFB),
or multisets, based on a reduction to quantifier-free Presburger arithmetic
(QFPA) first appeared in Zarba [22]. The theory signature did not include
cardinality constraints or difference operators. These are supported in a new
decision procedure by Logozzo et al. [16]. The new decision procedure reduces
QFB to $\text{QFPA}^{\star}$, which extends QFPA with formulas
$\bar{u}\in\\{\bar{x}\;|\;\phi\\}$, where $\phi\in$ QFPA. Then, the
$\text{QFPA}^{\star}$ formula is translated into a QFPA formula, but with the
addition of space overhead [15]. An improved decision procedure which
addresses the space overhead issue by using approximations and interpolation
with a set of Constrained Horn Clauses was provided in Levatich et al. [15].
Our work is closest to Zarba’s [22], with additional support for map and
filter operators. As in that work, we do not support the cardinality operator
yet.111Indirect support for that will be provided in future work through the
support for SQL aggregations.  cvc5 already supports the theory of finite sets
[2] and its extension to finite relations [17]. We add support for the map and
filter operators to cvc5’s theory solver for sets and, by extension, to the
theory solver for relations, proving the decidability of the satisfiability
problem in a restricted fragment of the theory of finite sets. That fragment
is enough to handle the benchmarks considered in our experiments under set
semantics.

any tools have been developed to address the SQL query equivalence problem.
For example [namedAttributes] used Coq to formally prove known equivalences in
the database literature. This approach can help in verifying optimization
algorithms before implementing them by query optimizers. However, it is not
suitable for database administrators/developers, who are not expected to write
Coq proofs manually for their queries. Cosette is an automated tool
specifically written to prove SQL query equivalence [7]. t generates a proof
in Coq or Lean to show equivalence of two queries, or generates a database
instance as a counterexample to their equivalence [7]. To do that, it
translates the two SQL queries into algebraic expressions over an unbounded
semiring, which it then normalizes to a _sum-product_ normal form. Finally, it
searches for an isomorphism between the two normal forms using a custom
decision procedure. If an isomorphism is found, the two queries are declared
equivalent. To show that queries are inequivalent, Cosette translates the SQL
queries into bounded lists and uses an SMT solver to find a counterexample to
the equivalence. Cosette is a significant step forward in checking SQL query
equivalences. However, it has several limitations. For instance, it does not
support null values, intersection, difference, arithmetic operations, or
string operations, which are all common in SQL queries.

EQUITAS [23] and its successor SPES [24] are used to identify shared
subqueries automatically in cloud databases. Both support aggregate queries
and null values. They use symbolic representations to prove query equivalence.
EQUITAS follows set semantics, whereas SPES follows bag semantics for tables.
EQUITAS starts by assigning symbolic tuples for the input tables in the
queries, and then applies specialized algorithms to build two formulas
representing output tuples for the two queries. If the two formulas are
equivalent, then the two queries are classified as such. SPES also uses
symbolic representations for queries. However, it reduces the query
equivalence problem to the existence of an identity map between the tuples
returned by the two queries [24]. In experimental evaluations [24], SPES
proved more queries than EQUITAS and was 3 times as fast. Both tools have the
limitation of only supporting queries with similar structure. They do not
process queries with structurally different abstract syntax trees (e.g.,
queries with different number of joins), or queries that use basic operations
such as difference or intersection. They also do not support concrete tables,
built using the keyword `VALUES`.

SQLSolver, which to our knowledge represents the current state of the art, was
released recently and addresses many of the limitations highlighted above [9].
It follows bag semantics and, similar to Cosette, reduces the input queries to
unbounded semiring expressions. However, it then translates them into formulas
in an extension of $\text{QFPA}^{\star}$ that supports nested, parametrized,
or nonlinear summation. This extension supports projection, product, and
aggregate functions. SQLSolver implements algorithms similar to those in
Levatich et al. [15] to translate these formulas into QFPA. SQLSolver
dominates other tools both in terms of performance and expressiveness of the
supported SQL fragment. However, it lacks the ability to generate
counterexamples for inequivalent queries [9].

We follow a different approach from all the equivalence checkers discussed
above. Our solver, incorporated into cvc5, supports difference and
intersection operations, as well as evaluation on concrete tables. Thanks to
the rich set of background theories provided by cvc5, it also supports
arithmetic and string operations, as well as null values. Finally, our solver
is not restricted to SQL query equivalence, as it supports in general any
quantifier-free statements over SQL queries. As a consequence, it can also be
used for other applications such as, for instance, checking for query
containment or emptiness [21].

###  0.1.2 Formal Preliminaries

We define our theories and our calculi in the context of many-sorted logic
with equality and polymorphic sorts and functions. We assume the reader is
familiar with the following notions from that logic: signature, term, formula,
free variable, interpretation, and satisfiability of a formula in an
interpretation. Let $\Sigma$ be a many-sorted signature. We will denote sort
parameters in polymorphic sorts with $\alpha$ and $\beta$, and denote
monomorphic sorts with $\tau$. We will use $\approx$ as the (infix) logical
symbol for equality — which has polymorphic rank $\alpha\times\alpha$ and is
always interpreted as the identity relation over $\alpha$. We assume all
signatures $\Sigma$ contain the Boolean sort $\mathsf{Bool}$, always
interpreted as the binary set $\\{\mathit{true},\mathit{false}\\}$, and two
Boolean constant symbols, $\top$ and $\bot$, for $\mathit{true}$ and
$\mathit{false}$. Without loss of generality, we assume $\approx$ is the only
predicate symbol in $\Sigma$, as all other predicates can be modeled as
functions with return sort $\mathsf{Bool}$. We will write, e.g., $p(x)$ as
shorthand for $p(x)\approx\top$, where $p(x)$ has sort $\mathsf{Bool}$. We
write $s\not\approx t$ as an abbreviation for $\lnot\,s\approx t$. When
talking about sorts, we will normally say just “sort” to mean monomorphic
sort, and say “polymorphic sort” otherwise.

A $\Sigma$-term is a well-sorted term, all of whose function symbols are from
$\Sigma$. A $\Sigma$-formula is defined analogously. 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 $\mathcal{I}(t)$ the value of $t$ in $\mathcal{I}$. A
theory is a pair $\mathbb{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}$). $\mathbf{I}$ is also referred to as the models of
$\mathbb{T}$. A $\Sigma$-formula $\varphi$ is satisfiable (resp.,
unsatisfiable) in $\mathbb{T}$ if it is satisfied by some (resp., no)
interpretation in $\mathbf{I}$. A set $\Gamma$ of $\Sigma$-formulas entails in
$\mathbb{T}$ a $\Sigma$-formula $\varphi$, written
$\Gamma\models_{\mathbb{T}}\varphi$, if every interpretation in $\mathbf{I}$
that satisfies all formulas in $\Gamma$ satisfies $\varphi$ as well. We write
$\Gamma\models\varphi$ to denote that $\Gamma$ entails $\varphi$ in the class
of all $\Sigma$-interpretations. Two $\Sigma$-formulas are equisatisfiable in
$\mathbb{T}$ if for every interpretation $\mathcal{A}$ of $\mathbb{T}$ that
satisfies one, there is an interpretation of $\mathbb{T}$ that satisfies the
other and differs from $\mathcal{A}$ at most in how it interprets the free
variables not shared by the two formulas.

##  0.2 Theory of Tables

$\begin{array}[]{l}\begin{array}[]{@{}l@{\quad}l@{\quad}l@{\quad}l@{}}\hline\cr\hline\cr\textbf{Symbol}&\textbf{Type}&\textbf{SMT-
LIB syntax}&\textbf{Description}\\\ \hline\cr
n&\mathsf{Int}&\text{n}&\text{All constants }\verb|n|\in\mathbb{N}\\\
+&\mathsf{Int}\times\mathsf{Int}\to\mathsf{Int}&\verb|+|&\text{Integer
addition}\\\
&\mathsf{Int}\times\mathsf{Int}\to\mathsf{Int}&\verb|*|&\text{Integer
multiplication}\\\ -&\mathsf{Int}\to\mathsf{Int}&\verb|-|&\text{Unary Integer
minus}\\\
{\leq}&\mathsf{Int}\times\mathsf{Int}\rightarrow\mathsf{Bool}&\verb|<=|&\text{Integer
inequality}\\\
\hline\cr\varnothing_{\alpha}&\mathsf{Bag}(\alpha)&\verb|bag.empty|&\text{Empty
bag}\\\
\mathsf{bag}&\alpha\times\mathsf{Int}\rightarrow\mathsf{Bag}(\alpha)&\verb|bag|&\text{Bag
constructor}\\\
\mathsf{m}&\alpha\times\mathsf{Bag}(\alpha)\rightarrow\mathsf{Int}&\verb|bag.count|&\text{Multiplicity}\\\
\mathsf{setof}&\mathsf{Bag}(\alpha)\rightarrow\mathsf{Bag}(\alpha)&\verb|bag.setof|&\text{Duplicate
remove }\\\
\sqcup&\mathsf{Bag}(\alpha)\times\mathsf{Bag}(\alpha)\rightarrow\mathsf{Bag}(\alpha)&\verb|bag.union_max|&\text{Max
union}\\\ \mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.26582pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}&\mathsf{Bag}(\alpha)\times\mathsf{Bag}(\alpha)\rightarrow\mathsf{Bag}(\alpha)&\verb|bag.union_disjoint|&\text{Disjoint
union}\\\
\sqcap&\mathsf{Bag}(\alpha)\times\mathsf{Bag}(\alpha)\rightarrow\mathsf{Bag}(\alpha)&\verb|bag.inter_min|&\text{Intersection}\\\
\setminus&\mathsf{Bag}(\alpha)\times\mathsf{Bag}(\alpha)\rightarrow\mathsf{Bag}(\alpha)&\verb|bag.diff_subtract|&\text{Difference
subtract}\\\
\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}&\mathsf{Bag}(\alpha)\times\mathsf{Bag}(\alpha)\rightarrow\mathsf{Bag}(\alpha)&\verb|bag.diff_remove|&\text{Difference
remove}\\\
\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}&\alpha\times\mathsf{Bag}(\alpha)\rightarrow\mathsf{Bool}&\verb|bag.member|&\text{Member
}\\\
\sqsubseteq&\mathsf{Bag}(\alpha)\times\mathsf{Bag}(\alpha)\rightarrow\mathsf{Bool}&\verb|bag.subbag|&\text{Subbag}\\\
\hline\cr\sigma&\left(\alpha\rightarrow\mathsf{Bool}\right)\times\mathsf{Bag}(\alpha)\rightarrow\mathsf{Bag}(\alpha)&\verb|bag.filter|&\text{Bag
filter}\\\
\pi&\left(\alpha_{1}\rightarrow\alpha_{2}\right)\times\mathsf{Bag}(\alpha_{1})\rightarrow\mathsf{Bag}(\alpha_{2})&\verb|bag.map|&\text{Bag
map}\\\
\hline\cr\langle\ldots\rangle&\alpha_{0}\times\dots\times\alpha_{k}\rightarrow\mathsf{Tuple}(\alpha_{0},\ldots,\alpha_{k})&\verb|tuple|&\text{Tuple
constructor}\\\
\mathsf{select}_{i}&\mathsf{Tuple}(\alpha_{0},\ldots,\alpha_{k})\rightarrow\alpha_{i}&\verb|(_
tuple.select i)|&\text{Tuple selector}\\\\[2.41112pt]
\mathsf{tuple.proj}_{i_{1}\ldots
i_{n}}&\mathsf{Tuple}(\alpha_{0},\ldots,\alpha_{k})\rightarrow\mathsf{Tuple}(\alpha_{i_{1}},\ldots,\alpha_{i_{n}})&(\verb|_
tuple.proj |i_{1}\cdots i_{n})&\text{Tuple projection}\\\
\hline\cr\otimes&\mathsf{Table}(\bm{\alpha})\times\mathsf{Table}(\bm{\beta})\rightarrow\mathsf{Table}(\bm{\alpha},\bm{\beta})&\verb|table.product|&\text{Table
cross join}\\\ \bowtie_{i_{1}j_{1}\cdots
i_{p}j_{p}}&\mathsf{Table}(\bm{\alpha})\times\mathsf{Table}(\bm{\beta})\rightarrow\mathsf{Table}(\bm{\alpha},\bm{\beta})&(\verb|_
table.join |i_{1}j_{1}\cdots i_{p}j_{p})&\text{Table inner
join}\\\\[2.41112pt] \mathsf{table.proj}_{i_{1}\ldots
i_{n}}&\mathsf{Table}(\alpha_{0},\ldots,\alpha_{k})\rightarrow\mathsf{Table}(\alpha_{i_{1}},\ldots,\alpha_{i_{n}})&(\verb|_
table.proj |i_{1}\cdots i_{n})&\text{Table projection}\\\
\hline\cr\hline\cr\end{array}\\\\[12.05554pt] \end{array}$

Figure 1:  Signature $\Sigma_{\mathsf{Tab}}$ for the theory of tables. Here
$\mathsf{Table}(\bm{\alpha},\bm{\beta})$ is a shorthand for
$\mathsf{Table}(\alpha_{0},\ldots,\alpha_{p},\beta_{0},\ldots,\beta_{q})$ when
$\bm{\alpha}=\alpha_{0},\ldots,\alpha_{p}$ and
$\bm{\beta}=\beta_{0},\ldots,\beta_{q}$.

We define a many-sorted theory $\mathbb{T}_{\mathsf{Tab}}$ of (database)
tables. Its signature $\Sigma_{\mathsf{Tab}}$ is given in Figure 1. We use
$\alpha$ and $\beta$, possibly with subscripts, as sort parameters in
polymorphic sorts. The theory includes the integer sort $\mathsf{Int}$ and a
number of integer operators, with the same interpretation as in the theory of
arithmetic. Additionally, $\mathbb{T}_{\mathsf{Tab}}$ has three classes of
sorts, with a corresponding polymorphic sort constructor: function sorts,
tuple sorts, and bag sorts. Function sorts are monomorphic instances of
$\alpha_{1}\times\dots\times\alpha_{k}\rightarrow\alpha$ for all $k\geq 0$.
Tuple sorts are constructed by the varyadic constructor $\mathsf{Tuple}$ which
takes zero or more sort arguments. With no arguments, $\mathsf{Tuple}$ denotes
the singleton set containing the empty tuple. With $k+1$ arguments for $k\geq
0$, $\mathsf{Tuple}(\tau_{0},\ldots,\tau_{k})$ denotes the set of tuples of
size $k+1$ with elements of sort $\tau_{0},\ldots,\tau_{k}$, respectively. Bag
sorts are monomorphic instances $\mathsf{Bag}(\tau)$ of
$\mathsf{Bag}(\alpha)$. The sort $\mathsf{Bag}(\tau)$ denotes the set of all
_finite_ bags (i.e., finite multisets) of elements of sort $\tau$. We model
tables as bags of tuples. We write $\mathsf{Table}(\tau_{0},\ldots,\tau_{k})$
as shorthand for the sort
$\mathsf{Bag}(\mathsf{Tuple}(\tau_{0},\ldots,\tau_{k}))$. The sort
$\mathsf{Table}$, with no arguments, abbreviates
$\mathsf{Bag}(\mathsf{Tuple})$.222And so denotes the set of all tables
containing just occurrences of the empty tuple.  Following databases
terminology, we refer to $\tau_{0},\dots,\tau_{k}$ as the columns of
$\mathsf{Table}(\tau_{0},\ldots,\tau_{k})$, and to the elements of a given
table as its rows. For convenience, we index the columns of a table by natural
numbers (starting with 0), instead of alphanumeric names, as in SQL.

The symbols in the first five lines in Figure 1 are from arithmetic and are
interpreted as expected. The next eleven function symbols operate on bags and
are defined as in Logozzo et al. [16]. Specifically, for all sorts $\tau$,
$\varnothing_{\tau}$ is interpreted as the empty bag of elements of sort
$\tau$. The term $\mathsf{bag}(e,n)$ denotes a singleton bag with $n$
occurrences of the bag element $e$ if $n\geq 1$; otherwise; it denotes
$\varnothing_{\tau}$ where $\tau$ is the sort of $e$. The term
$\mathsf{m}(e,s)$ denotes the multiplicity of element $e$ in bag $s$, that is,
the number of times $e$ occurs in $s$. Its codomain is the set of natural
numbers. For convenience, we use $\mathsf{Int}$ as the codomain and, during
reasoning, assert $\mathsf{m}(e,s)\geq 0$ for each multiplicity term. The term
$\mathsf{setof}(s)$ denotes the bag with the same elements as $s$ but without
duplicates. The predicate
$e\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s$ holds
iff element $e$ has positive multiplicity in bag $s$. The predicate
$s\sqsubseteq t$ holds iff bag $s$ is contained in bag $t$ in the sense that
$\mathsf{m}(e,s)\leq\mathsf{m}(e,t)$ for all elements $e$. The binary
operators $\sqcup,\mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle+$}\hfil\cr}},\sqcap,\setminus,\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}$
are interpreted as functions that take two bags $s$ and $t$ and return their
max union, disjoint union, subtract difference, and remove difference,
respectively, making the following equalities valid in
$\mathbb{T}_{\mathsf{Tab}}$:

$\begin{array}[]{rcl@{\qquad}rcl}\mathsf{m}(e,s\sqcup
t)&\approx&\max(\mathsf{m}(e,s),\mathsf{m}(e,t))&\mathsf{m}(e,s\mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}t)&\approx&\mathsf{m}(e,s)+\mathsf{m}(e,t)\\\
\mathsf{m}(e,s\sqcap
t)&\approx&\min(\mathsf{m}(e,s),\mathsf{m}(e,t))&\mathsf{m}(e,s\setminus
t)&\approx&\max(\mathsf{m}(e,s)-\mathsf{m}(e,t),0)\\\
\mathsf{m}(e,s\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}t)&\approx&\mathsf{ite}(\mathsf{m}(e,t)\geq
1,0,\mathsf{m}(e,s))&\end{array}$

The next two symbols in Figure 1 are the filter and map functionals. These
symbols require an SMT solver that supports higher-order logic, which is the
case for cvc5 [4]. The term $\sigma(p,s)$ denotes the bag consisting of the
elements of bag $s$ that satisfy predicate $p$, with the same multiplicity
they have in $s$. The term $\pi(f,s)$ denotes the bag consisting of the
elements $f(e)$, for all $e$ that occur in $s$. The multiplicity of $f(e)$ in
$\sigma(f,s)$ is the sum of the multiplicities (in $s$) of all the elements of
$s$ that $f$ maps to $f(e)$. Note that while $\pi(f,s)$ and $s$ have the same
cardinality, i.e., the same number of element occurrences,
$\mathsf{m}(f(e),\pi(f,s))$ may be greater than $\mathsf{m}(e,s)$ for some
elements $e$ unless $f$ is injective.

The last six symbols denote dependent families of functions over tuples and
tables. The term $\langle e_{1},\dots,e_{k}\rangle$ is interpreted as the
tuple comprised of the elements $e_{1},\dots,e_{k}$, in that order, with
$\langle\rangle$ denoting the empty tuple. For $0\leq i\leq k$ where $k+1$ is
the size of a tuple $t$, $\mathsf{select}_{i}(t)$ is interpreted as the
element at position $i$ of $t$. Note that $i$ in $\mathsf{select}_{i}$ is a
numeral, not a symbolic index. This means in particular that
$\mathsf{select}_{3}(\langle a,b\rangle)$ is an ill-sorted term.
$\mathsf{tuple.proj}$ takes an unbounded number of integer arguments, followed
by a tuple. $\mathsf{tuple.proj}_{i_{1}\ldots i_{n}}$ where $n\geq 1$ and each
$i_{j}$ is an element of $\\{\,0,\ldots,k\,\\}$, applies to any tuple of size
at least $k+1$ and returns the tuple obtained by collecting the values at
position $i_{1},\ldots,i_{n}$ in $t$. In other words, it is equivalent to
$\langle\mathsf{select}_{i_{1}}(t),\ldots,\mathsf{select}_{i_{n}}(t)\rangle$.
Note that $i_{1},\ldots,i_{n}$ are not required to be distinct. When $n=0$,
the term is equivalent to the empty tuple. $\mathsf{table.proj}_{i_{1}\ldots
i_{n}}$ extends the notion of projection to tables. It is similar to
$\mathsf{tuple.proj}$ except that it takes a table instead of a tuple as
argument. Note that the cardinality of $\mathsf{table.proj}_{i_{1}\ldots
i_{n}}(s)$ is the same as the cardinality of $s$. The term $t\otimes
t^{\prime}$ is interpreted as the cross join of tables $t$ and $t^{\prime}$,
with every tuple occurrence in $t$ being concatenated with every tuple
occurrence in $t^{\prime}$. The operator $\bowtie_{i_{1}j_{1}\cdots
i_{n}j_{n}}$ is indexed by $n$ pairs of natural numbers. It takes two tables
as input, each with at least $n$ columns, and outputs the inner join of these
tables on the columns specified by these index pairs. The paired columns have
to be of the same sort. Notice that if $n=0$, the join is equivalent to a
product.

#### Simplifying Assumptions

_To simplify the exposition_ and the description of the calculus, from now on,
we will consider only bags whose elements are not themselves bags, and only
tuples whose elements are neither tuples nor bags. Note that this _non-
nestedness_ restriction applies to tables as well — as they are just bags of
tuples. This is enough in principle to model and reason about SQL
tables.333Commercial databases do allow table elements to be tuples. We could
easily support this capability in the future simply by providing two kinds of
tuple sorts, one for rows and one for table elements.  We stress, however,
that none of these restrictions are necessary in our approach, nor required by
our implementation, where we rely on cvc5’s ability to reason modularly about
arbitrarily nested sorts. Finally, we will not formalize in the calculus how
we process constraints containing table projections (i.e., applications of
$\mathsf{table.proj}$). Such constraints are reduced internally to map
constraints, with mapping functions generated on the fly, and added to the
relevant background solver. For instance, a constraint of the form
$s\approx\mathsf{table.proj}_{2,0}(t)$ where $t$ has sort
$\mathsf{Table}(\tau_{0},\ldots,\tau_{3})$, say, is reduced to the constraint
$s\approx\pi(f,t)$ where $f$ is a function symbol defined internally to be
equivalent to $\lambda e.\,\mathsf{tuple.proj}_{2,0}(e)$.

$\begin{array}[]{rl@{\quad\qquad}rl@{\quad\qquad}rl}\mathsf{m}(e,\varnothing_{\varepsilon})&~{}\longrightarrow~{}0&s\mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}\varnothing_{\varepsilon}&~{}\longrightarrow~{}s\\\
e\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s&~{}\longrightarrow~{}1\leq\mathsf{m}(e,s)&\varnothing_{\varepsilon}\mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}t&~{}\longrightarrow~{}t\\\
\mathsf{bag}(e,-n)&~{}\longrightarrow~{}\varnothing_{\varepsilon}&s\sqsubseteq
t&~{}\longrightarrow~{}(s\setminus t)\approx\varnothing_{\varepsilon}\\\
\end{array}$

Figure 2: Simplification rules for $\Sigma_{\mathsf{Tab}}$-terms. In the last
two rules, $\varepsilon$ is the sort of $e$ and of the elements of $s$,
respectively; $n$ is a numeral.

######  Definition 0.2.1.

A (monomorphic) sort is an element sort if it is not an instance of
$\mathsf{Bag}(\alpha)$. An element term is a term of an element sort. A
tuple/bag/table term is a term of tuple/bag/table sort, respectively. A
$\mathbb{T}_{\mathsf{Tab}}$-atom is an atomic $\Sigma_{\mathsf{Tab}}$-formula
of the form $t_{1}\approx t_{2}$,
$e\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s$, or
$s_{1}\sqsubseteq s_{2}$, where $t_{1}$ and $t_{2}$ are terms of the same
sort, $e$ is a term of some element sort $\tau$ and $s$, $s_{1}$, and $s_{2}$
are terms of sort $\mathsf{Bag}(\tau)$.

A $\Sigma_{\mathsf{Tab}}$-formula $\varphi$ is a table constraint if it has
the form $s\approx t$ or $s\not\approx t$; it is an arithmetic constraint if
it has the form $s\approx t$, $s\not\approx t$, or $s\leq t$, where $s$, $t$
are terms of sort $\mathsf{Int}$; it is an element constraint if it has the
form $e_{1}\approx e_{2},e_{1}\not\approx e_{2},p(e),f(e_{1})\approx e_{2}$,
where $e,e_{1},e_{2}$ are terms of some element sort, $p$ is a function symbol
of sort $\varepsilon\rightarrow\mathsf{Bool}$ for some element sort
$\varepsilon$, and $f$ is a function symbol of sort
$\varepsilon_{1}\rightarrow\varepsilon_{2}$, for some element sorts
$\varepsilon_{1}$ and $\varepsilon_{2}$.

Note that table constraints include (dis)equalities between terms of any sort.
This implies that (dis)equalities between terms of sort $\mathsf{Int}$ are
both table and arithmetic constraints.

###  0.2.1 Calculus

We now describe a tableaux-style calculus with derivation rules designed to
determine the satisfiability in $\mathbb{T}_{\mathsf{Tab}}$ of quantifier-free
$\Sigma_{\mathsf{Tab}}$-formulas $\varphi$. To simplify the description, we
will pretend that all tables have columns of the same element sort, denoted
generically by $\varepsilon$.

Without loss of generality, we assume that the atoms of $\varphi$ are in
reduced form with respect to the (terminating) rewrite system in Figure 2,
which means that $\varphi$ is a Boolean combination of only equality
constraints and arithmetic constraints. Thanks to the following lemma, we will
further focus on just sets of table constraints and arithmetic constraints.444
Proofs of this lemma and later results can be found in a longer version of
this paper [arxiv]. Proofs of this lemma and later results can be found in the
appendix.

######  Lemma 0.2.1.

For every quantifier-free $\Sigma_{\mathsf{Tab}}$-formula $\varphi$, there are
sets $B_{1},\ldots,B_{n}$ of table constraints, sets $A_{1},\ldots,A_{n}$ of
arithmetic constraints, and sets $E_{1},\ldots,E_{n}$ of elements constraints
such that $\varphi$ is satisfiable in $\mathbb{T}_{\mathsf{Tab}}$ iff
$A_{i}\cup B_{i}\cup E_{i}$ is satisfiable in $\mathbb{T}_{\mathsf{Tab}}$ for
some $i\in[1,n]$.

As a final simplification, we can also assume, without loss of generality,
that for every term $t$ of sort $\mathsf{Tuple}(\tau_{0},\ldots,\tau_{k})$
occurring in one of the sets $B_{i}$ above, $B_{i}$ also contains the
constraint $t\approx\langle x_{0},\ldots,x_{k}\rangle$ where
$x_{0},\ldots,x_{k}$ are variables of sort $\tau_{0},\ldots,\tau_{k}$,
respectively.

#### Configurations and Derivation Trees.

The calculus operates on data structures we call _configurations_. These are
either the distinguished configuration $\mathsf{unsat}$ or triples
$(\mathsf{A},\mathsf{B},\mathsf{E})$ consisting of a set $\mathsf{A}$ of
arithmetic constraints, a set $\mathsf{B}$ of table constraints, and a set
$\mathsf{E}$ of element constraints. Our calculus is a set of derivation rules
that apply to configurations.

We assume we have a (possibly multi-theory) element solver that can decide the
satisfiability of constraints in $\mathsf{E}$. This requires the computability
of all predicates $p$ and functions $f$ used as arguments in applications of
filter ($\sigma$) and map ($\pi$), respectively. We also define the set $W$ to
be an infinite set of fresh variables, which will be used in specific
derivation rules.

Derivation rules take a configuration and, if applicable to it, generate one
or more alternative configurations. A derivation rule applies to a
configuration $c$ if all the conditions in the rule’s premises hold for $c$
_and_ the rule application is not redundant. An application of a rule is
redundant if it has a conclusion where each component in the derived
configuration is a subset of the corresponding component in the premise
configuration.

A configuration other than $\mathsf{unsat}$ is saturated with respect to a set
$R$ of derivation rules if every possible application of a rule in $R$ to it
is redundant. It is saturated if it is saturated with respect to all
derivation rules in the calculus. A configuration
$(\mathsf{A},\mathsf{B},\mathsf{E})$ is satisfiable in
$\mathbb{T}_{\mathsf{Tab}}$ if the set
$\mathsf{A}\cup\mathsf{B}\cup\mathsf{E}$ is satisfiable in
$\mathbb{T}_{\mathsf{Tab}}$.

A derivation tree is a (possibly infinite) tree where each node is a
configuration whose (finitely-many) children, if any, are obtained by a non-
redundant application of a rule of the calculus to the node. A derivation tree
is closed if it is finite and all its leaves are $\mathsf{unsat}$. As we show
later, a closed derivation tree with root $(\mathsf{A},\mathsf{B},\mathsf{E})$
is a proof that $\mathsf{A}\cup\mathsf{B}\cup\mathsf{E}$ is unsatisfiable in
$\mathbb{T}_{\mathsf{Tab}}$. In contrast, a derivation tree with root
$(\mathsf{A},\mathsf{B},\mathsf{E})$ and a saturated leaf with respect to all
the rules of the calculus is a witness that
$\mathsf{A}\cup\mathsf{B}\cup\mathsf{E}$ is satisfiable in
$\mathbb{T}_{\mathsf{Tab}}$.

$\mathsf{A}\models_{\mathsf{NIA}}\bot$ A-Conf $\mathsf{unsat}$ $t\not\approx
t\in\mathsf{B}^{*}$ B-Conf $\mathsf{unsat}$
$\mathsf{E}\models_{\mathsf{EL}}\bot$ E-Conf $\mathsf{unsat}$

$s\approx t\in\mathsf{B}^{*}$ $s,t:\mathsf{Int}$ B-A-Prop
$\mathsf{A}:=\mathsf{A},s\approx t$ $e_{1}\approx e_{2}\in\mathsf{B}^{*}$
$e_{1},e_{2}$ are elem. terms B-E-Prop $\mathsf{E}:=\mathsf{E},e_{1}\approx
e_{2}$

$e_{1},e_{2}\in\mathcal{T}(\mathsf{B}^{*})$ $e_{1},e_{2}$ are element terms of
the same sort E-Ident $\mathsf{B}:=\mathsf{B},e_{1}\approx
e_{2}~{}~{}~{}||~{}~{}~{}\mathsf{B}:=\mathsf{B},e_{1}\not\approx e_{2}$

$\mathsf{A}\models_{\mathsf{NIA}}s\approx t$ $s,t\in\mathsf{A}$ $s\text{ or
}t$ is a multiplicity term A-Prop $\mathsf{B}:=\mathsf{B},s\approx t$

$s\not\approx t\in\mathsf{B}^{*}$ $w$ is a fresh variable Diseq
$\mathsf{B}:=\mathsf{B},\mathsf{m}(w,s)\not\approx\mathsf{m}(w,t)\quad\mathsf{A}:=\mathsf{A},\mathsf{m}(w,s)\not\approx\mathsf{m}(w,t)$
$\mathsf{m}(e,s)\in\mathcal{T}(\mathsf{B}^{*})$ Nonneg
$\mathsf{A}:=\mathsf{A},0\leq\mathsf{m}(e,s)$

$s\approx\mathsf{bag}(e,n)\in\mathsf{B}^{*}$ $n\leq 0\notin\mathsf{A}$ $1\leq
n\notin\mathsf{A}$ Cons1 $\begin{array}[]{ll}&\mathsf{A}:=\mathsf{A},n\leq
0,\mathsf{m}(e,s)\approx
0\quad\mathsf{B}:=\mathsf{B},s\approx\varnothing_{\varepsilon}\\\
||&\mathsf{A}:=\mathsf{A},1\leq n,\mathsf{m}(e,s)\approx
n\quad\mathsf{B}:=\mathsf{B},s\not\approx\varnothing_{\varepsilon}\end{array}$

$s\approx\mathsf{bag}(e,n)\in\mathsf{B}^{*}$ $x\not\approx e\in\mathsf{B}^{*}$
Cons2 $\begin{array}[]{l}\mathsf{A}:=\mathsf{A},\mathsf{m}(x,s)\approx
0\end{array}$ $s\approx\varnothing_{\varepsilon}\in\mathsf{B}^{*}$
$\mathsf{m}(e,s)\in\mathcal{T}(\mathsf{B})$ Empty
$\mathsf{A}:=\mathsf{A},\mathsf{m}(e,s)\approx 0$

$s\approx t\mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}u\in\mathsf{B}^{*}$
$\mathsf{m}(e,v)\in\mathcal{T}(\mathsf{B})$ $v\in\\{s,t,u\\}$ Disj Union
$\begin{array}[]{c}\mathsf{A}:=\mathsf{A},\mathsf{m}(e,s)\approx\mathsf{m}(e,t)+\mathsf{m}(e,u)\end{array}$

$s\approx t\sqcup u\in\mathsf{B}^{*}$
$\mathsf{m}(e,v)\in\mathcal{T}(\mathsf{B})$ $v\in\\{s,t,u\\}$ Max Union
$\begin{array}[]{c}\mathsf{A}:=\mathsf{A},\mathsf{m}(e,s)\approx\max(\mathsf{m}(e,t),\mathsf{m}(e,u))\end{array}$

$s\approx t\sqcap u\in\mathsf{B}^{*}$
$\mathsf{m}(e,v)\in\mathcal{T}(\mathsf{B})$ $v\in\\{s,t,u\\}$ Inter
$\begin{array}[]{c}\mathsf{A}:=\mathsf{A},\mathsf{m}(e,s)\approx\min(\mathsf{m}(e,t),\mathsf{m}(e,u))\end{array}$

$s\approx t\setminus u\in\mathsf{B}^{*}$
$\mathsf{m}(e,v)\in\mathcal{T}(\mathsf{B})$ $v\in\\{s,t,u\\}$ Diff Sub
$\begin{array}[]{ll}&\mathsf{A}:=\mathsf{A},\mathsf{m}(e,t)\leq\mathsf{m}(e,u),\mathsf{m}(e,s)\approx
0\\\
||&\mathsf{A}:=\mathsf{A},\mathsf{m}(e,t)>\mathsf{m}(e,u),\mathsf{m}(e,s)\approx\mathsf{m}(e,t)-\mathsf{m}(e,u)\end{array}$

$s\approx t\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}u\in\mathsf{B}^{*}$
$\mathsf{m}(e,v)\in\mathcal{T}(\mathsf{B})$ $v\in\\{s,t,u\\}$ Diff Rem
$\begin{array}[]{c}\mathsf{A}:=\mathsf{A},\mathsf{m}(e,u)\approx
0,\mathsf{m}(e,s)\approx\mathsf{m}(e,t)~{}~{}~{}||~{}~{}~{}\mathsf{A}:=\mathsf{A},\mathsf{m}(e,u)\not\approx
0,\mathsf{m}(e,s)\approx 0\end{array}$

$s\approx\mathsf{setof}(t)\in\mathsf{B}^{*}$
$\mathsf{m}(e,v)\in\mathcal{T}(\mathsf{B}^{*})$ $v\in\\{s,t\\}$ Setof
$\begin{array}[]{c}\mathsf{A}:=\mathsf{A},1\leq\mathsf{m}(e,t),\mathsf{m}(e,s)\approx
1~{}~{}~{}||~{}~{}~{}\mathsf{A}:=\mathsf{A},\mathsf{m}(e,t)\leq
0,\mathsf{m}(e,s)\approx 0\end{array}$

Figure 3: Bag rules.

$\mathsf{A}\models_{\mathsf{NIA}}1\leq\mathsf{m}(\langle\bar{x}_{m}\rangle,s)\wedge
1\leq\mathsf{m}(\langle\bar{y}_{n}\rangle,t)$ $s\otimes
t\in\mathcal{T}(\mathsf{B})$ Prod Up
$\mathsf{A}:=\mathsf{A},\mathsf{m}(\langle{\bar{x}_{m}},{\bar{y}_{n}}\rangle,s\otimes
t)\approx\mathsf{m}(\langle\bar{x}_{m}\rangle,s)*\mathsf{m}(\langle\bar{y}_{n}\rangle,t)$

$\mathsf{A}\models_{\mathsf{NIA}}1\leq\mathsf{m}(\langle\bar{x}_{m},\bar{y}_{n}\rangle,s\otimes
t)$ Prod Down
$\mathsf{A}:=\mathsf{A},\mathsf{m}(\langle\bar{x}_{m},\bar{y}_{n}\rangle,s\otimes
t)\approx\mathsf{m}(\langle\bar{x}_{m}\rangle,s)*\mathsf{m}(\langle\bar{y}_{n}\rangle,t)$

$\begin{array}[]{c}\mathsf{A}\models_{\mathsf{NIA}}1\leq\mathsf{m}(\langle\bar{x}_{m}\rangle,s)\wedge
1\leq\mathsf{m}(\langle\bar{y}_{n}\rangle,t)\\\\[3.01385pt]
s\bowtie_{i_{1}j_{1}\cdots i_{p}j_{p}}t\in\mathcal{T}(\mathsf{B})\quad
x_{i_{1}}\approx y_{j_{1}},\dots,x_{i_{p}}\approx
y_{j_{p}}\in\mathsf{B}^{*}\end{array}$ Join Up
$\mathsf{A}:=\mathsf{A},\mathsf{m}(\langle\bar{x}_{m},\bar{y}_{n}\rangle,s\bowtie_{i_{1}j_{1}\cdots
i_{p}j_{p}}t)\approx\mathsf{m}(\langle\bar{x}_{m}\rangle,s)*\mathsf{m}(\langle\bar{y}_{n}\rangle,t)$

$\mathsf{A}\models_{\mathsf{NIA}}1\leq\mathsf{m}(\langle\bar{x}_{m},\bar{y}_{n}\rangle,s\bowtie_{i_{1}j_{1}\cdots
i_{p}j_{p}}t)$ Join Down
$\begin{array}[]{c}\mathsf{A}:=\mathsf{A},\mathsf{m}(\langle\bar{x}_{m},\bar{y}_{n}\rangle,s\bowtie_{i_{1}j_{1}\cdots
i_{p}j_{p}}t)\approx\mathsf{m}(\langle\bar{x}_{m}\rangle,s)*\mathsf{m}(\langle\bar{y}_{n}\rangle,t)\\\
\mathsf{B}:=\mathsf{B},x_{i_{1}}\approx y_{j_{1}},\dots,x_{i_{p}}\approx
y_{j_{p}}\end{array}$

Figure 4: Table rules. The syntax $\bar{x}_{m}$ abbreviates
$x_{0},\dots,x_{m}$.

#### The Derivation Rules.

The rules of our calculus are provided in Figures 3, 4 and 5. They are
expressed in guarded assignment form where the premise describes the
conditions on the current configuration under which the rule can be applied,
and the conclusion is either $\mathsf{unsat}$, or otherwise describes changes
to the current configuration. Rules with two conclusions, separated by the
symbol $||$, are non-deterministic branching rules.

In the rules, we write $\mathsf{B},c$, as an abbreviation of
$\mathsf{B}\cup\\{c\\}$ and denote by $\mathcal{T}(\mathsf{B})$ the set of all
terms and subterms occurring in $\mathsf{B}$. Premises of the form
$\mathsf{A}\models_{\mathsf{NIA}}c$, where $c$ is an arithmetic constraint,
can be checked by a solver for (nonlinear) integer arithmetic.555A linear
arithmetic solver is enough for problems not containing the $\otimes$
operator. For problems with SQL joins, whose encoding to SMT does require the
$\otimes$ operator, a solver for nonlinear arithmetic is needed, at the cost
of losing decidability in that case.  Premises of the form
$\mathsf{E}\models_{\mathsf{EL}}\bot$ are checked by the element solver
discussed earlier.

We define the following closure for $\mathsf{B}$ where $\models_{\text{tup}}$
denotes entailment in the theory of tuples, which treats all other symbols as
uninterpreted functions.

$\displaystyle\mathcal{\mathsf{B}}^{*}$ $\displaystyle=\ \\{s\approx
t\;|\;s,t\in\mathcal{T}(\mathsf{B}),\mathsf{B}\models_{\text{tup}}s\approx
t\\}\>\cup\>\\{m(e,s)\approx m(e,t)\mid\mathsf{B}\models_{\text{tup}}s\approx
t,\ m(e,s)\in\mathcal{T}(\mathsf{B})\\}\ $ $\displaystyle\cup\
\\{m(e_{1},s)\approx m(e_{2},s)\mid\mathsf{B}\models_{\text{tup}}e_{1}\approx
e_{2},\ m(e_{1},s)\in\mathcal{T}(\mathsf{B})\\}\ $ $\displaystyle\cup\
\\{s\not\approx
t\;|\;s,t\in\mathcal{T}(\mathsf{B}),\mathsf{B}\models_{\text{tup}}s\approx
s^{\prime}\wedge t\approx t^{\prime}\text{ for some }s^{\prime}\not\approx
t^{\prime}\in\mathsf{B}\\}$ (1)

The set $\mathsf{B}^{*}$ is computable by extending standard congruence
closure procedures with rules for adding equalities of the form
$\mathsf{select}_{i}(\langle x_{0},\ldots,x_{i},\ldots,x_{k}\rangle)\approx
x_{i}$ and rules for deducing consequences of equalities of the form $\langle
s_{1},\dots,s_{n}\rangle\approx\langle t_{1},\dots,t_{n}\rangle$.

Among the derivation rules in Figure 3, rules A-Conf, E-Conf are applied when
conflicts are found by the arithmetic solver or the element solver. Likewise,
rule B-Conf is applied when the congruence closure procedure finds a conflict
between an equality and a disequality constraint. Rules B-A-Prop, B-E-Prop,
and A-Prop communicate equalities between the three solvers. Rule Diseq
handles disequality between two bags $s,t$ by stating that some element,
represented by a fresh variable $w$, occurs with different multiplicities in
$s$ and $t$. Rule Nonneg ensures that all multiplicities are nonnegative. Rule
Empty enforces zero multiplicity for elements to a bag that is provably equal
to the empty bag.

Rules Cons1 and Cons2 reason about singleton bags, denoted by terms of the
form $\mathsf{bag}(e,n)$. The first one splits on whether $n$ is positive or
not to determine whether $\mathsf{bag}(e,n)$ is empty, and if not, it also
determines the multiplicity of element $e$ to be $n$. The second one ensures
that no elements different from $e$ are in $\mathsf{bag}(e,n)$. Rules Disj
Union, Max Union, Inter, Diff Sub, Diff Rem, and Setof correspond directly to
the semantics of their operators. For example, the Disj Union rule applies to
any multiplicity term related to bags
$(t,u,t\mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}u)$ or their equivalence
classes if $t\mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}u\in\mathcal{T}(B)$.

The rules in Figure 4 are specific to table operations. Prod Up and Prod Down
are upward and downward rules for the $\otimes$ operator. They are the ones
which introduce nonlinear arithmetic constraints on multiplicities. Join Up
and Join Down are similar to the product rules. However, they consider the
equality constraints between joining columns, to account for the semantics of
inner joins.

$\mathsf{A}\models_{\mathsf{NIA}}1\leq\mathsf{m}(e,t)$
$\mathsf{m}(e,t)\in\mathcal{T}(\mathsf{B}^{*})$
$s\approx\sigma(p,t)\in\mathsf{B}^{*}$ Filter Up
$\mathsf{E}:=\mathsf{E},p(e)\quad\mathsf{A}:=\mathsf{A},\mathsf{m}(e,s)\approx\mathsf{m}(e,t)~{}~{}||~{}~{}\mathsf{E}:=\mathsf{E},\neg
p(e)\quad\mathsf{A}:=\mathsf{A},\mathsf{m}(e,s)\approx 0$

$\mathsf{A}\models_{\mathsf{NIA}}1\leq\mathsf{m}(e,s)$
$\mathsf{m}(e,s)\in\mathcal{T}(\mathsf{B}^{*})$
$s\approx\sigma(p,t)\in\mathsf{B}^{*}$ Filter Down
$\mathsf{E}:=\mathsf{E},p(e)\qquad\mathsf{A}:=\mathsf{A},\mathsf{m}(e,s)\approx\mathsf{m}(e,t)$

$\mathsf{A}\models_{\mathsf{NIA}}1\leq\mathsf{m}(e,t)$
$\mathsf{m}(e,t)\in\mathcal{T}(\mathsf{B}^{*})$
$s\approx\pi(f,t)\in\mathsf{B}^{*}$ $e\not\in W$ Map Up
$\mathsf{A}:=\mathsf{A},\mathsf{m}(e,t)\leq\mathsf{m}(f(e),s)$

$\mathsf{m}(e,s)\in\mathcal{T}(\mathsf{B}^{*})$
$s\approx\pi(f,t)\in\mathsf{B}^{*}$ $f$ is injective Inj Map Down
$\mathsf{E}:=\mathsf{E},f(w)\approx
e\qquad\mathsf{A}:=\mathsf{A},\mathsf{m}(e,s)\approx\mathsf{m}(w,t)$

$\mathsf{A}\models_{\mathsf{NIA}}1\leq\mathsf{m}(e,t)$
$s\approx\pi(f,t)\in\mathsf{B}^{*}$ NotInj Up
$\mathsf{B}:=\mathsf{B},i\approx\mathit{ind}(e,t)\qquad\mathsf{A}:=\mathsf{A},1\leq
i\leq\mathit{delem}(t)$

$\mathsf{A}\models_{\mathsf{NIA}}1\leq\mathsf{m}(e,s)\quad
s\approx\pi(f,t)\in\mathsf{B}^{*}$ NotInj Down
$\mathsf{A}:=\mathsf{A},\mathit{sum}(e,t,\mathit{delem}(t))\approx\mathsf{m}(e,s),\mathit{sum}(e,t,0)\approx
0$

Figure 5: Bag filter and map rules. $w,i$ are fresh variables.

The rules in Figure 5 reason about the filter ($\sigma$) and map ($\pi$)
operators. Filter Up splits on whether an element $e$ in $s$ satisfies (the
predicate denoted by) $p$ or not in order to determine its multiplicity in bag
$\sigma(p,s)$. Filter Down concludes that every element with positive
multiplicity in $\sigma(p,s)$ necessarily satisfies $p$ and has the same
multiplicity in $s$. Map Up applies the function symbol $f$ to every element
$e$ that is provably in bag $t$. Note that it cannot determine the exact
multiplicity of $f(e)$ in bag $\pi(f,t)$ since multiple elements can be mapped
to the same one by $f$ if (the function denoted by) $f$ is not injective.
Therefore, the rule just asserts that $\mathsf{m}(f(e),\pi(f,t))$ is at least
$\mathsf{m}(e,t)$. To prevent derivation cycles with Inj Map Down, rule Map Up
applies only if $e$ is not a variable introduced by the downward rule.

The downward direction for map terms is more complex, and expensive, if $f$ is
not injective. Therefore, before solving, we check the injectivity of each
function symbol $f$ occurring in map terms. This is done via a subsolver
instance that checks the satisfiability of the formula $f(x)\approx f(y)\wedge
x\not\approx y$ for fresh variables $x,y$. If the subsolver returns
$\mathsf{unsat}$, which means that $f$ is injective, we apply rule Inj Map
Down which introduces a fresh variable $w$ for each term
$\mathsf{m}(e,\pi(f,t))$ such that $e=f(w)$ and $w$ is in $t$ with the same
multiplicity. In contrast, if the subsolver returns $\mathsf{sat}$ or
$\mathsf{unknown}$, we treat $f$ as non-injective and rely on a number of
features of cvc5 to construct and process a set of quantified constraints
which, informally speaking and mixing syntax and semantics here for
simplicity, formalize the following relationship between the multiplicity of
an element $e$ in a bag $\pi(f,t)$ and that of the elements of $t$ that $f$
maps to $e$:

$\displaystyle\mathsf{m}(e,\pi(f,t))=\sum\\{\,\mathsf{m}(x,t)\mid x\in
t\,\wedge\,f(x)=e\,\\}$ (2)

To encode this constraint, we introduce three uninterpreted symbols,
$\mathit{delem}:\mathsf{Bag}(\alpha)\rightarrow\mathsf{Int}$,
$\mathit{ind}:\alpha\times\mathsf{Bag}(\alpha)\rightarrow\mathsf{Int}$, and
$\mathit{sum}:\alpha\times\mathsf{Bag}(\alpha)\times\mathsf{Int}\rightarrow\mathsf{Int}$.
The value $\mathit{delem}(t)$ represents the number of distinct elements in
(the bag denoted by) $t$; $\mathit{ind}(e,t)$ represents a unique index in the
range $[1,\mathit{delem}(t)]$ for element $e$ in bag $t$; for an element $e$
in $\pi(f,t)$, $\mathit{sum}(e,t,i)$ accumulates the multiplicities of the
elements of $t$ with index in $[1,i]$ that $f$ maps to $e$. Rule NotInj Up
ensures that every element in $t$ is assigned an index $i$ in
$[1,\mathit{delem}(t)]$, whereas NotInj Up constrains the multiplicity
$\mathsf{m}(e,s)$ to be $\mathit{sum}(e,t,\mathit{delem}(t))$ when $e$ is in
$s$. We do not describe the encoding of (2) here due to space limitations.
However, it is an axiom with bounded quantification over the interval
$[1,\mathit{delem}(t)]$ that is processed by cvc5’s model-based quantifier
instantiation module [boundedQuantifiers]. The encoding of the quantified
formula is given in 9.

######  Example 0.2.1.

Suppose we have the constraints:
$\\{\,x\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s,y\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\pi(f,s),y\approx
x+1\,\\}$ where $x,y$ are integers and $f$ is defined in the arithmetic solver
to be the integer successor function ($f(x)=x+1$). After applying
simplification rules in Figure 2, we end up with
$c_{0}=(\mathsf{A}_{0},\mathsf{B}_{0},\mathsf{E}_{0})$, where
$\mathsf{A}_{0}=\\{\,\neg(1\leq\mathsf{m}(x,s)),1\leq\mathsf{m}(y,\pi(f,s)),y\approx
x+1\,\\}$ and $\mathsf{E}_{0}=\\{\,y\approx x+1\,\\}$. Applying rule Nonneg,
we get $c_{1}=(\mathsf{A}_{1},\mathsf{B}_{1},\mathsf{E}_{1})$, where
$\mathsf{A}_{1}=\mathsf{A}_{0}\cup\\{\,0\leq\mathsf{m}(x,s),0\leq\mathsf{m}(y,\pi(f,s))\,\\}$
and $\mathsf{E}_{1}=\mathsf{E}_{0}$. Since $f$ is injective, we can apply rule
Inj Map Down to get $c_{2}=(\mathsf{A}_{2},\mathsf{B}_{2},\mathsf{E}_{2})$,
where
$\mathsf{A}_{2}=\mathsf{A}_{1}\cup\\{\,\mathsf{m}(w,s)\approx\mathsf{m}(y,\pi(f,s))\,\\}$
and $\mathsf{E}_{2}=\mathsf{E}_{1}\cup\\{\,y\approx w+1\,\\}$. Next, we apply
the propagation rule E-Ident followed by B-A-Prop to get
$\mathsf{A}_{3}=\mathsf{A}_{2}$,
$\mathsf{A}_{4}=\mathsf{A}_{3}\cup\\{\,y\approx w+1\,\\}$. Now,
$\mathsf{A}_{4}$ is unsatisfiable because it entails $x\approx w$,
$\neg(1\leq\mathsf{m}(x,s))$, and $1\leq\mathsf{m}(w,s)$. Hence the rule
A-Conf applies, and we get $\mathsf{unsat}$. If we remove the constraint
$x\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s$,
then the problem is satisfiable and we can construct a model $\mathcal{I}$
where $\mathcal{I}(x)$ is any natural $n$, $\mathcal{I}(y)=n+1$, and
$\mathcal{I}(s)$ is a singleton bag containing $n$ with multiplicity 1.

###  0.2.2 Calculus Correctness

Logozzo et al. [16] proved the decidability of the theory of bags with linear
constraints over bag cardinality and the operators: $\varnothing$,
$\mathsf{bag}$, $\mathsf{m}$, $\sqcup$,
$\mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}$, $\sqcap$, $\setminus$,
$\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}$, $\mathsf{setof}$,
$\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}$,
$\sqsubseteq$. In this work, we exclude the cardinality operator. However, we
prove that adding the $\sigma$ operator with computable predicates preserves
decidability (See Proposition 0.2.5 below). In contrast, the further addition
of the $\otimes$ and $\mathsf{proj}$ operators makes the problem undecidable.
This is provable with a reduction from the undecidable equivalence problem for
unions of conjunctive SQL queries [14]. Our calculus is not refutation
complete in general in the presence of maps because of the possibility of
nontermination, as shown in the example below.

######  Example 0.2.2.

Suppose $x$ is an integer variable, and $s$ is an integer bag variable and
consider just the constraint set $\\{\mathsf{m}(x,s)\approx
1,\,s\approx\pi(f,s)\\}$ where $f$ is again the successor function. The set is
unsatisfiable in the theory of finite bags. However, this is not provable in
our calculus as it allows the repeated application of rules Map Up and A-Prop,
which add fresh elements $x+1,x+2,x+3,\dots$ to $s$.

Another source of refutation incompleteness is the presence of constraints
with the cross product operator $\otimes$, which causes the generation of
nonlinear constraints for the arithmetic subsolver, making the entailment
checks in rules such as A-Conf and B-A-Prop undecidable.

However, in the absence of $\pi$ and $\otimes$, the calculus is both
refutation and solution sound, as well as terminating. The soundness
properties are a consequence of the fact that each derivation rule preserves
models, as specified in the following lemma.

######  Lemma 0.2.2.

For all applications of a rule from the calculus, the premise configuration is
satisfiable in $\mathbb{T}_{\mathsf{Tab}}$ if and only if one of the
conclusion configurations is satisfiable in $\mathbb{T}_{\mathsf{Tab}}$.

The proof of this lemma provides actually a stronger result than stated in the
right-to-left implication above: for each of the conclusion configurations
$C^{\prime}$, every model of $\mathbb{T}_{\mathsf{Tab}}$ that satisfies
$C^{\prime}$ satisfies the premise configuration as well. This implies that
any model that satisfies a saturated leaf of a derivation tree satisfies the
root configuration as well.

######  Proposition 0.2.3 (Refutation Soundness).

For every closed derivation tree with root node $C$, configuration $C$ is
$\mathbb{T}_{\mathsf{Tab}}$-unsatisfiable.

The proposition above implies that deriving a closed tree with a root
$\langle\mathsf{A},\mathsf{B},\mathsf{E}\rangle$ is sufficient to prove the
unsatisfiability in $\mathbb{T}_{\mathsf{Tab}}$ of the constraints
$\mathsf{A}\cup\mathsf{B}\cup\mathsf{E}$. The proof of the proposition is a
routine proof by induction on the structure of the derivation tree.

Solution soundness has a more interesting proof since it relies on the
construction of a satisfying interpretation for a saturated leaf of a
derivation tree, which is a witness to the satisfiability of the root
configuration. We describe next at a high level how to construct an
interpretation $\mathcal{I}$ for a saturated configuration
$C=(\mathsf{A},\mathsf{B},\mathsf{E})$.666The full model construction and its
correctness are discussed in detail in the longer version of this paper
[arxiv]. appendix.  More precisely, we construct a _valuation_ $\mathcal{I}$
of the variables and terms in $C$ that agrees with the semantics of the theory
symbols and satisfies $\mathsf{A}\cup\mathsf{B}\cup\mathsf{E}$.

Once again, to simplify the exposition, we assume, _with_ loss of generality,
that any element sort $\varepsilon$ in the problem can be interpreted as an
infinite set. The actual implementation uses cvc5’s theory combination
mechanism to allow also sorts denoting finite sets, under mild restrictions on
the theories involved [20].

Model Construction Steps

  1. 1.

Sorts: The meaning of the sort constructors $\mathsf{Bag}$, $\mathsf{Tuple}$,
and $\mathsf{Int}$ is fixed by the theory. The element sort $\varepsilon$ is
interpreted as an infinite set. As a concrete representation of bags, and
hence of tables, consistent with the theory, we choose sets of pairs $(e,n)$,
where $e$ is an element of the bag in question, and $n$ is its (positive)
multiplicity.

  2. 2.

$\Sigma_{\mathsf{Tab}}$: $\mathbb{T}_{\mathsf{Tab}}$ enforces the
interpretation of all $\Sigma_{\mathsf{Tab}}$-symbols. Saturation guarantees
that equivalent bag/tuple terms will be interpreted by $\mathcal{I}$ as the
same bag/tuple.

  3. 3.

Integer variables: Saturation guarantees that there is some model of
$\mathbb{T}_{\mathsf{\mathsf{NIA}}}$ that satisfies $\mathsf{A}$. We define
$\mathcal{I}$ to interpret integer variables according to this model.

  4. 4.

Variables of sort $\varepsilon$: The calculus effectively partitions them into
equivalent classes (where $x$ is in the same class as $y$ iff $x\approx y$ is
entailed by $\mathsf{B}$). Each class is assigned a distinct element from
$\mathcal{I}(\varepsilon)$, which is possible since it is infinite.

  5. 5.

Bag variables: $\mathcal{I}$ interprets each bag variable $s$ as the set

$\mathcal{I}(s)=\\{\,(\mathcal{I}(e),n)\mid\mathsf{m}(e,s)\in\mathcal{T}(\mathsf{B}^{*}),\;\mathcal{I}(\mathsf{m}(e,s))=n>0\,\\}.$

A well-foundedness argument on $\mathcal{I}$’s construction guarantees that
the equation above is well defined. Note that $\mathcal{I}(s)$ is the empty
bag iff there is no term $\mathsf{m}(e,s)$ in $\mathcal{T}(\mathsf{B}^{*})$
that satisfies the conditions in the comprehension above.

######  Example 0.2.3.

From Example 0.2.1, the set of constraints
$\\{\,y\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\pi(f,s),y\approx
x+1\,\\}$ is satisfiable. In this example the element sort is $\mathsf{Int}$,
interpreted as the integers. Similar to Example 0.2.1, the terms
$\mathsf{m}(y,\pi(f,s)),w,\mathsf{m}(w,s)$ are generated during solving. After
saturation, and for simplicity, suppose we end up with the following sets of
equivalence classes for the terms involved: $\\{\mathsf{m}(y,\pi(f,s))$,
$\mathsf{m}(x,s)\\}$, $\\{x,w\\}$, $\\{y,x+1\\}$, $\\{s\\}$, $\\{\pi(f,s)\\}$.
The theory of arithmetic assigns consistent concrete values to the first three
equivalence classes, say 1, 10, 11, respectively. In Step 5, $s$ is
interpreted as the set $\\{(\mathcal{I}(x),\mathcal{I}(\mathsf{m}(x,s))),\
(\mathcal{I}(w),\mathcal{I}(\mathsf{m}(w,s)))\\}=\\{(10,1)\\}$, and similarly
$\mathcal{I}(\pi(f,s))=\\{(\mathcal{I}(y),\mathcal{I}(\mathsf{m}(y,\pi(f,s))))\\}=\\{(11,1)\\}$.

######  Proposition 0.2.4 (Solution Soundness).

For every derivation tree with root node $C_{0}$ and a saturated leaf $C$,
configuration $C_{0}$ is satisfiable in $\mathbb{T}_{\mathsf{Tab}}$.

While the calculus is not terminating in general, we can show that all
derivations are finite in restricted cases.

######  Proposition 0.2.5 (Termination).

Let $C$ be a configuration containing no product, join, or map terms. All
derivation trees with root $C$ are finite.

Under the restrictions in the proposition above, the rules of the calculus
will never generate nonlinear arithmetic constraints. This means that for
input problems that also have no such constraints, any derivation strategy for
the calculus yields a decision procedure.

##  0.3 A Theory of Finite Relations with Filter and Map

$\begin{array}[]{c}\langle
x_{1},\dots,x_{m}\rangle\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s\in\mathsf{S}^{*}\qquad\langle
y_{1},\dots,y_{n}\rangle\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}t\in\mathsf{S}^{*}\\\\[3.01385pt]
s\bowtie_{i_{1}j_{1}\cdots i_{p}j_{p}}t\in\mathcal{T}(\mathsf{S})\qquad
x_{i_{1}}\approx y_{j_{1}},\dots,x_{i_{p}}\approx
y_{j_{p}}\in\mathsf{S}^{*}\end{array}$ Join Up $\mathsf{S}:=\mathsf{S},\langle
x_{1},\dots,x_{m},y_{1},\dots,y_{n}\rangle\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s\bowtie_{i_{1}j_{1}\cdots
i_{p}j_{p}}t$

$\langle
x_{1},\dots,x_{m},y_{1},\dots,y_{n}\rangle\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}{s\bowtie_{i_{1}j_{1}\cdots
i_{p}j_{p}}t}\in\mathsf{S}^{*}$ Join Down
$\begin{array}[]{c}\mathsf{S}:=\mathsf{S},\langle
x_{1},\dots,x_{m}\rangle\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s,\langle
y_{1},\dots,y_{n}\rangle\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}t,x_{i_{1}}\approx
y_{j_{1}},\dots,x_{i_{p}}\approx y_{j_{p}}\end{array}$

$e\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s\in\mathsf{S}^{*}$
$\sigma(p,s)\in\mathcal{T}(\mathsf{S})$ Filter up
$\mathsf{E}:=\mathsf{E},p(e)\quad\mathsf{S}:=\mathsf{S},e\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\sigma(p,s)~{}~{}~{}||~{}~{}~{}\mathsf{E}:=\mathsf{E},\neg
p(e)\quad\mathsf{S}:=\mathsf{S},e\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\sigma(p,s)$

$e\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s\in\mathsf{S}^{*}$
$\pi(f,s)\in\mathcal{T}(S)$ $e\not\in W$ Map up
$\mathsf{S}:=\mathsf{S},f(e)\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\pi(f,s)$

$e\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\pi(f,s)\in\mathsf{S}^{*}$
$w\in W$ Map down $\mathsf{E}:=\mathsf{E},f(w)\approx
e\quad\mathsf{S}:=\mathsf{S},w\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s$
$e\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\sigma(p,s)\in\mathsf{S}^{*}$
Filter down
$\mathsf{E}:=\mathsf{E},p(e)\quad\mathsf{S}:=\mathsf{S},e\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s$

Figure 6: Set filter and map rules. $w$ is a fresh variable unique per
$e,f,s$.

To reason about SQL queries under set semantics, we rely on the theory of
finite relations $\mathbb{T}_{\mathsf{Rel}}$, whose signature and calculus are
described in Meng et al. [17]. We extend the signature with filter and map
operators analogous to those in the theory of tables. We overload the symbols
$\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}},\sqsubseteq,\sqcup,\sqcap,\setminus,\otimes,\sigma,\pi,\bowtie$
for set operations membership, subset, union, intersection, difference,
product, filter, map, and (inner) join,777This is analogous to the inner join
operator for tables but differs from the relational join operator defined in
Meng et al. [17].  respectively. We use $\mathsf{rel.proj}$ for relation
projection.

A calculus to reason about constraints in $\mathbb{T}_{\mathsf{Rel}}$ can be
defined over configurations of the form $\langle\mathsf{S},\mathsf{E}\rangle$,
where $\mathsf{S}$ is a set of $\mathbb{T}_{\mathsf{Rel}}$-constraints, and
$\mathsf{E}$ is a set of element constraints similar to the one defined in
Section 0.2. We again assume we have a solver that can decide the
satisfiability of element constraints. The
$\mathbb{T}_{\mathsf{Rel}}$-constraints are equational constraints of the form
$s\approx t$ and $s\not\approx t$ and membership constraints of the form
$e\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s$ and
$e\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s$,
where $e,s,t$ are $\Sigma_{r}$-terms. Similar to bags, we also define the set
$W$ to be an infinite set of fresh variables specific for map rules. The
closure $\mathsf{S}^{*}$ for the $\mathsf{S}$ component of a configuration is
defined as:

$\displaystyle\mathcal{\mathsf{S}}^{*}=\ $ $\displaystyle\\{s\approx
t\;|\;s,t\in\mathcal{T}(\mathsf{S}),\mathsf{S}\models_{\text{tup}}s\approx
t\\}$ $\displaystyle\cup\ $ $\displaystyle\\{s\not\approx
t\;|\;s,t\in\mathcal{T}(\mathsf{S}),\mathsf{S}\models_{\text{tup}}s\approx
s^{\prime}\wedge t\approx t^{\prime}\text{ for some }s^{\prime}\not\approx
t^{\prime}\in\mathsf{S}\\}$ $\displaystyle\cup\ $
$\displaystyle\\{e\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s\;|\;e,s\in\mathcal{T}(\mathsf{S}),\mathsf{S}\models_{\text{tup}}e\approx
e^{\prime}\wedge s\approx s^{\prime}\text{ for some
}e^{\prime}\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s^{\prime}\in\mathsf{S}\\}$

For space constraints, we refer the reader to the extended version of this
paper [arxiv] for a full description of the extended signature and calculus.
The extended signature and the original derivation rules are provided in
Appendix .8 for reference. We provide in Figure 6 only our additional rules:
those for filter and map, which resemble the corresponding rules given in
Figure 5 for bags, and those for inner joins.

#### Calculus correctness.

Bansal et al. [2] provide a sound, complete, and terminating calculus for a
theory of finite sets with cardinality. The calculus is extended to relations
but without cardinality by Meng et al. [17]. That extension is refutation- and
solution-sound but not terminating in general. While it is proven terminating
over a fragment of the theory of relations, that fragment excludes the
relational product operator, which we are interested in here.

We have proved that the calculus by Meng et al. extended with the filter rules
in Figure 6 is terminating for constraints built with the operators
$\\{\approx,\sqcup,\sqcap,\setminus,\otimes,\sigma\\}$ [arxiv]. (see Lemma
LABEL:newlemma). Termination is lost with the addition of map rules, also in
Figure 6. Example 0.2.2 works in this case too as a witness.

However, termination can be recovered when the initial configuration satisfies
a certain _acyclicity_ condition. To express this condition, we associate with
each configuration $C=\langle\mathsf{S},\mathsf{E}\rangle$ an undirected
multi-graph $G$ whose vertices are the relation terms of sort $\mathsf{Set}$
occurring in $\mathsf{S}$, and whose edges are labeled with an operator in
$\\{\approx,\sqcup,\sqcap,\setminus,\otimes,\bowtie,\sigma,\pi\\}$. Two
vertices have an edge in $G$ if and only if they are in the same equivalence
class or a membership rule can be applied (either upward or downward) to $C$
such that one of the vertices occurs as a child of the other vertex in the
premises or conclusions of the rule. Furthermore, each edge between vertices
$\pi(f,s)$ and $s$ is colored red while the remaining edges are colored black.

######  Proposition 0.3.1.

Let $C_{0}=\langle\mathsf{S}_{0},\mathsf{E}_{0}\rangle$ be an initial
configuration and let $G_{0}$ be its associated multi-graph. The calculus is
terminating for $C_{0}$ if there is no cycle in $G_{0}$ with red edges, and
all cycles are located in a subgraph without map terms.

Figure 7 shows the graph for Example 0.2.2 which has a cycle with a red edge.
Figure 8 shows a graph with no red cycles. For the purposes of this paper, the
acyclicity condition is not a serious restriction because typical SQL queries
translate to initial configurations whose associated graph does not have
cycles with red edges.888Examples of SQL queries that do have cycles with red
edges are queries with recursive common table expressions.

$s$$\pi(f,s)$$\approx$$\pi$ Figure 7: A cycle that contains a red edge with
$\pi$ label.

$s_{i}$$\pi(f_{i},s_{i})$ $\cdots$$\cdots$$t$$s_{j}$$\pi(f_{j},s_{j})$
$\pi$$\pi$$\approx$$\sqcup$$\approx$$\sqcap$$\setminus$

Figure 8: A graph with no cycles that contain red edges.

##  0.4 Supporting Nullable Sorts

SQL and relational databases allow tables with _null values_. To support them
in SMT, one could rely in principle on SMT solvers that accept user-defined
algebraic datatypes [18], as nullable types are a form of option types. That
is, however, not enough since, to encode SQL operations on nullable types, one
also needs to lift all operators over a given sort to its nullable version.
Since this is extremely tedious and error-prone when done at the user level,
we extended the datatypes solver in cvc5 by adding built-in parametric
$\mathsf{Nullable}$ sorts, along with selectors, testers, and a family of
(second-order) lifting operators. The signature of the corresponding theory of
nullable sorts is provided in Figure 9. The meaning of constructors
$\mathsf{null}$ and $\mathsf{some}$, the selector $\mathsf{val}$, and the
testers $\mathsf{isNull},\mathsf{isSome}$ is standard; that of $\mathsf{lift}$
is:

$\displaystyle\mathsf{lift}(f,x_{1},\dots,x_{k})=\begin{cases}\mathsf{null}&\text{if
}x_{i}=\mathsf{null}\text{ for some }i\in[1,k]\\\
\mathsf{some}(f(\mathsf{val}(x_{1}),\dots,\mathsf{val}(x_{k})))&\text{otherwise}\end{cases}$

which is analogous to the semantics of eager evaluation in programming
languages. This semantics covers most SQL operations, except for OR and AND,
as SQL adopts a three-valued logic for nullable Booleans [11], interpreting,
for instance, NULL OR TRUE as TRUE and NULL AND FALSE as FALSE. We can support
this short-circuiting semantics through an encoding from SQL to SMT based on
the if-then-else operator.

$\begin{array}[]{l}\begin{array}[]{@{}l@{\quad}l@{\quad}l@{\quad}l@{}}\hline\cr\hline\cr\textbf{Symbol}&\textbf{Arity}&\textbf{SMTLIB}&\textbf{Description}\\\
\hline\cr\mathsf{null}&\mathsf{Nullable}(\alpha)&\verb|nullable.null|&\text{Null
constructor}\\\
\mathsf{some}&\alpha\rightarrow\mathsf{Nullable}(\alpha)&\verb|nullable.some|&\text{Some
constructor}\\\
\mathsf{val}&\mathsf{Nullable}(\alpha)\rightarrow\alpha&\verb|nullable.val|&\text{Value
selector}\\\
\mathsf{isNull}&\mathsf{Nullable}(\alpha)\rightarrow\mathsf{Bool}&\verb|nullable.is_null|&\text{Is
null tester}\\\
\mathsf{isSome}&\mathsf{Nullable}(\alpha)\rightarrow\mathsf{Bool}&\verb|nullable.is_some|&\text{Is
some tester}\\\
\mathsf{lift}&\tiny\left(\alpha_{1}\times\dots\times\alpha_{k}\rightarrow\alpha\right)\times\\\
&\tiny\mathsf{Nullable}(\alpha_{1})\times\dots\times\mathsf{Nullable}(\alpha_{k})\rightarrow\mathsf{Nullable}(\alpha)&\verb|nullable.lift|&\text{Lifting
operators}\\\ \hline\cr\hline\cr\end{array}\\\\[12.05554pt] \end{array}$

Figure 9: Signature for the theory of nullable sorts. $\mathsf{lift}$ is a
variadic function symbol.

##  0.5 Evaluation of Benchmarks on Sets and Bags

We evaluated our cvc5 implementation using a subset of the benchmarks [12]
derived from optimization rewrites of Apache calcite, an open source database
management framework [10]. The benchmark set provides a database schema for
all the benchmarks. Each benchmark contains two queries over that schema which
are intended to be equivalent under bag semantics, in the sense that they
should result in the same table for any instance of the schema. The total
number of available benchmarks is 232. We modified many queries that had
syntax errors or could not actually be parsed by calcite. We then excluded
benchmarks with queries containing constructs we currently do not support,
such as ORDER BY clauses999Both SPES and SQLSolver provide partial support for
ORDER BY. They classify two input queries with ORDER BY clauses as equivalent
if they can prove their respective subqueries without the ORDER BY clause
equivalent. Otherwise, they return $\mathsf{unknown}$.  or aggregate
functions, or benchmarks converted to queries with aggregate functions by the
calcite parser. That left us with 88 usable benchmarks, that is, about 38% of
all benchmarks. For the purposes of the evaluation we developed a prototype
translator from those benchmarks into SMT problems over the theory of tables
and of relations presented earlier, following SQL’s bag semantics and set
semantics, respectively. The translator uses different encodings for bag
semantics and set semantics. Each SMT problem is unsatisfiable iff the SQL
queries in the corresponding benchmark are equivalent under the corresponding
semantics.

We ran cvc5 on the translated benchmarks on a computer with 128GB RAM and with
a 12th Gen Intel(R) Core(TM) i9-12950HX processor. We compared our results
with those of SQLSolver and SPES analyzers — which can both process the
calcite benchmarks directly. The results are shown in Figure 10(a). The first
three lines show the results for the bags semantics encoding (b) while the
fourth line shows the results for the set semantics encoding (s). The column
headers $\not\equiv$, $\equiv$, and uk stand for inequivalent, equivalent, and
$\mathsf{unknown}$ respectively. Unknown for SPES means it returns “not
proven,” whereas for cvc5 it means that it timed out after 10 seconds.
SQLSolver solves all benchmarks efficiently within few seconds. However, it
incorrectly claims that the two queries in one benchmark, testPullNull, are
equivalent, despite the fact that they return tables which differ by the order
of their columns. The SQLSolver developers acknowledged this issue as an error
after we reported it to them, and they fixed it in a later version. SPES too
misclassified benchmark testPullNull as well as another one
(testAddRedundantSemiJoinRule) where the two queries are equivalent only under
set semantics. The SPES authors acknowledged this as an error in their code.
The tool is supposed to answer $\mathsf{unknown}$ for the second benchmark, as
the two queries have different structures, a case that SPES does not support.
cvc5 gives the correct answer for these two benchmarks. In each case, it
provides counterexamples in the form of a small database over which the two
SQL queries differ, something that we were able to verify independently using
the PostgreSQL database server [13]. Under set semantics, cvc5 found 83 out of
88 benchmarks to contain equivalent queries, found 1 to contain inequivalent
queries (testPullNull), and timed out on 4 benchmarks. Under bag semantics,
cvc5 proved fewer benchmarks than both SPES and SQLSolver. However, it found
the benchmark whose queries are inequivalent under bag semantics but
equivalent under set semantics.

Since the calcite benchmark set is heavily skewed towards equivalent queries,
we mutated each of the 88 benchmarks to make the mutated queries inequivalent.
The mutation was performed manually but _blindly_ , to avoid any bias towards
the tools being compared. For the same reason, we excluded the two original
benchmarks that SPES misclassifies. The results of running the three tools on
the mutated benchmarks are shown in Figure 10(b). SQLSolver was able to solve
all of them correctly. As expected, SPES returned $\mathsf{unknown}$ on all of
them since it cannot verify that two queries are inequivalent.

Note that cvc5’s performance improves with the mutated benchmarks because many
of them use non-injective map functions, and it is easier to find
countermodels for such benchmarks than it is to prove equivalence. Consistent
with that, we observe that cvc5 times out for more benchmarks under set
semantics than for bag semantics. We conjecture that this is because more
queries are equivalent under set semantics than they are under bag semantics.

Looking at cvc5’s overall results, more benchmarks were proven equivalent by
cvc5 under set semantics than bag semantics. How to improve performance under
bag semantics requires further investigation. However, we find it interesting
and useful for the overall development of SQL analyzers that cvc5 was able to
expose a couple of bugs in the compared tools.

|  | $\not\equiv$ | $\equiv$ | uk | Total
---|---|---|---|---|---
SQLSolver | (b) | 1 | 87 |  | 88
SPES | (b) |  | 54 | 34 | 88
cvc5 | (b) | 2 | 42 | 44 | 88
cvc5 | (s) | 1 | 83 | 4 | 88
(a)

|  | $\not\equiv$ | $\equiv$ | uk | Total
---|---|---|---|---|---
SQLSolver | (b) | 86 |  |  | 86
SPES | (b) |  |  | 86 | 86
cvc5 | (b) | 81 |  | 5 | 86
cvc5 | (s) | 67 | 9 | 10 | 86
(b)

Figure 10: Left table is the original benchmarks, right table is the mutated
one. SPES can only answer equivalent or $\mathsf{unknown}$.

##  0.6 Conclusion and Future Work

We showed how to reason about SQL queries automatically using a number of
theories in SMT solvers. We introduced a theory of finite tables to support
SQL’s bag semantics. We extended a theory of relations to support SQL’s set
semantics. We handled null values by extending a theory of algebraic datatypes
with nullable sorts and a generalized lifting operator. We also showed how to
translate SQL queries without aggregation into these theories. Our comparative
evaluation has shown that our implementation is not yet fully competitive
performance-wise with that of specialized SQL analyzers, particularly on
equivalent queries with non-injective mapping functions. We plan to address
this in future work.

We are experimenting with adding support for _fold_ functionals in order to
encode and handle SQL queries with aggregation operators. Another direction
for future work is adding filter and map operators to a theory of sequences
[19] to reason about SQL queries with _order-by_ clauses, which current tools
support only in part.

#### Acknowledgements

This work was supported in part by a gift from Amazon Web Services. We are
grateful to Qi Zhou and Joy Arulraj, the authors of SPES, for their help,
detailed answers to our questions, and for sharing the source code and
benchmarks of SPES, which we used in this paper. We are also grateful to
Haoran Ding, the first author of SQLSolver, for his prompt answers to our
questions and his clarifications on some aspects of the tool. Finally, we
thank Abdalrhman Mohamed and the anonymous reviewers for their for his
feedback and suggestions for improving the paper.

## References

  * [1] Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases: The Logical Level. Addison-Wesley Longman Publishing Co., Inc., USA, 1st edn. (1995), https://dl.acm.org/doi/10.5555/551350
  * [2] Bansal, K., Barrett, C.W., Reynolds, A., Tinelli, C.: Reasoning with finite sets and cardinality constraints in SMT. Log. Methods Comput. Sci. 14(4) (2018), https://doi.org/10.23638/LMCS-14(4:12)2018
  * [3] Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength SMT solver. In: TACAS (1). Lecture Notes in Computer Science, vol. 13243, pp. 415–442. Springer (2022)
  * [4] Barbosa, H., Reynolds, A., Ouraoui, D.E., Tinelli, C., Barrett, C.W.: Extending SMT solvers to higher-order logic. In: Fontaine, P. (ed.) Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11716, pp. 35–54. Springer (2019), https://doi.org/10.1007/978-3-030-29436-6_3
  * [5] Chandra, A.K., Merlin, P.M.: Optimal implementation of conjunctive queries in relational data bases. In: Proceedings of the Ninth Annual ACM Symposium on Theory of Computing. pp. 77–90. STOC ’77, Association for Computing Machinery, New York, NY, USA (1977), https://doi.org/10.1145/800105.803397
  * [6] Chaudhuri, S., Vardi, M.Y.: Optimization of real conjunctive queries. In: Proceedings of the Twelfth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems. pp. 59–70. PODS ’93, Association for Computing Machinery, New York, NY, USA (1993), https://doi.org/10.1145/153850.153856
  * [7] Chu, S., Wang, C., Weitz, K., Cheung, A.: Cosette: An automated prover for SQL. In: CIDR 2017, 8th Biennial Conference on Innovative Data Systems Research, Chaminade, CA, USA, January 8-11, 2017, Online Proceedings (2017), http://cidrdb.org/cidr2017/papers/p51-chu-cidr17.pdf
  * [8] Cohen, S.: Equivalence of queries combining set and bag-set semantics. In: Vansummeren, S. (ed.) Proceedings of the Twenty-Fifth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 26-28, 2006, Chicago, Illinois, USA. pp. 70–79. ACM (2006). 10.1145/1142351.1142362
  * [9] Ding, H., Wang, Z., Yang, Y., Zhang, D., Xu, Z., Chen, H., Piskac, R., Li, J.: Proving query equivalence using linear integer arithmetic. Proc. ACM Manag. Data 1(4) (dec 2023), https://doi.org/10.1145/3626768
  * [10] Foundation, A.S.: Apache calcite (2014), https://calcite.apache.org/docs/, accessed on Feb 25, 2024
  * [11] Garcia-Molina, H., Ullman, J.D., Widom, J.: Database Systems: The Complete Book. Prentice Hall Press, USA, 2 edn. (2008)
  * [12] Group, G.T.D.: Calcite benchmarks (2020), https://github.com/georgia-tech-db/spes/blob/main/testData/calcite˙tests.json, accessed on Feb 25, 2024
  * [13] Group, T.P.G.D.: Postgresql (2024), https://www.postgresql.org/, accessed on Feb 25, 2024
  * [14] Ioannidis, Y.E., Ramakrishnan, R.: Containment of conjunctive queries: beyond relations as sets. ACM Trans. Database Syst. 20(3), 288–324 (sep 1995), https://doi.org/10.1145/211414.211419
  * [15] Levatich, M., Bjørner, N., Piskac, R., Shoham, S.: Solving $\text{LIA}^{\star}$ using approximations. In: Beyer, D., Zufferey, D. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 360–378. Springer International Publishing, Cham (2020)
  * [16] Logozzo, F., Peled, D.A., Zuck, L.D.: Decision procedures for multisets with cardinality constraints. In: VMCAI, Lecture Notes in Computer Science, vol. 4905, pp. 218–232. Springer Berlin / Heidelberg, Germany (2008)
  * [17] Meng, B., Reynolds, A., Tinelli, C., Barrett, C.W.: Relational constraint solving in SMT. In: de Moura, L. (ed.) Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10395, pp. 148–165. Springer (2017). 10.1007/978-3-319-63046-5_10, https://doi.org/10.1007/978-3-319-63046-5_10
  * [18] Reynolds, A., Viswanathan, A., Barbosa, H., Tinelli, C., Barrett, C.W.: Datatypes with shared selectors. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10900, pp. 591–608. Springer (2018), https://doi.org/10.1007/978-3-319-94205-6_39
  * [19] Sheng, Y., Nötzli, A., Reynolds, A., Zohar, Y., Dill, D., Grieskamp, W., Park, J., Qadeer, S., Barrett, C., Tinelli, C.: Reasoning about vectors using an smt theory of sequences. In: Blanchette, J., Kovács, L., Pattinson, D. (eds.) Automated Reasoning. pp. 125–143. Springer International Publishing, Cham (2022)
  * [20] Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., Barrett, C.W.: Politeness for the theory of algebraic datatypes. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12166, pp. 238–255. Springer (2020), https://doi.org/10.1007/978-3-030-51074-9_14
  * [21] Veanes, M., Grigorenko, P., de Halleux, P., Tillmann, N.: Symbolic query exploration. In: Formal Methods and Software Engineering, pp. 49–68. Lecture Notes in Computer Science, Springer Berlin Heidelberg, Berlin, Heidelberg (2009)
  * [22] Zarba, C.G.: Combining multisets with integers. In: Voronkov, A. (ed.) Automated Deduction—CADE-18. pp. 363–376. Springer Berlin Heidelberg, Berlin, Heidelberg (2002)
  * [23] Zhou, Q., Arulraj, J., Navathe, S., Harris, W., Xu, D.: Automated verification of query equivalence using satisfiability modulo theories. Proceedings of the VLDB Endowment 12(11), 1276–1288 (2019)
  * [24] Zhou, Q., Arulraj, J., Navathe, S.B., Harris, W., Wu, J.: A symbolic approach to proving query equivalence under bag semantics. CoRR abs/2004.00481 (2020), https://arxiv.org/abs/2004.00481

##  .7 Proofs for Tables Theory

###  .7.1 Proof of Lemma 0.2.1

See 0.2.1

###### Proof.

$\varphi$ can be transformed into an equisatisfiable disjunctive normal form
$\varphi_{1}\vee\dots\vee\varphi_{n}$ using standard techniques, where
$\varphi_{i}$ is a conjunction of $\varphi_{i}^{1},\dots,\varphi_{i}^{k_{i}}$
of literals for $i\in[1,n]$. Each literal is either a table constraint, an
arithmetic constraint, or an element constraint. For each $i\in[1,n]$ define:

$\displaystyle\mathsf{B}_{i}$
$\displaystyle=\\{\varphi_{i}^{j}\;|\;\varphi_{i}^{j}\text{ is a table
constraint}\\}$ $\displaystyle\mathsf{A}_{i}$
$\displaystyle=\\{\varphi_{i}^{j}\;|\;\varphi_{i}^{j}\text{ is an arithmetic
constraint}\\}$ $\displaystyle\mathsf{E}_{i}$
$\displaystyle=\\{\varphi_{i}^{j}\;|\;\varphi_{i}^{j}\text{ is an element
constraint}\\}$

where $j\in[1,k_{i}]$ for each $i\in[1,n]$. It is clear that $\varphi$ is
satisfiable if and only if
$\mathsf{B}_{i}\cup\mathsf{A}_{i}\cup\mathsf{E}_{i}$ is satisfiable for some
$i\in[1,n]$. ∎

###  .7.2 Proof of Lemma 0.2.2

See 0.2.2 It follows from Lemma 0.2.2 that if all children of a configuration
$C$ are unsatisfiable, then $C$ is unsatisfiable. Hence by induction on the
structure of the derivation tree, if a derivation tree of root $c_{0}$ is
closed, then $c_{0}$ itself is $\mathbb{T}_{\mathsf{Tab}}$-unsatisfiable. In
the proofs, we abuse the notation $\mathsf{m}(e,s)$ to denote multiplicity
term in the syntax, and also denote multiplicity in the interpretation.

###### Proof.

Suppose $c=(\mathsf{A},\mathsf{B},\mathsf{E})$ is satisfied by an
interpretation $\mathcal{I}$, we show that it also satisfies at least one
child
$c^{\prime}=(\mathsf{A}^{\prime},\mathsf{B}^{\prime},\mathsf{E}^{\prime})$ of
$C$. This is clear for communication rules B-A-Prop, B-E-Prop, E-Ident, and
A-Prop which only add equality constraints satisfied by $\mathcal{I}$. For
rule Diseq, every model that satisfies $s\not\approx t$, there exists an
element $z$ in $\mathcal{I}(\varepsilon)$ that witnesses this disequality such
that $\mathsf{m}(z,\mathcal{I}(s))\neq\mathsf{m}(z,\mathcal{I}(t))$.
$c^{\prime}$ is satisfiable by interpreting the fresh variable $w$ as
$\mathcal{I}(w)=z$. In rules Nonneg and Empty, $c^{\prime}$ is satisfiable
from the semantics of $\mathsf{m}(e,s)$ and $\varnothing_{\varepsilon}$ in
Section 0.2. For Cons1, the model value $\mathcal{I}(\mathsf{bag}(e,n))$ is
either empty or nonempty. If it is the former, it must be the case that
$\mathcal{I}(n)\leq 0$, and hence the left branch is satisfiable. The right
branch is satisfied by the latter. For Cons2, if $x\not\approx
e\in\mathsf{B}^{*}$ then $\mathcal{I}(x\not\approx e)=true$, which means
$\mathcal{I}(x)\neq\mathcal{I}(e)$ holds. Therefore, any child branch
$c^{\prime}$ is satisfied because
$\mathcal{I}(\mathsf{m}(x,\mathsf{bag}(e,n)))=0$. We skip the proofs for rules
Disj Union, Max Union, Inter, Diff Sub, Setof since they are quite similar to
the cases above. For rule Prod Up, suppose $\mathcal{I}(\mathsf{m}(\langle
x_{1},\dots,x_{m}\rangle,s))=i$ and $\mathcal{I}(\mathsf{m}(\langle
y_{1},\dots,y_{n}\rangle,t))=j$. Then the conclusion is satisfied by
$\mathcal{I}(\mathsf{m}(\langle
x_{1}^{\mathcal{I}},\dots,x_{m}^{\mathcal{I}},y_{1}^{\mathcal{I}},\dots,y_{n}^{\mathcal{I}}\rangle,s\otimes
t))=i*j$. The proofs of the remaining rules are similar.

For the other direction, suppose a child configuration $c^{\prime}$ is
satisfiable. In all rules, we have $\mathsf{E}\subseteq\mathsf{E}^{\prime}$.
So if $\mathsf{E}^{\prime}$ is satisfiable, then $\mathsf{E}$ is also
satisfiable. Similarly, we have $\mathsf{A}\subseteq\mathsf{A}^{\prime}$ and
$\mathsf{B}\subseteq\mathsf{B}^{\prime}$. Therefore, $C$ is satisfiable. ∎

######  Corollary .7.1.

If a leaf in a derivation tree is satisfiable, then the root $c_{0}$ is
satisfiable.

###### Proof.

This follows by induction from Lemma 0.2.2. ∎

###  .7.3 Proof of Proposition 0.2.3

See 0.2.3

###### Proof.

We prove by induction on the structure of the derivation tree. Suppose
$c=(\mathsf{A},\mathsf{B},\mathsf{E})$ is closed. Then all leaves are
$\mathsf{unsat}$. For the base case, suppose $c^{\prime}$ is the deepest leaf.
Then it is $\mathsf{unsat}$ because of our assumption.

For the inductive case, suppose all children of a configuration $C$ are
unsatisfiable. Then $C$ must be unsatisfiable because if it is not, then from
Lemma 0.2.2 one of its children is satisfiable which is a contradiction.

We conclude that $C$ is $\mathbb{T}_{\mathsf{Tab}}$-unsatisfiable. ∎

###  .7.4 Proof of Proposition 0.2.4

See 0.2.4

To prove Proposition 0.2.4, we build a model $\mathcal{I}$ of
$\mathbb{T}_{\mathsf{Tab}}$ that satisfies $C$ by construction. Then, we can
argue that $C_{0}$ is satisfiable by Corollary .7.1.

Consider a saturated configuration $C=(\mathsf{A},\mathsf{B},\mathsf{E})$. We
define an interpretation $\mathcal{I}$ that satisfies
$\mathsf{A}\cup\mathsf{B}\cup\mathsf{E}$. The following definitions completely
define the model $\mathcal{I}$. Concretely, Definition .7.1 defines the
domains of $\mathcal{I}$; Definition .7.2 defines the function symbols of
$\Sigma_{\mathsf{Tab}}$; Definition .7.3 defines the interpretations of
variables of sort $\mathsf{Int}$ and $\varepsilon$; Finally, Definition .7.4
defines the interpretations of variables of sort $\mathsf{Bag}$. We start by
assigning domains to the sorts of $\mathbb{T}_{\mathsf{Tab}}$.

######  Definition .7.1 (Model construction: domains).

  1. 1.

$\mathcal{I}(\mathsf{Int})=\mathbb{Z}$, the set of integers.

  2. 2.

$\mathcal{I}(\varepsilon)$ is some countably infinite set.

  3. 3.

$\mathcal{I}(\mathsf{Bag})$ is the set of finite bags whose elements are taken
from $\mathcal{I}(\varepsilon)$.

The exact identity of $\varepsilon$ is not important, and so we set its
elements to be arbitrary. In contrast, its cardinality is important, and is
set to be infinite.

######  Definition .7.2 (Model construction: function symbols).

The symbols shown in Figure 1 are interpreted in such a way that $\mathcal{I}$
is both a $\mathbb{T}_{\mathsf{\mathsf{NIA}}}$-interpretation and a
$\mathbb{T}_{\mathsf{Tab}}$-interpretation, as described in Figure 1 and in
Section 0.2.

Now we assign values to variables of sort $\mathsf{Int}$ and $\varepsilon$.

######  Definition .7.3 (Model construction: $\mathsf{Int}$ and $\varepsilon$
variables).

  1. 1.

Let $\mathcal{A}$ be a $\mathbb{T}_{\mathsf{\mathsf{NIA}}}$-interpretation
with $\mathcal{A}(\mathsf{Int})=\mathbb{Z}$ that satisfies $\mathsf{A}$. Then
$\mathcal{I}(x):=\mathcal{A}(x)$ for every variable $x$ of sort
$\mathsf{Int}$.

  2. 2.

We consider equivalence classes defined as follows: two terms $t_{1},t_{2}$
are in the same equivalence class if
$\mathsf{B}\models_{\mathsf{Tup}}t_{1}\approx t_{2}$. Let $a_{1},a_{2},\ldots$
be an enumeration of $\mathcal{I}(\varepsilon)$, and let $e_{1},\ldots,e_{n}$
be an enumeration of the equivalence classes of $\equiv_{\mathsf{B}}$ whose
variables have sort $\varepsilon$. Then, for every $i\in[1,n]$ and every
variable $x\in e_{i}$, $\mathcal{I}(x):=a_{i}$.

We now turn to assigning values to variables of sort $\mathsf{Bag}$. We
interpret them as a set of pairs $\langle e,n\rangle$ where $e\in
I(\varepsilon)$ and $n$ is a positive integer. We use $\cup$ to denote the
union operation over sets. Likewise, we define the disjoint union $\uplus$ of
these sets as follows:

$\displaystyle u\uplus v$ $\displaystyle:=\;\\{\langle e,n\rangle\mid\langle
e,n\rangle\in u,\langle e,m\rangle\notin v\text{ for all }m\\}\;\cup$
$\displaystyle\qquad\\{\langle e,n\rangle\mid\langle e,n\rangle\in v,\langle
e,m\rangle\notin u\text{ for all }m\\}\;\cup$ $\displaystyle\qquad\\{\langle
e,n\rangle\mid\langle e,n_{1}\rangle\in u,\langle e,n_{2}\rangle\in
v,n=n_{1}+n_{2}\\}$ (3)

######  Definition .7.4 (Model construction: $\mathsf{Bag}$ terms).

For any variable $s\in\mathrm{Vars}(\mathsf{B})$ of sort $\mathsf{Bag}$, and
every $e$ of sort $\varepsilon$,

$\displaystyle\mathcal{I}(s)$
$\displaystyle:=\\{\langle\mathcal{I}(e),\mathcal{I}(\mathsf{m}(e,s))\rangle\mid{\mathsf{m}(e,s)\in\mathcal{T}(\mathsf{B}^{*})},\mathcal{I}(\mathsf{m}(e,s))>0\\}.$
(4)

There is no cycle in 4 since $\mathcal{I}(\mathsf{m}(e,s))$ is an integer that
has already been assigned a numeral in Definition .7.3. It does not matter
which element is picked from its equivalence class since $e_{1}\approx e_{2}$
implies
$\langle\mathcal{I}(e_{1}),\mathcal{I}(\mathsf{m}(e_{1},s))\rangle=\langle\mathcal{I}(e_{2}),\mathcal{I}(\mathsf{m}(e_{2},s))\rangle$
from Definition .7.3 and 1. Equation 4 is well-defined as we prove below that
$s\approx t$ implies $\mathcal{I}(s)=\mathcal{I}(t)$.

We define the interpretation of other terms inductively as follows:

$\displaystyle\mathcal{I}(\varnothing_{\varepsilon})$
$\displaystyle:=\;\\{\\}$ $\displaystyle\mathcal{I}(\mathsf{bag}(e,n))$
$\displaystyle:=\;\\{\langle\mathcal{I}(e),\mathcal{I}(n)\rangle\mid\mathcal{I}(n)>0\\}$
$\displaystyle\mathcal{I}(s\sqcup t)$ $\displaystyle:=\;\\{\langle
e,n\rangle\mid\langle e,n\rangle\in\mathcal{I}(s),\langle
e,m\rangle\notin\mathcal{I}(t)\text{ for all }m\\}\;\cup$
$\displaystyle\qquad\\{\langle e,n\rangle\mid\langle
e,n\rangle\in\mathcal{I}(t),\langle e,m\rangle\notin\mathcal{I}(s)\text{ for
all }m\\}\;\cup$ $\displaystyle\qquad\\{\langle e,n\rangle\mid\langle
e,n_{1}\rangle\in\mathcal{I}(s),\langle
e,n_{2}\rangle\in\mathcal{I}(t),n=\max(n_{1},n_{2})\\}$
$\displaystyle\mathcal{I}(s\mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}t)$
$\displaystyle:=\;\mathcal{I}(s)\uplus\mathcal{I}(t)$
$\displaystyle\mathcal{I}(s\sqcap t)$ $\displaystyle:=\;\\{\langle
e,n\rangle\mid\langle e,n_{1}\rangle\in\mathcal{I}(s),\langle
e,n_{2}\rangle\in\mathcal{I}(t),n=\min(n_{1},n_{2})\\}$
$\displaystyle\mathcal{I}(s\setminus t)$ $\displaystyle:=\;\\{\langle
e,n\rangle\mid\langle e,n\rangle\in\mathcal{I}(s),\langle
e,m\rangle\notin\mathcal{I}(t)\text{ for all }m\\}\;\cup$
$\displaystyle\qquad\\{\langle e,n\rangle\mid\langle
e,n_{1}\rangle\in\mathcal{I}(s),\langle
e,n_{2}\rangle\in\mathcal{I}(t),n=n_{1}-n_{2},n>0\\}$
$\displaystyle\mathcal{I}(s\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}t)$
$\displaystyle:=\;\\{\langle e,n\rangle\mid\langle
e,n\rangle\in\mathcal{I}(s),\langle e,m\rangle\notin\mathcal{I}(t)\text{ for
all }m\\}$ $\displaystyle\mathcal{I}(\mathsf{setof}(s))$
$\displaystyle:=\;\\{\langle e,1\rangle\mid\langle
e,n\rangle\in\mathcal{I}(s)\\}$ $\displaystyle\mathcal{I}(s\otimes t)$
$\displaystyle:=\;\\{\langle(e_{1},e_{2}),n\rangle\mid\langle
e_{1},n_{1}\rangle\in\mathcal{I}(s),\langle
e_{2},n_{2}\rangle\in\mathcal{I}(t),n=n_{1}\times n_{2}\\}$
$\displaystyle\mathcal{I}(\sigma(p,s))$ $\displaystyle:=\;\\{\langle
e,n\rangle\mid\langle e,n\rangle\in\mathcal{I}(s),\mathcal{I}(p)(e)\\}$
$\displaystyle\mathcal{I}(\pi(f,s))$ $\displaystyle:=\;\biguplus_{\langle
e,n\rangle\in\mathcal{I}(s)}\\{\langle\mathcal{I}(f)(e),n\rangle\\}$

where $(e_{1},e_{2})$ in $\mathcal{I}(s\otimes t)$ is a shorthand for the
concatenation of elements of tuple $e_{1}$ and elements of tuple $e_{2}$, and
$e_{1_{i_{k}}},e_{2_{j_{k}}}$ are elements at positions $i_{k},j_{k}$ in
tuples $e_{1},e_{2}$ respectively. The interpretation of
$s\bowtie_{i_{1}j_{1}\cdots i_{p}j_{p}}t$ and
$\mathsf{table.proj}_{i_{1},\dots,i_{k}}(s)$ are skipped since the former is
reduced to a filter of a product, and the latter is reduced to a map term.

######  Proposition .7.2 ($\mathcal{I}$ is a model).

If a configuration $C=(\mathsf{A},\mathsf{B},\mathsf{E})$ is saturated, then
the interpretation $\mathcal{I}$ defined in Definitions .7.1 to .7.4 satisfies
all constraints in $\mathsf{A}\cup\mathsf{B}\cup\mathsf{E}$.

###### Proof.

It is clear from construction of $\mathcal{I}$ that it satisfies all
constraints in $\mathsf{A}\cup\mathsf{E}$. It also satisfies (dis)equalities
in $\mathsf{B}$ of terms with sorts $\mathsf{E}$ and $\mathsf{Int}$ since
these constraints are in $\mathsf{A}\cup\mathsf{E}$. So we focus here on
(dis)equalities in $\mathsf{B}$ of terms with $\mathsf{Bag}$ sorts. We assume
for every non-variable bag term $t^{\prime}\in\mathcal{T}(\mathsf{B}^{*})$,
there exists a variable $t$ such that $t\approx t^{\prime}\in\mathsf{B}^{*}$.
This assumption is without loss of generality as any set of constraints can
easily be transformed into an equisatisfiable set satisfying the assumption by
the addition of fresh variables and equalities. For constraints $s\approx t$,
we prove by induction on the structure of $t$ that
$\mathcal{I}(s)=\mathcal{I}(t)$. We show this for each case of $t$. In the
proofs below, we assume $s,t,u$ are variables.

  1. 1.

$s\approx t$ where $t$ is a variable. The proof is by contradiction. Suppose
$\mathcal{I}(s)\neq\mathcal{I}(t)$. This means there exists a pair
$\langle\mathcal{I}(e),\mathcal{I}(\mathsf{m}(e,t))\rangle$ in
$\mathcal{I}(t)$ and not in $\mathcal{I}(s)$ or vice versa. We prove the first
case, and the proof for the second case is similar. Suppose
$\langle\mathcal{I}(e),\mathcal{I}(\mathsf{m}(e,t))\rangle\in\mathcal{I}(t)$
and
$\langle\mathcal{I}(e),\mathcal{I}(\mathsf{m}(e,t))\rangle\notin\mathcal{I}(s)$.
From the definition of $\mathcal{I}(t)$, we have
$\mathsf{m}(e,t)\in\mathcal{T}(\mathsf{B}^{*})$ such that
$\mathcal{I}(\mathsf{m}(e,t))>0$. Since $s\approx t$, from the definition of
$\mathsf{B}^{*}$ in 1 we have $\mathsf{m}(e,s)\in\mathcal{T}(\mathsf{B}^{*})$
and $\mathsf{m}(e,s)\approx\mathsf{m}(e,t)\in\mathsf{B}^{*}$. Now the
constraint $\mathsf{m}(e,s)\approx\mathsf{m}(e,t)\in\mathsf{A}$, because
otherwise $C$ is not saturated and we can apply rule B-A-Prop. Therefore,
$\mathcal{I}(\mathsf{m}(e,s))=\mathcal{I}(\mathsf{m}(e,t))$. Now from the
definition of $\mathcal{I}(s)$ we have
$\langle\mathcal{I}(e),\mathcal{I}(\mathsf{m}(e,s))\rangle=\langle\mathcal{I}(e),\mathcal{I}(\mathsf{m}(e,t))\rangle\in\mathcal{I}(s)$
which contradicts
$\langle\mathcal{I}(e),\mathcal{I}(\mathsf{m}(e,t))\rangle\notin\mathcal{I}(s)$.

  2. 2.

$s\approx\varnothing_{\varepsilon}$. Suppose by contradiction that
$\mathcal{I}(s)\neq\mathcal{I}(\varnothing_{\varepsilon})=\\{\\}$. This means
there exists a pair
$\langle\mathcal{I}(e),\mathcal{I}(\mathsf{m}(e,s))\rangle\in\mathcal{I}(s)$.
The constraint $\mathsf{m}(e,s)\approx 0\in\mathsf{A}$ because otherwise, $C$
is not saturated, and we can apply rule Empty to add it to $\mathsf{A}$. This
means $\mathcal{I}(\mathsf{m}(e,s))=0$ and therefore,
$\langle\mathcal{I}(e),\mathcal{I}(\mathsf{m}(e,s))\rangle\notin\mathcal{I}(s)$
which contradicts our assumption
$\langle\mathcal{I}(e),\mathcal{I}(\mathsf{m}(e,s))\rangle\in\mathcal{I}(s)$.

  3. 3.

$s\approx\mathsf{bag}(e,n)$. Here we have two cases depending on whether
$1\leq\mathcal{I}(n)$:

    1. (a)

$\mathcal{I}(n)\leq 0$ which means $\mathcal{I}(\mathsf{bag}(e,n))=\\{\\}$. It
must be the case that $n\leq 0\in\mathsf{A}$ and
$s\approx\varnothing_{\varepsilon}\in\mathsf{B}$ because otherwise we can
apply rule Cons1 to add these constraints. From
$s\approx\varnothing_{\varepsilon}\in\mathsf{B}$ we have already proven
$\mathcal{I}(s)=\\{\\}$ in the previous step. We can not apply the right
branch of the rule because it adds the constraint $1\leq n$ to $\mathsf{A}$
which is not satisfied by $\mathcal{I}(n)\leq 0$.

    2. (b)

$1\leq\mathcal{I}(n)$ which means
$\mathcal{I}(\mathsf{bag}(e,n))=\\{\langle\mathcal{I}(e),\mathcal{I}(n)\rangle\\}$.
Suppose $\mathcal{I}(s)\neq\\{\langle\mathcal{I}(e),\mathcal{I}(n)\rangle\\}$.
This implies either
$\langle\mathcal{I}(e),\mathcal{I}(n)\rangle\notin\mathcal{I}(s)$ or there
exists an element $x$ such that
$\langle\mathcal{I}(x),\mathcal{I}(\mathsf{m}(x,s))\rangle\in\mathcal{I}(s)$
and
$\langle\mathcal{I}(x),\mathcal{I}(\mathsf{m}(x,s))\rangle\notin\\{\langle\mathcal{I}(e),\mathcal{I}(n)\rangle\\}$

       * •

Suppose $\langle\mathcal{I}(e),\mathcal{I}(n)\rangle\notin\mathcal{I}(s)$.
Note that this condition also includes the case
$\langle\mathcal{I}(e),m\rangle\in\mathcal{I}(s),\mathcal{I}(n)\neq m$. We
have the constraints $1\leq n,\mathsf{m}(e,s)\approx n$ in $\mathsf{A}$
because otherwise $C$ is not saturated, and we can apply the Cons1. This means
$\mathcal{I}(\mathsf{m}(e,s))=\mathcal{I}(n)$ which implies
$\langle\mathcal{I}(e),\mathcal{I}(n)\rangle\in\mathcal{I}(s)$. This
contradicts our assumption. We can not apply the left branch because it adds
the constraint $n\leq 0$ which is not satisfied by $1\leq\mathcal{I}(n)$.

       * •

Suppose there exists an element $x$ such that
$\langle\mathcal{I}(x),\mathcal{I}(\mathsf{m}(x,s))\rangle\in\mathcal{I}(s)$
and
$\langle\mathcal{I}(x),\mathcal{I}(\mathsf{m}(x,s))\rangle\notin\\{\langle\mathcal{I}(e),\mathcal{I}(n)\rangle\\}$.
From the definition of $\mathcal{I}(s)$ we have
$\mathsf{m}(x,s)\in\mathcal{T}(\mathsf{B}^{*})$, and hence
$x\in\mathcal{T}(\mathsf{B}^{*})$. We also know
$e\in\mathcal{T}(\mathsf{B}^{*})$ because the constraint
$s\approx\mathsf{bag}(e,n)\in\mathsf{B}$. Now either $x\approx e\in\mathsf{B}$
or $x\not\approx e\in\mathsf{B}$ because otherwise we can apply the splitting
rule E-Ident to $C$. Suppose $x\approx e\in\mathsf{B}$ which means
$\mathcal{I}(x)=\mathcal{I}(e)$. This implies
$\langle\mathcal{I}(e),\mathcal{I}(\mathsf{m}(e,s))\rangle\notin\\{\langle\mathcal{I}(e),\mathcal{I}(n)\rangle\\}$.
This means $\mathcal{I}(\mathsf{m}(e,s))\neq\mathcal{I}(n)$. This implies
$\langle\mathcal{I}(e),\mathcal{I}(n)\rangle\notin\mathcal{I}(s)$ which was
proved impossible in the previous case. Now suppose $x\not\approx
e\in\mathsf{B}$. Then, it must be the case that $\mathsf{m}(x,s)\approx
0\in\mathsf{A}$ because otherwise we can apply rule Cons2 to $C$. This implies
$\mathcal{I}(\mathsf{m}(x,s))=0$ which contradicts our assumption that
$\langle\mathcal{I}(x),\mathcal{I}(\mathsf{m}(x,s))\rangle\in\mathcal{I}(s)$
which requires $\mathcal{I}(\mathsf{m}(x,s))>0$.

We conclude $\mathcal{I}(s)=\mathcal{I}(\mathsf{bag}(e,n))$.

  4. 4.

$s\approx\mathsf{setof}(t)$. We want to show
$\mathcal{I}(s)=\mathcal{I}(\mathsf{setof}(t))$. We know from the definition
of $\mathcal{I}$ that
$\mathcal{I}(\mathsf{setof}(t))=\\{\langle\mathcal{I}(e),1\rangle\mid\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(t)\\}$.

    1. (a)

Suppose $\langle\mathcal{I}(e),1\rangle\in\mathcal{I}(\mathsf{setof}(t))$.
Since $t$ is a variable, we have
$\mathsf{m}(e,t)\in\mathcal{T}(\mathsf{B}^{*})$ and
$\mathcal{I}(\mathsf{m}(e,t))=n\geq 1$. Now $\mathsf{A}$ contain the
constraints $1\leq\mathsf{m}(e,t),\mathsf{m}(e,s)\approx 1$, because otherwise
we can apply rule Setof. The right branch can not be applied because it adds
the constraint $\mathsf{m}(e,t)\leq 0$ to $\mathsf{A}$ which is not satisfied
by $\mathcal{I}(\mathsf{m}(e,t))=n>0$. Therefore, $\mathsf{m}(e,s)\approx 1$
and $\mathcal{I}(\mathsf{m}(e,s))=1$. Therefore,
$\langle\mathcal{I}(e),1\rangle\in\mathcal{I}(s)$.

    2. (b)

For the other direction suppose
$\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(s)$. From the definition of
$\mathcal{I}(s)$, we have $\mathsf{m}(e,s)\in\mathcal{T}(\mathsf{B}^{*})$ and
$\mathcal{I}(\mathsf{m}(e,s))=n>0$. Now $\mathsf{A}$ contains the constraints
$1\leq\mathsf{m}(e,t),\mathsf{m}(e,s)\approx 1$ because otherwise we can apply
rule Setof and add them to $\mathsf{A}$ using the left branch. We can not
apply the right branch because it adds the constraint $\mathsf{m}(e,s)\approx
0$ which is not satisfied by $\mathcal{I}(\mathsf{m}(e,s))=n>0$. Therefore,
$\mathcal{I}(\mathsf{m}(e,s))=n=1$, and $1\leq\mathcal{I}(\mathsf{m}(e,t))$.
Hence,
$\langle\mathcal{I}(e),\mathcal{I}(\mathsf{m}(e,t))\rangle\in\mathcal{I}(t)$
which means $\langle\mathcal{I}(e),1\rangle\in\mathcal{I}(\mathsf{setof}(t))$.

We conclude $\mathcal{I}(s)=\mathcal{I}(\mathsf{setof}(t))$.

  5. 5.

$s\approx t\mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}u$. We want to show
$\mathcal{I}(s)=\mathcal{I}(t)\uplus\mathcal{I}(u)$.

    1. (a)

Suppose
$\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(t\mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}u)=\mathcal{I}(t)\uplus\mathcal{I}(u)$.
Since $t,u$ are variables, $\mathcal{T}(\mathsf{B}^{*})$ either contains
$\mathsf{m}(e,t)$ or $\mathsf{m}(e,u)$. Either way, $\mathsf{A}$ contains the
constraint $\mathsf{m}(e,s)\approx\mathsf{m}(e,t)+\mathsf{m}(e,u)$ because
otherwise we can apply rule Disj Union and add it to $\mathsf{A}$.
Furthermore, the three multiplicity terms are in $\mathcal{T}(\mathsf{B}^{*})$
because otherwise we can apply rule A-Prop to add the constraint to
$\mathsf{B}$. This means they are assigned values by the interpretation
$\mathcal{I}$ in $\mathcal{I}(s)$, $\mathcal{I}(t)$, and $\mathcal{I}(u)$.
Suppose $\mathcal{I}(\mathsf{m}(e,t))=n_{1}$,
$\mathcal{I}(\mathsf{m}(e,u))=n_{2}$ such that $n=n_{1}+n_{2}$. Now both
$n_{1},n_{2}$ are non-negative because rule Nonneg is saturated and
$0\leq\mathsf{m}(e,t),0\leq\mathsf{m}(e,u)\in\mathsf{A}$. Since $n>0$ we have
three cases that correspond to the three disjoint sets in the definition of
$\mathcal{I}(t)\uplus\mathcal{I}(u)$ in 3: $(n=n_{1},n_{2}=0)$,
$(n=n_{2},n_{1}=0)$ and $(n=n_{1}+n_{2},n_{1},n_{2}>0)$. In all cases, we have
$\mathcal{I}(\mathsf{m}(e,s))=\mathcal{I}(\mathsf{m}(e,t))+\mathcal{I}(\mathsf{m}(e,u))=n$.
Hence, $\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(s)$.

    2. (b)

Suppose $\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(s)$. From the definition
of $\mathcal{I}(s)$ we have $\mathsf{m}(e,s)\in\mathcal{T}(\mathsf{B}^{*})$.
Now $\mathsf{A}$ has the constraint
$\mathsf{m}(e,s)\approx\mathsf{m}(e,t)+\mathsf{m}(e,u)$ because otherwise we
can apply rule Disj Union and add it to $\mathsf{A}$. The arithmetic solver
must satisfy this constraint, and we have
$\mathcal{I}(\mathsf{m}(e,s))=\mathcal{I}(\mathsf{m}(e,t))+\mathcal{I}(\mathsf{m}(e,u))=n$.
Suppose $\mathcal{I}(\mathsf{m}(e,t))=n_{1}$,
$\mathcal{I}(\mathsf{m}(e,u))=n_{2}$ such that $n=n_{1}+n_{2}$. We know
$n_{1},n_{2}$ are non-negative because of the saturation of rule Nonneg. There
are 3 cases: $(n=n_{1},n_{2}=0)$, $(n=n_{2},n_{1}=0)$ and
$(n=n_{1}+n_{2},n_{1},n_{2}>0)$. In all cases we have
$\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(t\mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}u)$ from the definition of
$\mathcal{I}(t\mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}u)$.

We conclude $\mathcal{I}(s)=\mathcal{I}(t)\uplus\mathcal{I}(u)$.

  6. 6.

The proofs for other cases
$\sqcup,\sqcap,\setminus,\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}},\otimes$
are quite similar to the proof of $\mathbin{\ooalign{$\sqcup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}$.

  7. 7.

$s\approx\sigma(p,t)$. Here we assume all element constraints of the form
$p(e)$ or $\neg p(e)$ are satisfied by $\mathcal{I}$.

    1. (a)

Suppose $\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(\sigma(p,t))$. From the
definition of $\mathcal{I}(\sigma(p,t))$ we have
$\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(t)$ and
$\mathcal{I}(p)(\mathcal{I}(e))$. From the definition of $\mathcal{I}(t)$, we
have
$\mathsf{m}(e,t)\in\mathcal{T}(\mathsf{B}^{*}),\mathcal{I}(\mathsf{m}(e,t))>0$.
Now $\mathsf{m}(e,s)\approx\mathsf{m}(e,t)\in\mathsf{A},p(e)\in\mathsf{E}$
because otherwise we can apply rule Filter Up. We can not apply the second
branch because the constraint $\neg p(e)$ is not satisfied by $\mathcal{I}$.
Hence, $\mathcal{I}(\mathsf{m}(e,s))=\mathcal{I}(\mathsf{m}(e,t))=n$ and
$\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(s)$.

    2. (b)

Suppose $\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(s)$. From the definition
of $\mathcal{I}(s)$, $\mathsf{m}(e,s)\in\mathcal{T}(\mathsf{B}^{*})$ and
$\mathcal{I}(\mathsf{m}(e,s))=n>0$. Now we have
$\mathsf{m}(e,t)\approx\mathsf{m}(e,s)\in\mathsf{A},p(e)\in\mathsf{E}$ because
otherwise we can apply rule Filter Down. The constraints in $\mathsf{E}$ are
satisfied because $C$ is saturated, and we can not apply rule E-Conf. Hence,
$n=\mathcal{I}(\mathsf{m}(e,s))=\mathcal{I}(\mathsf{m}(e,t))$ and
$\mathcal{I}(p)(e)$ holds. Therefore,
$\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(\sigma(p,t))$.

We conclude $\mathcal{I}(s)=\mathcal{I}(\sigma(p,t))$.

  8. 8.

$s\approx\pi(f,t)$. We have two cases for $f$:

    1. (a)

$f$ is injective. We want to show $\mathcal{I}(s)=\mathcal{I}(\pi(f,t))$.

      1. i.

Suppose $\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(\pi(f,t))$. From the
definition of $\mathcal{I}(\pi(f,t))$, there exists $x$ such that
$\mathcal{I}(f)(\mathcal{I}(x))=\mathcal{I}(f(x))=\mathcal{I}(e)$, and
$\langle\mathcal{I}(x),n\rangle\in\mathcal{I}(t)$ since $f$ is injective and
$\mathcal{I}(\mathsf{m}(x,t))=n$. This implies
$\mathsf{m}(x,t)\in\mathcal{T}(\mathsf{B}^{*})$. Now
$\mathsf{m}(f(x),s)\in\mathcal{T}(\mathsf{B}^{*})$, and
$\mathcal{I}(\mathsf{m}(x,t))\leq\mathcal{I}(\mathsf{m}(f(x),s))\in\mathsf{A}$
because otherwise we can apply rule Map Up. Furthermore,
$\mathsf{m}(f(x),s)\approx\mathsf{m}(w,t)\in\mathsf{A},f(w)\approx
f(x)\in\mathsf{E}$ for some fresh $w$ because otherwise we can apply rule Inj
Map Down. Since $f$ is injective, it must be the case that $w\approx
x\in\mathsf{B}$ because otherwise we can apply the splitting rule E-Ident and
add it to $\mathsf{B}$. We could not have applied the right branch because $f$
is injective and $w\not\approx x$ implies $f(w)\not\approx f(x)$ which would
lead to a conflict. Now $w\approx x$ implies
$\mathcal{I}(\mathsf{m}(w,t))=\mathcal{I}(\mathsf{m}(x,t))=n$ from 1. This
means $\mathcal{I}(\mathsf{m}(f(x),s))=\mathcal{I}(\mathsf{m}(w,t))=n$ and
hence $\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(s)$.

      2. ii.

Suppose $\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(s)$. From the definition
of $\mathcal{I}(s)$, we have $\mathsf{m}(e,s)\in\mathcal{T}(\mathsf{B}^{*})$.
Now $\mathsf{m}(e,s)\approx\mathsf{m}(w,t)\in\mathsf{A},f(w)\approx
e\in\mathsf{E}$ for some fresh $w$ because otherwise we can apply rule Inj Map
Down. This means $\mathcal{I}(\mathsf{m}(e,s))=\mathcal{I}(\mathsf{m}(w,t))=n$
and, therefore, $\langle\mathcal{I}(w),n\rangle\in\mathcal{I}(t)$. Since $f$
is injective,
$\langle\mathcal{I}(f)(\mathcal{I}(w)),n\rangle\in\mathcal{I}(\pi(f,t))$ which
means $\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(\pi(f,t))$.

    2. (b)

$f$ is not injective. Here, we assume the quantifier subsolver terminated
satisfying the formula below which constrains the functions $\mathit{ind}$ and
$\mathit{sum}$ derived from constraint 2. We also assume that all instantiated
terms, and constraints related to $\mathbb{T}_{\mathsf{Tab}}$ have been added
to configuration $C$.

$\displaystyle\begin{array}[]{ll}\forall\,x,i.&1\leq
i\leq\mathit{delem}(t)\wedge i\approx\mathit{ind}(x,t)\rightarrow\\\
&\quad\mathsf{m}(x,t)\geq 1\\\ &\wedge\left(\begin{pmatrix}e\approx
f(x)\;\wedge\\\
\mathit{sum}(e,t,i)\approx\mathit{sum}(e,t,i-1)+\mathsf{m}(x,t)\end{pmatrix}\vee\begin{pmatrix}e\not\approx
f(x)\;\wedge\\\
\mathit{sum}(e,t,i)\approx\mathit{sum}(e,t,i-1)\end{pmatrix}\right)\\\
&\wedge\;\forall\,y,j\;.\;i<j\leq\mathit{delem}(t)\wedge
j\approx\mathit{ind}(y,t)\rightarrow x\not\approx y\end{array}$ (9)

      1. i.

Suppose $\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(\pi(f,t))$. We want to
show that $\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(s)$. Recall
$\mathcal{I}(\pi(f,t)):=\;\biguplus_{\langle
e,n\rangle\in\mathcal{I}(t)}\\{\langle\mathcal{I}(f)(e),n\rangle\\}$. Then,
there exists at least a pair $\langle y,n_{y}\rangle\in\mathcal{I}(t)$ such
that $\mathcal{I}(f)(y)=\mathcal{I}(e)$. From the definition of
$\mathcal{I}(t)$ there exists $x$ such that
$\mathsf{m}(x,t)\in\mathcal{T}(\mathsf{B}^{*})$, $\mathcal{I}(x)=y$, and
$\mathcal{I}(\mathsf{m}(x,t))=n_{y}$. Now
$\mathsf{m}(f(x),s)\in\mathcal{T}(\mathsf{B}^{*})$, and
$\mathsf{m}(x,t)\leq\mathsf{m}(f(x),s)\in\mathsf{A}$ because otherwise we can
apply rule Map Up. The two terms $f(x),e\in\mathcal{T}(\mathsf{B}^{*})$ are
assigned the same value because
$\mathcal{I}(f(x))=\mathcal{I}(f)(\mathcal{I}(x))=\mathcal{I}(f)(y)=\mathcal{I}(e)$.
From Definition .7.3 they should be in the same equivalence class, which
implies $f(x)\approx e\in\mathsf{B}^{*}$. From the definition of
$\mathsf{B}^{*}$ in 1, we have
$\mathsf{m}(f(x),s)\in\mathcal{T}(\mathsf{B}^{*})$ and $f(x)\approx e$ which
implies $\mathsf{m}(e,s)\in\mathcal{T}(\mathsf{B}^{*})$. Now,
$\mathit{sum}(e,t,\mathit{delem}(t))\approx\mathsf{m}(e,s)\in\mathsf{A}$
because otherwise we can apply rule NotInj Down. We prove by contradiction
that $\mathcal{I}(\mathsf{m}(e,s))=n$. Suppose
$\mathcal{I}(\mathsf{m}(e,s))\neq n$, and hence,
$\mathcal{I}(\mathit{sum}(e,t,\mathit{delem}(t)))\neq n$. Let

$\displaystyle U=\\{$
$\displaystyle\langle\mathcal{I}(x),\mathcal{I}(\mathsf{m}(x,t))\rangle\mid$
$\displaystyle\mathcal{I}(f(x))\approx\mathcal{I}(e),i\approx\mathit{ind}(x,t),1\leq
i\leq\mathit{delem}(t),\mathsf{m}(x,t)\in\mathcal{T}(\mathsf{B}^{*})\\}.$

Then we have:

$\displaystyle\mathcal{I}(\mathsf{m}(e,s))$
$\displaystyle=\mathcal{I}(\mathit{sum}(e,t,\mathit{delem}(t)))$
$\displaystyle=\sum\limits_{\langle\mathcal{I}(x),\mathcal{I}(\mathsf{m}(x,t))\rangle\in
U}{\mathcal{I}(\mathsf{m}(x,t))}\neq n=\sum\limits_{\langle
y,n_{y}\rangle\in\mathcal{I}(t),\mathcal{I}(f)(y)=\mathcal{I}(e)}n_{y}.$

There are two possible reasons for the disequality:

        1. A.

There exists element $y$ such that $\langle
y,n_{y}\rangle\in\mathcal{I}(t),\mathcal{I}(f)(y)=\mathcal{I}(e),\langle
y,n_{y}\rangle\not\in U$. We show that this can not happen because $C$ is
saturated. $\langle y,n_{y}\rangle\in\mathcal{I}(t)$ implies there exists $x$
such that $\mathsf{m}(x,t)\in\mathcal{T}(\mathsf{B}^{*})$,
$\mathcal{I}(x)=y,\mathcal{I}(\mathsf{m}(x,t))=n_{y}$. Since we can not apply
rule NotInj Up, there exists $1\leq i\leq\mathit{delem}(t)$ such that
$i\approx\mathit{ind}(x,t)$. Furthermore,
$\mathcal{I}(f(x))=\mathcal{I}(f)(\mathcal{I}(x))=\mathcal{I}(f)(y)=\mathcal{I}(e)$.
This implies $\langle
y,n_{y}\rangle=\langle\mathcal{I}(x),\mathcal{I}(\mathsf{m}(x,t))\rangle\in
U$, which is a contradiction.

        2. B.

There exists $\langle\mathcal{I}(x),\mathcal{I}(\mathsf{m}(x,t))\rangle\in U$
such that $\mathcal{I}(f)(\mathcal{I}(x))=\mathcal{I}(e)$ but
$\langle\mathcal{I}(x),\mathcal{I}(\mathsf{m}(x,t))\rangle\not\in\mathcal{I}(t)$.
This means there exists $i$ such that $i\approx\mathit{ind}(x,t),1\leq
i\leq\mathit{delem}(t),\mathsf{m}(x,t)\in\mathcal{T}(\mathsf{B}^{*})$. We have
$\mathsf{m}(x,t)\geq 1$ from 9, which implies
$\mathcal{I}(\mathsf{m}(x,t))>0$. This means
$\langle\mathcal{I}(x),\mathcal{I}(\mathsf{m}(x,t))\rangle\in\mathcal{I}(t)$
from the definition of $\mathcal{I}(t)$, a contradiction.

Therefore, $\mathcal{I}(\mathsf{m}(e,s))=n$ and hence
$\langle\mathcal{I}(e),n\rangle\in\mathcal{I}(s)$.

      2. ii.

The proof for the other case is similar.

We conclude $\mathcal{I}(s)=\mathcal{I}(\pi(f,t))$.

We now switch to disequality constraints $s\not\approx t$. Without loss of
generality, we assume $s,t$ are bag variables, because if they are not, we can
convert the constraint to an equisatisfiable one that uses fresh variables
$s^{\prime}\approx s\wedge t^{\prime}\approx t\wedge s^{\prime}\not\approx
t^{\prime}$. Then
$\mathcal{I}(s^{\prime})=\mathcal{I}(s),\mathcal{I}(t^{\prime})=\mathcal{I}(t)$.
If $s\not\approx t\in\mathsf{B}^{*}$, we want to prove
$\mathcal{I}(s)\neq\mathcal{I}(t)$. For the sake of contradiction, suppose
$\mathcal{I}(s)=\mathcal{I}(t)$. This means

$\displaystyle\\{\langle\mathcal{I}(e),\mathcal{I}(\mathsf{m}(e,s))\rangle\mid{\mathsf{m}(e,s)\in\mathcal{T}(\mathsf{B}^{*})},\mathcal{I}(\mathsf{m}(e,s))>0\\}=$
$\displaystyle\\{\langle\mathcal{I}(e),\mathcal{I}(\mathsf{m}(e,t))\rangle\mid{\mathsf{m}(e,t)\in\mathcal{T}(\mathsf{B}^{*})},\mathcal{I}(\mathsf{m}(e,t))>0\\}.$

Now there exists an element term $w$ such that both $\mathsf{A},\mathsf{B}$
contain the constraint $\mathsf{m}(w,s)\not\approx\mathsf{m}(w,t)$ because
otherwise we can apply rule Diseq. This implies
$\mathcal{I}(\mathsf{m}(w,s))\neq\mathcal{I}(\mathsf{m}(w,t))$ and at least
one of them is positive because of the saturation of rule Nonneg. Without loss
of generality, suppose $\mathcal{I}(\mathsf{m}(w,s))>0$. This means
$\langle\mathcal{I}(w),\mathcal{I}(\mathsf{m}(w,s))\rangle\in\mathcal{I}(s)$
and
$\langle\mathcal{I}(w),\mathcal{I}(\mathsf{m}(w,s))\rangle\notin\mathcal{I}(t),$
which contradicts our assumption. We conclude
$\mathcal{I}(s)\neq\mathcal{I}(t)$. ∎

###  .7.5 Proof of Proposition 0.2.5

See 0.2.5

###### Proof.

We show that any tree starts with $C$ does not grow indefinitely. Let
$C=(\mathsf{A},\mathsf{B},\mathsf{E})$ and
$\mathcal{T}(\varepsilon_{c}),\mathcal{T}(\mathsf{Int}_{c}),\mathcal{T}(\mathsf{Bag}_{c})$
be all the finitely-many terms at $C$ of sorts
$\varepsilon,\mathsf{Int},\mathsf{Bag}$ respectively. Suppose
$e_{c},i_{c},b_{c}$ are the numbers of these terms respectively. None of the
calculus rules introduces new $\mathsf{Bag}$ terms. So $b_{c}$ remains the
same in all derivation trees with root $C$. Only rule Diseq generates new
$\varepsilon$ terms, but it is only applied once for each disequality
constraint. At the worst case all bag terms are distinct. So $e_{c}$ can
increase by at most $b_{c}^{2}$ terms in all derivation trees. Define
$e^{\prime}_{c}=e_{c}+b_{c}^{2}$. For multiplicity terms, assume each one of
the $e^{\prime}_{c}$ element terms occurs in a multiplicity term for each bag
term at the worst case. This means we have at most $m_{c}=e^{\prime}_{c}\times
b_{c}$ multiplicity terms. So the number of integer terms would be at most
$i^{\prime}_{c}=O(m_{c}^{2})+i_{c}$ with $O(m_{c}^{2})$ accounting for terms
introduced by binary arithmetic operators. We define the order relation
$\succ$ over configurations as follows:

  * •

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

  * •

$c\succ c^{\prime}$ if $c\neq\mathsf{unsat}$ and
$c^{\prime}\neq\mathsf{unsat}$ and $\langle
f_{1}(c),\dots,f_{17}(c)\rangle>_{lex}^{17}\langle
f_{1}(c^{\prime}),\dots,f_{17}(c^{\prime})\rangle$ where $f_{i}$ are the
ranking functions defined in Figure 11.

  * •

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

$f_{i}$ | Rule | Definition
---|---|---
$f_{1}$ | B-A-Prop | ${i^{\prime}}_{c}^{2}-\lvert\\{s\approx t\mid s\approx t\in\mathsf{A},s,t:\mathsf{Int}\\}\rvert$
$f_{2}$ | B-E-Prop | ${e^{\prime}_{c}}^{2}-\lvert\\{s\approx t\mid s\approx t\in\mathsf{E},s,t:\varepsilon\\}\rvert$
$f_{3}$ | E-Ident | $\begin{matrix}{e^{\prime}_{c}}^{2}-\lvert\\{s\approx t\mid s\approx t\in\mathsf{B},s,t:\varepsilon\\}\rvert-\lvert\\{s\not\approx t\mid s\approx t\in\mathsf{B},s,t:\varepsilon\\}\rvert\end{matrix}$
$f_{4}$ | A-Prop | ${i^{\prime}}_{c}^{2}-\lvert\\{s\approx t\mid s\approx t\in\mathsf{B},s,t:\mathsf{Int}\\}\rvert$
$f_{5}$ | Diseq | $b_{c}^{2}-\lvert\\{\mathsf{m}(w,s)\not\approx\mathsf{m}(w,t)\mid\mathsf{m}(w,s)\not\approx\mathsf{m}(w,t)\in\mathsf{A}\\}\rvert$
$f_{6}$ | Nonneg | $m_{c}-\lvert\\{\mathsf{m}(e,s)\mid 0\leq\mathsf{m}(e,s)\in\mathsf{A}\\}\rvert$
$f_{7}$ | Empty | $e^{\prime}_{c}\times b_{c}-\lvert\\{\mathsf{m}(e,s)\mid 0\approx\mathsf{m}(e,s)\in\mathsf{A}\\}\rvert$
$f_{8}$ | Cons1 | $\begin{array}[]{ll}b_{c}^{2}&-\lvert\\{s\approx\varnothing_{\varepsilon}\mid s\approx\varnothing_{\varepsilon}\in\mathsf{B},s\approx\mathsf{bag}(e,n)\in\mathsf{B}^{*}\\}\rvert\\\ &-\lvert\\{s\not\approx\varnothing_{\varepsilon}\mid s\not\approx\varnothing_{\varepsilon}\in\mathsf{B},s\approx\mathsf{bag}(e,n)\in\mathsf{B}^{*}\\}\rvert\end{array}$
$f_{9}$ | Cons2 | $m_{c}-\lvert\\{\mathsf{m}(e,s)\approx 0\mid\mathsf{m}(e,s)\approx 0\in\mathsf{A},s\approx\mathsf{bag}(e,n)\\}\rvert$
$f_{10}$ | Disj Union | $e^{\prime}_{c}\times b_{c}^{3}-\lvert\\{\varphi=\mathsf{m}(e,s)\approx\mathsf{m}(e,t)+\mathsf{m}(e,u)\mid\varphi\in\mathsf{A},s\approx t\mathbin{\ooalign{$\sqcup$\cr\hfil\raise 1.62747pt\hbox{$\scriptscriptstyle+$}\hfil\cr}}u\in\mathsf{B}^{*}\\}\rvert$
$f_{11}$ | Max Union | $e^{\prime}_{c}\times b_{c}^{3}-\lvert\\{\varphi=\mathsf{m}(e,s)\approx\max(\mathsf{m}(e,t),\mathsf{m}(e,u))\mid\varphi\in\mathsf{A},s\approx t\sqcup u\in\mathsf{B}^{*}\\}\rvert$
$f_{12}$ | Inter | $e^{\prime}_{c}\times b_{c}^{3}-\lvert\\{\varphi=\mathsf{m}(e,s)\approx\min(\mathsf{m}(e,t),\mathsf{m}(e,u))\mid\varphi\in\mathsf{A},s\approx t\sqcap u\in\mathsf{B}^{*}\\}\rvert$
$f_{13}$ | Diff Sub | $\begin{array}[]{ll}e^{\prime}_{c}\times b_{c}^{3}&-\lvert\\{\langle\varphi_{1},\varphi_{2}\rangle\mid\varphi_{1}=\mathsf{m}(e,t)\leq\mathsf{m}(e,u),\varphi_{2}=\mathsf{m}(e,s)\approx 0,\varphi_{i}\in\mathsf{A},s\approx t\setminus u\in\mathsf{B}^{*}\\}\rvert\\\ &-\lvert\\{\langle\varphi_{1},\varphi_{2}\rangle\mid\varphi_{1}=\mathsf{m}(e,t)>\mathsf{m}(e,u),\varphi_{2}=\mathsf{m}(e,s)\approx\mathsf{m}(e,t)-\mathsf{m}(e,u),\\\ &\qquad\varphi_{i}\in\mathsf{A},s\approx t\setminus u\in\mathsf{B}^{*}\\}\rvert\end{array}$
$f_{14}$ | Diff Rem | $\begin{array}[]{ll}e^{\prime}_{c}\times b_{c}^{3}&-\lvert\\{\langle\varphi_{1},\varphi_{2}\rangle\mid\varphi_{1}=\mathsf{m}(e,u)\approx 0,\varphi_{2}=\mathsf{m}(e,s)\approx\mathsf{m}(e,t),\varphi_{i}\in\mathsf{A},s\approx t\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}u\in\mathsf{B}^{*}\\}\rvert\\\ &-\lvert\\{\langle\varphi_{1},\varphi_{2}\rangle\mid\varphi_{1}=\mathsf{m}(e,u)\not\approx 0,\varphi_{2}=\mathsf{m}(e,s)\approx 0,\varphi_{i}\in\mathsf{A},s\approx t\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}u\in\mathsf{B}^{*}\\}\rvert\end{array}$
$f_{15}$ | Setof | $\begin{array}[]{l@{~}l}e^{\prime}_{c}\times b_{c}^{2}\hfil~{}&-\lvert\\{\langle\varphi_{1},\varphi_{2}\rangle\mid\varphi_{1}=1\leq\mathsf{m}(e,t),\varphi_{2}=\mathsf{m}(e,s)\approx 1,\varphi_{i}\in\mathsf{A},s\approx\mathsf{setof}(t)\in\mathsf{B}^{*}\\}\rvert\\\ \hfil~{}&{}-\lvert\\{\langle\varphi_{1},\varphi_{2}\rangle\mid\varphi_{1}=\mathsf{m}(e,t)\leq 0,\varphi_{2}=\mathsf{m}(e,s)\approx 0,\varphi_{i}\in\mathsf{A},s\approx\mathsf{setof}(t)\in\mathsf{B}^{*}\\}\rvert\end{array}$
$f_{16}$ | Filter Up | $\begin{array}[]{ll}e^{\prime}_{c}\times b_{c}^{2}&-\lvert\\{\langle\varphi_{1},\varphi_{2}\rangle\mid\varphi_{1}=p(e),\varphi_{2}=\mathsf{m}(e,s)\approx\mathsf{m}(e,t),\varphi_{1}\in\mathsf{E},\varphi_{2}\in\mathsf{A},s\approx\sigma(p,t)\in\mathsf{B}^{*}\\}\rvert\\\ &-\lvert\\{\langle\varphi_{1},\varphi_{2}\rangle\mid\varphi_{1}=\neg p(e),\varphi_{2}=\mathsf{m}(e,s)\approx 0,\varphi_{1}\in\mathsf{E},\varphi_{2}\in\mathsf{A},s\approx\sigma(p,t)\in\mathsf{B}^{*}\\}\rvert\end{array}$
$f_{17}$ | Filter Down | $e^{\prime}_{c}\times b_{c}^{2}-\lvert\\{\langle\varphi_{1},\varphi_{2}\rangle\mid\varphi_{1}=p(e),\varphi_{2}=\mathsf{m}(e,s)\approx\mathsf{m}(e,t),\varphi_{1}\in\mathsf{E},\varphi_{2}\in\mathsf{A},s\approx\sigma(p,t)\in\mathsf{B}^{*}\\}\rvert$
Figure 11: Ranking functions for table rules.

Each application of any rule would only decrease its corresponding function
and leave the other functions unchanged. In other words,
$f_{i}(c^{\prime})=f_{i}(c)-1$, and $f_{j}(c^{\prime})=f_{j}(c)$ for
$i,j\in[1,17],i\neq j$. It is clear that $c\succ c^{\prime}$. This means the
derivation tree is finite, and therefore the calculus with the above
assumptions is terminating. ∎

##  .8 Theory of Finite Relations

$\begin{array}[]{l}\begin{array}[]{@{}l@{\quad}l@{\quad}l@{\quad}l@{}}\hline\cr\hline\cr\textbf{Symbol}&\textbf{Arity}&\textbf{SMTLIB}&\textbf{Description}\\\
\hline\cr[\,]&\mathsf{Set}(\alpha)&\verb|set.empty|&\text{Empty set}\\\
[\,\text{-}\,]&\alpha\rightarrow\mathsf{Set}(\alpha)&\verb|set.singleton|&\text{Set
constructor}\\\
\sqcup&\mathsf{Set}(\alpha)\times\mathsf{Set}(\alpha)\rightarrow\mathsf{Set}(\alpha)&\verb|set.union|&\text{Union}\\\
\sqcap&\mathsf{Set}(\alpha)\times\mathsf{Set}(\alpha)\rightarrow\mathsf{Set}(\alpha)&\verb|set.inter|&\text{Intersection}\\\
\setminus&\mathsf{Set}(\alpha)\times\mathsf{Set}(\alpha)\rightarrow\mathsf{Set}(\alpha)&\verb|set.minus|&\text{Difference}\\\
\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}&\alpha\times\mathsf{Set}(\alpha)\rightarrow\mathsf{Bool}&\verb|set.member|&\text{Member
}\\\
\sqsubseteq&\mathsf{Set}(\alpha)\times\mathsf{Set}(\alpha)\rightarrow\mathsf{Bool}&\verb|set.subset|&\text{Subset}\\\
\hline\cr\sigma&\left(\alpha\rightarrow\mathsf{Bool}\right)\times\mathsf{Set}(\alpha)\rightarrow\mathsf{Set}(\alpha)&\verb|set.filter|&\text{Set
filter}\\\
\pi&\left(\alpha_{1}\rightarrow\alpha_{2}\right)\times\mathsf{Set}(\alpha_{1})\rightarrow\mathsf{Set}(\alpha_{2})&\verb|set.map|&\text{Set
map}\\\
\hline\cr\langle\ldots\rangle&\alpha_{0}\times\dots\times\alpha_{k}\rightarrow\mathsf{Tuple}(\alpha_{0},\ldots,\alpha_{k})&\verb|tuple|&\text{Tuple
constructor}\\\
\mathsf{select}_{i}&\mathsf{Tuple}(\alpha_{0},\ldots,\alpha_{k})\rightarrow\alpha_{i}&\verb|(_
tuple.select i)|&\text{Tuple selector}\\\\[2.41112pt]
\mathsf{tuple.proj}_{i_{1}\ldots
i_{n}}&\mathsf{Tuple}(\alpha_{0},\ldots,\alpha_{k})\rightarrow\mathsf{Tuple}(\alpha_{i_{1}},\ldots,\alpha_{i_{n}})&(\verb|_
tuple.proj |i_{1}\cdots i_{n})&\text{Tuple projection}\\\
\hline\cr\otimes&\mathsf{Relation}(\bm{\alpha})\times\mathsf{Relation}(\bm{\beta})\rightarrow\mathsf{Relation}(\bm{\alpha},\bm{\beta})&\verb|rel.product|&\text{Relation
cross join}\\\ \bowtie_{i_{1}j_{1}\cdots
i_{p}j_{p}}&\mathsf{Relation}(\bm{\alpha})\times\mathsf{Relation}(\bm{\beta})\rightarrow\mathsf{Relation}(\bm{\alpha},\bm{\beta})&(\verb|_
rel.join |i_{1}j_{1}\cdots i_{p}j_{p})&\text{Relation inner
join}\\\\[2.41112pt] \mathsf{rel.proj}_{i_{1}\ldots
i_{n}}&\mathsf{Relation}(\alpha_{0},\ldots,\alpha_{k})\rightarrow\mathsf{Relation}(\alpha_{i_{1}},\ldots,\alpha_{i_{n}})&(\verb|_
rel.proj |i_{1}\cdots i_{n})&\text{Relation projection}\\\
\hline\cr\hline\cr\end{array}\\\\[12.05554pt] \end{array}$
Figure 12:  Signature $\Sigma_{r}$ for the theory of relations. Here
$\mathsf{Relation}(\bm{\alpha},\bm{\beta})$ is a shorthand for
$\mathsf{Relation}(\alpha_{0},\ldots,\alpha_{p},\beta_{0},\ldots,\beta_{q})$
when $\bm{\alpha}=\alpha_{0},\ldots,\alpha_{p}$ and
$\bm{\beta}=\beta_{0},\ldots,\beta_{q}$.
$\mathsf{S}:=\mathsf{S},\,x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\sqcap
tx\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\in\mathsf{S}^{*}\quad
x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\in\mathsf{S}^{*}\quad s\sqcap
t\in\mathcal{T}(\mathsf{S})$
$\mathsf{S}:=\mathsf{S},\,x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s,\,x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}tx\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\sqcap
t\in\mathsf{S}^{*}$
---
$\mathsf{S}:=\mathsf{S},\,x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\sqcup
tx\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}u\in\mathsf{S}^{*}\quad
u\in\\{s,t\\}\quad s\sqcup t\in\mathcal{T}(\mathsf{S})$
$\mathsf{S}:=\mathsf{S},\,x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\
\parallel\
\mathsf{S}:=\mathsf{S},\,x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}tx\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\sqcup
t\in\mathsf{S}^{*}$
$\mathsf{S}:=\mathsf{S},\,x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\
\parallel\
\mathsf{S}:=\mathsf{S},\,x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\setminus
tx\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\in\mathsf{S}^{*}\quad s\setminus
t\in\mathcal{T}(\mathsf{S})$
$\mathsf{S}:=\mathsf{S},\,x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s,\,x\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}tx\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s\setminus
t\in\mathsf{S}^{*}$
$\mathsf{S}:=\mathsf{S},\,x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}[\,x\,][\,x\,]\in\mathcal{T}(\mathsf{S})$
$\mathsf{S}:=\mathsf{S},\,x\approx
yx\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}[\,y\,]\in\mathsf{S}^{*}$
$\mathsf{unsat}x\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}[\,]\in\mathsf{S}^{*}$
$\mathsf{S}:=\mathsf{S},\,z\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s,\,z\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}t\quad\parallel\quad\mathsf{S}:=\mathsf{S},\,z\not\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}s,\,z\mathrel{\ooalign{$\sqsubset$\cr{$-$}}}ts\not\approx
t\in\mathsf{S}^{*}$ $\mathsf{unsat}(t\not\approx t)\in\mathsf{S}^{*}$
$\mathsf{S}:=\mathsf{S},\,\langle
x_{1},\ldots,x_{m},y_{1},\ldots,y_{n}\rangle\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}R_{1}\otimes
R_{2}\langle
x_{1},\ldots,x_{m}\rangle\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}R_{1}\in\mathsf{S}^{*}\quad\langle
y_{1},\ldots,y_{n}\rangle\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}R_{2}\in\mathsf{S}^{*}\quad
R_{1}\otimes R_{2}\in\mathcal{T}(\mathsf{S})$
$\mathsf{S}:=\mathsf{S},\,\langle
x_{1},\ldots,x_{m}\rangle\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}R_{1},\,\langle
y_{1},\ldots,y_{n}\rangle\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}R_{2}\langle
x_{1},\ldots,x_{m},y_{1},\ldots,y_{n}\rangle\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}R_{1}\otimes
R_{2}\in\mathsf{S}^{*}\quad\mathrm{ar}(R_{1})=m$
Figure 13: Basic rules for set intersection, union, difference, singleton,
disequality and contradiction. In Set Diseq, $z$ is a fresh variable.

###  .8.1 Proofs for Relations Theory

######  Lemma .8.1.

The calculus for $\mathbb{T}_{\mathsf{Rel}}$ is terminating with operators
$\\{=,\sqcup,\sqcap,\setminus,\otimes,\sigma\\}$.

###### Proof.

Suppose we start with a configuration $c=(\mathsf{S},\mathsf{E})$. Without
loss of generality assume all set terms are relations, and all element terms
are tuples. Now let $\mathcal{T}(\varepsilon_{c}),\mathcal{T}(\mathsf{S}_{c})$
be all the finitely-many terms at $c$ of sorts $\mathsf{Tup},\mathsf{Set}$
respectively. Suppose $e_{0},s_{0}$ are the numbers of these terms
respectively. None of the calculus rules introduces new $\mathsf{Set}$ terms.
So $s_{0}$ remains constant in all derivation trees with root $c$. Rule Set
Diseq generates new element terms, but it is only applied once for each
disequality constraint. At the worst case all set terms are distinct. So
$e_{0}$ can increase by at most $s_{0}^{2}$ terms in all derivation trees
using Set Diseq rule. Define $e_{1}=e_{0}+s_{0}^{2}$. Rule Prod Up introduces
at most $e_{1}^{2}$ new terms. Rule Prod Down introduces at most $2e_{1}$ new
element terms. Define $e_{2}=e_{1}^{2}+2e_{1}$. So the number of element terms
in all derivation is at most $e_{2}$. We define the order relation $\succ$
over configurations as follows:

  * •

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

  * •

$c\succ c^{\prime}$ if $c\neq\mathsf{unsat}$ and
$c^{\prime}\neq\mathsf{unsat}$ and $\langle
f_{1}(c),\dots,f_{15}(c)\rangle>_{lex}^{15}\langle
f_{1}(c^{\prime}),\dots,f_{15}(c^{\prime})\rangle$ where $f_{i}$ are ranking
functions defined in Figure 14.

  * •

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

$f_{i}$ | Rule | Definition
---|---|---
$f_{1}$ | Inter Up | $e_{2}\times s_{0}^{2}-\lvert\\{x\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s\sqcap t\mid x\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s\sqcap t\in\mathsf{S}\\}\rvert$
$f_{2}$ | Inter Down | $e_{2}\times s_{0}^{2}-\lvert\\{x\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s\mid x\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s\in\mathsf{S}\\}\rvert$
$f_{3}$ | Union Up | $e_{2}\times s_{0}^{2}-\lvert\\{x\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s\sqcup t\mid x\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}s\sqcup t\in\mathsf{S}\\}\rvert$