1 | % (c) 2009-2016 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(seq_rewriter, [rewrite_seq_to_set/2]). | |
6 | ||
7 | :- use_module(probsrc(module_information),[module_info/2]). | |
8 | :- module_info(group,smt_solvers). | |
9 | :- module_info(description,'This module implements transformations of sequences to sets as needed by the SMT-LIB translation.'). | |
10 | ||
11 | :- use_module(library(lists),[maplist/3, | |
12 | append/2, | |
13 | is_list/1, | |
14 | include/3]). | |
15 | ||
16 | :- use_module(probsrc(bsyntaxtree),[remove_bt/4, | |
17 | create_texpr/4, | |
18 | safe_create_texpr/3, | |
19 | get_texpr_expr/2, | |
20 | get_texpr_type/2, | |
21 | conjunct_predicates/2, | |
22 | disjunct_predicates/2, | |
23 | create_forall/3, | |
24 | create_exists/3, | |
25 | create_implication/3, | |
26 | syntaxtransformation/5, | |
27 | unique_typed_id/3, | |
28 | find_typed_identifier_uses/2]). | |
29 | :- use_module(probsrc(error_manager), [add_internal_error/2, | |
30 | add_error_fail/3]). | |
31 | :- use_module(probsrc(typing_tools), [normalize_type/2]). | |
32 | ||
33 | :- use_module(smt_common_predicates). | |
34 | ||
35 | rewrite_seq_to_set(Expr,Out) :- | |
36 | %translate:translate_bexpression(Expr,PPExpr), | |
37 | %write(before(PPExpr)),nl, | |
38 | %write(before(Expr)),nl, | |
39 | rewrite_seq_to_set(Expr,CExpr,[],AC,IDs), | |
40 | % translate:translate_bexpression(CExpr,PPCExpr), | |
41 | % write(after(PPCExpr)),nl, | |
42 | combine_pred_and_ac(CExpr,AC,IDs,Out). % Do not call regular ast_cleanup afterwards: It undoes some of the changes done here | |
43 | rewrite_seq_to_set(Expr,CExprOut,Path,ACOut,IDsOut) :- | |
44 | rewrites(pre,Expr,[],TPExpr,Path,ACPre,IDsPre), | |
45 | remove_bt(TPExpr,PExpr,LExpr,TLExpr), | |
46 | syntaxtransformation(PExpr,Subs,_,NewSubs,LExpr), | |
47 | functor(PExpr,F,N), | |
48 | % recursively clean up sub-expressions | |
49 | maplist(rewrite_seq_to_set,ACPre,ACPreClean), | |
50 | rewrite_seq_to_set_l(Subs,NewSubs,F/N,1,Path,ACL,IDsL), | |
51 | maplist(rewrite_seq_to_set,ACL,ACLClean), | |
52 | rewrites(post,TLExpr,[],CExpr,Path,ACPost,IDsPost), | |
53 | maplist(rewrite_seq_to_set,ACPost,ACPostClean), | |
54 | append([ACPreClean,ACLClean,ACPostClean],AC), | |
55 | append([IDsPre,IDsL,IDsPost],IDs), | |
56 | (get_texpr_type(CExpr,pred) | |
57 | -> combine_pred_and_ac(CExpr,AC,IDs,CExprOut), IDsOut = [], ACOut = [] | |
58 | ; CExprOut = CExpr, ACOut = AC, IDsOut = IDs). | |
59 | ||
60 | combine_pred_and_ac(Pred,AC,IDs,Out) :- | |
61 | conjunct_predicates(AC,ACPred), | |
62 | conjunct_predicates([Pred,ACPred],OutInnerPred), | |
63 | create_exists(IDs,OutInnerPred,Out). | |
64 | ||
65 | rewrite_seq_to_set_l([],[],_Functor,_Nr,_Path,[],[]). | |
66 | rewrite_seq_to_set_l([Expr|Rest],[CExpr|CRest],Functor,ArgNr,Path,AC,IDs) :- | |
67 | rewrite_seq_to_set(Expr,CExpr,[arg(Functor,ArgNr)|Path],ACC,IDsC), | |
68 | A1 is ArgNr+1, | |
69 | rewrite_seq_to_set_l(Rest,CRest,Functor,A1,Path,ACL,IDsL), | |
70 | append(ACC,ACL,AC), | |
71 | append(IDsC,IDsL,IDs). | |
72 | ||
73 | rewrites(Phase,Expr,AppliedRules,Result,Path,ACS,IDs) :- | |
74 | assure_single_rules(AppliedRules,Rule), | |
75 | ( rewrite_phase(Phase,Expr,NExpr,Mode/Rule,Path,ACPhase,IDsPhase) -> % try to apply a rule (matching the current phase) | |
76 | ( Mode==single -> AppRules = [Rule|AppliedRules] % if the rule is marked as "single", we add to the list of already applied rules | |
77 | ; Mode==multi -> AppRules = AppliedRules % if "multi", we do not add it to the list, the rule might be applied more than once | |
78 | ; otherwise -> add_error_fail(ast_cleanup_for_smt,'Unexpected rule mode ',Mode)), | |
79 | rewrites(Phase,NExpr,AppRules,Result,Path,ACRec,IDsRec), % continue recursively with the new expression | |
80 | append(ACPhase,ACRec,ACS), append(IDsPhase,IDsRec,IDs) | |
81 | ; otherwise -> % if no rule matches anymore, | |
82 | Result = Expr, % we leave the expression unmodified | |
83 | ACS = [], IDs = [], | |
84 | Rule = none). % and unblock the co-routine (see assure_single_rules/2) | |
85 | ||
86 | assure_single_rules([],_Rule) :- !. | |
87 | assure_single_rules(AppliedRules,Rule) :- | |
88 | assure_single_rules2(AppliedRules,Rule). | |
89 | :- block assure_single_rules2(?,-). | |
90 | assure_single_rules2(_AppliedRules,none) :- !. | |
91 | assure_single_rules2(AppliedRules,Rule) :- | |
92 | \+ member(Rule, AppliedRules). | |
93 | ||
94 | rewrite_phase(Phase,OTExpr,NTExpr,Mode/Rule,Path,AC,IDs) :- | |
95 | create_texpr(OExpr,OType,OInfo,OTExpr), | |
96 | create_texpr(NExpr,NType,NInfo,NTExpr), | |
97 | rewrite_phase2(Phase,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path,AC,IDs). | |
98 | rewrite_phase2(pre,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,_Path,AC,IDs) :- | |
99 | rewrite_pre(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule,AC,IDs), | |
100 | (functor(Mode_Rule,'/',2) -> Mode_Rule = Mode/Rule | |
101 | ; add_internal_error('Illegal cleanup_pre rule, missing mode: ',Mode_Rule),fail). | |
102 | rewrite_phase2(post,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path,AC,IDs) :- | |
103 | rewrite_post_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule,Path,AC,IDs), | |
104 | (functor(Mode_Rule,'/',2) | |
105 | -> Mode_Rule = Mode/Rule %,format(' rewrite_post Rule: ~w/~w~n',[Mode,Rule]) | |
106 | ; add_internal_error('Illegal rewrite_post rule, missing mode: ',Mode_Rule),fail). | |
107 | ||
108 | rewrite_pre(empty_sequence,seq(T),I,empty_set,set(couple(integer,T)),I,multi/empty_sequence_to_set,[],[]). | |
109 | rewrite_pre(sequence_extension(SeqExtValues),seq(Type),I,set_extension(SetExtValues),set(couple(integer,Type)),I,multi/seq_ext_to_set_ext,[],[]) :- | |
110 | seq_ext_to_set_ext(SeqExtValues,1,Type,SetExtValues). | |
111 | ||
112 | % change type of values to set instead of seq | |
113 | %rewrite_pre(value(A),seq(integer),I,value(A),set(couple(integer,integer)),I,multi/replace_type_identifier,[],[]). | |
114 | %rewrite_pre(value(A),seq(string),I,value(A),set(couple(string,string)),I,multi/replace_type_identifier,[],[]). | |
115 | ||
116 | % seq(S) | |
117 | % {f | f : NATURAL1 +-> S & #n.(n : NATURAL & dom(f) = 1..n)} | |
118 | % warum nicht: | |
119 | % {f | #n.(n : NATURAL & f : 1..n --> S)} | |
120 | % scheint kein speedup zu liefern.... | |
121 | rewrite_pre(seq(S),set(seq(Type)),I,comprehension_set([F],Pred),set(set(couple(integer,Type))),I,multi/rewrite_seq,[],[]) :- | |
122 | unique_typed_id("_smt_tmp",integer,N), | |
123 | unique_typed_id("_smt_tmp",set(couple(integer,Type)),F), | |
124 | ||
125 | % f : NATURAL1 +-> S | |
126 | safe_create_texpr(partial_function(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartFunc), | |
127 | safe_create_texpr(member(F,PartFunc),pred,FMember), | |
128 | ||
129 | safe_create_texpr(member(N,b(integer_set('NATURAL'),set(integer),[])),pred,NMember), | |
130 | safe_create_texpr(interval(b(integer(1),integer,[]),N),set(integer),Interval), | |
131 | safe_create_texpr(domain(F),set(integer),Dom), | |
132 | safe_create_texpr(equal(Dom,Interval),pred,DomIsEqualToInterval), | |
133 | ||
134 | conjunct_predicates([NMember,DomIsEqualToInterval],ExistsInner), | |
135 | create_exists([N],ExistsInner,Exists), | |
136 | conjunct_predicates([Exists,FMember],Pred). | |
137 | ||
138 | % seq1(S) | |
139 | % {f | f : NATURAL1 +-> S & #n.(n : NATURAL1 & dom(f) = 1..n)} | |
140 | % warum nicht: | |
141 | % {f | #n.(n : NATURAL1 & f : 1..n +-> S)} | |
142 | % scheint kein speedup zu liefern.... | |
143 | rewrite_pre(seq1(S),set(seq(Type)),I,comprehension_set([F],Pred),set(set(couple(integer,Type))),I,multi/rewrite_seq,[],[]) :- | |
144 | unique_typed_id("_smt_tmp",integer,N), | |
145 | unique_typed_id("_smt_tmp",set(couple(integer,Type)),F), | |
146 | ||
147 | % f : NATURAL1 +-> S | |
148 | safe_create_texpr(partial_function(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartFunc), | |
149 | safe_create_texpr(member(F,PartFunc),pred,FMember), | |
150 | ||
151 | safe_create_texpr(member(N,b(integer_set('NATURAL1'),set(integer),[])),pred,NMember), | |
152 | safe_create_texpr(interval(b(integer(1),integer,[]),N),set(integer),Interval), | |
153 | safe_create_texpr(domain(F),set(integer),Dom), | |
154 | safe_create_texpr(equal(Dom,Interval),pred,DomIsEqualToInterval), | |
155 | ||
156 | conjunct_predicates([NMember,DomIsEqualToInterval],ExistsInner), | |
157 | create_exists([N],ExistsInner,Exists), | |
158 | conjunct_predicates([Exists,FMember],Pred). | |
159 | ||
160 | % iseq(S) | |
161 | % {f | f : NATURAL1 +-> S & #n.(n : NATURAL & dom(f) = 1..n)} /\ (NATURAL1 >+> S) | |
162 | % warum nicht: | |
163 | % {f | #n.(n : NATURAL & f : 1..n +-> S )} /\ (NATURAL1 >+> S) | |
164 | % scheint kein speedup zu liefern.... | |
165 | rewrite_pre(iseq(S),set(seq(Type)),I,intersection(CompSet,PartInj),set(set(couple(integer,Type))),I,multi/rewrite_seq,[],[]) :- | |
166 | unique_typed_id("_smt_tmp",integer,N), | |
167 | unique_typed_id("_smt_tmp",set(couple(integer,Type)),F), | |
168 | ||
169 | % f : NATURAL1 +-> S | |
170 | safe_create_texpr(partial_function(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartFunc), | |
171 | safe_create_texpr(member(F,PartFunc),pred,FMember), | |
172 | ||
173 | safe_create_texpr(member(N,b(integer_set('NATURAL'),set(integer),[])),pred,NMember), | |
174 | safe_create_texpr(interval(b(integer(1),integer,[]),N),set(integer),Interval), | |
175 | safe_create_texpr(domain(F),set(integer),Dom), | |
176 | safe_create_texpr(equal(Dom,Interval),pred,DomIsEqualToInterval), | |
177 | ||
178 | conjunct_predicates([NMember,DomIsEqualToInterval],ExistsInner), | |
179 | create_exists([N],ExistsInner,Exists), | |
180 | conjunct_predicates([Exists,FMember],Pred), | |
181 | safe_create_texpr(comprehension_set([F],Pred),set(set(couple(integer,Type))),CompSet), | |
182 | ||
183 | safe_create_texpr(partial_injection(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartInj). | |
184 | ||
185 | % perm(S) | |
186 | % {f | f : NATURAL1 +-> S & #n.(n : NATURAL & dom(f) = 1..n)} /\ (NATURAL1 >+> S) /\ (NATURAL1 +->> S) | |
187 | % warum nicht: | |
188 | % {f | #n.(n : NATURAL & f : 1..n +-> S )} /\ (NATURAL1 >+> S) /\ (NATURAL1 +->> S) | |
189 | % scheint kein speedup zu liefern.... | |
190 | rewrite_pre(perm(S),set(seq(Type)),I,intersection(CompSet,Intersec),set(set(couple(integer,Type))),I,multi/rewrite_seq,[],[]) :- | |
191 | unique_typed_id("_smt_tmp",integer,N), | |
192 | unique_typed_id("_smt_tmp",set(couple(integer,Type)),F), | |
193 | ||
194 | % f : NATURAL1 +-> S | |
195 | safe_create_texpr(partial_function(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartFunc), | |
196 | safe_create_texpr(member(F,PartFunc),pred,FMember), | |
197 | ||
198 | safe_create_texpr(member(N,b(integer_set('NATURAL'),set(integer),[])),pred,NMember), | |
199 | safe_create_texpr(interval(b(integer(1),integer,[]),N),set(integer),Interval), | |
200 | safe_create_texpr(domain(F),set(integer),Dom), | |
201 | safe_create_texpr(equal(Dom,Interval),pred,DomIsEqualToInterval), | |
202 | ||
203 | conjunct_predicates([NMember,DomIsEqualToInterval],ExistsInner), | |
204 | create_exists([N],ExistsInner,Exists), | |
205 | conjunct_predicates([Exists,FMember],Pred), | |
206 | safe_create_texpr(comprehension_set([F],Pred),set(set(couple(integer,Type))),CompSet), | |
207 | ||
208 | safe_create_texpr(partial_injection(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartInj), | |
209 | safe_create_texpr(partial_surjection(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),TotalSurj), | |
210 | safe_create_texpr(intersection(PartInj,TotalSurj),pred,Intersec). | |
211 | ||
212 | % replace size by card -> card performance really bad, timeout with around 20 elements | |
213 | %rewrite_pre(size(A),integer,I,card(A),integer,I,multi/replace_size_card,[],[]). | |
214 | % better take maximum of indices | |
215 | %rewrite_pre(size(b(empty_sequence,_,_)),integer,I,b(integer(0),integer,[]),integer,I,multi/rewrite_size,[],[]). | |
216 | rewrite_pre(size(S),integer,I,UnwrappedId,integer,I,multi/rewrite_size,[AC1,AC2],[UId]) :- | |
217 | unique_typed_id("_smt_tmp",integer,UId), | |
218 | get_texpr_expr(UId,UnwrappedId), | |
219 | % two axioms: | |
220 | % !(i,v).((i,v) : Set => uid >= x) | |
221 | % #(i,v).((i,v) : Set & uid = x) | |
222 | ||
223 | unique_typed_id("_smt_tmp",integer,Index), | |
224 | ||
225 | (get_texpr_type(S,seq(SeqType)), ! | |
226 | ; get_texpr_type(S,set(couple(integer,SeqType)))), | |
227 | ||
228 | unique_typed_id("_smt_tmp",SeqType,Value), | |
229 | safe_create_texpr(couple(Index,Value),couple(integer,SeqType),QuantifiedVar), | |
230 | ||
231 | safe_create_texpr(greater_equal(UId,Index),pred,GreaterEqual), | |
232 | safe_create_texpr(equal(UId,Index),pred,Equal), | |
233 | safe_create_texpr(member(QuantifiedVar,S),pred,QuantifiedInSet), | |
234 | ||
235 | conjunct_predicates([QuantifiedInSet,Equal],ExistsInner), | |
236 | create_implication(QuantifiedInSet,GreaterEqual,ForallInner), | |
237 | ||
238 | create_exists([Index,Value],ExistsInner,AC1), | |
239 | create_forall([Index,Value],ForallInner,AC2). | |
240 | % gets first element of non-empty seq | |
241 | % card performance, solver answers unknown with >=13 elements (card timeout?) | |
242 | %rewrite_pre(first(A),Type,I,UnwrappedId,Type,I,multi/rewrite_first,[AC],[UId]) :- | |
243 | % unique_typed_id("_smt_tmp",integer,UId), | |
244 | % get_texpr_expr(UId,UnwrappedId), | |
245 | ||
246 | % safe_create_texpr(couple(b(integer(1),integer,[]),UId),couple(integer,Type),TheCouple), | |
247 | % safe_create_texpr(member(TheCouple,A),pred,AC). | |
248 | rewrite_pre(first(A),Type,I,function(A,b(integer(1),integer,[])),Type,I,multi/rewrite_first,[],[]). | |
249 | % this should be handled by the function(...) itself | |
250 | % safe_create_texpr(size(A),integer,Card). | |
251 | % create_texpr(greater_equal(Card,b(integer(1),integer,[])),pred,[],AC). | |
252 | % gets last element of non-empty seq | |
253 | % card performance, solver answers unknown with >=13 elements (card timeout?) | |
254 | rewrite_pre(last(A),integer,I,function(A,Card),integer,I,multi/rewrite_last,[],[]) :- | |
255 | safe_create_texpr(size(A),integer,Card). | |
256 | % this should be handled by the function(...) itself | |
257 | % create_texpr(greater_equal(Card,b(integer(1),integer,[])),pred,[],AC). | |
258 | % reverses sequence | |
259 | rewrite_pre(rev(S),seq(Type),I,comprehension_set([Index,Value],QuantifiedInSet),set(couple(integer,Type)),I,multi/rewrite_rev,[AC1],[TmpCard]) :- | |
260 | % {(i,v) | (card(S)-i+1,b) : x} | |
261 | safe_create_texpr(size(S),integer,Card), | |
262 | unique_typed_id("_smt_tmp",Type,Index), | |
263 | unique_typed_id("_smt_tmp",Type,Value), | |
264 | ||
265 | % size is stored outside of the set comprehension using a temp. identifier | |
266 | % to increase performance | |
267 | unique_typed_id("_smt_tmp",integer,TmpCard), | |
268 | safe_create_texpr(equal(TmpCard,Card),pred,AC1), | |
269 | ||
270 | safe_create_texpr(minus(TmpCard,Index),integer,TmpIndex), | |
271 | safe_create_texpr(add(TmpIndex,b(integer(1),integer,[])),integer,NIndex), | |
272 | safe_create_texpr(couple(NIndex,Value),couple(integer,Type),TheCouple), | |
273 | ||
274 | safe_create_texpr(member(TheCouple,S),pred,QuantifiedInSet). | |
275 | % concat returns S2 concatenated to S1 as a Sequence | |
276 | rewrite_pre(concat(S1,S2),seq(Type),I,comprehension_set([Index,Value],Disjunct),set(couple(integer,Type)),I,multi/rewrite_concat,[AC1],[TmpCard]) :- | |
277 | % {(i,v) | (i,v) : S1 or (i-card(S1),v) : S2} | |
278 | unique_typed_id("_smt_tmp",integer,Index), | |
279 | unique_typed_id("_smt_tmp",Type,Value), | |
280 | ||
281 | safe_create_texpr(size(S1),integer,Card1), | |
282 | % size is stored outside of the set comprehension using a temp. identifier | |
283 | % to increase performance | |
284 | unique_typed_id("_smt_tmp",integer,TmpCard), | |
285 | safe_create_texpr(equal(TmpCard,Card1),pred,AC1), | |
286 | ||
287 | safe_create_texpr(couple(Index,Value),couple(integer,Type),QuantifiedVar), | |
288 | % (i,v) : S1 | |
289 | safe_create_texpr(member(QuantifiedVar,S1),pred,QuantifiedInSet1), | |
290 | ||
291 | % (i-card(S1),v) : S2 | |
292 | safe_create_texpr(minus(Index,TmpCard),integer,NIndex), | |
293 | safe_create_texpr(couple(NIndex,Value),couple(integer,Type),QuantifiedVar2), | |
294 | safe_create_texpr(member(QuantifiedVar2,S2),pred,QuantifiedInSet2), | |
295 | ||
296 | disjunct_predicates([QuantifiedInSet1,QuantifiedInSet2],Disjunct). | |
297 | % restrict_front returns the first N elements of the sequence S as a Sequence | |
298 | rewrite_pre(restrict_front(S,N),seq(Type),I,comprehension_set([Index,Value],Conjunct),set(couple(integer,Type)),I,multi/rewrite_restrict_front,[],[]) :- | |
299 | % {(i,v) | (i,v) : S & i <= N} | |
300 | unique_typed_id("_smt_tmp",integer,Index), | |
301 | unique_typed_id("_smt_tmp",Type,Value), | |
302 | safe_create_texpr(couple(Index,Value),couple(integer,Type),QuantifiedVar), | |
303 | % (i,v) : S | |
304 | safe_create_texpr(member(QuantifiedVar,S),pred,QuantifiedInSet), | |
305 | % i <= N | |
306 | safe_create_texpr(less_equal(Index,N),pred,LessEqual), | |
307 | ||
308 | conjunct_predicates([QuantifiedInSet,LessEqual],Conjunct). | |
309 | % restrict_tail returns the sequence S without the first N elements | |
310 | % special case to increase performance | |
311 | rewrite_pre(restrict_tail(S,N),seq(Type),I,SExpr,set(couple(integer,Type)),I,multi/rewrite_restrict_tail_special,[],[]) :- | |
312 | get_texpr_expr(N,integer(0)), !, | |
313 | get_texpr_expr(S,SExpr). | |
314 | rewrite_pre(restrict_tail(S,N),seq(Type),I,comprehension_set([Index,Value],Conjunct),set(couple(integer,Type)),I,multi/rewrite_restrict_tail,[],[]) :- | |
315 | % {(i,v) | (i+N,v) : S & i > 0} | |
316 | unique_typed_id("_smt_tmp",integer,Index), | |
317 | unique_typed_id("_smt_tmp",Type,Value), | |
318 | %create_texpr(couple(Index,Value),couple(integer,Type),[],AC), | |
319 | ||
320 | % NIndex = i+N | |
321 | create_texpr(add(N,Index),integer,[],NIndex), | |
322 | safe_create_texpr(couple(NIndex,Value),couple(integer,Type),TheCouple), | |
323 | safe_create_texpr(member(TheCouple,S),pred,QuantifiedInSet), | |
324 | ||
325 | % i > 0 | |
326 | safe_create_texpr(integer(0),integer,Null), | |
327 | safe_create_texpr(greater(Index,Null),pred,GreaterEqual), | |
328 | ||
329 | conjunct_predicates([QuantifiedInSet,GreaterEqual],Conjunct). | |
330 | % prepends element E to Sequence S | |
331 | rewrite_pre(insert_front(E,S),seq(Type),I,union(AC,CompSet),set(couple(integer,Type)),I,multi/rewrite_insert_front,[],[]) :- | |
332 | % {(i,v) | (i-1,v) : S or (i = 1 & v = E)} | |
333 | % easier to code: {(i,v) | (i-1,v) : S} \/ {(1,E)} | |
334 | % {(1,E)} | |
335 | safe_create_texpr(set_extension([b(couple(b(integer(1),integer,[]),E),couple(integer,Type),[])]),set(couple(integer,Type)),AC), | |
336 | ||
337 | % {(i,v) | (i-1,v) : S} | |
338 | unique_typed_id("_smt_tmp",integer,Index), | |
339 | unique_typed_id("_smt_tmp",Type,Value), | |
340 | ||
341 | safe_create_texpr(minus(Index,b(integer(1),integer,[])),integer,NIndex), | |
342 | safe_create_texpr(member(TheCouple,S),pred,QuantifiedInSet), | |
343 | safe_create_texpr(couple(NIndex,Value),couple(integer,Type),TheCouple), | |
344 | ||
345 | safe_create_texpr(comprehension_set([Index,Value],QuantifiedInSet),set(couple(integer,Type)),CompSet). | |
346 | % append element S <- E: S \/ {(size(S)+1,E)} | |
347 | rewrite_pre(insert_tail(S,E),seq(Type),I,union(S,AC),set(couple(integer,Type)),I,multi/rewrite_insert_tail,[],[]) :- | |
348 | % NIndex = size(S)+1 | |
349 | safe_create_texpr(size(S),integer,Card), | |
350 | safe_create_texpr(add(Card,b(integer(1),integer,[])),integer,NIndex), | |
351 | % AC = {(NIndex,E)} | |
352 | safe_create_texpr(set_extension([b(couple(NIndex,E),couple(integer,Type),[])]),set(couple(integer,Type)),AC). | |
353 | % get front: S - {(size(S),function(S,size(S)))} | |
354 | %rewrite_pre(front(A),seq(Type),I,restrict_front(A,N),seq(Type),I,multi/rewrite_front,[],[]) :- | |
355 | % safe_create_texpr(size(A),integer,Card), | |
356 | % safe_create_texpr(minus(Card,b(integer(1),integer,[])),integer,N). | |
357 | rewrite_pre(front(A),seq(Type),I,set_subtraction(A,AC),set(couple(integer,Type)),I,multi/rewrite_front,[],[]) :- | |
358 | safe_create_texpr(size(A),integer,Card), | |
359 | safe_create_texpr(function(A,Card),Type,Last), | |
360 | % AC = {(size(A),function(A,size(A)))} | |
361 | safe_create_texpr(set_extension([b(couple(Card,Last),couple(integer,Type),[])]),set(couple(integer,Type)),AC). | |
362 | rewrite_pre(tail(S),seq(Type),I,comprehension_set([Index,Value],Conjunct),set(couple(integer,Type)),I,multi/rewrite_tail,[],[]) :- | |
363 | % {(i,v) | (i+1,v) : S & i > 0} | |
364 | unique_typed_id("_smt_tmp",integer,Index), | |
365 | unique_typed_id("_smt_tmp",Type,Value), | |
366 | ||
367 | % (i+1,v) : S | |
368 | safe_create_texpr(add(Index,b(integer(1),integer,[])),integer,NIndex), | |
369 | safe_create_texpr(couple(NIndex,Value),couple(integer,Type),TheCouple), | |
370 | safe_create_texpr(member(TheCouple,S),pred,QuantifiedInSet), | |
371 | ||
372 | % i > 0 | |
373 | safe_create_texpr(greater(Index,b(integer(0),integer,[])),pred,Greater), | |
374 | ||
375 | conjunct_predicates([QuantifiedInSet,Greater],Conjunct). | |
376 | % Change seq -> set(couple(...)) | |
377 | rewrite_pre(A,TypeIn,I,A,TypeOut,I,multi/replace_seq_type_by_set_type,[],[]) :- | |
378 | normalize_type(TypeIn,TypeOut), TypeIn \= TypeOut. | |
379 | ||
380 | % iseq and permutation introduce member of intersection. split again to make cleanup easier later on | |
381 | rewrite_post_with_path(member(X,Intersection),pred,I,conjunct(Member1,Member2),pred,I,multi/split_member_of_intersection,_,[],[]) :- | |
382 | get_texpr_expr(Intersection,intersection(SetA,SetB)), | |
383 | safe_create_texpr(member(X,SetA),pred,Member1), | |
384 | safe_create_texpr(member(X,SetB),pred,Member2). | |
385 | ||
386 | seq_ext_to_set_ext([],_,_,[]). | |
387 | seq_ext_to_set_ext([H|T],Counter,Type,[b(couple(CounterAsBExpr,H),couple(integer,Type),[])|List]) :- | |
388 | NCounter is Counter + 1, | |
389 | safe_create_texpr(integer(Counter),integer,CounterAsBExpr), | |
390 | seq_ext_to_set_ext(T,NCounter,Type,List). |