1 % (c) 2014-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(kodkod_rewrite,[ apply_rewriting_rules/2 ]).
6
7 :- use_module(probsrc(module_information),[module_info/2]).
8 :- module_info(group,kodkod).
9 :- module_info(description,'This module contains rewriting rules that are applied during tge translation to Kodkod.').
10
11 :- use_module(library(lists)).
12 :- use_module(probsrc(bsyntaxtree)).
13 :- use_module(kodkod_tools).
14
15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16 % applying re-writing rules to make some statements translatable to Kodkod
17
18 apply_rewriting_rules(TExpr,NTExpr) :-
19 remove_bt(TExpr,Expr,NExpr,NTExpr),
20 get_texpr_info(TExpr,Info),
21 apply_rewriting_rules_pre(Expr,Info,IExpr),
22 syntaxtransformation(IExpr,Subs,_,NSubs,Expr1),
23 maplist(apply_rewriting_rules,Subs,NSubs),
24 apply_rewriting_rules_post(Expr1,Info,NExpr).
25 apply_rewriting_rules_pre(Expr,Info,NExpr) :-
26 kodkod_rewrite_pre(Expr,Info,Expr1),!,
27 apply_rewriting_rules_pre(Expr1,Info,NExpr).
28 apply_rewriting_rules_pre(Expr,_,Expr).
29 apply_rewriting_rules_post(Expr,Info,NExpr) :-
30 kodkod_rewrite_post(Expr,Info,Expr1),!,
31 apply_rewriting_rules_post(Expr1,Info,NExpr).
32 apply_rewriting_rules_post(Expr,_,Expr).
33
34 :- use_module(probsrc(bsyntaxtree),[get_texpr_set_type/2, replace_ids_by_exprs/4]).
35 kodkod_rewrite_pre(let_expression(Ids,Exprs,Body),_,Res) :- !, % expand LET expression
36 replace_ids_by_exprs(Body,Ids,Exprs,b(NewBody,_,I2)),
37 (kodkod_rewrite_pre(NewBody,I2,Res2) -> Res=Res2; Res = NewBody).
38 kodkod_rewrite_pre(let_predicate(Ids,Exprs,Body),_,Res) :- !, % expand LET predicate
39 replace_ids_by_exprs(Body,Ids,Exprs,b(NewBody,_,I2)),
40 (kodkod_rewrite_pre(NewBody,I2,Res2) -> Res=Res2; Res = NewBody).
41 kodkod_rewrite_pre(not_equal(A,B),_,negation(Equal)) :- !,
42 create_kk_tpred(equal(A,B),Equal).
43 kodkod_rewrite_pre(member(Elem,Powset),_,Result) :-
44 get_texpr_expr(Powset,PExpr),
45 get_texpr_info(Elem,ElemInfo),
46 ? kodkod_rewrite_membership(PExpr,Elem,ElemInfo,Result),
47 !.
48 kodkod_rewrite_pre(subset(Subset,Powset),_,forall([Elem],TPre,TCond)) :-
49 get_texpr_info(Subset,Info),
50 get_texpr_set_type(Subset,ElemType),
51 unique_identifier(TId),
52 element_analysis(Info,ElemInfo),
53 create_texpr(identifier(TId),ElemType,ElemInfo,Elem),
54 get_texpr_expr(Powset,PExpr),
55 kodkod_rewrite_membership(PExpr,Elem,ElemInfo,Cond),!,
56 create_texpr(member(Elem,Subset),pred,[],TPre),
57 create_texpr(Cond,pred,[],TCond).
58 kodkod_rewrite_pre(size(Seq),_,card(Seq)) :- !.
59 kodkod_rewrite_post(interval(A,B),Info,comprehension_set([TmpId],Predicate)) :- !,
60 element_analysis(Info,ElemInfo),
61 unique_identifier(TId),
62 create_texpr(identifier(TId),integer,ElemInfo,TmpId),
63 create_texpr(less_equal(A,TmpId),pred,[],Left),
64 create_texpr(less_equal(TmpId,B),pred,[],Right),
65 conjunct_predicates([Left,Right],Predicate).
66 kodkod_rewrite_post(sequence_extension(Elems),_Info,set_extension(Pairs)) :- !,
67 convert_elements_to_pairs(Elems,1,Pairs).
68 kodkod_rewrite_post(general_sum([TId],Pred,Expr),_Info,general_sum([TId],NPred,Expr)) :-
69 get_texpr_id(TId,Id), get_texpr_id(TElem,Id),
70 extract_finite_integer_range(TId,[],IRange),
71 \+ get_texpr_expr(Pred,member(TElem,_TSet)),!,
72 write('rewritten\n'),
73 create_texpr(comprehension_set([TId],Pred),set(integer),[analysis([elem(interval):IRange])],
74 TCompSet),
75 create_texpr(member(TId,TCompSet),pred,[],NPred).
76 convert_elements_to_pairs([],_,[]).
77 convert_elements_to_pairs([Elem|Erest],Index,[Pair|Prest]) :-
78 convert_element_to_pair(Elem,Index,Pair),
79 I2 is Index + 1,
80 convert_elements_to_pairs(Erest,I2,Prest).
81 convert_element_to_pair(Elem,Index,Pair) :-
82 Range = irange(Index,Index),
83 create_texpr(integer(Index),integer,[analysis([interval:Range])],TIndex),
84 get_texpr_type(Elem,Type),
85 get_texpr_info(Elem,EInfo),
86 findall(right(Scope):Info,
87 ( memberchk(analysis(AInfos),EInfo),member(Scope:Info,AInfos)),
88 RInfos),
89 create_texpr(couple(TIndex,Elem),couple(integer,Type),[analysis([left(interval):Range|RInfos])],Pair).
90
91 kodkod_rewrite_membership(pow_subset(Set),Elem,_,subset(Elem,Set)).
92 kodkod_rewrite_membership(fin_subset(Set),Elem,_,subset(Elem,Set)).
93 kodkod_rewrite_membership(relations(A,B),Elem,_,subset(Elem,Cartesian)) :-
94 create_kk_tpred(cartesian_product(A,B),Cartesian).
95 kodkod_rewrite_membership(pow1_subset(Set),Elem,ElemInfo,conjunct(Subset,Exists)) :-
96 get_texpr_set_type(Set,Type),
97 create_texpr(identifier('___elem'),Type,[kodkod|ElemInfo],Id),
98 create_kk_tpred(subset(Elem,Set),Subset),
99 create_kk_tpred(exists([Id],Member),Exists),
100 create_kk_tpred(member(Id,Set),Member).
101 kodkod_rewrite_membership(fin1_subset(Set),Elem,Info,Pred) :-
102 kodkod_rewrite_membership(pow1_subset(Set),Elem,Info,Pred).
103 kodkod_rewrite_membership(interval(A,B),Elem,_,conjunct(Lower,Upper)) :-
104 create_kk_tpred(less_equal(A,Elem),Lower),
105 create_kk_tpred(less_equal(Elem,B),Upper).
106 kodkod_rewrite_membership(integer_set('NATURAL'),Elem,_,less_equal(Zero,Elem)) :-
107 create_integer_with_analysis(0,Zero).
108 kodkod_rewrite_membership(integer_set('NATURAL1'),Elem,_,less_equal(One,Elem)) :-
109 create_integer_with_analysis(1,One).
110 create_kk_tpred(Pred,TPred) :-
111 create_texpr(Pred,pred,[kodkod],TPred).
112 create_integer_with_analysis(I,Expr) :-
113 create_texpr(integer(I),integer,[analysis([interval:irange(I,I)])],Expr).
114
115 element_analysis(SetInfo,[analysis(MemberInfo)]) :-
116 findall( S:R,
117 ( member(analysis(Analysis), SetInfo),
118 member(elem(S):R,Analysis)),
119 MemberInfo).