A Decision Procedure for Restricted Intensional Sets

In this paper we present a decision procedure for Restricted Intensional Sets (RIS), i.e. sets given by a property rather than by enumerating their elements, similar to set comprehensions available in specification languages such as B and Z. The proposed procedure is parametric with respect to a first-order language and theory chi, providing at least equality and a decision procedure to check for satisfiability of chi-formulas. We show how this framework can be applied when chi is the theory of hereditarily finite sets as is supported by the language CLP(SET). We also present a working implementation of RIS as part of the {log} tool and we show how it compares with a mainstream solver and how it helps in the automatic verification of code fragments.