1 % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(clpfd_interface,[try_post_constraint/1, post_constraint/2, post_constraint2/2,
6 force_post_constraint/1,
7 clpfd_neq_expr/2, clpfd_eq_expr/2, clpfd_eq_expr_optimized/2,
8 clpfd_eq_div/3, clpfd_eq_fdiv/3,
9 clpfd_eq_guarded_div/3, clpfd_eq_guarded_fdiv/3,
10 clpfd_eq/2, clpfd_neq/2,
11 clpfd_nr_eq/2,
12 clpfd_geq2/3,
13 clpfd_geq/3, clpfd_gt/3, clpfd_leq/3, clpfd_lt/3,
14 clpfd_leq_expr/2, clpfd_lt_expr/2,
15 clpfd_inrange/3, clpfd_inrange/4,
16 clpfd_not_inrange/3, clpfd_not_in_non_empty_range/3,
17 clpfd_sum/2,
18 clpfd_inlist/2, clpfd_not_inlist/2,
19 clpfd_reify_inlist/4, force_clpfd_inlist/2,
20 clpfd_minimum/2, clpfd_maximum/2,
21 clpfd_if_then_else/4,
22 clpfd_domain/3, clpfd_size/2,
23 clpfd_in_domain/3,
24 clpfd_some_element_in_domain/2,
25 clpfd_max_bounded/1,
26 clpfd_can_match/2,
27 clpfd_check_geq_nr/2,
28 clpfd_alldifferent/1,
29 %clpfd_labeling/1, % not used at the moment
30 clpfd_degree/2,
31 clpfd_in_domain/1, clpfd_labeling/2,
32 clpfd_can_intersect/2,
33 %clpfd_reverse_labeling/1, clpfd_reverse_labeling/2,
34 clpfd_get_next_variable_to_label/2, clpfd_get_next_variable_to_label/3,
35 %clpfd_get_next_variable_to_label_ffc/3,
36 is_64_bit_system/0, clpfd_overflow_error_message/0, clpfd_overflow_warning_message/0,
37 integer_too_large_for_clpfd/1, integer_too_small_for_clpfd/1,
38 catch_clpfd_overflow_call1/1, catch_clpfd_overflow_call2/2, catch_clpfd_overflow_call3/3,
39 catch_and_ignore_clpfd_overflow/2,
40 computable_arith_expression/1,
41 clpfd_randomised_labeling/2, clpfd_randomised_in_domain/1,
42 clpfd_observe/2, clpfd_observe_state/1,
43 clpfd_gcd/3, clpfd_lcm/3, clpfd_abs/2, clpfd_sign/2]).
44
45 :- meta_predicate try_post_constraint(0).
46 :- meta_predicate post_constraint(0,0).
47 :- meta_predicate post_constraint2(0,*).
48 :- meta_predicate time_out_constraint(0,0).
49 %:- meta_predicate force_post_constraint(0).
50 %:- meta_predicate force_post_constraint(0,0).
51 :- meta_predicate catch_clpfd_overflow_call1(0).
52 :- meta_predicate catch_clpfd_overflow_call2(0,0).
53 :- meta_predicate catch_clpfd_overflow_call3(0,*,0).
54 :- meta_predicate catch_and_ignore_clpfd_overflow(-,0).
55 :- meta_predicate handle_representation_error(*,*,0).
56
57 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
58 :- use_module(library(clpfd)).
59 :- use_module(chrsrc(chr_integer_inequality),[chr_leq/2, chr_lt/2, chr_eq/2, chr_eq/3, chr_neq/2]).
60
61
62
63 %:- use_module(typechecker).
64 :- use_module(tools).
65 :- use_module(preferences).
66 :- use_module(library(timeout)).
67 :- use_module(error_manager).
68 :- use_module(self_check).
69
70 :- use_module(module_information,[module_info/2]).
71 :- module_info(group,kernel).
72 :- module_info(description,'Provide interface to CLP(FD), with Prolog fallback in case of errors or when CLP(FD) turned off.').
73
74 % an equality which tries to avoid CLP(FD) overflows
75 clpfd_nr_eq(Nr,FDVar) :- integer(Nr), var(FDVar),!,
76 clpfd_domain(FDVar,Low,Up),
77 (number(Low), Low>Nr -> fail % fail without unification; prevent overflows
78 ; number(Up), Up<Nr -> fail % ditto
79 ; FDVar=Nr).
80 clpfd_nr_eq(Nr,E2) :- Nr=E2.
81
82 % Note: clpfd_eq is sometimes called with arithmetic expressions (treatment of plus/minus/...)
83 % does not do the computable_arith_expression check
84 clpfd_eq(E1,E2) :- simple(E1), simple(E2), % was (before 29.8.2014): number(E1),number(E2),
85 !,
86 E1=E2.
87 clpfd_eq(E1,E2) :-
88 (preferences:preference(use_chr_solver,true) -> chr_eq(E1,E2) ; true),
89 ? try_post_constraint( E1 #= E2 ).
90
91 clpfd_neq(E1,E2) :- number(E1),!,
92 (number(E2) -> E1\=E2 ; try_post_constraint(E1 #\= E2),dif(E1,E2)). % no need to post dif constraint if one arg is number in clpfd mode
93 clpfd_neq(E1,E2) :- number(E2),!, % no need to post dif constraint in clpfd mode
94 post_constraint( E1 #\= E2, dif(E1,E2)).
95 clpfd_neq(E1,E2) :-
96 % Note: | ?- X #\= Y, Y #=X. --> does not fail; hence we also execute dif(E1,E2) in CLPFD mode !
97 % We might be able to skip calling dif, if we enable the CHR solver by default
98 % Let's try it: only set up dif if CHR is disabled!
99 (preferences:preference(use_chr_solver,true) -> chr_neq(E1,E2) ; dif(E1,E2)),
100 try_post_constraint(E1 #\= E2).
101 % clpfd_domain(E1,D1,D2), clpfd_domain(E2,B1,B2), print(dom(D1:D2,B1:B2)),nl.
102
103 % set up a dif co-routine only if necessary; assumption: E1,E2 are either number or variable
104 dif_when_necesssary(E1,E2) :- %print(dif_when_necesssary(E1,E2)),nl,
105 var(E1),var(E2),!, dif(E1,E2).
106 dif_when_necesssary(_,_).
107
108 % this will force Y to be nonzero
109 clpfd_eq_div(E1,X,Y) :- post_constraint( E1 #= X//Y, prolog_eq(E1,X//Y)), % truncated division -1 // 4 = 0
110 propagate_div_eq_eq(E1,X,Y).
111 clpfd_eq_fdiv(E1,X,Y) :- post_constraint( E1 #= X div Y, prolog_eq(E1,X div Y)). % floored division -1 div 4 = -1
112
113 % certain == propagation rules not done by CLPFD
114 propagate_div_eq_eq(E1,X,Y) :-
115 (var(E1),X==Y
116 -> %print(setting1(E1,X,Y)),nl,
117 E1=1 % X/X can only be 1 or undefined when X=0
118 ; true).
119 % we could check if E1==X --> Y=1 if X /= 0
120
121 % this waits until we are sure Y is not zero
122 % E1 = X / Y
123 clpfd_eq_guarded_div(E1,X,Y) :-
124 post_constraint3((E1 #= X//YY #/\ MY in 0..1 #/\ Y #= MY*YY), % Y can either be 0 or equal to YY
125 prolog_eq(E1,X//Y),Posted),
126 % Note: E1 can be at most abs(X); if the range of E1 is already beyond that the above will fail
127 % and not detect WD errors !
128 % this is better than the previous solution:
129 % post_constraint(Y#\=0 #=> YY#=Y, prolog_eq(Y,YY)).
130 % however, x:44..77 & E : 1..5555 & E = x/y & y:0..4 only restricts E to 1..77, not 11..77
131 % what is still missing is propagating upper bounds of Y to YY
132 % Y in 0..4, M in 0..1, YY in 1..77, Y #=M*YY
133 % with this propagation below, we at least obtain propagation for x:44..77 & E : 1..5555 & y:0..4 & E = x/y
134 % what we need is continously propagating the bounds from Y to YY (but not vice versa for 0)
135 % maybe we can achieve this using indexicals ??
136 (Posted==true
137 -> fd_max(Y,YUp), (number(YUp) -> YY #=< YUp ; true),
138 fd_min(Y,YLow), (number(YLow) -> YY #>= YLow ; true),
139 propagate_div_eq_eq(E1,X,Y)
140 ; true).
141
142 /*
143 Note: X #= Y//0 fails in CLPFD.
144 Here is an example:
145 | ?- X = 1, Y #>= 0, E1 #= X//YY #/\ MY in 0..1 #/\ Y #= MY*YY.
146 X = 1,
147 Y in 0..sup,
148 YY in(inf.. -1)\/(1..sup),
149 E1 in-1..1,
150 MY in 0..1 ?
151 As you can see, we infer that the result is -1..1; this can prevent finding WD errors
152 */
153
154 % now a similar solution for floored division
155 clpfd_eq_guarded_fdiv(E1,X,Y) :-
156 post_constraint3((E1 #= X div YY #/\ MY in 0..1 #/\ Y #= MY*YY), prolog_eq(E1,X div Y),_Posted).
157 % TO DO: add propagation like above or using indexicals
158
159 % do we need to instantiate YY if Y becomes 0 ??
160 %:- block copy_divisor(-,?).
161 %copy_divisor(Y,Y).
162
163
164
165 % we check whether we have simple expressions of the form X = Y OP Z
166 % in this case it is better to call ProB's implementations, as they have stronger propagation
167 % (e.g., 0 = X-Y => X=Y or 1 = X-Y => X/=Y)
168 clpfd_eq_expr_optimized(CLPFD_Expr1,CLPFD_Expr2) :-
169 (simple(CLPFD_Expr1) -> call_eq_expr1(CLPFD_Expr2,CLPFD_Expr1)
170 ; simple(CLPFD_Expr2) -> call_eq_expr2(CLPFD_Expr1,CLPFD_Expr2)
171 ; clpfd_eq_expr_nonsimple(CLPFD_Expr1,CLPFD_Expr2)).
172
173 :- use_module(kernel_dif).
174 call_eq_expr1(CLPFD_Expr2,CLPFD_Expr1) :-
175 (simple(CLPFD_Expr2) -> %print(unify(CLPFD_Expr2,CLPFD_Expr1)),nl, translate:print_clpfd_variable(CLPFD_Expr2),nl, translate:print_clpfd_variable(CLPFD_Expr1),nl,
176 % first check if we have a pending dif; unification could trigger CLPFD enumeration
177 ((var(CLPFD_Expr1),kernel_dif:frozen_dif(CLPFD_Expr2,CLPFD_Expr1)) -> /* print(dif),nl,*/ fail ; true),
178 CLPFD_Expr2=CLPFD_Expr1
179 ; call_eq_expr2(CLPFD_Expr2,CLPFD_Expr1)).
180
181 % first arg not simple, second arg simple
182 call_eq_expr2(CLPFD_Expr2,CLPFD_Expr1) :- CLPFD_Expr2 = -(A,B),simple(A),simple(B),!,
183 %kernel_objects:int_minus(int(A),int(B),int(CLPFD_Expr1)). % has special propagation rules
184 (number(A),number(B) -> CLPFD_Expr1 is CLPFD_Expr2
185 ; clpfd_eq_expr_nonsimple(CLPFD_Expr2,CLPFD_Expr1),
186 propagate_zero(A,B,CLPFD_Expr1)).
187 call_eq_expr2(CLPFD_Expr2,CLPFD_Expr1) :- CLPFD_Expr2 = +(A,B),simple(A),simple(B),!,
188 (number(A),number(B) -> CLPFD_Expr1 is CLPFD_Expr2
189 ; clpfd_eq_expr_nonsimple(CLPFD_Expr1,CLPFD_Expr2),
190 propagate_zero(CLPFD_Expr1,A,B)).
191 %kernel_objects:int_plus(int(A),int(B),int(CLPFD_Expr1)). % has special propagation rules
192 call_eq_expr2(CLPFD_Expr2,CLPFD_Expr1) :-
193 (computable_arith_expression(CLPFD_Expr2) -> CLPFD_Expr1 is CLPFD_Expr2
194 ; clpfd_eq_expr_nonsimple(CLPFD_Expr1,CLPFD_Expr2)).
195
196 % a propagation rule not done by CLP(FD)
197 :- block propagate_zero(-,-,-).
198 propagate_zero(Sum,A,B) :- % print(prop_zero(Sum,A,B)),nl,
199 (A==0 -> Sum=B ; B==0 -> Sum=A ; true).
200
201 % eq_expr takes expressions as arguments
202 clpfd_eq_expr(E1,E2) :- simple(E1),!,
203 (simple(E2) -> E1=E2
204 ; computable_arith_expression(E2) -> E1 is E2
205 ; clpfd_eq_expr_nonsimple(E1,E2)).
206 clpfd_eq_expr(E1,E2) :- simple(E2),computable_arith_expression(E1),!, E2 is E1.
207 clpfd_eq_expr(E1,E2) :- clpfd_eq_expr_nonsimple(E1,E2).
208
209 clpfd_eq_expr_nonsimple(E1,E2) :-
210 (preferences:preference(use_chr_solver,true) -> chr_eq(E1,E2) ; true),
211 post_constraint( E1 #= E2, prolog_eq(E1,E2)).
212 %% post_constraint( E1 #= E2). % Used instead of line below because of serious bug in SICStus 4.1.3
213 % BUG: X*X #= 100, X #= 9. succeeds !
214
215 :- assert_must_succeed((clpfd_interface:prolog_eq(X,2+1),X==3)).
216 :- assert_must_succeed((clpfd_interface:prolog_eq(X,2+Z),Z=3,X==5)).
217 :- assert_must_succeed((clpfd_interface:prolog_eq(X,2+Z),X=5,Z=3)).
218 :- assert_must_succeed((clpfd_interface:prolog_eq(4-1,X),X==3)).
219 :- assert_must_succeed((clpfd_interface:prolog_eq(5-2,(2*2)-Y),Y=1)).
220 :- assert_must_succeed((clpfd_interface:prolog_eq(5-X,(2*2)-Y),Y=1,X=2)).
221 :- assert_must_fail((clpfd_interface:prolog_eq(5-2,(2*2)-Y),Y=0)).
222 % used as Prolog backup when posting constraints, only right-hand side can be an arithmetic term
223 prolog_eq(A,B) :- simple(A),!, when(ground(B), A is B).
224 prolog_eq(A,B) :- simple(B),!, when(ground(A), B is A).
225 prolog_eq(A,B) :- when((ground(A),ground(B)),=:=(A,B)).
226
227 computable_arith_expression(X) :- number(X),!.
228 computable_arith_expression(X) :- var(X),!,fail.
229 computable_arith_expression(-(X)) :- computable_arith_expression(X).
230 computable_arith_expression(abs(X)) :- computable_arith_expression(X).
231 computable_arith_expression(+(X,Y)) :- computable_arith_expression(X),computable_arith_expression(Y).
232 computable_arith_expression(-(X,Y)) :- computable_arith_expression(X),computable_arith_expression(Y).
233 computable_arith_expression(*(X,Y)) :- computable_arith_expression(X),computable_arith_expression(Y).
234
235 clpfd_neq_expr(E1,E2) :- number(E1),number(E2),!,E1\=E2.
236 clpfd_neq_expr(E1,E2) :- %print(neq_expr(E1,E2)),nl,
237 var(E1), var(E2), !,
238 (preferences:preference(use_chr_solver,true) -> chr_neq(E1,E2) ; dif(E1,E2)),
239 try_post_constraint( E1 #\= E2 ). % does not matter if posted
240 % Note: | ?- X #\= Y, Y #=X. --> does not fail; hence we also execute dif(E1,E2) in CLPFD mode !
241 clpfd_neq_expr(E1,E2) :- % print(neq_expr(E1,E2)),nl,
242 post_constraint3( E1 #\= E2, prolog_neq(E1,E2), Posted),
243 (Posted=true -> my_dif(E1,E2) ; true).
244
245 :- assert_must_succeed((clpfd_interface:prolog_neq(X,2+1),X=2)).
246 :- assert_must_succeed((clpfd_interface:prolog_neq(X,2+Z),X=2,Z=1)).
247 :- assert_must_succeed((clpfd_interface:prolog_neq(X,2+Z),Z=1,X=2)).
248 :- assert_must_fail((clpfd_interface:prolog_neq(X,2+1),X=3)).
249 :- assert_must_succeed((clpfd_interface:prolog_neq(3,X),X=2)).
250 :- assert_must_succeed((clpfd_interface:prolog_neq(5-2,(2*2)-Y),Y=2)).
251 % used as Prolog backup when posting constraints,
252 prolog_neq(A,B) :- simple(A),simple(B),!, dif(A,B).
253 prolog_neq(A,B) :- A \== B, when((ground(A),ground(B)),=\=(A,B)).
254
255 my_dif(A,B) :- (simple(A);simple(B)),!. % do we need to setup things like dif(X,0) ?
256 my_dif(A,B) :- comm_assoc_dif(A,B).
257
258 % note: here we do not block, we use \== now rather than waiting on variables to be bound
259 comm_assoc_dif(A,B) :- var(A),!, A \== B.
260 comm_assoc_dif(A,B) :- var(B),!, A \== B.
261 comm_assoc_dif(*(A1,A2),*(B1,B2)) :- !,
262 extract_factors2(A1,A2,FA,[]), sort(FA,SFA),
263 extract_factors2(B1,B2,FB,[]), sort(FB,SFB),
264 %print(comm_assoc_dif_mul(SFA,SFB)),nl,
265 SFA \== SFB.
266 comm_assoc_dif(+(A1,A2),+(B1,B2)) :- !,
267 extract_terms2(A1,A2,FA,[]), sort(FA,SFA),
268 extract_terms2(B1,B2,FB,[]), sort(FB,SFB),
269 %print(comm_assoc_dif_sum(SFA,SFB)),nl,
270 SFA \== SFB.
271 comm_assoc_dif(-(A1),-(B1)) :- !, comm_assoc_dif(A1,B1).
272 comm_assoc_dif(-(A1,A2),-(B1,B2)) :- !,
273 (comm_assoc_dif(A1,B1) -> true ; comm_assoc_dif(A2,B2)).
274 % note : exponentiation and division are not handed directly to CLPFD at the moment, so no need to check here:
275 %comm_assoc_dif(**(A1,A2),**(B1,B2)) :- !, (comm_assoc_dif(A1,B1) -> true ; comm_assoc_dif(A2,B2)).
276 comm_assoc_dif(A,B) :- A \== B. % ,((nonvar(A),nonvar(B)) -> nl,print(cadif(A,B)),nl ; true).
277
278 extract_factors2(A,B) --> extract_factors(A), extract_factors(B).
279 extract_factors(A) --> {var(A)},!, [A].
280 extract_factors(*(A,B)) --> !, extract_factors(A), extract_factors(B).
281 extract_factors(+(A,B)) --> !, [sum(ST)], {extract_terms2(A,B,T,[]),sort(T,ST)}.
282 extract_factors(A) --> [A].
283
284 extract_terms2(A,B) --> extract_terms(A), extract_terms(B).
285 extract_terms(A) --> {var(A)},!, [A].
286 extract_terms(+(A,B)) --> !, extract_terms(A), extract_terms(B).
287 extract_terms(*(A,B)) --> !, [mul(ST)], {extract_factors2(A,B,T,[]),sort(T,ST)}.
288 extract_terms(A) --> [A].
289
290
291 :- assert_must_succeed((clpfd_interface:clpfd_leq_expr(3,X+1),X=3)).
292 :- assert_must_fail((clpfd_interface:clpfd_leq_expr(2,X-1),X=2)).
293 clpfd_leq_expr(E1,E2) :- number(E1),number(E2), !, E1 =< E2.
294 clpfd_leq_expr(E1,E2) :- useless_leq_constraint(E1,E2),!.
295 clpfd_leq_expr(E1,E2) :-
296 (preferences:preference(use_chr_solver,true) -> chr_leq(E1,E2) ; true),
297 post_constraint( E1 #=< E2, prolog_leq(E1,E2)).
298 prolog_leq(A,B) :- when((ground(A),ground(B)),=<(A,B)).
299
300 :- assert_must_succeed((clpfd_interface:clpfd_lt_expr(3,X+1),X=3)).
301 :- assert_must_fail((clpfd_interface:clpfd_lt_expr(2,X-1),X=3)).
302 clpfd_lt_expr(E1,E2) :- number(E1),number(E2), !, E1 < E2.
303 clpfd_lt_expr(E1,E2) :- useless_lt_constraint(E1,E2),!.
304 clpfd_lt_expr(E1,E2) :-
305 (preferences:preference(use_chr_solver,true) -> chr_lt(E1,E2) ; dif_when_necesssary(E1,E2)), % dif useful to detect that x<y & x=y is inconsisent; or x+1 < y+1 & x=y; note however x+1 < y & x=y is not detected as inconsistent without CHR
306 post_constraint( E1 #< E2, prolog_lt(E1,E2)).
307 prolog_lt(A,B) :- when((ground(A),ground(B)),<(A,B)).
308
309 /* TO DO: do custom equalities div, plus, ...
310 mydiv(X, Y, Z) :-
311 (Y#=0 #\/ (Y#\=0 #/\ X/Y #= Z)). */
312
313 % a version of geq which avoids posting constraints if possible
314 clpfd_geq2(E1,E2,Posted) :- number(E1),number(E2),!, E1 >= E2, Posted=true.
315 clpfd_geq2(E1,E2,Posted) :-
316 (preferences:preference(use_chr_solver,true) -> chr_leq(E2,E1) ; true),
317 %E1 #>= E2, Posted=true.
318 post_constraint2( E1 #>= E2 , Posted).
319
320 clpfd_geq(E1,E2,Posted) :- clpfd_leq(E2,E1,Posted).
321 clpfd_gt(E1,E2,Posted) :- clpfd_lt(E2,E1,Posted).
322
323 clpfd_leq(E1,E2,Posted) :-
324 useless_leq_constraint(E1,E2),
325 !, Posted=true. % we have a useless constraint which is already known; avoid overhead of catch and time_out
326 clpfd_leq(E1,E2,Posted) :-
327 (preferences:preference(use_chr_solver,true) -> chr_leq(E1,E2) ; true),
328 %E1 #=< E2, Posted=true.
329 ? post_constraint2( E1 #=< E2 , Posted).
330
331 useless_leq_constraint(E1,E2) :- number(E1), !, var(E2), fd_min(E2,Low), number(Low),E1 =< Low.
332 useless_leq_constraint(E1,E2) :- number(E2), var(E1), fd_max(E1,Up), number(Up),Up =< E2.
333
334
335 clpfd_lt(E1,E2,Posted) :-
336 useless_lt_constraint(E1,E2),
337 !, Posted=true. % we have a useless constraint which is already known; avoid overhead of catch and time_out
338 clpfd_lt(E1,E2,Posted) :-
339 (preferences:preference(use_chr_solver,true) -> chr_lt(E1,E2) ; dif_when_necesssary(E1,E2)),
340 post_constraint2( E1 #< E2 , Posted).
341
342 useless_lt_constraint(E1,E2) :- number(E1), !, var(E2), fd_min(E2,Low), number(Low),E1 < Low.
343 useless_lt_constraint(E1,E2) :- number(E2), var(E1), fd_max(E1,Up), number(Up),Up < E2.
344
345 clpfd_inrange(X,Low,Up) :- clpfd_inrange(X,Low,Up,_Posted).
346 clpfd_inrange(X,Low,Up,Posted) :-
347 (Low==Up -> X=Low, Posted=true
348 ; (number(Low),number(Up)
349 -> Low =< Up, % otherwise interval empty
350 (number(X) -> X >= Low, X =< Up, Posted=true %, Low =<Up
351 ; post_constraint2(X in Low..Up, Posted)
352 % Note: X in 1..Y, Y in 0..3. fails! Range needs to be constant
353 % post_chr_inrange(X,Low,Up) % not useful, as CLPFD will be propagating bounds anyway?
354 % if one performs CHR propgation before CLPFD, test 2133 fails for
355 % xx:0..3 & not(xx>xx-1 & card(xx..xx) = 1) loops
356 )
357 ; post_chr_inrange(X,Low,Up),
358 post_constraint2( (X #>=Low #/\ X #=< Up),Posted ) % #/\ Low #=< Up should be implied
359 %,translate:print_clpfd_variables([X,Low,Up]),nl
360 )
361 ).
362
363 post_chr_inrange(X,Low,Up) :-
364 (preferences:preference(use_chr_solver,true)
365 -> chr_leq(Low,X),
366 chr_leq(X,Up)
367 ; true).
368
369 % assumes Low =< Up !
370 clpfd_not_in_non_empty_range(X,Low,Up) :-
371 ? post_constraint((X #<Low #\/ X #> Up),outside_range_blocking(X,Low,Up)).
372
373 :- block outside_range_blocking(-,?,?).
374 outside_range_blocking(X,Low,Up) :- (X<Low ; X>Up).
375
376 % assumes Low =< Up !
377 clpfd_not_inrange(X,Low,Up) :- preferences:preference(use_clpfd_solver,false),
378 !, % avoid building up constraint below
379 not_in_range_blocking(X,Low,Up).
380 clpfd_not_inrange(X,Low,Up) :-
381 % special treatment due to limitation of CLP(FD) disjunct: | ?- X #>10 #\/ X #>9. ---> X in inf..sup
382 post_constraint2(XLow #<=> (X #<Low), Posted1), Posted1==true,
383 post_constraint2(UpX #<=> (Up #< X), Posted2), Posted2==true,
384 post_constraint2(UpLow #<=> (Up #< Low), Posted3), Posted3==true,
385 !,
386 clpfd_not_inrange_prop(XLow,UpX,UpLow,X,Low,Up).
387 clpfd_not_inrange(X,Low,Up) :-
388 force_post_constraint((X #<Low #\/ X #> Up #\/ Up #< Low),not_in_range_blocking(X,Low,Up)).
389
390 :- block clpfd_not_inrange_prop(-,-,-,?,?,?).
391 clpfd_not_inrange_prop(XLow,UpX,UpLow,_X,_Low,_Up) :- %print(unblock(XLow,UpX,UpLow,X,Low,Up)),nl,
392 (XLow==1 ; UpX==1 ; UpLow==1),!.
393 clpfd_not_inrange_prop(XLow,UpX,UpLow,X,Low,Up) :- XLow==0,!,
394 post_constraint2(Up #< max(X,Low),_), disjunct_reify(UpX,UpLow).
395 clpfd_not_inrange_prop(XLow,UpX,UpLow,X,Low,Up) :- UpX==0,!,
396 post_constraint2(Low #> min(X,Up),_), disjunct_reify(XLow,UpLow).
397 clpfd_not_inrange_prop(XLow,UpX,_UpLow,_X,_Low,_Up) :- % UpLow==0,
398 % Anything more we can infer here ??
399 disjunct_reify(XLow,UpX).
400
401 :- block disjunct_reify(-,-).
402 disjunct_reify(UpX,UpLow) :- (UpX==1 ; UpLow==1),!.
403 disjunct_reify(UpX,UpLow) :- (UpX==0 -> UpLow=1 ; UpX=1).
404
405
406 :- block not_in_range_blocking(-,?,?),not_in_range_blocking(?,-,?).
407 not_in_range_blocking(X,Y,Z) :-
408 (X<Y -> true ; not_in_range_blocking2(X,Y,Z)).
409 :- block not_in_range_blocking2(?,?,-).
410 not_in_range_blocking2(X,Y,Z) :- (Z<Y -> true ; Z<X).
411
412 clpfd_sum(List,Sum) :-
413 clpfd_sum(List,Sum,Posted),
414 (Posted==true -> true
415 ; sum_list(List,int(0),int(Sum))).
416 clpfd_sum(List,Sum,Posted) :- post_constraint2( sum(List,'#=',Sum),Posted).
417
418 :- use_module(kernel_objects,[int_plus/3]).
419 % non-CLPFD backup, when posting fails or CLPFD turned off
420 :- block sum_list(-,?,?).
421 sum_list([],Acc,Acc).
422 sum_list([H|T],Acc,Res) :- int_plus(int(H),Acc,NewAcc), sum_list(T,NewAcc,Res).
423
424
425 % assert that a variable is one of the numbers in the FDList; FDList must be numbers, cannot be unbound FD variable
426 % can fail due to overflows; one should not rely on it for soundness, see test 1353
427 clpfd_inlist(El,[X]) :- !, El=X.
428 clpfd_inlist(El,FDList) :-
429 try_post_constraint( (list_to_fdset(FDList,FDSET), El in_set FDSET)).
430
431 % a version that always posts constraints independent of CLPFD preference
432 force_clpfd_inlist(El,[X]) :- !, El=X.
433 force_clpfd_inlist(El,FDList) :-
434 list_to_fdset(FDList,FDSET), El in_set FDSET.
435
436 % can fail due to overflows; one should not rely on it for soundness
437 clpfd_not_inlist(El,FDList) :-
438 try_post_constraint( (list_to_fdset(FDList,FDSET), fdset_complement(FDSET,C),El in_set C)).
439
440 % library(clpfd) on e. g. SWI does not support maximum/2 and minimum/2
441
442 :- if(\+ predicate_property(maximum(_,_), _)).
443 clpfd_maximum(_El,_List). % the current usage in maximum_of_set only uses this as additional constraint
444 :- else.
445 clpfd_maximum(El,List) :- %print(maximum(El,List)),nl,
446 maximum(El,List).
447 %force_post_constraint( maximum(El,List)). %, print(done(El)).
448 :- endif.
449
450 :- if(\+ predicate_property(minimum(_,_), _)).
451 clpfd_minimum(_El,_List). % the current usage in minimum_of_set only uses this as additional constraint
452 % TODO: provide a real implementation in SWI
453 :- else.
454 clpfd_minimum(El,List) :- %print(minimum(El,List)),nl,
455 %force_post_constraint( minimum(El,List)).
456 minimum(El,List).
457 :- endif.
458
459
460 :- assert_must_succeed((clpfd_interface:clpfd_if_then_else(pred_true,1,2,X), X==1)).
461 :- assert_must_succeed((clpfd_interface:clpfd_if_then_else(pred_false,1,2,X), X==2)).
462 :- assert_must_succeed_any((clpfd_interface:clpfd_if_then_else(_,21,21,X), X==21)).
463
464 clpfd_if_then_else(_,ThenValue,ElseValue,Value) :- ThenValue==ElseValue,!,
465 Value=ThenValue.
466 clpfd_if_then_else(PredRes,ThenValue,ElseValue,Value) :-
467 % TO DO: catch overflows and revert to simpler treatment then
468 element(Idx,[ThenValue,ElseValue],Value), % Idx=1 if Value=ThenValue; Idx=2 if Value=ElseValue
469 prop_12(PredRes,Idx). % if PredRes=pred_true -> Idx must be 1, 2 otherwise
470
471 :- block prop_12(-,-).
472 prop_12(P,V12) :- var(P),!,(V12=1 -> P=pred_true ; P=pred_false).
473 prop_12(pred_true,1).
474 prop_12(pred_false,2).
475
476 /*
477 catch(list_to_fdset([0,8589934592],R),E,true)
478 E= error(domain_error(integer_list,[0,8589934592]),domain_error(list_to_fdset([0,8589934592],_A),1,integer_list,[0,8589934592]))
479 domain_error
480 */
481
482
483 clpfd_reify_inlist(El,FDList,FDRes, Posted) :-
484 post_constraint2( (list_to_fdset(FDList,FDSET), (El in_set FDSET) #<=> FDRes), Posted).
485
486
487 try_post_constraint(_) :- preferences:preference(use_clpfd_solver,false),!.
488 :- if( environ(enable_time_out_for_constraints, true)).
489 try_post_constraint(C) :- % print(posting(C)),nl, %
490 catch(time_out_constraint(C,true), error(Err,_), check_error(Err,C)).
491 % Note: this will only catch exceptions that occur while posting !
492 % CLPFD integer overflow exceptions can still happen after posting :-(
493 :- else.
494 try_post_constraint(C) :- % print(posting(C)),nl, %
495 ? catch(C, error(Err,_), check_error(Err,C)).
496 :- endif.
497
498 post_constraint2(_,Posted) :-
499 preferences:preference(use_clpfd_solver,false),!,Posted=false.
500 :- if( environ(enable_time_out_for_constraints, true)).
501 post_constraint2(C,Posted) :- % print(posting(C)),nl, %
502 catch(time_out_constraint(C,(Posted=false)), error(Err,_), (check_error(Err,C),Posted=false)),
503 (Posted==false -> true ; Posted=true).
504 :- else.
505 post_constraint2(C,Posted) :- % print(posting(C)),nl, %
506 ? catch((C,Posted=true), error(Err,_), (check_error(Err,C),Posted=false)).
507 :- endif.
508
509
510 check_error(representation_error(ErrMsg),C) :-
511 is_clpfd_overflow_representation_error_msg(ErrMsg),
512 !,
513 print_message('Ignoring constraint (clpfd overflow):'),
514 print_message(C).
515 check_error(domain_error(_Type,_Val),C) :- !, print_message('Ignoring constraint (domain error):'),
516 % print(Type), print(' : '), print(Val), print(' : '),
517 print_message(C).
518 check_error(Err,C) :-
519 %print_message('Ignoring constraint (unknown error):'), print(Err), print(' : '), print_message(C),
520 add_error(clpfd_interface,'Ignoring constraint (unknown error):',Err:C).
521
522
523 :- assert_must_succeed((print('Is 64-bit: '),(clpfd_interface:is_64_bit_system -> print('Yes') ; print('NO')),nl)).
524
525 is_64_bit_system :-
526 % 268435456 = 2^28, will generate overflow in 32-bit system
527 catch(_X #= 268435456, error(representation_error(_),_), fail).
528
529
530 clpfd_overflow_error_message :- add_clpfd_overflow_message(error).
531 clpfd_overflow_warning_message :- add_clpfd_overflow_message(warning).
532
533 add_clpfd_overflow_message(error) :- !, clpfd_overflow_msg(M),
534 add_error(clpfd_overflow,M).
535 add_clpfd_overflow_message(message) :- !, clpfd_overflow_msg(M),
536 add_message(clpfd_overflow,M).
537 add_clpfd_overflow_message(silent) :- !, _X #= 1. % needed to somehow clear overflow in SICStus, see x>1 & y:NATURAL & y=x+x & z={y,x} (test 2142)
538 add_clpfd_overflow_message(warning) :- !, clpfd_overflow_msg(M),
539 add_warning(clpfd_overflow,M).
540 add_clpfd_overflow_message(Unknown) :-
541 add_internal_error('Illegal call: ',add_clpfd_overflow_message(Unknown)).
542
543 %clpfd_overflow_print_message :- clpfd_overflow_msg(M),write(user_error,M),nl(user_error).
544
545 integer_too_small_for_clpfd(X) :- current_prolog_flag(min_tagged_integer,Min), X<Min.
546 integer_too_large_for_clpfd(X) :- current_prolog_flag(max_tagged_integer,Max), X>Max.
547
548
549 % post_constraint3(CLPFD,PrologBackup,Posted)
550 post_constraint3(_,C,Posted) :- preferences:preference(use_clpfd_solver,false),!,Posted=false,call(C).
551 post_constraint3(C,PrologBackup,Posted) :- % print(posting(C,PrologBackup)),nl,
552 catch(
553 time_out_constraint((C,Posted=true),(Posted=false,PrologBackup)),
554 error(Err,_),
555 (check_error(Err,C),Posted=false,call(PrologBackup))).
556
557 % post_constraint(CLPFD,PrologBackup)
558 ?post_constraint(_,C) :- preferences:preference(use_clpfd_solver,false),!,call(C).
559 :- if(environ(enable_time_out_for_constraints, true)).
560 post_constraint(C,PrologBackup) :- % print(posting(C,PrologBackup)),nl,
561 catch(time_out_constraint(C,PrologBackup), error(Err,_), (check_error(Err,C),call(PrologBackup))).
562 :- else.
563 post_constraint(C,PrologBackup) :- % print(posting(C,PrologBackup)),nl,
564 catch(C, error(Err,_), (check_error(Err,C),call(PrologBackup))).
565 :- endif.
566
567 % no use_clpfd_solver check:
568 force_post_constraint(C) :- call(C). % to use fd_batch(C) we need to convert C to list
569 force_post_constraint(C,PrologBackup) :- % print(posting(C,PrologBackup)),nl,
570 catch(time_out_constraint(C,PrologBackup), error(Err,_), (check_error(Err,C),call(PrologBackup))).
571
572
573 :- if(\+ environ(enable_time_out_for_constraints, true)).
574 time_out_constraint(C,_) :- call(C). % to use fd_batch(C) we need to convert C to list
575 :- else.
576 % Note: time_out/3 is quite expensive !
577 time_out_constraint(C,PrologBackup) :- %% debug:new_pp(C,PP), %%
578 %%preferences:preference(time_out,CurTO), TO is 800 + (CurTO//100), time_out(C,TO,T),
579 preferences:preference(solver_strength,Strength),
580 TO is 1200 + Strength*200,
581 time_out(C,TO,T), %% debug:new_sol(C,PP), %%
582 (T==time_out -> print_message('Timeout when posting constraint:'), print_message(C),
583 (preferences:preference(fail_if_clpfd_timeout,true)
584 -> print_message('Assuming unsatisfiable !'),fail
585 ; call(PrologBackup))
586 ; true).
587 :- endif.
588
589
590 :- assert_must_succeed_any((clpfd:in(X,1..4), clpfd_interface:clpfd_domain(X,L,U), L==1, U==4)).
591 :- assert_must_succeed((clpfd_interface:clpfd_domain(3,L,U), L==3, U==3)).
592 clpfd_domain(Var,Low,Up) :- var(Var),!,
593 fd_min(Var,Low), fd_max(Var,Up).
594 % one could call fd_set(Var,Set), fdset_parts(Set,Min,Max,_Rest) or undocumented clpfd:fd_min_max(Var,Low,Up).
595 % used to check (preferences:preference(use_clpfd_solver,false) -> Low=inf,Up=sup ; fd_min(Var,Low), fd_max(Var,Up) ).
596 % but can also be called when CLPFD false for global_set values
597 %used to call: fd_dom(Var, Low..Up)). fd_dom will sometimes return {1} \/ 2..3 or something like that !
598 clpfd_domain(X,X,X).
599
600 % allows to have Up as inf
601 :- assert_must_succeed_any((clpfd_interface:clpfd_in_domain(X,1,4), clpfd_interface:clpfd_domain(X,L,U), L==1, U==4)).
602 :- assert_must_succeed_any((clpfd_interface:clpfd_in_domain(X,1,inf),
603 clpfd_interface:clpfd_domain(X,L,U), L==1, U==sup)).
604 clpfd_in_domain(Var,Low,Up) :- Up==inf,!, % we use inf as infinity not as infinum
605 Var #>= Low.
606 clpfd_in_domain(Var,Low,Up) :-
607 Var in Low..Up.
608
609
610 % find some element in the domain of a FD variable
611 :- assert_must_succeed((clpfd_interface:clpfd_some_element_in_domain(1,X), X==1)).
612 :- assert_must_succeed_any((clpfd:in(X,1..4), clpfd_interface:clpfd_some_element_in_domain(X,_))).
613 :- assert_must_fail((clpfd:in(X,1..4), clpfd:in(Y,5..6),
614 clpfd_interface:clpfd_some_element_in_domain(X,E),
615 clpfd_interface:clpfd_some_element_in_domain(Y,E))).
616 clpfd_some_element_in_domain(Var,El) :- nonvar(Var),!, El=Var.
617 clpfd_some_element_in_domain(Var,El) :- fd_set(Var,Set), fdset_parts(Set,Min,Max,_Rest),
618 (number(Min) -> El=Min ; number(Max),El=Max ; El=0).
619 /* the latter should always succeed; here are some example calls:
620 | ?- X #\= 3, fd_set(X,S), fdset_parts(S,Min,Max,Parts).
621 S = [[inf|2],[4|sup]],
622 Min = inf,
623 Max = 2,
624 Parts = [[4|sup]],
625
626 | ?- fd_set(X,S), fdset_parts(S,Min,Max,Parts).
627 S = [[inf|sup]],
628 Min = inf,
629 Max = sup,
630 Parts = []
631 */
632
633
634 % succeed if we have a number or a CLPFD Var whose upper value is bounded
635 :- assert_must_succeed_any((clpfd:in(X,1..4), clpfd_interface:clpfd_max_bounded(X))).
636 :- assert_must_succeed(clpfd_interface:clpfd_max_bounded(4)).
637 :- assert_must_fail( clpfd_interface:clpfd_max_bounded(_) ).
638 clpfd_max_bounded(Var) :- var(Var), !, fd_max(Var,Up), number(Up).
639 clpfd_max_bounded(N) :- number(N).
640
641 :- assert_must_succeed(clpfd_interface:clpfd_can_match(1,1)).
642 :- assert_must_succeed(clpfd_interface:clpfd_can_match(11,_X)).
643 :- assert_must_succeed(clpfd_interface:clpfd_can_match(_X,22)).
644 :- assert_must_succeed(clpfd_interface:clpfd_can_match(X,X)).
645 :- assert_must_fail(clpfd_interface:clpfd_can_match(21,22)).
646 :- assert_must_fail((dif(A,B),clpfd_interface:clpfd_can_match(A,B))).
647 % check if two numbers or fd variables can match without unifying (as this could trigger propagations)
648 % TODO: merge with fd_frozen_dif
649 clpfd_can_match(Var1,Var2) :- var(Var1),!, (var(Var2) -> clpfd_var_can_unify(Var1,Var2) ; clpfd_can_match_nr(Var1,Var2)).
650 clpfd_can_match(Nr1,Var2) :- var(Var2),!,clpfd_can_match_nr(Var2,Nr1).
651 clpfd_can_match(Nr1,Nr2) :- Nr1=Nr2.
652 clpfd_can_match_nr(Var,Nr) :- % is it also worthwhile to check for frozen_dif here ? A #>10, B =15, B #\=A, clpfd_interface:clpfd_can_match(A,B) fails without it
653 fd_set(Var,FDS), Nr in_set FDS.
654
655 clpfd_var_can_unify(Var1,Var2) :-
656 (Var1==Var2 -> true
657 ; fd_set(Var1,FDS1), fd_set(Var2,FDS2), fdset_intersect(FDS1,FDS2),
658 ? \+ kernel_dif:frozen_dif(Var1,Var2)
659 ).
660
661 % check if FD variables or numbers have common possible value
662 % called by fd_frozen_dif
663 :- assert_must_succeed_any((clpfd:in(X,1..4), clpfd_interface:clpfd_can_intersect(X,X))).
664 :- assert_must_succeed_any((clpfd:in(X,1..4), clpfd:in(Y,0..1), clpfd_interface:clpfd_can_intersect(X,Y))).
665 :- assert_must_succeed_any((clpfd:in(X,1..4), clpfd:in(Y,1..1), clpfd_interface:clpfd_can_intersect(X,Y))).
666 :- assert_must_succeed((clpfd:in(X,4..4), clpfd:in(Y,4..4), clpfd_interface:clpfd_can_intersect(X,Y))).
667 :- assert_must_succeed_any((clpfd:in(X,4..4), clpfd:in(Y,0..6), clpfd_interface:clpfd_can_intersect(X,Y))).
668 :- assert_must_succeed_any((clpfd:in(X,1..4), clpfd_interface:clpfd_can_intersect(X,_))).
669 :- assert_must_succeed_any( clpfd_interface:clpfd_can_intersect(_X,_Y)).
670 :- assert_must_fail((clpfd:in(X,2..4), clpfd:in(Y,0..1), clpfd_interface:clpfd_can_intersect(X,Y))).
671 :- assert_must_fail((clpfd:in(X,2..4), clpfd:in(Y,0..0), clpfd_interface:clpfd_can_intersect(X,Y))).
672 :- assert_must_fail((clpfd:in(X,1..1), clpfd:in(Y,0..0), clpfd_interface:clpfd_can_intersect(X,Y))).
673 clpfd_can_intersect(Number1,NrOrVar2) :- nonvar(Number1),!,
674 (nonvar(NrOrVar2) -> Number1==NrOrVar2
675 ; fd_set(NrOrVar2,FDS2), fdset_member(Number1,FDS2)).
676 clpfd_can_intersect(Var1,Number2) :- nonvar(Number2),!,
677 fd_set(Var1,FDS1), fdset_member(Number2,FDS1).
678 clpfd_can_intersect(Var1,Var2) :-
679 fd_set(Var1,FDS1), fd_set(Var2,FDS2), fdset_intersect(FDS1,FDS2).
680
681 % check if we can currently determine an integer to be greater or equal to a given number
682 clpfd_check_geq_nr(X,Nr) :-
683 number(X),!,
684 X>=Nr.
685 clpfd_check_geq_nr(X,_) :-
686 (nonvar(X) % something like X+Y
687 ; preferences:preference(use_clpfd_solver,false)),
688 !,fail.
689 clpfd_check_geq_nr(X,Nr) :-
690 fd_min(X,Low), number(Low), Low>=Nr.
691
692 :- assert_must_succeed_any((clpfd:in(X,1..4), clpfd_interface:clpfd_size(X,Sz), Sz==4)).
693 :- assert_must_succeed_any((clpfd:in(X,1..1), clpfd_interface:clpfd_size(X,Sz), Sz==1)).
694 clpfd_size(Var,Size) :- number(Var),!, Size=1. % fd_size(1152921504606846976,X) creates overflow in SICStus 4.7
695 clpfd_size(Var,Size) :- fd_size(Var,Size). % also works for free variables, returning sup
696 %clpfd_size(Var,Size) :- (preferences:preference(use_clpfd_solver,false)
697 % -> Size = sup ; fd_size(Var,Size) ).
698
699 :- assert_must_succeed(clpfd_interface:clpfd_alldifferent([1,2,3])).
700 :- assert_must_succeed((preferences:preference(use_clpfd_solver,false) -> true ; clpfd:in(X,1..4), clpfd_interface:clpfd_alldifferent([1,X,2,3]), X==4)).
701 :- assert_must_succeed(clpfd_interface:all_dif([1,2,3],[])).
702 :- assert_must_fail(clpfd_interface:clpfd_alldifferent([1,2,3,2])).
703 :- assert_must_fail((preferences:preference(use_clpfd_solver,true), clpfd:in(X,1..3), clpfd_interface:clpfd_alldifferent([1,X,2,3]))).
704 :- assert_must_fail(clpfd_interface:all_dif([1,2,3,2],[])).
705
706 clpfd_alldifferent([]) :- !.
707 clpfd_alldifferent(L) :- post_constraint(all_different(L),all_dif(L,[])).
708
709 all_dif([],_).
710 all_dif([H|T],All) :- all_dif_aux(All,H), all_dif(T,[H|All]).
711
712 all_dif_aux([],_).
713 all_dif_aux([H|T],X) :- dif(H,X), all_dif_aux(T,X).
714
715 /*
716 clpfd_labeling(Variables) :-
717 (preferences:preference(use_clpfd_solver,false) -> true
718 ; labeling([ffc,enum],Variables)). %ff, enum
719 */
720
721 % a version of labeling that performs randomized enumeration if requested
722 % Currently, random enumeration does not support variable selection options
723 % TODO: Maybe we should only randomize enumeration on "large enough" intervals
724 clpfd_randomised_labeling([],ListOfVars) :-
725 preferences:get_preference(randomise_enumeration_order,true)
726 -> clpfd_randomised_labeling_aux(ListOfVars)
727 ? ; labeling([],ListOfVars).
728 clpfd_randomised_labeling([Op|Ops],ListOfVars) :-
729 labeling([Op|Ops],ListOfVars).
730
731 clpfd_randomised_labeling_aux([]).
732 clpfd_randomised_labeling_aux([Var|Vars]) :-
733 clpfd_randomised_in_domain(Var),
734 clpfd_randomised_labeling_aux(Vars).
735
736 :- use_module(library(random)).
737 :- use_module(extension('random_permutations/random_permutations'),
738 [enum_fd_random/3]).
739
740 clpfd_randomised_in_domain(Var) :-
741 clpfd_domain(Var,Low,Up),
742 (number(Low),number(Up)
743 -> enum_fd_random(Var,Low,Up)
744 ; add_internal_error('Unbounded FD variable: ',clpfd_randomised_in_domain(Var)),
745 %trace, kernel_waitflags:get_fd_priority(Var,_),
746 fail
747 ).
748
749
750 %:- use_module(library(lists),[reverse/2]).
751 %clpfd_reverse_labeling(Vars) :- clpfd_reverse_labeling(Vars,[ffc,enum]).
752 %% label a list of variables which was reversed:
753 %clpfd_reverse_labeling(Variables,Opt) :- var(Variables),!,
754 % add_internal_error('Must be list of variables: ',clpfd_reverse_labeling(Variables,Opt)).
755 %clpfd_reverse_labeling(Variables,Options) :- !,
756 % reverse(Variables,RevV),
757 % clpfd_labeling(RevV,Options).
758
759 clpfd_labeling(Variables,Options) :-
760 % Options = [ffc,enum]
761 catch(labeling(Options,Variables), error(instantiation_error,Err), (
762 print(Err),nl,
763 % this can happen when CLP(FD) has a time-out for other constraints
764 add_error(clpfd_interface,'CLP(FD) Variables not set up for ',labeling(Options,Variables))
765 )).
766
767
768 clpfd_in_domain(Variable) :- !,
769 ? catch(indomain(Variable), error(instantiation_error,Err), (
770 print(Err),nl,
771 % this can happen when CLP(FD) has a time-out for other constraints
772 add_error(clpfd_interface,'CLP(FD) Variables not set up for ',indomain(Variable))
773 )).
774
775
776 clpfd_degree(Variable,Degree) :- fd_degree(Variable,Degree). % can be called with plain variables and with numbers
777
778 % a new predicate to obtain the next variable that would be enumerated
779 % (useful if you want to interleave other labeling with CLPFD labeling)
780
781 :- assert_must_succeed((X in 1..3, Y in 3..5, X #> Z, clpfd_interface:clpfd_get_next_variable_to_label([Y,2,X,3],V),V==X, X=3, Y=3, Z=2)).
782 clpfd_get_next_variable_to_label(Variables,Var) :-
783 clpfd_get_next_variable_to_label(Variables,Var,ffc).
784
785 :- if(predicate_property(clpfd:'$fd_delete'(_, _, _), _)).
786 % possible options : ff, ffc, step, enum, bisect, median, ...
787 clpfd_get_next_variable_to_label(Variables,Var,Opt) :- Variables \= [], % there is a segmentation fault if we call fd_delete with empty list
788 % this also causes segmentation fault:
789 % X in 1..2 , Y in 3..5, clpfd_get_next_variable_to_label([2,3,Y,2,X],Var,ffc). rlwrap: warning: sicstus crashed, killed by SIGSEGV.
790 clpfd:'$fd_delete'(Variables,Var,Opt).
791 :- else.
792 clpfd_get_next_variable_to_label(Variables,Var,ffc) :-
793 clpfd_get_next_variable_to_label_ffc(Variables,Var,_).
794 % a version of the above just for ffc, re-implemented by hand so as not to be dependent on internal predicates of clpfd
795 % also: it returns the remaining variables (filters out non-variables)
796 % but it can be much slower than clpfd:$fd_delete (e.g., NQueens50)
797 clpfd_get_next_variable_to_label_ffc([H|T],Var,RestV) :-
798 (get_fd_info(H,HI) -> get_next_aux(T,H,HI,Var,RestV)
799 %,((clpfd_get_next_variable_to_label([H|T],VV,ffc), VV\==Var) -> print(different_choice(Var,VV)),nl , tools_printing:print_vars([H|T]) ; true)
800 ; clpfd_get_next_variable_to_label_ffc(T,Var,RestV)
801 ).
802 % , tools_printing:print_vars([H|T]),print(sel(Var,RestV)),nl.
803
804 get_next_aux([],Var,_,Var,[]).
805 get_next_aux([H|T],VarSoFar,VInfo,Var,Rest) :-
806 (get_fd_info(H,HI)
807 -> (HI @< VInfo -> Rest = [VarSoFar|TRest], get_next_aux(T,H,HI,Var,TRest)
808 ; Rest = [H|TRest], get_next_aux(T,VarSoFar,VInfo,Var,TRest)
809 )
810 ; get_next_aux(T,VarSoFar,VInfo,Var,Rest)).
811
812 get_fd_info(Var,(Sz,NDg)) :- fd_size(Var,Sz), Sz \= 1, % note: we have 2 @<sup
813 % kernel_waitflags:size_of_attached_goals(Var,Dg),
814 fd_degree(Var,Dg),
815 NDg is -Dg. % negate to give higher priority to goals with high degree
816 :- endif.
817
818
819 catch_clpfd_overflow_call1(Call) :- catch_clpfd_overflow_call3(Call,error,fail).
820 ?catch_clpfd_overflow_call2(Call,Handler) :- catch_clpfd_overflow_call3(Call,error,Handler).
821 catch_clpfd_overflow_call3(Call,Type,Handler) :-
822 ? catch(Call,
823 error(_ErrMsg,ErrTerm), % the ErrMsg can be representation_error or domain_error
824 handle_representation_error(ErrTerm,Type,Handler)).
825
826 handle_representation_error(ErrTerm,Type,Call) :-
827 (is_clpfd_overflow_representation_error(ErrTerm,_)
828 -> add_clpfd_overflow_message(Type),
829 Call
830 ; throw(representation_error(ErrTerm))).
831
832 :- use_module(debug,[debug_println/2]).
833 catch_and_ignore_clpfd_overflow(PP,Call) :-
834 catch(Call,
835 error(_,ErrTerm),
836 (is_clpfd_overflow_representation_error(ErrTerm,_)
837 -> debug_println(19,ignoring_clpfd_overflow(PP,ErrTerm))
838 ; throw(representation_error(ErrTerm))
839 )).
840
841
842 % -----------------------
843 % a debugging utility:
844
845 % observe changes in domains for a CLP(FD) variable:
846 clpfd_observe(Variable,Name) :- nonvar(Name),!,
847 fd_global(clpfd_observe(Variable,Name),inst(0),[dom(Variable)]).
848 clpfd_observe(Variable,Name) :-
849 add_internal_error('Illegal var name:',clpfd_observe(Variable,Name)).
850
851 :- multifile clpfd:dispatch_global/4.
852 clpfd:dispatch_global(clpfd_observe(Var,Name), inst(Nr), inst(N1), Actions) :- !,
853 fd_dom(Var,Dom),
854 format(' -(~w)-> clpfd var ~w : ~w : ~w~n',[Nr,Name,Var,Dom]),
855 N1 is Nr+1,
856 Actions=[].
857
858 % observe bindings in a B state:
859 clpfd_observe_state([]).
860 clpfd_observe_state([bind(Name,Var)|T]) :-
861 clpfd_observe_value(Var,Name),
862 clpfd_observe_state(T).
863
864 :- block clpfd_observe_value(-,?).
865 clpfd_observe_value(int(Var),Name) :- !, clpfd_observe(Var,Name).
866 clpfd_observe_value(fd(Var,_T),Name) :- !, clpfd_observe(Var,Name).
867 % TODO: more types
868 clpfd_observe_value(_,_).
869
870 /*
871 Testing for how large the integers can be, 32-bit system:
872 | ?- X is integer(2**30), Y#=X+1.
873 ! Representation error in argument 2 of user:'t=u+c'/3
874 ! CLPFD integer overflow
875 ! goal: 't=u+c'(_102,1073741824,1)
876 | ?- X is integer(2**30), Y#=X.
877 X = 1073741824,
878 Y = 1073741824 ?
879 64-bit system:
880 | ?- X is integer(2**60), Y#=X.
881 ! Representation error in argument 2 of user:(#=)/2
882 ! CLPFD integer overflow
883 ! goal: _413#=1152921504606846976
884
885 | ?- X is integer(2**60)-1, Y#=X.
886 X = 1152921504606846975,
887 Y = 1152921504606846975 ?
888 yes
889 */
890
891 % ---------------
892
893 % a few other arithmetic operators provided in external functions
894
895 :- assert_must_succeed(clpfd_interface:clpfd_gcd(6,3,3)).
896 :- assert_must_succeed(clpfd_interface:clpfd_gcd(6,-3,3)).
897 :- assert_must_succeed((clpfd_interface:clpfd_gcd(X,Y,R), X=12, Y=10, R==2)).
898 :- assert_must_fail((preferences:preference(use_clpfd_solver,true),clpfd_interface:clpfd_gcd(X,_,R), X=12, R==13)).
899 :- assert_must_fail((preferences:preference(use_clpfd_solver,true),clpfd_interface:clpfd_gcd(_,Y,R), Y=12, R==13)).
900 % Greatest Common Divisor (largest common factor)
901 clpfd_gcd(X,Y,R) :-
902 gcd2(X,Y,R),
903 (var(R) -> try_post_constraint((R #>0, R #=< abs(X), R#=< abs(Y))) ; true).
904 :- block gcd2(?,-,?),gcd2(-,?,?).
905 gcd2(X,Y,R) :- R is gcd(X,Y).
906
907 :- assert_must_succeed(clpfd_interface:clpfd_lcm(6,3,6)).
908 :- assert_must_succeed(clpfd_interface:clpfd_lcm(6,-3,6)).
909 :- assert_must_succeed((clpfd_interface:clpfd_lcm(X,Y,R), X=12, Y=10, R==60)).
910 :- assert_must_fail((preferences:preference(use_clpfd_solver,true),clpfd_interface:clpfd_lcm(X,_,R), X=12, R==11)).
911 :- assert_must_fail((preferences:preference(use_clpfd_solver,true),clpfd_interface:clpfd_lcm(_,Y,R), Y=12, R==11)).
912 % Least Common Multiple
913 clpfd_lcm(X,Y,R) :-
914 lcm2(X,Y,R),
915 (var(R) -> try_post_constraint((R #>=abs(X), R #>= abs(Y), R#=< abs(X*Y))) ; true).
916
917 :- block lcm2(?,-,?),lcm2(-,?,?).
918 lcm2(X,Y,R) :- CD is gcd(X,Y), R is (abs(X*Y) // CD).
919
920 :- assert_must_succeed((clpfd_interface:clpfd_abs(6,R), R == 6)).
921 :- assert_must_succeed((clpfd_interface:clpfd_abs(Y,R), Y = -6, R == 6)).
922 :- assert_must_fail((preferences:preference(use_clpfd_solver,true),clpfd_interface:clpfd_abs(_,R), R = -1)).
923 :- assert_must_fail((preferences:preference(use_clpfd_solver,true),clpfd_interface:clpfd_abs(X,R), R=0, X \== 0)).
924 % Absolute value
925 clpfd_abs(X,R) :- preferences:preference(use_clpfd_solver,true),!,
926 clpfd_eq_expr(R,abs(X)).
927 clpfd_abs(X,R) :- when(nonvar(X),R is abs(X)).
928
929 :- assert_must_succeed((clpfd_interface:clpfd_sign(6,R), R == 1)).
930 :- assert_must_succeed((clpfd_interface:clpfd_sign(Y,R), Y = -6, R == -1)).
931 :- assert_must_succeed((clpfd_interface:clpfd_sign(Y,R), Y = 0, R == 0)).
932 :- assert_must_fail((preferences:preference(use_clpfd_solver,true),clpfd_interface:clpfd_sign(_,R), R = -2)).
933 :- assert_must_fail((preferences:preference(use_clpfd_solver,true),clpfd_interface:clpfd_sign(X,R), R=0, X \== 0)).
934
935 clpfd_sign(X,R) :-
936 sign2(X,R),
937 (var(R) -> try_post_constraint((R in -1..1, X #> 0 #<=> R #= 1, X #< 0 #<=> R #= -1, X #= 0 #<=> R #= 0)) ; true).
938
939 :- block sign2(-,?).
940 sign2(X,R) :- R is sign(X).
941