1 | | % (c) 2009-2016 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(fd_utils_clpfd,[eq_fd/2, neq_fd/3, |
6 | | in_fd/3, in_fd_wf/4, |
7 | | /* neq_fdpair/4, not_in_fd/3, not used anymore */ |
8 | | enum_fd/3, enum_fd_linear/3]). |
9 | | |
10 | | :- use_module(module_information). |
11 | | :- module_info(group,kernel). |
12 | | :- module_info(description,'Basic checks for SET elements (equality, ...); maps to CLP(FD).'). |
13 | | |
14 | | /* File: fd_utils_clpfd.pl */ |
15 | | /* Created: 21/3/06 by Michael Leuschel */ |
16 | | |
17 | | |
18 | | :- use_module(self_check). |
19 | | |
20 | | :- use_module(library(clpfd)). |
21 | | |
22 | | :- assert_must_succeed(( fd_utils_clpfd:eq_fd(2,2) )). |
23 | | :- assert_must_fail(( fd_utils_clpfd:eq_fd(2,3) )). |
24 | | |
25 | ? | eq_fd(X,Y) :- X=Y. |
26 | | |
27 | | %eq_fd(X,Y) :- %print_message(informational,eq_fd(X,Y)), |
28 | | % %((var(X),frozen(X,G)) -> print_message(informational,frozen(X,G)) ; true), |
29 | | % X = Y, |
30 | | % print_message(informational,done_eq(X,Y)). |
31 | | |
32 | | |
33 | | :- assert_must_succeed(( fd_utils_clpfd:in_fd(X,1,3), |
34 | | fd_utils_clpfd:neq_fd(X,1,'Name'), fd_utils_clpfd:neq_fd(X,3,'Name'), X==2 )). |
35 | | |
36 | | :- assert_must_succeed(( fd_utils_clpfd:neq_fd(1,2,'Name') )). |
37 | | :- assert_must_fail(( fd_utils_clpfd:neq_fd(2,2,'Name') )). |
38 | | |
39 | | neq_fd(X,Y,_Type) :- %print(neq_fd(X,Y,_Type)),nl, |
40 | | % sometimes no CLP(FD) constraints set up for X or Y; can mean that we only detect inconsistencies much later |
41 | | %(var(X) -> b_global_sets:global_type(fd(X,_Type),_Type) ; true), % commenting it in causes test 496 to fail; |
42 | | %(var(Y) -> b_global_sets:global_type(fd(Y,_Type),_Type) ; true), % TO DO: investigate |
43 | | X #\= Y, |
44 | | ((var(X),var(Y)) -> dif(X,Y) ; true). % even for finite domains X in 1..10, Y in 1..10, X#\=Y, X=Y. does not fail; |
45 | | |
46 | | |
47 | | |
48 | | /* |
49 | | :- assert_must_succeed(( fd_utils_clpfd:neq_fdpair(2,3,2,4) )). |
50 | | :- assert_must_succeed(( fd_utils_clpfd:neq_fdpair(2,3,3,3) )). |
51 | | :- assert_must_fail(( fd_utils_clpfd:neq_fdpair(2,3,2,3) )). |
52 | | |
53 | | neq_fdpair(X1,Y1,X2,Y2) :- |
54 | | when((?=(X1,X2);?=(Y1,Y2)), |
55 | | (?=(X1,X2) -> (X1 \= X2 -> true ; dif(Y1,Y2)) |
56 | | ; (Y1 \= Y2 -> true ; dif(X1,X2)) |
57 | | )). |
58 | | */ |
59 | | |
60 | | :- use_module(kernel_waitflags,[add_fd_variable_for_labeling/2]). |
61 | | |
62 | | in_fd(X,Low,Up) :- number(Low), number(Up), !, X in Low..Up. |
63 | | in_fd(X,Low,Up) :- X #>=Low, X#=<Up. %when((ground(Low),ground(Up)), X in Low..Up). |
64 | | |
65 | | in_fd_wf(X,Low,Up,WF) :- number(Low), number(Up), !, X in Low..Up, |
66 | | in_fd_wf2(X,Low,Up,WF). |
67 | | in_fd_wf(X,Low,Up,WF) :- X #>=Low, X#=<Up, in_fd_wf2(X,Low,Up,WF). |
68 | | |
69 | | :- block in_fd_wf2(?,-,?,?), in_fd_wf2(?,?,-,?). |
70 | | in_fd_wf2(X,_Low,_Up,WF) :- |
71 | | (ground(X) -> true |
72 | | ; %Size is Up+1-Low, |
73 | | %fd_size(X,Size), |
74 | | add_fd_variable_for_labeling(X,WF) % will automatically do enumeration |
75 | | ). |
76 | | |
77 | | /* TO DO: check if we have to add FD variables to kernel_waitflags store using label_clpfd_vars |
78 | | in other circumstances; |
79 | | Provide support for x: {aa,bb,cc} ... constraints |
80 | | */ |
81 | | |
82 | | |
83 | | |
84 | | |
85 | | enum_fd(X,Low,Up) :- % we could use clpfd labeling |
86 | ? | preferences:get_preference(randomise_enumeration_order,true) |
87 | | -> %print(random_enum(X,Low,Up)),nl, |
88 | | enum_fd_random(X,Low,Up) |
89 | ? | ; enum_fd_linear(X,Low,Up). |
90 | | enum_fd_linear(X,Low,Up) :- |
91 | ? | Low =< Up |
92 | | -> ( %print(enum_fd(X,Low,Up)),translate:print_clpfd_variable(X),nl, |
93 | ? | X=Low %, tools:print_bt_message(done_enum_fd(X,Low,Up)) |
94 | | ; |
95 | | %print(continue(X,Low,Up)),nl, |
96 | | % TO DO: We could assert that X>Low and/or try to trigger all equalities for X=y with y<=Low |
97 | ? | L1 is Low+1, enum_fd_linear(X,L1,Up) |
98 | | ) |
99 | | ; fail. |
100 | | |
101 | | |
102 | | :- use_module(library(random)). |
103 | | :- use_module(extension('random_permutations/random_permutations')). |
104 | | enum_fd_random(Var,Low,Up) :- |
105 | | init_random_permutations, |
106 | | IntervalLength is Up - Low + 1, |
107 | | get_num_bits(IntervalLength,MaxIdx,NumBits), |
108 | | get_masks(NumBits,LeftMask,RightMask), |
109 | | % the seed relies on the random predicate, not on now/1, thus prob can be made deterministic by setting a central random seed |
110 | | random(TempSeed), |
111 | | Seed is floor(TempSeed * 10000), |
112 | | enum_fd_random_aux(Var,0,MaxIdx,Low,Up,Seed,NumBits,LeftMask,RightMask). |
113 | | |
114 | | enum_fd_random_aux(Var,CurIdx,MaxIdx,From,To,Seed,NumBits,LeftMask,RightMask) :- |
115 | | random_permutation_element(CurIdx,MaxIdx,From,To,Seed,NumBits,LeftMask,RightMask,Drawn,NextIdx), |
116 | | (Var=Drawn ; enum_fd_random_aux(Var,NextIdx,MaxIdx,From,To,Seed,NumBits,LeftMask,RightMask)). |
117 | | |
118 | | |
119 | | % not really required, would be a type error |
120 | | %:- block not_in_fd(-,?,?), not_in_fd(?,-,?), not_in_fd(?,?,-). |
121 | | %not_in_fd(X,Low,Up) :- |
122 | | % (X < Low ; X > Up),!. |