1		% (c) 2009-2026 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		:- use_module(probsrc(bsyntaxtree),[is_set_type/2]).
114		is_seq_type(SeqType,T) :- is_set_type(SeqType,couple(integer,T)).
115		rewrite_pre(if_then_else(If,Then,Else),IsWd,Type,I,NExpr,Type,NI,multi/rewrite_if_then_else_expr,[],[]) :-
116		IsWd == 'FALSE',
117		Type \== pred,
118		!, % 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
119		% 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
120		rewrite_if_then_else_expr_to_b(if_then_else(If,Then,Else), NExpr),
121		NI = I.
122		rewrite_pre(let_expression(Ids,Exprs,Body),IsWd,Type,_,Unfolded,Type,NI,multi/unfold_let_expression,[],[]) :-
123		IsWd == 'FALSE',
124		!, % 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
125		% see above
126		replace_ids_by_exprs(Body, Ids, Exprs, b(Unfolded,_,NI)).
127		rewrite_pre(empty_sequence,_,Type,I,empty_set,set(couple(integer,T)),I,multi/empty_sequence_to_set,[],[]) :-
128		is_seq_type(Type,T).
129		rewrite_pre(general_concat(A),_,Type,I,empty_set,set(couple(integer,T)),I,multi/empty_general_concat,[],[]) :-
130		( A = b(empty_sequence,_,_) ; A = b(empty_set,_,_)),
131		is_seq_type(Type,T).
132		rewrite_pre(sequence_extension(SeqExtValues),_,SType,I,set_extension(SetExtValues),set(couple(integer,Type)),I,multi/seq_ext_to_set_ext,[],[]) :-
133		is_seq_type(SType,Type),
134		seq_ext_to_set_ext(SeqExtValues,1,Type,SetExtValues).
135		% change type of values to set instead of seq
136		%rewrite_pre(value(A),_,seq(integer),I,value(A),set(couple(integer,integer)),I,multi/replace_type_identifier,[],[]).
137		%rewrite_pre(value(A),_,seq(string),I,value(A),set(couple(string,string)),I,multi/replace_type_identifier,[],[]).
138
139		% seq(S)
140		% {f | f : NATURAL1 +-> S & #n.(n : NATURAL & dom(f) = 1..n)}
141		% warum nicht:
142		% {f | #n.(n : NATURAL & f : 1..n --> S)}
143		% scheint kein speedup zu liefern....
144		rewrite_pre(seq(S),_,set(SType),I,comprehension_set([F],Pred),set(set(couple(integer,Type))),I,multi/rewrite_seq,[],[]) :-
145		is_seq_type(SType,Type),
146		unique_typed_id("_smt_tmp",integer,N),
147		unique_typed_id("_smt_tmp",set(couple(integer,Type)),F),
148
149		% f : NATURAL1 +-> S
150		safe_create_texpr(partial_function(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartFunc),
151		safe_create_texpr(member(F,PartFunc),pred,FMember),
152
153		safe_create_texpr(member(N,b(integer_set('NATURAL'),set(integer),[])),pred,NMember),
154		safe_create_texpr(interval(b(integer(1),integer,[]),N),set(integer),Interval),
155		safe_create_texpr(domain(F),set(integer),Dom),
156		safe_create_texpr(equal(Dom,Interval),pred,DomIsEqualToInterval),
157
158		conjunct_predicates([NMember,DomIsEqualToInterval],ExistsInner),
159		create_exists([N],ExistsInner,Exists),
160		conjunct_predicates([Exists,FMember],Pred).
161
162		% seq1(S)
163		% {f | f : NATURAL1 +-> S & #n.(n : NATURAL1 & dom(f) = 1..n)}
164		% warum nicht:
165		% {f | #n.(n : NATURAL1 & f : 1..n +-> S)}
166		% scheint kein speedup zu liefern....
167		rewrite_pre(seq1(S),_,set(SType),I,comprehension_set([F],Pred),set(set(couple(integer,Type))),I,multi/rewrite_seq,[],[]) :-
168		is_seq_type(SType,Type),
169		unique_typed_id("_smt_tmp",integer,N),
170		unique_typed_id("_smt_tmp",set(couple(integer,Type)),F),
171
172		% f : NATURAL1 +-> S
173		safe_create_texpr(partial_function(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartFunc),
174		safe_create_texpr(member(F,PartFunc),pred,FMember),
175
176		safe_create_texpr(member(N,b(integer_set('NATURAL1'),set(integer),[])),pred,NMember),
177		safe_create_texpr(interval(b(integer(1),integer,[]),N),set(integer),Interval),
178		safe_create_texpr(domain(F),set(integer),Dom),
179		safe_create_texpr(equal(Dom,Interval),pred,DomIsEqualToInterval),
180
181		conjunct_predicates([NMember,DomIsEqualToInterval],ExistsInner),
182		create_exists([N],ExistsInner,Exists),
183		conjunct_predicates([Exists,FMember],Pred).
184
185		% iseq(S)
186		% {f | f : NATURAL1 +-> S & #n.(n : NATURAL & dom(f) = 1..n)} /\ (NATURAL1 >+> S)
187		% warum nicht:
188		% {f | #n.(n : NATURAL & f : 1..n +-> S )} /\ (NATURAL1 >+> S)
189		% scheint kein speedup zu liefern....
190		rewrite_pre(iseq(S),_,set(SType),I,intersection(CompSet,PartInj),set(set(couple(integer,Type))),I,multi/rewrite_seq,[],[]) :-
191		is_seq_type(SType,Type),
192		unique_typed_id("_smt_tmp",integer,N),
193		unique_typed_id("_smt_tmp",set(couple(integer,Type)),F),
194
195		% f : NATURAL1 +-> S
196		safe_create_texpr(partial_function(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartFunc),
197		safe_create_texpr(member(F,PartFunc),pred,FMember),
198
199		safe_create_texpr(member(N,b(integer_set('NATURAL'),set(integer),[])),pred,NMember),
200		safe_create_texpr(interval(b(integer(1),integer,[]),N),set(integer),Interval),
201		safe_create_texpr(domain(F),set(integer),Dom),
202		safe_create_texpr(equal(Dom,Interval),pred,DomIsEqualToInterval),
203
204		conjunct_predicates([NMember,DomIsEqualToInterval],ExistsInner),
205		create_exists([N],ExistsInner,Exists),
206		conjunct_predicates([Exists,FMember],Pred),
207		safe_create_texpr(comprehension_set([F],Pred),set(set(couple(integer,Type))),CompSet),
208
209		safe_create_texpr(partial_injection(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartInj).
210
211		% perm(S)
212		% {f | f : NATURAL1 +-> S & #n.(n : NATURAL & dom(f) = 1..n)} /\ (NATURAL1 >+> S) /\ (NATURAL1 +->> S)
213		% warum nicht:
214		% {f | #n.(n : NATURAL & f : 1..n +-> S )} /\ (NATURAL1 >+> S) /\ (NATURAL1 +->> S)
215		% scheint kein speedup zu liefern....
216		rewrite_pre(perm(S),_,set(SType),I,intersection(CompSet,Intersec),set(set(couple(integer,Type))),I,multi/rewrite_seq,[],[]) :-
217		is_seq_type(SType,Type),
218		unique_typed_id("_smt_tmp",integer,N),
219		unique_typed_id("_smt_tmp",set(couple(integer,Type)),F),
220
221		% f : NATURAL1 +-> S
222		safe_create_texpr(partial_function(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartFunc),
223		safe_create_texpr(member(F,PartFunc),pred,FMember),
224
225		safe_create_texpr(member(N,b(integer_set('NATURAL'),set(integer),[])),pred,NMember),
226		safe_create_texpr(interval(b(integer(1),integer,[]),N),set(integer),Interval),
227		safe_create_texpr(domain(F),set(integer),Dom),
228		safe_create_texpr(equal(Dom,Interval),pred,DomIsEqualToInterval),
229
230		conjunct_predicates([NMember,DomIsEqualToInterval],ExistsInner),
231		create_exists([N],ExistsInner,Exists),
232		conjunct_predicates([Exists,FMember],Pred),
233		safe_create_texpr(comprehension_set([F],Pred),set(set(couple(integer,Type))),CompSet),
234
235		safe_create_texpr(partial_injection(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartInj),
236		safe_create_texpr(partial_surjection(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),TotalSurj),
237		safe_create_texpr(intersection(PartInj,TotalSurj),pred,Intersec).
238
239		% replace size by card -> card performance really bad, timeout with around 20 elements
240		%rewrite_pre(size(A),integer,I,card(A),integer,I,multi/replace_size_card,[],[]).
241		% better take maximum of indices
242		%rewrite_pre(size(b(empty_sequence,_,_)),integer,I,b(integer(0),integer,[]),integer,I,multi/rewrite_size,[],[]).
243		rewrite_pre(size(S),_,integer,I,UnwrappedId,integer,I,multi/rewrite_size,[AC1,AC2],[UId]) :-
244		unique_typed_id("_smt_tmp",integer,UId),
245		get_texpr_expr(UId,UnwrappedId),
246		% two axioms:
247		% !(i,v).((i,v) : Set => uid >= x)
248		% uid=0 or #(i,v).((i,v) : Set & uid = x)
249		% Note: #(i,v) FAILS if set is empty
250
251		unique_typed_id("_smt_tmp",integer,Index),
252		get_texpr_type(S,Type),
253		get_set_type(Type,couple(integer,SeqType)),
254
255		unique_typed_id("_smt_tmp",SeqType,Value),
256		safe_create_texpr(couple(Index,Value),couple(integer,SeqType),QuantifiedVar),
257
258		safe_create_texpr(greater_equal(UId,Index),pred,GreaterEqual),
259		safe_create_texpr(equal(UId,Index),pred,Equal),
260		safe_create_texpr(member(QuantifiedVar,S),pred,QuantifiedInSet),
261		safe_create_texpr(integer(0),integer,Zero),
262		safe_create_texpr(equal(UId,Zero),pred,EqualZero),
263
264		conjunct_predicates([QuantifiedInSet,Equal],ExistsInner),
265		create_implication(QuantifiedInSet,GreaterEqual,ForallInner),
266
267		create_exists([Index,Value],ExistsInner,AC0),
268		disjunct_predicates([EqualZero,AC0],AC1),
269		create_forall([Index,Value],ForallInner,AC2).
270		% gets first element of non-empty seq
271		% card performance, solver answers unknown with >=13 elements (card timeout?)
272		%rewrite_pre(first(A),Type,I,UnwrappedId,Type,I,multi/rewrite_first,[AC],[UId]) :-
273		% unique_typed_id("_smt_tmp",integer,UId),
274		% get_texpr_expr(UId,UnwrappedId),
275
276		% safe_create_texpr(couple(b(integer(1),integer,[]),UId),couple(integer,Type),TheCouple),
277		% safe_create_texpr(member(TheCouple,A),pred,AC).
278		rewrite_pre(first(A),_,Type,I,function(A,b(integer(1),integer,[])),Type,I,multi/rewrite_first,[],[]).
279		% this should be handled by the function(...) itself
280		% safe_create_texpr(size(A),integer,Card).
281		% create_texpr(greater_equal(Card,b(integer(1),integer,[])),pred,[],AC).
282		% gets last element of non-empty seq
283		% card performance, solver answers unknown with >=13 elements (card timeout?)
284		rewrite_pre(last(A),_,Type,I,function(A,Card),Type,I,multi/rewrite_last,[],[]) :-
285		safe_create_texpr(size(A),integer,Card).
286		% this should be handled by the function(...) itself
287		% create_texpr(greater_equal(Card,b(integer(1),integer,[])),pred,[],AC).
288		% reverses sequence
289		rewrite_pre(rev(S),_,SType,I,comprehension_set([Index,Value],QuantifiedInSet),set(couple(integer,Type)),I,multi/rewrite_rev,[AC1],[TmpCard]) :-
290		is_seq_type(SType,Type),
291		% {(i,v) | (card(S)-i+1,b) : x}
292		safe_create_texpr(size(S),integer,Card),
293		unique_typed_id("_smt_tmp",integer,Index),
294		unique_typed_id("_smt_tmp",Type,Value),
295
296		% size is stored outside of the set comprehension using a temp. identifier
297		% to increase performance
298		unique_typed_id("_smt_tmp",integer,TmpCard),
299		safe_create_texpr(equal(TmpCard,Card),pred,AC1),
300
301		safe_create_texpr(minus(TmpCard,Index),integer,TmpIndex),
302		safe_create_texpr(add(TmpIndex,b(integer(1),integer,[])),integer,NIndex),
303		safe_create_texpr(couple(NIndex,Value),couple(integer,Type),TheCouple),
304
305		safe_create_texpr(member(TheCouple,S),pred,QuantifiedInSet).
306		% concat returns S2 concatenated to S1 as a Sequence
307		rewrite_pre(concat(S1,S2),_,SType,I,comprehension_set([Index,Value],Disjunct),set(couple(integer,Type)),I,multi/rewrite_concat,[AC1],[TmpCard]) :-
308		is_seq_type(SType,Type),
309		% {(i,v) | (i,v) : S1 or (i-card(S1),v) : S2}
310		unique_typed_id("_smt_tmp",integer,Index),
311		unique_typed_id("_smt_tmp",Type,Value),
312
313		safe_create_texpr(size(S1),integer,Card1),
314		% size is stored outside of the set comprehension using a temp. identifier
315		% to increase performance
316		unique_typed_id("_smt_tmp",integer,TmpCard),
317		safe_create_texpr(equal(TmpCard,Card1),pred,AC1),
318
319		safe_create_texpr(couple(Index,Value),couple(integer,Type),QuantifiedVar),
320		% (i,v) : S1
321		safe_create_texpr(member(QuantifiedVar,S1),pred,QuantifiedInSet1),
322
323		% (i-card(S1),v) : S2
324		safe_create_texpr(minus(Index,TmpCard),integer,NIndex),
325		safe_create_texpr(couple(NIndex,Value),couple(integer,Type),QuantifiedVar2),
326		safe_create_texpr(member(QuantifiedVar2,S2),pred,QuantifiedInSet2),
327
328		disjunct_predicates([QuantifiedInSet1,QuantifiedInSet2],Disjunct).
329		% restrict_front returns the first N elements of the sequence S as a Sequence
330		rewrite_pre(restrict_front(S,N),_,SType,I,comprehension_set([Index,Value],Conjunct),set(couple(integer,Type)),I,multi/rewrite_restrict_front,[],[]) :-
331		is_seq_type(SType,Type),
332		% {(i,v) | (i,v) : S & i <= N}
333		unique_typed_id("_smt_tmp",integer,Index),
334		unique_typed_id("_smt_tmp",Type,Value),
335		safe_create_texpr(couple(Index,Value),couple(integer,Type),QuantifiedVar),
336		% (i,v) : S
337		safe_create_texpr(member(QuantifiedVar,S),pred,QuantifiedInSet),
338		% i <= N
339		safe_create_texpr(less_equal(Index,N),pred,LessEqual),
340
341		conjunct_predicates([QuantifiedInSet,LessEqual],Conjunct).
342		% restrict_tail returns the sequence S without the first N elements
343		% special case to increase performance
344		rewrite_pre(restrict_tail(S,N),_,SType,I,SExpr,set(couple(integer,Type)),I,multi/rewrite_restrict_tail_special,[],[]) :-
345		is_seq_type(SType,Type),
346		get_texpr_expr(N,integer(0)), !,
347		get_texpr_expr(S,SExpr).
348		rewrite_pre(restrict_tail(S,N),_,SType,I,comprehension_set([Index,Value],Conjunct),set(couple(integer,Type)),I,multi/rewrite_restrict_tail,[],[]) :-
349		is_seq_type(SType,Type),
350		% {(i,v) | (i+N,v) : S & i > 0}
351		unique_typed_id("_smt_tmp",integer,Index),
352		unique_typed_id("_smt_tmp",Type,Value),
353		%create_texpr(couple(Index,Value),couple(integer,Type),[],AC),
354
355		% NIndex = i+N
356		create_texpr(add(N,Index),integer,[],NIndex),
357		safe_create_texpr(couple(NIndex,Value),couple(integer,Type),TheCouple),
358		safe_create_texpr(member(TheCouple,S),pred,QuantifiedInSet),
359
360		% i > 0
361		safe_create_texpr(integer(0),integer,Null),
362		safe_create_texpr(greater(Index,Null),pred,GreaterEqual),
363
364		conjunct_predicates([QuantifiedInSet,GreaterEqual],Conjunct).
365		% prepends element E to Sequence S
366		rewrite_pre(insert_front(E,S),_,SType,I,union(AC,CompSet),set(couple(integer,Type)),I,multi/rewrite_insert_front,[],[]) :-
367		is_seq_type(SType,Type),
368		% {(i,v) | (i-1,v) : S or (i = 1 & v = E)}
369		% easier to code: {(i,v) | (i-1,v) : S} \/ {(1,E)}
370		% {(1,E)}
371		safe_create_texpr(set_extension([b(couple(b(integer(1),integer,[]),E),couple(integer,Type),[])]),set(couple(integer,Type)),AC),
372
373		% {(i,v) | (i-1,v) : S}
374		unique_typed_id("_smt_tmp",integer,Index),
375		unique_typed_id("_smt_tmp",Type,Value),
376
377		safe_create_texpr(minus(Index,b(integer(1),integer,[])),integer,NIndex),
378		safe_create_texpr(couple(NIndex,Value),couple(integer,Type),TheCouple),
379		safe_create_texpr(member(TheCouple,S),pred,QuantifiedInSet),
380
381		safe_create_texpr(comprehension_set([Index,Value],QuantifiedInSet),set(couple(integer,Type)),CompSet).
382		% append element S <- E: S \/ {(size(S)+1,E)}
383		rewrite_pre(insert_tail(S,E),_,SType,I,union(S,AC),set(couple(integer,Type)),I,multi/rewrite_insert_tail,[],[]) :-
384		is_seq_type(SType,Type),
385		% NIndex = size(S)+1
386		safe_create_texpr(size(S),integer,Card),
387		safe_create_texpr(add(Card,b(integer(1),integer,[])),integer,NIndex),
388		% AC = {(NIndex,E)}
389		safe_create_texpr(set_extension([b(couple(NIndex,E),couple(integer,Type),[])]),set(couple(integer,Type)),AC).
390		% get front: S - {(size(S),function(S,size(S)))}
391		%rewrite_pre(front(A),seq(Type),I,restrict_front(A,N),seq(Type),I,multi/rewrite_front,[],[]) :-
392		% safe_create_texpr(size(A),integer,Card),
393		% safe_create_texpr(minus(Card,b(integer(1),integer,[])),integer,N).
394		rewrite_pre(front(A),_,SType,I,set_subtraction(A,AC),set(couple(integer,Type)),I,multi/rewrite_front,[],[]) :-
395		is_seq_type(SType,Type),
396		safe_create_texpr(size(A),integer,Card),
397		safe_create_texpr(function(A,Card),Type,Last),
398		% AC = {(size(A),function(A,size(A)))}
399		safe_create_texpr(set_extension([b(couple(Card,Last),couple(integer,Type),[])]),set(couple(integer,Type)),AC).
400		rewrite_pre(tail(S),_,SType,I,comprehension_set([Index,Value],Conjunct),set(couple(integer,Type)),I,multi/rewrite_tail,[],[]) :-
401		is_seq_type(SType,Type),
402		% {(i,v) | (i+1,v) : S & i > 0}
403		unique_typed_id("_smt_tmp",integer,Index),
404		unique_typed_id("_smt_tmp",Type,Value),
405
406		% (i+1,v) : S
407		safe_create_texpr(add(Index,b(integer(1),integer,[])),integer,NIndex),
408		safe_create_texpr(couple(NIndex,Value),couple(integer,Type),TheCouple),
409		safe_create_texpr(member(TheCouple,S),pred,QuantifiedInSet),
410
411		% i > 0
412		safe_create_texpr(greater(Index,b(integer(0),integer,[])),pred,Greater),
413
414		conjunct_predicates([QuantifiedInSet,Greater],Conjunct).
415		% Change seq -> set(couple(...))
416		rewrite_pre(A,_,TypeIn,I,A,TypeOut,I,multi/replace_seq_type_by_set_type,[],[]) :-
417		normalize_type(TypeIn,TypeOut), TypeIn \= TypeOut.
418
419		% iseq and permutation introduce member of intersection. split again to make cleanup easier later on
420		rewrite_post_with_path(member(X,Intersection),pred,I,conjunct(Member1,Member2),pred,I,multi/split_member_of_intersection,_,[],[]) :-
421		get_texpr_expr(Intersection,intersection(SetA,SetB)),
422		safe_create_texpr(member(X,SetA),pred,Member1),
423		safe_create_texpr(member(X,SetB),pred,Member2).
424
425		seq_ext_to_set_ext([],_,_,[]).
426		seq_ext_to_set_ext([H|T],Counter,Type,[b(couple(CounterAsBExpr,H),couple(integer,Type),[])|List]) :-
427		NCounter is Counter + 1,
428		safe_create_texpr(integer(Counter),integer,CounterAsBExpr),
429		seq_ext_to_set_ext(T,NCounter,Type,List).