Functional Modelling System



The set constructs are the last fundamental part of the language. Up to now we have only encountered enumerations like {"a","c"} and ranges like {1..5}.

IDP4 supports more advanced set expressions. In a set you can write down a double pipe || and after that you can write a number of different things:

  • a <- s, picks a new variable a out of a set. This variable can then be used in the members of the set. It behaves a lot like a for-loop. {2*a || a <- s} contains the double of all the elements of a set s.
  • a < 5, any Boolean expression is seen as a guard that limits the content of the set. {a || a <- s, a < 5} is the set containing of all numbers in s which are smaller than 5.
  • a := 8, behaves like a local let expression, {a || a := 8} is the singleton set of 8.

Note that these expressions are order dependent, as you can use the variables introduced in one expression in the next one. Look for at example at a definition of union


When you take the union of 2 sets a and b this can be done through first selecting a set s out of the two. And then taking all elements x in this set.


There are a few builtins over sets predefined.

  • quantifiers: forall (!) and exists (?)
  • member: membership test
  • count: returns the cardinality of a set
  • sum : returns the sum of the members of a set
  • sumBy : returns the sum of the members of a set based on the result of a function
  • min: returns the minimum of the members of a set
  • max: returns the maximum of the members of a set
Set Builtins

The other way around

Just like element of you can declare a symbol subset of and let IDP4 search for a set.

Uninterpreted Set
Create your playground on
This playground was created on, our hands-on, knowledge-sharing platform for developers.
Go to