| 1 | | % (c) 2009-2019 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_geq2/3, |
| 12 | | clpfd_geq/3, clpfd_gt/3, clpfd_leq/3, clpfd_lt/3, |
| 13 | | clpfd_leq_expr/2, clpfd_lt_expr/2, |
| 14 | | clpfd_inrange/3, clpfd_inrange/4, |
| 15 | | clpfd_not_inrange/3, clpfd_not_in_non_empty_range/3, |
| 16 | | clpfd_sum/2, |
| 17 | | clpfd_inlist/2, clpfd_not_inlist/2, clpfd_reify_inlist/3, force_clpfd_inlist/2, |
| 18 | | clpfd_minimum/2, clpfd_maximum/2, |
| 19 | | clpfd_if_then_else/4, |
| 20 | | clpfd_domain/3, clpfd_size/2, |
| 21 | | clpfd_some_element_in_domain/2, |
| 22 | | clpfd_max_bounded/1, |
| 23 | | clpfd_can_match/2, |
| 24 | | clpfd_check_geq_nr/2, |
| 25 | | clpfd_alldifferent/1, |
| 26 | | %clpfd_labeling/1, % not used at the moment |
| 27 | | clpfd_degree/2, |
| 28 | | clpfd_in_domain/1, clpfd_labeling/2, |
| 29 | | clpfd_can_intersect/2, |
| 30 | | %clpfd_reverse_labeling/1, clpfd_reverse_labeling/2, |
| 31 | | clpfd_get_next_variable_to_label/2, clpfd_get_next_variable_to_label/3, |
| 32 | | %clpfd_get_next_variable_to_label_ffc/3, |
| 33 | | is_64_bit_system/0, clpfd_overflow_error_message/0, clpfd_overflow_warning_message/0, |
| 34 | | integer_too_large_for_clpfd/1, integer_too_small_for_clpfd/1, |
| 35 | | catch_clpfd_overflow_call1/1, catch_clpfd_overflow_call2/2, |
| 36 | | computable_arith_expression/1, |
| 37 | | clpfd_randomised_labeling/2, clpfd_randomised_in_domain/1]). |
| 38 | | |
| 39 | | :- use_module(library(clpfd)). |
| 40 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
| 41 | | :- if(\+ environ(disable_chr, true)). |
| 42 | | :- use_module(chrsrc(chr_integer_inequality)). |
| 43 | | :- endif. |
| 44 | | |
| 45 | | |
| 46 | | :- if((current_prolog_flag(version_data,sicstus(4,X,Y,_,_)),X<3,Y<3)). |
| 47 | | % -------- patch provided by SICS ----------- |
| 48 | | % solves lost solution in CLP(FD) when calling: |
| 49 | | % when(nonvar(X),member(Y,[1,2])), X in 1..2, X in 2..3. |
| 50 | | % patch provided 23rd June 2012 for SICS 4.2.1 |
| 51 | | % bug cause ProB to miss solutions in e.g. following set comprehension: |
| 52 | | % {xx | xx:{1|->TRUE,2|->TRUE,2|->FALSE} & (xx : {(2|->TRUE),(2|->FALSE),(3|->TRUE)} or xx : {(1|->TRUE),(1|->FALSE),(2|->TRUE),(2|->FALSE),(3|->TRUE),(3|->FALSE)})} |
| 53 | | :- set_prolog_flag(redefine_warnings,proceed). |
| 54 | | clpfd:propagate_interval_chk(Pruned, Min, Max) :- |
| 55 | | clpfd:'$fd_in_interval'(Pruned, Min, Max, 1), !, % 20120623 |
| 56 | | clpfd:'$fd_evaluate_indexical'(RC, Global), |
| 57 | | clpfd:evaluate(RC, Global). |
| 58 | | clpfd:propagate_interval_chk(Pruned, Min, Max) :- |
| 59 | | clpfd:arg_attribute(Pruned, _, in(Pruned,Min..Max), 1), !, |
| 60 | | fail. |
| 61 | | clpfd:propagate_interval_chk(_, _, _). |
| 62 | | |
| 63 | | clpfd:prune_and_propagate_chk(Pruned, Set) :- |
| 64 | | clpfd:'$fd_in_set'(Pruned, Set, 1), !, % 20120623 |
| 65 | | clpfd:'$fd_evaluate_indexical'(RC, Global), |
| 66 | | clpfd:evaluate(RC, Global). |
| 67 | | clpfd:prune_and_propagate_chk(Pruned, Set) :- |
| 68 | | clpfd:arg_attribute(Pruned, _, in_set(Pruned,Set), 1), !, |
| 69 | | fail. |
| 70 | | clpfd:prune_and_propagate_chk(_, _). |
| 71 | | %:- set_prolog_flag(redefine_warnings,on). |
| 72 | | % ---------- end patch --------------- |
| 73 | | :- endif. |
| 74 | | |
| 75 | | |
| 76 | | %:- use_module(typechecker). |
| 77 | | :- use_module(tools). |
| 78 | | :- use_module(preferences). |
| 79 | | :- use_module(library(timeout)). |
| 80 | | :- use_module(error_manager). |
| 81 | | :- use_module(self_check). |
| 82 | | |
| 83 | | :- use_module(module_information,[module_info/2]). |
| 84 | | :- module_info(group,kernel). |
| 85 | | :- module_info(description,'Provide interface to CLP(FD), with Prolog fallback in case of errors or when CLP(FD) turned off.'). |
| 86 | | |
| 87 | | :- meta_predicate try_post_constraint(0). |
| 88 | | :- meta_predicate post_constraint(0,0). |
| 89 | | :- meta_predicate post_constraint2(0,*). |
| 90 | | :- meta_predicate time_out_constraint(0,0). |
| 91 | | %:- meta_predicate force_post_constraint(0). |
| 92 | | %:- meta_predicate force_post_constraint(0,0). |
| 93 | | |
| 94 | | |
| 95 | | % Note: clpfd_eq is sometimes called with arithmetic expressions (treatment of plus/minus/...) |
| 96 | | % does not do the computable_arith_expression check |
| 97 | | clpfd_eq(E1,E2) :- simple(E1), simple(E2), % was (before 29.8.2014): number(E1),number(E2), |
| 98 | | !, |
| 99 | | E1=E2. |
| 100 | | clpfd_eq(E1,E2) :- |
| 101 | | (preferences:preference(use_chr_solver,true) -> chr_eq(E1,E2) ; true), |
| 102 | | try_post_constraint( E1 #= E2 ). |
| 103 | | |
| 104 | | clpfd_neq(E1,E2) :- number(E1),!, |
| 105 | | (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 |
| 106 | | clpfd_neq(E1,E2) :- number(E2),!, % no need to post dif constraint in clpfd mode |
| 107 | | post_constraint( E1 #\= E2, dif(E1,E2)). |
| 108 | | clpfd_neq(E1,E2) :- |
| 109 | | % Note: | ?- X #\= Y, Y #=X. --> does not fail; hence we also execute dif(E1,E2) in CLPFD mode ! |
| 110 | | % We might be able to skip calling dif, if we enable the CHR solver by default |
| 111 | | % Let's try it: only set up dif if CHR is disabled! |
| 112 | | (preferences:preference(use_chr_solver,true) -> chr_neq(E1,E2) ; dif(E1,E2)), |
| 113 | | try_post_constraint(E1 #\= E2). |
| 114 | | % clpfd_domain(E1,D1,D2), clpfd_domain(E2,B1,B2), print(dom(D1:D2,B1:B2)),nl. |
| 115 | | |
| 116 | | % set up a dif co-routine only if necessary; assumption: E1,E2 are either number or variable |
| 117 | | dif_when_necesssary(E1,E2) :- %print(dif_when_necesssary(E1,E2)),nl, |
| 118 | | var(E1),var(E2),!, dif(E1,E2). |
| 119 | | dif_when_necesssary(_,_). |
| 120 | | |
| 121 | | % this will force Y to be nonzero |
| 122 | | clpfd_eq_div(E1,X,Y) :- post_constraint( E1 #= X/Y, prolog_eq(E1,X//Y)), % truncated division -1 // 4 = 0 |
| 123 | | propagate_div_eq_eq(E1,X,Y). |
| 124 | | clpfd_eq_fdiv(E1,X,Y) :- post_constraint( E1 #= X div Y, prolog_eq(E1,X div Y)). % floored division -1 div 4 = -1 |
| 125 | | |
| 126 | | % certain == propagation rules not done by CLPFD |
| 127 | | propagate_div_eq_eq(E1,X,Y) :- |
| 128 | | (var(E1),X==Y |
| 129 | | -> %print(setting1(E1,X,Y)),nl, |
| 130 | | E1=1 % X/X can only be 1 or undefined when X=0 |
| 131 | | ; true). |
| 132 | | % we could check if E1==X --> Y=1 if X /= 0 |
| 133 | | |
| 134 | | % this waits until we are sure Y is not zero |
| 135 | | clpfd_eq_guarded_div(E1,X,Y) :- |
| 136 | | post_constraint3((E1 #= X/YY,MY in 0..1, Y #= MY*YY), prolog_eq(E1,X//Y),Posted), % Y can either be 0 or equal to YY |
| 137 | | % this is better than the previous solution: |
| 138 | | % post_constraint(Y#\=0 #=> YY#=Y, prolog_eq(Y,YY)). |
| 139 | | % however, x:44..77 & E : 1..5555 & E = x/y & y:0..4 only restricts E to 1..77, not 11..77 |
| 140 | | % what is still missing is propagating upper bounds of Y to YY |
| 141 | | % Y in 0..4, M in 0..1, YY in 1..77, Y #=M*YY |
| 142 | | % with this propagation below, we at least obtain propagation for x:44..77 & E : 1..5555 & y:0..4 & E = x/y |
| 143 | | % what we need is continously propagating the bounds from Y to YY (but not vice versa for 0) |
| 144 | | % maybe we can achieve this using indexicals ?? |
| 145 | | (Posted==true |
| 146 | | -> fd_max(Y,YUp), (number(YUp) -> YY #=< YUp ; true), |
| 147 | | fd_min(Y,YLow), (number(YLow) -> YY #>= YLow ; true), |
| 148 | | propagate_div_eq_eq(E1,X,Y) |
| 149 | | ; true). |
| 150 | | |
| 151 | | % now a similar solution for floored division |
| 152 | | clpfd_eq_guarded_fdiv(E1,X,Y) :- |
| 153 | | post_constraint3((E1 #= X div YY,MY in 0..1, Y #= MY*YY), prolog_eq(E1,X div Y),_Posted). |
| 154 | | % TO DO: add propagation like above or using indexicals |
| 155 | | |
| 156 | | % do we need to instantiate YY if Y becomes 0 ?? |
| 157 | | %:- block copy_divisor(-,?). |
| 158 | | %copy_divisor(Y,Y). |
| 159 | | |
| 160 | | |
| 161 | | |
| 162 | | % we check whether we have simple expressions of the form X = Y OP Z |
| 163 | | % in this case it is better to call ProB's implementations, as they have stronger propagation |
| 164 | | % (e.g., 0 = X-Y => X=Y or 1 = X-Y => X/=Y) |
| 165 | | clpfd_eq_expr_optimized(CLPFD_Expr1,CLPFD_Expr2) :- |
| 166 | | (simple(CLPFD_Expr1) -> call_eq_expr1(CLPFD_Expr2,CLPFD_Expr1) |
| 167 | | ; simple(CLPFD_Expr2) -> call_eq_expr2(CLPFD_Expr1,CLPFD_Expr2) |
| 168 | | ; clpfd_eq_expr_nonsimple(CLPFD_Expr1,CLPFD_Expr2)). |
| 169 | | |
| 170 | | :- use_module(kernel_dif). |
| 171 | | call_eq_expr1(CLPFD_Expr2,CLPFD_Expr1) :- |
| 172 | | (simple(CLPFD_Expr2) -> %print(unify(CLPFD_Expr2,CLPFD_Expr1)),nl, translate:print_clpfd_variable(CLPFD_Expr2),nl, translate:print_clpfd_variable(CLPFD_Expr1),nl, |
| 173 | | % first check if we have a pending dif; unification could trigger CLPFD enumeration |
| 174 | | ((var(CLPFD_Expr1),kernel_dif:frozen_dif(CLPFD_Expr2,CLPFD_Expr1)) -> /* print(dif),nl,*/ fail ; true), |
| 175 | | CLPFD_Expr2=CLPFD_Expr1 |
| 176 | | ; call_eq_expr2(CLPFD_Expr2,CLPFD_Expr1)). |
| 177 | | |
| 178 | | % first arg not simple, second arg simple |
| 179 | | call_eq_expr2(CLPFD_Expr2,CLPFD_Expr1) :- CLPFD_Expr2 = -(A,B),simple(A),simple(B),!, |
| 180 | | %kernel_objects:int_minus(int(A),int(B),int(CLPFD_Expr1)). % has special propagation rules |
| 181 | | (number(A),number(B) -> CLPFD_Expr1 is CLPFD_Expr2 |
| 182 | | ; clpfd_eq_expr_nonsimple(CLPFD_Expr2,CLPFD_Expr1), |
| 183 | | propagate_zero(A,B,CLPFD_Expr1)). |
| 184 | | call_eq_expr2(CLPFD_Expr2,CLPFD_Expr1) :- CLPFD_Expr2 = +(A,B),simple(A),simple(B),!, |
| 185 | | (number(A),number(B) -> CLPFD_Expr1 is CLPFD_Expr2 |
| 186 | | ; clpfd_eq_expr_nonsimple(CLPFD_Expr1,CLPFD_Expr2), |
| 187 | | propagate_zero(CLPFD_Expr1,A,B)). |
| 188 | | %kernel_objects:int_plus(int(A),int(B),int(CLPFD_Expr1)). % has special propagation rules |
| 189 | | call_eq_expr2(CLPFD_Expr2,CLPFD_Expr1) :- |
| 190 | | (computable_arith_expression(CLPFD_Expr2) -> CLPFD_Expr1 is CLPFD_Expr2 |
| 191 | | ; clpfd_eq_expr_nonsimple(CLPFD_Expr1,CLPFD_Expr2)). |
| 192 | | |
| 193 | | % a propagation rule not done by CLP(FD) |
| 194 | | :- block propagate_zero(-,-,-). |
| 195 | | propagate_zero(Sum,A,B) :- % print(prop_zero(Sum,A,B)),nl, |
| 196 | | (A==0 -> Sum=B ; B==0 -> Sum=A ; true). |
| 197 | | |
| 198 | | % eq_expr takes expressions as arguments |
| 199 | | clpfd_eq_expr(E1,E2) :- simple(E1),!, |
| 200 | | (simple(E2) -> E1=E2 |
| 201 | | ; computable_arith_expression(E2) -> E1 is E2 |
| 202 | | ; clpfd_eq_expr_nonsimple(E1,E2)). |
| 203 | | clpfd_eq_expr(E1,E2) :- simple(E2),computable_arith_expression(E1),!, E2 is E1. |
| 204 | | clpfd_eq_expr(E1,E2) :- clpfd_eq_expr_nonsimple(E1,E2). |
| 205 | | |
| 206 | | clpfd_eq_expr_nonsimple(E1,E2) :- |
| 207 | | (preferences:preference(use_chr_solver,true) -> chr_eq(E1,E2) ; true), |
| 208 | | post_constraint( E1 #= E2, prolog_eq(E1,E2)). |
| 209 | | %% post_constraint( E1 #= E2). % Used instead of line below because of serious bug in SICStus 4.1.3 |
| 210 | | % BUG: X*X #= 100, X #= 9. succeeds ! |
| 211 | | |
| 212 | | :- assert_must_succeed((clpfd_interface:prolog_eq(X,2+1),X==3)). |
| 213 | | :- assert_must_succeed((clpfd_interface:prolog_eq(4-1,X),X==3)). |
| 214 | | :- assert_must_succeed((clpfd_interface:prolog_eq(5-2,(2*2)-Y),Y=1)). |
| 215 | | :- assert_must_fail((clpfd_interface:prolog_eq(5-2,(2*2)-Y),Y=0)). |
| 216 | | prolog_eq(A,B) :- simple(A),!, when(ground(B), A is B). |
| 217 | | prolog_eq(A,B) :- simple(B),!, when(ground(A), B is A). |
| 218 | | prolog_eq(A,B) :- when((ground(A),ground(B)),=:=(A,B)). |
| 219 | | |
| 220 | | computable_arith_expression(X) :- number(X),!. |
| 221 | | computable_arith_expression(X) :- var(X),!,fail. |
| 222 | | computable_arith_expression(-(X)) :- computable_arith_expression(X). |
| 223 | | computable_arith_expression(+(X,Y)) :- computable_arith_expression(X),computable_arith_expression(Y). |
| 224 | | computable_arith_expression(-(X,Y)) :- computable_arith_expression(X),computable_arith_expression(Y). |
| 225 | | computable_arith_expression(*(X,Y)) :- computable_arith_expression(X),computable_arith_expression(Y). |
| 226 | | |
| 227 | | clpfd_neq_expr(E1,E2) :- number(E1),number(E2),!,E1\=E2. |
| 228 | | clpfd_neq_expr(E1,E2) :- %print(neq_expr(E1,E2)),nl, |
| 229 | | var(E1), var(E2), !, |
| 230 | | (preferences:preference(use_chr_solver,true) -> chr_neq(E1,E2) ; dif(E1,E2)), |
| 231 | | try_post_constraint( E1 #\= E2 ). % does not matter if posted |
| 232 | | % Note: | ?- X #\= Y, Y #=X. --> does not fail; hence we also execute dif(E1,E2) in CLPFD mode ! |
| 233 | | clpfd_neq_expr(E1,E2) :- % print(neq_expr(E1,E2)),nl, |
| 234 | | post_constraint3( E1 #\= E2, prolog_neq(E1,E2), Posted), |
| 235 | | (Posted=true -> my_dif(E1,E2) ; true). |
| 236 | | |
| 237 | | :- assert_must_succeed((clpfd_interface:prolog_neq(X,2+1),X=2)). |
| 238 | | :- assert_must_fail((clpfd_interface:prolog_neq(X,2+1),X=3)). |
| 239 | | :- assert_must_succeed((clpfd_interface:prolog_neq(3,X),X=2)). |
| 240 | | :- assert_must_succeed((clpfd_interface:prolog_neq(5-2,(2*2)-Y),Y=2)). |
| 241 | | prolog_neq(A,B) :- simple(A),simple(B),!, dif(A,B). |
| 242 | | prolog_neq(A,B) :- A \== B, when((ground(A),ground(B)),=\=(A,B)). |
| 243 | | |
| 244 | ? | my_dif(A,B) :- (simple(A);simple(B)),!. % do we need to setup things like dif(X,0) ? |
| 245 | | my_dif(A,B) :- comm_assoc_dif(A,B). |
| 246 | | |
| 247 | | % note: here we do not block, we use \== now rather than waiting on variables to be bound |
| 248 | | comm_assoc_dif(A,B) :- var(A),!, A \== B. |
| 249 | | comm_assoc_dif(A,B) :- var(B),!, A \== B. |
| 250 | | comm_assoc_dif(*(A1,A2),*(B1,B2)) :- !, |
| 251 | | extract_factors2(A1,A2,FA,[]), sort(FA,SFA), |
| 252 | | extract_factors2(B1,B2,FB,[]), sort(FB,SFB), |
| 253 | | %print(comm_assoc_dif_mul(SFA,SFB)),nl, |
| 254 | | SFA \== SFB. |
| 255 | | comm_assoc_dif(+(A1,A2),+(B1,B2)) :- !, |
| 256 | | extract_terms2(A1,A2,FA,[]), sort(FA,SFA), |
| 257 | | extract_terms2(B1,B2,FB,[]), sort(FB,SFB), |
| 258 | | %print(comm_assoc_dif_sum(SFA,SFB)),nl, |
| 259 | | SFA \== SFB. |
| 260 | | comm_assoc_dif(-(A1),-(B1)) :- !, comm_assoc_dif(A1,B1). |
| 261 | | comm_assoc_dif(-(A1,A2),-(B1,B2)) :- !, |
| 262 | | (comm_assoc_dif(A1,B1) -> true ; comm_assoc_dif(A2,B2)). |
| 263 | | % note : exponentiation and division are not handed directly to CLPFD at the moment, so no need to check here: |
| 264 | | %comm_assoc_dif(**(A1,A2),**(B1,B2)) :- !, (comm_assoc_dif(A1,B1) -> true ; comm_assoc_dif(A2,B2)). |
| 265 | | comm_assoc_dif(A,B) :- A \== B. % ,((nonvar(A),nonvar(B)) -> nl,print(cadif(A,B)),nl ; true). |
| 266 | | |
| 267 | | extract_factors2(A,B) --> extract_factors(A), extract_factors(B). |
| 268 | | extract_factors(A) --> {var(A)},!, [A]. |
| 269 | | extract_factors(*(A,B)) --> !, extract_factors(A), extract_factors(B). |
| 270 | | extract_factors(+(A,B)) --> !, [sum(ST)], {extract_terms2(A,B,T,[]),sort(T,ST)}. |
| 271 | | extract_factors(A) --> [A]. |
| 272 | | |
| 273 | | extract_terms2(A,B) --> extract_terms(A), extract_terms(B). |
| 274 | | extract_terms(A) --> {var(A)},!, [A]. |
| 275 | | extract_terms(+(A,B)) --> !, extract_terms(A), extract_terms(B). |
| 276 | | extract_terms(*(A,B)) --> !, [mul(ST)], {extract_factors2(A,B,T,[]),sort(T,ST)}. |
| 277 | | extract_terms(A) --> [A]. |
| 278 | | |
| 279 | | |
| 280 | | :- assert_must_succeed((clpfd_interface:clpfd_leq_expr(3,X+1),X=3)). |
| 281 | | :- assert_must_fail((clpfd_interface:clpfd_leq_expr(2,X-1),X=2)). |
| 282 | | clpfd_leq_expr(E1,E2) :- number(E1),number(E2), !, E1 =< E2. |
| 283 | | clpfd_leq_expr(E1,E2) :- useless_leq_constraint(E1,E2),!. |
| 284 | | clpfd_leq_expr(E1,E2) :- |
| 285 | | (preferences:preference(use_chr_solver,true) -> chr_leq(E1,E2) ; true), |
| 286 | | post_constraint( E1 #=< E2, prolog_leq(E1,E2)). |
| 287 | | prolog_leq(A,B) :- when((ground(A),ground(B)),=<(A,B)). |
| 288 | | |
| 289 | | :- assert_must_succeed((clpfd_interface:clpfd_lt_expr(3,X+1),X=3)). |
| 290 | | :- assert_must_fail((clpfd_interface:clpfd_lt_expr(2,X-1),X=3)). |
| 291 | | clpfd_lt_expr(E1,E2) :- number(E1),number(E2), !, E1 < E2. |
| 292 | | clpfd_lt_expr(E1,E2) :- useless_lt_constraint(E1,E2),!. |
| 293 | | clpfd_lt_expr(E1,E2) :- |
| 294 | | (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 |
| 295 | | post_constraint( E1 #< E2, prolog_lt(E1,E2)). |
| 296 | | prolog_lt(A,B) :- when((ground(A),ground(B)),<(A,B)). |
| 297 | | |
| 298 | | /* TO DO: do custom equalities div, plus, ... |
| 299 | | mydiv(X, Y, Z) :- |
| 300 | | (Y#=0 #\/ (Y#\=0 #/\ X/Y #= Z)). */ |
| 301 | | |
| 302 | | % a version of geq which avoids posting constraints if possible |
| 303 | | clpfd_geq2(E1,E2,Posted) :- number(E1),number(E2),!, E1 >= E2, Posted=true. |
| 304 | | clpfd_geq2(E1,E2,Posted) :- |
| 305 | | (preferences:preference(use_chr_solver,true) -> chr_leq(E2,E1) ; true), |
| 306 | | %E1 #>= E2, Posted=true. |
| 307 | | post_constraint2( E1 #>= E2 , Posted). |
| 308 | | |
| 309 | | clpfd_geq(E1,E2,Posted) :- clpfd_leq(E2,E1,Posted). |
| 310 | | clpfd_gt(E1,E2,Posted) :- clpfd_lt(E2,E1,Posted). |
| 311 | | |
| 312 | | clpfd_leq(E1,E2,Posted) :- |
| 313 | | useless_leq_constraint(E1,E2), |
| 314 | | !, Posted=true. % we have a useless constraint which is already known; avoid overhead of on_exception and time_out |
| 315 | | clpfd_leq(E1,E2,Posted) :- |
| 316 | | (preferences:preference(use_chr_solver,true) -> chr_leq(E1,E2) ; true), |
| 317 | | %E1 #=< E2, Posted=true. |
| 318 | | post_constraint2( E1 #=< E2 , Posted). |
| 319 | | |
| 320 | | useless_leq_constraint(E1,E2) :- number(E1), !, var(E2), fd_min(E2,Low), number(Low),E1 =< Low. |
| 321 | | useless_leq_constraint(E1,E2) :- number(E2), var(E1), fd_max(E1,Up), number(Up),Up =< E2. |
| 322 | | |
| 323 | | |
| 324 | | clpfd_lt(E1,E2,Posted) :- |
| 325 | | useless_lt_constraint(E1,E2), |
| 326 | | !, Posted=true. % we have a useless constraint which is already known; avoid overhead of on_exception and time_out |
| 327 | | clpfd_lt(E1,E2,Posted) :- |
| 328 | | (preferences:preference(use_chr_solver,true) -> chr_lt(E1,E2) ; dif_when_necesssary(E1,E2)), |
| 329 | | post_constraint2( E1 #< E2 , Posted). |
| 330 | | |
| 331 | | useless_lt_constraint(E1,E2) :- number(E1), !, var(E2), fd_min(E2,Low), number(Low),E1 < Low. |
| 332 | | useless_lt_constraint(E1,E2) :- number(E2), var(E1), fd_max(E1,Up), number(Up),Up < E2. |
| 333 | | |
| 334 | | clpfd_inrange(X,Low,Up) :- clpfd_inrange(X,Low,Up,_Posted). |
| 335 | | clpfd_inrange(X,Low,Up,Posted) :- |
| 336 | | (Low==Up -> X=Low, Posted=true |
| 337 | | ; (preferences:preference(use_chr_solver,true) |
| 338 | | -> chr_leq(Low,X), chr_leq(X,Up) |
| 339 | | ; true), |
| 340 | | (number(Low),number(Up) |
| 341 | | -> Low =< Up, % otherwise interval empty |
| 342 | | (number(X) -> X >= Low, X =< Up, Posted=true %, Low =<Up |
| 343 | | ; post_constraint2(X in Low..Up, Posted)) % Note: X in 1..Y, Y in 0..3. fails ! Range needs to be constant |
| 344 | | ; post_constraint2( (X #>=Low #/\ X #=< Up),Posted ) % #/\ Low #=< Up should be implied |
| 345 | | %,translate:print_clpfd_variables([X,Low,Up]),nl |
| 346 | | ) |
| 347 | | ). |
| 348 | | |
| 349 | | % assumes Low =< Up ! |
| 350 | | clpfd_not_in_non_empty_range(X,Low,Up) :- |
| 351 | ? | post_constraint((X #<Low #\/ X #> Up),outside_range_blocking(X,Low,Up)). |
| 352 | | |
| 353 | | :- block outside_range_blocking(-,?,?). |
| 354 | ? | outside_range_blocking(X,Low,Up) :- (X<Low ; X>Up). |
| 355 | | |
| 356 | | % assumes Low =< Up ! |
| 357 | | clpfd_not_inrange(X,Low,Up) :- preferences:preference(use_clpfd_solver,false), |
| 358 | | !, % avoid building up constraint below |
| 359 | | not_in_range_blocking(X,Low,Up). |
| 360 | | clpfd_not_inrange(X,Low,Up) :- |
| 361 | | % special treatment due to limitation of CLP(FD) disjunct: | ?- X #>10 #\/ X #>9. ---> X in inf..sup |
| 362 | | post_constraint2(XLow #<=> (X #<Low), Posted1), Posted1==true, |
| 363 | | post_constraint2(UpX #<=> (Up #< X), Posted2), Posted2==true, |
| 364 | | post_constraint2(UpLow #<=> (Up #< Low), Posted3), Posted3==true, |
| 365 | | !, |
| 366 | | clpfd_not_inrange_prop(XLow,UpX,UpLow,X,Low,Up). |
| 367 | | clpfd_not_inrange(X,Low,Up) :- |
| 368 | | force_post_constraint((X #<Low #\/ X #> Up #\/ Up #< Low),not_in_range_blocking(X,Low,Up)). |
| 369 | | |
| 370 | | :- block clpfd_not_inrange_prop(-,-,-,?,?,?). |
| 371 | | clpfd_not_inrange_prop(XLow,UpX,UpLow,_X,_Low,_Up) :- %print(unblock(XLow,UpX,UpLow,X,Low,Up)),nl, |
| 372 | ? | (XLow==1 ; UpX==1 ; UpLow==1),!. |
| 373 | | clpfd_not_inrange_prop(XLow,UpX,UpLow,X,Low,Up) :- XLow==0,!, |
| 374 | | post_constraint2(Up #< max(X,Low),_), disjunct_reify(UpX,UpLow). |
| 375 | | clpfd_not_inrange_prop(XLow,UpX,UpLow,X,Low,Up) :- UpX==0,!, |
| 376 | | post_constraint2(Low #> min(X,Up),_), disjunct_reify(XLow,UpLow). |
| 377 | | clpfd_not_inrange_prop(XLow,UpX,_UpLow,_X,_Low,_Up) :- % UpLow==0, |
| 378 | | % Anything more we can infer here ?? |
| 379 | | disjunct_reify(XLow,UpX). |
| 380 | | |
| 381 | | :- block disjunct_reify(-,-). |
| 382 | ? | disjunct_reify(UpX,UpLow) :- (UpX==1 ; UpLow==1),!. |
| 383 | | disjunct_reify(UpX,UpLow) :- (UpX==0 -> UpLow=1 ; UpX=1). |
| 384 | | |
| 385 | | |
| 386 | | :- block not_in_range_blocking(-,?,?),not_in_range_blocking(?,-,?). |
| 387 | | not_in_range_blocking(X,Y,Z) :- |
| 388 | | (X<Y -> true ; not_in_range_blocking2(X,Y,Z)). |
| 389 | | :- block not_in_range_blocking2(?,?,-). |
| 390 | | not_in_range_blocking2(X,Y,Z) :- (Z<Y -> true ; Z<X). |
| 391 | | |
| 392 | | clpfd_sum(List,Sum) :- |
| 393 | | clpfd_sum(List,Sum,Posted), |
| 394 | | (Posted==true -> true |
| 395 | | ; sum_list(List,int(0),int(Sum))). |
| 396 | | clpfd_sum(List,Sum,Posted) :- post_constraint2( sum(List,'#=',Sum),Posted). |
| 397 | | |
| 398 | | % non-CLPFD backup, when posting fails or CLPFD turned off |
| 399 | | :- block sum_list(-,?,?). |
| 400 | | sum_list([],Acc,Acc). |
| 401 | | sum_list([H|T],Acc,Res) :- kernel_objects:int_plus(int(H),Acc,NewAcc), sum_list(T,NewAcc,Res). |
| 402 | | |
| 403 | | |
| 404 | | % assert that a variable is one of the numbers in the FDList; FDList must be numbers, cannot be unbound FD variable |
| 405 | | % can fail due to overflows; one should not rely on it for soundness, see test 1353 |
| 406 | | clpfd_inlist(El,[X]) :- !, El=X. |
| 407 | | clpfd_inlist(El,FDList) :- |
| 408 | | try_post_constraint( (list_to_fdset(FDList,FDSET), El in_set FDSET)). |
| 409 | | |
| 410 | | % a version that always posts constraints independent of CLPFD preference |
| 411 | | force_clpfd_inlist(El,[X]) :- !, El=X. |
| 412 | | force_clpfd_inlist(El,FDList) :- |
| 413 | | list_to_fdset(FDList,FDSET), El in_set FDSET. |
| 414 | | |
| 415 | | % can fail due to overflows; one should not rely on it for soundness |
| 416 | | clpfd_not_inlist(El,FDList) :- |
| 417 | | try_post_constraint( (list_to_fdset(FDList,FDSET), fdset_complement(FDSET,C),El in_set C)). |
| 418 | | |
| 419 | | clpfd_maximum(El,List) :- %print(maximum(El,List)),nl, |
| 420 | | maximum(El,List). |
| 421 | | %force_post_constraint( maximum(El,List)). %, print(done(El)). |
| 422 | | clpfd_minimum(El,List) :- %print(minimum(El,List)),nl, |
| 423 | | %force_post_constraint( minimum(El,List)). |
| 424 | | minimum(El,List). |
| 425 | | |
| 426 | | |
| 427 | | clpfd_if_then_else(PredRes,ThenValue,ElseValue,Value) :- |
| 428 | | % TO DO: catch overflows and revert to simpler treatment then |
| 429 | | element(Idx,[ThenValue,ElseValue],Value), % Idx=1 if Value=ThenValue; Idx=2 if Value=ElseValue |
| 430 | | prop_12(PredRes,Idx). % if PredRes=pred_true -> Idx must be 1, 2 otherwise |
| 431 | | |
| 432 | | :- block prop_12(-,-). |
| 433 | | prop_12(P,V12) :- var(P),!,(V12=1 -> P=pred_true ; P=pred_false). |
| 434 | | prop_12(pred_true,1). |
| 435 | | prop_12(pred_false,2). |
| 436 | | |
| 437 | | /* |
| 438 | | on_exception(E,list_to_fdset([0,8589934592],R),true) |
| 439 | | E= error(domain_error(integer_list,[0,8589934592]),domain_error(list_to_fdset([0,8589934592],_A),1,integer_list,[0,8589934592])) |
| 440 | | domain_error |
| 441 | | */ |
| 442 | | |
| 443 | | |
| 444 | | clpfd_reify_inlist(El,FDList,FDRes) :- |
| 445 | | try_post_constraint( (list_to_fdset(FDList,FDSET), (El in_set FDSET) #<=> FDRes)). |
| 446 | | |
| 447 | | |
| 448 | | try_post_constraint(_) :- preferences:preference(use_clpfd_solver,false),!. |
| 449 | | :- if( environ(enable_time_out_for_constraints, true)). |
| 450 | | try_post_constraint(C) :- % print(posting(C)),nl, % |
| 451 | | on_exception(error(Err,_),time_out_constraint(C,true), check_error(Err,C) ). |
| 452 | | % Note: this will only catch exceptions that occur while posting ! |
| 453 | | % CLPFD integer overflow exceptions can still happen after posting :-( |
| 454 | | :- else. |
| 455 | | try_post_constraint(C) :- % print(posting(C)),nl, % |
| 456 | | on_exception(error(Err,_),C, check_error(Err,C) ). |
| 457 | | :- endif. |
| 458 | | |
| 459 | | post_constraint2(_,Posted) :- |
| 460 | | preferences:preference(use_clpfd_solver,false),!,Posted=false. |
| 461 | | :- if( environ(enable_time_out_for_constraints, true)). |
| 462 | | post_constraint2(C,Posted) :- % print(posting(C)),nl, % |
| 463 | | on_exception(error(Err,_),time_out_constraint(C,(Posted=false)), (check_error(Err,C),Posted=false) ), |
| 464 | | (Posted==false -> true ; Posted=true). |
| 465 | | :- else. |
| 466 | | post_constraint2(C,Posted) :- % print(posting(C)),nl, % |
| 467 | | on_exception(error(Err,_),(C,Posted=true), (check_error(Err,C),Posted=false) ). |
| 468 | | :- endif. |
| 469 | | |
| 470 | | |
| 471 | | check_error(representation_error(ErrMsg),C) :- |
| 472 | | is_clpfd_overflow_representation_error(ErrMsg), |
| 473 | | !, |
| 474 | | print_message('Ignoring constraint (integer overflow):'), |
| 475 | | print_message(C). |
| 476 | | check_error(domain_error(_Type,_Val),C) :- !, print_message('Ignoring constraint (domain error):'), |
| 477 | | % print(Type), print(' : '), print(Val), print(' : '), |
| 478 | | print_message(C). |
| 479 | | check_error(Err,C) :- |
| 480 | | %print_message('Ignoring constraint (unknown error):'), print(Err), print(' : '), print_message(C), |
| 481 | | add_error(clpfd_interface,'Ignoring constraint (unknown error):',Err:C). |
| 482 | | |
| 483 | | |
| 484 | | :- assert_must_succeed((print('Is 64-bit: '),(clpfd_interface:is_64_bit_system -> print('Yes') ; print('NO')),nl)). |
| 485 | | |
| 486 | | is_64_bit_system :- |
| 487 | | Err = error(representation_error(_),_), |
| 488 | | on_exception(Err, _X #= 268435456, fail). % 268435456 = 2^28, will generate overflow in 32-bit system |
| 489 | | |
| 490 | | |
| 491 | | clpfd_overflow_error_message :- clpfd_overflow_msg(M), |
| 492 | | add_error(clpfd_overflow,M). |
| 493 | | clpfd_overflow_warning_message :- clpfd_overflow_msg(M), |
| 494 | | add_warning(clpfd_overflow,M). |
| 495 | | %clpfd_overflow_print_message :- clpfd_overflow_msg(M),write(user_error,M),nl(user_error). |
| 496 | | |
| 497 | | clpfd_overflow_msg(M) :- clpfd_interface:is_64_bit_system, !, |
| 498 | | M = 'A CLPFD integer overflow occurred.\nSet CLPFD preference to FALSE (Animation Preferences).'. |
| 499 | | clpfd_overflow_msg('A CLPFD integer overflow occurred.\nSet CLPFD preference to FALSE (Animation Preferences) or use a 64 bit version of ProB.'). |
| 500 | | |
| 501 | | |
| 502 | | integer_too_small_for_clpfd(X) :- prolog_flag(min_tagged_integer,Min), X<Min. |
| 503 | | integer_too_large_for_clpfd(X) :- prolog_flag(max_tagged_integer,Max), X>Max. |
| 504 | | |
| 505 | | |
| 506 | | % post_constraint3(CLPFD,PrologBackup,Posted) |
| 507 | | post_constraint3(_,C,Posted) :- preferences:preference(use_clpfd_solver,false),!,Posted=false,call(C). |
| 508 | | post_constraint3(C,PrologBackup,Posted) :- % print(posting(C,PrologBackup)),nl, |
| 509 | | on_exception(error(Err,_), |
| 510 | | time_out_constraint((C,Posted=true),(Posted=false,PrologBackup)), |
| 511 | | (check_error(Err,C),Posted=false,call(PrologBackup)) ). |
| 512 | | |
| 513 | | % post_constraint(CLPFD,PrologBackup) |
| 514 | ? | post_constraint(_,C) :- preferences:preference(use_clpfd_solver,false),!,call(C). |
| 515 | | :- if(environ(enable_time_out_for_constraints, true)). |
| 516 | | post_constraint(C,PrologBackup) :- % print(posting(C,PrologBackup)),nl, |
| 517 | | on_exception(error(Err,_),time_out_constraint(C,PrologBackup), (check_error(Err,C),call(PrologBackup)) ). |
| 518 | | :- else. |
| 519 | | post_constraint(C,PrologBackup) :- % print(posting(C,PrologBackup)),nl,trace, |
| 520 | | on_exception(error(Err,_),C, (check_error(Err,C),call(PrologBackup)) ). |
| 521 | | :- endif. |
| 522 | | |
| 523 | | % no use_clpfd_solver check: |
| 524 | | force_post_constraint(C) :- call(C). % to use fd_batch(C) we need to convert C to list |
| 525 | | force_post_constraint(C,PrologBackup) :- % print(posting(C,PrologBackup)),nl, |
| 526 | | on_exception(error(Err,_),time_out_constraint(C,PrologBackup), (check_error(Err,C),call(PrologBackup)) ). |
| 527 | | |
| 528 | | |
| 529 | | :- if(\+ environ(enable_time_out_for_constraints, true)). |
| 530 | | time_out_constraint(C,_) :- call(C). % to use fd_batch(C) we need to convert C to list |
| 531 | | :- else. |
| 532 | | % Note: time_out/3 is quite expensive ! |
| 533 | | time_out_constraint(C,PrologBackup) :- %% debug:new_pp(C,PP), %% |
| 534 | | %%preferences:preference(time_out,CurTO), TO is 800 + (CurTO//100), time_out(C,TO,T), |
| 535 | | preferences:preference(solver_strength,Strength), |
| 536 | | TO is 1200 + Strength*200, |
| 537 | | time_out(C,TO,T), %% debug:new_sol(C,PP), %% |
| 538 | | (T==time_out -> print_message('Timeout when posting constraint:'), print_message(C), |
| 539 | | (preferences:preference(fail_if_clpfd_timeout,true) |
| 540 | | -> print_message('Assuming unsatisfiable !'),fail |
| 541 | | ; call(PrologBackup)) |
| 542 | | ; true). |
| 543 | | :- endif. |
| 544 | | |
| 545 | | |
| 546 | | :- assert_must_succeed((clpfd_interface:clpfd_domain(3,L,U), L==3, U==3)). |
| 547 | | clpfd_domain(Var,Low,Up) :- var(Var),!, |
| 548 | | fd_min(Var,Low), fd_max(Var,Up). |
| 549 | | % used to check (preferences:preference(use_clpfd_solver,false) -> Low=inf,Up=sup ; fd_min(Var,Low), fd_max(Var,Up) ). |
| 550 | | % but can also be called when CLPFD false for global_set values |
| 551 | | %used to call: fd_dom(Var, Low..Up)). fd_dom will sometimes return {1} \/ 2..3 or something like that ! |
| 552 | | clpfd_domain(X,X,X). |
| 553 | | |
| 554 | | % find some element in the domain of a FD variable |
| 555 | | clpfd_some_element_in_domain(Var,El) :- nonvar(Var),!, El=Var. |
| 556 | | clpfd_some_element_in_domain(Var,El) :- fd_min(Var,Low), number(Low),!,El=Low. |
| 557 | | clpfd_some_element_in_domain(Var,El) :- fd_max(Var,Up), number(Up),!,El=Up. |
| 558 | | clpfd_some_element_in_domain(Var,El) :- fd_set(Var,Set), fdset_parts(Set,Min,Max,_Rest), |
| 559 | | (number(Min) -> El=Min ; number(Max),El=Max). |
| 560 | | |
| 561 | | |
| 562 | | % succeed if we have a number or a CLPFD Var whose upper value is bounded |
| 563 | | clpfd_max_bounded(Var) :- var(Var), !, fd_max(Var,Up), number(Up). |
| 564 | | clpfd_max_bounded(N) :- number(N). |
| 565 | | |
| 566 | | :- assert_must_succeed(clpfd_interface:clpfd_can_match(1,1)). |
| 567 | | :- assert_must_succeed(clpfd_interface:clpfd_can_match(11,_X)). |
| 568 | | :- assert_must_succeed(clpfd_interface:clpfd_can_match(_X,22)). |
| 569 | | :- assert_must_succeed(clpfd_interface:clpfd_can_match(X,X)). |
| 570 | | :- assert_must_fail(clpfd_interface:clpfd_can_match(21,22)). |
| 571 | | :- assert_must_fail((dif(A,B),clpfd_interface:clpfd_can_match(A,B))). |
| 572 | | % check if two numbers or fd variables can match without unifying (as this could trigger propagations) |
| 573 | | clpfd_can_match(Var1,Var2) :- var(Var1),!, (var(Var2) -> clpfd_can_unify(Var1,Var2) ; clpfd_can_match_nr(Var1,Var2)). |
| 574 | | clpfd_can_match(Nr1,Var2) :- var(Var2),!,clpfd_can_match_nr(Var2,Nr1). |
| 575 | | clpfd_can_match(Nr1,Nr2) :- Nr1=Nr2. |
| 576 | | 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 |
| 577 | | fd_set(Var,FDS), Nr in_set FDS. |
| 578 | | clpfd_can_unify(Var1,Var2) :- |
| 579 | | fd_set(Var1,FDS1), fd_set(Var2,FDS2), fdset_intersect(FDS1,FDS2), |
| 580 | | \+ kernel_dif:frozen_dif(Var1,Var2). |
| 581 | | |
| 582 | | % check if FD variables or numbers have common possible value |
| 583 | | clpfd_can_intersect(Number1,NrOrVar2) :- nonvar(Number1),!, |
| 584 | | (nonvar(NrOrVar2) -> Number1==NrOrVar2 |
| 585 | | ; fd_set(NrOrVar2,FDS2), fdset_member(Number1,FDS2)). |
| 586 | | clpfd_can_intersect(Var1,Number2) :- nonvar(Number2),!, |
| 587 | | fd_set(Var1,FDS1), fdset_member(Number2,FDS1). |
| 588 | | clpfd_can_intersect(Var1,Var2) :- |
| 589 | | fd_set(Var1,FDS1), fd_set(Var2,FDS2), fdset_intersect(FDS1,FDS2). |
| 590 | | |
| 591 | | % check if we can currently determine an integer to be greater or equal to a given number |
| 592 | | clpfd_check_geq_nr(X,Nr) :- |
| 593 | | number(X),!, |
| 594 | | X>=Nr. |
| 595 | | clpfd_check_geq_nr(X,_) :- |
| 596 | | (nonvar(X) % something like X+Y |
| 597 | | ; preferences:preference(use_clpfd_solver,false)), |
| 598 | | !. |
| 599 | | clpfd_check_geq_nr(X,Nr) :- |
| 600 | | fd_min(X,Low), number(Low), Low>=Nr. |
| 601 | | |
| 602 | | clpfd_size(Var,Size) :- number(Var),!, Size=1. |
| 603 | | clpfd_size(Var,Size) :- |
| 604 | | (preferences:preference(use_clpfd_solver,false) |
| 605 | | -> Size = inf |
| 606 | | ; fd_size(Var,Size) |
| 607 | | ). |
| 608 | | |
| 609 | | :- assert_must_succeed(clpfd_interface:clpfd_alldifferent([1,2,3])). |
| 610 | | :- assert_must_succeed(clpfd_interface:all_dif([1,2,3],[])). |
| 611 | | :- assert_must_fail(clpfd_interface:clpfd_alldifferent([1,2,3,2])). |
| 612 | | :- assert_must_fail(clpfd_interface:all_dif([1,2,3,2],[])). |
| 613 | | |
| 614 | | clpfd_alldifferent([]) :- !. |
| 615 | | clpfd_alldifferent(L) :- post_constraint(all_different(L),all_dif(L,[])). |
| 616 | | |
| 617 | | all_dif([],_). |
| 618 | | all_dif([H|T],All) :- all_dif_aux(All,H), all_dif(T,[H|All]). |
| 619 | | |
| 620 | | all_dif_aux([],_). |
| 621 | | all_dif_aux([H|T],X) :- dif(H,X), all_dif_aux(T,X). |
| 622 | | |
| 623 | | /* |
| 624 | | clpfd_labeling(Variables) :- |
| 625 | | (preferences:preference(use_clpfd_solver,false) -> true |
| 626 | | ; labeling([ffc,enum],Variables)). %ff, enum |
| 627 | | */ |
| 628 | | |
| 629 | | % a version of labeling that performs randomized enumeration if requested |
| 630 | | % Currently, random enumeration does not support variable selection options |
| 631 | | % TODO: Maybe we should only randomize enumeration on "large enough" intervals |
| 632 | | :- use_module(library(random)). |
| 633 | | :- use_module(extension('random_permutations/random_permutations')). |
| 634 | | clpfd_randomised_labeling([],ListOfVars) :- |
| 635 | ? | preferences:get_preference(randomise_enumeration_order,true) |
| 636 | | -> clpfd_randomised_labeling_aux(ListOfVars) |
| 637 | ? | ; labeling([],ListOfVars). |
| 638 | | clpfd_randomised_labeling([Op|Ops],ListOfVars) :- |
| 639 | | labeling([Op|Ops],ListOfVars). |
| 640 | | |
| 641 | | clpfd_randomised_labeling_aux([]). |
| 642 | | clpfd_randomised_labeling_aux([Var|Vars]) :- |
| 643 | | clpfd_randomised_in_domain(Var), |
| 644 | | clpfd_randomised_labeling_aux(Vars). |
| 645 | | |
| 646 | | clpfd_randomised_in_domain(Var) :- |
| 647 | | init_random_permutations, |
| 648 | | clpfd_domain(Var,Low,Up), |
| 649 | | ((\+ number(Low) ; \+ number(Up)) |
| 650 | | -> add_internal_error('Unbounded FD variable: ',clpfd_randomised_in_domain(Var)), |
| 651 | | %trace, kernel_waitflags:get_fd_priority(Var,_), |
| 652 | | fail |
| 653 | | ; true), |
| 654 | | IntervalLength is Up - Low + 1, |
| 655 | | get_num_bits(IntervalLength,MaxIdx,NumBits), |
| 656 | | get_masks(NumBits,LeftMask,RightMask), |
| 657 | | % the seed relies on the random predicate, not on now/1, thus prob can be made deterministic by setting a central random seed |
| 658 | | random(TempSeed), |
| 659 | | Seed is floor(TempSeed * 10000), |
| 660 | | clpfd_randomised_labeling_aux(Var,0,MaxIdx,Low,Up,Seed,NumBits,LeftMask,RightMask). |
| 661 | | |
| 662 | | clpfd_randomised_labeling_aux(N,CurIdx,MaxIdx,From,To,Seed,NumBits,LeftMask,RightMask) :- |
| 663 | | random_permutation_element(CurIdx,MaxIdx,From,To,Seed,NumBits,LeftMask,RightMask,Drawn,NextIdx), |
| 664 | | %format('enumerate_int2: Setting variable ~w to ~w~n',[N,Drawn]), |
| 665 | | ( N=Drawn |
| 666 | | ; clpfd_randomised_labeling_aux(N,NextIdx,MaxIdx,From,To,Seed,NumBits,LeftMask,RightMask)). |
| 667 | | |
| 668 | | |
| 669 | | %:- use_module(library(lists),[reverse/2]). |
| 670 | | %clpfd_reverse_labeling(Vars) :- clpfd_reverse_labeling(Vars,[ffc,enum]). |
| 671 | | %% label a list of variables which was reversed: |
| 672 | | %clpfd_reverse_labeling(Variables,Opt) :- var(Variables),!, |
| 673 | | % add_internal_error('Must be list of variables: ',clpfd_reverse_labeling(Variables,Opt)). |
| 674 | | %clpfd_reverse_labeling(Variables,Options) :- !, |
| 675 | | % reverse(Variables,RevV), |
| 676 | | % clpfd_labeling(RevV,Options). |
| 677 | | |
| 678 | ? | clpfd_labeling(Variables,Options) :- !, |
| 679 | ? | on_exception(error(instantiation_error,Err),labeling(Options,Variables), |
| 680 | | (print(Err),nl, |
| 681 | | % this can happen when CLP(FD) has a time-out for other constraints |
| 682 | | add_error(clpfd_interface,'CLP(FD) Variables not set up for ',labeling(Options,Variables)))). % Options = [ffc,enum] |
| 683 | | |
| 684 | | |
| 685 | ? | clpfd_in_domain(Variable) :- !, |
| 686 | ? | on_exception(error(instantiation_error,Err),indomain(Variable), |
| 687 | | (print(Err),nl, |
| 688 | | % this can happen when CLP(FD) has a time-out for other constraints |
| 689 | | add_error(clpfd_interface,'CLP(FD) Variables not set up for ',indomain(Variable)))). |
| 690 | | |
| 691 | | |
| 692 | | clpfd_degree(Variable,Degree) :- fd_degree(Variable,Degree). % can be called with plain variables and with numbers |
| 693 | | |
| 694 | | % a new predicate to obtain the next variable that would be enumerated |
| 695 | | % (useful if you want to interleave other labeling with CLPFD labeling) |
| 696 | | |
| 697 | | :- assert_must_succeed((clpfd:in(X,1..3), clpfd:in(Y,3..5), clpfd:'#>'(X,Z), clpfd_interface:clpfd_get_next_variable_to_label([Y,2,X,3],V),V==X, X=3, Y=3, Z=2)). |
| 698 | | clpfd_get_next_variable_to_label(Variables,Var) :- |
| 699 | | clpfd_get_next_variable_to_label(Variables,Var,ffc). |
| 700 | | |
| 701 | | % possible options : ff, ffc, step, enum, bisect, median, ... |
| 702 | | clpfd_get_next_variable_to_label(Variables,Var,Opt) :- Variables \= [], % there is a segmentation fault if we call fd_delete with empty list |
| 703 | | % this also causes segmentation fault: |
| 704 | | % 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. |
| 705 | | clpfd:'$fd_delete'(Variables,Var,Opt). |
| 706 | | |
| 707 | | /* ------------ |
| 708 | | % a version of the above just for ffc, re-implemented by hand so as not to be dependent on internal predicates of clpfd |
| 709 | | % also: it returns the remaining variables (filters out non-variables) |
| 710 | | % but it can be much slower than clpfd:$fd_delete (e.g., NQueens50) |
| 711 | | clpfd_get_next_variable_to_label_ffc([H|T],Var,RestV) :- |
| 712 | | (get_fd_info(H,HI) -> get_next_aux(T,H,HI,Var,RestV) |
| 713 | | %,((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) |
| 714 | | ; clpfd_get_next_variable_to_label_ffc(T,Var,RestV) |
| 715 | | ). |
| 716 | | % , tools_printing:print_vars([H|T]),print(sel(Var,RestV)),nl. |
| 717 | | |
| 718 | | get_next_aux([],Var,_,Var,[]). |
| 719 | | get_next_aux([H|T],VarSoFar,VInfo,Var,Rest) :- |
| 720 | | (get_fd_info(H,HI) |
| 721 | | -> (HI @< VInfo -> Rest = [VarSoFar|TRest], get_next_aux(T,H,HI,Var,TRest) |
| 722 | | ; Rest = [H|TRest], get_next_aux(T,VarSoFar,VInfo,Var,TRest) |
| 723 | | ) |
| 724 | | ; get_next_aux(T,VarSoFar,VInfo,Var,Rest)). |
| 725 | | |
| 726 | | get_fd_info(Var,(Sz,NDg)) :- fd_size(Var,Sz), Sz \= 1, % note: we have 2 @<sup |
| 727 | | % kernel_waitflags:size_of_attached_goals(Var,Dg), |
| 728 | | fd_degree(Var,Dg), |
| 729 | | NDg is -Dg. % negate to give higher priority to goals with high degree |
| 730 | | ----- */ |
| 731 | | |
| 732 | | % would could also use size of attached frozen goals as a tiebreaker : frozen_degree(Var,FDg), NFDg is -FDg. |
| 733 | | % maybe we should compute this only on demand |
| 734 | | %frozen_degree(Var,Dg) :- var(Var), !,frozen(Var,Goal), size_of_goal(Goal,Dg). |
| 735 | | %frozen_degree(_,0). |
| 736 | | %size_of_goal((A,B),S) :- !, size_of_goal(A,SA), size_of_goal(B,SB), S is SA+SB. |
| 737 | | %size_of_goal(_,1). |
| 738 | | |
| 739 | | |
| 740 | | :- meta_predicate catch_clpfd_overflow_call1(0). |
| 741 | | :- meta_predicate catch_clpfd_overflow_call2(0,0). |
| 742 | ? | catch_clpfd_overflow_call1(Call) :- catch_clpfd_overflow_call2(Call,fail). |
| 743 | | catch_clpfd_overflow_call2(Call,Handler) :- |
| 744 | ? | on_exception(error(representation_error(ErrMsg),E), |
| 745 | | Call, |
| 746 | | handle_representation_error(ErrMsg,E,Handler)). |
| 747 | | |
| 748 | | handle_representation_error(ErrMsg,_E,Call) :- |
| 749 | | (is_clpfd_overflow_representation_error(ErrMsg) |
| 750 | | -> clpfd_overflow_error_message, Call |
| 751 | | ; throw(representation_error(ErrMsg))). |
| 752 | | |
| 753 | | is_clpfd_overflow_representation_error('CLPFD integer overflow'). |
| 754 | | is_clpfd_overflow_representation_error('max_clpfd_integer'). |
| 755 | | is_clpfd_overflow_representation_error('min_clpfd_integer'). |
| 756 | | |
| 757 | | |
| 758 | | |
| 759 | | /* |
| 760 | | Testing for how large the integers can be, 32-bit system: |
| 761 | | | ?- X is integer(2**30), Y#=X+1. |
| 762 | | ! Representation error in argument 2 of user:'t=u+c'/3 |
| 763 | | ! CLPFD integer overflow |
| 764 | | ! goal: 't=u+c'(_102,1073741824,1) |
| 765 | | | ?- X is integer(2**30), Y#=X. |
| 766 | | X = 1073741824, |
| 767 | | Y = 1073741824 ? |
| 768 | | 64-bit system: |
| 769 | | | ?- X is integer(2**60), Y#=X. |
| 770 | | ! Representation error in argument 2 of user:(#=)/2 |
| 771 | | ! CLPFD integer overflow |
| 772 | | ! goal: _413#=1152921504606846976 |
| 773 | | |
| 774 | | | ?- X is integer(2**60)-1, Y#=X. |
| 775 | | X = 1152921504606846975, |
| 776 | | Y = 1152921504606846975 ? |
| 777 | | yes |
| 778 | | */ |
| 779 | | |
| 780 | | |