Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add documentation to gecode.mzn #193

Merged
merged 1 commit into from
Jan 29, 2024
Merged

Add documentation to gecode.mzn #193

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions changelog.in
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,13 @@ Date: 2020-??-??
[DESCRIPTION]
Let's see.

[ENTRY]
Module: flatzinc
What: change
Rank: minor
[DESCRIPTION]
Add MiniZinc documentation comments to the Gecode-specific library file.

[ENTRY]
Module: flatzinc
What: bug
Expand Down
85 changes: 73 additions & 12 deletions gecode/flatzinc/mznlib/gecode.mzn
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,44 +30,87 @@
%
%

% This file contains predicate definitions for additional constraints available
% in the Gecode FlatZinc interpreter.
/***
@groupdef gecode Additional declarations for Gecode

These annotations and predicates are available for the Gecode
solver. In order to use them in a model, include the file "gecode.mzn".
*/

% Additional search annotations
/***
@groupdef gecode.annotations Additional Gecode search annotations
*/

/** @group gecode.annotations Select variable with smallest accumulated failure count */
annotation afc_min;
/** @group gecode.annotations Select variable with smallest accumulated failure count divided by domain size */
annotation afc_size_min;
/** @group gecode.annotations Select variable with largest accumulated failure count */
annotation afc_max;
/** @group gecode.annotations Select variable with largest accumulated failure count divided by domain size */
annotation afc_size_max;
/** @group gecode.annotations Select variable with smallest action count */
annotation action_min;
/** @group gecode.annotations Select variable with smallest action count divided by domain size */
annotation action_size_min;
/** @group gecode.annotations Select variable with largest action count */
annotation action_max;
/** @group gecode.annotations Select variable with largest action count divided by domain size */
annotation action_size_max;
/** @group gecode.annotations Select random variable */
annotation random;

annotation int_assign(array[int] of var int: x, ann:a);

/** @group gecode.annotations Specify default search strategy for integer variables to use variable selection
strategy \a varsel, and value choice strategy \a valsel. */
annotation int_default_search(ann: varsel, ann: valsel);
/** @group gecode.annotations Specify default search strategy for Boolean variables to use variable selection
strategy \a varsel, and value choice strategy \a valsel. */
annotation bool_default_search(ann: varsel, ann: valsel);
/** @group gecode.annotations Specify default search strategy for set variables to use variable selection
strategy \a varsel, and value choice strategy \a valsel. */
annotation set_default_search(ann: varsel, ann: valsel);
/** @group gecode.annotations Specify default search strategy for float variables to use variable selection
strategy \a varsel, and value choice strategy \a valsel. */
annotation float_default_search(ann: varsel, ann: valsel);

% Simple LNS: upon restart, for each variable the probability of it being
% fixed to the previous solution is 'percentage' (out of 100).
/** @group gecode.annotations
Simple large neighbourhood search strategy: upon restart, for each variable in \a x,
the probability of it being fixed to the previous solution is \a percentage (out of 100).
*/
annotation relax_and_reconstruct(array[int] of var int: x, int: percentage);

% Simple LNS: upon restart, for each variable the probability of it being
% fixed to the previous solution is 'percentage' (out of 100). Start from
% an initial solution y.
/** @group gecode.annotations
Simple large neighbourhood search strategy: upon restart, for each variable in \a x,
the probability of it being fixed to the previous solution is \a percentage (out of 100).
Start from an initial solution \a y.
*/
annotation relax_and_reconstruct(array[int] of var int: x, int: percentage, array[int] of int: y);

% i in z <-> forall (j in x) (i in y[j])
/***
@groupdef gecode.constraints Additional Gecode constraints
*/

/** @group gecode.constraints
Constrain \a z to be the intersection of all sets
in \a y that are selected by \a x: \(i \in \a z \leftrightarrow \forall j \in \a x: (i \in \a y[j]) \)
*/
predicate gecode_array_set_element_intersect(var set of int: x,
array[int] of var set of int: y, var set of int: z);

% (i in z <-> exists (j in x) (i in y[j])) /\ (i in x /\ j in x /\ i!=j -> disjoint(y[i],y[j]))
/** @group gecode.constraints
Constrain \a z to be the disjoint union of all sets
in \a y that are selected by \a x: \(i \in \a z \leftrightarrow \exists j \in \a x: (i \in \a y[j]) \)
and \( i \in \a x \land j \in \a x \land i\neq j \rightarrow \a y[i] \cap \a y[j]=\emptyset \)
*/
predicate gecode_array_set_element_partition(var set of int: x,
array[int] of var set of int: y, var set of int: z);

% z subset u /\ ( i in z <-> forall (j in x) (i in y[j]) )
/** @group gecode.constraints
Constrain \a z to be a subset of \a u, and \a z to be the intersection of all sets
in \a y that are selected by \a x: \(i \in \a z \leftrightarrow \forall j \in \a x: (i \in \a y[j]) \)
*/
predicate gecode_array_set_element_intersect_in(var set of int: x,
array[int] of var set of int: y,
var set of int: z, set of int: u);
Expand All @@ -82,9 +125,16 @@ predicate gecode_among_seq_int(array[int] of var int: x, set of int: S,
predicate gecode_among_seq_bool(array[int] of var bool: x, bool: b,
int: l, int: m, int: n);

% Overloading for among_seq
/** @group gecode.constraints
Every subsequence of \a x of length \a l has at least \a m and at most \a n occurrences
of the values in \a S
*/
predicate among_seq(array[int] of var int: x, set of int: S,
int: l, int: m, int: n) = gecode_among_seq_int(x,S,l,m,n);
/** @group gecode.constraints
Every subsequence of \a x of length \a l has at least \a m and at most \a n occurrences
of the value \a b
*/
predicate among_seq(array[int] of var bool: x, bool: b,
int: l, int: m, int: n) = gecode_among_seq_bool(x,b,l,m,n);

Expand All @@ -94,10 +144,21 @@ predicate gecode_circuit_cost_array(array[int] of int: c,
predicate gecode_circuit_cost(array[int] of int: c, array[int] of var int: x,
var int: z);

/** @group gecode.constraints
Constrains the elements of \a x to define a circuit where \a x[\p i] = \p j means
that \p j is the successor of \p i. Additionally, constrain \a z to
be the cost of the circuit. Each edge cost is defined by array \a c. The variables
\a y[i] are constrained to be the edge cost of the node \a x[i].
*/
predicate circuit_cost_array(array[int] of int: c,
array[int] of var int: x, array[int] of var int: y, var int: z) =
gecode_circuit_cost_array(c,[x[i]-min(index_set(x)) | i in index_set(x)],
y,z);
/** @group gecode.constraints
Constrains the elements of \a x to define a circuit where \a x[\p i] = \p j means
that \p j is the successor of \p i. Additionally, constrain \a z to
be the cost of the circuit. Each edge cost is defined by array \a c.
*/
predicate circuit_cost(array[int] of int: c, array[int] of var int: x,
var int: z) =
gecode_circuit_cost(c, [x[i]-min(index_set(x)) | i in index_set(x)], z);
Expand Down