Functional Modelling System

Syntax Overview

This document should serve as a quick overview of the statements which are possible in IDP4.

Directives

Directives are always of the form # directiveName number.

Supported directives are:

• nbModels, determines the number of models which need to be printed
• printFullStructure, determines whether the full ASP structure needs to be outputted to the model or not
• printASP, determines whether the full ASP source needs to be printed or not
• constrain, determines whether you want to see all the structures given the definitions or only the models
• inline, determines whether the inliner does its work
• pushNegs, determines whether negations are pushed

Scripts

It is possible to directly write external functions scripts for use in clingo. These are not conform the other directives. (See the example for more info about these)

Imports

Import statements are of the form: import "filename.fml".

A file containing only definitions is considered a library file and can be imported. Some useful symbols are predefined in the stdlib which is implicitly imported.

Declarations

It is possible to introduce a new symbol in a few ways:

• a := expression., which defines the new symbol a to have the interpretation of the expressions.
• a :: subset of expression., which introduces a to be a subset of the set determined by the expression.
• a :: element of expression., same as the previous one but a will be a single element instead of the full set
• a :: function to expression., which introduces a to be a unary function with codomain the set determined by the expression
• a :: predicate., which introduces a to be a predicate (a unary function to booleans).
• a :: proposition., introduces a to be a proposition
• a\2 :: constructor., introduces the binary constructor function a
• a\2 :: external function., introduces the binary external function a, this should only be used in conjunction with a script directive

Expressions

Expressions are based on the lambda calculus:

• ! set predicate is used to say that the function predicate should hold for every member of set set.
• ? set predicate same as ! but existential.
• Arithmetic operators over integers + - / * are supported.
• Comparison operators over integers < =< >= > = ~= are supported
• Boolean operators & | ~ <=> => <= are supported
• Integers and strings can be used 1 "Hello World"
• let a := 1 ; b := 2 in a+b. is used to locally define a and b so this expressions evaluates to 3
• {x,y || a <- {{1,2},{3,4}}, x <- a, x != 1, y := x + 1} the set consisting of the x and y's, such that a is an element of the set {{1,2},{3,4}}, x is an element of a, x is not equal to 1, and y is one larger than x.
• if p then a else b represents is equal to a if boolean p is true, and b otherwise.

Patterns

• variableName
• constructor [arg1 arg2 ...]
• 5, "a"
• <5
• >5
• _