1:- encoding(utf8).
2
36
76
77:- module(clpfd, [
78 op(760, yfx, #<==>),
79 op(750, xfy, #==>),
80 op(750, yfx, #<==),
81 op(740, yfx, #\/),
82 op(730, yfx, #\),
83 op(720, yfx, #/\),
84 op(710, fy, #\),
85 op(700, xfx, #>),
86 op(700, xfx, #<),
87 op(700, xfx, #>=),
88 op(700, xfx, #=<),
89 op(700, xfx, #=),
90 op(700, xfx, #\=),
91 op(700, xfx, in),
92 op(700, xfx, ins),
93 op(700, xfx, in_set),
94 op(450, xfx, ..), 95 (#>)/2,
96 (#<)/2,
97 (#>=)/2,
98 (#=<)/2,
99 (#=)/2,
100 (#\=)/2,
101 (#\)/1,
102 (#<==>)/2,
103 (#==>)/2,
104 (#<==)/2,
105 (#\/)/2,
106 (#\)/2,
107 (#/\)/2,
108 (in)/2,
109 (ins)/2,
110 all_different/1,
111 all_distinct/1,
112 sum/3,
113 scalar_product/4,
114 tuples_in/2,
115 labeling/2,
116 label/1,
117 indomain/1,
118 lex_chain/1,
119 serialized/2,
120 global_cardinality/2,
121 global_cardinality/3,
122 circuit/1,
123 cumulative/1,
124 cumulative/2,
125 disjoint2/1,
126 element/3,
127 automaton/3,
128 automaton/8,
129 transpose/2,
130 zcompare/3,
131 chain/2,
132 fd_var/1,
133 fd_inf/2,
134 fd_sup/2,
135 fd_size/2,
136 fd_dom/2,
137 fd_degree/2,
138 139 (in_set)/2,
140 fd_set/2,
141 is_fdset/1,
142 empty_fdset/1,
143 fdset_parts/4,
144 empty_interval/2,
145 fdset_interval/3,
146 fdset_singleton/2,
147 fdset_min/2,
148 fdset_max/2,
149 fdset_size/2,
150 list_to_fdset/2,
151 fdset_to_list/2,
152 range_to_fdset/2,
153 fdset_to_range/2,
154 fdset_add_element/3,
155 fdset_del_element/3,
156 fdset_disjoint/2,
157 fdset_intersect/2,
158 fdset_intersection/3,
159 fdset_member/2,
160 fdset_eq/2,
161 fdset_subset/2,
162 fdset_subtract/3,
163 fdset_union/3,
164 fdset_union/2,
165 fdset_complement/2
166 ]). 167
168:- meta_predicate with_local_attributes(?, ?, 0, ?). 169:- public 170 clpfd_equal/2,
171 clpfd_geq/2. 172
173:- use_module(library(apply)). 174:- use_module(library(apply_macros)). 175:- use_module(library(assoc)). 176:- use_module(library(error)). 177:- use_module(library(lists)). 178:- use_module(library(pairs)). 179
180:- set_prolog_flag(generate_debug_info, false). 181
182:- create_prolog_flag(optimise_clpfd, true, [keep(true)]). 183:- create_prolog_flag(clpfd_monotonic, false, [keep(true)]). 184:- create_prolog_flag(clpfd_propagation, default, [keep(true)]). 185
186:- op(700, xfx, cis). 187:- op(700, xfx, cis_geq). 188:- op(700, xfx, cis_gt). 189:- op(700, xfx, cis_leq). 190:- op(700, xfx, cis_lt). 191
965
973
974is_bound(n(N)) :- integer(N).
975is_bound(inf).
976is_bound(sup).
977
978defaulty_to_bound(D, P) :- ( integer(D) -> P = n(D) ; P = D ).
979
984
985goal_expansion(A cis B, Expansion) :-
986 phrase(cis_goals(B, A), Goals),
987 list_goal(Goals, Expansion).
988goal_expansion(A cis_lt B, B cis_gt A).
989goal_expansion(A cis_leq B, B cis_geq A).
990goal_expansion(A cis_geq B, cis_leq_numeric(B, N)) :- nonvar(A), A = n(N).
991goal_expansion(A cis_geq B, cis_geq_numeric(A, N)) :- nonvar(B), B = n(N).
992goal_expansion(A cis_gt B, cis_lt_numeric(B, N)) :- nonvar(A), A = n(N).
993goal_expansion(A cis_gt B, cis_gt_numeric(A, N)) :- nonvar(B), B = n(N).
994
996cis_gt(sup, B0) :- B0 \== sup.
997cis_gt(n(N), B) :- cis_lt_numeric(B, N).
998
999cis_lt_numeric(inf, _).
1000cis_lt_numeric(n(B), A) :- B < A.
1001
1002cis_gt_numeric(sup, _).
1003cis_gt_numeric(n(B), A) :- B > A.
1004
1005cis_geq(inf, inf).
1006cis_geq(sup, _).
1007cis_geq(n(N), B) :- cis_leq_numeric(B, N).
1008
1009cis_leq_numeric(inf, _).
1010cis_leq_numeric(n(B), A) :- B =< A.
1011
1012cis_geq_numeric(sup, _).
1013cis_geq_numeric(n(B), A) :- B >= A.
1014
1015cis_min(inf, _, inf).
1016cis_min(sup, B, B).
1017cis_min(n(N), B, Min) :- cis_min_(B, N, Min).
1018
1019cis_min_(inf, _, inf).
1020cis_min_(sup, N, n(N)).
1021cis_min_(n(B), A, n(M)) :- M is min(A,B).
1022
1023cis_max(sup, _, sup).
1024cis_max(inf, B, B).
1025cis_max(n(N), B, Max) :- cis_max_(B, N, Max).
1026
1027cis_max_(inf, N, n(N)).
1028cis_max_(sup, _, sup).
1029cis_max_(n(B), A, n(M)) :- M is max(A,B).
1030
1031cis_plus(inf, _, inf).
1032cis_plus(sup, _, sup).
1033cis_plus(n(A), B, Plus) :- cis_plus_(B, A, Plus).
1034
1035cis_plus_(sup, _, sup).
1036cis_plus_(inf, _, inf).
1037cis_plus_(n(B), A, n(S)) :- S is A + B.
1038
1039cis_minus(inf, _, inf).
1040cis_minus(sup, _, sup).
1041cis_minus(n(A), B, M) :- cis_minus_(B, A, M).
1042
1043cis_minus_(inf, _, sup).
1044cis_minus_(sup, _, inf).
1045cis_minus_(n(B), A, n(M)) :- M is A - B.
1046
1047cis_uminus(inf, sup).
1048cis_uminus(sup, inf).
1049cis_uminus(n(A), n(B)) :- B is -A.
1050
1051cis_abs(inf, sup).
1052cis_abs(sup, sup).
1053cis_abs(n(A), n(B)) :- B is abs(A).
1054
1055cis_times(inf, B, P) :-
1056 ( B cis_lt n(0) -> P = sup
1057 ; B cis_gt n(0) -> P = inf
1058 ; P = n(0)
1059 ).
1060cis_times(sup, B, P) :-
1061 ( B cis_gt n(0) -> P = sup
1062 ; B cis_lt n(0) -> P = inf
1063 ; P = n(0)
1064 ).
1065cis_times(n(N), B, P) :- cis_times_(B, N, P).
1066
1067cis_times_(inf, A, P) :- cis_times(inf, n(A), P).
1068cis_times_(sup, A, P) :- cis_times(sup, n(A), P).
1069cis_times_(n(B), A, n(P)) :- P is A * B.
1070
1071cis_exp(inf, n(Y), R) :-
1072 ( even(Y) -> R = sup
1073 ; R = inf
1074 ).
1075cis_exp(sup, _, sup).
1076cis_exp(n(N), Y, R) :- cis_exp_(Y, N, R).
1077
1078cis_exp_(n(Y), N, n(R)) :- R is N^Y.
1079cis_exp_(sup, _, sup).
1080cis_exp_(inf, _, inf).
1081
1082cis_goals(V, V) --> { var(V) }, !.
1083cis_goals(n(N), n(N)) --> [].
1084cis_goals(inf, inf) --> [].
1085cis_goals(sup, sup) --> [].
1086cis_goals(sign(A0), R) --> cis_goals(A0, A), [cis_sign(A, R)].
1087cis_goals(abs(A0), R) --> cis_goals(A0, A), [cis_abs(A, R)].
1088cis_goals(-A0, R) --> cis_goals(A0, A), [cis_uminus(A, R)].
1089cis_goals(A0+B0, R) -->
1090 cis_goals(A0, A),
1091 cis_goals(B0, B),
1092 [cis_plus(A, B, R)].
1093cis_goals(A0-B0, R) -->
1094 cis_goals(A0, A),
1095 cis_goals(B0, B),
1096 [cis_minus(A, B, R)].
1097cis_goals(min(A0,B0), R) -->
1098 cis_goals(A0, A),
1099 cis_goals(B0, B),
1100 [cis_min(A, B, R)].
1101cis_goals(max(A0,B0), R) -->
1102 cis_goals(A0, A),
1103 cis_goals(B0, B),
1104 [cis_max(A, B, R)].
1105cis_goals(A0*B0, R) -->
1106 cis_goals(A0, A),
1107 cis_goals(B0, B),
1108 [cis_times(A, B, R)].
1109cis_goals(div(A0,B0), R) -->
1110 cis_goals(A0, A),
1111 cis_goals(B0, B),
1112 [cis_div(A, B, R)].
1113cis_goals(A0//B0, R) -->
1114 cis_goals(A0, A),
1115 cis_goals(B0, B),
1116 [cis_slash(A, B, R)].
1117cis_goals(A0^B0, R) -->
1118 cis_goals(A0, A),
1119 cis_goals(B0, B),
1120 [cis_exp(A, B, R)].
1121
1122list_goal([], true).
1123list_goal([G|Gs], Goal) :- foldl(list_goal_, Gs, G, Goal).
1124
1125list_goal_(G, G0, (G0,G)).
1126
1127cis_sign(sup, n(1)).
1128cis_sign(inf, n(-1)).
1129cis_sign(n(N), n(S)) :- S is sign(N).
1130
1131cis_slash(sup, Y, Z) :- ( Y cis_geq n(0) -> Z = sup ; Z = inf ).
1132cis_slash(inf, Y, Z) :- ( Y cis_geq n(0) -> Z = inf ; Z = sup ).
1133cis_slash(n(X), Y, Z) :- cis_slash_(Y, X, Z).
1134
1135cis_slash_(sup, _, n(0)).
1136cis_slash_(inf, _, n(0)).
1137cis_slash_(n(Y), X, Z) :-
1138 ( Y =:= 0 -> ( X >= 0 -> Z = sup ; Z = inf )
1139 ; Z0 is X // Y, Z = n(Z0)
1140 ).
1141
1142cis_div(sup, Y, Z) :- ( Y cis_geq n(0) -> Z = sup ; Z = inf ).
1143cis_div(inf, Y, Z) :- ( Y cis_geq n(0) -> Z = inf ; Z = sup ).
1144cis_div(n(X), Y, Z) :- cis_div_(Y, X, Z).
1145
1146cis_div_(sup, _, n(0)).
1147cis_div_(inf, _, n(0)).
1148cis_div_(n(Y), X, Z) :-
1149 ( Y =:= 0 -> ( X >= 0 -> Z = sup ; Z = inf )
1150 ; Z0 is X div Y, Z = n(Z0)
1151 ).
1152
1153
1170
1174
1175check_domain(D) :-
1176 ( var(D) -> instantiation_error(D)
1177 ; is_domain(D) -> true
1178 ; domain_error(clpfd_domain, D)
1179 ).
1180
1181is_domain(empty).
1182is_domain(from_to(From,To)) :-
1183 is_bound(From), is_bound(To),
1184 From cis_leq To.
1185is_domain(split(S, Left, Right)) :-
1186 integer(S),
1187 is_domain(Left), is_domain(Right),
1188 all_less_than(Left, S),
1189 all_greater_than(Right, S).
1190
1191all_less_than(empty, _).
1192all_less_than(from_to(From,To), S) :-
1193 From cis_lt n(S), To cis_lt n(S).
1194all_less_than(split(S0,Left,Right), S) :-
1195 S0 < S,
1196 all_less_than(Left, S),
1197 all_less_than(Right, S).
1198
1199all_greater_than(empty, _).
1200all_greater_than(from_to(From,To), S) :-
1201 From cis_gt n(S), To cis_gt n(S).
1202all_greater_than(split(S0,Left,Right), S) :-
1203 S0 > S,
1204 all_greater_than(Left, S),
1205 all_greater_than(Right, S).
1206
1207default_domain(from_to(inf,sup)).
1208
1209domain_infimum(from_to(I, _), I).
1210domain_infimum(split(_, Left, _), I) :- domain_infimum(Left, I).
1211
1212domain_supremum(from_to(_, S), S).
1213domain_supremum(split(_, _, Right), S) :- domain_supremum(Right, S).
1214
1215domain_num_elements(empty, n(0)).
1216domain_num_elements(from_to(From,To), Num) :- Num cis To - From + n(1).
1217domain_num_elements(split(_, Left, Right), Num) :-
1218 domain_num_elements(Left, NL),
1219 domain_num_elements(Right, NR),
1220 Num cis NL + NR.
1221
1222domain_direction_element(from_to(n(From), n(To)), Dir, E) :-
1223 ( Dir == up -> between(From, To, E)
1224 ; between(From, To, E0),
1225 E is To - (E0 - From)
1226 ).
1227domain_direction_element(split(_, D1, D2), Dir, E) :-
1228 ( Dir == up ->
1229 ( domain_direction_element(D1, Dir, E)
1230 ; domain_direction_element(D2, Dir, E)
1231 )
1232 ; ( domain_direction_element(D2, Dir, E)
1233 ; domain_direction_element(D1, Dir, E)
1234 )
1235 ).
1236
1240
1241domain_contains(from_to(From,To), I) :- From cis_leq n(I), n(I) cis_leq To.
1242domain_contains(split(S, Left, Right), I) :-
1243 ( I < S -> domain_contains(Left, I)
1244 ; I > S -> domain_contains(Right, I)
1245 ).
1246
1250
1251domain_subdomain(Dom, Sub) :- domain_subdomain(Dom, Dom, Sub).
1252
1253domain_subdomain(from_to(_,_), Dom, Sub) :-
1254 domain_subdomain_fromto(Sub, Dom).
1255domain_subdomain(split(_, _, _), Dom, Sub) :-
1256 domain_subdomain_split(Sub, Dom, Sub).
1257
1258domain_subdomain_split(empty, _, _).
1259domain_subdomain_split(from_to(From,To), split(S,Left0,Right0), Sub) :-
1260 ( To cis_lt n(S) -> domain_subdomain(Left0, Left0, Sub)
1261 ; From cis_gt n(S) -> domain_subdomain(Right0, Right0, Sub)
1262 ).
1263domain_subdomain_split(split(_,Left,Right), Dom, _) :-
1264 domain_subdomain(Dom, Dom, Left),
1265 domain_subdomain(Dom, Dom, Right).
1266
1267domain_subdomain_fromto(empty, _).
1268domain_subdomain_fromto(from_to(From,To), from_to(From0,To0)) :-
1269 From0 cis_leq From, To0 cis_geq To.
1270domain_subdomain_fromto(split(_,Left,Right), Dom) :-
1271 domain_subdomain_fromto(Left, Dom),
1272 domain_subdomain_fromto(Right, Dom).
1273
1279
1280domain_remove(empty, _, empty).
1281domain_remove(from_to(L0, U0), X, D) :- domain_remove_(L0, U0, X, D).
1282domain_remove(split(S, Left0, Right0), X, D) :-
1283 ( X =:= S -> D = split(S, Left0, Right0)
1284 ; X < S ->
1285 domain_remove(Left0, X, Left1),
1286 ( Left1 == empty -> D = Right0
1287 ; D = split(S, Left1, Right0)
1288 )
1289 ; domain_remove(Right0, X, Right1),
1290 ( Right1 == empty -> D = Left0
1291 ; D = split(S, Left0, Right1)
1292 )
1293 ).
1294
1296
1297domain_remove_(inf, U0, X, D) :-
1298 ( U0 == n(X) -> U1 is X - 1, D = from_to(inf, n(U1))
1299 ; U0 cis_lt n(X) -> D = from_to(inf,U0)
1300 ; L1 is X + 1, U1 is X - 1,
1301 D = split(X, from_to(inf, n(U1)), from_to(n(L1),U0))
1302 ).
1303domain_remove_(n(N), U0, X, D) :- domain_remove_upper(U0, N, X, D).
1304
1305domain_remove_upper(sup, L0, X, D) :-
1306 ( L0 =:= X -> L1 is X + 1, D = from_to(n(L1),sup)
1307 ; L0 > X -> D = from_to(n(L0),sup)
1308 ; L1 is X + 1, U1 is X - 1,
1309 D = split(X, from_to(n(L0),n(U1)), from_to(n(L1),sup))
1310 ).
1311domain_remove_upper(n(U0), L0, X, D) :-
1312 ( L0 =:= U0, X =:= L0 -> D = empty
1313 ; L0 =:= X -> L1 is X + 1, D = from_to(n(L1), n(U0))
1314 ; U0 =:= X -> U1 is X - 1, D = from_to(n(L0), n(U1))
1315 ; between(L0, U0, X) ->
1316 U1 is X - 1, L1 is X + 1,
1317 D = split(X, from_to(n(L0), n(U1)), from_to(n(L1), n(U0)))
1318 ; D = from_to(n(L0),n(U0))
1319 ).
1320
1324
1325domain_remove_greater_than(empty, _, empty).
1326domain_remove_greater_than(from_to(From0,To0), G, D) :-
1327 ( From0 cis_gt n(G) -> D = empty
1328 ; To cis min(To0,n(G)), D = from_to(From0,To)
1329 ).
1330domain_remove_greater_than(split(S,Left0,Right0), G, D) :-
1331 ( S =< G ->
1332 domain_remove_greater_than(Right0, G, Right),
1333 ( Right == empty -> D = Left0
1334 ; D = split(S, Left0, Right)
1335 )
1336 ; domain_remove_greater_than(Left0, G, D)
1337 ).
1338
1339domain_remove_smaller_than(empty, _, empty).
1340domain_remove_smaller_than(from_to(From0,To0), V, D) :-
1341 ( To0 cis_lt n(V) -> D = empty
1342 ; From cis max(From0,n(V)), D = from_to(From,To0)
1343 ).
1344domain_remove_smaller_than(split(S,Left0,Right0), V, D) :-
1345 ( S >= V ->
1346 domain_remove_smaller_than(Left0, V, Left),
1347 ( Left == empty -> D = Right0
1348 ; D = split(S, Left, Right0)
1349 )
1350 ; domain_remove_smaller_than(Right0, V, D)
1351 ).
1352
1353
1357
1358domain_subtract(Dom0, Sub, Dom) :- domain_subtract(Dom0, Dom0, Sub, Dom).
1359
1360domain_subtract(empty, _, _, empty).
1361domain_subtract(from_to(From0,To0), Dom, Sub, D) :-
1362 ( Sub == empty -> D = Dom
1363 ; Sub = from_to(From,To) ->
1364 ( From == To -> From = n(X), domain_remove(Dom, X, D)
1365 ; From cis_gt To0 -> D = Dom
1366 ; To cis_lt From0 -> D = Dom
1367 ; From cis_leq From0 ->
1368 ( To cis_geq To0 -> D = empty
1369 ; From1 cis To + n(1),
1370 D = from_to(From1, To0)
1371 )
1372 ; To1 cis From - n(1),
1373 ( To cis_lt To0 ->
1374 From = n(S),
1375 From2 cis To + n(1),
1376 D = split(S,from_to(From0,To1),from_to(From2,To0))
1377 ; D = from_to(From0,To1)
1378 )
1379 )
1380 ; Sub = split(S, Left, Right) ->
1381 ( n(S) cis_gt To0 -> domain_subtract(Dom, Dom, Left, D)
1382 ; n(S) cis_lt From0 -> domain_subtract(Dom, Dom, Right, D)
1383 ; domain_subtract(Dom, Dom, Left, D1),
1384 domain_subtract(D1, D1, Right, D)
1385 )
1386 ).
1387domain_subtract(split(S, Left0, Right0), _, Sub, D) :-
1388 domain_subtract(Left0, Left0, Sub, Left),
1389 domain_subtract(Right0, Right0, Sub, Right),
1390 ( Left == empty -> D = Right
1391 ; Right == empty -> D = Left
1392 ; D = split(S, Left, Right)
1393 ).
1394
1398
1399domain_complement(D, C) :-
1400 default_domain(Default),
1401 domain_subtract(Default, D, C).
1402
1406
1407domain_intervals(D, Is) :- phrase(domain_intervals(D), Is).
1408
1409domain_intervals(split(_, Left, Right)) -->
1410 domain_intervals(Left), domain_intervals(Right).
1411domain_intervals(empty) --> [].
1412domain_intervals(from_to(From,To)) --> [From-To].
1413
1419
1420domains_intersection(D1, D2, Intersection) :-
1421 domains_intersection_(D1, D2, Intersection),
1422 Intersection \== empty.
1423
1424domains_intersection_(empty, _, empty).
1425domains_intersection_(from_to(L0,U0), D2, Dom) :-
1426 narrow(D2, L0, U0, Dom).
1427domains_intersection_(split(S,Left0,Right0), D2, Dom) :-
1428 domains_intersection_(Left0, D2, Left1),
1429 domains_intersection_(Right0, D2, Right1),
1430 ( Left1 == empty -> Dom = Right1
1431 ; Right1 == empty -> Dom = Left1
1432 ; Dom = split(S, Left1, Right1)
1433 ).
1434
1435narrow(empty, _, _, empty).
1436narrow(from_to(L0,U0), From0, To0, Dom) :-
1437 From1 cis max(From0,L0), To1 cis min(To0,U0),
1438 ( From1 cis_gt To1 -> Dom = empty
1439 ; Dom = from_to(From1,To1)
1440 ).
1441narrow(split(S, Left0, Right0), From0, To0, Dom) :-
1442 ( To0 cis_lt n(S) -> narrow(Left0, From0, To0, Dom)
1443 ; From0 cis_gt n(S) -> narrow(Right0, From0, To0, Dom)
1444 ; narrow(Left0, From0, To0, Left1),
1445 narrow(Right0, From0, To0, Right1),
1446 ( Left1 == empty -> Dom = Right1
1447 ; Right1 == empty -> Dom = Left1
1448 ; Dom = split(S, Left1, Right1)
1449 )
1450 ).
1451
1455
1456domains_union(D1, D2, Union) :-
1457 domain_intervals(D1, Is1),
1458 domain_intervals(D2, Is2),
1459 append(Is1, Is2, IsU0),
1460 merge_intervals(IsU0, IsU1),
1461 intervals_to_domain(IsU1, Union).
1462
1466
1467domain_shift(empty, _, empty).
1468domain_shift(from_to(From0,To0), O, from_to(From,To)) :-
1469 From cis From0 + n(O), To cis To0 + n(O).
1470domain_shift(split(S0, Left0, Right0), O, split(S, Left, Right)) :-
1471 S is S0 + O,
1472 domain_shift(Left0, O, Left),
1473 domain_shift(Right0, O, Right).
1474
1479
1480domain_expand(D0, M, D) :-
1481 ( M < 0 ->
1482 domain_negate(D0, D1),
1483 M1 is abs(M),
1484 domain_expand_(D1, M1, D)
1485 ; M =:= 1 -> D = D0
1486 ; domain_expand_(D0, M, D)
1487 ).
1488
1489domain_expand_(empty, _, empty).
1490domain_expand_(from_to(From0, To0), M, from_to(From,To)) :-
1491 From cis From0*n(M),
1492 To cis To0*n(M).
1493domain_expand_(split(S0, Left0, Right0), M, split(S, Left, Right)) :-
1494 S is M*S0,
1495 domain_expand_(Left0, M, Left),
1496 domain_expand_(Right0, M, Right).
1497
1504
1505domain_expand_more(D0, M, Op, D) :-
1506 1507 1508 1509 1510 1511 domain_expand_more_(D0, M, Op, D).
1512 1513
1514domain_expand_more_(empty, _, _, empty).
1515domain_expand_more_(from_to(From0, To0), M, Op, D) :-
1516 M1 is abs(M),
1517 ( Op = // ->
1518 ( From0 cis_leq n(0) -> From1 cis (From0-n(1))*n(M1) + n(1)
1519 ; From1 cis From0*n(M1)
1520 ),
1521 ( To0 cis_lt n(0) -> To1 cis To0*n(M1)
1522 ; To1 cis (To0+n(1))*n(M1) - n(1)
1523 )
1524 ; Op = div ->
1525 From1 cis From0*n(M1),
1526 To1 cis (To0+n(1))*n(M1)-sign(n(M))
1527 ),
1528 ( M < 0 -> domain_negate(from_to(From1,To1), D)
1529 ; D = from_to(From1,To1)
1530 ).
1531domain_expand_more_(split(S0, Left0, Right0), M, Op, split(S, Left, Right)) :-
1532 S is M*S0,
1533 domain_expand_more_(Left0, M, Op, Left),
1534 domain_expand_more_(Right0, M, Op, Right).
1535
1539
1540domain_contract(D0, M, D) :-
1541 1542 ( M < 0 -> domain_negate(D0, D1), M1 is abs(M)
1543 ; D1 = D0, M1 = M
1544 ),
1545 domain_contract_(D1, M1, D).
1546
1547domain_contract_(empty, _, empty).
1548domain_contract_(from_to(From0, To0), M, from_to(From,To)) :-
1549 ( From0 cis_geq n(0) ->
1550 From cis (From0 + n(M) - n(1)) // n(M)
1551 ; From cis From0 // n(M)
1552 ),
1553 ( To0 cis_geq n(0) ->
1554 To cis To0 // n(M)
1555 ; To cis (To0 - n(M) + n(1)) // n(M)
1556 ).
1557domain_contract_(split(_,Left0,Right0), M, D) :-
1558 1559 1560 domain_contract_(Left0, M, Left),
1561 domain_contract_(Right0, M, Right),
1562 domains_union(Left, Right, D).
1563
1568
1569domain_contract_less(D0, M, Op, D) :-
1570 ( M < 0 -> domain_negate(D0, D1), M1 is abs(M)
1571 ; D1 = D0, M1 = M
1572 ),
1573 domain_contract_less_(D1, M1, Op, D).
1574
1575domain_contract_less_(empty, _, _, empty).
1576domain_contract_less_(from_to(From0, To0), M, Op, from_to(From,To)) :-
1577 ( Op = div -> From cis From0 div n(M),
1578 To cis To0 div n(M)
1579 ; Op = // -> From cis From0 // n(M),
1580 To cis To0 // n(M)
1581 ).
1582
1583domain_contract_less_(split(_,Left0,Right0), M, Op, D) :-
1584 1585 1586 domain_contract_less_(Left0, M, Op, Left),
1587 domain_contract_less_(Right0, M, Op, Right),
1588 domains_union(Left, Right, D).
1589
1593
1594domain_negate(empty, empty).
1595domain_negate(from_to(From0, To0), from_to(From, To)) :-
1596 From cis -To0, To cis -From0.
1597domain_negate(split(S0, Left0, Right0), split(S, Left, Right)) :-
1598 S is -S0,
1599 domain_negate(Left0, Right),
1600 domain_negate(Right0, Left).
1601
1605
1606list_to_disjoint_intervals([], []).
1607list_to_disjoint_intervals([N|Ns], Is) :-
1608 list_to_disjoint_intervals(Ns, N, N, Is).
1609
1610list_to_disjoint_intervals([], M, N, [n(M)-n(N)]).
1611list_to_disjoint_intervals([B|Bs], M, N, Is) :-
1612 ( B =:= N + 1 ->
1613 list_to_disjoint_intervals(Bs, M, B, Is)
1614 ; Is = [n(M)-n(N)|Rest],
1615 list_to_disjoint_intervals(Bs, B, B, Rest)
1616 ).
1617
1618list_to_domain(List0, D) :-
1619 ( List0 == [] -> D = empty
1620 ; sort(List0, List),
1621 list_to_disjoint_intervals(List, Is),
1622 intervals_to_domain(Is, D)
1623 ).
1624
1625intervals_to_domain([], empty) :- !.
1626intervals_to_domain([M-N], from_to(M,N)) :- !.
1627intervals_to_domain(Is, D) :-
1628 length(Is, L),
1629 FL is L // 2,
1630 length(Front, FL),
1631 append(Front, Tail, Is),
1632 Tail = [n(Start)-_|_],
1633 Hole is Start - 1,
1634 intervals_to_domain(Front, Left),
1635 intervals_to_domain(Tail, Right),
1636 D = split(Hole, Left, Right).
1637
1639
1640
1654
1655Var in Dom :- clpfd_in(Var, Dom).
1656
1657clpfd_in(V, D) :-
1658 fd_variable(V),
1659 drep_to_domain(D, Dom),
1660 domain(V, Dom).
1661
1662fd_variable(V) :-
1663 ( var(V) -> true
1664 ; integer(V) -> true
1665 ; type_error(integer, V)
1666 ).
1667
1672
1673Vs ins D :-
1674 fd_must_be_list(Vs),
1675 maplist(fd_variable, Vs),
1676 drep_to_domain(D, Dom),
1677 domains(Vs, Dom).
1678
1679fd_must_be_list(Ls) :-
1680 ( fd_var(Ls) -> type_error(list, Ls)
1681 ; must_be(list, Ls)
1682 ).
1683
1688
1689indomain(Var) :- label([Var]).
1690
1691order_dom_next(up, Dom, Next) :- domain_infimum(Dom, n(Next)).
1692order_dom_next(down, Dom, Next) :- domain_supremum(Dom, n(Next)).
1693order_dom_next(random_value(_), Dom, Next) :-
1694 phrase(domain_to_intervals(Dom), Is),
1695 length(Is, L),
1696 R is random(L),
1697 nth0(R, Is, From-To),
1698 random_between(From, To, Next).
1699
1700domain_to_intervals(from_to(n(From),n(To))) --> [From-To].
1701domain_to_intervals(split(_, Left, Right)) -->
1702 domain_to_intervals(Left),
1703 domain_to_intervals(Right).
1704
1708
1709label(Vs) :- labeling([], Vs).
1710
1795
1796labeling(Options, Vars) :-
1797 must_be(list, Options),
1798 fd_must_be_list(Vars),
1799 maplist(must_be_finite_fdvar, Vars),
1800 label(Options, Options, default(leftmost), default(up), default(step), [], upto_ground, Vars).
1801
1802finite_domain(Dom) :-
1803 domain_infimum(Dom, n(_)),
1804 domain_supremum(Dom, n(_)).
1805
1806must_be_finite_fdvar(Var) :-
1807 ( fd_get(Var, Dom, _) ->
1808 ( finite_domain(Dom) -> true
1809 ; instantiation_error(Var)
1810 )
1811 ; integer(Var) -> true
1812 ; must_be(integer, Var)
1813 ).
1814
1815
1816label([O|Os], Options, Selection, Order, Choice, Optim, Consistency, Vars) :-
1817 ( var(O)-> instantiation_error(O)
1818 ; override(selection, Selection, O, Options, S1) ->
1819 label(Os, Options, S1, Order, Choice, Optim, Consistency, Vars)
1820 ; override(order, Order, O, Options, O1) ->
1821 label(Os, Options, Selection, O1, Choice, Optim, Consistency, Vars)
1822 ; override(choice, Choice, O, Options, C1) ->
1823 label(Os, Options, Selection, Order, C1, Optim, Consistency, Vars)
1824 ; optimisation(O) ->
1825 label(Os, Options, Selection, Order, Choice, [O|Optim], Consistency, Vars)
1826 ; consistency(O, O1) ->
1827 label(Os, Options, Selection, Order, Choice, Optim, O1, Vars)
1828 ; domain_error(labeling_option, O)
1829 ).
1830label([], _, Selection, Order, Choice, Optim0, Consistency, Vars) :-
1831 maplist(arg(1), [Selection,Order,Choice], [S,O,C]),
1832 ( Optim0 == [] ->
1833 label(Vars, S, O, C, Consistency)
1834 ; reverse(Optim0, Optim),
1835 exprs_singlevars(Optim, SVs),
1836 optimise(Vars, [S,O,C], SVs)
1837 ).
1838
1841
1842exprs_singlevars([], []).
1843exprs_singlevars([E|Es], [SV|SVs]) :-
1844 E =.. [F,Expr],
1845 ?(Single) #= Expr,
1846 SV =.. [F,Single],
1847 exprs_singlevars(Es, SVs).
1848
1849all_dead(fd_props(Bs,Gs,Os)) :-
1850 all_dead_(Bs),
1851 all_dead_(Gs),
1852 all_dead_(Os).
1853
1854all_dead_([]).
1855all_dead_([propagator(_, S)|Ps]) :- S == dead, all_dead_(Ps).
1856
1857label([], _, _, _, Consistency) :- !,
1858 ( Consistency = upto_in(I0,I) -> I0 = I
1859 ; true
1860 ).
1861label(Vars, Selection, Order, Choice, Consistency) :-
1862 ( Vars = [V|Vs], nonvar(V) -> label(Vs, Selection, Order, Choice, Consistency)
1863 ; select_var(Selection, Vars, Var, RVars),
1864 ( var(Var) ->
1865 ( Consistency = upto_in(I0,I), fd_get(Var, _, Ps), all_dead(Ps) ->
1866 fd_size(Var, Size),
1867 I1 is I0*Size,
1868 label(RVars, Selection, Order, Choice, upto_in(I1,I))
1869 ; Consistency = upto_in, fd_get(Var, _, Ps), all_dead(Ps) ->
1870 label(RVars, Selection, Order, Choice, Consistency)
1871 ; choice_order_variable(Choice, Order, Var, RVars, Vars, Selection, Consistency)
1872 )
1873 ; label(RVars, Selection, Order, Choice, Consistency)
1874 )
1875 ).
1876
1877choice_order_variable(step, Order, Var, Vars, Vars0, Selection, Consistency) :-
1878 fd_get(Var, Dom, _),
1879 order_dom_next(Order, Dom, Next),
1880 ( Var = Next,
1881 label(Vars, Selection, Order, step, Consistency)
1882 ; neq_num(Var, Next),
1883 do_queue,
1884 label(Vars0, Selection, Order, step, Consistency)
1885 ).
1886choice_order_variable(enum, Order, Var, Vars, _, Selection, Consistency) :-
1887 fd_get(Var, Dom0, _),
1888 domain_direction_element(Dom0, Order, Var),
1889 label(Vars, Selection, Order, enum, Consistency).
1890choice_order_variable(bisect, Order, Var, _, Vars0, Selection, Consistency) :-
1891 fd_get(Var, Dom, _),
1892 domain_infimum(Dom, n(I)),
1893 domain_supremum(Dom, n(S)),
1894 Mid0 is (I + S) // 2,
1895 ( Mid0 =:= S -> Mid is Mid0 - 1 ; Mid = Mid0 ),
1896 ( Order == up -> ( Var #=< Mid ; Var #> Mid )
1897 ; Order == down -> ( Var #> Mid ; Var #=< Mid )
1898 ; domain_error(bisect_up_or_down, Order)
1899 ),
1900 label(Vars0, Selection, Order, bisect, Consistency).
1901
1902override(What, Prev, Value, Options, Result) :-
1903 call(What, Value),
1904 override_(Prev, Value, Options, Result).
1905
1906override_(default(_), Value, _, user(Value)).
1907override_(user(Prev), Value, Options, _) :-
1908 ( Value == Prev ->
1909 domain_error(nonrepeating_labeling_options, Options)
1910 ; domain_error(consistent_labeling_options, Options)
1911 ).
1912
1913selection(ff).
1914selection(ffc).
1915selection(min).
1916selection(max).
1917selection(leftmost).
1918selection(random_variable(Seed)) :-
1919 must_be(integer, Seed),
1920 set_random(seed(Seed)).
1921
1922choice(step).
1923choice(enum).
1924choice(bisect).
1925
1926order(up).
1927order(down).
1930order(random_value(Seed)) :-
1931 must_be(integer, Seed),
1932 set_random(seed(Seed)).
1933
1934consistency(upto_in(I), upto_in(1, I)).
1935consistency(upto_in, upto_in).
1936consistency(upto_ground, upto_ground).
1937
1938optimisation(min(_)).
1939optimisation(max(_)).
1940
1941select_var(leftmost, [Var|Vars], Var, Vars).
1942select_var(min, [V|Vs], Var, RVars) :-
1943 find_min(Vs, V, Var),
1944 delete_eq([V|Vs], Var, RVars).
1945select_var(max, [V|Vs], Var, RVars) :-
1946 find_max(Vs, V, Var),
1947 delete_eq([V|Vs], Var, RVars).
1948select_var(ff, [V|Vs], Var, RVars) :-
1949 fd_size_(V, n(S)),
1950 find_ff(Vs, V, S, Var),
1951 delete_eq([V|Vs], Var, RVars).
1952select_var(ffc, [V|Vs], Var, RVars) :-
1953 find_ffc(Vs, V, Var),
1954 delete_eq([V|Vs], Var, RVars).
1955select_var(random_variable(_), Vars0, Var, Vars) :-
1956 length(Vars0, L),
1957 I is random(L),
1958 nth0(I, Vars0, Var),
1959 delete_eq(Vars0, Var, Vars).
1960
1961find_min([], Var, Var).
1962find_min([V|Vs], CM, Min) :-
1963 ( min_lt(V, CM) ->
1964 find_min(Vs, V, Min)
1965 ; find_min(Vs, CM, Min)
1966 ).
1967
1968find_max([], Var, Var).
1969find_max([V|Vs], CM, Max) :-
1970 ( max_gt(V, CM) ->
1971 find_max(Vs, V, Max)
1972 ; find_max(Vs, CM, Max)
1973 ).
1974
1975find_ff([], Var, _, Var).
1976find_ff([V|Vs], CM, S0, FF) :-
1977 ( nonvar(V) -> find_ff(Vs, CM, S0, FF)
1978 ; ( fd_size_(V, n(S1)), S1 < S0 ->
1979 find_ff(Vs, V, S1, FF)
1980 ; find_ff(Vs, CM, S0, FF)
1981 )
1982 ).
1983
1984find_ffc([], Var, Var).
1985find_ffc([V|Vs], Prev, FFC) :-
1986 ( ffc_lt(V, Prev) ->
1987 find_ffc(Vs, V, FFC)
1988 ; find_ffc(Vs, Prev, FFC)
1989 ).
1990
1991
1992ffc_lt(X, Y) :-
1993 ( fd_get(X, XD, XPs) ->
1994 domain_num_elements(XD, n(NXD))
1995 ; NXD = 1, XPs = []
1996 ),
1997 ( fd_get(Y, YD, YPs) ->
1998 domain_num_elements(YD, n(NYD))
1999 ; NYD = 1, YPs = []
2000 ),
2001 ( NXD < NYD -> true
2002 ; NXD =:= NYD,
2003 props_number(XPs, NXPs),
2004 props_number(YPs, NYPs),
2005 NXPs > NYPs
2006 ).
2007
2008min_lt(X,Y) :- bounds(X,LX,_), bounds(Y,LY,_), LX < LY.
2009
2010max_gt(X,Y) :- bounds(X,_,UX), bounds(Y,_,UY), UX > UY.
2011
2012bounds(X, L, U) :-
2013 ( fd_get(X, Dom, _) ->
2014 domain_infimum(Dom, n(L)),
2015 domain_supremum(Dom, n(U))
2016 ; L = X, U = L
2017 ).
2018
2019delete_eq([], _, []).
2020delete_eq([X|Xs], Y, List) :-
2021 ( nonvar(X) -> delete_eq(Xs, Y, List)
2022 ; X == Y -> List = Xs
2023 ; List = [X|Tail],
2024 delete_eq(Xs, Y, Tail)
2025 ).
2026
2032
2033contracting(Vs) :-
2034 must_be(list, Vs),
2035 maplist(must_be_finite_fdvar, Vs),
2036 contracting(Vs, false, Vs).
2037
2038contracting([], Repeat, Vars) :-
2039 ( Repeat -> contracting(Vars, false, Vars)
2040 ; true
2041 ).
2042contracting([V|Vs], Repeat, Vars) :-
2043 fd_inf(V, Min),
2044 ( \+ \+ (V = Min) ->
2045 fd_sup(V, Max),
2046 ( \+ \+ (V = Max) ->
2047 contracting(Vs, Repeat, Vars)
2048 ; V #\= Max,
2049 contracting(Vs, true, Vars)
2050 )
2051 ; V #\= Min,
2052 contracting(Vs, true, Vars)
2053 ).
2054
2061
2062fds_sespsize(Vs, S) :-
2063 must_be(list, Vs),
2064 maplist(fd_variable, Vs),
2065 fds_sespsize(Vs, n(1), S1),
2066 bound_portray(S1, S).
2067
2068fd_size_(V, S) :-
2069 ( fd_get(V, D, _) ->
2070 domain_num_elements(D, S)
2071 ; S = n(1)
2072 ).
2073
2074fds_sespsize([], S, S).
2075fds_sespsize([V|Vs], S0, S) :-
2076 fd_size_(V, S1),
2077 S2 cis S0*S1,
2078 fds_sespsize(Vs, S2, S).
2079
2092
2093optimise(Vars, Options, Whats) :-
2094 Whats = [What|WhatsRest],
2095 Extremum = extremum(none),
2096 ( catch(store_extremum(Vars, Options, What, Extremum),
2097 time_limit_exceeded,
2098 false)
2099 ; Extremum = extremum(n(Val)),
2100 arg(1, What, Expr),
2101 append(WhatsRest, Options, Options1),
2102 ( Expr #= Val,
2103 labeling(Options1, Vars)
2104 ; Expr #\= Val,
2105 optimise(Vars, Options, Whats)
2106 )
2107 ).
2108
2109store_extremum(Vars, Options, What, Extremum) :-
2110 catch((labeling(Options, Vars), throw(w(What))), w(What1), true),
2111 functor(What, Direction, _),
2112 maplist(arg(1), [What,What1], [Expr,Expr1]),
2113 optimise(Direction, Options, Vars, Expr1, Expr, Extremum).
2114
2115optimise(Direction, Options, Vars, Expr0, Expr, Extremum) :-
2116 must_be(ground, Expr0),
2117 nb_setarg(1, Extremum, n(Expr0)),
2118 catch((tighten(Direction, Expr, Expr0),
2119 labeling(Options, Vars),
2120 throw(v(Expr))), v(Expr1), true),
2121 optimise(Direction, Options, Vars, Expr1, Expr, Extremum).
2122
2123tighten(min, E, V) :- E #< V.
2124tighten(max, E, V) :- E #> V.
2125
2127
2133
2134all_different(Ls) :-
2135 fd_must_be_list(Ls),
2136 maplist(fd_variable, Ls),
2137 Orig = original_goal(_, all_different(Ls)),
2138 all_different(Ls, [], Orig),
2139 do_queue.
2140
2141all_different([], _, _).
2142all_different([X|Right], Left, Orig) :-
2143 ( var(X) ->
2144 make_propagator(pdifferent(Left,Right,X,Orig), Prop),
2145 init_propagator(X, Prop),
2146 trigger_prop(Prop)
2147 ; exclude_fire(Left, Right, X)
2148 ),
2149 all_different(Right, [X|Left], Orig).
2150
2163
2164all_distinct(Ls) :-
2165 fd_must_be_list(Ls),
2166 maplist(fd_variable, Ls),
2167 make_propagator(pdistinct(Ls), Prop),
2168 distinct_attach(Ls, Prop, []),
2169 trigger_once(Prop).
2170
2183
2184sum(Vs, Op, Value) :-
2185 must_be(list, Vs),
2186 same_length(Vs, Ones),
2187 maplist(=(1), Ones),
2188 scalar_product(Ones, Vs, Op, Value).
2189
2195
2196scalar_product(Cs, Vs, Op, Value) :-
2197 must_be(list(integer), Cs),
2198 must_be(list, Vs),
2199 maplist(fd_variable, Vs),
2200 ( Op = (#=), single_value(Value, Right), ground(Vs) ->
2201 foldl(coeff_int_linsum, Cs, Vs, 0, Right)
2202 ; must_be(callable, Op),
2203 ( memberchk(Op, [#=,#\=,#<,#>,#=<,#>=]) -> true
2204 ; domain_error(scalar_product_relation, Op)
2205 ),
2206 must_be(acyclic, Value),
2207 foldl(coeff_var_plusterm, Cs, Vs, 0, Left),
2208 ( left_right_linsum_const(Left, Value, Cs1, Vs1, Const) ->
2209 scalar_product_(Op, Cs1, Vs1, Const)
2210 ; sum(Cs, Vs, 0, Op, Value)
2211 )
2212 ).
2213
2214single_value(V, V) :- var(V), !, non_monotonic(V).
2215single_value(V, V) :- integer(V).
2216single_value(?(V), V) :- fd_variable(V).
2217
2218coeff_var_plusterm(C, V, T0, T0+(C* ?(V))).
2219
2220coeff_int_linsum(C, I, S0, S) :- S is S0 + C*I.
2221
2222sum([], _, Sum, Op, Value) :- call(Op, Sum, Value).
2223sum([C|Cs], [X|Xs], Acc, Op, Value) :-
2224 ?(NAcc) #= Acc + C* ?(X),
2225 sum(Cs, Xs, NAcc, Op, Value).
2226
2227multiples([], [], _).
2228multiples([C|Cs], [V|Vs], Left) :-
2229 ( ( Cs = [N|_] ; Left = [N|_] ) ->
2230 ( N =\= 1, gcd(C,N) =:= 1 ->
2231 gcd(Cs, N, GCD0),
2232 gcd(Left, GCD0, GCD),
2233 ( GCD > 1 -> ?(V) #= GCD * ?(_)
2234 ; true
2235 )
2236 ; true
2237 )
2238 ; true
2239 ),
2240 multiples(Cs, Vs, [C|Left]).
2241
2242abs(N, A) :- A is abs(N).
2243
2244divide(D, N, R) :- R is N // D.
2245
2246scalar_product_(#=, Cs0, Vs, S0) :-
2247 ( Cs0 = [C|Rest] ->
2248 gcd(Rest, C, GCD),
2249 S0 mod GCD =:= 0,
2250 maplist(divide(GCD), [S0|Cs0], [S|Cs])
2251 ; S0 =:= 0, S = S0, Cs = Cs0
2252 ),
2253 ( S0 =:= 0 ->
2254 maplist(abs, Cs, As),
2255 multiples(As, Vs, [])
2256 ; true
2257 ),
2258 propagator_init_trigger(Vs, scalar_product_eq(Cs, Vs, S)).
2259scalar_product_(#\=, Cs, Vs, C) :-
2260 propagator_init_trigger(Vs, scalar_product_neq(Cs, Vs, C)).
2261scalar_product_(#=<, Cs, Vs, C) :-
2262 propagator_init_trigger(Vs, scalar_product_leq(Cs, Vs, C)).
2263scalar_product_(#<, Cs, Vs, C) :-
2264 C1 is C - 1,
2265 scalar_product_(#=<, Cs, Vs, C1).
2266scalar_product_(#>, Cs, Vs, C) :-
2267 C1 is C + 1,
2268 scalar_product_(#>=, Cs, Vs, C1).
2269scalar_product_(#>=, Cs, Vs, C) :-
2270 maplist(negative, Cs, Cs1),
2271 C1 is -C,
2272 scalar_product_(#=<, Cs1, Vs, C1).
2273
2274negative(X0, X) :- X is -X0.
2275
2276coeffs_variables_const([], [], [], [], I, I).
2277coeffs_variables_const([C|Cs], [V|Vs], Cs1, Vs1, I0, I) :-
2278 ( var(V) ->
2279 Cs1 = [C|CRest], Vs1 = [V|VRest], I1 = I0
2280 ; I1 is I0 + C*V,
2281 Cs1 = CRest, Vs1 = VRest
2282 ),
2283 coeffs_variables_const(Cs, Vs, CRest, VRest, I1, I).
2284
2285sum_finite_domains([], [], [], [], Inf, Sup, Inf, Sup).
2286sum_finite_domains([C|Cs], [V|Vs], Infs, Sups, Inf0, Sup0, Inf, Sup) :-
2287 fd_get(V, _, Inf1, Sup1, _),
2288 ( Inf1 = n(NInf) ->
2289 ( C < 0 ->
2290 Sup2 is Sup0 + C*NInf
2291 ; Inf2 is Inf0 + C*NInf
2292 ),
2293 Sups = Sups1,
2294 Infs = Infs1
2295 ; ( C < 0 ->
2296 Sup2 = Sup0,
2297 Sups = [C*V|Sups1],
2298 Infs = Infs1
2299 ; Inf2 = Inf0,
2300 Infs = [C*V|Infs1],
2301 Sups = Sups1
2302 )
2303 ),
2304 ( Sup1 = n(NSup) ->
2305 ( C < 0 ->
2306 Inf2 is Inf0 + C*NSup
2307 ; Sup2 is Sup0 + C*NSup
2308 ),
2309 Sups1 = Sups2,
2310 Infs1 = Infs2
2311 ; ( C < 0 ->
2312 Inf2 = Inf0,
2313 Infs1 = [C*V|Infs2],
2314 Sups1 = Sups2
2315 ; Sup2 = Sup0,
2316 Sups1 = [C*V|Sups2],
2317 Infs1 = Infs2
2318 )
2319 ),
2320 sum_finite_domains(Cs, Vs, Infs2, Sups2, Inf2, Sup2, Inf, Sup).
2321
2322remove_dist_upper_lower([], _, _, _).
2323remove_dist_upper_lower([C|Cs], [V|Vs], D1, D2) :-
2324 ( fd_get(V, VD, VPs) ->
2325 ( C < 0 ->
2326 domain_supremum(VD, n(Sup)),
2327 L is Sup + D1//C,
2328 domain_remove_smaller_than(VD, L, VD1),
2329 domain_infimum(VD1, n(Inf)),
2330 G is Inf - D2//C,
2331 domain_remove_greater_than(VD1, G, VD2)
2332 ; domain_infimum(VD, n(Inf)),
2333 G is Inf + D1//C,
2334 domain_remove_greater_than(VD, G, VD1),
2335 domain_supremum(VD1, n(Sup)),
2336 L is Sup - D2//C,
2337 domain_remove_smaller_than(VD1, L, VD2)
2338 ),
2339 fd_put(V, VD2, VPs)
2340 ; true
2341 ),
2342 remove_dist_upper_lower(Cs, Vs, D1, D2).
2343
2344
2345remove_dist_upper_leq([], _, _).
2346remove_dist_upper_leq([C|Cs], [V|Vs], D1) :-
2347 ( fd_get(V, VD, VPs) ->
2348 ( C < 0 ->
2349 domain_supremum(VD, n(Sup)),
2350 L is Sup + D1//C,
2351 domain_remove_smaller_than(VD, L, VD1)
2352 ; domain_infimum(VD, n(Inf)),
2353 G is Inf + D1//C,
2354 domain_remove_greater_than(VD, G, VD1)
2355 ),
2356 fd_put(V, VD1, VPs)
2357 ; true
2358 ),
2359 remove_dist_upper_leq(Cs, Vs, D1).
2360
2361
2362remove_dist_upper([], _).
2363remove_dist_upper([C*V|CVs], D) :-
2364 ( fd_get(V, VD, VPs) ->
2365 ( C < 0 ->
2366 ( domain_supremum(VD, n(Sup)) ->
2367 L is Sup + D//C,
2368 domain_remove_smaller_than(VD, L, VD1)
2369 ; VD1 = VD
2370 )
2371 ; ( domain_infimum(VD, n(Inf)) ->
2372 G is Inf + D//C,
2373 domain_remove_greater_than(VD, G, VD1)
2374 ; VD1 = VD
2375 )
2376 ),
2377 fd_put(V, VD1, VPs)
2378 ; true
2379 ),
2380 remove_dist_upper(CVs, D).
2381
2382remove_dist_lower([], _).
2383remove_dist_lower([C*V|CVs], D) :-
2384 ( fd_get(V, VD, VPs) ->
2385 ( C < 0 ->
2386 ( domain_infimum(VD, n(Inf)) ->
2387 G is Inf - D//C,
2388 domain_remove_greater_than(VD, G, VD1)
2389 ; VD1 = VD
2390 )
2391 ; ( domain_supremum(VD, n(Sup)) ->
2392 L is Sup - D//C,
2393 domain_remove_smaller_than(VD, L, VD1)
2394 ; VD1 = VD
2395 )
2396 ),
2397 fd_put(V, VD1, VPs)
2398 ; true
2399 ),
2400 remove_dist_lower(CVs, D).
2401
2402remove_upper([], _).
2403remove_upper([C*X|CXs], Max) :-
2404 ( fd_get(X, XD, XPs) ->
2405 D is Max//C,
2406 ( C < 0 ->
2407 domain_remove_smaller_than(XD, D, XD1)
2408 ; domain_remove_greater_than(XD, D, XD1)
2409 ),
2410 fd_put(X, XD1, XPs)
2411 ; true
2412 ),
2413 remove_upper(CXs, Max).
2414
2415remove_lower([], _).
2416remove_lower([C*X|CXs], Min) :-
2417 ( fd_get(X, XD, XPs) ->
2418 D is -Min//C,
2419 ( C < 0 ->
2420 domain_remove_greater_than(XD, D, XD1)
2421 ; domain_remove_smaller_than(XD, D, XD1)
2422 ),
2423 fd_put(X, XD1, XPs)
2424 ; true
2425 ),
2426 remove_lower(CXs, Min).
2427
2429
2438
2440
2441make_queue :- nb_setval('$clpfd_queue', fast_slow([], [])).
2442
2443push_queue(E, Which) :-
2444 nb_getval('$clpfd_queue', Qs),
2445 arg(Which, Qs, Q),
2446 ( Q == [] ->
2447 setarg(Which, Qs, [E|T]-T)
2448 ; Q = H-[E|T],
2449 setarg(Which, Qs, H-T)
2450 ).
2451
2452pop_queue(E) :-
2453 nb_getval('$clpfd_queue', Qs),
2454 ( pop_queue(E, Qs, 1) -> true
2455 ; pop_queue(E, Qs, 2)
2456 ).
2457
2458pop_queue(E, Qs, Which) :-
2459 arg(Which, Qs, [E|NH]-T),
2460 ( var(NH) ->
2461 setarg(Which, Qs, [])
2462 ; setarg(Which, Qs, NH-T)
2463 ).
2464
2465fetch_propagator(Prop) :-
2466 pop_queue(P),
2467 ( propagator_state(P, S), S == dead -> fetch_propagator(Prop)
2468 ; Prop = P
2469 ).
2470
2477
2478constrain_to_integer(Var) :-
2479 ( integer(Var) -> true
2480 ; fd_get(Var, D, Ps),
2481 fd_put(Var, D, Ps)
2482 ).
2483
2484power_var_num(P, X, N) :-
2485 ( var(P) -> X = P, N = 1
2486 ; P = Left*Right,
2487 power_var_num(Left, XL, L),
2488 power_var_num(Right, XR, R),
2489 XL == XR,
2490 X = XL,
2491 N is L + R
2492 ).
2493
2503
2504:- op(800, xfx, =>). 2505
2506parse_clpfd(E, R,
2507 [g(cyclic_term(E)) => [g(domain_error(clpfd_expression, E))],
2508 g(var(E)) => [g(non_monotonic(E)),
2509 g(constrain_to_integer(E)), g(E = R)],
2510 g(integer(E)) => [g(R = E)],
2511 ?(E) => [g(must_be_fd_integer(E)), g(R = E)],
2512 #(E) => [g(must_be_fd_integer(E)), g(R = E)],
2513 m(A+B) => [p(pplus(A, B, R))],
2514 2515 g(power_var_num(E, V, N)) => [p(pexp(V, N, R))],
2516 m(A*B) => [p(ptimes(A, B, R))],
2517 m(A-B) => [p(pplus(R,B,A))],
2518 m(-A) => [p(ptimes(-1,A,R))],
2519 m(max(A,B)) => [g(A #=< ?(R)), g(B #=< R), p(pmax(A, B, R))],
2520 m(min(A,B)) => [g(A #>= ?(R)), g(B #>= R), p(pmin(A, B, R))],
2521 m(A mod B) => [g(B #\= 0), p(pmod(A, B, R))],
2522 m(A rem B) => [g(B #\= 0), p(prem(A, B, R))],
2523 m(abs(A)) => [g(?(R) #>= 0), p(pabs(A, R))],
2525 m(A//B) => [g(B #\= 0), p(ptzdiv(A, B, R))],
2526 m(A div B) => [g(B #\= 0), p(pdiv(A, B, R))],
2527 m(A rdiv B) => [g(B #\= 0), p(prdiv(A, B, R))],
2528 m(A^B) => [p(pexp(A, B, R))],
2529 2530 m(\A) => [p(pfunction(\, A, R))],
2531 m(msb(A)) => [p(pfunction(msb, A, R))],
2532 m(lsb(A)) => [p(pfunction(lsb, A, R))],
2533 m(popcount(A)) => [p(pfunction(popcount, A, R))],
2534 m(A<<B) => [p(pshift(A, B, R, 1))],
2535 m(A>>B) => [p(pshift(A, B, R, -1))],
2536 m(A/\B) => [p(pfunction(/\, A, B, R))],
2537 m(A\/B) => [p(pfunction(\/, A, B, R))],
2538 m(A xor B) => [p(pfunction(xor, A, B, R))],
2539 g(true) => [g(domain_error(clpfd_expression, E))]
2540 ]).
2541
2542non_monotonic(X) :-
2543 ( \+ fd_var(X), current_prolog_flag(clpfd_monotonic, true) ->
2544 instantiation_error(X)
2545 ; true
2546 ).
2547
2550
2551make_parse_clpfd(Clauses) :-
2552 parse_clpfd_clauses(Clauses0),
2553 maplist(goals_goal, Clauses0, Clauses).
2554
2555goals_goal((Head :- Goals), (Head :- Body)) :-
2556 list_goal(Goals, Body).
2557
2558parse_clpfd_clauses(Clauses) :-
2559 parse_clpfd(E, R, Matchers),
2560 maplist(parse_matcher(E, R), Matchers, Clauses).
2561
2562parse_matcher(E, R, Matcher, Clause) :-
2563 Matcher = (Condition0 => Goals0),
2564 phrase((parse_condition(Condition0, E, Head),
2565 parse_goals(Goals0)), Goals),
2566 Clause = (parse_clpfd(Head, R) :- Goals).
2567
2568parse_condition(g(Goal), E, E) --> [Goal, !].
2569parse_condition(?(E), _, ?(E)) --> [!].
2570parse_condition(#(E), _, #(E)) --> [!].
2571parse_condition(m(Match), _, Match0) -->
2572 [!],
2573 { copy_term(Match, Match0),
2574 term_variables(Match0, Vs0),
2575 term_variables(Match, Vs)
2576 },
2577 parse_match_variables(Vs0, Vs).
2578
2579parse_match_variables([], []) --> [].
2580parse_match_variables([V0|Vs0], [V|Vs]) -->
2581 [parse_clpfd(V0, V)],
2582 parse_match_variables(Vs0, Vs).
2583
2584parse_goals([]) --> [].
2585parse_goals([G|Gs]) --> parse_goal(G), parse_goals(Gs).
2586
2587parse_goal(g(Goal)) --> [Goal].
2588parse_goal(p(Prop)) -->
2589 [make_propagator(Prop, P)],
2590 { term_variables(Prop, Vs) },
2591 parse_init(Vs, P),
2592 [trigger_once(P)].
2593
2594parse_init([], _) --> [].
2595parse_init([V|Vs], P) --> [init_propagator(V, P)], parse_init(Vs, P).
2596
2599
2600
2603
2604trigger_once(Prop) :- trigger_prop(Prop), do_queue.
2605
2606neq(A, B) :- propagator_init_trigger(pneq(A, B)).
2607
2608propagator_init_trigger(P) -->
2609 { term_variables(P, Vs) },
2610 propagator_init_trigger(Vs, P).
2611
2612propagator_init_trigger(Vs, P) -->
2613 [p(Prop)],
2614 { make_propagator(P, Prop),
2615 maplist(prop_init(Prop), Vs),
2616 trigger_once(Prop) }.
2617
2618propagator_init_trigger(P) :-
2619 phrase(propagator_init_trigger(P), _).
2620
2621propagator_init_trigger(Vs, P) :-
2622 phrase(propagator_init_trigger(Vs, P), _).
2623
2624prop_init(Prop, V) :- init_propagator(V, Prop).
2625
2626geq(A, B) :-
2627 ( fd_get(A, AD, APs) ->
2628 domain_infimum(AD, AI),
2629 ( fd_get(B, BD, _) ->
2630 domain_supremum(BD, BS),
2631 ( AI cis_geq BS -> true
2632 ; propagator_init_trigger(pgeq(A,B))
2633 )
2634 ; ( AI cis_geq n(B) -> true
2635 ; domain_remove_smaller_than(AD, B, AD1),
2636 fd_put(A, AD1, APs),
2637 do_queue
2638 )
2639 )
2640 ; fd_get(B, BD, BPs) ->
2641 domain_remove_greater_than(BD, A, BD1),
2642 fd_put(B, BD1, BPs),
2643 do_queue
2644 ; A >= B
2645 ).
2646
2671
2672match_expand(#>=, clpfd_geq_).
2673match_expand(#=, clpfd_equal_).
2674match_expand(#\=, clpfd_neq).
2675
2676symmetric(#=).
2677symmetric(#\=).
2678
2679matches([
2680 m_c(any(X) #>= any(Y), left_right_linsum_const(X, Y, Cs, Vs, Const)) =>
2681 [g(( Cs = [1], Vs = [A] -> geq(A, Const)
2682 ; Cs = [-1], Vs = [A] -> Const1 is -Const, geq(Const1, A)
2683 ; Cs = [1,1], Vs = [A,B] -> ?(A) + ?(B) #= ?(S), geq(S, Const)
2684 ; Cs = [1,-1], Vs = [A,B] ->
2685 ( Const =:= 0 -> geq(A, B)
2686 ; C1 is -Const,
2687 propagator_init_trigger(x_leq_y_plus_c(B, A, C1))
2688 )
2689 ; Cs = [-1,1], Vs = [A,B] ->
2690 ( Const =:= 0 -> geq(B, A)
2691 ; C1 is -Const,
2692 propagator_init_trigger(x_leq_y_plus_c(A, B, C1))
2693 )
2694 ; Cs = [-1,-1], Vs = [A,B] ->
2695 ?(A) + ?(B) #= ?(S), Const1 is -Const, geq(Const1, S)
2696 ; scalar_product_(#>=, Cs, Vs, Const)
2697 ))],
2698 m(any(X) - any(Y) #>= integer(C)) => [d(X, X1), d(Y, Y1), g(C1 is -C), p(x_leq_y_plus_c(Y1, X1, C1))],
2699 m(integer(X) #>= any(Z) + integer(A)) => [g(C is X - A), r(C, Z)],
2700 m(abs(any(X)-any(Y)) #>= integer(I)) => [d(X, X1), d(Y, Y1), p(absdiff_geq(X1, Y1, I))],
2701 m(abs(any(X)) #>= integer(I)) => [d(X, RX), g((I>0 -> I1 is -I, RX in inf..I1 \/ I..sup; true))],
2702 m(integer(I) #>= abs(any(X))) => [d(X, RX), g(I>=0), g(I1 is -I), g(RX in I1..I)],
2703 m(any(X) #>= any(Y)) => [d(X, RX), d(Y, RY), g(geq(RX, RY))],
2704
2705 2706 2707
2708 m(var(X) #= var(Y)) => [g(constrain_to_integer(X)), g(X=Y)],
2709 m(var(X) #= var(Y)+var(Z)) => [p(pplus(Y,Z,X))],
2710 m(var(X) #= var(Y)-var(Z)) => [p(pplus(X,Z,Y))],
2711 m(var(X) #= var(Y)*var(Z)) => [p(ptimes(Y,Z,X))],
2712 m(var(X) #= -var(Z)) => [p(ptimes(-1, Z, X))],
2713 m_c(any(X) #= any(Y), left_right_linsum_const(X, Y, Cs, Vs, S)) =>
2714 [g(scalar_product_(#=, Cs, Vs, S))],
2715 m(var(X) #= any(Y)) => [d(Y,X)],
2716 m(any(X) #= any(Y)) => [d(X, RX), d(Y, RX)],
2717
2718 2719 2720
2721 m(var(X) #\= integer(Y)) => [g(neq_num(X, Y))],
2722 m(var(X) #\= var(Y)) => [g(neq(X,Y))],
2723 m(var(X) #\= var(Y) + var(Z)) => [p(x_neq_y_plus_z(X, Y, Z))],
2724 m(var(X) #\= var(Y) - var(Z)) => [p(x_neq_y_plus_z(Y, X, Z))],
2725 m(var(X) #\= var(Y)*var(Z)) => [p(ptimes(Y,Z,P)), g(neq(X,P))],
2726 m(integer(X) #\= abs(any(Y)-any(Z))) => [d(Y, Y1), d(Z, Z1), p(absdiff_neq(Y1, Z1, X))],
2727 m_c(any(X) #\= any(Y), left_right_linsum_const(X, Y, Cs, Vs, S)) =>
2728 [g(scalar_product_(#\=, Cs, Vs, S))],
2729 m(any(X) #\= any(Y) + any(Z)) => [d(X, X1), d(Y, Y1), d(Z, Z1), p(x_neq_y_plus_z(X1, Y1, Z1))],
2730 m(any(X) #\= any(Y) - any(Z)) => [d(X, X1), d(Y, Y1), d(Z, Z1), p(x_neq_y_plus_z(Y1, X1, Z1))],
2731 m(any(X) #\= any(Y)) => [d(X, RX), d(Y, RY), g(neq(RX, RY))]
2732 ]).
2733
2739
2740make_matches(Clauses) :-
2741 matches(Ms),
2742 findall(F, (member(M=>_, Ms), arg(1, M, M1), functor(M1, F, _)), Fs0),
2743 sort(Fs0, Fs),
2744 maplist(prevent_cyclic_argument, Fs, PrevCyclicClauses),
2745 phrase(matchers(Ms), Clauses0),
2746 maplist(goals_goal, Clauses0, MatcherClauses),
2747 append(PrevCyclicClauses, MatcherClauses, Clauses1),
2748 sort_by_predicate(Clauses1, Clauses).
2749
2750sort_by_predicate(Clauses, ByPred) :-
2751 map_list_to_pairs(predname, Clauses, Keyed),
2752 keysort(Keyed, KeyedByPred),
2753 pairs_values(KeyedByPred, ByPred).
2754
2755predname((H:-_), Key) :- !, predname(H, Key).
2756predname(M:H, M:Key) :- !, predname(H, Key).
2757predname(H, Name/Arity) :- !, functor(H, Name, Arity).
2758
2759prevent_cyclic_argument(F0, Clause) :-
2760 match_expand(F0, F),
2761 Head =.. [F,X,Y],
2762 Clause = (Head :- ( cyclic_term(X) ->
2763 domain_error(clpfd_expression, X)
2764 ; cyclic_term(Y) ->
2765 domain_error(clpfd_expression, Y)
2766 ; false
2767 )).
2768
2769matchers([]) --> [].
2770matchers([Condition => Goals|Ms]) -->
2771 matcher(Condition, Goals),
2772 matchers(Ms).
2773
2774matcher(m(M), Gs) --> matcher(m_c(M,true), Gs).
2775matcher(m_c(Matcher,Cond), Gs) -->
2776 [(Head :- Goals0)],
2777 { Matcher =.. [F,A,B],
2778 match_expand(F, Expand),
2779 Head =.. [Expand,X,Y],
2780 phrase((match(A, X), match(B, Y)), Goals0, [Cond,!|Goals1]),
2781 phrase(match_goals(Gs, Expand), Goals1) },
2782 ( { symmetric(F), \+ (subsumes_term(A, B), subsumes_term(B, A)) } ->
2783 { Head1 =.. [Expand,Y,X] },
2784 [(Head1 :- Goals0)]
2785 ; []
2786 ).
2787
2788match(any(A), T) --> [A = T].
2789match(var(V), T) --> [( nonvar(T), ( T = ?(Var) ; T = #(Var) ) ->
2790 must_be_fd_integer(Var), V = Var
2791 ; v_or_i(T), V = T
2792 )].
2793match(integer(I), T) --> [integer(T), I = T].
2794match(-X, T) --> [nonvar(T), T = -A], match(X, A).
2795match(abs(X), T) --> [nonvar(T), T = abs(A)], match(X, A).
2796match(Binary, T) -->
2797 { Binary =.. [Op,X,Y], Term =.. [Op,A,B] },
2798 [nonvar(T), T = Term],
2799 match(X, A), match(Y, B).
2800
2801match_goals([], _) --> [].
2802match_goals([G|Gs], F) --> match_goal(G, F), match_goals(Gs, F).
2803
2804match_goal(r(X,Y), F) --> { G =.. [F,X,Y] }, [G].
2805match_goal(d(X,Y), _) --> [parse_clpfd(X, Y)].
2806match_goal(g(Goal), _) --> [Goal].
2807match_goal(p(Prop), _) -->
2808 [make_propagator(Prop, P)],
2809 { term_variables(Prop, Vs) },
2810 parse_init(Vs, P),
2811 [trigger_once(P)].
2812
2813
2815
2816
2817
2823
2824X #>= Y :- clpfd_geq(X, Y).
2825
2826clpfd_geq(X, Y) :- clpfd_geq_(X, Y), reinforce(X), reinforce(Y).
2827
2834
2835X #=< Y :- Y #>= X.
2836
2843
2844X #= Y :- clpfd_equal(X, Y).
2845
2846clpfd_equal(X, Y) :- clpfd_equal_(X, Y), reinforce(X).
2847
2852
2853expr_conds(E, E) --> [integer(E)],
2854 { var(E), !, \+ current_prolog_flag(clpfd_monotonic, true) }.
2855expr_conds(E, E) --> { integer(E) }.
2856expr_conds(?(E), E) --> [integer(E)].
2857expr_conds(#(E), E) --> [integer(E)].
2858expr_conds(-E0, -E) --> expr_conds(E0, E).
2859expr_conds(abs(E0), abs(E)) --> expr_conds(E0, E).
2860expr_conds(A0+B0, A+B) --> expr_conds(A0, A), expr_conds(B0, B).
2861expr_conds(A0*B0, A*B) --> expr_conds(A0, A), expr_conds(B0, B).
2862expr_conds(A0-B0, A-B) --> expr_conds(A0, A), expr_conds(B0, B).
2863expr_conds(A0//B0, A//B) -->
2864 expr_conds(A0, A), expr_conds(B0, B),
2865 [B =\= 0].
2867expr_conds(min(A0,B0), min(A,B)) --> expr_conds(A0, A), expr_conds(B0, B).
2868expr_conds(max(A0,B0), max(A,B)) --> expr_conds(A0, A), expr_conds(B0, B).
2869expr_conds(A0 mod B0, A mod B) -->
2870 expr_conds(A0, A), expr_conds(B0, B),
2871 [B =\= 0].
2872expr_conds(A0^B0, A^B) -->
2873 expr_conds(A0, A), expr_conds(B0, B),
2874 [(B >= 0 ; A =:= -1)].
2876expr_conds(\ A0, \ A) --> expr_conds(A0, A).
2877expr_conds(A0<<B0, A<<B) --> expr_conds(A0, A), expr_conds(B0, B).
2878expr_conds(A0>>B0, A>>B) --> expr_conds(A0, A), expr_conds(B0, B).
2879expr_conds(A0/\B0, A/\B) --> expr_conds(A0, A), expr_conds(B0, B).
2880expr_conds(A0\/B0, A\/B) --> expr_conds(A0, A), expr_conds(B0, B).
2881expr_conds(A0 xor B0, A xor B) --> expr_conds(A0, A), expr_conds(B0, B).
2882expr_conds(lsb(A0), lsb(A)) --> expr_conds(A0, A).
2883expr_conds(msb(A0), msb(A)) --> expr_conds(A0, A).
2884expr_conds(popcount(A0), popcount(A)) --> expr_conds(A0, A).
2885
2886:- multifile
2887 system:goal_expansion/2. 2888:- dynamic
2889 system:goal_expansion/2. 2890
2891system:goal_expansion(Goal, Expansion) :-
2892 \+ current_prolog_flag(optimise_clpfd, false),
2893 clpfd_expandable(Goal),
2894 prolog_load_context(module, M),
2895 ( M == clpfd
2896 -> true
2897 ; predicate_property(M:Goal, imported_from(clpfd))
2898 ),
2899 clpfd_expansion(Goal, Expansion).
2900
2901clpfd_expandable(_ in _).
2902clpfd_expandable(_ #= _).
2903clpfd_expandable(_ #>= _).
2904clpfd_expandable(_ #=< _).
2905clpfd_expandable(_ #> _).
2906clpfd_expandable(_ #< _).
2907
2908clpfd_expansion(Var in Dom, In) :-
2909 ( ground(Dom), Dom = L..U, integer(L), integer(U) ->
2910 expansion_simpler(
2911 ( integer(Var) ->
2912 between(L, U, Var)
2913 ; clpfd:clpfd_in(Var, Dom)
2914 ), In)
2915 ; In = clpfd:clpfd_in(Var, Dom)
2916 ).
2917clpfd_expansion(X0 #= Y0, Equal) :-
2918 phrase(expr_conds(X0, X), CsX),
2919 phrase(expr_conds(Y0, Y), CsY),
2920 list_goal(CsX, CondX),
2921 list_goal(CsY, CondY),
2922 expansion_simpler(
2923 ( CondX ->
2924 ( var(Y) -> Y is X
2925 ; CondY -> X =:= Y
2926 ; T is X, clpfd:clpfd_equal(T, Y0)
2927 )
2928 ; CondY ->
2929 ( var(X) -> X is Y
2930 ; T is Y, clpfd:clpfd_equal(X0, T)
2931 )
2932 ; clpfd:clpfd_equal(X0, Y0)
2933 ), Equal).
2934clpfd_expansion(X0 #>= Y0, Geq) :-
2935 phrase(expr_conds(X0, X), CsX),
2936 phrase(expr_conds(Y0, Y), CsY),
2937 list_goal(CsX, CondX),
2938 list_goal(CsY, CondY),
2939 expansion_simpler(
2940 ( CondX ->
2941 ( CondY -> X >= Y
2942 ; T is X, clpfd:clpfd_geq(T, Y0)
2943 )
2944 ; CondY -> T is Y, clpfd:clpfd_geq(X0, T)
2945 ; clpfd:clpfd_geq(X0, Y0)
2946 ), Geq).
2947clpfd_expansion(X #=< Y, Leq) :- clpfd_expansion(Y #>= X, Leq).
2948clpfd_expansion(X #> Y, Gt) :- clpfd_expansion(X #>= Y+1, Gt).
2949clpfd_expansion(X #< Y, Lt) :- clpfd_expansion(Y #> X, Lt).
2950
2951expansion_simpler((True->Then0;_), Then) :-
2952 is_true(True), !,
2953 expansion_simpler(Then0, Then).
2954expansion_simpler((False->_;Else0), Else) :-
2955 is_false(False), !,
2956 expansion_simpler(Else0, Else).
2957expansion_simpler((If->Then0;Else0), (If->Then;Else)) :- !,
2958 expansion_simpler(Then0, Then),
2959 expansion_simpler(Else0, Else).
2960expansion_simpler((A0,B0), (A,B)) :-
2961 expansion_simpler(A0, A),
2962 expansion_simpler(B0, B).
2963expansion_simpler(Var is Expr0, Goal) :-
2964 ground(Expr0), !,
2965 phrase(expr_conds(Expr0, Expr), Gs),
2966 ( maplist(call, Gs) -> Value is Expr, Goal = (Var = Value)
2967 ; Goal = false
2968 ).
2969expansion_simpler(Var =:= Expr0, Goal) :-
2970 ground(Expr0), !,
2971 phrase(expr_conds(Expr0, Expr), Gs),
2972 ( maplist(call, Gs) -> Value is Expr, Goal = (Var =:= Value)
2973 ; Goal = false
2974 ).
2975expansion_simpler(Var is Expr, Var = Expr) :- var(Expr), !.
2976expansion_simpler(Var is Expr, Goal) :- !,
2977 ( var(Var), nonvar(Expr),
2978 Expr = E mod M, nonvar(E), E = A^B ->
2979 Goal = ( ( integer(A), integer(B), integer(M),
2980 A >= 0, B >= 0, M > 0 ->
2981 Var is powm(A, B, M)
2982 ; Var is Expr
2983 ) )
2984 ; Goal = ( Var is Expr )
2985 ).
2986expansion_simpler(between(L,U,V), Goal) :- maplist(integer, [L,U,V]), !,
2987 ( between(L,U,V) -> Goal = true
2988 ; Goal = false
2989 ).
2990expansion_simpler(Goal, Goal).
2991
2992is_true(true).
2993is_true(integer(I)) :- integer(I).
2994:- if(current_predicate(var_property/2)). 2995is_true(var(X)) :- var(X), var_property(X, fresh(true)).
2996is_false(integer(X)) :- var(X), var_property(X, fresh(true)).
2997is_false((A,B)) :- is_false(A) ; is_false(B).
2998:- endif. 2999is_false(var(X)) :- nonvar(X).
3000
3001
3003
3004linsum(X, S, S) --> { var(X), !, non_monotonic(X) }, [vn(X,1)].
3005linsum(I, S0, S) --> { integer(I), S is S0 + I }.
3006linsum(?(X), S, S) --> { must_be_fd_integer(X) }, [vn(X,1)].
3007linsum(#(X), S, S) --> { must_be_fd_integer(X) }, [vn(X,1)].
3008linsum(-A, S0, S) --> mulsum(A, -1, S0, S).
3009linsum(N*A, S0, S) --> { integer(N) }, !, mulsum(A, N, S0, S).
3010linsum(A*N, S0, S) --> { integer(N) }, !, mulsum(A, N, S0, S).
3011linsum(A+B, S0, S) --> linsum(A, S0, S1), linsum(B, S1, S).
3012linsum(A-B, S0, S) --> linsum(A, S0, S1), mulsum(B, -1, S1, S).
3013
3014mulsum(A, M, S0, S) -->
3015 { phrase(linsum(A, 0, CA), As), S is S0 + M*CA },
3016 lin_mul(As, M).
3017
3018lin_mul([], _) --> [].
3019lin_mul([vn(X,N0)|VNs], M) --> { N is N0*M }, [vn(X,N)], lin_mul(VNs, M).
3020
3021v_or_i(V) :- var(V), !, non_monotonic(V).
3022v_or_i(I) :- integer(I).
3023
3024must_be_fd_integer(X) :-
3025 ( var(X) -> constrain_to_integer(X)
3026 ; must_be(integer, X)
3027 ).
3028
3029left_right_linsum_const(Left, Right, Cs, Vs, Const) :-
3030 phrase(linsum(Left, 0, CL), Lefts0, Rights),
3031 phrase(linsum(Right, 0, CR), Rights0),
3032 maplist(linterm_negate, Rights0, Rights),
3033 msort(Lefts0, Lefts),
3034 Lefts = [vn(First,N)|LeftsRest],
3035 vns_coeffs_variables(LeftsRest, N, First, Cs0, Vs0),
3036 filter_linsum(Cs0, Vs0, Cs, Vs),
3037 Const is CR - CL.
3038 3039
3040linterm_negate(vn(V,N0), vn(V,N)) :- N is -N0.
3041
3042vns_coeffs_variables([], N, V, [N], [V]).
3043vns_coeffs_variables([vn(V,N)|VNs], N0, V0, Ns, Vs) :-
3044 ( V == V0 ->
3045 N1 is N0 + N,
3046 vns_coeffs_variables(VNs, N1, V0, Ns, Vs)
3047 ; Ns = [N0|NRest],
3048 Vs = [V0|VRest],
3049 vns_coeffs_variables(VNs, N, V, NRest, VRest)
3050 ).
3051
3052filter_linsum([], [], [], []).
3053filter_linsum([C0|Cs0], [V0|Vs0], Cs, Vs) :-
3054 ( C0 =:= 0 ->
3055 constrain_to_integer(V0),
3056 filter_linsum(Cs0, Vs0, Cs, Vs)
3057 ; Cs = [C0|Cs1], Vs = [V0|Vs1],
3058 filter_linsum(Cs0, Vs0, Cs1, Vs1)
3059 ).
3060
3061gcd([], G, G).
3062gcd([N|Ns], G0, G) :-
3063 G1 is gcd(N, G0),
3064 gcd(Ns, G1, G).
3065
3066even(N) :- N mod 2 =:= 0.
3067
3068odd(N) :- \+ even(N).
3069
3075
3076integer_kth_root(N, K, R) :-
3077 ( even(K) ->
3078 N >= 0
3079 ; true
3080 ),
3081 ( N < 0 ->
3082 odd(K),
3083 integer_kroot(N, 0, N, K, R)
3084 ; integer_kroot(0, N, N, K, R)
3085 ).
3086
3087integer_kroot(L, U, N, K, R) :-
3088 ( L =:= U -> N =:= L^K, R = L
3089 ; L + 1 =:= U ->
3090 ( L^K =:= N -> R = L
3091 ; U^K =:= N -> R = U
3092 ; false
3093 )
3094 ; Mid is (L + U)//2,
3095 ( Mid^K > N ->
3096 integer_kroot(L, Mid, N, K, R)
3097 ; integer_kroot(Mid, U, N, K, R)
3098 )
3099 ).
3100
3101integer_log_b(N, B, Log0, Log) :-
3102 T is B^Log0,
3103 ( T =:= N -> Log = Log0
3104 ; T < N,
3105 Log1 is Log0 + 1,
3106 integer_log_b(N, B, Log1, Log)
3107 ).
3108
3109floor_integer_log_b(N, B, Log0, Log) :-
3110 T is B^Log0,
3111 ( T > N -> Log is Log0 - 1
3112 ; T =:= N -> Log = Log0
3113 ; T < N,
3114 Log1 is Log0 + 1,
3115 floor_integer_log_b(N, B, Log1, Log)
3116 ).
3117
3118
3122
3123:- if(current_predicate(nth_integer_root_and_remainder/4)). 3124
3126integer_kth_root_leq(N, K, R) :-
3127 nth_integer_root_and_remainder(K, N, R, _).
3128
3129:- else. 3130
3131integer_kth_root_leq(N, K, R) :-
3132 ( even(K) ->
3133 N >= 0
3134 ; true
3135 ),
3136 ( N < 0 ->
3137 odd(K),
3138 integer_kroot_leq(N, 0, N, K, R)
3139 ; integer_kroot_leq(0, N, N, K, R)
3140 ).
3141
3142integer_kroot_leq(L, U, N, K, R) :-
3143 ( L =:= U -> R = L
3144 ; L + 1 =:= U ->
3145 ( U^K =< N -> R = U
3146 ; R = L
3147 )
3148 ; Mid is (L + U)//2,
3149 ( Mid^K > N ->
3150 integer_kroot_leq(L, Mid, N, K, R)
3151 ; integer_kroot_leq(Mid, U, N, K, R)
3152 )
3153 ).
3154
3155:- endif. 3156
3163
3164X #\= Y :- clpfd_neq(X, Y), do_queue.
3165
3167
3168x_neq_y_plus_z(X, Y, Z) :-
3169 propagator_init_trigger(x_neq_y_plus_z(X,Y,Z)).
3170
3173
3174neq_num(X, N) :-
3175 ( fd_get(X, XD, XPs) ->
3176 domain_remove(XD, N, XD1),
3177 fd_put(X, XD1, XPs)
3178 ; X =\= N
3179 ).
3180
3186
3187X #> Y :- X #>= Y + 1.
3188
3209
3210X #< Y :- Y #> X.
3211
3222
3223#\ Q :- reify(Q, 0), do_queue.
3224
3262
3263L #<==> R :- reify(L, B), reify(R, B), do_queue.
3264
3268
3281
3282L #==> R :-
3283 reify(L, LB, LPs),
3284 reify(R, RB, RPs),
3285 append(LPs, RPs, Ps),
3286 propagator_init_trigger([LB,RB], pimpl(LB,RB,Ps)).
3287
3291
3292L #<== R :- R #==> L.
3293
3297
3298L #/\ R :- reify(L, 1), reify(R, 1), do_queue.
3299
3300conjunctive_neqs_var_drep(Eqs, Var, Drep) :-
3301 conjunctive_neqs_var(Eqs, Var),
3302 phrase(conjunctive_neqs_vals(Eqs), Vals),
3303 list_to_domain(Vals, Dom),
3304 domain_complement(Dom, C),
3305 domain_to_drep(C, Drep).
3306
3307conjunctive_neqs_var(V, _) :- var(V), !, false.
3308conjunctive_neqs_var(L #\= R, Var) :-
3309 ( var(L), integer(R) -> Var = L
3310 ; integer(L), var(R) -> Var = R
3311 ; false
3312 ).
3313conjunctive_neqs_var(A #/\ B, VA) :-
3314 conjunctive_neqs_var(A, VA),
3315 conjunctive_neqs_var(B, VB),
3316 VA == VB.
3317
3318conjunctive_neqs_vals(L #\= R) --> ( { integer(L) } -> [L] ; [R] ).
3319conjunctive_neqs_vals(A #/\ B) -->
3320 conjunctive_neqs_vals(A),
3321 conjunctive_neqs_vals(B).
3322
3338
3339L #\/ R :-
3340 ( disjunctive_eqs_var_drep(L #\/ R, Var, Drep) -> Var in Drep
3341 ; reify(L, X, Ps1),
3342 reify(R, Y, Ps2),
3343 propagator_init_trigger([X,Y], reified_or(X,Ps1,Y,Ps2,1))
3344 ).
3345
3346disjunctive_eqs_var_drep(Eqs, Var, Drep) :-
3347 disjunctive_eqs_var(Eqs, Var),
3348 phrase(disjunctive_eqs_vals(Eqs), Vals),
3349 list_to_drep(Vals, Drep).
3350
3351disjunctive_eqs_var(V, _) :- var(V), !, false.
3352disjunctive_eqs_var(V in I, V) :- var(V), integer(I).
3353disjunctive_eqs_var(L #= R, Var) :-
3354 ( var(L), integer(R) -> Var = L
3355 ; integer(L), var(R) -> Var = R
3356 ; false
3357 ).
3358disjunctive_eqs_var(A #\/ B, VA) :-
3359 disjunctive_eqs_var(A, VA),
3360 disjunctive_eqs_var(B, VB),
3361 VA == VB.
3362
3363disjunctive_eqs_vals(L #= R) --> ( { integer(L) } -> [L] ; [R] ).
3364disjunctive_eqs_vals(_ in I) --> [I].
3365disjunctive_eqs_vals(A #\/ B) -->
3366 disjunctive_eqs_vals(A),
3367 disjunctive_eqs_vals(B).
3368
3373
3374L #\ R :- (L #\/ R) #/\ #\ (L #/\ R).
3375
3400
3401parse_reified(E, R, D,
3402 [g(cyclic_term(E)) => [g(domain_error(clpfd_expression, E))],
3403 g(var(E)) => [g(non_monotonic(E)),
3404 g(constrain_to_integer(E)), g(R = E), g(D=1)],
3405 g(integer(E)) => [g(R=E), g(D=1)],
3406 ?(E) => [g(must_be_fd_integer(E)), g(R=E), g(D=1)],
3407 #(E) => [g(must_be_fd_integer(E)), g(R=E), g(D=1)],
3408 m(A+B) => [d(D), p(pplus(A,B,R)), a(A,B,R)],
3409 m(A*B) => [d(D), p(ptimes(A,B,R)), a(A,B,R)],
3410 m(A-B) => [d(D), p(pplus(R,B,A)), a(A,B,R)],
3411 m(-A) => [d(D), p(ptimes(-1,A,R)), a(R)],
3412 m(max(A,B)) => [d(D), p(pgeq(R, A)), p(pgeq(R, B)), p(pmax(A,B,R)), a(A,B,R)],
3413 m(min(A,B)) => [d(D), p(pgeq(A, R)), p(pgeq(B, R)), p(pmin(A,B,R)), a(A,B,R)],
3414 m(abs(A)) => [g(?(R)#>=0), d(D), p(pabs(A, R)), a(A,R)],
3416 m(A//B) => [skeleton(A,B,D,R,ptzdiv)],
3417 m(A div B) => [skeleton(A,B,D,R,pdiv)],
3418 m(A rdiv B) => [skeleton(A,B,D,R,prdiv)],
3419 m(A mod B) => [skeleton(A,B,D,R,pmod)],
3420 m(A rem B) => [skeleton(A,B,D,R,prem)],
3421 m(A^B) => [d(D), p(pexp(A,B,R)), a(A,B,R)],
3422 3423 m(\A) => [function(D,\,A,R)],
3424 m(msb(A)) => [function(D,msb,A,R)],
3425 m(lsb(A)) => [function(D,lsb,A,R)],
3426 m(popcount(A)) => [function(D,popcount,A,R)],
3427 m(A<<B) => [d(D), p(pshift(A,B,R,1)), a(A,B,R)],
3428 m(A>>B) => [d(D), p(pshift(A,B,R,-1)), a(A,B,R)],
3429 m(A/\B) => [function(D,/\,A,B,R)],
3430 m(A\/B) => [function(D,\/,A,B,R)],
3431 m(A xor B) => [function(D,xor,A,B,R)],
3432 g(true) => [g(domain_error(clpfd_expression, E))]]
3433 ).
3434
3440
3441make_parse_reified(Clauses) :-
3442 parse_reified_clauses(Clauses0),
3443 maplist(goals_goal_dcg, Clauses0, Clauses).
3444
3445goals_goal_dcg((Head --> Goals), Clause) :-
3446 list_goal(Goals, Body),
3447 expand_term((Head --> Body), Clause).
3448
3449parse_reified_clauses(Clauses) :-
3450 parse_reified(E, R, D, Matchers),
3451 maplist(parse_reified(E, R, D), Matchers, Clauses).
3452
3453parse_reified(E, R, D, Matcher, Clause) :-
3454 Matcher = (Condition0 => Goals0),
3455 phrase((reified_condition(Condition0, E, Head, Ds),
3456 reified_goals(Goals0, Ds)), Goals, [a(D)]),
3457 Clause = (parse_reified_clpfd(Head, R, D) --> Goals).
3458
3459reified_condition(g(Goal), E, E, []) --> [{Goal}, !].
3460reified_condition(?(E), _, ?(E), []) --> [!].
3461reified_condition(#(E), _, #(E), []) --> [!].
3462reified_condition(m(Match), _, Match0, Ds) -->
3463 [!],
3464 { copy_term(Match, Match0),
3465 term_variables(Match0, Vs0),
3466 term_variables(Match, Vs)
3467 },
3468 reified_variables(Vs0, Vs, Ds).
3469
3470reified_variables([], [], []) --> [].
3471reified_variables([V0|Vs0], [V|Vs], [D|Ds]) -->
3472 [parse_reified_clpfd(V0, V, D)],
3473 reified_variables(Vs0, Vs, Ds).
3474
3475reified_goals([], _) --> [].
3476reified_goals([G|Gs], Ds) --> reified_goal(G, Ds), reified_goals(Gs, Ds).
3477
3478reified_goal(d(D), Ds) -->
3479 ( { Ds = [X] } -> [{D=X}]
3480 ; { Ds = [X,Y] } ->
3481 { phrase(reified_goal(p(reified_and(X,[],Y,[],D)), _), Gs),
3482 list_goal(Gs, Goal) },
3483 [( {X==1, Y==1} -> {D = 1} ; Goal )]
3484 ; { domain_error(one_or_two_element_list, Ds) }
3485 ).
3486reified_goal(g(Goal), _) --> [{Goal}].
3487reified_goal(p(Vs, Prop), _) -->
3488 [{make_propagator(Prop, P)}],
3489 parse_init_dcg(Vs, P),
3490 [{trigger_once(P)}],
3491 [( { propagator_state(P, S), S == dead } -> [] ; [p(P)])].
3492reified_goal(p(Prop), Ds) -->
3493 { term_variables(Prop, Vs) },
3494 reified_goal(p(Vs,Prop), Ds).
3495reified_goal(function(D,Op,A,B,R), Ds) -->
3496 reified_goals([d(D),p(pfunction(Op,A,B,R)),a(A,B,R)], Ds).
3497reified_goal(function(D,Op,A,R), Ds) -->
3498 reified_goals([d(D),p(pfunction(Op,A,R)),a(A,R)], Ds).
3499reified_goal(skeleton(A,B,D,R,F), Ds) -->
3500 { Prop =.. [F,X,Y,Z] },
3501 reified_goals([d(D1),l(p(P)),g(make_propagator(Prop, P)),
3502 p([A,B,D2,R], pskeleton(A,B,D2,[X,Y,Z]-P,R,F)),
3503 p(reified_and(D1,[],D2,[],D)),a(D2),a(A,B,R)], Ds).
3504reified_goal(a(V), _) --> [a(V)].
3505reified_goal(a(X,V), _) --> [a(X,V)].
3506reified_goal(a(X,Y,V), _) --> [a(X,Y,V)].
3507reified_goal(l(L), _) --> [[L]].
3508
3509parse_init_dcg([], _) --> [].
3510parse_init_dcg([V|Vs], P) --> [{init_propagator(V, P)}], parse_init_dcg(Vs, P).
3511
3514
3515reify(E, B) :- reify(E, B, _).
3516
3517reify(Expr, B, Ps) :-
3518 ( acyclic_term(Expr), reifiable(Expr) -> phrase(reify(Expr, B), Ps)
3519 ; domain_error(clpfd_reifiable_expression, Expr)
3520 ).
3521
3522reifiable(E) :- var(E), non_monotonic(E).
3523reifiable(E) :- integer(E), E in 0..1.
3524reifiable(?(E)) :- must_be_fd_integer(E).
3525reifiable(#(E)) :- must_be_fd_integer(E).
3526reifiable(V in _) :- fd_variable(V).
3527reifiable(V in_set _) :- fd_variable(V).
3528reifiable(Expr) :-
3529 Expr =.. [Op,Left,Right],
3530 ( memberchk(Op, [#>=,#>,#=<,#<,#=,#\=])
3531 ; memberchk(Op, [#==>,#<==,#<==>,#/\,#\/,#\]),
3532 reifiable(Left),
3533 reifiable(Right)
3534 ).
3535reifiable(#\ E) :- reifiable(E).
3536reifiable(tuples_in(Tuples, Relation)) :-
3537 must_be(list(list), Tuples),
3538 maplist(maplist(fd_variable), Tuples),
3539 must_be(list(list(integer)), Relation).
3540reifiable(finite_domain(V)) :- fd_variable(V).
3541
3542reify(E, B) --> { B in 0..1 }, reify_(E, B).
3543
3544reify_(E, B) --> { var(E), !, E = B }.
3545reify_(E, B) --> { integer(E), E = B }.
3546reify_(?(B), B) --> [].
3547reify_(#(B), B) --> [].
3548reify_(V in Drep, B) -->
3549 { drep_to_domain(Drep, Dom) },
3550 propagator_init_trigger(reified_in(V,Dom,B)),
3551 a(B).
3552reify_(V in_set Dom, B) -->
3553 propagator_init_trigger(reified_in(V,Dom,B)),
3554 a(B).
3555reify_(tuples_in(Tuples, Relation), B) -->
3556 { maplist(relation_tuple_b_prop(Relation), Tuples, Bs, Ps),
3557 maplist(monotonic, Bs, Bs1),
3558 fold_statement(conjunction, Bs1, And),
3559 ?(B) #<==> And },
3560 propagator_init_trigger([B], tuples_not_in(Tuples, Relation, B)),
3561 kill_reified_tuples(Bs, Ps, Bs),
3562 list(Ps),
3563 as([B|Bs]).
3564reify_(finite_domain(V), B) -->
3565 propagator_init_trigger(reified_fd(V,B)),
3566 a(B).
3567reify_(L #>= R, B) --> arithmetic(L, R, B, reified_geq).
3568reify_(L #= R, B) --> arithmetic(L, R, B, reified_eq).
3569reify_(L #\= R, B) --> arithmetic(L, R, B, reified_neq).
3570reify_(L #> R, B) --> reify_(L #>= (R+1), B).
3571reify_(L #=< R, B) --> reify_(R #>= L, B).
3572reify_(L #< R, B) --> reify_(R #>= (L+1), B).
3573reify_(L #==> R, B) --> reify_((#\ L) #\/ R, B).
3574reify_(L #<== R, B) --> reify_(R #==> L, B).
3575reify_(L #<==> R, B) --> reify_((L #==> R) #/\ (R #==> L), B).
3576reify_(L #\ R, B) --> reify_((L #\/ R) #/\ #\ (L #/\ R), B).
3577reify_(L #/\ R, B) -->
3578 ( { conjunctive_neqs_var_drep(L #/\ R, V, D) } -> reify_(V in D, B)
3579 ; boolean(L, R, B, reified_and)
3580 ).
3581reify_(L #\/ R, B) -->
3582 ( { disjunctive_eqs_var_drep(L #\/ R, V, D) } -> reify_(V in D, B)
3583 ; boolean(L, R, B, reified_or)
3584 ).
3585reify_(#\ Q, B) -->
3586 reify(Q, QR),
3587 propagator_init_trigger(reified_not(QR,B)),
3588 a(B).
3589
3590arithmetic(L, R, B, Functor) -->
3591 { phrase((parse_reified_clpfd(L, LR, LD),
3592 parse_reified_clpfd(R, RR, RD)), Ps),
3593 Prop =.. [Functor,LD,LR,RD,RR,Ps,B] },
3594 list(Ps),
3595 propagator_init_trigger([LD,LR,RD,RR,B], Prop),
3596 a(B).
3597
3598boolean(L, R, B, Functor) -->
3599 { reify(L, LR, Ps1), reify(R, RR, Ps2),
3600 Prop =.. [Functor,LR,Ps1,RR,Ps2,B] },
3601 list(Ps1), list(Ps2),
3602 propagator_init_trigger([LR,RR,B], Prop),
3603 a(LR, RR, B).
3604
3605list([]) --> [].
3606list([L|Ls]) --> [L], list(Ls).
3607
3608a(X,Y,B) -->
3609 ( { nonvar(X) } -> a(Y, B)
3610 ; { nonvar(Y) } -> a(X, B)
3611 ; [a(X,Y,B)]
3612 ).
3613
3614a(X, B) -->
3615 ( { var(X) } -> [a(X, B)]
3616 ; a(B)
3617 ).
3618
3619a(B) -->
3620 ( { var(B) } -> [a(B)]
3621 ; []
3622 ).
3623
3624as([]) --> [].
3625as([B|Bs]) --> a(B), as(Bs).
3626
3627kill_reified_tuples([], _, _) --> [].
3628kill_reified_tuples([B|Bs], Ps, All) -->
3629 propagator_init_trigger([B], kill_reified_tuples(B, Ps, All)),
3630 kill_reified_tuples(Bs, Ps, All).
3631
3632relation_tuple_b_prop(Relation, Tuple, B, p(Prop)) :-
3633 put_attr(R, clpfd_relation, Relation),
3634 make_propagator(reified_tuple_in(Tuple, R, B), Prop),
3635 tuple_freeze_(Tuple, Prop),
3636 init_propagator(B, Prop).
3637
3638
3639tuples_in_conjunction(Tuples, Relation, Conj) :-
3640 maplist(tuple_in_disjunction(Relation), Tuples, Disjs),
3641 fold_statement(conjunction, Disjs, Conj).
3642
3643tuple_in_disjunction(Relation, Tuple, Disj) :-
3644 maplist(tuple_in_conjunction(Tuple), Relation, Conjs),
3645 fold_statement(disjunction, Conjs, Disj).
3646
3647tuple_in_conjunction(Tuple, Element, Conj) :-
3648 maplist(var_eq, Tuple, Element, Eqs),
3649 fold_statement(conjunction, Eqs, Conj).
3650
3651fold_statement(Operation, List, Statement) :-
3652 ( List = [] -> Statement = 1
3653 ; List = [First|Rest],
3654 foldl(Operation, Rest, First, Statement)
3655 ).
3656
3657conjunction(E, Conj, Conj #/\ E).
3658
3659disjunction(E, Disj, Disj #\/ E).
3660
3661var_eq(V, N, ?(V) #= N).
3662
3664
3665skeleton(Vs, Vs-Prop) :-
3666 maplist(prop_init(Prop), Vs),
3667 trigger_once(Prop).
3668
3673
3674is_drep(N) :- integer(N).
3675is_drep(N..M) :- drep_bound(N), drep_bound(M), N \== sup, M \== inf.
3676is_drep(D1\/D2) :- is_drep(D1), is_drep(D2).
3677is_drep({AI}) :- is_and_integers(AI).
3678is_drep(\D) :- is_drep(D).
3679
3680is_and_integers(I) :- integer(I).
3681is_and_integers((A,B)) :- is_and_integers(A), is_and_integers(B).
3682
3683drep_bound(I) :- integer(I).
3684drep_bound(sup).
3685drep_bound(inf).
3686
3687drep_to_intervals(I) --> { integer(I) }, [n(I)-n(I)].
3688drep_to_intervals(N..M) -->
3689 ( { defaulty_to_bound(N, N1), defaulty_to_bound(M, M1),
3690 N1 cis_leq M1} -> [N1-M1]
3691 ; []
3692 ).
3693drep_to_intervals(D1 \/ D2) -->
3694 drep_to_intervals(D1), drep_to_intervals(D2).
3695drep_to_intervals(\D0) -->
3696 { drep_to_domain(D0, D1),
3697 domain_complement(D1, D),
3698 domain_to_drep(D, Drep) },
3699 drep_to_intervals(Drep).
3700drep_to_intervals({AI}) -->
3701 and_integers_(AI).
3702
3703and_integers_(I) --> { integer(I) }, [n(I)-n(I)].
3704and_integers_((A,B)) --> and_integers_(A), and_integers_(B).
3705
3706drep_to_domain(DR, D) :-
3707 must_be(ground, DR),
3708 ( is_drep(DR) -> true
3709 ; domain_error(clpfd_domain, DR)
3710 ),
3711 phrase(drep_to_intervals(DR), Is0),
3712 merge_intervals(Is0, Is1),
3713 intervals_to_domain(Is1, D).
3714
3715merge_intervals(Is0, Is) :-
3716 keysort(Is0, Is1),
3717 merge_overlapping(Is1, Is).
3718
3719merge_overlapping([], []).
3720merge_overlapping([A-B0|ABs0], [A-B|ABs]) :-
3721 merge_remaining(ABs0, B0, B, Rest),
3722 merge_overlapping(Rest, ABs).
3723
3724merge_remaining([], B, B, []).
3725merge_remaining([N-M|NMs], B0, B, Rest) :-
3726 Next cis B0 + n(1),
3727 ( N cis_gt Next -> B = B0, Rest = [N-M|NMs]
3728 ; B1 cis max(B0,M),
3729 merge_remaining(NMs, B1, B, Rest)
3730 ).
3731
3732domain(V, Dom) :-
3733 ( fd_get(V, Dom0, VPs) ->
3734 domains_intersection(Dom, Dom0, Dom1),
3735 3736 fd_put(V, Dom1, VPs),
3737 do_queue,
3738 reinforce(V)
3739 ; domain_contains(Dom, V)
3740 ).
3741
3742domains([], _).
3743domains([V|Vs], D) :- domain(V, D), domains(Vs, D).
3744
3745props_number(fd_props(Gs,Bs,Os), N) :-
3746 length(Gs, N1),
3747 length(Bs, N2),
3748 length(Os, N3),
3749 N is N1 + N2 + N3.
3750
3751fd_get(X, Dom, Ps) :-
3752 ( get_attr(X, clpfd, Attr) -> Attr = clpfd_attr(_,_,_,Dom,Ps)
3753 ; var(X) -> default_domain(Dom), Ps = fd_props([],[],[])
3754 ).
3755
3756fd_get(X, Dom, Inf, Sup, Ps) :-
3757 fd_get(X, Dom, Ps),
3758 domain_infimum(Dom, Inf),
3759 domain_supremum(Dom, Sup).
3760
3774
3775fd_put(X, Dom, Ps) :-
3776 ( current_prolog_flag(clpfd_propagation, full) ->
3777 put_full(X, Dom, Ps)
3778 ; put_terminating(X, Dom, Ps)
3779 ).
3780
3781put_terminating(X, Dom, Ps) :-
3782 Dom \== empty,
3783 ( Dom = from_to(F, F) -> F = n(X)
3784 ; ( get_attr(X, clpfd, Attr) ->
3785 Attr = clpfd_attr(Left,Right,Spread,OldDom, _OldPs),
3786 put_attr(X, clpfd, clpfd_attr(Left,Right,Spread,Dom,Ps)),
3787 ( OldDom == Dom -> true
3788 ; ( Left == (.) -> Bounded = yes
3789 ; domain_infimum(Dom, Inf), domain_supremum(Dom, Sup),
3790 ( Inf = n(_), Sup = n(_) ->
3791 Bounded = yes
3792 ; Bounded = no
3793 )
3794 ),
3795 ( Bounded == yes ->
3796 put_attr(X, clpfd, clpfd_attr(.,.,.,Dom,Ps)),
3797 trigger_props(Ps, X, OldDom, Dom)
3798 ; 3799 domain_infimum(OldDom, OldInf),
3800 ( Inf == OldInf -> LeftP = Left
3801 ; LeftP = yes
3802 ),
3803 domain_supremum(OldDom, OldSup),
3804 ( Sup == OldSup -> RightP = Right
3805 ; RightP = yes
3806 ),
3807 domain_spread(OldDom, OldSpread),
3808 domain_spread(Dom, NewSpread),
3809 ( NewSpread == OldSpread -> SpreadP = Spread
3810 ; NewSpread cis_lt OldSpread -> SpreadP = no
3811 ; SpreadP = yes
3812 ),
3813 put_attr(X, clpfd, clpfd_attr(LeftP,RightP,SpreadP,Dom,Ps)),
3814 ( RightP == yes, Right = yes -> true
3815 ; LeftP == yes, Left = yes -> true
3816 ; SpreadP == yes, Spread = yes -> true
3817 ; trigger_props(Ps, X, OldDom, Dom)
3818 )
3819 )
3820 )
3821 ; var(X) ->
3822 put_attr(X, clpfd, clpfd_attr(no,no,no,Dom, Ps))
3823 ; true
3824 )
3825 ).
3826
3827domain_spread(Dom, Spread) :-
3828 domain_smallest_finite(Dom, S),
3829 domain_largest_finite(Dom, L),
3830 Spread cis L - S.
3831
3832smallest_finite(inf, Y, Y).
3833smallest_finite(n(N), _, n(N)).
3834
3835domain_smallest_finite(from_to(F,T), S) :- smallest_finite(F, T, S).
3836domain_smallest_finite(split(_, L, _), S) :- domain_smallest_finite(L, S).
3837
3838largest_finite(sup, Y, Y).
3839largest_finite(n(N), _, n(N)).
3840
3841domain_largest_finite(from_to(F,T), L) :- largest_finite(T, F, L).
3842domain_largest_finite(split(_, _, R), L) :- domain_largest_finite(R, L).
3843
3848
3849reinforce(X) :-
3850 ( current_prolog_flag(clpfd_propagation, full) ->
3851 3852 true
3853 ; term_variables(X, Vs),
3854 maplist(reinforce_, Vs),
3855 do_queue
3856 ).
3857
3858reinforce_(X) :-
3859 ( fd_var(X), fd_get(X, Dom, Ps) ->
3860 put_full(X, Dom, Ps)
3861 ; true
3862 ).
3863
3864put_full(X, Dom, Ps) :-
3865 Dom \== empty,
3866 ( Dom = from_to(F, F) -> F = n(X)
3867 ; ( get_attr(X, clpfd, Attr) ->
3868 Attr = clpfd_attr(_,_,_,OldDom, _OldPs),
3869 put_attr(X, clpfd, clpfd_attr(no,no,no,Dom, Ps)),
3870 3871 ( OldDom == Dom -> true
3872 ; trigger_props(Ps, X, OldDom, Dom)
3873 )
3874 ; var(X) -> 3875 put_attr(X, clpfd, clpfd_attr(no,no,no,Dom, Ps))
3876 ; true
3877 )
3878 ).
3879
3887
3888make_propagator(C, propagator(C, _)).
3889
3890propagator_state(propagator(_,S), S).
3891
3892trigger_props(fd_props(Gs,Bs,Os), X, D0, D) :-
3893 ( ground(X) ->
3894 trigger_props_(Gs),
3895 trigger_props_(Bs)
3896 ; Bs \== [] ->
3897 domain_infimum(D0, I0),
3898 domain_infimum(D, I),
3899 ( I == I0 ->
3900 domain_supremum(D0, S0),
3901 domain_supremum(D, S),
3902 ( S == S0 -> true
3903 ; trigger_props_(Bs)
3904 )
3905 ; trigger_props_(Bs)
3906 )
3907 ; true
3908 ),
3909 trigger_props_(Os).
3910
3911trigger_props(fd_props(Gs,Bs,Os), X) :-
3912 trigger_props_(Os),
3913 trigger_props_(Bs),
3914 ( ground(X) ->
3915 trigger_props_(Gs)
3916 ; true
3917 ).
3918
3919trigger_props(fd_props(Gs,Bs,Os)) :-
3920 trigger_props_(Gs),
3921 trigger_props_(Bs),
3922 trigger_props_(Os).
3923
3924trigger_props_([]).
3925trigger_props_([P|Ps]) :- trigger_prop(P), trigger_props_(Ps).
3926
3927trigger_prop(Propagator) :-
3928 propagator_state(Propagator, State),
3929 ( State == dead -> true
3930 ; get_attr(State, clpfd_aux, queued) -> true
3931 ; b_getval('$clpfd_current_propagator', C), C == State -> true
3932 ; 3933 3934 put_attr(State, clpfd_aux, queued),
3935 ( arg(1, Propagator, C), functor(C, F, _), global_constraint(F) ->
3936 push_queue(Propagator, 2)
3937 ; push_queue(Propagator, 1)
3938 )
3939 ).
3940
3941kill(State) :- del_attr(State, clpfd_aux), State = dead.
3942
3943kill(State, Ps) :-
3944 kill(State),
3945 maplist(kill_entailed, Ps).
3946
3947kill_entailed(p(Prop)) :-
3948 propagator_state(Prop, State),
3949 kill(State).
3950kill_entailed(a(V)) :-
3951 del_attr(V, clpfd).
3952kill_entailed(a(X,B)) :-
3953 ( X == B -> true
3954 ; del_attr(B, clpfd)
3955 ).
3956kill_entailed(a(X,Y,B)) :-
3957 ( X == B -> true
3958 ; Y == B -> true
3959 ; del_attr(B, clpfd)
3960 ).
3961
3962no_reactivation(rel_tuple(_,_)).
3963no_reactivation(pdistinct(_)).
3964no_reactivation(pgcc(_,_,_)).
3965no_reactivation(pgcc_single(_,_)).
3967
3968activate_propagator(propagator(P,State)) :-
3969 3970 del_attr(State, clpfd_aux),
3971 ( no_reactivation(P) ->
3972 b_setval('$clpfd_current_propagator', State),
3973 run_propagator(P, State),
3974 b_setval('$clpfd_current_propagator', [])
3975 ; run_propagator(P, State)
3976 ).
3977
3978disable_queue :- b_setval('$clpfd_queue_status', disabled).
3979enable_queue :- b_setval('$clpfd_queue_status', enabled).
3980
3981portray_propagator(propagator(P,_), F) :- functor(P, F, _).
3982
3983portray_queue(V, []) :- var(V), !.
3984portray_queue([P|Ps], [F|Fs]) :-
3985 portray_propagator(P, F),
3986 portray_queue(Ps, Fs).
3987
3988do_queue :-
3989 3990 3991 3992 ( b_getval('$clpfd_queue_status', enabled) ->
3993 ( fetch_propagator(Propagator) ->
3994 activate_propagator(Propagator),
3995 do_queue
3996 ; true
3997 )
3998 ; true
3999 ).
4000
4001init_propagator(Var, Prop) :-
4002 ( fd_get(Var, Dom, Ps0) ->
4003 insert_propagator(Prop, Ps0, Ps),
4004 fd_put(Var, Dom, Ps)
4005 ; true
4006 ).
4007
4008constraint_wake(pneq, ground).
4009constraint_wake(x_neq_y_plus_z, ground).
4010constraint_wake(absdiff_neq, ground).
4011constraint_wake(pdifferent, ground).
4012constraint_wake(pexclude, ground).
4013constraint_wake(scalar_product_neq, ground).
4014
4015constraint_wake(x_leq_y_plus_c, bounds).
4016constraint_wake(scalar_product_eq, bounds).
4017constraint_wake(scalar_product_leq, bounds).
4018constraint_wake(pplus, bounds).
4019constraint_wake(pgeq, bounds).
4020constraint_wake(pgcc_single, bounds).
4021constraint_wake(pgcc_check_single, bounds).
4022
4023global_constraint(pdistinct).
4024global_constraint(pgcc).
4025global_constraint(pgcc_single).
4026global_constraint(pcircuit).
4029
4030insert_propagator(Prop, Ps0, Ps) :-
4031 Ps0 = fd_props(Gs,Bs,Os),
4032 arg(1, Prop, Constraint),
4033 functor(Constraint, F, _),
4034 ( constraint_wake(F, ground) ->
4035 Ps = fd_props([Prop|Gs], Bs, Os)
4036 ; constraint_wake(F, bounds) ->
4037 Ps = fd_props(Gs, [Prop|Bs], Os)
4038 ; Ps = fd_props(Gs, Bs, [Prop|Os])
4039 ).
4040
4042
4046
4047lex_chain(Lss) :-
4048 must_be(list(list), Lss),
4049 maplist(maplist(fd_variable), Lss),
4050 ( Lss == [] -> true
4051 ; Lss = [First|Rest],
4052 make_propagator(presidual(lex_chain(Lss)), Prop),
4053 foldl(lex_chain_(Prop), Rest, First, _)
4054 ).
4055
4056lex_chain_(Prop, Ls, Prev, Ls) :-
4057 maplist(prop_init(Prop), Ls),
4058 lex_le(Prev, Ls).
4059
4060lex_le([], []).
4061lex_le([V1|V1s], [V2|V2s]) :-
4062 ?(V1) #=< ?(V2),
4063 ( integer(V1) ->
4064 ( integer(V2) ->
4065 ( V1 =:= V2 -> lex_le(V1s, V2s) ; true )
4066 ; freeze(V2, lex_le([V1|V1s], [V2|V2s]))
4067 )
4068 ; freeze(V1, lex_le([V1|V1s], [V2|V2s]))
4069 ).
4070
4072
4073
4116
4117tuples_in(Tuples, Relation) :-
4118 must_be(list(list), Tuples),
4119 maplist(maplist(fd_variable), Tuples),
4120 must_be(list(list(integer)), Relation),
4121 maplist(relation_tuple(Relation), Tuples),
4122 do_queue.
4123
4124relation_tuple(Relation, Tuple) :-
4125 relation_unifiable(Relation, Tuple, Us, _, _),
4126 ( ground(Tuple) -> memberchk(Tuple, Relation)
4127 ; tuple_domain(Tuple, Us),
4128 ( Tuple = [_,_|_] -> tuple_freeze(Tuple, Us)
4129 ; true
4130 )
4131 ).
4132
4133tuple_domain([], _).
4134tuple_domain([T|Ts], Relation0) :-
4135 maplist(list_first_rest, Relation0, Firsts, Relation1),
4136 ( Firsts = [Unique] -> T = Unique
4137 ; var(T) ->
4138 ( Firsts = [Unique] -> T = Unique
4139 ; list_to_domain(Firsts, FDom),
4140 fd_get(T, TDom, TPs),
4141 domains_intersection(TDom, FDom, TDom1),
4142 fd_put(T, TDom1, TPs)
4143 )
4144 ; true
4145 ),
4146 tuple_domain(Ts, Relation1).
4147
4148tuple_freeze(Tuple, Relation) :-
4149 put_attr(R, clpfd_relation, Relation),
4150 make_propagator(rel_tuple(R, Tuple), Prop),
4151 tuple_freeze_(Tuple, Prop).
4152
4153tuple_freeze_([], _).
4154tuple_freeze_([T|Ts], Prop) :-
4155 ( var(T) ->
4156 init_propagator(T, Prop),
4157 trigger_prop(Prop)
4158 ; true
4159 ),
4160 tuple_freeze_(Ts, Prop).
4161
4162relation_unifiable([], _, [], Changed, Changed).
4163relation_unifiable([R|Rs], Tuple, Us, Changed0, Changed) :-
4164 ( all_in_domain(R, Tuple) ->
4165 Us = [R|Rest],
4166 relation_unifiable(Rs, Tuple, Rest, Changed0, Changed)
4167 ; relation_unifiable(Rs, Tuple, Us, true, Changed)
4168 ).
4169
4170all_in_domain([], []).
4171all_in_domain([A|As], [T|Ts]) :-
4172 ( fd_get(T, Dom, _) ->
4173 domain_contains(Dom, A)
4174 ; T =:= A
4175 ),
4176 all_in_domain(As, Ts).
4177
4179
4181run_propagator(presidual(_), _).
4182
4184run_propagator(pdifferent(Left,Right,X,_), MState) :-
4185 run_propagator(pexclude(Left,Right,X), MState).
4186
4187run_propagator(weak_distinct(Left,Right,X,_), _MState) :-
4188 ( ground(X) ->
4189 disable_queue,
4190 exclude_fire(Left, Right, X),
4191 enable_queue
4192 ; outof_reducer(Left, Right, X)
4193 4194 4195 4196 ).
4197
4198run_propagator(pexclude(Left,Right,X), _) :-
4199 ( ground(X) ->
4200 disable_queue,
4201 exclude_fire(Left, Right, X),
4202 enable_queue
4203 ; true
4204 ).
4205
4206run_propagator(pdistinct(Ls), _MState) :-
4207 distinct(Ls).
4208
4209run_propagator(check_distinct(Left,Right,X), _) :-
4210 \+ list_contains(Left, X),
4211 \+ list_contains(Right, X).
4212
4214
4215run_propagator(pelement(N, Is, V), MState) :-
4216 ( fd_get(N, NDom, _) ->
4217 ( fd_get(V, VDom, VPs) ->
4218 integers_remaining(Is, 1, NDom, empty, VDom1),
4219 domains_intersection(VDom, VDom1, VDom2),
4220 fd_put(V, VDom2, VPs)
4221 ; true
4222 )
4223 ; kill(MState), nth1(N, Is, V)
4224 ).
4225
4227
4228run_propagator(pgcc_single(Vs, Pairs), _) :- gcc_global(Vs, Pairs).
4229
4230run_propagator(pgcc_check_single(Pairs), _) :- gcc_check(Pairs).
4231
4232run_propagator(pgcc_check(Pairs), _) :- gcc_check(Pairs).
4233
4234run_propagator(pgcc(Vs, _, Pairs), _) :- gcc_global(Vs, Pairs).
4235
4237
4238run_propagator(pcircuit(Vs), _MState) :-
4239 distinct(Vs),
4240 propagate_circuit(Vs).
4241
4243run_propagator(pneq(A, B), MState) :-
4244 ( nonvar(A) ->
4245 ( nonvar(B) -> A =\= B, kill(MState)
4246 ; fd_get(B, BD0, BExp0),
4247 domain_remove(BD0, A, BD1),
4248 kill(MState),
4249 fd_put(B, BD1, BExp0)
4250 )
4251 ; nonvar(B) -> run_propagator(pneq(B, A), MState)
4252 ; A \== B,
4253 fd_get(A, _, AI, AS, _), fd_get(B, _, BI, BS, _),
4254 ( AS cis_lt BI -> kill(MState)
4255 ; AI cis_gt BS -> kill(MState)
4256 ; true
4257 )
4258 ).
4259
4261run_propagator(pgeq(A,B), MState) :-
4262 ( A == B -> kill(MState)
4263 ; nonvar(A) ->
4264 ( nonvar(B) -> kill(MState), A >= B
4265 ; fd_get(B, BD, BPs),
4266 domain_remove_greater_than(BD, A, BD1),
4267 kill(MState),
4268 fd_put(B, BD1, BPs)
4269 )
4270 ; nonvar(B) ->
4271 fd_get(A, AD, APs),
4272 domain_remove_smaller_than(AD, B, AD1),
4273 kill(MState),
4274 fd_put(A, AD1, APs)
4275 ; fd_get(A, AD, AL, AU, APs),
4276 fd_get(B, _, BL, BU, _),
4277 AU cis_geq BL,
4278 ( AL cis_geq BU -> kill(MState)
4279 ; AU == BL -> kill(MState), A = B
4280 ; NAL cis max(AL,BL),
4281 domains_intersection(AD, from_to(NAL,AU), NAD),
4282 fd_put(A, NAD, APs),
4283 ( fd_get(B, BD2, BL2, BU2, BPs2) ->
4284 NBU cis min(BU2, AU),
4285 domains_intersection(BD2, from_to(BL2,NBU), NBD),
4286 fd_put(B, NBD, BPs2)
4287 ; true
4288 )
4289 )
4290 ).
4291
4293
4294run_propagator(rel_tuple(R, Tuple), MState) :-
4295 get_attr(R, clpfd_relation, Relation),
4296 ( ground(Tuple) -> kill(MState), memberchk(Tuple, Relation)
4297 ; relation_unifiable(Relation, Tuple, Us, false, Changed),
4298 Us = [_|_],
4299 ( Tuple = [First,Second], ( ground(First) ; ground(Second) ) ->
4300 kill(MState)
4301 ; true
4302 ),
4303 ( Us = [Single] -> kill(MState), Single = Tuple
4304 ; Changed ->
4305 put_attr(R, clpfd_relation, Us),
4306 disable_queue,
4307 tuple_domain(Tuple, Us),
4308 enable_queue
4309 ; true
4310 )
4311 ).
4312
4314
4315run_propagator(pserialized(S_I, D_I, S_J, D_J, _), MState) :-
4316 ( nonvar(S_I), nonvar(S_J) ->
4317 kill(MState),
4318 ( S_I + D_I =< S_J -> true
4319 ; S_J + D_J =< S_I -> true
4320 ; false
4321 )
4322 ; serialize_lower_upper(S_I, D_I, S_J, D_J, MState),
4323 serialize_lower_upper(S_J, D_J, S_I, D_I, MState)
4324 ).
4325
4327
4329run_propagator(absdiff_neq(X,Y,C), MState) :-
4330 ( C < 0 -> kill(MState)
4331 ; nonvar(X) ->
4332 kill(MState),
4333 ( nonvar(Y) -> abs(X - Y) =\= C
4334 ; V1 is X - C, neq_num(Y, V1),
4335 V2 is C + X, neq_num(Y, V2)
4336 )
4337 ; nonvar(Y) -> kill(MState),
4338 V1 is C + Y, neq_num(X, V1),
4339 V2 is Y - C, neq_num(X, V2)
4340 ; true
4341 ).
4342
4344run_propagator(absdiff_geq(X,Y,C), MState) :-
4345 ( C =< 0 -> kill(MState)
4346 ; nonvar(X) ->
4347 kill(MState),
4348 ( nonvar(Y) -> abs(X-Y) >= C
4349 ; P1 is X - C, P2 is X + C,
4350 Y in inf..P1 \/ P2..sup
4351 )
4352 ; nonvar(Y) ->
4353 kill(MState),
4354 P1 is Y - C, P2 is Y + C,
4355 X in inf..P1 \/ P2..sup
4356 ; true
4357 ).
4358
4360run_propagator(x_neq_y_plus_z(X,Y,Z), MState) :-
4361 ( nonvar(X) ->
4362 ( nonvar(Y) ->
4363 ( nonvar(Z) -> kill(MState), X =\= Y + Z
4364 ; kill(MState), XY is X - Y, neq_num(Z, XY)
4365 )
4366 ; nonvar(Z) -> kill(MState), XZ is X - Z, neq_num(Y, XZ)
4367 ; true
4368 )
4369 ; nonvar(Y) ->
4370 ( nonvar(Z) ->
4371 kill(MState), YZ is Y + Z, neq_num(X, YZ)
4372 ; Y =:= 0 -> kill(MState), neq(X, Z)
4373 ; true
4374 )
4375 ; Z == 0 -> kill(MState), neq(X, Y)
4376 ; true
4377 ).
4378
4380run_propagator(x_leq_y_plus_c(X,Y,C), MState) :-
4381 ( nonvar(X) ->
4382 ( nonvar(Y) -> kill(MState), X =< Y + C
4383 ; kill(MState),
4384 R is X - C,
4385 fd_get(Y, YD, YPs),
4386 domain_remove_smaller_than(YD, R, YD1),
4387 fd_put(Y, YD1, YPs)
4388 )
4389 ; nonvar(Y) ->
4390 kill(MState),
4391 R is Y + C,
4392 fd_get(X, XD, XPs),
4393 domain_remove_greater_than(XD, R, XD1),
4394 fd_put(X, XD1, XPs)
4395 ; ( X == Y -> C >= 0, kill(MState)
4396 ; fd_get(Y, YD, _),
4397 ( domain_supremum(YD, n(YSup)) ->
4398 YS1 is YSup + C,
4399 fd_get(X, XD, XPs),
4400 domain_remove_greater_than(XD, YS1, XD1),
4401 fd_put(X, XD1, XPs)
4402 ; true
4403 ),
4404 ( fd_get(X, XD2, _), domain_infimum(XD2, n(XInf)) ->
4405 XI1 is XInf - C,
4406 ( fd_get(Y, YD1, YPs1) ->
4407 domain_remove_smaller_than(YD1, XI1, YD2),
4408 ( domain_infimum(YD2, n(YInf)),
4409 domain_supremum(XD2, n(XSup)),
4410 XSup =< YInf + C ->
4411 kill(MState)
4412 ; true
4413 ),
4414 fd_put(Y, YD2, YPs1)
4415 ; true
4416 )
4417 ; true
4418 )
4419 )
4420 ).
4421
4422run_propagator(scalar_product_neq(Cs0,Vs0,P0), MState) :-
4423 coeffs_variables_const(Cs0, Vs0, Cs, Vs, 0, I),
4424 P is P0 - I,
4425 ( Vs = [] -> kill(MState), P =\= 0
4426 ; Vs = [V], Cs = [C] ->
4427 kill(MState),
4428 ( C =:= 1 -> neq_num(V, P)
4429 ; C*V #\= P
4430 )
4431 ; Cs == [1,-1] -> kill(MState), Vs = [A,B], x_neq_y_plus_z(A, B, P)
4432 ; Cs == [-1,1] -> kill(MState), Vs = [A,B], x_neq_y_plus_z(B, A, P)
4433 ; P =:= 0, Cs = [1,1,-1] ->
4434 kill(MState), Vs = [A,B,C], x_neq_y_plus_z(C, A, B)
4435 ; P =:= 0, Cs = [1,-1,1] ->
4436 kill(MState), Vs = [A,B,C], x_neq_y_plus_z(B, A, C)
4437 ; P =:= 0, Cs = [-1,1,1] ->
4438 kill(MState), Vs = [A,B,C], x_neq_y_plus_z(A, B, C)
4439 ; true
4440 ).
4441
4442run_propagator(scalar_product_leq(Cs0,Vs0,P0), MState) :-
4443 coeffs_variables_const(Cs0, Vs0, Cs, Vs, 0, I),
4444 P is P0 - I,
4445 ( Vs = [] -> kill(MState), P >= 0
4446 ; sum_finite_domains(Cs, Vs, Infs, Sups, 0, 0, Inf, Sup),
4447 D1 is P - Inf,
4448 disable_queue,
4449 ( Infs == [], Sups == [] ->
4450 Inf =< P,
4451 ( Sup =< P -> kill(MState)
4452 ; remove_dist_upper_leq(Cs, Vs, D1)
4453 )
4454 ; Infs == [] -> Inf =< P, remove_dist_upper(Sups, D1)
4455 ; Sups = [_], Infs = [_] ->
4456 remove_upper(Infs, D1)
4457 ; Infs = [_] -> remove_upper(Infs, D1)
4458 ; true
4459 ),
4460 enable_queue
4461 ).
4462
4463run_propagator(scalar_product_eq(Cs0,Vs0,P0), MState) :-
4464 coeffs_variables_const(Cs0, Vs0, Cs, Vs, 0, I),
4465 P is P0 - I,
4466 ( Vs = [] -> kill(MState), P =:= 0
4467 ; Vs = [V], Cs = [C] -> kill(MState), P mod C =:= 0, V is P // C
4468 ; Cs == [1,1] -> kill(MState), Vs = [A,B], A + B #= P
4469 ; Cs == [1,-1] -> kill(MState), Vs = [A,B], A #= P + B
4470 ; Cs == [-1,1] -> kill(MState), Vs = [A,B], B #= P + A
4471 ; Cs == [-1,-1] -> kill(MState), Vs = [A,B], P1 is -P, A + B #= P1
4472 ; P =:= 0, Cs == [1,1,-1] -> kill(MState), Vs = [A,B,C], A + B #= C
4473 ; P =:= 0, Cs == [1,-1,1] -> kill(MState), Vs = [A,B,C], A + C #= B
4474 ; P =:= 0, Cs == [-1,1,1] -> kill(MState), Vs = [A,B,C], B + C #= A
4475 ; sum_finite_domains(Cs, Vs, Infs, Sups, 0, 0, Inf, Sup),
4476 4477 D1 is P - Inf,
4478 D2 is Sup - P,
4479 disable_queue,
4480 ( Infs == [], Sups == [] ->
4481 between(Inf, Sup, P),
4482 remove_dist_upper_lower(Cs, Vs, D1, D2)
4483 ; Sups = [] -> P =< Sup, remove_dist_lower(Infs, D2)
4484 ; Infs = [] -> Inf =< P, remove_dist_upper(Sups, D1)
4485 ; Sups = [_], Infs = [_] ->
4486 remove_lower(Sups, D2),
4487 remove_upper(Infs, D1)
4488 ; Infs = [_] -> remove_upper(Infs, D1)
4489 ; Sups = [_] -> remove_lower(Sups, D2)
4490 ; true
4491 ),
4492 enable_queue
4493 ).
4494
4496run_propagator(pplus(X,Y,Z), MState) :-
4497 ( nonvar(X) ->
4498 ( X =:= 0 -> kill(MState), Y = Z
4499 ; Y == Z -> kill(MState), X =:= 0
4500 ; nonvar(Y) -> kill(MState), Z is X + Y
4501 ; nonvar(Z) -> kill(MState), Y is Z - X
4502 ; fd_get(Z, ZD, ZPs),
4503 fd_get(Y, YD, _),
4504 domain_shift(YD, X, Shifted_YD),
4505 domains_intersection(ZD, Shifted_YD, ZD1),
4506 fd_put(Z, ZD1, ZPs),
4507 ( fd_get(Y, YD1, YPs) ->
4508 O is -X,
4509 domain_shift(ZD1, O, YD2),
4510 domains_intersection(YD1, YD2, YD3),
4511 fd_put(Y, YD3, YPs)
4512 ; true
4513 )
4514 )
4515 ; nonvar(Y) -> run_propagator(pplus(Y,X,Z), MState)
4516 ; nonvar(Z) ->
4517 ( X == Y -> kill(MState), even(Z), X is Z // 2
4518 ; fd_get(X, XD, _),
4519 fd_get(Y, YD, YPs),
4520 domain_negate(XD, XDN),
4521 domain_shift(XDN, Z, YD1),
4522 domains_intersection(YD, YD1, YD2),
4523 fd_put(Y, YD2, YPs),
4524 ( fd_get(X, XD1, XPs) ->
4525 domain_negate(YD2, YD2N),
4526 domain_shift(YD2N, Z, XD2),
4527 domains_intersection(XD1, XD2, XD3),
4528 fd_put(X, XD3, XPs)
4529 ; true
4530 )
4531 )
4532 ; ( X == Y -> kill(MState), 2*X #= Z
4533 ; X == Z -> kill(MState), Y = 0
4534 ; Y == Z -> kill(MState), X = 0
4535 ; fd_get(X, XD, XL, XU, XPs),
4536 fd_get(Y, _, YL, YU, _),
4537 fd_get(Z, _, ZL, ZU, _),
4538 NXL cis max(XL, ZL-YU),
4539 NXU cis min(XU, ZU-YL),
4540 update_bounds(X, XD, XPs, XL, XU, NXL, NXU),
4541 ( fd_get(Y, YD2, YL2, YU2, YPs2) ->
4542 NYL cis max(YL2, ZL-NXU),
4543 NYU cis min(YU2, ZU-NXL),
4544 update_bounds(Y, YD2, YPs2, YL2, YU2, NYL, NYU)
4545 ; NYL = n(Y), NYU = n(Y)
4546 ),
4547 ( fd_get(Z, ZD2, ZL2, ZU2, ZPs2) ->
4548 NZL cis max(ZL2,NXL+NYL),
4549 NZU cis min(ZU2,NXU+NYU),
4550 update_bounds(Z, ZD2, ZPs2, ZL2, ZU2, NZL, NZU)
4551 ; true
4552 )
4553 )
4554 ).
4555
4557
4558run_propagator(ptimes(X,Y,Z), MState) :-
4559 ( nonvar(X) ->
4560 ( nonvar(Y) -> kill(MState), Z is X * Y
4561 ; X =:= 0 -> kill(MState), Z = 0
4562 ; X =:= 1 -> kill(MState), Z = Y
4563 ; nonvar(Z) -> kill(MState), 0 =:= Z mod X, Y is Z // X
4564 ; ( Y == Z -> kill(MState), Y = 0
4565 ; fd_get(Y, YD, _),
4566 fd_get(Z, ZD, ZPs),
4567 domain_expand(YD, X, Scaled_YD),
4568 domains_intersection(ZD, Scaled_YD, ZD1),
4569 fd_put(Z, ZD1, ZPs),
4570 ( fd_get(Y, YDom2, YPs2) ->
4571 domain_contract(ZD1, X, Contract),
4572 domains_intersection(YDom2, Contract, NYDom),
4573 fd_put(Y, NYDom, YPs2)
4574 ; kill(MState), Z is X * Y
4575 )
4576 )
4577 )
4578 ; nonvar(Y) -> run_propagator(ptimes(Y,X,Z), MState)
4579 ; nonvar(Z) ->
4580 ( X == Y ->
4581 kill(MState),
4582 integer_kth_root(Z, 2, R),
4583 NR is -R,
4584 X in NR \/ R
4585 ; fd_get(X, XD, XL, XU, XPs),
4586 fd_get(Y, YD, YL, YU, _),
4587 min_max_factor(n(Z), n(Z), YL, YU, XL, XU, NXL, NXU),
4588 update_bounds(X, XD, XPs, XL, XU, NXL, NXU),
4589 ( fd_get(Y, YD2, YL2, YU2, YPs2) ->
4590 min_max_factor(n(Z), n(Z), NXL, NXU, YL2, YU2, NYL, NYU),
4591 update_bounds(Y, YD2, YPs2, YL2, YU2, NYL, NYU)
4592 ; ( Y =\= 0 -> 0 =:= Z mod Y, kill(MState), X is Z // Y
4593 ; kill(MState), Z = 0
4594 )
4595 ),
4596 ( Z =:= 0 ->
4597 ( \+ domain_contains(XD, 0) -> kill(MState), Y = 0
4598 ; \+ domain_contains(YD, 0) -> kill(MState), X = 0
4599 ; true
4600 )
4601 ; neq_num(X, 0), neq_num(Y, 0)
4602 )
4603 )
4604 ; ( X == Y -> kill(MState), X^2 #= Z
4605 ; fd_get(X, XD, XL, XU, XPs),
4606 fd_get(Y, _, YL, YU, _),
4607 fd_get(Z, ZD, ZL, ZU, _),
4608 ( Y == Z, \+ domain_contains(ZD, 0) -> kill(MState), X = 1
4609 ; X == Z, \+ domain_contains(ZD, 0) -> kill(MState), Y = 1
4610 ; min_max_factor(ZL, ZU, YL, YU, XL, XU, NXL, NXU),
4611 update_bounds(X, XD, XPs, XL, XU, NXL, NXU),
4612 ( fd_get(Y, YD2, YL2, YU2, YPs2) ->
4613 min_max_factor(ZL, ZU, NXL, NXU, YL2, YU2, NYL, NYU),
4614 update_bounds(Y, YD2, YPs2, YL2, YU2, NYL, NYU)
4615 ; NYL = n(Y), NYU = n(Y)
4616 ),
4617 ( fd_get(Z, ZD2, ZL2, ZU2, ZPs2) ->
4618 min_product(NXL, NXU, NYL, NYU, NZL),
4619 max_product(NXL, NXU, NYL, NYU, NZU),
4620 ( NZL cis_leq ZL2, NZU cis_geq ZU2 -> ZD3 = ZD2
4621 ; domains_intersection(ZD2, from_to(NZL,NZU), ZD3),
4622 fd_put(Z, ZD3, ZPs2)
4623 ),
4624 ( domain_contains(ZD3, 0) -> true
4625 ; neq_num(X, 0), neq_num(Y, 0)
4626 )
4627 ; true
4628 )
4629 )
4630 )
4631 ).
4632
4634
4636run_propagator(pdiv(X,Y,Z), MState) :-
4637 ( nonvar(X) ->
4638 ( nonvar(Y) -> kill(MState), Y =\= 0, Z is X div Y
4639 ; fd_get(Y, YD, YL, YU, YPs),
4640 ( nonvar(Z) ->
4641 ( Z =:= 0 ->
4642 ( X =:= 0 -> NI = split(0, from_to(inf,n(-1)),
4643 from_to(n(1),sup))
4644 ; NY_ is X+sign(X),
4645 ( X > 0 -> NI = from_to(n(NY_), sup)
4646 ; NI = from_to(inf, n(NY_))
4647 )
4648 ),
4649 domains_intersection(YD, NI, NYD),
4650 fd_put(Y, NYD, YPs)
4651 ; ( sign(X) =:= 1 ->
4652 NYL cis max(div(n(X)*n(Z), n(Z)*(n(Z)+n(1))) + n(1), YL),
4653 NYU cis min(div(n(X), n(Z)), YU)
4654 ; NYL cis max(-(div(-n(X), n(Z))), YL),
4655 NYU cis min(-(div(-n(X)*n(Z), (n(Z)*(n(Z)+n(1))))) - n(1), YU)
4656 ),
4657 update_bounds(Y, YD, YPs, YL, YU, NYL, NYU)
4658 )
4659 ; fd_get(Z, ZD, ZL, ZU, ZPs),
4660 ( X >= 0, ( YL cis_gt n(0) ; YU cis_lt n(0) )->
4661 NZL cis max(div(n(X), YU), ZL),
4662 NZU cis min(div(n(X), YL), ZU)
4663 ; X < 0, ( YL cis_gt n(0) ; YU cis_lt n(0) ) ->
4664 NZL cis max(div(n(X), YL), ZL),
4665 NZU cis min(div(n(X), YU), ZU)
4666 ; 4667 NZL cis max(-abs(n(X)), ZL),
4668 NZU cis min(abs(n(X)), ZU)
4669 ),
4670 update_bounds(Z, ZD, ZPs, ZL, ZU, NZL, NZU),
4671 ( X >= 0, NZL cis_gt n(0), fd_get(Y, YD1, YPs1) ->
4672 NYL cis div(n(X), (NZU + n(1))) + n(1),
4673 NYU cis div(n(X), NZL),
4674 domains_intersection(YD1, from_to(NYL, NYU), NYD1),
4675 fd_put(Y, NYD1, YPs1)
4676 ; 4677 true
4678 )
4679 )
4680 )
4681 ; nonvar(Y) ->
4682 Y =\= 0,
4683 ( Y =:= 1 -> kill(MState), X = Z
4684 ; Y =:= -1 -> kill(MState), Z #= -X
4685 ; fd_get(X, XD, XL, XU, XPs),
4686 ( nonvar(Z) ->
4687 kill(MState),
4688 ( Y > 0 ->
4689 NXL cis max(n(Z)*n(Y), XL),
4690 NXU cis min((n(Z)+n(1))*n(Y)-n(1), XU)
4691 ; NXL cis max((n(Z)+n(1))*n(Y)+n(1), XL),
4692 NXU cis min(n(Z)*n(Y), XU)
4693 ),
4694 update_bounds(X, XD, XPs, XL, XU, NXL, NXU)
4695 ; fd_get(Z, ZD, ZPs),
4696 domain_contract_less(XD, Y, div, Contracted),
4697 domains_intersection(ZD, Contracted, NZD),
4698 fd_put(Z, NZD, ZPs),
4699 ( fd_get(X, XD2, XPs2) ->
4700 domain_expand_more(NZD, Y, div, Expanded),
4701 domains_intersection(XD2, Expanded, NXD2),
4702 fd_put(X, NXD2, XPs2)
4703 ; true
4704 )
4705 )
4706 )
4707 ; nonvar(Z) ->
4708 fd_get(X, XD, XL, XU, XPs),
4709 fd_get(Y, _, YL, YU, _),
4710 ( YL cis_geq n(0), XL cis_geq n(0) ->
4711 NXL cis max(YL*n(Z), XL),
4712 NXU cis min(YU*(n(Z)+n(1))-n(1), XU)
4713 ; 4714 NXL = XL, NXU = XU
4715 ),
4716 update_bounds(X, XD, XPs, XL, XU, NXL, NXU)
4717 ; ( X == Y -> kill(MState), Z = 1
4718 ; fd_get(X, _, XL, XU, _),
4719 fd_get(Y, _, YL, _, _),
4720 fd_get(Z, ZD, ZPs),
4721 NZU cis max(abs(XL), XU),
4722 NZL cis -NZU,
4723 domains_intersection(ZD, from_to(NZL,NZU), NZD0),
4724 ( XL cis_geq n(0), YL cis_geq n(0) ->
4725 domain_remove_smaller_than(NZD0, 0, NZD1)
4726 ; 4727 NZD1 = NZD0
4728 ),
4729 fd_put(Z, NZD1, ZPs)
4730 )
4731 ).
4732
4734run_propagator(prdiv(X,Y,Z), MState) :- kill(MState), Z*Y #= X.
4735
4737run_propagator(ptzdiv(X,Y,Z), MState) :-
4738 ( nonvar(X) ->
4739 ( nonvar(Y) -> kill(MState), Y =\= 0, Z is X // Y
4740 ; fd_get(Y, YD, YL, YU, YPs),
4741 ( nonvar(Z) ->
4742 ( Z =:= 0 ->
4743 NYL is -abs(X) - 1,
4744 NYU is abs(X) + 1,
4745 domains_intersection(YD, split(0, from_to(inf,n(NYL)),
4746 from_to(n(NYU), sup)),
4747 NYD),
4748 fd_put(Y, NYD, YPs)
4749 ; ( sign(X) =:= sign(Z) ->
4750 NYL cis max(n(X) // (n(Z)+sign(n(Z))) + n(1), YL),
4751 NYU cis min(n(X) // n(Z), YU)
4752 ; NYL cis max(n(X) // n(Z), YL),
4753 NYU cis min(n(X) // (n(Z)+sign(n(Z))) - n(1), YU)
4754 ),
4755 update_bounds(Y, YD, YPs, YL, YU, NYL, NYU)
4756 )
4757 ; fd_get(Z, ZD, ZL, ZU, ZPs),
4758 ( X >= 0, ( YL cis_gt n(0) ; YU cis_lt n(0) )->
4759 NZL cis max(n(X)//YU, ZL),
4760 NZU cis min(n(X)//YL, ZU)
4761 ; X < 0, ( YL cis_gt n(0) ; YU cis_lt n(0) ) ->
4762 NZL cis max(n(X)//YL, ZL),
4763 NZU cis min(n(X)//YU, ZU)
4764 ; 4765 NZL cis max(-abs(n(X)), ZL),
4766 NZU cis min(abs(n(X)), ZU)
4767 ),
4768 update_bounds(Z, ZD, ZPs, ZL, ZU, NZL, NZU),
4769 ( X >= 0, NZL cis_gt n(0), fd_get(Y, YD1, YPs1) ->
4770 NYL cis n(X) // (NZU + n(1)) + n(1),
4771 NYU cis n(X) // NZL,
4772 domains_intersection(YD1, from_to(NYL, NYU), NYD1),
4773 fd_put(Y, NYD1, YPs1)
4774 ; 4775 true
4776 )
4777 )
4778 )
4779 ; nonvar(Y) ->
4780 Y =\= 0,
4781 ( Y =:= 1 -> kill(MState), X = Z
4782 ; Y =:= -1 -> kill(MState), Z #= -X
4783 ; fd_get(X, XD, XL, XU, XPs),
4784 ( nonvar(Z) ->
4785 kill(MState),
4786 ( sign(Z) =:= sign(Y) ->
4787 NXL cis max(n(Z)*n(Y), XL),
4788 NXU cis min((abs(n(Z))+n(1))*abs(n(Y))-n(1), XU)
4789 ; Z =:= 0 ->
4790 NXL cis max(-abs(n(Y)) + n(1), XL),
4791 NXU cis min(abs(n(Y)) - n(1), XU)
4792 ; NXL cis max((n(Z)+sign(n(Z)))*n(Y)+n(1), XL),
4793 NXU cis min(n(Z)*n(Y), XU)
4794 ),
4795 update_bounds(X, XD, XPs, XL, XU, NXL, NXU)
4796 ; fd_get(Z, ZD, ZPs),
4797 domain_contract_less(XD, Y, //, Contracted),
4798 domains_intersection(ZD, Contracted, NZD),
4799 fd_put(Z, NZD, ZPs),
4800 ( fd_get(X, XD2, XPs2) ->
4801 domain_expand_more(NZD, Y, //, Expanded),
4802 domains_intersection(XD2, Expanded, NXD2),
4803 fd_put(X, NXD2, XPs2)
4804 ; true
4805 )
4806 )
4807 )
4808 ; nonvar(Z) ->
4809 fd_get(X, XD, XL, XU, XPs),
4810 fd_get(Y, _, YL, YU, _),
4811 ( YL cis_geq n(0), XL cis_geq n(0) ->
4812 NXL cis max(YL*n(Z), XL),
4813 NXU cis min(YU*(n(Z)+n(1))-n(1), XU)
4814 ; 4815 NXL = XL, NXU = XU
4816 ),
4817 update_bounds(X, XD, XPs, XL, XU, NXL, NXU)
4818 ; ( X == Y -> kill(MState), Z = 1
4819 ; fd_get(X, _, XL, XU, _),
4820 fd_get(Y, _, YL, _, _),
4821 fd_get(Z, ZD, ZPs),
4822 NZU cis max(abs(XL), XU),
4823 NZL cis -NZU,
4824 domains_intersection(ZD, from_to(NZL,NZU), NZD0),
4825 ( XL cis_geq n(0), YL cis_geq n(0) ->
4826 domain_remove_smaller_than(NZD0, 0, NZD1)
4827 ; 4828 NZD1 = NZD0
4829 ),
4830 fd_put(Z, NZD1, ZPs)
4831 )
4832 ).
4833
4834
4837
4838run_propagator(pabs(X,Y), MState) :-
4839 ( nonvar(X) -> kill(MState), Y is abs(X)
4840 ; nonvar(Y) ->
4841 kill(MState),
4842 Y >= 0,
4843 YN is -Y,
4844 X in YN \/ Y
4845 ; fd_get(X, XD, XPs),
4846 fd_get(Y, YD, _),
4847 domain_negate(YD, YDNegative),
4848 domains_union(YD, YDNegative, XD1),
4849 domains_intersection(XD, XD1, XD2),
4850 fd_put(X, XD2, XPs),
4851 ( fd_get(Y, YD1, YPs1) ->
4852 domain_negate(XD2, XD2Neg),
4853 domains_union(XD2, XD2Neg, YD2),
4854 domain_remove_smaller_than(YD2, 0, YD3),
4855 domains_intersection(YD1, YD3, YD4),
4856 fd_put(Y, YD4, YPs1)
4857 ; true
4858 )
4859 ).
4862
4863run_propagator(pmod(X,Y,Z), MState) :-
4864 ( nonvar(X) ->
4865 ( nonvar(Y) -> kill(MState), Y =\= 0, Z is X mod Y
4866 ; true
4867 )
4868 ; nonvar(Y) ->
4869 Y =\= 0,
4870 ( abs(Y) =:= 1 -> kill(MState), Z = 0
4871 ; var(Z) ->
4872 YP is abs(Y) - 1,
4873 ( Y > 0, fd_get(X, _, n(XL), n(XU), _) ->
4874 ( XL >= 0, XU < Y ->
4875 kill(MState), Z = X, ZL = XL, ZU = XU
4876 ; ZL = 0, ZU = YP
4877 )
4878 ; Y > 0 -> ZL = 0, ZU = YP
4879 ; YN is -YP, ZL = YN, ZU = 0
4880 ),
4881 ( fd_get(Z, ZD, ZPs) ->
4882 domains_intersection(ZD, from_to(n(ZL), n(ZU)), ZD1),
4883 domain_infimum(ZD1, n(ZMin)),
4884 domain_supremum(ZD1, n(ZMax)),
4885 fd_put(Z, ZD1, ZPs)
4886 ; ZMin = Z, ZMax = Z
4887 ),
4888 ( fd_get(X, XD, XPs), domain_infimum(XD, n(XMin)) ->
4889 Z1 is XMin mod Y,
4890 ( between(ZMin, ZMax, Z1) -> true
4891 ; Y > 0 ->
4892 Next is ((XMin - ZMin + Y - 1) div Y)*Y + ZMin,
4893 domain_remove_smaller_than(XD, Next, XD1),
4894 fd_put(X, XD1, XPs)
4895 ; neq_num(X, XMin)
4896 )
4897 ; true
4898 ),
4899 ( fd_get(X, XD2, XPs2), domain_supremum(XD2, n(XMax)) ->
4900 Z2 is XMax mod Y,
4901 ( between(ZMin, ZMax, Z2) -> true
4902 ; Y > 0 ->
4903 Prev is ((XMax - ZMin) div Y)*Y + ZMax,
4904 domain_remove_greater_than(XD2, Prev, XD3),
4905 fd_put(X, XD3, XPs2)
4906 ; neq_num(X, XMax)
4907 )
4908 ; true
4909 )
4910 ; fd_get(X, XD, XPs),
4911 4912 ( domain_infimum(XD, n(Min)) ->
4913 ( Min mod Y =:= Z -> true
4914 ; Y > 0 ->
4915 Next is ((Min - Z + Y - 1) div Y)*Y + Z,
4916 domain_remove_smaller_than(XD, Next, XD1),
4917 fd_put(X, XD1, XPs)
4918 ; neq_num(X, Min)
4919 )
4920 ; true
4921 ),
4922 ( fd_get(X, XD2, XPs2) ->
4923 ( domain_supremum(XD2, n(Max)) ->
4924 ( Max mod Y =:= Z -> true
4925 ; Y > 0 ->
4926 Prev is ((Max - Z) div Y)*Y + Z,
4927 domain_remove_greater_than(XD2, Prev, XD3),
4928 fd_put(X, XD3, XPs2)
4929 ; neq_num(X, Max)
4930 )
4931 ; true
4932 )
4933 ; true
4934 )
4935 )
4936 ; X == Y -> kill(MState), Z = 0
4937 ; true 4938 ).
4939
4942
4943run_propagator(prem(X,Y,Z), MState) :-
4944 ( nonvar(X) ->
4945 ( nonvar(Y) -> kill(MState), Y =\= 0, Z is X rem Y
4946 ; U is abs(X),
4947 fd_get(Y, YD, _),
4948 ( X >=0, domain_infimum(YD, n(Min)), Min >= 0 -> L = 0
4949 ; L is -U
4950 ),
4951 Z in L..U
4952 )
4953 ; nonvar(Y) ->
4954 Y =\= 0,
4955 ( abs(Y) =:= 1 -> kill(MState), Z = 0
4956 ; var(Z) ->
4957 YP is abs(Y) - 1,
4958 YN is -YP,
4959 ( Y > 0, fd_get(X, _, n(XL), n(XU), _) ->
4960 ( abs(XL) < Y, XU < Y -> kill(MState), Z = X, ZL = XL
4961 ; XL < 0, abs(XL) < Y -> ZL = XL
4962 ; XL >= 0 -> ZL = 0
4963 ; ZL = YN
4964 ),
4965 ( XU > 0, XU < Y -> ZU = XU
4966 ; XU < 0 -> ZU = 0
4967 ; ZU = YP
4968 )
4969 ; ZL = YN, ZU = YP
4970 ),
4971 ( fd_get(Z, ZD, ZPs) ->
4972 domains_intersection(ZD, from_to(n(ZL), n(ZU)), ZD1),
4973 fd_put(Z, ZD1, ZPs)
4974 ; ZD1 = from_to(n(Z), n(Z))
4975 ),
4976 ( fd_get(X, XD, _), domain_infimum(XD, n(Min)) ->
4977 Z1 is Min rem Y,
4978 ( domain_contains(ZD1, Z1) -> true
4979 ; neq_num(X, Min)
4980 )
4981 ; true
4982 ),
4983 ( fd_get(X, XD1, _), domain_supremum(XD1, n(Max)) ->
4984 Z2 is Max rem Y,
4985 ( domain_contains(ZD1, Z2) -> true
4986 ; neq_num(X, Max)
4987 )
4988 ; true
4989 )
4990 ; fd_get(X, XD1, XPs1),
4991 4992 ( domain_infimum(XD1, n(Min)) ->
4993 ( Min rem Y =:= Z -> true
4994 ; Y > 0, Min > 0 ->
4995 Next is ((Min - Z + Y - 1) div Y)*Y + Z,
4996 domain_remove_smaller_than(XD1, Next, XD2),
4997 fd_put(X, XD2, XPs1)
4998 ; 4999 neq_num(X, Min)
5000 )
5001 ; true
5002 ),
5003 ( fd_get(X, XD3, XPs3) ->
5004 ( domain_supremum(XD3, n(Max)) ->
5005 ( Max rem Y =:= Z -> true
5006 ; Y > 0, Max > 0 ->
5007 Prev is ((Max - Z) div Y)*Y + Z,
5008 domain_remove_greater_than(XD3, Prev, XD4),
5009 fd_put(X, XD4, XPs3)
5010 ; 5011 neq_num(X, Max)
5012 )
5013 ; true
5014 )
5015 ; true
5016 )
5017 )
5018 ; X == Y -> kill(MState), Z = 0
5019 ; fd_get(Z, ZD, ZPs) ->
5020 fd_get(Y, _, YInf, YSup, _),
5021 fd_get(X, _, XInf, XSup, _),
5022 M cis max(abs(YInf),YSup),
5023 ( XInf cis_geq n(0) -> Inf0 = n(0)
5024 ; Inf0 = XInf
5025 ),
5026 ( XSup cis_leq n(0) -> Sup0 = n(0)
5027 ; Sup0 = XSup
5028 ),
5029 NInf cis max(max(Inf0, -M + n(1)), min(XInf,-XSup)),
5030 NSup cis min(min(Sup0, M - n(1)), max(abs(XInf),XSup)),
5031 domains_intersection(ZD, from_to(NInf,NSup), ZD1),
5032 fd_put(Z, ZD1, ZPs)
5033 ; true 5034 ).
5035
5038
5039run_propagator(pmax(X,Y,Z), MState) :-
5040 ( nonvar(X) ->
5041 ( nonvar(Y) -> kill(MState), Z is max(X,Y)
5042 ; nonvar(Z) ->
5043 ( Z =:= X -> kill(MState), X #>= Y
5044 ; Z > X -> Z = Y
5045 ; false 5046 )
5047 ; fd_get(Y, _, YInf, YSup, _),
5048 ( YInf cis_gt n(X) -> Z = Y
5049 ; YSup cis_lt n(X) -> Z = X
5050 ; YSup = n(M) ->
5051 fd_get(Z, ZD, ZPs),
5052 domain_remove_greater_than(ZD, M, ZD1),
5053 fd_put(Z, ZD1, ZPs)
5054 ; true
5055 )
5056 )
5057 ; nonvar(Y) -> run_propagator(pmax(Y,X,Z), MState)
5058 ; fd_get(Z, ZD, ZPs) ->
5059 fd_get(X, _, XInf, XSup, _),
5060 fd_get(Y, _, YInf, YSup, _),
5061 ( YInf cis_gt YSup -> kill(MState), Z = Y
5062 ; YSup cis_lt XInf -> kill(MState), Z = X
5063 ; n(M) cis max(XSup, YSup) ->
5064 domain_remove_greater_than(ZD, M, ZD1),
5065 fd_put(Z, ZD1, ZPs)
5066 ; true
5067 )
5068 ; true
5069 ).
5070
5073
5074run_propagator(pmin(X,Y,Z), MState) :-
5075 ( nonvar(X) ->
5076 ( nonvar(Y) -> kill(MState), Z is min(X,Y)
5077 ; nonvar(Z) ->
5078 ( Z =:= X -> kill(MState), X #=< Y
5079 ; Z < X -> Z = Y
5080 ; false 5081 )
5082 ; fd_get(Y, _, YInf, YSup, _),
5083 ( YSup cis_lt n(X) -> Z = Y
5084 ; YInf cis_gt n(X) -> Z = X
5085 ; YInf = n(M) ->
5086 fd_get(Z, ZD, ZPs),
5087 domain_remove_smaller_than(ZD, M, ZD1),
5088 fd_put(Z, ZD1, ZPs)
5089 ; true
5090 )
5091 )
5092 ; nonvar(Y) -> run_propagator(pmin(Y,X,Z), MState)
5093 ; fd_get(Z, ZD, ZPs) ->
5094 fd_get(X, _, XInf, XSup, _),
5095 fd_get(Y, _, YInf, YSup, _),
5096 ( YSup cis_lt YInf -> kill(MState), Z = Y
5097 ; YInf cis_gt XSup -> kill(MState), Z = X
5098 ; n(M) cis min(XInf, YInf) ->
5099 domain_remove_smaller_than(ZD, M, ZD1),
5100 fd_put(Z, ZD1, ZPs)
5101 ; true
5102 )
5103 ; true
5104 ).
5107
5108run_propagator(pexp(X,Y,Z), MState) :-
5109 ( X == 1 -> kill(MState), Z = 1
5110 ; X == 0 -> kill(MState), Z in 0..1, Z #<==> Y #= 0
5111 ; Y == 0 -> kill(MState), Z = 1
5112 ; Y == 1 -> kill(MState), Z = X
5113 ; nonvar(X) ->
5114 ( nonvar(Y) ->
5115 ( Y >= 0 -> true ; X =:= -1 ),
5116 kill(MState),
5117 Z is X^Y
5118 ; nonvar(Z) ->
5119 ( Z > 1 ->
5120 kill(MState),
5121 integer_log_b(Z, X, 1, Y)
5122 ; true
5123 )
5124 ; fd_get(Y, _, YL, YU, _),
5125 fd_get(Z, ZD, ZPs),
5126 ( X > 0, YL cis_geq n(0) ->
5127 NZL cis n(X)^YL,
5128 NZU cis n(X)^YU,
5129 domains_intersection(ZD, from_to(NZL,NZU), NZD),
5130 fd_put(Z, NZD, ZPs)
5131 ; true
5132 ),
5133 ( X > 0,
5134 fd_get(Z, _, _, n(ZMax), _),
5135 ZMax > 0 ->
5136 floor_integer_log_b(ZMax, X, 1, YCeil),
5137 Y in inf..YCeil
5138 ; true
5139 )
5140 )
5141 ; nonvar(Z) ->
5142 ( nonvar(Y) ->
5143 integer_kth_root(Z, Y, R),
5144 kill(MState),
5145 ( even(Y) ->
5146 N is -R,
5147 X in N \/ R
5148 ; X = R
5149 )
5150 ; fd_get(X, _, n(NXL), _, _), NXL > 1 ->
5151 ( Z > 1, between(NXL, Z, Exp), NXL^Exp > Z ->
5152 Exp1 is Exp - 1,
5153 fd_get(Y, YD, YPs),
5154 domains_intersection(YD, from_to(n(1),n(Exp1)), YD1),
5155 fd_put(Y, YD1, YPs),
5156 ( fd_get(X, XD, XPs) ->
5157 domain_infimum(YD1, n(YL)),
5158 integer_kth_root_leq(Z, YL, RU),
5159 domains_intersection(XD, from_to(n(NXL),n(RU)), XD1),
5160 fd_put(X, XD1, XPs)
5161 ; true
5162 )
5163 ; true
5164 )
5165 ; true
5166 )
5167 ; nonvar(Y), Y > 0 ->
5168 ( even(Y) ->
5169 geq(Z, 0)
5170 ; true
5171 ),
5172 ( fd_get(X, XD, XL, XU, _), fd_get(Z, ZD, ZL, ZU, ZPs) ->
5173 ( domain_contains(ZD, 0) -> XD1 = XD
5174 ; domain_remove(XD, 0, XD1)
5175 ),
5176 ( domain_contains(XD, 0) -> ZD1 = ZD
5177 ; domain_remove(ZD, 0, ZD1)
5178 ),
5179 ( even(Y) ->
5180 ( XL cis_geq n(0) ->
5181 NZL cis XL^n(Y)
5182 ; XU cis_leq n(0) ->
5183 NZL cis XU^n(Y)
5184 ; NZL = n(0)
5185 ),
5186 NZU cis max(abs(XL),abs(XU))^n(Y),
5187 domains_intersection(ZD1, from_to(NZL,NZU), ZD2)
5188 ; ( finite(XL) ->
5189 NZL cis XL^n(Y),
5190 NZU cis XU^n(Y),
5191 domains_intersection(ZD1, from_to(NZL,NZU), ZD2)
5192 ; ZD2 = ZD1
5193 )
5194 ),
5195 fd_put(Z, ZD2, ZPs),
5196 ( even(Y), ZU = n(Num) ->
5197 integer_kth_root_leq(Num, Y, RU),
5198 ( XL cis_geq n(0), ZL = n(Num1) ->
5199 integer_kth_root_leq(Num1, Y, RL0),
5200 ( RL0^Y < Num1 -> RL is RL0 + 1
5201 ; RL = RL0
5202 )
5203 ; RL is -RU
5204 ),
5205 RL =< RU,
5206 NXD = from_to(n(RL),n(RU))
5207 ; odd(Y), ZL cis_geq n(0), ZU = n(Num) ->
5208 integer_kth_root_leq(Num, Y, RU),
5209 ZL = n(Num1),
5210 integer_kth_root_leq(Num1, Y, RL0),
5211 ( RL0^Y < Num1 -> RL is RL0 + 1
5212 ; RL = RL0
5213 ),
5214 RL =< RU,
5215 NXD = from_to(n(RL),n(RU))
5216 ; NXD = XD1 5217 ),
5218 ( fd_get(X, XD2, XPs) ->
5219 domains_intersection(XD2, XD1, XD3),
5220 domains_intersection(XD3, NXD, XD4),
5221 fd_put(X, XD4, XPs)
5222 ; true
5223 )
5224 ; true
5225 )
5226 ; fd_get(X, _, XL, _, _),
5227 XL cis_gt n(0),
5228 fd_get(Y, _, YL, _, _),
5229 YL cis_gt n(0),
5230 fd_get(Z, ZD, ZPs) ->
5231 n(NZL) cis XL^YL,
5232 domain_remove_smaller_than(ZD, NZL, ZD1),
5233 fd_put(Z, ZD1, ZPs)
5234 ; true
5235 ).
5236
5239
5240run_propagator(pshift(X,Y,Z,S), MState) :-
5241 ( Y == 0 -> kill(MState), Z = X
5242 ; nonvar(X) ->
5243 ( nonvar(Y) -> kill(MState), Z is X << (Y*S)
5244 ; nonvar(Z) ->
5245 kill(MState),
5246 ( X =:= 0 -> Z =:= 0
5247 ; abs(Z) > abs(X) -> Z #= X * 2^(Y*S)
5248 ; X div (2^(-Y*S)) #= Z
5249 )
5250 ; 5251 true
5252 )
5253 ; nonvar(Y) ->
5254 kill(MState),
5255 ( Y*S > 0 -> Z #= X * 2^(Y*S)
5256 ; X div (2^(-Y*S)) #= Z
5257 )
5258 ; 5259 true
5260 ).
5261
5263run_propagator(pzcompare(Order, A, B), MState) :-
5264 ( A == B -> kill(MState), Order = (=)
5265 ; ( nonvar(A) ->
5266 ( nonvar(B) ->
5267 kill(MState),
5268 ( A > B -> Order = (>)
5269 ; Order = (<)
5270 )
5271 ; fd_get(B, _, BL, BU, _),
5272 ( BL cis_gt n(A) -> kill(MState), Order = (<)
5273 ; BU cis_lt n(A) -> kill(MState), Order = (>)
5274 ; true
5275 )
5276 )
5277 ; nonvar(B) ->
5278 fd_get(A, _, AL, AU, _),
5279 ( AL cis_gt n(B) -> kill(MState), Order = (>)
5280 ; AU cis_lt n(B) -> kill(MState), Order = (<)
5281 ; true
5282 )
5283 ; fd_get(A, _, AL, AU, _),
5284 fd_get(B, _, BL, BU, _),
5285 ( AL cis_gt BU -> kill(MState), Order = (>)
5286 ; AU cis_lt BL -> kill(MState), Order = (<)
5287 ; true
5288 )
5289 )
5290 ).
5291
5293
5295
5297
5298run_propagator(reified_in(V,Dom,B), MState) :-
5299 ( integer(V) ->
5300 kill(MState),
5301 ( domain_contains(Dom, V) -> B = 1
5302 ; B = 0
5303 )
5304 ; B == 1 -> kill(MState), domain(V, Dom)
5305 ; B == 0 -> kill(MState), domain_complement(Dom, C), domain(V, C)
5306 ; fd_get(V, VD, _),
5307 ( domains_intersection(VD, Dom, I) ->
5308 ( I == VD -> kill(MState), B = 1
5309 ; true
5310 )
5311 ; kill(MState), B = 0
5312 )
5313 ).
5314
5315run_propagator(reified_tuple_in(Tuple, R, B), MState) :-
5316 get_attr(R, clpfd_relation, Relation),
5317 ( B == 1 -> kill(MState), tuples_in([Tuple], Relation)
5318 ; ( ground(Tuple) ->
5319 kill(MState),
5320 ( memberchk(Tuple, Relation) -> B = 1
5321 ; B = 0
5322 )
5323 ; relation_unifiable(Relation, Tuple, Us, _, _),
5324 ( Us = [] -> kill(MState), B = 0
5325 ; true
5326 )
5327 )
5328 ).
5329
5330run_propagator(tuples_not_in(Tuples, Relation, B), MState) :-
5331 ( B == 0 ->
5332 kill(MState),
5333 tuples_in_conjunction(Tuples, Relation, Conj),
5334 #\ Conj
5335 ; true
5336 ).
5337
5338run_propagator(kill_reified_tuples(B, Ps, Bs), _) :-
5339 ( B == 0 ->
5340 maplist(kill_entailed, Ps),
5341 phrase(as(Bs), As),
5342 maplist(kill_entailed, As)
5343 ; true
5344 ).
5345
5346run_propagator(reified_fd(V,B), MState) :-
5347 ( fd_inf(V, I), I \== inf, fd_sup(V, S), S \== sup ->
5348 kill(MState),
5349 B = 1
5350 ; B == 0 ->
5351 ( fd_inf(V, inf) -> true
5352 ; fd_sup(V, sup) -> true
5353 ; false
5354 )
5355 ; true
5356 ).
5357
5359
5360run_propagator(pskeleton(X,Y,D,Skel,Z,_), MState) :-
5361 ( Y == 0 -> kill(MState), D = 0
5362 ; D == 1 -> kill(MState), neq_num(Y, 0), skeleton([X,Y,Z], Skel)
5363 ; integer(Y), Y =\= 0 -> kill(MState), D = 1, skeleton([X,Y,Z], Skel)
5364 ; fd_get(Y, YD, _), \+ domain_contains(YD, 0) ->
5365 kill(MState),
5366 D = 1, skeleton([X,Y,Z], Skel)
5367 ; true
5368 ).
5369
5374
5375run_propagator(pfunction(Op,A,B,R), MState) :-
5376 ( integer(A), integer(B) ->
5377 kill(MState),
5378 Expr =.. [Op,A,B],
5379 R is Expr
5380 ; true
5381 ).
5382run_propagator(pfunction(Op,A,R), MState) :-
5383 ( integer(A) ->
5384 kill(MState),
5385 Expr =.. [Op,A],
5386 R is Expr
5387 ; true
5388 ).
5389
5391
5392run_propagator(reified_geq(DX,X,DY,Y,Ps,B), MState) :-
5393 ( DX == 0 -> kill(MState, Ps), B = 0
5394 ; DY == 0 -> kill(MState, Ps), B = 0
5395 ; B == 1 -> kill(MState), DX = 1, DY = 1, geq(X, Y)
5396 ; DX == 1, DY == 1 ->
5397 ( var(B) ->
5398 ( nonvar(X) ->
5399 ( nonvar(Y) ->
5400 kill(MState),
5401 ( X >= Y -> B = 1 ; B = 0 )
5402 ; fd_get(Y, _, YL, YU, _),
5403 ( n(X) cis_geq YU -> kill(MState, Ps), B = 1
5404 ; n(X) cis_lt YL -> kill(MState, Ps), B = 0
5405 ; true
5406 )
5407 )
5408 ; nonvar(Y) ->
5409 fd_get(X, _, XL, XU, _),
5410 ( XL cis_geq n(Y) -> kill(MState, Ps), B = 1
5411 ; XU cis_lt n(Y) -> kill(MState, Ps), B = 0
5412 ; true
5413 )
5414 ; X == Y -> kill(MState, Ps), B = 1
5415 ; fd_get(X, _, XL, XU, _),
5416 fd_get(Y, _, YL, YU, _),
5417 ( XL cis_geq YU -> kill(MState, Ps), B = 1
5418 ; XU cis_lt YL -> kill(MState, Ps), B = 0
5419 ; true
5420 )
5421 )
5422 ; B =:= 0 -> kill(MState), X #< Y
5423 ; true
5424 )
5425 ; true
5426 ).
5427
5429run_propagator(reified_eq(DX,X,DY,Y,Ps,B), MState) :-
5430 ( DX == 0 -> kill(MState, Ps), B = 0
5431 ; DY == 0 -> kill(MState, Ps), B = 0
5432 ; B == 1 -> kill(MState), DX = 1, DY = 1, X = Y
5433 ; DX == 1, DY == 1 ->
5434 ( var(B) ->
5435 ( nonvar(X) ->
5436 ( nonvar(Y) ->
5437 kill(MState),
5438 ( X =:= Y -> B = 1 ; B = 0)
5439 ; fd_get(Y, YD, _),
5440 ( domain_contains(YD, X) -> true
5441 ; kill(MState, Ps), B = 0
5442 )
5443 )
5444 ; nonvar(Y) -> run_propagator(reified_eq(DY,Y,DX,X,Ps,B), MState)
5445 ; X == Y -> kill(MState), B = 1
5446 ; fd_get(X, _, XL, XU, _),
5447 fd_get(Y, _, YL, YU, _),
5448 ( XL cis_gt YU -> kill(MState, Ps), B = 0
5449 ; YL cis_gt XU -> kill(MState, Ps), B = 0
5450 ; true
5451 )
5452 )
5453 ; B =:= 0 -> kill(MState), X #\= Y
5454 ; true
5455 )
5456 ; true
5457 ).
5459run_propagator(reified_neq(DX,X,DY,Y,Ps,B), MState) :-
5460 ( DX == 0 -> kill(MState, Ps), B = 0
5461 ; DY == 0 -> kill(MState, Ps), B = 0
5462 ; B == 1 -> kill(MState), DX = 1, DY = 1, X #\= Y
5463 ; DX == 1, DY == 1 ->
5464 ( var(B) ->
5465 ( nonvar(X) ->
5466 ( nonvar(Y) ->
5467 kill(MState),
5468 ( X =\= Y -> B = 1 ; B = 0)
5469 ; fd_get(Y, YD, _),
5470 ( domain_contains(YD, X) -> true
5471 ; kill(MState, Ps), B = 1
5472 )
5473 )
5474 ; nonvar(Y) -> run_propagator(reified_neq(DY,Y,DX,X,Ps,B), MState)
5475 ; X == Y -> kill(MState), B = 0
5476 ; fd_get(X, _, XL, XU, _),
5477 fd_get(Y, _, YL, YU, _),
5478 ( XL cis_gt YU -> kill(MState, Ps), B = 1
5479 ; YL cis_gt XU -> kill(MState, Ps), B = 1
5480 ; true
5481 )
5482 )
5483 ; B =:= 0 -> kill(MState), X = Y
5484 ; true
5485 )
5486 ; true
5487 ).
5489run_propagator(reified_and(X,Ps1,Y,Ps2,B), MState) :-
5490 ( nonvar(X) ->
5491 kill(MState),
5492 ( X =:= 0 -> maplist(kill_entailed, Ps2), B = 0
5493 ; B = Y
5494 )
5495 ; nonvar(Y) -> run_propagator(reified_and(Y,Ps2,X,Ps1,B), MState)
5496 ; B == 1 -> kill(MState), X = 1, Y = 1
5497 ; true
5498 ).
5499
5501run_propagator(reified_or(X,Ps1,Y,Ps2,B), MState) :-
5502 ( nonvar(X) ->
5503 kill(MState),
5504 ( X =:= 1 -> maplist(kill_entailed, Ps2), B = 1
5505 ; B = Y
5506 )
5507 ; nonvar(Y) -> run_propagator(reified_or(Y,Ps2,X,Ps1,B), MState)
5508 ; B == 0 -> kill(MState), X = 0, Y = 0
5509 ; true
5510 ).
5511
5513run_propagator(reified_not(X,Y), MState) :-
5514 ( X == 0 -> kill(MState), Y = 1
5515 ; X == 1 -> kill(MState), Y = 0
5516 ; Y == 0 -> kill(MState), X = 1
5517 ; Y == 1 -> kill(MState), X = 0
5518 ; true
5519 ).
5520
5522run_propagator(pimpl(X, Y, Ps), MState) :-
5523 ( nonvar(X) ->
5524 kill(MState),
5525 ( X =:= 1 -> Y = 1
5526 ; maplist(kill_entailed, Ps)
5527 )
5528 ; nonvar(Y) ->
5529 kill(MState),
5530 ( Y =:= 0 -> X = 0
5531 ; maplist(kill_entailed, Ps)
5532 )
5533 ; true
5534 ).
5535
5538
5539update_bounds(X, XD, XPs, XL, XU, NXL, NXU) :-
5540 ( NXL == XL, NXU == XU -> true
5541 ; domains_intersection(XD, from_to(NXL, NXU), NXD),
5542 fd_put(X, NXD, XPs)
5543 ).
5544
5545min_product(L1, U1, L2, U2, Min) :-
5546 Min cis min(min(L1*L2,L1*U2),min(U1*L2,U1*U2)).
5547max_product(L1, U1, L2, U2, Max) :-
5548 Max cis max(max(L1*L2,L1*U2),max(U1*L2,U1*U2)).
5549
5550finite(n(_)).
5551
5552in_(L, U, X) :-
5553 fd_get(X, XD, XPs),
5554 domains_intersection(XD, from_to(L,U), NXD),
5555 fd_put(X, NXD, XPs).
5556
5557min_max_factor(L1, U1, L2, U2, L3, U3, Min, Max) :-
5558 ( U1 cis_lt n(0),
5559 L2 cis_lt n(0), U2 cis_gt n(0),
5560 L3 cis_lt n(0), U3 cis_gt n(0) ->
5561 maplist(in_(L1,U1), [Z1,Z2]),
5562 with_local_attributes([X1,Y1,X2,Y2], [], (
5563 in_(L2, n(-1), X1), in_(n(1), U3, Y1),
5564 ( X1*Y1 #= Z1 ->
5565 ( fd_get(Y1, _, Inf1, Sup1, _) -> true
5566 ; Inf1 = n(Y1), Sup1 = n(Y1)
5567 )
5568 ; Inf1 = inf, Sup1 = n(-1)
5569 ),
5570 in_(n(1), U2, X2), in_(L3, n(-1), Y2),
5571 ( X2*Y2 #= Z2 ->
5572 ( fd_get(Y2, _, Inf2, Sup2, _) -> true
5573 ; Inf2 = n(Y2), Sup2 = n(Y2)
5574 )
5575 ; Inf2 = n(1), Sup2 = sup
5576 )
5577 ), [Inf1,Sup1,Inf2,Sup2]),
5578 Min cis max(min(Inf1,Inf2), L3),
5579 Max cis min(max(Sup1,Sup2), U3)
5580 ; L1 cis_gt n(0),
5581 L2 cis_lt n(0), U2 cis_gt n(0),
5582 L3 cis_lt n(0), U3 cis_gt n(0) ->
5583 maplist(in_(L1,U1), [Z1,Z2]),
5584 with_local_attributes([X1,Y1,X2,Y2], [], (
5585 in_(L2, n(-1), X1), in_(L3, n(-1), Y1),
5586 ( X1*Y1 #= Z1 ->
5587 ( fd_get(Y1, _, Inf1, Sup1, _) -> true
5588 ; Inf1 = n(Y1), Sup1 = n(Y1)
5589 )
5590 ; Inf1 = n(1), Sup1 = sup
5591 ),
5592 in_(n(1), U2, X2), in_(n(1), U3, Y2),
5593 ( X2*Y2 #= Z2 ->
5594 ( fd_get(Y2, _, Inf2, Sup2, _) -> true
5595 ; Inf2 = n(Y2), Sup2 = n(Y2)
5596 )
5597 ; Inf2 = inf, Sup2 = n(-1)
5598 )
5599 ), [Inf1,Sup1,Inf2,Sup2]),
5600 Min cis max(min(Inf1,Inf2), L3),
5601 Max cis min(max(Sup1,Sup2), U3)
5602 ; min_factor(L1, U1, L2, U2, Min0),
5603 Min cis max(L3,Min0),
5604 max_factor(L1, U1, L2, U2, Max0),
5605 Max cis min(U3,Max0)
5606 ).
5607
5608min_factor(L1, U1, L2, U2, Min) :-
5609 ( L1 cis_geq n(0), L2 cis_gt n(0), finite(U2) ->
5610 Min cis (L1+U2-n(1))//U2
5611 ; L1 cis_gt n(0), U2 cis_lt n(0) -> Min cis U1//U2
5612 ; L1 cis_gt n(0), L2 cis_geq n(0) -> Min = n(1)
5613 ; L1 cis_gt n(0) -> Min cis -U1
5614 ; U1 cis_lt n(0), U2 cis_leq n(0) ->
5615 ( finite(L2) -> Min cis (U1+L2+n(1))//L2
5616 ; Min = n(1)
5617 )
5618 ; U1 cis_lt n(0), L2 cis_geq n(0) -> Min cis L1//L2
5619 ; U1 cis_lt n(0) -> Min = L1
5620 ; L2 cis_leq n(0), U2 cis_geq n(0) -> Min = inf
5621 ; Min cis min(min(L1//L2,L1//U2),min(U1//L2,U1//U2))
5622 ).
5623max_factor(L1, U1, L2, U2, Max) :-
5624 ( L1 cis_geq n(0), L2 cis_geq n(0) -> Max cis U1//L2
5625 ; L1 cis_gt n(0), U2 cis_leq n(0) ->
5626 ( finite(L2) -> Max cis (L1-L2-n(1))//L2
5627 ; Max = n(-1)
5628 )
5629 ; L1 cis_gt n(0) -> Max = U1
5630 ; U1 cis_lt n(0), U2 cis_lt n(0) -> Max cis L1//U2
5631 ; U1 cis_lt n(0), L2 cis_geq n(0) ->
5632 ( finite(U2) -> Max cis (U1-U2+n(1))//U2
5633 ; Max = n(-1)
5634 )
5635 ; U1 cis_lt n(0) -> Max cis -L1
5636 ; L2 cis_leq n(0), U2 cis_geq n(0) -> Max = sup
5637 ; Max cis max(max(L1//L2,L1//U2),max(U1//L2,U1//U2))
5638 ).
5639
5645
5646distinct_attach([], _, _).
5647distinct_attach([X|Xs], Prop, Right) :-
5648 ( var(X) ->
5649 init_propagator(X, Prop),
5650 make_propagator(pexclude(Xs,Right,X), P1),
5651 init_propagator(X, P1),
5652 trigger_prop(P1)
5653 ; exclude_fire(Xs, Right, X)
5654 ),
5655 distinct_attach(Xs, Prop, [X|Right]).
5656
5671
5672difference_arcs(Vars, FreeLeft, FreeRight) :-
5673 empty_assoc(E),
5674 phrase(difference_arcs(Vars, FreeLeft), [E], [NumVar]),
5675 assoc_to_list(NumVar, LsNumVar),
5676 pairs_values(LsNumVar, FreeRight).
5677
5678domain_to_list(Domain, List) :- phrase(domain_to_list(Domain), List).
5679
5680domain_to_list(split(_, Left, Right)) -->
5681 domain_to_list(Left), domain_to_list(Right).
5682domain_to_list(empty) --> [].
5683domain_to_list(from_to(n(F),n(T))) --> { numlist(F, T, Ns) }, list(Ns).
5684
5685difference_arcs([], []) --> [].
5686difference_arcs([V|Vs], FL0) -->
5687 ( { fd_get(V, Dom, _),
5688 finite_domain(Dom) } ->
5689 { FL0 = [V|FL],
5690 domain_to_list(Dom, Ns) },
5691 enumerate(Ns, V),
5692 difference_arcs(Vs, FL)
5693 ; difference_arcs(Vs, FL0)
5694 ).
5695
5696enumerate([], _) --> [].
5697enumerate([N|Ns], V) -->
5698 state(NumVar0, NumVar),
5699 { ( get_assoc(N, NumVar0, Y) -> NumVar0 = NumVar
5700 ; put_assoc(N, NumVar0, Y, NumVar),
5701 put_attr(Y, value, N)
5702 ),
5703 put_attr(F, flow, 0),
5704 append_edge(Y, edges, flow_from(F,V)),
5705 append_edge(V, edges, flow_to(F,Y)) },
5706 enumerate(Ns, V).
5707
5708append_edge(V, Attr, E) :-
5709 ( get_attr(V, Attr, Es) ->
5710 put_attr(V, Attr, [E|Es])
5711 ; put_attr(V, Attr, [E])
5712 ).
5713
5718
5719clear_parent(V) :- del_attr(V, parent).
5720
5721maximum_matching([]).
5722maximum_matching([FL|FLs]) :-
5723 augmenting_path_to([[FL]], Levels, To),
5724 phrase(augmenting_path(FL, To), Path),
5725 maplist(maplist(clear_parent), Levels),
5726 del_attr(To, free),
5727 adjust_alternate_1(Path),
5728 maximum_matching(FLs).
5729
5730reachables([]) --> [].
5731reachables([V|Vs]) -->
5732 { get_attr(V, edges, Es) },
5733 reachables_(Es, V),
5734 reachables(Vs).
5735
5736reachables_([], _) --> [].
5737reachables_([E|Es], V) -->
5738 edge_reachable(E, V),
5739 reachables_(Es, V).
5740
5741edge_reachable(flow_to(F,To), V) -->
5742 ( { get_attr(F, flow, 0),
5743 \+ get_attr(To, parent, _) } ->
5744 { put_attr(To, parent, V-F) },
5745 [To]
5746 ; []
5747 ).
5748edge_reachable(flow_from(F,From), V) -->
5749 ( { get_attr(F, flow, 1),
5750 \+ get_attr(From, parent, _) } ->
5751 { put_attr(From, parent, V-F) },
5752 [From]
5753 ; []
5754 ).
5755
5756augmenting_path_to(Levels0, Levels, Right) :-
5757 Levels0 = [Vs|_],
5758 Levels1 = [Tos|Levels0],
5759 phrase(reachables(Vs), Tos),
5760 Tos = [_|_],
5761 ( member(Right, Tos), get_attr(Right, free, true) ->
5762 Levels = Levels1
5763 ; augmenting_path_to(Levels1, Levels, Right)
5764 ).
5765
5766augmenting_path(S, V) -->
5767 ( { V == S } -> []
5768 ; { get_attr(V, parent, V1-Augment) },
5769 [Augment],
5770 augmenting_path(S, V1)
5771 ).
5772
5773adjust_alternate_1([A|Arcs]) :-
5774 put_attr(A, flow, 1),
5775 adjust_alternate_0(Arcs).
5776
5777adjust_alternate_0([]).
5778adjust_alternate_0([A|Arcs]) :-
5779 put_attr(A, flow, 0),
5780 adjust_alternate_1(Arcs).
5781
5785
5786g_g0(V) :-
5787 get_attr(V, edges, Es),
5788 maplist(g_g0_(V), Es).
5789
5790g_g0_(V, flow_to(F,To)) :-
5791 ( get_attr(F, flow, 1) ->
5792 append_edge(V, g0_edges, flow_to(F,To))
5793 ; append_edge(To, g0_edges, flow_to(F,V))
5794 ).
5795
5796
5797g0_successors(V, Tos) :-
5798 ( get_attr(V, g0_edges, Tos0) ->
5799 maplist(arg(2), Tos0, Tos)
5800 ; Tos = []
5801 ).
5802
5803put_free(F) :- put_attr(F, free, true).
5804
5805free_node(F) :- get_attr(F, free, true).
5806
5807del_vars_attr(Vars, Attr) :- maplist(del_attr_(Attr), Vars).
5808
5809del_attr_(Attr, Var) :- del_attr(Var, Attr).
5810
5811with_local_attributes(Vars, Attrs, Goal, Result) :-
5812 catch((maplist(del_vars_attr(Vars), Attrs),
5813 Goal,
5814 maplist(del_attrs, Vars),
5815 5816 throw(local_attributes(Result,Vars))),
5817 local_attributes(Result,Vars),
5818 true).
5819
5820distinct(Vars) :-
5821 with_local_attributes(Vars, [edges,parent,g0_edges,index,visited],
5822 (difference_arcs(Vars, FreeLeft, FreeRight0),
5823 length(FreeLeft, LFL),
5824 length(FreeRight0, LFR),
5825 LFL =< LFR,
5826 maplist(put_free, FreeRight0),
5827 maximum_matching(FreeLeft),
5828 include(free_node, FreeRight0, FreeRight),
5829 maplist(g_g0, FreeLeft),
5830 scc(FreeLeft, g0_successors),
5831 maplist(dfs_used, FreeRight),
5832 phrase(distinct_goals(FreeLeft), Gs)), Gs),
5833 disable_queue,
5834 maplist(call, Gs),
5835 enable_queue.
5836
5837distinct_goals([]) --> [].
5838distinct_goals([V|Vs]) -->
5839 { get_attr(V, edges, Es) },
5840 distinct_goals_(Es, V),
5841 distinct_goals(Vs).
5842
5843distinct_goals_([], _) --> [].
5844distinct_goals_([flow_to(F,To)|Es], V) -->
5845 ( { get_attr(F, flow, 0),
5846 \+ get_attr(F, used, true),
5847 get_attr(V, lowlink, L1),
5848 get_attr(To, lowlink, L2),
5849 L1 =\= L2 } ->
5850 { get_attr(To, value, N) },
5851 [neq_num(V, N)]
5852 ; []
5853 ),
5854 distinct_goals_(Es, V).
5855
5859
5860dfs_used(V) :-
5861 ( get_attr(V, visited, true) -> true
5862 ; put_attr(V, visited, true),
5863 ( get_attr(V, g0_edges, Es) ->
5864 dfs_used_edges(Es)
5865 ; true
5866 )
5867 ).
5868
5869dfs_used_edges([]).
5870dfs_used_edges([flow_to(F,To)|Es]) :-
5871 put_attr(F, used, true),
5872 dfs_used(To),
5873 dfs_used_edges(Es).
5874
5891
5892scc(Vs, Succ) :- phrase(scc(Vs), [s(0,[],Succ)], _).
5893
5894scc([]) --> [].
5895scc([V|Vs]) -->
5896 ( vindex_defined(V) -> scc(Vs)
5897 ; scc_(V), scc(Vs)
5898 ).
5899
5900vindex_defined(V) --> { get_attr(V, index, _) }.
5901
5902vindex_is_index(V) -->
5903 state(s(Index,_,_)),
5904 { put_attr(V, index, Index) }.
5905
5906vlowlink_is_index(V) -->
5907 state(s(Index,_,_)),
5908 { put_attr(V, lowlink, Index) }.
5909
5910index_plus_one -->
5911 state(s(I,Stack,Succ), s(I1,Stack,Succ)),
5912 { I1 is I+1 }.
5913
5914s_push(V) -->
5915 state(s(I,Stack,Succ), s(I,[V|Stack],Succ)),
5916 { put_attr(V, in_stack, true) }.
5917
5918vlowlink_min_lowlink(V, VP) -->
5919 { get_attr(V, lowlink, VL),
5920 get_attr(VP, lowlink, VPL),
5921 VL1 is min(VL, VPL),
5922 put_attr(V, lowlink, VL1) }.
5923
5924successors(V, Tos) --> state(s(_,_,Succ)), { call(Succ, V, Tos) }.
5925
5926scc_(V) -->
5927 vindex_is_index(V),
5928 vlowlink_is_index(V),
5929 index_plus_one,
5930 s_push(V),
5931 successors(V, Tos),
5932 each_edge(Tos, V),
5933 ( { get_attr(V, index, VI),
5934 get_attr(V, lowlink, VI) } -> pop_stack_to(V, VI)
5935 ; []
5936 ).
5937
5938pop_stack_to(V, N) -->
5939 state(s(I,[First|Stack],Succ), s(I,Stack,Succ)),
5940 { del_attr(First, in_stack) },
5941 ( { First == V } -> []
5942 ; { put_attr(First, lowlink, N) },
5943 pop_stack_to(V, N)
5944 ).
5945
5946each_edge([], _) --> [].
5947each_edge([VP|VPs], V) -->
5948 ( vindex_defined(VP) ->
5949 ( v_in_stack(VP) ->
5950 vlowlink_min_lowlink(V, VP)
5951 ; []
5952 )
5953 ; scc_(VP),
5954 vlowlink_min_lowlink(V, VP)
5955 ),
5956 each_edge(VPs, V).
5957
5958state(S), [S] --> [S].
5959
5960state(S0, S), [S] --> [S0].
5961
5962v_in_stack(V) --> { get_attr(V, in_stack, true) }.
5963
5972
5973weak_arc_all_distinct(Ls) :-
5974 must_be(list, Ls),
5975 Orig = original_goal(_, weak_arc_all_distinct(Ls)),
5976 all_distinct(Ls, [], Orig),
5977 do_queue.
5978
5979all_distinct([], _, _).
5980all_distinct([X|Right], Left, Orig) :-
5981 5982 ( var(X) ->
5983 make_propagator(weak_distinct(Left,Right,X,Orig), Prop),
5984 init_propagator(X, Prop),
5985 trigger_prop(Prop)
5989 ; exclude_fire(Left, Right, X)
5990 ),
5991 outof_reducer(Left, Right, X),
5992 all_distinct(Right, [X|Left], Orig).
5993
5994exclude_fire(Left, Right, E) :-
5995 all_neq(Left, E),
5996 all_neq(Right, E).
5997
5998list_contains([X|Xs], Y) :-
5999 ( X == Y -> true
6000 ; list_contains(Xs, Y)
6001 ).
6002
6003kill_if_isolated(Left, Right, X, MState) :-
6004 append(Left, Right, Others),
6005 fd_get(X, XDom, _),
6006 ( all_empty_intersection(Others, XDom) -> kill(MState)
6007 ; true
6008 ).
6009
6010all_empty_intersection([], _).
6011all_empty_intersection([V|Vs], XDom) :-
6012 ( fd_get(V, VDom, _) ->
6013 domains_intersection_(VDom, XDom, empty),
6014 all_empty_intersection(Vs, XDom)
6015 ; all_empty_intersection(Vs, XDom)
6016 ).
6017
6018outof_reducer(Left, Right, Var) :-
6019 ( fd_get(Var, Dom, _) ->
6020 append(Left, Right, Others),
6021 domain_num_elements(Dom, N),
6022 num_subsets(Others, Dom, 0, Num, NonSubs),
6023 ( n(Num) cis_geq N -> false
6024 ; n(Num) cis N - n(1) ->
6025 reduce_from_others(NonSubs, Dom)
6026 ; true
6027 )
6028 ; 6029 6030 true
6031 ).
6032
6033reduce_from_others([], _).
6034reduce_from_others([X|Xs], Dom) :-
6035 ( fd_get(X, XDom, XPs) ->
6036 domain_subtract(XDom, Dom, NXDom),
6037 fd_put(X, NXDom, XPs)
6038 ; true
6039 ),
6040 reduce_from_others(Xs, Dom).
6041
6042num_subsets([], _Dom, Num, Num, []).
6043num_subsets([S|Ss], Dom, Num0, Num, NonSubs) :-
6044 ( fd_get(S, SDom, _) ->
6045 ( domain_subdomain(Dom, SDom) ->
6046 Num1 is Num0 + 1,
6047 num_subsets(Ss, Dom, Num1, Num, NonSubs)
6048 ; NonSubs = [S|Rest],
6049 num_subsets(Ss, Dom, Num0, Num, Rest)
6050 )
6051 ; num_subsets(Ss, Dom, Num0, Num, NonSubs)
6052 ).
6053
6055
6077
6078serialized(Starts, Durations) :-
6079 must_be(list(integer), Durations),
6080 pairs_keys_values(SDs, Starts, Durations),
6081 Orig = original_goal(_, serialized(Starts, Durations)),
6082 serialize(SDs, Orig).
6083
6084serialize([], _).
6085serialize([S-D|SDs], Orig) :-
6086 D >= 0,
6087 serialize(SDs, S, D, Orig),
6088 serialize(SDs, Orig).
6089
6090serialize([], _, _, _).
6091serialize([S-D|Rest], S0, D0, Orig) :-
6092 D >= 0,
6093 propagator_init_trigger([S0,S], pserialized(S,D,S0,D0,Orig)),
6094 serialize(Rest, S0, D0, Orig).
6095
6098
6099earliest_start_time(Start, EST) :-
6100 ( fd_get(Start, D, _) ->
6101 domain_infimum(D, EST)
6102 ; EST = n(Start)
6103 ).
6104
6105latest_start_time(Start, LST) :-
6106 ( fd_get(Start, D, _) ->
6107 domain_supremum(D, LST)
6108 ; LST = n(Start)
6109 ).
6110
6111serialize_lower_upper(S_I, D_I, S_J, D_J, MState) :-
6112 ( var(S_I) ->
6113 serialize_lower_bound(S_I, D_I, S_J, D_J, MState),
6114 ( var(S_I) -> serialize_upper_bound(S_I, D_I, S_J, D_J, MState)
6115 ; true
6116 )
6117 ; true
6118 ).
6119
6120serialize_lower_bound(I, D_I, J, D_J, MState) :-
6121 fd_get(I, DomI, Ps),
6122 ( domain_infimum(DomI, n(EST_I)),
6123 latest_start_time(J, n(LST_J)),
6124 EST_I + D_I > LST_J,
6125 earliest_start_time(J, n(EST_J)) ->
6126 ( nonvar(J) -> kill(MState)
6127 ; true
6128 ),
6129 EST is EST_J+D_J,
6130 domain_remove_smaller_than(DomI, EST, DomI1),
6131 fd_put(I, DomI1, Ps)
6132 ; true
6133 ).
6134
6135serialize_upper_bound(I, D_I, J, D_J, MState) :-
6136 fd_get(I, DomI, Ps),
6137 ( domain_supremum(DomI, n(LST_I)),
6138 earliest_start_time(J, n(EST_J)),
6139 EST_J + D_J > LST_I,
6140 latest_start_time(J, n(LST_J)) ->
6141 ( nonvar(J) -> kill(MState)
6142 ; true
6143 ),
6144 LST is LST_J-D_I,
6145 domain_remove_greater_than(DomI, LST, DomI1),
6146 fd_put(I, DomI1, Ps)
6147 ; true
6148 ).
6149
6151
6156
6157element(N, Is, V) :-
6158 must_be(list, Is),
6159 length(Is, L),
6160 N in 1..L,
6161 element_(Is, 1, N, V),
6162 propagator_init_trigger([N|Is], pelement(N,Is,V)).
6163
6164element_domain(V, VD) :-
6165 ( fd_get(V, VD, _) -> true
6166 ; VD = from_to(n(V), n(V))
6167 ).
6168
6169element_([], _, _, _).
6170element_([I|Is], N0, N, V) :-
6171 ?(I) #\= ?(V) #==> ?(N) #\= N0,
6172 N1 is N0 + 1,
6173 element_(Is, N1, N, V).
6174
6175integers_remaining([], _, _, D, D).
6176integers_remaining([V|Vs], N0, Dom, D0, D) :-
6177 ( domain_contains(Dom, N0) ->
6178 element_domain(V, VD),
6179 domains_union(D0, VD, D1)
6180 ; D1 = D0
6181 ),
6182 N1 is N0 + 1,
6183 integers_remaining(Vs, N1, Dom, D1, D).
6184
6186
6200
6201global_cardinality(Xs, Pairs) :- global_cardinality(Xs, Pairs, []).
6202
6221
6222global_cardinality(Xs, Pairs, Options) :-
6223 must_be(list(list), [Xs,Pairs,Options]),
6224 maplist(fd_variable, Xs),
6225 maplist(gcc_pair, Pairs),
6226 pairs_keys_values(Pairs, Keys, Nums),
6227 ( sort(Keys, Keys1), same_length(Keys, Keys1) -> true
6228 ; domain_error(gcc_unique_key_pairs, Pairs)
6229 ),
6230 length(Xs, L),
6231 Nums ins 0..L,
6232 list_to_drep(Keys, Drep),
6233 Xs ins Drep,
6234 gcc_pairs(Pairs, Xs, Pairs1),
6235 6236 6237 propagator_init_trigger(Xs, pgcc_check(Pairs1)),
6238 propagator_init_trigger(Nums, pgcc_check_single(Pairs1)),
6239 ( member(OD, Options), OD == consistency(value) -> true
6240 ; propagator_init_trigger(Nums, pgcc_single(Xs, Pairs1)),
6241 propagator_init_trigger(Xs, pgcc(Xs, Pairs, Pairs1))
6242 ),
6243 ( member(OC, Options), functor(OC, cost, 2) ->
6244 OC = cost(Cost, Matrix),
6245 must_be(list(list(integer)), Matrix),
6246 maplist(keys_costs(Keys), Xs, Matrix, Costs),
6247 sum(Costs, #=, Cost)
6248 ; true
6249 ).
6250
6251keys_costs(Keys, X, Row, C) :-
6252 element(N, Keys, X),
6253 element(N, Row, C).
6254
6255gcc_pair(Pair) :-
6256 ( Pair = Key-Val ->
6257 must_be(integer, Key),
6258 fd_variable(Val)
6259 ; domain_error(gcc_pair, Pair)
6260 ).
6261
6271
6272gcc_pairs([], _, []).
6273gcc_pairs([Key-Num0|KNs], Vs, [Key-Num|Rest]) :-
6274 put_attr(Num, clpfd_gcc_num, Num0),
6275 put_attr(Num, clpfd_gcc_vs, Vs),
6276 put_attr(Num, clpfd_gcc_occurred, 0),
6277 gcc_pairs(KNs, Vs, Rest).
6278
6283
6284gcc_global(Vs, KNs) :-
6285 gcc_check(KNs),
6286 6287 do_queue,
6288 with_local_attributes(Vs, [edges,parent,index],
6289 (gcc_arcs(KNs, S, Vals),
6290 variables_with_num_occurrences(Vs, VNs),
6291 maplist(target_to_v(T), VNs),
6292 ( get_attr(S, edges, Es) ->
6293 put_attr(S, parent, none), 6294 feasible_flow(Es, S, T), 6295 maximum_flow(S, T), 6296 gcc_consistent(T),
6297 scc(Vals, gcc_successors),
6298 phrase(gcc_goals(Vals), Gs)
6299 ; Gs = [] )), Gs),
6300 disable_queue,
6301 maplist(call, Gs),
6302 enable_queue.
6303
6304gcc_consistent(T) :-
6305 get_attr(T, edges, Es),
6306 maplist(saturated_arc, Es).
6307
6308saturated_arc(arc_from(_,U,_,Flow)) :- get_attr(Flow, flow, U).
6309
6310gcc_goals([]) --> [].
6311gcc_goals([Val|Vals]) -->
6312 { get_attr(Val, edges, Es) },
6313 gcc_edges_goals(Es, Val),
6314 gcc_goals(Vals).
6315
6316gcc_edges_goals([], _) --> [].
6317gcc_edges_goals([E|Es], Val) -->
6318 gcc_edge_goal(E, Val),
6319 gcc_edges_goals(Es, Val).
6320
6321gcc_edge_goal(arc_from(_,_,_,_), _) --> [].
6322gcc_edge_goal(arc_to(_,_,V,F), Val) -->
6323 ( { get_attr(F, flow, 0),
6324 get_attr(V, lowlink, L1),
6325 get_attr(Val, lowlink, L2),
6326 L1 =\= L2,
6327 get_attr(Val, value, Value) } ->
6328 [neq_num(V, Value)]
6329 ; []
6330 ).
6331
6336
6337maximum_flow(S, T) :-
6338 ( gcc_augmenting_path([[S]], Levels, T) ->
6339 phrase(augmenting_path(S, T), Path),
6340 Path = [augment(_,First,_)|Rest],
6341 path_minimum(Rest, First, Min),
6342 maplist(gcc_augment(Min), Path),
6343 maplist(maplist(clear_parent), Levels),
6344 maximum_flow(S, T)
6345 ; true
6346 ).
6347
6348feasible_flow([], _, _).
6349feasible_flow([A|As], S, T) :-
6350 make_arc_feasible(A, S, T),
6351 feasible_flow(As, S, T).
6352
6353make_arc_feasible(A, S, T) :-
6354 A = arc_to(L,_,V,F),
6355 get_attr(F, flow, Flow),
6356 ( Flow >= L -> true
6357 ; Diff is L - Flow,
6358 put_attr(V, parent, S-augment(F,Diff,+)),
6359 gcc_augmenting_path([[V]], Levels, T),
6360 phrase(augmenting_path(S, T), Path),
6361 path_minimum(Path, Diff, Min),
6362 maplist(gcc_augment(Min), Path),
6363 maplist(maplist(clear_parent), Levels),
6364 make_arc_feasible(A, S, T)
6365 ).
6366
6367gcc_augmenting_path(Levels0, Levels, T) :-
6368 Levels0 = [Vs|_],
6369 Levels1 = [Tos|Levels0],
6370 phrase(gcc_reachables(Vs), Tos),
6371 Tos = [_|_],
6372 ( member(To, Tos), To == T -> Levels = Levels1
6373 ; gcc_augmenting_path(Levels1, Levels, T)
6374 ).
6375
6376gcc_reachables([]) --> [].
6377gcc_reachables([V|Vs]) -->
6378 { get_attr(V, edges, Es) },
6379 gcc_reachables_(Es, V),
6380 gcc_reachables(Vs).
6381
6382gcc_reachables_([], _) --> [].
6383gcc_reachables_([E|Es], V) -->
6384 gcc_reachable(E, V),
6385 gcc_reachables_(Es, V).
6386
6387gcc_reachable(arc_from(_,_,V,F), P) -->
6388 ( { \+ get_attr(V, parent, _),
6389 get_attr(F, flow, Flow),
6390 Flow > 0 } ->
6391 { put_attr(V, parent, P-augment(F,Flow,-)) },
6392 [V]
6393 ; []
6394 ).
6395gcc_reachable(arc_to(_L,U,V,F), P) -->
6396 ( { \+ get_attr(V, parent, _),
6397 get_attr(F, flow, Flow),
6398 Flow < U } ->
6399 { Diff is U - Flow,
6400 put_attr(V, parent, P-augment(F,Diff,+)) },
6401 [V]
6402 ; []
6403 ).
6404
6405
6406path_minimum([], Min, Min).
6407path_minimum([augment(_,A,_)|As], Min0, Min) :-
6408 Min1 is min(Min0,A),
6409 path_minimum(As, Min1, Min).
6410
6411gcc_augment(Min, augment(F,_,Sign)) :-
6412 get_attr(F, flow, Flow0),
6413 gcc_flow_(Sign, Flow0, Min, Flow),
6414 put_attr(F, flow, Flow).
6415
6416gcc_flow_(+, F0, A, F) :- F is F0 + A.
6417gcc_flow_(-, F0, A, F) :- F is F0 - A.
6418
6422
6423gcc_arcs([], _, []).
6424gcc_arcs([Key-Num0|KNs], S, Vals) :-
6425 ( get_attr(Num0, clpfd_gcc_vs, Vs) ->
6426 get_attr(Num0, clpfd_gcc_num, Num),
6427 get_attr(Num0, clpfd_gcc_occurred, Occ),
6428 ( nonvar(Num) -> U is Num - Occ, U = L
6429 ; fd_get(Num, _, n(L0), n(U0), _),
6430 L is L0 - Occ, U is U0 - Occ
6431 ),
6432 put_attr(Val, value, Key),
6433 Vals = [Val|Rest],
6434 put_attr(F, flow, 0),
6435 append_edge(S, edges, arc_to(L, U, Val, F)),
6436 put_attr(Val, edges, [arc_from(L, U, S, F)]),
6437 variables_with_num_occurrences(Vs, VNs),
6438 maplist(val_to_v(Val), VNs)
6439 ; Vals = Rest
6440 ),
6441 gcc_arcs(KNs, S, Rest).
6442
6443variables_with_num_occurrences(Vs0, VNs) :-
6444 include(var, Vs0, Vs1),
6445 msort(Vs1, Vs),
6446 ( Vs == [] -> VNs = []
6447 ; Vs = [V|Rest],
6448 variables_with_num_occurrences(Rest, V, 1, VNs)
6449 ).
6450
6451variables_with_num_occurrences([], Prev, Count, [Prev-Count]).
6452variables_with_num_occurrences([V|Vs], Prev, Count0, VNs) :-
6453 ( V == Prev ->
6454 Count1 is Count0 + 1,
6455 variables_with_num_occurrences(Vs, Prev, Count1, VNs)
6456 ; VNs = [Prev-Count0|Rest],
6457 variables_with_num_occurrences(Vs, V, 1, Rest)
6458 ).
6459
6460
6461target_to_v(T, V-Count) :-
6462 put_attr(F, flow, 0),
6463 append_edge(V, edges, arc_to(0, Count, T, F)),
6464 append_edge(T, edges, arc_from(0, Count, V, F)).
6465
6466val_to_v(Val, V-Count) :-
6467 put_attr(F, flow, 0),
6468 append_edge(V, edges, arc_from(0, Count, Val, F)),
6469 append_edge(Val, edges, arc_to(0, Count, V, F)).
6470
6471
6472gcc_successors(V, Tos) :-
6473 get_attr(V, edges, Tos0),
6474 phrase(gcc_successors_(Tos0), Tos).
6475
6476gcc_successors_([]) --> [].
6477gcc_successors_([E|Es]) --> gcc_succ_edge(E), gcc_successors_(Es).
6478
6479gcc_succ_edge(arc_to(_,U,V,F)) -->
6480 ( { get_attr(F, flow, Flow),
6481 Flow < U } -> [V]
6482 ; []
6483 ).
6484gcc_succ_edge(arc_from(_,_,V,F)) -->
6485 ( { get_attr(F, flow, Flow),
6486 Flow > 0 } -> [V]
6487 ; []
6488 ).
6489
6497
6498gcc_check(Pairs) :-
6499 disable_queue,
6500 gcc_check_(Pairs),
6501 enable_queue.
6502
6503gcc_done(Num) :-
6504 del_attr(Num, clpfd_gcc_vs),
6505 del_attr(Num, clpfd_gcc_num),
6506 del_attr(Num, clpfd_gcc_occurred).
6507
6508gcc_check_([]).
6509gcc_check_([Key-Num0|KNs]) :-
6510 ( get_attr(Num0, clpfd_gcc_vs, Vs) ->
6511 get_attr(Num0, clpfd_gcc_num, Num),
6512 get_attr(Num0, clpfd_gcc_occurred, Occ0),
6513 vs_key_min_others(Vs, Key, 0, Min, Os),
6514 put_attr(Num0, clpfd_gcc_vs, Os),
6515 put_attr(Num0, clpfd_gcc_occurred, Occ1),
6516 Occ1 is Occ0 + Min,
6517 geq(Num, Occ1),
6518 6519 6520 6521 6522 6523 ( Occ1 == Num -> all_neq(Os, Key), gcc_done(Num0)
6524 ; Os == [] -> gcc_done(Num0), Num = Occ1
6525 ; length(Os, L),
6526 Max is Occ1 + L,
6527 geq(Max, Num),
6528 ( nonvar(Num) -> Diff is Num - Occ1
6529 ; fd_get(Num, ND, _),
6530 domain_infimum(ND, n(NInf)),
6531 Diff is NInf - Occ1
6532 ),
6533 L >= Diff,
6534 ( L =:= Diff ->
6535 Num is Occ1 + Diff,
6536 maplist(=(Key), Os),
6537 gcc_done(Num0)
6538 ; true
6539 )
6540 )
6541 ; true
6542 ),
6543 gcc_check_(KNs).
6544
6545vs_key_min_others([], _, Min, Min, []).
6546vs_key_min_others([V|Vs], Key, Min0, Min, Others) :-
6547 ( fd_get(V, VD, _) ->
6548 ( domain_contains(VD, Key) ->
6549 Others = [V|Rest],
6550 vs_key_min_others(Vs, Key, Min0, Min, Rest)
6551 ; vs_key_min_others(Vs, Key, Min0, Min, Others)
6552 )
6553 ; ( V =:= Key ->
6554 Min1 is Min0 + 1,
6555 vs_key_min_others(Vs, Key, Min1, Min, Others)
6556 ; vs_key_min_others(Vs, Key, Min0, Min, Others)
6557 )
6558 ).
6559
6560all_neq([], _).
6561all_neq([X|Xs], C) :-
6562 neq_num(X, C),
6563 all_neq(Xs, C).
6564
6566
6582
6583circuit(Vs) :-
6584 must_be(list, Vs),
6585 maplist(fd_variable, Vs),
6586 length(Vs, L),
6587 Vs ins 1..L,
6588 ( L =:= 1 -> true
6589 ; neq_index(Vs, 1),
6590 make_propagator(pcircuit(Vs), Prop),
6591 distinct_attach(Vs, Prop, []),
6592 trigger_once(Prop)
6593 ).
6594
6595neq_index([], _).
6596neq_index([X|Xs], N) :-
6597 neq_num(X, N),
6598 N1 is N + 1,
6599 neq_index(Xs, N1).
6600
6611
6612propagate_circuit(Vs) :-
6613 with_local_attributes([], [],
6614 (same_length(Vs, Ts),
6615 circuit_graph(Vs, Ts, Ts),
6616 scc(Ts, circuit_successors),
6617 maplist(single_component, Ts)), _).
6618
6619single_component(V) :- get_attr(V, lowlink, 0).
6620
6621circuit_graph([], _, _).
6622circuit_graph([V|Vs], Ts0, [T|Ts]) :-
6623 ( nonvar(V) -> Ns = [V]
6624 ; fd_get(V, Dom, _),
6625 domain_to_list(Dom, Ns)
6626 ),
6627 phrase(circuit_edges(Ns, Ts0), Es),
6628 put_attr(T, edges, Es),
6629 circuit_graph(Vs, Ts0, Ts).
6630
6631circuit_edges([], _) --> [].
6632circuit_edges([N|Ns], Ts) -->
6633 { nth1(N, Ts, T) },
6634 [arc_to(T)],
6635 circuit_edges(Ns, Ts).
6636
6637circuit_successors(V, Tos) :-
6638 get_attr(V, edges, Tos0),
6639 maplist(arg(1), Tos0, Tos).
6640
6642
6646
6647cumulative(Tasks) :- cumulative(Tasks, [limit(1)]).
6648
6683
6684cumulative(Tasks, Options) :-
6685 must_be(list(list), [Tasks,Options]),
6686 ( Options = [] -> L = 1
6687 ; Options = [limit(L)] -> must_be(integer, L)
6688 ; domain_error(cumulative_options_empty_or_limit, Options)
6689 ),
6690 ( Tasks = [] -> true
6691 ; fully_elastic_relaxation(Tasks, L),
6692 maplist(task_bs, Tasks, Bss),
6693 maplist(arg(1), Tasks, Starts),
6694 maplist(fd_inf, Starts, MinStarts),
6695 maplist(arg(3), Tasks, Ends),
6696 maplist(fd_sup, Ends, MaxEnds),
6697 min_list(MinStarts, Start),
6698 max_list(MaxEnds, End),
6699 resource_limit(Start, End, Tasks, Bss, L)
6700 ).
6701
6706
6707fully_elastic_relaxation(Tasks, Limit) :-
6708 maplist(task_duration_consumption, Tasks, Ds, Cs),
6709 maplist(area, Ds, Cs, As),
6710 sum(As, #=, ?(Area)),
6711 ?(MinTime) #= (Area + Limit - 1) // Limit,
6712 tasks_minstart_maxend(Tasks, MinStart, MaxEnd),
6713 MaxEnd #>= MinStart + MinTime.
6714
6715task_duration_consumption(task(_,D,_,C,_), D, C).
6716
6717area(X, Y, Area) :- ?(Area) #= ?(X) * ?(Y).
6718
6719tasks_minstart_maxend(Tasks, Start, End) :-
6720 maplist(task_start_end, Tasks, [Start0|Starts], [End0|Ends]),
6721 foldl(min_, Starts, Start0, Start),
6722 foldl(max_, Ends, End0, End).
6723
6724max_(E, M0, M) :- ?(M) #= max(E, M0).
6725
6726min_(E, M0, M) :- ?(M) #= min(E, M0).
6727
6728task_start_end(task(Start,_,End,_,_), ?(Start), ?(End)).
6729
6733
6734resource_limit(T, T, _, _, _) :- !.
6735resource_limit(T0, T, Tasks, Bss, L) :-
6736 maplist(contribution_at(T0), Tasks, Bss, Cs),
6737 sum(Cs, #=<, L),
6738 T1 is T0 + 1,
6739 resource_limit(T1, T, Tasks, Bss, L).
6740
6741task_bs(Task, InfStart-Bs) :-
6742 Task = task(Start,D,End,_,_Id),
6743 ?(D) #> 0,
6744 ?(End) #= ?(Start) + ?(D),
6745 maplist(must_be_finite_fdvar, [End,Start,D]),
6746 fd_inf(Start, InfStart),
6747 fd_sup(End, SupEnd),
6748 L is SupEnd - InfStart,
6749 length(Bs, L),
6750 task_running(Bs, Start, End, InfStart).
6751
6752task_running([], _, _, _).
6753task_running([B|Bs], Start, End, T) :-
6754 ((T #>= Start) #/\ (T #< End)) #<==> ?(B),
6755 T1 is T + 1,
6756 task_running(Bs, Start, End, T1).
6757
6758contribution_at(T, Task, Offset-Bs, Contribution) :-
6759 Task = task(Start,_,End,C,_),
6760 ?(C) #>= 0,
6761 fd_inf(Start, InfStart),
6762 fd_sup(End, SupEnd),
6763 ( T < InfStart -> Contribution = 0
6764 ; T >= SupEnd -> Contribution = 0
6765 ; Index is T - Offset,
6766 nth0(Index, Bs, B),
6767 ?(Contribution) #= B*C
6768 ).
6769
6771
6779
6780disjoint2(Rs0) :-
6781 must_be(list, Rs0),
6782 maplist(=.., Rs0, Rs),
6783 non_overlapping(Rs).
6784
6785non_overlapping([]).
6786non_overlapping([R|Rs]) :-
6787 maplist(non_overlapping_(R), Rs),
6788 non_overlapping(Rs).
6789
6790non_overlapping_(A, B) :-
6791 a_not_in_b(A, B),
6792 a_not_in_b(B, A).
6793
6794a_not_in_b([_,AX,AW,AY,AH], [_,BX,BW,BY,BH]) :-
6795 ?(AX) #=< ?(BX) #/\ ?(BX) #< ?(AX) + ?(AW) #==>
6796 ?(AY) + ?(AH) #=< ?(BY) #\/ ?(BY) + ?(BH) #=< ?(AY),
6797 ?(AY) #=< ?(BY) #/\ ?(BY) #< ?(AY) + ?(AH) #==>
6798 ?(AX) + ?(AW) #=< ?(BX) #\/ ?(BX) + ?(BW) #=< ?(AX).
6799
6801
6826
6827automaton(Sigs, Ns, As) :- automaton(_, _, Sigs, Ns, As, [], [], _).
6828
6829
6895
6896template_var_path(V, Var, []) :- var(V), !, V == Var.
6897template_var_path(T, Var, [N|Ns]) :-
6898 arg(N, T, Arg),
6899 template_var_path(Arg, Var, Ns).
6900
6901path_term_variable([], V, V).
6902path_term_variable([P|Ps], T, V) :-
6903 arg(P, T, Arg),
6904 path_term_variable(Ps, Arg, V).
6905
6906initial_expr(_, []-1).
6907
6908automaton(Seqs, Template, Sigs, Ns, As0, Cs, Is, Fs) :-
6909 must_be(list(list), [Sigs,Ns,As0,Cs,Is]),
6910 ( var(Seqs) ->
6911 ( current_prolog_flag(clpfd_monotonic, true) ->
6912 instantiation_error(Seqs)
6913 ; Seqs = Sigs
6914 )
6915 ; must_be(list, Seqs)
6916 ),
6917 maplist(monotonic, Cs, CsM),
6918 maplist(arc_normalized(CsM), As0, As),
6919 include_args1(sink, Ns, Sinks),
6920 include_args1(source, Ns, Sources),
6921 maplist(initial_expr, Cs, Exprs0),
6922 phrase((arcs_relation(As, Relation),
6923 nodes_nums(Sinks, SinkNums0),
6924 nodes_nums(Sources, SourceNums0)),
6925 [s([]-0, Exprs0)], [s(_,Exprs1)]),
6926 maplist(expr0_expr, Exprs1, Exprs),
6927 phrase(transitions(Seqs, Template, Sigs, Start, End, Exprs, Cs, Is, Fs), Tuples),
6928 list_to_drep(SourceNums0, SourceDrep),
6929 Start in SourceDrep,
6930 list_to_drep(SinkNums0, SinkDrep),
6931 End in SinkDrep,
6932 tuples_in(Tuples, Relation).
6933
6934expr0_expr(Es0-_, Es) :-
6935 pairs_keys(Es0, Es1),
6936 reverse(Es1, Es).
6937
6938transitions([], _, [], S, S, _, _, Cs, Cs) --> [].
6939transitions([Seq|Seqs], Template, [Sig|Sigs], S0, S, Exprs, Counters, Cs0, Cs) -->
6940 [[S0,Sig,S1|Is]],
6941 { phrase(exprs_next(Exprs, Is, Cs1), [s(Seq,Template,Counters,Cs0)], _) },
6942 transitions(Seqs, Template, Sigs, S1, S, Exprs, Counters, Cs1, Cs).
6943
6944exprs_next([], [], []) --> [].
6945exprs_next([Es|Ess], [I|Is], [C|Cs]) -->
6946 exprs_values(Es, Vs),
6947 { element(I, Vs, C) },
6948 exprs_next(Ess, Is, Cs).
6949
6950exprs_values([], []) --> [].
6951exprs_values([E0|Es], [V|Vs]) -->
6952 { term_variables(E0, EVs0),
6953 copy_term(E0, E),
6954 term_variables(E, EVs),
6955 ?(V) #= E },
6956 match_variables(EVs0, EVs),
6957 exprs_values(Es, Vs).
6958
6959match_variables([], _) --> [].
6960match_variables([V0|Vs0], [V|Vs]) -->
6961 state(s(Seq,Template,Counters,Cs0)),
6962 { ( template_var_path(Template, V0, Ps) ->
6963 path_term_variable(Ps, Seq, V)
6964 ; template_var_path(Counters, V0, Ps) ->
6965 path_term_variable(Ps, Cs0, V)
6966 ; domain_error(variable_from_template_or_counters, V0)
6967 ) },
6968 match_variables(Vs0, Vs).
6969
6970nodes_nums([], []) --> [].
6971nodes_nums([Node|Nodes], [Num|Nums]) -->
6972 node_num(Node, Num),
6973 nodes_nums(Nodes, Nums).
6974
6975arcs_relation([], []) --> [].
6976arcs_relation([arc(S0,L,S1,Es)|As], [[From,L,To|Ns]|Rs]) -->
6977 node_num(S0, From),
6978 node_num(S1, To),
6979 state(s(Nodes, Exprs0), s(Nodes, Exprs)),
6980 { exprs_nums(Es, Ns, Exprs0, Exprs) },
6981 arcs_relation(As, Rs).
6982
6983exprs_nums([], [], [], []).
6984exprs_nums([E|Es], [N|Ns], [Ex0-C0|Exs0], [Ex-C|Exs]) :-
6985 ( member(Exp-N, Ex0), Exp == E -> C = C0, Ex = Ex0
6986 ; N = C0, C is C0 + 1, Ex = [E-C0|Ex0]
6987 ),
6988 exprs_nums(Es, Ns, Exs0, Exs).
6989
6990node_num(Node, Num) -->
6991 state(s(Nodes0-C0, Exprs), s(Nodes-C, Exprs)),
6992 { ( member(N-Num, Nodes0), N == Node -> C = C0, Nodes = Nodes0
6993 ; Num = C0, C is C0 + 1, Nodes = [Node-C0|Nodes0]
6994 )
6995 }.
6996
6997include_args1(Goal, Ls0, As) :-
6998 include(Goal, Ls0, Ls),
6999 maplist(arg(1), Ls, As).
7000
7001source(source(_)).
7002
7003sink(sink(_)).
7004
7005monotonic(Var, ?(Var)).
7006
7007arc_normalized(Cs, Arc0, Arc) :- arc_normalized_(Arc0, Cs, Arc).
7008
7009arc_normalized_(arc(S0,L,S,Cs), _, arc(S0,L,S,Cs)).
7010arc_normalized_(arc(S0,L,S), Cs, arc(S0,L,S,Cs)).
7011
7013
7067
7068transpose(Ls, Ts) :-
7069 must_be(list(list), Ls),
7070 lists_transpose(Ls, Ts).
7071
7072lists_transpose([], []).
7073lists_transpose([L|Ls], Ts) :-
7074 maplist(same_length(L), Ls),
7075 foldl(transpose_, L, Ts, [L|Ls], _).
7076
7077transpose_(_, Fs, Lists0, Lists) :-
7078 maplist(list_first_rest, Lists0, Fs, Lists).
7079
7080list_first_rest([L|Ls], L, Ls).
7081
7083
7141
7142zcompare(Order, A, B) :-
7143 ( nonvar(Order) ->
7144 zcompare_(Order, A, B)
7145 ; integer(A), integer(B) ->
7146 compare(Order, A, B)
7147 ; freeze(Order, zcompare_(Order, A, B)),
7148 fd_variable(A),
7149 fd_variable(B),
7150 propagator_init_trigger([A,B], pzcompare(Order, A, B))
7151 ).
7152
7153zcompare_(=, A, B) :- ?(A) #= ?(B).
7154zcompare_(<, A, B) :- ?(A) #< ?(B).
7155zcompare_(>, A, B) :- ?(A) #> ?(B).
7156
7169
7170chain(Zs, Relation) :-
7171 must_be(list, Zs),
7172 maplist(fd_variable, Zs),
7173 must_be(ground, Relation),
7174 ( chain_relation(Relation) -> true
7175 ; domain_error(chain_relation, Relation)
7176 ),
7177 chain_(Zs, Relation).
7178
7179chain_([], _).
7180chain_([X|Xs], Relation) :- foldl(chain(Relation), Xs, X, _).
7181
7182chain_relation(#=).
7183chain_relation(#<).
7184chain_relation(#=<).
7185chain_relation(#>).
7186chain_relation(#>=).
7187
7188chain(Relation, X, Prev, X) :- call(Relation, ?(Prev), ?(X)).
7189
7194
7198
7199fd_var(X) :- get_attr(X, clpfd, _).
7200
7204
7205fd_inf(X, Inf) :-
7206 ( fd_get(X, XD, _) ->
7207 domain_infimum(XD, Inf0),
7208 bound_portray(Inf0, Inf)
7209 ; must_be(integer, X),
7210 Inf = X
7211 ).
7212
7216
7217fd_sup(X, Sup) :-
7218 ( fd_get(X, XD, _) ->
7219 domain_supremum(XD, Sup0),
7220 bound_portray(Sup0, Sup)
7221 ; must_be(integer, X),
7222 Sup = X
7223 ).
7224
7230
7231fd_size(X, S) :-
7232 ( fd_get(X, XD, _) ->
7233 domain_num_elements(XD, S0),
7234 bound_portray(S0, S)
7235 ; must_be(integer, X),
7236 S = 1
7237 ).
7238
7268
7269fd_dom(X, Drep) :-
7270 ( fd_get(X, XD, _) ->
7271 domain_to_drep(XD, Drep)
7272 ; must_be(integer, X),
7273 Drep = X..X
7274 ).
7275
7279
7280fd_degree(X, Degree) :-
7281 ( fd_get(X, _, Ps) ->
7282 props_number(Ps, Degree)
7283 ; must_be(integer, X),
7284 Degree = 0
7285 ).
7286
7291
7300
7304
7305X in_set Set :- domain(X, Set).
7306
7310
7311fd_set(X, Set) :-
7312 ( fd_get(X, Set, _) ->
7313 true
7314 ; must_be(integer, X),
7315 Set = from_to(n(X), n(X))
7316 ).
7317
7321
7322is_fdset(Set) :-
7323 nonvar(Set),
7324 is_domain(Set).
7325
7329
7330empty_fdset(empty).
7331
7343
7345fdset_parts(from_to(CMin, CMax), Min, Max, empty) :-
7346 !,
7347 fdset_interval(from_to(CMin, CMax), Min, Max).
7349fdset_parts(Set, Min, Max, Rest) :-
7350 var(Set),
7351 !,
7352 Set = split(Hole, Left, Rest),
7353 fdset_interval(Left, Min, Max),
7354 7355 7356 Max \== sup,
7357 Hole is Max + 1,
7358 7359 all_greater_than(Rest, Hole).
7362fdset_parts(split(_, empty, Right), Min, Max, Rest) :-
7363 !,
7364 fdset_parts(Right, Min, Max, Rest).
7366fdset_parts(split(Hole, Left, Right), Min, Max, Rest) :-
7367 fdset_parts(Left, Min, Max, LeftRest),
7368 ( LeftRest == empty
7369 -> Rest = Right
7370 ; Rest = split(Hole, LeftRest, Right)
7371 ).
7372
7377
7378empty_interval(inf, inf) :- !.
7379empty_interval(sup, inf) :- !.
7380empty_interval(sup, sup) :- !.
7381empty_interval(Min, Max) :-
7382 Min \== inf,
7383 Max \== sup,
7384 Min > Max.
7385
7394
7395fdset_interval(from_to(inf, sup), inf, sup) :- !.
7396fdset_interval(from_to(inf, n(Max)), inf, Max) :-
7397 !,
7398 integer(Max).
7399fdset_interval(from_to(n(Min), sup), Min, sup) :-
7400 !,
7401 integer(Min).
7402fdset_interval(from_to(n(Min), n(Max)), Min, Max) :-
7403 integer(Min),
7404 integer(Max),
7405 Min =< Max.
7406
7412
7413fdset_singleton(Set, Elt) :- fdset_interval(Set, Elt, Elt).
7414
7419
7420fdset_min(Set, Min) :-
7421 domain_infimum(Set, CMin),
7422 bound_portray(CMin, Min).
7423
7428
7429fdset_max(Set, Max) :-
7430 domain_supremum(Set, CMax),
7431 bound_portray(CMax, Max).
7432
7437
7438fdset_size(Set, Size) :-
7439 domain_num_elements(Set, CSize),
7440 bound_portray(CSize, Size).
7441
7446
7447list_to_fdset(List, Set) :- list_to_domain(List, Set).
7448
7453
7454fdset_to_list(Set, List) :- domain_to_list(Set, List).
7455
7460
7461range_to_fdset(Domain, Set) :- drep_to_domain(Domain, Set).
7462
7467
7468fdset_to_range(empty, 1..0) :- !.
7469fdset_to_range(Set, Domain) :- domain_to_drep(Set, Domain).
7470
7475
7476fdset_add_element(Set1, Elt, Set2) :-
7477 fdset_singleton(EltSet, Elt),
7478 domains_union(Set1, EltSet, Set2).
7479
7484
7485fdset_del_element(Set1, Elt, Set2) :- domain_remove(Set1, Elt, Set2).
7486
7490
7491fdset_disjoint(Set1, Set2) :- \+ fdset_intersect(Set1, Set2).
7492
7496
7497fdset_intersect(Set1, Set2) :- domains_intersection(Set1, Set2, _).
7498
7503
7504fdset_intersection(Set1, Set2, Intersection) :-
7505 domains_intersection_(Set1, Set2, Intersection).
7506
7511
7512fdset_member(Elt, Set) :-
7513 ( var(Elt)
7514 -> domain_direction_element(Set, up, Elt)
7515 ; integer(Elt),
7516 domain_contains(Set, Elt)
7517 ).
7518
7525
7526fdset_eq(empty, empty) :- !.
7527fdset_eq(Set1, Set2) :-
7528 fdset_parts(Set1, Min, Max, Rest1),
7529 fdset_parts(Set2, Min, Max, Rest2),
7530 fdset_eq(Rest1, Rest2).
7531
7536
7537fdset_subset(Set1, Set2) :- domain_subdomain(Set2, Set1).
7538
7543
7544fdset_subtract(Set1, Set2, Difference) :-
7545 domain_subtract(Set1, Set2, Difference).
7546
7550
7551fdset_union(Set1, Set2, Union) :- domains_union(Set1, Set2, Union).
7552
7557
7558fdset_union([], empty).
7559fdset_union([Set|Sets], Union) :- fdset_union_(Sets, Set, Union).
7560
7561fdset_union_([], Set, Set).
7562fdset_union_([Set2|Sets], Set1, Union) :-
7563 domains_union(Set1, Set2, SetTemp),
7564 fdset_union_(Sets, SetTemp, Union).
7565
7570
7571fdset_complement(Set, Complement) :- domain_complement(Set, Complement).
7572
7573
7594
7595goals_entail(Goals, E) :-
7596 must_be(list, Goals),
7597 \+ ( maplist(call, Goals), #\ E,
7598 term_variables(Goals-E, Vs),
7599 label(Vs)
7600 ).
7601
7605
7606attr_unify_hook(clpfd_attr(_,_,_,Dom,Ps), Other) :-
7607 ( nonvar(Other) ->
7608 ( integer(Other) -> true
7609 ; type_error(integer, Other)
7610 ),
7611 domain_contains(Dom, Other),
7612 trigger_props(Ps),
7613 do_queue
7614 ; fd_get(Other, OD, OPs),
7615 domains_intersection(OD, Dom, Dom1),
7616 append_propagators(Ps, OPs, Ps1),
7617 fd_put(Other, Dom1, Ps1),
7618 trigger_props(Ps1),
7619 do_queue
7620 ).
7621
7622append_propagators(fd_props(Gs0,Bs0,Os0), fd_props(Gs1,Bs1,Os1), fd_props(Gs,Bs,Os)) :-
7623 maplist(append, [Gs0,Bs0,Os0], [Gs1,Bs1,Os1], [Gs,Bs,Os]).
7624
7625bound_portray(inf, inf).
7626bound_portray(sup, sup).
7627bound_portray(n(N), N).
7628
7629list_to_drep(List, Drep) :-
7630 list_to_domain(List, Dom),
7631 domain_to_drep(Dom, Drep).
7632
7633domain_to_drep(Dom, Drep) :-
7634 domain_intervals(Dom, [A0-B0|Rest]),
7635 bound_portray(A0, A),
7636 bound_portray(B0, B),
7637 ( A == B -> Drep0 = A
7638 ; Drep0 = A..B
7639 ),
7640 intervals_to_drep(Rest, Drep0, Drep).
7641
7642intervals_to_drep([], Drep, Drep).
7643intervals_to_drep([A0-B0|Rest], Drep0, Drep) :-
7644 bound_portray(A0, A),
7645 bound_portray(B0, B),
7646 ( A == B -> D1 = A
7647 ; D1 = A..B
7648 ),
7649 intervals_to_drep(Rest, Drep0 \/ D1, Drep).
7650
7651attribute_goals(X) -->
7652 7653 { get_attr(X, clpfd, clpfd_attr(_,_,_,Dom,fd_props(Gs,Bs,Os))),
7654 append(Gs, Bs, Ps0),
7655 append(Ps0, Os, Ps),
7656 domain_to_drep(Dom, Drep) },
7657 ( { default_domain(Dom), \+ all_dead_(Ps) } -> []
7658 ; [clpfd:(X in Drep)]
7659 ),
7660 attributes_goals(Ps).
7661
7662clpfd_aux:attribute_goals(_) --> [].
7663clpfd_aux:attr_unify_hook(_,_) :- false.
7664
7665clpfd_gcc_vs:attribute_goals(_) --> [].
7666clpfd_gcc_vs:attr_unify_hook(_,_) :- false.
7667
7668clpfd_gcc_num:attribute_goals(_) --> [].
7669clpfd_gcc_num:attr_unify_hook(_,_) :- false.
7670
7671clpfd_gcc_occurred:attribute_goals(_) --> [].
7672clpfd_gcc_occurred:attr_unify_hook(_,_) :- false.
7673
7674clpfd_relation:attribute_goals(_) --> [].
7675clpfd_relation:attr_unify_hook(_,_) :- false.
7676
7677attributes_goals([]) --> [].
7678attributes_goals([propagator(P, State)|As]) -->
7679 ( { ground(State) } -> []
7680 ; { phrase(attribute_goal_(P), Gs) } ->
7681 { del_attr(State, clpfd_aux), State = processed,
7682 ( current_prolog_flag(clpfd_monotonic, true) ->
7683 maplist(unwrap_with(bare_integer), Gs, Gs1)
7684 ; maplist(unwrap_with(=), Gs, Gs1)
7685 ),
7686 maplist(with_clpfd, Gs1, Gs2) },
7687 list(Gs2)
7688 ; [P] 7689 ),
7690 attributes_goals(As).
7691
7692with_clpfd(G, clpfd:G).
7693
7694unwrap_with(_, V, V) :- var(V), !.
7695unwrap_with(Goal, ?(V0), V) :- !, call(Goal, V0, V).
7696unwrap_with(Goal, Term0, Term) :-
7697 Term0 =.. [F|Args0],
7698 maplist(unwrap_with(Goal), Args0, Args),
7699 Term =.. [F|Args].
7700
7701bare_integer(V0, V) :- ( integer(V0) -> V = V0 ; V = #(V0) ).
7702
7703attribute_goal_(presidual(Goal)) --> [Goal].
7704attribute_goal_(pgeq(A,B)) --> [?(A) #>= ?(B)].
7705attribute_goal_(pplus(X,Y,Z)) --> [?(X) + ?(Y) #= ?(Z)].
7706attribute_goal_(pneq(A,B)) --> [?(A) #\= ?(B)].
7707attribute_goal_(ptimes(X,Y,Z)) --> [?(X) * ?(Y) #= ?(Z)].
7708attribute_goal_(absdiff_neq(X,Y,C)) --> [abs(?(X) - ?(Y)) #\= C].
7709attribute_goal_(absdiff_geq(X,Y,C)) --> [abs(?(X) - ?(Y)) #>= C].
7710attribute_goal_(x_neq_y_plus_z(X,Y,Z)) --> [?(X) #\= ?(Y) + ?(Z)].
7711attribute_goal_(x_leq_y_plus_c(X,Y,C)) --> [?(X) #=< ?(Y) + C].
7712attribute_goal_(ptzdiv(X,Y,Z)) --> [?(X) // ?(Y) #= ?(Z)].
7713attribute_goal_(pdiv(X,Y,Z)) --> [?(X) div ?(Y) #= ?(Z)].
7714attribute_goal_(prdiv(X,Y,Z)) --> [?(X) rdiv ?(Y) #= ?(Z)].
7715attribute_goal_(pshift(X,Y,Z,1)) --> [?(X) << ?(Y) #= ?(Z)].
7716attribute_goal_(pshift(X,Y,Z,-1)) --> [?(X) >> ?(Y) #= ?(Z)].
7717attribute_goal_(pexp(X,Y,Z)) --> [?(X) ^ ?(Y) #= ?(Z)].
7718attribute_goal_(pabs(X,Y)) --> [?(Y) #= abs(?(X))].
7719attribute_goal_(pmod(X,M,K)) --> [?(X) mod ?(M) #= ?(K)].
7720attribute_goal_(prem(X,Y,Z)) --> [?(X) rem ?(Y) #= ?(Z)].
7721attribute_goal_(pmax(X,Y,Z)) --> [?(Z) #= max(?(X),?(Y))].
7722attribute_goal_(pmin(X,Y,Z)) --> [?(Z) #= min(?(X),?(Y))].
7723attribute_goal_(scalar_product_neq(Cs,Vs,C)) -->
7724 [Left #\= Right],
7725 { scalar_product_left_right([-1|Cs], [C|Vs], Left, Right) }.
7726attribute_goal_(scalar_product_eq(Cs,Vs,C)) -->
7727 [Left #= Right],
7728 { scalar_product_left_right([-1|Cs], [C|Vs], Left, Right) }.
7729attribute_goal_(scalar_product_leq(Cs,Vs,C)) -->
7730 [Left #=< Right],
7731 { scalar_product_left_right([-1|Cs], [C|Vs], Left, Right) }.
7732attribute_goal_(pdifferent(_,_,_,O)) --> original_goal(O).
7733attribute_goal_(weak_distinct(_,_,_,O)) --> original_goal(O).
7734attribute_goal_(pdistinct(Vs)) --> [all_distinct(Vs)].
7735attribute_goal_(pexclude(_,_,_)) --> [].
7736attribute_goal_(pelement(N,Is,V)) --> [element(N, Is, V)].
7737attribute_goal_(pgcc(Vs, Pairs, _)) --> [global_cardinality(Vs, Pairs)].
7738attribute_goal_(pgcc_single(_,_)) --> [].
7739attribute_goal_(pgcc_check_single(_)) --> [].
7740attribute_goal_(pgcc_check(_)) --> [].
7741attribute_goal_(pcircuit(Vs)) --> [circuit(Vs)].
7742attribute_goal_(pserialized(_,_,_,_,O)) --> original_goal(O).
7743attribute_goal_(rel_tuple(R, Tuple)) -->
7744 { get_attr(R, clpfd_relation, Rel) },
7745 [tuples_in([Tuple], Rel)].
7746attribute_goal_(pzcompare(O,A,B)) --> [zcompare(O,A,B)].
7748attribute_goal_(reified_in(V, D, B)) -->
7749 [V in Drep #<==> ?(B)],
7750 { domain_to_drep(D, Drep) }.
7751attribute_goal_(reified_tuple_in(Tuple, R, B)) -->
7752 { get_attr(R, clpfd_relation, Rel) },
7753 [tuples_in([Tuple], Rel) #<==> ?(B)].
7754attribute_goal_(kill_reified_tuples(_,_,_)) --> [].
7755attribute_goal_(tuples_not_in(_,_,_)) --> [].
7756attribute_goal_(reified_fd(V,B)) --> [finite_domain(V) #<==> ?(B)].
7757attribute_goal_(pskeleton(X,Y,D,_,Z,F)) -->
7758 { Prop =.. [F,X,Y,Z],
7759 phrase(attribute_goal_(Prop), Goals), list_goal(Goals, Goal) },
7760 [?(D) #= 1 #==> Goal, ?(Y) #\= 0 #==> ?(D) #= 1].
7761attribute_goal_(reified_neq(DX,X,DY,Y,_,B)) -->
7762 conjunction(DX, DY, ?(X) #\= ?(Y), B).
7763attribute_goal_(reified_eq(DX,X,DY,Y,_,B)) -->
7764 conjunction(DX, DY, ?(X) #= ?(Y), B).
7765attribute_goal_(reified_geq(DX,X,DY,Y,_,B)) -->
7766 conjunction(DX, DY, ?(X) #>= ?(Y), B).
7767attribute_goal_(reified_and(X,_,Y,_,B)) --> [?(X) #/\ ?(Y) #<==> ?(B)].
7768attribute_goal_(reified_or(X, _, Y, _, B)) --> [?(X) #\/ ?(Y) #<==> ?(B)].
7769attribute_goal_(reified_not(X, Y)) --> [#\ ?(X) #<==> ?(Y)].
7770attribute_goal_(pimpl(X, Y, _)) --> [?(X) #==> ?(Y)].
7771attribute_goal_(pfunction(Op, A, B, R)) -->
7772 { Expr =.. [Op,?(A),?(B)] },
7773 [?(R) #= Expr].
7774attribute_goal_(pfunction(Op, A, R)) -->
7775 { Expr =.. [Op,?(A)] },
7776 [?(R) #= Expr].
7777
7778conjunction(A, B, G, D) -->
7779 ( { A == 1, B == 1 } -> [G #<==> ?(D)]
7780 ; { A == 1 } -> [(?(B) #/\ G) #<==> ?(D)]
7781 ; { B == 1 } -> [(?(A) #/\ G) #<==> ?(D)]
7782 ; [(?(A) #/\ ?(B) #/\ G) #<==> ?(D)]
7783 ).
7784
7785original_goal(original_goal(State, Goal)) -->
7786 ( { var(State) } ->
7787 { State = processed },
7788 [Goal]
7789 ; []
7790 ).
7791
7795
7796scalar_product_left_right(Cs, Vs, Left, Right) :-
7797 pairs_keys_values(Pairs0, Cs, Vs),
7798 partition(ground, Pairs0, Grounds, Pairs),
7799 maplist(pair_product, Grounds, Prods),
7800 sum_list(Prods, Const),
7801 NConst is -Const,
7802 partition(compare_coeff0, Pairs, Negatives, _, Positives),
7803 maplist(negate_coeff, Negatives, Rights),
7804 scalar_plusterm(Rights, Right0),
7805 scalar_plusterm(Positives, Left0),
7806 ( Const =:= 0 -> Left = Left0, Right = Right0
7807 ; Right0 == 0 -> Left = Left0, Right = NConst
7808 ; Left0 == 0 -> Left = Const, Right = Right0
7809 ; ( Const < 0 ->
7810 Left = Left0, Right = Right0+NConst
7811 ; Left = Left0+Const, Right = Right0
7812 )
7813 ).
7814
7815negate_coeff(A0-B, A-B) :- A is -A0.
7816
7817pair_product(A-B, Prod) :- Prod is A*B.
7818
7819compare_coeff0(Coeff-_, Compare) :- compare(Compare, Coeff, 0).
7820
7821scalar_plusterm([], 0).
7822scalar_plusterm([CV|CVs], T) :-
7823 coeff_var_term(CV, T0),
7824 foldl(plusterm_, CVs, T0, T).
7825
7826plusterm_(CV, T0, T0+T) :- coeff_var_term(CV, T).
7827
7828coeff_var_term(C-V, T) :- ( C =:= 1 -> T = ?(V) ; T = C * ?(V) ).
7829
7833
7834:- discontiguous term_expansion/2. 7835
7836term_expansion(make_parse_clpfd, Clauses) :- make_parse_clpfd(Clauses).
7837term_expansion(make_parse_reified, Clauses) :- make_parse_reified(Clauses).
7838term_expansion(make_matches, Clauses) :- make_matches(Clauses).
7839
7840make_parse_clpfd.
7841make_parse_reified.
7842make_matches.
7843
7847
7848make_clpfd_var('$clpfd_queue') :-
7849 make_queue.
7850make_clpfd_var('$clpfd_current_propagator') :-
7851 nb_setval('$clpfd_current_propagator', []).
7852make_clpfd_var('$clpfd_queue_status') :-
7853 nb_setval('$clpfd_queue_status', enabled).
7854
7855:- multifile user:exception/3. 7856
7857user:exception(undefined_global_variable, Name, retry) :-
7858 make_clpfd_var(Name), !.
7859
7860warn_if_bounded_arithmetic :-
7861 ( current_prolog_flag(bounded, true) ->
7862 print_message(warning, clpfd(bounded))
7863 ; true
7864 ).
7865
7866:- initialization(warn_if_bounded_arithmetic). 7867
7868
7872
7873:- multifile prolog:message//1. 7874
7875prolog:message(clpfd(bounded)) -->
7876 ['Using CLP(FD) with bounded arithmetic may yield wrong results.'-[]].
7877
7878
7879 7882
7889
7890:- multifile
7891 sandbox:safe_primitive/1. 7892
7893safe_api(Name/Arity, sandbox:safe_primitive(clpfd:Head)) :-
7894 functor(Head, Name, Arity).
7895
7896term_expansion(safe_api, Clauses) :-
7897 module_property(clpfd, exports(API)),
7898 maplist(safe_api, API, Clauses).
7899
7900safe_api.
7902sandbox:safe_primitive(clpfd:clpfd_equal(_,_)).
7903sandbox:safe_primitive(clpfd:clpfd_geq(_,_)).
7904sandbox:safe_primitive(clpfd:clpfd_in(_,_)).
7906sandbox:safe_primitive(set_prolog_flag(clpfd_monotonic, _))