4.2.1.2. Annotations

These annotations control evaluation and solving behaviour.

General annotations

In this section: mzn_output_section, add_to_output, annotated_expression, cache_result, constraint_name, defines_var, doc_comment, domain_change_constraint, empty_annotation, expression_name, is_defined_var, is_reverse_map, maybe_partial, mzn_add_annotated_expression, mzn_check_enum_var, mzn_check_var, mzn_constraint_name, mzn_deprecated, mzn_expression_name, mzn_path, mzn_rhs_from_assignment, no_cse, no_output, output, output_array, output_only, output_var, promise_commutative, promise_total, var_is_introduced.

Functions and Predicates

mzn_output_section

annotation mzn_output_section(string: s)

Used internally by the compiler to set the output section s for an output item. An output item can be annotated directly with a string literal to set its output section as in output :: "my_section" ["hello, world\n"] or using the syntax output ["hello, world\n"] to "my_section.

Annotations

add_to_output

annotation add_to_output

Declare that the annotated variable should be added to the output of the model. This annotation only has an effect when the model does not have an output item.

annotated_expression

annotation annotated_expression

Mark annotation argument as annotated expression

cache_result

annotation cache_result

Enables caching of the result of the annotated function declaration such that further calls with the same arguments yield the cached initial result.

Currently only supported for par functions with at least one parameter.

constraint_name

annotation constraint_name(string: s)

Used to attach a name s to a constraint and its decomposition. String annotations on constraint keywords are re-written as constraint_name annotations

defines_var

1.  annotation defines_var(var opt $T: c)

2.  annotation defines_var(array [$U] of var opt $T: arr)
  1. Declare variable: c as being functionally defined by the annotated constraint. This annotation is introduced into FlatZinc code by the compiler.

  2. Declare an array of variables arr as being functionally defined by the annotated constraint. This annotation is introduced into FlatZinc code by the compiler.

doc_comment

annotation doc_comment(string: s)

Document the function or variable declaration item with the string s.

domain_change_constraint

annotation domain_change_constraint

Marks a constraint as a recorded domain changing constraint (when mzn2fzn called with -g flag

empty_annotation

annotation empty_annotation

Empty annotation, will be removed during compilation

expression_name

annotation expression_name(string: s)

Used to attach a name s to an expression, this should also propagate to any sub-expressions or decomposition of the annotated expression. String annotations on expressions are re-written as expression_name annotations

is_defined_var

annotation is_defined_var

Declare the annotated variable as being functionally defined. This annotation is introduced into FlatZinc code by the compiler.

is_reverse_map

annotation is_reverse_map

Declare that the annotated expression is used to map an expression back from FlatZinc to MiniZinc.

maybe_partial

annotation maybe_partial

Declare that expression may have undefined result (to avoid warnings)

mzn_add_annotated_expression

annotation mzn_add_annotated_expression(int: idx)

Used internally by the compiler

mzn_check_enum_var

annotation mzn_check_enum_var(array [int] of set of int: x)

Declare that the annotated variable is required for checking solutions and has an enum type x.

mzn_check_var

annotation mzn_check_var

Declare that the annotated variable is required for checking solutions.

mzn_constraint_name

annotation mzn_constraint_name(string: n)

Declare a name n for the annotated constraint.

mzn_deprecated

annotation mzn_deprecated(string: version, string: explanation)

State that a function is deprecated since MiniZinc version version with humand readable explanation.

mzn_expression_name

annotation mzn_expression_name(string: n)

Declare a name n for the annotated expression.

mzn_path

annotation mzn_path(string: s)

Representation of the call-stack when the annotated item was introduced, as a string s. Can be used to uniquely identify variables and constraints across different compilations of a model that may have different names. This annotations is introduced into FlatZinc code by the compiler and is retained if –keep-paths argument is used.

mzn_rhs_from_assignment

annotation mzn_rhs_from_assignment

Used internally by the compiler

no_cse

annotation no_cse

This annotation will prevent calls to the function annotated to be added to the Common Subexpression Elimination map.

WARNING: using this annotation might result in duplicated constraints when used incorrectly.

no_output

annotation no_output

Declare that the annotated variable should not be added to the output of the model. This annotation only has an effect when the model does not have an output item.

output

annotation 'output'(any $T: x)
annotation 'output'(array [$U] of any $T: x)

Declare that the annotated variable x should be added to the output of the model. This annotation only has an effect when the model does not have an output item.

output_array

annotation output_array(array [$U] of set of int: a)

Declare that the annotated array should be printed by the solver with the given index sets a. This annotation is introduced into FlatZinc code by the compiler.

output_only

annotation output_only

Declare that the annotated variable should be only used for output. This annotation can be used to define variables that are required for solution checkers, or that are necessary for the output item. The annotated variable must be par.

output_var

annotation output_var

Declare that the annotated variable should be printed by the solver. This annotation is introduced into FlatZinc code by the compiler.

promise_commutative

annotation promise_commutative

Declare the function to be commutative, i.e., the function has the same result regardless of the order in which the function parameters are provided.

WARNING: a commutative function must have only arguments of a single type, or a single array as an argument.

promise_total

annotation promise_total

Declare function as total, i.e. it does not put any constraints on its arguments.

var_is_introduced

annotation var_is_introduced

Declare a variable as being introduced by the compiler.

Propagation strength annotations

In this section: bounds, bounds_propagation, domain, domain_propagation, value_propagation.

bounds

annotation bounds

Annotate a constraint to use bounds propagation

Note: This annotation will be deprecated. Use bounds_propagation instead.

bounds_propagation

annotation bounds_propagation

Annotate a constraint to use bounds propagation

domain

annotation domain

Annotate a constraint to use domain propagation

Note: This annotation will be deprecated. Use domain_propagation instead.

domain_propagation

annotation domain_propagation

Annotate a constraint to use domain propagation

value_propagation

annotation value_propagation

Annotate a constraint to use value propagation

Search annotations

Variable selection annotations

In this section: anti_first_fail, dom_w_deg, first_fail, impact, input_order, largest, max_regret, most_constrained, occurrence, smallest.

anti_first_fail

annotation anti_first_fail

Choose the variable with the largest domain

dom_w_deg

annotation dom_w_deg

Choose the variable with largest domain, divided by the number of attached constraints weighted by how often they have caused failure

first_fail

annotation first_fail

Choose the variable with the smallest domain

impact

annotation impact

Choose the variable with the highest impact so far during the search

input_order

annotation input_order

Search variables in the given order

largest

annotation largest

Choose the variable with the largest value in its domain

max_regret

annotation max_regret

Choose the variable with largest difference between the two smallest values in its domain

most_constrained

annotation most_constrained

Choose the variable with the smallest domain, breaking ties using the number of attached constraints

occurrence

annotation occurrence

Choose the variable with the largest number of attached constraints

smallest

annotation smallest

Choose the variable with the smallest value in its domain

Value choice annotations

In this section: indomain, indomain_interval, indomain_max, indomain_median, indomain_middle, indomain_min, indomain_random, indomain_reverse_split, indomain_split, indomain_split_random, outdomain_max, outdomain_median, outdomain_min, outdomain_random.

indomain

annotation indomain

Assign values in ascending order

indomain_interval

annotation indomain_interval

If the domain consists of several contiguous intervals, reduce the domain to the first interval. Otherwise bisect the domain.

indomain_max

annotation indomain_max

Assign the largest value in the domain

indomain_median

annotation indomain_median

Assign the middle value in the domain, or the smaller of the two middle values in case of an even number of elements in the domain

indomain_middle

annotation indomain_middle

Assign the value in the domain closest to the mean of its current bounds

indomain_min

annotation indomain_min

Assign the smallest value in the domain

indomain_random

annotation indomain_random

Assign a random value from the domain

indomain_reverse_split

annotation indomain_reverse_split

Bisect the domain, excluding the lower half first

indomain_split

annotation indomain_split

Bisect the domain, excluding the upper half first

indomain_split_random

annotation indomain_split_random

Bisect the domain, randomly selecting which half to exclude first

outdomain_max

annotation outdomain_max

Exclude the largest value from the domain

outdomain_median

annotation outdomain_median

Exclude the middle value from the domain

outdomain_min

annotation outdomain_min

Exclude the smallest value from the domain

outdomain_random

annotation outdomain_random

Exclude a random value from the domain

Exploration strategy annotations

In this section: complete.

complete

annotation complete

Perform a complete search

Restart annotations

In this section: restart_constant, restart_geometric, restart_linear, restart_luby, restart_none.

restart_constant

annotation restart_constant(int: scale)

Restart after constant number of nodes scale

restart_geometric

annotation restart_geometric(float: base, int: scale)

Restart with geometric sequence with parameters base and scale

restart_linear

annotation restart_linear(int: scale)

Restart with linear sequence scaled by scale

restart_luby

annotation restart_luby(int: scale)

Restart with Luby sequence scaled by scale

restart_none

annotation restart_none

Do not restart

Other declarations

In this section: bool_search, float_search, int_search, set_search, seq_search.

Functions and Predicates

Annotations

Warm start annotations

To be put on the solve item, similar to search annotations. A variable can be mentioned several times and in different annotations but only one of the values is taken

Warm start annotations with optional values

The value arrays can contain <> elements (absent values). The following decompositions eliminate those elements because FlatZinc 1.6 does not support optionals.

In this section: warm_start.

warm_start

1.  annotation warm_start(array [int] of var bool: x,
                          array [int] of opt bool: v)

2.  annotation warm_start(array [int] of var int: x,
                          array [int] of opt int: v)

3.  annotation warm_start(array [int] of var float: x,
                          array [int] of opt float: v)

4.  annotation warm_start(array [int] of var set of int: x,
                          array [int] of opt set of int: v)
  1. Specify warm start values v for an array of booleans x

  2. Specify warm start values v for an array of integers x

  3. Specify warm start values v for an array of floats x

  4. Specify warm start values v for an array of sets x

Other declarations

In this section: warm_start, warm_start_array.

warm_start

1.  annotation warm_start(array [int] of var bool: x,
                          array [int] of bool: v)

2.  annotation warm_start(array [int] of var int: x, array [int] of int: v)

3.  annotation warm_start(array [int] of var float: x,
                          array [int] of float: v)

4.  annotation warm_start(array [int] of var set of int: x,
                          array [int] of set of int: v)
  1. Specify warm start values v for an array of booleans x

  2. Specify warm start values v for an array of integers x

  3. Specify warm start values v for an array of floats x

  4. Specify warm start values v for an array of sets x

warm_start_array

annotation warm_start_array(array [int] of ann: w)

Specify an array w of warm_start annotations or other warm_start_array annotations. Can be useful to keep the annotation order in FlatZinc for manual updating.

Note: if you have search annotations as well, put warm_starts into seq_search in order to have precedence between both, which may matter.

Large Neighbourhood Search annotations

These annotations can be used on the solve item (similar to search annotations) to specify Large Neighbourhood Search meta-heuristics.

These annotations specify how the search is restricted to a neighbourhood when a solver restarts. The annotations define which variables will be fixed to their values from a previous solution in that case. All other variables will be reset to their initial domains by the restart.

The annotations can be used together with search annotations and restart annotations.

In this section: relax_and_reconstruct.

relax_and_reconstruct

annotation relax_and_reconstruct(array [int] of var int: x, int: p)

Random neighbourhood over variables x with probability p percent

Upon restart, each variable in x is fixed to the value of the incumbent solution with a probability of p percent.

Context annotations

These are used internally by the compiler, and should not be used in models.

In this section: ctx_mix, ctx_neg, ctx_pos, ctx_root.

ctx_mix

annotation ctx_mix

Mixed context

ctx_neg

annotation ctx_neg

Negative context

ctx_pos

annotation ctx_pos

Positive context

ctx_root

annotation ctx_root

Root context

Redundant and symmetry breaking constraints

These predicates allow users to mark constraints as e.g. symmetry breaking or redundant, so that solvers can choose to implement them differently.

We cannot easily use annotations for this purpose, since annotations are propagated to all constraints in a decomposition, which may be incorrect for redundant or symmetry breaking constraints in the presence of common subexpression elimination (CSE).

In this section: implied_constraint, redundant_constraint, symmetry_breaking_constraint.

implied_constraint

predicate implied_constraint(var bool: b)

Mark b as an implied constraint (synonym for redundant_constraint)

redundant_constraint

predicate redundant_constraint(var bool: b)

Mark b as a redundant constraint

symmetry_breaking_constraint

predicate symmetry_breaking_constraint(var bool: b)

Mark b as a symmetry breaking constraint