1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
%
% Main authors:
% Guido Tack <tack@gecode.org>
%
% Copyright:
% Guido Tack, 2007
%
% This file is part of Gecode, the generic constraint
% development environment:
% http://www.gecode.org
%
% Permission is hereby granted, free of charge, to any person obtaining
% a copy of this software and associated documentation files (the
% "Software"), to deal in the Software without restriction, including
% without limitation the rights to use, copy, modify, merge, publish,
% distribute, sublicense, and/or sell copies of the Software, and to
% permit persons to whom the Software is furnished to do so, subject to
% the following conditions:
%
% The above copyright notice and this permission notice shall be
% included in all copies or substantial portions of the Software.
%
% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
%
%
/***
@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".
*/
/***
@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);
/** @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);
/** @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);
/***
@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);
/** @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);
/** @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);
% Every subsequence of x of length l has at least m and at most occurrences
% of the values in S
predicate gecode_among_seq_int(array[int] of var int: x, set of int: S,
int: l, int: m, int: n);
% Every subsequence of x of length l has at least m and at most occurrences
% of the value b
predicate gecode_among_seq_bool(array[int] of var bool: x, bool: b,
int: l, int: m, int: 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 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);
% Circuit constraints
predicate gecode_circuit_cost_array(array[int] of int: c,
array[int] of var int: x, array[int] of var int: y, var int: z);
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);
% Scheduling constraints
predicate gecode_schedule_unary(array[int] of var int: x, array[int] of int: p);
predicate gecode_schedule_unary_optional(array[int] of var int: x,
array[int] of int: p, array[int] of var bool: m);
predicate gecode_schedule_cumulative_optional(array[int] of var int: start,
array[int] of int: duration, array[int] of int: usage,
array[int] of var bool: m, int: capacity);
|
