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