1 % (c) 2012-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 :- module(external_functions,[call_external_function/7, call_external_predicate/8,
6 call_external_substitution/6,
7 reset_external_functions/0,
8 print_external_function_profile/0,
9 external_pred_always_true/1,
10 reset_side_effect_occurred/0,
11 side_effect_occurred/1,
12 performs_io/1, not_declarative/1,
13 is_external_function_name/1,
14 get_external_function_type/3, % version with types with Prolog variables
15 external_fun_type/3,
16 external_subst_enabling_condition/3,
17 external_fun_has_wd_condition/1,
18 external_fun_can_be_inverted/1,
19 do_not_evaluate_args/1,
20 reset_argv/0, set_argv_from_list/1, set_argv_from_atom/1,
21
22 observe_parameters/2, observe_state/1, observe_value/2
23 ]).
24
25 % Note: there is also the predicate external_procedure_used/1 in bmachine_construction
26
27 :- use_module(error_manager).
28 :- use_module(self_check).
29 :- use_module(library(avl)).
30 :- use_module(library(lists)).
31 :- use_module(translate).
32
33 % TO DO: add external Prolog files
34 % Should we do auto-conversion of B to Prolog types ,... ?
35
36 :- use_module(kernel_waitflags).
37 :- use_module(debug).
38 :- use_module(bsyntaxtree).
39
40 :- use_module(module_information,[module_info/2]).
41 :- module_info(group,external_functions).
42 :- module_info(description,'This module provides a way to call external functions and predicates.').
43
44 :- set_prolog_flag(double_quotes, codes).
45
46 :- dynamic side_effect_occurred/1.
47 % TRUE if a side effect has occured
48 % possible values (user_output, file)
49 reset_side_effect_occurred :- (retract(side_effect_occurred(_)) -> retractall(side_effect_occurred(_)) ; true).
50 assert_side_effect_occurred(Location) :-
51 (side_effect_occurred(Location) -> true ; assertz(side_effect_occurred(Location))).
52
53 :- discontiguous expects_waitflag/1.
54 :- discontiguous expects_spaninfo/1.
55 :- discontiguous expects_type/1. % only used for external functions, not predicates or subst
56 :- discontiguous performs_io/1.
57 :- discontiguous is_not_declarative/1. % does not perform io but is still not declarative
58 :- discontiguous does_not_modify_state/1.
59 :- discontiguous expects_unevaluated_args/1.
60 :- discontiguous do_not_evaluate_args/1. % currently only used for external predicates, not for functions
61 :- discontiguous expects_state/1. % currently only used for external predicates
62 :- discontiguous external_pred_always_true/1. % external predicates which are always true
63 :- discontiguous external_subst_enabling_condition/3. % external predicates which are always true
64 :- discontiguous external_fun_has_wd_condition/1.
65 :- discontiguous external_fun_can_be_inverted/1.
66 :- discontiguous external_fun_type/3. % external_fun_type(FUN,ListOfTypeParameters,ListOfArgTypes); also applicable to external predicates
67
68 :- meta_predicate safe_call(0,-,-).
69 :- meta_predicate safe_call(0,-).
70
71 :- meta_predicate observe_ground(-,-,-,-,-,0).
72
73 not_declarative(FunName) :- if(performs_io(FunName),true,is_not_declarative(FunName)).
74
75 is_external_function_name(Name) :- if(external_fun_type(Name,_,_),true,
76 if(expects_waitflag(Name),true,
77 if(expects_spaninfo(Name),true,
78 if(external_subst_enabling_condition(Name,_,_),true,
79 if(not_declarative(Name),true,
80 if(expects_unevaluated_args(Name),true,fail)
81 ))))).
82
83
84 :- use_module(state_space,[current_state_id/1, get_current_context_state/1]).
85 % no longer used :- dynamic current_state_id_for_external_fun/1.
86 % some external functions access the current state; here we can set a particular state, without changing the animator/state_space
87 % useful, e.g., when exporting a VisB HTML trace when the JSON glue file uses ENABLED
88 % TODO: some commands also access the history;
89
90 get_current_state_id(ID) :-
91 (state_space:get_current_context_state(CID) -> ID=CID
92 ; current_state_id(ID)).
93
94 :- assert_must_succeed(( external_functions:call_external_function('COS',[b(integer(0),integer,[])],
95 [int(0)],int(100),integer,unknown,_WF) )).
96 :- assert_must_succeed(( external_functions:call_external_function('SIN',[b(integer(0),integer,[])],
97 [int(0)],int(0),integer,unknown,_WF) )).
98 % first a few hard-wired external functions for efficiency:
99 call_external_function('COS',_,[X],Value,_,_,_WF) :- !, 'COS'(X,Value). % already use safe_is
100 call_external_function('SIN',_,[X],Value,_,_,_WF) :- !, 'SIN'(X,Value).
101 call_external_function('TAN',_,[X],Value,_,_,_WF) :- !, 'TAN'(X,Value).
102 %call_external_function('STRING_APPEND',_,[A,B],Value,_,_,WF) :- !, 'STRING_APPEND'(A,B,Value,WF). % do we need safe_call?
103 %call_external_function('STRING_LENGTH',_,[A],Value,_,_,_WF) :- !, 'STRING_LENGTH'(A,Value).
104 % now the generic case:
105 call_external_function(F,Args,EvaluatedArgs,Value,Type,SpanInfo,WF) :-
106 (expects_waitflag(F)
107 -> E1=[WF],
108 (expects_spaninfo(F) -> E2=[SpanInfo|E1] ; E2=E1)
109 ; E1=[],
110 (expects_spaninfo(F) -> add_call_stack_to_span(SpanInfo,WF,S2), E2=[S2|E1] ; E2=E1)
111 ),
112 (expects_unevaluated_args(F) -> E3=[Args|E2] ; E3=E2),
113 (expects_type(F) -> E4=[Type|E3] ; E4=E3),
114 append(EvaluatedArgs,[Value|E4],AV),
115 % Check if there is better way to do this
116 Call =.. [F|AV],
117 % print('EXTERNAL FUNCTION CALL: '), print(F), print(' '), print(Call),nl,
118 safe_call(Call,SpanInfo,WF)
119 %, print(result(Value)),nl.
120 .
121
122 call_external_predicate(F,Args,EvaluatedArgs,LocalState,State,PREDRES,SpanInfo,WF) :-
123 (expects_waitflag(F)
124 -> E1=[WF],
125 (expects_spaninfo(F) -> E2=[SpanInfo|E1] ; E2=E1)
126 ; E1=[],
127 (expects_spaninfo(F) -> add_call_stack_to_span(SpanInfo,WF,S2), E2=[S2|E1] ; E2=E1)
128 ),
129 (expects_unevaluated_args(F) -> E3=[Args|E2] ; E3=E2),
130 (expects_state(F) -> E4=[LocalState,State|E3] ; E4=E3),
131 append(EvaluatedArgs,[PREDRES|E4],AV),
132 Call =.. [F|AV],
133 % print('EXTERNAL PREDICATE CALL: '), print(Call),nl, %%
134 safe_call(Call,SpanInfo,WF).
135
136 call_external_substitution(FunName,Args,InState,OutState,Info,WF) :-
137 % TO DO: signal if substitution can be backtracked
138 get_wait_flag_for_subst(FunName,WF,Flag),
139 (does_not_modify_state(FunName) -> OutState=[] ; OutState = OutState2),
140 call_external_substitution2(Flag,FunName,Args,InState,OutState2,Info,WF).
141
142 get_wait_flag_for_subst(FunName,WF,Flag) :- perform_directly(FunName),!,
143 get_wait_flag1(WF,Flag). % ensure that precondition, ... have been evaluated
144 get_wait_flag_for_subst(FunName,WF,Flag) :- performs_io(FunName),!,
145 get_enumeration_finished_wait_flag(WF,Flag). % ensure that precondition, ... have been evaluated
146 % get_enumeration_starting_wait_flag(external(FunName),WF,Flag).
147 get_wait_flag_for_subst(FunName,WF,Flag) :- get_binary_choice_wait_flag(external(FunName),WF,Flag).
148
149 :- block call_external_substitution2(-,?,?,?,?,?,?).
150 call_external_substitution2(_,F,Args,InState,OutState,SpanInfo,WF) :-
151 (expects_waitflag(F) -> E1=[WF] ; E1=[]),
152 (expects_spaninfo(F) -> E2=[SpanInfo|E1] ; E2=E1),
153 append(Args,[InState,OutState|E2],AV),
154 Call =.. [F|AV],
155 % print('EXTERNAL SUBSTITUTION CALL: '), print(Call),nl, %%
156 safe_call(Call,SpanInfo,WF).
157
158 safe_call(X,SpanInfo) :- safe_call(X,SpanInfo,no_wf_available).
159 safe_call(X,SpanInfo,WF) :-
160 catch(call(X), Exception, add_exception_error(Exception,X,SpanInfo,WF)).
161
162 safe_is(Context,X,Y,Span) :- safe_is(Context,X,Y,Span,no_wf_available).
163 safe_is(Context,X,Y,Span,WF) :- % print(safe_is(Context,X,Y)),nl,
164 catch(X is Y, Exception, add_exception_error(Exception,Context,Span,WF)). %, print(res(X)),nl.
165
166 add_exception_error(Exception,Context,Span,WF) :-
167 get_function_call_info(Context,SimplifiedContext),
168 add_exception_error2(Exception,SimplifiedContext,Span,WF),
169 (debug:debug_mode(on) -> tools_printing:print_term_summary(Context),nl ; true).
170
171 get_function_call_info(external_functions:X,Func) :- nonvar(X),!,functor(X,Func,_Arity).
172 get_function_call_info(M:X,M:Func) :- nonvar(X),!,functor(X,Func,_Arity).
173 get_function_call_info(X,X).
174
175 :- use_module(kernel_waitflags,[add_error_wf/5, add_warning_wf/5,add_wd_error_span/4]).
176 add_exception_error2(error(existence_error(procedure,external_functions:FUN),_),_X,SpanInfo,WF) :- !,
177 add_error_wf(external_functions,
178 'EXTERNAL function does not exist (check that you have an up-to-date version of ProB):',FUN,SpanInfo,WF),
179 fail.
180 add_exception_error2(error(existence_error(procedure,MODULE:FUN),_),_X,SpanInfo,WF) :- !,
181 add_error_wf(external_functions,'Predicate called by EXTERNAL function does not exist:',MODULE:FUN,SpanInfo,WF),
182 fail.
183 add_exception_error2(error(undefined,ERR),X,SpanInfo,WF) :-
184 is_error(ERR,ExprTerm),!,
185 ajoin(['Arithmetic operation ',X,' not defined:'],Msg),
186 add_error_wf(external_functions,Msg,ExprTerm,SpanInfo,WF),
187 fail.
188 add_exception_error2(error(evaluation_error(undefined),ERR),X,SpanInfo,WF) :-
189 is_error(ERR,ExprTerm),!,
190 ajoin(['Arithmetic operation ',X,' not defined for given argument(s):'],Msg),
191 add_wd_error_span(Msg,ExprTerm,SpanInfo,WF).
192 add_exception_error2(error(evaluation_error(zero_divisor),ERR),X,SpanInfo,WF) :-
193 is_error(ERR,_),!,
194 % TO DO: use add_wd_error_set_result:
195 add_wd_error_span('Division by 0 in arithmetic operation: ',X,SpanInfo,WF).
196 add_exception_error2(error(existence_error(source_sink,File),_),X,SpanInfo,WF) :- !,
197 add_error_wf(external_functions,'File does not exist (calling external function):',File:X,SpanInfo,WF),
198 fail.
199 add_exception_error2(error(consistency_error(Msg,_,format_arguments),_),_X,SpanInfo,WF) :- !,
200 add_error_wf(external_functions,'Illegal format string (see SICStus Prolog reference manual for syntax):',Msg,SpanInfo,WF),
201 fail.
202 add_exception_error2(enumeration_warning(A,B,C,D,E),X,SpanInfo,WF) :-
203 Exception = enumeration_warning(A,B,C,D,E),!,
204 debug_println(20,Exception),
205 get_predicate_name(X,Pred),
206 add_warning_wf(external_functions,'Enumeration warning occured while calling external function: ',Pred,SpanInfo,WF),
207 % or should we just print a message on the console ?
208 % or use
209 throw(Exception).
210 add_exception_error2(user_interrupt_signal,X,SpanInfo,WF) :- !,
211 get_predicate_name(X,Pred),
212 add_warning_wf(external_functions,'User Interrupt during external function evaluation: ',Pred,SpanInfo,WF),
213 throw(user_interrupt_signal).
214 add_exception_error2(Exception,X,SpanInfo,WF) :-
215 debug_println(20,Exception),
216 ajoin(['Exception occurred while calling external function ',X,':'],Msg),
217 add_error_wf(external_functions,Msg,Exception,SpanInfo,WF),
218 fail.
219
220 get_predicate_name(Var,P) :- var(Var),!,P='_VAR_'.
221 get_predicate_name(external_functions:C,P) :- !, get_predicate_name(C,P).
222 get_predicate_name(Module:C,Module:P) :- !, get_predicate_name(C,P).
223 get_predicate_name(Call,F/P) :- functor(Call,F,P).
224
225 is_error(evaluation_error('is'(_,ExprTerm),2,_,_),ExprTerm).
226 is_error(domain_error('is'(_,ExprTerm),2,_,_),ExprTerm).
227
228 get_external_function_type(FunName,ArgTypes,ReturnType) :-
229 external_fun_type(FunName,TypeParas,AllTypes),
230 (member(TP,TypeParas),nonvar(TP)
231 -> add_internal_error('External function type parameter not a variable:,',
232 external_fun_type(FunName,TypeParas,AllTypes))
233 ; true
234 ),
235 append(ArgTypes,[ReturnType],AllTypes).
236
237 % STANDARD EXTERNAL FUNCTIONS
238
239
240 % -------------------------------
241
242
243 :- use_module(extrasrc(external_functions_reals)). % removed explicit imports for Spider
244
245
246 expects_waitflag('STRING_TO_REAL').
247 external_fun_type('STRING_TO_REAL',[],[string,real]).
248
249 expects_waitflag('RADD').
250 external_fun_type('RADD',[],[real,real,real]).
251 expects_waitflag('RSUB').
252 external_fun_type('RSUB',[],[real,real,real]).
253 expects_waitflag('RMUL').
254 external_fun_type('RMUL',[],[real,real,real]).
255 expects_waitflag('RDIV').
256 expects_spaninfo('RDIV').
257 external_fun_type('RDIV',[],[real,real,real]).
258 external_fun_has_wd_condition('RDIV').
259 expects_waitflag('RINV').
260 expects_spaninfo('RINV').
261 external_fun_type('RINV',[],[real,real]).
262 external_fun_has_wd_condition('RINV').
263
264 external_fun_type('RPI',[],[real]).
265 external_fun_type('RZERO',[],[real]).
266 external_fun_type('RONE',[],[real]).
267 external_fun_type('REULER',[],[real]).
268
269 external_fun_type('RSIN',[],[real,real]).
270 expects_waitflag('RSIN').
271 external_fun_type('RCOS',[],[real,real]).
272 expects_waitflag('RCOS').
273 external_fun_type('RTAN',[],[real,real]).
274 expects_waitflag('RTAN').
275 external_fun_type('RCOT',[],[real,real]).
276 expects_waitflag('RCOT').
277 external_fun_type('RSINH',[],[real,real]).
278 expects_waitflag('RSINH').
279 external_fun_type('RCOSH',[],[real,real]).
280 expects_waitflag('RCOSH').
281 external_fun_type('RTANH',[],[real,real]).
282 expects_waitflag('RTANH').
283 external_fun_type('RCOTH',[],[real,real]).
284 expects_waitflag('RCOTH').
285 external_fun_type('RASIN',[],[real,real]).
286 expects_waitflag('RASIN').
287 external_fun_type('RACOS',[],[real,real]).
288 expects_waitflag('RACOS').
289 external_fun_type('RATAN',[],[real,real]).
290 expects_waitflag('RATAN').
291 external_fun_type('RACOT',[],[real,real]).
292 expects_waitflag('RACOT').
293 external_fun_type('RASINH',[],[real,real]).
294 expects_waitflag('RASINH').
295 external_fun_type('RACOSH',[],[real,real]).
296 expects_waitflag('RACOSH').
297 external_fun_type('RATANH',[],[real,real]).
298 expects_waitflag('RATANH').
299 external_fun_type('RACOTH',[],[real,real]).
300 expects_waitflag('RACOTH').
301 external_fun_type('RADIANS',[],[real,real]).
302 expects_waitflag('RADIANS').
303 expects_spaninfo('RADIANS').
304 external_fun_type('DEGREE',[],[real,real]).
305 expects_waitflag('DEGREE').
306 expects_spaninfo('DEGREE').
307
308
309 external_fun_type('RUMINUS',[],[real,real]).
310 expects_waitflag('RUMINUS').
311 external_fun_type('REXP',[],[real,real]).
312 expects_waitflag('REXP').
313 external_fun_type('RLOGe',[],[real,real]).
314 expects_waitflag('RLOGe').
315 expects_spaninfo('RLOGe').
316 external_fun_has_wd_condition('RLOGe').
317 external_fun_type('RSQRT',[],[real,real]).
318 expects_waitflag('RSQRT').
319 expects_spaninfo('RSQRT').
320 external_fun_has_wd_condition('RSQRT'). % for negative numbers obviously
321 external_fun_type('RABS',[],[real,real]).
322 expects_waitflag('RABS').
323 external_fun_type('ROUND',[],[real,integer]).
324 expects_waitflag('ROUND').
325 external_fun_type('RSIGN',[],[real,real]).
326 expects_waitflag('RSIGN').
327 external_fun_type('RINTEGER',[],[real,real]).
328 expects_waitflag('RINTEGER').
329 external_fun_type('RFRACTION',[],[real,real]).
330 expects_waitflag('RFRACTION').
331
332 expects_waitflag('RMAX').
333 expects_spaninfo('RMAX').
334 external_fun_type('RMAX',[],[real,real,real]).
335 expects_waitflag('RMIN').
336 expects_spaninfo('RMIN').
337 external_fun_type('RMIN',[],[real,real,real]).
338 expects_spaninfo('RPOW').
339 expects_waitflag('RPOW').
340 external_fun_type('RPOW',[],[real,real,real]).
341 external_fun_has_wd_condition('RPOW'). % for negative numbers, e.g., RPOW(-1.0,1.1) or RPOW(-1.0,0.5)
342 expects_spaninfo('RDECIMAL').
343 expects_waitflag('RDECIMAL').
344 external_fun_type('RDECIMAL',[],[integer,integer,real]).
345 expects_waitflag('RLOG').
346 expects_spaninfo('RLOG').
347 external_fun_type('RLOG',[],[real,real,real]).
348 external_fun_has_wd_condition('RLOG').
349
350 expects_waitflag('RLT').
351 external_fun_type('RLT',[],[real,real,boolean]).
352 expects_waitflag('REQ').
353 external_fun_type('REQ',[],[real,real,boolean]).
354 expects_waitflag('RNEQ').
355 external_fun_type('RNEQ',[],[real,real,boolean]).
356 expects_waitflag('RLEQ').
357 external_fun_type('RLEQ',[],[real,real,boolean]).
358 expects_waitflag('RGT').
359 external_fun_type('RGT',[],[real,real,boolean]).
360 expects_waitflag('RGEQ').
361 external_fun_type('RGEQ',[],[real,real,boolean]).
362 expects_waitflag('RMAXIMUM').
363 expects_spaninfo('RMAXIMUM').
364 external_fun_type('RMAXIMUM',[],[set(real),real]).
365 external_fun_has_wd_condition('RMAXIMUM'). % empty set or unbounded set
366 expects_waitflag('RMINIMUM').
367 expects_spaninfo('RMINIMUM').
368 external_fun_type('RMINIMUM',[],[set(real),real]).
369 external_fun_has_wd_condition('RMINIMUM'). % empty set or unbounded set
370
371
372
373 % -------------------------------
374
375 external_fun_type('SFADD16',[],[real,real,real]).
376 external_fun_type('SFSUB16',[],[real,real,real]).
377 external_fun_type('SFMUL16',[],[real,real,real]).
378 external_fun_type('SFDIV16',[],[real,real,real]).
379 external_fun_type('SFSQRT16',[],[real,real]).
380 external_fun_type('SFMULADD16',[],[real,real,real,real]).
381 external_fun_type('SFADD32',[],[real,real,real]).
382 external_fun_type('SFSUB32',[],[real,real,real]).
383 external_fun_type('SFMUL32',[],[real,real,real]).
384 external_fun_type('SFDIV32',[],[real,real,real]).
385 external_fun_type('SFSQRT32',[],[real,real]).
386 external_fun_type('SFMULADD32',[],[real,real,real,real]).
387 external_fun_type('SFADD64',[],[real,real,real]).
388 external_fun_type('SFSUB64',[],[real,real,real]).
389 external_fun_type('SFMUL64',[],[real,real,real]).
390 external_fun_type('SFDIV64',[],[real,real,real]).
391 external_fun_type('SFSQRT64',[],[real,real]).
392 external_fun_type('SFMULADD64',[],[real,real,real,real]).
393 external_fun_type('SFADD80',[],[couple(int,int),couple(int,int),couple(int,int)]).
394 external_fun_type('SFSUB80',[],[couple(int,int),couple(int,int),couple(int,int)]).
395 external_fun_type('SFMUL80',[],[couple(int,int),couple(int,int),couple(int,int)]).
396 external_fun_type('SFDIV80',[],[couple(int,int),couple(int,int),couple(int,int)]).
397 external_fun_type('SFSQRT80',[],[couple(int,int),couple(int,int)]).
398 external_fun_type('SFADD128',[],[couple(int,int),couple(int,int),couple(int,int)]).
399 external_fun_type('SFSUB128',[],[couple(int,int),couple(int,int),couple(int,int)]).
400 external_fun_type('SFMUL128',[],[couple(int,int),couple(int,int),couple(int,int)]).
401 external_fun_type('SFDIV128',[],[couple(int,int),couple(int,int),couple(int,int)]).
402 external_fun_type('SFSQRT128',[],[couple(int,int),couple(int,int)]).
403 external_fun_type('SFMULADD128',[],[couple(int,int),couple(int,int),couple(int,int),couple(int,int)]).
404
405 % -------------------------------
406
407 :- use_module(extrasrc(external_functions_svg)). %, [svg_points/4, svg_train/8, svg_car/8, svg_axis/7, svg_set_polygon/7]).
408
409 expects_waitflag('svg_points').
410 expects_spaninfo('svg_points').
411 external_fun_type('svg_points',[T1,T2],[seq(couple(T1,T2)),string]). % T1, T2 should be numbers
412
413 expects_waitflag('svg_train').
414 expects_spaninfo('svg_train').
415 external_fun_type('svg_train',[T1,T2],[T1,T1,T2,T2,T2,string]). % T1, T2 should be numbers
416 expects_waitflag('svg_car').
417 expects_spaninfo('svg_car').
418 external_fun_type('svg_car',[T1,T2],[T1,T1,T2,T2,T2,string]). % T1, T2 should be numbers
419
420 expects_waitflag('svg_axis').
421 expects_spaninfo('svg_axis').
422 external_fun_type('svg_axis',[T1,T2],[set(T1),T2,T2,T2,string]). % T1, T2 should be numbers
423
424 expects_waitflag('svg_set_polygon').
425 expects_spaninfo('svg_set_polygon').
426 external_fun_type('svg_set_polygon',[T2],[set(integer),T2,T2,T2,string]). % T2 should be number type
427
428 expects_waitflag('svg_set_polygon_auto').
429 expects_spaninfo('svg_set_polygon_auto').
430 external_fun_type('svg_set_polygon_auto',[T2],[set(integer),T2,T2,string]). % T2 should be number type
431
432 expects_waitflag('svg_dasharray_for_intervals').
433 expects_spaninfo('svg_dasharray_for_intervals').
434 external_fun_type('svg_dasharray_for_intervals',[T1,T2],[set(couple(T1,T2)),string]). % T1, T2 should be numbers
435
436 expects_waitflag('svg_set_dasharray').
437 expects_spaninfo('svg_set_dasharray').
438 external_fun_type('svg_set_dasharray',[],[set(integer),string]).
439
440 % -------------------------------
441
442 % MATHEMATICAL FUNCTIONS
443
444 external_fun_type('COS',[],[integer,integer]).
445 :- public 'COS'/2.
446 :- block 'COS'(-,?). % redundant; we could add CLPFD constraints for R
447 'COS'(int(X),int(R)) :- cos2(100,X,R,unknown).
448 external_fun_type('COSx',[],[integer,integer,integer]).
449 expects_spaninfo('COSx').
450 :- public 'COSx'/4.
451 :- block 'COSx'(-,?,?,?),'COSx'(?,-,?,?).
452 'COSx'(int(PrecisionMultiplier),int(X),int(R),Span) :- cos2(PrecisionMultiplier,X,R,Span).
453 :- block cos2(-,?,?,?),cos2(?,-,?,?).
454 cos2(Multiplier,X,R,Span) :- safe_is('COSx',R,round(Multiplier*cos(X/Multiplier)),Span).
455
456 external_fun_type('SIN',[],[integer,integer]).
457 :- public 'SIN'/2.
458 :- block 'SIN'(-,?). % redundant; we could add CLPFD constraints for R
459 'SIN'(int(X),int(R)) :- sin2(100,X,R,unknown).
460 external_fun_type('SINx',[],[integer,integer,integer]).
461 expects_spaninfo('SINx').
462 :- public 'SINx'/4.
463 :- block 'SINx'(-,?,?,?),'SINx'(?,-,?,?).
464 'SINx'(int(PrecisionMultiplier),int(X),int(R),Span) :- %print('SINx'(PrecisionMultiplier,X,R)),nl,
465 sin2(PrecisionMultiplier,X,R,Span).
466 :- block sin2(-,?,?,?),sin2(?,-,?,?).
467 sin2(Multiplier,X,R,Span) :- safe_is('SINx',R,round(Multiplier*sin(X/Multiplier)),Span).
468
469 external_fun_type('TAN',[],[integer,integer]).
470 :- public 'TAN'/2.
471 :- block 'TAN'(-,?). % redundant; we could add CLPFD constraints for R
472 'TAN'(int(X),int(R)) :- tan2(100,X,R,unknown).
473 external_fun_type('TANx',[],[integer,integer,integer]).
474 expects_spaninfo('TANx').
475 :- public 'TANx'/4.
476 :- block 'TANx'(-,?,?,?),'TANx'(?,-,?,?).
477 'TANx'(int(PrecisionMultiplier),int(X),int(R),Span) :- tan2(PrecisionMultiplier,X,R,Span).
478 :- block tan2(?,-,?,?),tan2(-,?,?,?).
479 tan2(Multiplier,X,R,Span) :- safe_is('TANx',R,round(Multiplier*tan(X/Multiplier)),Span).
480
481
482 external_fun_type('PROLOG_FUN',[],[string,integer,integer,integer]).
483 external_fun_has_wd_condition('PROLOG_FUN').
484 expects_spaninfo('PROLOG_FUN').
485 :- public 'PROLOG_FUN'/5.
486 'PROLOG_FUN'(string(Function),int(PrecisionMultiplier),int(Argument),int(Result),Span) :-
487 prolog_fun2(Function,PrecisionMultiplier,Argument,Result,Span).
488 % Function can be:
489 % sin, cos, tan, cot, sinh, cosh, tanh, asin, acos, atan, acot, asinh, acosh, atanh, acoth, sqrt, log, exp
490 :- block prolog_fun2(?,-,?,?,?),prolog_fun2(-,?,?,?,?), prolog_fun2(?,?,-,?,?).
491 prolog_fun2(Function,Multiplier,X,R,Span) :-
492 E =.. [Function,X/Multiplier],
493 safe_is(Function,R,round(Multiplier*E),Span).
494
495 external_fun_has_wd_condition('LOGx').
496 expects_spaninfo('LOGx').
497 external_fun_type('LOGx',[],[integer,integer,integer,integer]).
498 :- public 'LOGx'/5.
499 :- block 'LOGx'(-,?,?,?,?),'LOGx'(?,-,?,?,?), 'LOGx'(?,?,-,?,?).
500 'LOGx'(int(PrecisionMultiplier),int(Base),int(X),int(R),Span) :-
501 log2(PrecisionMultiplier,Base,X,R,Span).
502 :- block log2(?,-,?,?,?),log2(-,?,?,?,?),log2(?,?,-,?,?).
503 log2(Multiplier,Base,X,R,Span) :-
504 logx_internal(Multiplier,Base,X,R,Span).
505
506 :- use_module(tools_portability, [check_arithmetic_function/1]).
507 :- if(check_arithmetic_function(log(2, 4))).
508 % Native log(Base, Power) function is available - use it.
509 logx_internal(Multiplier,Base,X,R,Span) :-
510 safe_is('LOGx',R,round(Multiplier*log(Base/Multiplier,X/Multiplier)),Span).
511 :- else.
512 % No native log(Base, Power) support, so construct it using natural logarithms.
513 logx_internal(Multiplier,Base,X,R,Span) :-
514 safe_is('LOGx',R,round(Multiplier*(log(X/Multiplier)/log(Base/Multiplier))),Span).
515 :- endif.
516
517 :- use_module(clpfd_interface,[clpfd_gcd/3, clpfd_lcm/3, clpfd_abs/2, clpfd_sign/2]).
518 external_fun_type('GCD',[],[integer,integer,integer]).
519 :- public 'GCD'/3.
520 :- block 'GCD'(-,-,-).
521 'GCD'(int(X),int(Y),int(R)) :-
522 clpfd_gcd(X,Y,R).
523
524 % least / smallest common multiple
525 external_fun_type('LCM',[],[integer,integer,integer]).
526 :- public 'LCM'/3.
527 :- block 'LCM'(-,-,-).
528 'LCM'(int(X),int(Y),int(R)) :- clpfd_lcm(X,Y,R).
529
530 external_fun_type('ABS',[],[integer,integer]).
531 :- public 'ABS'/2.
532 :- use_module(clpfd_interface,[clpfd_eq_expr/2]).
533 :- block 'ABS'(-,-). % do we need this ??
534 'ABS'(int(X),int(R)) :-
535 clpfd_abs(X,R).
536
537 external_fun_type('SIGN',[],[integer,integer]).
538 :- public 'SIGN'/2.
539 :- block 'SIGN'(-,-).
540 'SIGN'(int(X),int(R)) :-
541 clpfd_sign(X,R).
542
543
544 % TLA style floored division
545 external_fun_has_wd_condition('FDIV').
546 expects_spaninfo('FDIV').
547 expects_waitflag('FDIV').
548 external_fun_type('FDIV',[],[integer,integer,integer]).
549 :- public 'FDIV'/5.
550 :- block 'FDIV'(-,-,-,?,?).
551 'FDIV'(X,Y,Z,Span,WF) :-
552 kernel_objects:floored_division(X,Y,Z,Span,WF).
553
554 % ceiling division
555 external_fun_has_wd_condition('CDIV').
556 expects_spaninfo('CDIV').
557 expects_waitflag('CDIV').
558 external_fun_type('CDIV',[],[integer,integer,integer]).
559 :- public 'CDIV'/5.
560 :- block 'CDIV'(-,?,?,?,?),'CDIV'(?,-,?,?,?).
561 'CDIV'(int(X),int(Y),Res,Span,WF) :-
562 ceiling_division(X,Y,Res,Span,WF).
563
564 :- block ceiling_division(-,?,?,?,?),ceiling_division(?,-,?,?,?).
565 ceiling_division(X,Y,_Res,Span,WF) :- Y=0,!,
566 add_wd_error_span('Ceiling division by zero:',X,Span,WF).
567 ceiling_division(X,Y,Res,_Span,_WF) :-
568 X mod Y =:= 0,!,
569 XY is X//Y, Res = int(XY).
570 ceiling_division(X,Y,Res,Span,WF) :-
571 kernel_objects:floored_division(int(X),int(Y),int(Z),Span,WF),
572 Z1 is 1 + Z,
573 Res = int(Z1).
574
575 external_fun_has_wd_condition('SQRT').
576 expects_spaninfo('SQRT').
577 expects_waitflag('SQRT').
578 external_fun_type('SQRT',[],[integer,integer]).
579 :- public 'SQRT'/4.
580 :- block 'SQRT'(-,?,?,?).
581 'SQRT'(int(X),R,Span,WF) :-
582 positive_integer_sqrt(X,R,Span,WF). % TO DO: maybe do CLPFD propagation?
583
584 :- block positive_integer_sqrt(-,?,?,?).
585 positive_integer_sqrt(X,_,Span,WF) :- X<0,!,
586 add_wd_error_span('Trying to compute square root of negative number:',X,Span,WF).
587 positive_integer_sqrt(X,Res,Span,_WF) :-
588 Candidate is floor(sqrt(X)), % compute using floating number function
589 (Candidate*Candidate =< X
590 -> C1 is Candidate+1,
591 (C1*C1 > X
592 -> Res = int(Candidate)
593 ; (C1+1)*(C1+1) > X
594 -> Res = int(C1)
595 ; % SQR is (C1+1)^2, Delta is X-SQR, write(sqr_candidate(C1,SQR,X,Delta)),nl,
596 % >>> SQRT(9999911144210000019*9999911144210000019+2)
597 add_error(external_functions,'Rounding error (2) while computing SQRT of: ',X,Span),
598 Res = int(C1)
599 )
600 ; add_error(external_functions,'Rounding error (1) while computing SQRT of: ',X,Span),
601 % SQRT(999991114421000001*999991114421000001+2)
602 Res = int(Candidate)
603 ).
604
605 external_fun_type('MSB',[],[integer,integer]).
606 expects_spaninfo('MSB').
607 :- public 'MSB'/3.
608 :- block 'MSB'(-,?,?).
609 'MSB'(int(X),int(R),Span) :- msb2(X,R,Span). % most significant bit
610 :- block msb2(-,?,?).
611 msb2(X,R,Span) :- safe_is('MSB',R,msb(X),Span). % TO DO: could be made reversible by propagating constraint if R known
612
613
614 external_fun_type('FACTORIAL',[],[integer,integer]).
615 expects_spaninfo('FACTORIAL').
616 expects_waitflag('FACTORIAL').
617 :- public 'FACTORIAL'/4.
618 :- block 'FACTORIAL'(-,?,?,?).
619 'FACTORIAL'(int(X),int(R),Span,WF) :- fact(X,R,Span,WF). % most significant bit
620 :- block fact(-,?,?,?).
621 fact(X,_,Span,WF) :- X<0,!, add_wd_error_span('FACTORIAL applied to negative number: ',X,Span,WF).
622 fact(X,_,Span,WF) :- X>10000,!, add_wd_error_span('FACTORIAL overflow, argument too large: ',X,Span,WF).
623 fact(X,Res,_,_) :- fact_acc(X,1,Res).
624
625 fact_acc(0,Acc,Res) :- !,Res=Acc.
626 fact_acc(N,Acc,Res) :- NAcc is Acc*N,
627 N1 is N-1, fact_acc(N1,NAcc,Res).
628
629 % TODO: fact_k, choose_nk
630
631 % BITWISE OPERATORS
632 external_fun_type('BNOT',[],[integer,integer]).
633 expects_spaninfo('BNOT').
634 :- public 'BNOT'/3.
635 :- block 'BNOT'(-,-,?).
636 'BNOT'(int(X),int(R),Span) :- bitwise_not(X,R,Span).
637 :- block bitwise_not(-,-,?).
638 bitwise_not(X,R,Span) :- number(X),!,safe_is('BNOT',R,\(X),Span).
639 bitwise_not(X,R,Span) :- safe_is('BNOT',X,\(R),Span).
640
641 external_fun_type('BAND',[],[integer,integer,integer]).
642 :- public 'BAND'/3.
643 :- block 'BAND'(-,?,?),'BAND'(?,-,?).
644 'BAND'(int(X),int(Y),int(R)) :- bitwise_and(X,Y,R).
645 :- block bitwise_and(?,-,?),bitwise_and(-,?,?).
646 bitwise_and(X,Y,R) :- R is X /\ Y. % we could do some early consistency checking, e.g., when X and R known
647
648 external_fun_type('BOR',[],[integer,integer,integer]).
649 :- public 'BOR'/3.
650 :- block 'BOR'(-,?,?),'BOR'(?,-,?).
651 'BOR'(int(X),int(Y),int(R)) :- bitwise_or(X,Y,R).
652 :- block bitwise_or(?,-,?),bitwise_or(-,?,?).
653 bitwise_or(X,Y,R) :- R is X \/ Y. % we could do some early consistency checking, e.g., when X and R known
654
655 external_fun_type('BXOR',[],[integer,integer,integer]).
656 :- public 'BXOR'/3.
657 :- block 'BXOR'(-,-,?),'BXOR'(?,-,-),'BXOR'(-,?,-).
658 'BXOR'(int(X),int(Y),int(R)) :- bitwise_xor(X,Y,R).
659 :- block bitwise_xor(-,-,?),bitwise_xor(?,-,-),bitwise_xor(-,?,-).
660 % DO WE NEED TO KNOW THE sizes of X,Y,R ?
661 % TODO: in SICStus 4.9 there is a CLP(FD) constraint for xor
662 bitwise_xor(X,Y,R) :- var(X),!, X is xor(R,Y).
663 bitwise_xor(X,Y,R) :- var(Y),!, Y is xor(X,R).
664 bitwise_xor(X,Y,R) :- R is xor(X,Y).
665
666 % TO DO: do some clpfd propagations ? X:0..N & Y:0..M -> BAND(X,Y) : 0..min(N,M)
667
668 % EXTERNAL_FUNCTION_BITS == INTEGER --> seq(INTEGER)
669 % BITS(x) == [0]
670 external_fun_type('BLSHIFT',[],[integer,integer,integer]).
671 :- public 'BLSHIFT'/3.
672 :- block 'BLSHIFT'(-,?,?),'BLSHIFT'(?,-,?).
673 'BLSHIFT'(int(X),int(Y),int(R)) :- bitwise_left_shift(X,Y,R).
674 :- block bitwise_left_shift(?,-,?),bitwise_left_shift(-,?,?).
675 bitwise_left_shift(X,Y,R) :- R is X << Y.
676 external_fun_type('BRSHIFT',[],[integer,integer,integer]).
677 :- public 'BRSHIFT'/3.
678 :- block 'BRSHIFT'(-,?,?),'BRSHIFT'(?,-,?).
679 'BRSHIFT'(int(X),int(Y),int(R)) :- bitwise_right_shift(X,Y,R).
680 :- block bitwise_right_shift(?,-,?),bitwise_right_shift(-,?,?).
681 bitwise_right_shift(X,Y,R) :- R is X >> Y.
682
683 :- assert_must_succeed(( external_functions:call_external_function('BITS',[12],[int(12)],R,integer,unknown,_WF),
684 equal_object(R,[(int(1),int(1)),(int(2),int(1)),(int(3),int(0)),(int(4),int(0))]) )).
685
686 external_fun_type('BITS',[],[integer,seq(integer)]).
687 :- public 'BITS'/2.
688 :- block 'BITS'(-,?).
689 'BITS'(int(X),Res) :- convert_to_bits(X,Res).
690
691 :- block convert_to_bits(-,?).
692 convert_to_bits(0,Res) :- !, convert_list_to_seq([int(0)],Res).
693 convert_to_bits(N,Res) :- convert_to_bits(N,[],List),
694 convert_list_to_seq(List,Res).
695 convert_to_bits(0,Acc,Res) :- !, Res=Acc.
696 convert_to_bits(X,Acc,Res) :- XM2 is X mod 2, XD2 is X // 2,
697 convert_to_bits(XD2,[int(XM2)|Acc],Res).
698 % TO DO: maybe do some constraint propagation from Result to number, or use CLP(FD) size info to infer size of sequence?
699
700 % -------------------------------
701
702 % THE CHOOSE operator (for TLA, recursive functions over sets,...)
703 % or choice operator from Abrial Book, page 60ff
704
705 :- use_module(custom_explicit_sets).
706 :- use_module(kernel_waitflags,[add_wd_error_span/4]).
707 external_fun_type('CHOOSE',[X],[set(X),X]).
708 external_fun_has_wd_condition('CHOOSE').
709 expects_waitflag('CHOOSE').
710 expects_spaninfo('CHOOSE').
711 :- public 'CHOOSE'/4.
712 :- block 'CHOOSE'(-,?,?,?).
713 'CHOOSE'([],_,Span,WF) :-
714 add_wd_error_span('CHOOSE applied to empty set: ',[],Span,WF).
715 'CHOOSE'(CS,H,_,_) :- is_interval_closure_or_integerset(CS,Low,Up),
716 !,
717 choose_interval(Low,Up,H).
718 'CHOOSE'([H|T],C,_Span,WF) :- T==[], !, kernel_objects:equal_object_optimized_wf(C,H,'CHOOSE',WF).
719 'CHOOSE'([H|T],C,Span,WF) :- !,
720 ground_value_check([H|T],Gr),
721 when(nonvar(Gr),
722 (convert_to_avl([H|T],AVL) -> 'CHOOSE'(AVL,C,Span,WF)
723 ; add_wd_error_span('Cannot determine minimum element for CHOOSE: ',[H|T],Span,WF),
724 kernel_objects:equal_object_wf(C,H,WF))
725 ).
726 'CHOOSE'(avl_set(A),H,_,WF) :- !, avl_min(A,Min), kernel_objects:equal_object_wf(H,Min,WF).
727 'CHOOSE'(global_set(GS),H,_,_) :- !, H = fd(1,GS). % assume GS not empty, integer sets covered above
728 'CHOOSE'(freetype(ID),H,Span,WF) :- !,
729 (kernel_freetypes:enumerate_freetype_wf(basic,FV,freetype(ID),WF)
730 -> kernel_objects:equal_object_wf(FV,H,WF)
731 ; add_internal_error('Could not generate freetype element: ','CHOOSE'(freetype(ID),H,Span,WF))).
732 'CHOOSE'(CS,H,Span,WF) :- custom_explicit_sets:is_cartesian_product_closure(CS,Set1,Set2),!,
733 'CHOOSE'(Set1,H1,Span,WF),
734 'CHOOSE'(Set2,H2,Span,WF),
735 kernel_objects:equal_object_wf(H,(H1,H2),WF).
736 'CHOOSE'(closure(P,T,B),H,Span,WF) :-
737 custom_explicit_sets:expand_custom_set_wf(closure(P,T,B),ER,'CHOOSE',WF),
738 'CHOOSE'(ER,H,Span,WF).
739
740 :- block choose_interval(-,?,?).
741 choose_interval(Low,_Up,H) :- number(Low),!,H=int(Low).
742 choose_interval(_Low,Up,H) :- choose_interval2(Up,H). % lower-bound is minus infinity
743 :- block choose_interval2(-,?).
744 choose_interval2(Up,H) :- number(Up),!,H=int(Up). % for those intervals we choose Up
745 choose_interval2(_,int(0)). % we have INTEGER or something equivalent; simply choose 0
746
747 :- use_module(kernel_objects,[singleton_set_element/4, singleton_set_element_wd/4]).
748 external_fun_type('MU',[X],[set(X),X]).
749 external_fun_has_wd_condition('MU').
750 expects_waitflag('MU').
751 expects_spaninfo('MU').
752 :- public 'MU'/4.
753 'MU'(Set,Res,Span,WF) :-
754 singleton_set_element(Set,Res,Span,WF).
755
756 external_fun_type('MU_WD',[X],[set(X),X]).
757 external_fun_has_wd_condition('MU_WD').
758 expects_waitflag('MU_WD').
759 expects_spaninfo('MU_WD').
760 % a version of MU which propagates more strongly from result to input
761 % but may thus fail to generate WD errors; can be used for stronger constraint propagation if MU is known to be WD
762 :- public 'MU_WD'/4.
763 'MU_WD'(Set,Res,Span,WF) :-
764 singleton_set_element_wd(Set,Res,Span,WF).
765 % -----------------
766
767 % sort a set and generate a sequence
768 % external_fun_has_wd_condition('SORT'). SORT generates virtual time-out for infinite sets; but has no WD-condition
769 % important to remove wd_condition fact to allow b_compiler to pre-compute calls to SORT
770 expects_waitflag('SORT').
771 expects_spaninfo('SORT').
772 external_fun_type('SORT',[X],[set(X),seq(X)]).
773 :- public 'SORT'/4.
774 :- block 'SORT'(-,?,?,?).
775 'SORT'([],Res,_Span,_WF) :- !, Res=[].
776 'SORT'(CS,Res,_,WF) :- custom_explicit_sets:is_custom_explicit_set(CS),!,
777 custom_explicit_sets:expand_custom_set_to_list_wf(CS,ER,Done,'SORT',WF),
778 sort_aux(Done,ER,Res,WF).
779 'SORT'([H|T],Res,_,WF) :-
780 when(ground([H|T]),
781 (maplist(convert_to_avl_if_possible,[H|T],List),
782 sort(List,SList),sort_aux(done,SList,Res,WF))).
783
784 convert_to_avl_if_possible(H,Res) :- convert_to_avl(H,CH),!,Res=CH.
785 convert_to_avl_if_possible(H,H) :-
786 add_warning(external_functions,'Cannot guarantee order when sorting:',H).
787
788 :- block sort_aux(-,?,?,?).
789 sort_aux(_,ER,Res,_WF) :- convert_list_to_seq(ER,Res).
790
791 % construct a B sequence from a Prolog list
792 convert_list_to_seq(ER,Res) :- convert_list_to_seq(ER,1,Seq), equal_object_optimized(Seq,Res).
793
794 convert_list_to_seq([],_,[]).
795 convert_list_to_seq([H|T],N,[(int(N),H)|CT]) :- N1 is N+1, convert_list_to_seq(T,N1,CT).
796
797 % :- use_module(library(samsort),[samsort/3]).
798 % TO DO: version of SORT with samsort/3 and user provided sorting predicate
799
800 % Z Compaction / squash operator to fill up gaps in sequence
801 external_fun_has_wd_condition('SQUASH'). % needs to be a function
802 expects_waitflag('SQUASH').
803 external_fun_type('SQUASH',[X],[set(couple(integer,X)),seq(X)]). % input not necessarily proper sequence
804
805 :- use_module(kernel_z,[compaction/3]).
806 :- public 'SQUASH'/3.
807 'SQUASH'(Sequence,Value,WF) :- compaction(Sequence,Value,WF).
808
809 external_fun_has_wd_condition('REPLACE'). % needs to be a function
810 expects_waitflag('REPLACE').
811 expects_spaninfo('REPLACE').
812 external_fun_type('REPLACE',[X],[seq(X),seq(X),seq(X),set(seq(X))]).
813 % Replace a pattern by another pattern within a sequence
814 % Currently it also performs a squashing of its arguments and does not check if its argument is a function or sequence.
815 % REPLACE([a],[b],[a,c,a]) = { [b,c,a], [a,c,b] };
816 % REPLACE([a],[],[a,c,a]) = { [c,a], [a,c] };
817 % REPLACE([a,a],[],[a,c,a]) = { }
818 :- public 'REPLACE'/6.
819 :- block 'REPLACE'(-,?,?,?,?,?), 'REPLACE'(?,-,?,?,?,?), 'REPLACE'(?,?,-,?,?,?).
820 'REPLACE'(Pat,Replacement,InSequence,Res,Span,_WF) :-
821 ground_value_check((Pat,Replacement,InSequence),Gr),
822 replace_pat_aux(Gr,Pat,Replacement,InSequence,Res,Span).
823 :- block replace_pat_aux(-,?,?,?,?,?).
824 replace_pat_aux(_,Pat,Replacement,InSequence,Res,Span) :-
825 convert_to_sorted_seq_list(Pat,PL,Span),
826 convert_to_sorted_seq_list(Replacement,RL,Span),
827 convert_to_sorted_seq_list(InSequence,SL,Span),
828 findall(ResList,replace_pattern(PL,RL,SL,ResList),ResLists),
829 equal_object_optimized(ResLists,Res,'REPLACE').
830
831 % convert argument to avl list and then on to a list of elements without indices
832 convert_to_sorted_seq_list([],List,_Span) :- !, List=[].
833 convert_to_sorted_seq_list(Sequence,List,_Span) :-
834 convert_to_avl(Sequence,avl_set(AVL)),
835 custom_explicit_sets:get_avl_sequence(AVL,List),!.
836 convert_to_sorted_seq_list(Sequence,_,Span) :-
837 add_error(external_functions,'Cannot convert argument to finite sequences: ',Sequence,Span).
838
839 replace_pattern(Pat,Rep,Seq,ResBSequence) :- % Prefix.Pat.Post ---> Prefix.Rep.Post
840 append(Pat,Post,PatPost),
841 append(Rep,Post,RepPost),
842 append(Prefix,PatPost,Seq),
843 append(Prefix,RepPost,ResList),
844 convert_list_to_seq(ResList,ResBSequence).
845
846
847 % Prolog term order on encoding
848 external_fun_type('LESS',[X],[X,X,boolean]).
849 :- public 'LESS'/3.
850 :- block 'LESS'(-,?,?), 'LESS'(?,-,?).
851 'LESS'(string(A),string(B),Res) :- !, less2(A,B,Res).
852 'LESS'(int(A),int(B),Res) :- !, less_clpfd(A,B,Res). % use CLPFD less ?
853 'LESS'(fd(A,G),fd(B,G),Res) :- !, less_clpfd(A,B,Res).
854 'LESS'(pred_false,B,Res) :- !, B=Res. % if B=pred_true then < , otherwise not
855 'LESS'(pred_true,_,Res) :- !, Res=pred_false.
856 % TO DO: expand finite closures, couples, avl_sets, ...
857 'LESS'(X,Y,Res) :- when((ground(X),ground(Y)), less2(X,Y,Res)).
858 % TO DO: use kernel_ordering,[ordered_value/2]).
859
860 :- use_module(clpfd_interface,[clpfd_leq_expr/2,clpfd_lt_expr/2]).
861 :- block less_clpfd(-,?,-), less_clpfd(?,-,-).
862 less_clpfd(A,B,Res) :- Res==pred_true, !, clpfd_lt_expr(A,B).
863 less_clpfd(A,B,Res) :- Res==pred_false, !, clpfd_leq_expr(B,A).
864 less_clpfd(A,B,Res) :- (A < B -> Res=pred_true ; Res=pred_false).
865
866
867 :- block less2(-,?,?), less2(?,-,?).
868 less2(A,B,Res) :- (A @< B -> Res=pred_true ; Res=pred_false).
869
870 :- use_module(kernel_ordering,[leq_ordered_value/3]).
871
872 :- public 'LEQ_SYM_BREAK'/4.
873 expects_waitflag('LEQ_SYM_BREAK').
874 external_fun_type('LEQ_SYM_BREAK',[X],[X,X,boolean]).
875 'LEQ_SYM_BREAK'(A,B,Res,WF) :- 'LEQ_SYM'(A,B,Res,WF).
876
877 expects_waitflag('LEQ_SYM').
878 external_fun_type('LEQ_SYM',[X],[X,X,boolean]).
879 % true if arg1 <= arg2 according to Prolog term order; may return true for some symbolic representations
880 % Note: it is sometimes ignored, e.g., by Kodkod or Z3 translation
881 % Also: LEQ_SYM_BREAK / LEQ_SYM do not fully support all types yet, see sym_break_supported_type
882 :- block 'LEQ_SYM'(-,?,?,?).
883 'LEQ_SYM'(int(A),int(B),Res,_WF) :- !,
884 b_interpreter_check:check_arithmetic_operator('<=',A,B,Res).
885 'LEQ_SYM'(fd(A,G),fd(B,G),Res,_WF) :- !,
886 b_interpreter_check:check_arithmetic_operator('<=',A,B,Res).
887 'LEQ_SYM'(pred_false,_,Res,_WF) :- !, Res=pred_true. % pred_false @< pred_true
888 'LEQ_SYM'(pred_true,B,Res,_WF) :- !, Res=B. % if B=pred_true -> ok; otherwise Res=pred_false
889 'LEQ_SYM'([],_,Res,_W) :- !, Res=pred_true. % the empty set is the smallest set
890 'LEQ_SYM'(closure(_,_,_),_,Res,_) :- !, Res=pred_true. % otherwise we would have to expand it
891 'LEQ_SYM'(global_set(_),_,Res,_) :- !, Res=pred_true. % ditto
892 'LEQ_SYM'(X,Y,Res,WF) :- 'LEQ_SYM2'(X,Y,Res,WF).
893
894 :- block 'LEQ_SYM2'(?,-,?,?).
895 %'LEQ_SYM'(X,Y,Res) :- print('LEQ_SYM'(X,Y,Res)),nl,fail.
896 'LEQ_SYM2'(string(A),string(B),Res,_WF) :- !, less_eq2(A,B,Res).
897 'LEQ_SYM2'(_,closure(_,_,_),Res,_WF) :- !, Res=pred_true. % we would have to expand it
898 'LEQ_SYM2'(Set1,[],Res,WF) :- !, kernel_equality:empty_set_test_wf(Set1,Res,WF).
899 'LEQ_SYM2'((A,B),(X,Y),Res,_WF) :- Res==pred_true,!, leq_ordered_value((A,B),(X,Y),_Equal).
900 'LEQ_SYM2'(rec(FA),rec(FB),Res,_WF) :- Res==pred_true,!, leq_ordered_value(rec(FA),rec(FB),_Equal).
901 % TODO: support sets, e.g., by comparing cardinality or minimal elements
902 'LEQ_SYM2'(_A,_B,Res,_WF) :- Res=pred_true.
903 %'LEQ_SYM2'(X,Y,Res,_WF) :- when((ground(X),ground(Y)), less_eq2(X,Y,Res)). % unsafe to use; we should normalize AVLs ...
904 % TO DO: use kernel_ordering:leq_ordered_value/2 more or use lex_chain([[X,X],[Y,Z]],[op(#=<)]) for pairs/records of FD values
905 % Note: it is reified in b_interpreter_check
906
907 :- block less_eq2(-,?,?), less_eq2(?,-,?).
908 less_eq2(A,B,Res) :- (A @=< B -> Res=pred_true ; Res=pred_false).
909
910 % -------------------------------
911
912 % a first prototype for implementing recursive functions
913 % still a bit clumsy to define recursive functions (using STRING parameter for names)
914 % a restriction is that we can only have one version per machine, i.e.
915 % one can only define recursive function in the CONSTANTS section and only
916 % in a deterministic fashion not depending on enumerated constants,...
917 % also: we still need to ensure that the recurisve closures are not expanded
918 % this should probably go hand in hand with the symbolic pragma
919
920 reset_external_functions :-
921 retractall(last_walltime(_)),
922 reset_ident,
923 reset_kodkod,
924 reset_observe,
925 close_all_files.
926
927 :- use_module(eventhandling,[register_event_listener/3]).
928 :- register_event_listener(clear_specification,reset_external_functions,
929 'Reset B External Functions.').
930
931 print_external_function_profile :-
932 %TODO: we could register number of external function calls, ..
933 portray_instantiations.
934
935 %:- dynamic recursive_function/2.
936 %expects_waitflag('REC'). % DEPRECATED
937 %expects_spaninfo('RECx'). % DEPRECATED
938 %expects_spaninfo('REC_LET'). % DEPRECATED
939
940
941 % -------------------------------
942
943 expects_waitflag('FORCE').
944 external_fun_type('FORCE',[T],[T,T]).
945 :- public 'FORCE'/3.
946 % example usage halve = FORCE( %x.(x:0..1000 & x mod 2 = 0 | x/2))
947 :- block 'FORCE'(-,?,?).
948 %'FORCE'(A,B,_) :- print(force(A)),nl,fail.
949 'FORCE'(avl_set(A),Result,_) :- !, equal_object(avl_set(A),Result).
950 'FORCE'([],Result,_) :- !, equal_object([],Result).
951 'FORCE'(closure(P,T,B),Result,WF) :- !,
952 (debug:debug_mode(on) -> print('FORCING : '),translate:print_bvalue(closure(P,T,B)),nl ; true),
953 custom_explicit_sets:expand_closure_to_avl_or_list(P,T,B,ExpandedValue,no_check,WF),
954 (debug:debug_mode(on) -> print('RESULT : '),translate:print_bvalue(ExpandedValue),nl,
955 print(' ASSIGNING TO : '), translate:print_bvalue(Result),nl
956 ; true),
957 equal_object(ExpandedValue,Result).
958 'FORCE'((A,B),(FA,FB),WF) :- !,'FORCE'(A,FA,WF), 'FORCE'(B,FB,WF).
959 % TO DO: treat lists and records ...
960 'FORCE'(A,B,_) :- equal_object_optimized(A,B,'FORCE').
961
962
963
964
965 % -----------------------------------------
966
967 :- public 'ENUM'/2.
968 % example usage: ENUM((x,y)) : AVLSet
969 % external function used for deriving info field annotations in ast_cleanup
970 'ENUM'(Obj,Obj).
971
972 % -----------------------------------------
973
974 expects_unevaluated_args('DO_NOT_ENUMERATE').
975 :- public 'DO_NOT_ENUMERATE'/3.
976 :- block 'DO_NOT_ENUMERATE'(-,?,?).
977 'DO_NOT_ENUMERATE'((A,B),PredRes,UEA) :- !, 'DO_NOT_ENUMERATE'(A,PredRes,UEA),'DO_NOT_ENUMERATE'(B,PredRes,UEA).
978 'DO_NOT_ENUMERATE'(fd(V,_),PredRes,UEA) :- !, 'DO_NOT_ENUMERATE'(V,PredRes,UEA).
979 'DO_NOT_ENUMERATE'(int(V),PredRes,UEA) :- !, 'DO_NOT_ENUMERATE'(V,PredRes,UEA).
980 'DO_NOT_ENUMERATE'(string(V),PredRes,UEA) :- !, 'DO_NOT_ENUMERATE'(V,PredRes,UEA).
981 'DO_NOT_ENUMERATE'(_Obj,PredRes,_UEA) :-
982 %print('INSTANTIATED: '),nl, _UEA=[UnEvalArg],translate:print_bexpr(UnEvalArg),nl, print(_Obj),nl,
983 PredRes=pred_true.
984 % add_message('DO_NOT_ENUMERATE','Enumerating: ',UnEvalArgs).
985
986 % a utility to avoid propagation of values, can be used as "enumeration barrier"
987 expects_waitflag('COPY').
988 :- public 'COPY'/3.
989 :- block 'COPY'(-,?,?).
990 'COPY'(Val,Result,WF) :- ground_value_check(Val,GrVal),
991 when(nonvar(GrVal),equal_object_optimized_wf(Val,Result,'COPY',WF)).
992
993
994 % -------------------------------
995
996 :- assert_must_succeed(( external_functions:call_external_function('STRING_APPEND',[a,b],[string(a),string(b)],string(ab),string,unknown,_WF) )).
997 % STRING MANIPULATION FUNCTIONS
998
999 :- use_module(kernel_strings,[b_string_append_wf/4, b_concat_sequence_of_strings_wf/4, b_string_reverse_wf/3,
1000 b_string_chars/2, b_string_codes/2, b_string_length/2,
1001 b_string_to_uppercase/2, b_string_to_lowercase/2]).
1002
1003 % function to append two strings, reversible
1004 external_fun_can_be_inverted('STRING_APPEND').
1005 expects_waitflag('STRING_APPEND').
1006 external_fun_type('STRING_APPEND',[],[string,string,string]).
1007 :- public 'STRING_APPEND'/4.
1008 'STRING_APPEND'(A,B,C,WF) :- b_string_append_wf(A,B,C,WF).
1009
1010 % function to append two strings, reversible
1011 external_fun_can_be_inverted('STRING_REV').
1012 expects_waitflag('STRING_REV').
1013 external_fun_type('STRING_REV',[],[string,string]).
1014 :- public 'STRING_REV'/3.
1015 'STRING_REV'(A,B,WF) :- b_string_reverse_wf(A,B,WF).
1016
1017 expects_waitflag('STRING_CONC').
1018 expects_spaninfo('STRING_CONC').
1019 external_fun_type('STRING_CONC',[],[seq(string),string]).
1020 :- public 'STRING_CONC'/4.
1021 :- block 'STRING_CONC'(-,?,?,?).
1022 % the conc(.) operator is mapped to this for strings (instead to concat_sequence)
1023 'STRING_CONC'(List,Res,Span,WF) :-
1024 b_concat_sequence_of_strings_wf(List,Res,Span,WF).
1025
1026 external_fun_can_be_inverted('STRING_CHARS').
1027 external_fun_type('STRING_CHARS',[],[string,seq(string)]).
1028 :- public 'STRING_CHARS'/2.
1029 'STRING_CHARS'(Str,SeqOfChars) :- b_string_chars(Str,SeqOfChars).
1030 /* Note: STRING_CONC can be used as inverse to combine the chars */
1031
1032 external_fun_can_be_inverted('CODES_TO_STRING').
1033 external_fun_type('CODES_TO_STRING',[],[seq(integer),string]).
1034 :- public 'CODES_TO_STRING'/2.
1035 'CODES_TO_STRING'(A,SeqRes) :- 'STRING_CODES'(SeqRes,A).
1036
1037 external_fun_can_be_inverted('STRING_CODES').
1038 external_fun_type('STRING_CODES',[],[string,seq(integer)]).
1039 :- public 'STRING_CODES'/2.
1040 'STRING_CODES'(A,SeqRes) :- b_string_codes(A,SeqRes).
1041
1042
1043 external_fun_type('STRING_TO_UPPER',[],[string,string]).
1044 :- public 'STRING_TO_UPPER'/2.
1045 'STRING_TO_UPPER'(S,S2) :- b_string_to_uppercase(S,S2).
1046 external_fun_type('STRING_TO_LOWER',[],[string,string]).
1047 :- public 'STRING_TO_LOWER'/2.
1048 'STRING_TO_LOWER'(S,S2) :- b_string_to_lowercase(S,S2).
1049
1050 :- use_module(kernel_strings,[b_string_equal_case_insensitive/3]).
1051 external_fun_type('STRING_EQUAL_CASE_INSENSITIVE',[],[string,string,boolean]).
1052 :- public 'GET_STRING_EQUAL_CASE_INSENSITIVE'/3.
1053 'STRING_EQUAL_CASE_INSENSITIVE'(S1,S2,Res) :- b_string_equal_case_insensitive(S1,S2,Res).
1054
1055 :- assert_must_succeed(( external_functions:call_external_function('STRING_LENGTH',[a],[string(a)],int(1),integer,unknown,_WF) )).
1056 % function to get length of a string
1057 external_fun_type('STRING_LENGTH',[],[string,integer]).
1058 :- public 'STRING_LENGTH'/2.
1059 'STRING_LENGTH'(S,L) :- b_string_length(S,L).
1060
1061 :- use_module(kernel_strings,[b_string_split_wf/4, b_string_join_wf/5]).
1062
1063 % function to split a string into a list of strings which were delimited by a separator
1064 % WARNING: if the seperator is of length more than one, then first match-strategy will be used
1065 external_fun_can_be_inverted('STRING_SPLIT').
1066 expects_waitflag('STRING_SPLIT').
1067 external_fun_type('STRING_SPLIT',[],[string,string,seq(string)]).
1068 :- public 'STRING_SPLIT'/4.
1069 'STRING_SPLIT'(Str,Sep,Strings,WF) :- b_string_split_wf(Str,Sep,Strings,WF).
1070
1071 :- public 'STRING_JOIN'/5.
1072 expects_waitflag('STRING_JOIN').
1073 expects_spaninfo('STRING_JOIN').
1074 external_fun_type('STRING_JOIN',[],[seq(string),string,string]).
1075 'STRING_JOIN'(SplitAtoms,Sep,Res,Span,WF) :- b_string_join_wf(SplitAtoms,Sep,Res,Span,WF).
1076
1077
1078 expects_waitflag('STRING_CONTAINS_STRING').
1079 external_fun_type('STRING_CONTAINS_STRING',[],[string,string,boolean]).
1080 % TRUE when arg2 occurs as contiguous substring in arg1
1081 :- public 'STRING_CONTAINS_STRING'/4.
1082 :- block 'STRING_CONTAINS_STRING'(-,?,?,?), 'STRING_CONTAINS_STRING'(?,-,?,?).
1083 'STRING_CONTAINS_STRING'(string(A),string(B),PredRes,_WF) :-
1084 string_contains_string_aux(A,B,PredRes).
1085 :- use_module(library(lists),[sublist/5]).
1086 % TO DO: we could enumerate B if A known and waitflag instantiated
1087 :- block string_contains_string_aux(-,?,?),string_contains_string_aux(?,-,?).
1088 string_contains_string_aux(A,B,PredRes) :-
1089 atom_codes(A,ACodes),
1090 atom_codes(B,BCodes),
1091 ? (sublist(ACodes,BCodes,_,_,_) -> PredRes=pred_true ; PredRes=pred_false).
1092
1093 :- use_module(kernel_strings,[b_substring_wf/6]).
1094 :- public 'SUB_STRING'/6.
1095 expects_spaninfo('SUB_STRING').
1096 expects_waitflag('SUB_STRING').
1097 external_fun_type('SUB_STRING',[],[string,integer,integer,string]).
1098 'SUB_STRING'(S,From,Len,Res,Span,WF) :- b_substring_wf(S,From,Len,Res,Span,WF).
1099
1100
1101 :- use_module(kernel_strings,[b_string_replace/4]).
1102 :- public 'STRING_REPLACE'/4.
1103 external_fun_type('STRING_REPLACE',[],[string,string,string,string]).
1104 'STRING_REPLACE'(S,Pat,New,Res) :- b_string_replace(S,Pat,New,Res).
1105
1106
1107 :- use_module(probsrc(kernel_freetypes), [get_freetype_id/2, get_freeval_type/3, registered_freetype_case_value/3]).
1108 :- use_module(probsrc(translate), [pretty_type/2]).
1109 :- use_module(probsrc(btypechecker), [unify_types_werrors/4]).
1110
1111 external_fun_type('STRING_IS_FREETYPE',[],[string,boolean]).
1112 :- public 'STRING_IS_FREETYPE'/2.
1113 :- block 'STRING_IS_FREETYPE'(-,?).
1114 'STRING_IS_FREETYPE'(string(ID),Res) :-
1115 get_freeval_type(_,ID,_) -> Res=pred_true ; Res=pred_false.
1116
1117 external_fun_has_wd_condition('STRING_TO_FREETYPE').
1118 external_fun_type('STRING_TO_FREETYPE',[F],[string,F]). % F is freetype case
1119 expects_type('STRING_TO_FREETYPE').
1120 expects_spaninfo('STRING_TO_FREETYPE').
1121 :- public 'STRING_TO_FREETYPE'/4.
1122 :- block 'STRING_TO_FREETYPE'(-,?,?,?).
1123 'STRING_TO_FREETYPE'(string(ID),Value,Type,Span) :-
1124 string_to_freetype2(ID,Value,Type,Span).
1125
1126 :- block string_to_freetype2(-,?,?,?).
1127 string_to_freetype2(ID,Value,Type,Span) :-
1128 get_freetype_id(Type,FreetypeId), !, % checks implicitly that Type is freetype
1129 check_is_freetype_case(FreetypeId,ID,ArgType,Span),
1130 (Type = set(couple(_,freetype(_)))
1131 -> ExpectedType = set(couple(ArgType,freetype(FreetypeId)))
1132 ; ExpectedType = freetype(FreetypeId)
1133 ),
1134 unify_types_werrors(ExpectedType,Type,Span,'STRING_TO_FREETYPE'),
1135 (registered_freetype_case_value(ID,Type,Value) -> true
1136 ; add_error('STRING_TO_FREETYPE','error while accessing case value:',ID,Span)
1137 ).
1138 string_to_freetype2(ID,_,Type,Span) :-
1139 (nonvar(ID) -> pretty_type(Type,TS),
1140 add_error('STRING_TO_FREETYPE','STRING_TO_FREETYPE: Type mismatch: expected FREETYPE or FREETYPE case function (T <-> FREETYPE), but was',TS,Span)
1141 ; add_error('STRING_TO_FREETYPE','STRING_TO_FREETYPE cannot be inverted',ID,Span)),
1142 fail.
1143
1144 :- block check_is_freetype_case(?,-,?,?).
1145 check_is_freetype_case(FreetypeId,ID,ArgType,_) :- get_freeval_type(FreetypeId,ID,ArgType), !.
1146 check_is_freetype_case(_,ID,_,Span) :-
1147 add_error('STRING_TO_FREETYPE','STRING_TO_FREETYPE: no FREETYPE case found for string',ID,Span),
1148 fail.
1149
1150
1151 external_fun_has_wd_condition('TYPED_STRING_TO_ENUM').
1152 expects_waitflag('TYPED_STRING_TO_ENUM').
1153 expects_spaninfo('TYPED_STRING_TO_ENUM').
1154 external_fun_type('TYPED_STRING_TO_ENUM',[T],[set(T),string,T]).
1155 :- public 'TYPED_STRING_TO_ENUM'/5.
1156 :- block 'TYPED_STRING_TO_ENUM'(?,-,-,?,?),'TYPED_STRING_TO_ENUM'(-,?,?,?,?).
1157 'TYPED_STRING_TO_ENUM'(Type,string(S),Res,Span,WF) :-
1158 string_to_enum2(S,fd(Nr,GS),_,Span),
1159 check_type(Type,S,Nr,GS,Res,Span,WF).
1160
1161 :- block check_type(-,?,?, ?,?,?,?), check_type(?,-,?, ?,?,?,?), check_type(?,?,-, ?,?,?,?).
1162 check_type(GSTypeExpr,S,Nr,GS,Res,Span,WF) :-
1163 get_global_set_value_type(GSTypeExpr,'TYPED_STRING_TO_ENUM',ExpectedGS),
1164 ExpectedGS=GS,
1165 !,
1166 membership_test_wf(GSTypeExpr,fd(Nr,GS),MemTest,WF),
1167 check_value(MemTest,Nr,GS,Res,S,GSTypeExpr,Span,WF).
1168 check_type(GSTypeExpr,S,_,GS,_,Span,WF) :-
1169 get_global_set_value_type(GSTypeExpr,'TYPED_STRING_TO_ENUM',ExpectedGS),
1170 tools:ajoin(['String value ',S,' is of type ',GS,' and not of expected type:'],Msg),
1171 add_wd_error_span(Msg,ExpectedGS,Span,WF).
1172
1173 :- block check_value(-,?,?,?,?,?,?,?).
1174 check_value(pred_true,Nr,GS,Res,_,_,_,_) :- !, Res=fd(Nr,GS).
1175 check_value(pred_false,_,_GS,_,S,GSTypeExpr,Span,WF) :-
1176 tools:ajoin(['String value ',S,' is of correct type but not in set:'],Msg),
1177 translate:translate_bvalue(GSTypeExpr,SetStr),
1178 add_wd_error_span(Msg,SetStr,Span,WF).
1179
1180 % get type of a set of enumerated/deferred set elements
1181 get_global_set_value_type(global_set(GS),_,Res) :- !, Res=GS.
1182 get_global_set_value_type([fd(_,GS)|_],_,Res) :- !, Res=GS.
1183 get_global_set_value_type(avl_set(node(fd(_,GS),_True,_,_,_)),_,Res) :- !, Res=GS.
1184 get_global_set_value_type(Val,Source,_) :- translate:translate_bvalue(Val,VS),
1185 add_error(Source,'First argument of illegal type, it must be a set of deferred or enumerated set elements:',VS),fail.
1186
1187 :- use_module(probsrc(translate), [pretty_type/2]).
1188
1189 external_fun_can_be_inverted('STRING_TO_ENUM').
1190 external_fun_has_wd_condition('STRING_TO_ENUM').
1191 external_fun_type('STRING_TO_ENUM',[G],[string,G]). % G is enumerated set
1192 expects_type('STRING_TO_ENUM').
1193 expects_spaninfo('STRING_TO_ENUM').
1194 :- public 'STRING_TO_ENUM'/4.
1195 :- block 'STRING_TO_ENUM'(-,-,?,?).
1196 'STRING_TO_ENUM'(string(S),FD,global(Type),Span) :- !, string_to_enum2(S,FD,Type,Span).
1197 'STRING_TO_ENUM'(_,_,Type,Span) :- pretty_type(Type,TS),
1198 add_error('STRING_TO_ENUM','Illegal type for STRING_TO_ENUM (requires a SET type): ',TS,Span),fail.
1199
1200 :- block string_to_enum2(-,-,?,?).
1201 string_to_enum2(S,Res,Type,Span) :- nonvar(S),!,
1202 (b_global_sets:lookup_global_constant(S,FD),
1203 FD = fd(_,GS)
1204 -> check_type_aux(Type,GS,S,Span),
1205 Res=FD % fd(Nr,GS)
1206 ; % TO DO: use add_wd_error_set_result
1207 add_error('STRING_TO_ENUM','Could not convert string to enumerated set element: ',S,Span),fail).
1208 string_to_enum2(S,fd(Nr,GS),Type,Span) :-
1209 string_to_enum3(S,Nr,GS,Type,Span).
1210
1211
1212 check_type_aux(Type,GS,S,Span) :- Type \= GS,!,
1213 ajoin(['String value "',S,'" has illegal type ',GS,', expected: '],Msg),
1214 add_error('STRING_TO_ENUM',Msg,Type,Span),
1215 fail.
1216 check_type_aux(_,_,_,_).
1217
1218 :- block string_to_enum3(-,-,?,?,?),string_to_enum3(-,?,-,?,?).
1219 string_to_enum3(S,Nr,GS,Type,Span) :- nonvar(S),!,
1220 (b_global_sets:lookup_global_constant(S,fd(SNr,SGS))
1221 -> check_type_aux(Type,SGS,S,Span),
1222 (SGS,SNr) = (GS,Nr)
1223 ; add_error('STRING_TO_ENUM','Could not convert string to enumerated set element: ',S,Span),fail).
1224 string_to_enum3(S,Nr,GS,_,Span) :-
1225 (b_global_sets:is_b_global_constant_hash(GS,Nr,GNS)
1226 -> GNS=S
1227 ; add_error('STRING_TO_ENUM','Could not convert deferred set element to string: ',GS:Nr,Span),fail).
1228
1229 :- use_module(kernel_strings,[b_string_is_int/2]).
1230 external_fun_type('STRING_IS_INT',[],[string,boolean]).
1231 :- public 'GET_STRING_IS_INT'/2.
1232 'STRING_IS_INT'(S,Res) :- b_string_is_int(S,Res).
1233
1234 :- use_module(kernel_strings,[b_string_is_number/2]).
1235 external_fun_type('STRING_IS_NUMBER',[],[string,boolean]).
1236 :- public 'GET_STRING_IS_NUMBER'/2.
1237 'STRING_IS_NUMBER'(S,Res) :- b_string_is_number(S,Res).
1238
1239 :- use_module(kernel_strings,[b_string_is_decimal/2]).
1240 external_fun_type('STRING_IS_DECIMAL',[],[string,boolean]).
1241 :- public 'GET_STRING_IS_DECIMAL'/2.
1242 'STRING_IS_DECIMAL'(S,Res) :- b_string_is_decimal(S,Res).
1243
1244 external_fun_type('STRING_IS_ALPHANUMERIC',[],[string,boolean]).
1245 :- use_module(kernel_strings,[b_string_is_alphanumerical/2]).
1246 :- public 'GET_STRING_IS_ALPHANUMERIC'/2.
1247 'STRING_IS_ALPHANUMERIC'(X,Res) :- b_string_is_alphanumerical(X,Res).
1248
1249 % synonyms as use for functions to BOOL rather than predicates
1250 'GET_STRING_EQUAL_CASE_INSENSITIVE'(S1,S2,Res) :- 'STRING_EQUAL_CASE_INSENSITIVE'(S1,S2,Res).
1251 'GET_STRING_IS_ALPHANUMERIC'(S,Res) :- 'STRING_IS_ALPHANUMERIC'(S,Res).
1252 'GET_STRING_IS_DECIMAL'(S,Res) :- 'STRING_IS_DECIMAL'(S,Res).
1253 'GET_STRING_IS_NUMBER'(S,Res) :- 'STRING_IS_NUMBER'(S,Res).
1254 'GET_STRING_IS_INT'(S,Res) :- 'STRING_IS_INT'(S,Res).
1255
1256 % A Utility to convert Decimal Strings to Integers
1257 % TO DO: make a more precise version using just integers: currently DEC_STRING_TO_INT("1024.235",2) = 102423 !
1258 external_fun_has_wd_condition('DEC_STRING_TO_INT').
1259 expects_spaninfo('DEC_STRING_TO_INT').
1260 expects_waitflag('DEC_STRING_TO_INT').
1261 external_fun_type('DEC_STRING_TO_INT',[],[string,integer,integer]).
1262
1263 :- assert_must_succeed((atom_codes(A,"1024"),
1264 external_functions:'DEC_STRING_TO_INT'(string(A),int(0),int(1024),unknown,no_wf_available))).
1265 :- assert_must_succeed((atom_codes(A,"1024.1"),
1266 external_functions:'DEC_STRING_TO_INT'(string(A),int(1),int(10241),unknown,no_wf_available))).
1267 :- public 'DEC_STRING_TO_INT'/5.
1268 :- block 'DEC_STRING_TO_INT'(-,?,?,?,?),'DEC_STRING_TO_INT'(?,-,?,?,?).
1269 'DEC_STRING_TO_INT'(string(S),int(Precision),int(Res),Span,WF) :-
1270 dec_str_to_int(S,Precision,Res,Span,WF).
1271
1272 :- use_module(tools,[split_chars/3]).
1273 :- block dec_str_to_int(-,?,?,?,?),dec_str_to_int(?,-,?,?,?).
1274 dec_str_to_int(S,Precision,Res,Span,WF) :-
1275 atom_codes(S,Codes),
1276 split_chars(Codes,".",[Left|T]),
1277 (T=[] -> Right="", dec_str_to_int2(Left,Right,Precision,Res,Span,WF)
1278 ; T = [Right] -> dec_str_to_int2(Left,Right,Precision,Res,Span,WF)
1279 ; %add_error(external_functions,'Expecting integer or decimal number:',S,Span),fail
1280 add_wd_error_span('String contains multiple dots, expecting integer or decimal number for DEC_STRING_TO_INT:',S,Span,WF)
1281 ).
1282
1283
1284 get_sign([45|T],-1,Res) :- !,strip_ws(T,Res).
1285 get_sign([32|T],PosNeg,Res) :- !, get_sign(T,PosNeg,Res).
1286 get_sign(L,1,L).
1287 strip_ws([32|T],R) :- !, strip_ws(T,R).
1288 strip_ws(R,R).
1289
1290 ?rounding([H|_]) :- member(H,"56789").
1291
1292 is_zero(48). % code of 0
1293 is_digit(Code) :- Code >= 48, Code =< 57.
1294 check_digits(Codes,_,_,Res) :- maplist(is_digit,Codes),!,Res=ok.
1295 check_digits(Codes,Span,WF,ko) :-
1296 append([39|Codes],[39],C2), atom_codes(A,C2), % generate atom with quotes
1297 %add_error(external_functions,'Illegal number: ',A,Span),fail.
1298 add_wd_error_span('String contains illegal characters, expecting integer or decimal number for DEC_STRING_TO_INT:',A,Span,WF).
1299
1300 dec_safe_number_codes(Number,[],_,_) :- !, Number=0.
1301 dec_safe_number_codes(Number,Codes,Span,WF) :-
1302 (safe_number_codes(Nr,Codes) -> Number=Nr
1303 ; append([39|Codes],[39],C2), atom_codes(A,C2),
1304 %add_error(external_functions,'Cannot convert to number: ',A,Span),fail
1305 add_wd_error_span('Cannot convert string to number for DEC_STRING_TO_INT:',A,Span,WF),
1306 Number='$WDERROR$'
1307 ).
1308
1309 dec_str_to_int2(Left,Right,Precision,Res,Span,WF) :-
1310 maplist(is_zero,Right), Precision >= 0,
1311 !,
1312 dec_safe_number_codes(LeftNumber,Left,Span,WF),
1313 (LeftNumber=='$WDERROR$' -> true
1314 ; safe_is('DEC_STRING_TO_INT',Res,LeftNumber*(10^Precision),Span,WF)).
1315 dec_str_to_int2(Left,Right,Precision,Res,Span,WF) :- get_sign(Left,Sign,NewLeft),
1316 check_digits(NewLeft,Span,WF,Res1), check_digits(Right,Span,WF,Res2),
1317 (Res1==ok,Res2==ok
1318 -> shift(Precision,NewLeft,Right,ResL,ResR),
1319 dec_safe_number_codes(LeftInteger,ResL,Span,WF),
1320 ? (rounding(ResR)
1321 -> Res is Sign*(LeftInteger+1)
1322 ; Res is Sign*LeftInteger)
1323 ; true).
1324
1325 :- use_module(library(lists),[append_length/4]).
1326 % shift decimal values left or right depending on precision argument
1327 shift(0,Left,Right,Left,Right) :- !.
1328 shift(Pos,Left,Right,ResL,ResR) :- Pos>0,!,
1329 append(Left,Left2,ResL),
1330 length(Right,RLen),
1331 (RLen >= Pos -> append_length(Left2,ResR,Right,Pos) % take first Pos elements from R and shift left of .
1332 ; append(Right,Zeros,Left2), % take all of Right and add Zeros
1333 ResR = [],
1334 NrZeros is Pos - RLen,
1335 length(Zeros,NrZeros), maplist(is_zero,Zeros)
1336 ).
1337 shift(Pos,Left,Right,ResL,ResR) :- % Pos < 0
1338 length(Left,LLen), PPos is -Pos,
1339 (LLen >= PPos
1340 -> Shift is LLen-PPos, append_length(ResL,L2,Left,Shift), append(L2,Right,ResR)
1341 ; %Result always 0.0...
1342 NrZeros is PPos - LLen,length(Zeros,NrZeros), maplist(is_zero,Zeros),
1343 ResL = "0",
1344 append(Zeros,LR,ResR),
1345 append(Left,Right,LR)).
1346
1347 :- public 'STRING_PADLEFT'/6.
1348 external_fun_has_wd_condition('STRING_PADLEFT').
1349 expects_waitflag('STRING_PADLEFT').
1350 expects_spaninfo('STRING_PADLEFT').
1351 external_fun_type('STRING_PADLEFT',[],[string,integer,string,string]).
1352 :- block 'STRING_PADLEFT'(-,?,?,?,?,?),'STRING_PADLEFT'(?,-,?,?,?,?),'STRING_PADLEFT'(?,?,-,?,?,?).
1353 'STRING_PADLEFT'(string(S),int(Width),string(PadChar),Res,Span,WF) :-
1354 string_pad_left(S,Width,PadChar,Res,Span,WF).
1355
1356 :- block string_pad_left(-,?,?,?,?,?),string_pad_left(?,-,?,?,?,?),string_pad_left(?,?,-,?,?,?).
1357 string_pad_left(_S,_Width,PadChar,_Res,Span,WF) :-
1358 atom_length(PadChar,Len), Len \= 1,
1359 !,
1360 add_wd_error_span('STRING_PADLEFT requires padding string of length 1: ',PadChar,Span,WF).
1361 string_pad_left(S,Width,PadChar,Res,_Span,_WF) :-
1362 atom_length(S,Len),
1363 (Len >= Width % no padding necessary
1364 -> Res = string(S)
1365 ; ToPad is Width-Len,
1366 atom_codes(PadChar,[PadCode]),
1367 atom_codes(S,Codes),
1368 pad_char(ToPad,PadCode,PaddedCodes,Codes),
1369 atom_codes(ResStr,PaddedCodes),
1370 Res = string(ResStr)
1371 ).
1372
1373 pad_char(0,_,Res,Tail) :- !, Res=Tail.
1374 pad_char(Nr,Code,[Code|TR],Tail) :- N1 is Nr-1, pad_char(N1,Code,TR,Tail).
1375
1376
1377
1378
1379 :- use_module(kernel_strings,[b_string_to_int_wf/4]).
1380 external_fun_has_wd_condition('STRING_TO_INT').
1381 expects_waitflag('STRING_TO_INT').
1382 expects_spaninfo('STRING_TO_INT').
1383 external_fun_type('STRING_TO_INT',[],[string,integer]).
1384 :- public 'STRING_TO_INT'/4.
1385 :- block 'STRING_TO_INT'(-,-,?,?).
1386 'STRING_TO_INT'(S,I,Span,WF) :- b_string_to_int_wf(S,I,Span,WF).
1387
1388
1389 :- use_module(kernel_strings,[int_to_b_string/2]).
1390 external_fun_type('INT_TO_STRING',[],[integer,string]).
1391 :- public 'INT_TO_STRING'/2.
1392 'INT_TO_STRING'(I,S) :- int_to_b_string(I,S).
1393
1394 :- use_module(kernel_strings,[int_to_dec_b_string/3, real_to_dec_b_string/4]).
1395 external_fun_type('INT_TO_DEC_STRING',[],[integer,integer,string]).
1396 :- public 'INT_TO_DEC_STRING'/3.
1397 'INT_TO_DEC_STRING'(I,Precision,S) :- int_to_dec_b_string(I,Precision,S).
1398
1399 external_fun_type('REAL_TO_DEC_STRING',[],[real,integer,string]).
1400 expects_spaninfo('REAL_TO_DEC_STRING').
1401 :- public 'REAL_TO_DEC_STRING'/4.
1402 'REAL_TO_DEC_STRING'(R,Precision,S,Span) :- real_to_dec_b_string(R,Precision,S,Span).
1403
1404
1405 :- use_module(kernel_strings,[to_b_string/2,to_b_string_with_options/3,format_to_b_string/3]).
1406 external_fun_type('TO_STRING',[X],[X,string]).
1407 :- public 'TO_STRING'/2.
1408 'TO_STRING'(Value,S) :- to_b_string(Value,S).
1409
1410 external_fun_type('TO_STRING_UNICODE',[X],[X,string]).
1411 :- public 'TO_STRING_UNICODE'/2.
1412 'TO_STRING_UNICODE'(Value,S) :- to_b_string_with_options(Value,[unicode],S).
1413
1414 external_fun_type('FORMAT_TO_STRING',[X],[string,seq(X),string]).
1415 :- public 'FORMAT_TO_STRING'/3.
1416 'FORMAT_TO_STRING'(FormatString,ListOfStrings,Res) :- format_to_b_string(FormatString,ListOfStrings,Res).
1417
1418
1419 external_fun_type('STRINGIFY',[X],[X,string]).
1420 expects_unevaluated_args('STRINGIFY').
1421 :- public 'PRETTY_PRINT_TO_STRING'/3.
1422 :- public 'STRINGIFY'/3.
1423 % pretty print a formula to string, the value is not used (but will currently be evaluated !)
1424 % TO DO: should we enforce a certain mode? (ascii, unicode, ...)
1425
1426 'PRETTY_PRINT_TO_STRING'(V,R,A) :- 'STRINGIFY'(V,R,A). % old name
1427 'STRINGIFY'(_Value,Res,[AST]) :-
1428 translate:translate_bexpression(AST,S),
1429 Res = string(S).
1430
1431 external_fun_type('HASH',[X],[X,integer]).
1432 :- public 'HASH'/2.
1433 :- block 'HASH'(-,?).
1434 'HASH'(Value,Int) :-
1435 % TO DO: use ground_value_check
1436 when(ground(Value),(term_hash(Value,H),Int=int(H))).
1437
1438
1439 external_fun_type('TO_INT',[X],[X,integer]). % can translate enumerated/deferred set elements to integer
1440 expects_waitflag('TO_INT').
1441 expects_spaninfo('TO_INT').
1442 :- public 'TO_INT'/4.
1443 :- block 'TO_INT'(-,?,?,?).
1444 'TO_INT'(fd(X,_),I,_,_) :- !, I=int(X).
1445 'TO_INT'(int(X),I,_,_) :- !, I=int(X).
1446 'TO_INT'(string(X),I,Span,WF) :- !, 'STRING_TO_INT'(string(X),I,Span,WF).
1447 'TO_INT'(Val,_,Span,_WF) :- !, translate:translate_bvalue(Val,VS),
1448 add_error(external_functions,'Illegal argument type for TO_INT:',VS,Span).
1449
1450
1451 external_fun_has_wd_condition('INT_TO_ENUM').
1452 expects_waitflag('INT_TO_ENUM').
1453 expects_spaninfo('INT_TO_ENUM').
1454 external_fun_type('INT_TO_ENUM',[T],[set(T),integer,T]).
1455 :- public 'INT_TO_ENUM'/5.
1456 :- block 'INT_TO_ENUM'(?,-,?,?,?),'INT_TO_ENUM'(-,?,?,?,?).
1457 'INT_TO_ENUM'(GSTypeExpr,int(I),Res,Span,WF) :-
1458 get_global_set_value_type(GSTypeExpr,'INT_TO_ENUM',GS),
1459 int2enum(GS,GSTypeExpr,I,Res,Span,WF).
1460 :- use_module(b_global_sets,[b_get_fd_type_bounds/3]).
1461
1462 :- use_module(library(clpfd), []). % for .. operator
1463 :- block int2enum(?,?,-,?,?,?).
1464 int2enum(GS,_,I,_,Span,WF) :-
1465 b_get_fd_type_bounds(GS,Low,Up),
1466 (I<Low ; integer(Up),I>Up),!,
1467 tools:ajoin(['INT_TO_ENUM integer value ',I,' is not in expected range for ',GS,' :'],Msg),
1468 add_wd_error_span(Msg,Low..Up,Span,WF).
1469 int2enum(GS,GSTypeExpr,I,Res,Span,WF) :- Res = fd(I,GS),
1470 membership_test_wf(GSTypeExpr,Res,MemTest,WF),
1471 check_value(MemTest,I,GS,Res,I,GSTypeExpr,Span,WF).
1472
1473 % -------------------------------
1474 % REGULAR EXPRESSION FUNCTIONS
1475 % Using ECMAScript syntax: http://www.cplusplus.com/reference/regex/ECMAScript/
1476
1477 :- use_module(extension('regexp/regexp'),
1478 [regexp_match/3, is_regexp/1, regexp_replace/5,
1479 regexp_search_first/4, regexp_search_first_detailed/5]).
1480 external_fun_type('REGEX_MATCH',[],[string,string,boolean]).
1481 :- public 'REGEX_MATCH'/3, 'REGEX_IMATCH'/3.
1482 :- block 'REGEX_MATCH'(-,?,?), 'REGEX_MATCH'(?,-,?).
1483 'REGEX_MATCH'(string(String),string(Pattern),Res) :- block_regex_match(String,Pattern,match_case,Res).
1484
1485 external_fun_type('REGEX_IMATCH',[],[string,string,boolean]).
1486 :- block 'REGEX_IMATCH'(-,?,?), 'REGEX_IMATCH'(?,-,?).
1487 'REGEX_IMATCH'(string(String),string(Pattern),Res) :- block_regex_match(String,Pattern,ignore_case,Res).
1488
1489 :- block block_regex_match(-,?,?,?), block_regex_match(?,-,?,?).
1490 block_regex_match(String,Pattern,IgnoreCase,Res) :-
1491 (regexp_match(String,Pattern,IgnoreCase) -> Res=pred_true ; Res=pred_false).
1492
1493 external_fun_type('IS_REGEX',[],[string,boolean]).
1494 :- public 'IS_REGEX'/2.
1495 :- block 'IS_REGEX'(-,?).
1496 'IS_REGEX'(string(Pattern),Res) :- block_is_regexp(Pattern,Res).
1497 :- block block_is_regexp(-,?).
1498 block_is_regexp(Pattern,Res) :-
1499 (is_regexp(Pattern) -> Res=pred_true ; Res=pred_false).
1500
1501
1502 :- public 'GET_IS_REGEX'/2.
1503 :- public 'GET_IS_REGEX_MATCH'/3.
1504 :- public 'GET_IS_REGEX_IMATCH'/3.
1505 % synonyms as use for functions to BOOL rather than predicates
1506 'GET_IS_REGEX'(A,Res) :- 'IS_REGEX'(A,Res).
1507 'GET_IS_REGEX_MATCH'(S1,S2,Res) :- 'REGEX_MATCH'(S1,S2,Res).
1508 'GET_IS_REGEX_IMATCH'(S1,S2,Res) :- 'REGEX_IMATCH'(S1,S2,Res).
1509
1510 external_fun_type('REGEX_REPLACE',[],[string,string,string,string]).
1511 :- public 'REGEX_REPLACE'/4.
1512 :- block 'REGEX_REPLACE'(-,?,?,?), 'REGEX_REPLACE'(?,-,?,?), 'REGEX_REPLACE'(?,?,-,?).
1513 'REGEX_REPLACE'(string(String),string(Pattern),string(ReplString),Res) :-
1514 block_regex_replace(String,Pattern,match_case,ReplString,Res).
1515
1516 external_fun_type('REGEX_IREPLACE',[],[string,string,string,string]).
1517 :- public 'REGEX_IREPLACE'/4.
1518 :- block 'REGEX_IREPLACE'(-,?,?,?), 'REGEX_IREPLACE'(?,-,?,?), 'REGEX_IREPLACE'(?,?,-,?).
1519 'REGEX_IREPLACE'(string(String),string(Pattern),string(ReplString),Res) :-
1520 block_regex_replace(String,Pattern,ignore_case,ReplString,Res).
1521
1522 :- block block_regex_replace(-,?,?,?,?), block_regex_replace(?,-,?,?,?), block_regex_replace(?,?,?,-,?).
1523 block_regex_replace(String,Pattern,IgnoreCase,ReplString,Result) :-
1524 regexp_replace(String,Pattern,IgnoreCase,ReplString,Res), Result=string(Res).
1525
1526
1527 external_fun_type('REGEX_SEARCH_STR',[],[string,string,string]).
1528 :- public 'REGEX_SEARCH_STR'/3, 'REGEX_ISEARCH_STR'/3.
1529 :- block 'REGEX_SEARCH_STR'(-,?,?), 'REGEX_SEARCH_STR'(?,-,?).
1530 'REGEX_SEARCH_STR'(string(String),string(Pattern),Res) :- block_regex_search_first(String,Pattern,match_case,Res).
1531 external_fun_type('REGEX_ISEARCH_STR',[],[string,string,string]).
1532 :- block 'REGEX_ISEARCH_STR'(-,?,?), 'REGEX_ISEARCH_STR'(?,-,?).
1533 'REGEX_ISEARCH_STR'(string(String),string(Pattern),Res) :- block_regex_search_first(String,Pattern,ignore_case,Res).
1534 :- block block_regex_search_first(-,?,?,?), block_regex_search_first(?,-,?,?).
1535 block_regex_search_first(String,Pattern,IgnoreCase,Result) :-
1536 regexp_search_first(String,Pattern,IgnoreCase,Res), Result=string(Res).
1537
1538 external_fun_type('REGEX_SEARCH',[],[string,integer,string,
1539 record([field(length,integer),field(position,integer),
1540 field(string,string),
1541 field(submatches,seq(string))])]).
1542 :- public 'REGEX_SEARCH'/4, 'REGEX_ISEARCH'/4.
1543 'REGEX_SEARCH'(S,From,Pat,Res) :- 'REGEX_SEARCH5'(S,From,Pat,match_case,Res).
1544 external_fun_type('REGEX_ISEARCH',TV,T) :- external_fun_type('REGEX_SEARCH',TV,T).
1545 'REGEX_ISEARCH'(S,From,Pat,Res) :- 'REGEX_SEARCH5'(S,From,Pat,ignore_case,Res).
1546
1547 :- block 'REGEX_SEARCH5'(-,?,?,?,?), 'REGEX_SEARCH5'(?,-,?,?,?), 'REGEX_SEARCH5'(?,?,-,?,?).
1548 'REGEX_SEARCH5'(string(String),int(From),string(Pattern),IgnoreCase,Res) :-
1549 block_regex_search_first_detailed(String,From,Pattern,IgnoreCase,Res).
1550
1551 :- block block_regex_search_first_detailed(-,?,?,?,?),
1552 block_regex_search_first_detailed(?,-,?,?,?), block_regex_search_first_detailed(?,?,-,?,?).
1553 block_regex_search_first_detailed(String,FromIndex,Pattern,IgnoreCase,Result) :-
1554 regexp_search_first_detailed(String,FromIndex,Pattern,IgnoreCase,Res),
1555 construct_match_result(Res,Result).
1556
1557 construct_match_result(match(Pos,Len,[Str|SubMatches]),Res) :- !,
1558 BPos is Pos+1,
1559 maplist(mkstring,SubMatches,SubMatchesStr),
1560 convert_list_to_seq(SubMatchesStr,SubList),
1561 Res = rec([field(length,int(Len)), field(position,int(BPos)),
1562 field(string,string(Str)), field(submatches,SubList)]).
1563 construct_match_result('no-match',Res) :- !,
1564 Res = rec([field(length,int(-1)), field(position,int(-1)), field(string,string('')), field(submatches,[])]).
1565
1566 mkstring(A,string(A)).
1567
1568 :- use_module(extension('regexp/regexp'), [regexp_search_all/4]).
1569 external_fun_type('REGEX_SEARCH_ALL',[],[string,string,seq(string)]).
1570 :- public 'REGEX_SEARCH_ALL'/3, 'REGEX_ISEARCH_ALL'/3.
1571 :- block 'REGEX_SEARCH_ALL'(-,?,?), 'REGEX_SEARCH_ALL'(?,-,?).
1572 'REGEX_SEARCH_ALL'(string(String),string(Pattern),Res) :- block_regex_search_all(String,Pattern,match_case,Res).
1573
1574 external_fun_type('REGEX_ISEARCH_ALL',[],[string,string,seq(string)]).
1575 :- block 'REGEX_ISEARCH_ALL'(-,?,?), 'REGEX_ISEARCH_ALL'(?,-,?).
1576 'REGEX_ISEARCH_ALL'(string(String),string(Pattern),Res) :- block_regex_search_all(String,Pattern,ignore_case,Res).
1577
1578 :- block block_regex_search_all(-,?,?,?), block_regex_search_all(?,-,?,?).
1579 block_regex_search_all(String,Pattern,IgnoreCase,Result) :-
1580 regexp_search_all(String,Pattern,IgnoreCase,Matches),
1581 maplist(mkstring,Matches,MatchesStr),
1582 convert_list_to_seq(MatchesStr,Result).
1583
1584
1585 % -------------------------------
1586
1587 external_fun_type('SHA_HASH',[X],[X,set(couple(integer,integer))]).
1588 expects_waitflag('SHA_HASH').
1589 :- use_module(extension('probhash/probhash'),[raw_sha_hash/2]).
1590 :- use_module(store,[normalise_value_for_var/3]).
1591 :- public 'SHA_HASH'/3.
1592 :- block 'SHA_HASH'(-,?,?).
1593 'SHA_HASH'(Value,Res,WF) :-
1594 normalise_value_for_var('SHA_HASH',Value,NValue),
1595 ground_value_check(NValue,Gr),
1596 sha_hash(NValue,Gr,Res,WF).
1597 :- block sha_hash(?,-,?,?).
1598 sha_hash(Value,_,Res,WF) :-
1599 raw_sha_hash(Value,List),
1600 convert_to_int_seq(List,1,Seq),
1601 equal_object_optimized_wf(Seq,Res,'SHA_HASH',WF).
1602
1603 convert_to_int_seq([],_,[]).
1604 convert_to_int_seq([H|T],N,[(int(N),int(H))|CT]) :- N1 is N+1, convert_to_int_seq(T,N1,CT).
1605
1606 external_fun_type('SHA_HASH_HEX',[X],[X,string]).
1607 :- public 'SHA_HASH_HEX'/2.
1608 :- block 'SHA_HASH_HEX'(-,?).
1609 'SHA_HASH_HEX'(Value,Res) :-
1610 normalise_value_for_var('SHA_HASH_HEX',Value,NValue),
1611 ground_value_check(NValue,Gr),
1612 sha_hash_string(NValue,Gr,Res).
1613 :- block sha_hash_string(?,-,?).
1614 sha_hash_string(Value,_,Res) :-
1615 sha_hash_as_hex_codes(Value,SHAHexCodes), atom_codes(Atom,SHAHexCodes),
1616 Res = string(Atom).
1617
1618 % -------------------------------
1619
1620 % STRING FILE SYSTEM FUNCTIONS
1621
1622
1623 :- use_module(kernel_objects).
1624 :- use_module(library(file_systems)).
1625 performs_io('FILES').
1626 external_fun_type('FILES',[],[string,set(string)]).
1627 :- public 'FILES'/2.
1628 :- block 'FILES'(-,?).
1629 'FILES'(string(A),L) :- files2(A,L).
1630 :- block files2(-,?).
1631 files2(Dir,List) :- b_absolute_file_name(Dir,ADir),
1632 findall(string(F),file_member_of_directory(ADir,F,_FLong),L),
1633 equal_object_optimized(L,List,files2).
1634 performs_io('FULL_FILES').
1635 external_fun_type('FULL_FILES',[],[string,set(string)]).
1636 :- public 'FULL_FILES'/2.
1637 :- block 'FULL_FILES'(-,?).
1638 'FULL_FILES'(string(A),L) :- full_files2(A,L).
1639 :- block full_files2(-,?).
1640 full_files2(Dir,List) :-
1641 b_absolute_file_name(Dir,ADir),
1642 findall(string(FLong),file_member_of_directory(ADir,_F,FLong),L),
1643 equal_object_optimized(L,List,full_files2).
1644
1645
1646 performs_io('DIRECTORIES').
1647 external_fun_type('DIRECTORIES',[],[string,set(string)]).
1648 :- public 'DIRECTORIES'/2.
1649 :- block 'DIRECTORIES'(-,?).
1650 'DIRECTORIES'(string(A),L) :- dir2(A,L).
1651 :- block dir2(-,?).
1652 dir2(Dir,List) :- b_absolute_file_name(Dir,ADir),
1653 findall(string(F),directory_member_of_directory(ADir,F,_FLong),L),
1654 equal_object_optimized(L,List,dir2).
1655 performs_io('FULL_DIRECTORIES').
1656 external_fun_type('FULL_DIRECTORIES',[],[string,set(string)]).
1657 :- public 'FULL_DIRECTORIES'/2.
1658 :- block 'FULL_DIRECTORIES'(-,?).
1659 'FULL_DIRECTORIES'(string(A),L) :- full_dir2(A,L).
1660 :- block full_dir2(-,?).
1661 full_dir2(Dir,List) :- b_absolute_file_name(Dir,ADir),
1662 findall(string(FLong),directory_member_of_directory(ADir,_,FLong),L),
1663 equal_object_optimized(L,List,full_dir2).
1664
1665 :- public 'GET_FILE_EXISTS'/2.
1666 'GET_FILE_EXISTS'(S,PREDRES) :- 'FILE_EXISTS'(S,PREDRES). % synonym as external function
1667 performs_io('FILE_EXISTS').
1668 external_fun_type('FILE_EXISTS',[],[string,boolean]).
1669 :- public 'FILE_EXISTS'/2.
1670 :- block 'FILE_EXISTS'(-,?).
1671 'FILE_EXISTS'(string(A),PREDRES) :- file_exists2(A,PREDRES).
1672 :- block file_exists2(-,?).
1673 file_exists2(A,PREDRES) :- b_absolute_file_name(A,AA),
1674 (file_exists(AA) -> PREDRES=pred_true ; PREDRES=pred_false).
1675
1676 :- public 'GET_DIRECTORY_EXISTS'/2.
1677 'GET_DIRECTORY_EXISTS'(S,PREDRES) :- 'DIRECTORY_EXISTS'(S,PREDRES). % synonym as external function
1678 performs_io('DIRECTORY_EXISTS').
1679 external_fun_type('DIRECTORY_EXISTS',[],[string,boolean]).
1680 :- public 'DIRECTORY_EXISTS'/2.
1681 :- block 'DIRECTORY_EXISTS'(-,?).
1682 'DIRECTORY_EXISTS'(string(A),PREDRES) :- dir_exists2(A,PREDRES).
1683 :- block dir_exists2(-,?).
1684 dir_exists2(A,PREDRES) :- b_absolute_file_name(A,AA),
1685 (directory_exists(AA) -> PREDRES=pred_true ; PREDRES=pred_false).
1686
1687 :- use_module(tools,[get_parent_directory/2]).
1688 % a variant of the predicate b_absolute_file_name_relative_to_main_machine in bmachine using safe_call (with span):
1689 b_absolute_file_name(File,AbsFileName) :- b_absolute_file_name(File,AbsFileName,unknown).
1690 b_absolute_file_name(File,AbsFileName,Span) :-
1691 bmachine:b_get_main_filename(MainFileName),!,
1692 get_parent_directory(MainFileName,Directory),
1693 % in Jupyter main file is (machine from Jupyter cell).mch, which confuses SICStus as the file does not exist
1694 safe_call(
1695 absolute_file_name(File,AbsFileName,[relative_to(Directory)]),
1696 Span).
1697 b_absolute_file_name(File,AbsFileName,Span) :-
1698 % call is executed without machine context; we could simply throw an error and fail
1699 safe_call(
1700 absolute_file_name(File,AbsFileName),
1701 Span).
1702
1703 :- public 'GET_FILE_PROPERTY'/3.
1704 'GET_FILE_PROPERTY'(S1,S2,PREDRES) :- 'FILE_PROPERTY'(S1,S2,PREDRES). % synonym as external function
1705 performs_io('FILE_PROPERTY').
1706 external_fun_type('FILE_PROPERTY',[],[string,string,boolean]).
1707 :- public 'FILE_PROPERTY'/3.
1708 :- block 'FILE_PROPERTY'(-,?,?), 'FILE_PROPERTY'(?,-,?).
1709 'FILE_PROPERTY'(string(A),string(P),BoolRes) :-
1710 file_property2(A,P,BoolRes).
1711 :- block file_property2(-,?,?), file_property2(?,-,?).
1712 file_property2(File,Prop,BoolRes) :-
1713 b_absolute_file_name(File,AFile),
1714 file_property(AFile,Prop) -> BoolRes=pred_true ; BoolRes=pred_false.
1715 % possible properties: readable, writable, executable
1716
1717 performs_io('FILE_PROPERTY_VALUE').
1718 external_fun_type('FILE_PROPERTY_VALUE',[],[string,string,integer]).
1719 :- public 'FILE_PROPERTY_VALUE'/3.
1720 :- block 'FILE_PROPERTY_VALUE'(-,?,?), 'FILE_PROPERTY_VALUE'(?,-,?).
1721 'FILE_PROPERTY_VALUE'(string(A),string(P),int(R)) :-
1722 file_property_val2(A,P,R).
1723 :- block file_property_val2(-,?,?), file_property_val2(?,-,?).
1724 file_property_val2(File,Prop,Res) :-
1725 b_absolute_file_name(File,AFile),
1726 file_property(AFile,Prop,Val) -> Res=Val
1727 ; add_error(external_functions,'Illegal FILE_PROPERTY',Prop),Res=int(-1).
1728 % possible properties:
1729 % size_in_bytes, create_timestamp, modify_timestamp, access_timestamp
1730 % + on unix the follwing is also an integer: owner_user_id, owner_group_id
1731
1732 :- public 'GET_DIRECTORY_PROPERTY'/3.
1733 'GET_DIRECTORY_PROPERTY'(S1,S2,PREDRES) :- 'DIRECTORY_PROPERTY'(S1,S2,PREDRES). % synonym as external function
1734 performs_io('DIRECTORY_PROPERTY').
1735 external_fun_type('DIRECTORY_PROPERTY',[],[string,string,boolean]).
1736 :- public 'DIRECTORY_PROPERTY'/3.
1737 :- block 'DIRECTORY_PROPERTY'(-,?,?), 'DIRECTORY_PROPERTY'(?,-,?).
1738 'DIRECTORY_PROPERTY'(string(A),string(P),BoolRes) :-
1739 dir_property2(A,P,BoolRes).
1740 :- block dir_property2(-,?,?), dir_property2(?,-,?).
1741 dir_property2(File,Prop,BoolRes) :-
1742 b_absolute_file_name(File,AFile),
1743 directory_property(AFile,Prop) -> BoolRes=pred_true ; BoolRes=pred_false.
1744
1745 performs_io('DIRECTORY_PROPERTY_VALUE').
1746 external_fun_type('DIRECTORY_PROPERTY_VALUE',[],[string,string,integer]).
1747 :- public 'DIRECTORY_PROPERTY_VALUE'/3.
1748 :- block 'DIRECTORY_PROPERTY_VALUE'(-,?,?), 'DIRECTORY_PROPERTY_VALUE'(?,-,?).
1749 'DIRECTORY_PROPERTY_VALUE'(string(A),string(P),int(R)) :-
1750 dir_property_val2(A,P,R).
1751 :- block dir_property_val2(-,?,?), dir_property_val2(?,-,?).
1752 dir_property_val2(File,Prop,Res) :-
1753 b_absolute_file_name(File,AFile),
1754 directory_property(AFile,Prop,Val) -> Res=Val
1755 ; add_error(external_functions,'Illegal DIRECTORY_PROPERTY',Prop), Res=int(-1).
1756 % --------------------------------
1757
1758 % I/O
1759
1760
1761 % printf as predicate; can also be used as a function to BOOL
1762 expects_spaninfo('fprintf').
1763 external_pred_always_true('fprintf').
1764 :- public fprintf/5.
1765 :- block fprintf(-,?,?,?,?), fprintf(?,-,?,?,?), fprintf(?,?,-,?,?).
1766 fprintf(string(File),string(FormatString),Value,PredRes,Span) :- !, PredRes = pred_true,
1767 when((ground(FormatString),ground(Value)),
1768 fprintf2(File,FormatString,Value,Span)).
1769 fprintf(File,F,V,P,S) :- add_internal_error('Illegal call: ',fprintf(File,F,V,P,S)), P=pred_true.
1770
1771 expects_spaninfo('printf_opt_trace').
1772 external_pred_always_true('printf_opt_trace').
1773 :- public printf_opt_trace/5.
1774 :- block printf_opt_trace(-,?,?,?,?), printf_opt_trace(?,-,?,?,?).
1775 printf_opt_trace(string(FormatString),Value,Trace,PredRes,Span) :- !, PredRes = pred_true,
1776 when((ground(FormatString),ground(Value)),
1777 (fprintf2(user_output,FormatString,Value,Span),
1778 (Trace==pred_true -> try_trace ; true)
1779 )
1780 ).
1781 printf_opt_trace(F,V,T,P,S) :- add_internal_error('Illegal call: ',printf_opt_trace(F,V,T,P,S)), P=pred_true.
1782
1783 % try to perform trace commend if we are not in compiled version
1784 try_trace :-
1785 catch(trace, error(existence_error(_,_),_), (
1786 format('Cannot trace into source code in compiled version of ProB!~n<<<Type RETURN-Key to continue>>>',[]),
1787 read_line(user_input,_),nl
1788 )).
1789
1790 expects_spaninfo('printf').
1791 external_pred_always_true('printf').
1792 external_fun_type('printf',[T],[string,seq(T),boolean]).
1793
1794 :- assert_must_succeed(external_functions:printf(string('test ok = ~w~n'),[(int(1),pred_true)],pred_true,unknown)).
1795 :- block printf(-,?,?,?), printf(?,-,?,?).
1796 printf(string(FormatString),Value,PredRes,Span) :- !, PredRes = pred_true,
1797 when((ground(FormatString),ground(Value)),
1798 fprintf2(user_output,FormatString,Value,Span)).
1799 printf(F,V,P,S) :- add_internal_error('Illegal call: ',printf(F,V,P,S)), P=pred_true.
1800
1801 expects_spaninfo('printf_two'). % print two values, triggers as soon as first value is known
1802 external_pred_always_true('printf_two').
1803 :- assert_must_succeed(external_functions:printf_two(string('test ok = ~w~n'),[(int(1),pred_true)],string('test ok = ~w~n'),[(int(1),pred_true)],pred_true,unknown)).
1804 :- public printf_two/6.
1805 :- block printf_two(-,?,?,?,?,?), printf_two(?,-,?,?,?,?).
1806 printf_two(string(FormatString),Value,string(FormatString2),Value2,PredRes,Span) :- !, PredRes = pred_true,
1807 when((ground(FormatString),ground(Value)),
1808 (fprintf2(user_output,FormatString,Value,Span),
1809 fprintf2(user_output,FormatString2,Value2,Span))).
1810 printf_two(F,V,F2,V2,P,S) :- add_internal_error('Illegal call: ',printf_two(F,V,F2,V2,P,S)), P=pred_true.
1811
1812
1813 expects_spaninfo('printf_nonvar'). % print as soon as value becomes nonvar (printf waits until the value is ground)
1814 external_pred_always_true('printf_nonvar').
1815 :- public printf_nonvar/4.
1816 :- block printf_nonvar(-,?,?,?), printf_nonvar(?,-,?,?).
1817 printf_nonvar(string(FormatString),Value,PredRes,Span) :- !, PredRes = pred_true,
1818 when((ground(FormatString),nonvar(Value)),
1819 fprintf2(user_output,FormatString,Value,Span)).
1820 printf_nonvar(F,V,P,S) :- add_internal_error('Illegal call: ',printf(F,V,P,S)), P=pred_true.
1821
1822
1823 expects_spaninfo('dprintf'). % a version of printf which delays setting itself to TRUE until printing is performed
1824 external_pred_always_true('dprintf').
1825 :- public dprintf/4.
1826 :- block dprintf(-,?,?,?), dprintf(?,-,?,?).
1827 dprintf(string(FormatString),Value,PredRes,Span) :- !,
1828 when((ground(FormatString),ground(Value)),
1829 (fprintf2(user_output,FormatString,Value,Span),PredRes = pred_true)).
1830 dprintf(F,V,P,S) :- add_internal_error('Illegal call: ',dprintf(F,V,P,S)), P=pred_true.
1831
1832 :- use_module(kernel_strings,[convert_b_sequence_to_list_of_atoms/3]).
1833 fprintf2(File,FormatString,Value,Span) :-
1834 convert_b_sequence_to_list_of_atoms(Value,ListOfAtoms,Done),
1835 when(nonvar(Done),
1836 (file_format(File,FormatString,ListOfAtoms,Span),
1837 print_hash((FormatString,Value)),
1838 print_stats,
1839 fprint_log_info(File,Span)
1840 )).
1841 %fprintf2(File,FormatString,Value,Span) :- print('BACKTRACKING ') , file_format(File,FormatString,['?'],Span),nl,fail.
1842 % warning: format can call an argument as goal with ~@; this is dangerous
1843 % and we should prohibit this
1844 % Luckily PRINTF("@: <>~@<>~n","print(danger)") where print(danger)
1845 % is arbitrary code is not a security exploit:
1846 % our PRINTF translates the argument to an atom, i.e., one could
1847 % only call Prolog predicates without arguments, anything else leads to an exception
1848 % (even PRINTF("@: <>~@<>~n","nl") leads to an exception)
1849
1850
1851 :- use_module(hashing,[my_term_hash/2]).
1852 % optionally print hash and allow breakpoints
1853 print_hash(V) :-
1854 external_fun_pref(printf_hash,'TRUE'), % use SET_PREF("printf_hash","TRUE")
1855 !,
1856 my_term_hash(V,H), format('% HASH = ~w~n',H),
1857 %((H = 158201315 ; H=29759067) -> trace ; true),
1858 true.
1859 print_hash(_).
1860
1861
1862 :- use_module(probsrc(tools),[statistics_memory_used/1]).
1863 :- dynamic nr_of_printfs/1.
1864 nr_of_printfs(0).
1865 print_stats :-
1866 external_fun_pref(printf_stats,PFS), % use SET_PREF("printf_stats","TRUE")
1867 PFS='TRUE',
1868 retract(nr_of_printfs(N)),
1869 !,
1870 N1 is N+1,
1871 assertz(nr_of_printfs(N1)),
1872 statistics(walltime,[X,SL]),
1873 statistics_memory_used(M), MB is M / 1000000, % used instead of deprecated 1048576,
1874 statistics(gc_count,GCs),
1875 format('% Call ~w at walltime ~w ms (since last ~w ms), memory ~3f MB (~w GCs)~n',[N1,X,SL,MB,GCs]).
1876 print_stats.
1877
1878 :- dynamic external_fun_pref/2.
1879 % valid keys: log_info
1880 valid_external_fun_pref(log_info).
1881 valid_external_fun_pref(printf_stats).
1882 valid_external_fun_pref(printf_hash).
1883
1884 fprint_log_info(File,Span) :- external_fun_pref(log_info,X),
1885 'GET_INFO'(string(X),string(Res)),
1886 file_format(File,'%%% ~w~n',[Res],Span).
1887 fprint_log_info(_,_).
1888
1889 % example usage SET_PREF("log_info","time") or SET_PREF("printf_stats","TRUE")
1890 external_fun_type('SET_PREF',[],[string,string,boolean]).
1891 :- public 'SET_PREF'/3.
1892 :- block 'SET_PREF'(-,?,?), 'SET_PREF'(?,-,?).
1893 'SET_PREF'(string(S),string(Val),R) :-
1894 preferences:eclipse_preference(S,Pref),!, R=pred_true,
1895 format('Setting ProB preference ~w := ~w~n',[S,Val]),
1896 preferences:set_preference(Pref,Val).
1897 'SET_PREF'(string(S),string(Val),R) :- valid_external_fun_pref(S),!,
1898 R=pred_true,
1899 retractall(external_fun_pref(S,_)),
1900 format('Setting external function preference ~w := ~w~n',[S,Val]),
1901 assertz(external_fun_pref(S,Val)).
1902 'SET_PREF'(P,V,R) :-
1903 add_internal_error('Illegal call: ','SET_PREF'(P,V,R)), R=pred_false.
1904
1905 external_fun_type('GET_PREF',[],[string,string]).
1906 expects_waitflag('GET_PREF').
1907 expects_spaninfo('GET_PREF').
1908 :- assert_must_succeed(external_functions:'GET_PREF'(string('CLPFD'),string(_),unknown,_)).
1909 :- public 'GET_PREF'/4.
1910 'GET_PREF'(Str,Res,Span,WF) :-
1911 kernel_waitflags:get_wait_flag(10,'GET_PREF',WF,WF10), % will enumerate possible input strings
1912 get_pref2(Str,Res,_,WF10,Span).
1913 external_fun_type('GET_PREF_DEFAULT',[],[string,string]).
1914 expects_waitflag('GET_PREF_DEFAULT').
1915 expects_spaninfo('GET_PREF_DEFAULT').
1916 :- assert_must_succeed(external_functions:'GET_PREF_DEFAULT'(string('CLPFD'),string(true),unknown,_)).
1917 :- public 'GET_PREF_DEFAULT'/4.
1918 'GET_PREF_DEFAULT'(Str,Res,Span,WF) :-
1919 (nonvar(Str) -> true
1920 ; kernel_waitflags:get_wait_flag(10,'GET_PREF',WF,WF10)), % will enumerate possible input strings
1921 get_pref2(Str,_,Res,WF10,Span).
1922
1923 :- block get_pref2(-,?,?,-,?).
1924 get_pref2(string(S),Res,Res2,_,Span) :-
1925 if((preferences:eclipse_preference(S,Pref),
1926 preferences:get_preference(Pref,Val),
1927 preferences:preference_default_value(Pref,DefVal)),
1928 (make_string(Val,Res),make_string(DefVal,Res2)),
1929 (add_error(external_functions,'Illegal argument for GET_PREF: ',S,Span),
1930 fail)).
1931
1932
1933 % printf followed by fail; useful for print fail loops in the REPL
1934 expects_spaninfo('printfail').
1935 :- assert_must_fail(external_functions:printfail(string('test ok = ~w~n'),[(int(1),pred_true)],pred_true,unknown)).
1936 :- block printfail(-,?,?,?), printfail(?,-,?,?).
1937 printfail(string(FormatString),Value,PredRes,Span) :- !, PredRes = pred_true,
1938 when((ground(FormatString),ground(Value)),
1939 (fprintf2(user_output,FormatString,Value,Span),fail)).
1940 printfail(F,V,P,S) :-
1941 add_internal_error('Illegal call: ',printfail(F,V,P,S)), P=pred_true.
1942
1943 % a version of printf with automatic indenting and backtracking feedback
1944 expects_spaninfo('iprintf').
1945 external_pred_always_true('iprintf').
1946 :- assert_must_succeed(external_functions:iprintf(string('test ok = ~w~n'),[(int(1),pred_true)],pred_true,unknown)).
1947 :- block iprintf(-,?,?,?), iprintf(?,-,?,?).
1948 iprintf(string(FormatString),Value,PredRes,Span) :- !, PredRes = pred_true,
1949 when((ground(FormatString),ground(Value)),
1950 ifprintf2(user_output,FormatString,Value,no_trace,Span)).
1951 iprintf(F,V,P,S) :- add_internal_error('Illegal call: ',iprintf(F,V,P,S)), P=pred_true.
1952 ifprintf2(File,FormatString,Value,Trace,Span) :-
1953 my_term_hash((FormatString,Value),Hash),
1954 format(user_output,'[hash ~w] ',[Hash]), % (Hash=1087266573122589201 -> (trace ; trace,fail) ; true),
1955 translate:translate_bvalue(Value,TV),
1956 indent_format(File,FormatString,[TV],Trace),
1957 fprint_log_info(File,Span).
1958 expects_spaninfo('itprintf').
1959 external_pred_always_true('itprintf').
1960 :- public itprintf/4.
1961 :- block itprintf(-,?,?,?), itprintf(?,-,?,?).
1962 itprintf(string(FormatString),Value,PredRes,Span) :- PredRes = pred_true,
1963 when((ground(FormatString),ground(Value)),
1964 ifprintf2(user_output,FormatString,Value,trace,Span)).
1965
1966 % ---------------
1967
1968 % a more light-weight version of observe_indent below
1969 :- public observe/5.
1970 expects_spaninfo('observe').
1971 expects_unevaluated_args('observe').
1972 expects_waitflag('observe').
1973 external_pred_always_true('observe').
1974 external_fun_type('observe',[T],[T,boolean]).
1975 observe(Value,PredRes,[Arg],Span,WF) :-
1976 observe6(Value,PredRes,[Arg],Span,_,WF).
1977
1978 % a version which does not print instantiations; just registers them and the patterns
1979 % can be inspected later with -prob-profile (calling portray_instantiations)
1980 :- public observe_silent/5.
1981 expects_spaninfo('observe_silent').
1982 expects_unevaluated_args('observe_silent').
1983 expects_waitflag('observe_silent').
1984 external_pred_always_true('observe_silent').
1985 external_fun_type('observe_silent',[T],[T,boolean]).
1986 observe_silent(Value,PredRes,[Arg],Span,WF) :-
1987 observe6(Value,PredRes,[Arg],Span,silent,WF).
1988
1989 observe6(Value,PredRes,[Arg],_Span,IndentVar,WF) :-
1990 observe_couples(Value,Arg,IndentVar,WF),
1991 PredRes=pred_true,
1992 (Arg\=b(couple(_,_),_,_)
1993 -> true
1994 ; translate_bexpression(Arg,AS),
1995 ground_value_check(Value,GrVal),
1996 block_print_value_complete(GrVal,AS,Value,IndentVar,WF)
1997 ).
1998
1999 observe_couples((V1,V2),b(couple(A1,A2),_,_),IndentVar,WF) :- !,
2000 observe_couples(V1,A1,IndentVar,WF),
2001 observe_couples(V2,A2,IndentVar,WF).
2002 observe_couples(Val,Arg,IndentVar,WF) :-
2003 translate_bexpression(Arg,ArgString),
2004 (IndentVar==silent -> true ; format(user_output,' observing ~w~n',[ArgString])), % for values we could print_span
2005 ground_value_check(Val,GrVal),
2006 block_print_value(GrVal,ArgString,Val,IndentVar,WF).
2007
2008 :- block block_print_value(-,?,?,?,?).
2009 block_print_value(_,ArgString,V,IndentVar,WF) :-
2010 print_value(ArgString,V,IndentVar,WF).
2011 print_value(ArgString,V,IndentVar,WF) :-
2012 register_instantiation_wf(ArgString,WF),
2013 (IndentVar==silent -> true
2014 ; translate_bvalue(V,VS), statistics(walltime,[WT,_]),
2015 get_wf_summary(WF,WS),
2016 indent_var(IndentVar),
2017 format(user_output,' ~w = ~w (walltime: ~w ms) ~w~n',[ArgString,VS,WT,WS])
2018 %,set_prolog_flag(profiling,on), print_profile
2019 ).
2020 :- block block_print_value_complete(-,?,?,?,?).
2021 block_print_value_complete(_,ArgString,V,IndentVar,WF) :- print_value_complete(ArgString,V,IndentVar,WF).
2022 print_value_complete(ArgString,V,IndentVar,WF) :-
2023 register_instantiation_wf(ArgString,WF),
2024 (IndentVar==silent -> true
2025 ; translate_bvalue(V,VS), statistics(walltime,[WT,_]),
2026 get_wf_summary(WF,WS),
2027 indent_var(IndentVar),
2028 format(user_output,'* Value complete: ~w = ~w (walltime: ~w ms) ~w~n------~n',[ArgString,VS,WT,WS])
2029 %,set_prolog_flag(profiling,on), print_profile,trace
2030 ).
2031 % TODO: determine indentation based on overall instantiation of full value
2032
2033 :- use_module(kernel_waitflags,[get_minimum_waitflag_prio/3]).
2034 get_wf_summary(WF,R) :- debug_mode(on),get_minimum_waitflag_prio(WF,MinPrio,_Info),!, R=MinPrio.
2035 get_wf_summary(_,'').
2036
2037 % TODO: store indent var in WF store; so that we can share results/indentation amongst multiple observes
2038 % indent based upon a shared variable and increment it; it displays indentation locally for every observe call
2039 % using put_wf_dynamic_info we could display it for every WF store
2040 indent_var(X) :- var(X),!, X=inst(_). %, register_instantiation(ArgStr,Pred,Level).
2041 indent_var(inst(X)) :- !,print('.'), indent_var(X).
2042 indent_var(_) :- print('***').
2043
2044 % a small utility to observe list of atomic variable names with Prolog value terms
2045 % can be used on Ids,Vars for calls to set_up_localstate(Ids,Vars,LocalState,LetState)
2046 :- public observe_variables/2. %useful for debugging
2047 observe_variables(ListOfIDs,ListOfVals) :- observe_variables(ListOfIDs,ListOfVals,_).
2048 observe_variables([],[],_).
2049 observe_variables([TID|T],[Val|TV],IndentVar) :-
2050 (atomic(TID) -> ID=TID ; get_texpr_id(TID,ID) -> true ; ID=TID),
2051 ground_value_check(Val,GrVal),
2052 block_print_value(GrVal,ID,Val,IndentVar,no_wf_available),
2053 observe_variables(T,TV,IndentVar).
2054
2055 :- dynamic instantiation_link/4, instantiation_level_reached/1.
2056 % keep track of how variables are instantiated in which order
2057 register_instantiation(ArgStr,Pred,Level) :-
2058 (instantiation_level_reached(Level) -> true ; assertz(instantiation_level_reached(Level))),
2059 (retract(instantiation_link(Pred,ArgStr,Level,Hits))
2060 -> H1 is Hits+1
2061 ; H1 is 1),
2062 assertz(instantiation_link(Pred,ArgStr,Level,H1)).
2063
2064 :- use_module(probsrc(preferences), [get_preference/2]).
2065 register_instantiation_wf(ArgInstantiated,WF) :-
2066 (get_wf_dynamic_info(WF,instantiation_info,lvl_prev(Level,PrevArgInstantiated))
2067 -> true
2068 ; Level=0,
2069 (get_preference(provide_trace_information,false)
2070 -> Infos=[] % only have one virtual root
2071 ; get_wait_flag_infos(WF,Infos) %portray_wait_flag_infos(Infos),
2072 % Warning: these Infos can be large terms which get asserted below; they contain the call-stack
2073 ),
2074 PrevArgInstantiated = root(Infos)
2075 ),
2076 register_instantiation(ArgInstantiated,PrevArgInstantiated,Level),
2077 L1 is Level+1,
2078 put_wf_dynamic_info(WF,instantiation_info,lvl_prev(L1,ArgInstantiated)).
2079
2080 reset_observe :- retractall(instantiation_level_reached(_)),
2081 retractall(instantiation_link(_,_,_,_)).
2082
2083 portray_instantiations :-
2084 (instantiation_level_reached(0) -> true),
2085 format('--- ProB instantiation patterns observed ---~n',[]),
2086 instantiation_link(root(Infos),_,0,_),
2087 format('*PATTERNS*~n',[]),
2088 portray_wait_flag_infos(Infos),
2089 (Infos=[],get_preference(provide_trace_information,false)
2090 -> format(' (Set TRACE_INFO preference to TRUE to obtain more information.)~n',[])
2091 ; true),
2092 portray_inst(0,root(Infos)),
2093 fail.
2094 portray_instantiations.
2095
2096 % portray how the instantiations occurred
2097 portray_inst(Level,ArgStr) :-
2098 instantiation_link(ArgStr,Successor,Level,Hits),
2099 i_indent(Level), format(' ~w hits : ~w~n',[Hits,Successor]),
2100 L1 is Level+1,
2101 portray_inst(L1,Successor).
2102
2103 i_indent(X) :- X < 1, !, write('->').
2104 i_indent(X) :- write('-+'), X1 is X-1, i_indent(X1).
2105
2106 % ---------------
2107
2108 :- public observe_indent/5.
2109 expects_spaninfo('observe_indent').
2110 expects_unevaluated_args('observe_indent').
2111 expects_waitflag('observe_indent').
2112 external_pred_always_true('observe_indent').
2113 external_fun_type('observe_indent',[T],[T,boolean]).
2114 % observe pairs of values
2115 observe_indent(Value,PredRes,UnEvalArgs,Span,WF) :-
2116 observe2(Value,PredRes,UnEvalArgs,no_trace,Span,WF).
2117
2118 :- public tobserve/5.
2119 expects_spaninfo('tobserve'). % observe_indent but with tracing enabled
2120 expects_unevaluated_args('tobserve').
2121 expects_waitflag('tobserve').
2122 external_pred_always_true('tobserve').
2123 tobserve(Value,PredRes,UnEvalArgs,Span,WF) :-
2124 observe2(Value,PredRes,UnEvalArgs,trace,Span,WF).
2125
2126 observe2(Value,PredRes,[Arg],Trace,Span,WF) :- PredRes=pred_true,
2127 %kernel_waitflags:portray_waitflags(WF),
2128 kernel_waitflags:get_wait_flag0(WF,WF0),
2129 kernel_waitflags:get_wait_flag1(observe,WF,WF1),
2130 when(nonvar(WF0),(indent_format(user_output,'WAITFLAG 0 set~n',[],no_trace),kernel_waitflags:portray_waitflags(WF))),
2131 when(nonvar(WF1),(indent_format(user_output,'WAITFLAG 1 set~n',[],no_trace),kernel_waitflags:portray_waitflags(WF))),
2132 Hook = print_value_as_table_if_possible(Arg,Value),
2133 observe_aux(Value,Arg,1,_,Trace,Span,Hook),
2134 iprintf(string("observe full value complete: ~w~n~n"),Value,_,Span).
2135
2136 :- use_module(extrasrc(table_tools),[print_value_as_table/2]).
2137 :- public print_value_as_table_if_possible/2. % used as hook above
2138 %print_value_as_table_if_possible(_,_) :- !.
2139 print_value_as_table_if_possible(Arg,Value) :-
2140 translate:print_bexpr(Arg),nl,
2141 (print_value_as_table(Arg,Value) -> true ; true).
2142
2143 observe_aux((V1,V2),b(couple(A1,A2),_,_),Nr,R,Trace,Span,Hook) :- !,
2144 observe_aux(V1,A1,Nr,N1,Trace,Span,Hook),
2145 observe_aux(V2,A2,N1,R,Trace,Span,Hook).
2146 observe_aux(V,Arg,Nr,R,Trace,Span,Hook) :- R is Nr+1,
2147 translate:translate_bexpression(Arg,ArgString), %print(obs(Nr,ArgString)),nl,
2148 atom_codes(ArgString,ArgCodes),
2149 observe_value(V,ArgCodes,Nr,Trace,Span,Hook).
2150
2151 % entry for other modules:
2152 observe_value(Value,Info) :- (Info=[_|_] -> PCodes = Info ; atom_codes(Info,PCodes)),
2153 observe_value(Value,PCodes,1,no_trace,unknown,true).
2154
2155 observe_value(Value,ArgCodes,Nr,Trace,Span,Hook) :- %print(obs(Nr,ArgString)),nl,
2156 number_codes(Nr,NrCodes), append(NrCodes,") = ~w~n",Tail1), append(" (",Tail1,Tail2),
2157 append(ArgCodes,Tail2,FormatString),
2158 observe_set(Value,ArgCodes,1,Trace,Span,Value,Hook),
2159 when((ground(FormatString),ground(Value)),ifprintf2(user_output,FormatString,Value,Trace,Span)).
2160 observe_value_with_full_value(Value,ArgCodes,Nr,Trace,Span,FullValue,Hook) :- %print(obs(Nr,ArgString)),nl,
2161 number_codes(Nr,NrCodes), append(NrCodes,"):FULL = ~w~n",Tail1), append(" (",Tail1,Tail2),
2162 append(ArgCodes,Tail2,FormatString),
2163 observe_set(Value,ArgCodes,1,Trace,Span,Value,Hook),
2164 when((ground(FormatString),ground(Value)),
2165 observe_ground(FormatString,Value,FullValue,Trace,Span,Hook)).
2166
2167 observe_ground(FormatString,Value,FullValue,Trace,Span,Hook) :-
2168 ifprintf2(user_output,FormatString,rec([field(value,Value),field(full,FullValue)]),Trace,Span),
2169 (call(Hook) -> true ; print(hook_failed(Hook)),nl).
2170
2171
2172
2173 % observe sets and records:
2174 :- block observe_set(-,?,?,?,?,?,?).
2175 observe_set([],_ArgCodes,_,_Trace,_Span,_,_) :- !.
2176 observe_set([Value|T],ArgCodes,Pos,Trace,Span,FullValue,Hook) :- !, %print(obs(Value,Pos)),nl,
2177 append(ArgCodes," el -> ",ArgN),
2178 observe_value_with_full_value(Value,ArgN,Pos,Trace,Span,FullValue,Hook),
2179 %tools_files:put_codes(ArgN,user_output),print(Pos),print(' = '),tools_printing:print_arg(Value),nl,
2180 P1 is Pos+1, observe_set(T,ArgCodes,P1,Trace,Span,FullValue,Hook).
2181 observe_set((V1,V2),ArgCodes,Pos,Trace,Span,FullValue,Hook) :-
2182 preferences:preference(observe_precise_values,true),
2183 !, %print(obs(Value,Pos)),nl,
2184 append(ArgCodes," prj1 -> ",ArgN1),
2185 observe_value_with_full_value(V1,ArgN1,Pos,Trace,Span,FullValue,Hook),
2186 %tools_files:put_codes(ArgN,user_output),print(Pos),print(' = '),tools_printing:print_arg(Value),nl,
2187 Pos2 is Pos+1,
2188 append(ArgCodes," prj2 -> ",ArgN2),
2189 observe_value_with_full_value(V2,ArgN2,Pos2,Trace,Span,FullValue,Hook).
2190 observe_set(rec(Fields),ArgCodes,Pos,Trace,Span,_FullValue,Hook) :-
2191 preferences:preference(observe_precise_values,true),
2192 !,
2193 append(ArgCodes," rec -> ",ArgN),
2194 observe_field(Fields,ArgN,Pos,Trace,Span,Hook).
2195 observe_set(_,_,_,_,_,_,_).
2196
2197 :- block observe_field(-,?,?,?,?,?).
2198 observe_field([],ArgN,Pos,Trace,Span,_Hook) :-
2199 append(ArgN," complete (~w)~n",FormatString),
2200 ifprintf2(user_output,FormatString,Pos,Trace,Span).
2201 observe_field([field(Name,Value)|TFields],ArgN,Pos,Trace,Span,Hook) :-
2202 observe_value((string(Name),Value),ArgN,Pos,Trace,Span,Hook),
2203 observe_field(TFields,ArgN,Pos,Trace,Span,Hook).
2204
2205 :- use_module(bsyntaxtree,[get_texpr_id/2]).
2206 :- use_module(store,[lookup_value_with_span_wf/6]).
2207 % utility function for other modules to use observe on parameters
2208 observe_parameters(Parameters,LocalState) :-
2209 skel(LocalState,SetupDone),
2210 reset_ident, reset_walltime,
2211 when(nonvar(SetupDone),observe_parameters_aux(Parameters,1,LocalState)).
2212 :- block skel(-,?).
2213 skel([],pred_true).
2214 skel([_|T],Done) :- skel(T,Done).
2215 :- block observe_parameters_aux(-,?,?), observe_parameters_aux(?,?,-).
2216 observe_parameters_aux([],_,_).
2217 observe_parameters_aux([TID|T],Nr,LS) :-
2218 safe_get_texpr_id(TID,ID), atom_codes(ID,PCodes),
2219 lookup_value_with_span_wf(ID,[],LS,Value,TID,no_wf_available),
2220 debug_println(9,observing(ID,Value,LS)),
2221 Hook = print_value_as_table_if_possible(TID,Value),
2222 observe_value(Value,PCodes,Nr,no_trace,unknown,Hook),
2223 N1 is Nr+1,
2224 observe_parameters_aux(T,N1,LS).
2225 safe_get_texpr_id(TID,ID) :- (atom(TID) -> ID=TID ; get_texpr_id(TID,ID)).
2226
2227 construct_bind(Id,V,bind(Id,V)).
2228 % observe a list of identifiers and values
2229 :- public observe_state/2. % debugging utility
2230 observe_state(Ids,Values) :-
2231 maplist(construct_bind,Ids,Values,State),!,
2232 observe_state(State).
2233 observe_state(Ids,Values) :- add_internal_error('Illegal id and value lists: ',observe_state(Ids,Values)).
2234
2235 % utility to observe a state using the observe external function
2236 observe_state(State) :-
2237 reset_ident, reset_walltime,
2238 observe_state_aux(State,1).
2239 :- block observe_state_aux(-,?).
2240 observe_state_aux(no_state,_) :- !.
2241 observe_state_aux([],_) :- !.
2242 observe_state_aux(concrete_constants(C),Nr) :- !, observe_state_aux(C,Nr).
2243 observe_state_aux([Binding|T],Nr) :- get_binding_value(Binding,Nr,PCodes,Value),!,
2244 %print(observe(Id,Value,Nr,T)),nl,
2245 observe_value(Value,PCodes,Nr,no_trace,unknown,true),
2246 N1 is Nr+1,
2247 observe_state_aux(T,N1).
2248 observe_state_aux(State,Nr) :- add_internal_error('Illegal state: ',observe_state_aux(State,Nr)).
2249
2250 :- block get_binding_value(-,?,?,?).
2251 get_binding_value(bind(Id,Value),_,PCodes,Value) :- atom_codes(Id,PCodes).
2252 get_binding_value(typedval(Value,_Type,Id,_Trigger),_,PCodes,Value) :- atom_codes(Id,PCodes).
2253 get_binding_value(Value,Nr,PCodes,Value) :- number_codes(Nr,PCodes). % we have just a list of values without ids
2254
2255
2256 external_fun_type('observe_fun',[X],[X,boolean]).
2257 expects_unevaluated_args('observe_fun').
2258 external_pred_always_true('observe_fun').
2259 :- public observe_fun/3.
2260 % a specific predicate to observe enumeration of functions,...
2261 :- block observe_fun(-,-,?).
2262 observe_fun(Value,PredRes,[UnEvalArg]) :-
2263 translate:translate_bexpression(UnEvalArg,Str), format('Observe function : ~w~n',[Str]),
2264 obs_fun(Value,Str,Value),PredRes=pred_true.
2265
2266 :- block obs_fun(-,?,?).
2267 obs_fun([],_,_) :- !.
2268 obs_fun([(A,B)|T],Str,FullVal) :- !,
2269 obs_idx(A,B,Str,FullVal),
2270 obs_fun(T,Str,FullVal).
2271 obs_fun(V,Str,_) :- print(uncovered_obs_fun(V,Str)),nl.
2272
2273 :- block obs_idx(-,?,?,?), obs_idx(?,-,?,?).
2274 obs_idx(A,B,Str,FullVal) :-
2275 when(ground((A,B)),obs_idx_complete(FullVal,A,B,Str)).
2276
2277 obs_idx_complete(FullVal,A,B,Str) :-
2278 format('~n ~w = ',[Str]),obs_idx_complete_aux(FullVal,A,B).
2279 obs_idx_complete(FullVal,A,B,Str) :-
2280 format('~n [BACKTRACK] ~w = ',[Str]),obs_idx_complete_aux(FullVal,A,B),fail.
2281
2282 obs_idx_complete_aux(V,_,_) :- var(V),!,print(' OPEN '),nl.
2283 obs_idx_complete_aux([],_,_) :- !, nl.
2284 obs_idx_complete_aux([(X,Y)|T],A,B) :- !,
2285 ((X,Y)==(A,B) -> print(' * ') ; print(' ')), print_bvalue((X,Y)),
2286 obs_idx_complete_aux(T,A,B).
2287 obs_idx_complete_aux(_,_,_) :- print(unknown),nl.
2288
2289
2290 % -----------------------------
2291
2292 :- public tprintf/4.
2293 expects_spaninfo('tprintf').
2294 external_pred_always_true('tprintf').
2295 % a debugging version that switches into trace mode
2296 :- block tprintf(-,?,?,?), tprintf(?,-,?,?).
2297 tprintf(string(FormatString),Value,PredRes,Span) :- PredRes = pred_true,
2298 when((ground(FormatString),ground(Value)),
2299 (fprintf2(user_output,FormatString,Value,Span),
2300 try_trace %,print_profile,set_prolog_flag(profiling,on)
2301 )).
2302
2303 :- public 'prolog_printf'/5.
2304 expects_spaninfo('prolog_printf').
2305 expects_waitflag('prolog_printf').
2306 external_pred_always_true('prolog_printf').
2307 prolog_printf(string(FormatString),Value,PredRes,Span,WF) :- PredRes = pred_true,
2308 file_format(user_output,FormatString,[initial(Value,WF)],Span),
2309 when(nonvar(Value),file_format(user_output,FormatString,[nonvar(Value,WF)],Span)),
2310 when((ground(FormatString),ground(Value)),
2311 fprintf2(user_output,FormatString,Value,Span)).
2312
2313 % vprintf: expression which returns argument as value
2314 expects_spaninfo('vprintf').
2315 external_fun_type('vprintf',[T],[string,T,T]).
2316 :- public vprintf/4.
2317 vprintf(Format,Value,ValueRes,Span) :-
2318 printf(Format,[(int(1),Value)],pred_true,Span), % use itprintf for tracing
2319 equal_object(Value,ValueRes,vprintf). % we could generate a version which only instantiates when printing done
2320 expects_spaninfo('fvprintf').
2321 :- public fvprintf/5.
2322 fvprintf(File,Format,Value,ValueRes,Span) :-
2323 fprintf(File,Format,[(int(1),Value)],pred_true,Span),
2324 equal_object(Value,ValueRes,fvprintf). % we could generate a version which only instantiates when printing done
2325
2326
2327 % PRINT a single value as substitution
2328 performs_io('PRINT').
2329 external_subst_enabling_condition('PRINT',_,Truth) :- create_texpr(truth,pred,[],Truth).
2330 does_not_modify_state('PRINT').
2331 :- public 'PRINT'/3.
2332 :- block 'PRINT'(-,?,?), 'PRINT'(?,-,?).
2333 'PRINT'(Val,_Env,OutEnv) :- %print('PRINT : '), print(Env),nl,
2334 assert_side_effect_occurred(user_output),
2335 print_value(Val),nl, OutEnv=[].
2336
2337 % PRINT a single value as substitution; show backtracking
2338 performs_io('PRINT_BT').
2339 perform_directly('PRINT_BT').
2340 external_subst_enabling_condition('PRINT_BT',_,Truth) :- create_texpr(truth,pred,[],Truth).
2341 does_not_modify_state('PRINT_BT').
2342 :- public 'PRINT_BT'/3.
2343 :- block 'PRINT_BT'(-,?,?), 'PRINT_BT'(?,-,?).
2344 'PRINT_BT'(Val,_Env,OutEnv) :- %print('PRINT : '), print(Env),nl,
2345 assert_side_effect_occurred(user_output),
2346 print_value(Val),nl, OutEnv=[].
2347 'PRINT_BT'(Val,_Env,_OutEnv) :-
2348 assert_side_effect_occurred(user_output),
2349 print('BACKTRACKING: '),print_value(Val),nl, fail.
2350
2351 print_value(Val) :- translate:translate_bvalue(Val,TV), print(TV).
2352
2353
2354 performs_io('DEBUG_PRINT_STATE').
2355 external_subst_enabling_condition('DEBUG_PRINT_STATE',_,Truth) :- create_texpr(truth,pred,[],Truth).
2356 does_not_modify_state('DEBUG_PRINT_STATE').
2357 :- public 'DEBUG_PRINT_STATE'/3.
2358 :- block 'DEBUG_PRINT_STATE'(-,?,?).
2359 'DEBUG_PRINT_STATE'(Value,Env,OutEnv) :-
2360 assert_side_effect_occurred(user_output),
2361 print_value(Value),translate:print_bstate(Env),nl, OutEnv=[].
2362
2363 % PRINTF as substitution
2364 expects_spaninfo('PRINTF').
2365 performs_io('PRINTF').
2366 external_subst_enabling_condition('PRINTF',_,Truth) :- create_texpr(truth,pred,[],Truth).
2367 does_not_modify_state('PRINTF').
2368 :- public 'PRINTF'/5.
2369 :- block 'PRINTF'(-,?,?,?,?), 'PRINTF'(?,-,?,?,?), 'PRINTF'(?,?,-,?,?).
2370 'PRINTF'(string(FormatString),Value,_Env,OutEnvModifications,Span) :-
2371 % print('PRINTF'(FormatString,Value,_Env)),nl,
2372 when((ground(FormatString),ground(Value)),
2373 (fprintf2(user_output,FormatString,Value,Span),
2374 OutEnvModifications=[] /* substitution finished */
2375 )).
2376
2377 expects_spaninfo('FPRINTF').
2378 performs_io('FPRINTF').
2379 external_subst_enabling_condition('FPRINTF',_,Truth) :- create_texpr(truth,pred,[],Truth).
2380 does_not_modify_state('FPRINTF').
2381 :- public 'FPRINTF'/6.
2382 :- block 'FPRINTF'(-,?,?,?,?,?), 'FPRINTF'(?,-,?,?,?,?), 'FPRINTF'(?,?,-,?,?,?).
2383 'FPRINTF'(string(File),string(FormatString),Value,_Env,OutEnvModifications,Span) :-
2384 when((ground(FormatString),ground(Value)),
2385 (fprintf2(File,FormatString,Value,Span),
2386 OutEnvModifications=[] /* substitution finished */
2387 )).
2388
2389 file_format(user_output,FormatString,Args,Span) :- !,
2390 assert_side_effect_occurred(user_output),
2391 safe_call(myformat(user_output,FormatString,Args,Span),Span).
2392 file_format(File,FormatString,Args,Span) :-
2393 open(File,append,Stream,[encoding(utf8)]),
2394 assert_side_effect_occurred(file),
2395 safe_call(myformat(Stream,FormatString,Args,Span),Span),
2396 close(Stream). % TO DO: call_cleanup
2397
2398 % Simple check if the user forgot to put format specifiers in the format string.
2399 format_string_is_missing_tildes(FormatString) :-
2400 atom_codes(FormatString, Codes),
2401 \+ memberchk(0'~, Codes).
2402
2403 :- meta_predicate catch_format_error(0, 0).
2404 catch_format_error(Goal, Recover) :-
2405 catch(
2406 catch(
2407 Goal,
2408 error(consistency_error(_,_,format_arguments),_), % SICStus
2409 Recover),
2410 error(format(_Message),_), % SWI
2411 Recover).
2412
2413 :- public myformat/4.
2414 myformat(Stream,FormatString,Args,Span) :-
2415 catch_format_error(
2416 (Args \== [], format_string_is_missing_tildes(FormatString) ->
2417 % backup: the user has not provided ~w annotations:
2418 % instead print just the format string and then all arguments separately.
2419 % This case was previously detected by catching format errors,
2420 % but this causes problems with incomplete or duplicated output on SWI,
2421 % because SWI reports errors only during printing
2422 % (unlike SICStus, which checks the entire format string before printing anything).
2423 format(Stream,FormatString,[]),
2424 nl(Stream),
2425 format_args(Stream,Args)
2426 ; format(Stream,FormatString,Args)
2427 ),
2428 (length(Args,NrArgs),
2429 ajoin(['Illegal format string, expecting ',NrArgs,' ~w arguments (see SICStus Prolog reference manual for syntax):'],Msg),
2430 add_error(external_functions,Msg,FormatString,Span),
2431 format_args(Stream,Args))
2432 ),
2433 flush_output(Stream).
2434
2435 format_args(_Stream,[]).
2436 format_args(Stream,[H|T]) :- format(Stream,'~w~n',H), format_args(Stream,T).
2437
2438 % a format with indentation and backtracking info:
2439 :- dynamic indentation_level/1.
2440 indentation_level(0).
2441 inc_indent :- retract(indentation_level(X)), X1 is X+1, assertz(indentation_level(X1)).
2442 dec_indent :- retract(indentation_level(X)), X1 is X-1, assertz(indentation_level(X1)).
2443 reset_ident :- retractall(indentation_level(_)), assertz(indentation_level(0)).
2444 get_indent_level(L) :- indentation_level(LL), L is ceiling(sqrt(LL)).
2445 indent(Stream) :- get_indent_level(L), %(L>28 -> trace ; true),
2446 indent_aux(L,Stream).
2447 indent_aux(X,Stream) :- X < 1, !, write(Stream,' ').
2448 indent_aux(X,Stream) :- write(Stream,'+-'), X1 is X-1, indent_aux(X1,Stream).
2449
2450 indent_format(Stream,Format,Args,Trace) :- inc_indent,
2451 indent(Stream), format(Stream,Format,Args),
2452 print_walltime(Stream),
2453 % my_term_hash(Args,Hash), format(Stream,'[hash ~w]~n',[Hash]), (Hash=101755762 -> trace ; true), %%
2454 flush_output(Stream),
2455 (Trace=trace -> try_trace ; true).
2456 %indent_format(_Stream,_Format,Args,_Trace) :- my_term_hash(Args,Hash),(Hash=553878463258718990 -> try_trace).
2457 indent_format(Stream,Format,Args,Trace) :-
2458 indent(Stream), write(Stream,'BACKTRACKING '),
2459 % my_term_hash(Args,Hash), format(Stream,'[hash ~w] ',[Hash]), %% (Hash=553878463258718990 -> try_trace ; true), %%
2460 format(Stream,Format,Args),
2461 print_walltime(Stream), %% comment in to see walltime info
2462 flush_output(Stream),
2463 dec_indent,
2464 (Trace=trace -> try_trace ; true),
2465 fail.
2466
2467 :- dynamic ref_walltime/1, prev_walltime/1.
2468 reset_walltime :- retractall(prev_walltime(_)), retractall(ref_walltime(_)),
2469 statistics(walltime,[WT,_]),
2470 assertz(prev_walltime(WT)),
2471 assertz(ref_walltime(WT)).
2472 print_walltime(File) :- statistics(walltime,[WT,_]),
2473 (ref_walltime(RefWT) -> RWT is WT-RefWT ; RWT = 0, assertz(ref_walltime(WT))),
2474 (retract(prev_walltime(PWT)) -> T is WT-PWT, indent(File),format(File,' ~w ms (walltime; total ~w ms)~n',[T,RWT])
2475 ; true),
2476 assertz(prev_walltime(WT)).
2477 :- public 'TRACE'/2.
2478 :- block 'TRACE'(-,?).
2479 'TRACE'(pred_true,R) :- !,trace,R=pred_true.
2480 'TRACE'(pred_false,pred_true).
2481
2482 % --------------------------------------------
2483
2484 % ARGV, ARGC
2485
2486 :- dynamic argv_string/2, argc_number/1.
2487 argc_number(0).
2488 reset_argv :-
2489 retractall(argv_string(_,_)),
2490 retractall(argc_number(_)),
2491 assertz(argc_number(0)).
2492
2493 :- use_module(kernel_strings,[split_atom_string/3]).
2494 % call to set the commandline arguments, e.g., from probcli
2495 set_argv_from_atom(X) :-
2496 retractall(argv_string(_,_)),
2497 retractall(argc_number(_)),
2498 split_atom_string(X,' ',List),
2499 set_argv_from_list(List).
2500 set_argv_from_list(List) :-
2501 retractall(argv_string(_,_)),
2502 retractall(argc_number(_)),
2503 set_argv_from_list_aux(List).
2504 set_argv_from_list_aux(List) :-
2505 length(List,Len),
2506 assertz(argc_number(Len)),
2507 debug:debug_println(9,argc(Len)),
2508 nth1(N,List,String), % we number the arguments in B style
2509 debug:debug_println(9,argv(N,String)),
2510 assertz(argv_string(N,String)),
2511 fail.
2512 set_argv_from_list_aux(_).
2513
2514 external_fun_type('ARGV',[],[integer,string]).
2515 % access to the command-line arguments provided to probcli (after --)
2516 % first argument is ARGV(1) not ARGV(0)
2517 :- public 'ARGV'/2.
2518 :- block 'ARGV'(-,?).
2519 'ARGV'(int(N),S) :- argv2(N,S).
2520 :- block argv2(-,?).
2521 argv2(Nr,Res) :- % print(get_argv(Nr,Res)),nl,
2522 (argv_string(Nr,S) -> Res=string(S)
2523 ; Nr=0 -> add_error(external_functions,'Command-line argument does not exist, numbering starts at 1: ',Nr), Res=string('')
2524 ; add_error(external_functions,'Command-line argument does not exist: ',Nr), Res=string('')).
2525
2526 external_fun_type('ARGC',[],[integer]).
2527 :- public 'ARGC'/1.
2528 'ARGC'(int(X)) :- argc_number(X).
2529
2530 % --------------------------------------------
2531
2532 % RANDOM
2533
2534 :- assert_must_succeed(( external_functions:call_external_function('RANDOM',[0,1],[int(0),int(1)],int(0),integer,unknown,_WF) )).
2535 :- use_module(library(random),[random/3, random/1]).
2536 % Generate a random number >= Low and < Up
2537 % warning: this is not a mathematical function
2538 :- public 'RANDOM'/3.
2539 is_not_declarative('RANDOM').
2540 external_fun_type('RANDOM',[],[integer,integer,integer]).
2541 :- block 'RANDOM'(-,?,?), 'RANDOM'(?,-,?).
2542 'RANDOM'(int(Low),int(Up),int(R)) :- random2(Low,Up,R).
2543 :- block random2(-,?,?), random2(?,-,?).
2544 random2(L,U,R) :- random(L, U, R). % also works with reals
2545
2546 :- public 'RAND'/3.
2547 is_not_declarative('RAND').
2548 external_fun_type('RAND',[],[real,real,real]).
2549 :- block 'RAND'(-,?,?), 'RAND'(?,-,?).
2550 'RAND'(RLow,Rup,RR) :- is_real(RLow,Low),
2551 is_real(Rup,Up), is_real(RR,R),
2552 random2(Low,Up,R).
2553
2554
2555 % pick a random element from a set
2556 :- public 'random_element'/4.
2557 is_not_declarative('random_element').
2558 external_fun_type('random_element',[T],[set(T),T]).
2559 expects_waitflag('random_element').
2560 expects_spaninfo('random_element').
2561 :- block 'random_element'(-,?,?,?).
2562 random_element([],_,Span,WF) :- !,
2563 add_wd_error_span('random_element applied to empty set: ',[],Span,WF).
2564 random_element([H|T],El,_,WF) :- !,
2565 custom_explicit_sets:expand_custom_set_to_list_wf(T,ET,_Done,'random_element',WF),
2566 block_length(ET,1,Len),
2567 random_select_from_list([H|ET],Len,El).
2568 random_element(CS,Res,_,_) :- is_interval_closure_or_integerset(CS,Low,Up),!,
2569 U1 is Up+1,
2570 random(Low,U1,H), Res = int(H).
2571 random_element(CS,X,Span,WF) :-
2572 custom_explicit_sets:expand_custom_set_wf(CS,ER,random_element,WF),
2573 random_element(ER,X,Span,WF).
2574
2575 :- block block_length(-,?,?).
2576 block_length([],Acc,Acc).
2577 block_length([_|T],Acc,R) :- A1 is Acc+1, block_length(T,A1,R).
2578
2579 :- use_module(library(random),[random_member/2]).
2580 :- block random_select_from_list(?,-,?).
2581 random_select_from_list(List,_,Res) :-
2582 random_member(El,List),
2583 kernel_objects:equal_object(El,Res).
2584
2585 :- use_module(library(random),[random_numlist/4]).
2586 :- public 'random_numset'/6.
2587 is_not_declarative('random_numset').
2588 external_fun_type('random_numset',[],[integer,integer,integer,integer,set(integer)]).
2589 expects_waitflag('random_numset').
2590 :- block random_numset(-,?,?,?,?,?),random_numset(?,-,?,?,?,?),random_numset(?,?,-,?,?,?),random_numset(?,?,?,-,?,?).
2591 random_numset(int(P),int(Q),int(Low),int(Up),Res,WF) :-
2592 Prob is P/Q,
2593 random_numlist(Prob,Low,Up,List),
2594 maplist(gen_int,List,IntList),
2595 kernel_objects:equal_object_optimized_wf(IntList,Res,random_numset,WF).
2596
2597 gen_int(I,int(I)).
2598
2599
2600 :- public 'NORMAL'/3.
2601 is_not_declarative('NORMAL').
2602 external_fun_type('NORMAL',[],[integer,integer,integer]).
2603 % GAUSSIAN Distribution
2604 :- block 'NORMAL'(-,?,?), 'NORMAL'(?,-,?).
2605 'NORMAL'(int(Mu),int(Sigma),int(R)) :- random_normal(Mu,Sigma,R).
2606
2607 :- block random_normal(-,?,-), random_normal(?,-,?).
2608 random_normal(Mu,Sigma,R) :-
2609 random_normal(N),
2610 R is round(Mu+N*Sigma).
2611
2612 :- use_module(kernel_reals,[is_real/2]).
2613 :- public 'RNORMAL'/3.
2614 is_not_declarative('RNORMAL').
2615 external_fun_type('RNORMAL',[],[real,real,real]).
2616 :- block 'RNORMAL'(-,?,?), 'RNORMAL'(?,-,?).
2617 'RNORMAL'(RMU,RSigma,RR) :- is_real(RMU,MU),
2618 is_real(RSigma,Sigma), is_real(RR,R),
2619 random_normal_real(MU,Sigma,R).
2620
2621 :- block random_normal_real(-,?,-), random_normal_real(?,-,?).
2622 random_normal_real(Mu,Sigma,R) :-
2623 random_normal(N),
2624 R is (Mu+N*Sigma).
2625
2626 % inspired by: https://stackoverflow.com/questions/44503752/how-to-generate-normal-distributed-random-numbers-in-prolog
2627 % https://en.wikipedia.org/wiki/Box–Muller_transform
2628 :- dynamic cached_gauss/1.
2629 :- use_module(library(random),[random/1]).
2630 random_normal(R) :- retract(cached_gauss(N)),!,R=N.
2631 random_normal(R) :-
2632 random(U1), random(U2),
2633 Z0 is sqrt(-2 * log(U1)) * cos(2*pi*U2),
2634 Z1 is sqrt(-2 * log(U1)) * sin(2*pi*U2),
2635 assertz(cached_gauss(Z1)),
2636 R = Z0.
2637
2638 % generates a random subset of a finite set
2639 :- public 'random_subset'/4.
2640 is_not_declarative('random_subset').
2641 external_fun_type('random_subset',[T],[set(T),set(T)]).
2642 expects_waitflag('random_subset').
2643 expects_spaninfo('random_subset').
2644 :- block 'random_subset'(-,?,?,?).
2645 random_subset(Set,Subset,Span,WF) :- !,
2646 custom_explicit_sets:expand_custom_set_to_list_wf(Set,ESet,Done,'random_subset',WF),
2647 random_subset_aux(Done,ESet,Subset,Span,WF).
2648
2649 :- use_module(library(random),[random_subseq/3]).
2650 :- block random_subset_aux(-,?,?,?,?).
2651 random_subset_aux(_Done,ESet,Subset,_Span,WF) :-
2652 random_subseq(ESet,Result,_Rest),
2653 kernel_objects:equal_object_wf(Result,Subset,WF).
2654
2655 % generates a random subset of a finite set
2656 :- public 'random_ordering'/4.
2657 is_not_declarative('random_ordering').
2658 external_fun_type('random_ordering',[T],[set(T),seq(T)]).
2659 expects_waitflag('random_ordering').
2660 expects_spaninfo('random_ordering').
2661 :- block 'random_ordering'(-,?,?,?).
2662 random_ordering(Set,Permutation,Span,WF) :- !,
2663 custom_explicit_sets:expand_custom_set_to_list_wf(Set,ESet,Done,'random_ordering',WF),
2664 random_perm_aux(Done,ESet,Permutation,Span,WF).
2665
2666 :- use_module(library(random),[random_permutation/2]).
2667 :- block random_perm_aux(-,?,?,?,?).
2668 random_perm_aux(_Done,ESet,Permutation,_Span,_WF) :-
2669 random_permutation(ESet,Result),
2670 convert_list_to_seq(Result,Permutation). % should we call WF version
2671
2672 % generates a random subset of a finite sequence
2673 :- public 'random_permutation'/4.
2674 is_not_declarative('random_permutation').
2675 external_fun_type('random_permutation',[T],[seq(T),seq(T)]).
2676 expects_waitflag('random_permutation').
2677 expects_spaninfo('random_permutation').
2678 :- block 'random_permutation'(-,?,?,?).
2679 random_permutation(Set,Permutation,Span,WF) :- !,
2680 custom_explicit_sets:expand_custom_set_to_list_wf(Set,ESet,Done,'random_permutation',WF),
2681 random_perm_seq_aux(Done,ESet,Permutation,Span,WF).
2682
2683 :- block random_perm_seq_aux(-,?,?,?,?).
2684 random_perm_seq_aux(_Done,ESet,Permutation,_Span,_WF) :-
2685 sort(ESet,Sorted),
2686 maplist(drop_index,Sorted,PrologList),
2687 random_permutation(PrologList,Result),
2688 convert_list_to_seq(Result,Permutation). % should we call WF version
2689
2690 drop_index((int(_),El),El).
2691
2692 :- use_module(library(system)).
2693
2694 :- assert_must_succeed(( external_functions:call_external_function('TIME',[y],[string(year)],int(Y),integer,unknown,_WF), number(Y), Y>2011 )).
2695 :- assert_must_succeed(( external_functions:call_external_function('TIME',[m],[string(month)],int(M),integer,unknown,_WF), number(M), M>0, M<13 )).
2696 external_fun_type('TIME',[],[string,integer]).
2697 :- public 'TIME'/2.
2698 is_not_declarative('TIME'). % as time can change with next call
2699 'TIME'(string(S),int(N)) :- time2(S,N).
2700 :- block time2(-,?).
2701 time2(now,N) :- !, now(N). % provide UNIX timesstamp
2702 time2(year,N) :- !,datime(datime(N,_,_,_,_,_)).
2703 time2(month,N) :- !,datime(datime(_,N,_,_,_,_)).
2704 time2(day,N) :- !,datime(datime(_,_,N,_,_,_)).
2705 time2(hour,N) :- !,datime(datime(_,_,_,N,_,_)).
2706 time2(min,N) :- !,datime(datime(_,_,_,_,N,_)).
2707 time2(sec,N) :- !,datime(datime(_,_,_,_,_,N)).
2708 time2(OTHER,_) :- add_error(time2,'Illegal time field (must be now,year,month,day,hour,min,sec): ',OTHER),fail.
2709
2710 :- assert_must_succeed(( external_functions:call_external_function('GET_INFO',[time],[string(time)],string(M),string,unknown,_WF), atom(M) )).
2711 external_fun_type('GET_INFO',[],[string,string]).
2712 :- public 'GET_INFO'/2.
2713 'GET_INFO'(string(S),Res) :- get_info2(S,Res).
2714 :- use_module(library(codesio)).
2715 :- block get_info2(-,?).
2716 get_info2(time,Res) :- !, datime(datime(Year,Month,Day,Hour,Min,Sec)),
2717 (Min<10
2718 -> format_to_codes('~w/~w/~w - ~wh0~w ~ws',[Day,Month,Year,Hour,Min,Sec],Codes)
2719 ; format_to_codes('~w/~w/~w - ~wh~w ~ws',[Day,Month,Year,Hour,Min,Sec],Codes)
2720 ),
2721 atom_codes(INFO, Codes), Res=string(INFO).
2722 get_info2(OTHER,_) :- add_error(time2,'Illegal GET_INFO field (must be time): ',OTHER),fail.
2723
2724 :- public 'TIMESTAMP_INFO'/3.
2725 :- assert_must_succeed(external_functions:'TIMESTAMP_INFO'(string('year'),int(1498484624),int(2017))).
2726 :- assert_must_succeed(external_functions:'TIMESTAMP_INFO'(string('month'),int(1498484624),int(6))).
2727 % second argument is ticks obtained by TIME("now")
2728 external_fun_type('TIMESTAMP_INFO',[],[string,integer,integer]).
2729 :- block 'TIMESTAMP_INFO'(-,-,-).
2730 'TIMESTAMP_INFO'(string(S),int(Ticks),int(Res)) :- time_info2(S,Ticks,Res).
2731 :- block time_info2(-,?,?), time_info2(?,-,?).
2732 time_info2(year,Ticks,N) :- !,datime(Ticks,datime(N,_,_,_,_,_)).
2733 time_info2(month,Ticks,N) :- !,datime(Ticks,datime(_,N,_,_,_,_)).
2734 time_info2(day,Ticks,N) :- !,datime(Ticks,datime(_,_,N,_,_,_)).
2735 time_info2(hour,Ticks,N) :- !,datime(Ticks,datime(_,_,_,N,_,_)).
2736 time_info2(min,Ticks,N) :- !,datime(Ticks,datime(_,_,_,_,N,_)).
2737 time_info2(sec,Ticks,N) :- !,datime(Ticks,datime(_,_,_,_,_,N)).
2738 time_info2(OTHER,_,_) :- add_error(time_info2,'Illegal time field (must be now,year,month,day,hour,min,sec): ',OTHER),fail.
2739
2740 :- public 'TIMESTAMP'/7.
2741 % TIMESTAMP/datime converts between a Unix timestamp (UTC) and *local* time.
2742 % To avoid depending on the system time zone,
2743 % build the timestamp dynamically based on the expected test date.
2744 % This way the timestamp varies slightly depending on the system time zone,
2745 % but the date will always be consistent.
2746 :- assert_must_succeed((
2747 datime(Timestamp, datime(2017,6,26,15,43,44)),
2748 % Sanity check to ensure that Timestamp is roughly in the right range.
2749 Timestamp >= 1498437824, Timestamp =< 1498545824,
2750 external_functions:'TIMESTAMP'(int(2017),int(6),int(26),int(H),int(Min),int(S),int(Timestamp)),
2751 H==15, Min==43, S==44
2752 )).
2753 external_fun_type('TIMESTAMP',[],[integer,integer,integer,integer,integer,integer,integer]).
2754 :- block 'TIMESTAMP'(-,-,-,-,-,-,-).
2755 'TIMESTAMP'(int(Y),int(M),int(D),int(H),int(Min),int(S),int(Res)) :-
2756 timestamp2(Y,M,D,H,Min,S,Res).
2757
2758 :- block timestamp2(-,?,?,?,?,?,-), timestamp2(?,-,?,?,?,?,-), timestamp2(?,?,-,?,?,?,-),
2759 timestamp2(?,?,?,-,?,?,-), timestamp2(?,?,?,?,?,-,-).
2760 timestamp2(Y,M,D,H,Min,S,ResTimeStamp) :- datime(ResTimeStamp, datime(Y,M,D,H,Min,S)).
2761
2762
2763 :- public 'WALLTIME'/1.
2764 is_not_declarative('WALLTIME'). % as time can change with next call
2765 'WALLTIME'(int(X)) :- statistics(walltime,[X,_]).
2766
2767 :- volatile last_walltime/1.
2768 :- dynamic last_walltime/1.
2769 :- public 'DELTA_WALLTIME'/1.
2770 is_not_declarative('DELTA_WALLTIME'). % as time can change with next call
2771 'DELTA_WALLTIME'(int(D)) :- statistics(walltime,[X,_]),
2772 (retract(last_walltime(L)) -> D is X-L ; D = 0),
2773 assertz(last_walltime(X)).
2774
2775 :- public 'RUNTIME'/1.
2776 is_not_declarative('RUNTIME'). % as time can change with next call
2777 'RUNTIME'(int(X)) :- statistics(runtime,[X,_]).
2778
2779 :- public 'SLEEP'/3.
2780 external_subst_enabling_condition('SLEEP',_,Truth) :- create_texpr(truth,pred,[],Truth).
2781 :- use_module(library(system),[sleep/1]).
2782 :- block 'SLEEP'(-,?,?), 'SLEEP'(?,-,?).
2783 'SLEEP'(int(X),_Env,OutEnvModifications) :- when(nonvar(X),
2784 (Seconds is X / 1000, sleep(Seconds), OutEnvModifications=[])).
2785
2786
2787 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2788 % check if a given expression is valued in the deterministic phase; warn otherwise
2789
2790 :- use_module(kernel_tools,[ground_value_check/2]).
2791 expects_spaninfo('CHECK_DET').
2792 expects_unevaluated_args('CHECK_DET').
2793 expects_waitflag('CHECK_DET').
2794 :- public 'CHECK_DET'/5.
2795 'CHECK_DET'(Value,PredRes,[UnEvalArg],Span,WF) :-
2796 ground_value_check(Value,Ground),
2797 kernel_waitflags:get_wait_flag0(WF,WF0),
2798 kernel_waitflags:get_wait_flag1(WF,WF1),
2799 PredRes=pred_true,
2800 check_det_aux(Ground,Value,WF0,WF1,UnEvalArg,Span).
2801
2802 :- block check_det_aux(-,?,?,-,?,?).
2803 check_det_aux(Ground,Value,_WF0,_WF1,UnEvalArg,Span) :- var(Ground),!,
2804 translate:translate_bexpression(UnEvalArg,S),
2805 add_error(external_functions,'Argument has not been computed deterministically: ',S,Span),
2806 translate:print_bvalue(Value),nl.
2807 check_det_aux(_Ground,Value,WF0,WF1,UnEvalArg,_Span) :- debug:debug_mode(on),!,
2808 translate:translate_bexpression(UnEvalArg,S),
2809 format('Value determined (WF0=~w,WF1=~w) : ~w~n',[WF0,WF1,S]),
2810 translate:print_bvalue(Value),nl.
2811 check_det_aux(_Ground,_Value,_WF0,_WF1,_UnEvalArgs,_Span).
2812
2813 % check if a given expression has already a ground value when
2814 % the predicate is called
2815
2816 % the predicate is true when the value is ground, false otherwise
2817 :- public 'IS_DETERMINED'/2.
2818 'IS_DETERMINED'(Value,PredRes) :- ground(Value),!,PredRes=pred_true.
2819 'IS_DETERMINED'(_Value,pred_false).
2820
2821 % other variant: the predicate is always true, the information if the variable is written
2822 % to a file to check it later.
2823 expects_spaninfo('IS_DETERMINED_INTO_FILE').
2824 :- public 'IS_DETERMINED_INTO_FILE'/5.
2825 'IS_DETERMINED_INTO_FILE'(FileValue,VariableValue,Value,PredRes,SpanInfo) :-
2826 check_value_is_string(FileValue,'IS_DETERMINED_INTO_FILE','file name',SpanInfo,File),
2827 check_value_is_string(VariableValue,'IS_DETERMINED_INTO_FILE','variable name',SpanInfo,Varname),
2828 ( ground(File) ->
2829 open(File,write,S,[encoding(utf8)]),
2830 call_cleanup( check_determined2(Value,S,Varname), close(S))
2831 ;
2832 add_error(external_functions,'### EXTERNAL Unspecified file in check_determined','',SpanInfo)),
2833 PredRes = pred_true.
2834 check_determined2(Value,S,Varname) :-
2835 check_determined3(Value,Varname,Term),
2836 writeq(S,Term),write(S,'.\n').
2837 check_determined3(Value,Name,Term) :- ground(Value),!,Term=determined_value(Name,Value).
2838 check_determined3(_Value,Name,not_determined_value(Name)).
2839
2840 check_value_is_string(string(S),_PredName,_Location,_SpanInfo,String) :-
2841 !, String=S.
2842 check_value_is_string(Value,PredName,Location,SpanInfo,_String) :-
2843 atom_concat('### EXTERNAL ',PredName,Msg1),
2844 atom_concat(Msg1,': Type error, expected string as ',Msg2),
2845 atom_concat(Msg2,Location,Msg),
2846 add_error(external_functions,Msg,Value,SpanInfo),
2847 fail.
2848
2849
2850 :- public 'SEE'/3.
2851 is_not_declarative('SEE').
2852 :- dynamic open_stream/2.
2853 'SEE'(string(File),_S,[]) :- b_absolute_file_name(File,AFile),
2854 open_stream(AFile,_),!,
2855 print('File already open: '), print(File),nl.
2856 'SEE'(string(File),_S,[]) :-
2857 b_absolute_file_name(File,AFile),
2858 open_absolute_file_for_reading(AFile,_Stream).
2859
2860 open_file_for_reading_if_necessary(File,Stream) :-
2861 b_absolute_file_name(File,AFile),
2862 (open_stream(AFile,S) -> Stream=S
2863 ; open_absolute_file_for_reading(AFile,Stream)).
2864 open_absolute_file_for_reading(AFile,Stream) :-
2865 open(AFile,read,Stream,[encoding(utf8)]),
2866 print(opened_file(AFile,Stream)),nl,
2867 assert_side_effect_occurred(file),
2868 assertz(open_stream(AFile,Stream)).
2869
2870 %correct_file_open_mode(read).
2871 %correct_file_open_mode(write).
2872 %correct_file_open_mode(append).
2873
2874 :- public 'GET_CODE'/2.
2875 performs_io('GET_CODE').
2876 'GET_CODE'(string(File),int(Code)) :-
2877 b_absolute_file_name(File,AFile),
2878 open_stream(AFile,S),
2879 assert_side_effect_occurred(file),
2880 get_code(S,Code). %,print(got_code(S,Code)),nl.
2881
2882 :- public 'GET_CODE_STDIN'/1.
2883 performs_io('GET_CODE_STDIN').
2884 'GET_CODE_STDIN'(int(Code)) :- get_code(user_input,Code).
2885
2886 :- public 'SEEN'/3.
2887 is_not_declarative('SEEN').
2888 'SEEN'(string(File),_S,[]) :- b_absolute_file_name(File,AFile),
2889 retract(open_stream(AFile,S)),
2890 assert_side_effect_occurred(file),
2891 close(S).
2892
2893 close_all_files :- retract(open_stream(_File,S)),
2894 close(S),fail.
2895 close_all_files.
2896
2897
2898 open_utf8_file_for_reading(AFile,Stream,SpanInfo) :-
2899 safe_call(open(AFile,read,Stream,[encoding(utf8)]),SpanInfo).
2900
2901 :- public 'READ_FILE_AS_STRINGS'/3.
2902 performs_io('READ_FILE_AS_STRINGS').
2903 external_subst_enabling_condition('READ_FILE_AS_STRINGS',_,Truth) :- create_texpr(truth,pred,[],Truth).
2904 expects_spaninfo('READ_FILE_AS_STRINGS').
2905 :- block 'READ_FILE_AS_STRINGS'(-,?,?).
2906 'READ_FILE_AS_STRINGS'(string(File),Res,SpanInfo) :-
2907 b_absolute_file_name(File,AFile,SpanInfo),
2908 open_utf8_file_for_reading(AFile,Stream,SpanInfo),!,
2909 format('% Opened file: ~w~n',[File]),
2910 % no side-effect: as everything read in one go
2911 call_cleanup(read_lines(Stream,Res),
2912 close(Stream)).
2913 'READ_FILE_AS_STRINGS'(string(File),_Res,_SpanInfo) :-
2914 format('% Opening file failed: ~w~n',[File]),fail.
2915 read_lines(File,Res) :- read_lines_loop(1,File,Lines),
2916 kernel_objects:equal_object(Res,Lines).
2917 read_lines_loop(Nr,Stream,Lines) :- read_line(Stream,Line),
2918 debug:debug_println(9,read_line(Nr,Line)),
2919 (Line = end_of_file -> Lines = []
2920 ; atom_codes(Atom,Line), Lines = [(int(Nr),string(Atom))|T],
2921 N1 is Nr+1,read_lines_loop(N1,Stream,T)).
2922
2923
2924 :- public 'READ_FILE_AS_STRING'/3.
2925 performs_io('READ_FILE_AS_STRING').
2926 external_subst_enabling_condition('READ_FILE_AS_STRING',_,Truth) :- create_texpr(truth,pred,[],Truth).
2927 expects_spaninfo('READ_FILE_AS_STRING').
2928 :- block 'READ_FILE_AS_STRING'(-,?,?).
2929 'READ_FILE_AS_STRING'(string(File),Res,SpanInfo) :-
2930 b_absolute_file_name(File,AFile,SpanInfo),
2931 open_utf8_file_for_reading(AFile,Stream,SpanInfo),!,
2932 format('% Opened file: ~w~n',[File]),
2933 % no side-effect: as everything read in one go
2934 call_cleanup(read_all_codes(Stream,All,[]),
2935 close(Stream)),
2936 atom_codes(ResStr,All), Res = string(ResStr).
2937
2938 % read all codes in the stream:
2939 read_all_codes(Stream) --> {read_line(Stream,Line), Line \= end_of_file, !},
2940 Line, "\n",
2941 read_all_codes(Stream).
2942 read_all_codes(_) --> "".
2943
2944
2945 :- public 'READ_LINE'/3.
2946 expects_spaninfo('READ_LINE').
2947 external_subst_enabling_condition('READ_LINE',_,Truth) :- create_texpr(truth,pred,[],Truth).
2948 performs_io('READ_LINE').
2949 'READ_LINE'(string(File),Res,_SpanInfo) :-
2950 open_file_for_reading_if_necessary(File,Stream),
2951 read_line(Stream,Line),
2952 debug:debug_println(9,read_line(Line)),
2953 assert_side_effect_occurred(file),
2954 (Line = end_of_file
2955 -> add_error(external_functions,'Attempting to read past EOF: ',File),
2956 Res = ""
2957 ; atom_codes(Atom,Line), Res = string(Atom)).
2958
2959 is_not_declarative('EOF').
2960 :- public 'EOF'/2.
2961 'EOF'(string(File),Res) :- eof2(File,Res).
2962 :- block eof2(-,?).
2963 eof2(File,Res) :-
2964 open_file_for_reading_if_necessary(File,Stream),
2965 ((peek_code(Stream,C), C = -1) -> Res = pred_true ; Res = pred_false). % for Linux compatibility
2966 % (at_end_of_stream(Stream) -> Res = pred_true ; Res=pred_false).
2967
2968 is_not_declarative('EOF_STDIN').
2969 :- public 'EOF_STDIN'/2.
2970 'EOF_STDIN'(_,Res) :- % dummy argument to enable valid external predicate type declarations
2971 ((peek_code(user_input,C), C = -1) -> Res = pred_true ; Res = pred_false).
2972
2973
2974 external_fun_type('CURRENT_FILE_POSITION',[],[string,string,integer]).
2975 is_not_declarative('CURRENT_FILE_POSITION').
2976 :- public 'CURRENT_FILE_POSITION'/3.
2977 'CURRENT_FILE_POSITION'(string(File),string(Field),Res) :-
2978 open_file_for_reading_if_necessary(File,Stream),
2979 stream_position(Stream,Pos),
2980 % POS must be one of byte_count [only for binary streams], line_count, character_count, line_position
2981 stream_position_data(Field,Pos,R), Res=int(R).
2982
2983 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2984
2985 :- public 'ADD_ERROR'/6.
2986 expects_spaninfo('ADD_ERROR').
2987 expects_waitflag('ADD_ERROR').
2988 performs_io('ADD_ERROR').
2989 'ADD_ERROR'(string(Msg),Expr,_State,[],SpanInfo,WF) :-
2990 add_error_wf('ADD_ERROR',Msg,Expr,SpanInfo,WF).
2991
2992 :- public 'ADD_STATE_ERROR'/6.
2993 expects_spaninfo('ADD_STATE_ERROR').
2994 expects_waitflag('ADD_STATE_ERROR').
2995 performs_io('ADD_STATE_ERROR').
2996 'ADD_STATE_ERROR'(string(Msg),Expr,_State,[],SpanInfo,WF) :-
2997 %add_wd_error_span_now(Msg,Expr,SpanInfo,WF).
2998 %add_wd_error_span(Msg,Expr,SpanInfo,WF).
2999 add_state_error_wf('ADD_STATE_ERROR',Msg,Expr,SpanInfo,WF). % does not fail
3000
3001 :- public 'ADD_WARNING'/6.
3002 expects_spaninfo('ADD_WARNING').
3003 expects_waitflag('ADD_WARNING').
3004 performs_io('ADD_WARNING').
3005 'ADD_WARNING'(string(Msg),Expr,_State,[],SpanInfo,WF) :-
3006 add_warning_wf('ADD_WARNING',Msg,Expr,SpanInfo,WF).
3007
3008
3009 :- public 'ADD_ERRORS'/5.
3010 expects_spaninfo('ADD_ERRORS').
3011 expects_waitflag('ADD_ERRORS').
3012 performs_io('ADD_ERRORS').
3013 :- block 'ADD_ERRORS'(-,?,?,?,?).
3014 'ADD_ERRORS'(SetOfStrings,_State,[],SpanInfo,WF) :-
3015 custom_explicit_sets:expand_custom_set_to_list_wf(SetOfStrings,ESet,_,add_errors,WF),
3016 add_errors_aux(ESet,SpanInfo,WF).
3017 :- block add_errors_aux(-,?,?).
3018 add_errors_aux([],_SpanInfo,_WF).
3019 add_errors_aux([string(Msg)|T],SpanInfo,WF) :-
3020 add_error('ADD_ERRORS',Msg,'',SpanInfo),
3021 add_errors_aux(T,SpanInfo,WF).
3022
3023 :- public 'ADD_STATE_ERRORS'/5.
3024 expects_spaninfo('ADD_STATE_ERRORS').
3025 expects_waitflag('ADD_STATE_ERRORS').
3026 performs_io('ADD_STATE_ERRORS').
3027 :- block 'ADD_STATE_ERRORS'(-,?,?,?,?).
3028 'ADD_STATE_ERRORS'(SetOfStrings,_State,[],SpanInfo,WF) :-
3029 custom_explicit_sets:expand_custom_set_to_list_wf(SetOfStrings,ESet,_,add_state_errors,WF),
3030 add_state_errors_aux(ESet,SpanInfo,WF).
3031 :- block add_state_errors_aux(-,?,?).
3032 add_state_errors_aux([],_SpanInfo,_WF).
3033 add_state_errors_aux([string(Msg)|T],SpanInfo,WF) :-
3034 add_state_error_wf('ADD_STATE_ERRORS',Msg,'',SpanInfo,WF),
3035 add_state_errors_aux(T,SpanInfo,WF).
3036
3037 :- public 'ADD_WARNINGS'/5.
3038 expects_spaninfo('ADD_WARNINGS').
3039 expects_waitflag('ADD_WARNINGS').
3040 performs_io('ADD_WARNINGS').
3041 :- block 'ADD_WARNINGS'(-,?,?,?,?).
3042 'ADD_WARNINGS'(SetOfStrings,_State,[],SpanInfo,WF) :-
3043 custom_explicit_sets:expand_custom_set_to_list_wf(SetOfStrings,ESet,_,add_warnings,WF),
3044 add_warnings_aux(ESet,SpanInfo,WF).
3045 :- block add_warnings_aux(-,?,?).
3046 add_warnings_aux([],_SpanInfo,_WF).
3047 add_warnings_aux([string(Msg)|T],SpanInfo,WF) :-
3048 add_warning('ADD_WARNINGS',Msg,'',SpanInfo),
3049 % we do not add with WF and call stack: call stack contains call to ADD_WARNINGS with all error messages again
3050 add_warnings_aux(T,SpanInfo,WF).
3051
3052 :- public 'ASSERT_TRUE'/5.
3053 expects_spaninfo('ASSERT_TRUE').
3054 expects_waitflag('ASSERT_TRUE').
3055 external_fun_has_wd_condition('ASSERT_TRUE').
3056
3057 'ASSERT_TRUE'(PredVal,string(Msg),PredRes,SpanInfo,WF) :-
3058 assert_true(PredVal,Msg,PredRes,SpanInfo,WF).
3059
3060 :- block assert_true(-,?,?,?,?).
3061 assert_true(pred_true,_Msg,pred_true,_SpanInfo,_WF).
3062 assert_true(pred_false,Msg,Res,SpanInfo,WF) :-
3063 debug_format(19,'% Waiting for enumeration to finish to raise ASSERT_TRUE:~n ~w~n',[Msg]),
3064 add_error_ef('ASSERT_TRUE',Msg,'',SpanInfo,WF,Res).
3065
3066 % we could also use: add_wd_error_set_result
3067 add_error_ef(Source,Msg,Term,Span,WF,Res) :-
3068 get_enumeration_finished_wait_flag(WF,AWF),
3069 add_error_ef_aux(AWF,Source,Msg,Term,Span,WF,Res).
3070
3071 :- block add_error_ef_aux(-,?,?,?,?,?,?).
3072 add_error_ef_aux(_AWF,Source,Msg,Term,Span,_WF,Res) :-
3073 add_error(Source,Msg,Term,Span),
3074 Res = pred_false.
3075
3076 :- public 'ASSERT_EXPR'/6.
3077 expects_spaninfo('ASSERT_EXPR').
3078 expects_waitflag('ASSERT_EXPR').
3079 external_fun_has_wd_condition('ASSERT_EXPR').
3080 external_fun_type('ASSERT_EXPR',[T],[boolean,string,T,T]).
3081
3082 'ASSERT_EXPR'(PredVal,string(Msg),ExprVal,Res,SpanInfo,WF) :-
3083 % TO DO: call assertion_expression(Cond,ErrMsg,Expr)
3084 assert_expr(PredVal,Msg,ExprVal,Res,SpanInfo,WF).
3085
3086 :- block assert_expr(-,?,?,?,?,?).
3087 assert_expr(pred_true,_Msg,ExprVal,Res,_SpanInfo,_WF) :-
3088 Res = ExprVal.
3089 assert_expr(pred_false,Msg,_ExprVal,Res,SpanInfo,WF) :-
3090 add_error_ef('ASSERT_EXPR',Msg,'',SpanInfo,WF,Res).
3091
3092 % --------------------------
3093 % Reflection Functions
3094
3095 external_fun_type('STATE_AS_STRING',[],[integer,string]).
3096 :- public 'STATE_AS_STRING'/3.
3097 expects_waitflag('STATE_AS_STRING').
3098 'STATE_AS_STRING'(int(X),StateStr,WF) :-
3099 state_space:get_state_space_stats(NrNodes,_NrTransitions,_ProcessedNodes),
3100 get_wait_flag(NrNodes,'STATE_AS_STRING',WF,LWF),
3101 get_state2(X,StateStr,LWF).
3102 :- block get_state2(-,?,-).
3103 get_state2(X,StateStr,_) :-
3104 convert_id_to_nr(IDX,X),
3105 state_space:visited_expression(IDX,S),
3106 translate:translate_bstate(S,Str),
3107 StateStr = string(Str).
3108
3109 :- public 'CURRENT_STATE_AS_TYPED_STRING'/1.
3110 external_fun_type('CURRENT_STATE_AS_TYPED_STRING',[],[string]).
3111 % translate current state values as parseable string
3112 'CURRENT_STATE_AS_TYPED_STRING'(string(Translation)) :-
3113 'VARS_AS_TYPED_STRING'(string(''),string(Translation)).
3114
3115 external_fun_type('VARS_AS_TYPED_STRING',[],[string,string]).
3116 :- block 'VARS_AS_TYPED_STRING'(-,?).
3117 'VARS_AS_TYPED_STRING'(string(Prefix),string(Translation)) :-
3118 get_current_state_id(ID),
3119 visited_expression(ID,State),
3120 state_corresponds_to_fully_setup_b_machine(State,FullState),
3121 b_get_machine_constants(Constants),
3122 include(identifier_matches_prefix(Prefix),Constants,C1),
3123 b_get_machine_variables(Vars),
3124 include(identifier_matches_prefix(Prefix),Vars,V1),
3125 append(C1,V1,Ids),
3126 findall(Equality,(member(TID,Ids),
3127 generate_equality(TID,FullState,Equality)),Eqs),
3128 generate_typing_predicates(Ids,TypePreds),
3129 append(TypePreds,Eqs,Ps),
3130 conjunct_predicates(Ps,Pred),
3131 translate_bexpr_to_parseable(Pred,Translation).
3132
3133 :- use_module(probsrc(tools_strings), [atom_prefix/2]).
3134 identifier_matches_prefix(Prefix,b(identifier(ID),_,_)) :- atom_prefix(Prefix,ID).
3135
3136 generate_equality(TID,FullState,Equality) :- TID = b(identifier(ID),Type,_),
3137 if(member(bind(ID,Val),FullState),
3138 safe_create_texpr(equal(TID,b(value(Val),Type,[])),pred,Equality),
3139 add_error_fail('VARS_AS_TYPED_STRING','Could not find identifier:',TID)).
3140
3141 :- use_module(state_space,[visited_expression/2]).
3142 :- use_module(probsrc(tools_strings),[match_atom/3]).
3143 :- use_module(specfile,[property/2]).
3144 :- public 'STATE_PROPERTY'/3.
3145 % a useful function for VisB and XTL or CSP models to query state of model
3146 expects_spaninfo('STATE_PROPERTY').
3147 external_fun_type('STATE_PROPERTY',[],[string,string]).
3148 :- block 'STATE_PROPERTY'(-,?,?).
3149 'STATE_PROPERTY'(string(Prop),Res,Span) :- state_property2(Prop,Res,Span).
3150 :- block state_property2(-,?,?).
3151 state_property2(Prop,Res,Span) :-
3152 get_current_state_id(ID),
3153 visited_expression(ID,State),
3154 atom_codes(Prop,PC),
3155 (property(State,'='(StateProp,Val)), % TODO: this leads to error in B mode due to atom_codes error
3156 match_atom(Prop,PC,StateProp)
3157 -> (atom(Val) -> Res = string(Val)
3158 ; number(Val), number_codes(Val,CC), atom_codes(Atom,CC) -> Res = string(Atom)
3159 ; add_message(external_functions,'Cannot convert STATE_PROPERTY value to STRING ',Val,Span),
3160 Res = string('UNKNOWN')
3161 )
3162 ; add_message(external_functions,'Unknown value for STATE_PROPERTY: ',Prop,Span),
3163 Res = string('UNKNOWN')
3164 ).
3165
3166
3167 :- public 'STATE_SUCC'/4.
3168 external_fun_type('STATE_SUCC',[],[integer,integer,boolean]).
3169 expects_waitflag('STATE_SUCC').
3170 'STATE_SUCC'(X,Y,Res,WF) :- 'STATE_TRANS'(X,_,Y,Res,WF).
3171
3172 % synonym for function to BOOL rather than predicate
3173 'GET_IS_ENABLED'(OperationName,Res,WF) :- 'ENABLED'(OperationName,Res,WF).
3174 :- public 'GET_IS_ENABLED'/3.
3175 expects_waitflag('ENABLED').
3176 expects_waitflag('GET_IS_ENABLED').
3177 external_fun_type('ENABLED',[],[string,boolean]).
3178 'ENABLED'(OperationName,Res,WF) :-
3179 get_current_state_id(ID),
3180 tcltk_interface:compute_all_transitions_if_necessary(ID,false),
3181 NrOps = 10, get_wait_flag(NrOps,'ENABLED',WF,LWF),
3182 % format('Checking ENABLED of ~w in state ~w~n',[OperationName,ID]),
3183 enabled_op(ID,OperationName,Res,LWF).
3184
3185 :- block enabled_op(?,-,?,-).
3186 enabled_op(ID,OperationName,Res,_) :- var(OperationName), !,
3187 b_top_level_operation(OpName), OperationName=string(OpName),
3188 (state_space_transition(ID,_,OperationName,_) -> Res=pred_true ; Res=pred_false).
3189 enabled_op(ID,OperationName,Res,_) :-
3190 (state_space_transition(ID,_,OperationName,_) -> Res=pred_true ; Res=pred_false).
3191
3192 % synonym for function to BOOL rather than predicate
3193 'GET_IS_ENABLED_TRANSITION'(OperationName,Res,WF) :- 'ENABLED_TRANSITION'(OperationName,Res,WF).
3194 :- public 'GET_IS_ENABLED_TRANSITION'/3.
3195 % a variation of ENABLED where we can check for arguments; useful for VisB but it relies on argument order
3196 external_fun_type('ENABLED_TRANSITION',[],[string,boolean]).
3197 expects_waitflag('ENABLED_TRANSITION').
3198 expects_waitflag('GET_IS_ENABLED_TRANSITION').
3199 'ENABLED_TRANSITION'(TransString,Res,WF) :-
3200 get_current_state_id(ID),
3201 tcltk_interface:compute_all_transitions_if_necessary(ID,false),
3202 NrOps = 10, get_wait_flag(NrOps,'GET_IS_ENABLED_TRANSITION',WF,LWF),
3203 % format('Checking ENABLED_TRANSITION of ~w in state ~w~n',[TransString,ID]),
3204 enabled_trans(ID,TransString,Res,LWF).
3205
3206 :- block enabled_trans(?,-,?,-),enabled_trans(?,-,-,?).
3207 enabled_trans(ID,string(TransitionStr),Res,LWF) :-
3208 enabled_trans2(ID,TransitionStr,Res,LWF).
3209 :- block enabled_trans2(?,-,?,-),enabled_trans2(?,-,-,?).
3210 enabled_trans2(ID,TransitionStr,Res,_) :- var(TransitionStr),!,
3211 (Res=pred_true -> transition_string(ID,Str,1000,_), TransitionStr=Str
3212 ; enabled_trans2(ID,TransitionStr,Res,_) % wait until TransitionStr is known
3213 ).
3214 enabled_trans2(ID,TransitionStr,Res,_) :-
3215 atom_length(TransitionStr,Limit),
3216 (transition_string(ID,TransitionStr,Limit,_) -> Res=pred_true ; Res=pred_false).
3217
3218 :- use_module(state_space,[transition/4]).
3219 :- use_module(translate,[translate_event_with_src_and_target_id/5]).
3220 transition_string(ID,TransitionStr,Limit,ToID) :-
3221 transition(ID,TransitionTerm,_TransID,ToID),
3222 % This will currently also output --> Res for operation results; probably we do not want that
3223 translate_event_with_src_and_target_id(TransitionTerm,ID,ToID,Limit,TransitionStr).
3224
3225 :- public 'NON_DET_STATE'/1.
3226 %is_not_declarative('NON_DET_STATE'). % depends on current state, but for any given state it is declarative
3227 external_fun_type('NON_DET_STATE',[],[boolean]).
3228 % check if there is a non-deterministic transition: same transition different target state
3229 % similar to tcltk_goto_a_non_deterministic_node
3230 'NON_DET_STATE'(Res) :- get_current_state_id(ID),
3231 non_det_transition(ID,_OperationName,_,_), !,
3232 Res = pred_true.
3233 'NON_DET_STATE'(pred_false).
3234
3235 :- public 'NON_DET_OUTPUT_STATE'/1.
3236 %is_not_declarative('NON_DET_OUTPUT_STATE'). % depends on current state, but for any given state it is declarative
3237 external_fun_type('NON_DET_OUTPUT_STATE',[],[boolean]).
3238 % check if there is a non-deterministic transition: same transition different classic B operation result
3239 % similar to tcltk_goto_a_non_deterministic_output_node
3240 'NON_DET_OUTPUT_STATE'(Res) :- get_current_state_id(ID),
3241 non_det_output_transition2(ID,_OperationName), !,
3242 Res = pred_true.
3243 'NON_DET_OUTPUT_STATE'(pred_false).
3244
3245 % check if we find a state ID where OperationName leads to two different states with same arguments
3246 non_det_transition(ID,OperationName,TID1,TID2) :-
3247 tcltk_interface:compute_all_transitions_if_necessary(ID,false),
3248 transition(ID,Transition,TID1,ID1),
3249 get_operation_name(Transition,OperationName),
3250 get_operation_arguments(Transition,OperationArgs),
3251 transition(ID,Transition2,TID2,ID2),
3252 TID2 > TID1, ID1 \= ID2,
3253 get_operation_name(Transition2,OperationName), % same operation
3254 get_operation_arguments(Transition2,OperationArgs). % same arguments
3255
3256 :- use_module(probltlsrc(ltl_propositions), [non_det_output_transition/4]).
3257 % check if we find a state where an operation with output/result parameters is non-det in the output
3258 non_det_output_transition2(ID,OperationName) :-
3259 tcltk_interface:compute_all_transitions_if_necessary(ID,false), % TODO: detect if we are looping and computing guards/actions
3260 non_det_output_transition(ID,OperationName,_TID1,_TID2).
3261
3262 :- public 'GET_IS_DET'/3.
3263 expects_spaninfo('GET_IS_DET').
3264 external_fun_type('GET_IS_DET',[],[string,boolean]).
3265 % check if there is a non-deterministic transition for a given operation: same transition different target state
3266 :- block 'GET_IS_DET'(-,?,?).
3267 'GET_IS_DET'(string(OperationName),Res,Span) :-
3268 get_current_state_id(ID),
3269 nondet_op2(ID,OperationName,'GET_IS_DET',Res,Span).
3270
3271
3272 :- public 'GET_IS_DET_OUTPUT'/3.
3273 expects_spaninfo('GET_IS_DET_OUTPUT').
3274 external_fun_type('GET_IS_DET_OUTPUT',[],[string,boolean]).
3275 % check if there is a non-deterministic transition for a given operation: same transition different target state
3276 :- block 'GET_IS_DET_OUTPUT'(-,?,?).
3277 'GET_IS_DET_OUTPUT'(string(OperationName),Res,Span) :-
3278 get_current_state_id(ID),
3279 nondet_op2(ID,OperationName,'GET_IS_DET_OUTPUT',Res,Span).
3280
3281 :- block nondet_op2(?,-,?,?,?).
3282 nondet_op2(_ID,OperationName,XFUN,Res,Span) :- \+ b_top_level_operation(OperationName),!,
3283 add_error(XFUN,'Not a valid top-level operation:',OperationName,Span),
3284 Res = pred_false.
3285 % Check if it has outputs and throw warning if not ?
3286 nondet_op2(ID,OperationName,'GET_IS_DET',Res,_Span) :-
3287 non_det_transition(ID,OperationName,_,_),
3288 !,
3289 Res = pred_false.
3290 nondet_op2(ID,OperationName,'GET_IS_DET_OUTPUT',Res,_Span) :-
3291 non_det_output_transition2(ID,OperationName),
3292 !,
3293 Res = pred_false.
3294 nondet_op2(_,_,_,pred_true,_Span).
3295
3296 :- public 'NON_DET_OUTPUT_OPERATIONS'/1.
3297 external_fun_type('NON_DET_OUTPUT_OPERATIONS',[],[set(string)]).
3298 'NON_DET_OUTPUT_OPERATIONS'(Res) :-
3299 get_current_state_id(ID),
3300 findall(string(OpName),
3301 non_det_output_transition2(ID,OpName),
3302 List),
3303 sort(List,SList),
3304 kernel_objects:equal_object_optimized(SList,Res).
3305
3306
3307 % -------------------
3308
3309 external_fun_type('STATE_TRANS',[],[integer,string,integer,boolean]).
3310 expects_waitflag('STATE_TRANS').
3311 'STATE_TRANS'(int(X),OperationName,int(Y),Res,WF) :-
3312 'STATE_TRANS_ARGS'(int(X),OperationName,_,int(Y),Res,WF).
3313
3314 external_fun_type('STATE_TRANS_ARGS',[X],[integer,string,X,integer,boolean]).
3315 expects_waitflag('STATE_TRANS_ARGS').
3316 'STATE_TRANS_ARGS'(int(X),OperationName,OperationArgs,int(Y),Res,WF) :-
3317 (nonvar(X) -> true
3318 ; state_space:get_state_space_stats(NrNodes,_NrTransitions,_ProcessedNodes),
3319 get_wait_flag(NrNodes,'STATE_TRANS',WF,LWF)
3320 ),
3321 get_wait_flag1('STATE_TRANS_ARGS',WF,WF1),
3322 get_succ2(X,OperationName,OperationArgs,Y,Res,LWF,WF1).
3323 :- block get_succ2(-,?,?,-,?,-,?),
3324 get_succ2(?,?,?,?,?,?,-). % wait at least until WF1 (or at least wf0); as we do non-deterministic enumeration ! (e.g., otherwise b_interprter_components gets confused !!)
3325 get_succ2(X,OperationName,OperationArgs,Y,Res,_,_) :- convert_id_to_nr(IDX,X), convert_id_to_nr(IDY,Y),
3326 if(state_space_transition(IDX,IDY,OperationName,OperationArgs),Res=pred_true,Res=pred_false).
3327
3328 state_space_transition(IDX,IDY,OperationName,OperationArgs) :-
3329 state_space:transition(IDX,Transition,IDY),
3330 op_functor(Transition,OperationName),
3331 op_args(Transition,OperationArgs).
3332
3333 % root is represented as -1
3334 :- block convert_id_to_nr(-,-).
3335 convert_id_to_nr(ID,X) :- ID==root, !, X is -1.
3336 convert_id_to_nr(ID,X) :- X == -1, !, ID=root.
3337 convert_id_to_nr(X,X).
3338
3339 :- use_module(specfile,[get_operation_name/2,get_operation_arguments/2, get_operation_return_values_and_arguments/3]).
3340 op_functor(OpTerm,Res) :- get_operation_name(OpTerm,Name),
3341 Res = string(Name).
3342
3343 :- use_module(tools,[convert_list_into_pairs/2]).
3344 op_args(OpTerm,OperationArgs) :- get_operation_arguments(OpTerm,As),
3345 convert_list_into_pairs(As,ArgTerm),
3346 kernel_objects:equal_object(OperationArgs,ArgTerm).
3347
3348
3349 :- public 'STATE_SAT'/4.
3350 expects_waitflag('STATE_SAT').
3351 external_fun_type('STATE_SAT',[],[integer,string,boolean]).
3352 % check whether formula as string holds in a state
3353 :- block 'STATE_SAT'(?,-,?,?).
3354 'STATE_SAT'(int(X),string(Formula),Res,WF) :- %print(parsing(Formula)),nl, trace,
3355 parse_pred(Formula,TFormula),
3356 state_space:get_state_space_stats(NrNodes,_NrTransitions,_ProcessedNodes),
3357 get_wait_flag(NrNodes,'STATE_SAT',WF,LWF),
3358 state_sat2(X,TFormula,Res,LWF,WF).
3359 :- block state_sat2(?,-,?,?,?),state_sat2(-,?,?,-,?).
3360 state_sat2(X,TFormula,PredRes,_,WF) :-
3361 (number(X) -> test_formula_in_state(X,TFormula,PredRes,WF)
3362 ; test_formula_in_state(ID,TFormula,PredRes,WF), ID \= root, X=ID % avoid CLPFD errors on X
3363 ).
3364
3365 :- use_module(b_global_sets,[add_prob_deferred_set_elements_to_store/3]).
3366 :- use_module(specfile,[state_corresponds_to_fully_setup_b_machine/2]).
3367 %:- use_module(b_interpreter,[b_try_check_boolean_expression_wf/5]).
3368 test_formula_in_state(ID,Pred,PredRes,WF) :-
3369 state_space:visited_expression(ID,State),
3370 state_corresponds_to_fully_setup_b_machine(State,FullState),
3371 add_prob_deferred_set_elements_to_store(FullState,FullState1,visible),
3372 debug_println(9,check(Pred,FullState1,PredRes)),
3373 b_interpreter:b_try_check_boolean_expression_wf(Pred,[],FullState1,WF,PredRes).
3374
3375
3376 :- public 'EVAL'/4.
3377 expects_waitflag('EVAL'). % external function with unknown return type
3378 'EVAL'(int(X),string(Expr),Value,WF) :-
3379 'STATE_EVAL'(int(X),string(Expr),Value,pred_true,WF).
3380 :- public 'STATE_EVAL'/5.
3381 expects_waitflag('STATE_EVAL'). % external predicate
3382 % evaluate expression and check whether value corresponds to provided value
3383 % (needed for type inference of the external predicate)
3384 :- block 'STATE_EVAL'(?,-,?,?,?).
3385 'STATE_EVAL'(int(X),string(Expr),Value,PredRes,WF) :-
3386 % string must be provided ; we assume it will be ground
3387 parse_expr(Expr,TExpr),
3388 state_space:get_state_space_stats(NrNodes,_NrTransitions,_ProcessedNodes),
3389 get_wait_flag(NrNodes,'STATE_SAT',WF,LWF),
3390 state_eval2(X,TExpr,Value,LWF,PredRes).
3391 :- block state_eval2(?,-,?,?,?),state_eval2(-,?,?,-,?).
3392 state_eval2(X,TExpr,Value,_,PredRes) :-
3393 (number(X) -> eval_formula_in_state(X,TExpr,Value,PredRes)
3394 ; eval_formula_in_state(ID,TExpr,Value,PredRes), ID \= root, X=ID % avoid CLPFD errors on X
3395 ).
3396 :- use_module(kernel_equality,[equality_objects/3]).
3397 eval_formula_in_state(ID,TExpr,Value,PredRes) :-
3398 state_space:visited_expression(ID,State),
3399 state_corresponds_to_fully_setup_b_machine(State,FullState),
3400 add_prob_deferred_set_elements_to_store(FullState,FullState1,visible),
3401 debug_println(9,eval(TExpr,FullState1,Value)),
3402 equality_objects(Value,TExprValue,PredRes), % TO DO: Stronger Checks that types compatible
3403 b_interpreter:b_compute_expression_nowf(TExpr,[],FullState1,TExprValue,'STATE_EVAL',ID).
3404
3405 :- use_module(library(terms),[term_hash/2]).
3406 :- use_module(bmachine,[b_parse_machine_predicate/3]).
3407 :- dynamic parse_pred_cache/3.
3408 parse_pred(PredStr,TPred) :- term_hash(PredStr,Hash), parse_pred(PredStr,Hash,TPred).
3409 parse_pred(PredStr,Hash,TPred) :- parse_pred_cache(Hash,PredStr,TC),!, TPred=TC.
3410 parse_pred(PredStr,Hash,TPred) :-
3411 b_parse_machine_predicate(PredStr,[prob_ids(visible),variables],TC),
3412 assertz(parse_pred_cache(Hash,PredStr,TC)),
3413 TPred=TC.
3414
3415 :- dynamic parse_expr_cache/3.
3416 parse_expr(ExprStr,TExpr) :- term_hash(ExprStr,Hash), parse_expr(ExprStr,Hash,TExpr).
3417 parse_expr(ExprStr,Hash,TExpr) :- parse_expr_cache(Hash,ExprStr,TC),!, TExpr=TC.
3418 parse_expr(ExprStr,Hash,TExpr) :-
3419 atom_codes(ExprStr,Codes), %print(parsing(Expr,Codes)),nl,
3420 bmachine:b_parse_machine_expression_from_codes_with_prob_ids(Codes,TC),
3421 assertz(parse_expr_cache(Hash,ExprStr,TC)),
3422 TExpr=TC.
3423
3424 :- use_module(kernel_strings,[generate_code_sequence/3]).
3425 external_fun_type('HISTORY',[],[seq(integer)]).
3426 :- public 'HISTORY'/1.
3427 'HISTORY'(Value) :-
3428 state_space:history(RH), reverse(RH,[root|Rest]),
3429 generate_code_sequence(Rest,1,Hist),
3430 kernel_objects:equal_object(Value,Hist).
3431
3432 :- use_module(state_space,[is_initial_state_id/1]).
3433
3434 :- public 'INITIAL_STATE'/3.
3435 expects_waitflag('INITIAL_STATE'). % external function with unknown return type
3436 'INITIAL_STATE'(int(InitialState),PredRes,WF) :-
3437 get_wait_flag(2,'INITIAL_STATE',WF,LWF),
3438 is_init2(InitialState,PredRes,LWF).
3439 :- block is_init2(-,-,?), is_init2(-,?,-).
3440 is_init2(InitialState,PredRes,_) :-
3441 PredRes == pred_true,!,
3442 is_initial_state_id(InitialState).
3443 is_init2(InitialState,PredRes,_) :- number(InitialState),!,
3444 (is_initial_state_id(InitialState) -> PredRes=pred_true ; PredRes=pred_false).
3445 is_init2(InitialState,PredRes,_LWF) :-
3446 PredRes == pred_false,!,
3447 when(nonvar(InitialState), \+is_initial_state_id(InitialState)).
3448 is_init2(InitialState,PredRes,LWF) :-
3449 add_internal_error('Uncovered case: ', is_init2(InitialState,PredRes,LWF)),fail.
3450
3451
3452 % provide information about a particular B machine in the project
3453 :- public 'MACHINE_INFO'/4.
3454 expects_waitflag('MACHINE_INFO').
3455 external_fun_type('MACHINE_INFO',[],[string,string,string]).
3456 :- block 'MACHINE_INFO'(?,-,?,?).
3457 'MACHINE_INFO'(M,string(I),Value,WF) :-
3458 get_wait_flag(2,'MACHINE_INFO',WF,LWF), % TO DO: use number of machines
3459 machine_info2(I,M,Value,LWF).
3460
3461 :- use_module(b_machine_hierarchy,[machine_type/2]).
3462 :- block machine_info2(-,?,?,?), machine_info2(?,-,?,-).
3463 machine_info2(INFO,M,Value,_LWF) :-
3464 (ground(M) -> M = string(MachineName) ; true),
3465 machine_info3(INFO,MachineName,Type),
3466 (M,Value) = (string(MachineName),string(Type)).
3467
3468 :- use_module(b_machine_hierarchy,[machine_type/2]).
3469 % :- use_module(extension('probhash/probhash'),[raw_sha_hash/2]). % already imported above
3470 :- use_module(bmachine,[get_full_b_machine/2]).
3471 machine_info3('TYPE',MachineName,Type) :- !, machine_type(MachineName,Type).
3472 % SHA_HASH
3473 machine_info3(INFO,_,_) :- add_error('MACHINE_INFO','Unknown info field (TYPE recognised): ',INFO),fail.
3474
3475
3476 :- use_module(tools_strings,[get_hex_codes/2]).
3477 external_fun_type('INT_TO_HEX_STRING',[],[integer,string]).
3478 :- public 'INT_TO_HEX_STRING'/2.
3479 :- block 'INT_TO_HEX_STRING'(-,?).
3480 'INT_TO_HEX_STRING'(int(Int),Res) :- int_to_hex(Int,Res).
3481
3482 :- block int_to_hex(-,?).
3483 int_to_hex(Int,Res) :-
3484 (Int >= 0 -> Nat=Int ; Nat is -(Int)),
3485 get_hex_codes(Nat,Chars),
3486 (Int >= 0 -> atom_codes(Atom,Chars) ; atom_codes(Atom,[45|Chars])), % "-" = [45]
3487 Res = string(Atom).
3488
3489
3490 :- use_module(tools_strings,[get_hex_bytes/2]).
3491 sha_hash_as_hex_codes(Term,SHAHexCodes) :-
3492 raw_sha_hash(Term,RawListOfBytes),
3493 get_hex_bytes(RawListOfBytes,SHAHexCodes).
3494
3495
3496
3497 %-------------------
3498
3499 % returns list of strings for info string such as files, variables,...
3500 external_fun_type('PROJECT_STATISTICS',[],[string,integer]).
3501 expects_waitflag('PROJECT_STATISTICS').
3502 expects_spaninfo('PROJECT_STATISTICS').
3503 :- public 'PROJECT_STATISTICS'/4.
3504 'PROJECT_STATISTICS'(Str,Res,Span,WF) :-
3505 kernel_waitflags:get_wait_flag(10,'PROJECT_STATISTICS',WF,WF10), % will enumerate possible input strings
3506 project_stats1(Str,Res,WF10,Span).
3507
3508 :- use_module(bmachine,[b_machine_statistics/2]).
3509 :- block project_stats1(-,?,-,?).
3510 project_stats1(string(INFO),Res,_,Span) :-
3511 if(b_machine_statistics(INFO,Nr), Res=int(Nr),
3512 add_error('PROJECT_STATISTICS','Unknown info field: ',INFO,Span)).
3513
3514
3515 % returns list of strings for info string such as files, variables,...
3516 external_fun_type('PROJECT_INFO',[],[string,set(string)]).
3517 expects_waitflag('PROJECT_INFO').
3518 expects_spaninfo('PROJECT_INFO').
3519 :- public 'PROJECT_INFO'/4.
3520 'PROJECT_INFO'(Str,Res,Span,WF) :-
3521 kernel_waitflags:get_wait_flag(10,'PROJECT_INFO',WF,WF10), % will enumerate possible input strings
3522 project_info1(Str,Res,WF10,Span).
3523
3524 :- block project_info1(-,?,-,?).
3525 project_info1(string(INFO),Res,_,_Span) :- INFO==help,!,
3526 L = [files, absolute-files, main-file, main-machine, sha-hash,
3527 variables, constants, sets, operations, assertion_labels, invariant_labels],
3528 maplist(make_string,L,SL),
3529 kernel_objects:equal_object(SL,Res).
3530 project_info1(string(INFO),Res,_,Span) :-
3531 if(list_info(INFO,L),
3532 (maplist(make_string,L,SL),
3533 kernel_objects:equal_object(SL,Res)),
3534 (add_error(external_functions,'Illegal argument for PROJECT_INFO or :list (use help to obtain valid arguments) : ',INFO,Span),
3535 fail)).
3536
3537 :- use_module(bmachine).
3538 :- use_module(bsyntaxtree, [get_texpr_ids/2, get_texpr_label/2]).
3539 :- use_module(tools,[get_tail_filename/2]).
3540 list_info(files,TL) :- (b_get_all_used_filenames(L) -> true ; L=[]), maplist(get_tail_filename,L,TL).
3541 list_info('absolute-files',L) :- (b_get_all_used_filenames(L) -> true ; L=[]).
3542 list_info('main-file',L) :- (b_get_main_filename(F) -> get_tail_filename(F,TF),L=[TF] ; L=[]).
3543 list_info('main-machine',L) :- findall(Name,get_full_b_machine(Name,_),L). % gets only the main machine
3544 list_info('sha-hash',[AtomHash]) :-
3545 get_full_b_machine_sha_hash(Bytes),
3546 get_hex_bytes(Bytes,Hash), atom_codes(AtomHash,Hash).
3547 list_info(variables,L) :- b_get_machine_variables(LT), get_texpr_ids(LT,L).
3548 list_info(constants,L) :- b_get_machine_constants(LT), get_texpr_ids(LT,L).
3549 list_info(sets,L) :- findall(S,b_get_machine_set(S),L).
3550 list_info(operations,L) :- findall(S,b_top_level_operation(S),L).
3551 list_info(assertion_labels,L) :-
3552 findall(ID,(b_get_assertions(all,_,Ass), member(Assertion,Ass),get_texpr_label(Assertion,ID)),L).
3553 list_info(invariant_labels,L) :-
3554 findall(ID,(b_get_invariant_from_machine(C), conjunction_to_list(C,CL),
3555 member(Inv,CL),get_texpr_label(Inv,ID)),L).
3556
3557
3558 make_string(X,Res) :- atom(X),!,Res=string(X).
3559 make_string(X,Res) :- format_to_codes('~w',X,C), atom_codes(Atom,C), Res=string(Atom).
3560
3561 % obtain the source code of an identifier
3562 external_fun_type('SOURCE',[],[string,string]).
3563 :- public 'SOURCE'/2.
3564 'SOURCE'(string(ID),SourceCode) :- source2(ID,SourceCode).
3565 :- block source2(-,?).
3566 source2(ID,SourceCode) :-
3567 source_code_for_identifier(ID,_,_,_OriginStr,_,Source),
3568 translate:translate_bexpression(Source,SC),
3569 SourceCode = string(SC).
3570
3571
3572 % obtain various information about ProB (STRING result)
3573 external_fun_type('PROB_INFO_STR',[],[string,string]).
3574 expects_waitflag('PROB_INFO_STR').
3575 :- assert_must_succeed(external_functions:'PROB_INFO_STR'(string('prob-version'),string(_),_)).
3576 :- public 'PROB_INFO_STR'/3.
3577 % :- block 'PROB_INFO_STR'(-,?). % no block: this way we can via backtracking generate solutions
3578 'PROB_INFO_STR'(Str,Res,WF) :-
3579 kernel_waitflags:get_wait_flag(10,'PROB_INFO_STR',WF,WF10), % will enumerate possible input strings
3580 prob_info1(Str,Res,WF10,WF).
3581
3582 :- use_module(tools,[ajoin_with_sep/3]).
3583 :- block prob_info1(-,?,-,?).
3584 prob_info1(string(INFO),Res,_,WF) :-
3585 if(prob_info2(INFO,Str),true,
3586 (findall(I,prob_info2(I,_),Is),
3587 ajoin_with_sep(['Unknown info field, known fields:'|Is],' ',Msg),
3588 add_error_wf('PROB_INFO_STR',Msg,I,unknown,WF),
3589 Str = 'ERROR'
3590 )),
3591 make_string(Str,Res).
3592
3593 :- use_module(probsrc(tools_strings),[ajoin/2]).
3594 :- use_module(parsercall,[get_parser_version/1, get_java_command_path/1, get_java_fullversion/3]).
3595 :- use_module(version, [version_str/1, revision/1, lastchangeddate/1]).
3596 prob_info2('prob-version',V) :- version_str(V).
3597 prob_info2('parser-version',V) :- get_parser_version(V).
3598 prob_info2('prolog-version',V) :- current_prolog_flag(version,V).
3599 prob_info2('prob-revision',V) :- revision(V).
3600 prob_info2('prob-last-changed-date',V) :- lastchangeddate(V).
3601 prob_info2('java-version',V) :- get_java_fullversion(Maj,Min,Sfx), ajoin([Maj,'.',Min,'.',Sfx],V).
3602 prob_info2('java-command-path',V) :- get_java_command_path(V).
3603 prob_info2('current-time',V) :- get_info2(time,string(V)). % Maybe we can get rid of GET_INFO ?
3604
3605
3606 % obtain various information about ProB (INTEGER result)
3607 external_fun_type('PROB_STATISTICS',[],[string,integer]).
3608 expects_waitflag('PROB_STATISTICS').
3609 expects_spaninfo('PROB_STATISTICS').
3610 :- public 'PROB_STATISTICS'/4.
3611 'PROB_STATISTICS'(Str,Res,Span,WF) :-
3612 kernel_waitflags:get_wait_flag(10,'PROB_STATISTICS',WF,WF10), % will enumerate possible input strings
3613 prob_info_int1(Str,Res,Span,WF10,WF).
3614
3615 % old name of function:
3616 :- public 'PROB_INFO_INT'/4.
3617 'PROB_INFO_INT'(Str,Res,Span,WF) :- 'PROB_STATISTICS'(Str,Res,Span,WF).
3618
3619 :- block prob_info_int1(-,?,?,-,?).
3620 prob_info_int1(string(INFO),Res,Span,_,WF) :-
3621 if(prob_info_int1(INFO,I), Res=int(I),
3622 (add_error_wf('PROB_STATISTICS','Unknown info field: ',INFO,Span,WF),
3623 fail)).
3624
3625 :- use_module(state_space_exploration_modes,[get_current_breadth_first_level/1]).
3626 :- use_module(state_space,[get_state_space_stats/3]).
3627 prob_info_int1('current-state-id',StateIDNr) :- get_current_state_id(ID),convert_id_to_nr(ID,StateIDNr).
3628 prob_info_int1('states',NrNodes) :- get_state_space_stats(NrNodes,_,_).
3629 prob_info_int1('transitions',NrTransitions) :- get_state_space_stats(_,NrTransitions,_).
3630 prob_info_int1('processed-states',ProcessedNodes) :- get_state_space_stats(_,_,ProcessedNodes).
3631 prob_info_int1('bf-level',Level) :- (get_current_breadth_first_level(R) -> Level = R ; Level = -1).
3632 prob_info_int1('now-timestamp',N) :- now(N). % provide UNIX timesstamp
3633 prob_info_int1('prolog-runtime',V) :- statistics(runtime,[V,_]).
3634 prob_info_int1('prolog-walltime',V) :- statistics(walltime,[V,_]).
3635 prob_info_int1('prolog-memory-bytes-used',V) :- statistics(memory_used,V).
3636 prob_info_int1('prolog-memory-bytes-free',V) :- statistics(memory_free,V).
3637 prob_info_int1('prolog-global-stack-bytes-used',V) :- statistics(global_stack_used,V).
3638 prob_info_int1('prolog-local-stack-bytes-used',V) :- statistics(local_stack_used,V).
3639 %prob_info_int1('prolog-global-stack-bytes-free',V) :- statistics(global_stack_free,V).
3640 %prob_info_int1('prolog-local-stack-bytes-free',V) :- statistics(local_stack_free,V).
3641 prob_info_int1('prolog-trail-bytes-used',V) :- statistics(trail_used,V).
3642 prob_info_int1('prolog-choice-bytes-used',V) :- statistics(choice_used,V).
3643 prob_info_int1('prolog-atoms-bytes-used',V) :- statistics(atoms_used,V).
3644 prob_info_int1('prolog-atoms-nb-used',V) :- statistics(atoms_nbused,V).
3645 prob_info_int1('prolog-gc-count',V) :- statistics(gc_count,V).
3646 prob_info_int1('prolog-gc-time',V) :- statistics(gc_time,V).
3647
3648 % --------------------
3649
3650 % coverage/projection functions:
3651
3652 external_fun_type('STATE_VALUES',[T],[string,set(couple(couple(integer,integer),T))]).
3653 expects_unevaluated_args('STATE_VALUES').
3654 :- public 'STATE_VALUES'/3.
3655 :- block 'STATE_VALUES'(-,?,?).
3656 'STATE_VALUES'(_Value,Res,[AST]) :-
3657 state_space_reduction:compute_set_of_covered_values_for_typed_expression(AST,Set),
3658 kernel_objects:equal_object_optimized(Set,Res).
3659
3660 % TODO: other projection/reduction operators: projection as graph, ...
3661 % could be useful to have a minimum/maximum operator on sets which uses Prolog order in avl
3662
3663 % -----------------
3664
3665 % obtain various information about bvisual2 Formulas
3666 external_fun_type('FORMULA_INFOS',[],[string,seq(string)]).
3667 expects_waitflag('FORMULA_INFOS').
3668 :- public 'FORMULA_INFOS'/3.
3669 'FORMULA_INFOS'(Str,Res,WF) :-
3670 kernel_waitflags:get_wait_flag(10,'FORMULA_INFOS',WF,WF10), % will enumerate possible input strings
3671 formula_info(Str,_,Res,_,WF10).
3672 external_fun_type('FORMULA_VALUES',[],[string,seq(string)]).
3673 expects_waitflag('FORMULA_VALUES').
3674 :- public 'FORMULA_VALUES'/3.
3675 'FORMULA_VALUES'(Str,Res,WF) :-
3676 kernel_waitflags:get_wait_flag(10,'FORMULA_VALUES',WF,WF10), % will enumerate possible input strings
3677 formula_info(Str,_,_,Res,WF10).
3678
3679 :- use_module(extrasrc(bvisual2),[bv_get_top_level_formula/4, bv_value_to_atom/2]).
3680
3681 % valid TopLevelCategories are constants, definitions, guards_top_level, inv, sets, variables
3682 :- block formula_info(-,?,?,?,-).
3683 formula_info(string(TopLevelCategory),CatTextRes,LabelRes,ValuesRes,_) :-
3684 bv_get_top_level_formula(TopLevelCategory,CatText,Labels,Values),
3685 CatTextRes = string(CatText),
3686 maplist(make_string,Labels,LS),
3687 convert_list_to_seq(LS,LabelRes),
3688 maplist(make_value,Values,LV),
3689 convert_list_to_seq(LV,ValuesRes).
3690
3691 make_value(V,string(A)) :- bv_value_to_atom(V,A).
3692 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3693
3694
3695 % --------------------------
3696
3697 :- use_module(covsrc(hit_profiler),[add_hit/2, add_hit_if_not_covered/2,
3698 get_profile_statistics/2, profile_functor/1]). %profiler:profile_statistics.
3699
3700 :- public 'GET_PROFILE_STATISTICS'/3.
3701 is_not_declarative('GET_PROFILE_STATISTICS').
3702 :- block 'GET_PROFILE_STATISTICS'(-,?,?).
3703 'GET_PROFILE_STATISTICS'(string(PP),_DummyType,Res) :- % DummyType is just there for typing purposes
3704 if(profile_functor(PP),
3705 (get_profile_statistics(PP,Hits),
3706 maplist(translate_hit_to_b,Hits,List)),
3707 List = []),
3708 equal_object_optimized(List,Res, 'GET_PROFILE_STATISTICS').
3709 %equal_object(List,Res,'GET_PROFILE_STATISTICS'), print(res(Res)),nl.
3710
3711 translate_hit_to_b(hit(Arg,Nr),(Arg,int(Nr))).
3712
3713 :- public 'GET_PROFILE_POINTS'/1.
3714 'GET_PROFILE_POINTS'(Res) :- findall(string(S),profile_functor(S),List),
3715 equal_object_optimized(List,Res,'PROFILE_POINT').
3716
3717 expects_spaninfo('PROFILE').
3718 :- public 'PROFILE'/5.
3719 :- block 'PROFILE'(-,?,?,?,?), 'PROFILE'(?,-,?,?,?). %, 'PROFILE'(?,-,?,?,?).
3720 'PROFILE'(string(PP),Count,Value,ValueRes,SpanInfo) :-
3721 add_profile_exf_hit(Value,PP,SpanInfo,Count),
3722 equal_object(Value,ValueRes,'PROFILE').
3723
3724 :- block add_profile_exf_hit(-,?,?,?), add_profile_exf_hit(?,-,?,?).
3725 add_profile_exf_hit(pred_true,PP,SpanInfo,Count) :- !, add_value_hit(Count,pred_true,PP,SpanInfo).
3726 add_profile_exf_hit(pred_false,PP,SpanInfo,Count) :- !, add_value_hit(Count,pred_false,PP,SpanInfo).
3727 add_profile_exf_hit(int(X),PP,SpanInfo,Count) :- !, add_int_hit(X,PP,SpanInfo,Count).
3728 add_profile_exf_hit(string(X),PP,SpanInfo,Count) :- !, add_string_hit(X,PP,SpanInfo,Count).
3729 add_profile_exf_hit(Value,PP,SpanInfo,Count) :- when(ground(Value), add_complex_hit(Value,PP,SpanInfo,Count)).
3730
3731 add_complex_hit(Value,PP,SpanInfo,Count) :- print(PP), print(' : '), translate:print_bvalue(Value),nl,
3732 add_value_hit(Count,Value,PP,SpanInfo).
3733
3734 :- block add_int_hit(-,?,?,?).
3735 add_int_hit(X,PP,SpanInfo,Count) :- add_value_hit(Count,int(X),PP,SpanInfo).
3736 :- block add_string_hit(-,?,?,?).
3737 add_string_hit(X,PP,SpanInfo,Count) :- add_value_hit(Count,string(X),PP,SpanInfo).
3738
3739 add_value_hit(pred_true,Val,PP,_) :- add_hit(PP,Val).
3740 add_value_hit(pred_false,Val,PP,_) :- add_hit_if_not_covered(PP,Val).
3741
3742 % -------------------
3743
3744 :- use_module(memoization,[get_complete_memoization_expansion/6]).
3745
3746 expects_spaninfo('MEMOIZE_STORED_FUNCTION').
3747 expects_waitflag('MEMOIZE_STORED_FUNCTION').
3748 :- public 'MEMOIZE_STORED_FUNCTION'/4.
3749 :- block 'MEMOIZE_STORED_FUNCTION'(-,?,?,?).
3750 'MEMOIZE_STORED_FUNCTION'(int(MemoID),Res,Span,WF) :- memoize_get_aux(MemoID,Res,Span,WF).
3751
3752 :- block memoize_get_aux(-,?,?,?).
3753 memoize_get_aux(MemoID,Res,Span,WF) :-
3754 if(get_complete_memoization_expansion(MemoID,RV,_Done,Span,'MEMOIZE_STORED_FUNCTION',WF),
3755 kernel_objects:equal_object_wf(Res,RV,WF),
3756 add_error(external_functions,'Function ID not registered:',MemoID,Span)).
3757
3758 % -------------------
3759
3760 :- use_module(eval_let_store,[stored_let_value/3, set_stored_let_value/3,
3761 retract_stored_let_value/3, reset_let_values/0,
3762 extend_state_with_stored_lets/2, get_stored_let_typing_scope/1]).
3763
3764 :- public 'STORE'/4.
3765 external_fun_type('STORE',[X],[X,X]).
3766 expects_waitflag('STORE').
3767 expects_unevaluated_args('STORE').
3768 % stores values just like :let in the REPL does, but can be used within a predicate;
3769 % here name inferred from AST and it is a transparent function for more convenient annotation
3770 :- block 'STORE'(-,?,?,?).
3771 'STORE'(Val,Res,[TVal],WF) :- equal_object_optimized_wf(Val,Res,'STORE',WF),
3772 (translate:try_get_identifier(TVal,ID) -> true % also checks for was_identifier
3773 ; translate:translate_bexpression(TVal,ID),
3774 add_warning('STORE','The expression is not an identifier:',ID,TVal)
3775 ),
3776 'STORE_VALUE'(string(ID),Val,pred_true,[_,TVal],WF).
3777
3778 external_fun_type('STORE_VALUE',[X],[string,X,boolean]).
3779 expects_waitflag('STORE_VALUE').
3780 expects_unevaluated_args('STORE_VALUE').
3781 % stores values just like :let in the REPL does, but can be used within a predicate
3782 :- block 'STORE_VALUE'(-,?,?,?,?).
3783 'STORE_VALUE'(string(ID),Val,PredRes,[_,TVal],WF) :- PredRes=pred_true,
3784 get_enumeration_finished_wait_flag(WF,EWF),
3785 get_texpr_type(TVal,Type),
3786 store_value(ID,Type,Val,EWF).
3787
3788 :- block store_value(-,?,?,?), store_value(?,?,?,-).
3789 store_value(ID,Type,Val,_) :-
3790 set_stored_let_value(ID,Type,Val).
3791
3792
3793 :- use_module(btypechecker, [unify_types_werrors/4]).
3794 :- public 'RECALL_VALUE'/5.
3795 external_fun_type('RECALL_VALUE',[X],[string,X]).
3796 expects_waitflag('RECALL_VALUE').
3797 expects_spaninfo('RECALL_VALUE').
3798 expects_type('RECALL_VALUE').
3799 :- block 'RECALL_VALUE'(-,?,?,?,?).
3800 'RECALL_VALUE'(string(ID),Res,Type,Span,WF) :-
3801 recall_value(ID,Res,Type,Span,WF).
3802
3803 recall_value(ID,Res,Type,Span,WF) :-
3804 stored_let_value(ID,StoredType,Val),
3805 !,
3806 (unify_types_werrors(Type,StoredType,Span,'RECALL_VALUE')
3807 -> equal_object_optimized_wf(Val,Res,'RECALL_VALUE',WF)
3808 ; add_error_wf('RECALL_VALUE','Stored value has incompatible type:',ID,Span,WF)
3809 ).
3810 recall_value(ID,_,_,Span,WF) :-
3811 add_error_wf('RECALL_VALUE','No value stored with STORE_VALUE or :let for:',ID,Span,WF),
3812 fail.
3813
3814 % TODO: do we need a DELETE_STORED_VALUE external function
3815
3816 % -------------------
3817 % a few ugraphs (unweighted graphs) utilities:
3818
3819 % an alternate implementation of closure1
3820 expects_spaninfo('CLOSURE1').
3821 external_fun_type('CLOSURE1',[X],[set(couple(X,X)),set(couple(X,X))]).
3822 :- public 'CLOSURE1'/3.
3823 :- block 'CLOSURE1'(-,?,?).
3824 'CLOSURE1'([],Res,_) :- !, kernel_objects:equal_object(Res,[]).
3825 'CLOSURE1'(avl_set(A),Res,_) :- !, closure1_for_avl_set(A,R), kernel_objects:equal_object_optimized(R,Res).
3826 'CLOSURE1'(A,Res,Span) :- ground_value_check(A,Gr), closure1_gr(A,Gr,Res,Span).
3827
3828 closure1_gr(Set,_,Res,Span) :- convert_to_avl(Set,AVL),!, 'CLOSURE1'(AVL,Res,Span).
3829 closure1_gr(Set,_,_,Span) :-
3830 add_error(external_functions,'Cannot convert CLOSURE1 argument to set: ',Set,Span).
3831
3832 % compute strongly connected components
3833 expects_spaninfo('SCCS').
3834 external_fun_type('SCCS',[X],[set(couple(X,X)),set(set(X))]).
3835 :- public 'SCCS'/3.
3836 :- block 'SCCS'(-,?,?).
3837 'SCCS'([],Res,_) :- !, kernel_objects:equal_object(Res,[]).
3838 'SCCS'(avl_set(A),Res,_) :- !, sccs_for_avl_set(A,R), kernel_objects:equal_object_optimized(R,Res).
3839 'SCCS'(A,Res,Span) :- ground_value_check(A,Gr), sccs_gr(A,Gr,Res,Span).
3840
3841 sccs_gr(Set,_,Res,Span) :- convert_to_avl(Set,AVL),!, 'SCCS'(AVL,Res,Span).
3842 sccs_gr(Set,_,_,Span) :-
3843 add_error(external_functions,'Cannot convert SCCS argument to set: ',Set,Span).
3844
3845 :- use_module(extrasrc(avl_ugraphs),[avl_transitive_closure/2, avl_scc_sets/2]).
3846 closure1_for_avl_set(A,Res) :-
3847 avl_transitive_closure(A,TC),
3848 construct_avl_set(TC,Res).
3849 sccs_for_avl_set(A,Res) :-
3850 avl_scc_sets(A,TC),
3851 construct_avl_set(TC,Res).
3852 construct_avl_set(Avl,Res) :- empty_avl(Avl) -> Res = [] ; Res = avl_set(Avl).
3853 % -------------------
3854
3855 reset_kodkod :-
3856 true. %retractall(kodkod_pred(_,_)).
3857
3858 %:- use_module(probsrc(bsyntaxtree), [b_compute_expression/5]).
3859
3860 % KODKOD(ProblemID, LocalIDsOfPredicate, WaitToBeGroundBeforePosting, PredicateAsBooleanFunction)
3861 % EXTERNAL_PREDICATE_KODKOD(T1,T2) == INTEGER*T1*T2*BOOL;
3862 %:- dynamic kodkod_pred/2. % now stored as attribute in WF store
3863 do_not_evaluate_args('KODKOD').
3864 expects_unevaluated_args('KODKOD').
3865 expects_waitflag('KODKOD').
3866 expects_spaninfo('KODKOD').
3867 expects_state('KODKOD').
3868
3869 :- use_module(bsyntaxtree,[create_negation/2]).
3870 :- use_module(b_compiler,[b_optimize/6]).
3871 :- use_module(b_interpreter,[b_compute_expression/5]).
3872 :- public 'KODKOD'/6.
3873 :- block 'KODKOD'(-,?,?,?,?,?).
3874 'KODKOD'(PredRes,LocalState,State,UnevaluatedArgs,Span,WF) :-
3875 UnevaluatedArgs = [TID,IDEXPR,WAITIDEXPR,UEA],
3876 get_integer(TID,ID),
3877 construct_predicate(UEA,KPredicate),
3878 (PredRes == pred_false -> create_negation(KPredicate,Predicate) ; Predicate=KPredicate),
3879 must_get_identifiers('KODKOD',IDEXPR,TIdentifiers),
3880 get_texpr_ids(TIdentifiers,Ids),
3881 b_compute_expression(WAITIDEXPR,LocalState,State,WaitVal,WF),
3882 when(ground(WaitVal),
3883 ( b_optimize(Predicate,Ids,LocalState,State,CPredicate,WF),
3884 (debug:debug_mode(off) -> true
3885 ; add_message(kodkod,'STORING FOR KODKOD : ',ID:PredRes,Span), translate:print_bexpr(CPredicate),nl),
3886 kernel_waitflags:my_add_predicate_to_kodkod(WF,ID,CPredicate),
3887 %assertz(kodkod_pred(ID,CPredicate)), % TO DO: attach to WF Store !; assertz will break Prolog variable links !
3888 % TO DO: retract upon backtracking + store negation if PredRes = pred_false
3889 PredRes=pred_true
3890 )).
3891
3892
3893 :- use_module(probsrc(bsyntaxtree), [safe_create_texpr/3]).
3894 construct_predicate(b(convert_bool(P),_,_),Res) :- !, Res=P.
3895 construct_predicate(BoolExpr,Res) :-
3896 safe_create_texpr(equal(BoolExpr,b(boolean_true,boolean,[])),pred,Res).
3897
3898 :- use_module(kodkodsrc(kodkod), [replace_by_kodkod/3]).
3899 % EXTERNAL_PREDICATE_KODKOD_SOLVE(T1,T2) == INTEGER*T1*T2;
3900 expects_unevaluated_args('KODKOD_SOLVE').
3901 expects_waitflag('KODKOD_SOLVE').
3902 expects_state('KODKOD_SOLVE').
3903 :- public 'KODKOD_SOLVE'/8.
3904 :- block 'KODKOD_SOLVE'(-,?,?,?,?,?,?,?).
3905 'KODKOD_SOLVE'(int(ID),Ids,WaitIds,PredRes,LocalState,State,UEA,WF) :-
3906 when(ground(WaitIds),
3907 kodkod_solve_aux(ID,Ids,WaitIds,PredRes,LocalState,State,UEA,WF)).
3908
3909 :- use_module(library(ordsets),[ord_subtract/3]).
3910 kodkod_solve_aux(ID,Ids,_WaitIds,PredRes,LocalState,State,UEA,WF) :-
3911 %print(trigger_SOLVE(_WaitIds)),nl,
3912 get_wait_flag(2,'KODKOD_SOLVE',WF,LWF), % give other co-routines chance to fire
3913 kodkod_solve_aux2(ID,Ids,PredRes,LocalState,State,UEA,WF,LWF).
3914
3915 :- block kodkod_solve_aux2(?,?,?,?,?,?,?,-).
3916 kodkod_solve_aux2(ID,_,PredRes,LocalState,State,[_,IDEXPR,WAITIDEXPR],WF,_) :-
3917 %print(ls(LocalState,State)),nl,
3918 %findall(P,kodkod_pred(ID,P),Ps), % TO DO: obtain from WF Store
3919 kernel_waitflags:my_get_kodkod_predicates(WF,ID,Ps),
3920 length(Ps,Len),
3921 reverse(Ps,RPs), % we reverse Ps to put predicates in same order they were added by KODKOD / seems to influence analysis time
3922 conjunct_predicates(RPs,Predicate),
3923 %translate:print_bexpr(Predicate),nl,
3924 must_get_identifiers('KODKOD_SOLVE',IDEXPR,TIdentifiers),
3925 get_texpr_ids(TIdentifiers,Ids),
3926 ((get_identifiers(WAITIDEXPR,TWaitIds,[]), get_texpr_ids(TWaitIds,WaitIds),
3927 sort(WaitIds,SWIds),
3928 formatsilent('KODKOD_SOLVE Problem ~w (~w conjuncts), Identifiers: ~w, Waiting for ~w~n',[ID,Len,Ids,SWIds]),
3929 sort(Ids,SIds),
3930 ord_subtract(SIds,SWIds,IdsToSolve))
3931 -> b_optimize(Predicate,IdsToSolve,LocalState,State,CPredicate,WF), % inline known values
3932 (silent_mode(on) -> true ; print('compiled: '),translate:print_bexpr(CPredicate),nl,nl)
3933 ; CPredicate=Predicate
3934 ),
3935 (replace_by_kodkod(TIdentifiers,CPredicate,NewPredicate)
3936 -> (silent_mode(on) -> true ; print('AFTER KODKOD: '),translate:print_bexpr(NewPredicate),nl),
3937 b_interpreter:b_test_boolean_expression(NewPredicate,LocalState,State,WF)
3938 ; print('KODKOD cannot be applied'),nl,
3939 b_interpreter:b_test_boolean_expression(CPredicate,LocalState,State,WF)
3940 ),
3941 PredRes=pred_true.
3942
3943 must_get_identifiers(PP,TExpr,Res) :-
3944 (get_identifiers(TExpr,Ids,[]) -> Res=Ids
3945 ; add_error(PP,'Could not get identifiers: ',TExpr),fail).
3946
3947 get_identifiers(b(couple(A1,A2),_,_)) --> !, get_identifiers(A1), get_identifiers(A2).
3948 get_identifiers(b(identifier(ID),T,I)) --> [b(identifier(ID),T,I)].
3949 get_identifiers(b(integer(_),_,_)) --> []. % to do: accept other ground values; in case they are compiled
3950 get_identifiers(b(value(_),_,_)) --> []. % identifier has already been compiled
3951 get_identifiers(b(string(_),_,_)) --> [].
3952
3953
3954 % -------------------
3955 do_not_evaluate_args('SATSOLVER').
3956 expects_unevaluated_args('SATSOLVER').
3957 expects_waitflag('SATSOLVER').
3958 expects_spaninfo('SATSOLVER').
3959 expects_state('SATSOLVER').
3960
3961 :- use_module(kernel_tools,[value_variables/2]).
3962 :- public 'SATSOLVER'/6.
3963 :- block 'SATSOLVER'(-,?,?,?,?,?).
3964 'SATSOLVER'(PredRes,LocalState,State,UnevaluatedArgs,Span,WF) :-
3965 UnevaluatedArgs = [TID,IDEXPR,WAITIDEXPR,UEA],
3966 get_integer(TID,ID),
3967 construct_predicate(UEA,KPredicate),
3968 (PredRes == pred_false -> create_negation(KPredicate,Predicate) ; Predicate=KPredicate),
3969 must_get_identifiers('SATSOLVER',IDEXPR,TIdentifiers),
3970 get_texpr_ids(TIdentifiers,Ids),
3971 % Note: the Ids are not really necessary here; they are just used for b_optimize; see SATSOLVER_SOLVE below
3972 b_interpreter:b_compute_expression(WAITIDEXPR,LocalState,State,WaitVal,WF),
3973 value_variables(WaitVal,WVars),
3974 when(ground(WVars),
3975 ( %print(compile_for(ID,Ids)),nl,
3976 %nl,add_message(satsolver,'Optimzing for SATSOLVER_SOLVE: ',Predicate,Span), debug:nl_time,
3977 %translate:nested_print_bexpr(Predicate),nl,
3978 b_optimize(Predicate,Ids,LocalState,State,CPredicate,WF), % Ids are left in the closure
3979 (debug:debug_mode(off) -> true
3980 ; add_message(satsolver,'Storing for SATSOLVER_SOLVE: ',CPredicate,Span)
3981 ),
3982 kernel_waitflags:my_add_predicate_to_satsolver(WF,ID,CPredicate),
3983 % TO DO: retract upon backtracking + store negation if PredRes = pred_false
3984 PredRes=pred_true
3985 )).
3986
3987 expects_unevaluated_args('SATSOLVER_SOLVE').
3988 expects_waitflag('SATSOLVER_SOLVE').
3989 expects_state('SATSOLVER_SOLVE').
3990 :- public 'SATSOLVER_SOLVE'/8.
3991 :- block 'SATSOLVER_SOLVE'(-,?,?,?,?,?,?,?).
3992 'SATSOLVER_SOLVE'(int(ID),Ids,WaitIds,PredRes,LocalState,State,UEA,WF) :-
3993 value_variables(WaitIds,WVars),
3994 get_wait_flag1('SATSOLVER_SOLVE',WF,WF1),
3995 when(ground((WF1,WVars)),
3996 satsolver_solve_aux(ID,Ids,WaitIds,PredRes,LocalState,State,UEA,WF)).
3997 % Note: the Ids are not really necessary here; they are just used for b_optimize
3998 % The b_to_cnf conversion will look up all identifiers anyway, identifier or value(_) node makes no difference!
3999 % TODO: probably remove them
4000
4001 :- use_module(library(ordsets),[ord_subtract/3]).
4002 satsolver_solve_aux(ID,Ids,_WaitIds,PredRes,LocalState,State,UEA,WF) :-
4003 %print(trigger_SOLVE(_WaitIds)),nl,
4004 get_idle_wait_flag('SATSOLVER_SOLVE',WF,LWF), % give other co-routines chance to fire
4005 satsolver_solve_aux2(ID,Ids,PredRes,LocalState,State,UEA,WF,LWF).
4006
4007 :- use_module(extension('satsolver/b2sat'), [solve_predicate_with_satsolver/2]).
4008
4009 :- block satsolver_solve_aux2(?,?,?,?,?,?,?,-).
4010 satsolver_solve_aux2(ID,_,PredRes,LocalState,State,[_,IDEXPR,WAITIDEXPR],WF,_) :-
4011 print('SATSOLVER_SOLVE:'),nl,
4012 kernel_waitflags:my_get_satsolver_predicates(WF,ID,Ps),
4013 length(Ps,Len), format('Got ~w SATSOLVER predicates for ID: ~w~n',[Len,ID]),
4014 reverse(Ps,RPs), % we reverse Ps to put predicates in same order they were added, necessary??
4015 conjunct_predicates(RPs,Predicate),
4016 %translate:print_bexpr(Predicate),nl,
4017 must_get_identifiers('SATSOLVER_SOLVE',IDEXPR,TIdentifiers),
4018 get_texpr_ids(TIdentifiers,Ids),
4019 ((get_identifiers(WAITIDEXPR,TWaitIds,[]), get_texpr_ids(TWaitIds,WaitIds),
4020 sort(WaitIds,SWIds),
4021 formatsilent('Sat Solver identifiers: ~w ; waiting for ~w~n',[Ids,SWIds]),
4022 sort(Ids,SIds),
4023 ord_subtract(SIds,SWIds,IdsToSolve))
4024 -> b_optimize(Predicate,IdsToSolve,LocalState,State,CPredicate,WF), % inline known values
4025 (debug_mode(off) -> true
4026 ; print('compiled: '),translate:print_bexpr(CPredicate),nl,nl)
4027 ; CPredicate=Predicate
4028 ),
4029 (solve_predicate_with_satsolver(CPredicate,State)
4030 % if(b_interpreter:b_test_boolean_expression(CPredicate,[],State,WF),print(ok),
4031 % add_error_wf('SATSOLVER_SOLVE','SAT result not confirmed by ProB:',ID,CPredicate,WF))
4032 % TODO: catch errors if b_sat fails!
4033 %-> true
4034 % ; print('Calling SAT solver failed'),nl,
4035 % b_interpreter:b_test_boolean_expression(CPredicate,LocalState,State,WF)
4036 ),
4037 PredRes=pred_true.
4038 % -------------------
4039
4040
4041 expects_waitflag('UNSAT_CORE'). % WF not used at the moment
4042 expects_spaninfo('UNSAT_CORE').
4043 :- public 'UNSAT_CORE'/5.
4044 % EXTERNAL_FUNCTION_UNSAT_CORE(T) == (POW(T)-->BOOL)*POW(T) --> POW(T);
4045 % UNSAT_CORE(Fun,Set) == Set
4046 % example: UNSAT_CORE(f,0..200) = {2} with f = %x.(x:POW(INTEGER)|bool(x /\ 1..2={}))
4047 'UNSAT_CORE'(FunToBool,Set,ValueRes,SpanInfo,WF) :-
4048 'UNSAT_CORE_ACC'(FunToBool,Set,[],ValueRes,SpanInfo,WF).
4049
4050
4051 expects_waitflag('UNSAT_CORE_ACC'). % WF not used at the moment
4052 expects_spaninfo('UNSAT_CORE_ACC').
4053 % EXTERNAL_FUNCTION_UNSAT_CORE_ACC(T) == (POW(T)-->BOOL)*POW(T)*POW(T) --> POW(T);
4054 % UNSAT_CORE_ACC(Fun,Set,Acc) == Set\/Acc;
4055 % example: UNSAT_CORE_ACC(f,0..200,{}) = {2} & f = %x.(x:POW(INTEGER)|bool(x /\ 1..2={}))
4056 % provides a way to initialise the accumulator of the unsat core computation
4057 'UNSAT_CORE_ACC'(FunToBool,Set,Acc,ValueRes,SpanInfo,WF) :-
4058 custom_explicit_sets:expand_custom_set_to_list_wf(Set,ESet,_,compute_apply_true,WF),
4059 custom_explicit_sets:expand_custom_set_to_list_wf(Acc,EAcc,_,compute_apply_true,WF),
4060 debug_println(9,computing_unsat_core(ESet,EAcc)),
4061 when(ground((FunToBool,ESet)), compute_unsat_core(ESet,FunToBool,no_time_out,EAcc,ValueRes,SpanInfo,WF)).
4062
4063 % EXTERNAL_FUNCTION_UNSAT_CORE_ACC_TIMEOUT(T) == (POW(T)-->BOOL)*POW(T)*POW(T)*INTEGER --> POW(T);
4064 % UNSAT_CORE_ACC_TIMEOUT(Fun,Set,Acc,TO) == Set\/Acc;
4065 % example: UNSAT_CORE_ACC_TIMEOUT(f,0..200,{},100) = {2} & f = %x.(x:POW(INTEGER)|bool(x /\ 1..2={}))
4066 expects_waitflag('UNSAT_CORE_ACC_TIMEOUT'). % WF not used at the moment
4067 expects_spaninfo('UNSAT_CORE_ACC_TIMEOUT').
4068 :- public 'UNSAT_CORE_ACC_TIMEOUT'/7.
4069 'UNSAT_CORE_ACC_TIMEOUT'(FunToBool,Set,Acc,int(TimeOut),ValueRes,SpanInfo,WF) :-
4070 custom_explicit_sets:expand_custom_set_to_list_wf(Set,ESet,_,compute_apply_true,WF),
4071 custom_explicit_sets:expand_custom_set_to_list_wf(Acc,EAcc,_,compute_apply_true,WF),
4072 debug_println(9,computing_unsat_core(ESet,EAcc)),
4073 when(ground((FunToBool,ESet,TimeOut)), compute_unsat_core(ESet,FunToBool,TimeOut,EAcc,ValueRes,SpanInfo,WF)).
4074
4075 compute_unsat_core([],_FunToBool,_TimeOut,Core,Result,_SpanInfo,WF) :- equal_object_wf(Result,Core,WF).
4076 compute_unsat_core([H|T],FunToBool,TimeOut,Core,Result,SpanInfo,WF) :-
4077 debug_println(9,trying_to_remove(H,core(Core))),
4078 append(Core,T,CoreT),
4079 if(compute_apply_true_timeout(TimeOut,FunToBool,CoreT,SpanInfo),
4080 compute_unsat_core(T,FunToBool,TimeOut,[H|Core],Result,SpanInfo,WF), % we found a solution, H is needed in core
4081 compute_unsat_core(T,FunToBool,TimeOut, Core, Result,SpanInfo,WF) % contradiction also exists without H
4082 ).
4083
4084 :- use_module(library(timeout)).
4085 compute_apply_true_timeout(no_time_out,FunToBool,CoreT,SpanInfo) :- !,
4086 compute_apply_true(FunToBool,CoreT,SpanInfo).
4087 compute_apply_true_timeout(TO,FunToBool,CoreT,SpanInfo) :-
4088 time_out(compute_apply_true(FunToBool,CoreT,SpanInfo), TO, TORes),
4089 (TORes == success -> true ,format(user_output,'~nSUCCESS~n~n',[])
4090 ; format(user_output,'~nTIME-OUT: ~w~n~n',[TORes]),fail). % treat time-out like failure
4091
4092 compute_apply_true(FunToBool,CoreT,SpanInfo) :-
4093 init_wait_flags_with_call_stack(WF1,[prob_command_context(compute_apply_true,unknown)]),
4094 bsets_clp:apply_to(FunToBool,CoreT,pred_true,SpanInfo,WF1), % TO DO: also pass function type
4095 ground_wait_flags(WF1).
4096
4097 expects_waitflag('MAX_SAT').
4098 expects_spaninfo('MAX_SAT').
4099 :- public 'MAX_SAT'/5.
4100 % EXTERNAL_FUNCTION_MAX_SAT(T) == (POW(T)-->BOOL)*POW(T) --> POW(T);
4101 % MAX_SAT(Fun,Set) == Set;
4102 % example: MAX_SAT(f,0..3) = {0,3} & f = %x.(x:POW(INTEGER)|bool(x /\ 1..2={}))
4103
4104 'MAX_SAT'(FunToBool,Set,ValueRes,SpanInfo,WF) :-
4105 custom_explicit_sets:expand_custom_set_to_list_wf(Set,ESet,_,compute_apply_true,WF),
4106 debug_println(9,computing_unsat_core(ESet)),
4107 when(ground((FunToBool,ESet)), compute_maxsat_ground(ESet,FunToBool,ValueRes,SpanInfo,WF)).
4108
4109 compute_maxsat_ground(ESet,FunToBool,ValueRes,SpanInfo,WF) :-
4110 debug_println(9,computing_maxsat(ESet)), %nl,reset_walltime,
4111 get_wait_flag(1,'MAX_SAT',WF,LWF), % avoid computing straightaway in case pending co-routines fail; not really sure it is needed
4112 when(nonvar(LWF),compute_maxsat(ESet,FunToBool,[],ValueRes,SpanInfo,WF)).
4113 compute_maxsat([],_FunToBool,Core,Result,_SpanInfo,_WF) :- equal_object(Result,Core).
4114 compute_maxsat([H|T],FunToBool,Core,Result,SpanInfo,WF) :-
4115 debug_println(9,trying_to_add(H,core(Core))),
4116 %nl,nl,nl,print(maxsat(H,Core)),nl, print_walltime(user_output),nl,
4117 if(compute_apply_true(FunToBool,[H|Core],SpanInfo),
4118 compute_maxsat(T,FunToBool,[H|Core],Result,SpanInfo,WF),
4119 compute_maxsat(T,FunToBool, Core, Result,SpanInfo,WF) % contradiction also exists without H
4120 ).
4121
4122 % can be used to maximize a bounded integer expression
4123 % more limited than optimizing_solver (only optimizing integers), but using inlined branch and bound enumeration
4124 % example usage: xx:1..10 & res=10*xx-xx*xx & MAXIMIZE_EXPR(res)
4125 :- use_module(clpfd_interface,[clpfd_domain/3, clpfd_inrange/3, clpfd_size/2, clpfd_eq/2]).
4126 expects_waitflag('MAXIMIZE_EXPR').
4127 expects_spaninfo('MAXIMIZE_EXPR').
4128 :- public 'MAXIMIZE_EXPR'/4.
4129 'MAXIMIZE_EXPR'(int(X),PredRes,Span,WF) :-
4130 %get_wait_flag1('MAXIMIZE_EXPR',WF,LWF),
4131 get_wait_flag(2,'MAXIMIZE_EXPR',WF,LWF),
4132 PredRes=pred_true,
4133 maximize_expr_wf(LWF,X,Span,WF).
4134 :- block maximize_expr_wf(-,?,?,?).
4135 maximize_expr_wf(_LWF,X,Span,WF) :-
4136 clpfd_size(X,Size), Size \= sup,
4137 clpfd_domain(X,Min,Max),
4138 Mid is round((Min + Max)/2),
4139 !,
4140 maximize_expr_6(Min,Mid,Max,X,Span,WF).
4141 maximize_expr_wf(_,_,Span,_) :-
4142 add_error(external_functions,'MAXIMIZE_EXPR/MINIMIZE_EXPR called on unbounded expression',Span),
4143 fail.
4144 maximize_expr_6(M,M,M,X,Span,WF) :- !, X=M,
4145 add_message(external_functions,'Checking optimisation target for MAXIMIZE_EXPR/MINIMIZE_EXPR: ',X,Span),
4146 ground_wait_flags(WF). % NOTE: without fully grounding WF: we do not know if a solution has really been found !
4147 maximize_expr_6(Min,Mid,Max,X,Span,WF) :- % tools_printing:print_term_summary(maximize_expr_6(Min,Mid,Max,X)),nl,
4148 %add_message(external_functions,'Optimisation target for MAXIMIZE_EXPR/MINIMIZE_EXPR: ',Min:Max,Span),
4149 if( (clpfd_inrange(X,Mid,Max),
4150 NMid is round((Mid+Max)/2),
4151 maximize_expr_6(Mid,NMid,Max,X,Span,WF)),
4152 true, % we found a solution in the upper half
4153 (Mid>Min, M1 is Mid-1,
4154 clpfd_inrange(X,Min,M1),
4155 NMid is round((Min+M1)/2),
4156 maximize_expr_6(Min,NMid,M1,X,Span,WF)
4157 ) ).
4158
4159 expects_waitflag('MINIMIZE_EXPR').
4160 expects_spaninfo('MINIMIZE_EXPR').
4161 :- public 'MINIMIZE_EXPR'/4.
4162 'MINIMIZE_EXPR'(int(X),PredRes,Span,WF) :-
4163 clpfd_eq(-X,MaxVar),
4164 'MAXIMIZE_EXPR'(int(MaxVar),PredRes,Span,WF).
4165
4166
4167 :- use_module(kernel_tools,[bexpr_variables/2]).
4168 % maximize is actually quite similar to CHOOSE; but it will choose maximum and use special algorithm for closures
4169 expects_waitflag('MAXIMIZE').
4170 expects_spaninfo('MAXIMIZE').
4171 :- public 'MAXIMIZE'/4.
4172 :- block 'MAXIMIZE'(-,?,?,?).
4173 'MAXIMIZE'([],_,Span,WF) :- !,
4174 add_wd_error_span('MAXIMIZE applied to empty set: ',[],Span,WF).
4175 'MAXIMIZE'(avl_set(A),H,_,_) :- !, avl_max(A,Max),kernel_objects:equal_object(H,Max).
4176 'MAXIMIZE'(closure(P,T,Body),FunValue,SpanInfo,WF) :- !,
4177 bexpr_variables(Body,ClosureWaitVars),
4178 debug_println(19,wait_maximize(P,ClosureWaitVars)),
4179 when(ground(ClosureWaitVars),maximize_closure(P,T,Body,FunValue,SpanInfo,WF)).
4180 'MAXIMIZE'([H|T],C,Span,WF) :- !,
4181 when(ground([H|T]),
4182 (convert_to_avl([H|T],AVL) -> 'MAXIMIZE'(AVL,C,Span,WF)
4183 ; add_wd_error_span('Cannot determine maximum element for MAXIMIZE: ',[H|T],Span,WF),
4184 kernel_objects:equal_object_wf(C,H,WF))
4185 ).
4186 'MAXIMIZE'(_,_,SpanInfo,_WF) :-
4187 add_error(external_functions,'MAXIMIZE requires set of values',SpanInfo),
4188 fail.
4189
4190 % move to optimizing solver
4191 % difference here is that entire constraint is re-set up every time; allowing Kodkod to be used
4192 maximize_closure(Parameters,ParameterTypes,ClosureBody,FunValue,_SpanInfo,WF) :-
4193 debug_println(maximizing(Parameters)),
4194 length(Parameters,Len), length(ParValues,Len),
4195 test_closure(Parameters,ParameterTypes,ClosureBody,ParValues),
4196 debug_println(19,found_initial_solution(ParValues)),
4197 !,
4198 maximize_closure2(Parameters,ParameterTypes,ClosureBody,ParValues,FunValue,WF).
4199 maximize_closure(_Parameters,_ParameterTypes,_ClosureBody,_FunValue,SpanInfo,_WF) :-
4200 add_error(external_functions,'MAXIMIZE: could not find solution for set comprehension',SpanInfo),
4201 fail.
4202
4203 maximize_closure2(Parameters,ParameterTypes,ClosureBody,PrevSol,FunValue,WF) :-
4204 Parameters=[PMax|_], ParameterTypes=[T1|_],
4205 PrevSol = [ PrevVal | _],
4206 debug_println(19,trying_to_improve_upon(PrevVal,PMax)),
4207 better_sol_pred(PMax,T1,PrevVal,Better),
4208 %translate:print_bexpr(Better),nl,
4209 bsyntaxtree:conjunct_predicates([Better,ClosureBody],NewBody),
4210 length(Parameters,Len), length(NewParValues,Len),
4211 test_closure(Parameters,ParameterTypes,NewBody,NewParValues),
4212 debug_println(19,found_better_solution(NewParValues)),
4213 !,
4214 maximize_closure2(Parameters,ParameterTypes,ClosureBody,NewParValues,FunValue,WF).
4215 maximize_closure2(_Parameters,_ParameterTypes,_ClosureBody,PrevSol,FunValue,WF) :-
4216 debug_println(19,cannot_improve),
4217 tools:convert_list_into_pairs(PrevSol,ParTuple),
4218 kernel_objects:equal_object_wf(ParTuple,FunValue,WF).
4219
4220 :- use_module(probsrc(solver_interface),[apply_kodkod_or_other_optimisations/4]).
4221 test_closure(Parameters,ParameterTypes,Body,ParValues) :-
4222 apply_kodkod_or_other_optimisations(Parameters,ParameterTypes,Body,Body2),
4223 custom_explicit_sets:b_test_closure(Parameters,ParameterTypes,Body2,ParValues,positive,no_wf_available). % positive instead of all_solutions
4224
4225 % generate predicate for better solution; % TO DO: support MINIMIZE by inverting args
4226 % TO DO: support more types: couples, booleans, ...
4227 better_sol_pred(PMax,integer,PrevVal,Better) :- !,
4228 Better = b(less(b(value(PrevVal),integer,[]),b(identifier(PMax),integer,[])),pred,[]).
4229 better_sol_pred(PMax,set(T1),PrevVal,Better) :- !,
4230 % WARNING: for sets we will only find one maximum, not all due to the cuts in maximize_closure(2) above
4231 Better = b(subset_strict(b(value(PrevVal),set(T1),[]),b(identifier(PMax),set(T1),[])),pred,[]).
4232 better_sol_pred(PMax,Type,_Val,_) :-
4233 add_error(external_functions,'MAXIMIZE requires first argument of set comprehension to be integer or set; cannot optimize: ',PMax:Type),fail.
4234
4235 % ----------------------------------
4236
4237 % EXTERNAL_FUNCTION_READ_XML == STRING --> seq(XML_ELement_Type);
4238 % with XML_ELement_Type == struct( recId: NATURAL1, pId:NATURAL, element:STRING, attributes: STRING +-> STRING, meta: STRING +-> STRING );
4239
4240 % XML_ELement_Type from LibraryXML.def:
4241 xml_element_type(record([ field(recId,integer), field(pId, integer), field(element,string),
4242 field(attributes, set(couple(string,string))),
4243 field(meta, set(couple(string,string))) ]) ).
4244
4245 performs_io('READ_XML').
4246 expects_spaninfo('READ_XML').
4247 :- public 'READ_XML'/3.
4248 :- block 'READ_XML'(-,?,?).
4249 'READ_XML'(string(File),Res,Span) :-
4250 read_xml(File,auto,Res,Span).
4251
4252 %expects_spaninfo('READ_XML'). both versions expect span info
4253 external_fun_type('READ_XML',[],[string,string,seq(XT)]) :- xml_element_type(XT).
4254 :- public 'READ_XML'/4.
4255 :- block 'READ_XML'(-,?,?,?),'READ_XML'(?,-,?,?).
4256 'READ_XML'(string(File),string(Encoding),Res,Span) :-
4257 read_xml(File,Encoding,Res,Span).
4258
4259
4260 :- use_module(tools, [read_string_from_file/3, detect_xml_encoding/3]).
4261 :- use_module(extrasrc(xml2b), [convert_xml_to_b/4]).
4262 :- use_module(preferences, [is_of_type/2]).
4263 :- block read_xml(-,?,?,?), read_xml(?,-,?,?).
4264 read_xml(File,EncodingPref,Res,Span) :-
4265 b_absolute_file_name(File,AFile,Span),
4266 (EncodingPref = 'auto',
4267 detect_xml_encoding(AFile,_Version,HeaderEncoding)
4268 -> (is_of_type(HeaderEncoding,text_encoding)
4269 -> Encoding=HeaderEncoding
4270 ; add_warning(read_xml,'Illegal encoding in XML header (must be "UTF-8", "UTF-16", "ISO-8859-1",...): ',HeaderEncoding),
4271 Encoding=auto
4272 )
4273 ; is_of_type(EncodingPref,text_encoding) -> Encoding = EncodingPref
4274 ; add_error(read_xml,'Illegal encoding preference (must be "auto", "UTF-8", "UTF-16", "ISO-8859-1",...): ',EncodingPref),
4275 Encoding=auto
4276 ),
4277 statistics(walltime,_),
4278 safe_call(read_string_from_file(AFile,Encoding,Codes),Span),
4279 statistics(walltime,[_,W1]), formatsilent('% Walltime ~w ms to read in ~w~n',[W1,AFile]),
4280 convert_xml_to_b(Codes,BDataSequence,File,Span),
4281 statistics(walltime,[_,W2]),
4282 formatsilent('% Walltime ~w ms to parse and convert XML in ~w~n',[W2,AFile]),
4283 kernel_objects:equal_object_optimized(Res,BDataSequence).
4284
4285
4286 external_fun_type('READ_XML_FROM_STRING',[],[string,seq(XT)]) :- xml_element_type(XT).
4287 expects_spaninfo('READ_XML_FROM_STRING').
4288 :- public 'READ_XML_FROM_STRING'/3.
4289 :- block 'READ_XML_FROM_STRING'(-,?,?).
4290 'READ_XML_FROM_STRING'(string(Contents),Res,Span) :-
4291 atom_codes(Contents,Codes),
4292 statistics(walltime,[W1,_]),
4293 convert_xml_to_b(Codes,BDataSequence,'string',Span),
4294 statistics(walltime,[W2,_]), W is W2-W1,
4295 formatsilent('% Walltime ~w ms to parse and convert XML~n',[W]),
4296 kernel_objects:equal_object_optimized(Res,BDataSequence).
4297
4298 :- use_module(extrasrc(json_parser),[json_parse_file/3]).
4299 :- use_module(extrasrc(xml2b), [convert_json_to_b/3]).
4300 % reads in JSON file producing the same format as READ_XML
4301 performs_io('READ_JSON').
4302 external_fun_type('READ_JSON',[],[string,seq(XT)]) :- xml_element_type(XT).
4303 expects_spaninfo('READ_JSON').
4304 :- public 'READ_JSON'/3.
4305 :- block 'READ_JSON'(-,?,?).
4306 'READ_JSON'(string(File),Res,Span) :-
4307 read_json(File,Res,Span).
4308 :- block read_json(-,?,?).
4309 read_json(File,Res,Span) :-
4310 b_absolute_file_name(File,AFile,Span),
4311 statistics(walltime,_),
4312 safe_call(json_parse_file(AFile,[strings_as_atoms(true),position_infos(true)],JSONList),Span),
4313 statistics(walltime,[_,W1]), formatsilent('% Walltime ~w ms to read and parse ~w~n',[W1,AFile]),
4314 convert_json_to_b(JSONList,BDataSequence,Span),
4315 statistics(walltime,[_,W2]),
4316 formatsilent('% Walltime ~w ms to convert JSON from ~w~n',[W2,AFile]),
4317 kernel_objects:equal_object_optimized(Res,BDataSequence).
4318
4319 expects_spaninfo('WRITE_XML').
4320 external_fun_type('WRITE_XML',[],[seq(XT),string]) :- xml_element_type(XT).
4321 :- public 'WRITE_XML'/4.
4322 :- block 'WRITE_XML'(-,?,?,?),'WRITE_XML'(?,-,?,?).
4323 'WRITE_XML'(Records,string(File),Res,Span) :- write_xml2(Records,File,Res,Span).
4324 :- block write_xml2(?,-,?,?).
4325 write_xml2(Records,File,Res,Span) :-
4326 b_absolute_file_name(File,AFile,Span),
4327 statistics(walltime,_),
4328 'WRITE_XML_TO_STRING'(Records,String,Span),
4329 String = string(S),
4330 when(nonvar(S),
4331 (statistics(walltime,[_,W1]), formatsilent('% Walltime ~w ms to convert XML for ~w~n',[W1,AFile]),
4332 open(AFile,write,Stream,[encoding(utf8)]),
4333 write(Stream,S),nl(Stream),
4334 close(Stream),
4335 statistics(walltime,[_,W2]), formatsilent('% Walltime ~w ms to write XML to file ~w~n',[W2,AFile]),
4336 Res = pred_true
4337 )).
4338
4339
4340 %sequence of records of type:
4341 % rec(attributes:{("version"|->"03.04")},
4342 % element:"Data",
4343 % meta:{("xmlLineNumber"|->"2")},
4344 % pId:0,
4345 % recId:1),
4346 :- use_module(probsrc(xml_prob),[xml_parse/4, xml_pp/1]).
4347 expects_spaninfo('WRITE_XML_TO_STRING').
4348 :- public 'WRITE_XML_TO_STRING'/3.
4349 :- block 'WRITE_XML_TO_STRING'(-,?,?).
4350 'WRITE_XML_TO_STRING'(Records,Res,Span) :-
4351 custom_explicit_sets:expand_custom_set_to_list(Records,ESet,Done,'WRITE_XML_TO_STRING'),
4352 ground_value_check(ESet,Gr),
4353 when((nonvar(Done),nonvar(Gr)),
4354 ( % print(expanded(ESet)),nl,
4355 gen_prolog_xml_term(ESet,Prolog,Span),
4356 %print(prolog(Prolog)),nl,
4357 xml_parse(Codes,Prolog,[],Span),
4358 (debug:debug_mode(on) -> xml_pp(Prolog) ; true),
4359 atom_codes(S,Codes),
4360 Res = string(S))).
4361
4362 gen_prolog_xml_term(List,xml( [version="1.0", encoding="ASCII"], ContentList),Span) :-
4363 InitialLineNr = 2, % first line is xml-header !?
4364 gen_prolog_xml_dcg(InitialLineNr,_,0,[],ContentList,Span,List,[]).
4365
4366 gen_prolog_xml_dcg(LastLineNr,FinalLineNr,CurLevel, Parents, ResContentList,Span) -->
4367 [(int(Index),rec(Fields))],
4368 { %print(treat(Index,Fields)),nl,
4369 get_parentId(Fields,CurLevel,Span)}, % The element should be added to the current content list
4370 !,
4371 {get_element(Fields,Element,Span),
4372 get_attributes(Fields,Attributes,Span),
4373 get_line(Fields,LineNr,Span),
4374 gen_element(LastLineNr,LineNr,Element, Attributes, InnerContentList, ResContentList, TailContentList)
4375 },
4376 gen_prolog_xml_dcg(LineNr,LineNr2,Index,[CurLevel|Parents],InnerContentList,Span),
4377 gen_prolog_xml_dcg(LineNr2,FinalLineNr,CurLevel, Parents, TailContentList,Span).
4378 gen_prolog_xml_dcg(L,L,_,_,[],_Span) --> [].
4379
4380 gen_element(LastLineNr,NewLineNr,'CText',['='(text,Codes)],[], [PCDATA|Tail],Tail) :-
4381 insert_newlines(LastLineNr,NewLineNr,Codes,NLCodes),
4382 !,
4383 PCDATA=pcdata(NLCodes).
4384 gen_element(LastLineNr,NewLineNr,Element, Attributes, InnerContentList, [pcdata(NL),XELEMENT|Tail],Tail) :-
4385 LastLineNr < NewLineNr,
4386 insert_newlines(LastLineNr,NewLineNr,[],NL),
4387 !,
4388 XELEMENT = element( Element, Attributes, InnerContentList).
4389 gen_element(_,_,Element, Attributes, InnerContentList, [XELEMENT|Tail],Tail) :-
4390 XELEMENT = element( Element, Attributes, InnerContentList).
4391
4392 insert_newlines(LastLineNr,NewLineNr,C,R) :- NewLineNr =< LastLineNr,!,R=C.
4393 % TO DO: maybe we have to use 13 on Windows ??
4394 insert_newlines(LastLineNr,NewLineNr,C,[10|Res]) :- L1 is LastLineNr+1, insert_newlines(L1,NewLineNr,C,Res).
4395
4396 get_parentId(Fields,Nr,Span) :-
4397 (member(field(pId,int(ParentID)),Fields) -> Nr=ParentID
4398 ; add_error('WRITE_XML_TO_STRING','The record has no pId field: ',Fields,Span),
4399 Nr = 0).
4400 get_element(Fields,Atom,Span) :-
4401 (member(field(element,string(Atom)),Fields) -> true
4402 ; add_error('WRITE_XML_TO_STRING','The record has no element field: ',Fields,Span),
4403 Atom = '??').
4404
4405 get_attributes(Fields,Attrs,Span) :-
4406 (member(field(attributes,Set),Fields)
4407 -> custom_explicit_sets:expand_custom_set_to_list(Set,ESet,_Done,'get_attributes'),
4408 (maplist(get_xml_attr,ESet,Attrs) -> true
4409 ; add_error('WRITE_XML_TO_STRING','Illegal attributes field: ',ESet,Span),
4410 Attrs = []
4411 )
4412 ; add_error('WRITE_XML_TO_STRING','The record has no attributes field: ',Fields,Span),
4413 Attrs = []).
4414 get_line(Fields,LineNr,Span) :-
4415 (member(field(meta,Set),Fields)
4416 -> custom_explicit_sets:expand_custom_set_to_list(Set,ESet,_Done,'get_line'),
4417 (member((string(xmlLineNumber),string(LineNrS)),ESet)
4418 -> atom_codes(LineNrS,CC), number_codes(LineNr,CC)
4419 ; add_error('WRITE_XML_TO_STRING','The meta field has no xmlLineNumber entry: ',ESet,Span),
4420 LineNr = -1
4421 )
4422 ; add_error('WRITE_XML_TO_STRING','The record has no meta field: ',Fields,Span),
4423 LineNr = -1).
4424
4425 get_xml_attr((string(Attr),string(Val)),'='(Attr,ValCodes)) :- atom_codes(Val,ValCodes).
4426
4427
4428 % ----------------------------------
4429 % A flexible CVS Reader that always uses the same type
4430 % rec([field(attributes,BAttributes),field(lineNr,LineNr)])
4431
4432 % EXTERNAL_FUNCTION_READ_CSV_STRINGS == STRING --> seq(CSV_ELement_Type);
4433 % with CSV_ELement_Type == STRING +-> STRING ;
4434
4435 expects_spaninfo('READ_CSV_STRINGS').
4436 :- public 'READ_CSV_STRINGS'/3.
4437 :- block 'READ_CSV_STRINGS'(-,?,?).
4438 'READ_CSV_STRINGS'(string(File),Res,Span) :- read_csv_strings(File,Res,Span).
4439
4440 read_csv_strings(File,ResAVL,Span) :-
4441 b_absolute_file_name(File,AFile,Span),
4442 open_utf8_file_for_reading(AFile,Stream,Span),
4443 statistics(walltime,_),
4444 read_line(Stream,Line1),
4445 (Line1 = end_of_file -> ResAVL = []
4446 ; split_csv_line([],HeadersCodes,Span,Line1,[]),
4447 maplist(process_header,HeadersCodes,Headers),
4448 formatsilent('CSV Line Headers = ~w for ~w~n',[Headers,AFile]),
4449 safe_call(read_csv_strings_lines(Stream,1,Span,Headers,Res),Span),
4450 statistics(walltime,[_,W1]), formatsilent('% Walltime ~w ms to read in ~w~n',[W1,AFile]),
4451 kernel_objects:equal_object_optimized(Res,ResAVL),
4452 statistics(walltime,[_,W2]), formatsilent('% Walltime ~w ms to normalise in ~w~n',[W2,AFile])
4453 ),
4454 close(Stream). % TO DO: call_cleanup
4455
4456 process_header(HeaderC,HeaderAtom) :- safe_atom_codes(HeaderAtom,HeaderC).
4457
4458 read_csv_strings_lines(Stream,PrevLineNr,Span,Headers,Res) :-
4459 read_line(Stream,Line),
4460 (Line = end_of_file -> Res = []
4461 ; LineNr is PrevLineNr+1,
4462 split_csv_line([],AtomsC,Span,Line,[]),
4463 Res = [(int(PrevLineNr),Attrs)|ResT],
4464 construct_attributes(AtomsC,Headers,Attrs,Span,LineNr),
4465 read_csv_strings_lines(Stream,LineNr,Span,Headers,ResT)
4466 ).
4467
4468 construct_attributes([],_,[],_,_).
4469 construct_attributes([ [] | T],[ _|HT],Res,Span,LineNr) :- !,
4470 construct_attributes(T,HT,Res,Span,LineNr).
4471 construct_attributes([ AtomC | _T], [], Res,Span,LineNr) :- !,
4472 safe_atom_codes(A,AtomC),
4473 ajoin(['Additional field on line ',LineNr,' : '],Msg),
4474 add_error('READ_CSV_STRINGS',Msg,A,Span),
4475 Res=[].
4476 construct_attributes([ AtomC | T], [ Header | HT], [ (string(Header),string(A)) | ResT],Span,LineNr) :-
4477 safe_atom_codes(A,AtomC),
4478 construct_attributes(T,HT,ResT,Span,LineNr).
4479
4480 % ----------------------------------
4481 % A CSV Reader that uses the B types to adapt how it reads in values
4482
4483 expects_spaninfo('READ_CSV').
4484 expects_type('READ_CSV').
4485
4486 :- public 'READ_CSV'/6.
4487 :- block 'READ_CSV'(-,?,?,?,?,?).
4488 'READ_CSV'(string(File),BoolSkipLine1,AllowExtraValues,Res,Type,Span) :-
4489 read_csv(File,BoolSkipLine1,AllowExtraValues,pred_false,Res,Type,Span).
4490
4491 external_fun_type('READ_CSV',[T],[string,T]).
4492 :- public 'READ_CSV'/4.
4493 :- block 'READ_CSV'(-,?,?,?).
4494 'READ_CSV'(string(File),Res,Type,Span) :-
4495 read_csv(File,pred_false,pred_false,pred_false,Res,Type,Span).
4496
4497 expects_spaninfo('READ_CSV_SEQUENCE').
4498 expects_type('READ_CSV_SEQUENCE').
4499 :- public 'READ_CSV_SEQUENCE'/6.
4500 :- block 'READ_CSV_SEQUENCE'(-,?,?,?,?,?).
4501 'READ_CSV_SEQUENCE'(string(File),BoolSkipLine1,AllowExtraValues,Res,Type,Span) :-
4502 read_csv(File,BoolSkipLine1,AllowExtraValues,pred_true,Res,Type,Span).
4503
4504 :- use_module(bsyntaxtree,[get_set_type/2]).
4505 :- block read_csv(-,?,?,?,?,?,?).
4506 read_csv(File,BoolSkipLine1,AllowExtraValues,CreateSequence,Res,InType,Span) :-
4507 (CreateSequence=pred_true
4508 -> (get_set_type(InType,couple(integer,T)) -> Type=set(T), SeqIndex=1
4509 ; add_error('READ_CSV_SEQUENCE','Expecting sequence as return type:',InType),
4510 Type=InType, SeqIndex=none
4511 )
4512 ; SeqIndex=none,Type=InType),
4513 get_column_types(Type,Types,Skel,Vars,Span),
4514 b_absolute_file_name(File,AFile,Span),
4515 open_utf8_file_for_reading(AFile,Stream,Span),
4516 (debug:debug_mode(off) -> true
4517 ; formatsilent('~nReading CSV file ~w with Types = ~w and Skel = ~w for Vars = ~w~n~n',[AFile,Types,Skel,Vars])),
4518 (read_csv_lines(1,SeqIndex,BoolSkipLine1,AllowExtraValues,Stream,Types,Skel,Vars,Res,Span) -> true
4519 ; add_error('READ_CSV','Reading CSV File failed: ',AFile)),
4520 close(Stream). % TO DO: call_cleanup
4521
4522 read_csv_lines(Nr,SeqIndex,BoolSkipLine1,AllowExtraValues,Stream,Types,Skel,Vars,Res,Span) :- %print(line(Nr,Types)),nl,
4523 read_line(Stream,Line),
4524 debug:debug_println(9,read_line(Nr,Line)),
4525 (Line = end_of_file -> Res = []
4526 ; split_csv_line([],AtomsC,Span,Line,[]),
4527 %print(atoms(Nr,Atoms)),nl,
4528 %maplist(convert_atom_codes(Span),Types,Atoms,Tuple), % TO DO: check same length
4529 (Nr=1,BoolSkipLine1=pred_true
4530 -> maplist(codes_to_atom,AtomsC,Atoms), format('Skipping line 1: ~w~n',[Atoms]),
4531 Res=ResT
4532 ; Line=[] -> format('Skipping empty line ~w~n',[Nr]), Res=ResT
4533 ; l_convert_atom_codes(Types,AtomsC,Tuple,Span,Nr,AllowExtraValues),
4534 copy_term((Vars,Skel),(Tuple,BValue)),
4535 (number(SeqIndex) -> S1 is SeqIndex+1, Res = [(int(SeqIndex),BValue)|ResT]
4536 ; S1 = SeqIndex, Res = [BValue|ResT]
4537 )
4538 ),
4539 N1 is Nr+1,
4540 read_csv_lines(N1,S1,BoolSkipLine1,AllowExtraValues,Stream,Types,Skel,Vars,ResT,Span)).
4541
4542 codes_to_atom(C,A) :- atom_codes(A,C).
4543
4544 l_convert_atom_codes([],[],Vals,_Span,_LineNr,_) :- !, Vals=[].
4545 l_convert_atom_codes([Type|TT],[AtomC|TC],[Val|VT],Span,LineNr,AllowExtraValues) :- !,
4546 convert_atom_codes(Span,LineNr,Type,AtomC,Val),
4547 l_convert_atom_codes(TT,TC,VT,Span,LineNr,AllowExtraValues).
4548 l_convert_atom_codes([Type|TT],[],_,Span,LineNr,_) :- !,
4549 ajoin(['Missing value(s) on CSV line ',LineNr,' for types: '],Msg),
4550 add_error('READ_CSV',Msg,[Type|TT],Span),fail.
4551 l_convert_atom_codes([],[AtomC|AT],Vals,Span,LineNr,AllowExtraValues) :- !,
4552 (AllowExtraValues=pred_true -> true
4553 ; safe_atom_codes(Atom,AtomC),
4554 ajoin(['Extra value(s) on CSV line ',LineNr,' : ',Atom,' Rest = '],Msg),
4555 add_error('READ_CSV',Msg,AT,Span)
4556 ), Vals=[].
4557
4558 convert_atom_codes(Span,LineNr,T,AtomC,Val) :-
4559 (convert_atom2(T,AtomC,Val,Span,LineNr) -> true ;
4560 atom_codes(Atom,AtomC),
4561 ajoin(['Could not convert value to type ',T,' on CSV line ',LineNr,': '],Msg),
4562 add_error('READ_CSV',Msg,Atom,Span),
4563 Val = term('READ_CSV_ERROR')).
4564 :- use_module(tools,[safe_number_codes/2, safe_atom_codes/2]).
4565 convert_atom2(string,C,string(A),_,_) :- safe_atom_codes(A,C).
4566 convert_atom2(integer,C,int(Nr),_Span,LineNr) :-
4567 (C=[] -> (debug:debug_mode(off) -> true ; format('Translating empty string to -1 on line ~w~n',[LineNr])),
4568 % add_warning('READ_CSV','Translating empty string to -1 on line: ',LineNr,Span),
4569 Nr is -1
4570 ; safe_number_codes(Nr,C)).
4571 convert_atom2(global(G),C,FD,Span,LineNr) :- safe_atom_codes(A,C),convert_to_enum(G,A,FD,Span,LineNr).
4572 convert_atom2(boolean,C,Bool,Span,LineNr) :- safe_atom_codes(A,C),
4573 (convert_to_bool(A,Bool) -> true
4574 ; ajoin(['Could not convert value to BOOL on line ',LineNr,'; assuming FALSE: '],Msg),
4575 add_warning('READ_CSV',Msg,A,Span),
4576 Bool=pred_false).
4577 % TO DO: support set(_), seq(_)
4578
4579 convert_to_bool('0',pred_false).
4580 convert_to_bool('1',pred_true).
4581 convert_to_bool('FALSE',pred_false).
4582 convert_to_bool('TRUE',pred_true).
4583 convert_to_bool('false',pred_false).
4584 convert_to_bool('true',pred_true).
4585
4586 convert_to_enum(G,A,FD,Span,LineNr) :- string_to_enum2(A,FD,_,Span),
4587 (FD=fd(_,G) -> true ; add_error('READ_CSV','Enumerated element of incorrect type: ',A:expected(G):line(LineNr),Span)).
4588
4589 % split a CSV line into individual AtomCode lists
4590 split_csv_line([],T,Span) --> " ", !, split_csv_line([],T,Span).
4591 split_csv_line(Acc,[AtomC|T],Span) --> sep, !,
4592 {reverse(Acc,AtomC)}, split_csv_line([],T,Span).
4593 split_csv_line([],[String|T],Span) --> [34], % "
4594 scan_to_end_of_string([],String,Span),
4595 (sep -> split_csv_line([],T,Span)
4596 ; [XX] -> {add_error('READ_CSV','String not followed by separator: ',String,Span)}, split_csv_line([XX],T,Span)
4597 ; {T=[]}).
4598 split_csv_line(Acc,Atoms,Span) --> [X], !, split_csv_line([X|Acc],Atoms,Span).
4599 split_csv_line(Acc,[AtomC],_Span) --> !, % end of line
4600 {reverse(Acc,AtomC)}.
4601
4602 sep --> " ",!, sep.
4603 sep --> ("," ; ";" ; " ,").
4604
4605 scan_to_end_of_string(Acc,AtomC,_) --> [34],!,{reverse(Acc,AtomC)}.
4606 scan_to_end_of_string(Acc,String,Span) --> [X],!, scan_to_end_of_string([X|Acc],String,Span).
4607 scan_to_end_of_string(Acc,String,Span) -->
4608 {reverse(Acc,RAcc),atom_codes(String,RAcc),add_error('READ_CSV','String not terminated: ',String,Span)}.
4609
4610 % get the list of column types along with Value skeleton with variables in the places where CSV values should be inserted
4611 get_column_types(set(X),Types,Skel,Vars,_) :- !,flatten_pairs(X,Types,[]), %print(types(Types)),nl,
4612 flatten_pairs_value_skeleton(X,Skel,Vars,[]). % print(skel(Skel,Vars)),nl.
4613 get_column_types(seq(X),Types,Skel,Vars,Span) :- !,
4614 get_column_types(set(couple(integer,X)),Types,Skel,Vars,Span).
4615 get_column_types(Type,_,_,_,Span) :- add_error('READ_CSV','Invalid return type (must be relation): ',Type,Span),fail.
4616
4617 % flatten couple pairs and generate skeleton term
4618 flatten_pairs(couple(A,B)) --> !,flatten_pairs(A), flatten_pairs(B).
4619 flatten_pairs(record(Fields)) --> !, flatten_fields(Fields).
4620 flatten_pairs(X) --> [X].
4621
4622 /* note: currently record fields have to be alphabetically in the same order as in CSV file: the fields are sorted by ProB's kernel ! : TO DO: try and recover the original order of the fields */
4623 flatten_fields([]) --> [].
4624 flatten_fields([field(_Name,Type)|T]) --> [Type], % no nesting allowed; this has to be a basic type for CSV reading to work
4625 flatten_fields(T).
4626
4627 % generate a value skeleton
4628 flatten_pairs_value_skeleton(couple(A,B),(CA,CB)) --> !,
4629 flatten_pairs_value_skeleton(A,CA), flatten_pairs_value_skeleton(B,CB).
4630 flatten_pairs_value_skeleton(record(Fields),rec(SF)) --> !, flatten_field_skel(Fields,SF).
4631 flatten_pairs_value_skeleton(_X,Var) --> [Var].
4632
4633 flatten_field_skel([],[]) --> [].
4634 flatten_field_skel([field(Name,_Type)|T],[field(Name,Var)|ST]) --> [Var],
4635 flatten_field_skel(T,ST).
4636
4637
4638 % ----------------------------------
4639 % Writing a matrix to a .pgm graphics file
4640 % The header of such a file looks like:
4641 % P5
4642 % 752 864 (width height)
4643 % 255 (maximal pixel value)
4644 % after that we have bytes of grayscale values
4645 % https://en.wikipedia.org/wiki/Netpbm#File_formats
4646
4647 % TODO: try and support colors (.ppm files)
4648 % improve performance; possibly avoiding to expand avl_sets
4649
4650 :- use_module(probsrc(tools_io),[read_byte_line/2, read_byte_word/2, put_bytes/2]).
4651
4652 :- public 'READ_PGM_IMAGE_FILE'/4.
4653 external_fun_type('READ_PGM_IMAGE_FILE',[],[string,seq(seq(integer))]).
4654 expects_waitflag('READ_PGM_IMAGE_FILE').
4655 expects_spaninfo('READ_PGM_IMAGE_FILE').
4656 :- block 'READ_PGM_IMAGE_FILE'(-,?,?,?).
4657 'READ_PGM_IMAGE_FILE'(string(FileName),Matrix,Span,WF) :-
4658 when(nonvar(FileName),
4659 (statistics(walltime,[_,_]),
4660 b_absolute_file_name(FileName,AFile,Span),
4661 open(AFile,read,Stream,[type(binary)]),
4662 call_cleanup(read_pgm_file(Stream,MatrixList,Span,WF), close(Stream)),
4663 statistics(walltime,[_,W2]),
4664 formatsilent('% Walltime ~w ms to read matrix from PGM file ~w~n',[W2,AFile]),
4665 kernel_objects:equal_object_optimized(Matrix,MatrixList)
4666 )).
4667
4668 read_pgm_file(Stream,Matrix,Span,_WF) :-
4669 read_byte_line(Stream,FileType),
4670 (FileType = "P5"
4671 -> read_byte_number(Stream,Width,Span),
4672 read_byte_number(Stream,Height,Span),
4673 read_byte_number(Stream,MaxPix,Span),
4674 formatsilent('% Detected PGM file width=~w, height=~w, max=~w~n',[Width,Height,MaxPix]),
4675 read_pgm_matrix(1,Height,Width,MaxPix,Stream,Matrix,Span)
4676 ; atom_codes(FT,FileType),
4677 add_error('READ_PGM_IMAGE_FILE','Can only support P5 grayscale type:',FT,Span),fail
4678 ).
4679
4680 % read pgm bytes and covert to B sequence of sequence of numbers
4681 read_pgm_matrix(Nr,Height,_,_,Stream,Res,Span) :- Nr > Height, !,
4682 get_byte(Stream,Code),
4683 (Code = -1 -> true
4684 ; add_warning('READ_PGM_IMAGE_FILE','Bytes ignored after reading rows=',Height,Span)),
4685 Res=[].
4686 read_pgm_matrix(RowNr,Height,Width,MaxPix,Stream,[(int(RowNr),Row1)|ResT],Span) :-
4687 read_pgm_row(1,Width,MaxPix,Stream,Row1,Span),
4688 N1 is RowNr+1,
4689 read_pgm_matrix(N1,Height,Width,MaxPix,Stream,ResT,Span).
4690
4691 read_pgm_row(Nr,Width,_,_Stream,Res,_Span) :- Nr>Width, !, Res=[].
4692 read_pgm_row(ColNr,Width,MaxPix,Stream,[(int(ColNr),int(Code))|ResT],Span) :-
4693 (get_byte(Stream,Code), Code >= 0
4694 -> (Code =< MaxPix -> true
4695 ; add_warning('READ_PGM_IMAGE_FILE','Grayscale pixel value exceeds maximum: ',Code,Span)
4696 )
4697 ; add_error('READ_PGM_IMAGE_FILE','Unexpected EOF at column:',ColNr),
4698 fail
4699 ),
4700 N1 is ColNr+1,
4701 read_pgm_row(N1,Width,MaxPix,Stream,ResT,Span).
4702
4703
4704 % read a word (until ws or eof) and convert it to a number
4705 read_byte_number(Stream,Nr,Span) :- read_byte_word(Stream,Codes),
4706 (safe_number_codes(Nr,Codes) -> true
4707 ; add_error('READ_PGM_IMAGE_FILE','Expected number:',Codes,Span)
4708 ).
4709
4710 :- public 'WRITE_PGM_IMAGE_FILE'/5.
4711 external_fun_type('WRITE_PGM_IMAGE_FILE',[],[string,seq(seq(integer),boolean)]).
4712 expects_waitflag('WRITE_PGM_IMAGE_FILE').
4713 expects_spaninfo('WRITE_PGM_IMAGE_FILE').
4714 :- block 'WRITE_PGM_IMAGE_FILE'(-,?,?,?,?), 'WRITE_PGM_IMAGE_FILE'(?,-,?,?,?).
4715 'WRITE_PGM_IMAGE_FILE'(string(FileName),Matrix,Res,Span,WF) :-
4716 custom_explicit_sets:expand_custom_set_to_list(Matrix,ESet,Done,'WRITE_PGM_IMAGE_FILE'),
4717 ground_value_check(ESet,Gr),
4718 when((nonvar(FileName),nonvar(Done),nonvar(Gr)),
4719 (statistics(walltime,[_,_]),
4720 b_absolute_file_name(FileName,AFile,Span),
4721 open(AFile,write,Stream,[type(binary)]),
4722 call_cleanup(put_pgm_file(Stream,ESet,Width,Height,WF),
4723 close(Stream)),
4724 statistics(walltime,[_,W2]),
4725 formatsilent('% Walltime ~w ms to write matrix to PGM file (width=~w, height=~w) ~w~n',[W2,Width,Height,AFile]),
4726 Res = pred_true
4727 )).
4728
4729 put_pgm_file(Stream,ESet,Width,Height,WF) :-
4730 ESet = [(int(_),Row)|_],
4731 bsets_clp:size_of_sequence(Row,int(Width),WF),
4732 put_bytes(Stream,"P5\n"),
4733 number_codes(Width,WC), put_bytes(Stream,WC),
4734 put_bytes(Stream," "),
4735 bsets_clp:size_of_sequence(ESet,int(Height),WF),
4736 number_codes(Height,HC), put_bytes(Stream,HC),
4737 put_bytes(Stream,"\n"),
4738 put_bytes(Stream,"255\n"),
4739 sort(ESet,SESet),
4740 put_pgm_matrix(Stream,Width,SESet).
4741
4742 % put a pgm grayscale matrix as bytes into a stream
4743 put_pgm_matrix(_,_,[]).
4744 put_pgm_matrix(Stream,Width,[(int(_),RowVector)|T]) :-
4745 custom_explicit_sets:expand_custom_set_to_list(RowVector,ESet,_,'WRITE_PGM_IMAGE_FILE'),
4746 sort(ESet,SESet),
4747 put_pgm_row(Stream,Width,SESet),
4748 put_pgm_matrix(Stream,Width,T).
4749
4750 put_zeros(_,X) :- X<1, !.
4751 put_zeros(Stream,X) :- put_byte(Stream,0), X1 is X-1, put_zeros(Stream,X1).
4752
4753 put_pgm_row(Stream,W,[]) :-
4754 (W=0 -> true
4755 ; add_error('WRITE_PGM_IMAGE_FILE','Illegal PGM width in row: ',W),
4756 put_zeros(Stream,W)
4757 ).
4758 put_pgm_row(Stream,W,[(_,int(Pixel))|T]) :-
4759 W1 is W-1,
4760 ( W<1 -> add_error('WRITE_PGM_IMAGE_FILE','Additional PGM pixel in row: ',Pixel)
4761 ; Pixel >=0, Pixel =< 255
4762 -> put_byte(Stream,Pixel),
4763 put_pgm_row(Stream,W1,T)
4764 ; add_error('WRITE_PGM_IMAGE_FILE','Illegal PGM pixel (must be 0..255): ',Pixel),
4765 put_byte(Stream,0),
4766 put_pgm_row(Stream,W1,T)
4767 ).
4768
4769 % -----------------
4770
4771 :- use_module(extrasrc(mcts_game_play), [mcts_auto_play/4, mcts_auto_play_available/0]).
4772 external_subst_enabling_condition('MCTS_AUTO_PLAY',_,Truth) :- create_texpr(truth,pred,[],Truth).
4773 :- public 'MCTS_AUTO_PLAY'/3.
4774 :- block 'MCTS_AUTO_PLAY'(-,?,?).
4775 'MCTS_AUTO_PLAY'(_,_Env,OutEnvModifications) :- % TO DO: pass simulation runs and time_out as parameter
4776 mcts_auto_play_available,!,
4777 get_current_state_id(CurID),
4778 mcts_auto_play(CurID,_ActionAsTerm,_TransID,State2),
4779 state_space:get_variables_state_for_id(State2,OutEnvModifications).
4780 'MCTS_AUTO_PLAY'(_,_,[]).
4781
4782 % EXTERNAL_SUBSTITUTION_MCTS_AUTO_PLAY == BOOL; MCTS_AUTO_PLAY(x) == skip;
4783
4784
4785
4786