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).