1 % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(kernel_equality,[equality_objects_wf/4,
6 equality_objects_wf_no_enum/4, % a version which does not enumerate boolean result
7 equality_objects_lwf/5, equality_objects/3,
8 equality_objects_with_type_wf/5,
9 empty_set_test/2, empty_set_test_wf/3,
10 empty_cartesian_product_wf/4,
11 or_eq_obj/3,
12 get_cardinality_wait_flag/4, get_cardinality_wait_flag/5,
13 get_cardinality_powset_wait_flag/5,
14 get_cardinality_relation_over_wait_flag/6,
15 %get_cardinality_partial_function_wait_flag/7,
16 check_and_remove/4,
17 membership_test_wf/4,
18 membership_test_wf_with_force/4,
19 enum_equality_result_wf/3, enum_equality_result_smt_mode_wf/3,
20 cartesian_pair_test_wf/5,
21 in_nat_range_test/4,
22
23 dif/3, integer_dif/2, bool_dif/2, eq_atomic/4,
24
25 subset_test/4, subset_strict_test/4,
26 test_interval_subset_wf/6,
27 conjoin_test/4,
28 equality_can_be_decided_by_unification/1]).
29
30 :- use_module(module_information,[module_info/2]).
31 :- module_info(group,kernel).
32 :- module_info(description,'This module provides reified equality and membership predicates.').
33
34 :- use_module(library(clpfd)).
35
36 :- use_module(kernel_objects,[equal_object/3, equal_object_wf/4,
37 not_equal_object/2, not_equal_object_wf/3,
38 cardinality_as_int_for_wf/2,
39 empty_set_wf/2, not_empty_set_wf/2,
40 exhaustive_kernel_check/2, exhaustive_kernel_check/1,
41 exhaustive_kernel_check_wf/2, exhaustive_kernel_fail_check_wf/2,
42 exhaustive_kernel_check_wfdet/2, exhaustive_kernel_fail_check_wfinit/2,
43 exhaustive_kernel_fail_check/1]).
44 :- use_module(kernel_card_arithmetic,[safe_mul/3, safe_add_card/3, safe_pow2/2, is_inf_or_overflow_card/1]).
45 :- use_module(b_interpreter_check,[conjoin/6]).
46 :- use_module(kernel_dif).
47
48 :- use_module(self_check).
49
50
51 :- use_module(probsrc(clpfd_interface),[catch_clpfd_overflow_call3/3, clpfd_in_domain/3]).
52 :- use_module(probsrc(debug),[debug_println/2]).
53
54
55 :- use_module(error_manager).
56
57 % kernel_equality
58 % :- ensure_loaded(kernel_equality).
59
60 :- use_module(custom_explicit_sets).
61 :- use_module(kernel_waitflags).
62
63 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([int(2),int(1)],[int(2)],pred_false))).
64 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([int(2),int(1)],[],pred_false))).
65 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([int(2),int(1)],[int(1),int(2)],pred_true))).
66 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([[int(2)],[int(1)]],[[int(1)],[int(2)]],pred_true))).
67 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([string('STRING1')],[string('STRING2')],pred_false))).
68 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([string('STRING2'),string('STRING1')],
69 [string('STRING1'),string('STRING2')],pred_true))).
70 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([(int(1),int(2)),(int(1),int(3))],[(int(1),int(3)),(int(1),int(2))],pred_true))).
71 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([(int(2),int(2)),(int(1),int(3))],[(int(2),int(3)),(int(1),int(2))],pred_false))).
72 :- assert_must_succeed((equality_objects(A,B,R), A=[int(2),int(3)],B=[int(X),int(Y)],
73 X=4,Y=2, R==pred_false)).
74 :- assert_must_succeed((equality_objects(A,B,R), A=[int(2),int(3)],B=[int(X),int(Y)],
75 X=2,Y=4, R==pred_false)).
76 :- assert_must_succeed((equality_objects(A,B,R), A=[int(2),int(3)],B=[int(X),int(Y)],
77 X=3,Y=2, R==pred_true)).
78 :- assert_must_succeed((equality_objects(A,B,R), A=[int(2),int(3)],B=[int(X),int(Y)],
79 X=2,Y=3, R==pred_true)).
80 :- assert_must_succeed((equality_objects(A,B,R), A=int(2),B=int(X),
81 R=pred_true, X==2)).
82
83
84 /* equality_objects/3 is a function which compares two objects
85 and returns either pred_true or pred_false in the third argument,
86 as soon as it can be decided whether the objects are equal */
87
88
89 equality_objects_wf(X,Y,Res,no_wf_available) :- !,
90 ? equality_objects(X,Y,Res).
91 equality_objects_wf(X,Y,Res,WF) :-
92 equality_objects_lwf(X,Y,Res,LWF,WF),
93 ? (var(Res) -> get_last_wait_flag(equality_objects_wf,WF,LWF) ; true).
94
95 equality_objects_lwf(X,Y,Res,LWF,WF) :-
96 equality_objects_wf_no_enum(X,Y,Res,WF),
97 ? force_equality_objects_lwf2(X,Y,Res,LWF).
98
99 :- block force_equality_objects_lwf2(?,?,-,-).
100 force_equality_objects_lwf2(X,Y,Res,LWF) :-
101 % tools_printing:print_term_summary(force_equality(X,Y,Res,LWF)),nl,
102 ( nonvar(Res) -> true
103 ; nonvar(X), X=int(_),
104 number(LWF), LWF>= 1152921504606844951, % only catch overflows if equality's priority low
105 preferences:preference(use_clpfd_solver,true)
106 ? -> force_equality_int_clpfd(X,Y,Res)
107 ; ( % print(forcing_equal(_X,_Y,_LWF)),nl, %%
108 % alternative would be to propagate LWF down to and_equality ?
109 %Res \== pred_false, equal_object(X,Y,force_equality_objects_lwf2), % not required anymore as and_equality can propagate pred_true down (commented out 27.2.2015)
110 % this can trigger CLPFD overflow; e.g., for x>1 & y:NATURAL & y=x+x & z={y,x}
111 Res=pred_true
112 ; %Res \== pred_true, not_equal_object(X,Y), % note required anymore (commented out 27.2.2015)
113 Res=pred_false
114 )).
115
116 % useful for e.g. x>1 & y:NATURAL & y=x+x & z={y,x}
117 force_equality_int_clpfd(_X,_Y,Res) :- %print(try_force_equality_int_clpfd(Res,_X,_Y)),nl,
118 catch_clpfd_overflow_call3(Res=pred_true,silent,Overflow=true),
119 (Overflow==true
120 -> !, debug_println(19,'Not forcing equality to true due to CLPFD overflow') % hope that enumeration will work
121 ; true).
122 force_equality_int_clpfd(_X,_Y,Res) :-
123 ? catch_clpfd_overflow_call3(Res=pred_false,message,
124 (debug_println(19,'Not forcing equality to false due to CLPFD overflow'),
125 delay_check_pred_false(Res))).
126
127 :- block delay_check_pred_false(-).
128 delay_check_pred_false(pred_false).
129
130 :- block equality_objects_with_expansion(-,-,?,?), equality_objects_with_expansion(?,-,-,?), equality_objects_with_expansion(-,?,-,?).
131 % will expand second argument; use if first argument is a tail of a list (representing a set)
132 equality_objects_with_expansion(X,Y,R,WF) :-
133 nonvar(Y), is_custom_explicit_set_nonvar(Y),!,
134 expand_custom_set_wf(Y,ExpSet,equality_objects_with_expansion,WF),
135 equality_objects_wf_no_enum(X,ExpSet,R,WF).
136 equality_objects_with_expansion(X,Y,R,WF) :-
137 equality_objects_wf_no_enum(X,Y,R,WF).
138
139
140 :- use_module(bool_pred).
141 % a version of equality_objects with type information available: allows to dispatch to boolean version
142 equality_objects_with_type_wf(boolean,X,Y,R,_) :- !, bool_pred:bool_equality(X,Y,R).
143 equality_objects_with_type_wf(_,X,Y,R,WF) :-
144 (X==Y -> R=pred_true ; equality_objects_block_wf(X,Y,R,WF)).
145
146 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([int(1)],[],pred_false))).
147 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([int(1)],[int(2)],pred_false))).
148 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([int(1),int(2)],[int(2),int(1)],pred_true))).
149 :- assert_must_succeed((kernel_equality:equality_objects([int(1)],[],R),R==pred_false)).
150 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects(freeval(id1,case1,int(1)),freeval(id1,case1,int(1)),pred_true))).
151 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects(freeval(id1,case1,int(1)),freeval(id1,case1,int(2)),pred_false))).
152 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects(freeval(id1,case1,int(1)),freeval(id1,case2,int(1)),pred_false))).
153
154 ?equality_objects(X,Y,R) :- equality_objects_wf_no_enum(X,Y,R,no_wf_available).
155
156 equality_objects_wf_no_enum(X,Y,R,WF) :-
157 (X==Y % could be expensive for long lists
158 -> R=pred_true
159 ? ; equality_objects_block_wf(X,Y,R,WF)).
160 % This is in principle more precise: but entails some performance penalty?!
161 %equality_objects(X,Y,R) :- when((?=(X,Y);nonvar(X);nonvar(Y)), (X==Y -> R=pred_true ; equality_objectsb(X,Y,R))).
162 :- block equality_objects_block_wf(-,-,-,?).
163 %equality_objectsb_wf(X,Y,R) :- % this case no longer needed, basic_type below will instantiate Y for this special case
164 % (nonvar(X) -> X=fd(XN,GS) ; nonvar(Y) -> Y=fd(XN,GS)),
165 % (var(GS) -> print(var_gs(fd(XN,GS))),nl,fail ; true),
166 % b_global_sets:is_global_set_of_cardinality_one(GS,N),!, % there exist only one object of that type
167 % XN=N, Y=X, R=pred_true.
168 %equality_objectsb(X,Y,R) :- X==Y,!,R=pred_true. % only makes sense if all three are variables; cannot happen here; we could have int(X)==int(Y), but then code further below will trigger
169 equality_objects_block_wf(X,Y,R,WF) :-
170 ? equality_objects0(X,Y,R,WF).
171
172 %:- block %equality_objects0(-,-,?,?),
173 % equality_objects0(?,-,-,?), equality_objects0(-,?,-,?).
174 equality_objects0(X,Y,R,WF) :- nonvar(R),!, % we know the result of the comparison
175 ? ( R=pred_true -> equal_object_wf(X,Y,equality_objects0,WF)
176 ? ; R=pred_false -> not_equal_object_wf(X,Y,WF)
177 ; add_error_fail(equality_objects0,'Illegal result: ',equality_objects0(X,Y,R,WF))
178 ).
179 % now we know that either X or Y must be nonvar
180 equality_objects0(X,Y,R,WF) :-
181 (nonvar(Y)
182 -> (X==[] -> eq_empty_set_wf(Y,R,WF)
183 ? ; equality_objects1(Y,X,R,WF)
184 )
185 ; equality_objects1(X,Y,R,WF)
186 ).
187
188 :- use_module(chrsrc(chr_integer_inequality),[chr_eq/3]).
189 :- use_module(clpfd_interface,[post_constraint2/2]).
190
191 equality_int(X,Y,Res) :- nonvar(X),nonvar(Y),!,
192 (X=Y -> Res=pred_true ; Res=pred_false).
193 equality_int(X,Y,Res) :-
194 % check for attached dif co-routines; diabled if CHR is used (no dif coroutine needed)
195 % !! there might still be dif coroutines set up by equality_expr and dis
196 % preferences:preference(use_chr_solver,false),
197 ? fd_frozen_dif(X,Y),!, Res=pred_false.
198 equality_int(X,Y,Res) :-
199 (preferences:preference(use_chr_solver,true) -> chr_eq(X,Y,Res) ; true),
200 % with CHR we detect e.g. r=TRUE in (X=Y <=> r=TRUE) & X:1..100 & Y > X
201 % see code for equality_fd
202 post_constraint2( ((X#=Y) #<=> R01), Posted), % from clpfd_interface
203 (Posted = true
204 -> prop_eq_01(Res,R01),
205 (var(R01) -> syntactic_equality_test(X,Y,Res) ; true) % CLPFD does not detect variable equality
206 ; eq_atomic_simple(X,Y,integer,Res)).
207
208
209 :- use_module(kernel_freetypes,[freetype_with_single_case/2, instantiate_freetype_case/3]).
210 %:- block equality_objects1(?,-,-,?). % avoid instantiating arg2 if result not known, problem for test 1488 : R:INTEGER<->INTEGER & dom(R)=D & X /: D & dom({(X,Y),B}) = DS & D=DS & Y:INTEGER
211 % equality_objects1 assumes first argument is nonvar:
212 %%equality_objects1(X,Y,R,_) :- print(equality_objects1(X,Y,R)),nl,fail. %%
213 equality_objects1(pred_true /* bool_true */,X,Res,_WF) :- !,
214 X=Res. % equivalent to bool_equality(pred_true /* bool_true */,X,Res).
215 equality_objects1(pred_false /* bool_false */,X,Res,_WF) :- !,
216 bool_pred:negate(X,Res). % equivalent to bool_equality(pred_false /* bool_false */,X,Res).
217 ?equality_objects1(int(X),IY,Res,_WF) :- !, IY=int(Y), equality_int(X,Y,Res).
218 equality_objects1(term(X),TY,Res,WF) :- !, TY=term(Y), eq_term_wf(X,Y,Res,WF).
219 equality_objects1(string(X),SY,Res,_WF) :- !, SY=string(Y), eq_atomic(X,Y,string,Res).
220 equality_objects1(fd(X,Type),FY,Res,_WF) :- !,
221 b_global_sets:get_global_type_value(FY,Type,Y),
222 equality_fd_objects(X,Y,Type,Res).
223 equality_objects1(freeval(Id,Case1,Value1),FY,Res,WF) :- !, FY=freeval(Id,Case2,Value2),
224 (nonvar(Id), freetype_with_single_case(Id,Case)
225 -> (Case,Case)=(Case1,Case2), % cases must match
226 equality_objects_wf_no_enum(Value1,Value2,Res,WF)
227 ; and_equality(CaseRes,ValueRes,Res),
228 eq_atomic(Case1,Case2,freeval_case,CaseRes),
229 equality_freeval_content(CaseRes,Value1,Value2,ValueRes,WF),
230 (var(Id) -> instantiate_freetype_case(Id,Case1,Case2) ; true)
231 ).
232 equality_objects1(rec(X),RY,Res,WF) :- !, RY=rec(Y), equality_fields(X,Y,Res,WF).
233 equality_objects1((X,Y),XY2,Res,WF) :- !, XY2=(X2,Y2),
234 equality_objects_wf_no_enum(X,X2,RX,WF),
235 and_equality(RY,RX,Res), % typically Res is var, hence it is better to call and_equality after X
236 (RX==pred_false -> true
237 ? ; equality_objects_wf_no_enum(Y,Y2,RY,WF)).
238 equality_objects1([],S,R,WF) :- !,eq_empty_set_wf(S,R,WF).
239 %equality_objects1(X,[],R,WF) :- !,eq_empty_set_wf(X,R,WF).
240 equality_objects1(X,Y,R,WF) :- equality_objects2(X,Y,R,WF).
241
242 :- block equality_freeval_content(-,?,?,?,?).
243 % if the case is different, we don't care anymore about the content; and the types could be different
244 equality_freeval_content(pred_false,_Value1,_Value2,_,_).
245 equality_freeval_content(pred_true,Value1,Value2,Res,WF) :-
246 % if we do not wait until we now that the case is the same,
247 % an internal type error might be raised
248 equality_objects_wf_no_enum(Value1,Value2,Res,WF).
249
250
251 :- use_module(error_manager,[add_warning/2]).
252
253 :- block equality_objects2(?,-,-,?). % also wait on second or third argument
254 equality_objects2(X,Y,Res,WF) :- nonvar(Res),!,% we know the result of the comparison
255 ( Res=pred_true -> %% print(forcing_equal(X,Y)),nl,%%
256 ? equal_object_wf(X,Y,equality_objects2_1,WF)
257 ; Res=pred_false -> not_equal_object_wf(X,Y,WF)
258 ; add_error_fail(equality_objects2,'Illegal result: ',equality_objects2(X,Y,Res,WF))
259 ).
260 equality_objects2([H|T],S,Res,WF) :- !,eq_cons(S,H,T,Res,WF). % move to equality_objects1 ?!
261 equality_objects2(avl_set(A),S,Res,WF) :-
262 (S=[H|T] -> !, eq_cons(avl_set(A),H,T,Res,WF)
263 ; S = [] -> !, (A=empty -> add_warning(equality_objects2,'Empty avl_set'), Res=pred_true
264 ; Res=pred_false)).
265 equality_objects2(ES1,ES2,Res,WF) :-
266 equality_explicit_sets_wf(ES1,ES2,ERes,WF), !,
267 Res=ERes.
268 equality_objects2(ES1,S,Res,WF) :- is_custom_explicit_set(ES1,eq_cons),!, % move to custom_explicit_sets?
269 % S = [] or ES1 = [] is already covered above
270 (S=[H|T] -> eq_cons(ES1,H,T,Res,WF) % maybe we can avoid expanding ES1
271 ? ; is_infinite_explicit_set(ES1),is_custom_explicit_set(S,eq_cons)
272 -> expand_custom_set_wf(S,ExpSet,equality_objects2,WF),
273 equality_objects0(ExpSet,ES1,Res,WF)
274 ; expand_custom_set_wf(ES1,ExpSet,equality_objects2,WF), equality_objects0(ExpSet,S,Res,WF)
275 ).
276 equality_objects2(X,Y,Res,WF) :-
277 add_internal_error('Unknown objects:',equality_objects2(X,Y,Res,WF)), % could happen with abort(.) terms ?
278 (equal_object_wf(X,Y,equality_objects2_2,WF),Res=pred_true
279 ;
280 not_equal_object_wf(X,Y,WF),Res=pred_false
281 ).
282
283 %:- use_module(b_global_sets,[b_get_fd_type_bounds/3]).
284 equality_fd_objects(X,Y,_,Res) :- number(X),number(Y),!,
285 (X=Y -> Res=pred_true ; Res= pred_false).
286 equality_fd_objects(X,Y,_,Res) :- % check for attached dif co-routines; later we should probably use CHR
287 fd_frozen_dif(X,Y),!,
288 % THIS DROPS THE PERFORMANCE OF probsli ../prob_examples/examples/B/ClearSy/alloc_large.mch -init -p TIME_OUT 5000
289 Res=pred_false.
290 % Is it really necessary to keep code below: clp(FD) will do this for us ?!
291 equality_fd_objects(X,Y,Type,Res) :-
292 nonvar(Type),b_global_sets:b_get_fd_type_bounds(Type,LowBnd,UpBnd),!,
293 (LowBnd=UpBnd
294 -> X=Y,Res=pred_true /* only one object of Type exists */
295 ; LB1 is LowBnd+1,
296 (LB1 = UpBnd
297 -> bin_eq_atomic(X,Y,Res,LowBnd,UpBnd) /* two objects exist */
298 ; eq_atomic_simple(X,Y,global(Type),Res),
299 (var(Res),(var(X);var(Y))
300 -> clpfd_in_domain(X,LowBnd,UpBnd), % just like X in LowBnd..UpBnd but can deal with UpBnd=inf
301 clpfd_in_domain(Y,LowBnd,UpBnd),
302 % still required ! even with fd_utils_clpfd ! (for v8 of Bosch CrCtl_Comb2_Final_mch.eventb)
303 equality_fd(X,Y,Res)
304 ; true
305 )
306 )
307 ).
308 equality_fd_objects(X,Y,Type,Res) :-
309 add_internal_error('Unknown type: ',equality_fd_objects(X,Y,Type,Res)),
310 eq_atomic_simple(X,Y,global(Type),Res).
311
312
313 % a reified version of equality
314 %equality_fd(X,Y,Res) :- X==Y,!, Res=pred_true. % not necessary; syntactic_equality_test below will trigger
315 equality_fd(X,Y,Res) :-
316 ((X#=Y) #<=> Reification01),
317 % (preferences:preference(use_chr_solver,true) -> chr_eq(X,Y,Res) ; true), Probably not useful as we do not keep track of info for FD variables; Sebastian: please investigate
318 prop_eq_01(Res,Reification01),
319 (var(Reification01)
320 -> syntactic_equality_test(X,Y,Res)
321 ; true).
322
323
324 % propagate pred_false/true <-> 0/1
325 :- block prop_eq_01(-,-).
326 % prop_eq_01(A,B) :- print(prop(A,B)),nl,fail.
327 ?prop_eq_01(P,B) :- var(P), !, prop_01_eq(B,P).
328 prop_eq_01(pred_true,1).
329 prop_eq_01(pred_false,0).
330 prop_01_eq(1,pred_true).
331 prop_01_eq(0,pred_false).
332
333
334 :- use_module(kernel_non_empty_attr,[get_empty_set_attr/3]).
335 %eq_empty_set(Set,PredRes) :-
336 % var(Set), var(PredRes), clpfd_card_is_gt0_for_var(Set),!, PredRes=false.
337 %eq_empty_set(Set,Res) :- eq_empty_set_attr_wf(Set,Res,no_wf_available).
338
339 eq_empty_set_attr_wf(Set,PredRes,WF) :- var(PredRes), var(Set),!,
340 get_empty_set_attr(Set,PredRes,ExistsAlready), % get attribute or create one if it does not exist
341 (ExistsAlready=is_empty_attr_exists
342 -> true % no need to compute the predicate; another call will already do it
343 ; eq_empty_set_wf(Set,PredRes,WF)).
344 eq_empty_set_attr_wf(X,R,WF) :- eq_empty_set_wf(X,R,WF).
345
346 :- use_module(kernel_waitflags,[add_error_wf/5]).
347
348 :- block eq_empty_set_wf(-,-,?).
349 % TO DO: inspect kernel_cardinality attributes
350 eq_empty_set_wf(X,R,WF) :- var(X),!,
351 (R=pred_true -> empty_set_wf(X,WF) ; not_empty_set_wf(X,WF)).
352 eq_empty_set_wf([],R,_) :- !,R=pred_true.
353 eq_empty_set_wf([_|_],R,_) :- !,R=pred_false.
354 eq_empty_set_wf(CS,R,WF) :- is_custom_explicit_set(CS,eq_empty_set_wf),!,
355 test_empty_explicit_set_wf(CS,R,WF).
356 eq_empty_set_wf(S,R,WF) :-
357 (S==term(undefined)
358 -> add_error_wf(eq_empty_set_wf,'Accessing uninitialised set value','',unknown,WF)
359 ; add_internal_error('Illegal Set: ',eq_empty_set_wf(S,R,_))
360 ),fail.
361
362
363 %%eq_cons(S,H,T,Res,_) :- print(eq_cons(S,H,T,Res)),nl,fail.
364 eq_cons([],_,_,Res,_) :- !, Res=pred_false.
365 eq_cons([H2|T2],H1,T1,Res,WF) :- !, % T2==[] checked? TODO: call eq_singleton_set_cons
366 check_and_remove_wf([H2|T2],H1,NewSet2,RemoveSuccesful,WF),
367 %% print(removed(H1,H2,T2,NewSet2,RemoveSuccesful)), %%
368 eq_cons2(RemoveSuccesful,H1,T1,H2,T2,NewSet2,Res,WF).
369 eq_cons(avl_set(A),H1,T1,Res,WF) :- !,
370 eq_cons_avl_set(A,H1,T1,Res,WF).
371 eq_cons(global_set(G),_H,T,Res,WF) :- %print(chk(G,H,T)),nl,
372 ? is_infinite_global_set(G,_),!,
373 expand_custom_set_to_list_wf(T,_ET,_Done,eq_cons,WF), % this will either succeed and we have a finite list ; or it will raise an enumeration warning exception
374 Res = pred_false.
375 eq_cons(ES,H1,T1,Res,WF) :- is_custom_explicit_set(ES,eq_cons),
376 expand_custom_set_wf(ES,ExpSet,eq_cons,WF),
377 eq_cons1(ExpSet,H1,T1,Res,WF).
378
379 % check if {H2} = {H1|T1}
380 eq_singleton_set_cons(H2,H1,T1,Res,WF) :- T1==[], !, equality_objects_wf_no_enum(H2,H1,Res,WF).
381 eq_singleton_set_cons(H2,H1,T1,Res,WF) :- empty_set_test_wf(T1,T1Empty,WF),
382 % TODO: we could also call equality_objects(H2,H1,H2H1Eq) if T1Empty is not known and conjoin it
383 eq_singleton2(H2,H1,T1Empty,Res,WF).
384
385 :- block eq_singleton2(?,?,-,-,?).
386 eq_singleton2(H2,H1,T1Empty,Res,WF) :- T1Empty==pred_true,!,
387 equality_objects_wf_no_enum(H2,H1,Res,WF).
388 eq_singleton2(_,_,T1Empty,Res,_) :- T1Empty==pred_false,!,
389 Res=pred_false. % if T1 is not empty, [H1|T1] is different from [H2]
390 eq_singleton2(H2,H1,T1Empty,Res,WF) :- Res==pred_true,!,T1Empty=pred_true,
391 equal_object_wf(H2,H1,eq_singleton2,WF).
392 eq_singleton2(H2,H1,T1Empty,Res,WF) :- Res==pred_false,!,
393 when(nonvar(T1Empty),eq_singleton2(H2,H1,T1Empty,Res,WF)).
394
395
396 % this treatment (second clause) is relevant for avoiding unnecessary choice points
397 % see e.g. codespeed test probsli ../prob_examples/examples/B/Alstom/vesg_Aug11/gradient_train_altitude.mch -animate 5 -p TIME_OUT 300000000 -p MAXINT 2147483647 -p MININT -2147483647 -p CLPFD TRUE (walltime/2471)
398 eq_cons_avl_set(A,H1,T1,Res,WF) :- is_one_element_avl(A,AEl),
399 !,
400 eq_singleton_set_cons(AEl,H1,T1,Res,WF).
401 eq_cons_avl_set(A,H1,T1,Res,WF) :-
402 (var(Res) -> kernel_tools:ground_value_check(H1,GrH1) ; true), % if Res already bound, no need to do ground check
403 block_eq_cons_avl_set(A,H1,T1,Res,GrH1,WF).
404 :- block block_eq_cons_avl_set(?,?,?,-,-,?).
405 block_eq_cons_avl_set(A,H1,T1,Res,_,WF) :- Res==pred_true,!,
406 kernel_objects:equal_custom_explicit_set_cons_wf(avl_set(A),H1,T1,WF).
407 block_eq_cons_avl_set(A,H1,T1,Res,_,WF) :-
408 element_can_be_added_or_removed_to_avl(H1),!, % should hopefully be true as H1 is now ground
409 (remove_element_from_explicit_set(avl_set(A),H1,RA)
410 -> equality_objects_with_expansion(T1,RA,Res,WF) %%% PROBLEM: T1 has to be in list form !
411 ; Res = pred_false
412 ).
413 block_eq_cons_avl_set(A,H1,T1,Res,_,WF) :-
414 % TO DO: we could call propagate_avl_element_information(X,AVL,ApproxSize,WF) if Res=pred_true and with WF or something similar higher up to detect when an element cannot be within the AVL set
415 expand_custom_set_wf(avl_set(A),ExpSet,block_eq_cons_avl_set,WF),
416 eq_cons1(ExpSet,H1,T1,Res,WF).
417
418 :- block eq_cons1(-,?,?,?,?).
419 eq_cons1(ExpSet,H1,T1,Res,WF) :- eq_cons(ExpSet,H1,T1,Res,WF).
420
421 :- block eq_cons2(-, ?,?,?,?, ?,-,?).
422 eq_cons2(RemoveSuccesful, H1,T1,H2,T2, _NewSet2,Res,WF) :- var(RemoveSuccesful),!,
423 % result has been instantiated before Remove finished; now force equal_object or not_equal_object
424 % note: without this the remove could be pending (see test 1112, 1105)
425 % TO DO: look whether we could force remove and continue from there ?
426 ? equality_objects2([H1|T1],[H2|T2],Res,WF).
427 eq_cons2(not_successful, _,_T1,_,_, _NewSet2,pred_false,_).
428 eq_cons2(successful, _, T1,_,_, NewSet2,Res,WF) :- equality_objects_wf_no_enum(T1,NewSet2,Res,WF).
429
430
431 check_and_remove(Set,ElementToRemove,ResultingSet,Res) :-
432 check_and_remove_wf(Set,ElementToRemove,ResultingSet,Res,no_wf_available).
433
434 :- block check_and_remove_wf(-,?,?,?,?).
435 check_and_remove_wf([],_,ResultingSet,Res,_) :- !, ResultingSet=[],Res=not_successful.
436 check_and_remove_wf([H|T],ElementToRemove,ResultingSet,Res,WF) :- !,
437 equality_objects_wf_no_enum(H,ElementToRemove,RH,WF),
438 %%print(equality_objects_result(H,ElementToRemove,RH)),nl,
439 check_and_remove2(RH,H,T,ElementToRemove,ResultingSet,Res,WF).
440 check_and_remove_wf(CS,ElementToRemove,ResultingSet,Res,WF) :-
441 expand_custom_set_to_list_wf(CS,ESet,_,check_and_remove,WF),
442 check_and_remove_wf(ESet,ElementToRemove,ResultingSet,Res,WF).
443
444 :- block check_and_remove2(-,?,?,?,?,?,?).
445 check_and_remove2(pred_true, _H,T,_ElementToRemove,T,successful,_).
446 check_and_remove2(pred_false,H,T,ElementToRemove,[H|RT],Res,WF) :-
447 check_and_remove_wf(T,ElementToRemove,RT,Res,WF).
448
449
450 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:and_equality(pred_false,pred_false,pred_false))).
451 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:and_equality(pred_true,pred_false,pred_false))).
452 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:and_equality(pred_true,pred_true,pred_true))).
453 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_true,pred_true,pred_false))).
454 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_true,pred_false,pred_true))).
455 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_false,pred_true,pred_true))).
456 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_false,pred_false,pred_true))).
457 :- block and_equality(-,-,-).
458 and_equality(X,Y,Res) :-
459 ( X==pred_true -> Res=Y
460 ; X==pred_false -> Res=pred_false
461 ; Y==pred_true -> Res=X
462 ; Y==pred_false -> Res=pred_false
463 ; Res==pred_true -> X=pred_true, Y=pred_true
464 ; Res==pred_false -> and_equality2(X,Y,Res) % we know that one of X,Y must be pred_false; if X==Y we could infer X=Y=pred_false
465 ; add_error_fail(and_equality,'Illegal call: ',and_equality(X,Y,Res))
466 ).
467 :- block and_equality2(-,-,?).
468 and_equality2(X,Y,Res) :-
469 ( X==pred_true -> Res=Y
470 ; X==pred_false -> Res=pred_false
471 ; Y==pred_true -> Res=X
472 ; Y==pred_false -> Res=pred_false
473 ; add_error_fail(and_equality,'Illegal call: ',and_equality2(X,Y,Res))
474 ).
475
476 /*
477 :- block bool_eq_atomic(-,?,?,-).
478 bool_eq_atomic(X,Y,OtherY,Res) :- nonvar(Res),!,
479 (Res=pred_true -> X=Y ; X=OtherY).
480 bool_eq_atomic(X,Y,_,Res) :- X==Y -> Res=pred_true ; Res=pred_false. */
481
482 % a version for base types with just two possible values
483 :- block bin_eq_atomic(-,?,-,?,?), bin_eq_atomic(?,-,-,?,?).
484 % no need to check for frozen_dif: a dif would instantly trigger instantiation to other value
485 % However, we could use when(?=(X,Y) ; nonvar(Res) as trigger ! maybe this would slowdown SATLIB tests ??
486 bin_eq_atomic(X,Y,Res,V1,V2) :- nonvar(Res),!,
487 %print(forcing_bin_eq_atomic(X,Y,Res,V1,V2)),nl,
488 (Res=pred_true -> X=Y
489 ; %print(bin_dif(X,Y)),nl,
490 (X=V1,Y=V2 ; X=V2,Y=V1)
491 ). % difference with eq_atomic: we now know the value !
492 bin_eq_atomic(X,Y,Res,_,_) :-
493 %print(triggering_bin_eq(X,Y,Res)), translate:print_frozen_info(Res),nl,
494 (X==Y -> Res=pred_true ; Res=pred_false).
495
496 eq_atomic(X,Y,_Type,Res) :- nonvar(X),nonvar(Y),!,
497 (X=Y -> Res=pred_true ; Res=pred_false).
498 eq_atomic(X,Y,_,Res) :- % check for attached dif co-routines; later we should probably use CHR
499 frozen_dif(X,Y),!, Res=pred_false.
500 eq_atomic(X,Y,Type,Res) :- when((?=(X,Y);nonvar(Res)),eq_atomic2(X,Y,Type,Res)).
501
502 % version of eq_atomic without frozen_dif check (if already performed)
503 % eq_atomic_simple(X,Y,_Type,Res) :- % in all calling contexts this test is already performed
504 % nonvar(X),nonvar(Y),!, (X=Y -> Res=pred_true ; Res=pred_false).
505 eq_atomic_simple(X,Y,Type,Res) :- when((?=(X,Y);nonvar(Res)),eq_atomic2(X,Y,Type,Res)).
506
507 /*
508 Comment: % for integers CLPFD reification will not ground Res if X==Y, need to do when((?=(X,Y)...
509 | ?- X in 1..10, Y in 1..10, (X#=Y #<=> Z), X=Y.
510 Y = X,
511 X in 1..10,
512 Z in 0..1 ? */
513
514 eq_atomic2(X,Y,Type,Res) :- nonvar(Res),!,
515 (Res=pred_true -> X=Y ; dif(Type,X,Y)).
516 eq_atomic2(X,Y,_Type,Res) :-
517 (X=Y -> Res=pred_true
518 ; Res=pred_false).
519
520 :- block eq_term_wf(-,-,?,?).
521 eq_term_wf(TX,TY,Res,_WF) :- nonvar(TX),TX = floating(FX),!,
522 TY=floating(FY), eq_atomic(FX,FY,real,Res). % TODO: use a proper equality check for reals/floats
523 eq_term_wf(TY,TX,Res,_WF) :- nonvar(TX),TX = floating(FX),!,
524 TY=floating(FY), eq_atomic(FX,FY,real,Res).
525 eq_term_wf(TX,TY,Res,_) :- eq_atomic(TX,TY,term,Res).
526
527 :- use_module(fd_utils_clpfd,[neq_fd/3]).
528 dif(boolean,A,B) :- !,
529 bool_pred:negate(A,B). % was: bool_dif(A,B).
530 % usually not covered: equality_objects_with_type calls bool_equality,
531 % equality_objects waits for either arg to be fully instantiated to pred_false or pred_true
532 dif(integer,A,B) :- !, integer_dif(A,B).
533 dif(global(T),A,B) :- !, neq_fd(A,B,T).
534 dif(_,A,B) :- dif(A,B).
535
536 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:integer_dif(0,1))).
537 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:integer_dif(1,1))).
538 :- use_module(clpfd_interface,[clpfd_neq/2]).
539 integer_dif(A,B) :- clpfd_neq(A,B). % clpfd_neq calls dif on overflow
540
541
542 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:bool_dif(pred_false,pred_true))).
543 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:bool_dif(pred_true,pred_false))).
544 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:bool_dif(pred_true,pred_true))).
545 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:bool_dif(pred_false,pred_false))).
546 bool_dif(A,B) :- bool_pred:negate(A,B).
547
548 /* old version:
549 :- block eq_atomic(-,?,-), eq_atomic(?,-,-).
550 eq_atomic(X,Y,Res) :- nonvar(Res),!,
551 (Res=pred_true -> X=Y ; dif(X,Y)).
552 eq_atomic(X,Y,Res) :- X==Y -> Res=pred_true
553 ; Res=pred_false.
554 */
555
556 :- use_module(kernel_records,[check_field_name_compatibility/3]).
557 :- block equality_fields(-,?,-,?), equality_fields(?,-,-,?), equality_fields(-,-,?,?).
558 % if last argument is known we should propagate the field names from one record to another; see test 1289 (Hansen12)
559 equality_fields([],[],pred_true,_).
560 equality_fields([field(Name1,V1)|T1],[field(Name2,V2)|T2],Res,WF) :-
561 % should we wait for Name1 or Name2 to become nonvar?
562 ? check_field_name_compatibility(Name1,Name2,equality_fields),
563 and_equality(RH,RT,Res),
564 equality_objects_wf_no_enum(V1,V2,RH,WF),
565 (RH==pred_false -> true
566 ? ; equality_fields(T1,T2,RT,WF)).
567
568
569
570 empty_set_test_wf(Set,EqRes,WF) :- eq_empty_set_attr_wf(Set,EqRes,WF).
571 empty_set_test(Set,EqRes) :- eq_empty_set_attr_wf(Set,EqRes,no_wf_available).
572 empty_cartesian_product_wf(Set1,Set2,EqRes,WF) :- % TO DO: pass WF
573 eq_empty_set_wf(Set1,EqRes1,WF),
574 (EqRes1==pred_true -> EqRes=pred_true /* avoid inspecting Set2 */
575 ; or_eq_obj(EqRes1,EqRes2,EqRes),
576 eq_empty_set_wf(Set2,EqRes2,WF)).
577
578
579 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:or_eq_obj(pred_false,pred_false,pred_false))).
580 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:or_eq_obj(pred_false,pred_true,pred_true))).
581 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:or_eq_obj(pred_true,pred_true,pred_true))).
582 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_true,pred_true,pred_false))).
583 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_true,pred_false,pred_false))).
584 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_false,pred_true,pred_false))).
585 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_false,pred_false,pred_true))).
586 :- block or_eq_obj(-,-,-).
587 % very similar to disjoin in b_interpreter_check; no waitflag to instantiate if result false
588 or_eq_obj(X,Y,XorY) :-
589 ( (X==pred_true ; Y==pred_true) -> XorY=pred_true
590 ; XorY==pred_false -> X=pred_false,Y=pred_false
591 ; X==pred_false -> XorY = Y
592 ; Y==pred_false -> XorY = X
593 ; XorY==pred_true -> or_eq_obj2(X,Y)
594 ; add_internal_error('Illegal call: ',or_eq_obj(X,Y,XorY)) ).
595 :- block or_eq_obj2(-,-).
596 or_eq_obj2(X,Y) :- ((X==pred_true; Y=pred_true) -> true
597 ; X==pred_false -> Y=pred_true
598 ; Y==pred_false -> X=pred_true
599 ; add_internal_error('Illegal call: ',or_eq_obj2(X,Y))).
600
601 % ------------------------------------------------------------------
602
603
604 % not used at the moment:
605 %get_partial_subset_priority(Set,WF,LWF) :- get_partial_set_size(Set,Size),
606 % safe_pow2(Size,Prio),
607 % get_wait_flag(Prio,psubset(Set),WF,LWF).
608 %get_partial_set_priority(Set,WF,LWF) :- get_partial_set_size(Set,Size),
609 % get_wait_flag(Size,pset(Set),WF,LWF).
610 %get_partial_set_size(X,R) :- var(X),!,R=3.
611 %get_partial_set_size([],R) :- !,R=0.
612 %get_partial_set_size([_|T],R) :- !,get_partial_set_size(T,RT), R is RT+1.
613 %get_partial_set_size(_,10).
614
615
616 get_cardinality_wait_flag(Set,Info,WF,LWF) :-
617 ? get_cardinality_wait_flag(Set,Info,WF,_Card,LWF).
618 get_cardinality_wait_flag(Set,Info,WF,Card,LWF) :-
619 cardinality_as_int_for_wf(Set,Card),
620 % when(nonvar(X), (print(get_card_waitflag(X,Set,WF,LWF)),nl)),
621 (var(Card)
622 -> kernel_waitflags:get_last_wait_flag(get_cardinality_wait_flag(Info),WF,LastWF)
623 ; true), % ensure that we trigger choice points waiting on LWF before infinite enumeration starts
624 ? get_cardinality_wait_flag2(Card,Info,WF,LastWF,LWF).
625 :- block get_cardinality_wait_flag2(-,?,?,-,?).
626 get_cardinality_wait_flag2(X,_Info,_WF,LastWF,LWF) :- var(X),!,LWF=LastWF.
627 ?get_cardinality_wait_flag2(X,Info,WF,_,LWF) :- get_bounded_wait_flag(X,Info,WF,LWF).
628
629 get_cardinality_powset_wait_flag(Set,Info,WF,CardSet,LWF) :-
630 cardinality_as_int_for_wf(Set,CardSet),
631 get_cardinality_powset_wait_flag2(CardSet,Info,WF,LWF).
632 :- block get_cardinality_powset_wait_flag2(-,?,?,?).
633 get_cardinality_powset_wait_flag2(X,Info,WF,LWF) :-
634 safe_pow2(X,X2),
635 %safe_mul(X2,10000,X3), % as generating subsets this way will generate repetitions
636 (is_inf_or_overflow_card(X2)
637 ? -> integer_pow2_priority(R), get_wait_flag(R,powset_card(Info),WF,LWF)
638 ? ; get_bounded_wait_flag(X2,powset_card(Info),WF,LWF) % finite prio; ensure we do not exceed infinite prios if X2 very large
639 ).
640
641
642 % CARDINALITY FOR NUMBER OF PARTIAL FUNCTIONS: (not used at the moment)
643 %get_cardinality_partial_function_wait_flag(DomSet,RanSet,Info,WF,CardDomSet,CardRanSet,LWF) :-
644 % cardinality_as_int_for_wf(DomSet,CardDomSet),
645 % cardinality_as_int_for_wf(RanSet,CardRanSet),
646 % get_cardinality_partial_function_wait_flag(CardDomSet,CardRanSet,Info,WF,LWF).
647 %:- block get_cardinality_partial_function_wait_flag(-,?,?,?,?),
648 % get_cardinality_partial_function_wait_flag(?,-,?,?,?).
649 %get_cardinality_partial_function_wait_flag(DC,RC,Info,WF,LWF) :-
650 % priority_pow1n(RC,DC,PFCARD), print(prio(PFCARD)),nl,
651 % get_bounded_wait_flag(PFCARD,powset_card(Info),WF,LWF).
652 % % Cardinality of the set of partial functions : (card(Range)+1)^card(Domain)
653 %priority_pow1n(X,Y,R) :- (X==inf ; Y==inf),!, integer_pow2_priority(R). %R=10000010. % TO DO: provide a separate module for combining priorities in a systematic way !
654 %priority_pow1n(X,Y,RR) :- X1 is X+1, safe_pown(X1,Y,R),
655 % (R==inf -> integer_pow2_priority(RR) %RR=10000010
656 % ; RR=R).
657
658 % CARDINALITY FOR NUMBER OF RELATIONS:
659 get_cardinality_relation_over_wait_flag(Dom,Ran,WF,LWF,MaxCardOfRel,MaxNrOfRels) :-
660 cardinality_as_int_for_wf(Dom,X),
661 cardinality_as_int_for_wf(Ran,Y),
662 get_cardinality_relation_over_wait_flag2(X,Y,WF,LWF,MaxCardOfRel,MaxNrOfRels).
663
664 :- block get_cardinality_relation_over_wait_flag2(-,?,?,?,?,?), get_cardinality_relation_over_wait_flag2(?,-,?,?,?,?).
665 get_cardinality_relation_over_wait_flag2(X,Y,WF,LWF,MaxCardOfRel,MaxNrOfRels1) :-
666 safe_mul(X,Y,MaxCardOfRel),
667 safe_pow2(MaxCardOfRel,MaxNrOfRels),
668 safe_add_card(MaxNrOfRels,1,MaxNrOfRels1), /* add 1 to give priority to tighter_enum */
669 ? get_bounded_wait_flag(MaxNrOfRels1,powset_rel_card,WF,LWF).
670
671 % ------------------------------------------------------------------
672
673 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(2),pred_true,WF),WF)).
674 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(1),pred_true,WF),WF)).
675 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([int(2),int(1),int(3),int(4),int(5)],int(4),pred_true,WF),WF)).
676 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(3),pred_false,WF),WF)).
677 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([],int(3),pred_false,WF),WF)).
678 :- assert_must_succeed(exhaustive_kernel_fail_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(3),pred_true,WF),WF)).
679 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([[int(2)],[int(1),int(3)],[int(4),int(1)]],[int(1),int(4)],pred_true,WF),WF)).
680 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([[int(2)],[int(1),int(3)],[int(4),int(1)]],[int(4)],pred_false,WF),WF)).
681 :- assert_must_succeed(exhaustive_kernel_fail_check_wf(kernel_equality:membership_test_wf([[int(2)],[int(1),int(3)],[int(4),int(1)]],[int(4)],pred_true,WF),WF)).
682 :- assert_must_succeed((membership_test_wf([int(2),int(1)],int(2),R,_WF),R==pred_true)).
683 :- assert_must_succeed((membership_test_wf([int(2),int(1)],int(X),R,_WF),var(R),X=1,R==pred_true)).
684 :- assert_must_succeed((membership_test_wf([int(2),int(1)],int(3),R,_WF),R==pred_false)).
685 :- assert_must_succeed((membership_test_wf(global_set('Name'),fd(1,'Name'),R,_WF),R==pred_true)).
686
687 :- assert_must_succeed((kernel_equality:membership_test_wf(avl_set(node(rec([field(cardinality,int(2)),field(col,fd(2,setField1)),field(fill,fd(1,setField2)),field(shape,fd(1,setField1))]),true,0,empty,empty)),
688 rec([field(cardinality,int(2)),field(col,fd(2,setField1)),field(fill,fd(1,setField2)),field(shape,fd(1,setField1))]),R,_WF), R==pred_true)).
689 :- assert_must_succeed((
690 kernel_equality:membership_test_wf([rec([field(cardinality,int(2)),field(col,fd(2,setField1)),field(fill,fd(1,setField2)),field(shape,fd(1,setField1))])],
691 rec([field(cardinality,int(2)),field(col,fd(2,setField1)),field(fill,fd(1,setField2)),field(shape,fd(1,setField1))]),R,_WF), R==pred_true
692 )).
693 /* membership_test_wf: A function that instantiates last argument when membership test can be decided */
694
695
696 % a version which also creates a choice point in SMT mode
697 membership_test_wf_with_force(Set,X,Res,WF) :-
698 membership_test_wf(Set,X,Res,outer,WF),
699 enum_equality_result_smt_mode_wf(Res,membership_test_wf,WF).
700 :- block force_equality_result(-,-).
701 force_equality_result(pred_true,_).
702 force_equality_result(pred_false,_).
703
704 enum_equality_result_smt_mode_wf(Res,PP,WF) :- var(Res),
705 preferences:preference(use_smt_mode,true),!,
706 enum_equality_result_wf(Res,PP,WF).
707 enum_equality_result_smt_mode_wf(_,_,_).
708
709 enum_equality_result_wf(Res,PP,WF) :-
710 get_last_wait_flag(PP,WF,LWF),
711 force_equality_result(Res,LWF).
712
713 ?membership_test_wf(Set,X,Res,WF) :- membership_test_wf(Set,X,Res,outer,WF).
714
715 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
716 :- if(environ(prob_data_validation_mode,true)).
717 :- block membership_test_wf(-,?,?,?,?). % avoid instantiating Set
718 :- else.
719 :- block membership_test_wf(-,?,-,?,?).
720 :- endif.
721 membership_test_wf(Set,X,Res,_OuterInner,WF) :- nonvar(Res),!,
722 (Res==pred_true
723 ? -> call_check_element_of_wf0(X,Set,WF)
724 /* (kernel_objects:unbound_variable_for_cons(Set)
725 -> kernel_objects:mark_as_non_free(X), % attach co-routine to indicate that we cannot freely chose X
726 print(instantiate_set(Set,X,Res)),nl,
727 Set=[X|_] % TO DO: normalise X first ?
728 ; when(nonvar(Set), membership_test_wf2(Set,X,Res,OuterInner,WF))
729 ) */
730 ; membership_not_el(Set,X,WF)).
731 membership_test_wf(Set,X,Res,OuterInner,WF) :-
732 ? membership_test_wf2(Set,X,Res,OuterInner,WF).
733
734 % we are not sure if WF0 is set; go via kernel_mappings:
735 ?call_check_element_of_wf0(X,Set,WF) :- get_wait_flag0(WF,WF0),
736 ? kernel_mappings:check_element_of_wf0(X,Set,WF,WF0,unknown).
737
738
739 :- block membership_not_el(-,?,?).
740 membership_not_el([],_,_WF) :- !.
741 membership_not_el([H|T],X,WF) :- !,
742 not_equal_object_wf(H,X,WF),
743 membership_not_el(T,X,WF).
744 membership_not_el(avl_set(A),X,WF) :- !,membership_custom_set_wf(avl_set(A),X,pred_false,WF).
745 membership_not_el(CS,X,WF) :- is_custom_explicit_set_nonvar(CS),!,
746 membership_custom_set_wf(CS,X,pred_false,WF).
747
748 membership_test_wf2([],_X,Res,_,_WF) :- !, Res=pred_false.
749 membership_test_wf2([H|T],X,Res,OuterInner,WF) :- !,
750 (Res==pred_false
751 -> not_equal_object_wf(H,X,WF), membership_test_wf(T,X,Res,WF)
752 ? ; T==[] -> equality_objects_wf_no_enum(H,X,Res,WF)
753 % TO DO: at the outer level we could check whether the list has the same length as the type of X
754 ; OuterInner=outer, is_definitely_maximal_set([H|T]) -> Res=pred_true
755 ; (OuterInner=outer, % avoid re-checking ground_list_with_fd over and over again
756 preferences:preference(use_clpfd_solver,true),
757 ground_list_with_fd([H|T]),
758 construct_avl_from_lists_wf([H|T],CS,WF))
759 % this slows down: probsli ../prob_examples/public_examples/EventBPrologPackages/SET_Game/SET_GAM_Sym_NoSet20_mch.eventb -mc 10000000 -expcterr goal_found -p SYMMETRY_MODE hash -p TIME_OUT 7000 -p CLPFD TRUE -df -goal "n=18" -p MAX_OPERATIONS 82 -cc 155 833
760 % TO DO: call clpfd_reify_inlist directly ? avoid translating to AVL and back to list; detect maximal list
761 ? -> membership_custom_set_wf(CS,X,Res,WF) %, print(conv_to_avl(X,[H|T],CS,Res)),nl
762 ; %print(eq(Res,H,X,T,WF)),nl,equality_objects_wf_dbg(H,X,HXRes,WF), % makes test 1003 : plavis-MemoryLoad_SP_55 fail
763 ? equality_objects_wf_no_enum(H,X,HXRes,WF),cons_el_of(HXRes,T,X,Res,WF)
764 % ,(var(HXRes) -> print(mem(X,[H|T],Res)), tools_printing:print_arg(X),nl ; true)
765 ).
766 ?membership_test_wf2(avl_set(A),X,Res,_,WF) :- !, membership_avl_set_wf(A,X,Res,WF).
767 membership_test_wf2(CS,X,Res,_,WF) :- is_custom_explicit_set(CS,membership_test_wf),!,
768 ? membership_custom_set_wf(CS,X,Res,WF).
769 membership_test_wf2(term(Z),_,_,_,_WF) :- Z==undefined,!,
770 add_error_fail(membership_test_wf,'Encountered uninitialised set variable', ''). % we will normally generate other error messages as well
771 membership_test_wf2(Z,X,Res,OuterInner,WF) :-
772 add_error_fail(membership_test_wf,'Not Set as first argument: ', membership_test_wf(Z,X,Res,OuterInner,WF)).
773
774 % detect certain lists containing FD values and convert them to avl sets: they have improved reification and can detect when a list is complete
775 ground_list_with_fd(V) :- var(V),!,fail.
776 ground_list_with_fd([H|T]) :- nonvar(H),ground_val(H),ground_list_with_fd(T).
777 ground_list_with_fd([]).
778
779 :- use_module(kernel_tools,[ground_value/1]).
780 ground_val(int(X)) :- number(X).
781 ground_val(pred_false).
782 ground_val(pred_true).
783 ground_val(fd(X,T)) :- number(X),ground(T).
784 ground_val((A,B)) :- nonvar(A),ground_val(A),ground_value(B).
785 ground_val(rec(Fields)) :- nonvar(Fields), Fields = [field(Name,V)|TFields], ground(Name),
786 ground_val(V),
787 ground_value(rec(TFields)).
788 % TO DO: add more checks; do we need this check ? related to is_avl_fd_index_set
789
790 :- block cons_el_of(-,?,?,-,?).
791 cons_el_of(HX_EQRES,T,X,MEMRES,WF) :- var(HX_EQRES),!, %print(cons_el_of(HX_EQRES,T,X,MEMRES)),nl,
792 (MEMRES=pred_false -> HX_EQRES=pred_false, /* otherwise element of set */
793 membership_not_el(T,X,WF)
794 % MEMRES must be pred_true
795 ; (T==[] -> %print(forcing_cons_el_of(T,X,MEMRES)),nl,
796 HX_EQRES=pred_true
797 ; cons_el_of_mem_obj(HX_EQRES,T,X,WF)) /* we have to wait for result of comparison with X */
798 ).
799 cons_el_of(pred_true,_,_,pred_true,_WF).
800 cons_el_of(pred_false,T,X,Res,WF) :-
801 (Res==pred_true -> non_empty_chk(T) ; true),
802 ? membership_test_wf(T,X,Res,inner,WF).
803
804 non_empty_chk(V) :- var(V),!,V=[_|_].
805 non_empty_chk(X) :- X \= []. % could be avl_set or closure
806
807 :- block cons_el_of_mem_obj(-,?,?,?).
808 cons_el_of_mem_obj(pred_true,_,_,_WF).
809 cons_el_of_mem_obj(pred_false,T,X,WF) :-
810 % Instantiation of T will be done by membership_test_wf, relevant for test 1273
811 membership_test_wf(T,X,pred_true,inner,WF).
812
813
814 :- assert_must_succeed((kernel_equality:cartesian_pair_test_wf((int(1),int(1)),
815 [int(1),int(2)],[int(2),int(3)],R,_WF),R==pred_false)).
816 :- assert_must_succeed((kernel_equality:cartesian_pair_test_wf((int(3),int(1)),
817 [int(1),int(2)],[int(2),int(3)],R,_WF),R==pred_false)).
818 :- assert_must_succeed((kernel_equality:cartesian_pair_test_wf((int(2),int(3)),
819 [int(1),int(2)],[int(2),int(3)],R,_WF),R==pred_true)).
820 :- assert_must_fail((kernel_equality:cartesian_pair_test_wf((int(1),int(3)),
821 [int(1),int(2)],[int(2),int(3)],pred_false,_WF))).
822
823 cartesian_pair_test_wf((X,Y),XType,YType,Res,WF) :- check_cartesian_pair1(X,XType,Y,YType,Res,WF).
824
825 :- block check_cartesian_pair1(-,?,-,?,-,?).
826 %check_cartesian_pair1(X,XType,Y,YType,Res) :- Res==pred_true,!,
827 % is_cartesian_pair_wf((X,Y),XType,YType,WF).
828 %check_cartesian_pair1(X,XType,Y,YType,Res) :- Res==pred_false,!,
829 % not_is_cartesian_pair((X,Y),XType,YType,WF).
830 check_cartesian_pair1(X,XType,Y,YType,Res,WF) :-
831 ((var(X),nonvar(Y)) -> check_cartesian_pair2(Y,YType,X,XType,Res,WF)
832 ; check_cartesian_pair2(X,XType,Y,YType,Res,WF)).
833
834 check_cartesian_pair2(X,XType,Y,YType,Res,WF) :- prop_pred_true(Res,MemResX),
835 membership_test_wf(XType,X,MemResX,WF),
836 ((var(MemResX), is_definitely_maximal_set(YType)) % TO DO: maybe actually also call membership_test_wf
837 -> Res=MemResX
838 ; check_cartesian_pair3(MemResX,Y,YType,Res,WF)).
839
840 :- block check_cartesian_pair3(-,?,?,?,?).
841 check_cartesian_pair3(pred_true,Y,YType,Res,WF) :- membership_test_wf(YType,Y,Res,WF).
842 check_cartesian_pair3(pred_false,_Y,_YType,pred_false,_WF).
843
844 :- block prop_pred_true(-,?).
845 prop_pred_true(pred_true,pred_true).
846 prop_pred_true(pred_false,_).
847
848
849
850
851
852 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:in_nat_range_test(int(9),int(10),int(12),pred_false))).
853 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:in_nat_range_test(int(11),int(10),int(12),pred_true))).
854 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:in_nat_range_test(int(22),int(22),int(22),pred_true))).
855 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:in_nat_range_test(int(22),int(22),int(21),pred_false))).
856 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:in_nat_range_test(int(9),int(10),int(12),pred_true))).
857 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:in_nat_range_test(int(22),int(22),int(22),pred_false))).
858 :- assert_must_succeed((in_nat_range_test(X,int(11),int(12),pred_false), X=int(10) )).
859 :- assert_must_succeed((kernel_equality:in_nat_range_test(X,int(11),int(12),pred_false), X=int(13) )).
860 :- assert_must_succeed((in_nat_range_test(X,int(11),int(12),pred_true), X=int(11) )).
861 :- assert_must_succeed((kernel_equality:in_nat_range_test(int(11),X,int(12),pred_true), X=int(11) )).
862 :- assert_must_succeed((in_nat_range_test(int(11),X,int(12),pred_false), X=int(12) )).
863 :- assert_must_succeed((kernel_equality:in_nat_range_test(int(11),int(10),int(12),R), R==pred_true )).
864 :- assert_must_fail((kernel_equality:in_nat_range_test(int(11),int(10),int(12),pred_false))).
865
866 in_nat_range_test(int(X),int(Y),int(Z),Res) :- in_nat_range_test1(X,Y,Z,Res).
867
868 in_nat_range_test1(X,Y,Z,Res) :- number(X),number(Y),number(Z),!,
869 % for improved performance, e.g., inside large set differences with intervals
870 ( X < Y -> Res = pred_false
871 ; X > Z -> Res = pred_false
872 ; Res = pred_true).
873 % this clause does not seem to add any power: (x:x..x <=> b=TRUE) already determines b=TRUE deterministically
874 %in_nat_range_test1(X,Y,Z,ResYZ) :- Y==Z, !, print(in_nat_eq_obj(X,Y,ResYZ)),nl,
875 % equality_objects(int(X),int(Y),ResYZ).
876 in_nat_range_test1(X,Y,Z,ResYZ) :-
877 prop_eq_01(ResYZ,R01),
878 % TO DO: check CHR + possibly X==Y or X==Z
879 clpfd_interface:try_post_constraint((X#>=Y #/\ X#=<Z) #<=> R01), % reify constraint if CLP(FD) active
880 %was : convert_eq_to_mem(RYZ,Res),
881 and_equality(RY,RZ,ResYZ),
882 geq_test(X,Y,RY),
883 geq_test(Z,X,RZ).
884
885 :- block geq_test(?,-,-),geq_test(-,?,-).
886 geq_test(X,Y,Res) :- % TO DO: use CHR ?
887 ( Res==pred_true -> kernel_objects:less_than_equal_direct(Y,X)
888 ; Res==pred_false -> kernel_objects:less_than_direct(X,Y)
889 ; X >= Y -> Res=pred_true
890 ; Res = pred_false
891 ).
892
893
894
895 /* SUBSET CHECK REIFICATION */
896
897 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_test([int(2)],[],pred_false,WF),WF)).
898 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_test([int(2),int(1)],[int(2)],pred_false,WF),WF)).
899 :- assert_must_succeed(exhaustive_kernel_fail_check_wfinit(kernel_equality:subset_test([int(2),int(1)],[int(2)],pred_true,WF),WF)).
900 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_test([int(2),int(1)],[int(2),int(1)],pred_true,WF),WF)).
901 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_test([int(2),int(1)],[int(2),int(1),int(3)],pred_true,WF),WF)).
902 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_test([int(2),int(1)],global_set('NATURAL1'),pred_true,WF),WF)).
903 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_test([],[int(2),int(1)],pred_true,WF),WF)).
904 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:subset_test([],[int(2),int(1)],pred_false,_WF))).
905 :- assert_must_succeed((kernel_equality:subset_test([],[int(3)],R,_WF),R==pred_true)).
906 :- assert_must_succeed((kernel_equality:subset_test([int(2),int(1)],[int(2),int(1),int(3)],R,_WF),R==pred_true)).
907 :- assert_must_succeed((kernel_equality:subset_test([int(2),int(1),int(4)],[int(2),int(1),int(3)],R,_WF),R==pred_false)).
908 :- assert_must_succeed((kernel_equality:subset_test([int(222),int(1)],global_set('NATURAL'),R,_WF),R==pred_true)).
909 :- assert_must_succeed((kernel_equality:subset_test([int(222),int(1)],global_set('NATURAL1'),R,_WF),R==pred_true)).
910 :- assert_must_succeed((kernel_equality:subset_test([int(222),int(1),int(0)],global_set('NATURAL1'),R,_WF),R==pred_false)).
911 :- assert_must_succeed((kernel_equality:subset_test([int(222),int(1),int(0)],X,R,_WF),X=global_set('NATURAL1'),R==pred_false)).
912 :- assert_must_succeed((kernel_equality:subset_test([int(222),int(-11)],global_set('INTEGER'),R,_WF),R==pred_true)).
913 :- assert_must_succeed((kernel_equality:subset_test([int(222),int(-11)],global_set('INTEGER'),R,_WF),R==pred_true)).
914 :- assert_must_succeed((kernel_equality:subset_test(global_set('INTEGER'),global_set('NATURAL1'),R,_WF),R==pred_false)).
915 :- assert_must_succeed((kernel_equality:subset_test(global_set('NATURAL1'),global_set('NATURAL1'),R,_WF),R==pred_true)).
916
917 :- use_module(kernel_objects,[check_subset_of_wf/3, not_subset_of_wf/3,
918 check_subset_of_global_sets/2, check_not_subset_of_global_sets/2,
919 both_global_sets/4]).
920
921 :- use_module(custom_explicit_sets,[expand_custom_set_to_list/4,
922 expand_custom_set_to_list_no_dups_wf/5, expand_custom_set_to_list_wf/5,
923 is_definitely_maximal_set/1]).
924 :- block subset_test(-,-,-,?).
925 subset_test(_S1,S2,R,_WF) :- % tools_printing:print_term_summary(subset_test(_S1,S2,R,WF)), %%
926 is_definitely_maximal_set(S2),!,R=pred_true.
927 ?subset_test(S1,S2,R,WF) :- subset_test0(S1,S2,R,WF).
928
929 :- block subset_test0(-,?,-,?).
930 subset_test0(S1,S2,R,WF) :- % tools_printing:print_term_summary(subset_test0(S1,S2,R,WF)), %%
931 nonvar(R),!,
932 ? (R==pred_true -> check_subset_of_wf(S1,S2,WF)
933 ; R==pred_false -> not_subset_of_wf(S1,S2,WF)
934 ; add_error_fail(subset_test0,'Illegal result value: ',R)).
935 subset_test0([],_,R,_WF) :- !,R=pred_true.
936 subset_test0(S1,S2,R,WF) :- subset_test1(S1,S2,R,WF).
937
938
939 :- use_module(covsrc(coverage_tools_annotations),['$NOT_COVERED'/1]).
940
941 :- block subset_test1(-,?,-,?),subset_test1(?,-,-,?).
942 subset_test1(S1,S2,R,WF) :- nonvar(R),!,
943 ? (R==pred_true -> check_subset_of_wf(S1,S2,WF) ; not_subset_of_wf(S1,S2,WF)).
944 subset_test1([],_,R,_WF) :- !,R=pred_true, '$NOT_COVERED'('cannot be covered'). /* cannot be covered; emtpy set treated above */
945 subset_test1(Set1,Set2,R,WF) :- both_global_sets(Set1,Set2,G1,G2),!, % also deals with two intervals
946 test_subset_of_global_sets_wf(G1,G2,R,WF).
947 subset_test1(_Set1,Set2,R,_WF) :-
948 is_definitely_maximal_set(Set2),!, % TO DO: avoid re-checking it if we have already checked it above in subset_test
949 R=pred_true.
950 subset_test1(Set1,Set2,R,WF) :- Set2==[],!, eq_empty_set_attr_wf(Set1,R,WF).
951 ?subset_test1(Set1,Set2,R,WF) :- test_subset_of_explicit_set(Set1,Set2,R,WF,Code),!,
952 call(Code).
953 subset_test1(Set1,Set2,R,WF) :-
954 expand_custom_set_to_list_no_dups_wf(Set1,ESet1,_,subset_test1,WF),
955 % no_dups relevant for test 2202 on SWI Prolog, where conjoin(pred_true,X,Y) -> propagation of X & Y are separate
956 subset_test2(ESet1,Set2,R,WF).
957
958 :- block subset_test2(-,?,?,?).
959 subset_test2([],_,R,_WF) :- !, R=pred_true.
960 subset_test2(Set1,Set2,R,WF) :- R==pred_true,!,
961 ? check_subset_of_wf(Set1,Set2,WF). % may more aggressively instantiate Set2
962 % not useful to have special case for pred_false which uses membership_test_wf also
963 subset_test2([H|T],Set2,R,WF) :- %print(subset_test2([H|T],Set2,R)),nl,
964 (T==[]
965 -> membership_test_wf(Set2,H,R,WF)
966 ; membership_test_wf(Set2,H,MemRes,WF),
967 subset_test3(MemRes,T,Set2,R,WF),
968 (var(MemRes) -> propagate_true(R,MemRes) ; true) % in case overall subset holds, then MemRes must be true
969 ).
970
971 :- block subset_test3(-,?,?,?,?).
972 subset_test3(pred_false,_T,_Set2,R,_WF) :- R=pred_false.
973 ?subset_test3(pred_true,T,Set2,R,WF) :- subset_test2(T,Set2,R,WF).
974
975 :- block propagate_true(-,?).
976 propagate_true(pred_true,X) :- !, X=pred_true.
977 propagate_true(_,_).
978
979 %:- block test_subset_of_global_sets(-,?,?), not_subset_of_global_sets(?,-,?).
980 test_subset_of_global_sets_wf(interval(Low1,Up1),interval(Low2,Up2),Res,WF) :- !,
981 test_interval_subset_wf(Low1,Up1,Low2,Up2,Res,WF).
982 test_subset_of_global_sets_wf(G1,G2,R,_) :- G1==G2,!,R=pred_true.
983 test_subset_of_global_sets_wf(G1,G2,R,_) :- %print(check_subset(G1,G2)),nl,
984 when((nonvar(R);(ground(G1),ground(G2))),test_subset_of_global_sets_aux(G1,G2,R)).
985 % TO DO: provide better reified version, especially for intervals with variables !
986 % e.g., 1..x <: NATURAL1 ==> R=pred_true, ...
987
988 test_subset_of_global_sets_aux(G1,G2,R) :- R==pred_true,!, check_subset_of_global_sets(G1,G2).
989 test_subset_of_global_sets_aux(G1,G2,R) :- R==pred_false,!, check_not_subset_of_global_sets(G1,G2).
990 test_subset_of_global_sets_aux(G1,G2,R) :-
991 (check_subset_of_global_sets(G1,G2) -> R=pred_true ; R=pred_false).
992
993
994 :- use_module(b_interpreter_check,[imply/3, conjoin/6]).
995 test_interval_subset_wf(Low1,Up1,Low2,Up2,Res,WF) :-
996 % print(test_interval_subset_wf(Low1,Up1,Low2,Up2,Res)),nl,
997 check_less_than_equal_inf(Low1,Up1,NonEmpty),
998 (NonEmpty==false -> Res=pred_true % if Low1..Up1 is empty it is a subset of anything
999 ; check_less_than_equal_inf(Low2,Low1,R1),
1000 (R1 == pred_false, NonEmpty==pred_true -> Res=pred_false
1001 ; check_less_than_equal_inf(Up1,Up2,R2),
1002 conjoin_test(R1,R2,R12,WF),
1003 imply(NonEmpty,R12,Res) % if Low1..Up1 is empty the bounds must be within Low2..Up2
1004 )
1005 ).
1006
1007 :- use_module(b_interpreter_check,[check_less_than_equal/3]).
1008 % reify: X<=Y, a version of check_less_than_equal that can deal with minus_inf and inf
1009 % assumption: minus_inf, inf are either there directly; a variable will never be instantiated to inf, minus_inf
1010 % does not treat inf_overflow
1011 check_less_than_equal_inf(Low1,_,Res) :- Low1==minus_inf,!,Res=pred_true.
1012 check_less_than_equal_inf(_,Low2,Res) :- Low2==inf,!,Res=pred_true.
1013 check_less_than_equal_inf(Low1,_,Res) :- Low1==inf,!,Res=pred_false.
1014 check_less_than_equal_inf(_,Low2,Res) :- Low2==minus_inf,!,Res=pred_false.
1015 check_less_than_equal_inf(X,Y,Res) :- check_less_than_equal(X,Y,Res).
1016
1017
1018 % ---------------------------- strict subset reification
1019
1020
1021 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_strict_test([int(2)],[],pred_false,WF),WF)).
1022 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_strict_test([int(2),int(1)],[int(2)],pred_false,WF),WF)).
1023 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:subset_strict_test([int(2),int(1)],[int(2)],pred_true,_WF))).
1024 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_strict_test([int(2),int(1)],[int(2),int(1)],pred_false,WF),WF)).
1025 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_strict_test([int(2),int(1)],[int(2),int(1),int(3)],pred_true,WF),WF)).
1026 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_strict_test([int(2),int(1)],global_set('NATURAL1'),pred_true,WF),WF)).
1027 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_strict_test([],[int(2),int(1)],pred_true,WF),WF)).
1028 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:subset_strict_test([],[int(2),int(1)],pred_false,_WF))).
1029 :- assert_must_succeed((kernel_equality:subset_strict_test([],[int(3)],R,_WF),R==pred_true)).
1030 :- assert_must_succeed((kernel_equality:subset_strict_test([int(2),int(1)],[int(2),int(1),int(3)],R,_WF),R==pred_true)).
1031 :- assert_must_succeed((kernel_equality:subset_strict_test([int(2),int(1),int(4)],[int(2),int(1),int(3)],R,_WF),R==pred_false)).
1032 :- assert_must_succeed((kernel_equality:subset_strict_test([int(222),int(1)],global_set('NATURAL'),R,_WF),R==pred_true)).
1033 :- assert_must_succeed((kernel_equality:subset_strict_test([int(222),int(1)],global_set('NATURAL1'),R,_WF),R==pred_true)).
1034 :- assert_must_succeed((kernel_equality:subset_strict_test([int(222),int(1),int(0)],global_set('NATURAL1'),R,_WF),R==pred_false)).
1035 :- assert_must_succeed((kernel_equality:subset_strict_test([int(222),int(1),int(0)],X,R,_WF),X=global_set('NATURAL1'),R==pred_false)).
1036 :- assert_must_succeed((kernel_equality:subset_strict_test([int(222),int(-11)],global_set('INTEGER'),R,_WF),R==pred_true)).
1037 :- assert_must_succeed((kernel_equality:subset_strict_test([int(222),int(-11)],global_set('INTEGER'),R,_WF),R==pred_true)).
1038 :- assert_must_succeed((kernel_equality:subset_strict_test(global_set('INTEGER'),global_set('NATURAL1'),R,_WF),R==pred_false)).
1039
1040 :- assert_must_succeed((kernel_equality:subset_strict_test(global_set('NATURAL1'),global_set('NATURAL1'),R,_WF),R==pred_false)).
1041
1042 :- block subset_strict_test(-,-,-,?).
1043 subset_strict_test(_S1,S2,R,_WF) :- % tools_printing:print_term_summary(subset_test(_S1,S2,R,WF)), %%
1044 S2==[],!,R=pred_false.
1045 subset_strict_test(S1,S2,R,WF) :- % tools_printing:print_term_summary(subset_test(_S1,S2,R,WF)), %%
1046 S1==[],!,eq_empty_set_attr_wf(S2,Empty,WF), bool_pred:negate(Empty,R).
1047 subset_strict_test(S1,S2,R,WF) :- subset_strict_test0(S1,S2,R,WF).
1048
1049 :- use_module(kernel_objects,[strict_subset_of_wf/3, not_strict_subset_of_wf/3]).
1050 :- block subset_strict_test0(-,?,-,?).
1051 subset_strict_test0(S1,S2,R,WF) :- % tools_printing:print_term_summary(subset_test0(S1,S2,R,WF)), %%
1052 nonvar(R),!,
1053 (R==pred_true -> strict_subset_of_wf(S1,S2,WF)
1054 ; R==pred_false -> not_strict_subset_of_wf(S1,S2,WF)
1055 ; add_error_fail(subset_strict_test0,'Illegal result value: ',R)).
1056 subset_strict_test0(S1,S2,R,WF) :-
1057 subset_test(S1,S2,IsSubset,WF),
1058 (IsSubset==pred_false -> R=pred_false
1059 ; conjoin_test(IsSubset,NotEqual,R,WF),
1060 bool_pred:negate(NotEqual,Equal),
1061 equality_objects_wf(S1,S2,Equal,WF)
1062 ).
1063
1064 conjoin_test(A,B,AB,WF) :-
1065 ? conjoin(A,B,AB,b(truth,pred,[conjoin_test]),b(truth,pred,[conjoin_test]),WF).
1066 % Note: predicate controls get_priority_of_boolean_expression
1067
1068 % ----------------------
1069
1070 % check if we can decidate equality by Prolog unification:
1071 % see predicate: can_be_used_for_unification in b_interpreter
1072 % one argument has to satisfy this predicate, the other should be ground (or also satisfy this predicate)
1073 equality_can_be_decided_by_unification(V) :- var(V),!,fail.
1074 equality_can_be_decided_by_unification(pred_false).
1075 equality_can_be_decided_by_unification(pred_true).
1076 equality_can_be_decided_by_unification(int(N)) :- integer(N).
1077 equality_can_be_decided_by_unification(string(S)) :- atom(S).
1078 equality_can_be_decided_by_unification(fd(N,GS)) :- atom(GS),integer(N).
1079 equality_can_be_decided_by_unification((A,B)) :-
1080 equality_can_be_decided_by_unification(A),equality_can_be_decided_by_unification(B).
1081 % TODO: records ?
1082