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(static_symmetry_reduction, [static_symmetry_reduction_possible/5, perform_ssr/8]). | |
6 | ||
7 | :- use_module(module_information,[module_info/2]). | |
8 | :- module_info(group,kernel). | |
9 | :- module_info(description,'This module provides support for symmetry reduction on deferred sets.'). | |
10 | ||
11 | :- use_module(library(lists)). | |
12 | :- use_module(library(ordsets)). | |
13 | :- use_module(debug,[debug_println/2]). | |
14 | ||
15 | ||
16 | ||
17 | % peform MACE style static symmetry reduction for those global constants | |
18 | % that have not already been fixed | |
19 | % e.g., for constants aa,bb,cc,dd of type ID and bb/=cc --> nrs of bb,cc will be fixed as 1 and 2; we will ensure that numbers of aa:1..3 and dd:1..4 and that dd=4 only if aa=3 | |
20 | % TO DO: extend this kind of symmetry reduction to other constants (e.g., total fun over fixed domain f: ... --> ID) | |
21 | % TO DO: ensure this is also used in enabling analysis, symbolic_model checker, ... | |
22 | % TO DO: support detection of injections | |
23 | ||
24 | ||
25 | :- use_module(b_global_sets,[b_get_fd_type_bounds/3, is_b_global_constant/3, b_global_set/1]). | |
26 | :- use_module(bmachine,[b_get_properties_from_machine/1, b_get_disjoint_constants_of_type/3]). | |
27 | ||
28 | ||
29 | % check if we can apply static symmetry reduction for a global deferred set GS | |
30 | % means we have a deferred set GS with fixed element (DisjointConstants) | |
31 | % and some remaining deferred set elements (Other) whose index starts at FirstAvailableNewIdx | |
32 | static_symmetry_reduction_possible(GS,FirstAvailableNewIdx,Low,Up,Other) :- | |
33 | ? | b_global_set(GS), |
34 | b_get_fd_type_bounds(GS,Low,Up), | |
35 | (b_get_disjoint_constants_of_type(GS, DisjointConstants, AllConstantsIDs) -> true | |
36 | ; DisjointConstants=[], % find_constants_of_type(Constants,GS,AllConstantsIDs,_GSConstants) | |
37 | AllConstantsIDs=[] % otherwise at least one disjoint constant would have been returned | |
38 | ), | |
39 | findall(Nr,is_b_global_constant(GS,Nr,_Cst),Ns), | |
40 | (Ns=[] -> FirstAvailableNewIdx=1 | |
41 | ; max_member(Max,Ns), | |
42 | length(Ns,Max), % check contiguous, DisjointConstants are numbered 1..Max | |
43 | FirstAvailableNewIdx is Max+1 | |
44 | ), | |
45 | sort(AllConstantsIDs,SAll), | |
46 | sort(DisjointConstants,SDis), | |
47 | ord_subtract(SAll,SDis,Other), | |
48 | % Other \= [], % If Other = [] one could still use partition symmetry reduction | |
49 | debug_println(4,static_symmetry_possible(GS,FirstAvailableNewIdx,Up,Other,SDis)). | |
50 | ||
51 | ||
52 | % ----------------------------- | |
53 | ||
54 | :- use_module(store,[lookup_value_for_existing_id/3]). | |
55 | :- use_module(bsyntaxtree,[member_in_conjunction/2, get_texpr_expr/2,get_texpr_id/2]). | |
56 | :- use_module(fd_utils_clpfd,[in_fd/3]). | |
57 | :- use_module(clpfd_interface,[force_post_constraint/1, force_clpfd_inlist/2]). | |
58 | :- use_module(tools,[exact_member/2]). | |
59 | ||
60 | perform_ssr([],_PrevNrs,_InitialF,FirstNew,GS,_Low,Up,ConstantsState) :- FirstNew < Up, | |
61 | % if partition exists -> we could enforce order on partitions for Indexes in FirstAvailableNewIdx..Up | |
62 | b_get_properties_from_machine(Properties), | |
63 | ? | member_in_conjunction(C,Properties), |
64 | get_texpr_expr(C,partition(Set,DisjSets)), | |
65 | global_set_identifier(Set,GS), | |
66 | maplist(try_get_value(ConstantsState),DisjSets,DisjSetVals), % TO DO: try and evaluate at runtime in case DisjSets are not all identifiers but expressions such as {aa,bb} | |
67 | !, | |
68 | print(partition_symmetry_reduction(DisjSetVals,FirstNew,GS,Up)),nl, | |
69 | % when(ground(DisjSetVals), format('SETS=~w~n',[DisjSetVals])), | |
70 | partition_sym_reduction(DisjSetVals,FirstNew). | |
71 | perform_ssr([],PrevNrs,InitialF,FirstNew,GS,_,_,_) :- | |
72 | debug_println(4,done_ssr(GS,PrevNrs,InitialF,FirstNew)). | |
73 | perform_ssr([OtherID|T],PrevNrs,InitialF,FirstNew,GS,Low,Up,ConstantsState) :- | |
74 | % adding static symmetry breaking constraints for OtherID of type GS | |
75 | lookup_value_for_existing_id(OtherID,ConstantsState,fd(Nr,GS)), | |
76 | debug_println(4,ssr(OtherID,Nr,FirstNew,Up)), | |
77 | in_fd(Nr,Low,FirstNew), | |
78 | force_post_constraint(clpfd:'#<=>'( (Nr#>InitialF) , Trigger)), | |
79 | check_contiguous(Trigger,Nr,PrevNrs), | |
80 | (FirstNew<Up -> F1 is FirstNew+1 ; F1=Up), | |
81 | perform_ssr(T,[Nr|PrevNrs],InitialF,F1,GS,Low,Up,ConstantsState). | |
82 | ||
83 | ||
84 | ||
85 | try_get_value(ConstantsState,TID,DisjSetVals) :- | |
86 | get_texpr_id(TID,ID),lookup_value_for_existing_id(ID,ConstantsState,DisjSetVals). | |
87 | ||
88 | :- block check_contiguous(-,?,?),check_contiguous(?,-,?). % to do: do not delay on Nr | |
89 | check_contiguous(0,_Nr,_PrevNrs). % we have not used a new deferred set number | |
90 | check_contiguous(1,Nr,PrevNrs) :- % we have used a new number, check that previous number also used | |
91 | %print(check_used(Nr,PrevNrs)),nl, | |
92 | N1 is Nr-1, | |
93 | (exact_member(N1,PrevNrs) -> true | |
94 | ; when(ground(PrevNrs),force_clpfd_inlist(N1,PrevNrs))). | |
95 | ||
96 | ||
97 | global_set_identifier(C,GS) :- get_texpr_expr(C,BE), global_set_identifier2(BE,GS). | |
98 | global_set_identifier2(identifier(GlobalSet),GlobalSet). | |
99 | global_set_identifier2(value(global_set(GlobalSet)),GlobalSet). % generated by Z | |
100 | ||
101 | % -------------------- | |
102 | ||
103 | ||
104 | % This predicate implements a symmetry reduction on a partition of the deferred sets | |
105 | % DS = P1 \/ P2 ... Pn & P1 /\ P2 = {} ... | |
106 | % where we may have some constants already allocated fixed numbers (1..n) | |
107 | % and other constants ranging from 1..(n+m) and where n+m+1 is the FirstFreelyChoosableIndex | |
108 | % for any index >= FirstFreelyChoosableIndex we impose that these must be allocated in order to | |
109 | % the partitions | |
110 | ||
111 | % For example: if FirstFreelyChoosableIndex 1 and we have two sets, then we will only allow: | |
112 | % {}, {1,2,3} ; {1}, {2,3} ; {1,2}, {3} ; {1,2,3} , {} as partitions and not e.g. | |
113 | % {2}, {1,3} ... | |
114 | % Idea: if fd(Nr,_) appears in partition k, then all numbers from FirstFreelyChoosableIndex..Nr are prohibited in later partitions | |
115 | ||
116 | % partition_sym_reduction(List of Sets, FirstFreelyChoosableIndex) | |
117 | ||
118 | partition_sym_reduction([],_). | |
119 | partition_sym_reduction([PSet1|OtherPSets],FirstNew) :- | |
120 | check_partition_order(PSet1,OtherPSets,FirstNew), | |
121 | partition_sym_reduction(OtherPSets,FirstNew). | |
122 | ||
123 | :- block check_partition_order(-,?,?). | |
124 | check_partition_order([],_,_) :- !. | |
125 | check_partition_order([H|T],OtherSets,FirstNew) :- (T,OtherSets) \== ([],[]), | |
126 | !, | |
127 | check_partition_order_for_el(H,[T|OtherSets],FirstNew), | |
128 | check_partition_order(T,OtherSets,FirstNew). | |
129 | check_partition_order(global_set(_),_,_) :- !. % all other sets will be forced to be empty | |
130 | %check_partition_order(A,_,_) :- print(uncov_pset(A)),nl,fail. % TO DO: treat avl_set .. | |
131 | check_partition_order(_,_,_). | |
132 | ||
133 | :- block check_partition_order_for_el(-,?,?). | |
134 | check_partition_order_for_el(fd(Nr,_),OtherSets,FirstNew) :- | |
135 | check_partition_order_for_el2(Nr,OtherSets,FirstNew). | |
136 | :- block check_partition_order_for_el2(-,?,?). | |
137 | check_partition_order_for_el2(Nr,OtherSets,FirstNew) :- % print(sym_red(Nr,FirstNew,OtherSets)),nl, | |
138 | Nr > FirstNew,!, % sym. reduction applicable | |
139 | maplist(prohibit_indices(FirstNew,Nr),OtherSets). | |
140 | check_partition_order_for_el2(_,_,_). | |
141 | ||
142 | :- use_module(library(clpfd),[fdset_interval/3, fdset_complement/2, in_set/2]). | |
143 | prohibit_indices(FirstNew,Nr,Set) :- | |
144 | fdset_interval(Int,FirstNew,Nr), | |
145 | fdset_complement(Int,NotInt), | |
146 | %print(prohibit2(Set,NotInt)),nl, | |
147 | prohibit_indices2(Set,NotInt). | |
148 | :- block prohibit_indices2(-,?). | |
149 | prohibit_indices2([],_) :- !. | |
150 | prohibit_indices2([H|T],NotInt) :- !, %print(prohibit(H,T,NotInt)),nl, | |
151 | H = fd(Nr,_), | |
152 | Nr in_set NotInt, | |
153 | prohibit_indices2(T,NotInt). | |
154 | prohibit_indices2(A,_) :- % TO DO: treat avl_set, .. | |
155 | print(uncov_prohibit_indices2(A)),nl. |