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 % the element analysis of Subset can be derived from this subset predicate itself,
55 % e.g. for t/\s <: 1..z with z<1; the translation of a forall with an inconsistent
56 % identifier as true would then be wrong
57 \+ is_inconsistent_expression(Elem),
58 get_texpr_expr(Powset,PExpr),
59 kodkod_rewrite_membership(PExpr,Elem,ElemInfo,Cond),!,
60 create_texpr(member(Elem,Subset),pred,[],TPre),
61 create_texpr(Cond,pred,[],TCond).
62 kodkod_rewrite_pre(size(Seq),_,card(Seq)) :- !.
63 kodkod_rewrite_post(interval(A,B),Info,comprehension_set([TmpId],Predicate)) :- !,
64 element_analysis(Info,ElemInfo),
65 unique_identifier(TId),
66 create_texpr(identifier(TId),integer,ElemInfo,TmpId),
67 create_texpr(less_equal(A,TmpId),pred,[],Left),
68 create_texpr(less_equal(TmpId,B),pred,[],Right),
69 conjunct_predicates([Left,Right],Predicate).
70 kodkod_rewrite_post(sequence_extension(Elems),_Info,set_extension(Pairs)) :- !,
71 convert_elements_to_pairs(Elems,1,Pairs).
72 kodkod_rewrite_post(general_sum([TId],Pred,Expr),_Info,general_sum([TId],NPred,Expr)) :-
73 get_texpr_id(TId,Id), get_texpr_id(TElem,Id),
74 extract_finite_integer_range(TId,[],IRange),
75 \+ get_texpr_expr(Pred,member(TElem,_TSet)),!,
76 create_texpr(comprehension_set([TId],Pred),set(integer),[analysis([elem(interval):IRange])],
77 TCompSet),
78 create_texpr(member(TId,TCompSet),pred,[],NPred).
79 convert_elements_to_pairs([],_,[]).
80 convert_elements_to_pairs([Elem|Erest],Index,[Pair|Prest]) :-
81 convert_element_to_pair(Elem,Index,Pair),
82 I2 is Index + 1,
83 convert_elements_to_pairs(Erest,I2,Prest).
84 convert_element_to_pair(Elem,Index,Pair) :-
85 Range = irange(Index,Index),
86 create_texpr(integer(Index),integer,[analysis([interval:Range])],TIndex),
87 get_texpr_type(Elem,Type),
88 get_texpr_info(Elem,EInfo),
89 findall(right(Scope):Info,
90 ( memberchk(analysis(AInfos),EInfo),member(Scope:Info,AInfos)),
91 RInfos),
92 create_texpr(couple(TIndex,Elem),couple(integer,Type),[analysis([left(interval):Range|RInfos])],Pair).
93
94 kodkod_rewrite_membership(pow_subset(Set),Elem,_,subset(Elem,Set)).
95 kodkod_rewrite_membership(fin_subset(Set),Elem,_,subset(Elem,Set)).
96 kodkod_rewrite_membership(relations(A,B),Elem,_,subset(Elem,Cartesian)) :-
97 create_kk_tpred(cartesian_product(A,B),Cartesian).
98 kodkod_rewrite_membership(pow1_subset(Set),Elem,ElemInfo,conjunct(Subset,Exists)) :-
99 get_texpr_set_type(Set,Type),
100 create_texpr(identifier('___elem'),Type,[kodkod|ElemInfo],Id),
101 create_kk_tpred(subset(Elem,Set),Subset),
102 create_kk_tpred(exists([Id],Member),Exists),
103 create_kk_tpred(member(Id,Set),Member).
104 kodkod_rewrite_membership(fin1_subset(Set),Elem,Info,Pred) :-
105 kodkod_rewrite_membership(pow1_subset(Set),Elem,Info,Pred).
106 kodkod_rewrite_membership(interval(A,B),Elem,_,conjunct(Lower,Upper)) :-
107 create_kk_tpred(less_equal(A,Elem),Lower),
108 create_kk_tpred(less_equal(Elem,B),Upper).
109 kodkod_rewrite_membership(integer_set('NATURAL'),Elem,_,less_equal(Zero,Elem)) :-
110 create_integer_with_analysis(0,Zero).
111 kodkod_rewrite_membership(integer_set('NATURAL1'),Elem,_,less_equal(One,Elem)) :-
112 create_integer_with_analysis(1,One).
113 create_kk_tpred(Pred,TPred) :-
114 create_texpr(Pred,pred,[kodkod],TPred).
115 create_integer_with_analysis(I,Expr) :-
116 create_texpr(integer(I),integer,[analysis([interval:irange(I,I)])],Expr).
117
118 element_analysis(SetInfo,[analysis(MemberInfo)]) :-
119 findall( S:R,
120 ( member(analysis(Analysis), SetInfo),
121 member(elem(S):R,Analysis)),
122 MemberInfo).