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