34
74
75:- module(clpfd, [
76 op(760, yfx, #<==>),
77 op(750, xfy, #==>),
78 op(750, yfx, #<==),
79 op(740, yfx, #\/),
80 op(730, yfx, #\),
81 op(720, yfx, #/\),
82 op(710, fy, #\),
83 op(700, xfx, #>),
84 op(700, xfx, #<),
85 op(700, xfx, #>=),
86 op(700, xfx, #=<),
87 op(700, xfx, #=),
88 op(700, xfx, #\=),
89 op(700, xfx, in),
90 op(700, xfx, ins),
91 op(450, xfx, ..), 92 (#>)/2,
93 (#<)/2,
94 (#>=)/2,
95 (#=<)/2,
96 (#=)/2,
97 (#\=)/2,
98 (#\)/1,
99 (#<==>)/2,
100 (#==>)/2,
101 (#<==)/2,
102 (#\/)/2,
103 (#\)/2,
104 (#/\)/2,
105 (in)/2,
106 (ins)/2,
107 all_different/1,
108 all_distinct/1,
109 sum/3,
110 scalar_product/4,
111 tuples_in/2,
112 labeling/2,
113 label/1,
114 indomain/1,
115 lex_chain/1,
116 serialized/2,
117 global_cardinality/2,
118 global_cardinality/3,
119 circuit/1,
120 cumulative/1,
121 cumulative/2,
122 disjoint2/1,
123 element/3,
124 automaton/3,
125 automaton/8,
126 transpose/2,
127 zcompare/3,
128 chain/2,
129 fd_var/1,
130 fd_inf/2,
131 fd_sup/2,
132 fd_size/2,
133 fd_dom/2
134 ]). 135
136:- public 137 clpfd_equal/2,
138 clpfd_geq/2. 139
140:- use_module(library(apply)). 141:- use_module(library(apply_macros)). 142:- use_module(library(assoc)). 143:- use_module(library(error)). 144:- use_module(library(lists)). 145:- use_module(library(pairs)). 146
147:- op(700, xfx, cis). 148:- op(700, xfx, cis_geq). 149:- op(700, xfx, cis_gt). 150:- op(700, xfx, cis_leq). 151:- op(700, xfx, cis_lt). 152
926
927:- create_prolog_flag(clpfd_monotonic, false, []). 928
936
937is_bound(n(N)) :- integer(N).
938is_bound(inf).
939is_bound(sup).
940
941defaulty_to_bound(D, P) :- ( integer(D) -> P = n(D) ; P = D ).
942
947
948goal_expansion(A cis B, Expansion) :-
949 phrase(cis_goals(B, A), Goals),
950 list_goal(Goals, Expansion).
951goal_expansion(A cis_lt B, B cis_gt A).
952goal_expansion(A cis_leq B, B cis_geq A).
953goal_expansion(A cis_geq B, cis_leq_numeric(B, N)) :- nonvar(A), A = n(N).
954goal_expansion(A cis_geq B, cis_geq_numeric(A, N)) :- nonvar(B), B = n(N).
955goal_expansion(A cis_gt B, cis_lt_numeric(B, N)) :- nonvar(A), A = n(N).
956goal_expansion(A cis_gt B, cis_gt_numeric(A, N)) :- nonvar(B), B = n(N).
957
959cis_gt(sup, B0) :- B0 \== sup.
960cis_gt(n(N), B) :- cis_lt_numeric(B, N).
961
962cis_lt_numeric(inf, _).
963cis_lt_numeric(n(B), A) :- B < A.
964
965cis_gt_numeric(sup, _).
966cis_gt_numeric(n(B), A) :- B > A.
967
968cis_geq(inf, inf).
969cis_geq(sup, _).
970cis_geq(n(N), B) :- cis_leq_numeric(B, N).
971
972cis_leq_numeric(inf, _).
973cis_leq_numeric(n(B), A) :- B =< A.
974
975cis_geq_numeric(sup, _).
976cis_geq_numeric(n(B), A) :- B >= A.
977
978cis_min(inf, _, inf).
979cis_min(sup, B, B).
980cis_min(n(N), B, Min) :- cis_min_(B, N, Min).
981
982cis_min_(inf, _, inf).
983cis_min_(sup, N, n(N)).
984cis_min_(n(B), A, n(M)) :- M is min(A,B).
985
986cis_max(sup, _, sup).
987cis_max(inf, B, B).
988cis_max(n(N), B, Max) :- cis_max_(B, N, Max).
989
990cis_max_(inf, N, n(N)).
991cis_max_(sup, _, sup).
992cis_max_(n(B), A, n(M)) :- M is max(A,B).
993
994cis_plus(inf, _, inf).
995cis_plus(sup, _, sup).
996cis_plus(n(A), B, Plus) :- cis_plus_(B, A, Plus).
997
998cis_plus_(sup, _, sup).
999cis_plus_(inf, _, inf).
1000cis_plus_(n(B), A, n(S)) :- S is A + B.
1001
1002cis_minus(inf, _, inf).
1003cis_minus(sup, _, sup).
1004cis_minus(n(A), B, M) :- cis_minus_(B, A, M).
1005
1006cis_minus_(inf, _, sup).
1007cis_minus_(sup, _, inf).
1008cis_minus_(n(B), A, n(M)) :- M is A - B.
1009
1010cis_uminus(inf, sup).
1011cis_uminus(sup, inf).
1012cis_uminus(n(A), n(B)) :- B is -A.
1013
1014cis_abs(inf, sup).
1015cis_abs(sup, sup).
1016cis_abs(n(A), n(B)) :- B is abs(A).
1017
1018cis_times(inf, B, P) :-
1019 ( B cis_lt n(0) -> P = sup
1020 ; B cis_gt n(0) -> P = inf
1021 ; P = n(0)
1022 ).
1023cis_times(sup, B, P) :-
1024 ( B cis_gt n(0) -> P = sup
1025 ; B cis_lt n(0) -> P = inf
1026 ; P = n(0)
1027 ).
1028cis_times(n(N), B, P) :- cis_times_(B, N, P).
1029
1030cis_times_(inf, A, P) :- cis_times(inf, n(A), P).
1031cis_times_(sup, A, P) :- cis_times(sup, n(A), P).
1032cis_times_(n(B), A, n(P)) :- P is A * B.
1033
1034cis_exp(inf, n(Y), R) :-
1035 ( even(Y) -> R = sup
1036 ; R = inf
1037 ).
1038cis_exp(sup, _, sup).
1039cis_exp(n(N), Y, R) :- cis_exp_(Y, N, R).
1040
1041cis_exp_(n(Y), N, n(R)) :- R is N^Y.
1042cis_exp_(sup, _, sup).
1043cis_exp_(inf, _, inf).
1044
1045cis_goals(V, V) --> { var(V) }, !.
1046cis_goals(n(N), n(N)) --> [].
1047cis_goals(inf, inf) --> [].
1048cis_goals(sup, sup) --> [].
1049cis_goals(sign(A0), R) --> cis_goals(A0, A), [cis_sign(A, R)].
1050cis_goals(abs(A0), R) --> cis_goals(A0, A), [cis_abs(A, R)].
1051cis_goals(-A0, R) --> cis_goals(A0, A), [cis_uminus(A, R)].
1052cis_goals(A0+B0, R) -->
1053 cis_goals(A0, A),
1054 cis_goals(B0, B),
1055 [cis_plus(A, B, R)].
1056cis_goals(A0-B0, R) -->
1057 cis_goals(A0, A),
1058 cis_goals(B0, B),
1059 [cis_minus(A, B, R)].
1060cis_goals(min(A0,B0), R) -->
1061 cis_goals(A0, A),
1062 cis_goals(B0, B),
1063 [cis_min(A, B, R)].
1064cis_goals(max(A0,B0), R) -->
1065 cis_goals(A0, A),
1066 cis_goals(B0, B),
1067 [cis_max(A, B, R)].
1068cis_goals(A0*B0, R) -->
1069 cis_goals(A0, A),
1070 cis_goals(B0, B),
1071 [cis_times(A, B, R)].
1072cis_goals(div(A0,B0), R) -->
1073 cis_goals(A0, A),
1074 cis_goals(B0, B),
1075 [cis_div(A, B, R)].
1076cis_goals(A0//B0, R) -->
1077 cis_goals(A0, A),
1078 cis_goals(B0, B),
1079 [cis_slash(A, B, R)].
1080cis_goals(A0^B0, R) -->
1081 cis_goals(A0, A),
1082 cis_goals(B0, B),
1083 [cis_exp(A, B, R)].
1084
1085list_goal([], true).
1086list_goal([G|Gs], Goal) :- foldl(list_goal_, Gs, G, Goal).
1087
1088list_goal_(G, G0, (G0,G)).
1089
1090cis_sign(sup, n(1)).
1091cis_sign(inf, n(-1)).
1092cis_sign(n(N), n(S)) :- S is sign(N).
1093
1094cis_div(sup, Y, Z) :- ( Y cis_geq n(0) -> Z = sup ; Z = inf ).
1095cis_div(inf, Y, Z) :- ( Y cis_geq n(0) -> Z = inf ; Z = sup ).
1096cis_div(n(X), Y, Z) :- cis_div_(Y, X, Z).
1097
1098cis_div_(sup, _, n(0)).
1099cis_div_(inf, _, n(0)).
1100cis_div_(n(Y), X, Z) :-
1101 ( Y =:= 0 -> ( X >= 0 -> Z = sup ; Z = inf )
1102 ; Z0 is X // Y, Z = n(Z0)
1103 ).
1104
1105cis_slash(sup, _, sup).
1106cis_slash(inf, _, inf).
1107cis_slash(n(N), B, S) :- cis_slash_(B, N, S).
1108
1109cis_slash_(sup, _, n(0)).
1110cis_slash_(inf, _, n(0)).
1111cis_slash_(n(B), A, n(S)) :- S is A // B.
1112
1113
1130
1134
1135check_domain(D) :-
1136 ( var(D) -> instantiation_error(D)
1137 ; is_domain(D) -> true
1138 ; domain_error(clpfd_domain, D)
1139 ).
1140
1141is_domain(empty).
1142is_domain(from_to(From,To)) :-
1143 is_bound(From), is_bound(To),
1144 From cis_leq To.
1145is_domain(split(S, Left, Right)) :-
1146 integer(S),
1147 is_domain(Left), is_domain(Right),
1148 all_less_than(Left, S),
1149 all_greater_than(Right, S).
1150
1151all_less_than(empty, _).
1152all_less_than(from_to(From,To), S) :-
1153 From cis_lt n(S), To cis_lt n(S).
1154all_less_than(split(S0,Left,Right), S) :-
1155 S0 < S,
1156 all_less_than(Left, S),
1157 all_less_than(Right, S).
1158
1159all_greater_than(empty, _).
1160all_greater_than(from_to(From,To), S) :-
1161 From cis_gt n(S), To cis_gt n(S).
1162all_greater_than(split(S0,Left,Right), S) :-
1163 S0 > S,
1164 all_greater_than(Left, S),
1165 all_greater_than(Right, S).
1166
1167default_domain(from_to(inf,sup)).
1168
1169domain_infimum(from_to(I, _), I).
1170domain_infimum(split(_, Left, _), I) :- domain_infimum(Left, I).
1171
1172domain_supremum(from_to(_, S), S).
1173domain_supremum(split(_, _, Right), S) :- domain_supremum(Right, S).
1174
1175domain_num_elements(empty, n(0)).
1176domain_num_elements(from_to(From,To), Num) :- Num cis To - From + n(1).
1177domain_num_elements(split(_, Left, Right), Num) :-
1178 domain_num_elements(Left, NL),
1179 domain_num_elements(Right, NR),
1180 Num cis NL + NR.
1181
1182domain_direction_element(from_to(n(From), n(To)), Dir, E) :-
1183 ( Dir == up -> between(From, To, E)
1184 ; between(From, To, E0),
1185 E is To - (E0 - From)
1186 ).
1187domain_direction_element(split(_, D1, D2), Dir, E) :-
1188 ( Dir == up ->
1189 ( domain_direction_element(D1, Dir, E)
1190 ; domain_direction_element(D2, Dir, E)
1191 )
1192 ; ( domain_direction_element(D2, Dir, E)
1193 ; domain_direction_element(D1, Dir, E)
1194 )
1195 ).
1196
1200
1201domain_contains(from_to(From,To), I) :- From cis_leq n(I), n(I) cis_leq To.
1202domain_contains(split(S, Left, Right), I) :-
1203 ( I < S -> domain_contains(Left, I)
1204 ; I > S -> domain_contains(Right, I)
1205 ).
1206
1210
1211domain_subdomain(Dom, Sub) :- domain_subdomain(Dom, Dom, Sub).
1212
1213domain_subdomain(from_to(_,_), Dom, Sub) :-
1214 domain_subdomain_fromto(Sub, Dom).
1215domain_subdomain(split(_, _, _), Dom, Sub) :-
1216 domain_subdomain_split(Sub, Dom, Sub).
1217
1218domain_subdomain_split(empty, _, _).
1219domain_subdomain_split(from_to(From,To), split(S,Left0,Right0), Sub) :-
1220 ( To cis_lt n(S) -> domain_subdomain(Left0, Left0, Sub)
1221 ; From cis_gt n(S) -> domain_subdomain(Right0, Right0, Sub)
1222 ).
1223domain_subdomain_split(split(_,Left,Right), Dom, _) :-
1224 domain_subdomain(Dom, Dom, Left),
1225 domain_subdomain(Dom, Dom, Right).
1226
1227domain_subdomain_fromto(empty, _).
1228domain_subdomain_fromto(from_to(From,To), from_to(From0,To0)) :-
1229 From0 cis_leq From, To0 cis_geq To.
1230domain_subdomain_fromto(split(_,Left,Right), Dom) :-
1231 domain_subdomain_fromto(Left, Dom),
1232 domain_subdomain_fromto(Right, Dom).
1233
1239
1240domain_remove(empty, _, empty).
1241domain_remove(from_to(L0, U0), X, D) :- domain_remove_(L0, U0, X, D).
1242domain_remove(split(S, Left0, Right0), X, D) :-
1243 ( X =:= S -> D = split(S, Left0, Right0)
1244 ; X < S ->
1245 domain_remove(Left0, X, Left1),
1246 ( Left1 == empty -> D = Right0
1247 ; D = split(S, Left1, Right0)
1248 )
1249 ; domain_remove(Right0, X, Right1),
1250 ( Right1 == empty -> D = Left0
1251 ; D = split(S, Left0, Right1)
1252 )
1253 ).
1254
1256
1257domain_remove_(inf, U0, X, D) :-
1258 ( U0 == n(X) -> U1 is X - 1, D = from_to(inf, n(U1))
1259 ; U0 cis_lt n(X) -> D = from_to(inf,U0)
1260 ; L1 is X + 1, U1 is X - 1,
1261 D = split(X, from_to(inf, n(U1)), from_to(n(L1),U0))
1262 ).
1263domain_remove_(n(N), U0, X, D) :- domain_remove_upper(U0, N, X, D).
1264
1265domain_remove_upper(sup, L0, X, D) :-
1266 ( L0 =:= X -> L1 is X + 1, D = from_to(n(L1),sup)
1267 ; L0 > X -> D = from_to(n(L0),sup)
1268 ; L1 is X + 1, U1 is X - 1,
1269 D = split(X, from_to(n(L0),n(U1)), from_to(n(L1),sup))
1270 ).
1271domain_remove_upper(n(U0), L0, X, D) :-
1272 ( L0 =:= U0, X =:= L0 -> D = empty
1273 ; L0 =:= X -> L1 is X + 1, D = from_to(n(L1), n(U0))
1274 ; U0 =:= X -> U1 is X - 1, D = from_to(n(L0), n(U1))
1275 ; between(L0, U0, X) ->
1276 U1 is X - 1, L1 is X + 1,
1277 D = split(X, from_to(n(L0), n(U1)), from_to(n(L1), n(U0)))
1278 ; D = from_to(n(L0),n(U0))
1279 ).
1280
1284
1285domain_remove_greater_than(empty, _, empty).
1286domain_remove_greater_than(from_to(From0,To0), G, D) :-
1287 ( From0 cis_gt n(G) -> D = empty
1288 ; To cis min(To0,n(G)), D = from_to(From0,To)
1289 ).
1290domain_remove_greater_than(split(S,Left0,Right0), G, D) :-
1291 ( S =< G ->
1292 domain_remove_greater_than(Right0, G, Right),
1293 ( Right == empty -> D = Left0
1294 ; D = split(S, Left0, Right)
1295 )
1296 ; domain_remove_greater_than(Left0, G, D)
1297 ).
1298
1299domain_remove_smaller_than(empty, _, empty).
1300domain_remove_smaller_than(from_to(From0,To0), V, D) :-
1301 ( To0 cis_lt n(V) -> D = empty
1302 ; From cis max(From0,n(V)), D = from_to(From,To0)
1303 ).
1304domain_remove_smaller_than(split(S,Left0,Right0), V, D) :-
1305 ( S >= V ->
1306 domain_remove_smaller_than(Left0, V, Left),
1307 ( Left == empty -> D = Right0
1308 ; D = split(S, Left, Right0)
1309 )
1310 ; domain_remove_smaller_than(Right0, V, D)
1311 ).
1312
1313
1317
1318domain_subtract(Dom0, Sub, Dom) :- domain_subtract(Dom0, Dom0, Sub, Dom).
1319
1320domain_subtract(empty, _, _, empty).
1321domain_subtract(from_to(From0,To0), Dom, Sub, D) :-
1322 ( Sub == empty -> D = Dom
1323 ; Sub = from_to(From,To) ->
1324 ( From == To -> From = n(X), domain_remove(Dom, X, D)
1325 ; From cis_gt To0 -> D = Dom
1326 ; To cis_lt From0 -> D = Dom
1327 ; From cis_leq From0 ->
1328 ( To cis_geq To0 -> D = empty
1329 ; From1 cis To + n(1),
1330 D = from_to(From1, To0)
1331 )
1332 ; To1 cis From - n(1),
1333 ( To cis_lt To0 ->
1334 From = n(S),
1335 From2 cis To + n(1),
1336 D = split(S,from_to(From0,To1),from_to(From2,To0))
1337 ; D = from_to(From0,To1)
1338 )
1339 )
1340 ; Sub = split(S, Left, Right) ->
1341 ( n(S) cis_gt To0 -> domain_subtract(Dom, Dom, Left, D)
1342 ; n(S) cis_lt From0 -> domain_subtract(Dom, Dom, Right, D)
1343 ; domain_subtract(Dom, Dom, Left, D1),
1344 domain_subtract(D1, D1, Right, D)
1345 )
1346 ).
1347domain_subtract(split(S, Left0, Right0), _, Sub, D) :-
1348 domain_subtract(Left0, Left0, Sub, Left),
1349 domain_subtract(Right0, Right0, Sub, Right),
1350 ( Left == empty -> D = Right
1351 ; Right == empty -> D = Left
1352 ; D = split(S, Left, Right)
1353 ).
1354
1358
1359domain_complement(D, C) :-
1360 default_domain(Default),
1361 domain_subtract(Default, D, C).
1362
1366
1367domain_intervals(D, Is) :- phrase(domain_intervals(D), Is).
1368
1369domain_intervals(split(_, Left, Right)) -->
1370 domain_intervals(Left), domain_intervals(Right).
1371domain_intervals(empty) --> [].
1372domain_intervals(from_to(From,To)) --> [From-To].
1373
1379
1380domains_intersection(D1, D2, Intersection) :-
1381 domains_intersection_(D1, D2, Intersection),
1382 Intersection \== empty.
1383
1384domains_intersection_(empty, _, empty).
1385domains_intersection_(from_to(L0,U0), D2, Dom) :-
1386 narrow(D2, L0, U0, Dom).
1387domains_intersection_(split(S,Left0,Right0), D2, Dom) :-
1388 domains_intersection_(Left0, D2, Left1),
1389 domains_intersection_(Right0, D2, Right1),
1390 ( Left1 == empty -> Dom = Right1
1391 ; Right1 == empty -> Dom = Left1
1392 ; Dom = split(S, Left1, Right1)
1393 ).
1394
1395narrow(empty, _, _, empty).
1396narrow(from_to(L0,U0), From0, To0, Dom) :-
1397 From1 cis max(From0,L0), To1 cis min(To0,U0),
1398 ( From1 cis_gt To1 -> Dom = empty
1399 ; Dom = from_to(From1,To1)
1400 ).
1401narrow(split(S, Left0, Right0), From0, To0, Dom) :-
1402 ( To0 cis_lt n(S) -> narrow(Left0, From0, To0, Dom)
1403 ; From0 cis_gt n(S) -> narrow(Right0, From0, To0, Dom)
1404 ; narrow(Left0, From0, To0, Left1),
1405 narrow(Right0, From0, To0, Right1),
1406 ( Left1 == empty -> Dom = Right1
1407 ; Right1 == empty -> Dom = Left1
1408 ; Dom = split(S, Left1, Right1)
1409 )
1410 ).
1411
1415
1416domains_union(D1, D2, Union) :-
1417 domain_intervals(D1, Is1),
1418 domain_intervals(D2, Is2),
1419 append(Is1, Is2, IsU0),
1420 merge_intervals(IsU0, IsU1),
1421 intervals_to_domain(IsU1, Union).
1422
1426
1427domain_shift(empty, _, empty).
1428domain_shift(from_to(From0,To0), O, from_to(From,To)) :-
1429 From cis From0 + n(O), To cis To0 + n(O).
1430domain_shift(split(S0, Left0, Right0), O, split(S, Left, Right)) :-
1431 S is S0 + O,
1432 domain_shift(Left0, O, Left),
1433 domain_shift(Right0, O, Right).
1434
1439
1440domain_expand(D0, M, D) :-
1441 ( M < 0 ->
1442 domain_negate(D0, D1),
1443 M1 is abs(M),
1444 domain_expand_(D1, M1, D)
1445 ; M =:= 1 -> D = D0
1446 ; domain_expand_(D0, M, D)
1447 ).
1448
1449domain_expand_(empty, _, empty).
1450domain_expand_(from_to(From0, To0), M, from_to(From,To)) :-
1451 From cis From0*n(M),
1452 To cis To0*n(M).
1453domain_expand_(split(S0, Left0, Right0), M, split(S, Left, Right)) :-
1454 S is M*S0,
1455 domain_expand_(Left0, M, Left),
1456 domain_expand_(Right0, M, Right).
1457
1464
1465domain_expand_more(D0, M, D) :-
1466 1467 ( M < 0 -> domain_negate(D0, D1), M1 is abs(M)
1468 ; D1 = D0, M1 = M
1469 ),
1470 domain_expand_more_(D1, M1, D).
1471 1472
1473domain_expand_more_(empty, _, empty).
1474domain_expand_more_(from_to(From0, To0), M, from_to(From,To)) :-
1475 ( From0 cis_leq n(0) ->
1476 From cis (From0-n(1))*n(M) + n(1)
1477 ; From cis From0*n(M)
1478 ),
1479 ( To0 cis_lt n(0) ->
1480 To cis To0*n(M)
1481 ; To cis (To0+n(1))*n(M) - n(1)
1482 ).
1483domain_expand_more_(split(S0, Left0, Right0), M, split(S, Left, Right)) :-
1484 S is M*S0,
1485 domain_expand_more_(Left0, M, Left),
1486 domain_expand_more_(Right0, M, Right).
1487
1491
1492domain_contract(D0, M, D) :-
1493 1494 ( M < 0 -> domain_negate(D0, D1), M1 is abs(M)
1495 ; D1 = D0, M1 = M
1496 ),
1497 domain_contract_(D1, M1, D).
1498
1499domain_contract_(empty, _, empty).
1500domain_contract_(from_to(From0, To0), M, from_to(From,To)) :-
1501 ( From0 cis_geq n(0) ->
1502 From cis (From0 + n(M) - n(1)) // n(M)
1503 ; From cis From0 // n(M)
1504 ),
1505 ( To0 cis_geq n(0) ->
1506 To cis To0 // n(M)
1507 ; To cis (To0 - n(M) + n(1)) // n(M)
1508 ).
1509domain_contract_(split(_,Left0,Right0), M, D) :-
1510 1511 1512 domain_contract_(Left0, M, Left),
1513 domain_contract_(Right0, M, Right),
1514 domains_union(Left, Right, D).
1515
1520
1521domain_contract_less(D0, M, D) :-
1522 ( M < 0 -> domain_negate(D0, D1), M1 is abs(M)
1523 ; D1 = D0, M1 = M
1524 ),
1525 domain_contract_less_(D1, M1, D).
1526
1527domain_contract_less_(empty, _, empty).
1528domain_contract_less_(from_to(From0, To0), M, from_to(From,To)) :-
1529 From cis From0 // n(M), To cis To0 // n(M).
1530domain_contract_less_(split(_,Left0,Right0), M, D) :-
1531 1532 1533 domain_contract_less_(Left0, M, Left),
1534 domain_contract_less_(Right0, M, Right),
1535 domains_union(Left, Right, D).
1536
1540
1541domain_negate(empty, empty).
1542domain_negate(from_to(From0, To0), from_to(From, To)) :-
1543 From cis -To0, To cis -From0.
1544domain_negate(split(S0, Left0, Right0), split(S, Left, Right)) :-
1545 S is -S0,
1546 domain_negate(Left0, Right),
1547 domain_negate(Right0, Left).
1548
1552
1553list_to_disjoint_intervals([], []).
1554list_to_disjoint_intervals([N|Ns], Is) :-
1555 list_to_disjoint_intervals(Ns, N, N, Is).
1556
1557list_to_disjoint_intervals([], M, N, [n(M)-n(N)]).
1558list_to_disjoint_intervals([B|Bs], M, N, Is) :-
1559 ( B =:= N + 1 ->
1560 list_to_disjoint_intervals(Bs, M, B, Is)
1561 ; Is = [n(M)-n(N)|Rest],
1562 list_to_disjoint_intervals(Bs, B, B, Rest)
1563 ).
1564
1565list_to_domain(List0, D) :-
1566 ( List0 == [] -> D = empty
1567 ; sort(List0, List),
1568 list_to_disjoint_intervals(List, Is),
1569 intervals_to_domain(Is, D)
1570 ).
1571
1572intervals_to_domain([], empty) :- !.
1573intervals_to_domain([M-N], from_to(M,N)) :- !.
1574intervals_to_domain(Is, D) :-
1575 length(Is, L),
1576 FL is L // 2,
1577 length(Front, FL),
1578 append(Front, Tail, Is),
1579 Tail = [n(Start)-_|_],
1580 Hole is Start - 1,
1581 intervals_to_domain(Front, Left),
1582 intervals_to_domain(Tail, Right),
1583 D = split(Hole, Left, Right).
1584
1586
1587
1601
1602Var in Dom :- clpfd_in(Var, Dom).
1603
1604clpfd_in(V, D) :-
1605 fd_variable(V),
1606 drep_to_domain(D, Dom),
1607 domain(V, Dom).
1608
1609fd_variable(V) :-
1610 ( var(V) -> true
1611 ; integer(V) -> true
1612 ; type_error(integer, V)
1613 ).
1614
1619
1620Vs ins D :-
1621 fd_must_be_list(Vs),
1622 maplist(fd_variable, Vs),
1623 drep_to_domain(D, Dom),
1624 domains(Vs, Dom).
1625
1626fd_must_be_list(Ls) :-
1627 ( fd_var(Ls) -> type_error(list, Ls)
1628 ; must_be(list, Ls)
1629 ).
1630
1635
1636indomain(Var) :- label([Var]).
1637
1638order_dom_next(up, Dom, Next) :- domain_infimum(Dom, n(Next)).
1639order_dom_next(down, Dom, Next) :- domain_supremum(Dom, n(Next)).
1640order_dom_next(random_value(_), Dom, Next) :-
1641 phrase(domain_to_intervals(Dom), Is),
1642 length(Is, L),
1643 R is random(L),
1644 nth0(R, Is, From-To),
1645 random_between(From, To, Next).
1646
1647domain_to_intervals(from_to(n(From),n(To))) --> [From-To].
1648domain_to_intervals(split(_, Left, Right)) -->
1649 domain_to_intervals(Left),
1650 domain_to_intervals(Right).
1651
1655
1656label(Vs) :- labeling([], Vs).
1657
1742
1743labeling(Options, Vars) :-
1744 must_be(list, Options),
1745 fd_must_be_list(Vars),
1746 maplist(must_be_finite_fdvar, Vars),
1747 label(Options, Options, default(leftmost), default(up), default(step), [], upto_ground, Vars).
1748
1749finite_domain(Dom) :-
1750 domain_infimum(Dom, n(_)),
1751 domain_supremum(Dom, n(_)).
1752
1753must_be_finite_fdvar(Var) :-
1754 ( fd_get(Var, Dom, _) ->
1755 ( finite_domain(Dom) -> true
1756 ; instantiation_error(Var)
1757 )
1758 ; integer(Var) -> true
1759 ; must_be(integer, Var)
1760 ).
1761
1762
1763label([O|Os], Options, Selection, Order, Choice, Optim, Consistency, Vars) :-
1764 ( var(O)-> instantiation_error(O)
1765 ; override(selection, Selection, O, Options, S1) ->
1766 label(Os, Options, S1, Order, Choice, Optim, Consistency, Vars)
1767 ; override(order, Order, O, Options, O1) ->
1768 label(Os, Options, Selection, O1, Choice, Optim, Consistency, Vars)
1769 ; override(choice, Choice, O, Options, C1) ->
1770 label(Os, Options, Selection, Order, C1, Optim, Consistency, Vars)
1771 ; optimisation(O) ->
1772 label(Os, Options, Selection, Order, Choice, [O|Optim], Consistency, Vars)
1773 ; consistency(O, O1) ->
1774 label(Os, Options, Selection, Order, Choice, Optim, O1, Vars)
1775 ; domain_error(labeling_option, O)
1776 ).
1777label([], _, Selection, Order, Choice, Optim0, Consistency, Vars) :-
1778 maplist(arg(1), [Selection,Order,Choice], [S,O,C]),
1779 ( Optim0 == [] ->
1780 label(Vars, S, O, C, Consistency)
1781 ; reverse(Optim0, Optim),
1782 exprs_singlevars(Optim, SVs),
1783 optimise(Vars, [S,O,C], SVs)
1784 ).
1785
1788
1789exprs_singlevars([], []).
1790exprs_singlevars([E|Es], [SV|SVs]) :-
1791 E =.. [F,Expr],
1792 ?(Single) #= Expr,
1793 SV =.. [F,Single],
1794 exprs_singlevars(Es, SVs).
1795
1796all_dead(fd_props(Bs,Gs,Os)) :-
1797 all_dead_(Bs),
1798 all_dead_(Gs),
1799 all_dead_(Os).
1800
1801all_dead_([]).
1802all_dead_([propagator(_, S)|Ps]) :- S == dead, all_dead_(Ps).
1803
1804label([], _, _, _, Consistency) :- !,
1805 ( Consistency = upto_in(I0,I) -> I0 = I
1806 ; true
1807 ).
1808label(Vars, Selection, Order, Choice, Consistency) :-
1809 ( Vars = [V|Vs], nonvar(V) -> label(Vs, Selection, Order, Choice, Consistency)
1810 ; select_var(Selection, Vars, Var, RVars),
1811 ( var(Var) ->
1812 ( Consistency = upto_in(I0,I), fd_get(Var, _, Ps), all_dead(Ps) ->
1813 fd_size(Var, Size),
1814 I1 is I0*Size,
1815 label(RVars, Selection, Order, Choice, upto_in(I1,I))
1816 ; Consistency = upto_in, fd_get(Var, _, Ps), all_dead(Ps) ->
1817 label(RVars, Selection, Order, Choice, Consistency)
1818 ; choice_order_variable(Choice, Order, Var, RVars, Vars, Selection, Consistency)
1819 )
1820 ; label(RVars, Selection, Order, Choice, Consistency)
1821 )
1822 ).
1823
1824choice_order_variable(step, Order, Var, Vars, Vars0, Selection, Consistency) :-
1825 fd_get(Var, Dom, _),
1826 order_dom_next(Order, Dom, Next),
1827 ( Var = Next,
1828 label(Vars, Selection, Order, step, Consistency)
1829 ; neq_num(Var, Next),
1830 do_queue,
1831 label(Vars0, Selection, Order, step, Consistency)
1832 ).
1833choice_order_variable(enum, Order, Var, Vars, _, Selection, Consistency) :-
1834 fd_get(Var, Dom0, _),
1835 domain_direction_element(Dom0, Order, Var),
1836 label(Vars, Selection, Order, enum, Consistency).
1837choice_order_variable(bisect, Order, Var, _, Vars0, Selection, Consistency) :-
1838 fd_get(Var, Dom, _),
1839 domain_infimum(Dom, n(I)),
1840 domain_supremum(Dom, n(S)),
1841 Mid0 is (I + S) // 2,
1842 ( Mid0 =:= S -> Mid is Mid0 - 1 ; Mid = Mid0 ),
1843 ( Order == up -> ( Var #=< Mid ; Var #> Mid )
1844 ; Order == down -> ( Var #> Mid ; Var #=< Mid )
1845 ; domain_error(bisect_up_or_down, Order)
1846 ),
1847 label(Vars0, Selection, Order, bisect, Consistency).
1848
1849override(What, Prev, Value, Options, Result) :-
1850 call(What, Value),
1851 override_(Prev, Value, Options, Result).
1852
1853override_(default(_), Value, _, user(Value)).
1854override_(user(Prev), Value, Options, _) :-
1855 ( Value == Prev ->
1856 domain_error(nonrepeating_labeling_options, Options)
1857 ; domain_error(consistent_labeling_options, Options)
1858 ).
1859
1860selection(ff).
1861selection(ffc).
1862selection(min).
1863selection(max).
1864selection(leftmost).
1865selection(random_variable(Seed)) :-
1866 must_be(integer, Seed),
1867 set_random(seed(Seed)).
1868
1869choice(step).
1870choice(enum).
1871choice(bisect).
1872
1873order(up).
1874order(down).
1877order(random_value(Seed)) :-
1878 must_be(integer, Seed),
1879 set_random(seed(Seed)).
1880
1881consistency(upto_in(I), upto_in(1, I)).
1882consistency(upto_in, upto_in).
1883consistency(upto_ground, upto_ground).
1884
1885optimisation(min(_)).
1886optimisation(max(_)).
1887
1888select_var(leftmost, [Var|Vars], Var, Vars).
1889select_var(min, [V|Vs], Var, RVars) :-
1890 find_min(Vs, V, Var),
1891 delete_eq([V|Vs], Var, RVars).
1892select_var(max, [V|Vs], Var, RVars) :-
1893 find_max(Vs, V, Var),
1894 delete_eq([V|Vs], Var, RVars).
1895select_var(ff, [V|Vs], Var, RVars) :-
1896 fd_size_(V, n(S)),
1897 find_ff(Vs, V, S, Var),
1898 delete_eq([V|Vs], Var, RVars).
1899select_var(ffc, [V|Vs], Var, RVars) :-
1900 find_ffc(Vs, V, Var),
1901 delete_eq([V|Vs], Var, RVars).
1902select_var(random_variable(_), Vars0, Var, Vars) :-
1903 length(Vars0, L),
1904 I is random(L),
1905 nth0(I, Vars0, Var),
1906 delete_eq(Vars0, Var, Vars).
1907
1908find_min([], Var, Var).
1909find_min([V|Vs], CM, Min) :-
1910 ( min_lt(V, CM) ->
1911 find_min(Vs, V, Min)
1912 ; find_min(Vs, CM, Min)
1913 ).
1914
1915find_max([], Var, Var).
1916find_max([V|Vs], CM, Max) :-
1917 ( max_gt(V, CM) ->
1918 find_max(Vs, V, Max)
1919 ; find_max(Vs, CM, Max)
1920 ).
1921
1922find_ff([], Var, _, Var).
1923find_ff([V|Vs], CM, S0, FF) :-
1924 ( nonvar(V) -> find_ff(Vs, CM, S0, FF)
1925 ; ( fd_size_(V, n(S1)), S1 < S0 ->
1926 find_ff(Vs, V, S1, FF)
1927 ; find_ff(Vs, CM, S0, FF)
1928 )
1929 ).
1930
1931find_ffc([], Var, Var).
1932find_ffc([V|Vs], Prev, FFC) :-
1933 ( ffc_lt(V, Prev) ->
1934 find_ffc(Vs, V, FFC)
1935 ; find_ffc(Vs, Prev, FFC)
1936 ).
1937
1938
1939ffc_lt(X, Y) :-
1940 ( fd_get(X, XD, XPs) ->
1941 domain_num_elements(XD, n(NXD))
1942 ; NXD = 1, XPs = []
1943 ),
1944 ( fd_get(Y, YD, YPs) ->
1945 domain_num_elements(YD, n(NYD))
1946 ; NYD = 1, YPs = []
1947 ),
1948 ( NXD < NYD -> true
1949 ; NXD =:= NYD,
1950 props_number(XPs, NXPs),
1951 props_number(YPs, NYPs),
1952 NXPs > NYPs
1953 ).
1954
1955min_lt(X,Y) :- bounds(X,LX,_), bounds(Y,LY,_), LX < LY.
1956
1957max_gt(X,Y) :- bounds(X,_,UX), bounds(Y,_,UY), UX > UY.
1958
1959bounds(X, L, U) :-
1960 ( fd_get(X, Dom, _) ->
1961 domain_infimum(Dom, n(L)),
1962 domain_supremum(Dom, n(U))
1963 ; L = X, U = L
1964 ).
1965
1966delete_eq([], _, []).
1967delete_eq([X|Xs], Y, List) :-
1968 ( nonvar(X) -> delete_eq(Xs, Y, List)
1969 ; X == Y -> List = Xs
1970 ; List = [X|Tail],
1971 delete_eq(Xs, Y, Tail)
1972 ).
1973
1979
1980contracting(Vs) :-
1981 must_be(list, Vs),
1982 maplist(must_be_finite_fdvar, Vs),
1983 contracting(Vs, false, Vs).
1984
1985contracting([], Repeat, Vars) :-
1986 ( Repeat -> contracting(Vars, false, Vars)
1987 ; true
1988 ).
1989contracting([V|Vs], Repeat, Vars) :-
1990 fd_inf(V, Min),
1991 ( \+ \+ (V = Min) ->
1992 fd_sup(V, Max),
1993 ( \+ \+ (V = Max) ->
1994 contracting(Vs, Repeat, Vars)
1995 ; V #\= Max,
1996 contracting(Vs, true, Vars)
1997 )
1998 ; V #\= Min,
1999 contracting(Vs, true, Vars)
2000 ).
2001
2008
2009fds_sespsize(Vs, S) :-
2010 must_be(list, Vs),
2011 maplist(fd_variable, Vs),
2012 fds_sespsize(Vs, n(1), S1),
2013 bound_portray(S1, S).
2014
2015fd_size_(V, S) :-
2016 ( fd_get(V, D, _) ->
2017 domain_num_elements(D, S)
2018 ; S = n(1)
2019 ).
2020
2021fds_sespsize([], S, S).
2022fds_sespsize([V|Vs], S0, S) :-
2023 fd_size_(V, S1),
2024 S2 cis S0*S1,
2025 fds_sespsize(Vs, S2, S).
2026
2039
2040optimise(Vars, Options, Whats) :-
2041 Whats = [What|WhatsRest],
2042 Extremum = extremum(none),
2043 ( catch(store_extremum(Vars, Options, What, Extremum),
2044 time_limit_exceeded,
2045 false)
2046 ; Extremum = extremum(n(Val)),
2047 arg(1, What, Expr),
2048 append(WhatsRest, Options, Options1),
2049 ( Expr #= Val,
2050 labeling(Options1, Vars)
2051 ; Expr #\= Val,
2052 optimise(Vars, Options, Whats)
2053 )
2054 ).
2055
2056store_extremum(Vars, Options, What, Extremum) :-
2057 catch((labeling(Options, Vars), throw(w(What))), w(What1), true),
2058 functor(What, Direction, _),
2059 maplist(arg(1), [What,What1], [Expr,Expr1]),
2060 optimise(Direction, Options, Vars, Expr1, Expr, Extremum).
2061
2062optimise(Direction, Options, Vars, Expr0, Expr, Extremum) :-
2063 must_be(ground, Expr0),
2064 nb_setarg(1, Extremum, n(Expr0)),
2065 catch((tighten(Direction, Expr, Expr0),
2066 labeling(Options, Vars),
2067 throw(v(Expr))), v(Expr1), true),
2068 optimise(Direction, Options, Vars, Expr1, Expr, Extremum).
2069
2070tighten(min, E, V) :- E #< V.
2071tighten(max, E, V) :- E #> V.
2072
2074
2080
2081all_different(Ls) :-
2082 fd_must_be_list(Ls),
2083 maplist(fd_variable, Ls),
2084 Orig = original_goal(_, all_different(Ls)),
2085 all_different(Ls, [], Orig),
2086 do_queue.
2087
2088all_different([], _, _).
2089all_different([X|Right], Left, Orig) :-
2090 ( var(X) ->
2091 make_propagator(pdifferent(Left,Right,X,Orig), Prop),
2092 init_propagator(X, Prop),
2093 trigger_prop(Prop)
2094 ; exclude_fire(Left, Right, X)
2095 ),
2096 all_different(Right, [X|Left], Orig).
2097
2110
2111all_distinct(Ls) :-
2112 fd_must_be_list(Ls),
2113 maplist(fd_variable, Ls),
2114 make_propagator(pdistinct(Ls), Prop),
2115 distinct_attach(Ls, Prop, []),
2116 trigger_once(Prop).
2117
2130
2131sum(Vs, Op, Value) :-
2132 must_be(list, Vs),
2133 same_length(Vs, Ones),
2134 maplist(=(1), Ones),
2135 scalar_product(Ones, Vs, Op, Value).
2136
2142
2143scalar_product(Cs, Vs, Op, Value) :-
2144 must_be(list(integer), Cs),
2145 must_be(list, Vs),
2146 maplist(fd_variable, Vs),
2147 ( Op = (#=), single_value(Value, Right), ground(Vs) ->
2148 foldl(coeff_int_linsum, Cs, Vs, 0, Right)
2149 ; must_be(callable, Op),
2150 ( memberchk(Op, [#=,#\=,#<,#>,#=<,#>=]) -> true
2151 ; domain_error(scalar_product_relation, Op)
2152 ),
2153 must_be(acyclic, Value),
2154 foldl(coeff_var_plusterm, Cs, Vs, 0, Left),
2155 ( left_right_linsum_const(Left, Value, Cs1, Vs1, Const) ->
2156 scalar_product_(Op, Cs1, Vs1, Const)
2157 ; sum(Cs, Vs, 0, Op, Value)
2158 )
2159 ).
2160
2161single_value(V, V) :- var(V), !, non_monotonic(V).
2162single_value(V, V) :- integer(V).
2163single_value(?(V), V) :- fd_variable(V).
2164
2165coeff_var_plusterm(C, V, T0, T0+(C* ?(V))).
2166
2167coeff_int_linsum(C, I, S0, S) :- S is S0 + C*I.
2168
2169sum([], _, Sum, Op, Value) :- call(Op, Sum, Value).
2170sum([C|Cs], [X|Xs], Acc, Op, Value) :-
2171 ?(NAcc) #= Acc + C* ?(X),
2172 sum(Cs, Xs, NAcc, Op, Value).
2173
2174multiples([], [], _).
2175multiples([C|Cs], [V|Vs], Left) :-
2176 ( ( Cs = [N|_] ; Left = [N|_] ) ->
2177 ( N =\= 1, gcd(C,N) =:= 1 ->
2178 gcd(Cs, N, GCD0),
2179 gcd(Left, GCD0, GCD),
2180 ( GCD > 1 -> ?(V) #= GCD * ?(_)
2181 ; true
2182 )
2183 ; true
2184 )
2185 ; true
2186 ),
2187 multiples(Cs, Vs, [C|Left]).
2188
2189abs(N, A) :- A is abs(N).
2190
2191divide(D, N, R) :- R is N // D.
2192
2193scalar_product_(#=, Cs0, Vs, S0) :-
2194 ( Cs0 = [C|Rest] ->
2195 gcd(Rest, C, GCD),
2196 S0 mod GCD =:= 0,
2197 maplist(divide(GCD), [S0|Cs0], [S|Cs])
2198 ; S0 =:= 0, S = S0, Cs = Cs0
2199 ),
2200 ( S0 =:= 0 ->
2201 maplist(abs, Cs, As),
2202 multiples(As, Vs, [])
2203 ; true
2204 ),
2205 propagator_init_trigger(Vs, scalar_product_eq(Cs, Vs, S)).
2206scalar_product_(#\=, Cs, Vs, C) :-
2207 propagator_init_trigger(Vs, scalar_product_neq(Cs, Vs, C)).
2208scalar_product_(#=<, Cs, Vs, C) :-
2209 propagator_init_trigger(Vs, scalar_product_leq(Cs, Vs, C)).
2210scalar_product_(#<, Cs, Vs, C) :-
2211 C1 is C - 1,
2212 scalar_product_(#=<, Cs, Vs, C1).
2213scalar_product_(#>, Cs, Vs, C) :-
2214 C1 is C + 1,
2215 scalar_product_(#>=, Cs, Vs, C1).
2216scalar_product_(#>=, Cs, Vs, C) :-
2217 maplist(negative, Cs, Cs1),
2218 C1 is -C,
2219 scalar_product_(#=<, Cs1, Vs, C1).
2220
2221negative(X0, X) :- X is -X0.
2222
2223coeffs_variables_const([], [], [], [], I, I).
2224coeffs_variables_const([C|Cs], [V|Vs], Cs1, Vs1, I0, I) :-
2225 ( var(V) ->
2226 Cs1 = [C|CRest], Vs1 = [V|VRest], I1 = I0
2227 ; I1 is I0 + C*V,
2228 Cs1 = CRest, Vs1 = VRest
2229 ),
2230 coeffs_variables_const(Cs, Vs, CRest, VRest, I1, I).
2231
2232sum_finite_domains([], [], [], [], Inf, Sup, Inf, Sup).
2233sum_finite_domains([C|Cs], [V|Vs], Infs, Sups, Inf0, Sup0, Inf, Sup) :-
2234 fd_get(V, _, Inf1, Sup1, _),
2235 ( Inf1 = n(NInf) ->
2236 ( C < 0 ->
2237 Sup2 is Sup0 + C*NInf
2238 ; Inf2 is Inf0 + C*NInf
2239 ),
2240 Sups = Sups1,
2241 Infs = Infs1
2242 ; ( C < 0 ->
2243 Sup2 = Sup0,
2244 Sups = [C*V|Sups1],
2245 Infs = Infs1
2246 ; Inf2 = Inf0,
2247 Infs = [C*V|Infs1],
2248 Sups = Sups1
2249 )
2250 ),
2251 ( Sup1 = n(NSup) ->
2252 ( C < 0 ->
2253 Inf2 is Inf0 + C*NSup
2254 ; Sup2 is Sup0 + C*NSup
2255 ),
2256 Sups1 = Sups2,
2257 Infs1 = Infs2
2258 ; ( C < 0 ->
2259 Inf2 = Inf0,
2260 Infs1 = [C*V|Infs2],
2261 Sups1 = Sups2
2262 ; Sup2 = Sup0,
2263 Sups1 = [C*V|Sups2],
2264 Infs1 = Infs2
2265 )
2266 ),
2267 sum_finite_domains(Cs, Vs, Infs2, Sups2, Inf2, Sup2, Inf, Sup).
2268
2269remove_dist_upper_lower([], _, _, _).
2270remove_dist_upper_lower([C|Cs], [V|Vs], D1, D2) :-
2271 ( fd_get(V, VD, VPs) ->
2272 ( C < 0 ->
2273 domain_supremum(VD, n(Sup)),
2274 L is Sup + D1//C,
2275 domain_remove_smaller_than(VD, L, VD1),
2276 domain_infimum(VD1, n(Inf)),
2277 G is Inf - D2//C,
2278 domain_remove_greater_than(VD1, G, VD2)
2279 ; domain_infimum(VD, n(Inf)),
2280 G is Inf + D1//C,
2281 domain_remove_greater_than(VD, G, VD1),
2282 domain_supremum(VD1, n(Sup)),
2283 L is Sup - D2//C,
2284 domain_remove_smaller_than(VD1, L, VD2)
2285 ),
2286 fd_put(V, VD2, VPs)
2287 ; true
2288 ),
2289 remove_dist_upper_lower(Cs, Vs, D1, D2).
2290
2291
2292remove_dist_upper_leq([], _, _).
2293remove_dist_upper_leq([C|Cs], [V|Vs], D1) :-
2294 ( fd_get(V, VD, VPs) ->
2295 ( C < 0 ->
2296 domain_supremum(VD, n(Sup)),
2297 L is Sup + D1//C,
2298 domain_remove_smaller_than(VD, L, VD1)
2299 ; domain_infimum(VD, n(Inf)),
2300 G is Inf + D1//C,
2301 domain_remove_greater_than(VD, G, VD1)
2302 ),
2303 fd_put(V, VD1, VPs)
2304 ; true
2305 ),
2306 remove_dist_upper_leq(Cs, Vs, D1).
2307
2308
2309remove_dist_upper([], _).
2310remove_dist_upper([C*V|CVs], D) :-
2311 ( fd_get(V, VD, VPs) ->
2312 ( C < 0 ->
2313 ( domain_supremum(VD, n(Sup)) ->
2314 L is Sup + D//C,
2315 domain_remove_smaller_than(VD, L, VD1)
2316 ; VD1 = VD
2317 )
2318 ; ( domain_infimum(VD, n(Inf)) ->
2319 G is Inf + D//C,
2320 domain_remove_greater_than(VD, G, VD1)
2321 ; VD1 = VD
2322 )
2323 ),
2324 fd_put(V, VD1, VPs)
2325 ; true
2326 ),
2327 remove_dist_upper(CVs, D).
2328
2329remove_dist_lower([], _).
2330remove_dist_lower([C*V|CVs], D) :-
2331 ( fd_get(V, VD, VPs) ->
2332 ( C < 0 ->
2333 ( domain_infimum(VD, n(Inf)) ->
2334 G is Inf - D//C,
2335 domain_remove_greater_than(VD, G, VD1)
2336 ; VD1 = VD
2337 )
2338 ; ( domain_supremum(VD, n(Sup)) ->
2339 L is Sup - D//C,
2340 domain_remove_smaller_than(VD, L, VD1)
2341 ; VD1 = VD
2342 )
2343 ),
2344 fd_put(V, VD1, VPs)
2345 ; true
2346 ),
2347 remove_dist_lower(CVs, D).
2348
2349remove_upper([], _).
2350remove_upper([C*X|CXs], Max) :-
2351 ( fd_get(X, XD, XPs) ->
2352 D is Max//C,
2353 ( C < 0 ->
2354 domain_remove_smaller_than(XD, D, XD1)
2355 ; domain_remove_greater_than(XD, D, XD1)
2356 ),
2357 fd_put(X, XD1, XPs)
2358 ; true
2359 ),
2360 remove_upper(CXs, Max).
2361
2362remove_lower([], _).
2363remove_lower([C*X|CXs], Min) :-
2364 ( fd_get(X, XD, XPs) ->
2365 D is -Min//C,
2366 ( C < 0 ->
2367 domain_remove_greater_than(XD, D, XD1)
2368 ; domain_remove_smaller_than(XD, D, XD1)
2369 ),
2370 fd_put(X, XD1, XPs)
2371 ; true
2372 ),
2373 remove_lower(CXs, Min).
2374
2376
2385
2387
2388make_queue :- nb_setval('$clpfd_queue', fast_slow([], [])).
2389
2390push_queue(E, Which) :-
2391 nb_getval('$clpfd_queue', Qs),
2392 arg(Which, Qs, Q),
2393 ( Q == [] ->
2394 setarg(Which, Qs, [E|T]-T)
2395 ; Q = H-[E|T],
2396 setarg(Which, Qs, H-T)
2397 ).
2398
2399pop_queue(E) :-
2400 nb_getval('$clpfd_queue', Qs),
2401 ( pop_queue(E, Qs, 1) -> true
2402 ; pop_queue(E, Qs, 2)
2403 ).
2404
2405pop_queue(E, Qs, Which) :-
2406 arg(Which, Qs, [E|NH]-T),
2407 ( var(NH) ->
2408 setarg(Which, Qs, [])
2409 ; setarg(Which, Qs, NH-T)
2410 ).
2411
2412fetch_propagator(Prop) :-
2413 pop_queue(P),
2414 ( propagator_state(P, S), S == dead -> fetch_propagator(Prop)
2415 ; Prop = P
2416 ).
2417
2424
2425constrain_to_integer(Var) :-
2426 ( integer(Var) -> true
2427 ; fd_get(Var, D, Ps),
2428 fd_put(Var, D, Ps)
2429 ).
2430
2431power_var_num(P, X, N) :-
2432 ( var(P) -> X = P, N = 1
2433 ; P = Left*Right,
2434 power_var_num(Left, XL, L),
2435 power_var_num(Right, XR, R),
2436 XL == XR,
2437 X = XL,
2438 N is L + R
2439 ).
2440
2450
2451:- op(800, xfx, =>). 2452
2453parse_clpfd(E, R,
2454 [g(cyclic_term(E)) => [g(domain_error(clpfd_expression, E))],
2455 g(var(E)) => [g(non_monotonic(E)),
2456 g(constrain_to_integer(E)), g(E = R)],
2457 g(integer(E)) => [g(R = E)],
2458 ?(E) => [g(must_be_fd_integer(E)), g(R = E)],
2459 #(E) => [g(must_be_fd_integer(E)), g(R = E)],
2460 m(A+B) => [p(pplus(A, B, R))],
2461 2462 g(power_var_num(E, V, N)) => [p(pexp(V, N, R))],
2463 m(A*B) => [p(ptimes(A, B, R))],
2464 m(A-B) => [p(pplus(R,B,A))],
2465 m(-A) => [p(ptimes(-1,A,R))],
2466 m(max(A,B)) => [g(A #=< ?(R)), g(B #=< R), p(pmax(A, B, R))],
2467 m(min(A,B)) => [g(A #>= ?(R)), g(B #>= R), p(pmin(A, B, R))],
2468 m(A mod B) => [g(B #\= 0), p(pmod(A, B, R))],
2469 m(A rem B) => [g(B #\= 0), p(prem(A, B, R))],
2470 m(abs(A)) => [g(?(R) #>= 0), p(pabs(A, R))],
2472 m(A//B) => [g(B #\= 0), p(ptzdiv(A, B, R))],
2473 m(A div B) => [g(?(R) #= (A - (A mod B)) // B)],
2474 m(A rdiv B) => [g(B #\= 0), p(prdiv(A, B, R))],
2475 m(A^B) => [p(pexp(A, B, R))],
2476 2477 m(\A) => [p(pfunction(\, A, R))],
2478 m(msb(A)) => [p(pfunction(msb, A, R))],
2479 m(lsb(A)) => [p(pfunction(lsb, A, R))],
2480 m(popcount(A)) => [p(pfunction(popcount, A, R))],
2481 m(A<<B) => [p(pfunction(<<, A, B, R))],
2482 m(A>>B) => [p(pfunction(>>, A, B, R))],
2483 m(A/\B) => [p(pfunction(/\, A, B, R))],
2484 m(A\/B) => [p(pfunction(\/, A, B, R))],
2485 m(A xor B) => [p(pfunction(xor, A, B, R))],
2486 g(true) => [g(domain_error(clpfd_expression, E))]
2487 ]).
2488
2489non_monotonic(X) :-
2490 ( \+ fd_var(X), current_prolog_flag(clpfd_monotonic, true) ->
2491 instantiation_error(X)
2492 ; true
2493 ).
2494
2497
2498make_parse_clpfd(Clauses) :-
2499 parse_clpfd_clauses(Clauses0),
2500 maplist(goals_goal, Clauses0, Clauses).
2501
2502goals_goal((Head :- Goals), (Head :- Body)) :-
2503 list_goal(Goals, Body).
2504
2505parse_clpfd_clauses(Clauses) :-
2506 parse_clpfd(E, R, Matchers),
2507 maplist(parse_matcher(E, R), Matchers, Clauses).
2508
2509parse_matcher(E, R, Matcher, Clause) :-
2510 Matcher = (Condition0 => Goals0),
2511 phrase((parse_condition(Condition0, E, Head),
2512 parse_goals(Goals0)), Goals),
2513 Clause = (parse_clpfd(Head, R) :- Goals).
2514
2515parse_condition(g(Goal), E, E) --> [Goal, !].
2516parse_condition(?(E), _, ?(E)) --> [!].
2517parse_condition(#(E), _, #(E)) --> [!].
2518parse_condition(m(Match), _, Match0) -->
2519 [!],
2520 { copy_term(Match, Match0),
2521 term_variables(Match0, Vs0),
2522 term_variables(Match, Vs)
2523 },
2524 parse_match_variables(Vs0, Vs).
2525
2526parse_match_variables([], []) --> [].
2527parse_match_variables([V0|Vs0], [V|Vs]) -->
2528 [parse_clpfd(V0, V)],
2529 parse_match_variables(Vs0, Vs).
2530
2531parse_goals([]) --> [].
2532parse_goals([G|Gs]) --> parse_goal(G), parse_goals(Gs).
2533
2534parse_goal(g(Goal)) --> [Goal].
2535parse_goal(p(Prop)) -->
2536 [make_propagator(Prop, P)],
2537 { term_variables(Prop, Vs) },
2538 parse_init(Vs, P),
2539 [trigger_once(P)].
2540
2541parse_init([], _) --> [].
2542parse_init([V|Vs], P) --> [init_propagator(V, P)], parse_init(Vs, P).
2543
2546
2547
2550
2551trigger_once(Prop) :- trigger_prop(Prop), do_queue.
2552
2553neq(A, B) :- propagator_init_trigger(pneq(A, B)).
2554
2555propagator_init_trigger(P) -->
2556 { term_variables(P, Vs) },
2557 propagator_init_trigger(Vs, P).
2558
2559propagator_init_trigger(Vs, P) -->
2560 [p(Prop)],
2561 { make_propagator(P, Prop),
2562 maplist(prop_init(Prop), Vs),
2563 trigger_once(Prop) }.
2564
2565propagator_init_trigger(P) :-
2566 phrase(propagator_init_trigger(P), _).
2567
2568propagator_init_trigger(Vs, P) :-
2569 phrase(propagator_init_trigger(Vs, P), _).
2570
2571prop_init(Prop, V) :- init_propagator(V, Prop).
2572
2573geq(A, B) :-
2574 ( fd_get(A, AD, APs) ->
2575 domain_infimum(AD, AI),
2576 ( fd_get(B, BD, _) ->
2577 domain_supremum(BD, BS),
2578 ( AI cis_geq BS -> true
2579 ; propagator_init_trigger(pgeq(A,B))
2580 )
2581 ; ( AI cis_geq n(B) -> true
2582 ; domain_remove_smaller_than(AD, B, AD1),
2583 fd_put(A, AD1, APs),
2584 do_queue
2585 )
2586 )
2587 ; fd_get(B, BD, BPs) ->
2588 domain_remove_greater_than(BD, A, BD1),
2589 fd_put(B, BD1, BPs),
2590 do_queue
2591 ; A >= B
2592 ).
2593
2618
2619match_expand(#>=, clpfd_geq_).
2620match_expand(#=, clpfd_equal_).
2621match_expand(#\=, clpfd_neq).
2622
2623symmetric(#=).
2624symmetric(#\=).
2625
2626matches([
2627 m_c(any(X) #>= any(Y), left_right_linsum_const(X, Y, Cs, Vs, Const)) =>
2628 [g(( Cs = [1], Vs = [A] -> geq(A, Const)
2629 ; Cs = [-1], Vs = [A] -> Const1 is -Const, geq(Const1, A)
2630 ; Cs = [1,1], Vs = [A,B] -> ?(A) + ?(B) #= ?(S), geq(S, Const)
2631 ; Cs = [1,-1], Vs = [A,B] ->
2632 ( Const =:= 0 -> geq(A, B)
2633 ; C1 is -Const,
2634 propagator_init_trigger(x_leq_y_plus_c(B, A, C1))
2635 )
2636 ; Cs = [-1,1], Vs = [A,B] ->
2637 ( Const =:= 0 -> geq(B, A)
2638 ; C1 is -Const,
2639 propagator_init_trigger(x_leq_y_plus_c(A, B, C1))
2640 )
2641 ; Cs = [-1,-1], Vs = [A,B] ->
2642 ?(A) + ?(B) #= ?(S), Const1 is -Const, geq(Const1, S)
2643 ; scalar_product_(#>=, Cs, Vs, Const)
2644 ))],
2645 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))],
2646 m(integer(X) #>= any(Z) + integer(A)) => [g(C is X - A), r(C, Z)],
2647 m(abs(any(X)-any(Y)) #>= integer(I)) => [d(X, X1), d(Y, Y1), p(absdiff_geq(X1, Y1, I))],
2648 m(abs(any(X)) #>= integer(I)) => [d(X, RX), g((I>0 -> I1 is -I, RX in inf..I1 \/ I..sup; true))],
2649 m(integer(I) #>= abs(any(X))) => [d(X, RX), g(I>=0), g(I1 is -I), g(RX in I1..I)],
2650 m(any(X) #>= any(Y)) => [d(X, RX), d(Y, RY), g(geq(RX, RY))],
2651
2652 2653 2654
2655 m(var(X) #= var(Y)) => [g(constrain_to_integer(X)), g(X=Y)],
2656 m(var(X) #= var(Y)+var(Z)) => [p(pplus(Y,Z,X))],
2657 m(var(X) #= var(Y)-var(Z)) => [p(pplus(X,Z,Y))],
2658 m(var(X) #= var(Y)*var(Z)) => [p(ptimes(Y,Z,X))],
2659 m(var(X) #= -var(Z)) => [p(ptimes(-1, Z, X))],
2660 m_c(any(X) #= any(Y), left_right_linsum_const(X, Y, Cs, Vs, S)) =>
2661 [g(scalar_product_(#=, Cs, Vs, S))],
2662 m(var(X) #= any(Y)) => [d(Y,X)],
2663 m(any(X) #= any(Y)) => [d(X, RX), d(Y, RX)],
2664
2665 2666 2667
2668 m(var(X) #\= integer(Y)) => [g(neq_num(X, Y))],
2669 m(var(X) #\= var(Y)) => [g(neq(X,Y))],
2670 m(var(X) #\= var(Y) + var(Z)) => [p(x_neq_y_plus_z(X, Y, Z))],
2671 m(var(X) #\= var(Y) - var(Z)) => [p(x_neq_y_plus_z(Y, X, Z))],
2672 m(var(X) #\= var(Y)*var(Z)) => [p(ptimes(Y,Z,P)), g(neq(X,P))],
2673 m(integer(X) #\= abs(any(Y)-any(Z))) => [d(Y, Y1), d(Z, Z1), p(absdiff_neq(Y1, Z1, X))],
2674 m_c(any(X) #\= any(Y), left_right_linsum_const(X, Y, Cs, Vs, S)) =>
2675 [g(scalar_product_(#\=, Cs, Vs, S))],
2676 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))],
2677 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))],
2678 m(any(X) #\= any(Y)) => [d(X, RX), d(Y, RY), g(neq(RX, RY))]
2679 ]).
2680
2686
2687make_matches(Clauses) :-
2688 matches(Ms),
2689 findall(F, (member(M=>_, Ms), arg(1, M, M1), functor(M1, F, _)), Fs0),
2690 sort(Fs0, Fs),
2691 maplist(prevent_cyclic_argument, Fs, PrevCyclicClauses),
2692 phrase(matchers(Ms), Clauses0),
2693 maplist(goals_goal, Clauses0, MatcherClauses),
2694 append(PrevCyclicClauses, MatcherClauses, Clauses1),
2695 sort_by_predicate(Clauses1, Clauses).
2696
2697sort_by_predicate(Clauses, ByPred) :-
2698 map_list_to_pairs(predname, Clauses, Keyed),
2699 keysort(Keyed, KeyedByPred),
2700 pairs_values(KeyedByPred, ByPred).
2701
2702predname((H:-_), Key) :- !, predname(H, Key).
2703predname(M:H, M:Key) :- !, predname(H, Key).
2704predname(H, Name/Arity) :- !, functor(H, Name, Arity).
2705
2706prevent_cyclic_argument(F0, Clause) :-
2707 match_expand(F0, F),
2708 Head =.. [F,X,Y],
2709 Clause = (Head :- ( cyclic_term(X) ->
2710 domain_error(clpfd_expression, X)
2711 ; cyclic_term(Y) ->
2712 domain_error(clpfd_expression, Y)
2713 ; false
2714 )).
2715
2716matchers([]) --> [].
2717matchers([Condition => Goals|Ms]) -->
2718 matcher(Condition, Goals),
2719 matchers(Ms).
2720
2721matcher(m(M), Gs) --> matcher(m_c(M,true), Gs).
2722matcher(m_c(Matcher,Cond), Gs) -->
2723 [(Head :- Goals0)],
2724 { Matcher =.. [F,A,B],
2725 match_expand(F, Expand),
2726 Head =.. [Expand,X,Y],
2727 phrase((match(A, X), match(B, Y)), Goals0, [Cond,!|Goals1]),
2728 phrase(match_goals(Gs, Expand), Goals1) },
2729 ( { symmetric(F), \+ (subsumes_term(A, B), subsumes_term(B, A)) } ->
2730 { Head1 =.. [Expand,Y,X] },
2731 [(Head1 :- Goals0)]
2732 ; []
2733 ).
2734
2735match(any(A), T) --> [A = T].
2736match(var(V), T) --> [( nonvar(T), ( T = ?(Var) ; T = #(Var) ) ->
2737 must_be_fd_integer(Var), V = Var
2738 ; v_or_i(T), V = T
2739 )].
2740match(integer(I), T) --> [integer(T), I = T].
2741match(-X, T) --> [nonvar(T), T = -A], match(X, A).
2742match(abs(X), T) --> [nonvar(T), T = abs(A)], match(X, A).
2743match(Binary, T) -->
2744 { Binary =.. [Op,X,Y], Term =.. [Op,A,B] },
2745 [nonvar(T), T = Term],
2746 match(X, A), match(Y, B).
2747
2748match_goals([], _) --> [].
2749match_goals([G|Gs], F) --> match_goal(G, F), match_goals(Gs, F).
2750
2751match_goal(r(X,Y), F) --> { G =.. [F,X,Y] }, [G].
2752match_goal(d(X,Y), _) --> [parse_clpfd(X, Y)].
2753match_goal(g(Goal), _) --> [Goal].
2754match_goal(p(Prop), _) -->
2755 [make_propagator(Prop, P)],
2756 { term_variables(Prop, Vs) },
2757 parse_init(Vs, P),
2758 [trigger_once(P)].
2759
2760
2762
2763
2764
2770
2771X #>= Y :- clpfd_geq(X, Y).
2772
2773clpfd_geq(X, Y) :- clpfd_geq_(X, Y), reinforce(X), reinforce(Y).
2774
2781
2782X #=< Y :- Y #>= X.
2783
2790
2791X #= Y :- clpfd_equal(X, Y).
2792
2793clpfd_equal(X, Y) :- clpfd_equal_(X, Y), reinforce(X).
2794
2799
2800expr_conds(E, E) --> [integer(E)],
2801 { var(E), !, \+ current_prolog_flag(clpfd_monotonic, true) }.
2802expr_conds(E, E) --> { integer(E) }.
2803expr_conds(?(E), E) --> [integer(E)].
2804expr_conds(#(E), E) --> [integer(E)].
2805expr_conds(-E0, -E) --> expr_conds(E0, E).
2806expr_conds(abs(E0), abs(E)) --> expr_conds(E0, E).
2807expr_conds(A0+B0, A+B) --> expr_conds(A0, A), expr_conds(B0, B).
2808expr_conds(A0*B0, A*B) --> expr_conds(A0, A), expr_conds(B0, B).
2809expr_conds(A0-B0, A-B) --> expr_conds(A0, A), expr_conds(B0, B).
2810expr_conds(A0//B0, A//B) -->
2811 expr_conds(A0, A), expr_conds(B0, B),
2812 [B =\= 0].
2814expr_conds(min(A0,B0), min(A,B)) --> expr_conds(A0, A), expr_conds(B0, B).
2815expr_conds(max(A0,B0), max(A,B)) --> expr_conds(A0, A), expr_conds(B0, B).
2816expr_conds(A0 mod B0, A mod B) -->
2817 expr_conds(A0, A), expr_conds(B0, B),
2818 [B =\= 0].
2819expr_conds(A0^B0, A^B) -->
2820 expr_conds(A0, A), expr_conds(B0, B),
2821 [(B >= 0 ; A =:= -1)].
2823expr_conds(\ A0, \ A) --> expr_conds(A0, A).
2824expr_conds(A0<<B0, A<<B) --> expr_conds(A0, A), expr_conds(B0, B).
2825expr_conds(A0>>B0, A>>B) --> expr_conds(A0, A), expr_conds(B0, B).
2826expr_conds(A0/\B0, A/\B) --> expr_conds(A0, A), expr_conds(B0, B).
2827expr_conds(A0\/B0, A\/B) --> expr_conds(A0, A), expr_conds(B0, B).
2828expr_conds(A0 xor B0, A xor B) --> expr_conds(A0, A), expr_conds(B0, B).
2829expr_conds(lsb(A0), lsb(A)) --> expr_conds(A0, A).
2830expr_conds(msb(A0), msb(A)) --> expr_conds(A0, A).
2831expr_conds(popcount(A0), popcount(A)) --> expr_conds(A0, A).
2832
2833:- multifile
2834 system:goal_expansion/2. 2835:- dynamic
2836 system:goal_expansion/2. 2837
2838system:goal_expansion(Goal, Expansion) :-
2839 \+ current_prolog_flag(clpfd_goal_expansion, false),
2840 clpfd_expandable(Goal),
2841 prolog_load_context(module, M),
2842 ( M == clpfd
2843 -> true
2844 ; predicate_property(M:Goal, imported_from(clpfd))
2845 ),
2846 clpfd_expansion(Goal, Expansion).
2847
2848clpfd_expandable(_ in _).
2849clpfd_expandable(_ #= _).
2850clpfd_expandable(_ #>= _).
2851clpfd_expandable(_ #=< _).
2852clpfd_expandable(_ #> _).
2853clpfd_expandable(_ #< _).
2854
2855clpfd_expansion(Var in Dom, In) :-
2856 ( ground(Dom), Dom = L..U, integer(L), integer(U) ->
2857 expansion_simpler(
2858 ( integer(Var) ->
2859 between(L, U, Var)
2860 ; clpfd:clpfd_in(Var, Dom)
2861 ), In)
2862 ; In = clpfd:clpfd_in(Var, Dom)
2863 ).
2864clpfd_expansion(X0 #= Y0, Equal) :-
2865 phrase(expr_conds(X0, X), CsX),
2866 phrase(expr_conds(Y0, Y), CsY),
2867 list_goal(CsX, CondX),
2868 list_goal(CsY, CondY),
2869 expansion_simpler(
2870 ( CondX ->
2871 ( var(Y) -> Y is X
2872 ; CondY -> X =:= Y
2873 ; T is X, clpfd:clpfd_equal(T, Y0)
2874 )
2875 ; CondY ->
2876 ( var(X) -> X is Y
2877 ; T is Y, clpfd:clpfd_equal(X0, T)
2878 )
2879 ; clpfd:clpfd_equal(X0, Y0)
2880 ), Equal).
2881clpfd_expansion(X0 #>= Y0, Geq) :-
2882 phrase(expr_conds(X0, X), CsX),
2883 phrase(expr_conds(Y0, Y), CsY),
2884 list_goal(CsX, CondX),
2885 list_goal(CsY, CondY),
2886 expansion_simpler(
2887 ( CondX ->
2888 ( CondY -> X >= Y
2889 ; T is X, clpfd:clpfd_geq(T, Y0)
2890 )
2891 ; CondY -> T is Y, clpfd:clpfd_geq(X0, T)
2892 ; clpfd:clpfd_geq(X0, Y0)
2893 ), Geq).
2894clpfd_expansion(X #=< Y, Leq) :- clpfd_expansion(Y #>= X, Leq).
2895clpfd_expansion(X #> Y, Gt) :- clpfd_expansion(X #>= Y+1, Gt).
2896clpfd_expansion(X #< Y, Lt) :- clpfd_expansion(Y #> X, Lt).
2897
2898expansion_simpler((True->Then0;_), Then) :-
2899 is_true(True), !,
2900 expansion_simpler(Then0, Then).
2901expansion_simpler((False->_;Else0), Else) :-
2902 is_false(False), !,
2903 expansion_simpler(Else0, Else).
2904expansion_simpler((If->Then0;Else0), (If->Then;Else)) :- !,
2905 expansion_simpler(Then0, Then),
2906 expansion_simpler(Else0, Else).
2907expansion_simpler((A0,B0), (A,B)) :-
2908 expansion_simpler(A0, A),
2909 expansion_simpler(B0, B).
2910expansion_simpler(Var is Expr0, Goal) :-
2911 ground(Expr0), !,
2912 phrase(expr_conds(Expr0, Expr), Gs),
2913 ( maplist(call, Gs) -> Value is Expr, Goal = (Var = Value)
2914 ; Goal = false
2915 ).
2916expansion_simpler(Var =:= Expr0, Goal) :-
2917 ground(Expr0), !,
2918 phrase(expr_conds(Expr0, Expr), Gs),
2919 ( maplist(call, Gs) -> Value is Expr, Goal = (Var =:= Value)
2920 ; Goal = false
2921 ).
2922expansion_simpler(Var is Expr, Var = Expr) :- var(Expr), !.
2923expansion_simpler(Var is Expr, Goal) :- !,
2924 ( var(Var), nonvar(Expr),
2925 Expr = E mod M, nonvar(E), E = A^B ->
2926 Goal = ( ( integer(A), integer(B), integer(M),
2927 A >= 0, B >= 0, M > 0 ->
2928 Var is powm(A, B, M)
2929 ; Var is Expr
2930 ) )
2931 ; Goal = ( Var is Expr )
2932 ).
2933expansion_simpler(between(L,U,V), Goal) :- maplist(integer, [L,U,V]), !,
2934 ( between(L,U,V) -> Goal = true
2935 ; Goal = false
2936 ).
2937expansion_simpler(Goal, Goal).
2938
2939is_true(true).
2940is_true(integer(I)) :- integer(I).
2941:- if(current_predicate(var_property/2)). 2942is_true(var(X)) :- var(X), var_property(X, fresh(true)).
2943is_false(integer(X)) :- var(X), var_property(X, fresh(true)).
2944is_false((A,B)) :- is_false(A) ; is_false(B).
2945:- endif. 2946is_false(var(X)) :- nonvar(X).
2947
2948
2950
2951linsum(X, S, S) --> { var(X), !, non_monotonic(X) }, [vn(X,1)].
2952linsum(I, S0, S) --> { integer(I), S is S0 + I }.
2953linsum(?(X), S, S) --> { must_be_fd_integer(X) }, [vn(X,1)].
2954linsum(#(X), S, S) --> { must_be_fd_integer(X) }, [vn(X,1)].
2955linsum(-A, S0, S) --> mulsum(A, -1, S0, S).
2956linsum(N*A, S0, S) --> { integer(N) }, !, mulsum(A, N, S0, S).
2957linsum(A*N, S0, S) --> { integer(N) }, !, mulsum(A, N, S0, S).
2958linsum(A+B, S0, S) --> linsum(A, S0, S1), linsum(B, S1, S).
2959linsum(A-B, S0, S) --> linsum(A, S0, S1), mulsum(B, -1, S1, S).
2960
2961mulsum(A, M, S0, S) -->
2962 { phrase(linsum(A, 0, CA), As), S is S0 + M*CA },
2963 lin_mul(As, M).
2964
2965lin_mul([], _) --> [].
2966lin_mul([vn(X,N0)|VNs], M) --> { N is N0*M }, [vn(X,N)], lin_mul(VNs, M).
2967
2968v_or_i(V) :- var(V), !, non_monotonic(V).
2969v_or_i(I) :- integer(I).
2970
2971must_be_fd_integer(X) :-
2972 ( var(X) -> constrain_to_integer(X)
2973 ; must_be(integer, X)
2974 ).
2975
2976left_right_linsum_const(Left, Right, Cs, Vs, Const) :-
2977 phrase(linsum(Left, 0, CL), Lefts0, Rights),
2978 phrase(linsum(Right, 0, CR), Rights0),
2979 maplist(linterm_negate, Rights0, Rights),
2980 msort(Lefts0, Lefts),
2981 Lefts = [vn(First,N)|LeftsRest],
2982 vns_coeffs_variables(LeftsRest, N, First, Cs0, Vs0),
2983 filter_linsum(Cs0, Vs0, Cs, Vs),
2984 Const is CR - CL.
2985 2986
2987linterm_negate(vn(V,N0), vn(V,N)) :- N is -N0.
2988
2989vns_coeffs_variables([], N, V, [N], [V]).
2990vns_coeffs_variables([vn(V,N)|VNs], N0, V0, Ns, Vs) :-
2991 ( V == V0 ->
2992 N1 is N0 + N,
2993 vns_coeffs_variables(VNs, N1, V0, Ns, Vs)
2994 ; Ns = [N0|NRest],
2995 Vs = [V0|VRest],
2996 vns_coeffs_variables(VNs, N, V, NRest, VRest)
2997 ).
2998
2999filter_linsum([], [], [], []).
3000filter_linsum([C0|Cs0], [V0|Vs0], Cs, Vs) :-
3001 ( C0 =:= 0 ->
3002 constrain_to_integer(V0),
3003 filter_linsum(Cs0, Vs0, Cs, Vs)
3004 ; Cs = [C0|Cs1], Vs = [V0|Vs1],
3005 filter_linsum(Cs0, Vs0, Cs1, Vs1)
3006 ).
3007
3008gcd([], G, G).
3009gcd([N|Ns], G0, G) :-
3010 G1 is gcd(N, G0),
3011 gcd(Ns, G1, G).
3012
3013even(N) :- N mod 2 =:= 0.
3014
3015odd(N) :- \+ even(N).
3016
3022
3023integer_kth_root(N, K, R) :-
3024 ( even(K) ->
3025 N >= 0
3026 ; true
3027 ),
3028 ( N < 0 ->
3029 odd(K),
3030 integer_kroot(N, 0, N, K, R)
3031 ; integer_kroot(0, N, N, K, R)
3032 ).
3033
3034integer_kroot(L, U, N, K, R) :-
3035 ( L =:= U -> N =:= L^K, R = L
3036 ; L + 1 =:= U ->
3037 ( L^K =:= N -> R = L
3038 ; U^K =:= N -> R = U
3039 ; false
3040 )
3041 ; Mid is (L + U)//2,
3042 ( Mid^K > N ->
3043 integer_kroot(L, Mid, N, K, R)
3044 ; integer_kroot(Mid, U, N, K, R)
3045 )
3046 ).
3047
3048integer_log_b(N, B, Log0, Log) :-
3049 T is B^Log0,
3050 ( T =:= N -> Log = Log0
3051 ; T < N,
3052 Log1 is Log0 + 1,
3053 integer_log_b(N, B, Log1, Log)
3054 ).
3055
3056floor_integer_log_b(N, B, Log0, Log) :-
3057 T is B^Log0,
3058 ( T > N -> Log is Log0 - 1
3059 ; T =:= N -> Log = Log0
3060 ; T < N,
3061 Log1 is Log0 + 1,
3062 floor_integer_log_b(N, B, Log1, Log)
3063 ).
3064
3065
3069
3070:- if(current_predicate(nth_integer_root_and_remainder/4)). 3071
3073integer_kth_root_leq(N, K, R) :-
3074 nth_integer_root_and_remainder(K, N, R, _).
3075
3076:- else. 3077
3078integer_kth_root_leq(N, K, R) :-
3079 ( even(K) ->
3080 N >= 0
3081 ; true
3082 ),
3083 ( N < 0 ->
3084 odd(K),
3085 integer_kroot_leq(N, 0, N, K, R)
3086 ; integer_kroot_leq(0, N, N, K, R)
3087 ).
3088
3089integer_kroot_leq(L, U, N, K, R) :-
3090 ( L =:= U -> R = L
3091 ; L + 1 =:= U ->
3092 ( U^K =< N -> R = U
3093 ; R = L
3094 )
3095 ; Mid is (L + U)//2,
3096 ( Mid^K > N ->
3097 integer_kroot_leq(L, Mid, N, K, R)
3098 ; integer_kroot_leq(Mid, U, N, K, R)
3099 )
3100 ).
3101
3102:- endif. 3103
3110
3111X #\= Y :- clpfd_neq(X, Y), do_queue.
3112
3114
3115x_neq_y_plus_z(X, Y, Z) :-
3116 propagator_init_trigger(x_neq_y_plus_z(X,Y,Z)).
3117
3120
3121neq_num(X, N) :-
3122 ( fd_get(X, XD, XPs) ->
3123 domain_remove(XD, N, XD1),
3124 fd_put(X, XD1, XPs)
3125 ; X =\= N
3126 ).
3127
3133
3134X #> Y :- X #>= Y + 1.
3135
3156
3157X #< Y :- Y #> X.
3158
3169
3170#\ Q :- reify(Q, 0), do_queue.
3171
3209
3210L #<==> R :- reify(L, B), reify(R, B), do_queue.
3211
3215
3228
3229L #==> R :-
3230 reify(L, LB, LPs),
3231 reify(R, RB, RPs),
3232 append(LPs, RPs, Ps),
3233 propagator_init_trigger([LB,RB], pimpl(LB,RB,Ps)).
3234
3238
3239L #<== R :- R #==> L.
3240
3244
3245L #/\ R :- reify(L, 1), reify(R, 1), do_queue.
3246
3247conjunctive_neqs_var_drep(Eqs, Var, Drep) :-
3248 conjunctive_neqs_var(Eqs, Var),
3249 phrase(conjunctive_neqs_vals(Eqs), Vals),
3250 list_to_domain(Vals, Dom),
3251 domain_complement(Dom, C),
3252 domain_to_drep(C, Drep).
3253
3254conjunctive_neqs_var(V, _) :- var(V), !, false.
3255conjunctive_neqs_var(L #\= R, Var) :-
3256 ( var(L), integer(R) -> Var = L
3257 ; integer(L), var(R) -> Var = R
3258 ; false
3259 ).
3260conjunctive_neqs_var(A #/\ B, VA) :-
3261 conjunctive_neqs_var(A, VA),
3262 conjunctive_neqs_var(B, VB),
3263 VA == VB.
3264
3265conjunctive_neqs_vals(L #\= R) --> ( { integer(L) } -> [L] ; [R] ).
3266conjunctive_neqs_vals(A #/\ B) -->
3267 conjunctive_neqs_vals(A),
3268 conjunctive_neqs_vals(B).
3269
3285
3286L #\/ R :-
3287 ( disjunctive_eqs_var_drep(L #\/ R, Var, Drep) -> Var in Drep
3288 ; reify(L, X, Ps1),
3289 reify(R, Y, Ps2),
3290 propagator_init_trigger([X,Y], reified_or(X,Ps1,Y,Ps2,1))
3291 ).
3292
3293disjunctive_eqs_var_drep(Eqs, Var, Drep) :-
3294 disjunctive_eqs_var(Eqs, Var),
3295 phrase(disjunctive_eqs_vals(Eqs), Vals),
3296 list_to_drep(Vals, Drep).
3297
3298disjunctive_eqs_var(V, _) :- var(V), !, false.
3299disjunctive_eqs_var(V in I, V) :- var(V), integer(I).
3300disjunctive_eqs_var(L #= R, Var) :-
3301 ( var(L), integer(R) -> Var = L
3302 ; integer(L), var(R) -> Var = R
3303 ; false
3304 ).
3305disjunctive_eqs_var(A #\/ B, VA) :-
3306 disjunctive_eqs_var(A, VA),
3307 disjunctive_eqs_var(B, VB),
3308 VA == VB.
3309
3310disjunctive_eqs_vals(L #= R) --> ( { integer(L) } -> [L] ; [R] ).
3311disjunctive_eqs_vals(_ in I) --> [I].
3312disjunctive_eqs_vals(A #\/ B) -->
3313 disjunctive_eqs_vals(A),
3314 disjunctive_eqs_vals(B).
3315
3320
3321L #\ R :- (L #\/ R) #/\ #\ (L #/\ R).
3322
3347
3348parse_reified(E, R, D,
3349 [g(cyclic_term(E)) => [g(domain_error(clpfd_expression, E))],
3350 g(var(E)) => [g(non_monotonic(E)),
3351 g(constrain_to_integer(E)), g(R = E), g(D=1)],
3352 g(integer(E)) => [g(R=E), g(D=1)],
3353 ?(E) => [g(must_be_fd_integer(E)), g(R=E), g(D=1)],
3354 #(E) => [g(must_be_fd_integer(E)), g(R=E), g(D=1)],
3355 m(A+B) => [d(D), p(pplus(A,B,R)), a(A,B,R)],
3356 m(A*B) => [d(D), p(ptimes(A,B,R)), a(A,B,R)],
3357 m(A-B) => [d(D), p(pplus(R,B,A)), a(A,B,R)],
3358 m(-A) => [d(D), p(ptimes(-1,A,R)), a(R)],
3359 m(max(A,B)) => [d(D), p(pgeq(R, A)), p(pgeq(R, B)), p(pmax(A,B,R)), a(A,B,R)],
3360 m(min(A,B)) => [d(D), p(pgeq(A, R)), p(pgeq(B, R)), p(pmin(A,B,R)), a(A,B,R)],
3361 m(abs(A)) => [g(?(R)#>=0), d(D), p(pabs(A, R)), a(A,R)],
3363 m(A//B) => [skeleton(A,B,D,R,ptzdiv)],
3364 m(A div B) => [skeleton(A,B,D,R,pdiv)],
3365 m(A rdiv B) => [skeleton(A,B,D,R,prdiv)],
3366 m(A mod B) => [skeleton(A,B,D,R,pmod)],
3367 m(A rem B) => [skeleton(A,B,D,R,prem)],
3368 m(A^B) => [d(D), p(pexp(A,B,R)), a(A,B,R)],
3369 3370 m(\A) => [function(D,\,A,R)],
3371 m(msb(A)) => [function(D,msb,A,R)],
3372 m(lsb(A)) => [function(D,lsb,A,R)],
3373 m(popcount(A)) => [function(D,popcount,A,R)],
3374 m(A<<B) => [function(D,<<,A,B,R)],
3375 m(A>>B) => [function(D,>>,A,B,R)],
3376 m(A/\B) => [function(D,/\,A,B,R)],
3377 m(A\/B) => [function(D,\/,A,B,R)],
3378 m(A xor B) => [function(D,xor,A,B,R)],
3379 g(true) => [g(domain_error(clpfd_expression, E))]]
3380 ).
3381
3387
3388make_parse_reified(Clauses) :-
3389 parse_reified_clauses(Clauses0),
3390 maplist(goals_goal_dcg, Clauses0, Clauses).
3391
3392goals_goal_dcg((Head --> Goals), Clause) :-
3393 list_goal(Goals, Body),
3394 expand_term((Head --> Body), Clause).
3395
3396parse_reified_clauses(Clauses) :-
3397 parse_reified(E, R, D, Matchers),
3398 maplist(parse_reified(E, R, D), Matchers, Clauses).
3399
3400parse_reified(E, R, D, Matcher, Clause) :-
3401 Matcher = (Condition0 => Goals0),
3402 phrase((reified_condition(Condition0, E, Head, Ds),
3403 reified_goals(Goals0, Ds)), Goals, [a(D)]),
3404 Clause = (parse_reified_clpfd(Head, R, D) --> Goals).
3405
3406reified_condition(g(Goal), E, E, []) --> [{Goal}, !].
3407reified_condition(?(E), _, ?(E), []) --> [!].
3408reified_condition(#(E), _, #(E), []) --> [!].
3409reified_condition(m(Match), _, Match0, Ds) -->
3410 [!],
3411 { copy_term(Match, Match0),
3412 term_variables(Match0, Vs0),
3413 term_variables(Match, Vs)
3414 },
3415 reified_variables(Vs0, Vs, Ds).
3416
3417reified_variables([], [], []) --> [].
3418reified_variables([V0|Vs0], [V|Vs], [D|Ds]) -->
3419 [parse_reified_clpfd(V0, V, D)],
3420 reified_variables(Vs0, Vs, Ds).
3421
3422reified_goals([], _) --> [].
3423reified_goals([G|Gs], Ds) --> reified_goal(G, Ds), reified_goals(Gs, Ds).
3424
3425reified_goal(d(D), Ds) -->
3426 ( { Ds = [X] } -> [{D=X}]
3427 ; { Ds = [X,Y] } ->
3428 { phrase(reified_goal(p(reified_and(X,[],Y,[],D)), _), Gs),
3429 list_goal(Gs, Goal) },
3430 [( {X==1, Y==1} -> {D = 1} ; Goal )]
3431 ; { domain_error(one_or_two_element_list, Ds) }
3432 ).
3433reified_goal(g(Goal), _) --> [{Goal}].
3434reified_goal(p(Vs, Prop), _) -->
3435 [{make_propagator(Prop, P)}],
3436 parse_init_dcg(Vs, P),
3437 [{trigger_once(P)}],
3438 [( { propagator_state(P, S), S == dead } -> [] ; [p(P)])].
3439reified_goal(p(Prop), Ds) -->
3440 { term_variables(Prop, Vs) },
3441 reified_goal(p(Vs,Prop), Ds).
3442reified_goal(function(D,Op,A,B,R), Ds) -->
3443 reified_goals([d(D),p(pfunction(Op,A,B,R)),a(A,B,R)], Ds).
3444reified_goal(function(D,Op,A,R), Ds) -->
3445 reified_goals([d(D),p(pfunction(Op,A,R)),a(A,R)], Ds).
3446reified_goal(skeleton(A,B,D,R,F), Ds) -->
3447 { Prop =.. [F,X,Y,Z] },
3448 reified_goals([d(D1),l(p(P)),g(make_propagator(Prop, P)),
3449 p([A,B,D2,R], pskeleton(A,B,D2,[X,Y,Z]-P,R,F)),
3450 p(reified_and(D1,[],D2,[],D)),a(D2),a(A,B,R)], Ds).
3451reified_goal(a(V), _) --> [a(V)].
3452reified_goal(a(X,V), _) --> [a(X,V)].
3453reified_goal(a(X,Y,V), _) --> [a(X,Y,V)].
3454reified_goal(l(L), _) --> [[L]].
3455
3456parse_init_dcg([], _) --> [].
3457parse_init_dcg([V|Vs], P) --> [{init_propagator(V, P)}], parse_init_dcg(Vs, P).
3458
3461
3462reify(E, B) :- reify(E, B, _).
3463
3464reify(Expr, B, Ps) :-
3465 ( acyclic_term(Expr), reifiable(Expr) -> phrase(reify(Expr, B), Ps)
3466 ; domain_error(clpfd_reifiable_expression, Expr)
3467 ).
3468
3469reifiable(E) :- var(E), non_monotonic(E).
3470reifiable(E) :- integer(E), E in 0..1.
3471reifiable(?(E)) :- must_be_fd_integer(E).
3472reifiable(#(E)) :- must_be_fd_integer(E).
3473reifiable(V in _) :- fd_variable(V).
3474reifiable(Expr) :-
3475 Expr =.. [Op,Left,Right],
3476 ( memberchk(Op, [#>=,#>,#=<,#<,#=,#\=])
3477 ; memberchk(Op, [#==>,#<==,#<==>,#/\,#\/,#\]),
3478 reifiable(Left),
3479 reifiable(Right)
3480 ).
3481reifiable(#\ E) :- reifiable(E).
3482reifiable(tuples_in(Tuples, Relation)) :-
3483 must_be(list(list), Tuples),
3484 maplist(maplist(fd_variable), Tuples),
3485 must_be(list(list(integer)), Relation).
3486reifiable(finite_domain(V)) :- fd_variable(V).
3487
3488reify(E, B) --> { B in 0..1 }, reify_(E, B).
3489
3490reify_(E, B) --> { var(E), !, E = B }.
3491reify_(E, B) --> { integer(E), E = B }.
3492reify_(?(B), B) --> [].
3493reify_(#(B), B) --> [].
3494reify_(V in Drep, B) -->
3495 { drep_to_domain(Drep, Dom) },
3496 propagator_init_trigger(reified_in(V,Dom,B)),
3497 a(B).
3498reify_(tuples_in(Tuples, Relation), B) -->
3499 { maplist(relation_tuple_b_prop(Relation), Tuples, Bs, Ps),
3500 maplist(monotonic, Bs, Bs1),
3501 fold_statement(conjunction, Bs1, And),
3502 ?(B) #<==> And },
3503 propagator_init_trigger([B], tuples_not_in(Tuples, Relation, B)),
3504 kill_reified_tuples(Bs, Ps, Bs),
3505 list(Ps),
3506 as([B|Bs]).
3507reify_(finite_domain(V), B) -->
3508 propagator_init_trigger(reified_fd(V,B)),
3509 a(B).
3510reify_(L #>= R, B) --> arithmetic(L, R, B, reified_geq).
3511reify_(L #= R, B) --> arithmetic(L, R, B, reified_eq).
3512reify_(L #\= R, B) --> arithmetic(L, R, B, reified_neq).
3513reify_(L #> R, B) --> reify_(L #>= (R+1), B).
3514reify_(L #=< R, B) --> reify_(R #>= L, B).
3515reify_(L #< R, B) --> reify_(R #>= (L+1), B).
3516reify_(L #==> R, B) --> reify_((#\ L) #\/ R, B).
3517reify_(L #<== R, B) --> reify_(R #==> L, B).
3518reify_(L #<==> R, B) --> reify_((L #==> R) #/\ (R #==> L), B).
3519reify_(L #\ R, B) --> reify_((L #\/ R) #/\ #\ (L #/\ R), B).
3520reify_(L #/\ R, B) -->
3521 ( { conjunctive_neqs_var_drep(L #/\ R, V, D) } -> reify_(V in D, B)
3522 ; boolean(L, R, B, reified_and)
3523 ).
3524reify_(L #\/ R, B) -->
3525 ( { disjunctive_eqs_var_drep(L #\/ R, V, D) } -> reify_(V in D, B)
3526 ; boolean(L, R, B, reified_or)
3527 ).
3528reify_(#\ Q, B) -->
3529 reify(Q, QR),
3530 propagator_init_trigger(reified_not(QR,B)),
3531 a(B).
3532
3533arithmetic(L, R, B, Functor) -->
3534 { phrase((parse_reified_clpfd(L, LR, LD),
3535 parse_reified_clpfd(R, RR, RD)), Ps),
3536 Prop =.. [Functor,LD,LR,RD,RR,Ps,B] },
3537 list(Ps),
3538 propagator_init_trigger([LD,LR,RD,RR,B], Prop),
3539 a(B).
3540
3541boolean(L, R, B, Functor) -->
3542 { reify(L, LR, Ps1), reify(R, RR, Ps2),
3543 Prop =.. [Functor,LR,Ps1,RR,Ps2,B] },
3544 list(Ps1), list(Ps2),
3545 propagator_init_trigger([LR,RR,B], Prop),
3546 a(LR, RR, B).
3547
3548list([]) --> [].
3549list([L|Ls]) --> [L], list(Ls).
3550
3551a(X,Y,B) -->
3552 ( { nonvar(X) } -> a(Y, B)
3553 ; { nonvar(Y) } -> a(X, B)
3554 ; [a(X,Y,B)]
3555 ).
3556
3557a(X, B) -->
3558 ( { var(X) } -> [a(X, B)]
3559 ; a(B)
3560 ).
3561
3562a(B) -->
3563 ( { var(B) } -> [a(B)]
3564 ; []
3565 ).
3566
3567as([]) --> [].
3568as([B|Bs]) --> a(B), as(Bs).
3569
3570kill_reified_tuples([], _, _) --> [].
3571kill_reified_tuples([B|Bs], Ps, All) -->
3572 propagator_init_trigger([B], kill_reified_tuples(B, Ps, All)),
3573 kill_reified_tuples(Bs, Ps, All).
3574
3575relation_tuple_b_prop(Relation, Tuple, B, p(Prop)) :-
3576 put_attr(R, clpfd_relation, Relation),
3577 make_propagator(reified_tuple_in(Tuple, R, B), Prop),
3578 tuple_freeze_(Tuple, Prop),
3579 init_propagator(B, Prop).
3580
3581
3582tuples_in_conjunction(Tuples, Relation, Conj) :-
3583 maplist(tuple_in_disjunction(Relation), Tuples, Disjs),
3584 fold_statement(conjunction, Disjs, Conj).
3585
3586tuple_in_disjunction(Relation, Tuple, Disj) :-
3587 maplist(tuple_in_conjunction(Tuple), Relation, Conjs),
3588 fold_statement(disjunction, Conjs, Disj).
3589
3590tuple_in_conjunction(Tuple, Element, Conj) :-
3591 maplist(var_eq, Tuple, Element, Eqs),
3592 fold_statement(conjunction, Eqs, Conj).
3593
3594fold_statement(Operation, List, Statement) :-
3595 ( List = [] -> Statement = 1
3596 ; List = [First|Rest],
3597 foldl(Operation, Rest, First, Statement)
3598 ).
3599
3600conjunction(E, Conj, Conj #/\ E).
3601
3602disjunction(E, Disj, Disj #\/ E).
3603
3604var_eq(V, N, ?(V) #= N).
3605
3607
3608skeleton(Vs, Vs-Prop) :-
3609 maplist(prop_init(Prop), Vs),
3610 trigger_once(Prop).
3611
3616
3617is_drep(N) :- integer(N).
3618is_drep(N..M) :- drep_bound(N), drep_bound(M), N \== sup, M \== inf.
3619is_drep(D1\/D2) :- is_drep(D1), is_drep(D2).
3620is_drep({AI}) :- is_and_integers(AI).
3621is_drep(\D) :- is_drep(D).
3622
3623is_and_integers(I) :- integer(I).
3624is_and_integers((A,B)) :- is_and_integers(A), is_and_integers(B).
3625
3626drep_bound(I) :- integer(I).
3627drep_bound(sup).
3628drep_bound(inf).
3629
3630drep_to_intervals(I) --> { integer(I) }, [n(I)-n(I)].
3631drep_to_intervals(N..M) -->
3632 ( { defaulty_to_bound(N, N1), defaulty_to_bound(M, M1),
3633 N1 cis_leq M1} -> [N1-M1]
3634 ; []
3635 ).
3636drep_to_intervals(D1 \/ D2) -->
3637 drep_to_intervals(D1), drep_to_intervals(D2).
3638drep_to_intervals(\D0) -->
3639 { drep_to_domain(D0, D1),
3640 domain_complement(D1, D),
3641 domain_to_drep(D, Drep) },
3642 drep_to_intervals(Drep).
3643drep_to_intervals({AI}) -->
3644 and_integers_(AI).
3645
3646and_integers_(I) --> { integer(I) }, [n(I)-n(I)].
3647and_integers_((A,B)) --> and_integers_(A), and_integers_(B).
3648
3649drep_to_domain(DR, D) :-
3650 must_be(ground, DR),
3651 ( is_drep(DR) -> true
3652 ; domain_error(clpfd_domain, DR)
3653 ),
3654 phrase(drep_to_intervals(DR), Is0),
3655 merge_intervals(Is0, Is1),
3656 intervals_to_domain(Is1, D).
3657
3658merge_intervals(Is0, Is) :-
3659 keysort(Is0, Is1),
3660 merge_overlapping(Is1, Is).
3661
3662merge_overlapping([], []).
3663merge_overlapping([A-B0|ABs0], [A-B|ABs]) :-
3664 merge_remaining(ABs0, B0, B, Rest),
3665 merge_overlapping(Rest, ABs).
3666
3667merge_remaining([], B, B, []).
3668merge_remaining([N-M|NMs], B0, B, Rest) :-
3669 Next cis B0 + n(1),
3670 ( N cis_gt Next -> B = B0, Rest = [N-M|NMs]
3671 ; B1 cis max(B0,M),
3672 merge_remaining(NMs, B1, B, Rest)
3673 ).
3674
3675domain(V, Dom) :-
3676 ( fd_get(V, Dom0, VPs) ->
3677 domains_intersection(Dom, Dom0, Dom1),
3678 3679 fd_put(V, Dom1, VPs),
3680 do_queue,
3681 reinforce(V)
3682 ; domain_contains(Dom, V)
3683 ).
3684
3685domains([], _).
3686domains([V|Vs], D) :- domain(V, D), domains(Vs, D).
3687
3688props_number(fd_props(Gs,Bs,Os), N) :-
3689 length(Gs, N1),
3690 length(Bs, N2),
3691 length(Os, N3),
3692 N is N1 + N2 + N3.
3693
3694fd_get(X, Dom, Ps) :-
3695 ( get_attr(X, clpfd, Attr) -> Attr = clpfd_attr(_,_,_,Dom,Ps)
3696 ; var(X) -> default_domain(Dom), Ps = fd_props([],[],[])
3697 ).
3698
3699fd_get(X, Dom, Inf, Sup, Ps) :-
3700 fd_get(X, Dom, Ps),
3701 domain_infimum(Dom, Inf),
3702 domain_supremum(Dom, Sup).
3703
3717
3718fd_put(X, Dom, Ps) :-
3719 ( current_prolog_flag(clpfd_propagation, full) ->
3720 put_full(X, Dom, Ps)
3721 ; put_terminating(X, Dom, Ps)
3722 ).
3723
3724put_terminating(X, Dom, Ps) :-
3725 Dom \== empty,
3726 ( Dom = from_to(F, F) -> F = n(X)
3727 ; ( get_attr(X, clpfd, Attr) ->
3728 Attr = clpfd_attr(Left,Right,Spread,OldDom, _OldPs),
3729 put_attr(X, clpfd, clpfd_attr(Left,Right,Spread,Dom,Ps)),
3730 ( OldDom == Dom -> true
3731 ; ( Left == (.) -> Bounded = yes
3732 ; domain_infimum(Dom, Inf), domain_supremum(Dom, Sup),
3733 ( Inf = n(_), Sup = n(_) ->
3734 Bounded = yes
3735 ; Bounded = no
3736 )
3737 ),
3738 ( Bounded == yes ->
3739 put_attr(X, clpfd, clpfd_attr(.,.,.,Dom,Ps)),
3740 trigger_props(Ps, X, OldDom, Dom)
3741 ; 3742 domain_infimum(OldDom, OldInf),
3743 ( Inf == OldInf -> LeftP = Left
3744 ; LeftP = yes
3745 ),
3746 domain_supremum(OldDom, OldSup),
3747 ( Sup == OldSup -> RightP = Right
3748 ; RightP = yes
3749 ),
3750 domain_spread(OldDom, OldSpread),
3751 domain_spread(Dom, NewSpread),
3752 ( NewSpread == OldSpread -> SpreadP = Spread
3753 ; NewSpread cis_lt OldSpread -> SpreadP = no
3754 ; SpreadP = yes
3755 ),
3756 put_attr(X, clpfd, clpfd_attr(LeftP,RightP,SpreadP,Dom,Ps)),
3757 ( RightP == yes, Right = yes -> true
3758 ; LeftP == yes, Left = yes -> true
3759 ; SpreadP == yes, Spread = yes -> true
3760 ; trigger_props(Ps, X, OldDom, Dom)
3761 )
3762 )
3763 )
3764 ; var(X) ->
3765 put_attr(X, clpfd, clpfd_attr(no,no,no,Dom, Ps))
3766 ; true
3767 )
3768 ).
3769
3770domain_spread(Dom, Spread) :-
3771 domain_smallest_finite(Dom, S),
3772 domain_largest_finite(Dom, L),
3773 Spread cis L - S.
3774
3775smallest_finite(inf, Y, Y).
3776smallest_finite(n(N), _, n(N)).
3777
3778domain_smallest_finite(from_to(F,T), S) :- smallest_finite(F, T, S).
3779domain_smallest_finite(split(_, L, _), S) :- domain_smallest_finite(L, S).
3780
3781largest_finite(sup, Y, Y).
3782largest_finite(n(N), _, n(N)).
3783
3784domain_largest_finite(from_to(F,T), L) :- largest_finite(T, F, L).
3785domain_largest_finite(split(_, _, R), L) :- domain_largest_finite(R, L).
3786
3791
3792reinforce(X) :-
3793 ( current_prolog_flag(clpfd_propagation, full) ->
3794 3795 true
3796 ; term_variables(X, Vs),
3797 maplist(reinforce_, Vs),
3798 do_queue
3799 ).
3800
3801reinforce_(X) :-
3802 ( fd_var(X), fd_get(X, Dom, Ps) ->
3803 put_full(X, Dom, Ps)
3804 ; true
3805 ).
3806
3807put_full(X, Dom, Ps) :-
3808 Dom \== empty,
3809 ( Dom = from_to(F, F) -> F = n(X)
3810 ; ( get_attr(X, clpfd, Attr) ->
3811 Attr = clpfd_attr(_,_,_,OldDom, _OldPs),
3812 put_attr(X, clpfd, clpfd_attr(no,no,no,Dom, Ps)),
3813 3814 ( OldDom == Dom -> true
3815 ; trigger_props(Ps, X, OldDom, Dom)
3816 )
3817 ; var(X) -> 3818 put_attr(X, clpfd, clpfd_attr(no,no,no,Dom, Ps))
3819 ; true
3820 )
3821 ).
3822
3830
3831make_propagator(C, propagator(C, _)).
3832
3833propagator_state(propagator(_,S), S).
3834
3835trigger_props(fd_props(Gs,Bs,Os), X, D0, D) :-
3836 ( ground(X) ->
3837 trigger_props_(Gs),
3838 trigger_props_(Bs)
3839 ; Bs \== [] ->
3840 domain_infimum(D0, I0),
3841 domain_infimum(D, I),
3842 ( I == I0 ->
3843 domain_supremum(D0, S0),
3844 domain_supremum(D, S),
3845 ( S == S0 -> true
3846 ; trigger_props_(Bs)
3847 )
3848 ; trigger_props_(Bs)
3849 )
3850 ; true
3851 ),
3852 trigger_props_(Os).
3853
3854trigger_props(fd_props(Gs,Bs,Os), X) :-
3855 trigger_props_(Os),
3856 trigger_props_(Bs),
3857 ( ground(X) ->
3858 trigger_props_(Gs)
3859 ; true
3860 ).
3861
3862trigger_props(fd_props(Gs,Bs,Os)) :-
3863 trigger_props_(Gs),
3864 trigger_props_(Bs),
3865 trigger_props_(Os).
3866
3867trigger_props_([]).
3868trigger_props_([P|Ps]) :- trigger_prop(P), trigger_props_(Ps).
3869
3870trigger_prop(Propagator) :-
3871 propagator_state(Propagator, State),
3872 ( State == dead -> true
3873 ; get_attr(State, clpfd_aux, queued) -> true
3874 ; b_getval('$clpfd_current_propagator', C), C == State -> true
3875 ; 3876 3877 put_attr(State, clpfd_aux, queued),
3878 ( arg(1, Propagator, C), functor(C, F, _), global_constraint(F) ->
3879 push_queue(Propagator, 2)
3880 ; push_queue(Propagator, 1)
3881 )
3882 ).
3883
3884kill(State) :- del_attr(State, clpfd_aux), State = dead.
3885
3886kill(State, Ps) :-
3887 kill(State),
3888 maplist(kill_entailed, Ps).
3889
3890kill_entailed(p(Prop)) :-
3891 propagator_state(Prop, State),
3892 kill(State).
3893kill_entailed(a(V)) :-
3894 del_attr(V, clpfd).
3895kill_entailed(a(X,B)) :-
3896 ( X == B -> true
3897 ; del_attr(B, clpfd)
3898 ).
3899kill_entailed(a(X,Y,B)) :-
3900 ( X == B -> true
3901 ; Y == B -> true
3902 ; del_attr(B, clpfd)
3903 ).
3904
3905no_reactivation(rel_tuple(_,_)).
3906no_reactivation(pdistinct(_)).
3907no_reactivation(pgcc(_,_,_)).
3908no_reactivation(pgcc_single(_,_)).
3910
3911activate_propagator(propagator(P,State)) :-
3912 3913 del_attr(State, clpfd_aux),
3914 ( no_reactivation(P) ->
3915 b_setval('$clpfd_current_propagator', State),
3916 run_propagator(P, State),
3917 b_setval('$clpfd_current_propagator', [])
3918 ; run_propagator(P, State)
3919 ).
3920
3921disable_queue :- b_setval('$clpfd_queue_status', disabled).
3922enable_queue :- b_setval('$clpfd_queue_status', enabled).
3923
3924portray_propagator(propagator(P,_), F) :- functor(P, F, _).
3925
3926portray_queue(V, []) :- var(V), !.
3927portray_queue([P|Ps], [F|Fs]) :-
3928 portray_propagator(P, F),
3929 portray_queue(Ps, Fs).
3930
3931do_queue :-
3932 3933 3934 3935 ( b_getval('$clpfd_queue_status', enabled) ->
3936 ( fetch_propagator(Propagator) ->
3937 activate_propagator(Propagator),
3938 do_queue
3939 ; true
3940 )
3941 ; true
3942 ).
3943
3944init_propagator(Var, Prop) :-
3945 ( fd_get(Var, Dom, Ps0) ->
3946 insert_propagator(Prop, Ps0, Ps),
3947 fd_put(Var, Dom, Ps)
3948 ; true
3949 ).
3950
3951constraint_wake(pneq, ground).
3952constraint_wake(x_neq_y_plus_z, ground).
3953constraint_wake(absdiff_neq, ground).
3954constraint_wake(pdifferent, ground).
3955constraint_wake(pexclude, ground).
3956constraint_wake(scalar_product_neq, ground).
3957
3958constraint_wake(x_leq_y_plus_c, bounds).
3959constraint_wake(scalar_product_eq, bounds).
3960constraint_wake(scalar_product_leq, bounds).
3961constraint_wake(pplus, bounds).
3962constraint_wake(pgeq, bounds).
3963constraint_wake(pgcc_single, bounds).
3964constraint_wake(pgcc_check_single, bounds).
3965
3966global_constraint(pdistinct).
3967global_constraint(pgcc).
3968global_constraint(pgcc_single).
3969global_constraint(pcircuit).
3972
3973insert_propagator(Prop, Ps0, Ps) :-
3974 Ps0 = fd_props(Gs,Bs,Os),
3975 arg(1, Prop, Constraint),
3976 functor(Constraint, F, _),
3977 ( constraint_wake(F, ground) ->
3978 Ps = fd_props([Prop|Gs], Bs, Os)
3979 ; constraint_wake(F, bounds) ->
3980 Ps = fd_props(Gs, [Prop|Bs], Os)
3981 ; Ps = fd_props(Gs, Bs, [Prop|Os])
3982 ).
3983
3985
3989
3990lex_chain(Lss) :-
3991 must_be(list(list), Lss),
3992 maplist(maplist(fd_variable), Lss),
3993 ( Lss == [] -> true
3994 ; Lss = [First|Rest],
3995 make_propagator(presidual(lex_chain(Lss)), Prop),
3996 foldl(lex_chain_(Prop), Rest, First, _)
3997 ).
3998
3999lex_chain_(Prop, Ls, Prev, Ls) :-
4000 maplist(prop_init(Prop), Ls),
4001 lex_le(Prev, Ls).
4002
4003lex_le([], []).
4004lex_le([V1|V1s], [V2|V2s]) :-
4005 ?(V1) #=< ?(V2),
4006 ( integer(V1) ->
4007 ( integer(V2) ->
4008 ( V1 =:= V2 -> lex_le(V1s, V2s) ; true )
4009 ; freeze(V2, lex_le([V1|V1s], [V2|V2s]))
4010 )
4011 ; freeze(V1, lex_le([V1|V1s], [V2|V2s]))
4012 ).
4013
4015
4016
4059
4060tuples_in(Tuples, Relation) :-
4061 must_be(list(list), Tuples),
4062 maplist(maplist(fd_variable), Tuples),
4063 must_be(list(list(integer)), Relation),
4064 maplist(relation_tuple(Relation), Tuples),
4065 do_queue.
4066
4067relation_tuple(Relation, Tuple) :-
4068 relation_unifiable(Relation, Tuple, Us, _, _),
4069 ( ground(Tuple) -> memberchk(Tuple, Relation)
4070 ; tuple_domain(Tuple, Us),
4071 ( Tuple = [_,_|_] -> tuple_freeze(Tuple, Us)
4072 ; true
4073 )
4074 ).
4075
4076tuple_domain([], _).
4077tuple_domain([T|Ts], Relation0) :-
4078 maplist(list_first_rest, Relation0, Firsts, Relation1),
4079 ( var(T) ->
4080 ( Firsts = [Unique] -> T = Unique
4081 ; list_to_domain(Firsts, FDom),
4082 fd_get(T, TDom, TPs),
4083 domains_intersection(TDom, FDom, TDom1),
4084 fd_put(T, TDom1, TPs)
4085 )
4086 ; true
4087 ),
4088 tuple_domain(Ts, Relation1).
4089
4090tuple_freeze(Tuple, Relation) :-
4091 put_attr(R, clpfd_relation, Relation),
4092 make_propagator(rel_tuple(R, Tuple), Prop),
4093 tuple_freeze_(Tuple, Prop).
4094
4095tuple_freeze_([], _).
4096tuple_freeze_([T|Ts], Prop) :-
4097 ( var(T) ->
4098 init_propagator(T, Prop),
4099 trigger_prop(Prop)
4100 ; true
4101 ),
4102 tuple_freeze_(Ts, Prop).
4103
4104relation_unifiable([], _, [], Changed, Changed).
4105relation_unifiable([R|Rs], Tuple, Us, Changed0, Changed) :-
4106 ( all_in_domain(R, Tuple) ->
4107 Us = [R|Rest],
4108 relation_unifiable(Rs, Tuple, Rest, Changed0, Changed)
4109 ; relation_unifiable(Rs, Tuple, Us, true, Changed)
4110 ).
4111
4112all_in_domain([], []).
4113all_in_domain([A|As], [T|Ts]) :-
4114 ( fd_get(T, Dom, _) ->
4115 domain_contains(Dom, A)
4116 ; T =:= A
4117 ),
4118 all_in_domain(As, Ts).
4119
4121
4123run_propagator(presidual(_), _).
4124
4126run_propagator(pdifferent(Left,Right,X,_), MState) :-
4127 run_propagator(pexclude(Left,Right,X), MState).
4128
4129run_propagator(weak_distinct(Left,Right,X,_), _MState) :-
4130 ( ground(X) ->
4131 disable_queue,
4132 exclude_fire(Left, Right, X),
4133 enable_queue
4134 ; outof_reducer(Left, Right, X)
4135 4136 4137 4138 ).
4139
4140run_propagator(pexclude(Left,Right,X), _) :-
4141 ( ground(X) ->
4142 disable_queue,
4143 exclude_fire(Left, Right, X),
4144 enable_queue
4145 ; true
4146 ).
4147
4148run_propagator(pdistinct(Ls), _MState) :-
4149 distinct(Ls).
4150
4151run_propagator(check_distinct(Left,Right,X), _) :-
4152 \+ list_contains(Left, X),
4153 \+ list_contains(Right, X).
4154
4156
4157run_propagator(pelement(N, Is, V), MState) :-
4158 ( fd_get(N, NDom, _) ->
4159 ( fd_get(V, VDom, VPs) ->
4160 integers_remaining(Is, 1, NDom, empty, VDom1),
4161 domains_intersection(VDom, VDom1, VDom2),
4162 fd_put(V, VDom2, VPs)
4163 ; true
4164 )
4165 ; kill(MState), nth1(N, Is, V)
4166 ).
4167
4169
4170run_propagator(pgcc_single(Vs, Pairs), _) :- gcc_global(Vs, Pairs).
4171
4172run_propagator(pgcc_check_single(Pairs), _) :- gcc_check(Pairs).
4173
4174run_propagator(pgcc_check(Pairs), _) :- gcc_check(Pairs).
4175
4176run_propagator(pgcc(Vs, _, Pairs), _) :- gcc_global(Vs, Pairs).
4177
4179
4180run_propagator(pcircuit(Vs), _MState) :-
4181 distinct(Vs),
4182 propagate_circuit(Vs).
4183
4185run_propagator(pneq(A, B), MState) :-
4186 ( nonvar(A) ->
4187 ( nonvar(B) -> A =\= B, kill(MState)
4188 ; fd_get(B, BD0, BExp0),
4189 domain_remove(BD0, A, BD1),
4190 kill(MState),
4191 fd_put(B, BD1, BExp0)
4192 )
4193 ; nonvar(B) -> run_propagator(pneq(B, A), MState)
4194 ; A \== B,
4195 fd_get(A, _, AI, AS, _), fd_get(B, _, BI, BS, _),
4196 ( AS cis_lt BI -> kill(MState)
4197 ; AI cis_gt BS -> kill(MState)
4198 ; true
4199 )
4200 ).
4201
4203run_propagator(pgeq(A,B), MState) :-
4204 ( A == B -> kill(MState)
4205 ; nonvar(A) ->
4206 ( nonvar(B) -> kill(MState), A >= B
4207 ; fd_get(B, BD, BPs),
4208 domain_remove_greater_than(BD, A, BD1),
4209 kill(MState),
4210 fd_put(B, BD1, BPs)
4211 )
4212 ; nonvar(B) ->
4213 fd_get(A, AD, APs),
4214 domain_remove_smaller_than(AD, B, AD1),
4215 kill(MState),
4216 fd_put(A, AD1, APs)
4217 ; fd_get(A, AD, AL, AU, APs),
4218 fd_get(B, _, BL, BU, _),
4219 AU cis_geq BL,
4220 ( AL cis_geq BU -> kill(MState)
4221 ; AU == BL -> kill(MState), A = B
4222 ; NAL cis max(AL,BL),
4223 domains_intersection(AD, from_to(NAL,AU), NAD),
4224 fd_put(A, NAD, APs),
4225 ( fd_get(B, BD2, BL2, BU2, BPs2) ->
4226 NBU cis min(BU2, AU),
4227 domains_intersection(BD2, from_to(BL2,NBU), NBD),
4228 fd_put(B, NBD, BPs2)
4229 ; true
4230 )
4231 )
4232 ).
4233
4235
4236run_propagator(rel_tuple(R, Tuple), MState) :-
4237 get_attr(R, clpfd_relation, Relation),
4238 ( ground(Tuple) -> kill(MState), memberchk(Tuple, Relation)
4239 ; relation_unifiable(Relation, Tuple, Us, false, Changed),
4240 Us = [_|_],
4241 ( Tuple = [First,Second], ( ground(First) ; ground(Second) ) ->
4242 kill(MState)
4243 ; true
4244 ),
4245 ( Us = [Single] -> kill(MState), Single = Tuple
4246 ; Changed ->
4247 put_attr(R, clpfd_relation, Us),
4248 disable_queue,
4249 tuple_domain(Tuple, Us),
4250 enable_queue
4251 ; true
4252 )
4253 ).
4254
4256
4257run_propagator(pserialized(S_I, D_I, S_J, D_J, _), MState) :-
4258 ( nonvar(S_I), nonvar(S_J) ->
4259 kill(MState),
4260 ( S_I + D_I =< S_J -> true
4261 ; S_J + D_J =< S_I -> true
4262 ; false
4263 )
4264 ; serialize_lower_upper(S_I, D_I, S_J, D_J, MState),
4265 serialize_lower_upper(S_J, D_J, S_I, D_I, MState)
4266 ).
4267
4269
4271run_propagator(absdiff_neq(X,Y,C), MState) :-
4272 ( C < 0 -> kill(MState)
4273 ; nonvar(X) ->
4274 kill(MState),
4275 ( nonvar(Y) -> abs(X - Y) =\= C
4276 ; V1 is X - C, neq_num(Y, V1),
4277 V2 is C + X, neq_num(Y, V2)
4278 )
4279 ; nonvar(Y) -> kill(MState),
4280 V1 is C + Y, neq_num(X, V1),
4281 V2 is Y - C, neq_num(X, V2)
4282 ; true
4283 ).
4284
4286run_propagator(absdiff_geq(X,Y,C), MState) :-
4287 ( C =< 0 -> kill(MState)
4288 ; nonvar(X) ->
4289 kill(MState),
4290 ( nonvar(Y) -> abs(X-Y) >= C
4291 ; P1 is X - C, P2 is X + C,
4292 Y in inf..P1 \/ P2..sup
4293 )
4294 ; nonvar(Y) ->
4295 kill(MState),
4296 P1 is Y - C, P2 is Y + C,
4297 X in inf..P1 \/ P2..sup
4298 ; true
4299 ).
4300
4302run_propagator(x_neq_y_plus_z(X,Y,Z), MState) :-
4303 ( nonvar(X) ->
4304 ( nonvar(Y) ->
4305 ( nonvar(Z) -> kill(MState), X =\= Y + Z
4306 ; kill(MState), XY is X - Y, neq_num(Z, XY)
4307 )
4308 ; nonvar(Z) -> kill(MState), XZ is X - Z, neq_num(Y, XZ)
4309 ; true
4310 )
4311 ; nonvar(Y) ->
4312 ( nonvar(Z) ->
4313 kill(MState), YZ is Y + Z, neq_num(X, YZ)
4314 ; Y =:= 0 -> kill(MState), neq(X, Z)
4315 ; true
4316 )
4317 ; Z == 0 -> kill(MState), neq(X, Y)
4318 ; true
4319 ).
4320
4322run_propagator(x_leq_y_plus_c(X,Y,C), MState) :-
4323 ( nonvar(X) ->
4324 ( nonvar(Y) -> kill(MState), X =< Y + C
4325 ; kill(MState),
4326 R is X - C,
4327 fd_get(Y, YD, YPs),
4328 domain_remove_smaller_than(YD, R, YD1),
4329 fd_put(Y, YD1, YPs)
4330 )
4331 ; nonvar(Y) ->
4332 kill(MState),
4333 R is Y + C,
4334 fd_get(X, XD, XPs),
4335 domain_remove_greater_than(XD, R, XD1),
4336 fd_put(X, XD1, XPs)
4337 ; ( X == Y -> C >= 0, kill(MState)
4338 ; fd_get(Y, YD, _),
4339 ( domain_supremum(YD, n(YSup)) ->
4340 YS1 is YSup + C,
4341 fd_get(X, XD, XPs),
4342 domain_remove_greater_than(XD, YS1, XD1),
4343 fd_put(X, XD1, XPs)
4344 ; true
4345 ),
4346 ( fd_get(X, XD2, _), domain_infimum(XD2, n(XInf)) ->
4347 XI1 is XInf - C,
4348 ( fd_get(Y, YD1, YPs1) ->
4349 domain_remove_smaller_than(YD1, XI1, YD2),
4350 ( domain_infimum(YD2, n(YInf)),
4351 domain_supremum(XD2, n(XSup)),
4352 XSup =< YInf + C ->
4353 kill(MState)
4354 ; true
4355 ),
4356 fd_put(Y, YD2, YPs1)
4357 ; true
4358 )
4359 ; true
4360 )
4361 )
4362 ).
4363
4364run_propagator(scalar_product_neq(Cs0,Vs0,P0), MState) :-
4365 coeffs_variables_const(Cs0, Vs0, Cs, Vs, 0, I),
4366 P is P0 - I,
4367 ( Vs = [] -> kill(MState), P =\= 0
4368 ; Vs = [V], Cs = [C] ->
4369 kill(MState),
4370 ( C =:= 1 -> neq_num(V, P)
4371 ; C*V #\= P
4372 )
4373 ; Cs == [1,-1] -> kill(MState), Vs = [A,B], x_neq_y_plus_z(A, B, P)
4374 ; Cs == [-1,1] -> kill(MState), Vs = [A,B], x_neq_y_plus_z(B, A, P)
4375 ; P =:= 0, Cs = [1,1,-1] ->
4376 kill(MState), Vs = [A,B,C], x_neq_y_plus_z(C, A, B)
4377 ; P =:= 0, Cs = [1,-1,1] ->
4378 kill(MState), Vs = [A,B,C], x_neq_y_plus_z(B, A, C)
4379 ; P =:= 0, Cs = [-1,1,1] ->
4380 kill(MState), Vs = [A,B,C], x_neq_y_plus_z(A, B, C)
4381 ; true
4382 ).
4383
4384run_propagator(scalar_product_leq(Cs0,Vs0,P0), MState) :-
4385 coeffs_variables_const(Cs0, Vs0, Cs, Vs, 0, I),
4386 P is P0 - I,
4387 ( Vs = [] -> kill(MState), P >= 0
4388 ; sum_finite_domains(Cs, Vs, Infs, Sups, 0, 0, Inf, Sup),
4389 D1 is P - Inf,
4390 disable_queue,
4391 ( Infs == [], Sups == [] ->
4392 Inf =< P,
4393 ( Sup =< P -> kill(MState)
4394 ; remove_dist_upper_leq(Cs, Vs, D1)
4395 )
4396 ; Infs == [] -> Inf =< P, remove_dist_upper(Sups, D1)
4397 ; Sups = [_], Infs = [_] ->
4398 remove_upper(Infs, D1)
4399 ; Infs = [_] -> remove_upper(Infs, D1)
4400 ; true
4401 ),
4402 enable_queue
4403 ).
4404
4405run_propagator(scalar_product_eq(Cs0,Vs0,P0), MState) :-
4406 coeffs_variables_const(Cs0, Vs0, Cs, Vs, 0, I),
4407 P is P0 - I,
4408 ( Vs = [] -> kill(MState), P =:= 0
4409 ; Vs = [V], Cs = [C] -> kill(MState), P mod C =:= 0, V is P // C
4410 ; Cs == [1,1] -> kill(MState), Vs = [A,B], A + B #= P
4411 ; Cs == [1,-1] -> kill(MState), Vs = [A,B], A #= P + B
4412 ; Cs == [-1,1] -> kill(MState), Vs = [A,B], B #= P + A
4413 ; Cs == [-1,-1] -> kill(MState), Vs = [A,B], P1 is -P, A + B #= P1
4414 ; P =:= 0, Cs == [1,1,-1] -> kill(MState), Vs = [A,B,C], A + B #= C
4415 ; P =:= 0, Cs == [1,-1,1] -> kill(MState), Vs = [A,B,C], A + C #= B
4416 ; P =:= 0, Cs == [-1,1,1] -> kill(MState), Vs = [A,B,C], B + C #= A
4417 ; sum_finite_domains(Cs, Vs, Infs, Sups, 0, 0, Inf, Sup),
4418 4419 D1 is P - Inf,
4420 D2 is Sup - P,
4421 disable_queue,
4422 ( Infs == [], Sups == [] ->
4423 between(Inf, Sup, P),
4424 remove_dist_upper_lower(Cs, Vs, D1, D2)
4425 ; Sups = [] -> P =< Sup, remove_dist_lower(Infs, D2)
4426 ; Infs = [] -> Inf =< P, remove_dist_upper(Sups, D1)
4427 ; Sups = [_], Infs = [_] ->
4428 remove_lower(Sups, D2),
4429 remove_upper(Infs, D1)
4430 ; Infs = [_] -> remove_upper(Infs, D1)
4431 ; Sups = [_] -> remove_lower(Sups, D2)
4432 ; true
4433 ),
4434 enable_queue
4435 ).
4436
4438run_propagator(pplus(X,Y,Z), MState) :-
4439 ( nonvar(X) ->
4440 ( X =:= 0 -> kill(MState), Y = Z
4441 ; Y == Z -> kill(MState), X =:= 0
4442 ; nonvar(Y) -> kill(MState), Z is X + Y
4443 ; nonvar(Z) -> kill(MState), Y is Z - X
4444 ; fd_get(Z, ZD, ZPs),
4445 fd_get(Y, YD, _),
4446 domain_shift(YD, X, Shifted_YD),
4447 domains_intersection(ZD, Shifted_YD, ZD1),
4448 fd_put(Z, ZD1, ZPs),
4449 ( fd_get(Y, YD1, YPs) ->
4450 O is -X,
4451 domain_shift(ZD1, O, YD2),
4452 domains_intersection(YD1, YD2, YD3),
4453 fd_put(Y, YD3, YPs)
4454 ; true
4455 )
4456 )
4457 ; nonvar(Y) -> run_propagator(pplus(Y,X,Z), MState)
4458 ; nonvar(Z) ->
4459 ( X == Y -> kill(MState), even(Z), X is Z // 2
4460 ; fd_get(X, XD, _),
4461 fd_get(Y, YD, YPs),
4462 domain_negate(XD, XDN),
4463 domain_shift(XDN, Z, YD1),
4464 domains_intersection(YD, YD1, YD2),
4465 fd_put(Y, YD2, YPs),
4466 ( fd_get(X, XD1, XPs) ->
4467 domain_negate(YD2, YD2N),
4468 domain_shift(YD2N, Z, XD2),
4469 domains_intersection(XD1, XD2, XD3),
4470 fd_put(X, XD3, XPs)
4471 ; true
4472 )
4473 )
4474 ; ( X == Y -> kill(MState), 2*X #= Z
4475 ; X == Z -> kill(MState), Y = 0
4476 ; Y == Z -> kill(MState), X = 0
4477 ; fd_get(X, XD, XL, XU, XPs),
4478 fd_get(Y, _, YL, YU, _),
4479 fd_get(Z, _, ZL, ZU, _),
4480 NXL cis max(XL, ZL-YU),
4481 NXU cis min(XU, ZU-YL),
4482 update_bounds(X, XD, XPs, XL, XU, NXL, NXU),
4483 ( fd_get(Y, YD2, YL2, YU2, YPs2) ->
4484 NYL cis max(YL2, ZL-NXU),
4485 NYU cis min(YU2, ZU-NXL),
4486 update_bounds(Y, YD2, YPs2, YL2, YU2, NYL, NYU)
4487 ; NYL = n(Y), NYU = n(Y)
4488 ),
4489 ( fd_get(Z, ZD2, ZL2, ZU2, ZPs2) ->
4490 NZL cis max(ZL2,NXL+NYL),
4491 NZU cis min(ZU2,NXU+NYU),
4492 update_bounds(Z, ZD2, ZPs2, ZL2, ZU2, NZL, NZU)
4493 ; true
4494 )
4495 )
4496 ).
4497
4499
4500run_propagator(ptimes(X,Y,Z), MState) :-
4501 ( nonvar(X) ->
4502 ( nonvar(Y) -> kill(MState), Z is X * Y
4503 ; X =:= 0 -> kill(MState), Z = 0
4504 ; X =:= 1 -> kill(MState), Z = Y
4505 ; nonvar(Z) -> kill(MState), 0 =:= Z mod X, Y is Z // X
4506 ; ( Y == Z -> kill(MState), Y = 0
4507 ; fd_get(Y, YD, _),
4508 fd_get(Z, ZD, ZPs),
4509 domain_expand(YD, X, Scaled_YD),
4510 domains_intersection(ZD, Scaled_YD, ZD1),
4511 fd_put(Z, ZD1, ZPs),
4512 ( fd_get(Y, YDom2, YPs2) ->
4513 domain_contract(ZD1, X, Contract),
4514 domains_intersection(YDom2, Contract, NYDom),
4515 fd_put(Y, NYDom, YPs2)
4516 ; kill(MState), Z is X * Y
4517 )
4518 )
4519 )
4520 ; nonvar(Y) -> run_propagator(ptimes(Y,X,Z), MState)
4521 ; nonvar(Z) ->
4522 ( X == Y ->
4523 kill(MState),
4524 integer_kth_root(Z, 2, R),
4525 NR is -R,
4526 X in NR \/ R
4527 ; fd_get(X, XD, XL, XU, XPs),
4528 fd_get(Y, YD, YL, YU, _),
4529 min_max_factor(n(Z), n(Z), YL, YU, XL, XU, NXL, NXU),
4530 update_bounds(X, XD, XPs, XL, XU, NXL, NXU),
4531 ( fd_get(Y, YD2, YL2, YU2, YPs2) ->
4532 min_max_factor(n(Z), n(Z), NXL, NXU, YL2, YU2, NYL, NYU),
4533 update_bounds(Y, YD2, YPs2, YL2, YU2, NYL, NYU)
4534 ; ( Y =\= 0 -> 0 =:= Z mod Y, kill(MState), X is Z // Y
4535 ; kill(MState), Z = 0
4536 )
4537 ),
4538 ( Z =:= 0 ->
4539 ( \+ domain_contains(XD, 0) -> kill(MState), Y = 0
4540 ; \+ domain_contains(YD, 0) -> kill(MState), X = 0
4541 ; true
4542 )
4543 ; neq_num(X, 0), neq_num(Y, 0)
4544 )
4545 )
4546 ; ( X == Y -> kill(MState), X^2 #= Z
4547 ; fd_get(X, XD, XL, XU, XPs),
4548 fd_get(Y, _, YL, YU, _),
4549 fd_get(Z, ZD, ZL, ZU, _),
4550 ( Y == Z, \+ domain_contains(ZD, 0) -> kill(MState), X = 1
4551 ; X == Z, \+ domain_contains(ZD, 0) -> kill(MState), Y = 1
4552 ; min_max_factor(ZL, ZU, YL, YU, XL, XU, NXL, NXU),
4553 update_bounds(X, XD, XPs, XL, XU, NXL, NXU),
4554 ( fd_get(Y, YD2, YL2, YU2, YPs2) ->
4555 min_max_factor(ZL, ZU, NXL, NXU, YL2, YU2, NYL, NYU),
4556 update_bounds(Y, YD2, YPs2, YL2, YU2, NYL, NYU)
4557 ; NYL = n(Y), NYU = n(Y)
4558 ),
4559 ( fd_get(Z, ZD2, ZL2, ZU2, ZPs2) ->
4560 min_product(NXL, NXU, NYL, NYU, NZL),
4561 max_product(NXL, NXU, NYL, NYU, NZU),
4562 ( NZL cis_leq ZL2, NZU cis_geq ZU2 -> ZD3 = ZD2
4563 ; domains_intersection(ZD2, from_to(NZL,NZU), ZD3),
4564 fd_put(Z, ZD3, ZPs2)
4565 ),
4566 ( domain_contains(ZD3, 0) -> true
4567 ; neq_num(X, 0), neq_num(Y, 0)
4568 )
4569 ; true
4570 )
4571 )
4572 )
4573 ).
4574
4576
4578run_propagator(pdiv(X,Y,Z), MState) :- kill(MState), Z #= (X-(X mod Y)) // Y.
4579
4581run_propagator(prdiv(X,Y,Z), MState) :- kill(MState), Z*Y #= X.
4582
4584run_propagator(ptzdiv(X,Y,Z), MState) :-
4585 ( nonvar(X) ->
4586 ( nonvar(Y) -> kill(MState), Y =\= 0, Z is X // Y
4587 ; fd_get(Y, YD, YL, YU, YPs),
4588 ( nonvar(Z) ->
4589 ( Z =:= 0 ->
4590 NYL is -abs(X) - 1,
4591 NYU is abs(X) + 1,
4592 domains_intersection(YD, split(0, from_to(inf,n(NYL)),
4593 from_to(n(NYU), sup)),
4594 NYD),
4595 fd_put(Y, NYD, YPs)
4596 ; ( sign(X) =:= sign(Z) ->
4597 NYL cis max(n(X) // (n(Z)+sign(n(Z))) + n(1), YL),
4598 NYU cis min(n(X) // n(Z), YU)
4599 ; NYL cis max(n(X) // n(Z), YL),
4600 NYU cis min(n(X) // (n(Z)+sign(n(Z))) - n(1), YU)
4601 ),
4602 update_bounds(Y, YD, YPs, YL, YU, NYL, NYU)
4603 )
4604 ; fd_get(Z, ZD, ZL, ZU, ZPs),
4605 ( X >= 0, ( YL cis_gt n(0) ; YU cis_lt n(0) )->
4606 NZL cis max(n(X)//YU, ZL),
4607 NZU cis min(n(X)//YL, ZU)
4608 ; X < 0, ( YL cis_gt n(0) ; YU cis_lt n(0) ) ->
4609 NZL cis max(n(X)//YL, ZL),
4610 NZU cis min(n(X)//YU, ZU)
4611 ; 4612 NZL cis max(-abs(n(X)), ZL),
4613 NZU cis min(abs(n(X)), ZU)
4614 ),
4615 update_bounds(Z, ZD, ZPs, ZL, ZU, NZL, NZU),
4616 ( X >= 0, NZL cis_gt n(0), fd_get(Y, YD1, YPs1) ->
4617 NYL cis n(X) // (NZU + n(1)) + n(1),
4618 NYU cis n(X) // NZL,
4619 domains_intersection(YD1, from_to(NYL, NYU), NYD1),
4620 fd_put(Y, NYD1, YPs1)
4621 ; true
4622 )
4623 )
4624 )
4625 ; nonvar(Y) ->
4626 Y =\= 0,
4627 ( Y =:= 1 -> kill(MState), X = Z
4628 ; Y =:= -1 -> kill(MState), Z #= -X
4629 ; fd_get(X, XD, XL, XU, XPs),
4630 ( nonvar(Z) ->
4631 kill(MState),
4632 ( sign(Z) =:= sign(Y) ->
4633 NXL cis max(n(Z)*n(Y), XL),
4634 NXU cis min((abs(n(Z))+n(1))*abs(n(Y))-n(1), XU)
4635 ; Z =:= 0 ->
4636 NXL cis max(-abs(n(Y)) + n(1), XL),
4637 NXU cis min(abs(n(Y)) - n(1), XU)
4638 ; NXL cis max((n(Z)+sign(n(Z)))*n(Y)+n(1), XL),
4639 NXU cis min(n(Z)*n(Y), XU)
4640 ),
4641 update_bounds(X, XD, XPs, XL, XU, NXL, NXU)
4642 ; fd_get(Z, ZD, ZPs),
4643 domain_contract_less(XD, Y, Contracted),
4644 domains_intersection(ZD, Contracted, NZD),
4645 fd_put(Z, NZD, ZPs),
4646 ( fd_get(X, XD2, XPs2) ->
4647 domain_expand_more(NZD, Y, Expanded),
4648 domains_intersection(XD2, Expanded, NXD2),
4649 fd_put(X, NXD2, XPs2)
4650 ; true
4651 )
4652 )
4653 )
4654 ; nonvar(Z) ->
4655 fd_get(X, XD, XL, XU, XPs),
4656 fd_get(Y, _, YL, YU, _),
4657 ( YL cis_geq n(0), XL cis_geq n(0) ->
4658 NXL cis max(YL*n(Z), XL),
4659 NXU cis min(YU*(n(Z)+n(1))-n(1), XU)
4660 ; 4661 NXL = XL, NXU = XU
4662 ),
4663 update_bounds(X, XD, XPs, XL, XU, NXL, NXU)
4664 ; ( X == Y -> kill(MState), Z = 1
4665 ; fd_get(X, _, XL, XU, _),
4666 fd_get(Y, _, YL, _, _),
4667 fd_get(Z, ZD, ZPs),
4668 NZU cis max(abs(XL), XU),
4669 NZL cis -NZU,
4670 domains_intersection(ZD, from_to(NZL,NZU), NZD0),
4671 ( XL cis_geq n(0), YL cis_geq n(0) ->
4672 domain_remove_smaller_than(NZD0, 0, NZD1)
4673 ; 4674 NZD1 = NZD0
4675 ),
4676 fd_put(Z, NZD1, ZPs)
4677 )
4678 ).
4679
4680
4683
4684run_propagator(pabs(X,Y), MState) :-
4685 ( nonvar(X) -> kill(MState), Y is abs(X)
4686 ; nonvar(Y) ->
4687 kill(MState),
4688 Y >= 0,
4689 YN is -Y,
4690 X in YN \/ Y
4691 ; fd_get(X, XD, XPs),
4692 fd_get(Y, YD, _),
4693 domain_negate(YD, YDNegative),
4694 domains_union(YD, YDNegative, XD1),
4695 domains_intersection(XD, XD1, XD2),
4696 fd_put(X, XD2, XPs),
4697 ( fd_get(Y, YD1, YPs1) ->
4698 domain_negate(XD2, XD2Neg),
4699 domains_union(XD2, XD2Neg, YD2),
4700 domain_remove_smaller_than(YD2, 0, YD3),
4701 domains_intersection(YD1, YD3, YD4),
4702 fd_put(Y, YD4, YPs1)
4703 ; true
4704 )
4705 ).
4708
4709run_propagator(pmod(X,Y,Z), MState) :-
4710 ( nonvar(X) ->
4711 ( nonvar(Y) -> kill(MState), Y =\= 0, Z is X mod Y
4712 ; true
4713 )
4714 ; nonvar(Y) ->
4715 Y =\= 0,
4716 ( abs(Y) =:= 1 -> kill(MState), Z = 0
4717 ; var(Z) ->
4718 YP is abs(Y) - 1,
4719 ( Y > 0, fd_get(X, _, n(XL), n(XU), _) ->
4720 ( XL >= 0, XU < Y ->
4721 kill(MState), Z = X, ZL = XL, ZU = XU
4722 ; ZL = 0, ZU = YP
4723 )
4724 ; Y > 0 -> ZL = 0, ZU = YP
4725 ; YN is -YP, ZL = YN, ZU = 0
4726 ),
4727 ( fd_get(Z, ZD, ZPs) ->
4728 domains_intersection(ZD, from_to(n(ZL), n(ZU)), ZD1),
4729 domain_infimum(ZD1, n(ZMin)),
4730 domain_supremum(ZD1, n(ZMax)),
4731 fd_put(Z, ZD1, ZPs)
4732 ; ZMin = Z, ZMax = Z
4733 ),
4734 ( fd_get(X, XD, XPs), domain_infimum(XD, n(XMin)) ->
4735 Z1 is XMin mod Y,
4736 ( between(ZMin, ZMax, Z1) -> true
4737 ; Y > 0 ->
4738 Next is ((XMin - ZMin + Y - 1) div Y)*Y + ZMin,
4739 domain_remove_smaller_than(XD, Next, XD1),
4740 fd_put(X, XD1, XPs)
4741 ; neq_num(X, XMin)
4742 )
4743 ; true
4744 ),
4745 ( fd_get(X, XD2, XPs2), domain_supremum(XD2, n(XMax)) ->
4746 Z2 is XMax mod Y,
4747 ( between(ZMin, ZMax, Z2) -> true
4748 ; Y > 0 ->
4749 Prev is ((XMax - ZMin) div Y)*Y + ZMax,
4750 domain_remove_greater_than(XD2, Prev, XD3),
4751 fd_put(X, XD3, XPs2)
4752 ; neq_num(X, XMax)
4753 )
4754 ; true
4755 )
4756 ; fd_get(X, XD, XPs),
4757 4758 ( domain_infimum(XD, n(Min)) ->
4759 ( Min mod Y =:= Z -> true
4760 ; Y > 0 ->
4761 Next is ((Min - Z + Y - 1) div Y)*Y + Z,
4762 domain_remove_smaller_than(XD, Next, XD1),
4763 fd_put(X, XD1, XPs)
4764 ; neq_num(X, Min)
4765 )
4766 ; true
4767 ),
4768 ( fd_get(X, XD2, XPs2) ->
4769 ( domain_supremum(XD2, n(Max)) ->
4770 ( Max mod Y =:= Z -> true
4771 ; Y > 0 ->
4772 Prev is ((Max - Z) div Y)*Y + Z,
4773 domain_remove_greater_than(XD2, Prev, XD3),
4774 fd_put(X, XD3, XPs2)
4775 ; neq_num(X, Max)
4776 )
4777 ; true
4778 )
4779 ; true
4780 )
4781 )
4782 ; X == Y -> kill(MState), Z = 0
4783 ; true 4784 ).
4785
4788
4789run_propagator(prem(X,Y,Z), MState) :-
4790 ( nonvar(X) ->
4791 ( nonvar(Y) -> kill(MState), Y =\= 0, Z is X rem Y
4792 ; U is abs(X),
4793 fd_get(Y, YD, _),
4794 ( X >=0, domain_infimum(YD, n(Min)), Min >= 0 -> L = 0
4795 ; L is -U
4796 ),
4797 Z in L..U
4798 )
4799 ; nonvar(Y) ->
4800 Y =\= 0,
4801 ( abs(Y) =:= 1 -> kill(MState), Z = 0
4802 ; var(Z) ->
4803 YP is abs(Y) - 1,
4804 YN is -YP,
4805 ( Y > 0, fd_get(X, _, n(XL), n(XU), _) ->
4806 ( abs(XL) < Y, XU < Y -> kill(MState), Z = X, ZL = XL
4807 ; XL < 0, abs(XL) < Y -> ZL = XL
4808 ; XL >= 0 -> ZL = 0
4809 ; ZL = YN
4810 ),
4811 ( XU > 0, XU < Y -> ZU = XU
4812 ; XU < 0 -> ZU = 0
4813 ; ZU = YP
4814 )
4815 ; ZL = YN, ZU = YP
4816 ),
4817 ( fd_get(Z, ZD, ZPs) ->
4818 domains_intersection(ZD, from_to(n(ZL), n(ZU)), ZD1),
4819 fd_put(Z, ZD1, ZPs)
4820 ; ZD1 = from_to(n(Z), n(Z))
4821 ),
4822 ( fd_get(X, XD, _), domain_infimum(XD, n(Min)) ->
4823 Z1 is Min rem Y,
4824 ( domain_contains(ZD1, Z1) -> true
4825 ; neq_num(X, Min)
4826 )
4827 ; true
4828 ),
4829 ( fd_get(X, XD1, _), domain_supremum(XD1, n(Max)) ->
4830 Z2 is Max rem Y,
4831 ( domain_contains(ZD1, Z2) -> true
4832 ; neq_num(X, Max)
4833 )
4834 ; true
4835 )
4836 ; fd_get(X, XD1, XPs1),
4837 4838 ( domain_infimum(XD1, n(Min)) ->
4839 ( Min rem Y =:= Z -> true
4840 ; Y > 0, Min > 0 ->
4841 Next is ((Min - Z + Y - 1) div Y)*Y + Z,
4842 domain_remove_smaller_than(XD1, Next, XD2),
4843 fd_put(X, XD2, XPs1)
4844 ; 4845 neq_num(X, Min)
4846 )
4847 ; true
4848 ),
4849 ( fd_get(X, XD3, XPs3) ->
4850 ( domain_supremum(XD3, n(Max)) ->
4851 ( Max rem Y =:= Z -> true
4852 ; Y > 0, Max > 0 ->
4853 Prev is ((Max - Z) div Y)*Y + Z,
4854 domain_remove_greater_than(XD3, Prev, XD4),
4855 fd_put(X, XD4, XPs3)
4856 ; 4857 neq_num(X, Max)
4858 )
4859 ; true
4860 )
4861 ; true
4862 )
4863 )
4864 ; X == Y -> kill(MState), Z = 0
4865 ; fd_get(Z, ZD, ZPs) ->
4866 fd_get(Y, _, YInf, YSup, _),
4867 fd_get(X, _, XInf, XSup, _),
4868 M cis max(abs(YInf),YSup),
4869 ( XInf cis_geq n(0) -> Inf0 = n(0)
4870 ; Inf0 = XInf
4871 ),
4872 ( XSup cis_leq n(0) -> Sup0 = n(0)
4873 ; Sup0 = XSup
4874 ),
4875 NInf cis max(max(Inf0, -M + n(1)), min(XInf,-XSup)),
4876 NSup cis min(min(Sup0, M - n(1)), max(abs(XInf),XSup)),
4877 domains_intersection(ZD, from_to(NInf,NSup), ZD1),
4878 fd_put(Z, ZD1, ZPs)
4879 ; true 4880 ).
4881
4884
4885run_propagator(pmax(X,Y,Z), MState) :-
4886 ( nonvar(X) ->
4887 ( nonvar(Y) -> kill(MState), Z is max(X,Y)
4888 ; nonvar(Z) ->
4889 ( Z =:= X -> kill(MState), X #>= Y
4890 ; Z > X -> Z = Y
4891 ; false 4892 )
4893 ; fd_get(Y, _, YInf, YSup, _),
4894 ( YInf cis_gt n(X) -> Z = Y
4895 ; YSup cis_lt n(X) -> Z = X
4896 ; YSup = n(M) ->
4897 fd_get(Z, ZD, ZPs),
4898 domain_remove_greater_than(ZD, M, ZD1),
4899 fd_put(Z, ZD1, ZPs)
4900 ; true
4901 )
4902 )
4903 ; nonvar(Y) -> run_propagator(pmax(Y,X,Z), MState)
4904 ; fd_get(Z, ZD, ZPs) ->
4905 fd_get(X, _, XInf, XSup, _),
4906 fd_get(Y, _, YInf, YSup, _),
4907 ( YInf cis_gt YSup -> kill(MState), Z = Y
4908 ; YSup cis_lt XInf -> kill(MState), Z = X
4909 ; n(M) cis max(XSup, YSup) ->
4910 domain_remove_greater_than(ZD, M, ZD1),
4911 fd_put(Z, ZD1, ZPs)
4912 ; true
4913 )
4914 ; true
4915 ).
4916
4919
4920run_propagator(pmin(X,Y,Z), MState) :-
4921 ( nonvar(X) ->
4922 ( nonvar(Y) -> kill(MState), Z is min(X,Y)
4923 ; nonvar(Z) ->
4924 ( Z =:= X -> kill(MState), X #=< Y
4925 ; Z < X -> Z = Y
4926 ; false 4927 )
4928 ; fd_get(Y, _, YInf, YSup, _),
4929 ( YSup cis_lt n(X) -> Z = Y
4930 ; YInf cis_gt n(X) -> Z = X
4931 ; YInf = n(M) ->
4932 fd_get(Z, ZD, ZPs),
4933 domain_remove_smaller_than(ZD, M, ZD1),
4934 fd_put(Z, ZD1, ZPs)
4935 ; true
4936 )
4937 )
4938 ; nonvar(Y) -> run_propagator(pmin(Y,X,Z), MState)
4939 ; fd_get(Z, ZD, ZPs) ->
4940 fd_get(X, _, XInf, XSup, _),
4941 fd_get(Y, _, YInf, YSup, _),
4942 ( YSup cis_lt YInf -> kill(MState), Z = Y
4943 ; YInf cis_gt XSup -> kill(MState), Z = X
4944 ; n(M) cis min(XInf, YInf) ->
4945 domain_remove_smaller_than(ZD, M, ZD1),
4946 fd_put(Z, ZD1, ZPs)
4947 ; true
4948 )
4949 ; true
4950 ).
4953
4954run_propagator(pexp(X,Y,Z), MState) :-
4955 ( X == 1 -> kill(MState), Z = 1
4956 ; X == 0 -> kill(MState), Z in 0..1, Z #<==> Y #= 0
4957 ; Y == 0 -> kill(MState), Z = 1
4958 ; Y == 1 -> kill(MState), Z = X
4959 ; nonvar(X) ->
4960 ( nonvar(Y) ->
4961 ( Y >= 0 -> true ; X =:= -1 ),
4962 kill(MState),
4963 Z is X^Y
4964 ; nonvar(Z) ->
4965 ( Z > 1 ->
4966 kill(MState),
4967 integer_log_b(Z, X, 1, Y)
4968 ; true
4969 )
4970 ; fd_get(Y, _, YL, YU, _),
4971 fd_get(Z, ZD, ZPs),
4972 ( X > 0, YL cis_geq n(0) ->
4973 NZL cis n(X)^YL,
4974 NZU cis n(X)^YU,
4975 domains_intersection(ZD, from_to(NZL,NZU), NZD),
4976 fd_put(Z, NZD, ZPs)
4977 ; true
4978 ),
4979 ( X > 0,
4980 fd_get(Z, _, _, n(ZMax), _),
4981 ZMax > 0 ->
4982 floor_integer_log_b(ZMax, X, 1, YCeil),
4983 Y in inf..YCeil
4984 ; true
4985 )
4986 )
4987 ; nonvar(Z) ->
4988 ( nonvar(Y) ->
4989 integer_kth_root(Z, Y, R),
4990 kill(MState),
4991 ( even(Y) ->
4992 N is -R,
4993 X in N \/ R
4994 ; X = R
4995 )
4996 ; fd_get(X, _, n(NXL), _, _), NXL > 1 ->
4997 ( Z > 1, between(NXL, Z, Exp), NXL^Exp > Z ->
4998 Exp1 is Exp - 1,
4999 fd_get(Y, YD, YPs),
5000 domains_intersection(YD, from_to(n(1),n(Exp1)), YD1),
5001 fd_put(Y, YD1, YPs),
5002 ( fd_get(X, XD, XPs) ->
5003 domain_infimum(YD1, n(YL)),
5004 integer_kth_root_leq(Z, YL, RU),
5005 domains_intersection(XD, from_to(n(NXL),n(RU)), XD1),
5006 fd_put(X, XD1, XPs)
5007 ; true
5008 )
5009 ; true
5010 )
5011 ; true
5012 )
5013 ; nonvar(Y), Y > 0 ->
5014 ( even(Y) ->
5015 geq(Z, 0)
5016 ; true
5017 ),
5018 ( fd_get(X, XD, XL, XU, _), fd_get(Z, ZD, ZL, ZU, ZPs) ->
5019 ( domain_contains(ZD, 0) -> XD1 = XD
5020 ; domain_remove(XD, 0, XD1)
5021 ),
5022 ( domain_contains(XD, 0) -> ZD1 = ZD
5023 ; domain_remove(ZD, 0, ZD1)
5024 ),
5025 ( even(Y) ->
5026 ( XL cis_geq n(0) ->
5027 NZL cis XL^n(Y)
5028 ; XU cis_leq n(0) ->
5029 NZL cis XU^n(Y)
5030 ; NZL = n(0)
5031 ),
5032 NZU cis max(abs(XL),abs(XU))^n(Y),
5033 domains_intersection(ZD1, from_to(NZL,NZU), ZD2)
5034 ; ( finite(XL) ->
5035 NZL cis XL^n(Y),
5036 NZU cis XU^n(Y),
5037 domains_intersection(ZD1, from_to(NZL,NZU), ZD2)
5038 ; ZD2 = ZD1
5039 )
5040 ),
5041 fd_put(Z, ZD2, ZPs),
5042 ( even(Y), ZU = n(Num) ->
5043 integer_kth_root_leq(Num, Y, RU),
5044 ( XL cis_geq n(0), ZL = n(Num1) ->
5045 integer_kth_root_leq(Num1, Y, RL0),
5046 ( RL0^Y < Num1 -> RL is RL0 + 1
5047 ; RL = RL0
5048 )
5049 ; RL is -RU
5050 ),
5051 RL =< RU,
5052 NXD = from_to(n(RL),n(RU))
5053 ; odd(Y), ZL cis_geq n(0), ZU = n(Num) ->
5054 integer_kth_root_leq(Num, Y, RU),
5055 ZL = n(Num1),
5056 integer_kth_root_leq(Num1, Y, RL0),
5057 ( RL0^Y < Num1 -> RL is RL0 + 1
5058 ; RL = RL0
5059 ),
5060 RL =< RU,
5061 NXD = from_to(n(RL),n(RU))
5062 ; NXD = XD1 5063 ),
5064 ( fd_get(X, XD2, XPs) ->
5065 domains_intersection(XD2, XD1, XD3),
5066 domains_intersection(XD3, NXD, XD4),
5067 fd_put(X, XD4, XPs)
5068 ; true
5069 )
5070 ; true
5071 )
5072 ; fd_get(X, _, XL, _, _),
5073 XL cis_gt n(0),
5074 fd_get(Y, _, YL, _, _),
5075 YL cis_gt n(0),
5076 fd_get(Z, ZD, ZPs) ->
5077 n(NZL) cis XL^YL,
5078 domain_remove_smaller_than(ZD, NZL, ZD1),
5079 fd_put(Z, ZD1, ZPs)
5080 ; true
5081 ).
5082
5084run_propagator(pzcompare(Order, A, B), MState) :-
5085 ( A == B -> kill(MState), Order = (=)
5086 ; ( nonvar(A) ->
5087 ( nonvar(B) ->
5088 kill(MState),
5089 ( A > B -> Order = (>)
5090 ; Order = (<)
5091 )
5092 ; fd_get(B, _, BL, BU, _),
5093 ( BL cis_gt n(A) -> kill(MState), Order = (<)
5094 ; BU cis_lt n(A) -> kill(MState), Order = (>)
5095 ; true
5096 )
5097 )
5098 ; nonvar(B) ->
5099 fd_get(A, _, AL, AU, _),
5100 ( AL cis_gt n(B) -> kill(MState), Order = (>)
5101 ; AU cis_lt n(B) -> kill(MState), Order = (<)
5102 ; true
5103 )
5104 ; fd_get(A, _, AL, AU, _),
5105 fd_get(B, _, BL, BU, _),
5106 ( AL cis_gt BU -> kill(MState), Order = (>)
5107 ; AU cis_lt BL -> kill(MState), Order = (<)
5108 ; true
5109 )
5110 )
5111 ).
5112
5114
5116
5118
5119run_propagator(reified_in(V,Dom,B), MState) :-
5120 ( integer(V) ->
5121 kill(MState),
5122 ( domain_contains(Dom, V) -> B = 1
5123 ; B = 0
5124 )
5125 ; B == 1 -> kill(MState), domain(V, Dom)
5126 ; B == 0 -> kill(MState), domain_complement(Dom, C), domain(V, C)
5127 ; fd_get(V, VD, _),
5128 ( domains_intersection(VD, Dom, I) ->
5129 ( I == VD -> kill(MState), B = 1
5130 ; true
5131 )
5132 ; kill(MState), B = 0
5133 )
5134 ).
5135
5136run_propagator(reified_tuple_in(Tuple, R, B), MState) :-
5137 get_attr(R, clpfd_relation, Relation),
5138 ( B == 1 -> kill(MState), tuples_in([Tuple], Relation)
5139 ; ( ground(Tuple) ->
5140 kill(MState),
5141 ( memberchk(Tuple, Relation) -> B = 1
5142 ; B = 0
5143 )
5144 ; relation_unifiable(Relation, Tuple, Us, _, _),
5145 ( Us = [] -> kill(MState), B = 0
5146 ; true
5147 )
5148 )
5149 ).
5150
5151run_propagator(tuples_not_in(Tuples, Relation, B), MState) :-
5152 ( B == 0 ->
5153 kill(MState),
5154 tuples_in_conjunction(Tuples, Relation, Conj),
5155 #\ Conj
5156 ; true
5157 ).
5158
5159run_propagator(kill_reified_tuples(B, Ps, Bs), _) :-
5160 ( B == 0 ->
5161 maplist(kill_entailed, Ps),
5162 phrase(as(Bs), As),
5163 maplist(kill_entailed, As)
5164 ; true
5165 ).
5166
5167run_propagator(reified_fd(V,B), MState) :-
5168 ( fd_inf(V, I), I \== inf, fd_sup(V, S), S \== sup ->
5169 kill(MState),
5170 B = 1
5171 ; B == 0 ->
5172 ( fd_inf(V, inf) -> true
5173 ; fd_sup(V, sup) -> true
5174 ; false
5175 )
5176 ; true
5177 ).
5178
5180
5181run_propagator(pskeleton(X,Y,D,Skel,Z,_), MState) :-
5182 ( Y == 0 -> kill(MState), D = 0
5183 ; D == 1 -> kill(MState), neq_num(Y, 0), skeleton([X,Y,Z], Skel)
5184 ; integer(Y), Y =\= 0 -> kill(MState), D = 1, skeleton([X,Y,Z], Skel)
5185 ; fd_get(Y, YD, _), \+ domain_contains(YD, 0) ->
5186 kill(MState),
5187 D = 1, skeleton([X,Y,Z], Skel)
5188 ; true
5189 ).
5190
5195
5196run_propagator(pfunction(Op,A,B,R), MState) :-
5197 ( integer(A), integer(B) ->
5198 kill(MState),
5199 Expr =.. [Op,A,B],
5200 R is Expr
5201 ; true
5202 ).
5203run_propagator(pfunction(Op,A,R), MState) :-
5204 ( integer(A) ->
5205 kill(MState),
5206 Expr =.. [Op,A],
5207 R is Expr
5208 ; true
5209 ).
5210
5212
5213run_propagator(reified_geq(DX,X,DY,Y,Ps,B), MState) :-
5214 ( DX == 0 -> kill(MState, Ps), B = 0
5215 ; DY == 0 -> kill(MState, Ps), B = 0
5216 ; B == 1 -> kill(MState), DX = 1, DY = 1, geq(X, Y)
5217 ; DX == 1, DY == 1 ->
5218 ( var(B) ->
5219 ( nonvar(X) ->
5220 ( nonvar(Y) ->
5221 kill(MState),
5222 ( X >= Y -> B = 1 ; B = 0 )
5223 ; fd_get(Y, _, YL, YU, _),
5224 ( n(X) cis_geq YU -> kill(MState, Ps), B = 1
5225 ; n(X) cis_lt YL -> kill(MState, Ps), B = 0
5226 ; true
5227 )
5228 )
5229 ; nonvar(Y) ->
5230 fd_get(X, _, XL, XU, _),
5231 ( XL cis_geq n(Y) -> kill(MState, Ps), B = 1
5232 ; XU cis_lt n(Y) -> kill(MState, Ps), B = 0
5233 ; true
5234 )
5235 ; X == Y -> kill(MState, Ps), B = 1
5236 ; fd_get(X, _, XL, XU, _),
5237 fd_get(Y, _, YL, YU, _),
5238 ( XL cis_geq YU -> kill(MState, Ps), B = 1
5239 ; XU cis_lt YL -> kill(MState, Ps), B = 0
5240 ; true
5241 )
5242 )
5243 ; B =:= 0 -> kill(MState), X #< Y
5244 ; true
5245 )
5246 ; true
5247 ).
5248
5250run_propagator(reified_eq(DX,X,DY,Y,Ps,B), MState) :-
5251 ( DX == 0 -> kill(MState, Ps), B = 0
5252 ; DY == 0 -> kill(MState, Ps), B = 0
5253 ; B == 1 -> kill(MState), DX = 1, DY = 1, X = Y
5254 ; DX == 1, DY == 1 ->
5255 ( var(B) ->
5256 ( nonvar(X) ->
5257 ( nonvar(Y) ->
5258 kill(MState),
5259 ( X =:= Y -> B = 1 ; B = 0)
5260 ; fd_get(Y, YD, _),
5261 ( domain_contains(YD, X) -> true
5262 ; kill(MState, Ps), B = 0
5263 )
5264 )
5265 ; nonvar(Y) -> run_propagator(reified_eq(DY,Y,DX,X,Ps,B), MState)
5266 ; X == Y -> kill(MState), B = 1
5267 ; fd_get(X, _, XL, XU, _),
5268 fd_get(Y, _, YL, YU, _),
5269 ( XL cis_gt YU -> kill(MState, Ps), B = 0
5270 ; YL cis_gt XU -> kill(MState, Ps), B = 0
5271 ; true
5272 )
5273 )
5274 ; B =:= 0 -> kill(MState), X #\= Y
5275 ; true
5276 )
5277 ; true
5278 ).
5280run_propagator(reified_neq(DX,X,DY,Y,Ps,B), MState) :-
5281 ( DX == 0 -> kill(MState, Ps), B = 0
5282 ; DY == 0 -> kill(MState, Ps), B = 0
5283 ; B == 1 -> kill(MState), DX = 1, DY = 1, X #\= Y
5284 ; DX == 1, DY == 1 ->
5285 ( var(B) ->
5286 ( nonvar(X) ->
5287 ( nonvar(Y) ->
5288 kill(MState),
5289 ( X =\= Y -> B = 1 ; B = 0)
5290 ; fd_get(Y, YD, _),
5291 ( domain_contains(YD, X) -> true
5292 ; kill(MState, Ps), B = 1
5293 )
5294 )
5295 ; nonvar(Y) -> run_propagator(reified_neq(DY,Y,DX,X,Ps,B), MState)
5296 ; X == Y -> kill(MState), B = 0
5297 ; fd_get(X, _, XL, XU, _),
5298 fd_get(Y, _, YL, YU, _),
5299 ( XL cis_gt YU -> kill(MState, Ps), B = 1
5300 ; YL cis_gt XU -> kill(MState, Ps), B = 1
5301 ; true
5302 )
5303 )
5304 ; B =:= 0 -> kill(MState), X = Y
5305 ; true
5306 )
5307 ; true
5308 ).
5310run_propagator(reified_and(X,Ps1,Y,Ps2,B), MState) :-
5311 ( nonvar(X) ->
5312 kill(MState),
5313 ( X =:= 0 -> maplist(kill_entailed, Ps2), B = 0
5314 ; B = Y
5315 )
5316 ; nonvar(Y) -> run_propagator(reified_and(Y,Ps2,X,Ps1,B), MState)
5317 ; B == 1 -> kill(MState), X = 1, Y = 1
5318 ; true
5319 ).
5320
5322run_propagator(reified_or(X,Ps1,Y,Ps2,B), MState) :-
5323 ( nonvar(X) ->
5324 kill(MState),
5325 ( X =:= 1 -> maplist(kill_entailed, Ps2), B = 1
5326 ; B = Y
5327 )
5328 ; nonvar(Y) -> run_propagator(reified_or(Y,Ps2,X,Ps1,B), MState)
5329 ; B == 0 -> kill(MState), X = 0, Y = 0
5330 ; true
5331 ).
5332
5334run_propagator(reified_not(X,Y), MState) :-
5335 ( X == 0 -> kill(MState), Y = 1
5336 ; X == 1 -> kill(MState), Y = 0
5337 ; Y == 0 -> kill(MState), X = 1
5338 ; Y == 1 -> kill(MState), X = 0
5339 ; true
5340 ).
5341
5343run_propagator(pimpl(X, Y, Ps), MState) :-
5344 ( nonvar(X) ->
5345 kill(MState),
5346 ( X =:= 1 -> Y = 1
5347 ; maplist(kill_entailed, Ps)
5348 )
5349 ; nonvar(Y) ->
5350 kill(MState),
5351 ( Y =:= 0 -> X = 0
5352 ; maplist(kill_entailed, Ps)
5353 )
5354 ; true
5355 ).
5356
5359
5360update_bounds(X, XD, XPs, XL, XU, NXL, NXU) :-
5361 ( NXL == XL, NXU == XU -> true
5362 ; domains_intersection(XD, from_to(NXL, NXU), NXD),
5363 fd_put(X, NXD, XPs)
5364 ).
5365
5366min_product(L1, U1, L2, U2, Min) :-
5367 Min cis min(min(L1*L2,L1*U2),min(U1*L2,U1*U2)).
5368max_product(L1, U1, L2, U2, Max) :-
5369 Max cis max(max(L1*L2,L1*U2),max(U1*L2,U1*U2)).
5370
5371finite(n(_)).
5372
5373in_(L, U, X) :-
5374 fd_get(X, XD, XPs),
5375 domains_intersection(XD, from_to(L,U), NXD),
5376 fd_put(X, NXD, XPs).
5377
5378min_max_factor(L1, U1, L2, U2, L3, U3, Min, Max) :-
5379 ( U1 cis_lt n(0),
5380 L2 cis_lt n(0), U2 cis_gt n(0),
5381 L3 cis_lt n(0), U3 cis_gt n(0) ->
5382 maplist(in_(L1,U1), [Z1,Z2]),
5383 in_(L2, n(-1), X1), in_(n(1), U3, Y1),
5384 ( X1*Y1 #= Z1 ->
5385 ( fd_get(Y1, _, Inf1, Sup1, _) -> true
5386 ; Inf1 = n(Y1), Sup1 = n(Y1)
5387 )
5388 ; Inf1 = inf, Sup1 = n(-1)
5389 ),
5390 in_(n(1), U2, X2), in_(L3, n(-1), Y2),
5391 ( X2*Y2 #= Z2 ->
5392 ( fd_get(Y2, _, Inf2, Sup2, _) -> true
5393 ; Inf2 = n(Y2), Sup2 = n(Y2)
5394 )
5395 ; Inf2 = n(1), Sup2 = sup
5396 ),
5397 Min cis max(min(Inf1,Inf2), L3),
5398 Max cis min(max(Sup1,Sup2), U3)
5399 ; L1 cis_gt n(0),
5400 L2 cis_lt n(0), U2 cis_gt n(0),
5401 L3 cis_lt n(0), U3 cis_gt n(0) ->
5402 maplist(in_(L1,U1), [Z1,Z2]),
5403 in_(L2, n(-1), X1), in_(L3, n(-1), Y1),
5404 ( X1*Y1 #= Z1 ->
5405 ( fd_get(Y1, _, Inf1, Sup1, _) -> true
5406 ; Inf1 = n(Y1), Sup1 = n(Y1)
5407 )
5408 ; Inf1 = n(1), Sup1 = sup
5409 ),
5410 in_(n(1), U2, X2), in_(n(1), U3, Y2),
5411 ( X2*Y2 #= Z2 ->
5412 ( fd_get(Y2, _, Inf2, Sup2, _) -> true
5413 ; Inf2 = n(Y2), Sup2 = n(Y2)
5414 )
5415 ; Inf2 = inf, Sup2 = n(-1)
5416 ),
5417 Min cis max(min(Inf1,Inf2), L3),
5418 Max cis min(max(Sup1,Sup2), U3)
5419 ; min_factor(L1, U1, L2, U2, Min0),
5420 Min cis max(L3,Min0),
5421 max_factor(L1, U1, L2, U2, Max0),
5422 Max cis min(U3,Max0)
5423 ).
5424
5425min_factor(L1, U1, L2, U2, Min) :-
5426 ( L1 cis_geq n(0), L2 cis_gt n(0), finite(U2) ->
5427 Min cis div(L1+U2-n(1),U2)
5428 ; L1 cis_gt n(0), U2 cis_lt n(0) -> Min cis div(U1,U2)
5429 ; L1 cis_gt n(0), L2 cis_geq n(0) -> Min = n(1)
5430 ; L1 cis_gt n(0) -> Min cis -U1
5431 ; U1 cis_lt n(0), U2 cis_leq n(0) ->
5432 ( finite(L2) -> Min cis div(U1+L2+n(1),L2)
5433 ; Min = n(1)
5434 )
5435 ; U1 cis_lt n(0), L2 cis_geq n(0) -> Min cis div(L1,L2)
5436 ; U1 cis_lt n(0) -> Min = L1
5437 ; L2 cis_leq n(0), U2 cis_geq n(0) -> Min = inf
5438 ; Min cis min(min(div(L1,L2),div(L1,U2)),min(div(U1,L2),div(U1,U2)))
5439 ).
5440max_factor(L1, U1, L2, U2, Max) :-
5441 ( L1 cis_geq n(0), L2 cis_geq n(0) -> Max cis div(U1,L2)
5442 ; L1 cis_gt n(0), U2 cis_leq n(0) ->
5443 ( finite(L2) -> Max cis div(L1-L2-n(1),L2)
5444 ; Max = n(-1)
5445 )
5446 ; L1 cis_gt n(0) -> Max = U1
5447 ; U1 cis_lt n(0), U2 cis_lt n(0) -> Max cis div(L1,U2)
5448 ; U1 cis_lt n(0), L2 cis_geq n(0) ->
5449 ( finite(U2) -> Max cis div(U1-U2+n(1),U2)
5450 ; Max = n(-1)
5451 )
5452 ; U1 cis_lt n(0) -> Max cis -L1
5453 ; L2 cis_leq n(0), U2 cis_geq n(0) -> Max = sup
5454 ; Max cis max(max(div(L1,L2),div(L1,U2)),max(div(U1,L2),div(U1,U2)))
5455 ).
5456
5462
5463distinct_attach([], _, _).
5464distinct_attach([X|Xs], Prop, Right) :-
5465 ( var(X) ->
5466 init_propagator(X, Prop),
5467 make_propagator(pexclude(Xs,Right,X), P1),
5468 init_propagator(X, P1),
5469 trigger_prop(P1)
5470 ; exclude_fire(Xs, Right, X)
5471 ),
5472 distinct_attach(Xs, Prop, [X|Right]).
5473
5488
5489difference_arcs(Vars, FreeLeft, FreeRight) :-
5490 empty_assoc(E),
5491 phrase(difference_arcs(Vars, FreeLeft), [E], [NumVar]),
5492 assoc_to_list(NumVar, LsNumVar),
5493 pairs_values(LsNumVar, FreeRight).
5494
5495domain_to_list(Domain, List) :- phrase(domain_to_list(Domain), List).
5496
5497domain_to_list(split(_, Left, Right)) -->
5498 domain_to_list(Left), domain_to_list(Right).
5499domain_to_list(empty) --> [].
5500domain_to_list(from_to(n(F),n(T))) --> { numlist(F, T, Ns) }, list(Ns).
5501
5502difference_arcs([], []) --> [].
5503difference_arcs([V|Vs], FL0) -->
5504 ( { fd_get(V, Dom, _),
5505 finite_domain(Dom) } ->
5506 { FL0 = [V|FL],
5507 domain_to_list(Dom, Ns) },
5508 enumerate(Ns, V),
5509 difference_arcs(Vs, FL)
5510 ; difference_arcs(Vs, FL0)
5511 ).
5512
5513enumerate([], _) --> [].
5514enumerate([N|Ns], V) -->
5515 state(NumVar0, NumVar),
5516 { ( get_assoc(N, NumVar0, Y) -> NumVar0 = NumVar
5517 ; put_assoc(N, NumVar0, Y, NumVar),
5518 put_attr(Y, value, N)
5519 ),
5520 put_attr(F, flow, 0),
5521 append_edge(Y, edges, flow_from(F,V)),
5522 append_edge(V, edges, flow_to(F,Y)) },
5523 enumerate(Ns, V).
5524
5525append_edge(V, Attr, E) :-
5526 ( get_attr(V, Attr, Es) ->
5527 put_attr(V, Attr, [E|Es])
5528 ; put_attr(V, Attr, [E])
5529 ).
5530
5535
5536clear_parent(V) :- del_attr(V, parent).
5537
5538maximum_matching([]).
5539maximum_matching([FL|FLs]) :-
5540 augmenting_path_to([[FL]], Levels, To),
5541 phrase(augmenting_path(FL, To), Path),
5542 maplist(maplist(clear_parent), Levels),
5543 del_attr(To, free),
5544 adjust_alternate_1(Path),
5545 maximum_matching(FLs).
5546
5547reachables([]) --> [].
5548reachables([V|Vs]) -->
5549 { get_attr(V, edges, Es) },
5550 reachables_(Es, V),
5551 reachables(Vs).
5552
5553reachables_([], _) --> [].
5554reachables_([E|Es], V) -->
5555 edge_reachable(E, V),
5556 reachables_(Es, V).
5557
5558edge_reachable(flow_to(F,To), V) -->
5559 ( { get_attr(F, flow, 0),
5560 \+ get_attr(To, parent, _) } ->
5561 { put_attr(To, parent, V-F) },
5562 [To]
5563 ; []
5564 ).
5565edge_reachable(flow_from(F,From), V) -->
5566 ( { get_attr(F, flow, 1),
5567 \+ get_attr(From, parent, _) } ->
5568 { put_attr(From, parent, V-F) },
5569 [From]
5570 ; []
5571 ).
5572
5573augmenting_path_to(Levels0, Levels, Right) :-
5574 Levels0 = [Vs|_],
5575 Levels1 = [Tos|Levels0],
5576 phrase(reachables(Vs), Tos),
5577 Tos = [_|_],
5578 ( member(Right, Tos), get_attr(Right, free, true) ->
5579 Levels = Levels1
5580 ; augmenting_path_to(Levels1, Levels, Right)
5581 ).
5582
5583augmenting_path(S, V) -->
5584 ( { V == S } -> []
5585 ; { get_attr(V, parent, V1-Augment) },
5586 [Augment],
5587 augmenting_path(S, V1)
5588 ).
5589
5590adjust_alternate_1([A|Arcs]) :-
5591 put_attr(A, flow, 1),
5592 adjust_alternate_0(Arcs).
5593
5594adjust_alternate_0([]).
5595adjust_alternate_0([A|Arcs]) :-
5596 put_attr(A, flow, 0),
5597 adjust_alternate_1(Arcs).
5598
5602
5603g_g0(V) :-
5604 get_attr(V, edges, Es),
5605 maplist(g_g0_(V), Es).
5606
5607g_g0_(V, flow_to(F,To)) :-
5608 ( get_attr(F, flow, 1) ->
5609 append_edge(V, g0_edges, flow_to(F,To))
5610 ; append_edge(To, g0_edges, flow_to(F,V))
5611 ).
5612
5613
5614g0_successors(V, Tos) :-
5615 ( get_attr(V, g0_edges, Tos0) ->
5616 maplist(arg(2), Tos0, Tos)
5617 ; Tos = []
5618 ).
5619
5620put_free(F) :- put_attr(F, free, true).
5621
5622free_node(F) :- get_attr(F, free, true).
5623
5624del_vars_attr(Vars, Attr) :- maplist(del_attr_(Attr), Vars).
5625
5626del_attr_(Attr, Var) :- del_attr(Var, Attr).
5627
5628with_local_attributes(Vars, Attrs, Goal, Result) :-
5629 catch((maplist(del_vars_attr(Vars), Attrs),
5630 Goal,
5631 maplist(del_attrs, Vars),
5632 5633 throw(local_attributes(Result,Vars))),
5634 local_attributes(Result,Vars),
5635 true).
5636
5637distinct(Vars) :-
5638 with_local_attributes(Vars, [edges,parent,g0_edges,index,visited],
5639 (difference_arcs(Vars, FreeLeft, FreeRight0),
5640 length(FreeLeft, LFL),
5641 length(FreeRight0, LFR),
5642 LFL =< LFR,
5643 maplist(put_free, FreeRight0),
5644 maximum_matching(FreeLeft),
5645 include(free_node, FreeRight0, FreeRight),
5646 maplist(g_g0, FreeLeft),
5647 scc(FreeLeft, g0_successors),
5648 maplist(dfs_used, FreeRight),
5649 phrase(distinct_goals(FreeLeft), Gs)), Gs),
5650 disable_queue,
5651 maplist(call, Gs),
5652 enable_queue.
5653
5654distinct_goals([]) --> [].
5655distinct_goals([V|Vs]) -->
5656 { get_attr(V, edges, Es) },
5657 distinct_goals_(Es, V),
5658 distinct_goals(Vs).
5659
5660distinct_goals_([], _) --> [].
5661distinct_goals_([flow_to(F,To)|Es], V) -->
5662 ( { get_attr(F, flow, 0),
5663 \+ get_attr(F, used, true),
5664 get_attr(V, lowlink, L1),
5665 get_attr(To, lowlink, L2),
5666 L1 =\= L2 } ->
5667 { get_attr(To, value, N) },
5668 [neq_num(V, N)]
5669 ; []
5670 ),
5671 distinct_goals_(Es, V).
5672
5676
5677dfs_used(V) :-
5678 ( get_attr(V, visited, true) -> true
5679 ; put_attr(V, visited, true),
5680 ( get_attr(V, g0_edges, Es) ->
5681 dfs_used_edges(Es)
5682 ; true
5683 )
5684 ).
5685
5686dfs_used_edges([]).
5687dfs_used_edges([flow_to(F,To)|Es]) :-
5688 put_attr(F, used, true),
5689 dfs_used(To),
5690 dfs_used_edges(Es).
5691
5708
5709scc(Vs, Succ) :- phrase(scc(Vs), [s(0,[],Succ)], _).
5710
5711scc([]) --> [].
5712scc([V|Vs]) -->
5713 ( vindex_defined(V) -> scc(Vs)
5714 ; scc_(V), scc(Vs)
5715 ).
5716
5717vindex_defined(V) --> { get_attr(V, index, _) }.
5718
5719vindex_is_index(V) -->
5720 state(s(Index,_,_)),
5721 { put_attr(V, index, Index) }.
5722
5723vlowlink_is_index(V) -->
5724 state(s(Index,_,_)),
5725 { put_attr(V, lowlink, Index) }.
5726
5727index_plus_one -->
5728 state(s(I,Stack,Succ), s(I1,Stack,Succ)),
5729 { I1 is I+1 }.
5730
5731s_push(V) -->
5732 state(s(I,Stack,Succ), s(I,[V|Stack],Succ)),
5733 { put_attr(V, in_stack, true) }.
5734
5735vlowlink_min_lowlink(V, VP) -->
5736 { get_attr(V, lowlink, VL),
5737 get_attr(VP, lowlink, VPL),
5738 VL1 is min(VL, VPL),
5739 put_attr(V, lowlink, VL1) }.
5740
5741successors(V, Tos) --> state(s(_,_,Succ)), { call(Succ, V, Tos) }.
5742
5743scc_(V) -->
5744 vindex_is_index(V),
5745 vlowlink_is_index(V),
5746 index_plus_one,
5747 s_push(V),
5748 successors(V, Tos),
5749 each_edge(Tos, V),
5750 ( { get_attr(V, index, VI),
5751 get_attr(V, lowlink, VI) } -> pop_stack_to(V, VI)
5752 ; []
5753 ).
5754
5755pop_stack_to(V, N) -->
5756 state(s(I,[First|Stack],Succ), s(I,Stack,Succ)),
5757 { del_attr(First, in_stack) },
5758 ( { First == V } -> []
5759 ; { put_attr(First, lowlink, N) },
5760 pop_stack_to(V, N)
5761 ).
5762
5763each_edge([], _) --> [].
5764each_edge([VP|VPs], V) -->
5765 ( vindex_defined(VP) ->
5766 ( v_in_stack(VP) ->
5767 vlowlink_min_lowlink(V, VP)
5768 ; []
5769 )
5770 ; scc_(VP),
5771 vlowlink_min_lowlink(V, VP)
5772 ),
5773 each_edge(VPs, V).
5774
5775state(S), [S] --> [S].
5776
5777state(S0, S), [S] --> [S0].
5778
5779v_in_stack(V) --> { get_attr(V, in_stack, true) }.
5780
5789
5790weak_arc_all_distinct(Ls) :-
5791 must_be(list, Ls),
5792 Orig = original_goal(_, weak_arc_all_distinct(Ls)),
5793 all_distinct(Ls, [], Orig),
5794 do_queue.
5795
5796all_distinct([], _, _).
5797all_distinct([X|Right], Left, Orig) :-
5798 5799 ( var(X) ->
5800 make_propagator(weak_distinct(Left,Right,X,Orig), Prop),
5801 init_propagator(X, Prop),
5802 trigger_prop(Prop)
5806 ; exclude_fire(Left, Right, X)
5807 ),
5808 outof_reducer(Left, Right, X),
5809 all_distinct(Right, [X|Left], Orig).
5810
5811exclude_fire(Left, Right, E) :-
5812 all_neq(Left, E),
5813 all_neq(Right, E).
5814
5815list_contains([X|Xs], Y) :-
5816 ( X == Y -> true
5817 ; list_contains(Xs, Y)
5818 ).
5819
5820kill_if_isolated(Left, Right, X, MState) :-
5821 append(Left, Right, Others),
5822 fd_get(X, XDom, _),
5823 ( all_empty_intersection(Others, XDom) -> kill(MState)
5824 ; true
5825 ).
5826
5827all_empty_intersection([], _).
5828all_empty_intersection([V|Vs], XDom) :-
5829 ( fd_get(V, VDom, _) ->
5830 domains_intersection_(VDom, XDom, empty),
5831 all_empty_intersection(Vs, XDom)
5832 ; all_empty_intersection(Vs, XDom)
5833 ).
5834
5835outof_reducer(Left, Right, Var) :-
5836 ( fd_get(Var, Dom, _) ->
5837 append(Left, Right, Others),
5838 domain_num_elements(Dom, N),
5839 num_subsets(Others, Dom, 0, Num, NonSubs),
5840 ( n(Num) cis_geq N -> false
5841 ; n(Num) cis N - n(1) ->
5842 reduce_from_others(NonSubs, Dom)
5843 ; true
5844 )
5845 ; 5846 5847 true
5848 ).
5849
5850reduce_from_others([], _).
5851reduce_from_others([X|Xs], Dom) :-
5852 ( fd_get(X, XDom, XPs) ->
5853 domain_subtract(XDom, Dom, NXDom),
5854 fd_put(X, NXDom, XPs)
5855 ; true
5856 ),
5857 reduce_from_others(Xs, Dom).
5858
5859num_subsets([], _Dom, Num, Num, []).
5860num_subsets([S|Ss], Dom, Num0, Num, NonSubs) :-
5861 ( fd_get(S, SDom, _) ->
5862 ( domain_subdomain(Dom, SDom) ->
5863 Num1 is Num0 + 1,
5864 num_subsets(Ss, Dom, Num1, Num, NonSubs)
5865 ; NonSubs = [S|Rest],
5866 num_subsets(Ss, Dom, Num0, Num, Rest)
5867 )
5868 ; num_subsets(Ss, Dom, Num0, Num, NonSubs)
5869 ).
5870
5872
5894
5895serialized(Starts, Durations) :-
5896 must_be(list(integer), Durations),
5897 pairs_keys_values(SDs, Starts, Durations),
5898 Orig = original_goal(_, serialized(Starts, Durations)),
5899 serialize(SDs, Orig).
5900
5901serialize([], _).
5902serialize([S-D|SDs], Orig) :-
5903 D >= 0,
5904 serialize(SDs, S, D, Orig),
5905 serialize(SDs, Orig).
5906
5907serialize([], _, _, _).
5908serialize([S-D|Rest], S0, D0, Orig) :-
5909 D >= 0,
5910 propagator_init_trigger([S0,S], pserialized(S,D,S0,D0,Orig)),
5911 serialize(Rest, S0, D0, Orig).
5912
5915
5916earliest_start_time(Start, EST) :-
5917 ( fd_get(Start, D, _) ->
5918 domain_infimum(D, EST)
5919 ; EST = n(Start)
5920 ).
5921
5922latest_start_time(Start, LST) :-
5923 ( fd_get(Start, D, _) ->
5924 domain_supremum(D, LST)
5925 ; LST = n(Start)
5926 ).
5927
5928serialize_lower_upper(S_I, D_I, S_J, D_J, MState) :-
5929 ( var(S_I) ->
5930 serialize_lower_bound(S_I, D_I, S_J, D_J, MState),
5931 ( var(S_I) -> serialize_upper_bound(S_I, D_I, S_J, D_J, MState)
5932 ; true
5933 )
5934 ; true
5935 ).
5936
5937serialize_lower_bound(I, D_I, J, D_J, MState) :-
5938 fd_get(I, DomI, Ps),
5939 ( domain_infimum(DomI, n(EST_I)),
5940 latest_start_time(J, n(LST_J)),
5941 EST_I + D_I > LST_J,
5942 earliest_start_time(J, n(EST_J)) ->
5943 ( nonvar(J) -> kill(MState)
5944 ; true
5945 ),
5946 EST is EST_J+D_J,
5947 domain_remove_smaller_than(DomI, EST, DomI1),
5948 fd_put(I, DomI1, Ps)
5949 ; true
5950 ).
5951
5952serialize_upper_bound(I, D_I, J, D_J, MState) :-
5953 fd_get(I, DomI, Ps),
5954 ( domain_supremum(DomI, n(LST_I)),
5955 earliest_start_time(J, n(EST_J)),
5956 EST_J + D_J > LST_I,
5957 latest_start_time(J, n(LST_J)) ->
5958 ( nonvar(J) -> kill(MState)
5959 ; true
5960 ),
5961 LST is LST_J-D_I,
5962 domain_remove_greater_than(DomI, LST, DomI1),
5963 fd_put(I, DomI1, Ps)
5964 ; true
5965 ).
5966
5968
5973
5974element(N, Is, V) :-
5975 must_be(list, Is),
5976 length(Is, L),
5977 N in 1..L,
5978 element_(Is, 1, N, V),
5979 propagator_init_trigger([N|Is], pelement(N,Is,V)).
5980
5981element_domain(V, VD) :-
5982 ( fd_get(V, VD, _) -> true
5983 ; VD = from_to(n(V), n(V))
5984 ).
5985
5986element_([], _, _, _).
5987element_([I|Is], N0, N, V) :-
5988 ?(I) #\= ?(V) #==> ?(N) #\= N0,
5989 N1 is N0 + 1,
5990 element_(Is, N1, N, V).
5991
5992integers_remaining([], _, _, D, D).
5993integers_remaining([V|Vs], N0, Dom, D0, D) :-
5994 ( domain_contains(Dom, N0) ->
5995 element_domain(V, VD),
5996 domains_union(D0, VD, D1)
5997 ; D1 = D0
5998 ),
5999 N1 is N0 + 1,
6000 integers_remaining(Vs, N1, Dom, D1, D).
6001
6003
6017
6018global_cardinality(Xs, Pairs) :- global_cardinality(Xs, Pairs, []).
6019
6038
6039global_cardinality(Xs, Pairs, Options) :-
6040 must_be(list(list), [Xs,Pairs,Options]),
6041 maplist(fd_variable, Xs),
6042 maplist(gcc_pair, Pairs),
6043 pairs_keys_values(Pairs, Keys, Nums),
6044 ( sort(Keys, Keys1), same_length(Keys, Keys1) -> true
6045 ; domain_error(gcc_unique_key_pairs, Pairs)
6046 ),
6047 length(Xs, L),
6048 Nums ins 0..L,
6049 list_to_drep(Keys, Drep),
6050 Xs ins Drep,
6051 gcc_pairs(Pairs, Xs, Pairs1),
6052 6053 6054 propagator_init_trigger(Xs, pgcc_check(Pairs1)),
6055 propagator_init_trigger(Nums, pgcc_check_single(Pairs1)),
6056 ( member(OD, Options), OD == consistency(value) -> true
6057 ; propagator_init_trigger(Nums, pgcc_single(Xs, Pairs1)),
6058 propagator_init_trigger(Xs, pgcc(Xs, Pairs, Pairs1))
6059 ),
6060 ( member(OC, Options), functor(OC, cost, 2) ->
6061 OC = cost(Cost, Matrix),
6062 must_be(list(list(integer)), Matrix),
6063 maplist(keys_costs(Keys), Xs, Matrix, Costs),
6064 sum(Costs, #=, Cost)
6065 ; true
6066 ).
6067
6068keys_costs(Keys, X, Row, C) :-
6069 element(N, Keys, X),
6070 element(N, Row, C).
6071
6072gcc_pair(Pair) :-
6073 ( Pair = Key-Val ->
6074 must_be(integer, Key),
6075 fd_variable(Val)
6076 ; domain_error(gcc_pair, Pair)
6077 ).
6078
6088
6089gcc_pairs([], _, []).
6090gcc_pairs([Key-Num0|KNs], Vs, [Key-Num|Rest]) :-
6091 put_attr(Num, clpfd_gcc_num, Num0),
6092 put_attr(Num, clpfd_gcc_vs, Vs),
6093 put_attr(Num, clpfd_gcc_occurred, 0),
6094 gcc_pairs(KNs, Vs, Rest).
6095
6100
6101gcc_global(Vs, KNs) :-
6102 gcc_check(KNs),
6103 6104 do_queue,
6105 with_local_attributes(Vs, [edges,parent,index],
6106 (gcc_arcs(KNs, S, Vals),
6107 variables_with_num_occurrences(Vs, VNs),
6108 maplist(target_to_v(T), VNs),
6109 ( get_attr(S, edges, Es) ->
6110 put_attr(S, parent, none), 6111 feasible_flow(Es, S, T), 6112 maximum_flow(S, T), 6113 gcc_consistent(T),
6114 scc(Vals, gcc_successors),
6115 phrase(gcc_goals(Vals), Gs)
6116 ; Gs = [] )), Gs),
6117 disable_queue,
6118 maplist(call, Gs),
6119 enable_queue.
6120
6121gcc_consistent(T) :-
6122 get_attr(T, edges, Es),
6123 maplist(saturated_arc, Es).
6124
6125saturated_arc(arc_from(_,U,_,Flow)) :- get_attr(Flow, flow, U).
6126
6127gcc_goals([]) --> [].
6128gcc_goals([Val|Vals]) -->
6129 { get_attr(Val, edges, Es) },
6130 gcc_edges_goals(Es, Val),
6131 gcc_goals(Vals).
6132
6133gcc_edges_goals([], _) --> [].
6134gcc_edges_goals([E|Es], Val) -->
6135 gcc_edge_goal(E, Val),
6136 gcc_edges_goals(Es, Val).
6137
6138gcc_edge_goal(arc_from(_,_,_,_), _) --> [].
6139gcc_edge_goal(arc_to(_,_,V,F), Val) -->
6140 ( { get_attr(F, flow, 0),
6141 get_attr(V, lowlink, L1),
6142 get_attr(Val, lowlink, L2),
6143 L1 =\= L2,
6144 get_attr(Val, value, Value) } ->
6145 [neq_num(V, Value)]
6146 ; []
6147 ).
6148
6153
6154maximum_flow(S, T) :-
6155 ( gcc_augmenting_path([[S]], Levels, T) ->
6156 phrase(augmenting_path(S, T), Path),
6157 Path = [augment(_,First,_)|Rest],
6158 path_minimum(Rest, First, Min),
6159 maplist(gcc_augment(Min), Path),
6160 maplist(maplist(clear_parent), Levels),
6161 maximum_flow(S, T)
6162 ; true
6163 ).
6164
6165feasible_flow([], _, _).
6166feasible_flow([A|As], S, T) :-
6167 make_arc_feasible(A, S, T),
6168 feasible_flow(As, S, T).
6169
6170make_arc_feasible(A, S, T) :-
6171 A = arc_to(L,_,V,F),
6172 get_attr(F, flow, Flow),
6173 ( Flow >= L -> true
6174 ; Diff is L - Flow,
6175 put_attr(V, parent, S-augment(F,Diff,+)),
6176 gcc_augmenting_path([[V]], Levels, T),
6177 phrase(augmenting_path(S, T), Path),
6178 path_minimum(Path, Diff, Min),
6179 maplist(gcc_augment(Min), Path),
6180 maplist(maplist(clear_parent), Levels),
6181 make_arc_feasible(A, S, T)
6182 ).
6183
6184gcc_augmenting_path(Levels0, Levels, T) :-
6185 Levels0 = [Vs|_],
6186 Levels1 = [Tos|Levels0],
6187 phrase(gcc_reachables(Vs), Tos),
6188 Tos = [_|_],
6189 ( member(To, Tos), To == T -> Levels = Levels1
6190 ; gcc_augmenting_path(Levels1, Levels, T)
6191 ).
6192
6193gcc_reachables([]) --> [].
6194gcc_reachables([V|Vs]) -->
6195 { get_attr(V, edges, Es) },
6196 gcc_reachables_(Es, V),
6197 gcc_reachables(Vs).
6198
6199gcc_reachables_([], _) --> [].
6200gcc_reachables_([E|Es], V) -->
6201 gcc_reachable(E, V),
6202 gcc_reachables_(Es, V).
6203
6204gcc_reachable(arc_from(_,_,V,F), P) -->
6205 ( { \+ get_attr(V, parent, _),
6206 get_attr(F, flow, Flow),
6207 Flow > 0 } ->
6208 { put_attr(V, parent, P-augment(F,Flow,-)) },
6209 [V]
6210 ; []
6211 ).
6212gcc_reachable(arc_to(_L,U,V,F), P) -->
6213 ( { \+ get_attr(V, parent, _),
6214 get_attr(F, flow, Flow),
6215 Flow < U } ->
6216 { Diff is U - Flow,
6217 put_attr(V, parent, P-augment(F,Diff,+)) },
6218 [V]
6219 ; []
6220 ).
6221
6222
6223path_minimum([], Min, Min).
6224path_minimum([augment(_,A,_)|As], Min0, Min) :-
6225 Min1 is min(Min0,A),
6226 path_minimum(As, Min1, Min).
6227
6228gcc_augment(Min, augment(F,_,Sign)) :-
6229 get_attr(F, flow, Flow0),
6230 gcc_flow_(Sign, Flow0, Min, Flow),
6231 put_attr(F, flow, Flow).
6232
6233gcc_flow_(+, F0, A, F) :- F is F0 + A.
6234gcc_flow_(-, F0, A, F) :- F is F0 - A.
6235
6239
6240gcc_arcs([], _, []).
6241gcc_arcs([Key-Num0|KNs], S, Vals) :-
6242 ( get_attr(Num0, clpfd_gcc_vs, Vs) ->
6243 get_attr(Num0, clpfd_gcc_num, Num),
6244 get_attr(Num0, clpfd_gcc_occurred, Occ),
6245 ( nonvar(Num) -> U is Num - Occ, U = L
6246 ; fd_get(Num, _, n(L0), n(U0), _),
6247 L is L0 - Occ, U is U0 - Occ
6248 ),
6249 put_attr(Val, value, Key),
6250 Vals = [Val|Rest],
6251 put_attr(F, flow, 0),
6252 append_edge(S, edges, arc_to(L, U, Val, F)),
6253 put_attr(Val, edges, [arc_from(L, U, S, F)]),
6254 variables_with_num_occurrences(Vs, VNs),
6255 maplist(val_to_v(Val), VNs)
6256 ; Vals = Rest
6257 ),
6258 gcc_arcs(KNs, S, Rest).
6259
6260variables_with_num_occurrences(Vs0, VNs) :-
6261 include(var, Vs0, Vs1),
6262 msort(Vs1, Vs),
6263 ( Vs == [] -> VNs = []
6264 ; Vs = [V|Rest],
6265 variables_with_num_occurrences(Rest, V, 1, VNs)
6266 ).
6267
6268variables_with_num_occurrences([], Prev, Count, [Prev-Count]).
6269variables_with_num_occurrences([V|Vs], Prev, Count0, VNs) :-
6270 ( V == Prev ->
6271 Count1 is Count0 + 1,
6272 variables_with_num_occurrences(Vs, Prev, Count1, VNs)
6273 ; VNs = [Prev-Count0|Rest],
6274 variables_with_num_occurrences(Vs, V, 1, Rest)
6275 ).
6276
6277
6278target_to_v(T, V-Count) :-
6279 put_attr(F, flow, 0),
6280 append_edge(V, edges, arc_to(0, Count, T, F)),
6281 append_edge(T, edges, arc_from(0, Count, V, F)).
6282
6283val_to_v(Val, V-Count) :-
6284 put_attr(F, flow, 0),
6285 append_edge(V, edges, arc_from(0, Count, Val, F)),
6286 append_edge(Val, edges, arc_to(0, Count, V, F)).
6287
6288
6289gcc_successors(V, Tos) :-
6290 get_attr(V, edges, Tos0),
6291 phrase(gcc_successors_(Tos0), Tos).
6292
6293gcc_successors_([]) --> [].
6294gcc_successors_([E|Es]) --> gcc_succ_edge(E), gcc_successors_(Es).
6295
6296gcc_succ_edge(arc_to(_,U,V,F)) -->
6297 ( { get_attr(F, flow, Flow),
6298 Flow < U } -> [V]
6299 ; []
6300 ).
6301gcc_succ_edge(arc_from(_,_,V,F)) -->
6302 ( { get_attr(F, flow, Flow),
6303 Flow > 0 } -> [V]
6304 ; []
6305 ).
6306
6314
6315gcc_check(Pairs) :-
6316 disable_queue,
6317 gcc_check_(Pairs),
6318 enable_queue.
6319
6320gcc_done(Num) :-
6321 del_attr(Num, clpfd_gcc_vs),
6322 del_attr(Num, clpfd_gcc_num),
6323 del_attr(Num, clpfd_gcc_occurred).
6324
6325gcc_check_([]).
6326gcc_check_([Key-Num0|KNs]) :-
6327 ( get_attr(Num0, clpfd_gcc_vs, Vs) ->
6328 get_attr(Num0, clpfd_gcc_num, Num),
6329 get_attr(Num0, clpfd_gcc_occurred, Occ0),
6330 vs_key_min_others(Vs, Key, 0, Min, Os),
6331 put_attr(Num0, clpfd_gcc_vs, Os),
6332 put_attr(Num0, clpfd_gcc_occurred, Occ1),
6333 Occ1 is Occ0 + Min,
6334 geq(Num, Occ1),
6335 6336 6337 6338 6339 6340 ( Occ1 == Num -> all_neq(Os, Key), gcc_done(Num0)
6341 ; Os == [] -> gcc_done(Num0), Num = Occ1
6342 ; length(Os, L),
6343 Max is Occ1 + L,
6344 geq(Max, Num),
6345 ( nonvar(Num) -> Diff is Num - Occ1
6346 ; fd_get(Num, ND, _),
6347 domain_infimum(ND, n(NInf)),
6348 Diff is NInf - Occ1
6349 ),
6350 L >= Diff,
6351 ( L =:= Diff ->
6352 Num is Occ1 + Diff,
6353 maplist(=(Key), Os),
6354 gcc_done(Num0)
6355 ; true
6356 )
6357 )
6358 ; true
6359 ),
6360 gcc_check_(KNs).
6361
6362vs_key_min_others([], _, Min, Min, []).
6363vs_key_min_others([V|Vs], Key, Min0, Min, Others) :-
6364 ( fd_get(V, VD, _) ->
6365 ( domain_contains(VD, Key) ->
6366 Others = [V|Rest],
6367 vs_key_min_others(Vs, Key, Min0, Min, Rest)
6368 ; vs_key_min_others(Vs, Key, Min0, Min, Others)
6369 )
6370 ; ( V =:= Key ->
6371 Min1 is Min0 + 1,
6372 vs_key_min_others(Vs, Key, Min1, Min, Others)
6373 ; vs_key_min_others(Vs, Key, Min0, Min, Others)
6374 )
6375 ).
6376
6377all_neq([], _).
6378all_neq([X|Xs], C) :-
6379 neq_num(X, C),
6380 all_neq(Xs, C).
6381
6383
6399
6400circuit(Vs) :-
6401 must_be(list, Vs),
6402 maplist(fd_variable, Vs),
6403 length(Vs, L),
6404 Vs ins 1..L,
6405 ( L =:= 1 -> true
6406 ; neq_index(Vs, 1),
6407 make_propagator(pcircuit(Vs), Prop),
6408 distinct_attach(Vs, Prop, []),
6409 trigger_once(Prop)
6410 ).
6411
6412neq_index([], _).
6413neq_index([X|Xs], N) :-
6414 neq_num(X, N),
6415 N1 is N + 1,
6416 neq_index(Xs, N1).
6417
6428
6429propagate_circuit(Vs) :-
6430 with_local_attributes([], [],
6431 (same_length(Vs, Ts),
6432 circuit_graph(Vs, Ts, Ts),
6433 scc(Ts, circuit_successors),
6434 maplist(single_component, Ts)), _).
6435
6436single_component(V) :- get_attr(V, lowlink, 0).
6437
6438circuit_graph([], _, _).
6439circuit_graph([V|Vs], Ts0, [T|Ts]) :-
6440 ( nonvar(V) -> Ns = [V]
6441 ; fd_get(V, Dom, _),
6442 domain_to_list(Dom, Ns)
6443 ),
6444 phrase(circuit_edges(Ns, Ts0), Es),
6445 put_attr(T, edges, Es),
6446 circuit_graph(Vs, Ts0, Ts).
6447
6448circuit_edges([], _) --> [].
6449circuit_edges([N|Ns], Ts) -->
6450 { nth1(N, Ts, T) },
6451 [arc_to(T)],
6452 circuit_edges(Ns, Ts).
6453
6454circuit_successors(V, Tos) :-
6455 get_attr(V, edges, Tos0),
6456 maplist(arg(1), Tos0, Tos).
6457
6459
6463
6464cumulative(Tasks) :- cumulative(Tasks, [limit(1)]).
6465
6500
6501cumulative(Tasks, Options) :-
6502 must_be(list(list), [Tasks,Options]),
6503 ( Options = [] -> L = 1
6504 ; Options = [limit(L)] -> must_be(integer, L)
6505 ; domain_error(cumulative_options_empty_or_limit, Options)
6506 ),
6507 ( Tasks = [] -> true
6508 ; fully_elastic_relaxation(Tasks, L),
6509 maplist(task_bs, Tasks, Bss),
6510 maplist(arg(1), Tasks, Starts),
6511 maplist(fd_inf, Starts, MinStarts),
6512 maplist(arg(3), Tasks, Ends),
6513 maplist(fd_sup, Ends, MaxEnds),
6514 min_list(MinStarts, Start),
6515 max_list(MaxEnds, End),
6516 resource_limit(Start, End, Tasks, Bss, L)
6517 ).
6518
6523
6524fully_elastic_relaxation(Tasks, Limit) :-
6525 maplist(task_duration_consumption, Tasks, Ds, Cs),
6526 maplist(area, Ds, Cs, As),
6527 sum(As, #=, ?(Area)),
6528 ?(MinTime) #= (Area + Limit - 1) // Limit,
6529 tasks_minstart_maxend(Tasks, MinStart, MaxEnd),
6530 MaxEnd #>= MinStart + MinTime.
6531
6532task_duration_consumption(task(_,D,_,C,_), D, C).
6533
6534area(X, Y, Area) :- ?(Area) #= ?(X) * ?(Y).
6535
6536tasks_minstart_maxend(Tasks, Start, End) :-
6537 maplist(task_start_end, Tasks, [Start0|Starts], [End0|Ends]),
6538 foldl(min_, Starts, Start0, Start),
6539 foldl(max_, Ends, End0, End).
6540
6541max_(E, M0, M) :- ?(M) #= max(E, M0).
6542
6543min_(E, M0, M) :- ?(M) #= min(E, M0).
6544
6545task_start_end(task(Start,_,End,_,_), ?(Start), ?(End)).
6546
6550
6551resource_limit(T, T, _, _, _) :- !.
6552resource_limit(T0, T, Tasks, Bss, L) :-
6553 maplist(contribution_at(T0), Tasks, Bss, Cs),
6554 sum(Cs, #=<, L),
6555 T1 is T0 + 1,
6556 resource_limit(T1, T, Tasks, Bss, L).
6557
6558task_bs(Task, InfStart-Bs) :-
6559 Task = task(Start,D,End,_,_Id),
6560 ?(D) #> 0,
6561 ?(End) #= ?(Start) + ?(D),
6562 maplist(must_be_finite_fdvar, [End,Start,D]),
6563 fd_inf(Start, InfStart),
6564 fd_sup(End, SupEnd),
6565 L is SupEnd - InfStart,
6566 length(Bs, L),
6567 task_running(Bs, Start, End, InfStart).
6568
6569task_running([], _, _, _).
6570task_running([B|Bs], Start, End, T) :-
6571 ((T #>= Start) #/\ (T #< End)) #<==> ?(B),
6572 T1 is T + 1,
6573 task_running(Bs, Start, End, T1).
6574
6575contribution_at(T, Task, Offset-Bs, Contribution) :-
6576 Task = task(Start,_,End,C,_),
6577 ?(C) #>= 0,
6578 fd_inf(Start, InfStart),
6579 fd_sup(End, SupEnd),
6580 ( T < InfStart -> Contribution = 0
6581 ; T >= SupEnd -> Contribution = 0
6582 ; Index is T - Offset,
6583 nth0(Index, Bs, B),
6584 ?(Contribution) #= B*C
6585 ).
6586
6588
6596
6597disjoint2(Rs0) :-
6598 must_be(list, Rs0),
6599 maplist(=.., Rs0, Rs),
6600 non_overlapping(Rs).
6601
6602non_overlapping([]).
6603non_overlapping([R|Rs]) :-
6604 maplist(non_overlapping_(R), Rs),
6605 non_overlapping(Rs).
6606
6607non_overlapping_(A, B) :-
6608 a_not_in_b(A, B),
6609 a_not_in_b(B, A).
6610
6611a_not_in_b([_,AX,AW,AY,AH], [_,BX,BW,BY,BH]) :-
6612 ?(AX) #=< ?(BX) #/\ ?(BX) #< ?(AX) + ?(AW) #==>
6613 ?(AY) + ?(AH) #=< ?(BY) #\/ ?(BY) + ?(BH) #=< ?(AY),
6614 ?(AY) #=< ?(BY) #/\ ?(BY) #< ?(AY) + ?(AH) #==>
6615 ?(AX) + ?(AW) #=< ?(BX) #\/ ?(BX) + ?(BW) #=< ?(AX).
6616
6618
6643
6644automaton(Sigs, Ns, As) :- automaton(_, _, Sigs, Ns, As, [], [], _).
6645
6646
6712
6713template_var_path(V, Var, []) :- var(V), !, V == Var.
6714template_var_path(T, Var, [N|Ns]) :-
6715 arg(N, T, Arg),
6716 template_var_path(Arg, Var, Ns).
6717
6718path_term_variable([], V, V).
6719path_term_variable([P|Ps], T, V) :-
6720 arg(P, T, Arg),
6721 path_term_variable(Ps, Arg, V).
6722
6723initial_expr(_, []-1).
6724
6725automaton(Seqs, Template, Sigs, Ns, As0, Cs, Is, Fs) :-
6726 must_be(list(list), [Sigs,Ns,As0,Cs,Is]),
6727 ( var(Seqs) ->
6728 ( current_prolog_flag(clpfd_monotonic, true) ->
6729 instantiation_error(Seqs)
6730 ; Seqs = Sigs
6731 )
6732 ; must_be(list, Seqs)
6733 ),
6734 maplist(monotonic, Cs, CsM),
6735 maplist(arc_normalized(CsM), As0, As),
6736 include_args1(sink, Ns, Sinks),
6737 include_args1(source, Ns, Sources),
6738 maplist(initial_expr, Cs, Exprs0),
6739 phrase((arcs_relation(As, Relation),
6740 nodes_nums(Sinks, SinkNums0),
6741 nodes_nums(Sources, SourceNums0)),
6742 [s([]-0, Exprs0)], [s(_,Exprs1)]),
6743 maplist(expr0_expr, Exprs1, Exprs),
6744 phrase(transitions(Seqs, Template, Sigs, Start, End, Exprs, Cs, Is, Fs), Tuples),
6745 list_to_drep(SourceNums0, SourceDrep),
6746 Start in SourceDrep,
6747 list_to_drep(SinkNums0, SinkDrep),
6748 End in SinkDrep,
6749 tuples_in(Tuples, Relation).
6750
6751expr0_expr(Es0-_, Es) :-
6752 pairs_keys(Es0, Es1),
6753 reverse(Es1, Es).
6754
6755transitions([], _, [], S, S, _, _, Cs, Cs) --> [].
6756transitions([Seq|Seqs], Template, [Sig|Sigs], S0, S, Exprs, Counters, Cs0, Cs) -->
6757 [[S0,Sig,S1|Is]],
6758 { phrase(exprs_next(Exprs, Is, Cs1), [s(Seq,Template,Counters,Cs0)], _) },
6759 transitions(Seqs, Template, Sigs, S1, S, Exprs, Counters, Cs1, Cs).
6760
6761exprs_next([], [], []) --> [].
6762exprs_next([Es|Ess], [I|Is], [C|Cs]) -->
6763 exprs_values(Es, Vs),
6764 { element(I, Vs, C) },
6765 exprs_next(Ess, Is, Cs).
6766
6767exprs_values([], []) --> [].
6768exprs_values([E0|Es], [V|Vs]) -->
6769 { term_variables(E0, EVs0),
6770 copy_term(E0, E),
6771 term_variables(E, EVs),
6772 ?(V) #= E },
6773 match_variables(EVs0, EVs),
6774 exprs_values(Es, Vs).
6775
6776match_variables([], _) --> [].
6777match_variables([V0|Vs0], [V|Vs]) -->
6778 state(s(Seq,Template,Counters,Cs0)),
6779 { ( template_var_path(Template, V0, Ps) ->
6780 path_term_variable(Ps, Seq, V)
6781 ; template_var_path(Counters, V0, Ps) ->
6782 path_term_variable(Ps, Cs0, V)
6783 ; domain_error(variable_from_template_or_counters, V0)
6784 ) },
6785 match_variables(Vs0, Vs).
6786
6787nodes_nums([], []) --> [].
6788nodes_nums([Node|Nodes], [Num|Nums]) -->
6789 node_num(Node, Num),
6790 nodes_nums(Nodes, Nums).
6791
6792arcs_relation([], []) --> [].
6793arcs_relation([arc(S0,L,S1,Es)|As], [[From,L,To|Ns]|Rs]) -->
6794 node_num(S0, From),
6795 node_num(S1, To),
6796 state(s(Nodes, Exprs0), s(Nodes, Exprs)),
6797 { exprs_nums(Es, Ns, Exprs0, Exprs) },
6798 arcs_relation(As, Rs).
6799
6800exprs_nums([], [], [], []).
6801exprs_nums([E|Es], [N|Ns], [Ex0-C0|Exs0], [Ex-C|Exs]) :-
6802 ( member(Exp-N, Ex0), Exp == E -> C = C0, Ex = Ex0
6803 ; N = C0, C is C0 + 1, Ex = [E-C0|Ex0]
6804 ),
6805 exprs_nums(Es, Ns, Exs0, Exs).
6806
6807node_num(Node, Num) -->
6808 state(s(Nodes0-C0, Exprs), s(Nodes-C, Exprs)),
6809 { ( member(N-Num, Nodes0), N == Node -> C = C0, Nodes = Nodes0
6810 ; Num = C0, C is C0 + 1, Nodes = [Node-C0|Nodes0]
6811 )
6812 }.
6813
6814include_args1(Goal, Ls0, As) :-
6815 include(Goal, Ls0, Ls),
6816 maplist(arg(1), Ls, As).
6817
6818source(source(_)).
6819
6820sink(sink(_)).
6821
6822monotonic(Var, ?(Var)).
6823
6824arc_normalized(Cs, Arc0, Arc) :- arc_normalized_(Arc0, Cs, Arc).
6825
6826arc_normalized_(arc(S0,L,S,Cs), _, arc(S0,L,S,Cs)).
6827arc_normalized_(arc(S0,L,S), Cs, arc(S0,L,S,Cs)).
6828
6830
6884
6885transpose(Ls, Ts) :-
6886 must_be(list(list), Ls),
6887 lists_transpose(Ls, Ts).
6888
6889lists_transpose([], []).
6890lists_transpose([L|Ls], Ts) :-
6891 maplist(same_length(L), Ls),
6892 foldl(transpose_, L, Ts, [L|Ls], _).
6893
6894transpose_(_, Fs, Lists0, Lists) :-
6895 maplist(list_first_rest, Lists0, Fs, Lists).
6896
6897list_first_rest([L|Ls], L, Ls).
6898
6900
6958
6959zcompare(Order, A, B) :-
6960 ( nonvar(Order) ->
6961 zcompare_(Order, A, B)
6962 ; integer(A), integer(B) ->
6963 compare(Order, A, B)
6964 ; freeze(Order, zcompare_(Order, A, B)),
6965 fd_variable(A),
6966 fd_variable(B),
6967 propagator_init_trigger([A,B], pzcompare(Order, A, B))
6968 ).
6969
6970zcompare_(=, A, B) :- ?(A) #= ?(B).
6971zcompare_(<, A, B) :- ?(A) #< ?(B).
6972zcompare_(>, A, B) :- ?(A) #> ?(B).
6973
6986
6987chain(Zs, Relation) :-
6988 must_be(list, Zs),
6989 maplist(fd_variable, Zs),
6990 must_be(ground, Relation),
6991 ( chain_relation(Relation) -> true
6992 ; domain_error(chain_relation, Relation)
6993 ),
6994 chain_(Zs, Relation).
6995
6996chain_([], _).
6997chain_([X|Xs], Relation) :- foldl(chain(Relation), Xs, X, _).
6998
6999chain_relation(#=).
7000chain_relation(#<).
7001chain_relation(#=<).
7002chain_relation(#>).
7003chain_relation(#>=).
7004
7005chain(Relation, X, Prev, X) :- call(Relation, ?(Prev), ?(X)).
7006
7011
7015
7016fd_var(X) :- get_attr(X, clpfd, _).
7017
7021
7022fd_inf(X, Inf) :-
7023 ( fd_get(X, XD, _) ->
7024 domain_infimum(XD, Inf0),
7025 bound_portray(Inf0, Inf)
7026 ; must_be(integer, X),
7027 Inf = X
7028 ).
7029
7033
7034fd_sup(X, Sup) :-
7035 ( fd_get(X, XD, _) ->
7036 domain_supremum(XD, Sup0),
7037 bound_portray(Sup0, Sup)
7038 ; must_be(integer, X),
7039 Sup = X
7040 ).
7041
7047
7048fd_size(X, S) :-
7049 ( fd_get(X, XD, _) ->
7050 domain_num_elements(XD, S0),
7051 bound_portray(S0, S)
7052 ; must_be(integer, X),
7053 S = 1
7054 ).
7055
7085
7086fd_dom(X, Drep) :-
7087 ( fd_get(X, XD, _) ->
7088 domain_to_drep(XD, Drep)
7089 ; must_be(integer, X),
7090 Drep = X..X
7091 ).
7092
7113
7114goals_entail(Goals, E) :-
7115 must_be(list, Goals),
7116 \+ ( maplist(call, Goals), #\ E,
7117 term_variables(Goals-E, Vs),
7118 label(Vs)
7119 ).
7120
7124
7125attr_unify_hook(clpfd_attr(_,_,_,Dom,Ps), Other) :-
7126 ( nonvar(Other) ->
7127 ( integer(Other) -> true
7128 ; type_error(integer, Other)
7129 ),
7130 domain_contains(Dom, Other),
7131 trigger_props(Ps),
7132 do_queue
7133 ; fd_get(Other, OD, OPs),
7134 domains_intersection(OD, Dom, Dom1),
7135 append_propagators(Ps, OPs, Ps1),
7136 fd_put(Other, Dom1, Ps1),
7137 trigger_props(Ps1),
7138 do_queue
7139 ).
7140
7141append_propagators(fd_props(Gs0,Bs0,Os0), fd_props(Gs1,Bs1,Os1), fd_props(Gs,Bs,Os)) :-
7142 maplist(append, [Gs0,Bs0,Os0], [Gs1,Bs1,Os1], [Gs,Bs,Os]).
7143
7144bound_portray(inf, inf).
7145bound_portray(sup, sup).
7146bound_portray(n(N), N).
7147
7148list_to_drep(List, Drep) :-
7149 list_to_domain(List, Dom),
7150 domain_to_drep(Dom, Drep).
7151
7152domain_to_drep(Dom, Drep) :-
7153 domain_intervals(Dom, [A0-B0|Rest]),
7154 bound_portray(A0, A),
7155 bound_portray(B0, B),
7156 ( A == B -> Drep0 = A
7157 ; Drep0 = A..B
7158 ),
7159 intervals_to_drep(Rest, Drep0, Drep).
7160
7161intervals_to_drep([], Drep, Drep).
7162intervals_to_drep([A0-B0|Rest], Drep0, Drep) :-
7163 bound_portray(A0, A),
7164 bound_portray(B0, B),
7165 ( A == B -> D1 = A
7166 ; D1 = A..B
7167 ),
7168 intervals_to_drep(Rest, Drep0 \/ D1, Drep).
7169
7170attribute_goals(X) -->
7171 7172 { get_attr(X, clpfd, clpfd_attr(_,_,_,Dom,fd_props(Gs,Bs,Os))),
7173 append(Gs, Bs, Ps0),
7174 append(Ps0, Os, Ps),
7175 domain_to_drep(Dom, Drep) },
7176 ( { default_domain(Dom), \+ all_dead_(Ps) } -> []
7177 ; [clpfd:(X in Drep)]
7178 ),
7179 attributes_goals(Ps).
7180
7181clpfd_aux:attribute_goals(_) --> [].
7182clpfd_aux:attr_unify_hook(_,_) :- false.
7183
7184clpfd_gcc_vs:attribute_goals(_) --> [].
7185clpfd_gcc_vs:attr_unify_hook(_,_) :- false.
7186
7187clpfd_gcc_num:attribute_goals(_) --> [].
7188clpfd_gcc_num:attr_unify_hook(_,_) :- false.
7189
7190clpfd_gcc_occurred:attribute_goals(_) --> [].
7191clpfd_gcc_occurred:attr_unify_hook(_,_) :- false.
7192
7193clpfd_relation:attribute_goals(_) --> [].
7194clpfd_relation:attr_unify_hook(_,_) :- false.
7195
7196attributes_goals([]) --> [].
7197attributes_goals([propagator(P, State)|As]) -->
7198 ( { ground(State) } -> []
7199 ; { phrase(attribute_goal_(P), Gs) } ->
7200 { del_attr(State, clpfd_aux), State = processed,
7201 ( current_prolog_flag(clpfd_monotonic, true) ->
7202 maplist(unwrap_with(bare_integer), Gs, Gs1)
7203 ; maplist(unwrap_with(=), Gs, Gs1)
7204 ),
7205 maplist(with_clpfd, Gs1, Gs2) },
7206 list(Gs2)
7207 ; [P] 7208 ),
7209 attributes_goals(As).
7210
7211with_clpfd(G, clpfd:G).
7212
7213unwrap_with(_, V, V) :- var(V), !.
7214unwrap_with(Goal, ?(V0), V) :- !, call(Goal, V0, V).
7215unwrap_with(Goal, Term0, Term) :-
7216 Term0 =.. [F|Args0],
7217 maplist(unwrap_with(Goal), Args0, Args),
7218 Term =.. [F|Args].
7219
7220bare_integer(V0, V) :- ( integer(V0) -> V = V0 ; V = #(V0) ).
7221
7222attribute_goal_(presidual(Goal)) --> [Goal].
7223attribute_goal_(pgeq(A,B)) --> [?(A) #>= ?(B)].
7224attribute_goal_(pplus(X,Y,Z)) --> [?(X) + ?(Y) #= ?(Z)].
7225attribute_goal_(pneq(A,B)) --> [?(A) #\= ?(B)].
7226attribute_goal_(ptimes(X,Y,Z)) --> [?(X) * ?(Y) #= ?(Z)].
7227attribute_goal_(absdiff_neq(X,Y,C)) --> [abs(?(X) - ?(Y)) #\= C].
7228attribute_goal_(absdiff_geq(X,Y,C)) --> [abs(?(X) - ?(Y)) #>= C].
7229attribute_goal_(x_neq_y_plus_z(X,Y,Z)) --> [?(X) #\= ?(Y) + ?(Z)].
7230attribute_goal_(x_leq_y_plus_c(X,Y,C)) --> [?(X) #=< ?(Y) + C].
7231attribute_goal_(ptzdiv(X,Y,Z)) --> [?(X) // ?(Y) #= ?(Z)].
7232attribute_goal_(pdiv(X,Y,Z)) --> [?(X) div ?(Y) #= ?(Z)].
7233attribute_goal_(prdiv(X,Y,Z)) --> [?(X) rdiv ?(Y) #= ?(Z)].
7234attribute_goal_(pexp(X,Y,Z)) --> [?(X) ^ ?(Y) #= ?(Z)].
7235attribute_goal_(pabs(X,Y)) --> [?(Y) #= abs(?(X))].
7236attribute_goal_(pmod(X,M,K)) --> [?(X) mod ?(M) #= ?(K)].
7237attribute_goal_(prem(X,Y,Z)) --> [?(X) rem ?(Y) #= ?(Z)].
7238attribute_goal_(pmax(X,Y,Z)) --> [?(Z) #= max(?(X),?(Y))].
7239attribute_goal_(pmin(X,Y,Z)) --> [?(Z) #= min(?(X),?(Y))].
7240attribute_goal_(scalar_product_neq(Cs,Vs,C)) -->
7241 [Left #\= Right],
7242 { scalar_product_left_right([-1|Cs], [C|Vs], Left, Right) }.
7243attribute_goal_(scalar_product_eq(Cs,Vs,C)) -->
7244 [Left #= Right],
7245 { scalar_product_left_right([-1|Cs], [C|Vs], Left, Right) }.
7246attribute_goal_(scalar_product_leq(Cs,Vs,C)) -->
7247 [Left #=< Right],
7248 { scalar_product_left_right([-1|Cs], [C|Vs], Left, Right) }.
7249attribute_goal_(pdifferent(_,_,_,O)) --> original_goal(O).
7250attribute_goal_(weak_distinct(_,_,_,O)) --> original_goal(O).
7251attribute_goal_(pdistinct(Vs)) --> [all_distinct(Vs)].
7252attribute_goal_(pexclude(_,_,_)) --> [].
7253attribute_goal_(pelement(N,Is,V)) --> [element(N, Is, V)].
7254attribute_goal_(pgcc(Vs, Pairs, _)) --> [global_cardinality(Vs, Pairs)].
7255attribute_goal_(pgcc_single(_,_)) --> [].
7256attribute_goal_(pgcc_check_single(_)) --> [].
7257attribute_goal_(pgcc_check(_)) --> [].
7258attribute_goal_(pcircuit(Vs)) --> [circuit(Vs)].
7259attribute_goal_(pserialized(_,_,_,_,O)) --> original_goal(O).
7260attribute_goal_(rel_tuple(R, Tuple)) -->
7261 { get_attr(R, clpfd_relation, Rel) },
7262 [tuples_in([Tuple], Rel)].
7263attribute_goal_(pzcompare(O,A,B)) --> [zcompare(O,A,B)].
7265attribute_goal_(reified_in(V, D, B)) -->
7266 [V in Drep #<==> ?(B)],
7267 { domain_to_drep(D, Drep) }.
7268attribute_goal_(reified_tuple_in(Tuple, R, B)) -->
7269 { get_attr(R, clpfd_relation, Rel) },
7270 [tuples_in([Tuple], Rel) #<==> ?(B)].
7271attribute_goal_(kill_reified_tuples(_,_,_)) --> [].
7272attribute_goal_(tuples_not_in(_,_,_)) --> [].
7273attribute_goal_(reified_fd(V,B)) --> [finite_domain(V) #<==> ?(B)].
7274attribute_goal_(pskeleton(X,Y,D,_,Z,F)) -->
7275 { Prop =.. [F,X,Y,Z],
7276 phrase(attribute_goal_(Prop), Goals), list_goal(Goals, Goal) },
7277 [?(D) #= 1 #==> Goal, ?(Y) #\= 0 #==> ?(D) #= 1].
7278attribute_goal_(reified_neq(DX,X,DY,Y,_,B)) -->
7279 conjunction(DX, DY, ?(X) #\= ?(Y), B).
7280attribute_goal_(reified_eq(DX,X,DY,Y,_,B)) -->
7281 conjunction(DX, DY, ?(X) #= ?(Y), B).
7282attribute_goal_(reified_geq(DX,X,DY,Y,_,B)) -->
7283 conjunction(DX, DY, ?(X) #>= ?(Y), B).
7284attribute_goal_(reified_and(X,_,Y,_,B)) --> [?(X) #/\ ?(Y) #<==> ?(B)].
7285attribute_goal_(reified_or(X, _, Y, _, B)) --> [?(X) #\/ ?(Y) #<==> ?(B)].
7286attribute_goal_(reified_not(X, Y)) --> [#\ ?(X) #<==> ?(Y)].
7287attribute_goal_(pimpl(X, Y, _)) --> [?(X) #==> ?(Y)].
7288attribute_goal_(pfunction(Op, A, B, R)) -->
7289 { Expr =.. [Op,?(A),?(B)] },
7290 [?(R) #= Expr].
7291attribute_goal_(pfunction(Op, A, R)) -->
7292 { Expr =.. [Op,?(A)] },
7293 [?(R) #= Expr].
7294
7295conjunction(A, B, G, D) -->
7296 ( { A == 1, B == 1 } -> [G #<==> ?(D)]
7297 ; { A == 1 } -> [(?(B) #/\ G) #<==> ?(D)]
7298 ; { B == 1 } -> [(?(A) #/\ G) #<==> ?(D)]
7299 ; [(?(A) #/\ ?(B) #/\ G) #<==> ?(D)]
7300 ).
7301
7302original_goal(original_goal(State, Goal)) -->
7303 ( { var(State) } ->
7304 { State = processed },
7305 [Goal]
7306 ; []
7307 ).
7308
7312
7313scalar_product_left_right(Cs, Vs, Left, Right) :-
7314 pairs_keys_values(Pairs0, Cs, Vs),
7315 partition(ground, Pairs0, Grounds, Pairs),
7316 maplist(pair_product, Grounds, Prods),
7317 sum_list(Prods, Const),
7318 NConst is -Const,
7319 partition(compare_coeff0, Pairs, Negatives, _, Positives),
7320 maplist(negate_coeff, Negatives, Rights),
7321 scalar_plusterm(Rights, Right0),
7322 scalar_plusterm(Positives, Left0),
7323 ( Const =:= 0 -> Left = Left0, Right = Right0
7324 ; Right0 == 0 -> Left = Left0, Right = NConst
7325 ; Left0 == 0 -> Left = Const, Right = Right0
7326 ; ( Const < 0 ->
7327 Left = Left0, Right = Right0+NConst
7328 ; Left = Left0+Const, Right = Right0
7329 )
7330 ).
7331
7332negate_coeff(A0-B, A-B) :- A is -A0.
7333
7334pair_product(A-B, Prod) :- Prod is A*B.
7335
7336compare_coeff0(Coeff-_, Compare) :- compare(Compare, Coeff, 0).
7337
7338scalar_plusterm([], 0).
7339scalar_plusterm([CV|CVs], T) :-
7340 coeff_var_term(CV, T0),
7341 foldl(plusterm_, CVs, T0, T).
7342
7343plusterm_(CV, T0, T0+T) :- coeff_var_term(CV, T).
7344
7345coeff_var_term(C-V, T) :- ( C =:= 1 -> T = ?(V) ; T = C * ?(V) ).
7346
7350
7351:- discontiguous term_expansion/2. 7352
7353term_expansion(make_parse_clpfd, Clauses) :- make_parse_clpfd(Clauses).
7354term_expansion(make_parse_reified, Clauses) :- make_parse_reified(Clauses).
7355term_expansion(make_matches, Clauses) :- make_matches(Clauses).
7356
7357make_parse_clpfd.
7358make_parse_reified.
7359make_matches.
7360
7364
7365make_clpfd_var('$clpfd_queue') :-
7366 make_queue.
7367make_clpfd_var('$clpfd_current_propagator') :-
7368 nb_setval('$clpfd_current_propagator', []).
7369make_clpfd_var('$clpfd_queue_status') :-
7370 nb_setval('$clpfd_queue_status', enabled).
7371
7372:- multifile user:exception/3. 7373
7374user:exception(undefined_global_variable, Name, retry) :-
7375 make_clpfd_var(Name), !.
7376
7377warn_if_bounded_arithmetic :-
7378 ( current_prolog_flag(bounded, true) ->
7379 print_message(warning, clpfd(bounded))
7380 ; true
7381 ).
7382
7383:- initialization(warn_if_bounded_arithmetic). 7384
7385
7389
7390:- multifile prolog:message//1. 7391
7392prolog:message(clpfd(bounded)) -->
7393 ['Using CLP(FD) with bounded arithmetic may yield wrong results.'-[]].
7394
7395
7396 7399
7406
7407:- multifile
7408 sandbox:safe_primitive/1. 7409
7410safe_api(Name/Arity, sandbox:safe_primitive(clpfd:Head)) :-
7411 functor(Head, Name, Arity).
7412
7413term_expansion(safe_api, Clauses) :-
7414 module_property(clpfd, exports(API)),
7415 maplist(safe_api, API, Clauses).
7416
7417safe_api.
7419sandbox:safe_primitive(clpfd:clpfd_equal(_,_)).
7420sandbox:safe_primitive(clpfd:clpfd_geq(_,_)).
7421sandbox:safe_primitive(clpfd:clpfd_in(_,_)).
7423sandbox:safe_primitive(set_prolog_flag(clpfd_monotonic, _))