1 | | % (c) 2009-2019 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(kernel_mappings, |
6 | | [ unary_function/3, |
7 | | binary_function/3, binary_arg1_determines_value/3, |
8 | | unary_in_boolean_type/2, unary_not_in_boolean_type/2, |
9 | | unary_in_definitely_true/2, |
10 | | binary_in_boolean_type/2, |
11 | | binary_not_in_boolean_type/2, |
12 | | binary_in_definitely_true/2, |
13 | | cst_in_boolean_type/2, cst_not_in_boolean_type/2, |
14 | | binary_boolean_operator/3, |
15 | | negate_binary_boolean_operator/2, |
16 | | symbolic_closure_binary_operator/1, is_definitely_empty/3, do_not_keep_symbolic/5, |
17 | | symbolic_closure_unary_operator/1, do_not_keep_symbolic_unary/2, |
18 | | |
19 | | special_binary_predicate/6, |
20 | | |
21 | | unary_kernel_call/8, |
22 | | binary_kernel_call/9, |
23 | | unary_in_kernel_call/6, |
24 | | binary_in_kernel_call/7, |
25 | | kernel_call_predicate/4, |
26 | | kernel_call_predicate_check_element_of_wf/4, kernel_call_predicate_equal_object_optimized/3, |
27 | | kernel_call_predicate_not_equal_object/4, |
28 | | kernel_call_predicate_not_element_of_wf/3, |
29 | | kernel_call/4, |
30 | | kernel_call_apply_to/6, |
31 | | |
32 | | kernel_call_predicate3/7, kernel_call_predicate2/6 |
33 | | ]). |
34 | | |
35 | | % new profiler |
36 | | %:- use_module('../extensions/profiler/profiler.pl'). |
37 | | %:- use_module('../extensions/profiler/profiler_te.pl'). |
38 | | %:- enable_profiling(must_succ_kernel_call/4). |
39 | | %:- enable_profiling(kernel_call_predicate/4). |
40 | | %:- enable_profiling(kernel_call/4). |
41 | | %:- enable_profiling(kernel_call_apply_to/5). |
42 | | %:- enable_profiling(kernel_call_or/5). |
43 | | |
44 | | % old profiler |
45 | | %:- use_module(hit_profiler, [add_profile_hit/1,add_profile_hit/2]). |
46 | | |
47 | | :- use_module(tools). |
48 | | |
49 | | :- use_module(module_information,[module_info/2]). |
50 | | :- module_info(group,kernel). |
51 | | :- module_info(description,'This module translates AST constructs to calls in the ProB kernel.'). |
52 | | |
53 | | :- use_module(self_check). |
54 | | :- use_module(kernel_waitflags,[get_wait_flag0/2]). |
55 | | :- use_module(kernel_tools,[value_variables/2]). |
56 | | |
57 | | :- meta_predicate kernel_call_or(0,*,*,*,*). |
58 | | |
59 | | :- use_module(debugging_calls). |
60 | | :- if(debug:global_debug_flag). |
61 | | :- register_debugging_call must_succ(*,-). |
62 | | :- else. |
63 | | :- register_debugging_call must_succ(*,-),kernel_det_call(*,-,-,-). |
64 | | :- endif. |
65 | | |
66 | | |
67 | | |
68 | | |
69 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
70 | | |
71 | | |
72 | | unary_kernel_call(Module,KernelFunction,ESV1,Value,WF,Expr,Type,Span) :- |
73 | | (expects_waitflag_and_span(KernelFunction) |
74 | | -> KernelCall =.. [KernelFunction,ESV1,Value,Span,WF] |
75 | | ; expects_waitflag(KernelFunction) -> KernelCall =.. [KernelFunction,ESV1,Value,WF] |
76 | | ; KernelCall =.. [KernelFunction,ESV1,Value] |
77 | | ), |
78 | | %print(call(Type,KernelCall)),nl, |
79 | | (type_ok_for_wf0(Type) -> %print(direct_call(Type,KernelCall)),nl, |
80 | | Module:KernelCall |
81 | | ; reversible_unary_function(KernelFunction) |
82 | | -> kernel_call_or(Module:KernelCall,ESV1,Value,WF,Expr) |
83 | | ; must_succ_kernel_call(Module:KernelCall,ESV1,WF,Expr) |
84 | | ). |
85 | | |
86 | | % result is ok for wf0: no optimized AVL representation exists; we do not need to delay calling function |
87 | | type_ok_for_wf0(integer). |
88 | | type_ok_for_wf0(boolean). |
89 | | type_ok_for_wf0(global(_)). |
90 | | type_ok_for_wf0(string). |
91 | | |
92 | | |
93 | | binary_kernel_call(_,KernelFunction,ESV1,ESV2,Value,WF,_Expr,_Type,Span) :- |
94 | | determined_binary_integer_function(KernelFunction), |
95 | | !, |
96 | | get_wait_flag0(WF,WF0), |
97 | | call_determined_integer_function(KernelFunction,ESV1,ESV2,Value,WF0,WF,Span). |
98 | | binary_kernel_call(Module,KernelFunction,ESV1,ESV2,Value,WF,Expr,Type,Span) :- |
99 | | (expects_waitflag_and_span(KernelFunction) |
100 | | -> KernelCall =.. [KernelFunction,ESV1,ESV2,Value,Span,WF] |
101 | | ; expects_waitflag(KernelFunction) |
102 | | -> KernelCall =.. [KernelFunction,ESV1,ESV2,Value,WF] |
103 | | ; expects_waitflag_and_type(KernelFunction) |
104 | | -> KernelCall =.. [KernelFunction,ESV1,ESV2,Value,Type,WF] |
105 | | ; KernelCall =.. [KernelFunction,ESV1,ESV2,Value] |
106 | | ), |
107 | | special_propagate_binary_function(KernelFunction,ESV1,ESV2,Value,WF), |
108 | | must_succ_kernel_call(Module:KernelCall,(ESV1,ESV2),WF,Expr). |
109 | | |
110 | | binary_in_kernel_call(Module,Kernel_predicate,ElValue,SV1,SV2,WF,_Expr) :- |
111 | | %KernelCall =.. [Kernel_predicate,ElValue,SV1,SV2,WF], |
112 | | %kernel_call(Module:KernelCall,(ElValue,SV1,SV2),WF,Expr). |
113 | | get_wait_flag0(WF,WF0), |
114 | | binary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0). |
115 | | |
116 | | :- block binary_in_kernel_call2(?,?,-,?,?,?,-). % wait until either WF0 set or ElValue |
117 | | binary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0) :- nonvar(WF0),!, |
118 | | call(Module:Kernel_predicate,ElValue,SV1,SV2,WF). |
119 | | binary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0) :- |
120 | | not_symbolic_when_var(ElValue,EWait), % ensure that we do not call this in case ElValue is a closure which may need expanding |
121 | | value_variables(SV1,G1), value_variables(SV2,G2), |
122 | | when((nonvar(WF0) ; ground(EWait), ground(G1), ground(G2)), |
123 | | call(Module:Kernel_predicate,ElValue,SV1,SV2,WF)). |
124 | | |
125 | | :- block not_symbolic_when_var(-,?). |
126 | | not_symbolic_when_var(closure(_,_,_),_) :- !. |
127 | | not_symbolic_when_var(X,WV) :- value_variables(X,WV). |
128 | | |
129 | | unary_in_kernel_call(Module,Kernel_predicate,ElValue,SV1,WF,_Expr) :- |
130 | | %KernelCall =.. [Kernel_predicate,ElValue,SV1,WF], |
131 | | %kernel_call(Module:KernelCall,(ElValue,SV1),WF,Expr). |
132 | ? | get_wait_flag0(WF,WF0), |
133 | ? | unary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,WF,WF0). |
134 | | |
135 | | :- block unary_in_kernel_call2(?,?,-,?,?,-). % wait until either WF0 set or ElValue |
136 | | unary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,WF,WF0) :- nonvar(WF0),!, |
137 | | call(Module:Kernel_predicate,ElValue,SV1,WF). |
138 | | unary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,WF,WF0) :- |
139 | ? | not_symbolic_when_var(ElValue,EWait), % ensure that we do not call this in case ElValue is a closure which may need expanding; then we should at least wait until WF0 is ground |
140 | ? | value_variables(SV1,G1), |
141 | ? | when((nonvar(WF0) ; ground(EWait), ground(G1)), |
142 | | call(Module:Kernel_predicate,ElValue,SV1,WF)). |
143 | | |
144 | | |
145 | | :- use_module(tools_printing,[print_term_summary/1]). |
146 | | %must_succ_kernel_call(kernel_objects:equal_object_optimized(A,B),(A1,A2),WF,Expr) :- !, %%print('EQUAL'),nl, |
147 | | % Call = kernel_objects:equal_object_optimized(A,B), |
148 | | % kernel_call_or(Call,A1,A2,WF,Expr). |
149 | | must_succ_kernel_call(Call,HasToBeGround,WF,_Expr) :- |
150 | | get_wait_flag0(WF,WF0), |
151 | | (nonvar(WF0) |
152 | | -> call(Call) |
153 | | ; %hit_profiler:add_profile_hit(must_succ_kernel_call(Call,WF0),3), |
154 | | %ground_value_check(HasToBeGround,G1), % using this makes test 1562 fail; probably because co-routines remain active after WF0 has been set, leading un bound variables preventing optimisations in kernel_objects |
155 | | value_variables(HasToBeGround,VG1), |
156 | | %must_succ_kernel_call2(Call,WF0,G1) |
157 | | when((nonvar(WF0);ground(VG1)),call(Call)) |
158 | | ). |
159 | | |
160 | | :- block must_succ_kernel_call2(?,-,-). |
161 | | must_succ_kernel_call2(Call,_,_) :- call(Call). % was ~~must_succ(~~kernel_det_call(Call,WF,WF0,Expr),Expr) |
162 | | |
163 | | |
164 | | kernel_call_predicate(equal_object_optimized(A,B),kernel_objects,WF,_) :- !, %print('EQUAL'),nl, |
165 | | get_wait_flag0(WF,WF0), |
166 | | equal_obj(A,B,WF0,WF). |
167 | | % equality is the only predicate that can generate AVL trees |
168 | | % OTHER CALLS: partition_wf, member of empty set or singleton set, CLPFD operators: TO DO add |
169 | | |
170 | | kernel_call_predicate(not_equal_object_wf(A,B,WF),kernel_objects,WF,Expr) :- !, |
171 | | get_wait_flag0(WF,WF0),not_eq_wf(A,B,WF,WF0,Expr). |
172 | | kernel_call_predicate(partition_wf(A,B,PWF),kernel_objects,WF,Expr) :- !, |
173 | | (nonvar(B),B=[B1|T],T==[] % just one set |
174 | | -> kernel_call_predicate(equal_object_optimized(A,B1),kernel_objects,WF,Expr) |
175 | | ; all_but_one_set_known([A|B],Known), |
176 | | kernel_call(kernel_objects:partition_wf(A,B,PWF),Known,WF,Expr)). |
177 | | kernel_call_predicate(less_than(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than(A,B). |
178 | | kernel_call_predicate(less_than_equal(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than_equal(A,B). |
179 | | kernel_call_predicate(greater_than(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than(B,A). |
180 | | kernel_call_predicate(greater_than_equal(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than_equal(B,A). |
181 | | kernel_call_predicate(check_element_of_wf(A,B,PWF),kernel_objects,WF,Expr) :- !, |
182 | | get_wait_flag0(WF,WF0), check_element_of_wf0(A,B,PWF,WF0,Expr). |
183 | | kernel_call_predicate(Call,Module,WF,_Expr) :- get_wait_flag0(WF,WF0), |
184 | | %hit_profiler:add_profile_hit(kernel_call_predicate(Call,WF0),2), |
185 | | call_wf0(Module:Call,WF0). |
186 | | %kernel_call_predicate(Call,HasToBeGround,WF,Expr) :- kernel_call(Call,HasToBeGround,WF,Expr). |
187 | | |
188 | | :- if(debug:use_timer). |
189 | | :- block call_wf0(?,-). |
190 | | call_wf0(X,_) :- debug:timer_call(X). %debug:watch(10,X). |
191 | | :- else. |
192 | | :- block call_wf0(?,-). |
193 | | call_wf0(Call,_) :- call(Call). |
194 | | :- endif. |
195 | | |
196 | | % unfolded version of above (for efficiency): |
197 | | kernel_call_predicate_equal_object_optimized(A,B,WF) :- %print('EQUAL'),nl, |
198 | ? | get_wait_flag0(WF,WF0),equal_obj(A,B,WF0,WF). |
199 | | kernel_call_predicate_check_element_of_wf(A,B,WF,Span) :- |
200 | ? | get_wait_flag0(WF,WF0), check_element_of_wf0(A,B,WF,WF0,Span). |
201 | | kernel_call_predicate_not_equal_object(A,B,WF,Expr) :- |
202 | | get_wait_flag0(WF,WF0),not_eq_wf(A,B,WF,WF0,Expr). |
203 | | kernel_call_predicate_not_element_of_wf(A,B,WF) :- |
204 | | get_wait_flag0(WF,WF0),not_element_of_wf0(A,B,WF,WF0). |
205 | | |
206 | | :- block not_element_of_wf0(?,?,?,-). |
207 | | not_element_of_wf0(ElemValue,SetValue,WF,_) :- kernel_objects:not_element_of_wf(ElemValue,SetValue,WF). |
208 | | |
209 | | kernel_call_predicate3(KernelCall,Arg1,Arg2,Arg3,Module,WF,_Expression) :- |
210 | ? | get_wait_flag0(WF,WF0), |
211 | | %print(kernel_call3(KernelCall,Arg1,Arg2,Arg3)),nl, |
212 | ? | call_wf0_3(Module:KernelCall,Arg1,Arg2,Arg3,WF,WF0). |
213 | | :- block call_wf0_3(?, ?,?,?,?, -). |
214 | ? | call_wf0_3(Call,A1,A2,A3,WF,_) :- call(Call,A1,A2,A3,WF). |
215 | | |
216 | | kernel_call_predicate2(KernelCall,Arg1,Arg2,Module,WF,_Expression) :- |
217 | | get_wait_flag0(WF,WF0), |
218 | | %print(kernel_call3(KernelCall,Arg1,Arg2,Arg3)),nl, |
219 | | call_wf0_2(Module:KernelCall,Arg1,Arg2,WF,WF0). |
220 | | :- block call_wf0_2(?, ?,?,?, -). |
221 | | call_wf0_2(Call,A1,A2,WF,_) :- call(Call,A1,A2,WF). |
222 | | |
223 | | :- use_module(custom_explicit_sets,[singleton_set/2]). |
224 | | :- block check_element_of_wf0(?,-,?,-,?). |
225 | | check_element_of_wf0(_A,B,_WF,_,_) :- B==[],!,fail. % nothing can be element of empty set; CAN PREVENT WD-ERRORS from being detected ! |
226 | | check_element_of_wf0(A,B,WF,_WF0,_) :- |
227 | | singleton_set(B,B1),!, /* also does var check */ |
228 | | equal_object_optimized_wf(A,B1,check_element_of_wf0,WF). %was equal_obj(A,B1,WF0) but as B1 is ground value will always call equal_object_optimized directly |
229 | ? | check_element_of_wf0(A,B,WF,WF0,_) :- nonvar(WF0),!, |
230 | ? | kernel_objects:check_element_of_wf(A,B,WF). |
231 | | % below B must be nonvar |
232 | | check_element_of_wf0(A,global_set(GS),WF,_,Span) :- nonvar(A), |
233 | | !, % be sure that we check something like int(-1) : NATURAL |
234 | | %kernel_objects:check_element_of_wf(A,global_set(GS),WF). |
235 | | kernel_objects:element_of_global_set_wf(A,GS,WF,Span). % Span for enumeration warnings |
236 | | check_element_of_wf0(A,avl_set(AVL),WF,_,_) :- simple_ground_value(A), |
237 | | !, % we can already check this efficiently in phase 0 |
238 | | custom_explicit_sets:element_of_avl_set_wf(AVL,A,WF). % we could even call avl_fetch directly |
239 | | % kernel_objects:check_element_of_wf(A,avl_set(AVL),WF). |
240 | | check_element_of_wf0(A,B,WF,WF0,Span) :- |
241 | | check_element_of_wf0_aux(A,B,WF,WF0,Span). |
242 | | :- block check_element_of_wf0_aux(?,?,?,-,?). |
243 | | check_element_of_wf0_aux(A,global_set(GS),WF,_WF0,Span) :- !, |
244 | | kernel_objects:element_of_global_set_wf(A,GS,WF,Span). % Span for enumeration warnings |
245 | | check_element_of_wf0_aux(A,B,WF,_WF0,_Span) :- kernel_objects:check_element_of_wf(A,B,WF). |
246 | | |
247 | | simple_ground_value(A) :- nonvar(A), simple_ground_value_aux(A). |
248 | | simple_ground_value_aux(int(X)) :- number(X). |
249 | | simple_ground_value_aux(fd(X,_)) :- number(X). |
250 | | simple_ground_value_aux(string(S)) :- ground(S). |
251 | | simple_ground_value_aux((A,B)) :- simple_ground_value(A), simple_ground_value(B). |
252 | | simple_ground_value_aux(rec(F)) :- simple_ground_fields(F). |
253 | | simple_ground_value_aux([]). |
254 | | |
255 | | simple_ground_fields(Var) :- var(Var),!,fail. % TO DO: we could activate check as soon as it becomes ground |
256 | | simple_ground_fields([]). |
257 | | simple_ground_fields([field(N,V)|T]) :- nonvar(N),simple_ground_value(V),simple_ground_fields(T). |
258 | | |
259 | | :- assert_must_succeed( kernel_mappings:not_eq_wf(int(1),int(2),_,_,_) ). |
260 | | :- assert_must_succeed( kernel_mappings:not_eq_wf([int(1)],[int(2)],_,0,_) ). |
261 | | :- block not_eq_wf(-,?,?,-,?), not_eq_wf(?,-,?,-,?). |
262 | | not_eq_wf(A,B,WF,_,_) :- efficient_value(A),efficient_value(B),!, %print_term_summary(not_eq_wf(A,B)), |
263 | | kernel_objects:not_equal_object_wf(A,B,WF). |
264 | | not_eq_wf(A,B,WF,WF0,Expr) :- not_eq_wf0(A,B,WF,WF0,Expr). |
265 | | :- block not_eq_wf0(?,?,?,-,?). |
266 | | not_eq_wf0(A,B,WF,_,_Expr) :- |
267 | | %((var(A),var(B)) -> instantiate_argument(Expr,A) ; true), |
268 | | kernel_objects:not_equal_object_wf(A,B,WF). |
269 | | |
270 | | /* not required anymore ?! |
271 | | % instantiate argument according to type of expression to ensure not_equal_object (or other calls) are triggered and do not wait setting up dif constraints |
272 | | instantiate_argument(not_equal(AE,_),A) :- |
273 | | bsyntaxtree:get_texpr_type(AE,Type),!, print(instantiate(Type,A)),nl,trace, |
274 | | instantiate_arg(Type,A). |
275 | | instantiate_argument(_,_). |
276 | | |
277 | | instantiate_arg(string,R) :- !, R=string(_). |
278 | | instantiate_arg(integer,R) :- !, R=int(_). |
279 | | % missing: more cases global(G),.... ? |
280 | | instantiate_arg(_,_). |
281 | | */ |
282 | | |
283 | | % check whether disequality can be efficiently checked (already in WF0 phase) |
284 | | efficient_value(X) :- var(X),!,fail. |
285 | | efficient_value(int(_)). |
286 | | efficient_value(avl_set(_)). |
287 | | efficient_value([]). |
288 | | efficient_value(fd(_,_)). |
289 | | efficient_value(string(_)). |
290 | | efficient_value((A,B)) :- nonvar(A),nonvar(B),efficient_value(A), efficient_value(B). |
291 | | efficient_value(pred_true). efficient_value(pred_false). |
292 | | |
293 | | |
294 | | |
295 | | |
296 | | %:- meta_predicate kernel_call_or(0,*,*,*). |
297 | | kernel_call(Call,HasToBeGround,WF,Expr) :- |
298 | ? | get_wait_flag0(WF,WF0), |
299 | | %hit_profiler:add_profile_hit(kernel_call(Call,WF),2), |
300 | ? | (nonvar(WF0) |
301 | | -> ~~kernel_det_call(Call,WF,WF0,Expr) |
302 | ? | ; value_variables(HasToBeGround,G1), |
303 | ? | when((nonvar(WF0) ; ground(G1)) , |
304 | | ( %(var(WF0) -> print('enter :'),print_term_summary(Call) ; true), |
305 | | % print(kernel_det_call(Call,WF,WF0,Expr)),nl, |
306 | | ~~kernel_det_call(Call,WF,WF0,Expr) |
307 | | % ,print(finished_kernel_det_call(Call,WF,WF0)),nl |
308 | | %,(var(WF0) -> print('result :'),print_term_summary(Call) ; true) |
309 | | ) ) |
310 | | ). |
311 | | |
312 | | :- use_module(kernel_tools,[ground_value/1,ground_value_check/2]). |
313 | | % optimized custom versions of kernel_call for performacne: |
314 | | :- use_module(bsets_clp,[apply_to/5]). |
315 | | kernel_call_apply_to(FValue,ArgValue,Res,FunctionType,Span,WF) :- |
316 | | %hit_profiler:add_profile_hit(kernel_call_apply_to(FValue,ArgValue,Res,WF)), |
317 | ? | get_wait_flag0(WF,WF0), |
318 | ? | (var(WF0) %(var(WF0), \+ ground(ArgValue), \+ ground(FValue)) |
319 | | -> ground_value_check((ArgValue,FValue),WF1), |
320 | | call_apply_to(FValue,ArgValue,Res,FunctionType,Span,WF,WF0,WF1) |
321 | ? | ; bsets_clp:apply_to(FValue,ArgValue,Res,FunctionType,Span,WF) |
322 | | ). |
323 | | % TO DO: maybe transmit Type information for using with element/3 |
324 | | |
325 | | :- block call_apply_to(?,?,?,?,?,?,-,-). |
326 | | call_apply_to(FValue,ArgValue,Res,FunctionType,Span,WF,_,_Gr) :- |
327 | | %discard_ground_value_check(Gr), |
328 | | bsets_clp:apply_to(FValue,ArgValue,Res,FunctionType,Span,WF). |
329 | | |
330 | | |
331 | | /* ------------------------------- */ |
332 | | |
333 | | :- use_module(kernel_objects,[equal_object_optimized_wf/4]). |
334 | | :- block equal_obj(-,-,-,?). |
335 | | |
336 | ? | equal_obj(A,B,WF0,WF) :- nonvar(WF0),!, |
337 | ? | equal_object_optimized_wf(A,B,equal_obj1,WF). |
338 | | equal_obj(A,B,WF0,WF) :- %hit_profiler:add_profile_hit(eq(A,B)), |
339 | | %print(eq_obj(A,B)),nl, |
340 | | non_simple_value_variables(A,VA), |
341 | | (VA==[] -> equal_object_optimized_wf(A,B,equal_obj2,WF) |
342 | | ; non_simple_value_variables(B,VB), |
343 | | (VB==[] -> equal_object_optimized_wf(A,B,equal_obj3,WF) |
344 | | ; when((nonvar(WF0);ground(VA);ground(VB)), kernel_objects:equal_object_optimized_wf(A,B,equal_obj4,WF)) |
345 | | ) |
346 | | ). |
347 | | |
348 | | % a version of value_variables that also returns [] in some cases where there is a variable but equal_object can be called |
349 | | non_simple_value_variables(V,Vars) :- var(V),!, Vars=[V]. |
350 | | non_simple_value_variables(pred_false,Vars) :- !, Vars=[]. |
351 | | non_simple_value_variables(pred_true,Vars) :- !, Vars=[]. |
352 | | non_simple_value_variables(int(_),Vars) :- !, Vars=[]. % may contain var; but we can unify nonetheless |
353 | | non_simple_value_variables(string(_),Vars) :- !, Vars=[]. % ditto |
354 | | non_simple_value_variables(fd(_,_),Vars) :- !, Vars=[]. % ditto |
355 | | non_simple_value_variables(A,Vars) :- !, value_variables(A,Vars). |
356 | | |
357 | | |
358 | | :- if(debug:global_debug_flag). |
359 | | kernel_call_or(Call,HasToBeGround1,HasToBeGround2,WF,Expr) :- |
360 | | get_wait_flag0(WF,WF0), |
361 | | % print(kernel_call_start(Call)),nl, |
362 | | % det_call(Call) |
363 | | value_variables(HasToBeGround1,G1), |
364 | | (G1==[] -> G2=[] ; value_variables(HasToBeGround2,G2)), |
365 | | when((nonvar(WF0) ; ground(G1) ; ground(G2) ) , |
366 | | ( %(var(WF0) -> (print('enter o:'),print_term_summary(Call)) ; true), |
367 | | (var(WF0) -> ~~must_succ(~~kernel_det_call(Call,WF,WF0,Expr),Expr) |
368 | | ; ~~kernel_det_call(Call,WF,WF0,Expr)) |
369 | | %,(var(WF0) -> (print('resulto:'),print_term_summary(Call)) ; true) |
370 | | ) ) |
371 | | . |
372 | | :- else. |
373 | | kernel_call_or(Call,HasToBeGround1,HasToBeGround2,WF,_Expr) :- |
374 | | get_wait_flag0(WF,WF0), |
375 | | value_variables(HasToBeGround1,G1), |
376 | | (G1==[] -> G2=[] ; value_variables(HasToBeGround2,G2)), |
377 | | %hit_profiler:add_profile_hit(kernel_call_or(Call,WF0),2), |
378 | | when( (nonvar(WF0) ; ground(G1) ; ground(G2) ) , call(Call)). |
379 | | :- endif. |
380 | | |
381 | | |
382 | | % special case for calling binary integer functions: here we can use more efficient block declarations |
383 | | call_determined_integer_function(KF,V1,V2,Val,WF0,WF,Span) :- |
384 | | determined(V1,V2,Val,Determined,WF0), |
385 | | call_determined_integer_function2(KF,V1,V2,Val,WF0,Determined,WF,Span). |
386 | | :- block call_determined_integer_function2(?,?,?,?,-,-,?,?). |
387 | | %call_determined_integer_function2(KF,V1,V2,V,WF0,Det,_,_) :- |
388 | | % print(kernel_det_call(KF,V1,V2,V,WF0,Det)),nl,fail. |
389 | | call_determined_integer_function2(division,V1,V2,Val,_,_,WF,Span) :- |
390 | | kernel_objects:division(V1,V2,Val,Span,WF). |
391 | | call_determined_integer_function2(floored_division,V1,V2,Val,_,_,WF,Span) :- |
392 | | kernel_objects:floored_division(V1,V2,Val,Span,WF). |
393 | | call_determined_integer_function2(int_minus,V1,V2,Val,_,_,_WF,_Span) :- |
394 | | kernel_objects:int_minus(V1,V2,Val). |
395 | | call_determined_integer_function2(int_plus,V1,V2,Val,_,_,_WF,_Span) :- |
396 | | % kernel_call_determined(kernel_objects:int_plus(V1,V2,Val),V1,V2,Val,WF,integer). |
397 | | kernel_objects:int_plus(V1,V2,Val). |
398 | | call_determined_integer_function2(int_power,V1,V2,Val,_,_,WF,Span) :- |
399 | | kernel_objects:int_power(V1,V2,Val,Span,WF). |
400 | | call_determined_integer_function2(modulo,V1,V2,Val,_,_,WF,Span) :- |
401 | | kernel_objects:modulo(V1,V2,Val,Span,WF). |
402 | | call_determined_integer_function2(times,V1,V2,Val,_,_,_WF,_Span) :- |
403 | | kernel_objects:times(V1,V2,Val). |
404 | | |
405 | | % sets last argument to determined without instantiating its first three args |
406 | | % it is set when two integer values are known |
407 | | :- block determined(-,-,?,?,-), determined(-,?,-,?,-), determined(?,-,-,?,-). |
408 | | %:- block determined(-,-,?,?,?), determined(-,?,-,?,?), determined(?,-,-,?,?). |
409 | | %determined(Y,V,X,Det,WF0) :- print(determined(Y,V,X,Det,WF0)),nl,fail. |
410 | | determined(_X,_Y,_Z,Det,WF0) :- nonvar(WF0),!,Det=determined. |
411 | | % ((nonvar(_X),nonvar(_Y), \+ ground(_Y), var(_V)) -> trace ; true). |
412 | | determined(X,Y,V,Det,_) :- var(X),!, Y=int(YY),V=int(VV), %(YY=0 -> X=V ; true), |
413 | | determined2(X,YY,VV,Det). |
414 | | determined(Y,X,V,Det,_) :- var(X),!, Y=int(YY),V=int(VV), %(YY=0 -> X=V ; true), |
415 | | determined2(X,YY,VV,Det). |
416 | | determined(Y,V,X,Det,_) :- Y=int(YY),V=int(VV), %(YY=0 -> X=V ; VV=0 -> X=Y), |
417 | | determined2(X,YY,VV,Det). |
418 | | :- block determined2(-,-,?,?), determined2(-,?,-,?), determined2(?,-,-,?). |
419 | | %determined2(Y,V,X,Det) :- print(determined2(Y,V,X,Det)),nl,fail. |
420 | | determined2(X,_,_,Det) :- var(X),!,Det=determined. |
421 | | determined2(int(XX),YY,VV,Det) :- determined3(XX,YY,VV,Det). |
422 | | :- block determined3(-,-,?,?), determined3(-,?,-,?), determined3(?,-,-,?). |
423 | | %determined3(Y,V,X,Det) :- print(determined3(Y,V,X,Det)),nl,fail. |
424 | | determined3(_,_,_,determined). |
425 | | |
426 | | |
427 | | :- use_module(translate,[print_unwrapped_bexpr_with_limit/1]). |
428 | | :- public kernel_det_call/4. |
429 | | %kernel_det_call(X,_,_,_) :- !, call(X). %% comment in to avoid checks below |
430 | | :- if(debug:use_timer). |
431 | | kernel_det_call(X,_,_,_) :- debug:timer_call(X). %debug:watch(10,X). |
432 | | :- else. |
433 | | kernel_det_call(X,WF,WF0,_Expr) :- var(WF0),!, |
434 | | % print('+enter :'),print_term_summary(X),print('+ for :'), translate:print_unwrapped_bexpr_with_limit(_Expr) |
435 | | call(X), %debug:watch(10,X), |
436 | | % print('+result :'),print_term_summary(X), |
437 | | (self_check:run_time_type_check_mode(off) -> |
438 | | true |
439 | | ; ( (ground(X) ; (term_variables(X,XV), term_variables(WF,WV),XV==WV)) -> |
440 | | true |
441 | | ; add_message(kernel_det_call,'### Kernel Call does not ground variables: ',X) |
442 | | % note: can also occur when operator is undefined for args (front_of_sequence([],...) |
443 | | % in this case it is not an error |
444 | | ) |
445 | | ). |
446 | | kernel_det_call(X,_,_,_) :- call(X). |
447 | | :- endif. |
448 | | |
449 | | |
450 | | :- public must_succ/2. |
451 | | :- meta_predicate must_succ(0,*). |
452 | | must_succ(X,_Expr) :- self_check:run_time_type_check_mode(off),!, call(X). |
453 | | must_succ(X,Expr) :- |
454 | | if(call(X),true, (nl,print('FAILED: '),nl,print_unwrapped_bexpr_with_limit(Expr),print(X),nl,nl,fail)). |
455 | | |
456 | | |
457 | | :- use_module(error_manager). |
458 | | |
459 | | invalid_call(X) :- \+ check_valid_kernel_call(X,_). |
460 | | check_valid_kernel_call(X,unary) :- unary_function(_,_,X). |
461 | | check_valid_kernel_call(X,binary) :- binary_function(_,_,X). |
462 | | check_valid_kernel_call(X,_) :- add_error(check_valid_kernel_call,'Illegal Kernel Call: ',X),fail. |
463 | | :- assert_must_fail((kernel_mappings:expects_waitflag_and_span(X), |
464 | | kernel_mappings:invalid_call(X))). |
465 | | |
466 | | expects_waitflag_and_span(first_sequence). |
467 | | expects_waitflag_and_span(last_sequence). |
468 | | expects_waitflag_and_span(tail_sequence). |
469 | | expects_waitflag_and_span(front_sequence). |
470 | | expects_waitflag_and_span(minimum_of_set). |
471 | | expects_waitflag_and_span(maximum_of_set). |
472 | | expects_waitflag_and_span(intersection_generalized_wf). |
473 | | |
474 | | expects_waitflag_and_span(division). |
475 | | expects_waitflag_and_span(floored_division). |
476 | | expects_waitflag_and_span(modulo). |
477 | | expects_waitflag_and_span(int_power). |
478 | | expects_waitflag_and_span(singleton_set_element). |
479 | | |
480 | | :- assert_must_fail((kernel_mappings:expects_waitflag(X), |
481 | | kernel_mappings:invalid_call(X))). |
482 | | :- assert_must_fail((kernel_mappings:expects_waitflag(X), |
483 | | kernel_mappings:expects_waitflag_and_span(X))). |
484 | | /* |
485 | | comment in if we want to ensure that all kernel predicates take at least the WF |
486 | | :- assert_must_fail((kernel_mappings:unary_function(_,_,X), |
487 | | \+ (kernel_mappings:expects_waitflag(X) ; |
488 | | kernel_mappings:expects_waitflag_and_span(X)), |
489 | | print(unary_no_waitflag(X)),nl )). |
490 | | :- assert_must_fail((kernel_mappings:binary_function(_,_,X), |
491 | | \+ (kernel_mappings:expects_waitflag(X) ; |
492 | | kernel_mappings:expects_waitflag_and_span(X)), |
493 | | print(binary_no_waitflag(X)),nl )). |
494 | | */ |
495 | | |
496 | | expects_waitflag(append_sequence). |
497 | | expects_waitflag(bag_items). |
498 | | expects_waitflag(compaction). |
499 | | expects_waitflag(concat_sequence). |
500 | | expects_waitflag(concatentation_of_sequences). |
501 | | expects_waitflag(difference_set_wf). |
502 | | expects_waitflag(direct_product_wf). |
503 | | expects_waitflag(parallel_product_wf). |
504 | | expects_waitflag(domain_restriction_wf). |
505 | | expects_waitflag(domain_subtraction_wf). |
506 | | expects_waitflag(domain_wf). |
507 | | expects_waitflag(finite_cardinality_as_int). |
508 | | expects_waitflag(identity_relation_over_wf). |
509 | | expects_waitflag(image_wf). |
510 | | expects_waitflag(intersection). |
511 | | expects_waitflag(invert_relation_wf). |
512 | | expects_waitflag(relational_trans_closure_wf). |
513 | | expects_waitflag(override_relation). |
514 | | expects_waitflag(prefix_sequence_wf). |
515 | | expects_waitflag(prepend_sequence). |
516 | | expects_waitflag(range_restriction_wf). |
517 | | expects_waitflag(range_subtraction_wf). |
518 | | expects_waitflag(range_wf). |
519 | | expects_waitflag(rel_composition_wf). |
520 | | %expects_waitflag(rel_iterate_wf). |
521 | | expects_waitflag(rev_sequence). |
522 | | expects_waitflag(size_of_sequence). |
523 | | expects_waitflag(square). |
524 | | expects_waitflag(suffix_sequence). |
525 | | expects_waitflag(unary_minus_wf). |
526 | | expects_waitflag(union_generalized_wf). |
527 | | expects_waitflag(union_wf). |
528 | | |
529 | | expects_waitflag_and_type(rel_iterate_wf). |
530 | | |
531 | | :- use_module(bsyntaxtree,[get_texpr_set_type/2]). |
532 | | % only used when not in CLPFD mode: |
533 | | special_binary_predicate(greater(b(card(X),integer,_),Y), kernel_objects:cardinality_greater,X,TypeX,Y,integer) :- |
534 | | get_texpr_set_type(X,TypeX). |
535 | | special_binary_predicate(less(Y,b(card(X),integer,_)), kernel_objects:cardinality_greater,X,TypeX,Y,integer) :- |
536 | | get_texpr_set_type(X,TypeX). |
537 | | special_binary_predicate(greater_equal(b(card(X),integer,_),Y), kernel_objects:cardinality_greater_equal,X,TypeX,Y,integer) :- |
538 | | get_texpr_set_type(X,TypeX). |
539 | | special_binary_predicate(less_equal(Y,b(card(X),integer,_)), kernel_objects:cardinality_greater_equal,X,TypeX,Y,integer) :- |
540 | | get_texpr_set_type(X,TypeX). |
541 | | |
542 | | |
543 | | |
544 | | /* EXPRESSIONS */ |
545 | | |
546 | | |
547 | | :- assert_must_fail((kernel_mappings:reversible_unary_function(X), |
548 | | kernel_mappings:invalid_call(X))). |
549 | | |
550 | | reversible_unary_function(invert_relation_wf). |
551 | | reversible_unary_function(rev_sequence). |
552 | | reversible_unary_function(unary_minus_wf). |
553 | | |
554 | | unary_function(reverse,bsets_clp,invert_relation_wf). |
555 | | unary_function(closure,bsets_clp,relational_trans_closure_wf). % this is closure1 |
556 | | %unary_function(reflexive_closure,bsets_clp,relational_reflexive_closure). % now done in ast_cleanup |
557 | | unary_function(domain,bsets_clp,domain_wf). |
558 | | unary_function(range,bsets_clp,range_wf). |
559 | | |
560 | | unary_function(general_union,kernel_objects,union_generalized_wf). |
561 | | unary_function(general_intersection,kernel_objects,intersection_generalized_wf). |
562 | | |
563 | | unary_function(first,bsets_clp,first_sequence). |
564 | | unary_function(size,bsets_clp,size_of_sequence). |
565 | | unary_function(front,bsets_clp,front_sequence). |
566 | | unary_function(tail,bsets_clp,tail_sequence). |
567 | | unary_function(rev,bsets_clp,rev_sequence). |
568 | | unary_function(last,bsets_clp,last_sequence). |
569 | | |
570 | | unary_function(card,kernel_objects,finite_cardinality_as_int). |
571 | | unary_function(pow_subset,kernel_objects,power_set). % not really necessary anymore |
572 | | unary_function(fin_subset,kernel_objects,power_set). % not really necessary anymore |
573 | | unary_function(pow1_subset,kernel_objects,non_empty_power_set). % not really necessary anymore |
574 | | unary_function(fin1_subset,kernel_objects,non_empty_power_set). % not really necessary anymore |
575 | | unary_function(identity,bsets_clp,identity_relation_over_wf). |
576 | | %unary_function(perm,bsets_clp,enumerate_permutation_sequence). |
577 | | % unary_function(iseq,bsets_clp,enumerate_injective_sequence). |
578 | | %unary_function(iseq1,bsets_clp,enumerate_non_empty_injective_sequence). |
579 | | %unary_function(seq,bsets_clp,enumerate_sequence). |
580 | | %unary_function(seq1,bsets_clp,enumerate_non_empty_sequence). |
581 | | %unary_function(struct,kernel_records,enumerate_records). |
582 | | |
583 | | unary_function(general_concat,bsets_clp,concatentation_of_sequences). |
584 | | unary_function(unary_minus,kernel_objects,unary_minus_wf). |
585 | | unary_function(square_multiplication,kernel_objects,square). % artificial construct, detected when X*X is evaluated by interpreter; but square is directly called |
586 | | unary_function(min,kernel_objects,minimum_of_set). |
587 | | unary_function(max,kernel_objects,maximum_of_set). |
588 | | |
589 | | unary_function(first_of_pair,kernel_objects,first_of_pair). |
590 | | unary_function(second_of_pair,kernel_objects,second_of_pair). |
591 | | unary_function(mu,kernel_objects,singleton_set_element). % Z MU operator |
592 | | |
593 | | unary_function(compaction,kernel_z,compaction). |
594 | | unary_function(bag_items,kernel_z,bag_items). |
595 | | |
596 | | |
597 | | :- assert_must_fail((kernel_mappings:determined_binary_integer_function(X), |
598 | | kernel_mappings:invalid_call(X))). |
599 | | /* binary functions where 1 argument is determined from the other two */ |
600 | | determined_binary_integer_function(division). % isn't really determined X / 10 = 2 --> many possible values |
601 | | determined_binary_integer_function(int_minus). |
602 | | determined_binary_integer_function(int_plus). |
603 | | determined_binary_integer_function(int_power). |
604 | | determined_binary_integer_function(modulo). % isn't really determined; X mod 10 = 0 --> many possible values |
605 | | determined_binary_integer_function(times). |
606 | | |
607 | | %:- assert_must_fail((kernel_mappings:determined_binary_function(X), |
608 | | % kernel_mappings:invalid_call(X))). |
609 | | %determined_binary_function(nat_range). |
610 | | %determined_binary_function(concat_sequence). |
611 | | %determined_binary_function(prepend_sequence). |
612 | | %determined_binary_function(cartesian_product). |
613 | | |
614 | | % set up any special propagation rules which should trigger before Args1 and 2 are fully known: |
615 | | % we should probably move these rules down to kernel_objects, bsets_clp ... and validate them |
616 | | % maybe we can even store them in B format, prove them and read them in |
617 | | special_propagate_binary_function(union_wf,A,B,Res,WF) :- !, |
618 | | propagate_empty_set(Res,A,WF), % A\/B ={} => A={} |
619 | | propagate_empty_set(Res,B,WF). % A\/B ={} => B={} |
620 | | %special_propagate_binary_function(override_relation,A,B,Res,WF) :- !, % causes small slowdown for ticket 184 |
621 | | % propagate_empty_set(Res,A,WF), propagate_empty_set(Res,B). |
622 | | special_propagate_binary_function(intersection,A,B,Res,WF) :- !, |
623 | | propagate_empty_set(A,Res,WF), % A={} => A /\ B = {} |
624 | | propagate_empty_set(B,Res,WF). % B={} => A /\ B = {} |
625 | | special_propagate_binary_function(difference_set_wf,A,B,Res,WF) :- !, |
626 | | propagate_empty_set(A,Res,WF), % A={} => A \ B = {} |
627 | | propagate_empty_set_eq(B,A,Res,WF). % B={} => A \ B = A |
628 | | special_propagate_binary_function(image_wf,A,B,Res,WF) :- !, |
629 | | propagate_empty_set(B,Res,WF), % B={} => A[B] = {} |
630 | | propagate_id_eq(A,B,Res,WF). % (A={} => A[B] = {}) & (A=id => A[B] = B) |
631 | | special_propagate_binary_function(domain_restriction_wf,S,_R,Res,WF) :- !, |
632 | | propagate_empty_set(S,Res,WF). % if S ={} => S <| R = {} |
633 | | special_propagate_binary_function(domain_subtraction_wf,S,R,Res,WF) :- !, |
634 | | propagate_empty_set_eq(S,R,Res,WF). % if S ={} => S <<| R = R |
635 | | special_propagate_binary_function(range_restriction_wf,_R,S,Res,WF) :- !, |
636 | | propagate_empty_set(S,Res,WF). % if S ={} => R |> S = {} |
637 | | special_propagate_binary_function(range_subtraction_wf,R,S,Res,WF) :- !, |
638 | | propagate_empty_set_eq(S,R,Res,WF). % if S ={} => R |>> S = R |
639 | | special_propagate_binary_function(_,_,_,_,_WF). % no propagators available |
640 | | :- block propagate_empty_set(-,?,?). |
641 | | propagate_empty_set([],A,WF) :- !, |
642 | | % (A==[] -> true ; print(prop_empty(A)),nl), %% |
643 | | kernel_objects:empty_set_wf(A,WF). |
644 | | propagate_empty_set(_,_,_). |
645 | | :- block propagate_empty_set_eq(-,?,?,?). |
646 | | propagate_empty_set_eq([],A,B,WF) :- !,kernel_objects:equal_object_wf(A,B,propagate_empty_set_eq,WF). |
647 | | propagate_empty_set_eq(_,_,_,_). |
648 | | :- block propagate_id_eq(-,?,?,?). |
649 | | propagate_id_eq([],_A,B,WF) :- !,kernel_objects:empty_set_wf(B,WF). |
650 | | propagate_id_eq(closure(Par,Types,Body),A,B,WF) :- custom_explicit_sets:is_full_id_closure(Par,Types,Body), |
651 | | % print(prop_id_eq(A,B)),nl, |
652 | | !,kernel_objects:equal_object_wf(A,B,propagate_id_eq,WF). |
653 | | propagate_id_eq(_,_,_,_). |
654 | | |
655 | | binary_function(concat,bsets_clp,concat_sequence). % ^ |
656 | | binary_function(insert_front,bsets_clp,prepend_sequence). |
657 | | binary_function(insert_tail,bsets_clp,append_sequence). |
658 | | binary_function(restrict_front,bsets_clp,prefix_sequence_wf). % s /|\ n |
659 | | binary_function(restrict_tail,bsets_clp,suffix_sequence). % WF |
660 | | binary_function(union,kernel_objects,union_wf). |
661 | | binary_function(intersection,kernel_objects,intersection). |
662 | | binary_function(set_subtraction,kernel_objects,difference_set_wf). |
663 | | binary_function(cartesian_product,kernel_objects,cartesian_product). % always converted into closure |
664 | | binary_function(add,kernel_objects,int_plus). |
665 | | binary_function(multiplication,kernel_objects,times). |
666 | | binary_function(minus,kernel_objects,int_minus). |
667 | | binary_function(modulo,kernel_objects,modulo). |
668 | | binary_function(power_of,kernel_objects,int_power). |
669 | | binary_function(div,kernel_objects,division). |
670 | | binary_function(floored_div,kernel_objects,floored_division). |
671 | | %binary_function(interval,kernel_objects,nat_range). % always converted into closure, unless empty or singleton |
672 | | binary_function(image,bsets_clp,image_wf). |
673 | | %binary_function(function,apply_to). |
674 | | binary_function(domain_restriction,bsets_clp,domain_restriction_wf). |
675 | | binary_function(domain_subtraction,bsets_clp,domain_subtraction_wf). |
676 | | binary_function(range_subtraction,bsets_clp,range_subtraction_wf). |
677 | | binary_function(range_restriction,bsets_clp,range_restriction_wf). |
678 | | binary_function(overwrite,bsets_clp,override_relation). |
679 | | binary_function(composition,bsets_clp,rel_composition_wf). |
680 | | binary_function(iteration,bsets_clp,rel_iterate_wf). |
681 | | binary_function(direct_product,bsets_clp,direct_product_wf). |
682 | | binary_function(parallel_product,bsets_clp,parallel_product_wf). |
683 | | % functions below always converted into closure |
684 | | %binary_function(total_function,bsets_clp,enumerate_total_function). |
685 | | %binary_function(partial_function,bsets_clp,enumerate_partial_function). |
686 | | %binary_function(total_bijection,bsets_clp,enumerate_total_bijection). |
687 | | %binary_function(relations,bsets_clp,enumerate_relation). |
688 | | %binary_function(partial_injection,bsets_clp,enumerate_partial_injection). |
689 | | %binary_function(partial_surjection,bsets_clp,enumerate_partial_surjection). |
690 | | %binary_function(total_surjection,bsets_clp,enumerate_total_surjection). |
691 | | %binary_function(total_relation,bsets_clp,enumerate_total_relation). |
692 | | %binary_function(total_injection,bsets_clp,enumerate_total_injection). |
693 | | %binary_function(partial_bijection,bsets_clp,enumerate_partial_bijection). |
694 | | %binary_function(surjection_relation,bsets_clp,enumerate_surjection_relation). |
695 | | %binary_function(total_surjection_relation,bsets_clp,enumerate_total_surjection_relation). |
696 | | |
697 | | % check if the first argument determines the value of a binary_function: |
698 | | binary_arg1_determines_value(multiplication,A1,int(0)) :- zero(A1). |
699 | | binary_arg1_determines_value(intersection,A1,[]) :- A1==[]. |
700 | | binary_arg1_determines_value(set_subtraction,A1,[]) :- A1==[]. |
701 | | binary_arg1_determines_value(domain_restriction,A1,[]) :- A1==[]. % first arg is set |
702 | | binary_arg1_determines_value(range_subtraction,A1,[]) :- A1==[]. % first arg is rel |
703 | | binary_arg1_determines_value(range_restriction,A1,[]) :- A1==[]. % first arg is rel |
704 | | binary_arg1_determines_value(cartesian_product,A1,[]) :- A1==[]. |
705 | | binary_arg1_determines_value(composition,A1,[]) :- A1==[]. |
706 | | binary_arg1_determines_value(direct_product,A1,[]) :- A1==[]. |
707 | | binary_arg1_determines_value(parallel_product,A1,[]) :- A1==[]. |
708 | | |
709 | | |
710 | | zero(X) :- nonvar(X), X=int(X1),X1==0. |
711 | | |
712 | | /* add PartialBijection .... */ |
713 | | |
714 | | /* BOOLEAN EXPRESSIONS */ |
715 | | |
716 | | |
717 | | :- assert_must_succeed(kernel_mappings:symbolic_closure_binary_operator(partial_function)). |
718 | | :- assert_must_succeed(kernel_mappings:symbolic_closure_binary_operator(total_function)). |
719 | | |
720 | | symbolic_closure_binary_operator(Op) :- |
721 | | binary_in_boolean_type(Op,_), |
722 | | binary_not_in_boolean_type(Op,_), |
723 | | \+ not_symbolic_binary(Op). |
724 | | /* note every symbolic closure operator must be dealt with by a binary_in and |
725 | | a binary_not_in clause below, otherwise we have a problem */ |
726 | | |
727 | | %not_symbolic_binary(set_subtraction). % initially test 426 failed or runtime went from 6 to 12 secs ; now with do_not_keep_symbolic rules below it is fine and runtime is 3 secs |
728 | | %not_symbolic_binary(intersection). % seems to be ok to allow symbolic treatment |
729 | | not_symbolic_binary(range_subtraction). % important for test 1001 |
730 | | not_symbolic_binary(range_restriction). |
731 | | not_symbolic_binary(domain_subtraction). % important for test 1001 |
732 | | not_symbolic_binary(domain_restriction). |
733 | | /* interval symbolic: because we often have expressions of the form a..b where b is > MAXINT */ |
734 | | |
735 | | % return true if a symbolic closure for a binary operator would be definitely empty: |
736 | | is_definitely_empty(interval,int(A),int(B)) :- number(A),number(B), A>B. |
737 | | is_definitely_empty(cartesian_product,A,B) :- (B==[]->true ; A==[]). % A==[] actually already checked in binary_arg1_determines_value |
738 | | is_definitely_empty(parallel_product,A,B) :- (A==[]->true ; B==[]). |
739 | | is_definitely_empty(total_relation,A,B) :- B==[], definitely_not_empty(A). |
740 | | is_definitely_empty(total_function,A,B) :- B==[], definitely_not_empty(A). % {} --> {} = {{}} |
741 | | is_definitely_empty(total_injection,A,B) :- B==[], definitely_not_empty(A). |
742 | | is_definitely_empty(total_surjection,A,B) :- B==[], definitely_not_empty(A). |
743 | | is_definitely_empty(total_bijection,A,B) :- B==[], definitely_not_empty(A). |
744 | | is_definitely_empty(intersection,A,B) :- (A==[] ; B==[]). |
745 | | is_definitely_empty(set_subtraction,A,B) :- |
746 | | (A==[] ; nonvar(B), custom_explicit_sets:is_definitely_maximal_set(B)). |
747 | | |
748 | | :- use_module(kernel_freetypes,[is_non_empty_freetype/1]). |
749 | | definitely_not_empty(X) :- nonvar(X), definitely_not_empty_aux(X). |
750 | | definitely_not_empty_aux([_|_]). |
751 | | definitely_not_empty_aux(avl_set(_)). |
752 | | definitely_not_empty_aux(global_set(_)). |
753 | | definitely_not_empty_aux(freetype(ID)) :- is_non_empty_freetype(ID). |
754 | | |
755 | | % check if it is worthwhile keeping a binary operator symbolic, if so: return value |
756 | | do_not_keep_symbolic(cartesian_product,Set1,Set2,Res,_WF) :- %print(cart(Set1,Set2)),nl, |
757 | | (singleton_set(Set1,_) -> small_known_set(Set2) |
758 | | ; singleton_set(Set2,_) -> small_known_set(Set1) |
759 | | ), |
760 | | kernel_objects:cartesian_product(Set1,Set2,Res). |
761 | | do_not_keep_symbolic(interval,int(A),int(B),Res,_WF) :- |
762 | | ((number(A),number(B),A=B) % or B-A < some limit |
763 | | -> custom_explicit_sets:convert_to_avl([int(A)],Res)). |
764 | | do_not_keep_symbolic(parallel_product,Rel1,Rel2,Res,WF) :- |
765 | | not_closure(Rel1), not_closure(Rel2), |
766 | | bsets_clp:parallel_product_wf(Rel1,Rel2,Res,WF). |
767 | | do_not_keep_symbolic(intersection,Set1,Set2,_Res,_WF) :- nonvar(Set1), nonvar(Set2), |
768 | | % only keep symbolic if at least one non-interval closure |
769 | | nonvar_non_interval_closure(Set1,Set2), |
770 | | (nonvar_non_interval_closure(Set1) -> |
771 | | \+ small_known_set(Set2) % intersection with singleton set can always be computed |
772 | | ; nonvar_non_interval_closure(Set2) -> \+ small_known_set(Set1)), |
773 | | !, |
774 | | %% print(symbolic_intersection),nl, translate:print_bvalue(Set1),nl, translate:print_bvalue(Set2),nl,nl, %% |
775 | | fail. |
776 | | do_not_keep_symbolic(intersection,Set1,Set2,Res,WF) :- % otherwise: compute intersection normally |
777 | | Call=kernel_objects:intersection(Set1,Set2,Res,WF), |
778 | | must_succ_kernel_call(Call,[Set1,Set2],WF,Call). |
779 | | do_not_keep_symbolic(set_subtraction,Set1,Set2,Res,_WF) :- Set2 == [],!, |
780 | | Res = Set1. |
781 | | do_not_keep_symbolic(set_subtraction,Set1,Set2,_Res,_WF) :- nonvar(Set1), |
782 | | % only keep symbolic if at least one non-interval closure |
783 | | nonvar_non_interval_closure(Set1,Set2), |
784 | | % check if we cannot construct a complement closure: |
785 | ? | \+ can_construct_complement_closure(Set1,Set2), |
786 | | \+ small_known_set(Set1), |
787 | | !, |
788 | | %% nl,print(symbolic_set_subtr(Set1,Set2)),nl,nl, %% |
789 | | fail. |
790 | | do_not_keep_symbolic(set_subtraction,Set1,Set2,Res,WF) :- % otherwise: compute difference normally |
791 | | Call=kernel_objects:difference_set_wf(Set1,Set2,Res,WF), % print(diff_set(Set1,Set2,Res)),nl, |
792 | | must_succ_kernel_call(Call,[Set1,Set2],WF,Call). |
793 | | |
794 | | % should succeed if we do not want to keep a unary operator symbolic |
795 | | do_not_keep_symbolic_unary(_,ArgValue) :- ArgValue==[],!. |
796 | | do_not_keep_symbolic_unary(closure,Set1) :- % this is closure1 |
797 | | very_small_known_set(Set1). |
798 | | |
799 | | |
800 | | can_construct_complement_closure(Set1,Set2) :- |
801 | ? | nonvar(Set1), nonvar(Set2), Set2 = avl_set(_), |
802 | ? | custom_explicit_sets:is_very_large_maximal_global_set(Set1,_). |
803 | | |
804 | | nonvar_non_interval_closure(A,B) :- (nonvar_non_interval_closure(A) -> true ; nonvar_non_interval_closure(B)). |
805 | | nonvar_non_interval_closure(A) :- nonvar(A), A=closure(_,_,_), |
806 | | \+ custom_explicit_sets:is_interval_closure_or_integerset(A,_,_), |
807 | | \+ custom_explicit_sets:is_not_member_value_closure(A,_Type,_MS2). % there isn't full support for this for intersection yet ! TODO fix |
808 | | |
809 | | |
810 | | :- use_module(custom_explicit_sets,[quick_custom_explicit_set_approximate_size/2]). |
811 | | small_known_set(AVL) :- nonvar(AVL), AVL=avl_set(A), |
812 | | quick_custom_explicit_set_approximate_size(avl_set(A),Size), |
813 | | %print(size(Size)),nl, |
814 | | Size < 150. |
815 | | very_small_known_set(AVL) :- nonvar(AVL), AVL=avl_set(A), |
816 | | quick_custom_explicit_set_approximate_size(avl_set(A),Size), |
817 | | %print(size(Size)),nl, |
818 | | Size < 50. |
819 | | |
820 | | not_closure(X) :- nonvar(X), \+ functor(X,closure,3). %X \= closure(_,_,_). |
821 | | |
822 | | % explicit_set([]). explicit_set([_|_]). explicit_set(avl_set(_)). |
823 | | |
824 | | :- assert_must_fail((kernel_mappings:binary_in_boolean_type(Op,_), |
825 | | \+(kernel_mappings:binary_not_in_boolean_type(Op,_)))). |
826 | | :- assert_must_fail((kernel_mappings:binary_not_in_boolean_type(Op,_), |
827 | | \+(kernel_mappings:binary_in_boolean_type(Op,_)))). |
828 | | :- assert_must_fail((kernel_mappings:binary_in_boolean_type(Op,_), \+(kernel_mappings:binary_function(Op,_,_)), |
829 | | kernel_mappings:not_symbolic_binary(Op) )). |
830 | | |
831 | | binary_in_boolean_type(partial_function,bsets_clp:partial_function_wf). |
832 | | binary_in_boolean_type(total_function,bsets_clp:total_function_wf). |
833 | | binary_in_boolean_type(cartesian_product,kernel_objects:is_cartesian_pair_wf). |
834 | | binary_in_boolean_type(partial_surjection,bsets_clp:partial_surjection_wf). |
835 | | binary_in_boolean_type(partial_injection,bsets_clp:partial_injection_wf). |
836 | | binary_in_boolean_type(total_injection,bsets_clp:total_injection_wf). % >-> |
837 | | binary_in_boolean_type(partial_bijection,bsets_clp:partial_bijection_wf). |
838 | | binary_in_boolean_type(total_surjection,bsets_clp:total_surjection_wf). % -->> |
839 | | binary_in_boolean_type(total_bijection,bsets_clp:total_bijection_wf). % >->> |
840 | | binary_in_boolean_type(relations,bsets_clp:relation_over_wf). |
841 | | binary_in_boolean_type(total_relation,bsets_clp:total_relation_wf). |
842 | | binary_in_boolean_type(surjection_relation,bsets_clp:surjection_relation_wf). |
843 | | binary_in_boolean_type(total_surjection_relation,bsets_clp:total_surjection_relation_wf). |
844 | | binary_in_boolean_type(interval,kernel_objects:in_nat_range_wf). |
845 | | binary_in_boolean_type(parallel_product,bsets_clp:in_parallel_product_wf). |
846 | | binary_in_boolean_type(set_subtraction,kernel_objects:in_difference_set_wf). |
847 | | binary_in_boolean_type(intersection,kernel_objects:in_intersection_set_wf). |
848 | | %binary_in_boolean_type(union,bsets_clp:in_union_set_wf). % makes some CBC checks fail; TO DO: investigate |
849 | | binary_in_boolean_type(range_subtraction,bsets_clp:in_range_subtraction_wf). |
850 | | binary_in_boolean_type(range_restriction,bsets_clp:in_range_restriction_wf). |
851 | | binary_in_boolean_type(domain_subtraction,bsets_clp:in_domain_subtraction_wf). |
852 | | binary_in_boolean_type(domain_restriction,bsets_clp:in_domain_restriction_wf). |
853 | | %binary_function(overwrite,bsets_clp,in_override_relation). % TO DO: add this, for a more principled symbolic treatment (see test 1491) |
854 | | |
855 | | % check whether a binary operator is definitely true; irrespective of arguments |
856 | | binary_in_definitely_true(BOP,ValueOfEl) :- nonvar(ValueOfEl), |
857 | | binary_definitely_true_based_on_element_value(BOP,ValueOfEl). |
858 | | |
859 | | binary_definitely_true_based_on_element_value(partial_function,[]). % {} : A +-> B |
860 | | binary_definitely_true_based_on_element_value(partial_injection,[]). % {} : A >+> B |
861 | | binary_definitely_true_based_on_element_value(relations,[]). % {} : A <-> B |
862 | | |
863 | | % all make use of WF now: |
864 | | binary_not_in_boolean_type(interval,kernel_objects:not_in_nat_range_wf). |
865 | | binary_not_in_boolean_type(partial_function,bsets_clp:not_partial_function). |
866 | | binary_not_in_boolean_type(partial_surjection,bsets_clp:not_partial_surjection_wf). |
867 | | binary_not_in_boolean_type(total_surjection,bsets_clp:not_total_surjection_wf). |
868 | | binary_not_in_boolean_type(partial_injection,bsets_clp:not_partial_injection). |
869 | | binary_not_in_boolean_type(total_injection,bsets_clp:not_total_injection). |
870 | | binary_not_in_boolean_type(partial_bijection,bsets_clp:not_partial_bijection). |
871 | | binary_not_in_boolean_type(cartesian_product,kernel_objects:not_is_cartesian_pair). |
872 | | binary_not_in_boolean_type(relations,bsets_clp:not_relation_over). |
873 | | binary_not_in_boolean_type(total_function,bsets_clp:not_total_function). |
874 | | binary_not_in_boolean_type(total_bijection,bsets_clp:not_total_bijection). |
875 | | binary_not_in_boolean_type(total_relation,bsets_clp:not_total_relation_wf). |
876 | | binary_not_in_boolean_type(surjection_relation,bsets_clp:not_surjection_relation_wf). |
877 | | binary_not_in_boolean_type(total_surjection_relation,bsets_clp:not_total_surjection_relation_wf). |
878 | | binary_not_in_boolean_type(parallel_product,bsets_clp:not_in_parallel_product_wf). |
879 | | binary_not_in_boolean_type(set_subtraction,kernel_objects:not_in_difference_set_wf). |
880 | | binary_not_in_boolean_type(intersection,kernel_objects:not_in_intersection_set_wf). |
881 | | %binary_not_in_boolean_type(union,bsets_clp:not_in_union_set_wf). |
882 | | binary_not_in_boolean_type(range_subtraction,bsets_clp:not_in_range_subtraction_wf). |
883 | | binary_not_in_boolean_type(range_restriction,bsets_clp:not_in_range_restriction_wf). |
884 | | binary_not_in_boolean_type(domain_subtraction,bsets_clp:not_in_domain_subtraction_wf). |
885 | | binary_not_in_boolean_type(domain_restriction,bsets_clp:not_in_domain_restriction_wf). |
886 | | |
887 | | |
888 | | |
889 | | symbolic_closure_unary_operator(Op) :- |
890 | | (unary_in_boolean_type(Op,_)), |
891 | | unary_not_in_boolean_type(Op,_), |
892 | | \+ not_symbolic_unary(Op). |
893 | | |
894 | | not_symbolic_unary(domain). |
895 | | %not_symbolic_unary(identity). % for Siemens Models |
896 | | |
897 | | :- assert_must_fail((kernel_mappings:unary_in_boolean_type(Op,_), |
898 | | \+(kernel_mappings:unary_not_in_boolean_type(Op,_)))). |
899 | | /* note every symbolic closure operator must be dealt with by a unary_in and |
900 | | a unary_not_in clause below, otherwise we have a problem */ |
901 | | :- assert_must_fail((kernel_mappings:unary_in_boolean_type(UnOp,_), |
902 | | \+ kernel_mappings:symbolic_closure_unary_operator(UnOp), |
903 | | \+ kernel_mappings:unary_function(UnOp,_,_) )). |
904 | | |
905 | | |
906 | | /* a waitflags version is available for these taking one extra argument (the waitflags): */ |
907 | | unary_in_boolean_type(pow_subset,kernel_objects:check_subset_of_wf). |
908 | | unary_in_boolean_type(fin_subset,kernel_objects:check_finite_subset_of_wf). |
909 | | unary_in_boolean_type(pow1_subset,kernel_objects:check_non_empty_subset_of_wf). |
910 | | unary_in_boolean_type(fin1_subset,kernel_objects:check_finite_non_empty_subset_of_wf). |
911 | | unary_in_boolean_type(struct,kernel_records:is_a_record_wf). |
912 | | unary_in_boolean_type(seq,bsets_clp:is_sequence_wf). /* last arg: basic type */ |
913 | | unary_in_boolean_type(iseq,bsets_clp:injective_sequence_wf). |
914 | | unary_in_boolean_type(perm,bsets_clp:permutation_sequence_wf). |
915 | | unary_in_boolean_type(domain, bsets_clp:in_domain_wf). |
916 | | unary_in_boolean_type(seq1,bsets_clp:finite_non_empty_sequence). |
917 | | unary_in_boolean_type(iseq1,bsets_clp:injective_non_empty_sequence). |
918 | | unary_in_boolean_type(identity,bsets_clp:in_identity). |
919 | | unary_in_boolean_type(closure,bsets_clp:in_closure1_wf). %element_of_closure1_wf). % this is closure1 |
920 | | %unary_in_boolean_type(reflexive_closure,bsets_clp:element_of_reflexive_closure_wf). % this is closure |
921 | | % we could add : inverse?, general_concat, .... ? range: in_range_wf |
922 | | |
923 | | |
924 | | % check whether a unary operator is definitely true; irrespective of arguments |
925 | | unary_in_definitely_true(BOP,ValueOfEl) :- nonvar(ValueOfEl), |
926 | | unary_definitely_true_based_on_element_value(BOP,ValueOfEl). |
927 | | |
928 | | unary_definitely_true_based_on_element_value(pow_subset,[]). |
929 | | unary_definitely_true_based_on_element_value(fin_subset,[]). |
930 | | unary_definitely_true_based_on_element_value(seq,[]). |
931 | | unary_definitely_true_based_on_element_value(iseq,[]). |
932 | | |
933 | | unary_not_in_boolean_type(domain, bsets_clp:not_in_domain_wf). |
934 | | unary_not_in_boolean_type(iseq,bsets_clp:not_injective_sequence). |
935 | | unary_not_in_boolean_type(struct,kernel_records:not_is_a_record_wf). |
936 | | unary_not_in_boolean_type(pow_subset,kernel_objects:not_subset_of_wf). |
937 | | unary_not_in_boolean_type(pow1_subset,kernel_objects:not_non_empty_subset_of_wf). |
938 | | unary_not_in_boolean_type(fin_subset,kernel_objects:not_finite_subset_of_wf). |
939 | | unary_not_in_boolean_type(fin1_subset,kernel_objects:not_non_empty_finite_subset_of_wf). |
940 | | unary_not_in_boolean_type(seq,bsets_clp:not_is_sequence_wf). |
941 | | unary_not_in_boolean_type(seq1,bsets_clp:not_is_non_empty_sequence_wf). |
942 | | unary_not_in_boolean_type(iseq1,bsets_clp:not_non_empty_injective_sequence). |
943 | | unary_not_in_boolean_type(perm,bsets_clp:not_permutation_sequence). |
944 | | unary_not_in_boolean_type(identity,bsets_clp:not_in_identity). |
945 | | unary_not_in_boolean_type(closure,bsets_clp:not_in_closure1_wf). %not_element_of_closure1_wf). % this is closure1 |
946 | | %unary_not_in_boolean_type(reflexive_closure,bsets_clp:not_element_of_reflexive_closure_wf). |
947 | | |
948 | | |
949 | | :- assert_must_fail(( kernel_mappings:cst_in_boolean_type(X,_), |
950 | | \+ kernel_mappings:cst_not_in_boolean_type(X,_) )). |
951 | | :- assert_must_fail(( kernel_mappings:cst_not_in_boolean_type(X,_), |
952 | | \+ kernel_mappings:cst_in_boolean_type(X,_) )). |
953 | | |
954 | | cst_in_boolean_type(string_set,kernel_objects:is_string). |
955 | | cst_in_boolean_type(integer_set(IntSet),Call) :- integerset_in_boolean_type(IntSet,Call). |
956 | | |
957 | | |
958 | | :- assert_must_fail(( kernel_mappings:integerset_in_boolean_type(X,_), |
959 | | \+ kernel_mappings:integerset_not_in_boolean_type(X,_) )). |
960 | | :- assert_must_fail(( kernel_mappings:integerset_not_in_boolean_type(X,_), |
961 | | \+ kernel_mappings:integerset_in_boolean_type(X,_) )). |
962 | | |
963 | | integerset_in_boolean_type('INTEGER',kernel_objects:is_integer). |
964 | | integerset_in_boolean_type('NATURAL',kernel_objects:is_natural). |
965 | | integerset_in_boolean_type('NATURAL1',kernel_objects:is_natural1). |
966 | | integerset_in_boolean_type('INT',kernel_objects:is_implementable_int). |
967 | | integerset_in_boolean_type('NAT',kernel_objects:is_implementable_nat). |
968 | | integerset_in_boolean_type('NAT1',kernel_objects:is_implementable_nat1). |
969 | | |
970 | | cst_not_in_boolean_type(string_set,kernel_objects:is_not_string). |
971 | | cst_not_in_boolean_type(integer_set(IntSet),Call) :- integerset_not_in_boolean_type(IntSet,Call). |
972 | | |
973 | | integerset_not_in_boolean_type('INTEGER',kernel_objects:is_not_integer). |
974 | | integerset_not_in_boolean_type('NATURAL',kernel_objects:is_not_natural). |
975 | | integerset_not_in_boolean_type('NATURAL1',kernel_objects:is_not_natural1). |
976 | | integerset_not_in_boolean_type('INT',kernel_objects:is_not_implementable_int). |
977 | | integerset_not_in_boolean_type('NAT',kernel_objects:is_not_implementable_nat). |
978 | | integerset_not_in_boolean_type('NAT1',kernel_objects:is_not_implementable_nat1). |
979 | | |
980 | | % binary_boolean_operator(B-AST-NAME, Module:Predicate, WF_ENABLED) |
981 | | %binary_boolean_operator(member,kernel_objects:element_of). /* not really used: interpreter deals with In explicitly */ |
982 | | %binary_boolean_operator(not_member,kernel_objects:not_element_of_wf,yes). /* not really used: interpreter deals with In explicitly */ |
983 | | binary_boolean_operator(not_equal,kernel_objects:not_equal_object_wf,yes). |
984 | | binary_boolean_operator(equal,kernel_objects:equal_object_optimized,no). |
985 | | binary_boolean_operator(less,kernel_objects:less_than,no). |
986 | | binary_boolean_operator(less_equal,kernel_objects:less_than_equal,no). |
987 | | binary_boolean_operator(greater,kernel_objects:greater_than,no). |
988 | | binary_boolean_operator(greater_equal,kernel_objects:greater_than_equal,no). |
989 | | binary_boolean_operator(subset,kernel_objects:check_subset_of_wf,yes). |
990 | | binary_boolean_operator(subset_strict,kernel_objects:strict_subset_of_wf,yes). |
991 | | binary_boolean_operator(not_subset_strict,kernel_objects:not_strict_subset_of_wf,yes). |
992 | | binary_boolean_operator(not_subset,kernel_objects:not_subset_of_wf,yes). |
993 | | |
994 | | :- assert_must_fail(( kernel_mappings:binary_boolean_operator(X,_,_), |
995 | | \+ kernel_mappings:negate_binary_boolean_operator(X,_) )). |
996 | | :- assert_must_fail(( kernel_mappings:binary_boolean_operator(X,_,_), |
997 | | kernel_mappings:negate_binary_boolean_operator(X,Y), Y=X )). |
998 | | :- assert_must_fail(( kernel_mappings:negate_binary_boolean_operator(X,X) )). |
999 | | |
1000 | | negate_binary_boolean_operator(X,Y) :- |
1001 | | ( negate_binary_boolean_operator2(X,Y) -> true |
1002 | | ; negate_binary_boolean_operator2(Y,X)). |
1003 | | negate_binary_boolean_operator2(member,not_member). |
1004 | | negate_binary_boolean_operator2(subset,not_subset). |
1005 | | negate_binary_boolean_operator2(subset_strict,not_subset_strict). |
1006 | | |
1007 | | negate_binary_boolean_operator2(equal,not_equal). |
1008 | | negate_binary_boolean_operator2(less,greater_equal). |
1009 | | negate_binary_boolean_operator2(less_equal,greater). |
1010 | | |
1011 | | |
1012 | | |
1013 | | |
1014 | | % input must be list of sets -> second argument set to true if all but one set is known |
1015 | | :- block all_but_one_set_known(-,?). |
1016 | | all_but_one_set_known([],true). |
1017 | | all_but_one_set_known([H|T],KNOWN) :- |
1018 | | (T==[] -> KNOWN=true |
1019 | | ; all_but_one(T,H,KNOWN)). |
1020 | | :- block all_but_one(-,?,?). |
1021 | | all_but_one([],_H,true). |
1022 | | all_but_one([H2|T],H1,KNOWN) :- known_value(H2,K2), known_value(H1,K1), all_but_one_wait(K1,K2,T,KNOWN). |
1023 | | |
1024 | | :- block all_but_one_wait(-,-,?,?), all_but_one_wait(?,?,-,?). |
1025 | | all_but_one_wait(K1,K2,[],true) :- K1=true,K2=true. |
1026 | | all_but_one_wait(K1,K2,[H3|T],KNOWN) :- known_value(H3,K3), |
1027 | | (var(K2) -> all_but_one_wait(K2,K3,T,KNOWN) ; all_but_one_wait(K1,K3,T,KNOWN)). |
1028 | | |
1029 | | :- block known_value(-,-). |
1030 | | known_value(_,T) :- T==true,!. |
1031 | | known_value(int(X),K) :- !, known_atomic(X,K). |
1032 | | known_value(pred_true /* bool_true */,K) :- !, K=true. |
1033 | | known_value(pred_false /* bool_false */,K) :- !, K=true. |
1034 | | known_value(string(X),K) :- !, known_atomic(X,K). |
1035 | | known_value([],K) :- !, K=true. |
1036 | | known_value(avl_set(_A),K) :- !, K=true. |
1037 | | known_value(global_set(X),K) :- !,known_atomic(X,K). |
1038 | | known_value(freetype(X),K) :- !,known_atomic(X,K). |
1039 | | known_value(A,K) :- when(ground(A),K=true). |
1040 | | |
1041 | | :- block known_atomic(-,?). |
1042 | | known_atomic(_,true). |
1043 | | |
1044 | | |
1045 | | % some code to automatically generate documentation for kernel predicates: |
1046 | | kernel_predicate(M,P,expression,1,BAST,BOP,WF) :- |
1047 | | unary_function(BAST,M,P), get_waitflag_info(P,WF), |
1048 | | (translate:unary_prefix(BAST,BOP,_) -> true |
1049 | | ; translate:unary_postfix(BAST,BOP,_) -> true |
1050 | | ; translate:function_like(BAST,BOP) -> true |
1051 | | ; BOP = '??'). |
1052 | | kernel_predicate(M,P,expression,2,BAST,BOP,WF) :- |
1053 | | binary_function(BAST,M,P), get_waitflag_info(P,WF), |
1054 | | (translate:binary_infix(BAST,BOP,_,_) -> true |
1055 | | ; translate:function_like(BAST,BOP) -> true ; BOP = '??'). |
1056 | | kernel_predicate(M,P,predicate,2,BAST,BOP,WF) :- |
1057 | | binary_boolean_operator(BAST,M:P,WF), |
1058 | | (translate:binary_infix(BAST,BOP,_,_) -> true |
1059 | | ; translate:function_like(BAST,BOP) -> true ; BOP = '??'). |
1060 | | |
1061 | | get_waitflag_info(P,WF) :- |
1062 | | (expects_waitflag_and_span(P) -> WF = wf_span ; |
1063 | | expects_waitflag_and_span(P) -> WF = yes ; |
1064 | | WF = no). |
1065 | | :- public generate_documentation/0. |
1066 | | generate_documentation :- |
1067 | | kernel_predicate(M,P,_T,ARITY,BAST,BOP,_WF), |
1068 | | ( symbolic_closure_unary_operator(BOP) -> Sym=' (symbolic_unary)' |
1069 | | ; symbolic_closure_binary_operator(BOP) -> Sym=' (symbolic_binary)' % these not printed as binary_function does not include them |
1070 | | ; Sym= ''), |
1071 | | format(' ~w (~w/~w) --> ~w:~w ~w~n',[BOP,BAST,ARITY,M,P,Sym]), |
1072 | | fail. |
1073 | | generate_documentation. |
1074 | | |
1075 | | :- assert_must_succeed(kernel_mappings:generate_documentation). |
1076 | | |