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