1 % (c) 2009-2025 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 (RX==pred_false
236 -> Res=pred_false % no need to check Y=Y2
237 ; and_equality(RY,RX,Res), % typically Res is var, hence it is better to call and_equality after X
238 ? equality_objects_wf_no_enum(Y,Y2,RY,WF)).
239 ?equality_objects1([],S,R,WF) :- !,eq_empty_set_wf(S,R,WF).
240 %equality_objects1(X,[],R,WF) :- !,eq_empty_set_wf(X,R,WF).
241 ?equality_objects1(X,Y,R,WF) :- equality_objects2(X,Y,R,WF).
242
243 :- block equality_freeval_content(-,?,?,?,?).
244 % if the case is different, we don't care anymore about the content; and the types could be different
245 equality_freeval_content(pred_false,_Value1,_Value2,_,_).
246 equality_freeval_content(pred_true,Value1,Value2,Res,WF) :-
247 % if we do not wait until we now that the case is the same,
248 % an internal type error might be raised
249 equality_objects_wf_no_enum(Value1,Value2,Res,WF).
250
251
252 :- use_module(error_manager,[add_warning/2]).
253
254 :- block equality_objects2(?,-,-,?). % also wait on second or third argument
255 equality_objects2(X,Y,Res,WF) :- nonvar(Res),!,% we know the result of the comparison
256 ( Res=pred_true -> %% print(forcing_equal(X,Y)),nl,%%
257 ? equal_object_wf(X,Y,equality_objects2_1,WF)
258 ? ; Res=pred_false -> not_equal_object_wf(X,Y,WF)
259 ; add_error_fail(equality_objects2,'Illegal result: ',equality_objects2(X,Y,Res,WF))
260 ).
261 ?equality_objects2([H|T],S,Res,WF) :- !,eq_cons(S,H,T,Res,WF). % move to equality_objects1 ?!
262 equality_objects2(avl_set(A),S,Res,WF) :-
263 (S=[H|T] -> !, eq_cons(avl_set(A),H,T,Res,WF)
264 ; S = [] -> !, (A=empty -> add_warning(equality_objects2,'Empty avl_set'), Res=pred_true
265 ; Res=pred_false)).
266 equality_objects2(ES1,ES2,Res,WF) :-
267 equality_explicit_sets_wf(ES1,ES2,ERes,WF), !,
268 Res=ERes.
269 equality_objects2(ES1,S,Res,WF) :- is_custom_explicit_set(ES1,eq_cons),!, % move to custom_explicit_sets?
270 % S = [] or ES1 = [] is already covered above
271 ? (S=[H|T] -> eq_cons(ES1,H,T,Res,WF) % maybe we can avoid expanding ES1
272 ; is_infinite_explicit_set(ES1),is_custom_explicit_set(S,eq_cons)
273 -> expand_custom_set_wf(S,ExpSet,equality_objects2,WF),
274 equality_objects0(ExpSet,ES1,Res,WF)
275 ; expand_custom_set_wf(ES1,ExpSet,equality_objects2,WF), equality_objects0(ExpSet,S,Res,WF)
276 ).
277 equality_objects2(X,Y,Res,WF) :-
278 add_internal_error('Unknown objects:',equality_objects2(X,Y,Res,WF)), % could happen with abort(.) terms ?
279 (equal_object_wf(X,Y,equality_objects2_2,WF),Res=pred_true
280 ;
281 not_equal_object_wf(X,Y,WF),Res=pred_false
282 ).
283
284 %:- use_module(b_global_sets,[b_get_fd_type_bounds/3]).
285 equality_fd_objects(X,Y,_,Res) :- number(X),number(Y),!,
286 (X=Y -> Res=pred_true ; Res= pred_false).
287 equality_fd_objects(X,Y,_,Res) :- % check for attached dif co-routines; later we should probably use CHR
288 fd_frozen_dif(X,Y),!,
289 % THIS DROPS THE PERFORMANCE OF probsli ../prob_examples/examples/B/ClearSy/alloc_large.mch -init -p TIME_OUT 5000
290 Res=pred_false.
291 % Is it really necessary to keep code below: clp(FD) will do this for us ?!
292 equality_fd_objects(X,Y,Type,Res) :-
293 nonvar(Type),b_global_sets:b_get_fd_type_bounds(Type,LowBnd,UpBnd),!,
294 (LowBnd=UpBnd
295 -> X=Y,Res=pred_true /* only one object of Type exists */
296 ; LB1 is LowBnd+1,
297 (LB1 = UpBnd
298 -> bin_eq_atomic(X,Y,Res,LowBnd,UpBnd) /* two objects exist */
299 ; eq_atomic_simple(X,Y,global(Type),Res),
300 (var(Res),(var(X);var(Y))
301 -> clpfd_in_domain(X,LowBnd,UpBnd), % just like X in LowBnd..UpBnd but can deal with UpBnd=inf
302 clpfd_in_domain(Y,LowBnd,UpBnd),
303 % still required ! even with fd_utils_clpfd ! (for v8 of Bosch CrCtl_Comb2_Final_mch.eventb)
304 equality_fd(X,Y,Res)
305 ; true
306 )
307 )
308 ).
309 equality_fd_objects(X,Y,Type,Res) :-
310 add_internal_error('Unknown type: ',equality_fd_objects(X,Y,Type,Res)),
311 eq_atomic_simple(X,Y,global(Type),Res).
312
313
314 % a reified version of equality
315 %equality_fd(X,Y,Res) :- X==Y,!, Res=pred_true. % not necessary; syntactic_equality_test below will trigger
316 equality_fd(X,Y,Res) :-
317 ((X#=Y) #<=> Reification01),
318 % (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
319 prop_eq_01(Res,Reification01),
320 (var(Reification01)
321 -> syntactic_equality_test(X,Y,Res)
322 ; true).
323
324
325 % propagate pred_false/true <-> 0/1
326 :- block prop_eq_01(-,-).
327 % prop_eq_01(A,B) :- print(prop(A,B)),nl,fail.
328 ?prop_eq_01(P,B) :- var(P), !, prop_01_eq(B,P).
329 prop_eq_01(pred_true,1).
330 prop_eq_01(pred_false,0).
331 prop_01_eq(1,pred_true).
332 prop_01_eq(0,pred_false).
333
334
335 :- use_module(kernel_non_empty_attr,[get_empty_set_attr/3]).
336 %eq_empty_set(Set,PredRes) :-
337 % var(Set), var(PredRes), clpfd_card_is_gt0_for_var(Set),!, PredRes=false.
338 %eq_empty_set(Set,Res) :- eq_empty_set_attr_wf(Set,Res,no_wf_available).
339
340 eq_empty_set_attr_wf(Set,PredRes,WF) :- var(PredRes), var(Set),!,
341 get_empty_set_attr(Set,PredRes,ExistsAlready), % get attribute or create one if it does not exist
342 (ExistsAlready=is_empty_attr_exists
343 -> true % no need to compute the predicate; another call will already do it
344 ; eq_empty_set_wf(Set,PredRes,WF)).
345 eq_empty_set_attr_wf(X,R,WF) :- eq_empty_set_wf(X,R,WF).
346
347 :- use_module(kernel_waitflags,[add_error_wf/5]).
348
349 :- block eq_empty_set_wf(-,-,?).
350 % TO DO: inspect kernel_cardinality attributes
351 eq_empty_set_wf(X,R,WF) :- var(X),!,
352 ? (R=pred_true -> empty_set_wf(X,WF) ; not_empty_set_wf(X,WF)).
353 eq_empty_set_wf([],R,_) :- !,R=pred_true.
354 eq_empty_set_wf([_|_],R,_) :- !,R=pred_false.
355 eq_empty_set_wf(CS,R,WF) :- is_custom_explicit_set(CS,eq_empty_set_wf),!,
356 test_empty_explicit_set_wf(CS,R,WF).
357 eq_empty_set_wf(S,R,WF) :-
358 (S==term(undefined)
359 -> add_error_wf(eq_empty_set_wf,'Accessing uninitialised set value','',unknown,WF)
360 ; add_internal_error('Illegal Set: ',eq_empty_set_wf(S,R,_))
361 ),fail.
362
363
364 %%eq_cons(S,H,T,Res,_) :- print(eq_cons(S,H,T,Res)),nl,fail.
365 eq_cons([],_,_,Res,_) :- !, Res=pred_false.
366 eq_cons([H2|T2],H1,T1,Res,WF) :- !, % T2==[] checked? TODO: call eq_singleton_set_cons
367 check_and_remove_wf([H2|T2],H1,NewSet2,RemoveSuccesful,WF),
368 %% print(removed(H1,H2,T2,NewSet2,RemoveSuccesful)), %%
369 ? eq_cons2(RemoveSuccesful,H1,T1,H2,T2,NewSet2,Res,WF).
370 eq_cons(avl_set(A),H1,T1,Res,WF) :- !,
371 ? eq_cons_avl_set(A,H1,T1,Res,WF).
372 eq_cons(global_set(G),_H,T,Res,WF) :- %print(chk(G,H,T)),nl,
373 ? is_infinite_global_set(G,_),!,
374 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
375 Res = pred_false.
376 eq_cons(ES,H1,T1,Res,WF) :- is_custom_explicit_set(ES,eq_cons),
377 expand_custom_set_wf(ES,ExpSet,eq_cons,WF),
378 ? eq_cons1(ExpSet,H1,T1,Res,WF).
379
380 % check if {H2} = {H1|T1}
381 eq_singleton_set_cons(H2,H1,T1,Res,WF) :- T1==[], !, equality_objects_wf_no_enum(H2,H1,Res,WF).
382 eq_singleton_set_cons(H2,H1,T1,Res,WF) :- empty_set_test_wf(T1,T1Empty,WF),
383 % TODO: we could also call equality_objects(H2,H1,H2H1Eq) if T1Empty is not known and conjoin it
384 ? eq_singleton2(H2,H1,T1Empty,Res,WF).
385
386 :- block eq_singleton2(?,?,-,-,?).
387 eq_singleton2(H2,H1,T1Empty,Res,WF) :- T1Empty==pred_true,!,
388 ? equality_objects_wf_no_enum(H2,H1,Res,WF).
389 eq_singleton2(_,_,T1Empty,Res,_) :- T1Empty==pred_false,!,
390 Res=pred_false. % if T1 is not empty, [H1|T1] is different from [H2]
391 eq_singleton2(H2,H1,T1Empty,Res,WF) :- Res==pred_true,!,T1Empty=pred_true,
392 equal_object_wf(H2,H1,eq_singleton2,WF).
393 eq_singleton2(H2,H1,T1Empty,Res,WF) :- Res==pred_false,!,
394 when(nonvar(T1Empty),eq_singleton2(H2,H1,T1Empty,Res,WF)).
395
396
397 % this treatment (second clause) is relevant for avoiding unnecessary choice points
398 % 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)
399 eq_cons_avl_set(A,H1,T1,Res,WF) :- is_one_element_avl(A,AEl),
400 !,
401 ? eq_singleton_set_cons(AEl,H1,T1,Res,WF).
402 eq_cons_avl_set(A,H1,T1,Res,WF) :-
403 (var(Res) -> kernel_tools:ground_value_check(H1,GrH1) ; true), % if Res already bound, no need to do ground check
404 ? block_eq_cons_avl_set(A,H1,T1,Res,GrH1,WF).
405 :- block block_eq_cons_avl_set(?,?,?,-,-,?).
406 block_eq_cons_avl_set(A,H1,T1,Res,_,WF) :- Res==pred_true,!,
407 kernel_objects:equal_custom_explicit_set_cons_wf(avl_set(A),H1,T1,WF).
408 block_eq_cons_avl_set(A,H1,T1,Res,_,WF) :-
409 element_can_be_added_or_removed_to_avl(H1),!, % should hopefully be true as H1 is now ground
410 (remove_element_from_explicit_set(avl_set(A),H1,RA)
411 ? -> equality_objects_with_expansion(T1,RA,Res,WF) %%% PROBLEM: T1 has to be in list form !
412 ; Res = pred_false
413 ).
414 block_eq_cons_avl_set(A,H1,T1,Res,_,WF) :-
415 % 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
416 expand_custom_set_wf(avl_set(A),ExpSet,block_eq_cons_avl_set,WF),
417 eq_cons1(ExpSet,H1,T1,Res,WF).
418
419 :- block eq_cons1(-,?,?,?,?).
420 ?eq_cons1(ExpSet,H1,T1,Res,WF) :- eq_cons(ExpSet,H1,T1,Res,WF).
421
422 :- block eq_cons2(-, ?,?,?,?, ?,-,?).
423 eq_cons2(RemoveSuccesful, H1,T1,H2,T2, _NewSet2,Res,WF) :- var(RemoveSuccesful),!,
424 % result has been instantiated before Remove finished; now force equal_object or not_equal_object
425 % note: without this the remove could be pending (see test 1112, 1105)
426 % TO DO: look whether we could force remove and continue from there ?
427 ? equality_objects2([H1|T1],[H2|T2],Res,WF).
428 eq_cons2(not_successful, _,_T1,_,_, _NewSet2,pred_false,_).
429 ?eq_cons2(successful, _, T1,_,_, NewSet2,Res,WF) :- equality_objects_wf_no_enum(T1,NewSet2,Res,WF).
430
431
432 check_and_remove(Set,ElementToRemove,ResultingSet,Res) :-
433 check_and_remove_wf(Set,ElementToRemove,ResultingSet,Res,no_wf_available).
434
435 :- block check_and_remove_wf(-,?,?,?,?).
436 check_and_remove_wf([],_,ResultingSet,Res,_) :- !, ResultingSet=[],Res=not_successful.
437 check_and_remove_wf([H|T],ElementToRemove,ResultingSet,Res,WF) :- !,
438 equality_objects_wf_no_enum(H,ElementToRemove,RH,WF),
439 %%print(equality_objects_result(H,ElementToRemove,RH)),nl,
440 ? check_and_remove2(RH,H,T,ElementToRemove,ResultingSet,Res,WF).
441 check_and_remove_wf(CS,ElementToRemove,ResultingSet,Res,WF) :-
442 expand_custom_set_to_list_wf(CS,ESet,_,check_and_remove,WF),
443 check_and_remove_wf(ESet,ElementToRemove,ResultingSet,Res,WF).
444
445 :- block check_and_remove2(-,?,?,?,?,?,?).
446 check_and_remove2(pred_true, _H,T,_ElementToRemove,T,successful,_).
447 check_and_remove2(pred_false,H,T,ElementToRemove,[H|RT],Res,WF) :-
448 ? check_and_remove_wf(T,ElementToRemove,RT,Res,WF).
449
450
451 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:and_equality(pred_false,pred_false,pred_false))).
452 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:and_equality(pred_true,pred_false,pred_false))).
453 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:and_equality(pred_true,pred_true,pred_true))).
454 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_true,pred_true,pred_false))).
455 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_true,pred_false,pred_true))).
456 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_false,pred_true,pred_true))).
457 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_false,pred_false,pred_true))).
458 :- block and_equality(-,-,-).
459 and_equality(X,Y,Res) :-
460 ( X==pred_true -> Res=Y
461 ; X==pred_false -> Res=pred_false
462 ; Y==pred_true -> Res=X
463 ; Y==pred_false -> Res=pred_false
464 ; Res==pred_true -> X=pred_true, Y=pred_true
465 ; 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
466 ; add_error_fail(and_equality,'Illegal call: ',and_equality(X,Y,Res))
467 ).
468 :- block and_equality2(-,-,?).
469 and_equality2(X,Y,Res) :-
470 ( X==pred_true -> Res=Y
471 ; X==pred_false -> Res=pred_false
472 ; Y==pred_true -> Res=X
473 ; Y==pred_false -> Res=pred_false
474 ; add_error_fail(and_equality,'Illegal call: ',and_equality2(X,Y,Res))
475 ).
476
477 /*
478 :- block bool_eq_atomic(-,?,?,-).
479 bool_eq_atomic(X,Y,OtherY,Res) :- nonvar(Res),!,
480 (Res=pred_true -> X=Y ; X=OtherY).
481 bool_eq_atomic(X,Y,_,Res) :- X==Y -> Res=pred_true ; Res=pred_false. */
482
483 % a version for base types with just two possible values
484 :- block bin_eq_atomic(-,?,-,?,?), bin_eq_atomic(?,-,-,?,?).
485 % no need to check for frozen_dif: a dif would instantly trigger instantiation to other value
486 % However, we could use when(?=(X,Y) ; nonvar(Res) as trigger ! maybe this would slowdown SATLIB tests ??
487 bin_eq_atomic(X,Y,Res,V1,V2) :- nonvar(Res),!,
488 %print(forcing_bin_eq_atomic(X,Y,Res,V1,V2)),nl,
489 (Res=pred_true -> X=Y
490 ; %print(bin_dif(X,Y)),nl,
491 (X=V1,Y=V2 ; X=V2,Y=V1)
492 ). % difference with eq_atomic: we now know the value !
493 bin_eq_atomic(X,Y,Res,_,_) :-
494 %print(triggering_bin_eq(X,Y,Res)), translate:print_frozen_info(Res),nl,
495 (X==Y -> Res=pred_true ; Res=pred_false).
496
497 eq_atomic(X,Y,_Type,Res) :- nonvar(X),nonvar(Y),!,
498 (X=Y -> Res=pred_true ; Res=pred_false).
499 eq_atomic(X,Y,_,Res) :- % check for attached dif co-routines; later we should probably use CHR
500 ? frozen_dif(X,Y),!, Res=pred_false.
501 eq_atomic(X,Y,Type,Res) :- when((?=(X,Y);nonvar(Res)),eq_atomic2(X,Y,Type,Res)).
502
503 % version of eq_atomic without frozen_dif check (if already performed)
504 % eq_atomic_simple(X,Y,_Type,Res) :- % in all calling contexts this test is already performed
505 % nonvar(X),nonvar(Y),!, (X=Y -> Res=pred_true ; Res=pred_false).
506 eq_atomic_simple(X,Y,Type,Res) :- when((?=(X,Y);nonvar(Res)),eq_atomic2(X,Y,Type,Res)).
507
508 /*
509 Comment: % for integers CLPFD reification will not ground Res if X==Y, need to do when((?=(X,Y)...
510 | ?- X in 1..10, Y in 1..10, (X#=Y #<=> Z), X=Y.
511 Y = X,
512 X in 1..10,
513 Z in 0..1 ? */
514
515 eq_atomic2(X,Y,Type,Res) :- nonvar(Res),!,
516 ? (Res=pred_true -> X=Y ; dif(Type,X,Y)).
517 eq_atomic2(X,Y,_Type,Res) :-
518 (X=Y -> Res=pred_true
519 ; Res=pred_false).
520
521 :- block eq_term_wf(-,-,?,?).
522 eq_term_wf(TX,TY,Res,_WF) :- nonvar(TX),TX = floating(FX),!,
523 TY=floating(FY), eq_atomic(FX,FY,real,Res). % TODO: use a proper equality check for reals/floats
524 eq_term_wf(TY,TX,Res,_WF) :- nonvar(TX),TX = floating(FX),!,
525 TY=floating(FY), eq_atomic(FX,FY,real,Res).
526 eq_term_wf(TX,TY,Res,_) :- eq_atomic(TX,TY,term,Res).
527
528 :- use_module(fd_utils_clpfd,[neq_fd/3]).
529 dif(boolean,A,B) :- !,
530 bool_pred:negate(A,B). % was: bool_dif(A,B).
531 % usually not covered: equality_objects_with_type calls bool_equality,
532 % equality_objects waits for either arg to be fully instantiated to pred_false or pred_true
533 dif(integer,A,B) :- !, integer_dif(A,B).
534 ?dif(global(T),A,B) :- !, neq_fd(A,B,T).
535 dif(_,A,B) :- dif(A,B).
536
537 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:integer_dif(0,1))).
538 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:integer_dif(1,1))).
539 :- use_module(clpfd_interface,[clpfd_neq/2]).
540 integer_dif(A,B) :- clpfd_neq(A,B). % clpfd_neq calls dif on overflow
541
542
543 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:bool_dif(pred_false,pred_true))).
544 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:bool_dif(pred_true,pred_false))).
545 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:bool_dif(pred_true,pred_true))).
546 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:bool_dif(pred_false,pred_false))).
547 bool_dif(A,B) :- bool_pred:negate(A,B).
548
549 /* old version:
550 :- block eq_atomic(-,?,-), eq_atomic(?,-,-).
551 eq_atomic(X,Y,Res) :- nonvar(Res),!,
552 (Res=pred_true -> X=Y ; dif(X,Y)).
553 eq_atomic(X,Y,Res) :- X==Y -> Res=pred_true
554 ; Res=pred_false.
555 */
556
557 :- use_module(kernel_records,[check_field_name_compatibility/3]).
558 :- block equality_fields(-,?,-,?), equality_fields(?,-,-,?), equality_fields(-,-,?,?).
559 % if last argument is known we should propagate the field names from one record to another; see test 1289 (Hansen12)
560 equality_fields([],[],pred_true,_).
561 equality_fields([field(Name1,V1)|T1],[field(Name2,V2)|T2],Res,WF) :-
562 % should we wait for Name1 or Name2 to become nonvar?
563 ? check_field_name_compatibility(Name1,Name2,equality_fields),
564 equality_objects_wf_no_enum(V1,V2,RH,WF),
565 (RH==pred_false -> Res = pred_false % no need to check T1=T2
566 ; and_equality(RH,RT,Res),
567 ? equality_fields(T1,T2,RT,WF)
568 ).
569
570
571
572 empty_set_test_wf(Set,EqRes,WF) :- eq_empty_set_attr_wf(Set,EqRes,WF).
573 empty_set_test(Set,EqRes) :- eq_empty_set_attr_wf(Set,EqRes,no_wf_available).
574 empty_cartesian_product_wf(Set1,Set2,EqRes,WF) :- % TO DO: pass WF
575 eq_empty_set_wf(Set1,EqRes1,WF),
576 (EqRes1==pred_true -> EqRes=pred_true /* avoid inspecting Set2 */
577 ; or_eq_obj(EqRes1,EqRes2,EqRes),
578 eq_empty_set_wf(Set2,EqRes2,WF)).
579
580
581 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:or_eq_obj(pred_false,pred_false,pred_false))).
582 :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:or_eq_obj(pred_false,pred_true,pred_true))).
583 :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:or_eq_obj(pred_true,pred_true,pred_true))).
584 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_true,pred_true,pred_false))).
585 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_true,pred_false,pred_false))).
586 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_false,pred_true,pred_false))).
587 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_false,pred_false,pred_true))).
588 :- block or_eq_obj(-,-,-).
589 % very similar to disjoin in b_interpreter_check; no waitflag to instantiate if result false
590 or_eq_obj(X,Y,XorY) :-
591 ( (X==pred_true ; Y==pred_true) -> XorY=pred_true
592 ; XorY==pred_false -> X=pred_false,Y=pred_false
593 ; X==pred_false -> XorY = Y
594 ; Y==pred_false -> XorY = X
595 ; XorY==pred_true -> or_eq_obj2(X,Y)
596 ; add_internal_error('Illegal call: ',or_eq_obj(X,Y,XorY)) ).
597 :- block or_eq_obj2(-,-).
598 or_eq_obj2(X,Y) :- ((X==pred_true; Y=pred_true) -> true
599 ; X==pred_false -> Y=pred_true
600 ; Y==pred_false -> X=pred_true
601 ; add_internal_error('Illegal call: ',or_eq_obj2(X,Y))).
602
603 % ------------------------------------------------------------------
604
605
606 % not used at the moment:
607 %get_partial_subset_priority(Set,WF,LWF) :- get_partial_set_size(Set,Size),
608 % safe_pow2(Size,Prio),
609 % get_wait_flag(Prio,psubset(Set),WF,LWF).
610 %get_partial_set_priority(Set,WF,LWF) :- get_partial_set_size(Set,Size),
611 % get_wait_flag(Size,pset(Set),WF,LWF).
612 %get_partial_set_size(X,R) :- var(X),!,R=3.
613 %get_partial_set_size([],R) :- !,R=0.
614 %get_partial_set_size([_|T],R) :- !,get_partial_set_size(T,RT), R is RT+1.
615 %get_partial_set_size(_,10).
616
617
618 get_cardinality_wait_flag(Set,Info,WF,LWF) :-
619 ? get_cardinality_wait_flag(Set,Info,WF,_Card,LWF).
620 get_cardinality_wait_flag(Set,Info,WF,Card,LWF) :-
621 cardinality_as_int_for_wf(Set,Card),
622 % when(nonvar(X), (print(get_card_waitflag(X,Set,WF,LWF)),nl)),
623 (var(Card)
624 -> kernel_waitflags:get_last_wait_flag(get_cardinality_wait_flag(Info),WF,LastWF)
625 ; true), % ensure that we trigger choice points waiting on LWF before infinite enumeration starts
626 ? get_cardinality_wait_flag2(Card,Info,WF,LastWF,LWF).
627 :- block get_cardinality_wait_flag2(-,?,?,-,?).
628 get_cardinality_wait_flag2(X,_Info,_WF,LastWF,LWF) :- var(X),!,LWF=LastWF.
629 ?get_cardinality_wait_flag2(X,Info,WF,_,LWF) :- get_bounded_wait_flag(X,Info,WF,LWF).
630
631 get_cardinality_powset_wait_flag(Set,Info,WF,CardSet,LWF) :-
632 cardinality_as_int_for_wf(Set,CardSet),
633 get_cardinality_powset_wait_flag2(CardSet,Info,WF,LWF).
634 :- block get_cardinality_powset_wait_flag2(-,?,?,?).
635 get_cardinality_powset_wait_flag2(X,Info,WF,LWF) :-
636 safe_pow2(X,X2),
637 %safe_mul(X2,10000,X3), % as generating subsets this way will generate repetitions
638 (is_inf_or_overflow_card(X2)
639 ? -> integer_pow2_priority(R), get_wait_flag(R,powset_card(Info),WF,LWF)
640 ? ; get_bounded_wait_flag(X2,powset_card(Info),WF,LWF) % finite prio; ensure we do not exceed infinite prios if X2 very large
641 ).
642
643
644 % CARDINALITY FOR NUMBER OF PARTIAL FUNCTIONS: (not used at the moment)
645 %get_cardinality_partial_function_wait_flag(DomSet,RanSet,Info,WF,CardDomSet,CardRanSet,LWF) :-
646 % cardinality_as_int_for_wf(DomSet,CardDomSet),
647 % cardinality_as_int_for_wf(RanSet,CardRanSet),
648 % get_cardinality_partial_function_wait_flag(CardDomSet,CardRanSet,Info,WF,LWF).
649 %:- block get_cardinality_partial_function_wait_flag(-,?,?,?,?),
650 % get_cardinality_partial_function_wait_flag(?,-,?,?,?).
651 %get_cardinality_partial_function_wait_flag(DC,RC,Info,WF,LWF) :-
652 % priority_pow1n(RC,DC,PFCARD), print(prio(PFCARD)),nl,
653 % get_bounded_wait_flag(PFCARD,powset_card(Info),WF,LWF).
654 % % Cardinality of the set of partial functions : (card(Range)+1)^card(Domain)
655 %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 !
656 %priority_pow1n(X,Y,RR) :- X1 is X+1, safe_pown(X1,Y,R),
657 % (R==inf -> integer_pow2_priority(RR) %RR=10000010
658 % ; RR=R).
659
660 % CARDINALITY FOR NUMBER OF RELATIONS:
661 get_cardinality_relation_over_wait_flag(Dom,Ran,WF,LWF,MaxCardOfRel,MaxNrOfRels) :-
662 cardinality_as_int_for_wf(Dom,X),
663 cardinality_as_int_for_wf(Ran,Y),
664 get_cardinality_relation_over_wait_flag2(X,Y,WF,LWF,MaxCardOfRel,MaxNrOfRels).
665
666 :- block get_cardinality_relation_over_wait_flag2(-,?,?,?,?,?), get_cardinality_relation_over_wait_flag2(?,-,?,?,?,?).
667 get_cardinality_relation_over_wait_flag2(X,Y,WF,LWF,MaxCardOfRel,MaxNrOfRels1) :-
668 safe_mul(X,Y,MaxCardOfRel),
669 safe_pow2(MaxCardOfRel,MaxNrOfRels),
670 safe_add_card(MaxNrOfRels,1,MaxNrOfRels1), /* add 1 to give priority to tighter_enum */
671 ? get_bounded_wait_flag(MaxNrOfRels1,powset_rel_card,WF,LWF).
672
673 % ------------------------------------------------------------------
674
675 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(2),pred_true,WF),WF)).
676 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(1),pred_true,WF),WF)).
677 :- 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)).
678 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(3),pred_false,WF),WF)).
679 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([],int(3),pred_false,WF),WF)).
680 :- assert_must_succeed(exhaustive_kernel_fail_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(3),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(1),int(4)],pred_true,WF),WF)).
682 :- 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)).
683 :- 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)).
684 :- assert_must_succeed((membership_test_wf([int(2),int(1)],int(2),R,_WF),R==pred_true)).
685 :- assert_must_succeed((membership_test_wf([int(2),int(1)],int(X),R,_WF),var(R),X=1,R==pred_true)).
686 :- assert_must_succeed((membership_test_wf([int(2),int(1)],int(3),R,_WF),R==pred_false)).
687 :- assert_must_succeed((membership_test_wf(global_set('Name'),fd(1,'Name'),R,_WF),R==pred_true)).
688
689 :- 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)),
690 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)).
691 :- assert_must_succeed((
692 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))])],
693 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
694 )).
695 /* membership_test_wf: A function that instantiates last argument when membership test can be decided */
696
697
698 % a version which also creates a choice point in SMT mode
699 membership_test_wf_with_force(Set,X,Res,WF) :-
700 membership_test_wf(Set,X,Res,outer,WF),
701 enum_equality_result_smt_mode_wf(Res,membership_test_wf,WF).
702 :- block force_equality_result(-,-).
703 force_equality_result(pred_true,_).
704 force_equality_result(pred_false,_).
705
706 enum_equality_result_smt_mode_wf(Res,PP,WF) :- var(Res),
707 preferences:preference(use_smt_mode,true),!,
708 enum_equality_result_wf(Res,PP,WF).
709 enum_equality_result_smt_mode_wf(_,_,_).
710
711 enum_equality_result_wf(Res,PP,WF) :-
712 get_last_wait_flag(PP,WF,LWF),
713 force_equality_result(Res,LWF).
714
715 ?membership_test_wf(Set,X,Res,WF) :- membership_test_wf(Set,X,Res,outer,WF).
716
717 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
718 :- if(environ(prob_data_validation_mode,true)).
719 :- block membership_test_wf(-,?,?,?,?). % avoid instantiating Set
720 :- else.
721 :- block membership_test_wf(-,?,-,?,?).
722 :- endif.
723 membership_test_wf(Set,X,Res,_OuterInner,WF) :- nonvar(Res),!,
724 (Res==pred_true
725 ? -> call_check_element_of_wf0(X,Set,WF)
726 /* (kernel_objects:unbound_variable_for_cons(Set)
727 -> kernel_objects:mark_as_non_free(X), % attach co-routine to indicate that we cannot freely chose X
728 print(instantiate_set(Set,X,Res)),nl,
729 Set=[X|_] % TO DO: normalise X first ?
730 ; when(nonvar(Set), membership_test_wf2(Set,X,Res,OuterInner,WF))
731 ) */
732 ; membership_not_el(Set,X,WF)).
733 membership_test_wf(Set,X,Res,OuterInner,WF) :-
734 ? membership_test_wf2(Set,X,Res,OuterInner,WF).
735
736 % we are not sure if WF0 is set; go via kernel_mappings:
737 ?call_check_element_of_wf0(X,Set,WF) :- get_wait_flag0(WF,WF0),
738 ? kernel_mappings:check_element_of_wf0(X,Set,WF,WF0,unknown).
739
740
741 :- block membership_not_el(-,?,?).
742 membership_not_el([],_,_WF) :- !.
743 membership_not_el([H|T],X,WF) :- !,
744 ? not_equal_object_wf(H,X,WF),
745 membership_not_el(T,X,WF).
746 membership_not_el(avl_set(A),X,WF) :- !,membership_custom_set_wf(avl_set(A),X,pred_false,WF).
747 membership_not_el(CS,X,WF) :- is_custom_explicit_set_nonvar(CS),!,
748 membership_custom_set_wf(CS,X,pred_false,WF).
749
750 membership_test_wf2([],_X,Res,_,_WF) :- !, Res=pred_false.
751 membership_test_wf2([H|T],X,Res,OuterInner,WF) :- !,
752 (Res==pred_false
753 -> not_equal_object_wf(H,X,WF), membership_test_wf(T,X,Res,WF)
754 ? ; T==[] -> equality_objects_wf_no_enum(H,X,Res,WF)
755 % TO DO: at the outer level we could check whether the list has the same length as the type of X
756 ; OuterInner=outer, is_definitely_maximal_set([H|T]) -> Res=pred_true
757 ; (OuterInner=outer, % avoid re-checking ground_list_with_fd over and over again
758 preferences:preference(use_clpfd_solver,true),
759 ground_list_with_fd([H|T]),
760 construct_avl_from_lists_wf([H|T],CS,WF))
761 % 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
762 % TO DO: call clpfd_reify_inlist directly ? avoid translating to AVL and back to list; detect maximal list
763 ? -> membership_custom_set_wf(CS,X,Res,WF) %, print(conv_to_avl(X,[H|T],CS,Res)),nl
764 ; %print(eq(Res,H,X,T,WF)),nl,equality_objects_wf_dbg(H,X,HXRes,WF), % makes test 1003 : plavis-MemoryLoad_SP_55 fail
765 ? equality_objects_wf_no_enum(H,X,HXRes,WF),cons_el_of(HXRes,T,X,Res,WF)
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 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) :-
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) :-
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) :- !,
945 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) :-
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,_) :-
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 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) :-
1044 S2==[],!,R=pred_false.
1045 subset_strict_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) :-
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 %equality_can_be_decided_by_unification(rec(Fields)) :- equality_can_be_decided_fields(Fields).
1082 % TODO: freeval, records (must be sorted)
1083
1084 %equality_can_be_decided_fields(V) :- var(V),!,fail.
1085 %equality_can_be_decided_fields([]).
1086 %equality_can_be_decided_fields([field(Name,Value)|T]) :- nonvar(Name),
1087 % equality_can_be_decided_by_unification(Value),
1088 % equality_can_be_decided_fields(T).