1 % (c) 2009-2023 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 safe_mul/3, safe_add/3, safe_pow2/2, % safe_pown/3,
40 empty_set_wf/2, not_empty_set_wf/2,
41 exhaustive_kernel_check/2, exhaustive_kernel_check/1,
42 exhaustive_kernel_check_wf/2, exhaustive_kernel_fail_check_wf/2,
43 exhaustive_kernel_check_wfdet/2, exhaustive_kernel_fail_check_wfinit/2,
44 exhaustive_kernel_fail_check/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 %:- 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
210 % equality_objects1 assumes first argument is nonvar:
211 %%equality_objects1(X,Y,R,_) :- print(equality_objects1(X,Y,R)),nl,fail. %%
212 equality_objects1(pred_true /* bool_true */,X,Res,_WF) :- !,
213 X=Res. % equivalent to bool_equality(pred_true /* bool_true */,X,Res).
214 equality_objects1(pred_false /* bool_false */,X,Res,_WF) :- !,
215 ? bool_pred:negate(X,Res). % equivalent to bool_equality(pred_false /* bool_false */,X,Res).
216 ?equality_objects1(int(X),IY,Res,_WF) :- !, IY=int(Y), equality_int(X,Y,Res).
217 equality_objects1(term(X),TY,Res,WF) :- !, TY=term(Y), eq_term_wf(X,Y,Res,WF).
218 equality_objects1(string(X),SY,Res,_WF) :- !, SY=string(Y), eq_atomic(X,Y,string,Res).
219 equality_objects1(fd(X,Type),FY,Res,_WF) :- !,
220 b_global_sets:get_global_type_value(FY,Type,Y),
221 ? equality_fd_objects(X,Y,Type,Res).
222 equality_objects1(freeval(Id,Case1,Value1),FY,Res,WF) :- !, FY=freeval(Id,Case2,Value2),
223 (kernel_freetypes:freetype_with_single_case(Id,Case)
224 -> (Case,Case)=(Case1,Case2), % cases must match
225 equality_objects_wf_no_enum(Value1,Value2,Res,WF)
226 ; and_equality(CaseRes,ValueRes,Res),
227 eq_atomic(Case1,Case2,freeval_case,CaseRes),
228 equality_freeval_content(CaseRes,Value1,Value2,ValueRes,WF)
229 ).
230 equality_objects1(rec(X),RY,Res,WF) :- !, RY=rec(Y), equality_fields(X,Y,Res,WF).
231 equality_objects1((X,Y),XY2,Res,WF) :- !, XY2=(X2,Y2),
232 equality_objects_wf_no_enum(X,X2,RX,WF),
233 and_equality(RY,RX,Res), % typically Res is var, hence it is better to call and_equality after X
234 (RX==pred_false -> true
235 ? ; equality_objects_wf_no_enum(Y,Y2,RY,WF)).
236 ?equality_objects1([],S,R,WF) :- !,eq_empty_set_wf(S,R,WF).
237 %equality_objects1(X,[],R,WF) :- !,eq_empty_set_wf(X,R,WF).
238 ?equality_objects1(X,Y,R,WF) :- equality_objects2(X,Y,R,WF).
239
240 :- block equality_freeval_content(-,?,?,?,?).
241 % if the case is different, we don't care anymore about the content; and the types could be different
242 equality_freeval_content(pred_false,_Value1,_Value2,_,_).
243 equality_freeval_content(pred_true,Value1,Value2,Res,WF) :-
244 % if we do not wait until we now that the case is the same,
245 % an internal type error might be raised
246 equality_objects_wf_no_enum(Value1,Value2,Res,WF).
247
248
249 :- use_module(error_manager,[add_warning/2]).
250
251 :- block equality_objects2(?,-,-,?). % also wait on second or third argument
252 equality_objects2(X,Y,Res,WF) :- nonvar(Res),!,% we know the result of the comparison
253 ( Res=pred_true -> %% print(forcing_equal(X,Y)),nl,%%
254 ? equal_object_wf(X,Y,equality_objects2_1,WF)
255 ; Res=pred_false -> not_equal_object_wf(X,Y,WF)
256 ; add_error_fail(equality_objects2,'Illegal result: ',equality_objects2(X,Y,Res,WF))
257 ).
258 ?equality_objects2([H|T],S,Res,WF) :- !,eq_cons(S,H,T,Res,WF). % move to equality_objects1 ?!
259 equality_objects2(avl_set(A),S,Res,WF) :-
260 (S=[H|T] -> !, eq_cons(avl_set(A),H,T,Res,WF)
261 ; S = [] -> !, (A=empty -> add_warning(equality_objects2,'Empty avl_set'), Res=pred_true
262 ; Res=pred_false)).
263 equality_objects2(ES1,ES2,Res,WF) :-
264 equality_explicit_sets_wf(ES1,ES2,ERes,WF), !,
265 Res=ERes.
266 equality_objects2(ES1,S,Res,WF) :- is_custom_explicit_set(ES1,eq_cons),!, % move to custom_explicit_sets?
267 % S = [] or ES1 = [] is already covered above
268 ? (S=[H|T] -> eq_cons(ES1,H,T,Res,WF) % maybe we can avoid expanding ES1
269 ? ; is_infinite_explicit_set(ES1),is_custom_explicit_set(S,eq_cons)
270 -> expand_custom_set_wf(S,ExpSet,equality_objects2,WF),
271 equality_objects0(ExpSet,ES1,Res,WF)
272 ; expand_custom_set_wf(ES1,ExpSet,equality_objects2,WF), equality_objects0(ExpSet,S,Res,WF)
273 ).
274 equality_objects2(X,Y,Res,WF) :-
275 add_internal_error('Unknown objects:',equality_objects2(X,Y,Res,WF)), % could happen with abort(.) terms ?
276 (equal_object_wf(X,Y,equality_objects2_2,WF),Res=pred_true
277 ;
278 not_equal_object_wf(X,Y,WF),Res=pred_false
279 ).
280
281 %:- use_module(b_global_sets,[b_get_fd_type_bounds/3]).
282 equality_fd_objects(X,Y,_,Res) :- number(X),number(Y),!,
283 (X=Y -> Res=pred_true ; Res= pred_false).
284 equality_fd_objects(X,Y,_,Res) :- % check for attached dif co-routines; later we should probably use CHR
285 fd_frozen_dif(X,Y),!,
286 % THIS DROPS THE PERFORMANCE OF probsli ../prob_examples/examples/B/ClearSy/alloc_large.mch -init -p TIME_OUT 5000
287 Res=pred_false.
288 % Is it really necessary to keep code below: clp(FD) will do this for us ?!
289 equality_fd_objects(X,Y,Type,Res) :-
290 nonvar(Type),b_global_sets:b_get_fd_type_bounds(Type,LowBnd,UpBnd),!,
291 (LowBnd=UpBnd
292 -> X=Y,Res=pred_true /* only one object of Type exists */
293 ; LB1 is LowBnd+1,
294 (LB1 = UpBnd
295 -> bin_eq_atomic(X,Y,Res,LowBnd,UpBnd) /* two objects exist */
296 ; eq_atomic_simple(X,Y,global(Type),Res),
297 (var(Res),(var(X);var(Y))
298 -> clpfd_in_domain(X,LowBnd,UpBnd), % just like X in LowBnd..UpBnd but can deal with UpBnd=inf
299 clpfd_in_domain(Y,LowBnd,UpBnd),
300 % still required ! even with fd_utils_clpfd ! (for v8 of Bosch CrCtl_Comb2_Final_mch.eventb)
301 equality_fd(X,Y,Res)
302 ; true
303 )
304 )
305 ).
306 equality_fd_objects(X,Y,Type,Res) :-
307 add_internal_error('Unknown type: ',equality_fd_objects(X,Y,Type,Res)),
308 eq_atomic_simple(X,Y,global(Type),Res).
309
310
311 % a reified version of equality
312 %equality_fd(X,Y,Res) :- X==Y,!, Res=pred_true. % not necessary; syntactic_equality_test below will trigger
313 equality_fd(X,Y,Res) :-
314 ((X#=Y) #<=> Reification01),
315 % (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
316 prop_eq_01(Res,Reification01),
317 (var(Reification01)
318 -> syntactic_equality_test(X,Y,Res)
319 ; true).
320
321
322 % propagate pred_false/true <-> 0/1
323 :- block prop_eq_01(-,-).
324 % prop_eq_01(A,B) :- print(prop(A,B)),nl,fail.
325 ?prop_eq_01(P,B) :- var(P), !, prop_01_eq(B,P).
326 prop_eq_01(pred_true,1).
327 prop_eq_01(pred_false,0).
328 prop_01_eq(1,pred_true).
329 prop_01_eq(0,pred_false).
330
331
332 :- use_module(kernel_non_empty_attr,[get_empty_set_attr/3]).
333 %eq_empty_set(Set,PredRes) :-
334 % var(Set), var(PredRes), clpfd_card_is_gt0_for_var(Set),!, PredRes=false.
335 %eq_empty_set(Set,Res) :- eq_empty_set_attr_wf(Set,Res,no_wf_available).
336
337 eq_empty_set_attr_wf(Set,PredRes,WF) :- var(PredRes), var(Set),!,
338 get_empty_set_attr(Set,PredRes,ExistsAlready), % get attribute or create one if it does not exist
339 (ExistsAlready=is_empty_attr_exists
340 -> true % no need to compute the predicate; another call will already do it
341 ; eq_empty_set_wf(Set,PredRes,WF)).
342 eq_empty_set_attr_wf(X,R,WF) :- eq_empty_set_wf(X,R,WF).
343
344 :- use_module(kernel_waitflags,[add_error_wf/5]).
345
346 :- block eq_empty_set_wf(-,-,?).
347 % TO DO: inspect kernel_cardinality attributes
348 eq_empty_set_wf(X,R,WF) :- var(X),!,
349 ? (R=pred_true -> empty_set_wf(X,WF) ; not_empty_set_wf(X,WF)).
350 eq_empty_set_wf([],R,_) :- !,R=pred_true.
351 eq_empty_set_wf([_|_],R,_) :- !,R=pred_false.
352 eq_empty_set_wf(CS,R,WF) :- is_custom_explicit_set(CS,eq_empty_set_wf),!,
353 test_empty_explicit_set_wf(CS,R,WF).
354 eq_empty_set_wf(S,R,WF) :-
355 (S==term(undefined)
356 -> add_error_wf(eq_empty_set_wf,'Accessing uninitialised set value','',unknown,WF)
357 ; add_internal_error('Illegal Set: ',eq_empty_set_wf(S,R,_))
358 ),fail.
359
360
361 %%eq_cons(S,H,T,Res,_) :- print(eq_cons(S,H,T,Res)),nl,fail.
362 eq_cons([],_,_,Res,_) :- !, Res=pred_false.
363 eq_cons([H2|T2],H1,T1,Res,WF) :- !, % T2==[] checked? TODO: call eq_singleton_set_cons
364 check_and_remove_wf([H2|T2],H1,NewSet2,RemoveSuccesful,WF),
365 %% print(removed(H1,H2,T2,NewSet2,RemoveSuccesful)), %%
366 ? eq_cons2(RemoveSuccesful,H1,T1,H2,T2,NewSet2,Res,WF).
367 eq_cons(avl_set(A),H1,T1,Res,WF) :- !,
368 ? eq_cons_avl_set(A,H1,T1,Res,WF).
369 eq_cons(global_set(G),_H,T,Res,WF) :- %print(chk(G,H,T)),nl,
370 ? is_infinite_global_set(G,_),!,
371 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
372 Res = pred_false.
373 eq_cons(ES,H1,T1,Res,WF) :- is_custom_explicit_set(ES,eq_cons),
374 expand_custom_set_wf(ES,ExpSet,eq_cons,WF),
375 ? eq_cons1(ExpSet,H1,T1,Res,WF).
376
377 % check if {H2} = {H1|T1}
378 eq_singleton_set_cons(H2,H1,T1,Res,WF) :- T1==[], !, equality_objects_wf_no_enum(H2,H1,Res,WF).
379 eq_singleton_set_cons(H2,H1,T1,Res,WF) :- empty_set_test_wf(T1,T1Empty,WF),
380 % TODO: we could also call equality_objects(H2,H1,H2H1Eq) if T1Empty is not known and conjoin it
381 ? eq_singleton2(H2,H1,T1Empty,Res,WF).
382
383 :- block eq_singleton2(?,?,-,-,?).
384 eq_singleton2(H2,H1,T1Empty,Res,WF) :- T1Empty==pred_true,!,
385 ? equality_objects_wf_no_enum(H2,H1,Res,WF).
386 eq_singleton2(_,_,T1Empty,Res,_) :- T1Empty==pred_false,!,
387 Res=pred_false. % if T1 is not empty, [H1|T1] is different from [H2]
388 eq_singleton2(H2,H1,T1Empty,Res,WF) :- Res==pred_true,!,T1Empty=pred_true,
389 equal_object_wf(H2,H1,eq_singleton2,WF).
390 eq_singleton2(H2,H1,T1Empty,Res,WF) :- Res==pred_false,!,
391 when(nonvar(T1Empty),eq_singleton2(H2,H1,T1Empty,Res,WF)).
392
393
394 % this treatment (second clause) is relevant for avoiding unnecessary choice points
395 % 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)
396 eq_cons_avl_set(A,H1,T1,Res,WF) :- is_one_element_avl(A,AEl),
397 !,
398 ? eq_singleton_set_cons(AEl,H1,T1,Res,WF).
399 eq_cons_avl_set(A,H1,T1,Res,WF) :-
400 (var(Res) -> kernel_tools:ground_value_check(H1,GrH1) ; true), % if Res already bound, no need to do ground check
401 ? block_eq_cons_avl_set(A,H1,T1,Res,GrH1,WF).
402 :- block block_eq_cons_avl_set(?,?,?,-,-,?).
403 block_eq_cons_avl_set(A,H1,T1,Res,_,WF) :- Res==pred_true,!,
404 kernel_objects:equal_custom_explicit_set_cons_wf(avl_set(A),H1,T1,WF).
405 block_eq_cons_avl_set(A,H1,T1,Res,_,WF) :-
406 element_can_be_added_or_removed_to_avl(H1),!, % should hopefully be true as H1 is now ground
407 (remove_element_from_explicit_set(avl_set(A),H1,RA)
408 ? -> equality_objects_with_expansion(T1,RA,Res,WF) %%% PROBLEM: T1 has to be in list form !
409 ; Res = pred_false
410 ).
411 block_eq_cons_avl_set(A,H1,T1,Res,_,WF) :-
412 % 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
413 expand_custom_set_wf(avl_set(A),ExpSet,block_eq_cons_avl_set,WF),
414 eq_cons1(ExpSet,H1,T1,Res,WF).
415
416 :- block eq_cons1(-,?,?,?,?).
417 ?eq_cons1(ExpSet,H1,T1,Res,WF) :- eq_cons(ExpSet,H1,T1,Res,WF).
418
419 :- block eq_cons2(-, ?,?,?,?, ?,-,?).
420 eq_cons2(RemoveSuccesful, H1,T1,H2,T2, _NewSet2,Res,WF) :- var(RemoveSuccesful),!,
421 % result has been instantiated before Remove finished; now force equal_object or not_equal_object
422 % note: without this the remove could be pending (see test 1112, 1105)
423 % TO DO: look whether we could force remove and continue from there ?
424 ? equality_objects2([H1|T1],[H2|T2],Res,WF).
425 eq_cons2(not_successful, _,_T1,_,_, _NewSet2,pred_false,_).
426 ?eq_cons2(successful, _, T1,_,_, NewSet2,Res,WF) :- equality_objects_wf_no_enum(T1,NewSet2,Res,WF).
427
428
429 check_and_remove(Set,ElementToRemove,ResultingSet,Res) :-
430 check_and_remove_wf(Set,ElementToRemove,ResultingSet,Res,no_wf_available).
431
432 :- block check_and_remove_wf(-,?,?,?,?).
433 check_and_remove_wf([],_,ResultingSet,Res,_) :- !, ResultingSet=[],Res=not_successful.
434 check_and_remove_wf([H|T],ElementToRemove,ResultingSet,Res,WF) :- !,
435 equality_objects_wf_no_enum(H,ElementToRemove,RH,WF),
436 %%print(equality_objects_result(H,ElementToRemove,RH)),nl,
437 ? check_and_remove2(RH,H,T,ElementToRemove,ResultingSet,Res,WF).
438 check_and_remove_wf(CS,ElementToRemove,ResultingSet,Res,WF) :-
439 expand_custom_set_to_list_wf(CS,ESet,_,check_and_remove,WF),
440 check_and_remove_wf(ESet,ElementToRemove,ResultingSet,Res,WF).
441
442 :- block check_and_remove2(-,?,?,?,?,?,?).
443 check_and_remove2(pred_true, _H,T,_ElementToRemove,T,successful,_).
444 check_and_remove2(pred_false,H,T,ElementToRemove,[H|RT],Res,WF) :-
445 ? check_and_remove_wf(T,ElementToRemove,RT,Res,WF).
446
447
448 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:and_equality(pred_false,pred_false,pred_false))).
449 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:and_equality(pred_true,pred_false,pred_false))).
450 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:and_equality(pred_true,pred_true,pred_true))).
451 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_true,pred_true,pred_false))).
452 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_true,pred_false,pred_true))).
453 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_false,pred_true,pred_true))).
454 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_false,pred_false,pred_true))).
455 :- block and_equality(-,-,-).
456 and_equality(X,Y,Res) :-
457 ( X==pred_true -> Res=Y
458 ; X==pred_false -> Res=pred_false
459 ; Y==pred_true -> Res=X
460 ; Y==pred_false -> Res=pred_false
461 ; Res==pred_true -> X=pred_true, Y=pred_true
462 ; 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
463 ; add_error_fail(and_equality,'Illegal call: ',and_equality(X,Y,Res))
464 ).
465 :- block and_equality2(-,-,?).
466 and_equality2(X,Y,Res) :-
467 ( X==pred_true -> Res=Y
468 ; X==pred_false -> Res=pred_false
469 ; Y==pred_true -> Res=X
470 ; Y==pred_false -> Res=pred_false
471 ; add_error_fail(and_equality,'Illegal call: ',and_equality2(X,Y,Res))
472 ).
473
474 /*
475 :- block bool_eq_atomic(-,?,?,-).
476 bool_eq_atomic(X,Y,OtherY,Res) :- nonvar(Res),!,
477 (Res=pred_true -> X=Y ; X=OtherY).
478 bool_eq_atomic(X,Y,_,Res) :- X==Y -> Res=pred_true ; Res=pred_false. */
479
480 % a version for base types with just two possible values
481 :- block bin_eq_atomic(-,?,-,?,?), bin_eq_atomic(?,-,-,?,?).
482 % no need to check for frozen_dif: a dif would instantly trigger instantiation to other value
483 % However, we could use when(?=(X,Y) ; nonvar(Res) as trigger ! maybe this would slowdown SATLIB tests ??
484 bin_eq_atomic(X,Y,Res,V1,V2) :- nonvar(Res),!,
485 %print(forcing_bin_eq_atomic(X,Y,Res,V1,V2)),nl,
486 (Res=pred_true -> X=Y
487 ; %print(bin_dif(X,Y)),nl,
488 (X=V1,Y=V2 ; X=V2,Y=V1)
489 ). % difference with eq_atomic: we now know the value !
490 bin_eq_atomic(X,Y,Res,_,_) :-
491 %print(triggering_bin_eq(X,Y,Res)), translate:print_frozen_info(Res),nl,
492 (X==Y -> Res=pred_true ; Res=pred_false).
493
494 eq_atomic(X,Y,_Type,Res) :- nonvar(X),nonvar(Y),!,
495 (X=Y -> Res=pred_true ; Res=pred_false).
496 eq_atomic(X,Y,_,Res) :- % check for attached dif co-routines; later we should probably use CHR
497 ? frozen_dif(X,Y),!, Res=pred_false.
498 eq_atomic(X,Y,Type,Res) :- when((?=(X,Y);nonvar(Res)),eq_atomic2(X,Y,Type,Res)).
499
500 % version of eq_atomic without frozen_dif check (if already performed)
501 % eq_atomic_simple(X,Y,_Type,Res) :- % in all calling contexts this test is already performed
502 % nonvar(X),nonvar(Y),!, (X=Y -> Res=pred_true ; Res=pred_false).
503 eq_atomic_simple(X,Y,Type,Res) :- when((?=(X,Y);nonvar(Res)),eq_atomic2(X,Y,Type,Res)).
504
505 /*
506 Comment: % for integers CLPFD reification will not ground Res if X==Y, need to do when((?=(X,Y)...
507 | ?- X in 1..10, Y in 1..10, (X#=Y #<=> Z), X=Y.
508 Y = X,
509 X in 1..10,
510 Z in 0..1 ? */
511
512 eq_atomic2(X,Y,Type,Res) :- nonvar(Res),!,
513 ? (Res=pred_true -> X=Y ; dif(Type,X,Y)).
514 eq_atomic2(X,Y,_Type,Res) :-
515 (X=Y -> Res=pred_true
516 ; Res=pred_false).
517
518 :- block eq_term_wf(-,-,?,?).
519 eq_term_wf(TX,TY,Res,_WF) :- nonvar(TX),TX = floating(FX),!,
520 TY=floating(FY), eq_atomic(FX,FY,real,Res). % TODO: use a proper equality check for reals/floats
521 eq_term_wf(TY,TX,Res,_WF) :- nonvar(TX),TX = floating(FX),!,
522 TY=floating(FY), eq_atomic(FX,FY,real,Res).
523 eq_term_wf(TX,TY,Res,_) :- eq_atomic(TX,TY,term,Res).
524
525 :- use_module(fd_utils_clpfd,[neq_fd/3]).
526 dif(boolean,A,B) :- !,
527 bool_pred:negate(A,B). % was: bool_dif(A,B).
528 % usually not covered: equality_objects_with_type calls bool_equality,
529 % equality_objects waits for either arg to be fully instantiated to pred_false or pred_true
530 dif(integer,A,B) :- !, integer_dif(A,B).
531 ?dif(global(T),A,B) :- !, neq_fd(A,B,T).
532 dif(_,A,B) :- dif(A,B).
533
534 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:integer_dif(0,1))).
535 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:integer_dif(1,1))).
536 :- use_module(clpfd_interface,[clpfd_neq/2]).
537 integer_dif(A,B) :- clpfd_neq(A,B). % clpfd_neq calls dif on overflow
538
539
540 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:bool_dif(pred_false,pred_true))).
541 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:bool_dif(pred_true,pred_false))).
542 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:bool_dif(pred_true,pred_true))).
543 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:bool_dif(pred_false,pred_false))).
544 bool_dif(A,B) :- bool_pred:negate(A,B).
545
546 /* old version:
547 :- block eq_atomic(-,?,-), eq_atomic(?,-,-).
548 eq_atomic(X,Y,Res) :- nonvar(Res),!,
549 (Res=pred_true -> X=Y ; dif(X,Y)).
550 eq_atomic(X,Y,Res) :- X==Y -> Res=pred_true
551 ; Res=pred_false.
552 */
553
554 :- use_module(kernel_records,[check_field_name_compatibility/3]).
555 :- block equality_fields(-,?,-,?), equality_fields(?,-,-,?), equality_fields(-,-,?,?).
556 % if last argument is known we should propagate the field names from one record to another; see test 1289 (Hansen12)
557 equality_fields([],[],pred_true,_).
558 equality_fields([field(Name1,V1)|T1],[field(Name2,V2)|T2],Res,WF) :-
559 % should we wait for Name1 or Name2 to become nonvar?
560 ? check_field_name_compatibility(Name1,Name2,equality_fields),
561 and_equality(RH,RT,Res),
562 equality_objects_wf_no_enum(V1,V2,RH,WF),
563 (RH==pred_false -> true
564 ? ; equality_fields(T1,T2,RT,WF)).
565
566
567
568 empty_set_test_wf(Set,EqRes,WF) :- eq_empty_set_attr_wf(Set,EqRes,WF).
569 empty_set_test(Set,EqRes) :- eq_empty_set_attr_wf(Set,EqRes,no_wf_available).
570 empty_cartesian_product_wf(Set1,Set2,EqRes,WF) :- % TO DO: pass WF
571 eq_empty_set_wf(Set1,EqRes1,WF),
572 (EqRes1==pred_true -> EqRes=pred_true /* avoid inspecting Set2 */
573 ; or_eq_obj(EqRes1,EqRes2,EqRes),
574 eq_empty_set_wf(Set2,EqRes2,WF)).
575
576
577 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:or_eq_obj(pred_false,pred_false,pred_false))).
578 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:or_eq_obj(pred_false,pred_true,pred_true))).
579 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:or_eq_obj(pred_true,pred_true,pred_true))).
580 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_true,pred_true,pred_false))).
581 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_true,pred_false,pred_false))).
582 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_false,pred_true,pred_false))).
583 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_false,pred_false,pred_true))).
584 :- block or_eq_obj(-,-,-).
585 % very similar to disjoin in b_interpreter_check; no waitflag to instantiate if result false
586 or_eq_obj(X,Y,XorY) :-
587 ( (X==pred_true ; Y==pred_true) -> XorY=pred_true
588 ; XorY==pred_false -> X=pred_false,Y=pred_false
589 ; X==pred_false -> XorY = Y
590 ; Y==pred_false -> XorY = X
591 ; XorY==pred_true -> or_eq_obj2(X,Y)
592 ; add_internal_error('Illegal call: ',or_eq_obj(X,Y,XorY)) ).
593 :- block or_eq_obj2(-,-).
594 or_eq_obj2(X,Y) :- ((X==pred_true; Y=pred_true) -> true
595 ; X==pred_false -> Y=pred_true
596 ; Y==pred_false -> X=pred_true
597 ; add_internal_error('Illegal call: ',or_eq_obj2(X,Y))).
598
599 % ------------------------------------------------------------------
600
601
602 % not used at the moment:
603 %get_partial_subset_priority(Set,WF,LWF) :- get_partial_set_size(Set,Size),
604 % safe_pow2(Size,Prio),
605 % get_wait_flag(Prio,psubset(Set),WF,LWF).
606 %get_partial_set_priority(Set,WF,LWF) :- get_partial_set_size(Set,Size),
607 % get_wait_flag(Size,pset(Set),WF,LWF).
608 %get_partial_set_size(X,R) :- var(X),!,R=3.
609 %get_partial_set_size([],R) :- !,R=0.
610 %get_partial_set_size([_|T],R) :- !,get_partial_set_size(T,RT), R is RT+1.
611 %get_partial_set_size(_,10).
612
613
614 get_cardinality_wait_flag(Set,Info,WF,LWF) :-
615 ? get_cardinality_wait_flag(Set,Info,WF,_Card,LWF).
616 get_cardinality_wait_flag(Set,Info,WF,Card,LWF) :-
617 cardinality_as_int_for_wf(Set,Card),
618 % when(nonvar(X), (print(get_card_waitflag(X,Set,WF,LWF)),nl)),
619 (var(Card)
620 -> kernel_waitflags:get_last_wait_flag(get_cardinality_wait_flag(Info),WF,LastWF)
621 ; true), % ensure that we trigger choice points waiting on LWF before infinite enumeration starts
622 ? get_cardinality_wait_flag2(Card,Info,WF,LastWF,LWF).
623 :- block get_cardinality_wait_flag2(-,?,?,-,?).
624 get_cardinality_wait_flag2(X,_Info,_WF,LastWF,LWF) :- var(X),!,LWF=LastWF.
625 ?get_cardinality_wait_flag2(X,Info,WF,_,LWF) :- get_bounded_wait_flag(X,Info,WF,LWF).
626
627 get_cardinality_powset_wait_flag(Set,Info,WF,CardSet,LWF) :-
628 cardinality_as_int_for_wf(Set,CardSet),
629 get_cardinality_powset_wait_flag2(CardSet,Info,WF,LWF).
630 :- block get_cardinality_powset_wait_flag2(-,?,?,?).
631 get_cardinality_powset_wait_flag2(X,Info,WF,LWF) :-
632 priority_pow2(X,X2),
633 %safe_mul(X2,10000,X3), % as generating subsets this way will generate repetitions
634 %print(powset_waitflag(X,X2)),nl,
635 (X2=inf
636 ? -> integer_pow2_priority(R), get_wait_flag(R,powset_card(Info),WF,LWF)
637 ? ; get_bounded_wait_flag(X2,powset_card(Info),WF,LWF) % finite prio; ensure we do not exceed infinite prios if X2 very large
638 ).
639
640 priority_pow2(X,R) :- X==inf,!, R=inf. %R=10000010. % TO DO: provide a separate module for combining priorities in a systematic way !
641 priority_pow2(X,R) :- safe_pow2(X,R).
642
643 % CARDINALITY FOR NUMBER OF PARTIAL FUNCTIONS: (not used at the moment)
644 %get_cardinality_partial_function_wait_flag(DomSet,RanSet,Info,WF,CardDomSet,CardRanSet,LWF) :-
645 % cardinality_as_int_for_wf(DomSet,CardDomSet),
646 % cardinality_as_int_for_wf(RanSet,CardRanSet),
647 % get_cardinality_partial_function_wait_flag(CardDomSet,CardRanSet,Info,WF,LWF).
648 %:- block get_cardinality_partial_function_wait_flag(-,?,?,?,?),
649 % get_cardinality_partial_function_wait_flag(?,-,?,?,?).
650 %get_cardinality_partial_function_wait_flag(DC,RC,Info,WF,LWF) :-
651 % priority_pow1n(RC,DC,PFCARD), print(prio(PFCARD)),nl,
652 % get_bounded_wait_flag(PFCARD,powset_card(Info),WF,LWF).
653 % % Cardinality of the set of partial functions : (card(Range)+1)^card(Domain)
654 %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 !
655 %priority_pow1n(X,Y,RR) :- X1 is X+1, safe_pown(X1,Y,R),
656 % (R==inf -> integer_pow2_priority(RR) %RR=10000010
657 % ; RR=R).
658
659 % CARDINALITY FOR NUMBER OF RELATIONS:
660 get_cardinality_relation_over_wait_flag(Dom,Ran,WF,LWF,MaxCardOfRel,MaxNrOfRels) :-
661 cardinality_as_int_for_wf(Dom,X),
662 cardinality_as_int_for_wf(Ran,Y),
663 get_cardinality_relation_over_wait_flag2(X,Y,WF,LWF,MaxCardOfRel,MaxNrOfRels).
664
665 :- block get_cardinality_relation_over_wait_flag2(-,?,?,?,?,?), get_cardinality_relation_over_wait_flag2(?,-,?,?,?,?).
666 get_cardinality_relation_over_wait_flag2(X,Y,WF,LWF,MaxCardOfRel,MaxNrOfRels1) :-
667 safe_mul(X,Y,MaxCardOfRel),
668 safe_pow2(MaxCardOfRel,MaxNrOfRels),
669 safe_add(MaxNrOfRels,1,MaxNrOfRels1), /* add 1 to give priority to tighter_enum */
670 ? get_bounded_wait_flag(MaxNrOfRels1,powset_rel_card,WF,LWF).
671
672 % ------------------------------------------------------------------
673
674 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(2),pred_true,WF),WF)).
675 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(1),pred_true,WF),WF)).
676 :- 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)).
677 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(3),pred_false,WF),WF)).
678 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([],int(3),pred_false,WF),WF)).
679 :- assert_must_succeed(exhaustive_kernel_fail_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(3),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(1),int(4)],pred_true,WF),WF)).
681 :- 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)).
682 :- 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)).
683 :- assert_must_succeed((membership_test_wf([int(2),int(1)],int(2),R,_WF),R==pred_true)).
684 :- assert_must_succeed((membership_test_wf([int(2),int(1)],int(X),R,_WF),var(R),X=1,R==pred_true)).
685 :- assert_must_succeed((membership_test_wf([int(2),int(1)],int(3),R,_WF),R==pred_false)).
686 :- assert_must_succeed((membership_test_wf(global_set('Name'),fd(1,'Name'),R,_WF),R==pred_true)).
687
688 :- 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)),
689 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)).
690 :- assert_must_succeed((
691 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))])],
692 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
693 )).
694 /* membership_test_wf: A function that instantiates last argument when membership test can be decided */
695
696
697 % a version which also creates a choice point in SMT mode
698 membership_test_wf_with_force(Set,X,Res,WF) :-
699 membership_test_wf(Set,X,Res,outer,WF),
700 enum_equality_result_smt_mode_wf(Res,membership_test_wf,WF).
701 :- block force_equality_result(-,-).
702 force_equality_result(pred_true,_).
703 force_equality_result(pred_false,_).
704
705 enum_equality_result_smt_mode_wf(Res,PP,WF) :- var(Res),
706 preferences:preference(use_smt_mode,true),!,
707 enum_equality_result_wf(Res,PP,WF).
708 enum_equality_result_smt_mode_wf(_,_,_).
709
710 enum_equality_result_wf(Res,PP,WF) :-
711 get_last_wait_flag(PP,WF,LWF),
712 force_equality_result(Res,LWF).
713
714 ?membership_test_wf(Set,X,Res,WF) :- membership_test_wf(Set,X,Res,outer,WF).
715
716 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
717 :- if(environ(prob_data_validation_mode,true)).
718 :- block membership_test_wf(-,?,?,?,?). % avoid instantiating Set
719 :- else.
720 :- block membership_test_wf(-,?,-,?,?).
721 :- endif.
722 membership_test_wf(Set,X,Res,_OuterInner,WF) :- nonvar(Res),!,
723 (Res==pred_true
724 ? -> call_check_element_of_wf0(X,Set,WF)
725 /* (kernel_objects:unbound_variable_for_cons(Set)
726 -> kernel_objects:mark_as_non_free(X), % attach co-routine to indicate that we cannot freely chose X
727 print(instantiate_set(Set,X,Res)),nl,
728 Set=[X|_] % TO DO: normalise X first ?
729 ; when(nonvar(Set), membership_test_wf2(Set,X,Res,OuterInner,WF))
730 ) */
731 ; membership_not_el(Set,X,WF)).
732 membership_test_wf(Set,X,Res,OuterInner,WF) :-
733 ? membership_test_wf2(Set,X,Res,OuterInner,WF).
734
735 % we are not sure if WF0 is set; go via kernel_mappings:
736 ?call_check_element_of_wf0(X,Set,WF) :- get_wait_flag0(WF,WF0),
737 ? kernel_mappings:check_element_of_wf0(X,Set,WF,WF0,unknown).
738
739
740 :- block membership_not_el(-,?,?).
741 membership_not_el([],_,_WF) :- !.
742 membership_not_el([H|T],X,WF) :- !,
743 ? not_equal_object_wf(H,X,WF),
744 membership_not_el(T,X,WF).
745 membership_not_el(avl_set(A),X,WF) :- !,membership_custom_set_wf(avl_set(A),X,pred_false,WF).
746 membership_not_el(CS,X,WF) :- is_custom_explicit_set_nonvar(CS),!,
747 membership_custom_set_wf(CS,X,pred_false,WF).
748
749 membership_test_wf2([],_X,Res,_,_WF) :- !, Res=pred_false.
750 membership_test_wf2([H|T],X,Res,OuterInner,WF) :- !,
751 (Res==pred_false
752 -> not_equal_object_wf(H,X,WF), membership_test_wf(T,X,Res,WF)
753 ? ; T==[] -> equality_objects_wf_no_enum(H,X,Res,WF)
754 % TO DO: at the outer level we could check whether the list has the same length as the type of X
755 ; OuterInner=outer, is_definitely_maximal_set([H|T]) -> Res=pred_true
756 ; (OuterInner=outer, % avoid re-checking ground_list_with_fd over and over again
757 preferences:preference(use_clpfd_solver,true),
758 ground_list_with_fd([H|T]),
759 construct_avl_from_lists_wf([H|T],CS,WF))
760 % 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
761 % TO DO: call clpfd_reify_inlist directly ? avoid translating to AVL and back to list; detect maximal list
762 ? -> membership_custom_set_wf(CS,X,Res,WF) %, print(conv_to_avl(X,[H|T],CS,Res)),nl
763 ; %print(eq(Res,H,X,T,WF)),nl,equality_objects_wf_dbg(H,X,HXRes,WF), % makes test 1003 : plavis-MemoryLoad_SP_55 fail
764 ? equality_objects_wf_no_enum(H,X,HXRes,WF),cons_el_of(HXRes,T,X,Res,WF)
765 % ,(var(HXRes) -> print(mem(X,[H|T],Res)), tools_printing:print_arg(X),nl ; true)
766 ).
767 ?membership_test_wf2(avl_set(A),X,Res,_,WF) :- !, membership_avl_set_wf(A,X,Res,WF).
768 membership_test_wf2(CS,X,Res,_,WF) :- is_custom_explicit_set(CS,membership_test_wf),!,
769 ? membership_custom_set_wf(CS,X,Res,WF).
770 membership_test_wf2(term(Z),_,_,_,_WF) :- Z==undefined,!,
771 add_error_fail(membership_test_wf,'Encountered uninitialised set variable', ''). % we will normally generate other error messages as well
772 membership_test_wf2(Z,X,Res,OuterInner,WF) :-
773 add_error_fail(membership_test_wf,'Not Set as first argument: ', membership_test_wf(Z,X,Res,OuterInner,WF)).
774
775 % detect certain lists containing FD values and convert them to avl sets: they have improved reification and can detect when a list is complete
776 ground_list_with_fd(V) :- var(V),!,fail.
777 ground_list_with_fd([H|T]) :- nonvar(H),ground_val(H),ground_list_with_fd(T).
778 ground_list_with_fd([]).
779
780 :- use_module(kernel_tools,[ground_value/1]).
781 ground_val(int(X)) :- number(X).
782 ground_val(pred_false).
783 ground_val(pred_true).
784 ground_val(fd(X,T)) :- number(X),ground(T).
785 ground_val((A,B)) :- nonvar(A),ground_val(A),ground_value(B).
786 ground_val(rec(Fields)) :- nonvar(Fields), Fields = [field(Name,V)|TFields], ground(Name),
787 ground_val(V),
788 ground_value(rec(TFields)).
789 % TO DO: add more checks; do we need this check ? related to is_avl_fd_index_set
790
791 :- block cons_el_of(-,?,?,-,?).
792 cons_el_of(HX_EQRES,T,X,MEMRES,WF) :- var(HX_EQRES),!, %print(cons_el_of(HX_EQRES,T,X,MEMRES)),nl,
793 (MEMRES=pred_false -> HX_EQRES=pred_false, /* otherwise element of set */
794 ? membership_not_el(T,X,WF)
795 % MEMRES must be pred_true
796 ; (T==[] -> %print(forcing_cons_el_of(T,X,MEMRES)),nl,
797 HX_EQRES=pred_true
798 ; cons_el_of_mem_obj(HX_EQRES,T,X,WF)) /* we have to wait for result of comparison with X */
799 ).
800 cons_el_of(pred_true,_,_,pred_true,_WF).
801 cons_el_of(pred_false,T,X,Res,WF) :-
802 (Res==pred_true -> non_empty_chk(T) ; true),
803 ? membership_test_wf(T,X,Res,inner,WF).
804
805 non_empty_chk(V) :- var(V),!,V=[_|_].
806 non_empty_chk(X) :- X \= []. % could be avl_set or closure
807
808 :- block cons_el_of_mem_obj(-,?,?,?).
809 cons_el_of_mem_obj(pred_true,_,_,_WF).
810 cons_el_of_mem_obj(pred_false,T,X,WF) :-
811 % Instantiation of T will be done by membership_test_wf, relevant for test 1273
812 ? membership_test_wf(T,X,pred_true,inner,WF).
813
814
815 :- assert_must_succeed((kernel_equality:cartesian_pair_test_wf((int(1),int(1)),
816 [int(1),int(2)],[int(2),int(3)],R,_WF),R==pred_false)).
817 :- assert_must_succeed((kernel_equality:cartesian_pair_test_wf((int(3),int(1)),
818 [int(1),int(2)],[int(2),int(3)],R,_WF),R==pred_false)).
819 :- assert_must_succeed((kernel_equality:cartesian_pair_test_wf((int(2),int(3)),
820 [int(1),int(2)],[int(2),int(3)],R,_WF),R==pred_true)).
821 :- assert_must_fail((kernel_equality:cartesian_pair_test_wf((int(1),int(3)),
822 [int(1),int(2)],[int(2),int(3)],pred_false,_WF))).
823
824 cartesian_pair_test_wf((X,Y),XType,YType,Res,WF) :- check_cartesian_pair1(X,XType,Y,YType,Res,WF).
825
826 :- block check_cartesian_pair1(-,?,-,?,-,?).
827 %check_cartesian_pair1(X,XType,Y,YType,Res) :- Res==pred_true,!,
828 % is_cartesian_pair_wf((X,Y),XType,YType,WF).
829 %check_cartesian_pair1(X,XType,Y,YType,Res) :- Res==pred_false,!,
830 % not_is_cartesian_pair((X,Y),XType,YType,WF).
831 check_cartesian_pair1(X,XType,Y,YType,Res,WF) :-
832 ((var(X),nonvar(Y)) -> check_cartesian_pair2(Y,YType,X,XType,Res,WF)
833 ; check_cartesian_pair2(X,XType,Y,YType,Res,WF)).
834
835 check_cartesian_pair2(X,XType,Y,YType,Res,WF) :- prop_pred_true(Res,MemResX),
836 membership_test_wf(XType,X,MemResX,WF),
837 ((var(MemResX), is_definitely_maximal_set(YType)) % TO DO: maybe actually also call membership_test_wf
838 -> Res=MemResX
839 ; check_cartesian_pair3(MemResX,Y,YType,Res,WF)).
840
841 :- block check_cartesian_pair3(-,?,?,?,?).
842 check_cartesian_pair3(pred_true,Y,YType,Res,WF) :- membership_test_wf(YType,Y,Res,WF).
843 check_cartesian_pair3(pred_false,_Y,_YType,pred_false,_WF).
844
845 :- block prop_pred_true(-,?).
846 prop_pred_true(pred_true,pred_true).
847 prop_pred_true(pred_false,_).
848
849
850
851
852
853 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:in_nat_range_test(int(9),int(10),int(12),pred_false))).
854 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:in_nat_range_test(int(11),int(10),int(12),pred_true))).
855 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:in_nat_range_test(int(22),int(22),int(22),pred_true))).
856 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:in_nat_range_test(int(22),int(22),int(21),pred_false))).
857 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:in_nat_range_test(int(9),int(10),int(12),pred_true))).
858 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:in_nat_range_test(int(22),int(22),int(22),pred_false))).
859 :- assert_must_succeed((in_nat_range_test(X,int(11),int(12),pred_false), X=int(10) )).
860 :- assert_must_succeed((kernel_equality:in_nat_range_test(X,int(11),int(12),pred_false), X=int(13) )).
861 :- assert_must_succeed((in_nat_range_test(X,int(11),int(12),pred_true), X=int(11) )).
862 :- assert_must_succeed((kernel_equality:in_nat_range_test(int(11),X,int(12),pred_true), X=int(11) )).
863 :- assert_must_succeed((in_nat_range_test(int(11),X,int(12),pred_false), X=int(12) )).
864 :- assert_must_succeed((kernel_equality:in_nat_range_test(int(11),int(10),int(12),R), R==pred_true )).
865 :- assert_must_fail((kernel_equality:in_nat_range_test(int(11),int(10),int(12),pred_false))).
866
867 in_nat_range_test(int(X),int(Y),int(Z),Res) :- in_nat_range_test1(X,Y,Z,Res).
868
869 in_nat_range_test1(X,Y,Z,Res) :- number(X),number(Y),number(Z),!,
870 % for improved performance, e.g., inside large set differences with intervals
871 ( X < Y -> Res = pred_false
872 ; X > Z -> Res = pred_false
873 ; Res = pred_true).
874 % this clause does not seem to add any power: (x:x..x <=> b=TRUE) already determines b=TRUE deterministically
875 %in_nat_range_test1(X,Y,Z,ResYZ) :- Y==Z, !, print(in_nat_eq_obj(X,Y,ResYZ)),nl,
876 % equality_objects(int(X),int(Y),ResYZ).
877 in_nat_range_test1(X,Y,Z,ResYZ) :-
878 prop_eq_01(ResYZ,R01),
879 % TO DO: check CHR + possibly X==Y or X==Z
880 clpfd_interface:try_post_constraint((X#>=Y #/\ X#=<Z) #<=> R01), % reify constraint if CLP(FD) active
881 %was : convert_eq_to_mem(RYZ,Res),
882 and_equality(RY,RZ,ResYZ),
883 geq_test(X,Y,RY),
884 geq_test(Z,X,RZ).
885
886 :- block geq_test(?,-,-),geq_test(-,?,-).
887 geq_test(X,Y,Res) :- % TO DO: use CHR ?
888 ( Res==pred_true -> kernel_objects:less_than_equal_direct(Y,X)
889 ; Res==pred_false -> kernel_objects:less_than_direct(X,Y)
890 ; X >= Y -> Res=pred_true
891 ; Res = pred_false
892 ).
893
894
895
896 /* SUBSET CHECK REIFICATION */
897
898 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_test([int(2)],[],pred_false,WF),WF)).
899 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_test([int(2),int(1)],[int(2)],pred_false,WF),WF)).
900 :- assert_must_succeed(exhaustive_kernel_fail_check_wfinit(kernel_equality:subset_test([int(2),int(1)],[int(2)],pred_true,WF),WF)).
901 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_test([int(2),int(1)],[int(2),int(1)],pred_true,WF),WF)).
902 :- 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)).
903 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_test([int(2),int(1)],global_set('NATURAL1'),pred_true,WF),WF)).
904 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_equality:subset_test([],[int(2),int(1)],pred_true,WF),WF)).
905 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:subset_test([],[int(2),int(1)],pred_false,_WF))).
906 :- assert_must_succeed((kernel_equality:subset_test([],[int(3)],R,_WF),R==pred_true)).
907 :- assert_must_succeed((kernel_equality:subset_test([int(2),int(1)],[int(2),int(1),int(3)],R,_WF),R==pred_true)).
908 :- assert_must_succeed((kernel_equality:subset_test([int(2),int(1),int(4)],[int(2),int(1),int(3)],R,_WF),R==pred_false)).
909 :- assert_must_succeed((kernel_equality:subset_test([int(222),int(1)],global_set('NATURAL'),R,_WF),R==pred_true)).
910 :- assert_must_succeed((kernel_equality:subset_test([int(222),int(1)],global_set('NATURAL1'),R,_WF),R==pred_true)).
911 :- assert_must_succeed((kernel_equality:subset_test([int(222),int(1),int(0)],global_set('NATURAL1'),R,_WF),R==pred_false)).
912 :- assert_must_succeed((kernel_equality:subset_test([int(222),int(1),int(0)],X,R,_WF),X=global_set('NATURAL1'),R==pred_false)).
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([int(222),int(-11)],global_set('INTEGER'),R,_WF),R==pred_true)).
915 :- assert_must_succeed((kernel_equality:subset_test(global_set('INTEGER'),global_set('NATURAL1'),R,_WF),R==pred_false)).
916 :- assert_must_succeed((kernel_equality:subset_test(global_set('NATURAL1'),global_set('NATURAL1'),R,_WF),R==pred_true)).
917
918 :- use_module(kernel_objects,[check_subset_of_wf/3, not_subset_of_wf/3,
919 check_subset_of_global_sets/2, check_not_subset_of_global_sets/2,
920 both_global_sets/4]).
921
922 :- use_module(custom_explicit_sets,[expand_custom_set_to_list/4,
923 expand_custom_set_to_list_no_dups_wf/5, expand_custom_set_to_list_wf/5,
924 is_definitely_maximal_set/1]).
925 :- block subset_test(-,-,-,?).
926 subset_test(_S1,S2,R,_WF) :- % tools_printing:print_term_summary(subset_test(_S1,S2,R,WF)), %%
927 is_definitely_maximal_set(S2),!,R=pred_true.
928 ?subset_test(S1,S2,R,WF) :- subset_test0(S1,S2,R,WF).
929
930 :- block subset_test0(-,?,-,?).
931 subset_test0(S1,S2,R,WF) :- % tools_printing:print_term_summary(subset_test0(S1,S2,R,WF)), %%
932 nonvar(R),!,
933 ? (R==pred_true -> check_subset_of_wf(S1,S2,WF)
934 ; R==pred_false -> not_subset_of_wf(S1,S2,WF)
935 ; add_error_fail(subset_test0,'Illegal result value: ',R)).
936 subset_test0([],_,R,_WF) :- !,R=pred_true.
937 subset_test0(S1,S2,R,WF) :- subset_test1(S1,S2,R,WF).
938
939
940 :- use_module(covsrc(coverage_tools_annotations),['$NOT_COVERED'/1]).
941
942 :- block subset_test1(-,?,-,?),subset_test1(?,-,-,?).
943 subset_test1(S1,S2,R,WF) :- nonvar(R),!,
944 ? (R==pred_true -> check_subset_of_wf(S1,S2,WF) ; not_subset_of_wf(S1,S2,WF)).
945 subset_test1([],_,R,_WF) :- !,R=pred_true, '$NOT_COVERED'('cannot be covered'). /* cannot be covered; emtpy set treated above */
946 subset_test1(Set1,Set2,R,WF) :- both_global_sets(Set1,Set2,G1,G2),!, % also deals with two intervals
947 test_subset_of_global_sets_wf(G1,G2,R,WF).
948 subset_test1(_Set1,Set2,R,_WF) :-
949 is_definitely_maximal_set(Set2),!, % TO DO: avoid re-checking it if we have already checked it above in subset_test
950 R=pred_true.
951 subset_test1(Set1,Set2,R,WF) :- Set2==[],!, eq_empty_set_attr_wf(Set1,R,WF).
952 ?subset_test1(Set1,Set2,R,WF) :- test_subset_of_explicit_set(Set1,Set2,R,WF,Code),!,
953 call(Code).
954 subset_test1(Set1,Set2,R,WF) :-
955 expand_custom_set_to_list_no_dups_wf(Set1,ESet1,_,subset_test1,WF),
956 % no_dups relevant for test 2202 on SWI Prolog, where conjoin(pred_true,X,Y) -> propagation of X & Y are separate
957 subset_test2(ESet1,Set2,R,WF).
958
959 :- block subset_test2(-,?,?,?).
960 subset_test2([],_,R,_WF) :- !, R=pred_true.
961 subset_test2(Set1,Set2,R,WF) :- R==pred_true,!,
962 ? check_subset_of_wf(Set1,Set2,WF). % may more aggressively instantiate Set2
963 % not useful to have special case for pred_false which uses membership_test_wf also
964 subset_test2([H|T],Set2,R,WF) :- %print(subset_test2([H|T],Set2,R)),nl,
965 (T==[]
966 -> membership_test_wf(Set2,H,R,WF)
967 ; membership_test_wf(Set2,H,MemRes,WF),
968 subset_test3(MemRes,T,Set2,R,WF),
969 (var(MemRes) -> propagate_true(R,MemRes) ; true) % in case overall subset holds, then MemRes must be true
970 ).
971
972 :- block subset_test3(-,?,?,?,?).
973 subset_test3(pred_false,_T,_Set2,R,_WF) :- R=pred_false.
974 ?subset_test3(pred_true,T,Set2,R,WF) :- subset_test2(T,Set2,R,WF).
975
976 :- block propagate_true(-,?).
977 propagate_true(pred_true,X) :- !, X=pred_true.
978 propagate_true(_,_).
979
980 %:- block test_subset_of_global_sets(-,?,?), not_subset_of_global_sets(?,-,?).
981 test_subset_of_global_sets_wf(interval(Low1,Up1),interval(Low2,Up2),Res,WF) :- !,
982 test_interval_subset_wf(Low1,Up1,Low2,Up2,Res,WF).
983 test_subset_of_global_sets_wf(G1,G2,R,_) :- G1==G2,!,R=pred_true.
984 test_subset_of_global_sets_wf(G1,G2,R,_) :- %print(check_subset(G1,G2)),nl,
985 when((nonvar(R);(ground(G1),ground(G2))),test_subset_of_global_sets_aux(G1,G2,R)).
986 % TO DO: provide better reified version, especially for intervals with variables !
987 % e.g., 1..x <: NATURAL1 ==> R=pred_true, ...
988
989 test_subset_of_global_sets_aux(G1,G2,R) :- R==pred_true,!, check_subset_of_global_sets(G1,G2).
990 test_subset_of_global_sets_aux(G1,G2,R) :- R==pred_false,!, check_not_subset_of_global_sets(G1,G2).
991 test_subset_of_global_sets_aux(G1,G2,R) :-
992 (check_subset_of_global_sets(G1,G2) -> R=pred_true ; R=pred_false).
993
994
995 :- use_module(b_interpreter_check,[imply/3, conjoin/6]).
996 test_interval_subset_wf(Low1,Up1,Low2,Up2,Res,WF) :-
997 % print(test_interval_subset_wf(Low1,Up1,Low2,Up2,Res)),nl,
998 check_less_than_equal_inf(Low1,Up1,NonEmpty),
999 (NonEmpty==false -> Res=pred_true % if Low1..Up1 is empty it is a subset of anything
1000 ; check_less_than_equal_inf(Low2,Low1,R1),
1001 (R1 == pred_false, NonEmpty==pred_true -> Res=pred_false
1002 ; check_less_than_equal_inf(Up1,Up2,R2),
1003 conjoin_test(R1,R2,R12,WF),
1004 imply(NonEmpty,R12,Res) % if Low1..Up1 is empty the bounds must be within Low2..Up2
1005 )
1006 ).
1007
1008 :- use_module(b_interpreter_check,[check_less_than_equal/3]).
1009 % reify: X<=Y, a version of check_less_than_equal that can deal with minus_inf and inf
1010 % assumption: minus_inf, inf are either there directly; a variable will never be instantiated to inf, minus_inf
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