**Constraint (Logic) Programming with Sets**

*L*_{SET} is a constraint language for expressing and solving quantifier-free first-order formulas over a universe of finite sets.

It was initially defined as part of the Constraint Logic Programming language CLP(*SET*) [1].

Basically,* L*_{SET} provides a very general form of extensional sets, namely untyped hereditarily finite hybrid sets, where one or more set elements can be variables. Hereditarily finite sets are sets whose elements can be other hereditarily finite sets; while hybrid sets are sets whose elements can be non-set objects of any type. Sets can be manipulated through the usual set-theoretical operators (e.g., set equality, membership, union, inclusion, etc) which are provided in the form of (set) constraints. In particular, set equality among sets is implemented by set unification [2]. Constraint satisfiability is checked by a complete constraint solver (actually, a decision procedure for* L*_{SET} formulas).

Over the years, * L*_{SET} has been extended with various new features, leading to new

versions of the original constraint language:

*L*_{SET+FD}: adding intervals and FD-constraints (i.e., integer arithmetic over Finite

Domains) [3]*L*_{BR}: adding binary relations and partial functions [4]*L*_{CP}: adding Cartesian products [5]*L*_{RIS}: adding restricted intensional sets [6].

*L*_{SET}, along with all its extensions, has been implemented in two distinct tools:

– ** {log}** (pronounced ‘setlog’), a Prolog library and interactive interpreter for a CLP language extending Prolog (

*{log}*home page

**)**

– **JSetL**, a Java library supporting declarative (constraint) programming in O-O programming (JSetL home page**)**.

**Main papers related to L_{SET}** (for more specific papers about {log} and JSetL visit their respective web pages)

- A. Dovier, C. Piazza, E. Pontelli, and G. Rossi.

Sets and Constraint Logic Programming.

ACM Transaction on Programming Language and Systems, Vol. 22 (5), Sept. 2000,

861-931. - A. Dovier, E. Pontelli, and G. Rossi.

Set Unification.

Theory and Practice of Logic Programming (ISSN: 1471-0684), 6(6):645-701, 2006 - A. Dal Palu’, A. Dovier, E. Pontelli, and G. Rossi.

Integrating Finite Domain Constraints and CLP with Sets.

In D. Miller, ed., Fifth ACM-SIGPLAN Conference on Principles and Practice of

Declarative Programming, ACM Press (ISBN/ISSN: 1-58113-705-2), 2003, 219-229. - Maximiliano Cristiá, Gianfranco Rossi.

Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary

Relations.

Journal of Automated Reasoning. In press. 2019. - Maximiliano Cristiá, Gianfranco Rossi

A Set Solver for Finite Set Relation Algebra.

In: J. Desharnais, W. Guttmann, S. Joosten (Eds),

Relational and Algebraic Methods in Computer Science (RAMICS 2018).

Lecture Notes in Computer Science, Vol. 11194, Springer International

Publishing (ISSN: 0302-9743), 333-349, 2018. - Maximiliano Cristiá, Gianfranco Rossi

A Decision Procedure for Restricted Intensional Sets.

In: L. de Moura (Ed.), Automated Deduction – CADE 26,

Lecture Notes in Artificial Intelligence, Vol. 10395,

Springer International Publishing ( ISSN: 0302-9743), 186-201, 2017

**Rewrite
rules **for constraint
solving

The following documents list in an abstract compact way all the rewrite rules used in the constraint solver for:

– *L*_{BR} formulas (here)

– *L*_{RIS} formulas (here)