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