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.