Functional Modelling System

ingdas
25.1K views

Open Source Your Knowledge, Become a Contributor

Technology knowledge has to be shared and made accessible for free. Join the movement.

Create Content

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

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

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

The other way around

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

Uninterpreted Set
Open Source Your Knowledge: become a Contributor and help others learn. Create New Content