| 1 | | % (c) 2009-2019 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, equality_objects_lwf/4, equality_objects/3, |
| 6 | | equality_objects_with_type/4, |
| 7 | | empty_set_test/2, empty_cartesian_product/3, |
| 8 | | or_eq_obj/3, |
| 9 | | get_cardinality_wait_flag/4, get_cardinality_wait_flag/5, |
| 10 | | get_cardinality_powset_wait_flag/5, |
| 11 | | get_cardinality_relation_over_wait_flag/6, |
| 12 | | %get_cardinality_partial_function_wait_flag/7, |
| 13 | | check_and_remove/4, |
| 14 | | membership_test/3, membership_test_wf/4, |
| 15 | | membership_test_wf_with_force/4, |
| 16 | | cartesian_pair_test_wf/5, |
| 17 | | in_nat_range_test/4, |
| 18 | | |
| 19 | | dif/3, integer_dif/2, bool_dif/2, eq_atomic/4, |
| 20 | | |
| 21 | | subset_test/4, subset_strict_test/4, |
| 22 | | conjoin_test/4]). |
| 23 | | |
| 24 | | :- use_module(kernel_objects,[equal_object/3, |
| 25 | | not_equal_object/2, not_equal_object_wf/3, |
| 26 | | cardinality_as_int_for_wf/2, |
| 27 | | safe_mul/3, safe_add/3, safe_pow2/2, % safe_pown/3, |
| 28 | | empty_set/1, not_empty_set/1, |
| 29 | | exhaustive_kernel_check/2, exhaustive_kernel_check/1, |
| 30 | | exhaustive_kernel_check_wf/2, exhaustive_kernel_fail_check_wf/2, |
| 31 | | exhaustive_kernel_fail_check/1]). |
| 32 | | :- use_module(b_interpreter_check,[conjoin/6]). |
| 33 | | :- use_module(kernel_dif). |
| 34 | | |
| 35 | | :- use_module(self_check). |
| 36 | | |
| 37 | | |
| 38 | | :- use_module(module_information,[module_info/2]). |
| 39 | | :- module_info(group,kernel). |
| 40 | | :- module_info(description,'This module provides reified equality and membership predicates.'). |
| 41 | | |
| 42 | | :- use_module(error_manager). |
| 43 | | |
| 44 | | % kernel_equality |
| 45 | | % :- ensure_loaded(kernel_equality). |
| 46 | | |
| 47 | | :- use_module(custom_explicit_sets). |
| 48 | | :- use_module(kernel_waitflags). |
| 49 | | |
| 50 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([int(2),int(1)],[int(2)],pred_false))). |
| 51 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([int(2),int(1)],[],pred_false))). |
| 52 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([int(2),int(1)],[int(1),int(2)],pred_true))). |
| 53 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([[int(2)],[int(1)]],[[int(1)],[int(2)]],pred_true))). |
| 54 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([string('STRING1')],[string('STRING2')],pred_false))). |
| 55 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([string('STRING2'),string('STRING1')], |
| 56 | | [string('STRING1'),string('STRING2')],pred_true))). |
| 57 | | :- 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))). |
| 58 | | :- 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))). |
| 59 | | :- assert_must_succeed((equality_objects(A,B,R), A=[int(2),int(3)],B=[int(X),int(Y)], |
| 60 | | X=4,Y=2, R==pred_false)). |
| 61 | | :- assert_must_succeed((equality_objects(A,B,R), A=[int(2),int(3)],B=[int(X),int(Y)], |
| 62 | | X=2,Y=4, R==pred_false)). |
| 63 | | :- assert_must_succeed((equality_objects(A,B,R), A=[int(2),int(3)],B=[int(X),int(Y)], |
| 64 | | X=3,Y=2, R==pred_true)). |
| 65 | | :- assert_must_succeed((equality_objects(A,B,R), A=[int(2),int(3)],B=[int(X),int(Y)], |
| 66 | | X=2,Y=3, R==pred_true)). |
| 67 | | :- assert_must_succeed((equality_objects(A,B,R), A=int(2),B=int(X), |
| 68 | | R=pred_true, X==2)). |
| 69 | | |
| 70 | | |
| 71 | | /* equality_objects/3 is a function which compares two objects |
| 72 | | and returns either pred_true or pred_false in the third argument, |
| 73 | | as soon as it can be decided whether the objects are equal */ |
| 74 | | |
| 75 | | |
| 76 | | equality_objects_wf(X,Y,Res,WF) :- |
| 77 | | equality_objects_lwf(X,Y,Res,LWF), |
| 78 | | (var(Res),WF\==no_wf_available -> get_last_wait_flag(equality_objects_wf,WF,LWF) ; true). |
| 79 | | |
| 80 | | equality_objects_lwf(X,Y,Res,_LWF) :- X==Y,!, % NOTE: what if X,Y are not well-defined (e.g., division by 0); setting Res=pred_true could lead to failure and missing a WD-problem |
| 81 | | Res=pred_true. |
| 82 | | equality_objects_lwf(X,Y,Res,LWF) :- |
| 83 | ? | equality_objects(X,Y,Res), |
| 84 | ? | force_equality_objects_lwf2(X,Y,Res,LWF). |
| 85 | | |
| 86 | | :- block force_equality_objects_lwf2(?,?,-,-). |
| 87 | | force_equality_objects_lwf2(_X,_Y,Res,_LWF) :- |
| 88 | ? | ( nonvar(Res) -> true |
| 89 | | ; ( %% print(forcing_equal(X,Y,_WF)),nl, %% |
| 90 | | % alternative would be to propagate LWF down to and_equality ? |
| 91 | | %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) |
| 92 | ? | Res=pred_true |
| 93 | | ; %Res \== pred_true, not_equal_object(X,Y), % note required anymore (commented out 27.2.2015) |
| 94 | ? | Res=pred_false |
| 95 | | )). |
| 96 | | |
| 97 | | |
| 98 | | :- block equality_objects_with_expansion(-,-,?), equality_objects_with_expansion(?,-,-), equality_objects_with_expansion(-,?,-). |
| 99 | | % will expand second argument; use if first argument is a tail of a list (representing a set) |
| 100 | | equality_objects_with_expansion(X,Y,R) :- |
| 101 | | nonvar(Y), is_custom_explicit_set_nonvar(Y),!, |
| 102 | | expand_custom_set(Y,ExpSet), |
| 103 | | equality_objects(X,ExpSet,R). |
| 104 | | equality_objects_with_expansion(X,Y,R) :- equality_objects(X,Y,R). |
| 105 | | |
| 106 | | |
| 107 | | :- use_module(bool_pred). |
| 108 | | % a version of equality_objects with type information available: allows to dispatch to boolean version |
| 109 | | equality_objects_with_type(boolean,X,Y,R) :- !, bool_pred:bool_equality(X,Y,R). |
| 110 | | equality_objects_with_type(_,X,Y,R) :- (X==Y -> R=pred_true ; equality_objectsb(X,Y,R)). |
| 111 | | |
| 112 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([int(1)],[],pred_false))). |
| 113 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([int(1)],[int(2)],pred_false))). |
| 114 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects([int(1),int(2)],[int(2),int(1)],pred_true))). |
| 115 | | :- assert_must_succeed((kernel_equality:equality_objects([int(1)],[],R),R==pred_false)). |
| 116 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects(freeval(id1,case1,int(1)),freeval(id1,case1,int(1)),pred_true))). |
| 117 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects(freeval(id1,case1,int(1)),freeval(id1,case1,int(2)),pred_false))). |
| 118 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:equality_objects(freeval(id1,case1,int(1)),freeval(id1,case2,int(1)),pred_false))). |
| 119 | | |
| 120 | | |
| 121 | ? | equality_objects(X,Y,R) :- (X==Y -> R=pred_true ; equality_objectsb(X,Y,R)). |
| 122 | | % This is in principle more precise: but entails about a 10 % penalty for make cruise |
| 123 | | %equality_objects(X,Y,R) :- when((?=(X,Y);nonvar(X);nonvar(Y)), (X==Y -> R=pred_true ; equality_objectsb(X,Y,R))). |
| 124 | | :- block equality_objectsb(-,-,-). |
| 125 | | %equality_objectsb(X,Y,R) :- % this case no longer needed, basic_type below will instantiate Y for this special case |
| 126 | | % (nonvar(X) -> X=fd(XN,GS) ; nonvar(Y) -> Y=fd(XN,GS)), |
| 127 | | % (var(GS) -> print(var_gs(fd(XN,GS))),nl,fail ; true), |
| 128 | | % b_global_sets:is_global_set_of_cardinality_one(GS,N),!, % there exist only one object of that type |
| 129 | | % XN=N, Y=X, R=pred_true. |
| 130 | | %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 |
| 131 | ? | equality_objectsb(X,Y,R) :- equality_objects0(X,Y,R). |
| 132 | | |
| 133 | | %:- block %equality_objects0(-,-,?), |
| 134 | | % equality_objects0(?,-,-), equality_objects0(-,?,-). |
| 135 | | equality_objects0(X,Y,R) :- nonvar(R),!, % we know the result of the comparison |
| 136 | | ( R=pred_true -> equal_object(X,Y,equality_objects0) |
| 137 | | ; R=pred_false -> not_equal_object(X,Y) |
| 138 | | ; add_error_fail(equality_objects0,'Illegal result: ',equality_objects0(X,Y,R)) |
| 139 | | ). |
| 140 | | % now we know that either X or Y must be nonvar |
| 141 | | equality_objects0(X,Y,R) :- |
| 142 | ? | (nonvar(Y) |
| 143 | ? | -> (X==[] -> eq_empty_set(Y,R) |
| 144 | ? | ; equality_objects1(Y,X,R) |
| 145 | | ) |
| 146 | | ; equality_objects1(X,Y,R) |
| 147 | | ). |
| 148 | | |
| 149 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
| 150 | | :- if(environ(disable_chr, true)). |
| 151 | | :- else. |
| 152 | | :- use_module(chrsrc(chr_integer_inequality),[chr_eq/3]). |
| 153 | | :- endif. |
| 154 | | :- use_module(clpfd_interface,[post_constraint2/2]). |
| 155 | ? | equality_int(X,Y,Res) :- nonvar(X),nonvar(Y),!, |
| 156 | ? | (X=Y -> Res=pred_true ; Res=pred_false). |
| 157 | | equality_int(X,Y,Res) :- |
| 158 | | % check for attached dif co-routines; diabled if CHR is used (no dif coroutine needed) |
| 159 | | % !! there might still be dif coros set up by equality_epr and dis |
| 160 | | % preferences:preference(use_chr_solver,false), |
| 161 | | fd_frozen_dif(X,Y),!, Res=pred_false. |
| 162 | | equality_int(X,Y,Res) :- |
| 163 | | (preferences:preference(use_chr_solver,true) -> chr_eq(X,Y,Res) ; true), |
| 164 | | % with CHR we detect e.g. r=TRUE in (X=Y <=> r=TRUE) & X:1..100 & Y > X |
| 165 | | % see code for equality_fd |
| 166 | | post_constraint2( ((X#=Y) #<=> R01), Posted), % from clpfd_interface |
| 167 | | (Posted = true |
| 168 | | -> prop_eq_01(Res,R01), |
| 169 | | (var(R01) -> syntactic_equality_test(X,Y,Res) ; true) % CLPFD does not detect variable equality |
| 170 | | ; eq_atomic_simple(X,Y,integer,Res)). |
| 171 | | |
| 172 | | |
| 173 | | %:- 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 |
| 174 | | % equality_objects1 assumes first argument is nonvar: |
| 175 | | %%equality_objects1(X,Y,R) :- print(equality_objects1(X,Y,R)),nl,fail. %% |
| 176 | | equality_objects1(pred_true /* bool_true */,X,Res) :- !, bool_equality(pred_true /* bool_true */,X,Res). %bool_eq_atomic(X,bool_true,pred_false /* bool_false */,Res). |
| 177 | | equality_objects1(pred_false /* bool_false */,X,Res) :- !,bool_equality(pred_false /* bool_false */,X,Res). %bool_eq_atomic(X,bool_false,bool_true,Res). |
| 178 | ? | equality_objects1(int(X),IY,Res) :- !, IY=int(Y), equality_int(X,Y,Res). |
| 179 | | equality_objects1(term(X),TY,Res) :- !, TY=term(Y), eq_atomic(X,Y,term,Res). |
| 180 | | equality_objects1(string(X),SY,Res) :- !, SY=string(Y), eq_atomic(X,Y,string,Res). |
| 181 | | equality_objects1(fd(X,Type),FY,Res) :- !, |
| 182 | | b_global_sets:get_global_type_value(FY,Type,Y), |
| 183 | | equality_fd_objects(X,Y,Type,Res). |
| 184 | | equality_objects1(freeval(Id,Case1,Value1),FY,Res) :- !, FY=freeval(Id,Case2,Value2), |
| 185 | | and_equality(CaseRes,ValueRes,Res), |
| 186 | | eq_atomic(Case1,Case2,freeval_case,CaseRes), |
| 187 | | equality_freeval_content(CaseRes,Value1,Value2,ValueRes). |
| 188 | | equality_objects1(rec(X),RY,Res) :- !, RY=rec(Y), equality_fields(X,Y,Res). |
| 189 | | equality_objects1((X,Y),XY2,Res) :- !, XY2=(X2,Y2), |
| 190 | | and_equality(RY,RX,Res), |
| 191 | | equality_objects(X,X2,RX), |
| 192 | | (RX==pred_false -> true |
| 193 | | ; equality_objects(Y,Y2,RY)). |
| 194 | | equality_objects1([],S,R) :- !,eq_empty_set(S,R). |
| 195 | | %equality_objects1(X,[],R) :- !,eq_empty_set(X,R). |
| 196 | | equality_objects1(X,Y,R) :- equality_objects2(X,Y,R). |
| 197 | | |
| 198 | | :- block equality_freeval_content(-,?,?,?). |
| 199 | | % if the case is different, we don't care anymore about the content; and the types could be different |
| 200 | | equality_freeval_content(pred_false,_Value1,_Value2,_). |
| 201 | | equality_freeval_content(pred_true,Value1,Value2,Res) :- |
| 202 | | % if we do not wait until we now that the case is the same, |
| 203 | | % an internal type error might be raised |
| 204 | | equality_objects(Value1,Value2,Res). |
| 205 | | |
| 206 | | |
| 207 | | :- use_module(error_manager,[add_warning/2]). |
| 208 | | |
| 209 | | :- block equality_objects2(?,-,-). % also wait on second or third argument |
| 210 | ? | equality_objects2(X,Y,Res) :- nonvar(Res),!,% we know the result of the comparison |
| 211 | ? | ( Res=pred_true -> %% print(forcing_equal(X,Y)),nl,%% |
| 212 | ? | equal_object(X,Y,equality_objects2_1) |
| 213 | | ; Res=pred_false -> not_equal_object(X,Y) |
| 214 | | ; add_error_fail(equality_objects2,'Illegal result: ',equality_objects2(X,Y,Res)) |
| 215 | | ). |
| 216 | | equality_objects2([H|T],S,Res) :- !,eq_cons(S,H,T,Res). % move to equality_objects1 ?! |
| 217 | | equality_objects2(avl_set(A),S,Res) :- |
| 218 | | (S=[H|T] -> !, eq_cons(avl_set(A),H,T,Res) |
| 219 | | ; S = [] -> !, (A=empty -> add_warning(equality_objects2,'Empty avl_set'), Res=pred_true |
| 220 | | ; Res=pred_false)). |
| 221 | | equality_objects2(ES1,ES2,Res) :- equality_explicit_sets(ES1,ES2,ERes), !, Res=ERes. |
| 222 | | equality_objects2(ES1,S,Res) :- is_custom_explicit_set(ES1,eq_cons),!, % move to custom_explicit_sets? |
| 223 | | % S = [] or ES1 = [] is already covered above |
| 224 | | (S=[H|T] -> eq_cons(ES1,H,T,Res) % maybe we can avoid expanding ES1 |
| 225 | | ; (is_infinite_explicit_set(ES1),is_custom_explicit_set(S,eq_cons)) |
| 226 | | -> expand_custom_set(S,ExpSet), equality_objects0(ExpSet,ES1,Res) |
| 227 | | ; expand_custom_set(ES1,ExpSet), equality_objects0(ExpSet,S,Res)). |
| 228 | | equality_objects2(X,Y,Res) :- |
| 229 | | add_internal_error('Unknown objects:',equality_objects2(X,Y,Res)), % could happen with abort(.) terms ? |
| 230 | | (equal_object(X,Y,equality_objects2_2),Res=pred_true |
| 231 | | ; |
| 232 | | not_equal_object(X,Y),Res=pred_false |
| 233 | | ). |
| 234 | | |
| 235 | | %:- use_module(b_global_sets,[b_get_fd_type_bounds/3]). |
| 236 | | :- use_module(library(clpfd)). |
| 237 | | equality_fd_objects(X,Y,_,Res) :- number(X),number(Y),!, |
| 238 | | (X=Y -> Res=pred_true ; Res= pred_false). |
| 239 | | equality_fd_objects(X,Y,_,Res) :- % check for attached dif co-routines; later we should probably use CHR |
| 240 | | fd_frozen_dif(X,Y),!, |
| 241 | | % THIS DROPS THE PERFORMANCE OF probsli ../prob_examples/examples/B/ClearSy/alloc_large.mch -init -p TIME_OUT 5000 |
| 242 | | Res=pred_false. |
| 243 | | % Is it really necessary to keep code below: clp(FD) will do this for us ?! |
| 244 | | equality_fd_objects(X,Y,Type,Res) :- |
| 245 | | nonvar(Type),b_global_sets:b_get_fd_type_bounds(Type,LowBnd,UpBnd),!, |
| 246 | | (LowBnd=UpBnd |
| 247 | | -> X=Y,Res=pred_true /* only one object of Type exists */ |
| 248 | | ; (LowBnd+1 =:= UpBnd |
| 249 | | -> bin_eq_atomic(X,Y,Res,LowBnd,UpBnd) /* two objects exist */ |
| 250 | | ; eq_atomic_simple(X,Y,global(Type),Res), |
| 251 | | (var(Res),(var(X);var(Y)) |
| 252 | | -> X in LowBnd..UpBnd, Y in LowBnd..UpBnd, % still required ! even with fd_utils_clpfd ! (for v8 of Bosch CrCtl_Comb2_Final_mch.eventb) |
| 253 | | equality_fd(X,Y,Res) |
| 254 | | ; true |
| 255 | | ) |
| 256 | | ) |
| 257 | | ). |
| 258 | | equality_fd_objects(X,Y,Type,Res) :- |
| 259 | | add_internal_error('Unknown type: ',equality_fd_objects(X,Y,Type,Res)), |
| 260 | | eq_atomic_simple(X,Y,global(Type),Res). |
| 261 | | |
| 262 | | |
| 263 | | % a reified version of equality |
| 264 | | %equality_fd(X,Y,Res) :- X==Y,!, Res=pred_true. % not necessary; syntactic_equality_test below will trigger |
| 265 | | equality_fd(X,Y,Res) :- |
| 266 | | ((X#=Y) #<=> Reification01), |
| 267 | | % (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 |
| 268 | | prop_eq_01(Res,Reification01), |
| 269 | | (var(Reification01) |
| 270 | | -> syntactic_equality_test(X,Y,Res) |
| 271 | | ; true). |
| 272 | | |
| 273 | | |
| 274 | | % propagate pred_false/true <-> 0/1 |
| 275 | | :- block prop_eq_01(-,-). |
| 276 | | % prop_eq_01(A,B) :- print(prop(A,B)),nl,fail. |
| 277 | ? | prop_eq_01(P,B) :- var(P), !, prop_01_eq(B,P). |
| 278 | | prop_eq_01(pred_true,1). |
| 279 | | prop_eq_01(pred_false,0). |
| 280 | | prop_01_eq(1,pred_true). |
| 281 | | prop_01_eq(0,pred_false). |
| 282 | | |
| 283 | | |
| 284 | | :- block eq_empty_set(-,-). |
| 285 | | eq_empty_set(X,R) :- var(X),!, |
| 286 | | (R=pred_true -> empty_set(X) ; not_empty_set(X)). |
| 287 | ? | eq_empty_set([],R) :- !,R=pred_true. |
| 288 | ? | eq_empty_set([_|_],R) :- !,R=pred_false. |
| 289 | | eq_empty_set(CS,R) :- is_custom_explicit_set(CS,eq_empty_set),!, |
| 290 | | test_empty_explicit_set(CS,R). |
| 291 | | eq_empty_set(S,R) :- add_internal_error('Illegal Set: ',eq_empty_set(S,R)),fail. |
| 292 | | |
| 293 | | %%eq_cons(S,H,T,Res) :- print(eq_cons(S,H,T,Res)),nl,fail. |
| 294 | | eq_cons([],_,_,Res) :- !, Res=pred_false. |
| 295 | | eq_cons([H2|T2],H1,T1,Res) :- !, |
| 296 | | check_and_remove([H2|T2],H1,NewSet2,RemoveSuccesful), |
| 297 | | %% print(removed(H1,H2,T2,NewSet2,RemoveSuccesful)), %% |
| 298 | | eq_cons2(RemoveSuccesful,H1,T1,H2,T2,NewSet2,Res). |
| 299 | | eq_cons(avl_set(A),H1,T1,Res) :- !, |
| 300 | | (var(Res) -> kernel_tools:ground_value_check(H1,GrH1) ; true), % if Res already bound, no need to do ground check |
| 301 | | eq_cons_avl_set(A,H1,T1,Res,GrH1). |
| 302 | | eq_cons(global_set(G),_H,T,Res) :- %print(chk(G,H,T)),nl, |
| 303 | | is_infinite_global_set(G,_),!, |
| 304 | | expand_custom_set_to_list(T,_ET,_Done,eq_cons), % this will either succeed and we have a finite list ; or it will raise an enumeration warning exception |
| 305 | | Res = pred_false. |
| 306 | | eq_cons(ES,H1,T1,Res) :- is_custom_explicit_set(ES,eq_cons),expand_custom_set(ES,ExpSet), |
| 307 | | eq_cons1(ExpSet,H1,T1,Res). |
| 308 | | |
| 309 | | % this treatment is relevant for avoiding unnecessary choice points |
| 310 | | % 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 |
| 311 | | :- block eq_cons_avl_set(?,?,?,-,-). |
| 312 | ? | eq_cons_avl_set(A,H1,T1,Res,_) :- Res==pred_true,!, |
| 313 | ? | kernel_objects:equal_custom_explicit_set_cons_wf(avl_set(A),H1,T1,no_wf_available). |
| 314 | | eq_cons_avl_set(A,H1,T1,Res,_) :- |
| 315 | | element_can_be_added_or_removed_to_avl(H1),!, % should hopefully be true as H1 is now ground |
| 316 | | (remove_element_from_explicit_set(avl_set(A),H1,RA) |
| 317 | | -> equality_objects_with_expansion(T1,RA,Res) %%% PROBLEM: T1 has to be in list form ! |
| 318 | | ; Res = pred_false |
| 319 | | ). |
| 320 | | eq_cons_avl_set(A,H1,T1,Res,_) :- |
| 321 | | % 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 |
| 322 | | expand_custom_set(avl_set(A),ExpSet), |
| 323 | | eq_cons1(ExpSet,H1,T1,Res). |
| 324 | | |
| 325 | | :- block eq_cons1(-,?,?,?). |
| 326 | | eq_cons1(ExpSet,H1,T1,Res) :- eq_cons(ExpSet,H1,T1,Res). |
| 327 | | |
| 328 | | :- block eq_cons2(-, ?,?,?,?, ?,-). |
| 329 | | eq_cons2(RemoveSuccesful, H1,T1,H2,T2, _NewSet2,Res) :- var(RemoveSuccesful),!, |
| 330 | | % result has been instantiated before Remove finished; now force equal_object or not_equal_object |
| 331 | | % note: without this the remove could be pending (see test 1112, 1105) |
| 332 | | % TO DO: look whether we could force remove and continue from there ? |
| 333 | | equality_objects2([H1|T1],[H2|T2],Res). |
| 334 | | eq_cons2(not_successful, _,_T1,_,_, _NewSet2,pred_false). |
| 335 | | eq_cons2(successful, _, T1,_,_, NewSet2,Res) :- equality_objects(T1,NewSet2,Res). |
| 336 | | |
| 337 | | :- block check_and_remove(-,?,?,?). |
| 338 | | check_and_remove([],_,ResultingSet,Res) :- !, ResultingSet=[],Res=not_successful. |
| 339 | | check_and_remove([H|T],ElementToRemove,ResultingSet,Res) :- !, |
| 340 | | equality_objects(H,ElementToRemove,RH), |
| 341 | | %%print(equality_objects_result(H,ElementToRemove,RH)),nl, |
| 342 | | check_and_remove2(RH,H,T,ElementToRemove,ResultingSet,Res). |
| 343 | | check_and_remove(CS,ElementToRemove,ResultingSet,Res) :- |
| 344 | | expand_custom_set_to_list(CS,ESet,_,check_and_remove), |
| 345 | | check_and_remove(ESet,ElementToRemove,ResultingSet,Res). |
| 346 | | |
| 347 | | :- block check_and_remove2(-,?,?,?,?,?). |
| 348 | | check_and_remove2(pred_true, _H,T,_ElementToRemove,T,successful). |
| 349 | | check_and_remove2(pred_false,H,T,ElementToRemove,[H|RT],Res) :- |
| 350 | | check_and_remove(T,ElementToRemove,RT,Res). |
| 351 | | |
| 352 | | |
| 353 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:and_equality(pred_false,pred_false,pred_false))). |
| 354 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:and_equality(pred_true,pred_false,pred_false))). |
| 355 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:and_equality(pred_true,pred_true,pred_true))). |
| 356 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_true,pred_true,pred_false))). |
| 357 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_true,pred_false,pred_true))). |
| 358 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_false,pred_true,pred_true))). |
| 359 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:and_equality(pred_false,pred_false,pred_true))). |
| 360 | | :- block and_equality(-,-,-). |
| 361 | | and_equality(X,Y,Res) :- |
| 362 | | ( X==pred_true -> Res=Y |
| 363 | | ; X==pred_false -> Res=pred_false |
| 364 | | ; Y==pred_true -> Res=X |
| 365 | | ; Y==pred_false -> Res=pred_false |
| 366 | | ; Res==pred_true -> X=pred_true, Y=pred_true |
| 367 | | ; 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 |
| 368 | | ; add_error_fail(and_equality,'Illegal call: ',and_equality(X,Y,Res)) |
| 369 | | ). |
| 370 | | :- block and_equality2(-,-,?). |
| 371 | | and_equality2(X,Y,Res) :- |
| 372 | | ( X==pred_true -> Res=Y |
| 373 | | ; X==pred_false -> Res=pred_false |
| 374 | | ; Y==pred_true -> Res=X |
| 375 | | ; Y==pred_false -> Res=pred_false |
| 376 | | ; add_error_fail(and_equality,'Illegal call: ',and_equality2(X,Y,Res)) |
| 377 | | ). |
| 378 | | |
| 379 | | /* |
| 380 | | :- block bool_eq_atomic(-,?,?,-). |
| 381 | | bool_eq_atomic(X,Y,OtherY,Res) :- nonvar(Res),!, |
| 382 | | (Res=pred_true -> X=Y ; X=OtherY). |
| 383 | | bool_eq_atomic(X,Y,_,Res) :- X==Y -> Res=pred_true ; Res=pred_false. */ |
| 384 | | |
| 385 | | % a version for base types with just two possible values |
| 386 | | :- block bin_eq_atomic(-,?,-,?,?), bin_eq_atomic(?,-,-,?,?). |
| 387 | | % no need to check for frozen_dif: a dif would instantly trigger instantiation to other value |
| 388 | | % However, we could use when(?=(X,Y) ; nonvar(Res) as trigger ! maybe this would slowdown SATLIB tests ?? |
| 389 | ? | bin_eq_atomic(X,Y,Res,V1,V2) :- nonvar(Res),!, |
| 390 | | %print(forcing_bin_eq_atomic(X,Y,Res,V1,V2)),nl, |
| 391 | ? | (Res=pred_true -> X=Y |
| 392 | | ; %print(bin_dif(X,Y)),nl, |
| 393 | ? | (X=V1,Y=V2 ; X=V2,Y=V1) |
| 394 | | ). % difference with eq_atomic: we now know the value ! |
| 395 | | bin_eq_atomic(X,Y,Res,_,_) :- |
| 396 | | %print(triggering_bin_eq(X,Y,Res)), translate:print_frozen_info(Res),nl, |
| 397 | ? | (X==Y -> Res=pred_true ; Res=pred_false). |
| 398 | | |
| 399 | | eq_atomic(X,Y,_Type,Res) :- nonvar(X),nonvar(Y),!, |
| 400 | | (X=Y -> Res=pred_true ; Res=pred_false). |
| 401 | | eq_atomic(X,Y,_,Res) :- % check for attached dif co-routines; later we should probably use CHR |
| 402 | | frozen_dif(X,Y),!, Res=pred_false. |
| 403 | | eq_atomic(X,Y,Type,Res) :- when((?=(X,Y);nonvar(Res)),eq_atomic2(X,Y,Type,Res)). |
| 404 | | |
| 405 | | % version of eq_atomic without frozen_dif check (if already performed) |
| 406 | | % eq_atomic_simple(X,Y,_Type,Res) :- % in all calling contexts this test is already performed |
| 407 | | % nonvar(X),nonvar(Y),!, (X=Y -> Res=pred_true ; Res=pred_false). |
| 408 | | eq_atomic_simple(X,Y,Type,Res) :- when((?=(X,Y);nonvar(Res)),eq_atomic2(X,Y,Type,Res)). |
| 409 | | |
| 410 | | /* |
| 411 | | Comment: % for integers CLPFD reification will not ground Res if X==Y, need to do when((?=(X,Y)... |
| 412 | | | ?- X in 1..10, Y in 1..10, (X#=Y #<=> Z), X=Y. |
| 413 | | Y = X, |
| 414 | | X in 1..10, |
| 415 | | Z in 0..1 ? */ |
| 416 | | |
| 417 | | eq_atomic2(X,Y,Type,Res) :- nonvar(Res),!, |
| 418 | | (Res=pred_true -> X=Y ; dif(Type,X,Y)). |
| 419 | | eq_atomic2(X,Y,_Type,Res) :- |
| 420 | ? | (X=Y -> Res=pred_true |
| 421 | ? | ; Res=pred_false). |
| 422 | | |
| 423 | | :- use_module(fd_utils_clpfd,[neq_fd/3]). |
| 424 | | dif(boolean,A,B) :- !, bool_pred:negate(A,B). % was: bool_dif(A,B). |
| 425 | | dif(integer,A,B) :- !, integer_dif(A,B). |
| 426 | | dif(global(T),A,B) :- !, neq_fd(A,B,T). |
| 427 | | dif(_,A,B) :- dif(A,B). |
| 428 | | |
| 429 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:integer_dif(0,1))). |
| 430 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:integer_dif(1,1))). |
| 431 | | :- use_module(clpfd_interface,[clpfd_neq/2]). |
| 432 | | integer_dif(A,B) :- clpfd_neq(A,B). % clpfd_neq calls dif on overflow |
| 433 | | |
| 434 | | |
| 435 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:bool_dif(pred_false,pred_true))). |
| 436 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:bool_dif(pred_true,pred_false))). |
| 437 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:bool_dif(pred_true,pred_true))). |
| 438 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:bool_dif(pred_false,pred_false))). |
| 439 | | bool_dif(A,B) :- bool_pred:negate(A,B). |
| 440 | | |
| 441 | | /* old version: |
| 442 | | :- block eq_atomic(-,?,-), eq_atomic(?,-,-). |
| 443 | | eq_atomic(X,Y,Res) :- nonvar(Res),!, |
| 444 | | (Res=pred_true -> X=Y ; dif(X,Y)). |
| 445 | | eq_atomic(X,Y,Res) :- X==Y -> Res=pred_true |
| 446 | | ; Res=pred_false. |
| 447 | | */ |
| 448 | | |
| 449 | | :- use_module(kernel_records,[check_field_name_compatibility/2]). |
| 450 | | :- block equality_fields(-,?,-), equality_fields(?,-,-), equality_fields(-,-,?). |
| 451 | | % if last argument is known we should propagate the field names from one record to another; see test 1289 (Hansen12) |
| 452 | | equality_fields([],[],pred_true). |
| 453 | | equality_fields([field(Name1,V1)|T1],[field(Name2,V2)|T2],Res) :- |
| 454 | | % should we wait for Name1 or Name2 to become nonvar? |
| 455 | | check_field_name_compatibility(Name1,Name2), |
| 456 | | and_equality(RH,RT,Res), |
| 457 | | equality_objects(V1,V2,RH), |
| 458 | | (RH==pred_false -> true |
| 459 | | ; equality_fields(T1,T2,RT)). |
| 460 | | |
| 461 | | |
| 462 | | |
| 463 | | empty_set_test(Set,EqRes) :- kernel_equality:eq_empty_set(Set,EqRes). |
| 464 | | empty_cartesian_product(Set1,Set2,EqRes) :- |
| 465 | | eq_empty_set(Set1,EqRes1), |
| 466 | | (EqRes1==pred_true -> EqRes=pred_true /* avoid inspecting Set2 */ |
| 467 | | ; or_eq_obj(EqRes1,EqRes2,EqRes),eq_empty_set(Set2,EqRes2)). |
| 468 | | |
| 469 | | |
| 470 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:or_eq_obj(pred_false,pred_false,pred_false))). |
| 471 | | :- assert_must_succeed(exhaustive_kernel_check([commutative],kernel_equality:or_eq_obj(pred_false,pred_true,pred_true))). |
| 472 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:or_eq_obj(pred_true,pred_true,pred_true))). |
| 473 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_true,pred_true,pred_false))). |
| 474 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_true,pred_false,pred_false))). |
| 475 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_false,pred_true,pred_false))). |
| 476 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:or_eq_obj(pred_false,pred_false,pred_true))). |
| 477 | | :- block or_eq_obj(-,-,-). |
| 478 | | % very similar to disjoin in b_interpreter_check; no waitflag to instantiate if result false |
| 479 | | or_eq_obj(X,Y,XorY) :- |
| 480 | | ( (X==pred_true ; Y==pred_true) -> XorY=pred_true |
| 481 | | ; XorY==pred_false -> X=pred_false,Y=pred_false |
| 482 | | ; X==pred_false -> XorY = Y |
| 483 | | ; Y==pred_false -> XorY = X |
| 484 | | ; XorY==pred_true -> or_eq_obj2(X,Y) |
| 485 | | ; add_internal_error('Illegal call: ',or_eq_obj(X,Y,XorY)) ). |
| 486 | | :- block or_eq_obj2(-,-). |
| 487 | | or_eq_obj2(X,Y) :- ((X==pred_true; Y=pred_true) -> true |
| 488 | | ; X==pred_false -> Y=pred_true |
| 489 | | ; Y==pred_false -> X=pred_true |
| 490 | | ; add_internal_error('Illegal call: ',or_eq_obj2(X,Y))). |
| 491 | | |
| 492 | | % ------------------------------------------------------------------ |
| 493 | | |
| 494 | | |
| 495 | | % not used at the moment: |
| 496 | | %get_partial_subset_priority(Set,WF,LWF) :- get_partial_set_size(Set,Size), |
| 497 | | % safe_pow2(Size,Prio), |
| 498 | | % get_wait_flag(Prio,psubset(Set),WF,LWF). |
| 499 | | %get_partial_set_priority(Set,WF,LWF) :- get_partial_set_size(Set,Size), |
| 500 | | % get_wait_flag(Size,pset(Set),WF,LWF). |
| 501 | | %get_partial_set_size(X,R) :- var(X),!,R=3. |
| 502 | | %get_partial_set_size([],R) :- !,R=0. |
| 503 | | %get_partial_set_size([_|T],R) :- !,get_partial_set_size(T,RT), R is RT+1. |
| 504 | | %get_partial_set_size(_,10). |
| 505 | | |
| 506 | | |
| 507 | | get_cardinality_wait_flag(Set,Info,WF,LWF) :- |
| 508 | | get_cardinality_wait_flag(Set,Info,WF,_Card,LWF). |
| 509 | | get_cardinality_wait_flag(Set,Info,WF,Card,LWF) :- |
| 510 | | cardinality_as_int_for_wf(Set,Card), |
| 511 | | % when(nonvar(X), (print(get_card_waitflag(X,Set,WF,LWF)),nl)), |
| 512 | | (var(Card) |
| 513 | | -> kernel_waitflags:get_last_wait_flag(get_cardinality_wait_flag(Info),WF,LastWF) |
| 514 | | ; true), % ensure that we trigger choice points waiting on LWF before infinite enumeration starts |
| 515 | | get_cardinality_wait_flag2(Card,Info,WF,LastWF,LWF). |
| 516 | | :- block get_cardinality_wait_flag2(-,?,?,-,?). |
| 517 | | get_cardinality_wait_flag2(X,_Info,_WF,LastWF,LWF) :- var(X),!,LWF=LastWF. |
| 518 | | get_cardinality_wait_flag2(X,Info,WF,_,LWF) :- get_bounded_wait_flag(X,Info,WF,LWF). |
| 519 | | |
| 520 | | get_cardinality_powset_wait_flag(Set,Info,WF,CardSet,LWF) :- |
| 521 | | cardinality_as_int_for_wf(Set,CardSet), |
| 522 | | get_cardinality_powset_wait_flag2(CardSet,Info,WF,LWF). |
| 523 | | :- block get_cardinality_powset_wait_flag2(-,?,?,?). |
| 524 | | get_cardinality_powset_wait_flag2(X,Info,WF,LWF) :- |
| 525 | | priority_pow2(X,X2), |
| 526 | | %safe_mul(X2,10000,X3), % as generating subsets this way will generate repetitions |
| 527 | | %print(powset_waitflag(X,X2)),nl, |
| 528 | | (X2=inf |
| 529 | | -> integer_pow2_priority(R), get_wait_flag(R,powset_card(Info),WF,LWF) |
| 530 | | ; get_bounded_wait_flag(X2,powset_card(Info),WF,LWF) % finite prio; ensure we do not exceed infinite prios if X2 very large |
| 531 | | ). |
| 532 | | |
| 533 | | priority_pow2(X,R) :- X==inf,!, R=inf. %R=10000010. % TO DO: provide a separate module for combining priorities in a systematic way ! |
| 534 | | priority_pow2(X,R) :- safe_pow2(X,R). |
| 535 | | |
| 536 | | % CARDINALITY FOR NUMBER OF PARTIAL FUNCTIONS: (not used at the moment) |
| 537 | | %get_cardinality_partial_function_wait_flag(DomSet,RanSet,Info,WF,CardDomSet,CardRanSet,LWF) :- |
| 538 | | % cardinality_as_int_for_wf(DomSet,CardDomSet), |
| 539 | | % cardinality_as_int_for_wf(RanSet,CardRanSet), |
| 540 | | % get_cardinality_partial_function_wait_flag(CardDomSet,CardRanSet,Info,WF,LWF). |
| 541 | | %:- block get_cardinality_partial_function_wait_flag(-,?,?,?,?), |
| 542 | | % get_cardinality_partial_function_wait_flag(?,-,?,?,?). |
| 543 | | %get_cardinality_partial_function_wait_flag(DC,RC,Info,WF,LWF) :- |
| 544 | | % priority_pow1n(RC,DC,PFCARD), print(prio(PFCARD)),nl, |
| 545 | | % get_bounded_wait_flag(PFCARD,powset_card(Info),WF,LWF). |
| 546 | | % % Cardinality of the set of partial functions : (card(Range)+1)^card(Domain) |
| 547 | | %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 ! |
| 548 | | %priority_pow1n(X,Y,RR) :- X1 is X+1, safe_pown(X1,Y,R), |
| 549 | | % (R==inf -> integer_pow2_priority(RR) %RR=10000010 |
| 550 | | % ; RR=R). |
| 551 | | |
| 552 | | % CARDINALITY FOR NUMBER OF RELATIONS: |
| 553 | | get_cardinality_relation_over_wait_flag(Dom,Ran,WF,LWF,MaxCardOfRel,MaxNrOfRels) :- |
| 554 | | cardinality_as_int_for_wf(Dom,X), |
| 555 | | cardinality_as_int_for_wf(Ran,Y), |
| 556 | | get_cardinality_relation_over_wait_flag2(X,Y,WF,LWF,MaxCardOfRel,MaxNrOfRels). |
| 557 | | |
| 558 | | :- block get_cardinality_relation_over_wait_flag2(-,?,?,?,?,?), get_cardinality_relation_over_wait_flag2(?,-,?,?,?,?). |
| 559 | | get_cardinality_relation_over_wait_flag2(X,Y,WF,LWF,MaxCardOfRel,MaxNrOfRels1) :- |
| 560 | | safe_mul(X,Y,MaxCardOfRel), |
| 561 | | safe_pow2(MaxCardOfRel,MaxNrOfRels), |
| 562 | | safe_add(MaxNrOfRels,1,MaxNrOfRels1), /* add 1 to give priority to tighter_enum */ |
| 563 | | % print(get_rel_card(X,Y,XY2)),nl, |
| 564 | | get_bounded_wait_flag(MaxNrOfRels1,powset_rel_card,WF,LWF). |
| 565 | | |
| 566 | | % ------------------------------------------------------------------ |
| 567 | | |
| 568 | | :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(2),pred_true,WF),WF)). |
| 569 | | :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(1),pred_true,WF),WF)). |
| 570 | | :- 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)). |
| 571 | | :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(3),pred_false,WF),WF)). |
| 572 | | :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_equality:membership_test_wf([],int(3),pred_false,WF),WF)). |
| 573 | | :- assert_must_succeed(exhaustive_kernel_fail_check_wf(kernel_equality:membership_test_wf([int(2),int(1)],int(3),pred_true,WF),WF)). |
| 574 | | :- assert_must_succeed((membership_test_wf([int(2),int(1)],int(2),R,_WF),R==pred_true)). |
| 575 | | :- assert_must_succeed((membership_test_wf([int(2),int(1)],int(X),R,_WF),var(R),X=1,R==pred_true)). |
| 576 | | :- assert_must_succeed((membership_test_wf([int(2),int(1)],int(3),R,_WF),R==pred_false)). |
| 577 | | :- assert_must_succeed((membership_test_wf(global_set('Name'),fd(1,'Name'),R,_WF),R==pred_true)). |
| 578 | | |
| 579 | | :- 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)), |
| 580 | | 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)). |
| 581 | | :- assert_must_succeed(( |
| 582 | | 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))])], |
| 583 | | 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 |
| 584 | | )). |
| 585 | | /* A function that instantiates last argument when membership test can be decided */ |
| 586 | | membership_test(Set,X,Res) :- print(obsolete_membership_without_wf(Set,X,Res)),nl, |
| 587 | | membership_test_wf(Set,X,Res,_WF). |
| 588 | | |
| 589 | | % a version which also creates a choice point in SMT mode |
| 590 | | membership_test_wf_with_force(Set,X,Res,WF) :- |
| 591 | | membership_test_wf(Set,X,Res,outer,WF), |
| 592 | | (var(Res),preferences:preference(use_smt_mode,true) |
| 593 | | -> get_last_wait_flag(membership_test_wf,WF,LWF), |
| 594 | | force_equality_result(Res,LWF) |
| 595 | | ; true). |
| 596 | | :- block force_equality_result(-,-). |
| 597 | | force_equality_result(pred_true,_). |
| 598 | | force_equality_result(pred_false,_). |
| 599 | | |
| 600 | ? | membership_test_wf(Set,X,Res,WF) :- membership_test_wf(Set,X,Res,outer,WF). |
| 601 | | |
| 602 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
| 603 | | :- if(environ(prob_data_validation_mode,true)). |
| 604 | | :- block membership_test_wf(-,?,?,?,?). % avoid instantiating Set |
| 605 | | :- else. |
| 606 | | :- block membership_test_wf(-,?,-,?,?). |
| 607 | | :- endif. |
| 608 | | membership_test_wf(Set,X,Res,_OuterInner,WF) :- var(Set),!, |
| 609 | | (Res==pred_true |
| 610 | | -> call_check_element_of_wf0(X,Set,WF) |
| 611 | | /* (kernel_objects:unbound_variable_for_cons(Set) |
| 612 | | -> kernel_objects:mark_as_non_free(X), % attach co-routine to indicate that we cannot freely chose X |
| 613 | | print(instantiate_set(Set,X,Res)),nl, |
| 614 | | Set=[X|_] % TO DO: normalise X first ? |
| 615 | | ; when(nonvar(Set), membership_test_wf2(Set,X,Res,OuterInner,WF)) |
| 616 | | ) */ |
| 617 | | ; membership_not_el(Set,X,WF)). |
| 618 | | membership_test_wf(Set,X,Res,OuterInner,WF) :- |
| 619 | ? | membership_test_wf2(Set,X,Res,OuterInner,WF). |
| 620 | | |
| 621 | | % we are not sure if WF0 is set; go via kernel_mappings: |
| 622 | | call_check_element_of_wf0(X,Set,WF) :- get_wait_flag0(WF,WF0), |
| 623 | | kernel_mappings:check_element_of_wf0(X,Set,WF,WF0,unknown). |
| 624 | | |
| 625 | | |
| 626 | | :- block membership_not_el(-,?,?). |
| 627 | | membership_not_el([],_,_WF) :- !. |
| 628 | | membership_not_el([H|T],X,WF) :- !, |
| 629 | | not_equal_object_wf(H,X,WF), |
| 630 | | membership_not_el(T,X,WF). |
| 631 | | membership_not_el(avl_set(A),X,WF) :- !,membership_custom_set_wf(avl_set(A),X,pred_false,WF). |
| 632 | | membership_not_el(CS,X,WF) :- is_custom_explicit_set_nonvar(CS),!, |
| 633 | | membership_custom_set_wf(CS,X,pred_false,WF). |
| 634 | | |
| 635 | ? | membership_test_wf2([],_X,Res,_,_WF) :- !, Res=pred_false. |
| 636 | ? | membership_test_wf2([H|T],X,Res,OuterInner,WF) :- !, |
| 637 | ? | (Res==pred_false |
| 638 | | -> not_equal_object_wf(H,X,WF), membership_test_wf(T,X,Res,WF) |
| 639 | ? | ; T==[] -> equality_objects(H,X,Res) |
| 640 | | % TO DO: at the outer level we could check whether the list has the same length as the type of X |
| 641 | | ; OuterInner=outer, is_definitely_maximal_set([H|T]) -> Res=pred_true |
| 642 | | ; (OuterInner=outer, % avoid re-checking ground_list_with_fd over and over again |
| 643 | | preferences:preference(use_clpfd_solver,true), |
| 644 | | ground_list_with_fd([H|T]), |
| 645 | | construct_avl_from_lists([H|T],CS)) |
| 646 | | % 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 |
| 647 | | % TO DO: call clpfd_reify_inlist directly ? avoid translating to AVL and back to list; detect maximal list |
| 648 | | -> membership_custom_set_wf(CS,X,Res,WF) %, print(conv_to_avl(X,[H|T],CS,Res)),nl |
| 649 | | ; %print(eq(Res,H,X,T,WF)),nl,equality_objects_wf_dbg(H,X,HXRes,WF), % makes test 1003 : plavis-MemoryLoad_SP_55 fail |
| 650 | | equality_objects(H,X,HXRes),cons_el_of(HXRes,T,X,Res,WF) |
| 651 | | % ,(var(HXRes) -> print(mem(X,[H|T],Res)), tools_printing:print_arg(X),nl ; true) |
| 652 | | ). |
| 653 | ? | membership_test_wf2(avl_set(A),X,Res,_,WF) :- !, membership_avl_set_wf(A,X,Res,WF). |
| 654 | | membership_test_wf2(CS,X,Res,_,WF) :- is_custom_explicit_set(CS,membership_test_wf),!, |
| 655 | | membership_custom_set_wf(CS,X,Res,WF). |
| 656 | | membership_test_wf2(Z,X,Res,OuterInner,WF) :- |
| 657 | | add_error_fail(membership_test_wf,'Not Set as first argument: ', membership_test_wf(Z,X,Res,OuterInner,WF)). |
| 658 | | |
| 659 | | % detect certain lists containing FD values and convert them to avl sets: they have improved reification and can detect when a list is complete |
| 660 | | ground_list_with_fd(V) :- var(V),!,fail. |
| 661 | | ground_list_with_fd([H|T]) :- nonvar(H),ground_val(H),ground_list_with_fd(T). |
| 662 | | ground_list_with_fd([]). |
| 663 | | |
| 664 | | :- use_module(kernel_tools,[ground_value/1]). |
| 665 | | ground_val(int(X)) :- number(X). |
| 666 | | ground_val(pred_false). |
| 667 | | ground_val(pred_true). |
| 668 | | ground_val(fd(X,T)) :- number(X),ground(T). |
| 669 | | ground_val((A,B)) :- nonvar(A),ground_val(A),ground_value(B). |
| 670 | | ground_val(rec(Fields)) :- nonvar(Fields), Fields = [field(Name,V)|TFields], ground(Name), |
| 671 | | ground_val(V), |
| 672 | | ground_value(rec(TFields)). |
| 673 | | % TO DO: add more checks; do we need this check ? related to is_avl_fd_index_set |
| 674 | | |
| 675 | | :- block cons_el_of(-,?,?,-,?). |
| 676 | | cons_el_of(HX_EQRES,T,X,MEMRES,WF) :- var(HX_EQRES),!, %print(cons_el_of(HX_EQRES,T,X,MEMRES)),nl, |
| 677 | | (MEMRES=pred_false -> HX_EQRES=pred_false, /* otherwise element of set */ |
| 678 | | membership_not_el(T,X,WF) |
| 679 | | % MEMRES must be pred_true |
| 680 | | ; (T==[] -> %print(forcing_cons_el_of(T,X,MEMRES)),nl, |
| 681 | | HX_EQRES=pred_true |
| 682 | | ; cons_el_of_mem_obj(HX_EQRES,T,X,WF)) /* we have to wait for result of comparison with X */ |
| 683 | | ). |
| 684 | | cons_el_of(pred_true,_,_,pred_true,_WF). |
| 685 | | cons_el_of(pred_false,T,X,Res,WF) :- (Res==pred_true -> T=[_|_] ; true), |
| 686 | | membership_test_wf(T,X,Res,inner,WF). |
| 687 | | |
| 688 | | :- block cons_el_of_mem_obj(-,?,?,?). |
| 689 | | cons_el_of_mem_obj(pred_true,_,_,_WF). |
| 690 | | cons_el_of_mem_obj(pred_false,T,X,WF) :- |
| 691 | | % Instantiation of T will be done by membership_test_wf, relevant for test 1273 |
| 692 | | membership_test_wf(T,X,pred_true,inner,WF). |
| 693 | | |
| 694 | | |
| 695 | | :- assert_must_succeed((kernel_equality:cartesian_pair_test_wf((int(1),int(1)), |
| 696 | | [int(1),int(2)],[int(2),int(3)],R,_WF),R==pred_false)). |
| 697 | | :- assert_must_succeed((kernel_equality:cartesian_pair_test_wf((int(3),int(1)), |
| 698 | | [int(1),int(2)],[int(2),int(3)],R,_WF),R==pred_false)). |
| 699 | | :- assert_must_succeed((kernel_equality:cartesian_pair_test_wf((int(2),int(3)), |
| 700 | | [int(1),int(2)],[int(2),int(3)],R,_WF),R==pred_true)). |
| 701 | | :- assert_must_fail((kernel_equality:cartesian_pair_test_wf((int(1),int(3)), |
| 702 | | [int(1),int(2)],[int(2),int(3)],pred_false,_WF))). |
| 703 | | |
| 704 | | cartesian_pair_test_wf((X,Y),XType,YType,Res,WF) :- check_cartesian_pair1(X,XType,Y,YType,Res,WF). |
| 705 | | |
| 706 | | :- block check_cartesian_pair1(-,?,-,?,-,?). |
| 707 | | %check_cartesian_pair1(X,XType,Y,YType,Res) :- Res==pred_true,!, |
| 708 | | % is_cartesian_pair_wf((X,Y),XType,YType,WF). |
| 709 | | %check_cartesian_pair1(X,XType,Y,YType,Res) :- Res==pred_false,!, |
| 710 | | % not_is_cartesian_pair((X,Y),XType,YType,WF). |
| 711 | | check_cartesian_pair1(X,XType,Y,YType,Res,WF) :- |
| 712 | ? | ((var(X),nonvar(Y)) -> check_cartesian_pair2(Y,YType,X,XType,Res,WF) |
| 713 | ? | ; check_cartesian_pair2(X,XType,Y,YType,Res,WF)). |
| 714 | | |
| 715 | ? | check_cartesian_pair2(X,XType,Y,YType,Res,WF) :- prop_pred_true(Res,MemResX), |
| 716 | ? | membership_test_wf(XType,X,MemResX,WF), |
| 717 | ? | ((var(MemResX), is_definitely_maximal_set(YType)) % TO DO: maybe actually also call membership_test_wf |
| 718 | | -> Res=MemResX |
| 719 | ? | ; check_cartesian_pair3(MemResX,Y,YType,Res,WF)). |
| 720 | | |
| 721 | | :- block check_cartesian_pair3(-,?,?,?,?). |
| 722 | ? | check_cartesian_pair3(pred_true,Y,YType,Res,WF) :- membership_test_wf(YType,Y,Res,WF). |
| 723 | | check_cartesian_pair3(pred_false,_Y,_YType,pred_false,_WF). |
| 724 | | |
| 725 | | :- block prop_pred_true(-,?). |
| 726 | | prop_pred_true(pred_true,pred_true). |
| 727 | | prop_pred_true(pred_false,_). |
| 728 | | |
| 729 | | |
| 730 | | |
| 731 | | |
| 732 | | |
| 733 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:in_nat_range_test(int(9),int(10),int(12),pred_false))). |
| 734 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:in_nat_range_test(int(11),int(10),int(12),pred_true))). |
| 735 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:in_nat_range_test(int(22),int(22),int(22),pred_true))). |
| 736 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:in_nat_range_test(int(22),int(22),int(21),pred_false))). |
| 737 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:in_nat_range_test(int(9),int(10),int(12),pred_true))). |
| 738 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:in_nat_range_test(int(22),int(22),int(22),pred_false))). |
| 739 | | :- assert_must_succeed((in_nat_range_test(X,int(11),int(12),pred_false), X=int(10) )). |
| 740 | | :- assert_must_succeed((kernel_equality:in_nat_range_test(X,int(11),int(12),pred_false), X=int(13) )). |
| 741 | | :- assert_must_succeed((in_nat_range_test(X,int(11),int(12),pred_true), X=int(11) )). |
| 742 | | :- assert_must_succeed((kernel_equality:in_nat_range_test(int(11),X,int(12),pred_true), X=int(11) )). |
| 743 | | :- assert_must_succeed((in_nat_range_test(int(11),X,int(12),pred_false), X=int(12) )). |
| 744 | | :- assert_must_succeed((kernel_equality:in_nat_range_test(int(11),int(10),int(12),R), R==pred_true )). |
| 745 | | :- assert_must_fail((kernel_equality:in_nat_range_test(int(11),int(10),int(12),pred_false))). |
| 746 | | |
| 747 | | in_nat_range_test(int(X),int(Y),int(Z),Res) :- in_nat_range_test1(X,Y,Z,Res). |
| 748 | | |
| 749 | | in_nat_range_test1(X,Y,Z,Res) :- number(X),number(Y),number(Z),!, |
| 750 | | % for improved performance, e.g., inside large set differences with intervals |
| 751 | | ( X < Y -> Res = pred_false |
| 752 | | ; X > Z -> Res = pred_false |
| 753 | | ; Res = pred_true). |
| 754 | | % this clause does not seem to add any power: (x:x..x <=> b=TRUE) already determines b=TRUE deterministically |
| 755 | | %in_nat_range_test1(X,Y,Z,ResYZ) :- Y==Z, !, print(in_nat_eq_obj(X,Y,ResYZ)),nl, |
| 756 | | % equality_objects(int(X),int(Y),ResYZ). |
| 757 | | in_nat_range_test1(X,Y,Z,ResYZ) :- |
| 758 | | prop_eq_01(ResYZ,R01), |
| 759 | | % print(posting((X#>=Y #/\ X#=<Z) #<=> R01)),nl, |
| 760 | | % TO DO: check CHR + possibly X==Y or X==Z |
| 761 | | clpfd_interface:try_post_constraint(clpfd:'#<=>'( (X#>=Y #/\ X#=<Z) , R01)), % reify constraint if CLP(FD) active |
| 762 | | % print(in_nat_range_test(X,Y,Z,R01,ResYZ)),nl, |
| 763 | | %was : convert_eq_to_mem(RYZ,Res), |
| 764 | | and_equality(RY,RZ,ResYZ), |
| 765 | | geq_test(X,Y,RY), |
| 766 | | geq_test(Z,X,RZ). |
| 767 | | |
| 768 | | :- block geq_test(?,-,-),geq_test(-,?,-). |
| 769 | | geq_test(X,Y,Res) :- % TO DO: use CHR ? |
| 770 | | ( Res==pred_true -> kernel_objects:less_than_equal_direct(Y,X) |
| 771 | | ; Res==pred_false -> kernel_objects:less_than_direct(X,Y) |
| 772 | | ; X >= Y -> Res=pred_true |
| 773 | | ; Res = pred_false |
| 774 | | ). |
| 775 | | |
| 776 | | |
| 777 | | |
| 778 | | /* SUBSET CHECK REIFICATION */ |
| 779 | | |
| 780 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:subset_test([int(2)],[],pred_false,_WF))). |
| 781 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:subset_test([int(2),int(1)],[int(2)],pred_false,_WF))). |
| 782 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:subset_test([int(2),int(1)],[int(2)],pred_true,_WF))). |
| 783 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:subset_test([int(2),int(1)],[int(2),int(1)],pred_true,_WF))). |
| 784 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:subset_test([int(2),int(1)],[int(2),int(1),int(3)],pred_true,_WF))). |
| 785 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:subset_test([int(2),int(1)],global_set('NATURAL1'),pred_true,_WF))). |
| 786 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:subset_test([],[int(2),int(1)],pred_true,_WF))). |
| 787 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:subset_test([],[int(2),int(1)],pred_false,_WF))). |
| 788 | | :- assert_must_succeed((kernel_equality:subset_test([],[int(3)],R,_WF),R==pred_true)). |
| 789 | | :- assert_must_succeed((kernel_equality:subset_test([int(2),int(1)],[int(2),int(1),int(3)],R,_WF),R==pred_true)). |
| 790 | | :- assert_must_succeed((kernel_equality:subset_test([int(2),int(1),int(4)],[int(2),int(1),int(3)],R,_WF),R==pred_false)). |
| 791 | | :- assert_must_succeed((kernel_equality:subset_test([int(222),int(1)],global_set('NATURAL'),R,_WF),R==pred_true)). |
| 792 | | :- assert_must_succeed((kernel_equality:subset_test([int(222),int(1)],global_set('NATURAL1'),R,_WF),R==pred_true)). |
| 793 | | :- assert_must_succeed((kernel_equality:subset_test([int(222),int(1),int(0)],global_set('NATURAL1'),R,_WF),R==pred_false)). |
| 794 | | :- assert_must_succeed((kernel_equality:subset_test([int(222),int(1),int(0)],X,R,_WF),X=global_set('NATURAL1'),R==pred_false)). |
| 795 | | :- assert_must_succeed((kernel_equality:subset_test([int(222),int(-11)],global_set('INTEGER'),R,_WF),R==pred_true)). |
| 796 | | :- assert_must_succeed((kernel_equality:subset_test([int(222),int(-11)],global_set('INTEGER'),R,_WF),R==pred_true)). |
| 797 | | :- assert_must_succeed((kernel_equality:subset_test(global_set('INTEGER'),global_set('NATURAL1'),R,_WF),R==pred_false)). |
| 798 | | :- assert_must_succeed((kernel_equality:subset_test(global_set('NATURAL1'),global_set('NATURAL1'),R,_WF),R==pred_true)). |
| 799 | | |
| 800 | | :- use_module(kernel_objects,[check_subset_of_wf/3, not_subset_of_wf/3, |
| 801 | | check_subset_of_global_sets/2, check_not_subset_of_global_sets/2, |
| 802 | | both_global_sets/4]). |
| 803 | | |
| 804 | | :- use_module(custom_explicit_sets,[expand_custom_set_to_list/4, expand_custom_set_to_list_wf/5, |
| 805 | | is_definitely_maximal_set/1]). |
| 806 | | :- block subset_test(-,-,-,?). |
| 807 | | subset_test(_S1,S2,R,_WF) :- % tools_printing:print_term_summary(subset_test(_S1,S2,R,WF)), %% |
| 808 | | is_definitely_maximal_set(S2),!,R=pred_true. |
| 809 | | subset_test(S1,S2,R,WF) :- subset_test0(S1,S2,R,WF). |
| 810 | | |
| 811 | | :- block subset_test0(-,?,-,?). |
| 812 | | subset_test0(S1,S2,R,WF) :- % tools_printing:print_term_summary(subset_test0(S1,S2,R,WF)), %% |
| 813 | | nonvar(R),!, |
| 814 | | (R==pred_true -> check_subset_of_wf(S1,S2,WF) |
| 815 | | ; R==pred_false -> not_subset_of_wf(S1,S2,WF) |
| 816 | | ; add_error_fail(subset_test0,'Illegal result value: ',R)). |
| 817 | | subset_test0([],_,R,_WF) :- !,R=pred_true. |
| 818 | | subset_test0(S1,S2,R,WF) :- subset_test1(S1,S2,R,WF). |
| 819 | | |
| 820 | | |
| 821 | | :- use_module(coverage_tools_annotations,['$NOT_COVERED'/1]). |
| 822 | | |
| 823 | | :- block subset_test1(-,?,-,?),subset_test1(?,-,-,?). |
| 824 | | subset_test1(S1,S2,R,WF) :- nonvar(R),!, |
| 825 | | (R==pred_true -> check_subset_of_wf(S1,S2,WF) ; not_subset_of_wf(S1,S2,WF)). |
| 826 | | subset_test1([],_,R,_WF) :- !,R=pred_true, '$NOT_COVERED'('cannot be covered'). /* cannot be covered; emtpy set treated above */ |
| 827 | | subset_test1(Set1,Set2,R,_WF) :- both_global_sets(Set1,Set2,G1,G2),!, % also deals with two intervals |
| 828 | | % print(test_subset_of_global_sets(G1,G2,R)),nl, |
| 829 | | test_subset_of_global_sets(G1,G2,R). |
| 830 | | subset_test1(_Set1,Set2,R,_WF) :- |
| 831 | | is_definitely_maximal_set(Set2),!, % TO DO: avoid checking it again if have already checked it above in subset_test |
| 832 | | R=pred_true. |
| 833 | | subset_test1(Set1,Set2,R,_WF) :- Set2==[],!, eq_empty_set(Set1,R). |
| 834 | | subset_test1(Set1,Set2,R,WF) :- test_subset_of_explicit_set(Set1,Set2,R,WF,Code),!, |
| 835 | | call(Code). |
| 836 | | subset_test1(Set1,Set2,R,WF) :- |
| 837 | | expand_custom_set_to_list_wf(Set1,ESet1,_,subset_test1,WF), |
| 838 | | subset_test2(ESet1,Set2,R,WF). |
| 839 | | |
| 840 | | :- block subset_test2(-,?,?,?). |
| 841 | | subset_test2([],_,R,_WF) :- !, R=pred_true. |
| 842 | | subset_test2([H|T],Set2,R,WF) :- |
| 843 | | membership_test_wf(Set2,H,MemRes,WF), |
| 844 | | subset_test3(MemRes,T,Set2,R,WF). |
| 845 | | |
| 846 | | :- block subset_test3(-,?,?,?,?). |
| 847 | | subset_test3(pred_false,_T,_Set2,R,_WF) :- R=pred_false. |
| 848 | | subset_test3(pred_true,T,Set2,R,WF) :- subset_test2(T,Set2,R,WF). |
| 849 | | |
| 850 | | %:- block test_subset_of_global_sets(-,?,?), not_subset_of_global_sets(?,-,?). |
| 851 | | %test_subset_of_global_sets(interval(Low1,Up1),interval(Low2,Up2)) :- !, test_interval_subset(Low1,Up1,Low2,Up2). |
| 852 | | test_subset_of_global_sets(G1,G2,R) :- G1==G2,!,R=pred_true. |
| 853 | | test_subset_of_global_sets(G1,G2,R) :- %print(check_subset(G1,G2)),nl, |
| 854 | | when((nonvar(R);(ground(G1),ground(G2))),test_subset_of_global_sets_aux(G1,G2,R)). |
| 855 | | % TO DO: provide better reified version, especially for intervals with variables ! |
| 856 | | % e.g., 1..x <: NATURAL1 ==> R=pred_true, ... |
| 857 | | test_subset_of_global_sets_aux(G1,G2,R) :- R==pred_true,!, check_subset_of_global_sets(G1,G2). |
| 858 | | test_subset_of_global_sets_aux(G1,G2,R) :- R==pred_false,!, check_not_subset_of_global_sets(G1,G2). |
| 859 | | test_subset_of_global_sets_aux(G1,G2,R) :- |
| 860 | | (check_subset_of_global_sets(G1,G2) -> R=pred_true ; R=pred_false). |
| 861 | | |
| 862 | | % ---------------------------- strict subset reification |
| 863 | | |
| 864 | | |
| 865 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:subset_strict_test([int(2)],[],pred_false,_WF))). |
| 866 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:subset_strict_test([int(2),int(1)],[int(2)],pred_false,_WF))). |
| 867 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:subset_strict_test([int(2),int(1)],[int(2)],pred_true,_WF))). |
| 868 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:subset_strict_test([int(2),int(1)],[int(2),int(1)],pred_false,_WF))). |
| 869 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:subset_strict_test([int(2),int(1)],[int(2),int(1),int(3)],pred_true,_WF))). |
| 870 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:subset_strict_test([int(2),int(1)],global_set('NATURAL1'),pred_true,_WF))). |
| 871 | | :- assert_must_succeed(exhaustive_kernel_check(kernel_equality:subset_strict_test([],[int(2),int(1)],pred_true,_WF))). |
| 872 | | :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_equality:subset_strict_test([],[int(2),int(1)],pred_false,_WF))). |
| 873 | | :- assert_must_succeed((kernel_equality:subset_strict_test([],[int(3)],R,_WF),R==pred_true)). |
| 874 | | :- assert_must_succeed((kernel_equality:subset_strict_test([int(2),int(1)],[int(2),int(1),int(3)],R,_WF),R==pred_true)). |
| 875 | | :- 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)). |
| 876 | | :- assert_must_succeed((kernel_equality:subset_strict_test([int(222),int(1)],global_set('NATURAL'),R,_WF),R==pred_true)). |
| 877 | | :- assert_must_succeed((kernel_equality:subset_strict_test([int(222),int(1)],global_set('NATURAL1'),R,_WF),R==pred_true)). |
| 878 | | :- assert_must_succeed((kernel_equality:subset_strict_test([int(222),int(1),int(0)],global_set('NATURAL1'),R,_WF),R==pred_false)). |
| 879 | | :- assert_must_succeed((kernel_equality:subset_strict_test([int(222),int(1),int(0)],X,R,_WF),X=global_set('NATURAL1'),R==pred_false)). |
| 880 | | :- assert_must_succeed((kernel_equality:subset_strict_test([int(222),int(-11)],global_set('INTEGER'),R,_WF),R==pred_true)). |
| 881 | | :- assert_must_succeed((kernel_equality:subset_strict_test([int(222),int(-11)],global_set('INTEGER'),R,_WF),R==pred_true)). |
| 882 | | :- assert_must_succeed((kernel_equality:subset_strict_test(global_set('INTEGER'),global_set('NATURAL1'),R,_WF),R==pred_false)). |
| 883 | | |
| 884 | | :- assert_must_succeed((kernel_equality:subset_strict_test(global_set('NATURAL1'),global_set('NATURAL1'),R,_WF),R==pred_false)). |
| 885 | | |
| 886 | | :- block subset_strict_test(-,-,-,?). |
| 887 | | subset_strict_test(_S1,S2,R,_WF) :- % tools_printing:print_term_summary(subset_test(_S1,S2,R,WF)), %% |
| 888 | | S2==[],!,R=pred_false. |
| 889 | | subset_strict_test(S1,S2,R,_WF) :- % tools_printing:print_term_summary(subset_test(_S1,S2,R,WF)), %% |
| 890 | | S1==[],!,eq_empty_set(S2,Empty), bool_pred:negate(Empty,R). |
| 891 | | subset_strict_test(S1,S2,R,WF) :- subset_strict_test0(S1,S2,R,WF). |
| 892 | | |
| 893 | | :- use_module(kernel_objects,[strict_subset_of_wf/3, not_strict_subset_of_wf/3]). |
| 894 | | :- block subset_strict_test0(-,?,-,?). |
| 895 | | subset_strict_test0(S1,S2,R,WF) :- % tools_printing:print_term_summary(subset_test0(S1,S2,R,WF)), %% |
| 896 | | nonvar(R),!, |
| 897 | | (R==pred_true -> strict_subset_of_wf(S1,S2,WF) |
| 898 | | ; R==pred_false -> not_strict_subset_of_wf(S1,S2,WF) |
| 899 | | ; add_error_fail(subset_strict_test0,'Illegal result value: ',R)). |
| 900 | | subset_strict_test0(S1,S2,R,WF) :- |
| 901 | | subset_test(S1,S2,IsSubset,WF), |
| 902 | | (IsSubset==pred_false -> R=pred_false |
| 903 | | ; conjoin_test(IsSubset,NotEqual,R,WF), |
| 904 | | bool_pred:negate(NotEqual,Equal), |
| 905 | | equality_objects_wf(S1,S2,Equal,WF) |
| 906 | | ). |
| 907 | | |
| 908 | | conjoin_test(A,B,AB,WF) :- |
| 909 | | conjoin(A,B,AB,b(truth,pred,[]),b(truth,pred,[]),WF). |