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 | ||
6 | :- module(b_compiler,[b_compile/6, b_optimize/6, b_compile_closure/2]). | |
7 | ||
8 | :- use_module(library(lists)). | |
9 | ||
10 | :- use_module(self_check). | |
11 | :- use_module(bsyntaxtree). | |
12 | :- use_module(error_manager). | |
13 | :- use_module(debug,[debug_format/3]). | |
14 | :- use_module(btypechecker,[fasttype/2]). | |
15 | :- use_module(bmachine,[b_get_machine_operation_for_animation/6]). | |
16 | :- use_module(b_interpreter). | |
17 | :- use_module(custom_explicit_sets). | |
18 | :- use_module(kernel_waitflags,[add_error_wf/5, add_internal_error_wf/5]). | |
19 | %:- use_module(bmachine,[b_operation_reads_output_variables/3]). | |
20 | ||
21 | :- use_module(module_information,[module_info/2]). | |
22 | :- module_info(group,interpreter). | |
23 | :- module_info(description,'This module compiles set comprehensions into closures; making them independent of the state of the B machine.'). | |
24 | ||
25 | /* compile boolean expression into a closure where the local state and the global | |
26 | state has been incorporated, but any parameter is left in the closure */ | |
27 | ||
28 | :- public test_bexpr/3, test_bexpr2/3. | |
29 | test_bexpr(Expr,[bind(cc,int(1)),bind(nn,int(2))], [bind(db,[(int(1),int(2))])]) :- | |
30 | fasttype( +conjunct( +conjunct( +member( global('Name')<<identifier(nn), +identifier('Name')), | |
31 | +member( global('Code')<<identifier(cc), +identifier('Code'))), | |
32 | +not_member( global('Name')<<identifier(nn), | |
33 | +domain(set(couple(global('Name'),global('Code')))<<identifier(db)))), Expr). | |
34 | ||
35 | test_bexpr2(Expr,[],[]) :- | |
36 | fasttype( +implication( +equal( seq(any)<<identifier(ss), +empty_sequence), | |
37 | +equal( set(any)<<identifier(res), +empty_set)), Expr). | |
38 | ||
39 | ||
40 | ||
41 | b_compile_closure(closure(P,T,Body),Res) :- b_compiler:b_compile(Body,P,[],[],CBody),!, Res=closure(P,T,CBody). | |
42 | b_compile_closure(C,C). | |
43 | ||
44 | ||
45 | % difference with b_compile: the states LS, S will not be thrown away by the interpreter | |
46 | % thus: we do not have to compile all accesses, in particular lazy lookups ! | |
47 | %b_optimize(TExpr,Parameters,_LS,_S,NTExpr,_WF) :- TExpr=b(_,_,Infos), member(already_optimized,Infos), | |
48 | % !, NTExpr=TExpr. | |
49 | b_optimize(TExpr,Parameters,LS,S,NTExpr,WF) :- %print('OPTIMIZE: '),translate:print_bexpr(TExpr),nl, trace, | |
50 | append(LS,[bind('$do_not_force_lazy_lookups',pred_true)],NewLS), | |
51 | b_compile(TExpr,Parameters,NewLS,S,NTExpr,WF). | |
52 | %bsyntaxtree:add_texpr_info_if_new(NTExpr,already_optimized,ResTExpr). | |
53 | ||
54 | b_compile(TExpr,Parameters,NewLS,S,NTExpr) :- | |
55 | b_compile(TExpr,Parameters,NewLS,S,NTExpr,no_wf_available). % for unit tests | |
56 | ||
57 | :- assert_must_succeed(( b_compiler:test_bexpr(E,L,S), | |
58 | b_compiler:b_compile(E,[nn],L,S,_R) )). | |
59 | :- assert_must_succeed(( b_compiler:test_bexpr2(E,L,S), | |
60 | b_compiler:b_compile(E,[ss,res],L,S,_R) )). | |
61 | :- assert_must_succeed(( b_compiler:b_compile(b(greater(b(value(int(2)),integer,[]), | |
62 | b(value(int(1)),integer,[])),pred,[]),[],[],[],Res), | |
63 | check_eq(Res,b(truth,pred,_)) )). | |
64 | :- assert_must_succeed(( b_compiler:b_compile(b(greater(b(value(int(2)),integer,[]), | |
65 | b(value(int(3)),integer,[])),pred,[]),[],[],[],Res), | |
66 | check_eq(Res,b(falsity,pred,_)) )). | |
67 | :- assert_must_succeed(( E = b(greater(b(value(int(2)),integer,[]), | |
68 | b(value(int(_)),integer,[])),pred,[]), | |
69 | b_compiler:b_compile(E,[],[],[],Res), | |
70 | check_eq(Res,E) )). | |
71 | :- assert_must_succeed(( E = b(greater(b(value(int(2)),integer,[]), | |
72 | b(value(_),integer,[])),pred,[]), | |
73 | b_compiler:b_compile(E,[],[],[],Res), | |
74 | check_eq(Res,E) )). | |
75 | :- assert_must_succeed(( E = b(greater(b(value(int(2)),integer,[]), | |
76 | b(identifier(x),integer,[])),pred,[]), | |
77 | b_compiler:b_compile(E,[],[bind(x,int(1))],[],Res), | |
78 | check_eq(Res,b(truth,pred,_)) )). | |
79 | :- assert_must_succeed(( E = b(greater(b(value(int(2)),integer,[]), | |
80 | b(identifier(x),integer,[])),pred,[]), | |
81 | b_compiler:b_compile(E,[],[bind(x,int(3))],[],Res), | |
82 | check_eq(Res,b(falsity,pred,_)) )). | |
83 | ||
84 | %:- assert_pre(b_compiler:b_compile_boolean_expression(E,Parameters,LS,S,_), | |
85 | % (type_check(E,boolean_expression),type_check(Parameters,list(variable_id)), | |
86 | % type_check(LS,store),type_check(S,store))). | |
87 | %:- assert_post(b_compiler:b_compile_boolean_expression(_,_,_,_,E), type_check(E,boolean_expression)). | |
88 | ||
89 | /* probably not worthwhile: | |
90 | b_compile(TExpr,Parameters,LS,S,NTExpr) :- get_texpr_info(TExpr,Info), | |
91 | (memberchk(compiled(Parameters),Info) -> NTExpr = TExpr ,print(already_compiled(Parameters)),nl, translate:print_bexpr(TExpr),nl | |
92 | ; b_compile0(TExpr,Parameters,LS,S,b(E,T,I)), translate:print(compiling(Parameters)),nl, translate:print_bexpr(TExpr),nl, | |
93 | NTExpr = b(E,T,[compiled(Parameters)|I])). | |
94 | */ | |
95 | :- use_module(closures,[get_recursive_identifier_of_closure_body/2]). | |
96 | b_compile(TExpr,Parameters,LS,S,NTExpr,WF) :- | |
97 | check_is_id_list(Parameters,Parameters0), | |
98 | (get_recursive_identifier_of_closure_body(TExpr,TRID), | |
99 | def_get_texpr_id(TRID,RID), nonmember(bind(RID,_),LS) | |
100 | -> Parameters1=[RID|Parameters0] % add recursive ID virtually to parameters to avoid error messages | |
101 | ; Parameters1=Parameters0), | |
102 | % print('compile : '),translate:print_bexpr(TExpr),nl, statistics(runtime,[Start,_]),%% | |
103 | sort(Parameters1,Parameters2), | |
104 | if(b_compile1(TExpr,Parameters2,LS,S,NTExpr0,eval,FullyKnown,WF), | |
105 | (FullyKnown=true | |
106 | -> copy_pos_infos(TExpr,NTExpr0,NTExpr) | |
107 | % ensure position info is not deleted if full expression compiled away, see PROB-412 (test 1677) | |
108 | ; NTExpr=NTExpr0), | |
109 | (add_internal_error_wf(b_compiler,'Compilation failed: ',TExpr,TExpr,WF), | |
110 | %b_compile1(TExpr,Parameters1,LS,S,NTExpr0,eval,_FullyKnown,WF), | |
111 | NTExpr = TExpr) | |
112 | ). | |
113 | %, bsyntaxtree:check_ast(NTExpr). | |
114 | %, check_infos(TExpr,NTExpr). | |
115 | %, print('compiled: '), translate:print_bexpr(NTExpr), print(' '),statistics(runtime,[Stop,_]), T is Stop-Start, print(T), print(' ms '),nl, bsyntaxtree:check_ast(NTExpr). % , print(NTExpr),nl. check_ast | |
116 | ||
117 | /* | |
118 | check_infos(Old,New) :- bsyntaxtree:get_texpr_info(Old,IO), | |
119 | bsyntaxtree:get_texpr_info(New,IN), | |
120 | member(X,IO), \+ member(X,IN), | |
121 | bsyntaxtree:important_info(X), | |
122 | print(check_infos(Old,New)),nl, | |
123 | print('Not copied: '), print(X),fail. | |
124 | check_infos(_,_). */ | |
125 | ||
126 | :- use_module(bsyntaxtree,[always_well_defined/1]). | |
127 | :- use_module(translate,[translate_bexpression_with_limit/2]). | |
128 | %:- use_module(hit_profiler,[add_profile_hit/1]). | |
129 | ||
130 | % Eval=eval means the expression will be needed in a successful branch and we can pre-compute more aggressively | |
131 | % Eval=false means the expression may not be needed (e.g., in a disjunction) and only perform efficient precomputations | |
132 | b_compile1(TExpr,Parameters,LS,S,ResultTExpr,Eval,FullyKnown1,WF) :- | |
133 | TExpr = b(Expr,Type,Infos), | |
134 | NTExpr = b(NewUntypedExpr,Type,NewInfos), | |
135 | %remove_bt(TExpr,Expr,NewUntypedExpr,NTExpr), % remove top-level Type Information | |
136 | %hit_profiler:add_profile_hit(Expr), | |
137 | %functor(Expr,E1,N1), %print(start_compile(E1/N1,Eval,FullyKnown1)),nl, | |
138 | b_compile1_infos(Expr,Type,Infos,Parameters,LS,S,NewUntypedExpr,NewInfos,Eval,FullyKnown,WF), | |
139 | %functor(NewUntypedExpr,E2,N2), | |
140 | %format(' compiled ~w/~w -> ~w/~w : ',[E1,N1,E2,N2]),translate:print_bexpr_or_subst(NTExpr),nl, | |
141 | %format(' fully=~w, eval=~w~n',[FullyKnown,Eval]), | |
142 | (NTExpr = b(value(_),_,_) | |
143 | -> FullyKnown1=FullyKnown, ResultTExpr=NTExpr | |
144 | ; FullyKnown=true, evaluate_this(Eval,NewUntypedExpr,Type,NewInfos) | |
145 | -> % print('eval : '),translate:print_bexpr(NTExpr),nl, % | |
146 | (nonvar(NewUntypedExpr), | |
147 | % if( would be more prudent !?, also: we used to call b_compute_expression_nowf | |
148 | b_interpreter:b_compute_expression(NTExpr,LS,S,ResultValue,WF) | |
149 | -> %print(result(ResultValue)),nl, | |
150 | %remove_bt(TExpr,Expr,value(ResultValue),ResultTExpr) | |
151 | get_texpr_type(TExpr,TT),ResultTExpr = b(value(ResultValue),TT,[]), | |
152 | FullyKnown1 = FullyKnown | |
153 | %, print(compiled_value(ResultTExpr)),nl | |
154 | ; add_internal_error_wf(b_compiler,'Undefined value marked for evaluation:',NTExpr,Infos,WF), | |
155 | %trace, b_interpreter:b_compute_expression(NTExpr,LS,S,ResultValue,WF), | |
156 | ResultTExpr=NTExpr, FullyKnown1=false | |
157 | ) | |
158 | ; % ((FullyKnown=true, NTExpr\=b(value(_),_,_)) -> format('not eval: ~w (~w)~n',[NTExpr,Eval]) ; true), | |
159 | ResultTExpr=NTExpr, FullyKnown1=false | |
160 | ). | |
161 | ||
162 | ||
163 | :- use_module(library(ordsets),[ord_member/2, ord_union/3]). | |
164 | :- use_module(bsyntaxtree,[create_exists_or_let_predicate/3]). | |
165 | :- use_module(tools_lists,[delete_first/3]). | |
166 | add_parameters(SortedIds,NewIds,NewSortedIds) :- | |
167 | sort(NewIds,SNew), | |
168 | ord_union(SortedIds,SNew,NewSortedIds). | |
169 | ||
170 | b_compile1_infos(exists(ExistsPara,Pred),_,OldInfos,Parameters,LS,S,NExpr,NewInfos,Eval,FullyKnown,WF) :- !, | |
171 | FullyKnown=false, % predicates never automatically evaluated in b_compile1 | |
172 | get_texpr_ids(ExistsPara,AtomicIds), | |
173 | add_parameters(Parameters,AtomicIds,NParameters), | |
174 | b_compile1(Pred,NParameters,LS,S,NPred,Eval,_FullyKnown1,WF), | |
175 | (is_falsity(NPred) -> NExpr = falsity, NewInfos = OldInfos | |
176 | ; is_truth(NPred) -> NExpr = truth, NewInfos = OldInfos | |
177 | %; Pred==NPred, write(unchanged(Parameters)),nl, member(used_ids(Old),OldInfos), print(used(Old)),nl,nl,fail | |
178 | ; create_exists_or_let_predicate(ExistsPara,NPred,b(NExpr,pred,NI)), | |
179 | %print('COMPILED EXISTS: '), translate:print_bexpr(b(NExpr,pred,NI)),nl, | |
180 | (delete_first(OldInfos,used_ids(_),I1), | |
181 | member(used_ids(NewUsedIds),NI) -> NewInfos = [used_ids(NewUsedIds)|I1] | |
182 | ; %nl,print(missing_used_ids(OldInfos,NI)),nl, % can happen when we construt a let_predicate above | |
183 | update_infos(NExpr,OldInfos,Parameters,NewInfos)) | |
184 | ). | |
185 | b_compile1_infos(identifier(Id),Type,OldInfos,Parameters,LS,S,NExpr,NewInfos,_Eval,FullyKnown,WF) :- !, | |
186 | ( ord_member(Id,Parameters) -> | |
187 | NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos | |
188 | ; Id=op(_) -> | |
189 | NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos | |
190 | ; b_interpreter:lookup_value_in_store_and_global_sets_wf(Id,Type,LS,S,Value,OldInfos,WF) -> | |
191 | NExpr = value(Value), (known_value(Value) -> FullyKnown=true ; FullyKnown=false), | |
192 | NewInfos = [was_identifier(Id)|OldInfos] | |
193 | ; add_internal_error_wf(b_compiler,'Compilation of identifier failed: ',Id,OldInfos,WF), | |
194 | NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos | |
195 | ). | |
196 | b_compile1_infos(Expr,_,OldInfos,_Parameters,_LS,_S,NewUntypedExpr,NewInfos,_Eval,FullyKnown,_WF) :- | |
197 | b_ast_cleanup:is_integer_set(Expr,_Set),!, | |
198 | NewUntypedExpr=Expr, NewInfos=OldInfos,FullyKnown=true. | |
199 | b_compile1_infos(operation_call_in_expr(Operation,OpCallParas),_Type,OldInfos,Parameters,LS,S, | |
200 | Compiled,NewInfos,Eval,FullyKnown,WF) :- !, | |
201 | def_get_texpr_id(Operation,op(OperationName)), | |
202 | FullyKnown = false, | |
203 | b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF), | |
204 | b_get_operation_normalized_read_write_info(OperationName,ReadVars,Modified), | |
205 | %exclude(operation_identifier,Read,ReadVars), % Read used to contain operations used via operation_call_in_expr; TO DO: check if this is ok in other places of source code of ProB; see test 1957 | |
206 | (Modified=[] -> true | |
207 | ; add_error_wf(b_compiler,'Calling operation that modifies state in expression:',OperationName,OldInfos,WF)), | |
208 | % print(compile_call_op(OperationName,ReadVars,Modified,OpCallParaValues)),nl, | |
209 | (ReadVars=[] | |
210 | -> Compiled = operation_call_in_expr(Operation,OpCallParaValues), | |
211 | NewInfos = OldInfos | |
212 | ; maplist(create_value_for_read_variable(LS,S,WF),ReadVars,TRead,TValues), | |
213 | safe_create_texpr(let_expression_global(TRead,TValues, | |
214 | b(operation_call_in_expr(Operation,OpCallParaValues),any,OldInfos)),any,[generated_by_b_compiler],New), | |
215 | New = b(Compiled,_,NewInfos) | |
216 | %NewInfos = [generated_by_b_compiler], | |
217 | %Compiled = let_expression_global(TRead,TValues, | |
218 | % b(operation_call_in_expr(Operation,OpCallParaValues),any,OldInfos)) | |
219 | ). | |
220 | b_compile1_infos(kodkod(Id,Identifiers),_,OldInfos,Parameters,LS,S,NExpr,NewInfos,_Eval,FullyKnown,WF) :- !, | |
221 | FullyKnown=false, NewInfos=OldInfos, | |
222 | exclude(is_parameter(Parameters),Identifiers,IdsToCompile), | |
223 | (IdsToCompile=[] | |
224 | -> NExpr = kodkod(Id,Identifiers) | |
225 | ; maplist(precompile_id(LS,S,WF),IdsToCompile,Values), | |
226 | % as we cannot inspect kodkod problem: wrap it into a let with the values stored: | |
227 | NExpr = let_predicate(IdsToCompile,Values,b(kodkod(Id,Identifiers),pred,OldInfos)) | |
228 | ). | |
229 | b_compile1_infos(Expr,_,OldInfos,Parameters,LS,S,NewUntypedExpr,NewInfos,Eval,FullyKnown,WF) :- | |
230 | b_compile2(Expr,Parameters,LS,S,NewUntypedExpr,Eval,FullyKnown,WF), | |
231 | update_infos(NewUntypedExpr,OldInfos,Parameters,NewInfos). | |
232 | ||
233 | ||
234 | is_parameter(Parameters,b(identifier(Id),_,_)) :- ord_member(Id,Parameters). | |
235 | ||
236 | precompile_id(LS,S,WF,b(identifier(Id),Type,Info),b(value(Value),Type,[])) :- | |
237 | b_interpreter:lookup_value_in_store_and_global_sets_wf(Id,Type,LS,S,Value,Info,WF). | |
238 | % was_identifier is aded in b_compile1_infos | |
239 | ||
240 | :- use_module(bmachine,[b_get_operation_normalized_read_write_info/3]). | |
241 | ||
242 | %operation_identifier(op(_)). | |
243 | create_value_for_read_variable(LS,S,WF,Variable,TVariable,TValue) :- | |
244 | b_interpreter:lookup_value_in_store_and_global_sets_wf(Variable,_Type,LS,S,Value,unknown,WF),!, | |
245 | % TO DO: try and find type? | |
246 | TVariable = b(identifier(Variable),any,[]), | |
247 | TValue = b(value(Value),any,[]). | |
248 | create_value_for_read_variable(_LS,_S,WF,Variable,TVariable,b(value(term(undefined)),any,[])) :- | |
249 | TVariable = b(identifier(Variable),any,[]), | |
250 | add_internal_error_wf(b_compiler,'Cannot find variable (read) while compiling operation:',Variable,unknown,WF), | |
251 | fail. | |
252 | ||
253 | :- use_module(library(ordsets)). | |
254 | update_infos(forall(EParas,LHS,RHS),Infos,Parameters,NewInfos) :- | |
255 | % forall also has used_ids field as it may call exists in negative context | |
256 | conjunct_predicates([LHS,RHS],Cond), | |
257 | update_infos_aux(EParas,Cond,Infos,Parameters,NewInfos),!. | |
258 | update_infos(exists(EParas,Cond),Infos,Parameters,NewInfos) :- % we create_exists_or_let_predicate above, but other transformations may generate an exists below: | |
259 | update_infos_aux(EParas,Cond,Infos,Parameters,NewInfos),!. | |
260 | update_infos(BOP,Infos,_,NewInfos) :- bsyntaxtree:syntaxelement(BOP, [A,B],[], [], [], _), | |
261 | wd_and_efficient(BOP), % should not generate WD errors itself | |
262 | (select(contains_wd_condition,Infos,NewInfos) % there is a WD condition attached | |
263 | -> fast_check_wd(A), | |
264 | fast_check_wd(B) | |
265 | ), | |
266 | %print(removing_wd_condition(BOP)),nl, | |
267 | !. | |
268 | update_infos(_,I,_,I). | |
269 | ||
270 | update_infos_aux(EParas,Cond,Infos,Parameters,NewInfos) :- | |
271 | select_used_ids(UsedIds,Infos,I1,EParas,Cond), | |
272 | UsedIds \= [],!, | |
273 | % remove those used identifiers which will be compiled into the predicate | |
274 | sort(Parameters,SParas), | |
275 | ord_intersection(UsedIds,SParas,NewUsedIds), | |
276 | %print(update(Parameters,UsedIds,I1,new(NewUsedIds))),nl, | |
277 | NewInfos = [used_ids(NewUsedIds)|I1]. | |
278 | ||
279 | :- use_module(bsyntaxtree,[find_identifier_uses/3]). | |
280 | select_used_ids(UsedIds,Infos,I1,_,_) :- select(used_ids(UsedIds),Infos,I1),!. | |
281 | % check_used_ids_info(Parameters,Condition,UsedIds,b_compiler) | |
282 | select_used_ids(UsedIds,Infos,Infos,_Parameters,Condition) :- | |
283 | %add_error(bcompiler,'Expected information of used identifiers in exists operation information : ',Parameters:Infos), %% missing info can happen due to simplifcation rules below ! | |
284 | find_identifier_uses(Condition, [], UsedIds). % ,print(used(UsedIds,in_exist(Parameters))),nl. | |
285 | % TO DO: avoid re-computing used-ids; we should refactor b_compile2 to return new Info field | |
286 | ||
287 | ||
288 | ||
289 | evaluate_this(eval,X,Type,Info) :- !, worth_it_type(Type,X,Info). | |
290 | evaluate_this(_,function(A,B),Type,Info) :- !, | |
291 | A=b(value(avl_set(_)),_,_), | |
292 | B=b(value(_),_,_), | |
293 | worth_it_type(Type,function(A,B),Info). % will check well-definedness | |
294 | evaluate_this(_,X,_Type,_Info) :- wd_and_efficient(X). | |
295 | ||
296 | ||
297 | % things which are very quick to compute | |
298 | wd_and_efficient(sequence_extension(_)) :- !. | |
299 | wd_and_efficient(set_extension(_)) :- !. | |
300 | wd_and_efficient(integer_set(_)) :- !. % will be converted into value(global_set(_)) | |
301 | %% wd_and_efficient(value(_)) :- !. % is already computed | |
302 | % the following will reduce the size of the representation; usually a good thing; | |
303 | % we assume only avl_sets apprear here; inner set comprehensions are never computed into symbolic form by b_compile (see known_value below): | |
304 | %wd_and_efficient(identity(_)) :- !. | |
305 | wd_and_efficient(range(_)) :- !. | |
306 | wd_and_efficient(domain(_)) :- !. | |
307 | wd_and_efficient(domain_restriction(_,_)) :- !. | |
308 | wd_and_efficient(domain_subtraction(_,_)) :- !. | |
309 | wd_and_efficient(range_restriction(_,_)) :- !. | |
310 | wd_and_efficient(range_subtraction(_,_)) :- !. | |
311 | wd_and_efficient(intersection(_,_)) :- !. | |
312 | wd_and_efficient(set_subtraction(_,_)) :- !. | |
313 | wd_and_efficient(image(_,_)) :- !. | |
314 | wd_and_efficient(reverse(_)) :- !. % added for rgen_rgen_Worst_Case_Stopping_distance_NCT_trm13 | |
315 | % reverse has n.log(n) complexity, but is always wd and can be beneficial | |
316 | wd_and_efficient(union(A,B)) :- finite_set(A), finite_set(B), !. % has complexity n | |
317 | % usually the union of two avl_sets will be smaller than keeping them separate, what about intervals? | |
318 | wd_and_efficient(interval(_,_)) :- !. % ditto | |
319 | wd_and_efficient(card(S)) :- !, % added for rgen_rgen_Worst_Case_Stopping_distance_NCT_trm13 | |
320 | (finite_set(S) -> true % is wd for finite set; has currently linear complexity but reduces size of closure | |
321 | ; is_interval(S) -> true). % card is simple to compute | |
322 | wd_and_efficient(min(S)) :- !, % logarithmic for avl_set, see test 1338 | |
323 | finite_non_empty_set(S). | |
324 | wd_and_efficient(max(S)) :- !, % logarithmic for avl_set | |
325 | finite_non_empty_set(S). | |
326 | wd_and_efficient(string_set) :- !. | |
327 | % some other efficient operators: | |
328 | % external_function_call CHOOSE (test 1338) ? | |
329 | % first, last, ... need to ensure we have sequence | |
330 | wd_and_efficient(X) :- worth_it_int(X),!. | |
331 | wd_and_efficient(X) :- worth_it_other(X). | |
332 | ||
333 | is_interval(b(value(V),set(_),_)) :- nonvar(V), V=closure(P,T,B), | |
334 | is_fixed_interval(P,T,B,_,_). | |
335 | ||
336 | finite_set(b(value(V),set(_),_)) :- nonvar(V), finite_set_aux(V). | |
337 | finite_set_aux([]). | |
338 | finite_set_aux(avl_set(_)). | |
339 | finite_non_empty_set(b(value(V),set(_),_)) :- nonvar(V), V=avl_set(_). | |
340 | ||
341 | fast_check_wd(b(E,_,Infos)) :- | |
342 | (nonmember(contains_wd_condition,Infos) -> true | |
343 | ; nonvar(E), E=value(_)). | |
344 | ||
345 | check_wd(NTExpr) :- bsyntaxtree:always_well_defined(NTExpr). % ,print(wd(NTExpr)),nl. | |
346 | %(bsyntaxtree:always_well_defined(NTExpr) -> true ; print(not_guaranteed_wd(NTExpr)),nl). | |
347 | ||
348 | % (worth_it_type(Type,X,Info) -> true ; X=value(_) -> true ; print(not_evaluating(X)),nl,fail). | |
349 | worth_it_type(integer,X,Info) :- worth_it_int_wd(X),!, check_wd(b(X,integer,Info)). | |
350 | worth_it_type(T,function(A,B),Info) :- !, | |
351 | (check_wd(b(function(A,B),T,Info)) -> true | |
352 | ; fail). %print('not_precompiling_function '),translate:print_bexpr(A), print(' @ '), translate:print_bexpr(B),nl,fail). | |
353 | worth_it_type(integer,X,_) :- worth_it_int(X),!. | |
354 | worth_it_type(T,X,Info) :- worth_it_wd(X),!, check_wd(b(X,T,Info)). | |
355 | worth_it_type(set(_),X,_) :- worth_it_set(X),!. | |
356 | worth_it_type(seq(_),X,_) :- worth_it_set(X),!. | |
357 | worth_it_type(_,X,_) :- worth_it_other(X). | |
358 | ||
359 | % TO DO: we should use the predicate has_wd_condition from b_ast_cleanup | |
360 | ||
361 | % integer operations that could generate WD-errors | |
362 | worth_it_int_wd(div(_,_)). | |
363 | worth_it_int_wd(max(_)). | |
364 | worth_it_int_wd(min(_)). | |
365 | worth_it_int_wd(mod(_,_)). | |
366 | worth_it_int_wd(power_of(_,_)). | |
367 | worth_it_int_wd(card(_)). % has WD condition !! | |
368 | worth_it_int_wd(size(_)). | |
369 | ||
370 | % other operations that could generate WD-errors | |
371 | worth_it_wd(first(_)). | |
372 | worth_it_wd(last(_)). | |
373 | worth_it_wd(tail(_)). | |
374 | worth_it_wd(front(_)). | |
375 | worth_it_wd(restrict_front(_,_)). | |
376 | worth_it_wd(restrict_tail(_,_)). | |
377 | worth_it_wd(rel_iterate(_,_)). %% could be expensive | |
378 | worth_it_wd(general_intersection(_)). | |
379 | worth_it_wd(general_concat(_)). | |
380 | ||
381 | % to do: check other operators that could be not well-defined ! | |
382 | ||
383 | worth_it_int(unary_minus(_)). | |
384 | worth_it_int(add(_,_)). | |
385 | worth_it_int(minus(_,_)). | |
386 | worth_it_int(multiplication(_,_)). | |
387 | worth_it_int(max_int). | |
388 | worth_it_int(min_int). | |
389 | ||
390 | %worth_it_set(empty_set). % treated below | |
391 | %worth_it_set(empty_sequence). % treated below | |
392 | %worth_it_set(closure(_)). % this is closure1; it is currently always kept symbolic and can be counterproductive to compile; e.g., card(closure1(%x.(x : 1 .. 200|x + 1))) | |
393 | %% ?? need to be more careful here; can be expensive --> need to keep track which parts need definitely to be evaluated | |
394 | worth_it_set(integer_set(_)). % will be converted into value(global_set(_)) | |
395 | worth_it_set(comprehension_set(A,B)) :- b_ast_cleanup:is_integer_set(comprehension_set(A,B),_). | |
396 | worth_it_set(interval(_,_)). | |
397 | worth_it_set(reflexive_closure(A)) :- \+ symbolic_value(A). | |
398 | worth_it_set(reverse(_)). % function inverse | |
399 | worth_it_set(domain(_)). worth_it_set(range(_)). | |
400 | worth_it_set(union(_,_)). worth_it_set(intersection(_,_)). worth_it_set(set_subtraction(_,_)). | |
401 | worth_it_set(image(_,B)) :- \+ symbolic_value(B). | |
402 | worth_it_set(composition(_,_)). | |
403 | worth_it_set(domain_restriction(_,_)). worth_it_set(domain_subtraction(_,_)). | |
404 | worth_it_set(range_restriction(_,_)). worth_it_set(range_subtraction(_,_)). | |
405 | worth_it_set(direct_product(A,B)) :- \+ symbolic_value(A), \+ symbolic_value(B). | |
406 | worth_it_set(parallel_product(A,B)) :- \+ symbolic_value(A), \+ symbolic_value(B). | |
407 | worth_it_set(iteration(_,_)). | |
408 | worth_it_set(set_extension([H|_])) :- \+ symbolic_value(H). % otherwise we may get an enumeration warning | |
409 | worth_it_set(sequence_extension([H|_])) :- \+ symbolic_value(H). % ditto, TODO: check tail unless expensive | |
410 | worth_it_set(rev(_)). % reverse of sequence | |
411 | worth_it_set(concat(_,_)). | |
412 | worth_it_set(seq(_)). % will be kept symbolic anyway | |
413 | worth_it_set(seq1(_)). % will be kept symbolic anyway; relevant for test 1731 | |
414 | % f=%x.(x:iseq(struct(a:seq1(NATURAL),b:BOOL))|x) & f([rec(a:[222],b:TRUE)])=[rec(a:[222],b:xx)] & xx=TRUE | |
415 | % however: value can be put into a set-extension! | |
416 | worth_it_set(iseq(_)). % will be kept symbolic anyway | |
417 | worth_it_set(iseq1(_)). % will be kept symbolic anyway | |
418 | worth_it_set(perm(_)). % will be kept symbolic anyway | |
419 | worth_it_set(pow_subset(_)). % will be kept symbolic anyway | |
420 | worth_it_set(pow1_subset(_)). % will be kept symbolic anyway | |
421 | worth_it_set(fin_subset(_)). % will be kept symbolic anyway | |
422 | worth_it_set(fin1_subset(_)). % will be kept symbolic anyway | |
423 | worth_it_set(general_union(X)) :- \+ symbolic_value(X). % otherwise we can get enumeration warnings | |
424 | worth_it_set(identity(_)). | |
425 | worth_it_set(first_of_pair(_)). % can also produce set | |
426 | worth_it_set(second_of_pair(_)). % can also produce set | |
427 | worth_it_set(cartesian_product(_,_)). % will usually be kept symbolic | |
428 | worth_it_set(string_set). % ensure we have values inside compiled closures, e.g., for custom_explicit_set card computations | |
429 | worth_it_set(bool_set). | |
430 | ||
431 | symbolic_value(b(value(Val),_,_)) :- nonvar(Val), symbolic_val_aux(Val). | |
432 | symbolic_val_aux(closure(P,T,B)) :- \+ is_fixed_interval(P,T,B,_,_). | |
433 | symbolic_val_aux(global_set(_)). | |
434 | ||
435 | :- use_module(external_functions,[not_declarative/1,external_fun_has_wd_condition/1]). | |
436 | worth_it_other(boolean_true). | |
437 | worth_it_other(boolean_false). | |
438 | worth_it_other(string(_)). | |
439 | worth_it_other(first_of_pair(_)). | |
440 | worth_it_other(second_of_pair(_)). | |
441 | worth_it_other(couple(_,_)). | |
442 | worth_it_other(record_field(_,_)). | |
443 | worth_it_other(external_function_call(FunName,_)) :- | |
444 | \+ not_declarative(FunName), | |
445 | \+ external_fun_has_wd_condition(FunName). %print(compile(FunName)),nl. | |
446 | % CHOOSE for finite_non_empty_set ? | |
447 | worth_it_other(rec(_)). | |
448 | worth_it_other(struct(_)). | |
449 | %worth_it_other(value(_)). % does not have to be evaluted; already a value | |
450 | ||
451 | /* | |
452 | % To do: distinguish which parts definitely need to be evaluated | |
453 | %dont_eval_subexpressions(member). % special membership code can be used | |
454 | %dont_eval_subexpressions(not_member). % special membership code can be used | |
455 | dont_eval_subexpressions(disjunct(_,_)). % it may not be necessary to eval RHS | |
456 | dont_eval_subexpressions(implication(_,_)). % it may not be necessary to eval RHS | |
457 | */ | |
458 | ||
459 | :- use_module(bsyntaxtree, [get_negated_operator_expr/2]). | |
460 | :- use_module(kernel_objects,[equal_object/3]). | |
461 | :- use_module(kernel_mappings,[binary_boolean_operator/3]). | |
462 | :- use_module(kernel_tools,[filter_cannot_match/4, get_template_for_filter_cannot_match/2]). | |
463 | b_compile2(Exp,_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,WF) :- var(Exp), !, | |
464 | add_internal_error_wf(b_compiler,'Variable Expression: ',Exp,unknown,WF), | |
465 | NExpr=Exp, FullyKnown=false. | |
466 | b_compile2(truth,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=truth, FullyKnown=false. % predicates never fully known | |
467 | b_compile2(falsity,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=falsity, FullyKnown=false. % predicates never fully known | |
468 | b_compile2(empty_set,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value([]), FullyKnown=true. | |
469 | b_compile2(empty_sequence,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value([]), FullyKnown=true. | |
470 | b_compile2(boolean_false,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value(pred_false), FullyKnown=true. | |
471 | b_compile2(boolean_true,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value(pred_true), FullyKnown=true. | |
472 | b_compile2(value(Val),_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, | |
473 | NExpr=value(Val), | |
474 | (known_value(Val) -> % ground(Val) -> known_value ? | |
475 | FullyKnown=true ; FullyKnown=false). | |
476 | b_compile2(integer(Val),_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, | |
477 | NExpr=value(int(Val)), (number(Val) -> FullyKnown=true ; FullyKnown=false). | |
478 | b_compile2(lazy_lookup_pred(Id),Parameters,LS,S,NExpr,_Eval,FullyKnown,WF) :- !, | |
479 | ( ord_member(Id,Parameters) -> %print(lazy_lookup_pred_id_as_parameter(Id,Parameters)),nl, | |
480 | NExpr = lazy_lookup_pred(Id), FullyKnown=false | |
481 | ; compute_lazy_lookup(Id,lazy_lookup_pred(Id),LS,S,NExpr,FullyKnown,WF) | |
482 | ). | |
483 | b_compile2(lazy_lookup_expr(Id),Parameters,LS,S,NExpr,_Eval,FullyKnown,WF) :- !, | |
484 | ( ord_member(Id,Parameters) -> %print(lazy_lookup_expr_id_as_parameter(Id,Parameters)),nl, | |
485 | NExpr = lazy_lookup_expr(Id), FullyKnown=false | |
486 | ; compute_lazy_lookup(Id,lazy_lookup_expr(Id),LS,S,NExpr,FullyKnown,WF) | |
487 | ). | |
488 | ||
489 | % treat a few common cases, more efficiently than syntaxtransformation | |
490 | b_compile2(equal(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
491 | FullyKnown=false, % predicates never evaluated in b_compile1 | |
492 | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF), | |
493 | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF), | |
494 | ( FullyKnownA=true, FullyKnownB=true, | |
495 | NExprA = b(value(VA),_,_), NExprB = b(value(VB),_,_) | |
496 | -> (equal_object(VA,VB,b_compile2_1) -> NExpr = truth ; NExpr = falsity) | |
497 | ; generate_equality(NExprA,NExprB,NExpr) | |
498 | ). | |
499 | b_compile2(not_equal(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
500 | FullyKnown=false, % predicates never evaluated in b_compile1 | |
501 | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF), | |
502 | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF), | |
503 | ( FullyKnownA=true, FullyKnownB=true, | |
504 | NExprA = b(value(VA),_,_), NExprB = b(value(VB),_,_) | |
505 | -> %print(computing_neq(VA,VB)),nl, | |
506 | (kernel_objects:equal_object(VA,VB,b_compile2_2) -> NExpr = falsity ; NExpr = truth) | |
507 | %, print(result(NExpr)),nl | |
508 | ; NExpr = not_equal(NExprA,NExprB) | |
509 | ). | |
510 | b_compile2(member(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
511 | FullyKnown=false, % predicates never evaluated in b_compile1 | |
512 | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF), | |
513 | (NExprB = b(value(X),BT,BI) | |
514 | -> (X==[], always_well_defined(A) -> NExpr = falsity | |
515 | ; b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF), | |
516 | % check if we can decide membership (e.g., 1:{1}) | |
517 | (quick_test_membership1(NExprA,X,PRes) | |
518 | -> convert_pred_res(PRes,NExpr) | |
519 | % TO DO: maybe optimize x: {y|P(y)} --> P(x) ; by commenting in code below | |
520 | % However, ensure test 273 succeeds and closure equality correctly detected (e.g., for BV16 = {bt|bt : BIT_VECTOR & bv_size(bt) = 16}) | |
521 | % ; (get_texpr_id(NExprA,IDA), | |
522 | % get_comprehension_set(NExprB,IDB,Pred), get_texpr_info(NExprB,Info), | |
523 | % print(rename(IDB,IDA,Info)),nl, | |
524 | % bsyntaxtree:rename_bt(Pred,[rename(IDB,IDA)],PredA)) -> get_texpr_expr(PredA,NExpr) | |
525 | ; custom_explicit_sets:singleton_set(X,El) % replace x:{El} -> x=El | |
526 | -> get_texpr_type(NExprA,TA), | |
527 | generate_equality_with_value(NExprA,FullyKnownA,El,FullyKnownB,TA,NExpr) | |
528 | ; get_template_for_filter_cannot_match(NExprA,VA) | |
529 | -> filter_cannot_match(X,VA,NewX,Filtered), | |
530 | % (Filtered=false -> true ; print(filtered(NewX,VA,X)),nl), | |
531 | (Filtered=false -> NExpr = member(NExprA,NExprB) | |
532 | ; (NewX==[], always_well_defined(A)) -> NExpr = falsity | |
533 | ; custom_explicit_sets:singleton_set(NewX,El) | |
534 | -> get_texpr_type(NExprA,TA), | |
535 | %nl,print(create_equal(NExprA,FullyKnownA,El,FullyKnownB,NExprB)),nl,nl, | |
536 | generate_equality_with_value(NExprA,FullyKnownA,El,FullyKnownB,TA,NExpr) | |
537 | ; NExpr = member(NExprA, b(value(NewX),BT,BI)) | |
538 | ) | |
539 | % end fo filtering | |
540 | ; NExpr = member(NExprA,NExprB) | |
541 | ) | |
542 | % , print('compile: '),print(NExpr),nl | |
543 | ) | |
544 | ; NExpr = member(NExprA,NExprB), | |
545 | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF) | |
546 | ). | |
547 | % TO DO: also optimize things like: (ev1 |-> 0) |-> eg : #221:{((1|->0)|->3),((2|->0)|->0),...,((233|->0)|->218),((234|->0)|->228)} | |
548 | ||
549 | b_compile2(not_member(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
550 | FullyKnown=false, % predicates never evaluated in b_compile1 | |
551 | b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF), | |
552 | (NExprB = b(value(X),_,_) | |
553 | -> (X==[], always_well_defined(A) -> NExpr = truth | |
554 | ; b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF), | |
555 | (quick_test_membership1(NExprA,X,PRes) | |
556 | -> convert_neg_pred_res(PRes,NExpr) | |
557 | ; NExpr = not_member(NExprA,NExprB)) | |
558 | ) | |
559 | ; NExpr = not_member(NExprA,NExprB), | |
560 | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF) | |
561 | ). | |
562 | b_compile2(function(Fun,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
563 | (is_lazy_extension_function_for_fun_app(Fun) | |
564 | -> Eval1=false % extension function applications treated lazily | |
565 | % TO DO: first evaluate B, if known then only evaluate relevant part of extension function | |
566 | ; Eval1=Eval), | |
567 | b_compile1(Fun,Parameters,LS,S,NExprA,Eval1,FullyKnown1,WF), | |
568 | combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown12), | |
569 | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF), | |
570 | %tools_printing:print_term_summary(compiled_function(FullyKnown1,FullyKnown2,NExprA,NExprB)),nl, | |
571 | (FullyKnown2=true, preferences:preference(find_abort_values,false), | |
572 | % check if we have enough information to apply a partially specified function as a list | |
573 | % e.g. if the function is [(int(1),A),(int(2),B)] and the argument is int(2): we can apply the function without knowing A or B; can have a dramatic importance when expanding unversal quantifiers ! | |
574 | can_apply_partially_specified_function(NExprA,NExprB,ResultExpr,WF) | |
575 | -> NExpr = ResultExpr, | |
576 | (FullyKnown12=true -> FullyKnown=true | |
577 | ; ResultExpr=value(ResultValue),known_value(ResultValue) -> FullyKnown=true | |
578 | ; FullyKnown = false) | |
579 | ; %tools_printing:print_term_summary(cannot_apply_function(FullyKnown2,NExprA,NExprB)),nl, | |
580 | %translate:print_bexpr(NExprA),nl, translate:print_bexpr(NExprB),nl, | |
581 | NExpr = function(NExprA,NExprB), FullyKnown = FullyKnown12). | |
582 | ||
583 | b_compile2(conjunct(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
584 | FullyKnown=false, % predicates never automatically evaluated in b_compile1 | |
585 | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF), | |
586 | (is_falsity(NExprA) -> NExpr = falsity | |
587 | ; | |
588 | % TO DO: propagate static information from A to B, e.g. if A :: x=10 -> add x=10 to LS/Parameters | |
589 | % also: try and detect unsatisfiable predicates beforehand | |
590 | b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF), | |
591 | (is_falsity(NExprB) -> NExpr = falsity | |
592 | ; is_truth(NExprB) -> get_texpr_expr(NExprA,NExpr) | |
593 | ; is_truth(NExprA) -> get_texpr_expr(NExprB,NExpr) | |
594 | ; NExpr = conjunct(NExprA,NExprB)) | |
595 | ). | |
596 | b_compile2(disjunct(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
597 | FullyKnown=false, % predicates never automatically evaluated in b_compile1 | |
598 | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF), | |
599 | (is_truth(NExprA) -> NExpr = truth | |
600 | ; b_compile1(B,Parameters,LS,S,NExprB,false,_,WF), % does not have to be executed in a successful branch: set Eval to false to avoid computing expensive expressions which may not be needed | |
601 | (is_truth(NExprB) -> NExpr = truth | |
602 | ; is_falsity(NExprA) -> get_texpr_expr(NExprB,NExpr) | |
603 | ; is_falsity(NExprB) -> get_texpr_expr(NExprA,NExpr) | |
604 | ; NExpr = disjunct(NExprA,NExprB)) | |
605 | ). | |
606 | b_compile2(implication(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
607 | FullyKnown=false, % predicates never automatically evaluated in b_compile1 | |
608 | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF), | |
609 | (is_falsity(NExprA) -> NExpr = truth | |
610 | ; is_truth(NExprA) -> b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF), get_texpr_expr(NExprB,NExpr) | |
611 | ; NExpr = implication(NExprA,NExprB), | |
612 | b_compile1(B,Parameters,LS,S,NExprB,false,_,WF) % B does not have to be executed in a successful branch: set Eval to false to avoid computing expensive expressions which may not be needed | |
613 | % TO DO: add preference to force pre-computation everywhere and pass Eval instead of false to b_compile1; ditto for disjunction | |
614 | ). | |
615 | b_compile2(negation(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
616 | FullyKnown=false, % predicates never automatically evaluated in b_compile1 | |
617 | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF), | |
618 | ( get_negated_operator_expr(NExprA,NegatedA) -> NExpr = NegatedA | |
619 | ; NExpr = negation(NExprA) | |
620 | ). | |
621 | b_compile2(if_then_else(A,B,C),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
622 | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF), | |
623 | (is_falsity(NExprA) -> b_compile1(C,Parameters,LS,S,NExprC,Eval,FullyKnown,WF), get_texpr_expr(NExprC,NExpr) | |
624 | ; is_truth(NExprA) -> b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown,WF), get_texpr_expr(NExprB,NExpr) | |
625 | ; NExpr = if_then_else(NExprA,NExprB,NExprC), FullyKnown=false, | |
626 | b_compile1(B,Parameters,LS,S,NExprB,false,_,WF), % set Eval to false as we do not know if B will be needed | |
627 | b_compile1(C,Parameters,LS,S,NExprC,false,_,WF) % ditto for C | |
628 | ). | |
629 | /* b_compile2(comprehension_set(CParas,Body),Parameters,LS,S,NExpr,_Eval,FullyKnown,WF) :- | |
630 | sort(Parameters,SParas), | |
631 | b_ast_cleanup:not_occurs_in_predicate(SParas,Body), %can only be applied if Body does not reference Parameters | |
632 | !, | |
633 | b_generate_inner_closure_if_necessary(Parameters,CParas,Body,LS,S,Result), % will itself call b_compile | |
634 | NExpr = value(Result), | |
635 | (ground(Result) -> FullyKnown=true ; FullyKnown=false). */ | |
636 | b_compile2(forall(ForallPara,A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
637 | FullyKnown=false, % predicates never automatically evaluated in b_compile1 | |
638 | get_texpr_ids(ForallPara,AtomicIds), | |
639 | add_parameters(Parameters,AtomicIds,NParameters), | |
640 | b_compile1(A,NParameters,LS,S,NA,Eval,_FullyKnownA,WF), | |
641 | (is_falsity(NA) -> NExpr = truth | |
642 | ; b_compile1(B,NParameters,LS,S,NB,Eval,_FullyKnownB,WF), | |
643 | (is_truth(NB) -> NExpr = truth | |
644 | ; NExpr = forall(ForallPara,NA,NB) | |
645 | % TO DO ??: if we have an equality -> replace Body by value and remove quantifier | |
646 | %,print('COMPIlED: '),translate:print_bexpr(b(NExpr,pred,[])),nl | |
647 | ) | |
648 | ). | |
649 | % some special cases to avoid calling syntaxtransformation | |
650 | b_compile2(record_field(A,FieldName),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
651 | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF), | |
652 | % First: we can try compute even if value not fully known !, we just need record field list | |
653 | (get_record_field(NExprA,FieldName,NExpr,FullyKnown) -> true | |
654 | ; NExpr = record_field(NExprA,FieldName), FullyKnown=FullyKnownA). | |
655 | b_compile2(couple(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
656 | %NExpr = couple(NExprA,NExprB), | |
657 | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF), | |
658 | combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown), | |
659 | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF), | |
660 | (FullyKnown \== true, % evaluation will already combine the result | |
661 | NExprA=b(value(VA),_,_),NExprB=b(value(VB),_,_) | |
662 | -> NExpr = value((VA,VB)) | |
663 | ; NExpr = couple(NExprA,NExprB)). | |
664 | b_compile2(image(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
665 | %NExpr = image(NExprA,NExprB), | |
666 | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF), | |
667 | combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown), | |
668 | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF), | |
669 | (FullyKnown \= true, NExprA=b(value(VA),BT,BI), | |
670 | NExprB=b(value(VB),_,_), nonvar(VB), | |
671 | custom_explicit_sets:singleton_set(VB,VBX) | |
672 | -> filter_cannot_match(VA,(VBX,_),NewVA,_Filtered), %nl,print(filtered_image(VBX,VA,NewVA)),nl, | |
673 | NExpr = image(b(value(NewVA),BT,BI),NExprB) | |
674 | % TO DO: add case where VB==[] or VA==[] are the empty set | |
675 | ; NExpr = image(NExprA,NExprB) | |
676 | ). %, print('compile image: '),translate:print_bexpr(NExpr),nl. | |
677 | % TO DO: do something like can_apply_partially_specified_function; or filter_can_match | |
678 | b_compile2(assertion_expression(A,Msg,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
679 | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF), | |
680 | (is_truth(NExprA) -> % the ASSERT EXPR is redundant | |
681 | %print(removed_assert),nl, translate:print_bexpr(B),nl, | |
682 | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown,WF), | |
683 | get_texpr_expr(NExprB,NExpr) | |
684 | ; b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF), | |
685 | FullyKnown=false, % we cannot get rid of WD condition | |
686 | NExpr = assertion_expression(NExprA,Msg,NExprB) | |
687 | ). | |
688 | b_compile2(domain(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
689 | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF), | |
690 | (FullyKnown1=false,get_texpr_expr(NExprA,NA),evaluate_domain(NA,Domain) % try and compute domain even if not fully known | |
691 | -> FullyKnown = true, NExpr = value(Domain) | |
692 | ; FullyKnown = FullyKnown1, NExpr = domain(NExprA)). | |
693 | b_compile2(range(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
694 | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF), | |
695 | (FullyKnown1=false,evaluate_range(NExprA,Range) % try and compute range even if not fully known | |
696 | -> FullyKnown = true, NExpr = value(Range) | |
697 | ; FullyKnown = FullyKnown1, NExpr = range(NExprA)). | |
698 | b_compile2(assign(LHS_List,RHS_List),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, | |
699 | NExpr = assign(New_LHS_List,NewRHS_List), FullyKnown = false, | |
700 | maplist(b_compile_lhs(Parameters,LS,S,Eval,WF),LHS_List,New_LHS_List), | |
701 | b_compile_l(RHS_List,Parameters,LS,S,NewRHS_List,Eval,_FullyKnown2,WF). | |
702 | b_compile2(assign_single_id(ID,B),Parameters,LS,S,assign_single_id(ID,NExprB),Eval,FullyKnown,WF) :- !, | |
703 | FullyKnown = false, | |
704 | b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF). | |
705 | b_compile2(operation_call(Operation,OpCallResults,OpCallParas),Parameters,LS,S,InlinedOpCall,Eval,FullyKnown,WF) :- | |
706 | % TO DO: evaluate if we should also use the let_expression_global approach used for operation_call_in_expr | |
707 | !, | |
708 | def_get_texpr_id(Operation,op(OperationName)), | |
709 | FullyKnown = false, | |
710 | b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF), | |
711 | TopLevel=false, | |
712 | b_get_machine_operation_for_animation(OperationName,OpResults,OpFormalParameters,Body,_OType,TopLevel), | |
713 | bsyntaxtree:replace_ids_by_exprs(Body,OpResults,OpCallResults,Body2), | |
714 | get_texpr_ids(OpFormalParameters,OpIds), | |
715 | add_parameters(Parameters,OpIds,InnerParas), | |
716 | b_compile1(Body2,InnerParas,[],S,NBody,Eval,FullyKnown,WF), % do not pass local state: this may override constants,... from the called machine | |
717 | % Note: global state S should be valid for all machines in currently loaded specification | |
718 | get_texpr_ids(OpCallResults,OpRIds), | |
719 | add_parameters(Parameters,OpRIds,LocalKnownParas), | |
720 | simplify_assignment(OpFormalParameters,OpCallParaValues,LHSFormalParas,RHSCallVals), %% | |
721 | split_formal_parameters(LHSFormalParas,RHSCallVals,LocalKnownParas, | |
722 | FreshOpParas,FreshCallVals, | |
723 | ClashOpParas, ClashCallVals), % only set up VAR for fresh Paras | |
724 | % print(split(LHSFormalParas,LocalKnownParas,fresh(FreshOpParas),clash(ClashOpParas))),nl, | |
725 | (FreshOpParas=[] -> get_texpr_expr(NBody,Let1) | |
726 | ; create_equality_for_let(FreshOpParas,FreshCallVals,Equality1), | |
727 | Let1 = let(FreshOpParas,Equality1,NBody)), | |
728 | (ClashOpParas = [] | |
729 | -> InlinedOpCall = Let1 | |
730 | ; %nl,print(clash(ClashOpParas)),nl, | |
731 | maplist(create_fresh_id,ClashOpParas,FreshCopy), | |
732 | create_equality_for_let(ClashOpParas,FreshCopy,Equality2), % copy Values from Fresh Ids | |
733 | create_equality_for_let(FreshCopy,ClashCallVals,Equality3), % assign Parameter Vals to Fresh Ids | |
734 | get_texpr_pos(Body,BodyPos), BodyPosInfo = [nodeid(BodyPos)], | |
735 | Let2 = let(ClashOpParas,Equality2,b(Let1,subst,[BodyPosInfo])), | |
736 | InlinedOpCall = let(FreshCopy,Equality3,b(Let2,subst,[BodyPosInfo])) | |
737 | ). | |
738 | %, print('Compiled operation call: '), translate:print_subst(b(InlinedOpCall,subst,BodyPosInfo)),nl,nl. | |
739 | % Maybe this version is faster when no OpCallResults: | |
740 | %b_compile2(operation_call(Operation,OpCallResults,OpCallParas),Parameters,LS,S,InlinedOpCall,Eval,FullyKnown,WF) :- | |
741 | % OpCallResults=[], | |
742 | % !, | |
743 | % def_get_texpr_id(Operation,op(OperationName)), | |
744 | % FullyKnown = false, | |
745 | %% b_compile_l(Results,Parameters,LS,S,NResults,Eval,_,WF), | |
746 | % b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF), | |
747 | % TopLevel=false, | |
748 | % b_get_machine_operation_for_animation(OperationName,OpResults,OpParameters,Body,_OType,TopLevel), | |
749 | % % Note: input parameters cannot be assigned to: so replace ids is ok | |
750 | % % However, we cannot replace output parameters: these can be assigned to and we can have aliasing | |
751 | % % Note: no aliasing is allowed in OpCallResults (cf Atelier-B handbook x,x <-- op not allowed) | |
752 | % bsyntaxtree:replace_ids_by_exprs(Body,OpParameters,OpCallParaValues,Body2), | |
753 | % get_texpr_ids(OpResults,OpIds), | |
754 | % append(OpIds,Parameters,InnerParas), | |
755 | % b_compile1(Body2,InnerParas,LS,S,NBody,Eval,FullyKnown,WF), | |
756 | % FinalBody = NBody. | |
757 | b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- | |
758 | functor(Expr,BOP,2), | |
759 | binary_boolean_operator(BOP,_,_),!, % from kernel_mappings, slightly more efficient than syntaxtransformation | |
760 | arg(1,Expr,A), | |
761 | FullyKnown=false, % predicates never evaluated in b_compile1 | |
762 | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF), | |
763 | arg(2,Expr,B), | |
764 | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF), | |
765 | (eval_binary_bool(FullyKnownA,NExprA,FullyKnownB,NExprB,BOP,Result) | |
766 | -> NExpr = Result | |
767 | ; functor(NExpr,BOP,2), arg(1,NExpr,NExprA), arg(2,NExpr,NExprB) | |
768 | ). | |
769 | b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- | |
770 | functor(Expr,BOP,2), | |
771 | kernel_mappings:binary_function(BOP,_,_),!, % slightly more efficient than syntaxtransformation | |
772 | arg(1,Expr,A), | |
773 | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF), | |
774 | combine_fully_known(FullyKnownA,FullyKnownB,FullyKnown), | |
775 | arg(2,Expr,B), | |
776 | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF), | |
777 | functor(NExpr,BOP,2), arg(1,NExpr,NExprA), arg(2,NExpr,NExprB). | |
778 | b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- | |
779 | functor(Expr,UOP,1), | |
780 | kernel_mappings:unary_function(UOP,_,_),!, % slightly more efficient than syntaxtransformation | |
781 | arg(1,Expr,A), | |
782 | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown,WF), | |
783 | functor(NExpr,UOP,1), arg(1,NExpr,NExprA). | |
784 | b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- % GENERAL CASE | |
785 | %hit_profiler:add_profile_hit(Expr), | |
786 | syntaxtransformation(Expr,Subs,Names,NSubs,NExpr), | |
787 | get_texpr_ids(Names,Ids), | |
788 | add_parameters(Parameters,Ids,NParameters), | |
789 | b_compile_l(Subs,NParameters,LS,S,NSubs,Eval,FullyKnown,WF). | |
790 | ||
791 | b_compile_l([],_,_,_,[],_Eval,true,_WF). | |
792 | b_compile_l([Expr|ExprRest],P,LS,S,[NExpr|NExprRest],Eval,FullyKnown,WF) :- | |
793 | b_compile1(Expr,P,LS,S,NExpr,Eval,FullyKnown1,WF), | |
794 | combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown), | |
795 | b_compile_l(ExprRest,P,LS,S,NExprRest,Eval,FullyKnown2,WF). | |
796 | ||
797 | % detecth when a parameter clashes with existing known ids | |
798 | id_clash(LocalKnownParas,TID) :- def_get_texpr_id(TID,ID), member(ID,LocalKnownParas). | |
799 | ||
800 | /* comment in if we want to compile inner comprehension sets: | |
801 | :- use_module(bsyntaxtree,[split_names_and_types/3]). | |
802 | :- use_module(closures,[construct_closure_if_necessary/4]). | |
803 | b_generate_inner_closure_if_necessary(OuterParameters,ClosureParas,Condition,LocalState,State,Result) :- | |
804 | split_names_and_types(ClosureParas,Names,Types), | |
805 | add_parameters(OuterParameters,Names,FullNames), | |
806 | b_compile(Condition,FullNames,LocalState,State,ClosurePred), | |
807 | print('INNER COMPILE: '), translate:print_bexpr(ClosurePred),nl, | |
808 | construct_closure_if_necessary(Names,Types,ClosurePred,Result). | |
809 | */ | |
810 | ||
811 | ||
812 | % the LHS contains l-values which should not be looked up in the environment | |
813 | % however, we need to deal with things like f(i) := RHS and compile i | |
814 | b_compile_lhs(Parameters,LS,S,Eval,WF,TExpr,NewTExpr) :- | |
815 | TExpr = b(Expr,Type,Info), NewTExpr = b(NewExpr,Type,Info), | |
816 | b_compile_lhs_aux(Expr,Parameters,LS,S,NewExpr,Eval,WF). | |
817 | ||
818 | b_compile_lhs_aux(function(A,B),Parameters,LS,S,function(NewA,NewB),Eval,WF) :- !, | |
819 | b_compile_lhs(Parameters,LS,S,Eval,WF,A,NewA), % we can have nexted function calls f(e)(g) := | |
820 | b_compile1(B,Parameters,LS,S,NewB,Eval,_,WF). | |
821 | b_compile_lhs_aux(E,_,_,_,E,_,_WF). % other LHS should be identifier -> just copy | |
822 | ||
823 | get_record_field(b(value(Val),_,_),FieldName,value(Field),FullyKnown) :- !, | |
824 | nonvar(Val), Val=rec(Fields), | |
825 | safe_get_field(Fields,FieldName,Field), | |
826 | known_value(Field,FullyKnown). | |
827 | get_record_field(b(function(FUN,ARG),_Type,_Info),FieldName,function(ReducedFUN,ARG),false) :- | |
828 | % {1|->rec(a:1,b:2),...}(x)'b --> {1|->2,...}(x) | |
829 | %nl,print(get_field(FUN,ARG,FieldName)),nl, | |
830 | % TO DO: also allow nested functions calls {1|->rec(a:1,b:2),...}(x)(y)'b or other reduction operators | |
831 | get_field_in_range(FUN,FieldName,ReducedFUN). | |
832 | safe_get_field(V,FN,_) :- (var(V) ; var(FN)),!,fail. | |
833 | safe_get_field([field(N,V)|T],FieldName,Result) :- nonvar(N), | |
834 | (N=FieldName -> Result=V ; safe_get_field(T,FieldName,Result)). | |
835 | ||
836 | :- use_module(probsrc(custom_explicit_sets),[expand_custom_set_to_list/4, convert_to_avl/2]). | |
837 | :- use_module(probsrc(avl_tools),[avl_height_less_than/2]). | |
838 | get_field_in_range(b(value(OldVal),set(couple(Dom,OldRange)),Info),FieldName, | |
839 | b(value(NewVal),set(couple(Dom,NewRange)),Info)) :- | |
840 | nonvar(OldVal), OldVal=avl_set(AVL), | |
841 | avl_height_less_than(AVL,10), | |
842 | OldRange = record(Fields), | |
843 | member(field(FieldName,NewRange),Fields),!, | |
844 | expand_custom_set_to_list(avl_set(AVL),List,_,get_field_in_range), | |
845 | maplist(safe_get_range_field(FieldName),List,NewList), | |
846 | convert_to_avl(NewList,NewVal). | |
847 | ||
848 | % compute the field access for the range elements: | |
849 | safe_get_range_field(FieldName,(Dom,rec(Fields)),(Dom,Field)) :- safe_get_field(Fields,FieldName,Field). | |
850 | ||
851 | ||
852 | eval_binary_bool(true,b(value(ValA),_,_),true,b(value(ValB),_,_),BOP,Result) :- | |
853 | ground(ValA), | |
854 | ground(ValB), | |
855 | eval_binary_aux(BOP,ValA,ValB,Result). | |
856 | ||
857 | eval_binary_aux(less,int(A),int(B),Result) :- | |
858 | (A < B -> Result = truth ; Result = falsity). | |
859 | eval_binary_aux(greater,int(A),int(B),Result) :- | |
860 | (A > B -> Result = truth ; Result = falsity). | |
861 | eval_binary_aux(less_equal,int(A),int(B),Result) :- | |
862 | (A =< B -> Result = truth ; Result = falsity). | |
863 | eval_binary_aux(greater_equal,int(A),int(B),Result) :- | |
864 | (A >= B -> Result = truth ; Result = falsity). | |
865 | eval_binary_aux(subset,avl_set(A1),avl_set(A2),Result) :- | |
866 | (custom_explicit_sets:check_avl_subset(A1,A2) -> Result = truth ; Result = falsity). | |
867 | eval_binary_aux(subset,[],_,Result) :- Result=truth. | |
868 | %eval_binary_aux(less_real,real(A),real(B),Result) :- % TO DO | |
869 | % (A < B -> Result = truth ; Result = falsity). | |
870 | % TO DO: other operators are not_subset, strict_subset, ... intervals for subset,... | |
871 | ||
872 | ||
873 | ||
874 | :- use_module(store,[lookup_value_for_existing_id_wf/5]). | |
875 | compute_lazy_lookup(Id,Expr,LS,S,NExpr,FullyKnown,WF) :- | |
876 | lookup_value_for_existing_id_wf(Id,LS,S,(Evaluated,Value),WF), | |
877 | % the lazy expression has already been registered, but maybe not yet evaluated | |
878 | !, | |
879 | known_value(Value,FullyKnown), % compute if value fully known | |
880 | (Evaluated==pred_true -> NExpr = value(Value) | |
881 | ; FullyKnown==true -> NExpr = value(Value) | |
882 | ; memberchk(bind('$do_not_force_lazy_lookups',_),LS) -> NExpr = Expr % we do not force lookup: there could be WD issues ! TO DO: examine Infos for wd_condition; we could also return NExpr = lazy_value(Id,Evaluated,Value) | |
883 | ; if(Evaluated = pred_true, | |
884 | % will force evaluation ! Note: this means shared expression inside a compiled expression must be well-defined | |
885 | NExpr = value(Value), | |
886 | (add_internal_error_wf(b_compiler,'Compilation failed: ', Id, unknown,WF), | |
887 | fail)) | |
888 | ). | |
889 | compute_lazy_lookup(Id,_E,_LS,_S,_LazyValue,_,WF) :- | |
890 | add_internal_error_wf(b_compiler,'Compilation failed, illegal lazy_lookup_value: ',Id,unknown,WF), | |
891 | fail. | |
892 | ||
893 | combine_fully_known(true,A,A). | |
894 | combine_fully_known(false,_,false). | |
895 | ||
896 | :- use_module(tools_lists,[length_greater/2]). | |
897 | % is an extension function with at least two elements, but not too long | |
898 | % (for long set extensions it is much better to compile them to avl once; see private_examples/ClearSy/2019_Sep/rule_dummy) | |
899 | % extension functions are treated lazily in b_interpreter for function application under the condition: | |
900 | % memberchk(contains_wd_condition,FInfo) ; preferences:preference(use_clpfd_solver,false) ; ground_value(ArgValue) | |
901 | is_lazy_extension_function_for_fun_app(b(A,_,FInfo)) :- | |
902 | preferences:preference(data_validation_mode,false), | |
903 | (memberchk(contains_wd_condition,FInfo) -> Lim=98 ; Lim = 23), | |
904 | is_extension_function_aux(A,Lim). | |
905 | is_extension_function_aux(set_extension([_A,_|T]),Lim) :- \+ length_greater(T,Lim). | |
906 | is_extension_function_aux(sequence_extension([_,_|T]),Lim) :- \+ length_greater(T,Lim). | |
907 | ||
908 | :- use_module(bsyntaxtree,[is_set_type/2]). | |
909 | % check if we can apply an argument to a partially specified function (as a list and now also as AVL) | |
910 | %can_apply_partially_specified_function(Fun,X,_,_) :- print(fun(Fun)),nl,print(val(X)),nl,fail. | |
911 | can_apply_partially_specified_function(b(Expr,TYPE,_), b(value(X),TA,_),ResultExpr,WF) :- | |
912 | can_apply_aux(Expr,TYPE,X,TA,ResultExpr,WF). | |
913 | ||
914 | can_apply_aux(value(VAL),TYPE,X,TA,value(ResultValue),WF) :- | |
915 | is_set_type(TYPE,couple(TA,_TB)), | |
916 | lookup_result(VAL,X,ResultValue,WF). | |
917 | can_apply_aux(sequence_extension(List),_,X,integer,ResultExpr,_WF) :- | |
918 | % important, e.g., for solving test 1551: {b|[a,b,c](2)=333} =res & a : res & b:res | |
919 | nonvar(X), X=int(Index), number(Index), | |
920 | % this will prevent computing rest of sequence extension: can hide WD issues ! | |
921 | % print(apply_seq_extension(Index,List)),nl, | |
922 | nth1(Index,List,b(ResultExpr,_,_)). | |
923 | ||
924 | :- use_module(kernel_equality,[equality_objects_wf/4, equality_can_be_decided_by_unification/1]). | |
925 | %lookup_result(VAR,ArgValue,Result,WF) :- var(VAR),!,kernel_mappings:kernel_call_apply_to(VAR,ArgValue,Result,unknown,unknown,WF). | |
926 | % the clause above is unsound; as apply_to CAN RAISE WD ERRORS !! what if we have IF 1:dom(f) THEN f(1) ELSE f(0) END; we do not want to compute f(1) ! it can also instantiate unbound variables ! | |
927 | % the idea was to avoid that we wait on the full function, before compiled closure can be evaluated; test 1552 | |
928 | % important for e.g. a = {(1, {([]|->2)} ), (2, const(1, [a(1)]))} | |
929 | % or: a = {1 |-> {[] |-> 2}, 2 |-> (dom({pi,ff,p|((pi : seq(INTEGER) & ff : INTEGER) & p : seq(INTEGER)) & (p |-> ff : [a(1)](1) & pi = 1 -> p)}) \/ {[] |-> 1})} | |
930 | % test 1552 is currently skipped | |
931 | % TO DO: think whether there are other deterministic computations that can be done in b_compile: prj1,prj2, record-field access ? this would ensure that closures,... can be computed earlier | |
932 | lookup_result(VAR,_,_,_WF) :- var(VAR),!,fail. | |
933 | lookup_result(avl_set(A),X,Result,_WF) :- | |
934 | (custom_explicit_sets:try_apply_to_avl_set(X,Result,A) | |
935 | -> true % precompiled function application | |
936 | ; debug_format(19,'Function application in b_compiler for avl_set is not well-defined for: ~w~n',[X]), | |
937 | % We could transform the function application into a construct that raises a WD error | |
938 | fail). | |
939 | lookup_result(closure(_P,_T,_B),_X,_Result,_WF) :- !, | |
940 | fail. % TODO: should we replace parameters by values in body? if domain is full type? | |
941 | lookup_result(List,X,Result,WF) :- List = [_|_],equality_can_be_decided_by_unification(X),!, | |
942 | % this is relevant for long lists, | |
943 | % see public_examples/B/ExternalFunctions/Satsolver/QueensBoardVersionTF_Satsolver.mch | |
944 | fast_lookup_result(List,X,Result,WF). | |
945 | lookup_result(List,X,Result,WF) :- | |
946 | regular_lookup_result_in_list(List,X,Result,WF). | |
947 | ||
948 | regular_lookup_result_in_list([],X,_Result,_WF) :- | |
949 | debug_format(19,'Function application in b_compiler for list is not well-defined for: ~w~n',[X]), % ditto | |
950 | fail. | |
951 | regular_lookup_result_in_list([(HFrom,HTo)|T],X,Result,WF) :- | |
952 | equality_objects_wf(HFrom,X,PredRes,WF), | |
953 | %kernel_equality:equality_objects1(HFrom,X,PredRes,WF), % this could be called if X is guaranteed nonvar | |
954 | nonvar(PredRes), % only proceed if we have enough information to determine the result of the comparison | |
955 | (PredRes = pred_true -> Result = HTo % we have found the value; we assume there is no other value later | |
956 | % TO DO: if find_abort_values=true: look later in the list if for all other HFrom PredRes=pred_false | |
957 | ; regular_lookup_result_in_list(T,X,Result,WF)). | |
958 | ||
959 | % a faster version which does not use equality_objects_wf | |
960 | fast_lookup_result([(HFrom,HTo)|T],X,Result,WF) :- !, | |
961 | equality_can_be_decided_by_unification(HFrom), | |
962 | (HFrom=X -> Result = HTo | |
963 | ; fast_lookup_result(T,X,Result,WF) | |
964 | ). | |
965 | fast_lookup_result(List,X,Result,WF) :- | |
966 | regular_lookup_result_in_list(List,X,Result,WF). | |
967 | ||
968 | ||
969 | % get_comprehension_set(b(SET,_,_),ID,PRED) :- get_comprehension_set_aux(SET,ID,PRED). | |
970 | % get_comprehension_set_aux(comprehension_set([TID],PRED),ID,PRED) :- | |
971 | % get_texpr_id(TID,ID). | |
972 | % get_comprehension_set_aux(value(V),ID,PRED) :- nonvar(V), V = closure([ID],_,PRED). | |
973 | ||
974 | ||
975 | ||
976 | ||
977 | quick_test_membership1(b(value(VA),_,_),VB,Result) :- | |
978 | quick_test_membership_aux(VB,VA,Result). | |
979 | quick_test_membership_aux(VAR,_,_) :- var(VAR),!,fail. | |
980 | quick_test_membership_aux([],_,pred_false). | |
981 | quick_test_membership_aux(avl_set(AVL),X,Result) :- | |
982 | custom_explicit_sets:quick_test_avl_membership(AVL,X,Result). % we could also check that in case X is not ground but partially instantiated, whether there is a possible match in AVL (if not Result = pred_false) | |
983 | quick_test_membership_aux(global_set(GS),X,Result) :- nonvar(X), X=int(IX), nonvar(IX), | |
984 | custom_explicit_sets:membership_global_set(GS,X,R,_WF), | |
985 | nonvar(R), Result=R. | |
986 | quick_test_membership_aux(closure(P,T,B),X,Result) :- nonvar(X), X=int(IX), nonvar(IX), | |
987 | is_fixed_interval(P,T,B,LOW,UP), | |
988 | kernel_equality:in_nat_range_test(X,int(LOW),int(UP),R), | |
989 | nonvar(R), Result=R. | |
990 | quick_test_membership_aux(closure(P,T,B),X,Result) :- X==[], % check {} : POW(_) / FIN(_) and {} : POW1(_) / FIN1(_) | |
991 | custom_explicit_sets:is_powerset_closure(closure(P,T,B),Kind,_), | |
992 | (contains_empty_set(Kind) -> Result = pred_true ; Result=pred_false). | |
993 | ||
994 | is_fixed_interval(P,T,B,LOW,UP) :- | |
995 | custom_explicit_sets:is_interval_closure(P,T,B,LOW,UP), integer(LOW),integer(UP). | |
996 | ||
997 | contains_empty_set(pow). | |
998 | contains_empty_set(fin). | |
999 | ||
1000 | convert_pred_res(pred_false,falsity). | |
1001 | convert_pred_res(pred_true,truth). | |
1002 | convert_neg_pred_res(pred_true,falsity). | |
1003 | convert_neg_pred_res(pred_false,truth). | |
1004 | ||
1005 | generate_equality(b(A,_,_),b(B,_,_),Res) :- | |
1006 | ( generate_equality_aux(A,B,Res) ; | |
1007 | generate_equality_aux(B,A,Res) ), | |
1008 | !. | |
1009 | generate_equality(A,B,equal(A,B)). | |
1010 | ||
1011 | generate_equality_aux(convert_bool(AA),value(PT),Res) :- | |
1012 | PT==pred_true, | |
1013 | get_texpr_expr(AA,TA), | |
1014 | !, | |
1015 | Res = TA. | |
1016 | generate_equality_aux(convert_bool(AA),value(PF),Res) :- | |
1017 | PF==pred_false,!, | |
1018 | Res = negation(AA). | |
1019 | ||
1020 | % generate an equal(_,_) node where the second one is a Value | |
1021 | generate_equality_with_value(b(value(ValA),_,_),true,ValB,true,_TA,NExpr) :- | |
1022 | % both are FullyKnown | |
1023 | simple_value(ValA), % we should avoid closures | |
1024 | !, | |
1025 | kernel_equality:equality_objects(ValA,ValB,PRes), | |
1026 | convert_pred_res(PRes,NExpr). | |
1027 | generate_equality_with_value(NExprA,_,Value,_,TA,equal(NExprA,b(value(Value),TA,[]))). | |
1028 | ||
1029 | % similar to custom_explicit_sets:simple_value | |
1030 | % values where we can decide equality easily | |
1031 | simple_value(fd(_,_)). | |
1032 | simple_value(pred_true /* bool_true */). | |
1033 | simple_value(pred_false /* bool_false */). | |
1034 | simple_value(int(_)). | |
1035 | simple_value((A,B)) :- simple_value(A), simple_value(B). | |
1036 | simple_value(rec(Fields)) :- maplist(simple_field,Fields). | |
1037 | simple_value(string(_)). | |
1038 | ||
1039 | simple_field(field(_,Val)) :- simple_value(Val). | |
1040 | ||
1041 | known_value(X,FullyKnown) :- (known_value(X) -> FullyKnown=true ; FullyKnown=false). | |
1042 | known_value(X) :- nonvar(X), known_value2(X). | |
1043 | known_value2(global_set(GS)) :- nonvar(GS). | |
1044 | known_value2(freetype(GS)) :- nonvar(GS). | |
1045 | known_value2(closure(P,T,B)) :- known_closure(P,T,B). | |
1046 | %Note: for other closures: they still may have to be computed; some of the computations in wd_and_efficient could be expensive for closures | |
1047 | known_value2(avl_set(_)). % already fully normalised | |
1048 | known_value2((X,Y)) :- known_value(X),known_value(Y). | |
1049 | known_value2(fd(A,B)) :- number(A),atomic(B). | |
1050 | known_value2(int(N)) :- number(N). | |
1051 | known_value2([]). | |
1052 | known_value2(pred_true). | |
1053 | known_value2(pred_false). | |
1054 | known_value2(string(S)) :- atomic(S). | |
1055 | known_value2([H|T]) :- known_value(H), known_value(T). | |
1056 | %known_value2(record(Fields)) :- known_fields(Fields). | |
1057 | known_value2(rec(Fields)) :- known_fields(Fields). | |
1058 | ||
1059 | % something we could do: | |
1060 | %optimize_known_value([H|T],Res) :- (convert_to_avl([H|T],CS) -> Res=CS ; print(failed_to_convert_known_list),nl,fail). | |
1061 | % try_convert_to_avl | |
1062 | ||
1063 | known_closure(P,T,B) :- custom_explicit_sets:is_interval_closure(P,T,B,Low,Up), !, | |
1064 | number(Low), number(Up), | |
1065 | Up < Low+1000. | |
1066 | known_closure(P,T,B) :- | |
1067 | is_cartesian_product_closure(closure(P,T,B),A1,A2), | |
1068 | !,% we could call is_cartesian_product_closure_aux(P,T,B,A1,A2) | |
1069 | known_value(A1), known_value(A2). | |
1070 | ||
1071 | known_fields(X) :- var(X),!,fail. | |
1072 | known_fields([]). | |
1073 | known_fields([field(N,V)|T]) :- ground(N),known_value(V),known_fields(T). | |
1074 | ||
1075 | %b_evaluate1(TExpr,Parameters,LS,S,ResultTExpr,FullyKnown) :- | |
1076 | ||
1077 | check_is_id_list([],[]). | |
1078 | check_is_id_list([H|T],Res) :- | |
1079 | (H=b(identifier(_),_,_) | |
1080 | -> add_internal_error('Typed id list as argument: ',check_is_id_list([H|T],Res)), % use get_texpr_ids or maplist(def_get_texpr_id,P,PIDs) | |
1081 | maplist(def_get_texpr_id,[H|T],Res) | |
1082 | ; Res=[H|T]). | |
1083 | ||
1084 | :- use_module(kernel_frozen_info,[kfi_domain/2]). | |
1085 | ||
1086 | :- use_module(custom_explicit_sets,[construct_interval_closure/3]). | |
1087 | % try and evaluate domain of a list (avl_set already dealt with separately) | |
1088 | %evaluate_domain(X,_) :- print(dom(X)),nl,fail. | |
1089 | evaluate_domain(sequence_extension(L),Domain) :- length(L,Len), | |
1090 | % this will prevent computing range of sequence extension: can hide WD issues ! TO DO: check wd info and/or preference | |
1091 | construct_interval_closure(1,Len,Domain). | |
1092 | % TO DO: set_extension when possible ? | |
1093 | evaluate_domain(value(L),Domain) :- | |
1094 | get_domain(L,Domain). | |
1095 | ||
1096 | get_domain(V,Dom) :- var(V),!,kfi_domain(V,Dom). % try infer domain from attached co-routines | |
1097 | get_domain([],[]). | |
1098 | get_domain([V|VT],Result) :- nonvar(V), V=(D,_), | |
1099 | known_value(D),get_list_domain(VT,DT), | |
1100 | %length(DT,Len),print(got_list_domain(D,Len)),nl, | |
1101 | (custom_explicit_sets:try_convert_to_avl([D|DT],Res) -> Result=Res | |
1102 | ; write(could_not_convert_domain_to_avl(D)),nl, Result=[D|DT]). %sort([D|DT],Result)? | |
1103 | % we could also do this: | |
1104 | %get_domain(closure(Par,Typ,Body),Result) :- | |
1105 | % is_lambda_value_domain_closure(Par,Typ,Body, DomainValue,Expr), check_wd(Expr), | |
1106 | % Result=DomainValue. | |
1107 | get_list_domain(V,_) :- var(V),!,fail. | |
1108 | get_list_domain([],[]). | |
1109 | get_list_domain([V|VT],[D|DT]) :- nonvar(V), V=(D,_), | |
1110 | known_value(D),get_list_domain(VT,DT). | |
1111 | ||
1112 | ||
1113 | :- use_module(kernel_frozen_info,[kfi_range/2]). | |
1114 | ||
1115 | % try and evaluate range of a list (avl_set already dealt with separately) | |
1116 | evaluate_range(b(value(L),_T,_),Range) :- | |
1117 | get_range(L,Range). | |
1118 | get_range(V,Dom) :- var(V),!,kfi_range(V,Dom). % try infer range from attached co-routines | |
1119 | get_range([],[]). | |
1120 | get_range([V|VT],Result) :- nonvar(V), V=(_,D), | |
1121 | known_value(D), | |
1122 | get_list_range(VT,DT), | |
1123 | sort([D|DT],Result). | |
1124 | ||
1125 | get_list_range(V,_) :- var(V),!,fail. | |
1126 | get_list_range([],[]). | |
1127 | get_list_range([V|VT],[D|DT]) :- | |
1128 | nonvar(V), V=(_,D), | |
1129 | known_value(D), | |
1130 | get_list_range(VT,DT). | |
1131 | ||
1132 | create_equality_for_let(LHS,RHS,Conj) :- | |
1133 | maplist(create_eq,LHS,RHS,CL), | |
1134 | conjunct_predicates(CL,Conj). | |
1135 | create_eq(Id,Expr,TPred) :- safe_create_texpr(equal(Id,Expr),pred,TPred). | |
1136 | ||
1137 | % split formal operation call parameters into those which clash and those that do not: | |
1138 | split_formal_parameters([],[],_,[],[],[],[]). | |
1139 | split_formal_parameters([Formal1|FormalT],[Val1|VT],LocalKnownParas,Fresh,FV,Clash,CV) :- | |
1140 | (id_clash(LocalKnownParas,Formal1) | |
1141 | -> Fresh = FreshT, FV=FVT, Clash = [Formal1|ClashT], CV = [Val1|CVT] | |
1142 | ; Fresh = [Formal1|FreshT], FV = [Val1|FVT], Clash = ClashT, CV = CVT | |
1143 | ), split_formal_parameters(FormalT,VT,LocalKnownParas,FreshT,FVT,ClashT,CVT). | |
1144 | ||
1145 | :- use_module(gensym,[gensym/2]). | |
1146 | create_fresh_id(b(identifier(_),T,I),b(identifier(FRESHID),T,I)) :- | |
1147 | gensym('__COMPILED_ID__',FRESHID). | |
1148 | ||
1149 | :- use_module(bsyntaxtree, [get_texpr_pos/2,same_id/3]). | |
1150 | % compute which assignments are really necessary, remove skip assignments x := x | |
1151 | simplify_assignment([],[],[],[]). | |
1152 | simplify_assignment([ID1|T1],[ID2|T2],Res1,Res2) :- | |
1153 | (same_id(ID1,ID2,_) -> Res1=TR1, Res2=TR2 ; Res1=[ID1|TR1], Res2=[ID2|TR2]), | |
1154 | simplify_assignment(T1,T2,TR1,TR2). | |
1155 | ||
1156 | ||
1157 | /* | |
1158 | % check if an AST term is a total lambda without WD condition: | |
1159 | % NExprA=value(closure([x,...,'_lambda_result_'],b(equal())), NExprB=couple(,,,,) -> replace x by parameters | |
1160 | % possibly better to do this via contains_wd_condition or similar Info field?! | |
1161 | ||
1162 | ||
1163 | is_total_lambda(b(value(V),_,_),OtherIDs,LambdaExpr) :- nonvar(V), | |
1164 | V=closure(Args,_Types,Body), | |
1165 | is_total_lambda_closure(Args,Body, OtherIDs, LambdaExpr). | |
1166 | ||
1167 | :- use_module(probsrc(bsyntaxtree),[conjunction_to_list/2,occurs_in_expr/2]). | |
1168 | is_total_lambda_closure(Args,b(equal(TLambda,LambdaExpr),pred,_),OtherIDs,LambdaExpr) :- | |
1169 | get_texpr_id(TLambda,LambdaID), | |
1170 | append(OtherIDs,[LambdaID],Args), | |
1171 | \+ occurs_in_expr(LambdaID,LambdaExpr). | |
1172 | ||
1173 | % try and get arguments from expression | |
1174 | get_actual_arguments([_],Expr,Args) :- !, | |
1175 | % print('arg1: '),tools_printing:print_term_summary(Expr),nl, | |
1176 | check_simple(Expr), | |
1177 | Args= [Expr]. | |
1178 | get_actual_arguments([_|T],b(Couple,_,_),[Arg1|TArgs]) :- | |
1179 | get_couple(Couple,Arg1,Arg2), print('arg: '),tools_printing:print_term_summary(Arg1),nl, | |
1180 | check_simple(Arg1), | |
1181 | get_actual_arguments(T,Arg2,TArgs). | |
1182 | ||
1183 | check_simple(b(V,_,_)) :- simple2(V). | |
1184 | simple2(value(_)). | |
1185 | simple2(identifier(_)). | |
1186 | simple2(integer(_)). | |
1187 | ||
1188 | get_couple(couple(A,B),A,B). | |
1189 | %get_couple(value(V),A,B) :- nonvar(V), V=(V1,V2), ... % TODO | |
1190 | ||
1191 | ||
1192 | Code for bcompile2(function(...)) | |
1193 | ||
1194 | ||
1195 | % ; is_total_lambda(NExprA,Ids,Expr) , | |
1196 | % get_actual_arguments(Ids,NExprB,Args) %, print(ok),nl, translate:l_print_bexpr_or_subst(Args),nl | |
1197 | % -> | |
1198 | % bsyntaxtree:replace_ids_by_exprs(Expr,Ids,Args,Result), | |
1199 | % % only ok if we do not replicate expressions !! we could repeatedly re-apply rule / compilation on result | |
1200 | % print(' replaced: '),translate:print_bexpr(Result),nl, | |
1201 | % Result = b(NExpr,_,_), FullyKnown = FullyKnown12 | |
1202 | ||
1203 | */ |