# Automated Reasoning with Restricted Intensional Sets

MAXIMILIANO CRISTIÁ GIANFRANCO ROSSI  Universidad Nacional de Rosario and
CIFASIS, Argentina  Università di Parma, Italy

###### Abstract

Intensional sets, i.e., sets given by a property rather than by enumerating
elements, are widely recognized as a key feature to describe complex problems
(see, e.g., specification languages such as B and Z). Notwithstanding, very
few tools exist supporting high-level automated reasoning on general formulas
involving intensional sets. In this paper we present a decision procedure for
a first-order logic language offering both extensional and (a restricted form
of) intensional sets (RIS). RIS are introduced as first-class citizens of the
language and set-theoretical operators on RIS are dealt with as constraints.
Syntactic restrictions on RIS guarantee that the denoted sets are finite,
though unbounded. The language of RIS, called $\mathcal{L}_{\mathcal{RIS}}$,
is parametric with respect to any first-order theory $\mathcal{X}$ providing
at least equality and a decision procedure for $\mathcal{X}$-formulas. In
particular, we consider the instance of $\mathcal{L}_{\mathcal{RIS}}$ when
$\mathcal{X}$ is the theory of hereditarily finite sets and binary relations.
We also present a working implementation of this instance as part of the
$\\{log\\}$ tool and we show through a number of examples and two case studies
that, although RIS are a subclass of general intensional sets, they are still
sufficiently expressive as to encode and solve many interesting problems.
Finally, an extensive empirical evaluation provides evidence that the tool can
be used in practice.

###### category:

D.3.2 Programming Languages Constraint and Logic Languages

###### category:

D.3.3 Programming Languages Language Constructs and Features

###### category:

F.4 Mathematical Logic and Formal Languages Mathematical Logic

###### keywords:

Logic and Constraint Programming, Set Theory

###### keywords:

constraint programming, declarative programming, intensional sets, set
comprehensions, set theory

††terms: Languages,Theory, Verification

Maximiliano Cristiá and Gianfranco Rossi. 2019. Automated Reasoning with
Restricted Intensional Sets Authors’ addresses: M. Cristiá, Universidad
Nacional de Rosario and CIFASIS, Pellegrini 250, 2000 Rosario, Argentina;
email<EMAIL_ADDRESS>; G. Rossi, Università di Parma, Dip. di
Matematica, Via M. D’Azeglio, 85/A, 43100 Parma, Italy; email:
<EMAIL_ADDRESS>
##  1 Introduction

In the practice of mathematics very often a set is denoted by providing a
property that the elements must satisfy, rather than by explicitly enumerating
all its elements. This is usually achieved by the well-known mathematical
notation

$\\{\,x\,\mid\>\varphi(x)\,\\}$

where $x$ is a variable (the _control variable_) and $\varphi$ is a first-
order formula containing $x$. The logical meaning of such notation is the set
$S$ such that $\forall x(x\in S\Leftrightarrow\varphi(x))$, that is, the set
of all instances of $x$ for which $\varphi(x)$ holds. Sets defined by
properties are also known as _set comprehensions_ or _set abstractions_ or
_intensional defined sets_ ; hereafter, we will refer to such sets simply as
_intensional sets_.

Intensional sets are widely recognized as a key feature to describe complex
problems, possibly leading to more readable and compact programs than those
based on conventional data abstractions. As a matter of fact, various
specification or modeling languages provide intensional sets as first-class
entities. For example, some form of intensional sets are available in
notations such as Z [Woodcock and Davies (1996)] and B [Schneider (2001)],
Alloy [Jackson (2006)], MiniZinc [Nethercote et al. (2007)], and ProB
[Leuschel and Butler (2003)]. Also, a few programming languages support
intensional sets. Among them, SETL [Schwartz et al. (1986)], Python, and the
logic programming language Gödel [Hill and Lloyd (1994)].

However, as far as we know, none of these proposals provides the ability to
perform high-level automated reasoning on general formulas involving
intensional sets. No direct support for reasoning about intensional sets seem
to be readily available even in state-of-the-art satisfiability solvers, as
noted, for instance, by Lam and Cervesato with reference to SMT solvers [Lam
and Cervesato (2014)]. Generally speaking, such reasoning capabilities would
be of great interest to several communities, such as programming, constraint
solving, automated theorem proving, and formal verification.

Some form of automated reasoning about intensional sets is provided by
(Constraint) Logic Programming (CLP) languages with sets, such as LDL [Beeri
et al. (1991)] and CLP(SET) [Dovier et al. (2000)]. The processing of
intensional sets in these proposals is based on the availability of a _set-
grouping_ mechanism capable of collecting into an extensional set all the
elements satisfying the property characterizing the given intensional
definition. Restrictions are often put on the form of the collected sets, such
as non-emptiness and/or groundness. Allowing more general forms of set-
grouping, however, would require the ability to deal with logical negation in
a rather non-trivial way (see [Bruscoli et al. (1994), Dovier et al. (2001)]
for an analysis of the relationship between intensional sets and negation).

Actually, set-grouping is not always necessary to deal with intensional sets,
and sometimes it is not desirable, at all. For instance, given the formula
$t\in\\{x\mid\varphi\\}$, one could check whether it is satisfiable or not by
simply checking satisfiability of $\varphi[x\mapsto t]$, i.e., of the instance
of $\varphi$ which is obtained by substituting $x$ by $t$.

In this paper, we present a complete constraint solver which can act as a
decision procedure for an important fragment of a first-order logic language
offering both extensional and intensional sets. Intensional sets are
introduced as first-class citizens of the logic language, and set-theoretical
operators on intensional sets, such as membership, union, etc., are dealt with
as _constraints_ in that language. Complex formulas involving intensional sets
are processed and solved by a suitable constraint solver by using a sort of
_lazy partial evaluation_. That is, an intensional set $S$ is treated as a
block until it is necessary to identify one of its elements, say $d$. When
that happens, $S$ is transformed into an extensional set of the form
$\\{d\\}\cup R_{S}$, where $R_{S}$ is the “rest” of $S$. At this point,
classic set constraint rewriting (in particular set unification) is applied.

A similar approach, based on intensional set constraint solving, has been
proposed in [Dovier et al. (2003)]. Differently from that work, however, we
avoid problems arising if general intensional sets are allowed (namely, the
use of logical negation and possibly infinite sets), by considering a narrower
form of intensional sets, called _Restricted Intensional Sets_ (RIS). RIS have
similar syntax and semantics to the set comprehensions available in the formal
specification language Z, i.e.,

$\\{x:D\mid\phi\mathbin{\bullet}u(x)\\}$

where $D$ is a set, $\phi$ is a formula, and $u$ is a term containing $x$. The
intuitive semantics of $\\{x:D\mid\phi\mathbin{\bullet}u(x)\\}$ is “the set of
terms $u(x)$ such that $x$ belongs to $D$ and $\phi$ holds for $x$”.111In this
notation, as in Z, $x:D$ is interpreted as $x\in D$. $\phi$ is a quantifier-
free formula over a first-order theory $\mathcal{X}$, for which we assume a
complete satisfiability solver is available. Moreover, RIS have the
restriction that $D$ must be a _finite set_. This fact, along with a few
restrictions on variables occurring in $\phi$ and $u$, guarantees that the RIS
is a finite set, given that it is at most as large as $D$. It is important to
note that, although RIS are guaranteed to denote finite sets, nonetheless, RIS
can be not completely specified. In particular, as the domain can be a
variable or a partially specified set, RIS are finite but _unbounded_.

In previous work, we have proposed a constraint language dealing with RIS,
called $\mathcal{L}_{\mathcal{RIS}}$ [Cristiá and Rossi (2017)].
$\mathcal{L}_{\mathcal{RIS}}$ formulas are Boolean combinations of constraints
representing set equality and set membership and whose set terms can be both
extensional sets and RIS. Furthermore, $\mathcal{L}_{\mathcal{RIS}}$ is
parametric w.r.t. the language of $\mathcal{X}$, in the sense that set
elements and the formulas inside RIS are $\mathcal{X}$-terms and quantifier-
free $\mathcal{X}$-formulas, respectively. In particular, $\mathcal{X}$ can be
the theory of sets and binary relations described in [Cristiá and Rossi
(2019)]. Besides, $\mathcal{L}_{\mathcal{RIS}}$ is endowed with a complete
solver, called $\mathit{SAT}_{\mathcal{RIS}}$, which can act as a decision
procedure for an important fragment of $\mathcal{L}_{\mathcal{RIS}}$ formulas
(provided a decision procedure for $\mathcal{X}$ is available). In this paper
we extend our previous work on RIS in several ways:

  1. 1.

The Boolean algebra of sets is now supported; this is achieved by extending
the collection of primitive set constraints admitting RIS to union ($\cup$)
and disjointness ($\parallel$).

  2. 2.

The decision procedure for $\mathcal{L}_{\mathcal{RIS}}$,
$\mathit{SAT}_{\mathcal{RIS}}$, and its Prolog implementation are extended
accordingly.

  3. 3.

Formulas inside RIS can be existentially quantified $\mathcal{X}$-formulas as
long as the quantified variables are special parameters of functional
predicates.

  4. 4.

An extensive empirical evaluation of these extensions, based on problems drawn
from the TPTP library, is also made.

Though RIS are _restricted_ , we aim to show that in spite of these
restrictions $\mathcal{L}_{\mathcal{RIS}}$ is still a very expressive
language. In particular, we will show that it allows _Restricted Universal
Quantifiers_ (RUQ) on _finite_ domains to be expressed as
$\mathcal{L}_{\mathcal{RIS}}$ formulas, thus allowing an important class of
quantified formulas to lay inside the decision procedure. Besides encoding
RUQ, RIS provide a sort of second-order language of sets as they allow to
iterate over sets of sets and are useful to express partial functions, as well
as a programming facility similar to list/set comprehensions available in
programming languages.

The paper is organized as follows. In Section 2 the syntax and semantics of
$\mathcal{L}_{\mathcal{RIS}}$ are introduced; in particular Section 2.3
presents some basic examples of formulas involving RIS terms. Section 3 lists
and discusses the rewrite rules of $\mathit{SAT}_{\mathcal{RIS}}$, in
particular those for set union and disjointness. In Section 4 we precisely
characterize the admissible $\mathcal{L}_{\mathcal{RIS}}$ formulas involving
RIS, and we prove that $\mathit{SAT}_{\mathcal{RIS}}$ is a decision procedure
for such formulas. Section 5 shows two important applications for RIS: RUQ and
partial functions. The extension allowing existentially quantified formulas
inside a RIS term is motivated and discussed in Section 6. Section 7 presents
the implementation of our approach as part of the $\\{log\\}$ tool (pronounced
’setlog’) [Rossi (2008)] where two case studies are also discussed: the first
one presents an automated proof of a non-trivial security property, while the
second elaborates on the possibility to iterate over collections of sets and
shows how $\\{log\\}$ can be used as a programming tool and as a verification
tool. The results of the empirical evaluation of $\\{log\\}$ are presented in
Section 8. A comparison of our approach with other works and our conclusions
are presented in Sections 9 and 10, respectively.

##  2 Formal Syntax and Semantics

This section describes the syntax and semantics of the language of Restricted
Intensional Sets, $\mathcal{L}_{\mathcal{RIS}}$. A gentle, informal
introduction is provided in Section 2.3.

$\mathcal{L}_{\mathcal{RIS}}$ is a first-order predicate language with terms
of two sorts: terms designating sets and terms designating ur-elements. The
latter are provided by an external first-order theory $\mathcal{X}$ (i.e.,
$\mathcal{L}_{\mathcal{RIS}}$ is parametric with respect to $\mathcal{X}$).
$\mathcal{X}$ must include: a class $\Phi_{\mathcal{X}}$ of admissible
$\mathcal{X}$-formulas based on a set of function symbols
$\mathcal{F}_{\mathcal{X}}$ and a set of predicate symbols $\Pi_{\mathcal{X}}$
(providing at least equality); an interpretation structure
$\mathcal{I}_{\mathcal{X}}$ with domain $\mathcal{D}_{\mathsf{X}}$ and
interpretation function ${(\cdot)}^{\mathcal{I}_{\mathcal{X}}}$; and a
decision procedure $\mathit{SAT}_{\mathcal{X}}$ for $\mathcal{X}$-formulas.
When useful, we will write $\mathcal{L}_{\mathcal{RIS}}(\mathcal{X})$ to
denote the instance of $\mathcal{L}_{\mathcal{RIS}}$ based on theory
$\mathcal{X}$. On the other hand, $\mathcal{L}_{\mathcal{RIS}}$ provides
special set constructors, and a handful of reserved predicate symbols endowed
with a pre-designated set-theoretic meaning. Set constructors are used to
construct both RIS and extensional sets. Set elements are the objects provided
by $\mathcal{X}$, which are manipulated through the primitive operators that
$\mathcal{X}$ offers. Hence, $\mathcal{L}_{\mathcal{RIS}}$ sets represent
_untyped unbounded finite hybrid sets_ , i.e., unbounded finite sets whose
elements are of arbitrary sorts. $\mathcal{L}_{\mathcal{RIS}}$ formulas are
built in the usual way by using conjunction, disjunction and negation of
atomic formulas. A number of complex operators (in the form of predicates) are
defined as $\mathcal{L}_{\mathcal{RIS}}$ formulas, thus making it simpler for
the user to write complex formulas.

###  2.1 Syntax

Syntax is defined primarily by giving the signature upon which terms and
formulas of the language are built.

######  Definition 2.1 (Signature).

The signature $\Sigma_{\mathcal{RIS}}$ of $\mathcal{L}_{\mathcal{RIS}}$ is a
triple $\langle\mathcal{F},\Pi,\mathcal{V}\rangle$ where:

  * •

$\mathcal{F}$ is the set of function symbols, partitioned as
$\mathcal{F}=\mathcal{F}_{\mathcal{S}}\cup\mathcal{F}_{\mathcal{X}}$, where
$\mathcal{F}_{\mathcal{S}}$ contains $\emptyset$,
$\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\}$ and
$\\{\cdot:\cdot\mid\cdot\,\mathbin{\bullet}\,\cdot\\}$, while
$\mathcal{F}_{\mathcal{X}}$ contains the function symbols provided by the
theory $\mathcal{X}$ (at least, a constant and the binary function symbol
$(\cdot,\cdot)$).

  * •

$\Pi$ is the set of _primitive_ predicate symbols, partitioned as
$\Pi=\Pi_{\mathcal{S}}\cup\Pi_{\mathcal{T}}\cup\Pi_{\mathcal{X}}$, where
$\Pi_{\mathcal{S}}\triangleq\\{=_{\mathcal{S}},\neq_{\mathcal{S}},\in_{\mathcal{S}},\not\in_{\mathcal{S}},\mathit{un}_{\mathcal{S}},\parallel_{\mathcal{S}}\\}$,
$\Pi_{\mathcal{T}}\triangleq\\{\mathit{set},\mathit{isX}\\}$, while
$\Pi_{\mathcal{X}}$ contains the predicate symbols provided by the theory
$\mathcal{X}$ (at least $=_{\mathcal{X}}$).

  * •

$\mathcal{V}$ is a denumerable set of variables, partitioned as
$\mathcal{V}=\mathcal{V}_{\mathcal{S}}\cup\mathcal{V}_{\mathcal{X}}$. ∎

Intuitively, $\emptyset$ represents the empty set,
$\\{t\mathbin{\scriptstyle\sqcup}A\\}$ represents the set $\\{t\\}\cup A$, and
$\\{c(\vec{x}):D\mid\phi(\vec{x})\mathbin{\bullet}u(\vec{x})\\}$, where
$\vec{x}\triangleq\langle x_{1},\dots,x_{n}\rangle$, $n>0$, is the vector of
all variables occurring in $c$, represents the set of all instances of $u$
such that $c$ belongs to $D$ and $\phi$ holds. $=_{\mathcal{X}}$ is
interpreted as the identity in $\mathcal{D}_{\mathsf{X}}$, while
$(\cdot,\cdot)$ will be used to represent ordered pairs.

$\mathcal{L}_{\mathcal{RIS}}$ defines two sorts, $\mathsf{Set}$ and
$\mathsf{X}$, which intuitively represent the domain of set objects and the
domain of non-set objects (or ur-elements). We also assume a sort
$\mathsf{Bool}$ is available, representing the two-valued domain of truth
values $\\{\mathsf{false},\mathsf{true}\\}$.

To each variable in $\mathcal{V}$ and each constant in $\mathcal{F}$ we
associate a sort $\mathsf{S}$, while to each function symbol in $\mathcal{F}$
of arity $n\geq 1$ we associate a string
$\mathsf{S}_{1}\mathsf{\>x\>}\dots\mathsf{\>x\>}\mathsf{S}_{n}\texttt{\>->\>}\mathsf{S}$,
where $\mathsf{S},\mathsf{S}_{i}\in\\{\mathsf{Set},\mathsf{X}\\}$. Moreover,
if $t$ is a variable or a constant and $\mathsf{S}$ is the associated sort, or
$t$ is a term $h(t_{1},\dots,t_{n})$, $n\geq 1$, and
$\mathsf{S}_{1}\mathsf{\>x\>}\dots\mathsf{\>x\>}\mathsf{S}_{n}\texttt{\>->\>}\mathsf{S}$
is the sort associated to $h$, then we say that $t$ is of sort $\mathsf{S}$
and we write $t:\mathsf{S}$.

######  Definition 2.2 (Sorts of function symbols).

The sorts of the symbols defined in $\mathcal{F}$ are as follows:

$\displaystyle\emptyset:\mathsf{Set}$
$\displaystyle\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\}:\mathsf{X}\mathsf{\>x\>}\mathsf{Set}\texttt{\>->\>}\mathsf{Set}$
$\displaystyle\\{\cdot:\cdot\mid\cdot\,\mathbin{\bullet}\,\cdot\\}:\mathsf{X}\mathsf{\>x\>}\mathsf{Set}\mathsf{\>x\>}\mathsf{Bool}\mathsf{\>x\>}\mathsf{X}\texttt{\>->\>}\mathsf{Set}$
$\displaystyle
s:\overbrace{\mathsf{X}\mathsf{\>x\>}\dots\mathsf{\>x\>}\mathsf{X}}^{n_{s}}\texttt{\>->\>}\mathsf{X}\text{,
if $s\in\mathcal{F}_{\mathcal{X}}$, for some $n_{s}\geq 0$}$ $\displaystyle
v:\mathsf{Set}\text{, if $v\in\mathcal{V}_{\mathcal{S}}$}$ $\displaystyle
v:\mathsf{X}\text{, if $v\in\mathcal{V}_{\mathcal{X}}$}$

∎

In view of the intended interpretation, terms of sort $\mathsf{Set}$ are
called _set terms_ ; in particular, set terms of the form
$\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\}$ are _extensional set terms_ ,
whereas set terms of the form
$\\{\cdot:\cdot\mid\cdot\,\mathbin{\bullet}\,\cdot\\}$ are _RIS terms_ 222The
form of RIS terms is borrowed from the form of set comprehension expressions
available in Z.; variable set terms are simply called _set variables_.

Note that terms that constitute the elements of sets are all of sort
$\mathsf{X}$. Also note that in a RIS term,
$\\{c:D\mid\phi\mathbin{\bullet}u\\}$, $D$ (called _domain_) is a set term,
$\phi$ (called _filter_) is a $\mathcal{X}$-formula, while $c$ (called
_control term_) and $u$ (called _pattern_) are $\mathcal{X}$-terms.

Terms of $\mathcal{L}_{\mathcal{RIS}}$—called _$\mathcal{RIS}$ -terms_—are
built from symbols in $\mathcal{F}$ and $\mathcal{V}$ as follows.

######  Definition 2.3.

[$\mathcal{RIS}$-terms] Let $\mathcal{T}_{\mathcal{RIS}}^{0}$ be the set of
terms generated by the following grammar:

$\displaystyle\mathcal{T}_{\mathcal{RIS}}^{0}::=\mathit{Elem}\hskip
2.0pt\mid\hskip 2.0pt\mathit{Set}$
$\displaystyle\mathit{Elem}::=\mathcal{T}_{\mathcal{X}}\hskip 2.0pt\mid\hskip
2.0pt\mathcal{V}_{\mathcal{X}}$
$\displaystyle\begin{split}\mathit{Set}::=&\text{\'{}}\emptyset\text{\'{}}\hskip
5.0pt\\\ &\hskip 2.0pt\mid\hskip 2.0pt\mathit{Ris}\\\ &\hskip 2.0pt\mid\hskip
2.0pt\text{\'{}}\\{\text{\'{}}\hskip 5.0pt\mathit{Elem}\hskip
5.0pt\text{\'{}}\mathbin{\scriptstyle\sqcup}\text{\'{}}\hskip
5.0pt\mathit{Set}\hskip 5.0pt\text{\'{}}\\}\text{\'{}}\\\ &\hskip
2.0pt\mid\hskip 2.0pt\mathcal{V}_{\mathcal{S}}\end{split}$
$\displaystyle\mathit{Ctrl}::=\mathcal{V}_{\mathcal{X}}\hskip 2.0pt\mid\hskip
5.0pt\text{\'{}}(\text{\'{}}~{}~{}\mathit{Ctrl}~{}~{}\hskip
5.0pt\text{\'{}},\text{\'{}}~{}~{}\mathit{Ctrl}\hskip
5.0pt\text{\'{}})\text{\'{}}$
$\displaystyle\mathit{Pattern}::=\mathcal{V}_{\mathcal{X}}\hskip
2.0pt\mid\hskip 5.0pt\text{\'{}}(\text{\'{}}~{}~{}\mathit{Ctrl}~{}~{}\hskip
5.0pt\text{\'{}},\text{\'{}}~{}~{}\mathcal{T}_{\mathcal{X}}\hskip
5.0pt\text{\'{}})\text{\'{}}$ $\displaystyle\mathit{Ris}::=\hskip
5.0pt\text{\'{}}\\{\text{\'{}}\hskip 5.0pt\mathit{Ctrl}\hskip
5.0pt\text{\'{}}:\text{\'{}}\hskip 5.0pt\mathit{Set}\hskip
5.0pt\text{\'{}}\mid\text{\'{}}\hskip 5.0pt\Phi_{\mathcal{X}}\hskip
5.0pt\text{\'{}}\mathbin{\bullet}\text{\'{}}\hskip 5.0pt\mathit{Pattern}\hskip
5.0pt\text{\'{}}\\}\text{\'{}}\hskip 5.0pt$

where $\mathcal{T}_{\mathcal{X}}$ and $\Phi_{\mathcal{X}}$ represent the set
of non-variable $\mathcal{X}$-terms and the set of $\mathcal{X}$-formulas
built using symbols in $\mathcal{F}_{\mathcal{X}}$ and $\Pi_{\mathcal{X}}$,
respectively.

The set of _$\mathcal{RIS}$ -terms_, denoted by $\mathcal{T}_{\mathcal{RIS}}$,
is the maximal subset of $\mathcal{T}_{\mathcal{RIS}}^{0}$ complying with the
sorts as given in Definition 2.2 and respecting the following restriction on
RIS terms: if $c$ is the control term of a RIS, then its pattern can be either
$c$ or $(c,t)$. ∎

The special form of control terms and patterns will be precisely motivated and
discussed in Section 6.

Sets denoted by both extensional set terms and RIS terms can be _partially
specified_ because elements and sets can be variables. In particular, RIS can
have a variable domain.

######  Definition 2.4 (Variable-RIS).

A RIS term is a _variable-RIS_ if its domain is a variable or (recursively) a
variable-RIS; otherwise it is a _non-variable RIS_. ∎

Variable-RIS will be of special interest since they can be easily turned into
the empty set by substituting their domains by the empty set.

######  Definition 2.5 (Sorts of predicate symbols).

The sorts of the predicate symbols in $\Pi_{\mathcal{S}}\cup\Pi_{\mathcal{T}}$
are as follows (symbols $=$, $\neq$, $\in$, $\notin$ and $\parallel$ are
infix; all other symbols are prefix):

$\displaystyle=_{\mathcal{S}},\neq_{\mathcal{S}}:\mathsf{Set}\mathsf{\>x\>}\mathsf{Set}\texttt{\>->\>}\mathsf{Bool}$
$\displaystyle\in_{\mathcal{S}},\not\in_{\mathcal{S}}:\mathsf{X}\mathsf{\>x\>}\mathsf{Set}\texttt{\>->\>}\mathsf{Bool}$
$\displaystyle\mathit{un}_{\mathcal{S}}:\mathsf{Set}\mathsf{\>x\>}\mathsf{Set}\mathsf{\>x\>}\mathsf{Set}\texttt{\>->\>}\mathsf{Bool}$
$\displaystyle\parallel_{\mathcal{S}}:\mathsf{Set}\mathsf{\>x\>}\mathsf{Set}\texttt{\>->\>}\mathsf{Bool}$
$\displaystyle\mathit{set},\mathit{isX}:\mathsf{Set}\cup\mathsf{X}\texttt{\>->\>}\mathsf{Bool}$

∎

######  Definition 2.6 ($\mathcal{RIS}$-constraints).

A (primitive) _$\mathcal{RIS}$ -constraint_ is any atom built from symbols in
$\Pi_{\mathcal{S}}\cup\Pi_{\mathcal{T}}$ complying with the sorts as given in
Definition 2.2. The set of $\mathcal{RIS}$-constraints is denoted by
$\mathcal{C}_{\mathcal{RIS}}$. $\mathcal{RIS}$-constraints based on a symbol
$\pi$ (resp., on a set of symbols $\Pi$) are called _$\pi$ -constraints_
(resp., _$\Pi$ -constraints_). ∎

Formulas of $\mathcal{L}_{\mathcal{RIS}}$—called _$\mathcal{RIS}$
-formulas_—are built from $\mathcal{RIS}$-constraints and
$\mathcal{X}$-formulas as follows.

######  Definition 2.7 ($\mathcal{RIS}$-formulas).

The set of $\mathcal{RIS}$-formulas, denoted by $\Phi_{\mathcal{RIS}}$, is
given by the following grammar.

$\displaystyle\Phi_{\mathcal{RIS}}::=\mathit{true}\mid\mathcal{C}_{\mathcal{RIS}}\mid\Phi_{\mathcal{RIS}}\land\Phi_{\mathcal{RIS}}\mid\Phi_{\mathcal{RIS}}\lor\Phi_{\mathcal{RIS}}\mid\mathit{\Phi_{\mathcal{X}}}$

$\mathcal{RIS}$-formulas not containing any $\mathcal{X}$-formula are called
_pure $\mathcal{RIS}$-formulas_. ∎

######  Remark 2.8 (Notation).

The following notational conventions are used throughout this paper.
$s,t,u,a,b,c,d$ (possibly subscripted) stand for arbitrary terms of sort
$\mathsf{X}$; while $A,B,C,D$ stand for arbitrary terms of sort $\mathsf{Set}$
(either extensional or intensional, variable or not). When it is useful to be
more specific, we will use $\bar{A},\bar{B},\bar{C},\bar{D}$ to represent
either variables of sort $\mathsf{Set}$ or variable-RIS; $X,Y,Z,N$ to
represent variables of sort $\mathsf{Set}$ that are not variable-RIS; and
$x,y,z,n$ to represent variables of sort $\mathsf{X}$. $\Phi,\Gamma,\Lambda$
stand for $\mathcal{RIS}$-formulas, while $\phi,\gamma,\lambda$ stand for
$\mathcal{X}$-formulas; $p,q,r$ stand for atomic formulas/constraints.

Moreover, a number of special notational conventions are used for the sake of
conciseness. Specifically, we will write
$\\{t_{1}\mathbin{\scriptstyle\sqcup}\\{t_{2}\mathbin{\scriptstyle\sqcup}\cdots\\{t_{n}\mathbin{\scriptstyle\sqcup}A\\}\cdots\\}\\}$
(resp.,
$\\{t_{1}\mathbin{\scriptstyle\sqcup}\\{t_{2}\mathbin{\scriptstyle\sqcup}\cdots\\{t_{n}\mathbin{\scriptstyle\sqcup}\emptyset\\}\cdots\\}\\}$)
as $\\{t_{1},t_{2},\dots,t_{n}\mathbin{\scriptstyle\sqcup}A\\}$ (resp.,
$\\{t_{1},t_{2},\dots,t_{n}\\}$). We will also use the notation $[m,n]$, $m$
and $n$ integer constants, as a shorthand for $\\{m,m+1,\dots,n\\}$. As
concerns RIS, when the pattern is the control term and the filter is
$\mathit{true}$, they can be omitted (as in Z), although one must be present.
∎

###  2.2 Semantics

Sorts and symbols in $\Sigma_{\mathcal{RIS}}$ are interpreted according to the
interpretation structure
$\mathcal{R}=\langle\mathcal{D},(\cdot)^{\mathcal{R}}\rangle$, where
$\mathcal{D}$ and $(\cdot)^{\mathcal{R}}$ are defined as follows.

######  Definition 2.9 (Interpretation domain).

The interpretation domain $\mathcal{D}$ is partitioned as
$\mathcal{D}=\mathcal{D}_{\mathsf{Set}}\cup\mathcal{D}_{\mathsf{X}}$ where:

  * •

$\mathcal{D}_{\mathsf{Set}}$: the collection of all finite sets built from
elements in $\mathcal{D}_{\mathsf{X}}$

  * •

$\mathcal{D}_{\mathsf{X}}$: a collection of any other objects (not in
$\mathcal{D}_{\mathsf{Set}}$).

######  Definition 2.10 (Interpretation function).

The interpretation function $(\cdot)^{\mathcal{R}}$ for symbols in
$\Sigma_{\mathcal{RIS}}$ is defined as follows:

  * •

Each sort $\mathsf{S}\in\\{\mathsf{X},\mathsf{Set}\\}$ is mapped to the domain
$\mathcal{D}_{\mathsf{S}}$.

  * •

$\mathcal{R}$ coincides with $\mathcal{I}_{\mathcal{X}}$ for symbols in
$\mathcal{F}_{\mathcal{X}}$ and $\Pi_{\mathcal{X}}$.

  * •

For each sort $\mathsf{S}$, each variable $x$ of sort $\mathsf{S}$ is mapped
to an element $x^{\mathcal{R}}$ in $\mathcal{D}_{\mathsf{S}}$.

  * •

The constant and function symbols in $\mathcal{F}_{\mathcal{S}}$ are
interpreted as follows:

    * –

$\emptyset$ is interpreted as the empty set $\emptyset$;

    * –

$\\{t\mathbin{\scriptstyle\sqcup}A\\}$ is interpreted as the set
$\\{t^{\mathcal{R}}\\}\cup A^{\mathcal{R}}$;

    * –

Let $\vec{v}$ be a vector of free variables and $\vec{x}$ the vector of
variables occurring in $c$, then the set
$\\{c(\vec{x}):D\mid\phi(\vec{x},\vec{v})\mathbin{\bullet}u(\vec{x},\vec{v})\\}$
is interpreted as the set

$\\{y:\exists\vec{x}(c(\vec{x})\in_{\mathcal{X}}D\land\phi(\vec{x},\vec{v})\land
y=_{\mathcal{X}}u(\vec{x},\vec{v}))\\}$

Note that in RIS terms, $\vec{x}$ are bound variables whose scope is the RIS
itself, while $\vec{v}$ are free variables possibly occurring in the formula
where the RIS is participating in.

  * •

The predicate symbols in $\Pi_{\mathcal{S}}$ are interpreted as follows:

    * –

$A=_{\mathcal{S}}B$ is interpreted as $A^{\mathcal{R}}=B^{\mathcal{R}}$, where
$=$ is the identity relation in $\mathcal{D}_{\mathsf{Set}}$;

    * –

$t\in_{\mathcal{S}}A$ is interpreted as $t^{\mathcal{R}}\in A^{\mathcal{R}}$,
where $\in$ is the set membership relation in $D_{\mathsf{Set}}$;

    * –

$\mathit{un}_{\mathcal{S}}(A,B,C)$ is interpreted as $A^{\mathcal{R}}\cup
B^{\mathcal{R}}=C^{\mathcal{R}}$, where $\cup$ is the set union operator in
$D_{\mathsf{Set}}$;

    * –

$A\parallel_{\mathcal{S}}B$ is interpreted as $A^{\mathcal{R}}\cap
B^{\mathcal{R}}=\emptyset$, where $\cap$ is the set intersection operator in
$\mathcal{D}_{\mathsf{Set}}$;

    * –

$\mathit{isX}(t)$ is interpreted as
$t^{\mathcal{R}}\in\mathcal{D}_{\mathsf{X}}$;

    * –

$\mathit{set}(t)$ is interpreted as
$t^{\mathcal{R}}\in\mathcal{D}_{\mathsf{Set}}$;

    * –

$A\neq B$ and $t\notin A$ are interpreted as
$\lnot(A^{\mathcal{R}}=B^{\mathcal{R}})$ and $\lnot(t^{\mathcal{R}}\in
A^{\mathcal{R}})$, respectively.

Equality between extensional set terms is regulated by the following two
equational axioms [Dovier et al. (2000)]:

$\displaystyle\\{x,x\mathbin{\scriptstyle\sqcup}A\\}=\\{x\mathbin{\scriptstyle\sqcup}A\\}$
($Ab$)
$\displaystyle\\{x,y\mathbin{\scriptstyle\sqcup}A\\}=\\{y,x\mathbin{\scriptstyle\sqcup}A\\}$
($C\ell$)

which state that duplicates in a set term do not matter (_Absorption
property_) and that the order of elements in a set term is irrelevant
(_Commutativity on the left_), respectively. These two properties capture the
intuitive idea that, for instance, the set terms $\\{1,2\\}$, $\\{2,1\\}$, and
$\\{1,2,1\\}$ all denote the same set. In other words, duplicates do not occur
in a set, but they may occur in the set term that denotes it. On the other
hand, equality between $\mathcal{X}$-terms is assumed to be managed by the
parameter theory $\mathcal{X}$.

###  2.3 Examples of $\mathcal{L}_{\mathcal{RIS}}$ formulas using RIS

In this section we present some simple examples of
$\mathcal{L}_{\mathcal{RIS}}$ formulas, in particular those where RIS terms
play a major role, with the objective to help the reader to understand the
notation. A deeper discussion of the applicability of
$\mathcal{L}_{\mathcal{RIS}}$ can be found in Sections 5 and 7.

For the sake of presentation, in coming examples, we will assume that the
language of $\mathcal{X}$, $\mathcal{L}_{\mathcal{X}}$, provides the constant,
function and predicate symbols of the theory of the integer numbers. Moreover,
we will write $=$ (resp., $\neq,\in,\mathit{un}$) in place of
$=_{\mathcal{X}}$ and $=_{\mathcal{S}}$ (resp.,
$\in_{\mathcal{X}},\neq_{\mathcal{X}},\mathit{un}_{\mathcal{X}}$ and
$\in_{\mathcal{S}},\neq_{\mathcal{S}},\mathit{un}_{\mathcal{S}}$) whenever is
clear from context.

######  Example 2.11.

The following is an atomic $\mathcal{RIS}$-formula:

$\\{x:[-2,2]\mid x\mathbin{\mathrm{mod}}2=0\mathbin{\bullet}x\\}=\\{-2,0,2\\}$

This formula is clearly satisfiable with respect to the intended
interpretation $\mathcal{R}$. The RIS term can be written more compactly by
omitting the pattern as it is the control variable:

$\\{x:[-2,2]\mid x\mathbin{\mathrm{mod}}2=0\\}=\\{-2,0,2\\}$

∎

######  Example 2.12.

Set membership is also a viable operation on RIS:

$(5,y)\in\\{x:D\mid\mathit{true}\mathbin{\bullet}(x,x*x)\\}$

where $D$ is a variable. This formula is satisfiable with respect to
$\mathcal{R}$ provided $y$ is assigned the value $25$ and $D$ is bound to any
set containing $5$. The RIS can also be written as
$(5,y)\in\\{x:D\mathbin{\bullet}(x,x*x)\\}$ because the filter is
$\mathit{true}$. Note that the control term and the pattern verify the
condition stated in Definition 2.3. ∎

The negation of a set membership constraint, as all negations in
$\mathcal{L}_{\mathcal{RIS}}$, is written by using the corresponding predicate
symbol and not the logical negation which, anyway, is not part of
$\mathcal{L}_{\mathcal{RIS}}$.

######  Example 2.13.

A $\mathcal{RIS}$-formula containing negative constraints:

$(5,0)\notin\\{(x,y):\\{z\mathbin{\scriptstyle\sqcup}Z\\}\mid y\neq
0\mathbin{\bullet}(x,y)\\}$

where $z$ and $Z$ are free variables. This formula is satisfiable with respect
to $\mathcal{R}$ for any $z$ and $Z$. As above, the pattern can be omitted.
Observe that in $y\neq 0$ inequality corresponds to that of the theory
$\mathcal{X}$. ∎

######  Example 2.14.

The following is a non-atomic $\mathcal{RIS}$-formula involving RIS terms:

$A=\\{x:D\mid x\neq 0\\}\land\mathit{un}(A,B,C)\land A\parallel C\land
A\neq\emptyset$

This formula turns out to be unsatisfiable with respect to $\mathcal{R}$ since
$\mathit{un}(A,B,C)\land A\parallel C$ is satisfiable only if $A=\emptyset$,
while the input formula constraints $A$ to be distinct from $\emptyset$. ∎

Finally, note that we allow RIS terms to be the set part of extensional set
terms, e.g., $\\{z\mathbin{\scriptstyle\sqcup}\\{x:A\mid x\neq y\\}\\}$, as
well as to be the domain of other RIS. $\mathcal{L}_{\mathcal{RIS}}$ also
defines two constraints that are mainly used internally by the solver, namely
$\mathit{set}(t)$ and $\mathit{isX}(t)$. Each one asserts that its parameter
is of sort $\mathsf{Set}$ and $\mathsf{X}$, respectively.

###  2.4 Derived Constraints and Expressiveness

Dovier et al. [Dovier et al. (2000)] proved that the collection of predicate
symbols in $\Pi_{\mathcal{S}}$ is sufficient to define constraints
implementing other common set operators, such as $\cap$ and $\subseteq$.

Specifically, let us consider the following predicate symbols:
$\subseteq,\mathit{inters},\mathit{diff}$, along with their interpretations:
$A\subseteq B$ is interpreted as $A^{\mathcal{R}}\subseteq B^{\mathcal{R}}$;
$\mathit{inters}(A,B,C)$ is interpreted as
$C^{\mathcal{R}}=A^{\mathcal{R}}\cap B^{\mathcal{R}}$; $\mathit{diff}(A,B,C)$
is interpreted as $C^{\mathcal{R}}=A^{\mathcal{R}}\backslash B^{\mathcal{R}}$.
Dovier et al. [Dovier et al. (2000)] prove that these predicates can be made
available in $\mathcal{L}_{\mathcal{RIS}}$ without having to add them to the
collection of its primitive constraints. As an example, $A\subseteq B$ can be
defined by the $\mathcal{L}_{\mathcal{RIS}}$ formula $\mathit{un}(A,B,B)$.

With a little abuse of terminology, we say that atoms based on these
predicates are _derived constraints_. Whenever a formula contains a derived
constraint, the constraint is replaced by its definition turning the given
formula into a $\mathcal{L}_{\mathcal{RIS}}$ formula. Precisely, if $\Phi$ is
the ${\cal RIS}$-formula defining the constraint $c$, then $c$ is replaced by
$\Phi$ and the solver checks satisfiability of $\Phi$ to determine
satisfiability of $c$. Thus, we can completely ignore the presence of derived
constraints in the subsequent discussion about constraint solving and formal
properties of our solver (namely, soundness and termination).

The negated versions of set operators can be introduced as derived
constraints, as well. Specifically, if $p$ is a predicate symbol in $\Pi$, a
new predicate $p^{\prime}$ is associated to $p$ to obtain a positive form
$p^{\prime}(\vec{t})$ for literals $\neg p(\vec{t})$. Then, the definition of
$p^{\prime}$ for $p\in\\{\mathit{un},\parallel\\}$ can be given as a ${\cal
RIS}$-formula, hence, as a derived constraint. The derived constraint for
$\lnot\cup$ and $\lnot\parallel$ (called $\mathit{nun}$ and $\not\parallel$,
respectively) are shown in [Dovier et al. (2000)]. For example, $\lnot A\cup
B=C$ is introduced as:

$\mathit{nun}(A,B,C)\triangleq(n\in C\land n\notin A\land n\notin B)\lor(n\in
A\land n\notin C)\lor(n\in B\land n\notin C)$ (1)

The same approach can be used to define the derived constraint for
$\lnot\subseteq$, $\lnot\cap$ and $\lnot\backslash$, called $\not\subseteq$,
$\mathit{ninters}$ and $\mathit{ndiff}$, respectively. With a little abuse of
terminology, we will refer to atoms based on these predicates as _negative
constraints_. Thanks to the availability of negative constraints, classical
negation is not strictly necessary in $\mathcal{L}_{\mathcal{RIS}}$.

As concerns expressiveness, now $\mathcal{L}_{\mathcal{RIS}}$ supports
equality, set membership, union, disjointness, intersection, difference and
all their negations. Hence, the Boolean algebra of sets is fully supported.

##  3 A Solver for $\mathcal{L}_{\mathcal{RIS}}$

In this section we present a constraint solver for
$\mathcal{L}_{\mathcal{RIS}}$, called $\mathit{SAT}_{\mathcal{RIS}}$. The
solver provides a collection of rewrite rules for rewriting
$\mathcal{L}_{\mathcal{RIS}}$ formulas that are proved to be a decision
procedure for a large class of $\mathcal{L}_{\mathcal{RIS}}$ formulas. As
already observed, however, checking the satisfiability of
$\mathcal{RIS}$-formulas depends on the existence of a decision procedure for
$\mathcal{X}$-formulas (i.e., formulas over $\mathcal{L}_{\mathcal{X}}$).

###  3.1 The solver

$\mathit{SAT}_{\mathcal{RIS}}$ is a rewriting system whose global organization
is shown in Algorithm 1, where STEP is the core of the algorithm.

sort_infer is used to automatically add $\Pi_{\mathcal{T}}$-constraints to the
input formula $\Phi$ to force arguments of $\mathcal{RIS}$-constraints in
$\Phi$ to be of the proper sorts (see Remark 3.1 below). sort_infer is called
twice in Algorithm 1: first, at the beginning of the Algorithm, and second,
within the procedure STEP for the constraints that are generated during
constraint processing. sort_check checks $\Pi_{\mathcal{T}}$-constraints
occurring in $\Phi$: if they are satisfiable, then $\Phi$ is returned
unchanged; otherwise, $\Phi$ is rewritten to $\mathit{false}$.

procedure $\mathsf{STEP}$($\Phi$)  for all $\pi\in\Pi_{\mathcal{S}}\cup\Pi_{\mathcal{T}}:\Phi\leftarrow\mathsf{rw}_{\pi}(\Phi)$;  $\Phi\leftarrow\mathsf{sort\\_check}(\mathsf{sort\\_infer}(\Phi))$ return $\Phi$ procedure $\mathsf{rw}_{\pi}$($\Phi$)  if $\mathit{false}\in\Phi$ then return $\mathit{false}$ else repeat select a $\pi$-constraint $c$ in $\Phi$ apply any applicable rule to $c$ until no rule applies to any $\pi$-constraint  return $\Phi$ |  procedure $\mathit{SAT}_{\mathcal{RIS}}$($\Phi$)  $\Phi\leftarrow\textsf{sort\\_infer}(\Phi)$ repeat $\Phi^{\prime}\leftarrow\Phi$ repeat $\Phi^{\prime\prime}\leftarrow\Phi$ $\Phi\leftarrow\textsf{STEP}(\Phi)$ until $\Phi=\Phi^{\prime\prime}$ $\Phi\leftarrow\textsf{remove\\_neq}(\Phi)$ until $\Phi=\Phi^{\prime}$ $\Phi\textbf{ is }\Phi_{\mathcal{S}}\land\Phi_{\mathcal{X}}$ $\Phi\leftarrow\Phi_{\mathcal{S}}\land\mathit{SAT}_{\mathcal{X}}(\Phi_{\mathcal{X}})$ return $\Phi$
---|---
Algorithm 1 The $\mathit{SAT}_{\mathcal{RIS}}$ solver. $\Phi$ is the input
formula.

remove_neq deals with the elimination of $\neq$-constraints involving
variables of sort $\mathsf{Set}$, possibly occurring in the formula $\Phi$ at
the end of the innermost loop of $\mathit{SAT}_{\mathcal{RIS}}$. Its
motivation and definition will be made evident later in Section 3.4.

STEP applies specialized rewriting procedures to the current formula $\Phi$
and returns either $\mathit{false}$ or the modified formula. Each rewriting
procedure applies a few non-deterministic rewrite rules which reduce the
syntactic complexity of $\mathcal{RIS}$-constraints of one kind. Procedure
$\mathsf{rw}_{\pi}$ in Algorithm 1 represents the rewriting procedure for
($\Pi_{\mathcal{S}}\cup\Pi_{\mathcal{T}}$)-constraints. The execution of STEP
is iterated until a fixpoint is reached—i.e., the formula cannot be simplified
any further. STEP returns $\mathit{false}$ whenever (at least) one of the
procedures in it rewrites $\Phi$ to $\mathit{false}$. In this case, a fixpoint
is immediately detected, since $\textsf{STEP}(\mathit{false})$ returns
$\mathit{false}$. The rewrite rules for $\mathcal{RIS}$-constraints involving
only extensional set terms are described in Section 3.2, while those for
$\mathcal{RIS}$-constraints involving both extensional and RIS terms are
detailed in Section 3.3.

$\mathit{SAT}_{\mathcal{X}}$ is the constraint solver for
$\mathcal{X}$-formulas. The formula $\Phi$ can be seen, without loss of
generality, as $\Phi_{\mathcal{S}}\land\Phi_{\mathcal{X}}$, where
$\Phi_{\mathcal{S}}$ is a pure $\mathcal{RIS}$-formula and
$\Phi_{\mathcal{X}}$ is a $\mathcal{X}$-formula. $\mathit{SAT}_{\mathcal{X}}$
is applied only to the $\Phi_{\mathcal{X}}$ conjunct of $\Phi$. Note that,
conversely, STEP rewrites only $\mathcal{RIS}$-constraints, while it leaves
all other atoms unchanged. Nonetheless, as the rewrite rules show,
$\mathit{SAT}_{\mathcal{RIS}}$ generates $\mathcal{X}$-formulas that are
conjoined to $\Phi_{\mathcal{X}}$ so they are later solved by
$\mathit{SAT}_{\mathcal{X}}$.

As we will show in Section 4, when all the non-deterministic computations of
$\mathit{SAT}_{\mathcal{RIS}}(\Phi)$ terminate with $\mathit{false}$, then we
can conclude that $\Phi$ is unsatisfiable; otherwise, when all the
computations terminate and at least one of them does not return
$\mathit{false}$, then we can conclude that $\Phi$ is satisfiable and each
solution of the formulas returned by $\mathit{SAT}_{\mathcal{RIS}}$ is a
solution of $\Phi$, and vice versa.

######  Remark 3.1.

$\mathcal{L}_{\mathcal{RIS}}$ does not provide variable declarations. The sort
of variables are enforced by adding suitable _sort constraints_ to the formula
to be processed. Sort constraints are automatically added by the solver.
Specifically, a constraint $\mathit{set}(y)$ (resp., $\mathit{isX}(y)$) is
added for each variable $y$ which is required to be of sort $\mathsf{Set}$
(resp., $\mathsf{X}$). For example, given
$X=\\{y\mathbin{\scriptstyle\sqcup}A\\}$, sort_infer conjoins the sort
constraints $\mathit{set}(X)$, $\mathit{isX}(y)$ and $\mathit{set}(A)$. If the
set of function and predicate symbols of $\mathcal{RIS}$ and $\mathcal{X}$ are
disjoint, there is a unique sort constraint for each variable in the formula.

The rewrite rules used by $\mathit{SAT}_{\mathcal{RIS}}$ are defined as
follows.

######  Definition 3.2 (Rewrite rules).

If $\pi$ is a symbol in $\Pi_{\mathcal{S}}\cup\Pi_{\mathcal{T}}$ and $p$ is a
$\mathcal{RIS}$-constraint based on $\pi$, then a _rewrite rule for
$\pi$-constraints_ is a rule of the form
$p\longrightarrow\Phi_{1}\lor\dots\lor\Phi_{n}$, where $\Phi_{i}$, $i\geq 1$,
are $\mathcal{RIS}$-formulas. Each atom matching $p$ is non-deterministically
rewritten to one of the $\Phi_{i}$. Variables appearing in the right-hand side
but not in the left-hand side are assumed to be fresh variables, implicitly
existentially quantified over each $\Phi_{i}$. ∎

A _rewriting procedure_ for $\pi$-constraints consists of the collection of
all the rewrite rules for $\pi$-constraints. For each rewriting procedure,
STEP selects rules in the order they are listed in the figures below. The
first rule whose left-hand side matches the input $\pi$-constraint is used to
rewrite it. If no rule applies, then the input constraint is left unchanged
(i.e., it is irreducible).

###  3.2 Rewrite rules for extensional set terms

When $\mathcal{L}_{\mathcal{RIS}}$ formulas contain only extensional set
terms, all the operators defined in $\Pi_{\mathcal{S}}$ are dealt with the
rewrite rules given in [Dovier et al. (2000)]. In particular, set equality
between extensional set terms is implemented by _$(Ab)(C\ell)$ -set
unification_ [Dovier et al. (2006)]. One of the key rewrite rules of set
unification is the following, which implements axioms ($Ab$) and ($C\ell$)
(adapted from [Dovier et al. (2000)]):

$\displaystyle\\{t_{1}\mathbin{\scriptstyle\sqcup}A\\}$
$\displaystyle=\\{t_{2}\mathbin{\scriptstyle\sqcup}B\\}\longrightarrow$
$\displaystyle t_{1}=_{\mathcal{X}}t_{2}\land A=B\quad$
$\displaystyle\lor\quad$ $\displaystyle
t_{1}=_{\mathcal{X}}t_{2}\land\\{t_{1}\mathbin{\scriptstyle\sqcup}A\\}=B\quad\qquad\lor$
(2) $\displaystyle t_{1}=_{\mathcal{X}}t_{2}\land
A=\\{t_{2}\mathbin{\scriptstyle\sqcup}B\\}\quad$ $\displaystyle\lor\quad$
$\displaystyle
A=\\{t_{2}\mathbin{\scriptstyle\sqcup}N\\}\land\\{t_{1}\mathbin{\scriptstyle\sqcup}N\\}=B$

where $A$ and $B$ are extensional sets, $t_{1}$ and $t_{2}$ are arbitrary
$\mathcal{X}$-terms, $N$ is a new variable (of sort $\mathsf{Set}$), and
$=_{\mathcal{X}}$ is the equality provided by the theory $\mathcal{X}$. This
means that every time $\mathcal{L}_{\mathcal{RIS}}$ finds an atom such as the
left-hand side of rule (3.2), it attempts to find a solution for it in four
different ways. In some cases one or more will fail (i.e., they will be
$\mathit{false}$) but in general $\mathcal{L}_{\mathcal{RIS}}$ will compute
all the four solutions.

In this paper we will extend the set unification algorithm of [Dovier et al.
(2006)] to deal with also RIS terms.

Given that the rules for extensional set terms has been extensively studied by
the authors [Dovier et al. (2000), Dovier et al. (2006), Cristiá et al.
(2015), Cristiá and Rossi (2019)], they are not shown here, and can be found
in [Cristiá and Rossi (2019)].

###  3.3 Rewrite rules for RIS

When a $\mathcal{L}_{\mathcal{RIS}}$ formula includes RIS terms, the rewrite
rules for extensional sets are extended in a rather natural way. The following
is an example to intuitively show how $\mathit{SAT}_{\mathcal{RIS}}$ works
when RIS are involved.

######  Example 3.3.

If $S$ is a variable and $a,b$ are constants belonging to
$\mathcal{F}_{\mathcal{X}}$, then $\mathit{SAT}_{\mathcal{RIS}}$ can determine
the satisfiability of:

$\\{(x,y):\\{(a,1)\mathbin{\scriptstyle\sqcup}S\\}\mid
x\in\\{a,b\\}\\}=\\{(a,1)\\}$

by proceeding as follows (the arrow indicates a rewriting step; some steps are
simplified):

$\displaystyle\\{(x,y):\\{(a,1)\mathbin{\scriptstyle\sqcup}S\\}\mid
x\in\\{a,b\\}\\}=\\{(a,1)\\}$ $\displaystyle\rightarrow(x,y)=(a,1)\land
x\in\\{a,b\\}\land\\{(a,1)\mathbin{\scriptstyle\sqcup}\\{(x,y):S\mid
x\in\\{a,b\\}\\}\\}=\\{(a,1)\\}$ $\displaystyle\quad{}\lor(x,y)=(a,1)\land
x\notin\\{a,b\\}\land\\{(x,y):S\mid x\in\\{a,b\\}\\}=\\{(a,1)\\}$
$\displaystyle\rightarrow x=a\land y=1\land(x=a\lor x=b)$
$\displaystyle\qquad{}\land(\\{(x,y):S\mid
x\in\\{a,b\\}\\}=\emptyset\lor\\{(x,y):S\mid x\in\\{a,b\\}\\}=\\{(a,1)\\})$
$\displaystyle\quad{}\lor\mathit{false}$ $\displaystyle\rightarrow x=a\land
y=1$ $\displaystyle\quad{}\land(S=\emptyset\lor
S=\\{(a,1)\mathbin{\scriptstyle\sqcup}N\\}\land(a,1)\notin
N\land\\{(x,y):N\mid x\in\\{a,b\\}\\}=\emptyset)$

where $N$ is a fresh variable. At this point, Algorithm 1 stops thus returning
a disjunction of two $\mathcal{L}_{\mathcal{RIS}}$ formulas:

$\displaystyle x=a\land y=1\land S=\emptyset$ $\displaystyle\lor x=a\land
y=1\land S=\\{(a,1)\mathbin{\scriptstyle\sqcup}N\\}\land(a,1)\notin
N\land\\{(x,y):N\mid x\in\\{a,b\\}\\}=\emptyset$

which are surely satisfiable. The first one because all variables are bound to
terms and the second one because:

$(a,1)\notin N\land\\{(x,y):N\mid x\in\\{a,b\\}\\}=\emptyset$

is satisfiable by substituting $N$ by the empty set. ∎

Hence, intuitively, the key idea behind the extension of the rewriting rules
for extensional set terms to RIS terms is a sort of _lazy partial evaluation_
of RIS. That is, a RIS term is treated as a block until it is necessary to
identify one of its elements. When that happens, the RIS is transformed into
an extensional set whose element part is the identified element and whose set
part is the rest of the RIS. At this point, classic set constraint rewriting
(in particular set unification) can be applied. More precisely, when a term
such as
$\\{x:\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}$ is
processed, two cases are considered:

  * •

$x=d$ and $\phi$ holds for $d$, in which case the RIS is rewritten as the
extensional set
$\\{u(d)\mathbin{\scriptstyle\sqcup}\\{x:D\mid\phi\mathbin{\bullet}u\\}\\}$;
and

  * •

$x=d$ but $\phi$ does not hold for $d$, i.e., $\neg\phi(d)$ holds, in which
case the RIS is rewritten as $\\{x:D\mid\phi\mathbin{\bullet}u\\}$.

The main rewrite rules for $\Pi_{\mathcal{S}}$-constraints dealing with RIS
terms are given in Figures 1-4 and are discussed below; rules for special
cases are presented in Appendix A. In order to make the presentation more
accessible: _a_) the rules are given for RIS whose domain is not another RIS,
in particular, the domain of a variable-RIS is a single variable; and _b_) the
control term of RIS is always a _variable_. The generalization to cases in
which these restrictions are removed is discussed in Appendix A. In these
figures, a RIS of the form $\\{x:D\mid\phi\mathbin{\bullet}u\\}$ is
abbreviated as $\\{D\mid\phi\mathbin{\bullet}u\\}$. Besides, $\phi(d)$,
$\gamma(d)$, $u(d)$ and $v(d)$ are shorthands for $\phi[x\mapsto d]$,
$\gamma[x\mapsto d]$, $u[x\mapsto d]$ and $v[x\mapsto d]$, respectively, where
$[x\mapsto d]$ represents variable substitution. In all rules, $\varnothing$
represents either $\emptyset$ or a RIS with empty domain (e.g.,
$\\{\emptyset\mid\phi\mathbin{\bullet}u\\}$). Recall the notation used across
the paper given in Remark 2.8.

####  3.3.1 Equality

Figure 1 lists the main rewrite rules applied by STEP to deal with constraints
of the form $A=B$ and $A\neq B$, where $A$ and $B$ are
$\mathcal{L}_{\mathcal{RIS}}$ set terms and at least one of them is a RIS
term.

Equality between a RIS and an extensional set is governed by rules (3)–(7). In
particular:

  * •

Rule (5) deals with the case in which a RIS with a non-empty domain must be
equal to the empty set. It turns out that to force a RIS
$\\{D\mid\phi\mathbin{\bullet}u\\}$ to be empty it is enough that the filter
$\phi$ is false for all elements in $D$, i.e., $\forall x\in D:\lnot\phi$ (see
Proposition C.3 in the appendix). This restricted universal quantification is
conveniently implemented through recursion, by extracting one element $d$ at a
time from the RIS domain.

  * •

Rule (6) deals with the case illustrated by Example 3.3, i.e., equality
between a non-variable RIS and any other non-empty set (including variables
and RIS).

  * •

Rule (7) deals with equality between a variable-RIS and an extensional set.
The intuition behind this rule is as follows. Given that
$\\{t\mathbin{\scriptstyle\sqcup}A\\}$ is not empty, then $\bar{D}$ must be
not empty in which case it is equal to $\\{n\mathbin{\scriptstyle\sqcup}N\\}$
for some $n$ and $N$. Furthermore, $n$ must satisfy $\phi$ and $u(n)$ must be
equal to $t$. As the first element of $\\{t\mathbin{\scriptstyle\sqcup}A\\}$
belongs to the RIS, then the rest of the RIS must be equal to $A$. It is not
necessary to consider the case where $\lnot\phi(n)$, as in rule (6), because
$n$ is a fresh variable.

Other rules deal with the symmetric cases (e.g.,
$B=\\{\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}$,
$\\{t\mathbin{\scriptstyle\sqcup}A\\}=\\{\bar{D}\mid\phi\mathbin{\bullet}u\\}$),
and with special cases where some variables are shared between the two terms
to be compared (e.g.,
$\\{\bar{D}\mid\phi\mathbin{\bullet}u\\}=\\{t\mathbin{\scriptstyle\sqcup}\bar{D}\\}$),
see Appendix A. The cases not considered by any rule, namely, equality between
a variable and a variable-RIS, between a variable-RIS and the empty set, and
between two variable-RIS, are dealt with as irreducible (see Section 4.2).

Negated equality is governed by rule (8). Note that this rule serves for all
combinations of set terms and it is based on the definition of set inequality.
In fact, $D$ can be either a variable, or a variable-RIS, or a set term of the
form $\\{d\mathbin{\scriptstyle\sqcup}D\\}$, while $A$ can be any term,
including another RIS. In this case, the problem is handed over to the rules
for set membership.

$\displaystyle\\{\emptyset\mid\phi\mathbin{\bullet}u\\}=\varnothing\rightarrow\mathit{true}$
(3)
$\displaystyle\\{\emptyset\mid\phi\mathbin{\bullet}u\\}=\\{t\mathbin{\scriptstyle\sqcup}A\\}\rightarrow\mathit{false}$
(4)
$\displaystyle\\{\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}=\varnothing\rightarrow\lnot\phi(d)\land\\{D\mid\phi\mathbin{\bullet}u\\}=\emptyset$
(5) $\displaystyle\begin{split}&\text{If $B$ is any set term except
$\varnothing$:}\\\
&\\{\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}=B\rightarrow\\\
&(\phi(d)\land\\{u(d)\mathbin{\scriptstyle\sqcup}\\{D\mid\phi\mathbin{\bullet}u\\}\\}=B)\lor(\lnot\phi(d)\land\\{D\mid\phi\mathbin{\bullet}u\\}=B)\end{split}$
(6)
$\displaystyle\begin{split}&\\{\bar{D}\mid\phi\mathbin{\bullet}u\\}=\\{t\mathbin{\scriptstyle\sqcup}A\\}\rightarrow\\\
&\bar{D}=\\{n\mathbin{\scriptstyle\sqcup}N\\}\land\phi(n)\land
t=_{\mathcal{X}}u(n)\land\\{N\mid\phi\mathbin{\bullet}u\\}=A\end{split}$ (7)
$\displaystyle\begin{split}&\\{D\mid\phi\mathbin{\bullet}u\\}\neq
A\rightarrow\\\ &(n\in\\{D\mid\phi\mathbin{\bullet}u\\}\land n\notin
A)\lor(n\notin\\{D\mid\phi\mathbin{\bullet}u\\}\land n\in A)\end{split}$ (8)

Figure 1: Rewrite rules for $A=B$ and $R\neq B$; $A$ or $B$ RIS terms

####  3.3.2 Membership

Rules dealing with constraints of the form $t\in A$ and $t\notin A$, where $t$
is a $\mathcal{L}_{\mathcal{X}}$ term and $A$ is a RIS term, are listed in
Figure 2. The case $t\notin\bar{A}$ where $\bar{A}$ is a variable-RIS is dealt
with as irreducible (Section 4.2), while constraints of the form $t\in A$ are
eliminated in all cases.

$\displaystyle
t\in\\{\emptyset\mid\phi\mathbin{\bullet}u\\}\longrightarrow\mathit{false}$
(9) $\displaystyle t\in\\{D\mid\phi\mathbin{\bullet}u\\}\longrightarrow n\in
D\land\phi(n)\land t=_{\mathcal{X}}u(n)$ (10) $\displaystyle
t\notin\\{\emptyset\mid\phi\mathbin{\bullet}u\\}\longrightarrow\mathit{true}$
(11)
$\displaystyle\begin{split}&t\notin\\{\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}\longrightarrow\\\
&(\phi(d)\land t\neq_{\mathcal{X}}u(d)\land
t\notin\\{D\mid\phi\mathbin{\bullet}u\\})\lor(\lnot\phi(d)\land
t\notin\\{D\mid\phi\mathbin{\bullet}u\\})\end{split}$ (12)

Figure 2: Rewrite rules for $t\in A$ and $t\notin A$; $A$ RIS term

####  3.3.3 Union

The rules for the union operator are given in Figure 3.

  * •

Rules (14)-(16) extend similar rules dealing with extensional set terms to the
case where one argument is a RIS whose domain is the empty set. In these
cases, $\mathit{un}$-constraints are rewritten to equality constraints and
rules of Figure 1 are called into play.

  * •

Rules (17)-(19) are the same used for extensional set terms; the use of set
unification, however, forces arguments which are RIS terms to be possibly
converted into extensional sets.

  * •

Finally, rule (20) is added to deal with constraints where at least one
argument is a non variable-RIS and cannot be dealt with by the previous rules.
For example, rule (19) cannot be used when the last argument is a RIS, then
rule (20) is used instead.

In rule (20), each non variable-RIS is rewritten into either an extensional
set or a new RIS with one element less in its domain, plus the constraints
that assert or negate the filter. This is formalized by functions
$\mathcal{S}$ and $\mathcal{C}$.

The cases not considered in Figure 3, that is, when the three arguments are
either variables or variables-RIS and the first two are not the same variable,
are dealt with as irreducible (Section 4.2).

The rule for $\mathit{nun}$ is the standard rule for extensional set terms
(cf. rule (1)).

$\displaystyle\mathit{un}(X,X,B)\rightarrow X=B$ (13)
$\displaystyle\mathit{un}(A,B,\varnothing)\rightarrow A=\emptyset\land
B=\emptyset$ (14) $\displaystyle\mathit{un}(\varnothing,A,B)\rightarrow B=A$
(15) $\displaystyle\mathit{un}(A,\varnothing,B)\rightarrow B=A$ (16)
$\displaystyle\begin{split}\mathit{un}&(\\{t\sqcup
C\\},A,\bar{B})\rightarrow\\\ &\\{t\sqcup C\\}=\\{t\sqcup N_{1}\\}\land
t\notin N_{1}\land\bar{B}=\\{t\sqcup N\\}\\\ &\land(t\notin
A\land\mathit{un}(N_{1},A,N)\lor A=\\{t\sqcup N_{2}\\}\land t\notin
N_{2}\land\mathit{un}(N_{1},N_{2},N))\end{split}$ (17)
$\displaystyle\begin{split}\mathit{un}&(A,\\{t\sqcup
C\\},\bar{B})\rightarrow\\\ &\\{t\sqcup C\\}=\\{t\sqcup N_{1}\\}\land t\notin
N_{1}\land\bar{B}=\\{t\sqcup N\\}\\\ &\land(t\notin
A\land\mathit{un}(N_{1},A,N)\lor A=\\{t\sqcup N_{2}\\}\land t\notin
N_{2}\land\mathit{un}(N_{1},N_{2},N))\end{split}$ (18)
$\displaystyle\begin{split}\mathit{un}&(A,B,\\{t\sqcup C\\})\rightarrow\\\
&\\{t\sqcup C\\}=\\{t\sqcup N\\}\\\ &\land(A=\\{t\sqcup N_{1}\\}\land t\notin
N_{1}\land\mathit{un}(N_{1},B,N)\\\ &\qquad\lor B=\\{t\sqcup N_{1}\\}\land
t\notin N_{1}\land\mathit{un}(A,N_{1},N)\\\ &\qquad\lor A=\\{t\sqcup
N_{1}\\}\land t\notin N_{1}\land B=\\{t\sqcup N_{2}\\}\land t\notin
N_{2}\land\mathit{un}(N_{1},N_{2},N))\end{split}$ (19) If at least one of
$A,B,C$ is not a variable nor a variable-RIS:
$\displaystyle\mathit{un}(A,B,C)\rightarrow\mathit{un}(\mathcal{S}(A),\mathcal{S}(B),\mathcal{S}(C))\land\mathcal{C}(A)\land\mathcal{C}(B)\land\mathcal{C}(C)$
(20) where $\mathcal{S}$ is a set-valued function and $\mathcal{C}$ is a
constraint-valued function
$\displaystyle\quad\mathcal{S}(\sigma)=\begin{cases}N_{\sigma}&\text{if
$\sigma\equiv\\{\\{d\sqcup D\\}\mid\phi\mathbin{\bullet}u\\}$}\\\
\sigma&\text{otherwise}\end{cases}$
$\displaystyle\quad\mathcal{C}(\sigma)=\begin{cases}N_{\sigma}=(\\{u(d)\sqcup\\{D\mid\phi\mathbin{\bullet}u\\}\\}\land\phi(d))&\text{if
$\sigma\equiv\\{\\{d\sqcup D\\}\mid\phi\mathbin{\bullet}u\\}$}\\\
\quad{}\lor(N_{\sigma}=\\{D\mid\phi\mathbin{\bullet}u\\}\land\lnot\phi(d))&\\\
\mathit{true}&\text{otherwise}\end{cases}$

Figure 3: Rewrite rules for $\mathit{un}(A,B,C)$; $A$, $B$ or $C$ a RIS term

####  3.3.4 Disjointness

The rules for the $\parallel$ operator are listed in Figure 4. As with the
other operators, some of the standard rules for extensional set terms are
extended to deal with RIS and new rules are added. In particular:

  * •

Rule (22) is simply extended to RIS whose domain is the empty set.

  * •

Rule (26) is a new rule dealing with the case when the second argument is a
non variable-RIS. As can be seen, two cases are considered depending on
whether the filter holds or not for one of the elements of the domain. In the
first case, the rules for $\notin$ are called and then a recursion is started;
in the second case only the recursive call is made.

Note that $A\parallel B$ is not further rewritten if $A$ and $B$ are distinct
variables or variable-RIS. The rule for $\not\parallel$ is the standard rule
for extensional set terms (see [Cristiá and Rossi (2019)]).

$\displaystyle X\parallel X\rightarrow X=\emptyset$ (21) $\displaystyle
A\parallel\varnothing\rightarrow\mathit{true}$ (22)
$\displaystyle\varnothing\parallel A\rightarrow\mathit{true}$ (23)
$\displaystyle A\parallel\\{t\sqcup B\\}\rightarrow t\notin A\land A\parallel
B$ (24) $\displaystyle\\{t\sqcup B\\}\parallel A\rightarrow t\notin A\land
A\parallel B$ (25) $\displaystyle\begin{split}A\parallel&\\{\\{d\sqcup
D\\}\mid\phi\mathbin{\bullet}u\\}\rightarrow\\\ &\phi(d)\land u(d)\notin
A\land A\parallel\\{D\mid\phi\mathbin{\bullet}u\\}\lor\lnot\phi(d)\land
A\parallel\\{D\mid\phi\mathbin{\bullet}u\\}\end{split}$ (26)
$\displaystyle\begin{split}\\{\\{d&\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}\parallel
A\rightarrow\\\ &\phi(d)\land u(d)\notin
A\land\\{D\mid\phi\mathbin{\bullet}u\\}\parallel
A\lor\lnot\phi(d)\land\\{D\mid\phi\mathbin{\bullet}u\\}\parallel A\end{split}$
(27)

Figure 4: Rewrite rules for $A\parallel B$; $A$ or $B$ a RIS term

###  3.4 Procedure remove_neq

The ${\cal RIS}$-formula returned by Algorithm 1 when STEP reaches a fixpoint
is not guaranteed to be satisfiable due to the presence of inequalities
involving set variables. For example, the formula
$D\neq\emptyset\land\\{x:D\mid x=x\\}=\emptyset$ is dealt with by
$\mathit{SAT}_{\mathcal{RIS}}$ as irreducible but it is clearly unsatisfiable.
In order to guarantee satisfiability, all such inequalities must be removed
from the final formula returned by $\mathit{SAT}_{\mathcal{RIS}}$. This is
performed (see Algorithm 1) by executing the procedure remove_neq, which
applies the rewrite rule described by the generic rule scheme of Figure 5.
Basically, this rule exploits set extensionality to state that non-equal sets
can be distinguished by asserting that a fresh element ($n$) belongs to one
but not to the other.

If $A\in\mathcal{V}_{S}$, $t:\mathsf{X}$ and $\Phi$ is the input formula then:

$\begin{split}&\text{If $A$ is an argument of a $\mathit{un}$-constraint or
the domain of a variable-RIS}\\\ &\text{occurring as the argument of either a
$=$ or $\notin$ or $\mathit{un}$ constraint in $\Phi$:}\\\ &A\neq
t\rightarrow(n\in A\land n\notin t)\lor(n\in t\land n\notin A)\end{split}$
(28)

Figure 5: Rule scheme for $\neq$-constraint elimination rules

######  Example 3.4.

Given the formula
$D\neq\emptyset\land\\{x:D\mid\phi\mathbin{\bullet}u\\}=\emptyset$, remove_neq
rewrites $D\neq\emptyset$ as $n\in D$, where $n$ is a fresh variable. In turn,
$n\in D$ is rewritten as $D=\\{n\mathbin{\scriptstyle\sqcup}N\\}$ for another
fresh variable $N$. Finally, the whole formula is rewritten as
$D=\\{n\mathbin{\scriptstyle\sqcup}N\\}\land\\{x:\\{n\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}=\emptyset$,
which fires one of the rules given in Section 3.2. This rewriting chain is
fired only because $D$ is the domain of a RIS; otherwise remove_neq does
nothing with $D\neq\emptyset$. ∎

##  4 Decidability of $\mathcal{L}_{\mathcal{RIS}}$ Formulas

In this section we show that $\mathit{SAT}_{\mathcal{RIS}}$ can serve as a
decision procedure for a large fragment of $\mathcal{L}_{\mathcal{RIS}}$. To
this end, first we precisely characterize the admissible
$\mathcal{L}_{\mathcal{RIS}}$ formulas involving RIS; then we prove that:
_(a)_ when $\mathit{SAT}_{\mathcal{RIS}}$ terminates the answer is either
$\mathit{false}$ or a disjunction of $\mathcal{L}_{\mathcal{RIS}}$ formulas of
a very particular form; _(b)_ that disjunction is always satisfiable, and a
solution can be trivially found; _(c)_ the set of solutions of the computed
formula is the same of the input formula; and _(d)_
$\mathit{SAT}_{\mathcal{RIS}}$ terminates for every admissible formula.
Detailed proofs are given in Appendix C.

###  4.1 Admissible formulas

RIS are intended to denote finite sets. For this reason, RIS have the
restriction that the RIS domain must be a finite—though unbounded—set.
However, this is not enough to guarantee RIS finiteness.

######  Example 4.1.

The $\mathcal{L}_{\mathcal{RIS}}$ formula

$A=\\{1\mathbin{\scriptstyle\sqcup}\\{x:A\mid\mathit{true}\mathbin{\bullet}(x,y)\\}$
(29)

admits only the solution binding $A$ to the infinite set
$\\{1,(1,y),((1,y),y),$ $(((1,y),y),y),\dots\\}$. If
$\mathit{SAT}_{\mathcal{RIS}}$ is requested to solve this formula, it will
loop forever trying to build the extensional set term representing this
infinite set. ∎

In the rest of this section, we will analyze this kind of “cyclic”
definitions, introducing a few restrictions on $\mathcal{RIS}$-formulas that
prevent them from defining infinite sets.

First of all, observe that we have assumed that the set
$\mathcal{V}_{\mathcal{S}}$ of variables ranging over $\mathcal{RIS}$-terms
(i.e., set variables) and the set $\mathcal{V}_{\mathcal{X}}$ of variables
ranging over $\mathcal{X}$-terms are disjoint sets. Since RIS filters are
$\mathcal{X}$-formulas, then set variables cannot occur in them. This fact
prevents us from creating _recursively defined_ RIS of the form
$S=\\{c:D\mid\phi(S)\mathbin{\bullet}u\\}$. Moreover, since RIS patterns, as
well as elements of RIS domains, are $\mathcal{X}$-terms, then no cyclic
definitions of the form $S=\\{c:D\mid\phi\mathbin{\bullet}u(S)\\}$ or
$S=\\{c:\\{t_{1},\dots,S,\dots,t_{n}\mathbin{\scriptstyle\sqcup}A\\}\mid\phi\mathbin{\bullet}u\\}$
can be written in $\mathcal{L}_{\mathcal{RIS}}$.

Hence, the only possible way to create a cyclic definition involving a RIS is
through the set variable possibly occurring as the set part of the RIS domain,
e.g.,
$S=\\{c:\\{t_{1},\dots,t_{n}\mathbin{\scriptstyle\sqcup}S\\}\mid\phi\mathbin{\bullet}u\\}$.
When the pattern is the same as the control term, an equation such as
$S=\\{c:\\{t_{1},\dots,t_{n}\mathbin{\scriptstyle\sqcup}S\\}\mid\phi\\}$
admits the trivial solution in which $S$ is bound to the (finite) set
containing all $t_{i}$, $i=1,\dots,n$, such that $\phi(t_{i})$ holds. For
example, $S=\\{x:\\{-1,0,1\mathbin{\scriptstyle\sqcup}S\\}\mid x\neq 0\\}$ has
the solution $S=\\{-1,1\mathbin{\scriptstyle\sqcup}N\\}$, where $N$ is a fresh
variable. This is no longer true when the pattern is not the control term, for
instance as in formula (29). In other words, when the pattern is the control
term, then the RIS is a subset of the domain, while in all other cases this
relation does not hold.

As a consequence, processing a formula such as (29) may cause
$\mathit{SAT}_{\mathcal{RIS}}$ to enter into an infinite loop. In order to
allow $\mathit{SAT}_{\mathcal{RIS}}$ to be a decision procedure for
$\mathcal{L}_{\mathcal{RIS}}$, formulas such as (29) should be discarded.

In what follows, we provide sufficient (syntactic) conditions characterizing a
sub-language of $\mathcal{L}_{\mathcal{RIS}}$ for which
$\mathit{SAT}_{\mathcal{RIS}}$ will be proved to terminate and so to be a
decision procedure for that sub-language.

First, we define a transformation $\tau$ of $\mathcal{RIS}$-formulas that
allows us to restrict our attention to a single kind of constraints. Let
$\Phi=\Phi_{\mathcal{S}}\land\Phi_{\mathcal{X}}$ be the input formula, where
$\Phi_{\mathcal{S}}$ is a pure $\mathcal{RIS}$-formula and
$\Phi_{\mathcal{X}}$ is a $\mathcal{X}$-formula; $\Phi_{\mathcal{X}}$ is
removed from $\Phi$ and so we only consider its pure RIS part. Without loss of
generality, $\Phi_{\mathcal{S}}$ can be seen as
$\Phi_{1}\lor\dots\lor\Phi_{n}$, where the $\Phi_{i}$’s are conjunctions of
primitive $\mathcal{RIS}$-constraints (i.e., all derived constraints have been
replaced by their definitions and the corresponding DNF has been built). Then,
each $\Phi_{i}$ is transformed into $\Phi_{i}^{\prime}$ as follows:

  * •

constraints of the form $\mathit{un}(A,B,C)$, where $A,B,C$ are either
variables or variable-RIS whose innermost domain variables are $D_{A}$,
$D_{B}$, $D_{C}$, and none of these domain variables occur elsewhere in
$\Phi_{i}$, are removed from the formula

  * •

constraints of the form $A=B$, where neither is $\varnothing$, are rewritten
into $\mathit{un}(A,B,B)\land\mathit{un}(B,A,A)$

  * •

If one of the arguments of a $\mathit{un}$ constraint is of the form
$\\{x_{1},\dots,x_{n}\mathbin{\scriptstyle\sqcup}B\\}$ then it is replaced by
a new variable, $N$, and $\mathit{un}(\\{x_{1},\dots,x_{n}\\},B,N)$ is
conjoined to the formula.

  * •

all the $\neq$, $\in$, $\notin$, $\parallel$, and $\mathit{set}$ constraints,
and all the remaining $=$ constraints, are removed from the formula.

Hence, $\tau(\Phi)=\Phi_{1}^{\prime}\lor\dots\lor\Phi_{n}^{\prime}$, where
each $\Phi_{i}^{\prime}$ is a conjunction of $\mathit{un}$-constraints.

The following function allows to classify set terms occurring as arguments of
$\mathit{un}$-constraints.

######  Definition 4.2.

Let $\mathcal{T}$ be a function that takes a set term $T$ and returns an
element in $\\{\mathsf{S},\mathsf{P},\mathsf{U}\\}$, where $\mathsf{P}$
depends on one argument belonging to $\\{\mathsf{S},\mathsf{P},\mathsf{U}\\}$
and $\mathsf{U}$ depends on two arguments belonging to
$\\{\mathsf{S},\mathsf{P},\mathsf{U}\\}$. For each constraint of the form
$\mathit{un}(A,B,C)$ the function $\mathcal{T}(T)$ is defined as follows (note
that the definition of $\mathcal{T}$ depends on the position of the argument
in the constraint):

  1. 1.

If $T$ is $C$, then:
$\mathcal{T}(C)=\mathsf{U}(\mathcal{T}(A),\mathcal{T}(B))$

  2. 2.

If $T$ is either $A$ or $B$, then:

$\displaystyle\mathcal{T}(\emptyset)=\mathsf{S}$ (30)
$\displaystyle\mathcal{T}(\\{\cdot\mathbin{\scriptstyle\sqcup}V\\})=\mathcal{T}(V)$
(31) $\displaystyle\mathcal{T}(\\{c:D\mid F\\})=\mathcal{T}(D)$ (32)
$\displaystyle\mathcal{T}(\\{c:D\mid
F\mathbin{\bullet}P\\})=\mathsf{P}(\mathcal{T}(D)),c\not\equiv P$ (33)

and $\mathcal{T}(T)$ remains undefined when $T$ is a variable.

∎

######  Example 4.3.

If $\Phi_{i}$ is $\\{x:D\mid F\mathbin{\bullet}(x,y)\\}\subseteq D$, then
$\Phi_{i}^{\prime}$ is

$\mathit{un}(\\{x:D\mid F\mathbin{\bullet}(x,y)\\},D,D)$

and the $\mathcal{T}$ function for this constraint is:

$\displaystyle\mathcal{T}(D)=\mathsf{U}(\mathcal{T}(D),\mathcal{T}(\\{x:D\mid
F\mathbin{\bullet}(x,y)\\}))$
$\displaystyle\Leftrightarrow\mathcal{T}(D)=\mathsf{U}(\mathcal{T}(D),\mathsf{P}(\mathcal{T}(D)))$

where the computation of $\mathcal{T}$ stops because $D$ is a variable. ∎

######  Definition 4.4.

$\mathsf{P}^{*}(D)$ denotes a $\mathsf{P}$ that at some point depends on
variable $D$. ∎

######  Definition 4.5 (Admissible $\mathcal{RIS}$-formula).

Let $\Phi$ be a $\mathcal{RIS}$-formula not in solved form and $\mathcal{E}$
be the collection of equalities computed by (recursively) applying the
$\mathcal{T}$ function to all the $\mathit{un}$-constraints in $\tau(\Phi)$
and performing all possible term substitutions. Then $\Phi$ is _non-
admissible_ iff $\mathcal{E}$ contains at least one equality of the form
$X=\mathsf{U}(Y,Z)$ such that:

  * •

If $X$ depends on $\mathsf{P}^{*}(D)$, for some variable $D$, then $Y$ or $Z$
does not depend on $\mathsf{P}^{*}(D)$; and

  * •

If $Y$ or $Z$ depend on $\mathsf{P}^{*}(D)$, for some variable $D$, then $X$
does not depend on $\mathsf{P}^{*}(D)$.

All other $\mathcal{RIS}$-formulas are _admissible_. ∎

######  Example 4.6.

Given the formula $\Phi$

$\\{x:D\mid F\mathbin{\bullet}(x,y)\\}\subseteq D\land D\neq\emptyset$

then $\tau(\Phi)$ is

$\mathit{un}(\\{x:D\mid F\mathbin{\bullet}(x,y)\\},D,D)$

that is exactly the formula of Example 4.3. So $\Phi$ is classified as non-
admissible. Conversely, if $\Phi$ is just $\\{x:D\mid
F\mathbin{\bullet}(x,y)\\}\subseteq D$, that is, $D$ is a variable not
occurring elsewhere in $\Phi$, then $\mathcal{E}$ is empty and $\Phi$ is
classified as admissible. ∎

######  Example 4.7.

Given the formula $\Phi$

$\\{x:D\mid F\mathbin{\bullet}(x,y)\\}\subseteq\\{x:A\mid G\\}\land A\subseteq
D\land D\neq\emptyset$

$\tau(\Phi)$ is

$\mathit{un}(\\{x:D\mid F\mathbin{\bullet}(x,y)\\},\\{x:A\mid G\\},\\{x:A\mid
G\\})\land\mathit{un}(A,D,D)$

Then, the collection $\mathcal{E}$ for $\Phi$ is

$\displaystyle\\{\mathcal{T}(\\{x:A\mid
G\\})=\mathsf{U}(\mathcal{T}(\\{x:D\mid
F\mathbin{\bullet}(x,y)\\}),\mathcal{T}(\\{x:A\mid
G\\})),\mathcal{T}(D)=\mathsf{U}(\mathcal{T}(A),\mathcal{T}(D))\\}$
$\displaystyle\Leftrightarrow$
$\displaystyle\\{\mathcal{T}(A)=\mathsf{U}(\mathsf{P}(\mathcal{T}(D)),\mathcal{T}(A)),\mathcal{T}(D)=\mathsf{U}(\mathcal{T}(A),\mathcal{T}(D))\\}$
$\displaystyle\Leftrightarrow$ [by substitution]
$\displaystyle\\{\mathcal{T}(A)=\mathsf{U}(\mathsf{P}(\mathsf{U}(\mathcal{T}(A),\mathcal{T}(D))),\mathcal{T}(A)),\mathcal{T}(D)=\mathsf{U}(\mathcal{T}(A),\mathcal{T}(D))\\}$

So $\Phi$ is classified as non-admissible. Given a formula similar to the
previous one, but where the second RIS is a set of pairs, i.e.,

$\\{x:D\mid F\mathbin{\bullet}(x,y)\\}\subseteq\\{h:A\mid
G\mathbin{\bullet}(h,w)\\}\land A\subseteq D\land D\neq\emptyset$

then the final collection $\mathcal{E}$ for this formula is

$\\{\mathsf{P}(\mathcal{T}(A))=\mathsf{U}(\mathsf{P}(\mathsf{U}(\mathcal{T}(A),\mathcal{T}(D))),\mathsf{P}(\mathcal{T}(A))),\mathcal{T}(D)=\mathsf{U}(\mathcal{T}(A),\mathcal{T}(D))\\}$

so it is classified as admissible. ∎

From the above definitions, it is evident that, if the given formula $\Phi$
does not contain any RIS term, or if all RIS terms possibly occurring in it
have pattern identical to its control term, then $\Phi$ is surely classified
as admissible.

Intuitively, non-admissible formulas are those where a variable $A$ is the
domain of a RIS representing a function and, at the same, time $A$ is either a
sub or a superset of that function. For example, the non-admissible formula
$\\{x:D\mid\mathit{true}\mathbin{\bullet}(x,y)\\}\subseteq D\land
D\neq\emptyset$ implies that if $a\in D$ then $(a,n)\in D$ and so
$((a,n),n_{1})\in D$ and so forth, thus generating an infinite
$\mathcal{X}$-term. In other words, non-admissible formulas, in a way or
another, require to compare a function and its domain through the subset
relation. Note, however, that $\mathcal{RIS}$-formulas that are classified as
non-admissible are, in a sense, quite unusual formulas. Clearly, in most typed
formalisms, such formulas would not type-check (e.g., in B and Z [Spivey
(1992), Abrial (1996)]). Therefore, missing them from the decision procedure
implemented by $\mathit{SAT}_{\mathcal{RIS}}$ does not seem to be a real lack.

###  4.2 Satisfiability of solved form

As stated in the previous section, the formula $\Phi$ handled by
$\mathit{SAT}_{\mathcal{RIS}}$ can be written as
$\Phi_{\mathcal{S}}\land\Phi_{\mathcal{X}}$ where $\Phi_{\mathcal{S}}$ is a
pure $\mathcal{RIS}$-formula and $\Phi_{\mathcal{X}}$ is a
$\mathcal{X}$-formula. Right before Algorithm 1 calls
$\mathit{SAT}_{\mathcal{X}}$, $\Phi_{\mathcal{S}}$ is in a particular form
referred to as _solved form_. This fact can be easily proved by inspecting the
rewrite rules given in Section 3.2. The constraints in solved form are
selected as to allow trivial verification of satisfiability of the formula as
a whole.

######  Definition 4.8 (Solved form).

Let $\Phi_{\mathcal{S}}$ be a pure admissible $\mathcal{RIS}$-formula; let
$\bar{C}$, $\bar{D}$ and $\bar{E}$ be either variables of sort $\mathsf{Set}$
or variable-RIS, $X$ and $Y$ be variables of sort $\mathsf{Set}$ but not
variable-RIS, and $x$ a variable of sort $\mathsf{X}$; let $t$ be any term of
sort $\mathsf{X}$, and $S$ any term of sort $\mathsf{Set}$ but not a RIS. An
atom $p$ in $\Phi_{\mathcal{S}}$ is in _solved form_ if it has one of the
following forms:

  1. 1.

$\mathit{true}$

  2. 2.

$X=S$ or $X=\\{Y\mid\phi\mathbin{\bullet}u\\}$, and $X$ does not occur in $S$
nor in $\Phi_{\mathcal{S}}\setminus\\{p\\}$

  3. 3.

$\\{X\mid\phi\mathbin{\bullet}u\\}=\varnothing$ or
$\varnothing=\\{X\mid\phi\mathbin{\bullet}u\\}$

  4. 4.

$\\{X\mid\phi_{1}\mathbin{\bullet}u_{1}\\}=\\{Y\mid\phi_{2}\mathbin{\bullet}u_{2}\\}$.

  5. 5.

$X\neq S$, and $X$ does not occur in $S$ nor as the domain of a RIS which is
the argument of a $=$ or $\notin$ or $\mathit{un}$ constraint in
$\Phi_{\mathcal{S}}$ 333This is guaranteed by procedure remove_neq (see
Section 3).

  6. 6.

$t\notin\bar{D}$

  7. 7.

$\mathit{un}(\bar{C},\bar{D},\bar{E})$, and if
$\bar{C},\bar{D}\in\mathcal{V}_{S}$ then $\bar{C}\not\equiv\bar{D}$

  8. 8.

$\bar{C}\parallel\bar{D}$, and if $\bar{C},\bar{D}\in\mathcal{V}_{S}$ then
$\bar{C}\not\equiv\bar{D}$

  9. 9.

$\mathit{set}(X)$, and no constraint $\mathit{isX}(X)$ is in
$\Phi_{\mathcal{S}}$

  10. 10.

$\mathit{isX}(X)$

$\Phi_{\mathcal{S}}$ is in solved form if all its atoms are in solved form. ∎

######  Example 4.9.

The following are $\mathcal{L}_{\mathcal{RIS}}$ atoms in solved form,
occurring in a formula $\Phi$ (where $X$, $D$ and $D_{i}$ are variables):

  * •

$X=\\{x:D\mid x\neq 0\\}$ and $X$ does not occur elsewhere in $\Phi$ (note
that $X$ and $D$ can be the same variable)

  * •

$1\notin\\{x:D\mid x\neq 0\\}$

  * •

$\\{x:D_{1}\mid
x\mathbin{\mathrm{mod}}2=0\mathbin{\bullet}(x,x)\\}=\\{x:D_{2}\mid
x>0\mathbin{\bullet}(x,x+2)\\}$

  * •

$\mathit{un}(X,\\{D_{1}\mid F\mathbin{\bullet}P\\},\\{D_{2}\mid
G\mathbin{\bullet}Q\\})$ and, for any $t$, there are no constraints $D_{1}\neq
t$ nor $D_{2}\neq t$ in $\Phi$. ∎

Right before Algorithm 1 calls $\mathit{SAT}_{\mathcal{X}}$,
$\Phi_{\mathcal{S}}$ is either $\mathit{false}$ or it is in solved form, and
in this case it is satisfiable.

######  Theorem 4.10 (Satisfiability of solved form).

Any (pure) $\mathcal{RIS}$-formula in solved form is satisfiable w.r.t. the
interpretation structure of $\mathcal{L}_{\mathcal{RIS}}$.

######  Proof 4.11 (sketch).

Basically, the proof of this theorem uses the fact that, given a (pure)
$\mathcal{RIS}$-formula $\Phi$ in solved form, it is possible to guarantee the
existence of a successful assignment of values to all variables of $\Phi$
using pure sets only (in particular, the empty set for set variables), with
the exception of the variables $X$ occurring in atoms of the form $X=t$. ∎

Moreover, if $\Phi_{\mathcal{S}}$ is not $\mathit{false}$, the satisfiability
of $\Phi$ depends only on $\Phi_{\mathcal{X}}$.

######  Theorem 4.12 (Satisfiability of
$\Phi_{\mathcal{S}}\land\Phi_{\mathcal{X}}$).

Let $\Phi$ be $\Phi_{\mathcal{S}}\land\Phi_{\mathcal{X}}$ right before
Algorithm 1 calls $\mathit{SAT}_{\mathcal{X}}$. Then either
$\Phi_{\mathcal{S}}$ is $\mathit{false}$ or the satisfiability of $\Phi$
depends only on the satisfiability of $\Phi_{\mathcal{X}}$.

######  Proof 4.13 (sketch).

The proof is based on the observation that assigning values to variables of
sort $\mathcal{X}$ possibly occurring in $\Phi_{\mathcal{S}}$ does not affect
the solved form of $\Phi_{\mathcal{S}}$, i.e., $\Phi_{\mathcal{S}}$ remains in
solved form, hence satisfiable, disregarding of the values assigned to the
$\mathcal{X}$ variables. ∎

###  4.3 Equisatisfiability

In order to prove that Algorithm 1 is correct and complete, we prove that it
preserves the set of solutions of the input formula.

######  Theorem 4.14 (Equisatisfiability).

Let $\Phi$ be an admissible $\mathcal{RIS}$-formula and
$\\{\Phi_{i}\\}_{i=1}^{n}$ be the collection of $\mathcal{RIS}$-formulas
returned by $\mathit{SAT}_{\mathcal{RIS}}(\Phi)$. Then
$\bigvee_{i=1}^{n}\Phi_{i}$ is equisatisfiable w.r.t. $\Phi$, that is, every
possible solution444More precisely, each solution of $\Phi$ expanded to the
variables occurring in $\Phi_{i}$ but not in $\Phi$, so to account for the
possible fresh variables introduced into $\Phi_{i}$. of $\Phi$ is a solution
of one of $\\{\Phi_{i}\\}_{i=1}^{n}$ and, vice versa, every solution of one of
these formulas is a solution for $\Phi$.

######  Proof 4.15 (sketch).

The proof rests on a series of lemmas each showing that the set of solutions
of left and right-hand sides of each rewrite rule is the same. For all cases
dealing with extensional set terms the proofs can be found in [Dovier et al.
(2000)]. The proofs of equisatisfiability for the rules shown in Section 3 and
in Appendix A can be found in Appendix C. ∎

Observe that Theorems 4.10 and 4.14 imply that $\mathit{SAT}_{\mathcal{RIS}}$,
not only determines whether the input formula is satisfiable or not but also,
when the input formula is satisfiable, it computes a finite representation of
all the (possibly infinitely many) solutions.

###  4.4 Termination

Termination of $\mathit{SAT}_{\mathcal{RIS}}$ can be proved for admissible
formulas as is stated by the following theorem.

######  Theorem 4.16 (Termination).

The $\mathit{SAT}_{\mathcal{RIS}}$ procedure can be implemented in such a way
it terminates for every input admissible $\mathcal{RIS}$-formula $\Phi$.

The termination of $\mathit{SAT}_{\mathcal{RIS}}$ and the finiteness of the
number of non-deterministic choices generated during its computation guarantee
the finiteness of the number of $\mathcal{RIS}$-formulas non-deterministically
returned by $\mathit{SAT}_{\mathcal{RIS}}$. Therefore,
$\mathit{SAT}_{\mathcal{RIS}}$ applied to an admissible
$\mathcal{RIS}$-formula $\Phi$ always terminates, returning either
$\mathit{false}$ or a finite collection of satisfiable
$\mathcal{RIS}$-formulas in solved form.

Thanks to Theorems 4.10, 4.14 and 4.16 we can conclude that, given an
admissible $\mathcal{RIS}$-formula $\Phi$, $\Phi$ is satisfiable with respect
to the intended interpretation structure $\mathcal{R}$ if and only if there is
a non-deterministic choice in $\mathit{SAT}_{\mathcal{RIS}}(\Phi)$ that
returns a $\mathcal{RIS}$-formula $\Phi_{\mathcal{S}}\land\Phi_{\mathcal{X}}$
where $\Phi_{\mathcal{S}}$ is in solved form—i.e., there is a choice that does
not terminate with $\mathit{false}$. Hence, $\mathit{SAT}_{\mathcal{RIS}}$ is
a decision procedure for testing satisfiability of admissible
$\mathcal{RIS}$-formulas.

######  Remark 4.17.

Definition 4.5 gives only _sufficient_ conditions. In fact, not all formulas
classified as non-admissible are indeed formulas that our solver cannot deal
with. Given the formula:

$\\{x:A\mid\mathit{false}\mathbin{\bullet}(x,y)\\}\subseteq A\land Y\in A$
(34)

any set $A$ satisfying $Y\in A$ is a solution of it. So, we should accept it.
However, according to Definition 4.5, this formula is classified as non-
admissible. Note that the similar formula where the filter is $\mathit{true}$
admits only an infinite set solution and is (correctly) classified as non-
admissible.

Accepting or not formula (34) depends on the satisfiability of the RIS filter.
Checking the satisfiability of the filter, however, cannot be done, in
general, by simple syntactic analysis, i.e., without running the solver on it.
Thus, when aiming at providing a syntactic characterization of admissible
formulas, we must classify formulas disregarding the form of the RIS filters
possibly occurring in them. Finer characterizations would be feasible,
however, considering special forms of RIS filters, such as $\mathit{false}$
and $\mathit{true}$. ∎

######  Remark 4.18.

In practice many interesting theories are undecidable and only semi-decision
procedures exist for them. On the other hand, in fact, all of the theoretical
results presented so far apply provided RIS’ filters belong to a decidable
_fragment_ of the considered parameter theory, and a solver for this fragment
is called from $\mathit{SAT}_{\mathcal{RIS}}$. Hence, the condition on the
availability of a decision procedure for _all_ $\mathcal{X}$-formulas can be
often relaxed. Instead, the existence of some algorithm capable of deciding
the satisfiability of a significant fragment of $\mathcal{X}$-formulas can be
assumed. If such an algorithm exists and the user writes formulas inside the
corresponding fragment, all of our results still apply. For these reason, in
coming sections, we sometimes give examples where $\mathcal{X}$ is not
necessarily a decidable theory.

###  4.5 Complexity

$\mathit{SAT}_{\mathcal{RIS}}$ strongly relies on set unification. Basically,
rewrite rules dealing with RIS “extract” one element at a time from the domain
of a RIS by means of set unification and construct the corresponding
extensional set again through set unification. Hence, complexity of our
decision procedure strongly depends on complexity of set unification. As
observed in [Dovier et al. (2006)], the decision problem for set unification
is NP-complete. A simple proof of the NP-hardness of this problem has been
given in [Dovier et al. (1996)]. The proof is based on a reduction of 3-SAT to
a set unification problem. Concerning NP-completeness, the algorithm presented
here clearly does not belong to NP since it applies syntactic substitutions.
Nevertheless, it is possible to encode this algorithm using well-known
techniques that avoid explicit substitutions, maintaining a polynomial time
complexity along each non-deterministic branch of the computation.

Besides, $\mathit{SAT}_{\mathcal{RIS}}$ deals not only with the decision
problem for set unification but also with the associated function problem
(i.e., it can compute solutions for the problem at hand). Since solving the
function problem clearly implies solving the related decision problem, the
complexity of $\mathit{SAT}_{\mathcal{RIS}}$ can be no better than the
complexity of the decision problem for set unification. Finally, since
$\mathit{SAT}_{\mathcal{RIS}}$ is parametric w.r.t.
$\mathit{SAT}_{\mathcal{X}}$, its complexity is at least the maximum between
the complexity of both.

##  5 Encoding restricted universal quantifiers and partial functions

In this section we show how RIS can be used to encode restricted universal
quantifiers (Section 5.1) and partial functions (Section 5.2).

###  5.1 Restricted universal quantifiers

RIS can be used to encode restricted universal quantifiers. That is, if $A$ is
a finite set and $\phi$ is a formula of some theory $\mathcal{X}$, the
formula:

$\forall x\in A:\phi(x)$ (35)

is equivalent to the $\mathcal{L}_{\mathcal{RIS}}$ formula (see Proposition
C.1 in the appendix):

$A\subseteq\\{x:A\mid\phi(x)\\}$ (36)

where $\subseteq$ is a derived constraint based on $\mathit{un}$ (see Section
2.4).

This formula lies inside of the decision procedure of
$\mathcal{L}_{\mathcal{RIS}}$. Therefore, $\mathcal{L}_{\mathcal{RIS}}$ is
able to reason about universally quantified formulas.

The following example illustrates a possible use of RIS to express a
restricted universal quantification.

######  Example 5.1.

The formula $y\in S\land S\subseteq\\{x:S\mid y\leq x\\}$ states that $y$ is
the minimum of a set of integers $S$. If, for instance, $S=\\{2,4,1,6\\}$,
then $y$ is bound to $1$. The same RIS can be used in conjunction with a
partially specified $S$ to properly constraint its unknown elements. For
instance, if $S=\\{2,4,z,6\\}$, then the $\mathcal{L}_{\mathcal{RIS}}$ solver
returns either $y=2\land z\geq 2$ or $y=z\land z\leq 2$, provided the
underlying $\mathcal{L}_{\mathcal{X}}$ solver is able to manage simple integer
disequations. Similarly, if $R$ is a variable and
$S=\\{1\mathbin{\scriptstyle\sqcup}R\\}$, then the first answer returned by
$\mathcal{L}_{\mathcal{RIS}}$ will be $y=1\land R\subseteq\\{x:R\mid 1\leq
x\\}$, where $R$ represents the set of all integer numbers less or equal to
$1$. ∎

Restricted universal quantifiers can be exploited, for instance, in program
verification. As a matter of fact, many programs operate on finite, unbounded
inputs and states. Hence, if the formal specification of such a program uses
an universally quantified formula, indeed it can be replaced with a restricted
universally quantified formula. This implies that if theory $\mathcal{X}$ is
decidable, then the formal verification of those programs that can be
specified as $\mathcal{L}_{\mathcal{RIS}}(\mathcal{X})$ formulas, is decidable
as well.

For the sake of convenience, we introduce the following derived constraint:

$\mathsf{foreach}(x\in A,\phi)\triangleq
A\subseteq\\{x:A\mid\phi\\}\triangleq\mathit{un}(A,\\{x:A\mid\phi\\},\\{x:A\mid\phi\\})$
(37)

Hereafter, we will use $\mathsf{foreach}$ in place of the equivalent
$\subseteq$-constraint.

######  Example 5.2 (Linear integer algebra).

It is a known fact that linear algebra over $\mathbb{Z}$ is decidible; let us
call this theory $\mathcal{Z}$. Then, any admissible
$\mathcal{L}_{\mathcal{RIS}}$-formula including the
$\mathsf{foreach}$-constraints listed in Table 6 fall inside the decision
procedure of the restricted quantified theory
$\mathcal{L}_{\mathcal{RIS}}(\mathcal{Z})$.

All the even numbers in $A$ | $\mathsf{foreach}(x\in A,x\mathbin{\mathrm{mod}}2=0)$
---|---
Intersection of $B$ with the less-than relation | $\mathsf{foreach}((x,y)\in B,x\leq y)$
All the solutions of an equation with a free variable in $C$ | $\mathsf{foreach}(y\in C,3x+2y-14=0)$
Intersection of $D$ with the successor function | $\mathsf{foreach}((x,y)\in D,y=x+1)$
Figure 6:  Examples of decidable restricted quantified formulas over linear
integer algebra

######  Remark 5.3.

Although the rules for $\mathit{un}$ shown in Figure 3 can deal with the
$\mathsf{foreach}$ predicate, we introduce a set of specialized rewrite rules
to process this specific kind of predicates more efficiently (see Figure 7).
The key rule is (40) because it corresponds to the formula
$\mathsf{foreach}(x\in\\{t\sqcup A\\},\phi(x))$, where $x$ is a variable. In
turn, this formula can be seen as an iterative program whose iteration
variable is $x$, the range of iteration is $\\{t\sqcup A\\}$, and the body is
$\phi$. In fact, rule (40) basically iterates over $\\{t\sqcup A\\}$ and
evaluates $\phi$ for each element in that set. If one of these elements does
not satisfy $\phi$ then the loop terminates immediately, otherwise it
continues until the empty set is found (i.e., rule (38)) or a variable is
found (i.e., rule (39)).

$\displaystyle\mathit{un}(\varnothing,\\{A\mid\phi\\},\\{A\mid\phi\\})\rightarrow\mathit{true}$
(38)
$\displaystyle\mathit{un}(\bar{A},\\{\bar{A}\mid\phi\\},\\{\bar{A}\mid\phi\\})\rightarrow\text{irreducible}$
(39) $\displaystyle\mathit{un}(\\{t\sqcup A\\},\\{\\{t\sqcup
A\\}\mid\phi\\},\\{\\{t\sqcup
A\\}\mid\phi\\})\rightarrow\phi(t)\land\mathit{un}(A,\\{A\mid\phi\\},\\{A\mid\phi\\})$
(40)

Figure 7: Specialized rewrite rules to deal with restricted universal
quantifiers

###  5.2 Partial functions

Another important use of RIS is to define _(partial) functions_ by giving
their domains and the expressions that define them. In general, a RIS of the
form

$\\{x:D\mid F\mathbin{\bullet}(x,f(x))\\}$ (41)

where $f$ is any $\mathcal{L}_{\mathcal{X}}$ function symbol, defines a
partial function. Such a RIS contains ordered pairs whose first components
belong to $D$ which cannot have duplicates (because it is a set). Then, if no
two pairs share the same first component, then the RIS is a function. Given
that RIS are sets, then, in $\mathcal{L}_{\mathcal{RIS}}$, functions are sets
of ordered pairs as in Z and B. Therefore, through standard set operators,
functions can be evaluated, compared and point-wise composed; and by means of
constraint solving, the inverse of a function can also be computed. The
following examples illustrate these properties.

######  Example 5.4.

The square of 5 can be calculated by:
$(5,y)\in\\{x:D\mathbin{\bullet}(x,x*x)\\}$, yielding $y=25$. The same RIS
calculates the square root of a given number:
$(x,36)\in\\{x:D\mathbin{\bullet}(x,x*x)\\}$, returning $x=6$ and $x=-6$. Set
membership can also be used for the point-wise composition of functions. The
function $f(x)=x^{2}+8$ can be evaluated on 5 as follows:
$(5,y)\in\\{x:D\mathbin{\bullet}(x,x*x)\\}\land(y,z)\in\\{e:E\mathbin{\bullet}(e,e+8)\\}$
returning $y=25$ and $z=33$. ∎

##  6 Extensions

The formula $\Phi$ of a (general) intensional set $\\{x:\Phi(x)\\}$ may depend
on existentially quantified variables, declared inside the set. For example,
if $R$ is a set of ordered pairs and $D$ is a set, then the subset of $R$
where all the first components belong to $D$ can be denoted by

$\\{p:\exists x,y(x\in D\land(x,y)\in R\land p=(x,y))\\}.$ (42)

We will refer to these existentially quantified variables as _parameters_.

Allowing parameters in RIS rises major problems when RIS have to be
manipulated through the rewrite rules considered in the previous section. In
fact, if $\vec{p}$ is the vector of parameters possibly occurring in a RIS,
then literals of the form $\lnot\phi(d)$, occurring in the rules (e.g., (6)),
should be replaced with the more complex universally quantified formula
$\forall\vec{p}(\lnot\phi(d,\vec{p}))$. This, in turn, would require that the
theory $\mathcal{X}$ is equipped with a solver able to deal with such kind of
formulas.

In this section we describe two extensions to $\mathcal{L}_{\mathcal{RIS}}$
that increase its expressiveness concerning the presence of parameters,
without compromising decidability. The first one deals with control terms (and
patterns), while the second one deals with special kinds of predicates
occurring in RIS filters, called _functional predicates_.

Both extensions are supported by the implementation of
$\mathcal{L}_{\mathcal{RIS}}$ within $\\{log\\}$ (see Section 7).

###  6.1 Control terms and patterns

The first of these extensions is the possibility to use more general forms of
control terms and patterns in RIS.

As stated in Definition 2.3, $\mathcal{L}_{\mathcal{RIS}}$ is designed to
allow for terms of the form $(x,y)$ in place of the quantified control
variable of set comprehensions. In effect, the idea of allowing control terms
(not just control variables) steams from the observation that many uses of
parameters can be avoided by a proper use of the control term of a RIS.

######  Proposition 6.1.

If $\vec{p}$ is a vector of existentially quantified variables declared inside
an intensional set then:

$\displaystyle S=\\{x:D_{1}\mid\phi(x,\vec{p})\land\vec{p}\in
D_{2}\mathbin{\bullet}u(x,\vec{p})\\}$ $\displaystyle\Leftrightarrow
S=\\{(x,\vec{p}):D_{1}\times
D_{2}\mid\phi((x,\vec{p}))\mathbin{\bullet}u((x,\vec{p}))\\}$

This result can be applied to the example mentioned above.

######  Example 6.2.

The intensional set (42) can be expressed with a RIS (hence, without
parameters) as follows: $\\{(x,y):R\mid x\in D\\}$. If $R$ is for instance
$\\{(a,1),(b,2),(a,2)\\}$ and $D$ is $\\{a\\}$, then the formula
$\\{(x,y):R\mid x\in D\\}=\\{(a,1),(a,2)\\}$ is (correctly) found to be
satisfiable by $\mathit{SAT}_{\mathcal{RIS}}$.

Therefore, it would be interesting to extend RIS to allow more general forms
of control terms without loosing completeness of the solver. In this respect,
it is important to note that the proof of Theorem 4.14 relies on a particular
relation between the control term and the pattern of a RIS and a property that
patterns allowed in the language must verify. In order to state these
conditions we need the following definitions.

######  Definition 6.3 (Bijective pattern).

Let $\\{x:D\mid\phi(x)\mathbin{\bullet}u(x)\\}$ be a RIS, then its pattern is
_bijective_ if $u:\\{x:x\in D\land\phi(x)\\}\rightarrow Y$ is a bijective
function, where $Y$ is the set of images of $u$.

######  Definition 6.4 (Co-injective patterns).

Two patterns, $u$ and $v$, are said to be _co-injective_ if for any $x$ and
$y$, if $u(x)=v(y)$ then $x=y$.

Then, Theorem 4.14 can be proved provided all patterns are bijective and
pairwise co-injective.

Through Definition 2.3, $\mathcal{L}_{\mathcal{RIS}}$ is designed to guarantee
that patterns verify those conditions. In particular, when all the patterns
are the corresponding control terms, they verify the above conditions as they
are trivially bijective and pairwise co-injective. This is important because
this subclass of RIS is used to encode restricted universal quantifiers (see
Section 5.1).

The bijectivity of a pattern depends on the form of the control term. For
example, if the control term is $(x,y)$ and the pattern depends only on one
between $x$ and $y$, then it cannot be bijective because for a given $x$ or
$y$ there are many $(x,y)$. Conversely, if $x$ is the control term, then any
pattern of the form $(x,\cdot)$ is bijective.

Besides the terms considered in Definition 2.3, however, others can be
bijective patterns, although they might not be pairwise co-injective.

######  Example 6.5.

  * •

If $c$ is any control term then a pattern of the form $(\cdot,c)$ is
bijective. Further, these patterns are also pairwise co-injective. However, if
the language allows these patterns in conjunction with patterns of the form
$(c,\cdot)$, then pairwise co-injectivity is lost.

  * •

If $x$ is the control term and $n$ is a constant, then $x+n$ is a bijective
pattern. However, these patterns are not always pairwise co-injective.

  * •

If $x$ is the control term, then $x*x$ is not bijective as $x$ and $-x$ have
$x*x$ as image, while $(x,x*x)$ is indeed a bijective pattern, allowed in
$\mathcal{L}_{\mathcal{RIS}}$. ∎

The intuitive reason to ask for bijective patterns is that if $y$ belongs to a
RIS whose pattern, $u$, is not bijective then there may be two or more
elements in the RIS domain, say $x_{1}$ and $x_{2}$, such that
$u(x_{1})=u(x_{2})=y$. If this is the case, then eliminating, say, $x_{1}$
from the domain is not enough to eliminate $y$ from the RIS. And this makes it
difficult, for instance, to prove the equality between a variable-RIS and a
set (extensional or RIS) having at least one element.

In turn pairwise co-injectivity is necessary to solve equations such as:

$\\{x:X\mid\gamma\mathbin{\bullet}v\\}=\\{t\mathbin{\scriptstyle\sqcup}\\{y:X\mid\phi\mathbin{\bullet}u\\}\\}$
(43)

in a finite number of iterations. Let’s assume for a moment that patterns of
the form $x+n$ ($n$ constant) are allowed and (43) is instantiated as follows:

$\\{x:X\mid\mathit{true}\mathbin{\bullet}x+2\\}=\\{5\mathbin{\scriptstyle\sqcup}\\{y:X\mid\mathit{true}\mathbin{\bullet}y+8\\}\\}$
(44)

Over the integers, this equation is satisfiable only if $X$ equals
$\mathbb{Z}$, as we ask for the non-empty image of two different lines over
the same domain to be equal. $\mathit{SAT}_{\mathcal{RIS}}$ would be unable to
conclude this in a finite number of iterations. Given that 5 must belong to
the l.h.s. set, then $3\in X$. But this implies that 11 belongs to the r.h.s.
and so, to keep the sets equal, it must belong to the l.h.s., then $9\in X$
and so we have an infinite loop. On the other hand, if we ask whether the two
_lines_ are equal or not:

$\\{x:X\mid\mathit{true}\mathbin{\bullet}(x,x+2)\\}=\\{(3,5)\mathbin{\scriptstyle\sqcup}\\{y:X\mid\mathit{true}\mathbin{\bullet}(y,y+8)\\}\\}$
(45)

$\mathit{SAT}_{\mathcal{RIS}}$ is able to give the right answer. Given that
$(3,5)$ must belong to the l.h.s. set then $3\in X$. But this implies that
$(3,11)$ belongs to the r.h.s. and so, to keep the sets equal, it must belong
to the l.h.s. but this is impossible as $(3,11)$ is not a point in the line
with equation $y=x+2$. The difference between (44) and (45) is that in the
former patterns are not pairwise co-injective while in the latter they are.

Unfortunately, these properties cannot be easily syntactically assessed. Thus
we prefer to restrict $\mathcal{L}_{\mathcal{RIS}}$ by adopting a more
restrictive definition of admissible pattern that can be syntactically
checked. From a more practical point of view, however, other patterns could be
admitted instead of those given in Definition 2.3, with the assumption that if
they verify the conditions stated above the result is surely safe; while if
they do not, it is not safe.

###  6.2 Functional predicate symbols

Although in general is undecidable to assert the satisfiability of formulas of
the form $\forall\vec{p}(\lnot\phi(x,\vec{p}))$, where $\phi$ is a formula of
an arbitrary theory $\mathcal{T}$, we have identified a non-trivial fragment
of $\mathcal{T}$ whose satisfiability can be decided. Intuitively, this
fragment is composed by those formulas where $\phi$ is of the form
$\phi_{p}\land\phi_{r}$ such that
$\forall\vec{p}(\lnot(\phi_{p}(x,\vec{p})\land\phi_{r}(x,\vec{p})))$ is
equivalent to an existentially quantified formula.

######  Definition 6.6 (Functional predicate).

Let $p\in\Pi_{\mathcal{X}}$ be a predicate symbol of $\mathcal{X}$ with arity
$n\geq 2$ . $p(x_{1},\dots,x_{n-1},y)$ is said to be a _functional predicate_
if given $x_{1},\dots,x_{n-1}$ there exists _at most_ one $y$ such that
$p(x_{1},\dots,x_{n-1},y)$ holds. ∎

Functional predicates are a form of encoding functions in a logic language.
Indeed, if $p(x,y)$ is a functional predicate then it is equivalent to
$p(x)=y$ if $p$ is seen as a function. Further, $y$ can be seen as the name
given to the expression $p(x)$. In other words, we can say that $y$ is the
_definition_ of $p(x)$.

Note that, for any functional predicate $p$ and given $x_{1},\dots,x_{n-1}$,
it may be the case that $p(x_{1},\dots,x_{n-1},y)$ does not hold for all $y$.
For this reason we define the following.

######  Definition 6.7 (Pre-condition of a functional predicate).

Let $p(x_{1},\dots,x_{n-1},y)$ be a functional predicate. Let $\phi_{q}$ be an
$\mathcal{X}$-formula based on symbols in $\Pi_{\mathcal{X}}\setminus\\{p\\}$,
and $\vec{x}$ a subset of $x_{1},\dots,x_{n-1}$. $\phi_{q}$ is said to be the
_pre-condition_ of $p(x_{1},\dots,x_{n-1},y)$ if and only if for any given
$x_{1},\dots,x_{n-1}$:

$\phi_{q}(\vec{x})\Leftrightarrow\exists y(p(x_{1},\dots,x_{n-1},y))$

∎

The following proposition characterizes a class of formulas including an
existential quantification whose negation is free of universal quantifiers.
See the proof in Appendix C.

######  Proposition 6.8.

Let $\phi_{q}$ be the precondition of a functional predicate
$p(x_{1},\dots,x_{n-1},y)$. Let $\phi_{r}$ be an $\mathcal{X}$-formula, and
$\vec{x}_{q}$ and $\vec{x}_{r}$ subsets of $x_{1},\dots,x_{n-1}$. Then given
$x_{1},\dots,x_{n-1}$ the following holds:

$\displaystyle\forall
y(\lnot(p(x_{1},\dots,x_{n-1},y)\land\phi_{r}(\vec{x}_{r},y)))$
$\displaystyle\Leftrightarrow\lnot\phi_{q}(\vec{x}_{q})\lor\phi_{q}(\vec{x}_{q})\land\exists
z(p(x_{1},\dots,x_{n-1},z)\land\lnot\phi_{r}(\vec{x}_{r},z))$

∎

If a RIS has a filter of the form $\exists n(\phi(x,n))$ then its negation is
of the form $\forall n(\lnot\phi(x,n))$. However, if $\phi$ can be written as
$q(x)\land p(x,n)\land r(x,n)$ where $q$ is the pre-condition of the
functional predicate symbol $p$, then Proposition 6.8 permits to transform
$\forall n(\lnot\phi(x,n))$ into a formula free of universal quantifiers. In
effect, we have:

$\displaystyle\forall n(\lnot\phi(d,n))$ $\displaystyle\Leftrightarrow\forall
n(\lnot(q(x)\land p(x,n)\land r(x,n)))$ [by definition of $F$]
$\displaystyle\Leftrightarrow\forall n(\lnot q(x)\lor\lnot(p(x,n)\land
r(x,n)))$ [by distributivity] $\displaystyle\Leftrightarrow\lnot
q(x)\lor\forall n(\lnot(p(x,n)\land r(x,n)))$ [by $q$ does not depend on $n$]
$\displaystyle\Leftrightarrow\lnot q(x)\lor\lnot q(x)\lor\exists z(q(x)\land
p(x,z)\land\lnot r(x,z))$ [by Proposition 6.8]
$\displaystyle\Leftrightarrow\lnot q(x)\lor\exists z(q(x)\land
p(x,z)\land\lnot r(x,z))$

Hence, this proposition applied to RIS’ filters considerably enlarges the
fragment of decidable $\mathcal{L}_{\mathcal{RIS}}$ formulas, as is shown by
the following example.

######  Example 6.9.

Recently Cristiá and Rossi extended CLP($\mathcal{SET}$), and its $\\{log\\}$
implementation, to support binary relations and partial functions [Cristiá et
al. (2015), Cristiá and Rossi (2019)]. In this theory, called $\mathcal{BR}$,
binary relations and functions are sets of ordered pairs, and a number of
relational operators are provided as constraints. Such theory has been proved
to be semi-decidable for formulas involving conjunctions, disjunctions and
negations of its constraints. Notwithstanding, in the remaining of this paper,
we will consider the instance of $\mathcal{L}_{\mathcal{RIS}}$ based on the
decidable fragment of $\mathcal{BR}$ implemented in $\\{log\\}$.

Among others, $\mathcal{BR}$ provides the following constraints, where $F,G,H$
are binary relations or partial functions: $\mathit{apply}(F,x,y)$, whose
interpretation is $F(x)=y$; $\mathit{comp}(F,G,H)$ which is interpreted as the
composition of $F$ and $G$, i.e., $H=R\circ T$; and $\mathit{pfun}(F)$ which
constrains set $F$ to be a partial function.

$\mathit{apply}(F,x,y)$ is a functional predicate with precondition
$\mathit{pfun}(F)\land\mathit{ncomp}(\\{(x,x)\\},F,\emptyset)$, for any $F$
and $x$, where $\mathit{ncomp}$ is $\lnot\mathit{comp}$ (notice that, if $F$
is a partial function, $\mathit{ncomp}(\\{(x,x)\\},F,\emptyset)$ is true iff
$x$ belongs to the domain of $F$). Hence, the following
$\mathcal{L}_{\mathcal{RIS}}$ formula is decidable for any $F$, $x_{1}$,
$x_{2}$ and $x_{3}$:

$F=\\{(x_{1},x_{2}),(x_{1},x_{3})\\}\land\\{y:\\{1\\}\mid\exists
z(\mathit{apply}(F,y,z)\land z\neq 0)\\}=\emptyset$ (46)

as the negation of $\exists z(\mathit{apply}(F,y,z)\land z\neq 0)$ can be
turned into the following decidable $\mathcal{X}$-formula, due to Proposition
6.8:

$\lnot(\mathit{pfun}(F)\land\mathit{ncomp}(\\{(x,x)\\},F,\emptyset))\lor(\mathit{pfun}(F)\land\mathit{ncomp}(\\{(x,x)\\},F,\emptyset)\land\mathit{apply}(F,y,n)\land
n=0)$

for some new $n$. Possible solutions for (46) are: $x_{2}\neq x_{3}$ (i.e.,
$F$ is not a function), $x_{1}\neq 1$ (i.e., $1$ does not belong to the domain
of $F$); $x_{1}=1\land x_{2}=0\land x_{3}=0$ (i.e., $F=\\{(1,0)\\}$). ∎

##  7 RIS in Practice

RIS have been implemented in Prolog as an extension of $\\{log\\}$ [Rossi
(2008)], a freely available implementation of $\mathcal{BR}$ [Cristiá and
Rossi (2019)] extended with FD-constraints [Dal Palú et al. (2003)]. In this
case, the theory $\mathcal{X}$ is basically the theory of _hereditarily finite
hybrid sets and binary relations_ , augmented with that of
CLP($\mathcal{FD}$), that is integer arithmetic over finite domains. This
theory provides the same function symbols as $\mathcal{L}_{\mathcal{RIS}}$ for
building extensional set terms (namely, $\emptyset$ and
$\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\}$), along with a set of predicate
symbols including those of $\mathcal{L}_{\mathcal{RIS}}$, with the same
interpretation. In addition, $\mathcal{BR}$ provides predicate symbols such as
composition of binary relations, converse of binary relations, domain, range,
etc., and the usual function symbols representing operations over integer
numbers (e.g., $+,-,\mathbin{\mathsf{mod}}$, etc.), as well as the predicate
symbols $\mathsf{size}$, representing set cardinality, and $\leq$,
representing the order relation on the integers. One notable difference w.r.t.
$\mathcal{L}_{\mathcal{RIS}}$ is that set elements can be either finite sets
or non-set elements of any sort (i.e., nested sets are allowed).

The theory underlying $\\{log\\}$ is endowed with a constraint solver which is
proved to be a semi-decision procedure for its formulas. More precisely, the
constraint solver is a decision procedure for the subclass of
$\mathcal{BR}$-formulas not involving (two particular forms of) relational
composition [Cristiá and Rossi (2019)].

Syntactic differences between the abstract syntax used in this paper and the
concrete syntax used in $\\{log\\}$ are made evident by the following
examples.

######  Example 7.1.

The $\mathcal{RIS}$-formula:

$\\{5\\}\in\\{x:\\{y\mathbin{\scriptstyle\sqcup}D\\}\mid x\neq\emptyset\land
5\notin x\mathbin{\bullet}x\\}$

is written in $\\{log\\}$ as:

$\\{5\\}\mathbin{\mathsf{in}}\mathsf{ris}(X\mathbin{\mathsf{in}}\\{Y/D\\},X\mathbin{\mathsf{neq}}\\{\\}\mathbin{\&}5\mathbin{\mathsf{nin}}X,X)$

where $\mathsf{ris}$ is a function symbol whose arguments are: _i_) a
constraint of the form $X\mathbin{\mathsf{in}}A$ where $X$ is the control term
and $A$ the domain of the RIS; _ii_) the filter given as a $\\{log\\}$
formula; and _iii_) the pattern given as a $\\{log\\}$ term. Filters and
patterns can be omitted as in $\mathcal{L}_{\mathcal{RIS}}$. Variables must
start with an uppercase letter; the set constructor symbols for both
$\mathcal{L}_{\mathcal{RIS}}$ and $\\{log\\}$ sets terms are written as
$\\{\cdot/\cdot\\}$. If this formula is provided to $\\{log\\}$ it answers
$\mathsf{no}$ because the formula is unsatisfiable. ∎

The following are more examples of RIS that can be written in $\\{log\\}$.

######  Example 7.2.

  * •

The multiples of $N$ belonging to $D$:

$\mathsf{ris}(X\mathbin{\mathsf{in}}D,0\mathbin{\mathsf{is}}X\mathbin{\mathsf{mod}}N)$

where $\mathbin{\mathsf{is}}$ is the Prolog built-in predicate that forces the
evaluation of the arithmetic expression at its right-hand side.

  * •

The sets belonging to $D$ containing a given set $A$:

$\mathsf{ris}(S\mathbin{\mathsf{in}}D,\mathsf{subset}(A,S))$

  * •

A function that maps integers to their squares:

$\mathsf{ris}([X,Y]\mathbin{\mathsf{in}}D,Y\mathbin{\mathsf{is}}X*X)$

where ordered pairs are written using $[\cdot,\cdot]$; note that the pattern
can be omitted since it is the same as the control term, that is $[X,Y]$. ∎

Actually $\\{log\\}$ implements the extended version of
$\mathcal{L}_{\mathcal{RIS}}$ described in Section 6. In particular, in
$\\{log\\}$ a RIS can contain parameters, i.e., existentially quantified
variables local to the RIS; and functional predicates can be conveniently
declared. Parameters are listed as the second argument of the $\mathsf{ris}$
term, while functional predicates must be located just after the pattern, as
the last argument. Both parameters and functional predicates are optional
arguments of a RIS term.

######  Example 7.3.

A function that maps sets to their cardinalities provided they are greater
than $1$:

$\mathsf{ris}(S\mathbin{\mathsf{in}}D,[C],C>1,[S,C],\mathsf{size}(S,C))$

where $C$ is a parameter and $\mathsf{size}(S,C)$ is a functional predicate,
whose intuitive meaning is $C=\lvert S\rvert$. ∎

RIS patterns in $\\{log\\}$ can be any term (including $\\{\cdot/\cdot\\}$).
If they verify the conditions given in Section 6.1, then the solver is
guaranteed to be a decision procedure; otherwise this may be not the case.

######  Example 7.4.

The formula $\\{x:[1,4]\mathbin{\bullet}2*x\\}=\\{2,4,6,8\\}$ can be written
in $\\{log\\}$ as:

$\mathsf{ris}(X\mathbin{\mathsf{in}}\mathsf{int}(1,4),\mathsf{true},2*X)=\\{2,4,6,8\\}$

where $\mathsf{int}(1,4)$ is the $\\{log\\}$ syntax to denote the
interval$[1,4]$. If this formula is provided to $\\{log\\}$ it answers
$\mathsf{yes}$. Note that $2*X$ is a bijective pattern and since it is the
only pattern in the formula is trivially pairwise co-injective. Caution must
be taken if this pattern is mixed with others. ∎

When the domain of a RIS is at least partially specified it is also possible
to explicitly enumerate the elements of the set denoted by the RIS by means of
the $\mathbin{\mathsf{is}}$ operator.

######  Example 7.5.

When

$\mathit{Even}\mathbin{\mathsf{is}}\mathsf{ris}(X\mathbin{\mathsf{in}}\mathsf{int}(1,100),\mathsf{true},2*X)$

is run on $\\{log\\}$ it immediately answers $Even=\\{2,4,\dots,200\\}$. ∎

In $\\{log\\}$ the language of the RIS and the language of the parameter
theory $\mathcal{X}$ are completely amalgamated. Thus, it is possible for
example to use literals of the latter in formulas of the former, as well as to
share variables of both. The following example exploits this feature.

######  Example 7.6.

A formula to find out whether $N$ is prime or not:

$N>1\mathbin{\&}\mathit{MD}\mathbin{\mathsf{is}}N\mathbin{\mathsf{div}}2\mathbin{\&}\mathsf{ris}(X\mathbin{\mathsf{in}}\mathsf{int}(2,\mathit{MD}),0\mathbin{\mathsf{is}}N\mathbin{\mathsf{mod}}X)=\emptyset$

The idea is to check if the set of proper divisors of $N$ (i.e.,
$\\{x:[2,\mathit{MD}]\mid 0=N\mathbin{\mathrm{mod}}x\\}$) is empty or not.
Then, if $N$ is bound to, say, 20, $\\{log\\}$ answers no; but if it is bound
to 101 it answers $N=101,\mathit{MD}=50$. ∎

######  Remark 7.7.

In $\\{log\\}$ checks for detecting non-admissible formulas (see Definition
4.5) are limited to atomic formulas (i.e., $\mathcal{RIS}$-constraints). As a
consequence, if the solver has to deal with general non-admissible formulas,
then there is a risk that it will go into an infinite loop. As observed at the
end of Section 4.1, however, these formulas are quite “unusual”, hence this
behavior is not perceived as a problem in practice. ∎

###  7.1 Case studies

In this subsection we present two case studies showing the capabilities of
$\\{log\\}$ concerning RIS. The first one shows how $\\{log\\}$ can be used as
an automated theorem prover when restricted universal quantifiers are
involved. In this case study a non-trivial security property of a security
model is proved. In the second case study RIS are used to specify a simplified
version of the grep program. There we show that RIS provide a sort of second-
order language because it is possible to iterate over sets of sets.

######  Case study 1 (Bell-LaPadula’s security condition).

Bell and LaPadula proposed a security model of an operating system enforcing a
security policy known as multi-level security [Bell and LaPadula (1973a), Bell
and LaPadula (1973b)]. The model is a state machine described with set theory
and first-order logic. This model verifies two state invariants, one of which
is called _security condition_. This condition can be stated as follows:

$\forall(p,f)\in proctbl(\mathit{scf}(f)\preceq scp(p))$ (47)

where $proctbl$ is the process table represented as a set of ordered pairs of
the form $(p,f)$ where $p$ is a process and $f$ a file opened in read mode by
$p$; and $\mathit{scf}$ and $scp$ are functions returning the _security class_
of files and processes, respectively. A security class is an ordered pair of
the form $(l,C)$ where $l\in{\rm Nature}$ is called _security level_ , and $C$
is a _set of categories_. Security classes are partially ordered by the
_dominates_ relation ($\preceq$) defined as:
$(l_{1},C_{1})\preceq(l_{2},C_{2})\Leftrightarrow l_{1}\leq l_{2}\land
C_{1}\subseteq C_{2}$.

Bell-LaPadula’s security condition is expressible in $\\{log\\}$ using a
$\mathsf{foreach}$ constraint as follows (recall Example 6.9):

$\begin{split}\mathsf{sec}&\mathsf{Cond}(\mathit{Scf},Scp,Proctbl)\triangleq\\\
&\mathsf{foreach}([P,F]\in
Proctbl,\mathsf{apply}(\mathit{Scf},F,S_{f})\mathbin{\&}\mathsf{apply}(Scp,P,S_{p})\mathbin{\&}\mathsf{dominates}(S_{f},S_{p}))\end{split}$
(48)

where $S_{f}$ and $S_{p}$ are parameters (cf. Section 6.2). Since
$\mathsf{apply}(G,X,Y)$ is a functional predicate, formula (48) lies inside of
the results given in Section 6.2555Observe that, if $f$ and $g$ are two
functional predicates of arity 2, then we can introduce a new predicate $h$,
$h(x_{1},x_{2},w)\Leftrightarrow w=(n_{1},n_{2})\land f(x_{1},n_{1})\land
g(x_{2},n_{2})$, where $h(x_{1},x_{2},w)$ is trivially a functional
predicate.. In turn, the $\mathsf{dominates}$ relation can be defined easily:

$\mathsf{dominates}(S_{1},S_{2})\triangleq
S_{1}=[L_{1},C_{1}]\mathbin{\&}S_{2}=[L_{2},C_{2}]\mathbin{\&}L_{1}\leq
L_{2}\mathbin{\&}C_{1}\subseteq C_{2}$ (49)

More importantly, although $\\{log\\}$ implements a semi-decision procedure
for formulas involving partial functions, it can be used to (automatically)
prove whether or not a given operation in Bell-LaPadula’s model preserves the
security condition. For example, the operation describing process $P$
requesting file $F$ to be opened in read mode can be described with a
$\\{log\\}$ formula:

$\begin{split}\mathsf{openRead}&(\mathit{Scf},Scp,Proctbl,P,F,Proctbl^{\prime})\triangleq\\\
&[P,F]\notin
Proctbl\mathbin{\&}\mathsf{apply}(\mathit{Scf},F,S_{f})\mathbin{\&}\mathsf{apply}(Scp,P,S_{p})\mathbin{\&}\mathsf{dominates}(S_{f},S_{p})\\\
&\mathbin{\&}Proctbl^{\prime}=\\{[P,F]\mathbin{\scriptstyle\sqcup}Proctbl\\}\end{split}$
(50)

where $Proctbl^{\prime}$ represents the value of $Proctbl$ in the next state
(as is usual in formal notations such as B and Z).

Hence, the proof obligation asserting that $\mathsf{openRead}$ preserves
$\mathsf{secCond}$ as an invariant is, informally:

$\mathsf{secCond}$ is true of $Proctbl$
$\displaystyle{}\land\text{$\mathsf{openRead}$ is called on $Proctbl$, thus
returning $Proctbl^{\prime}$}$
$\displaystyle{}\implies\text{$\mathsf{secCond}$ is true of
$Proctbl^{\prime}$}$

However, if $\\{log\\}$ is going to be used to discharge this proof
obligation, it should be submitted in negated form:

$\displaystyle\mathsf{secCond}(\mathit{Scf},Scp,Proctbl)$
$\displaystyle{}\mathbin{\&}\mathsf{openRead}(Proctbl,P,F,Proctbl^{\prime})$
(51)
$\displaystyle{}\mathbin{\&}\mathsf{nforall}([P,F]\mathbin{\mathsf{in}}Proctbl^{\prime},\mathsf{apply}(\mathit{Scf},F_{1},S_{f})\mathbin{\&}\mathsf{apply}(Scp,P_{1},S_{p})\mathbin{\&}\mathit{dominates}(S_{f},S_{p}))$

in which case in $\approx$ .5 s $\\{log\\}$ answers $\mathit{false}$, as
expected.

Besides, assume the specifier makes a mistake in $\mathsf{openRead}$ such that
the security condition is no longer preserved. For instance, (s)he forgets
$\mathsf{dominates}(S_{f},S_{p})$ as a pre-condition. When (s)he attempts to
discharge (51), $\\{log\\}$ will return a counterexample showing why the
security condition has been violated666Only the core of the counterexample is
shown.:

$\displaystyle
Scf=\\{[F_{1},[Lf,\\{N_{6}\mathbin{\scriptstyle\sqcup}N_{5}\\}]]\mathbin{\scriptstyle\sqcup}N_{4}\\},$
$\displaystyle ScP=\\{[P_{1},[Lp,Cp]]\mathbin{\scriptstyle\sqcup}N_{2}\\},$
$\displaystyle
Proctbl^{\prime}=\\{[P_{1},F_{1}]\mathbin{\scriptstyle\sqcup}Proctbl\\},$
$\displaystyle\text{Constraint: }N_{6}\notin Cp$

That is, the security class of $P_{1}$ does not dominate the security class of
$F_{1}$ because $N_{6}$ does not belong to $Cp$.

The source code of this case study can be found in Appendix B. ∎

In $\mathcal{L}_{\mathcal{RIS}}$ it is possible to iterate or quantify over
sets whose elements are other sets—i.e., $\mathcal{L}_{\mathcal{RIS}}$ offers
a sort of second-order language. Differently from previous versions of
$\\{log\\}$, however, quantified set variables can be also intensional sets
(namely, RIS), not only extensional sets. In other words, in
$\mathcal{L}_{\mathcal{RIS}}$ intensional sets are real first-class citizens
of the constraint language. The following case study illustrates this feature
of $\mathcal{L}_{\mathcal{RIS}}$.

######  Case study 2 (A simple grep program).

We can model a text file as a set of lines and each line as a set of words,
i.e., the file is modeled as a collection of sets. With this representation it
is easy to implement a basic version of the usual $\mathsf{find}$ function
using a formula based on set unification:

$\mathsf{find}(File,Word)\triangleq File=\\{\\{Word/Line\\}/Rest\\}$ (52)

However, no formula based on set unification can describe the `grep` program
which collects _all_ the lines of the file where a given word is found. The
reason is that it requires to inspect all the lines of the file—i.e., all the
sets of a set. For such program a RIS can do the job:

$\mathsf{grep}(File,\mathit{Word},Result)\triangleq
Result=\mathsf{ris}(Line\mathbin{\mathsf{in}}File,\mathit{Word}\mathbin{\mathsf{in}}Line)$
(53)

Furthermore, by adding a parameter to the definition of $\mathsf{grep}$ we can
implement the `-v` option which reverses the search:

$\begin{split}\mathsf{grep}&(Opt,File,\mathit{Word},Result)\triangleq\\\
&Opt=\text{'
'}\mathbin{\&}Result=\mathsf{ris}(Line\mathbin{\mathsf{in}}File,\mathit{Word}\mathbin{\mathsf{in}}Line)\\\
&\mathbin{\mathsf{or}}Opt=\text{'v'}\mathbin{\&}Result=\mathsf{ris}(Line\mathbin{\mathsf{in}}File,\mathit{Word}\mathbin{\mathsf{nin}}Line)\end{split}$
(54)

In this way $\mathsf{grep}$ is both a program _and_ a formula. This means that
we can use $\\{log\\}$ to run $\mathsf{grep}$ and to prove properties of it.
For instance, we can run:

$\mathsf{grep(\text{'
'},\\{\\{hello,world\\},\\{to,be,or,not,to,be\\},\\{i,said,hello,sir\\}\\},hello},R)$
(55)

and the answer will be:

$R=\mathsf{\\{\\{i,said,hello,sir\\},\\{hello,world\\}\\}}$ (56)

Now we can use $\\{log\\}$ to prove the following two general properties of
$\mathsf{grep}$:

$\displaystyle\mathsf{grep}(\text{'
'},F,W,R_{1})\land\mathsf{grep}(\text{'v'},F,W,R_{2})\implies\mathsf{un}(R_{1},R_{2},F)$
(57) $\displaystyle\mathsf{grep}(\text{'
'},F,W,R_{1})\land\mathsf{grep}(\text{'v'},F,W,R_{2})\implies\mathsf{disj}(R_{1},R_{2})$
(58)

which, as always, should be submitted to $\\{log\\}$ in negated form:

$\displaystyle\mathsf{grep}(\text{'
'},F,W,R_{1})\mathbin{\&}\mathsf{grep}(\text{'v'},F,W,R_{2})\mathbin{\&}\mathsf{un}(R_{1},R_{2},F)$
(59) $\displaystyle\mathsf{grep}(\text{'
'},F,W,R_{1})\mathbin{\&}\mathsf{grep}(\text{'v'},F,W,R_{2})\mathbin{\&}\mathsf{ndisj}(R_{1},R_{2})$
(60)

in which case $\\{log\\}$ answers $\mathit{false}$, as expected. ∎

This is a significant extension w.r.t. previous versions of $\\{log\\}$. In
fact, in those versions it was possible to give a definition such as (53) by
using general intensional sets; but, in that case, the solver would fail to
prove the unsatisfiability of a general formula such as (59), simply because
it tries to replace the intensional sets with the corresponding extensional
definitions, instead of solving the relevant constraints directly over the
intensional sets, as it does when RIS are used.

##  8 Empirical evaluation

The goal of this empirical evaluation is to provide experimental evidence that
the $\\{log\\}$ implementation of $\mathit{SAT}_{\mathcal{RIS}}$ works in
practice. To this end we selected 176 problems from the SET collection of the
TPTP library [Sutcliffe (2009)]. The selected problems are those representing
quantifier-free, first-order set theory results involving conjunctions,
disjunctions and negations of set equality, membership, union, intersection,
difference, disjointness and complement that can be encoded in $\\{log\\}$.
The TPTP.SET problem collection has been used to empirically evaluate previous
versions of $\\{log\\}$ [Cristiá and Rossi (2019)].

From these 176 formulas we generated two larger collections of formulas
involving RIS: the Negative collection, where formulas are expected to be
unsatisfiable; and the Positive collection, where formulas are expected to be
satisfiable, although a few of them are not.

The Negative collection was generated as follows. Let $\Theta$ be the formula
of one of the selected 176 problems. Let $\mathit{vars}(\Theta)$ be the set of
free variables of $\Theta$. Then $\Theta$ is transformed into:

$\Theta^{\prime}\bigwedge_{A\in\mathit{vars}(\Theta)}A=\mathsf{ris}(X\mathbin{\mathsf{in}}D_{A},[\mathscr{V}],\mathscr{F},\mathscr{P},\mathscr{C})$

where: $X$ and $D_{A}$ are variables; $\Theta^{\prime}$ is obtained from
$\Theta$ by replacing every occurrence of $\\{\\}$ by
$\mathsf{ris}(X\mathbin{\mathsf{in}}\mathscr{D},[\;],\mathscr{F}_{\emptyset})$;
and $\mathscr{D}$, $\mathscr{F}_{\emptyset}$, $\mathscr{V}$, $\mathscr{F}$,
$\mathscr{P}$ and $\mathscr{C}$ are instantiated as depicted in Table 8. This
means that for each instance of $\mathscr{V}$, $\mathscr{F}$ and
$\mathscr{C}$, an instance of $\mathscr{P}$ and an instance of $\mathscr{D}$
and $\mathscr{F}_{\emptyset}$ are selected. Besides, note that for each
$A\in\mathit{vars}(\Theta)$ a different domain variable is generated (i.e.,
$D_{A}$). In this way, the initial 176 formulas are transformed into 5813
formulas where all variables and every occurrence of the empty set are RIS
terms.

Domain, filter, pattern and functional predicates used to generate RIS
formulas. Recall that in $\\{log\\}$ the fifth argument of a RIS term is used
to specify the functional predicates possibly occurring in the RIS.  Instances
of $\mathscr{V}$, $\mathscr{F}$ and $\mathscr{C}$ $B_{i}$ and $D$ are new
variables for each instance
$\mathsf{ris}(X\mathbin{\mathsf{in}}D,[\;],\mathsf{true},\mathscr{P},\mathsf{true})$
$\mathsf{ris}(X\mathbin{\mathsf{in}}D,[\;],X\mathbin{\mathsf{in}}B,\mathscr{P},\mathsf{true})$
$\mathsf{ris}(X\mathbin{\mathsf{in}}D,[\;],X\mathbin{\mathsf{nin}}B,\mathscr{P},\mathsf{true})$
$\mathsf{ris}(X\mathbin{\mathsf{in}}D,[B],X\mathbin{\mathsf{in}}B,\mathscr{P},\mathsf{un}(B_{1},B_{2},B))$
$\mathsf{ris}(X\mathbin{\mathsf{in}}D,[B],X\mathbin{\mathsf{nin}}B,\mathscr{P},\mathsf{un}(B_{1},B_{2},B))$
$\mathsf{ris}(X\mathbin{\mathsf{in}}D,[\;],\mathsf{disj}(X,B_{1}),\mathscr{P},\mathsf{true})$
$\mathsf{ris}(X\mathbin{\mathsf{in}}D,[\;],\mathsf{ndisj}(X,B_{1}),\mathscr{P},\mathsf{true})$
$\mathsf{ris}(X\mathbin{\mathsf{in}}D,[\;],X=B_{1},\mathscr{P},\mathsf{true})$
$\mathsf{ris}(X\mathbin{\mathsf{in}}D,[\;],X\mathbin{\mathsf{neq}}B_{1}),\mathscr{P},\mathsf{true})$
Instances of $\mathscr{P}$ $X$ is the control variable and $V$ is a new
variable for each instance $X$ $[X,V]$ Instances of $\mathscr{D}$ and
$\mathscr{F}_{\emptyset}$ $B_{i}$ are new variables for each instance
$\mathsf{ris}(X\mathbin{\mathsf{in}}\\{\\},[\;],\mathsf{false})$
$\mathsf{ris}(X\mathbin{\mathsf{in}}\\{\\},[\;],\mathsf{true})$
$\mathsf{ris}(X\mathbin{\mathsf{in}}\\{B_{1}/B_{2}\\},[\;],X\mathbin{\mathsf{neq}}B_{1}\mathbin{\&}X\mathbin{\mathsf{nin}}B_{2})$

In turn, the Positive collection is generated as follows. First, one
$\mathcal{RIS}$-constraint of each of the 176 original formulas is negated
(specifically, it is replaced by its negated version). In general this turns
the formula from unsatisfiable to satisfiable. However, 27 formulas become
trivial and so were removed. Then, if $\Theta$ is one of the remaining 149
formulas is transformed as follows:

$\Theta^{\prime}\bigwedge_{A\in\mathit{vars}(\Theta)}A=\mathsf{ris}(X\mathbin{\mathsf{in}}D_{A},[\mathscr{V}],\mathscr{F},\mathscr{P},\mathscr{C})\land
D_{A}\mathbin{\mathsf{neq}}\\{\\}$

where the same considerations of the Negative collection apply. The last
conjunct implies that every non-empty RIS has at least one element. In this
way the Positive collection has 4728 problems.

The union of the Negative and Positive collections makes a 10541 problems
benchmark to evaluate the automated processing of RIS.

We run two experiments to empirically assess the effectiveness and efficiency
of $\\{log\\}$ on the automated processing of RIS. In these experiments we
measure the number of formulas that $\\{log\\}$ solves before a given timeout
and the average time in doing so.

The results of these experiments are summarized in Table 8. In the first
experiment the timeout is 2 seconds; in the second experiment the timeout is
60 seconds but only the unsolved formulas of the first experiment are
considered. That is, the 976 ‘negative’ formulas and the 586 ‘positive’
formulas used in the 60 seconds experiment are those that remain unsolved in
the 2 seconds experiment. The last row of the table shows a summary of both
experiments.

According to these figures, it can be said that augmenting the timeout from 2
seconds to 60 seconds produces a modest gain in the number of solved formulas,
but given that most of the formulas are solved in a few milliseconds, setting
a higher timeout would not be harmful. Finally, considering both experiments
$\\{log\\}$ solves 89% of the benchmark in just below three quarters of a
second in average.

Summary of the empirical evaluation  Collection Problems Solved Percentage
Average Time First experiment (2 seconds timeout) Negative 5813 4837 83% 0.069
s Positive 4728 4142 88% 0.035 s Second experiment (60 seconds timeout)
Negative 976 266 27% 13.718 s Positive 586 173 30% 13.680 s Summary 10541 9418
89% 0.690 s

Although these results are good, there is room for improvements. One such
improvement is a more efficient implementation of derived constraints (cf.
Section 2.4). In a previous work [Cristiá and Rossi (2019)], we have used the
initial 176 formulas (that is, formulas where set variables are _not_ bound to
RIS terms) to assess a version of $\\{log\\}$ where intersection, subset and
difference are implemented as derived constraints. That is, for instance, an
$\mathit{inters}$ constraint is rewritten as a formula based on $\mathit{un}$
and $\mathit{disj}$ instead of being processed by an _ad-hoc_ rewriting
procedure. When these formulas are run on that version of $\\{log\\}$, it
solves 94% in 0.078 seconds in average; but when just intersection and subset
are processed by _ad-hoc_ rewriting procedures, $\\{log\\}$ solves all of
them. In the current version of $\\{log\\}$, intersection, subset and
difference on RIS terms are treated as derived constraints. Based on the
results obtained with the previous work, it is reasonable to assume that
extending the _ad-hoc_ rewriting procedures for these constraints to RIS terms
might yield significantly better results than those reported in Table 8.

###  8.1 Technical details of the empirical evaluation

The experiments were performed on a Latitude E7470 (06DC) with a 4 core
Intel(R) Core™ i7-6600U CPU at 2.60GHz with 8 Gb of main memory, running Linux
Ubuntu 18.04.3 (LTS) 64-bit with kernel 4.15.0-65-generic. $\\{log\\}$
4.9.6-17i over SWI-Prolog (multi-threaded, 64 bits, version 7.6.4) was used
during the experiments.

Each $\\{log\\}$ formula was run within the following Prolog program:

    use_module(library(dialect/sicstus/timeout)).
    consult(’setlog.pl’).
    consult_lib.
    set_prolog_flag(toplevel_print_options,[quoted(true),portray(true)]).
    get_time(Tini).
    time_out(setlog(<FORMULA>), <TIMEOUT>, _RES).
    get_time(Tend).

where `<FORMULA>` is replaced by each formula and `<TIMEOUT>` is either 2000
or 60000 depending on the experiment. Each of these programs was run from the
command line as follows:

    prolog -q < <PROG>

The execution time for each problem is calculated as Tend - Tini.

The full data set containing all these Prolog programs can be downloaded from
https://www.dropbox.com/s/d1ysiq3eji2xg9a/exTOPLAS.tar.gz?dl=0.

##  9 Related Work

As mentioned in Section 1, some form of intensional sets is offered by the CLP
language CLP($\mathcal{SET}$). Specifically, CLP($\mathcal{SET}$) supports
general intensional sets by implementing set-grouping on top of the language
itself (i.e., not as a primitive feature of the language). Hence, formulas
involving intensional sets fall outside the scope of CLP($\mathcal{SET}$)’s
decision procedure. As an example, the formula $A\cap B\neq\\{x:x\in A\land
x\in B\\}$, which is written in CLP($\mathcal{SET}$) as

$\mathsf{inters}(A,B,C)\mathbin{\&}D=\\{X:X\hskip 2.0pt\mathsf{in}\hskip
2.0ptA\mathbin{\&}X\hskip 2.0pt\mathsf{in}\hskip 2.0ptB\\}\mathbin{\&}C\hskip
2.0pt\mathsf{neq}\hskip 2.0ptD$

is (wrongly) found to be $\mathit{true}$ by the CLP($\mathcal{SET}$)