1% BEGIN LICENSE BLOCK
2% Version: CMPL 1.1
3%
4% The contents of this file are subject to the Cisco-style Mozilla Public
5% License Version 1.1 (the "License"); you may not use this file except
6% in compliance with the License.  You may obtain a copy of the License
7% at www.eclipse-clp.org/license.
8%
9% Software distributed under the License is distributed on an "AS IS"
10% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied.  See
11% the License for the specific language governing rights and limitations
12% under the License.
13%
14% The Original Code is  The ECLiPSe Constraint Logic Programming System.
15% The Initial Developer of the Original Code is  Cisco Systems, Inc.
16% Portions created by the Initial Developer are
17% Copyright (C) 2006 Cisco Systems, Inc.  All Rights Reserved.
18%
19% Contributor(s):
20%
21% END LICENSE BLOCK
22
23% FINITE and INFINITE DOMAINS
24% created 910527 ECRC thom fruehwirth
25% inspired by CHIP
26% 910913 modified
27% 920409 element/3 added
28% 920616 more CHIP predicates added
29% 930726 started porting to CHR release
30% 931014 mult/3 added for CHIC user meeting (Andre Chamard)
31% 931201 ported to CHR release
32% 931208 removed special case of integer domain
33% 940304 element/3 constraint loop due to finite domains with repeated
34%        elements fixed by replacing findall by setof and adding length where necessary
35% 980701 converted to new chr format, Kish Shen
36% 990316 fixed problem with imposing constraint with same domain
37% 990914 removed singleton warnings
38
39% X::Dom - X must be element of the finite or infinite domain Dom
40
41% Domains can be either numbers (including arithemtic expressions)
42% or arbitrary ground terms (!), the domain is set with setval(domain,Kind),
43% where Kind is either number or term. Default for Kind is term.
44
45:- lib(ech).
46
47:- setval(domain,term). 	% set default
48
49% Simplifies domains together with inequalities and some more CHIP predicates:
50% 	element/3, atmost/3, alldistinct/1, circuit/1 and mult/3
51% It also includes paired (!) domains (see element constraint)
52
53:- handler domain.
54
55%option(already_in_store, on).
56%option(already_in_heads, on).
57:- option(check_guard_bindings, off).
58
59% for domain constraints
60:- op(700,xfx,'::').
61:- op(600,xfx,'..').
62:- op(600,xfx,':').
63
64% for inequality constraints
65:-op(700,xfx,lt).
66:-op(700,xfx,le).
67:-op(700,xfx,gt).
68:-op(700,xfx,ge).
69:-op(700,xfx,ne).
70
71
72
73% INEQUALITIES ===============================================================
74% inequalities over numbers (including arithmetic expressions) or terms
75
76:- constraints lt/2,le/2,ne/2.
77
78A gt B :- B lt A.
79A ge B :- B le A.
80% some basic simplifications
81A lt A <=> fail.
82A le A <=> true.
83A ne A <=> fail.
84A lt B,B lt A <=> fail.
85A le B,B le A <=> A=B.
86% for number domain, allow arithmetic expressions in the arguments
87A  lt  B <=> domain(number),ground(A),not number(A) | A1 is A, A1 lt B.
88B  lt  A <=> domain(number),ground(A),not number(A) | A1 is A, B lt A1.
89A  le  B <=> domain(number),ground(A),not number(A) | A1 is A, A1 le B.
90B  le  A <=> domain(number),ground(A),not number(A) | A1 is A, B le A1.
91A  ne  B <=> domain(number),ground(A),not number(A) | A1 is A, A1 ne B.
92B  ne  A <=> domain(number),ground(A),not number(A) | A1 is A, B ne A1.
93% use built-ins to solve the predicates if arguments are known
94A  lt  B <=> ground(A),ground(B) | (domain(number) -> A < B ; A @< B).
95A  le  B <=> ground(A),ground(B) | (domain(number) -> A =< B ; A @=< B).
96A  ne  B <=> ground(A),ground(B) | (domain(number) -> A =\= B ; A \== B).
97A ne B \ B ne A <=> true.
98
99
100
101% FINITE and INFINITE DOMAINS ================================================
102
103% Domains must be ground and enumeration domains sorted (ascending) !
104
105:- constraints (::)/2, chr_labeling/0:at_lower(1).
106
107% enforce groundness
108 X::Dom <=> nonground(Dom) |
109	write('ERROR: Nonground Domain in '),writeln(X::Dom),abort.
110
111% binary search by splitting domain in halves
112 'label::2'(X,Min:Max) :-
113	Mid is (Min+Max)/2,
114	(X::Min:Mid ; X ne Mid, X::Mid:Max).
115
116%	ground(X):- not nonground(X).
117
118	domain(Kind):- getval(domain,Kind).
119
120% CHIP list shorthand for domain variables
121% list must be known (end in the empty list)
122
123 [X|L]::Dom <=> makedom([X|L],Dom).
124
125	makedom([],_D) :- true.
126	makedom([X|L],D) :-
127		X::D,
128		makedom(L,D).
129
130
131% Consecutive integer domain ---------------------------------------------
132% X::Min..Max - X is an integer between the numbers Min and Max (included)
133% constraint is mapped to enumeration domain constraint
134 X::Min..Max <=>
135	Min0 is Min,
136	(Min0=:=round(Min0) -> Min1 is fix(Min0) ; Min1 is fix(Min0+1)),
137	Max1 is fix(Max),
138	interval(Min1,Max1,L),
139	X::L.
140
141 	interval(M,N,[M|Ns]):-
142		M<N,
143		!,
144		M1 is M+1,
145		interval(M1,N,Ns).
146	interval(N,N,[N]).
147
148
149% Enumeration domain -----------------------------------------------------
150% X::Dom - X must be a ground term in the ascending sorted ground list Dom
151% for number domain, allow arithmetic expressions in domain
152% uses already_in_heads option
153 X::[A|L] <=> domain(number), member(X,[A|L]), not number(X) |
154		eval_list([A|L],L1),sort(L1,L2), X::L2.
155
156	eval_list([],[]).
157	eval_list([X|L1],[Y|L2]):-
158		Y is X,
159		eval_list(L1,L2).
160
161% special cases
162 X::[] <=> fail.
163 X::[Y] <=> X=Y.
164 X::[A|L] <=> ground(X) | (member(X,[A|L]) -> true).
165
166
167
168% special cases
169 I-I::L <=> setof(X,member(X-X,L),L1), I::L1.
170 I-V::L <=> ground(I) | setof(X,member(I-X,L),L1), V::L1.
171 I-V::L <=> ground(V) | setof(X,member(X-V,L),L1), I::L1.
172
173% Interval domain ---------------------------------------------------------
174% X::Min:Max - X must be a ground term between Min and Max (included)
175% for number domain, allow for arithmetic expressions ind omain
176% for integer domains, X::Min..Max should be used
177% uses already_in_heads option
178 X::Min:Max <=> domain(number), not (number(Min),number(Max)) |
179		Min1 is Min, Max1 is Max, X::Min1:Max1.
180% special cases
181 X::Min:Min <=> X=Min.
182 X::Min:Max <=> (domain(number) -> Min>Max ; Min@>Max) | fail.
183 X::Min:Max <=> ground(X) |
184		(domain(number) -> Min=<X,X=<Max ; Min@=<X,X@=<Max).
185
186% intersection of domains for the same variable
187 X::[A1|L1], X::[A2|L2] <=> intersection([A1|L1],[A2|L2],L) | X::L.
188% interaction with inequalities
189 X ne Y, X::[A|L] <=> ground(Y) , remove(Y,[A|L],L1), L1\==[A|L] |  X::L1.
190 Y ne X, X::[A|L] <=> ground(Y) , remove(Y,[A|L],L1), L1\==[A|L] |  X::L1.
191 Y le X, X::[A|L] <=> ground(Y) , remove_lower(Y,[A|L],L1), L1\==[A|L] | X::L1.
192 X le Y, X::[A|L] <=> ground(Y) , remove_higher(Y,[A|L],L1),L1\==[A|L] | X::L1.
193 Y lt X, X::[A|L] <=> ground(Y) , remove_lower(Y,[A|L],L1),remove(Y,L1,L2),
194	L2\==[A|L] |  X::L2.
195 X lt Y, X::[A|L] <=> ground(Y) , remove_higher(Y,[A|L],L1),remove(Y,L1,L2),
196	L2\==[A|L] |  X::L2.
197
198% interaction with interval domain
199 X::Min:Max, X::[A|L] <=> remove_lower(Min,[A|L],L1),remove_higher(Max,L1,L2),
200	L2\==[A|L] |  X::L2.
201
202
203% propagation of bounds
204 X le Y, Y::[A|L]   ==> var(X) | last([A|L],Max), X le Max.
205 X le Y, X::[Min|_] ==> var(Y) | Min le Y.
206 X lt Y, Y::[A|L]   ==> var(X) | last([A|L],Max), X lt Max.
207 X lt Y, X::[Min|_] ==> var(Y) | Min lt Y.
208
209	last(L,X):- append(_,[X],L),!.
210
211% intersection of domains for the same variable
212 X::Min1:Max1, X::Min2:Max2 <=> maximum(Min1,Min2,Min),minimum(Max1,Max2,Max) |
213		X::Min:Max.
214
215	minimum(A,B,C):- (domain(number) -> A<B ; A@<B) -> A=C ; B=C.
216	maximum(A,B,C):- (domain(number) -> A<B ; A@<B) -> B=C ; A=C.
217
218% interaction with inequalities
219 X::Min:Max \ X ne Y <=> ground(Y),
220	(domain(number) -> (Y<Min;Y>Max) ; (Y@<Min;Y@>Max)) | true.
221 X::Min:Max \ Y ne X <=> ground(Y),
222	(domain(number) -> (Y<Min;Y>Max) ; (Y@<Min;Y@>Max)) | true.
223 Min2 le X, X::Min1:Max <=> ground(Min2) , maximum(Min1,Min2,Min) | X::Min:Max.
224 X le Max2, X::Min:Max1 <=> ground(Max2) , minimum(Max1,Max2,Max) | X::Min:Max.
225 Min2 lt X, X::Min1:Max <=> ground(Min2) , maximum(Min1,Min2,Min) |
226		X::Min:Max, X ne Min.
227 X lt Max2, X::Min:Max1 <=> ground(Max2) , minimum(Max1,Max2,Max) |
228		X::Min:Max, X ne Max.
229% propagation of bounds
230 X le Y, Y::Min:Max ==> var(X) | X le Max.
231 X le Y, X::Min:Max ==> var(Y) | Min le Y.
232 X lt Y, Y::Min:Max ==> var(X) | X lt Max.
233 X lt Y, X::Min:Max ==> var(Y) | Min lt Y.
234
235
236
237% MULT/3 EXAMPLE EXTENSION ==================================================
238% mult(X,Y,C) - integer X multiplied by integer Y gives the integer constant C.
239
240:- constraints mult/3.
241
242mult(X,Y,C) <=> ground(X) | (X=:=0 -> C=:=0 ; 0=:=C mod X, Y is C//X).
243mult(Y,X,C) <=> ground(X) | (X=:=0 -> C=:=0 ; 0=:=C mod X, Y is C//X).
244mult(X,Y,C), X::MinX:MaxX ==>
245	%(Dom=MinX:MaxX -> true ; Dom=[MinX|L],last(L,MaxX)),
246	MinY is (C-1)//MaxX+1,
247        MaxY is C//MinX,
248	Y::MinY:MaxY.
249mult(Y,X,C), X::MinX:MaxX ==>
250	%(Dom=MinX:MaxX -> true ; Dom=[MinX|L],last(L,MaxX)),
251	MinY is (C-1)//MaxX+1,
252        MaxY is C//MinX,
253	Y::MinY:MaxY.
254
255/*
256[eclipse 46]: mult(X,Y,156),[X,Y]::2:156,X le Y.
257
258X = X_g307
259Y = Y_g331
260
261Constraints:
262(1) mult(X_g307, Y_g331, 156)
263(7) Y_g331 :: 2 : 78
264(8) X_g307 :: 2 : 78
265(10) X_g307 le Y_g331
266
267yes.
268[eclipse 47]: mult(X,Y,156),[X,Y]::2:156,X le Y,labeling.
269
270X = 12
271Y = 13     More? (;)
272
273X = 6
274Y = 26     More? (;)
275
276X = 4
277Y = 39     More? (;)
278
279X = 2
280Y = 78     More? (;)
281
282X = 3
283Y = 52     More? (;)
284
285no (more) solution.
286*/
287
288
289
290
291% CHIP ELEMENT/3 ============================================================
292% translated to "pair domains", a very powerful extension of usual domains
293% this version does not work with arithemtic expressions!
294% uses already_in_heads option
295
296element(I,VL,V):- length(VL,N),interval(1,N,IL),gen_pair(IL,VL,BL), I-V::BL.
297
298	gen_pair([],[],[]).
299	gen_pair([A|L1],[B|L2],[A-B|L3]):-
300		gen_pair(L1,L2,L3).
301
302% intersections
303 X::[A|L1], X-Y::L2 <=> intersect(I::[A|L1],I-V::L2,I-V::L3),
304			length(L2,N2),length(L3,N3),N2>N3 | X-Y::L3.
305 Y::[A|L1], X-Y::L2 <=> intersect(V::[A|L1],I-V::L2,I-V::L3),
306			length(L2,N2),length(L3,N3),N2>N3 | X-Y::L3.
307 X-Y::L1, Y-X::L2 <=> intersect(I-V::L1,V-I::L2,I-V::L3) | X-Y::L3.
308 X-Y::L1, X-Y::L2 <=> intersect(I-V::L1,I-V::L2,I-V::L3) | X-Y::L3.
309
310     intersect(A::L1,B::L2,C::L3):- findall(C,(member(A,L1),member(B,L2)),L3).
311
312% inequalties with two common variables
313 Y lt X, X-Y::L <=> A=R-S,findall(A,(member(A,L),R@< S),L1) | X-Y::L1.
314 X lt Y, X-Y::L <=> A=R-S,findall(A,(member(A,L),S@< R),L1) | X-Y::L1.
315 Y le X, X-Y::L <=> A=R-S,findall(A,(member(A,L),R@=<S),L1) | X-Y::L1.
316 X le Y, X-Y::L <=> A=R-S,findall(A,(member(A,L),S@=<R),L1) | X-Y::L1.
317 Y ne X, X-Y::L <=> A=R-S,findall(A,(member(A,L),R\==S),L1) | X-Y::L1.
318 X ne Y, X-Y::L <=> A=R-S,findall(A,(member(A,L),S\==R),L1) | X-Y::L1.
319% propagation between paired domains
320% X-Y::L1, Y-Z::L2 ==> intersect(A-B::L1,B-C::L2,A-C::L), X-Z::L.
321% X-Y::L1, Z-Y::L2 ==> intersect(A-B::L1,C-B::L2,A-C::L), X-Z::L.
322% X-Y::L1, X-Z::L2 ==> intersect(I-V::L1,I-W::L2,V-W::L), Y-Z::L.
323% propagation to usual unary domains
324 X-Y::L ==> A=R-S,setof(R,A^member(A,L),L1), X::L1,
325	          setof(S,A^member(A,L),L2), Y::L2.
326
327
328
329% ATMOST/3 ===================================================================
330
331atmost(N,List,V):-length(List,K),atmost(N,List,V,K).
332
333:- constraints atmost/4.
334
335atmost(N,List,V,K) <=> K=<N | true.
336atmost(0,List,V,K) <=> (ground(V);ground(List)) | outof(V,List).
337atmost(N,List,V,K) <=> K>N,ground(V),delete_ground(X,List,L1) |
338		(X==V -> N1 is N-1 ; N1=N),K1 is K-1, atmost(N1,L1,V,K1).
339
340	delete_ground(X,List,L1):- delete(X,List,L1),ground(X),!.
341
342
343
344% ALLDISTINCT/1 ===============================================================
345% uses ne/2 constraint
346
347:- constraints alldistinct/1.
348
349alldistinct([]) <=> true.
350alldistinct([X]) <=> true.
351alldistinct([X,Y]) <=> X ne Y.
352alldistinct([A|L]) <=> delete_ground(X,[A|L],L1) | outof(X,L1),alldistinct(L1).
353
354alldistinct([]).
355alldistinct([X|L]):-
356	outof(X,L),
357	alldistinct(L).
358
359outof(_X,[]).
360outof(X,[Y|L]):-
361	X ne Y,
362	outof(X,L).
363
364:- constraints alldistinct1/2.
365
366alldistinct1(R,[]) <=> true.
367alldistinct1(R,[X]), X::[A|L] <=> ground(R) |
368			remove_list(R,[A|L],T), X::T.
369alldistinct1(R,[X]) <=> (ground(R);ground(X)) | outof(X,R).
370alldistinct1(R,[A|L]) <=> ground(R),delete_ground(X,[A|L],L1) |
371			(member(X,R) -> fail ; alldistinct1([X|R],L1)).
372
373
374
375% CIRCUIT/1 =================================================================
376
377% constraints circuit1/1, circuit/1.
378% uses list domains and ne/2
379
380
381% lazy version
382
383circuit1(L):-length(L,N),N>1,circuit1(N,L).
384
385circuit1(2,[2,1]).
386circuit1(N,L):- N>2,
387		interval(1,N,D),
388		T=..[f|L],
389		domains1(1,D,L),
390		alldistinct1([],L),
391		no_subtours(N,1,T,[]).
392
393domains1(_N,_D,[]).
394domains1(N,D,[X|L]):-
395		remove(N,D,DX),
396		X::DX,
397		N1 is N+1,
398		domains1(N1,D,L).
399
400no_subtours(0,_N,_L,_R):- !.
401no_subtours(K,N,L,R):-
402	outof(N,R),
403	(var(N) -> delay(N,no_subtours1(K,N,L,R)) ; no_subtours1(K,N,L,R)).
404% no_subtours(K,N,T,R) \ no_subtours(K1,N,T,_) <=> K<K1 | true.
405
406	no_subtours1(K,N,L,R):-
407		K>0,K1 is K-1,arg(N,L,A),no_subtours(K1,A,L,[N|R]).
408
409
410% eager version
411
412circuit(L):- length(L,N),N>1,circuit(N,L).
413
414circuit(2,[2,1]).
415%circuit(3,[2,3,1]).
416%circuit(3,[3,1,2]).
417circuit(N,L):- 	N>2,
418		interval(1,N,D),
419		T=..[f|L],
420		N1 is N-1,
421		domains(1,D,L,T,N1),
422		alldistinct(L).
423
424domains(_N,_D,[],_T,_K).
425domains(N,D,[X|L],T,K):-
426		remove(N,D,DX),
427		X::DX,
428		N1 is N+1,
429		%no_subtours(K,N,T,[]),		% unfolded
430		no_subtours1(K,X,T,[N]),
431		domains(N1,D,L,T,K).
432
433
434
435
436% remove*/3 auxiliary predicates =============================================
437
438remove(A,B,C):-
439	delete(A,B,C) -> true ; B=C.
440
441remove_list(_,[],T):- !, T=[].
442remove_list([],S,T):- S=T.
443remove_list([X|R],[Y|S],T):- remove(X,[Y|S],S1),remove_list(R,S1,T).
444
445remove_lower(_,[],L1):- !, L1=[].
446remove_lower(Min,[X|L],L1):-
447	X@<Min,
448	!,
449	remove_lower(Min,L,L1).
450remove_lower(Min,[X|L],[X|L1]):-
451	remove_lower(Min,L,L1).
452
453remove_higher(_,[],L1):- !, L1=[].
454remove_higher(Max,[X|L],L1):-
455	X@>Max,
456	!,
457	remove_higher(Max,L,L1).
458remove_higher(Max,[X|L],[X|L1]):-
459	remove_higher(Max,L,L1).
460
461
462chr_labeling, X::[Y|L] <=> 'label::'(X,[Y|L]), wake, chr_labeling.
463'label::'(X,[Y|L]) :- member(X,[Y|L]).
464
465chr_labeling, X::Min:Max <=> domain(number) |  'label::2'(X,Min:Max), chr_labeling.
466
467% end of handler domain
468
469
470
471
472