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