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(kodkod2,
6 [ extract_used_types/4
7 , create_atoms_for_types/6
8 , create_identifier_relations/5
9 ]).
10
11 :- use_module(library(lists)).
12 :- use_module(library(avl)).
13 :- use_module(library(ordsets)).
14
15 :- use_module(kodkodsrc(kodkod_tools)).
16 :- use_module(kodkodsrc(kodkod_integer_recalc)).
17
18 :- use_module(probsrc(module_information),[module_info/2]).
19 :- use_module(probsrc(tools),[foldl/4,foldl/5]).
20 :- use_module(probsrc(error_manager)).
21 :- use_module(probsrc(bsyntaxtree)).
22 :- use_module(probsrc(bmachine)).
23 :- use_module(probsrc(b_interpreter),[b_compute_expression_nowf/6]).
24 :- use_module(probsrc(b_global_sets),[all_elements_of_type/2,is_b_global_constant/3]).
25 :- use_module(probsrc(store),[empty_state/1]).
26
27 :- module_info(group,kodkod).
28 :- module_info(description,'This module contains the several phases of a translation process to Kodkod.').
29
30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
31 % Phase 2
32 % extract all used types
33 % for integers, check if bitstrings are necessary and store
34 % the needed intervals
35
36 % extract_used_types(+TExpr,-UsedTypes,-IntegerRange,-BitstringRange):
37 % extracts from a syntax tree the list of used types, the
38 % ranges of integers and the ranges of integers that occur in sets
39 extract_used_types(TExpr,UsedTypes,IntegerRange,BitstringRange) :-
40 % first adapt the output of the interval analysis to our needs
41 % (see the comments in kodkod_integer_recalc for details)
42 integer_recalc(TExpr,RExpr),
43 % now extract the used types
44 extract_used_types1(RExpr,UsedTypes,IntegerRange,BitstringRange).
45
46 extract_used_types1(TExpr,UsedTypes,IntegerRange,BitstringRange) :-
47 syntaxtraversion(TExpr,Expr,Type,_,Subs1,Names),
48 ( higher_order_exception(Expr,Subs) ->
49 UsedTypesA=[],IntRangeA=none,BitRangeA=none
50 ; extract_type_information(Type,TExpr,Names,UsedTypesA,IntRangeA,BitRangeA) ->
51 Subs1 = Subs
52 ;
53 throw(kodkod(unsupported_type(Type)))),
54 extract_used_types_l(Subs,UsedTypesA,IntRangeA,BitRangeA,
55 UsedTypes,IntegerRange,BitstringRange).
56
57 extract_used_types_l([],Types,IntRange,BitRange,Types,IntRange,BitRange).
58 extract_used_types_l([Expr|Erest],TypesI,IntRangeI,BitRangeI,Types,IntRange,BitRange) :-
59 extract_used_types1(Expr,TypesA,IntRangeA,BitRangeA),
60 merge_integer_info(IntRangeI,IntRangeA,IntRangeB),
61 merge_integer_info(BitRangeI,BitRangeA,BitRangeB),
62 ord_union(TypesI,TypesA,TypesB),
63 extract_used_types_l(Erest,TypesB,IntRangeB,BitRangeB,Types,IntRange,BitRange).
64
65 extract_type_information(Type,TExpr,Names,UsedTypesA,IntRangeA,BitRangeA) :-
66 extract_type_information2(Type,TExpr,Names,[],UsedTypesA,IntRangeA,BitRangeA).
67 extract_type_information2(T,_,_,_,[T],none,none) :-
68 basic_type(T).
69 extract_type_information2(integer,TExpr,_,Scope,[],IntRange,none) :-
70 extract_finite_integer_range(TExpr,Scope,IntRange).
71 extract_type_information2(set(Type),TExpr,_,Scope,UsedTypes,IntRange,BitRange) :-
72 extract_type_information_set(Type,TExpr,[elem|Scope],UsedTypes,IntRange,BitRange).
73 extract_type_information2(seq(Type),TExpr,_,Scope,UsedTypes,IntRange,BitRange) :-
74 extract_type_information2(set(couple(integer,Type)),TExpr,[],Scope,UsedTypes,IntRange,BitRange).
75 extract_type_information2(couple(A,B),TExpr,_,Scope,UsedTypes,IntRange,BitRange) :-
76 extract_type_information2(A,TExpr,[],[left|Scope],TypesA,IntRangeA,BitRangeA),
77 extract_type_information2(B,TExpr,[],[right|Scope],TypesB,IntRangeB,BitRangeB),
78 merge_integer_info(IntRangeA,IntRangeB,IntRange),
79 merge_integer_info(BitRangeA,BitRangeB,BitRange),
80 ord_union(TypesA,TypesB,UsedTypes).
81 extract_type_information2(pred,_Expr,Names,_Scope,Types,IntRange,BitRange) :-
82 treat_quantified_integers_as_sets(Names,Types,IntRange,BitRange).
83
84 treat_quantified_integers_as_sets(Names,[],none,Range) :-
85 include(is_integer_expr,Names,Integers),
86 foldl(extract_integer_as_set,Integers,none,Range).
87
88 is_integer_expr(TExpr) :- get_texpr_type(TExpr,integer).
89
90 % Basic idea: extract_finite_integer_range/3 returns the bitrange (used for simple
91 % integers), but we treat as if it was the intRange (used for integer sets)
92 extract_integer_as_set(TExpr,IntRangeI,IntRangeO) :-
93 extract_finite_integer_range(TExpr,[],IntRange),
94 merge_integer_info(IntRangeI,IntRange,IntRangeO).
95
96 extract_type_information_set(T,_,_,[T],none,none) :-
97 basic_type(T).
98 extract_type_information_set(integer,TExpr,Scope,[],BitRange,BitRange) :-
99 extract_finite_integer_range(TExpr,Scope,BitRange).
100 extract_type_information_set(couple(A,B),TExpr,Scope,UsedTypes,IntRange,BitRange) :-
101 extract_type_information_set(A,TExpr,[left|Scope],TypesA,IntRangeA,BitRangeA),
102 extract_type_information_set(B,TExpr,[right|Scope],TypesB,IntRangeB,BitRangeB),
103 merge_integer_info(IntRangeA,IntRangeB,IntRange),
104 merge_integer_info(BitRangeA,BitRangeB,BitRange),
105 ord_union(TypesA,TypesB,UsedTypes).
106
107 basic_type(boolean).
108 basic_type(global(_)).
109
110 higher_order_exception(member(Elem,THOSet),[Elem|Subsets]) :-
111 get_texpr_expr(THOSet,HOSet),
112 higher_order_exception2(HOSet,Subsets).
113 higher_order_exception2(total_function(Dom,Ran),[Dom,Ran]).
114 higher_order_exception2(total_injection(Dom,Ran),[Dom,Ran]).
115 higher_order_exception2(total_surjection(Dom,Ran),[Dom,Ran]).
116 higher_order_exception2(total_bijection(Dom,Ran),[Dom,Ran]).
117 higher_order_exception2(partial_function(Dom,Ran),[Dom,Ran]).
118 higher_order_exception2(partial_injection(Dom,Ran),[Dom,Ran]).
119 higher_order_exception2(partial_surjection(Dom,Ran),[Dom,Ran]).
120 higher_order_exception2(partial_bijection(Dom,Ran),[Dom,Ran]).
121 higher_order_exception2(total_relation(Dom,Ran),[Dom,Ran]).
122 higher_order_exception2(surjection_relation(Dom,Ran),[Dom,Ran]).
123
124
125 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
126 % Phase 3
127 % create the relations for the used types
128
129 % create_atoms_for_types(+Types,+IntegerRange,+BitstringRange,
130 % -Size,-Typemap,-Idmap,-Valuemap):
131 % Types is a list of used types
132 % IntegerRange is the range of used integers
133 % IntsetRange is the range of used integers that occur in a set and
134 % have each to be modelled as an atom.
135 % Typemap is an AVL map from used types to relations
136 % Idmap is an AVL map from some constants (including __true and __false
137 % for true and false) to a relation
138 % Valuemap in an AVL mapping from B values to Kodkod tuples
139 create_atoms_for_types(Types,IntegerRange,IntsetRange,Typemap,Idmap,Valuemap) :-
140 empty_avl(EmptyMap),
141 create_atoms_for_intsets(IntsetRange,EmptyMap,TM1),
142 create_atoms_for_integers(IntegerRange,TM1,TM2),
143 create_atoms_for_types2(Types,TM2,EmptyMap,EmptyMap,Typemap,Idmap,Valuemap).
144
145 create_atoms_for_intsets(none,Map,Map).
146 create_atoms_for_intsets(irange(A,B),MapIn,MapOut) :-
147 Size is B-A+1,
148 intset_relation_kodkod_name(Relname),
149 add_type_relation(integer,Relname,Size,intsetrel(Relname,A,B),MapIn,MapOut).
150
151 create_atoms_for_integers(none,Map,Map).
152 create_atoms_for_integers(irange(A,B),MapIn,MapOut) :-
153 pow2integer_relation_kodkod_name(Relname),
154 add_type_relation('__pow2integer',Relname,unknown,pow2rel(Relname,A,B),MapIn,MapOut).
155
156 add_type_relation(Type,RelationName,Size,Relspec,In,Out) :-
157 avl_store(Type,In,relation(RelationName,Size,Relspec),Out).
158 add_standard_relation(BType,KType,Id,Size,In,Out) :-
159 create_relation_for_type(Id,KType,Relspec),
160 avl_store(BType,In,relation(Id,Size,Relspec),Out).
161 add_global_type_relation(GType,RelationPrefix,Size,Id,In,Out) :-
162 unique_identifier(RelationPrefix,GType,Id),
163 add_standard_relation(global(GType),Id,Id,Size,In,Out).
164
165 create_atoms_for_types2([],TypeMap,IdMap,ValueMap,TypeMap,IdMap,ValueMap).
166 create_atoms_for_types2([Type|Trest],TMin,IDMin,VMin,TMout,IDMout,VMout) :-
167 create_atoms_for_type(Type,TMin,IDMin,VMin,TM,IDM,VM),
168 create_atoms_for_types2(Trest,TM,IDM,VM,TMout,IDMout,VMout).
169
170 create_atoms_for_type(boolean,TMIn,IdIn,VMIn,TMOut,IdOut,VMOut) :-
171 add_standard_relation(boolean,bool,bool,2,TMIn,TMOut),
172 lookup_constant_value(boolean_true,boolean,VTrue),
173 lookup_constant_value(boolean_false,boolean,VFalse),
174 assign_values_to_atoms([VTrue,VFalse],boolean,VMIn,VMOut),
175 assign_elements_to_atoms(['__kodkod__true','__kodkod__false'],bool,IdIn,IdOut).
176 create_atoms_for_type(global(G),TMIn,IdIn,VMIn,TMOut,IdOut,VMOut) :-
177 all_elements_of_type(G,ABValues),
178 sort(ABValues,BValues), % in case of random enumeration there are problems; see test 1666
179 % Note: all_elements_of_type now provides elements in sorted order; so sort/2 call is in principle not necessary anymore
180 length(BValues,Size),
181 add_global_type_relation(G,g,Size,RelId,TMIn,TMOut),
182 assign_values_to_atoms(BValues,global(G),VMIn,VMOut),
183 findall(E, is_b_global_constant(G,_,E), Elements),
184 assign_elements_to_atoms(Elements,RelId,IdIn,IdOut).
185
186 lookup_constant_value(Expr,Type,Value) :-
187 create_texpr(Expr,Type,[],TExpr),
188 empty_state(Empty),
189 b_compute_expression_nowf(TExpr,Empty,Empty,Value,'KODKOD constant',0).
190
191 assign_values_to_atoms(BValues,Type,VMin,VMout) :-
192 assign_values_to_atoms2(BValues,Type,0,VMin,VMout).
193 assign_values_to_atoms2([],_Type,_Index,ValueMap,ValueMap).
194 assign_values_to_atoms2([BValue|BVrest],Type,Index,VMin,VMout) :-
195 assign_value_to_atom(BValue,Type,Index,VMin,VM),
196 Index2 is Index+1,
197 assign_values_to_atoms2(BVrest,Type,Index2,VM,VMout).
198 assign_value_to_atom(BValue,Type,Index,VMin,VMout) :-
199 avl_store(Type:BValue,VMin,Index,VMout).
200
201 assign_elements_to_atoms(Elements,Type,IdMapIn,IdMapOut) :-
202 assign_elements_to_atoms2(Elements,Type,0,IdMapIn,IdMapOut).
203 assign_elements_to_atoms2([],_Type,_Index,IdMap,IdMap).
204 assign_elements_to_atoms2([Elem|Erest],Type,Index,IdMapIn,IdMapOut) :-
205 assign_element_to_atom(Elem,Type,Index,IdMapIn,IdMap),
206 Index2 is Index+1,
207 assign_elements_to_atoms2(Erest,Type,Index2,IdMap,IdMapOut).
208 assign_element_to_atom(Elem,Type,Index,In,Out) :-
209 unique_identifier(e,Elem,Id),
210 create_element_relation(Id,Type,Index,Rel),
211 avl_store(Elem,In,Rel,Out).
212
213 create_relation_for_type(Id,Type,Rel) :-
214 create_generic_relation(Id,[Type],set,exact,full,Rel).
215 create_element_relation(Id,Type,Index,Rel) :-
216 create_generic_relation(Id,[Type],set,exact,[tuple([Index])],Rel).
217 create_generic_relation(Id,Types,SetOrSingle,ExactOrSubset,TupleSet,reldef(Id,Types,SetOrSingle,ExactOrSubset,TupleSet)).
218
219 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
220 % Phase 4
221 % create the relations for global constants or variables (i.e. those identifiers
222 % which are not introduced by quantifiers)
223
224 create_identifier_relations(TIds,Typemap,Bits,IdMapIn,IdMapOut) :-
225 maplist(create_identifier_relation(Typemap,Bits),TIds,Ids,Rels),
226 foldl(store_in_avl,Ids,Rels,IdMapIn,IdMapOut).
227 store_in_avl(Id,Rel,In,Out) :-
228 avl_store(Id,In,Rel,Out).
229
230 create_identifier_relation(Typemap,Bits,TId,Id,Rel) :-
231 get_texpr_id(TId,Id),
232 get_texpr_type(TId,Type),
233 get_texpr_info(TId,Info),
234 unique_identifier(id,Id,RelId),
235 is_set_or_single(Type,SetOrSingle,RestType),
236 create_identifier_relation2(RestType,SetOrSingle,RelId,Info,Bits,Typemap,Rel).
237 create_identifier_relation2(integer,set,RelId,_Info,_Bits,_Typemap,Rel) :-
238 !,intset_relation_kodkod_name(Type),
239 create_generic_relation(RelId,[Type],set,subset,full,Rel).
240 create_identifier_relation2(integer,single,RelId,Info,Bits,_Typemap,Rel) :-
241 !,
242 % if the type does not fit into the bitset range, the choice is clear:
243 % we have to use the pow2 representation
244 (in_bitrange(Info,Bits) -> intset_relation_kodkod_name(Type) ; pow2integer_relation_kodkod_name(Type)),
245 create_generic_relation(RelId,[Type],single,subset,full,Rel).
246 create_identifier_relation2(RestType,SetOrSingle,RelId,_Info,_Bits,Typemap,Rel) :-
247 extract_ktypes(RestType,Typemap,Types),
248 create_generic_relation(RelId,Types,SetOrSingle,subset,full,Rel).
249
250 in_bitrange(Info,irange(BLow,BUp)) :-
251 integer_range(Info,Low,Up),
252 BLow =< Low,
253 Up =< BUp.
254 integer_range(Info,Lower,Upper) :-
255 memberchk(analysis(A),Info),
256 memberchk(interval:irange(Lower,Upper),A).
257
258
259 is_set_or_single(seq(T),set,couple(integer,T)) :- !.
260 is_set_or_single(set(T),set,T) :- !.
261 is_set_or_single(T,single,T).
262
263 extract_ktypes(couple(A,B),Typemap,Types) :- !,
264 extract_ktypes(A,Typemap,ATypes),
265 append(ATypes,BTypes,Types),
266 extract_ktypes(B,Typemap,BTypes).
267 extract_ktypes(Type,Typemap,[Name]) :-
268 avl_fetch(Type,Typemap,Relation),
269 Relation = relation(Name,_Size,_Relspec).
270
271
272 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
273 % Get all referenced relations in the Kodkod formula
274 /* currently not used:
275
276 remove_unused_relations(Typemap,Idmap,Valuemap,Formula,NTypemap,NIdmap,Valuemap) :-
277 get_used_relations(Formula,UsedRels),
278 remove_unused_idrelations(UsedRels,Idmap,NIdmap),
279 get_used_types_in_rels(NIdmap,UsedRels,UsedRels2),
280 remove_unused_types(Typemap,UsedRels2,NTypemap).
281
282 remove_unused_idrelations(UsedRels,Idmap,NIdmap) :-
283 avl_to_list(Idmap,IdList),
284 include(is_used_idrelation(UsedRels),IdList,NIdList),
285 list_to_avl(NIdList,NIdmap).
286 is_used_idrelation(UsedRels,_-reldef(Id,_,_,_,_)) :- memberchk(Id,UsedRels).
287
288 get_used_types_in_rels(Idmap,UsedRels,NewUsed) :-
289 avl_to_list(Idmap,IdList),
290 findall(T, (member(_-reldef(_,Ts,_,_,_),IdList),member(T,Ts)), Types),
291 append(UsedRels,Types,U2),
292 sort(U2,NewUsed).
293
294 remove_unused_types(Typemap,UsedRels,NTypemap) :-
295 avl_to_list(Typemap,TypeList),
296 include(is_used_type(UsedRels),TypeList,NTypeList),
297 list_to_avl(NTypeList,NTypemap).
298 is_used_type(UsedRels,_-relation(Id,_,_)) :- memberchk(Id,UsedRels).
299
300 get_used_relations(K,UsedRels) :-
301 get_used_relations2(K,U,[]),
302 sort(U,UsedRels).
303 get_used_relations2(relref(Id)) --> !,[Id].
304 get_used_relations2(K) -->
305 {compound(K),!,K =.. Args},get_used_relations_l(Args).
306 get_used_relations2(_K) --> [].
307 get_used_relations_l([]) --> [].
308 get_used_relations_l([K|Krest]) -->
309 get_used_relations2(K),
310 get_used_relations_l(Krest).
311 */