I have some questions about the meaning and usage for some of the General Annotations for the MiniZinc language. Please explain when they should be used and if possible, give examples.
I have copied the definitions I have found to make the questions more straight forward, from the MiniZinc official lib.
annotation is_defined_var
Declare the annotated variable as being functionally defined. This annotation is introduced into FlatZinc code by the compiler.
What does it mean that the variable is functionally defined? When should this be used?
annotation maybe_partial
Declare that expression may have undefined result (to avoid warnings)
What does it mean that an expression has undefined result? Could someone give an example of this?
annotation promise_total
Declare function as total, i.e. it does not put any constraints on its arguments.
What does this mean? I would love to see an example of this. Is this when you introduce your own function, or can it also be used for the already defined Minizink functions?
annotation var_is_introduced
Declare a variable as being introduced by the compiler.
Again, what does it mean that the variable is introduced by a complier? What would be the opposite statement? The variable is not introduced by the compiler?
annotation defines_var(var $t: c)
Declare variable: c as being functionally defined by the annotated constraint. This annotation is introduced into FlatZinc code by the compiler.
Again what does it mean that c is functionally defined, and could someone give an example of this?
I know that these are a lot of questions about a very specific library, but I could not find any good explanations anywhere.
Let me start off by saying that the annotations that you are asking about are generally not used while modelling in MiniZinc. (With maybe the exception of maybe_partial, which could be useful to hide warnings in a model.) These annotations should be used by the implementers of FlatZinc solvers and their MiniZinc libraries. For anyone that is still interested: here follow some explainations + examples of the usage of these annotations.
Defined Variables
is_defined_var and defines_var(...) are annotations that are used when an variable is functionally defined. These annotations always occur in pairs. When a variable x has the is_defined_var annotation, then there is a constraint item with the defines_var(x).
A variable is functionally defined when it's solution value follows from a single constraint/function. For example we can type a * b = c, now the solution value of c will follow from just a * b. This means that in the resulting FlatZinc we will find something like:
var int: a;
var int: b;
var int: c ::is_defined_var;
constraint int_times(a,b,c) ::defines_var(c);
Note that these functional definitions often happen in mathematical expressions and reifications.
You will likely never have to add these annotations. They will be automatically added by the MiniZinc compiler. These annotations can then be used by the solver to analyse the relationship between constraints and variables. A solver might for example use a view instead of a full variable in some cases.
Introduced Variables
Some expressions in MiniZinc cannot be expressed in a simple conjunction of constraints. Because of the relationship between various constraints, a new variable might have to be added to have an equivalent logical expression in FlatZinc as the original MiniZinc expression.
Take for example the expression a \/ (b /\ c). This expression needs at least two constraints, a bool_and and a bool_or constraint. However in FlatZinc a predicate call cannot contain anything other than an identifier or a literal. So to express our example in FlatZinc we'll have to reify the and-expression and use the truth value in the or-expression. The resulting FlatZinc will be something like:
var bool: a;
var bool: b;
var bool: c;
var bool: X_INTRODUCED_0_ ::var_is_introduced ::is_defined_var;
constraint bool_or(a,X_INTRODUCED_0_,true);
constraint bool_and(b,c,X_INTRODUCED_0_) ::defines_var(X_INTRODUCED_0_);
Note that because we are using a reification we again see a functionally defined variable.
The annotation var_is_introduced can again be used by the solver to optimise it's process. It can use views for the variable or maybe even lose the variable's value once it is known.
Partial Functions
Some functions, even in bare mathematics, are partial, meaning they do not have a defined result for all possible inputs. The most common example is division: we cannot divide by zero, x / 0 == ??. In most programming languages writing something like this would produce a compilation error. In MiniZinc however an undefined expression will "bubble up" to it's nearest parental Boolean context and define it as false. More on this mechanism can be read in the paper "The Proper Treatment of Undefinedness in Constraint Languages" where it is referred to as relational semantics.
In MiniZinc the most common functions that can be undefined are array access a[i] (undefined when out of bounds), division, and value lookup of an optional variable deopt(x) (undefined when absent).
For example, given an array a with range 1..1 and a Boolean variable b I could write an expression b -> (a[0] == 1). Since a[0] does not exist, there is no value to compare to 1. According to the MiniZinc semantics this means that (a[0] == 1) will be set to false.
Although this is a valid use of MiniZinc, the use of partial functions in such a way is likely a mistake. (This often happens when loops have boundaries that are to big). To make the modeller aware of this, the MiniZinc compiler will print a warning WARNING: undefined result becomes false in Boolean context. Sometimes however the modeller knows what he's doing and might actually want to use these semantics. In that can the expression can be annotated with maybe_partial to tell the compiler that the modeller doesn't need to be warned. For our example we could use b -> (a[0] == 1)::maybe_partial
The maybe_partial annotation is mostly used in MiniZinc libraries when this partial semantics have to be used. Since the modeller shouldn't get any warnings for the correct usage of a library function, these annotations are important.
Total Functions
A total function is the opposite of a partial function. promise_total signals the compiler that the function provided can be used for all possible inputs to the function. You can find it in many places in the standard library.
Because of these promises our library functions can implement relational semantics (as described in the paper "The Proper Treatment of Undefinedness in Constraint Languages") for included functions. Generally a partial function will have to do an extra check and then post constraints based on that check. To ensure that there isn't an endless amount of checking the predicates called in a partial function are promised to be total.
In the compiler a function with promise_total will then behave as if the language would use strict semantics (as described in the same paper) and an undefined result might result in a compilation or solver error.