1 % (c) 2009-2026 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 :- module(kernel_tools,[
5 ground_value_check/2,
6 ground_value_opt_check/3, % version with an additional flag to discard check if no longer needed
7 bexpr_variables/2,
8 ground_bexpr/1,
9 ground_bexpr_check/2,
10 value_variables/2, value_variables/3,
11 ground_value/1,
12 ground_value_or_field/1,
13 ground_state_check/2, ground_state/1,
14 ground_typedvals_check/2,
15 %discard_ground_value_check/1,
16 %map_over_bvalue/3,
17 filter_cannot_match/4, get_template_for_filter_cannot_match/2,
18 cannot_match/2, can_match/2,
19 cannot_match_aggressive/2,
20 quick_same_value/2,
21 add_call_residue_error/3,
22 check_residue_for_call/2, check_residue_for_call_wf/5,
23 clpfd_residue_ok/1
24 ]).
25
26
27 :- use_module(module_information,[module_info/2]).
28 :- module_info(group,kernel).
29 :- module_info(description,'This module provides utilities for term variables for B expressions and values.').
30
31 :- use_module(self_check).
32 :- use_module(error_manager).
33 :- use_module(bsyntaxtree,[safe_syntaxelement_det/5]).
34
35 % use when ground value check no longer need to instantiate result variable:
36 % seems to have performance issues
37 %discard_ground_value_check(X) :- nonvar(X),!,
38 % (X==ground_value -> true ; print(illegal_ground_value_check(X)),nl).
39 %discard_ground_value_check(ground_value).
40
41 :- assert_must_succeed((kernel_tools:ground_value_check(int(X),V), var(V), X=1, nonvar(V))).
42 :- assert_must_succeed((kernel_tools:ground_value_check(string(X),V), var(V), X=a, nonvar(V))).
43 :- assert_must_succeed((kernel_tools:ground_value_check([int(1),int(X)],V), var(V), X=1, nonvar(V))).
44 % instantiate second argument to atomic-nonvar term if first argument ground B value
45 :- block ground_value_check(-,?).
46 ground_value_check([],R) :- !, R=ground_value.
47 ground_value_check(pred_true,R) :- !, R=ground_value.
48 ground_value_check(pred_false,R) :- !, R=ground_value.
49 ground_value_check(int(X),R) :- !, ground_atom(X,R).
50 ground_value_check(global_set(X),R) :- !, ground_atom(X,R).
51 ground_value_check(fd(X,_T),R) :- !,ground_atom(X,R). % avoid waking up co-routines with R=X.
52 ?ground_value_check(string(X),R) :- !, ground_atom(X,R).
53 ground_value_check((A,B),R) :- !, ground_value_check(A,GA), ground_value_check_aux(GA,B,R).
54 ?ground_value_check([H|T],R) :- !, ground_value_check(H,GA), ground_value_check_aux(GA,T,R).
55 ground_value_check(avl_set(A),R) :- !, % assume avl_set grounded
56 check_avl_set(A),
57 R = ground_value.
58 ground_value_check(rec(F),R) :- !, ground_fields(F,R).
59 ground_value_check(freeval(ID,Case,Val),R) :- !,
60 ? ground_freeval_check(ID,Case,Val,R).
61 ground_value_check(closure(_P,_T,B),R) :- !,
62 bexpr_variables(B,Vars),
63 ground_value_check(Vars,R).
64 %when(ground(Vars),R=ground_value).
65 ?ground_value_check(term(X),R) :- !, ground_term(X,R).
66 ground_value_check(Val,R) :- %print(uncov(Val,R)),nl,trace,
67 (atomic(Val) -> R=ground_value ; when(ground(Val),R=ground_value)).
68
69 :- block ground_term(-,?).
70 ?ground_term(floating(F),R) :- !, ground_atom(F,R).
71 ?ground_term(Term,R) :- when(ground(Term),R=ground_value).
72
73 :- block ground_atom(-,?).
74 ground_atom(_,ground_value). %we could do a check ground_atom(X,R) :- (nonvar(R) -> nl,print(illegal_grval(X,R)),nl,nl ; R=X).
75 % we use this co-routine rather than direct unification to avoid unnecessarily waking up pending nonvar/ground checks
76 % indeed: if we unify X with another variable Y, this will wake up all when(nonvar(X) checks
77 % in test 1101 for prob_examples/examples/B/Systerel/C578.EML.014/612_001.mch this caused performance problems
78 % we woke up another pending co-routine with the same waitflag priority, it had a check when((nonvar(X);ground(WF1),
79 % WF1 was already ground: this meant we started evaluating another Prolog kernel call before finishing the current one
80
81 :- block ground_value_check_aux(-,?,?).
82 % :- block ground_value_check_aux(-,?,-). % this slows down test 884, 292, 293, 1456, 1737
83 %ground_value_check_aux(_,_,R) :- nonvar(R),!. % groundness check no longer needed
84 ?ground_value_check_aux(_,V,R) :- ground_value_check(V,R).
85
86 :- block ground_fields(-,?).
87 ground_fields([],R) :- !, R=ground_value.
88 ground_fields([field(F,V)|T],R) :- ground_fields_aux(F,V,T,R).
89
90 :- block ground_fields_aux(-,?,?,?).
91 ground_fields_aux(_,V,T,R) :- ground_fields(T,GrT), ground_value_check_aux(GrT,V,R).
92
93 :- block ground_freeval_check(-,?,?,?), ground_freeval_check(?,-,?,?).
94 ground_freeval_check(_ID,_,Val,R) :-
95 % Note: for polymorphic types the ID can contain type variables, but should be ground
96 ? ground_value_check(Val,R).
97 % -------------------------------
98
99 :- block ground_state_check(-,?).
100 ground_state_check([],R) :- !, R=ground_value.
101 ground_state_check([bind(F,Val)|T],R) :- !, ground_state_check_aux(F,Val,T,R).
102 ground_state_check(BL,R) :- add_internal_error('Illegal bind list:',ground_state_check(BL,R)).
103
104 :- block ground_state_check_aux(-,?,?,?).
105 ground_state_check_aux(_,Val,T,R) :- ground_state_check(T,GrT), ground_value_check_aux(GrT,Val,R).
106
107
108 :- block ground_typedvals_check(-,?).
109 ground_typedvals_check([],R) :- !, R=ground_value.
110 ground_typedvals_check([typedval(Val,_Type,VarID,_EnumWarning)|T],R) :- !, ground_typedvals_check_aux(VarID,Val,T,R).
111 ground_typedvals_check(TL,R) :- add_internal_error('Illegal typedval list:',ground_typedvals_check(TL,R)).
112
113 :- block ground_typedvals_check_aux(-,?,?,?).
114 ground_typedvals_check_aux(_,Val,T,R) :- ground_typedvals_check(T,GrT), ground_value_check_aux(GrT,Val,R).
115
116
117 :- block ground_bexpr_check(-,?).
118 ground_bexpr_check(BExpr,R) :-
119 bexpr_variables(BExpr,Vars),
120 ground_value_check(Vars,R).
121
122 % -------------------------------
123
124
125 % attempt at a more efficient version of term_variables; avoiding traversing big avl_set's
126 %bexpr_variables(T,V) :- !, term_variables(T,V).
127 bexpr_variables(b(P,_,_),Vars) :-
128 bexpr_variables_aux(P,[],Vars), !.
129 bexpr_variables(T,V) :- var(V),
130 add_internal_error('Computation of vars failed: ',bexpr_variables(T,V)),
131 term_variables(T,V).
132
133 % check if a B expression or predicate is ground
134 ground_bexpr(b(P,_,_)) :- !,
135 bexpr_variables_aux(P,[],[]).
136 ground_bexpr(T) :- add_internal_error('Illegal call: ',ground_bexpr(T)),
137 ground(T).
138
139 % get free variables inside a B value
140 value_variables(V,Vars) :- var(V),!, Vars=[V]. % optimize a few frequent cases
141 value_variables(avl_set(A),Vars) :- !, check_avl_set(A),Vars=[].
142 value_variables([],Vars) :- !, Vars=[].
143 value_variables(Val,Vars) :-
144 value_variables(Val,[],Vars).
145
146 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
147
148 % check if a B value is ground
149 %version below seems a bit faster than ground_value(Val) :- value_variables(Val,[],[]).
150
151 :- if(environ(prob_safe_mode,true)).
152 ground_value(Val) :- ground_value1(Val),!,
153 (ground(Val) -> true
154 ; add_internal_error('Value incorrectly marked as ground by:',ground_val(Val)),fail).
155 ground_value(Val) :- ground(Val), !,add_internal_error('Value incorrectly marked as non-ground:',ground_val(Val)).
156 :- else.
157 ground_value(Val) :-ground_value1(Val).
158 :- endif.
159
160 ground_value1(V) :- var(V),!,fail.
161 ground_value1(pred_true) :- !.
162 ground_value1(pred_false) :- !.
163 ground_value1(int(N)) :- !, nonvar(N).
164 ground_value1(global_set(N)) :- !, ground(N).
165 ground_value1(freetype(N)) :- !, ground(N).
166 ground_value1(string(S)) :- !, ground(S).
167 ground_value1(fd(X,T)) :- !, nonvar(X),nonvar(T).
168 ground_value1([]) :- !.
169 ground_value1(avl_set(A)) :- !,check_avl_set(A).
170 ground_value1([H|T]) :- !, ground_value1(H),ground_value1(T).
171 ground_value1((A,B)) :- !, ground_value1(A),ground_value1(B).
172 ground_value1(freeval(ID,Case,Value)) :- !,
173 ground(ID),
174 ground(Case), % Case can be non-ground, ID should be nonvar, but could contain type variables!
175 ground_value1(Value).
176 ground_value1(rec(F)) :- !, ground_fields(F).
177 ground_value1(closure(_P,_T,B)) :- !, ground_bexpr(B). %% DO WE NEED TO CHECK P ? Probably not
178 ground_value1(term(T)) :- !, ground(T).
179 ground_value1(T) :- functor(T,F,N), format('~n*** uncovered term in ground_value ~w/~w~n',[F,N]),
180 ground(T).
181
182 ground_fields(V) :- var(V),!,fail.
183 ground_fields([]).
184 ground_fields([field(Name,Val)|T]) :- ground(Name), ground_value1(Val), ground_fields(T).
185
186 % a version of ground_value that also accepts record fields and lists of record fields without printing warnings
187 ground_value_or_field(V) :- var(V),!,fail.
188 ground_value_or_field(field(F,Value)) :- !, ground(F), ground_value(Value).
189 ground_value_or_field([H|T]) :- !, ground_value_or_field(H),ground_value_or_field(T).
190 ground_value_or_field(V) :- ground_value(V).
191
192 % check if a B state is ground
193 ground_state(V) :- var(V),!,fail.
194 ground_state([]) :- !.
195 ground_state([bind(N,V)|T]) :- !, ground(N),
196 ground_value(V), ground_state(T).
197 ground_state(S) :- add_internal_error('Illegal state: ',ground_state(S)),fail.
198
199 :- use_module(library(aggregate),[term_variables/3]).
200
201 bexpr_variables(b(P,_,_)) --> bexpr_variables_aux(P).
202 % following clause not really needed !?, bexpr_variables_bin/l_bexpr_variables perform propagation
203 %bexpr_variables(b(P,_,_),In,Out) :-
204 % (Out==[] -> In=[] ; true), % useful to propagate empty set to output for ground_bexpr checks
205 % bexpr_variables_aux(P,In,Out).
206
207 value_variables(V) --> {var(V)},!,term_variables_atomic(V). % slightly unnecessary to do two var checks
208 value_variables(avl_set(A)) --> !,{check_avl_set(A)},[].
209 value_variables((A,B)) --> !, value_variables(A),value_variables(B).
210 value_variables([H|T]) --> !, value_variables(H),value_variables(T).
211 value_variables(closure(_P,_T,B)) --> !, bexpr_variables(B). %% DO WE NEED TO CHECK P ? Probably not
212 value_variables(pred_false) --> !,[].
213 value_variables(pred_true) --> !,[].
214 value_variables(fd(X,T)) --> !, {check_nonvar(T)},term_variables_atomic(X).
215 value_variables([]) --> !,[].
216 value_variables(rec(F)) --> !, record_variables(F).
217 value_variables(freeval(ID,Case,Value)) --> !,
218 value_variables(ID),
219 value_variables(Case), % Case can be a variable
220 value_variables(Value).
221 value_variables(string(S)) --> !,term_variables_atomic(S). % not sure this is useful
222 value_variables(int(I)) --> !,term_variables_atomic(I).
223 value_variables(global_set(S)) --> !, term_variables_atomic(S). % normally global_sets should always be ground
224 value_variables(T) --> %{ functor(T,F,N), print(uncov_value_variables(F,N)),nl},
225 term_variables(T).
226
227 check_nonvar(T) :- (var(T) -> add_internal_error('Unexpected variable: ',T) ; true).
228
229 record_variables(V) --> {var(V)},!,term_variables(V).
230 record_variables([]) --> [].
231 record_variables([field(F,V)|T]) -->
232 term_variables_atomic(F), % is this necessary ?
233 value_variables(V), record_variables(T).
234
235 :- use_module(tools, [exact_member/2]).
236 % an optimized version of term_variables/3 which assumes argument is either var or ground
237 term_variables_atomic(VarOrGround,Vars,NewVars) :-
238 var(VarOrGround),
239 \+ exact_member(VarOrGround,Vars),
240 !,
241 NewVars = [VarOrGround|Vars].
242 term_variables_atomic(_,Vars,Vars).
243
244 %bexpr_variables_aux(value(V)) --> !,value_variables(V).
245 bexpr_variables_aux(value(V),In,Out) :- !,
246 (Out==[] -> In=[], ground_value(V) % avoid collecting variables after first variable found, useful for ground_bexpr
247 ; value_variables(V,In,Out)).
248 % 0-ary
249 bexpr_variables_aux(boolean_false) --> !,[].
250 bexpr_variables_aux(boolean_true) --> !,[].
251 bexpr_variables_aux(bool_set) --> !,[].
252 bexpr_variables_aux(empty_set) --> !,[].
253 bexpr_variables_aux(empty_sequence) --> !,[].
254 bexpr_variables_aux(falsity) --> !,[].
255 bexpr_variables_aux(max_int) --> !,[].
256 bexpr_variables_aux(min_int) --> !,[].
257 bexpr_variables_aux(float_set) --> !,[].
258 bexpr_variables_aux(real_set) --> !,[].
259 bexpr_variables_aux(string_set) --> !,[].
260 bexpr_variables_aux(truth) --> !,[].
261 %unary:
262 bexpr_variables_aux(card(A)) --> !, bexpr_variables(A).
263 bexpr_variables_aux(closure(A)) --> !, bexpr_variables(A).
264 %bexpr_variables_aux(closure1(A)) --> !, bexpr_variables(A).
265 bexpr_variables_aux(convert_bool(A)) --> !, bexpr_variables(A).
266 bexpr_variables_aux(convert_real(A)) --> !, bexpr_variables(A).
267 bexpr_variables_aux(convert_int_floor(A)) --> !, bexpr_variables(A).
268 bexpr_variables_aux(convert_int_ceiling(A)) --> !, bexpr_variables(A).
269 bexpr_variables_aux(domain(A)) --> !, bexpr_variables(A).
270 bexpr_variables_aux(identifier(_)) --> !,[].
271 bexpr_variables_aux(integer(_)) --> !,[].
272 bexpr_variables_aux(integer_set(_)) --> !,[].
273 bexpr_variables_aux(first(A)) --> !, bexpr_variables(A).
274 bexpr_variables_aux(first_of_pair(A)) --> !, bexpr_variables(A).
275 bexpr_variables_aux(last(A)) --> !, bexpr_variables(A).
276 bexpr_variables_aux(max(A)) --> !, bexpr_variables(A).
277 bexpr_variables_aux(min(A)) --> !, bexpr_variables(A).
278 bexpr_variables_aux(perm(A)) --> !, bexpr_variables(A).
279 bexpr_variables_aux(pow_subset(A)) --> !, bexpr_variables(A).
280 bexpr_variables_aux(pow1_subset(A)) --> !, bexpr_variables(A).
281 bexpr_variables_aux(range(A)) --> !, bexpr_variables(A).
282 bexpr_variables_aux(real(_)) --> !,[].
283 bexpr_variables_aux(reflexive_closure(A)) --> !, bexpr_variables(A).
284 bexpr_variables_aux(rev(A)) --> !, bexpr_variables(A).
285 bexpr_variables_aux(reverse(A)) --> !, bexpr_variables(A).
286 bexpr_variables_aux(second_of_pair(A)) --> !, bexpr_variables(A).
287 bexpr_variables_aux(seq(A)) --> !, bexpr_variables(A).
288 bexpr_variables_aux(seq1(A)) --> !, bexpr_variables(A).
289 bexpr_variables_aux(size(A)) --> !, bexpr_variables(A).
290 bexpr_variables_aux(string(_)) --> !, [].
291 bexpr_variables_aux(unary_minus(A)) --> !, bexpr_variables(A).
292 bexpr_variables_aux(unary_minus_real(A)) --> !, bexpr_variables(A).
293 % binary:
294 bexpr_variables_aux(add(A,B)) --> !, bexpr_variables_bin(A,B).
295 bexpr_variables_aux(add_real(A,B)) --> !, bexpr_variables_bin(A,B).
296 bexpr_variables_aux(conjunct(A,B)) --> !, bexpr_variables_bin(A,B).
297 bexpr_variables_aux(disjunct(A,B)) --> !, bexpr_variables_bin(A,B).
298 bexpr_variables_aux(div(A,B)) --> !, bexpr_variables_bin(A,B).
299 bexpr_variables_aux(div_real(A,B)) --> !, bexpr_variables_bin(A,B).
300 bexpr_variables_aux(domain_restriction(A,B)) --> !, bexpr_variables_bin(A,B).
301 bexpr_variables_aux(domain_subtraction(A,B)) --> !, bexpr_variables_bin(A,B).
302 bexpr_variables_aux(cartesian_product(A,B)) --> !, bexpr_variables_bin(A,B).
303 %bexpr_variables_aux(comprehension_set(A,B)) --> !, bexpr_variables_bin(A,B).
304 bexpr_variables_aux(couple(A,B)) --> !, bexpr_variables_bin(A,B).
305 bexpr_variables_aux(equal(A,B)) --> !, bexpr_variables_bin(A,B).
306 bexpr_variables_aux(equivalence(A,B)) --> !, bexpr_variables_bin(A,B).
307 bexpr_variables_aux(function(A,B)) --> !, bexpr_variables_bin(A,B).
308 bexpr_variables_aux(greater_equal(A,B)) --> !, bexpr_variables_bin(A,B).
309 bexpr_variables_aux(greater(A,B)) --> !, bexpr_variables_bin(A,B).
310 bexpr_variables_aux(image(A,B)) --> !, bexpr_variables_bin(A,B).
311 bexpr_variables_aux(implication(A,B)) --> !, bexpr_variables_bin(A,B).
312 bexpr_variables_aux(insert_front(A,B)) --> !, bexpr_variables_bin(A,B).
313 bexpr_variables_aux(insert_tail(A,B)) --> !, bexpr_variables_bin(A,B).
314 bexpr_variables_aux(intersection(A,B)) --> !, bexpr_variables_bin(A,B).
315 bexpr_variables_aux(interval(A,B)) --> !, bexpr_variables_bin(A,B).
316 bexpr_variables_aux(lazy_lookup_expr(_)) --> !,[].
317 bexpr_variables_aux(lazy_lookup_pred(_)) --> !,[].
318 bexpr_variables_aux(less_equal(A,B)) --> !, bexpr_variables_bin(A,B).
319 bexpr_variables_aux(less(A,B)) --> !, bexpr_variables_bin(A,B).
320 bexpr_variables_aux(less_equal_real(A,B)) --> !, bexpr_variables_bin(A,B).
321 bexpr_variables_aux(less_real(A,B)) --> !, bexpr_variables_bin(A,B).
322 bexpr_variables_aux(member(A,B)) --> !, bexpr_variables_bin(A,B).
323 bexpr_variables_aux(minus(A,B)) --> !, bexpr_variables_bin(A,B).
324 bexpr_variables_aux(minus_real(A,B)) --> !, bexpr_variables_bin(A,B).
325 bexpr_variables_aux(modulo(A,B)) --> !, bexpr_variables_bin(A,B).
326 bexpr_variables_aux(multiplication(A,B)) --> !, bexpr_variables_bin(A,B).
327 bexpr_variables_aux(multiplication_real(A,B)) --> !, bexpr_variables_bin(A,B).
328 bexpr_variables_aux(negation(A)) --> !, bexpr_variables(A).
329 bexpr_variables_aux(not_equal(A,B)) --> !, bexpr_variables_bin(A,B).
330 bexpr_variables_aux(not_member(A,B)) --> !, bexpr_variables_bin(A,B).
331 bexpr_variables_aux(not_subset(A,B)) --> !, bexpr_variables_bin(A,B).
332 bexpr_variables_aux(not_subset_strict(A,B)) --> !, bexpr_variables_bin(A,B).
333 bexpr_variables_aux(overwrite(A,B)) --> !, bexpr_variables_bin(A,B).
334 bexpr_variables_aux(partial_function(A,B)) --> !, bexpr_variables_bin(A,B).
335 bexpr_variables_aux(partition(A,BL)) --> !, bexpr_variables(A), l_bexpr_variables(BL).
336 bexpr_variables_aux(range_restriction(A,B)) --> !, bexpr_variables_bin(A,B).
337 bexpr_variables_aux(range_subtraction(A,B)) --> !, bexpr_variables_bin(A,B).
338 bexpr_variables_aux(record_field(A,_FieldName)) --> !, bexpr_variables(A).
339 bexpr_variables_aux(restrict_front(A,B)) --> !, bexpr_variables_bin(A,B).
340 bexpr_variables_aux(restrict_tail(A,B)) --> !, bexpr_variables_bin(A,B).
341 bexpr_variables_aux(set_subtraction(A,B)) --> !, bexpr_variables_bin(A,B).
342 bexpr_variables_aux(subset(A,B)) --> !, bexpr_variables_bin(A,B).
343 bexpr_variables_aux(subset_strict(A,B)) --> !, bexpr_variables_bin(A,B).
344 bexpr_variables_aux(union(A,B)) --> !, bexpr_variables_bin(A,B).
345 % ternary
346 bexpr_variables_aux(if_then_else(A,B,C)) --> !, l_bexpr_variables([A,B,C]).
347 % with new local variables:
348 bexpr_variables_aux(comprehension_set(_Ids,A)) --> !, bexpr_variables(A).
349 bexpr_variables_aux(exists(_Ids,A)) --> !, bexpr_variables(A).
350 bexpr_variables_aux(event_b_comprehension_set(_Ids,A,B)) --> !, bexpr_variables_bin(A,B).
351 bexpr_variables_aux(forall(_Ids,A,B)) --> !, bexpr_variables_bin(A,B).
352 bexpr_variables_aux(lambda(_Ids,A,B)) --> !, bexpr_variables_bin(A,B).
353 bexpr_variables_aux(lazy_let_expr(_ID,A,B)) --> !, bexpr_variables_bin(A,B).
354 bexpr_variables_aux(lazy_let_pred(_ID,A,B)) --> !, bexpr_variables_bin(A,B).
355 bexpr_variables_aux(lazy_let_subst(_ID,A,B)) --> !, bexpr_variables_bin(A,B).
356 %bexpr_variables_aux(let_predicate(_Ids,E,A)) --> !, bexpr_variables(E), bexpr_variables(A).
357 %bexpr_variables_aux(let_expression(_Ids,E,A)) --> !, bexpr_variables(E), bexpr_variables(A).
358 bexpr_variables_aux(general_sum(_Ids,A,B)) --> !, bexpr_variables_bin(A,B).
359 bexpr_variables_aux(general_product(_Ids,A,B)) --> !, bexpr_variables_bin(A,B).
360 bexpr_variables_aux(quantified_union(_Ids,A,B)) --> !, bexpr_variables_bin(A,B).
361 bexpr_variables_aux(quantified_intersection(_Ids,A,B)) --> !, bexpr_variables_bin(A,B).
362 % with lists:
363 bexpr_variables_aux(sequence_extension(A)) --> !, l_bexpr_variables(A).
364 bexpr_variables_aux(set_extension(A)) --> !, l_bexpr_variables(A).
365 bexpr_variables_aux(struct(A)) --> !, bexpr_variables(A).
366 bexpr_variables_aux(tail(A)) --> !, bexpr_variables(A).
367 bexpr_variables_aux(total_function(A,B)) --> !, bexpr_variables_bin(A,B).
368 bexpr_variables_aux(external_function_call(_FunName,A)) --> !, l_bexpr_variables(A).
369 bexpr_variables_aux(external_pred_call(_FunName,A)) --> !, l_bexpr_variables(A).
370 % TODO: rec(Fields)
371 % general case (could be used for all above; but is considerably slower)
372 bexpr_variables_aux(Expr) -->
373 %{ functor(Expr,F,N), print(uncov_var_aux(F,N)),nl },
374 {safe_syntaxelement_det(Expr,Subs,_Names,_List,_Constant)},
375 l_bexpr_variables(Subs).
376
377 bexpr_variables_bin(A,B,In,Out) :-
378 (Out==[] -> In=[],Int=[] ; true), % propagate for ground_bexpr use case where Out is []
379 bexpr_variables(A,In,Int), bexpr_variables(B,Int,Out).
380
381 l_bexpr_variables([]) --> [].
382 %l_bexpr_variables([H]) --> !, bexpr_variables(H). % propagate empty result list for ground_bexpr
383 l_bexpr_variables([H|T],In,Out) :-
384 (Out==[] -> In=[], Int=[] ; true), % propagate for ground_bexpr use case where Out is []
385 bexpr_variables(H,In,Int), l_bexpr_variables(T,Int,Out).
386
387
388
389
390 %:- use_module(custom_explicit_sets, [expand_custom_set_to_list_now/2]).
391 % dispatch. TODO: closure/3 and freetype
392 %:- meta_predicate map_over_bvalue(2,?,?).
393 %map_over_bvalue(_,[],[]) :- !.
394 %map_over_bvalue(Pred,[H|T],[Res|Tail]) :- !,
395 % map_over_bvalue(Pred,H,Res),
396 % map_over_bvalue(Pred,T,Tail).
397 %map_over_bvalue(Pred,(A,B),(ResA,ResB)) :- !,
398 % map_over_bvalue(Pred,A,ResA),
399 % map_over_bvalue(Pred,B,ResB).
400 %map_over_bvalue(Pred,rec(L),rec(Res)) :- !,
401 % map_over_bvalue(Pred,L,Res).
402 %map_over_bvalue(Pred,avl_set(A),Res) :- !,
403 % custom_explicit_sets:expand_custom_set_to_list_now(avl_set(A),L),
404 % map_over_bvalue(Pred,L,Res).
405 %map_over_bvalue(Pred,global_set(A), Res) :- !,
406 % custom_explicit_sets:expand_custom_set_to_list_now(global_set(A), L),
407 % map_over_bvalue(Pred,L,Res).
408 %map_over_bvalue(Pred,field(Name,Value),field(Name,TValue)) :- !,
409 % map_over_bvalue(Pred,Value,TValue).
410 %% apply
411 %map_over_bvalue(Pred,BValue,OutValue) :- !,
412 % call(Pred,BValue,OutValue).
413
414 % ----------------------------------
415 :- assert_must_succeed((kernel_tools:filter_cannot_match([int(X),int(11),Y],int(12),R,F), R==[int(X),Y],F==true)).
416
417 % filter out from the set Set (list part) all elements that cannot match X
418 % Filtered=true means at least one element was filtered out
419 filter_cannot_match(Set,X,NewSet,Filtered) :- instantiated_enough(X),!,
420 filter_cannot_match_aux(Set,X,NewSet,Filtered).
421 filter_cannot_match(S,_,S,false).
422
423 :- use_module(library(avl),[avl_domain/2, avl_height/2]).
424 :- use_module(custom_explicit_sets,[sorted_ground_normalised_list_to_avlset/3]).
425 :- use_module(performance_messages,[cond_perfmessage/2]).
426 filter_cannot_match_aux(Var,_,Res,Filtered) :- var(Var),!,Res=Var,Filtered=false.
427 filter_cannot_match_aux([],_,Res,Filtered) :- !, Res=[],Filtered=false.
428 filter_cannot_match_aux([H|T],X,Res,Filtered) :- !,
429 (cannot_match(X,H) -> Filtered=true,filter_cannot_match_aux(T,X,Res,_)
430 ; Res=[H|RT], filter_cannot_match_aux(T,X,RT,Filtered)).
431 filter_cannot_match_aux(avl_set(Avl),X,R,Filtered) :- check_avl_set(Avl),
432 avl_height(Avl,H),
433 (H<8 -> true % TODO: we could add Solver Strength here
434 ; cond_perfmessage([data_validation_mode/false],avl_set_not_filtered(H,X)),fail),
435 !,
436 avl_domain(Avl,List),
437 filter_cannot_match_aux(List,X,L2,Filtered),
438 (Filtered=true
439 -> sorted_ground_normalised_list_to_avlset(L2,R,filter_cannot_match_aux)
440 ; R=avl_set(Avl)).
441 filter_cannot_match_aux(S,_,S,false).
442
443 :- use_module(probsrc(tools_lists),[member_nonvar_list/2]).
444 % does it make sense to filter Set, or will cannot_match always fail
445 instantiated_enough(V) :- var(V),!,fail.
446 instantiated_enough(pred_true) :- !.
447 instantiated_enough(pred_false) :- !.
448 instantiated_enough(int(X)) :- !, nonvar(X).
449 instantiated_enough(fd(X,T)) :- !, nonvar(X),nonvar(T).
450 instantiated_enough(string(X)) :- !, nonvar(X).
451 instantiated_enough((A,B)) :- instantiated_enough(A) -> true ; instantiated_enough(B).
452 instantiated_enough(rec(Fs)) :- (member_nonvar_list(field(N,V),Fs),nonvar(N),instantiated_enough(V) -> true).
453 % TO DO: free-types, ...
454
455
456 %delay_filter_cannot_match(Set,X,NewSet) :-
457 % block_filter_cannot_match_aux(Set,X,NewSet).
458 %
459 %:- block block_filter_cannot_match_aux(-,?,?).
460 %block_filter_cannot_match_aux([],_,Res) :- !, Res=[].
461 %block_filter_cannot_match_aux([H|T],X,Res) :-
462 % (cannot_match(X,H) -> block_filter_cannot_match_aux(T,X,Res)
463 % ; Res=[H|RT], block_filter_cannot_match_aux(T,X,RT)).
464 %block_filter_cannot_match_aux(S,_,S).
465
466
467 % convert a typed expression into a value that can be used to filter a list of values with filter_cannot_match
468 get_template_for_filter_cannot_match(TExpr,ValueForFiltering) :-
469 get_template_for_filter3(TExpr,ValueForFiltering,NonVar), nonvar(NonVar).
470 get_template_for_filter3(b(E,_,_),Val,NonVar) :-
471 get_template_for_filter_aux(E,Val,NonVar).
472 get_template_for_filter_aux(value(Val),Val,NonVar) :- !, (nonvar(Val) -> NonVar=nonvar ; true).
473 get_template_for_filter_aux(couple(A,B),(VA,VB),NonVar) :- !,
474 get_template_for_filter3(A,VA,NonVar),
475 get_template_for_filter3(B,VB,NonVar).
476 %get_template_for_filter_aux(identifier(_),_,_).
477 get_template_for_filter_aux(_,_,_).
478
479
480 :- assert_must_succeed((kernel_tools:can_match(int(1),_V))).
481 :- assert_must_fail((kernel_tools:cannot_match(int(1),_V))).
482 :- assert_must_succeed((kernel_tools:can_match(int(12),int(12)))).
483 :- assert_must_succeed((kernel_tools:cannot_match(int(1),int(2)))).
484 :- assert_must_succeed((kernel_tools:cannot_match(string(a),string(b)))).
485 :- assert_must_succeed((kernel_tools:can_match(string(a),string(a)))).
486 :- assert_must_succeed((kernel_tools:can_match(string(a),string(_)))).
487 :- assert_must_succeed((kernel_tools:can_match(string(_),string(b)))).
488 :- assert_must_succeed((kernel_tools:cannot_match([],[string(b)]))).
489 :- assert_must_succeed((kernel_tools:cannot_match([_],[]))).
490 :- assert_must_succeed((kernel_tools:cannot_match((int(11),string(a)),(int(11),string(b))))).
491 :- assert_must_succeed((kernel_tools:can_match((int(11),string(a)),(int(11),string(_))))).
492 :- assert_must_succeed((kernel_tools:cannot_match(pred_false,pred_true))).
493 :- assert_must_succeed((kernel_tools:can_match(pred_true,pred_true))).
494 :- assert_must_succeed((kernel_tools:can_match(record([field(a,pred_true)]),record([field(a,_)])))).
495 :- assert_must_succeed((kernel_tools:cannot_match(record([field(a,pred_false)]),record([field(a,pred_true)])))).
496
497 % can_match: quick check to see if the (AVL or List) element could match
498
499 can_match(A,B) :- \+ cannot_match(A,B).
500 cannot_match(A,B) :- \+ can_match_aux(A,B). % Note: probably better to wrap can_match into negation to avoid instantiations
501
502 :- use_module(clpfd_interface,[clpfd_can_match/2]).
503
504 can_match_aux(A,_) :- var(A),!. % TO DO: we could check for not_empty_set co-routine if A or B = []?
505 can_match_aux(_,B) :- var(B),!.
506 can_match_aux((A,B),(ElA,ElB)) :- !,can_match_aux(A,ElA), can_match_aux(B,ElB).
507 can_match_aux(int(A),R) :- !,
508 % (\+ ground(R) -> true,print(ok(int(A),R)),nl ; print(unify(R,int(A))),nl,R=int(A)). % unification could trigger other constraint propagations and be expensive; we could just check that A is in domain
509 (var(R) -> true
510 ; R=int(B), clpfd_can_match(A,B)). %,(B=A -> true ; print(ko(A,B)),nl,fail)).%,fail,trace,B=A)).
511 can_match_aux(fd(NrA,GS),R) :- !,
512 %(\+ ground(R) -> true ; R=fd(Nr,GS)). % ditto (see, e.g., test 985 - graph iso)
513 (var(R) -> true ; R=fd(NrB,GS), clpfd_can_match(NrA,NrB)).
514 can_match_aux(pred_false,R) :- !, R=pred_false.
515 can_match_aux(pred_true,R) :- !, R=pred_true.
516 can_match_aux(string(A),R) :- !, %(\+ ground(R) -> true ; R=string(A)). % may instantiate LHS
517 (var(R) -> true ; R=string(B), can_match_atomic(A,B)).
518 can_match_aux(term(A),R) :- !, %(\+ ground(R) -> true ; R=term(A)). % ditto
519 (var(R) -> true ; R=term(B), can_match_term(A,B)).
520 can_match_aux(freeval(ID,Case,Value),R) :- !,
521 (var(R) -> true
522 ; R=freeval(IDR,CaseR,VR),
523 (var(IDR) ; var(CaseR) -> true
524 ; (ID,Case)=(IDR,CaseR),
525 can_match_aux(Value,VR))).
526 can_match_aux([],R) :- !, R \= avl_set(node(_,_,_,_,_)), R\= [_|_].
527 can_match_aux(avl_set(A),R) :- !, check_avl_set(A),
528 can_match_avl_set(R,A).
529 can_match_aux(global_set(_),R) :- !, R \= []. % global sets must be non-empty; TO DO: maybe quick check in case global_set is infinite; TO DO: check if two global_sets are identical
530 can_match_aux([_|_],R) :- !, R \= [].
531 can_match_aux(record(Fields1),record(Fields2)) :- !,can_match_fields(Fields1,Fields2).
532 can_match_aux(_,_). % catch-all other types
533
534 can_match_fields(A,B) :- (var(A);var(B)),!.
535 can_match_fields([],[]).
536 can_match_fields([F1|T1],[F2|T2]) :- can_match_field(F1,F2), can_match_fields(T1,T2).
537
538 can_match_field(A,B) :- (var(A);var(B)),!.
539 can_match_field(field(F1,V1),field(F2,V2)) :- F1==F2,!, can_match_aux(V1,V2).
540 can_match_field(F1,F2) :- add_internal_error('Non-matching fields: ',can_match_field(F1,F2)).
541
542 can_match_term(floating(F1),FF2) :- !,
543 (var(FF2) -> true ; FF2=floating(F2), can_match_atomic(F1,F2)). % floating numbers / reals
544 can_match_term(T1,T2) :- can_match_atomic(T1,T2).
545
546 :- use_module(kernel_dif,[frozen_dif/2]).
547 can_match_atomic(A,B) :- var(A),!, \+ frozen_dif(A,B).
548 can_match_atomic(A,B) :- var(B),!, \+ frozen_dif(B,A).
549 can_match_atomic(A,B) :- A=B.
550
551 :- use_module(library(avl),[avl_min/2, avl_max/2, avl_size/2]).
552
553 can_match_avl_set([],A) :- !, A=empty.
554 can_match_avl_set([H|T],A) :- !, list_can_match_avl_set([H|T],0,A).
555 can_match_avl_set(avl_set(B),A) :- !, avl_min(A,Min), avl_min(B,Min), avl_max(A,Max),avl_max(B,Max).
556 can_match_avl_set(_,_).
557
558 list_can_match_avl_set(T,_,_) :- var(T),!.
559 list_can_match_avl_set([],Sze,A) :- !, avl_size(A,Sze).
560 list_can_match_avl_set([H|T],Sze,A) :- !,
561 (custom_explicit_sets:quick_test_avl_membership(A,H,PredRes)
562 -> PredRes=pred_true, S1 is Sze+1,
563 list_can_match_avl_set(T,S1,A)
564 ; true). % TO DO: maybe also check T ?
565 list_can_match_avl_set(_,_,_).
566
567 % ------------------------
568
569 ?cannot_match_aggressive(A,B) :- \+ can_match_aggr(A,B).
570
571 % a more aggressive version; which may trigger co-routines for left-side A
572 can_match_aggr(A,_) :- var(A),!.
573 can_match_aggr(_,B) :- var(B),!.
574 can_match_aggr((A,B),(ElA,ElB)) :- !,can_match_aggr(A,ElA), can_match_aggr(B,ElB).
575 can_match_aggr(int(A),R) :- !, % R=int(A). % can trigger co-routines both sides; causes problem for 985
576 (var(R) -> true
577 ; R=int(B), (var(B) -> clpfd_can_match(A,B) ; A=B)). % only triggers co-routines for left side
578 can_match_aggr(fd(NrA,GS),R) :- !, % R=fd(Nr,GS). % ditto
579 (var(R) -> true
580 ; R=fd(NrB,GS), (var(NrB) -> clpfd_can_match(NrA,NrB) ; NrA=NrB)).
581 can_match_aggr(string(A),R) :- !, %R=string(A). % ditto
582 (var(R) -> true
583 ; R=string(B), (var(B) -> can_match_atomic(A,B) ; A=B)).
584 can_match_aggr(pred_false,R) :- !, R=pred_false.
585 can_match_aggr(pred_true,R) :- !, R=pred_true.
586 can_match_aggr(A,B) :- can_match_aux(A,B).
587
588
589 % ----------------------------------------
590
591
592
593 /* COMPARING TWO CLOSURES */
594
595
596
597 :- use_module(probsrc(avl_tools),[avl_height_less_than/2]).
598 :- use_module(probsrc(btypechecker),[l_unify_types_strict/2, unify_types_strict/2]).
599
600 % a quick check, use instead of == to compare values
601 quick_same_value(V1,V2) :- var(V1),!,V1==V2.
602 quick_same_value(_,V2) :- var(V2),!,fail.
603 quick_same_value(closure(P,T1,B1),closure(P,T2,B2)) :- !,
604 l_unify_types_strict(T1,T2),
605 quick_same_texpr_body(B1,B2).
606 quick_same_value(avl_set(A),AB) :-
607 !, % == for avl_set can be expensive ! triggered e.g. by x = (1..100000) \ {55} & (x \ {33}) <: x
608 % top-level avl_set usually handled by subset_of_explicit_set or similar code
609 AB=avl_set(B),
610 avl_height_less_than(A,3), % what depth value to use? maybe we should simply not compare at all
611 % TODO: what about other values pairs (avl_set(),_), rec(Fields), ...
612 A==B.
613 quick_same_value(V1,V2) :- V1==V2.
614
615 :- use_module(probsrc(custom_explicit_sets),[quick_definitely_maximal_set_avl/1]).
616 inner_quick_same_value(V1,V2) :- var(V1),!,V1==V2.
617 inner_quick_same_value(_,V2) :- var(V2),!,fail.
618 inner_quick_same_value(closure(P,T1,B1),closure(P,T2,B2)) :- !,
619 l_unify_types_strict(T1,T2), % should never fail
620 quick_same_texpr_body(B1,B2).
621 inner_quick_same_value((V1a,V1b),(V2a,V2b)) :- !,
622 inner_quick_same_value(V1a,V2a),
623 inner_quick_same_value(V1b,V2b).
624 inner_quick_same_value(rec(F1),rec(F2)) :- !,
625 inner_quick_same_fields(F1,F2).
626 inner_quick_same_value(avl_set(AVL),global_set(_)) :- !,
627 quick_definitely_maximal_set_avl(AVL).
628 inner_quick_same_value(global_set(_),avl_set(AVL)) :- !,
629 quick_definitely_maximal_set_avl(AVL).
630 inner_quick_same_value(V1,V2) :- % TODO: we could compare avl_sets
631 V1==V2.
632
633 inner_quick_same_fields(V1,V2) :- var(V1),!,V1==V2.
634 inner_quick_same_fields(_,V2) :- var(V2),!,fail.
635 inner_quick_same_fields([],[]).
636 inner_quick_same_fields([F1|T1],[F2|T2]) :- % TODO: check nonvar(Name...)
637 inner_quick_same_field(F1,F2),
638 inner_quick_same_fields(T1,T2).
639
640 inner_quick_same_field(V1,V2) :- var(V1),!,V1==V2.
641 inner_quick_same_field(_,V2) :- var(V2),!,fail.
642 inner_quick_same_field(field(Name1,V1),field(Name2,V2)) :- Name1==Name2,
643 inner_quick_same_value(V1,V2).
644
645 quick_same_texpr_body(b(E1,Type1,_),b(E2,Type2,_)) :-
646 check_unify_types_strict(Type1,Type2), % types should always match
647 qsame_texpr2(E1,E2).
648
649 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
650 :- if(true). %environ(prob_safe_mode,true)).
651 check_unify_types_strict(T1,T2) :- unify_types_strict(T1,T2),!.
652 check_unify_types_strict(T1,T2) :-
653 add_warning(check_unify_types_strict,'Unexpected difference in types: ',T1 \= T2),fail.
654 :- else.
655 check_unify_types_strict(_,_).
656 :- endif.
657
658 qsame_texpr2(value(V1),value(V2)) :- !,
659 inner_quick_same_value(V1,V2).
660 qsame_texpr2(E1,E2) :-
661 functor(E1,F,Arity),
662 functor(E2,F,Arity),
663 safe_syntaxelement_det(E1,Subs1,_Names1,_List1,Constant1),
664 safe_syntaxelement_det(E2,Subs2,_Names2,_List2,Constant2), Constant2==Constant1,
665 quick_same_sub_expressions(Subs1,Subs2).
666
667 quick_same_sub_expressions([],[]).
668 quick_same_sub_expressions([H1|T1],[H2|T2]) :-
669 quick_same_texpr_body(H1,H2),
670 quick_same_sub_expressions(T1,T2).
671
672 % --------------------
673
674 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
675 :- if(environ(prob_safe_mode,true)).
676 :- use_module(avl_tools,[check_is_non_empty_avl/1]).
677 check_avl_set(V) :- check_is_non_empty_avl(V).
678 :- else.
679 check_avl_set(_).
680 :- endif.
681
682 % ------------------------------------------
683
684
685 :- assert_must_succeed((kernel_tools:ground_value_opt_check(int(X),_,V), var(V), X=1, nonvar(V))).
686 :- assert_must_succeed((kernel_tools:ground_value_opt_check(string(X),_,V), var(V), X=a, nonvar(V))).
687 :- assert_must_succeed((kernel_tools:ground_value_opt_check([int(1),int(X)],_,V), var(V), X=1, nonvar(V))).
688 % instantiate third argument to atomic-nonvar term if first argument ground B value
689 % if second argument is instantiated the check is no longer required, co-routines should be discarded
690 % useful to ensure e.g. that enumeration_only_fdvar or similar checks work
691
692 % a version with an additional Needed flag that can discard the ground value check if no longer needed
693 :- block ground_value_opt_check(-,-,?).
694 ground_value_opt_check(_,Needed,_) :- nonvar(Needed),!,
695 true. % R=ground_value. Warning: instantiating R can change order of firing co-routines in kernel_mappings
696 % This makes test 1720 fail: int_plus instantiates a variable to int(_) -> which triggers ground_value_opt_check
697 % this in turn instantiates R and then triggers another co-routine (convert_list_of_expressions_into_set_wf)
698 % before finishing int_plus (which should have run until int_plus4, frozen_dif in a subsidiary call sees not pending int_plus4 co-routine)
699 % Other tests which fail: 983, 1380
700 ground_value_opt_check([],_,R) :- !, R=ground_value.
701 ground_value_opt_check(pred_true,_,R) :- !, R=ground_value.
702 ground_value_opt_check(pred_false,_,R) :- !, R=ground_value.
703 ground_value_opt_check(int(X),Needed,R) :- !, opt_ground_atom(X,Needed,R).
704 ground_value_opt_check(global_set(X),Needed,R) :- !, opt_ground_atom(X,Needed,R).
705 ground_value_opt_check(fd(X,_T),Needed,R) :- !,opt_ground_atom(X,Needed,R). % avoid waking up co-routines with R=X.
706 ground_value_opt_check(string(X),Needed,R) :- !, opt_ground_atom(X,Needed,R).
707 ground_value_opt_check((A,B),Needed,R) :- !,
708 ground_value_opt_check(A,Needed,GA), ground_value_opt_check_aux(GA,B,Needed,R).
709 ground_value_opt_check([H|T],Needed,R) :- !,
710 ground_value_opt_check(H,Needed,GA), ground_value_opt_check_aux(GA,T,Needed,R).
711 ground_value_opt_check(avl_set(A),_,R) :- !, % assume avl_set grounded
712 check_avl_set(A),
713 R = ground_value.
714 ground_value_opt_check(rec(F),Needed,R) :- !, opt_ground_fields(F,Needed,R).
715 ground_value_opt_check(closure(_P,_T,B),Needed,R) :- !,
716 bexpr_variables(B,Vars),
717 ground_value_opt_check(Vars,Needed,R).
718 %when(ground(Vars),R=ground_value).
719 ground_value_opt_check(term(X),Needed,R) :- !, opt_ground_term(X,Needed,R).
720 ground_value_opt_check(Val,Needed,R) :- %print(uncov(Val,R)),nl,trace,
721 (atomic(Val) -> R=ground_value ; when((ground(Val);nonvar(Needed)),R=ground_value)).
722
723
724 :- block opt_ground_term(-,-,?).
725 opt_ground_term(_,Needed,_) :- nonvar(Needed),!.
726 opt_ground_term(floating(F),Needed,R) :- !, opt_ground_atom(F,Needed,R).
727 opt_ground_term(X,Needed,R) :-
728 when((ground(X); nonvar(Needed)),R=ground_value).
729
730 :- block opt_ground_atom(-,-,?).
731 opt_ground_atom(A,_,Res) :- nonvar(A),!, Res=ground_value.
732 opt_ground_atom(_,_,_).
733
734 :- block ground_value_opt_check_aux(-,?,-,?).
735 ground_value_opt_check_aux(_,V,Needed,R) :- ground_value_opt_check(V,Needed,R).
736 % :- block ground_value_check_aux(-,?,-). % this slows down test 884, 292, 293, 1456, 1737
737
738
739 :- block opt_ground_fields(-,-,?).
740 opt_ground_fields(_,Needed,_) :- nonvar(Needed),!.
741 opt_ground_fields([],_,R) :- !, R=ground_value.
742 opt_ground_fields([field(F,V)|T],Needed,R) :- opt_ground_fields_aux(F,V,T,Needed,R).
743
744 :- block opt_ground_fields_aux(-,?,?,-,?).
745 opt_ground_fields_aux(_,V,T,Needed,R) :- opt_ground_fields(T,Needed,GrT), ground_value_opt_check_aux(GrT,V,Needed,R).
746
747 % ------------------------------------------
748
749 :- use_module(tools_meta, [residue_has_only_clpfd_in_constraints/1]).
750 :- use_module(kernel_reals,[use_clpfd_real_solver/0, do_not_double_check_solution/0]).
751 :- use_module(debug, [debug_mode/1]).
752 add_call_residue_error(Source,Msg,Residue) :-
753 clpfd_residue_ok(Residue),
754 !,
755 ajoin([Msg,' (probably due to use of CLP(FD) for reals): '],Msg2),
756 add_message(Source,Msg2,Residue),
757 (debug_mode(on) -> portray_residue(Residue) ; true).
758 add_call_residue_error(Source,Msg,Residue) :-
759 add_error(Source,Msg,Residue),
760 portray_residue(Residue).
761
762 clpfd_residue_ok(Residue) :-
763 residue_has_only_clpfd_in_constraints(Residue),
764 use_clpfd_real_solver,
765 do_not_double_check_solution. % at the moment CLP(FD) leaves uninstantiated intermediate vars
766 % TODO: check if we should also check get_preference(use_chr_solver,true)
767
768 portray_residue(L) :- gen_clause(L,C), portray_clause((residue :- C)).
769 gen_clause([],true).
770 gen_clause([X],X) :- !.
771 gen_clause([H|T],(H,R)) :- gen_clause(T,R).
772
773 get_functor(Mod:E,Mod:F,N) :- !, get_functor(E,F,N).
774 get_functor(E,F,N) :- functor(E,F,N).
775
776 :- use_module(probsrc(tools_strings),[ajoin/2]).
777 :- use_module(tools_printing, [print_goal/1]).
778
779 check_residue_for_call([],_) :- !.
780 check_residue_for_call(Residue,Call) :-
781 check_residue_for_call_wf(Residue,Call,unknown,no_wf_available,_).
782
783 :- use_module(kernel_waitflags,[add_warning_wf/5, add_internal_error_wf/5, add_message_wf/5]).
784 check_residue_for_call_wf([],_,_,_,Res) :- !, Res=residue_ok.
785 check_residue_for_call_wf(Residue,Call,Span,WF,Res) :-
786 get_functor(Call,F,N),
787 (clpfd_residue_ok(Residue)
788 -> ajoin(['Prolog residue for call to ',F,'/',N,' (probably due to use of CLP(FD) for reals): '],Msg),
789 add_message_wf(kernel_tools,Msg,Residue,Span,WF),
790 (debug_mode(on) -> portray_residue(Residue) ; true),
791 Res=residue_ok
792 ; get_preference(use_chr_solver,true) ->
793 ajoin(['Prolog residue for call to ',F,'/',N,' (possibly due to call_residue imprecise for CHR): '],Msg),
794 add_warning_wf(kernel_tools,Msg,Residue,Span,WF),
795 portray_residue(Residue), Res=residue_warning
796 ; ajoin(['Prolog residue for call to ',F,'/',N,':'],Msg),
797 add_internal_error_wf(kernel_tools,Msg,Residue,Span,WF),
798 portray_residue(Residue), print_goal(Call),nl,
799 Res=residue_error
800 ).