1 % (c) 2009-2022 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 elements (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 % Note: the disjoint constants will have been asserted by add_named_constants_to_global_set
40 findall(Nr,is_b_global_constant(GS,Nr,_Cst),Ns),
41 (Ns=[] -> FirstAvailableNewIdx=1
42 ; max_member(Max,Ns),
43 length(Ns,Max), % check contiguous, DisjointConstants are numbered 1..Max
44 FirstAvailableNewIdx is Max+1
45 ),
46 sort(AllConstantsIDs,SAll),
47 sort(DisjointConstants,SDis),
48 ord_subtract(SAll,SDis,Other),
49 % Other \= [], % If Other = [] one could still use partition symmetry reduction
50 debug_println(4,static_symmetry_possible(GS,FirstAvailableNewIdx,Up,Other,SDis)).
51
52
53
54 % -----------------------------
55
56 :- use_module(store,[lookup_value_for_existing_id/3]).
57 :- use_module(bsyntaxtree,[member_in_conjunction/2, get_texpr_expr/2,get_texpr_id/2]).
58 :- use_module(fd_utils_clpfd,[in_fd/3]).
59 :- use_module(library(clpfd), [(#<=>)/2]).
60 :- use_module(clpfd_interface,[force_post_constraint/1, force_clpfd_inlist/2]).
61 :- use_module(tools,[exact_member/2]).
62
63 % perform_ssr(ConstatsOfTypeGSNotAssignedYet, ...)
64 perform_ssr([],_PrevNrs,_InitialF,FirstNew,GS,_Low,Up,ConstantsState) :- less_than_inf(FirstNew,Up),
65 % if partition exists -> we could enforce order on partitions for Indexes in FirstAvailableNewIdx..Up
66 b_get_properties_from_machine(Properties),
67 member_in_conjunction(C,Properties),
68 get_texpr_expr(C,partition(Set,DisjSets)),
69 global_set_identifier(Set,GS),
70 maplist(get_value_for_constant(ConstantsState),DisjSets,DisjSetVals),
71 % TO DO: try and evaluate at runtime in case DisjSets are not all identifiers but expressions such as {aa,bb}
72 !,
73 debug_println(19,partition_symmetry_reduction(DisjSetVals,FirstNew,GS,Up)),
74 % when(ground(DisjSetVals), format('SETS=~w~n',[DisjSetVals])),
75 partition_sym_reduction(DisjSetVals,FirstNew).
76 perform_ssr([],PrevNrs,InitialF,FirstNew,GS,_,_,_) :-
77 debug_println(4,done_ssr(GS,PrevNrs,InitialF,FirstNew)).
78 perform_ssr([OtherID|T],PrevNrs,InitialF,FirstNew,GS,Low,Up,ConstantsState) :-
79 % adding static symmetry breaking constraints for OtherID of type GS
80 lookup_value_for_existing_id(OtherID,ConstantsState,fd(Nr,GS)),
81 debug_println(4,ssr(OtherID,Nr,FirstNew,Up)),
82 in_fd(Nr,Low,FirstNew),
83 force_post_constraint((Nr#>InitialF) #<=> Trigger),
84 check_contiguous(Trigger,Nr,PrevNrs),
85 (less_than_inf(FirstNew,Up) -> F1 is FirstNew+1 ; F1=Up),
86 perform_ssr(T,[Nr|PrevNrs],InitialF,F1,GS,Low,Up,ConstantsState).
87
88 less_than_inf(X,Up) :- (Up=inf -> true ; X < Up).
89
90
91 get_value_for_constant(ConstantsState,TID,DisjSetVals) :-
92 get_texpr_id(TID,ID),
93 lookup_value_for_existing_id(ID,ConstantsState,DisjSetVals).
94
95 :- block check_contiguous(-,?,?),check_contiguous(?,-,?). % to do: do not delay on Nr
96 check_contiguous(0,_Nr,_PrevNrs). % we have not used a new deferred set number
97 check_contiguous(1,Nr,PrevNrs) :- % we have used a new number, check that previous number also used
98 %print(check_used(Nr,PrevNrs)),nl,
99 N1 is Nr-1,
100 (exact_member(N1,PrevNrs) -> true
101 ; when(ground(PrevNrs),force_clpfd_inlist(N1,PrevNrs))).
102
103
104 global_set_identifier(C,GS) :- get_texpr_expr(C,BE), global_set_identifier2(BE,GS).
105 global_set_identifier2(identifier(GlobalSet),GlobalSet).
106 global_set_identifier2(value(global_set(GlobalSet)),GlobalSet). % generated by Z
107
108 % --------------------
109
110
111 % This predicate implements a symmetry reduction on a partition of the deferred sets
112 % DS = P1 \/ P2 ... Pn & P1 /\ P2 = {} ...
113 % where we may have some constants already allocated fixed numbers (1..n)
114 % and other constants ranging from 1..(n+m) and where n+m+1 is the FirstFreelyChoosableIndex
115 % for any index >= FirstFreelyChoosableIndex we impose that these must be allocated in order to
116 % the partitions
117
118 % For example: if FirstFreelyChoosableIndex 1 and we have two sets, then we will only allow:
119 % {}, {1,2,3} ; {1}, {2,3} ; {1,2}, {3} ; {1,2,3} , {} as partitions and not e.g.
120 % {2}, {1,3} ...
121 % Idea: if fd(Nr,_) appears in partition k, then all numbers from FirstFreelyChoosableIndex..Nr are prohibited in later partitions
122
123 % partition_sym_reduction(List of Sets, FirstFreelyChoosableIndex)
124
125 partition_sym_reduction([],_).
126 partition_sym_reduction([PSet1|OtherPSets],FirstNew) :-
127 check_partition_order(PSet1,OtherPSets,FirstNew),
128 partition_sym_reduction(OtherPSets,FirstNew).
129
130 :- block check_partition_order(-,?,?).
131 check_partition_order([],_,_) :- !.
132 check_partition_order([H|T],OtherSets,FirstNew) :- (T,OtherSets) \== ([],[]),
133 !,
134 check_partition_order_for_el(H,[T|OtherSets],FirstNew),
135 check_partition_order(T,OtherSets,FirstNew).
136 check_partition_order(global_set(_),_,_) :- !. % all other sets will be forced to be empty
137 %check_partition_order(A,_,_) :- print(uncov_pset(A)),nl,fail. % TO DO: treat avl_set ..
138 check_partition_order(_,_,_).
139
140 :- block check_partition_order_for_el(-,?,?).
141 check_partition_order_for_el(fd(Nr,_),OtherSets,FirstNew) :-
142 check_partition_order_for_el2(Nr,OtherSets,FirstNew).
143 :- block check_partition_order_for_el2(-,?,?).
144 check_partition_order_for_el2(Nr,OtherSets,FirstNew) :- % print(sym_red(Nr,FirstNew,OtherSets)),nl,
145 Nr > FirstNew,!, % sym. reduction applicable
146 maplist(prohibit_indices(FirstNew,Nr),OtherSets).
147 check_partition_order_for_el2(_,_,_).
148
149 :- use_module(library(clpfd),[fdset_interval/3, fdset_complement/2, in_set/2]).
150 prohibit_indices(FirstNew,Nr,Set) :-
151 fdset_interval(Int,FirstNew,Nr),
152 fdset_complement(Int,NotInt),
153 %print(prohibit2(Set,NotInt)),nl,
154 prohibit_indices2(Set,NotInt).
155 :- block prohibit_indices2(-,?).
156 prohibit_indices2([],_) :- !.
157 prohibit_indices2([H|T],NotInt) :- !, %print(prohibit(H,T,NotInt)),nl,
158 H = fd(Nr,_),
159 Nr in_set NotInt,
160 prohibit_indices2(T,NotInt).
161 prohibit_indices2(A,_) :- % TO DO: treat avl_set, ..
162 print(uncov_prohibit_indices2(A)),nl.