# IDP4 playground

IngmarDasseville
2,847 views

## Sets

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.
Sets
1
2
3
4
5
6
7
8
9
10
11
12
s1 := {1,2,3,5}.
//Applying a function to every element of a set
s2 := {x*2 || x <- s1}.
//Filtering only the elements which satisfy a certain property
s3 := {x || x <- s2, x < 5}.
//Defining an intermediate symbol s.
s4 := {y, y + 100 || x <- s3, y := x + 2}.
relevant {s1, s2, s3, s4}.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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

Sets
1
2
3
4
5
6
7
8
9
s1 := {1,2,3}.
s2 := {3,4,5}.
myUnion # noprint.
myUnion a b := {x || s <- {a,b}, x <- s}.
s3 := myUnion s1 s2.
relevant {s1,s2,s3}.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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.

## Builtins

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
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
s := {1,2,3}.
//is true iff 2 is an element of s
memberTest1 := member 2 s.
//is true iff 5 is an element of s
memberTest2 := member 5 s.
//is true iff all elements of s are smaller than 4
memberTest3 := ! s (\x -> x < 4).
//is true iff any element of s is larger than 2
memberTest4 := ? s (\x -> x > 2).
three := count s.
six := sum s.
//for every element of s, add a 3 true to the sum
nine := sumBy (\x -> 3) s.
mini := min s.
maxi := max s.
relevant {memberTest1, memberTest2, memberTest3, memberTest4}.
relevant {three, six, nine, mini, maxi}.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

## The other way around

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

Uninterpreted Set
1
2
3
4
s :: subset of {1..10}.
count s = 4.
sum s = 16.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Open Source Your Knowledge: become a Contributor and help others learn.