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