| 1 | | % (c) 2009-2023 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
| 2 | | % Heinrich Heine Universitaet Duesseldorf |
| 3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
| 4 | | |
| 5 | | :- module(kernel_mappings, |
| 6 | | [ unary_function/3, |
| 7 | | binary_function/3, binary_arg1_determines_value/3, |
| 8 | | unary_in_boolean_type/2, unary_not_in_boolean_type/2, |
| 9 | | unary_in_definitely_true/2, |
| 10 | | binary_in_boolean_type/2, |
| 11 | | binary_not_in_boolean_type/2, |
| 12 | | binary_in_definitely_true/2, |
| 13 | | cst_in_boolean_type/2, cst_not_in_boolean_type/2, |
| 14 | | binary_boolean_operator/3, |
| 15 | | negate_binary_boolean_operator/2, |
| 16 | | negate_binary_boolean_operator_swap/2, |
| 17 | | symbolic_closure_binary_operator/1, is_definitely_empty/3, do_not_keep_symbolic/5, |
| 18 | | symbolic_closure_unary_operator/1, do_not_keep_symbolic_unary/2, |
| 19 | | |
| 20 | | special_binary_predicate/6, |
| 21 | | |
| 22 | | unary_kernel_call/8, |
| 23 | | binary_kernel_call/9, |
| 24 | | unary_in_kernel_call/6, |
| 25 | | binary_in_kernel_call/7, |
| 26 | | kernel_call_predicate/4, |
| 27 | | kernel_call_predicate_check_element_of_wf/4, kernel_call_predicate_equal_object_optimized/3, |
| 28 | | kernel_call_predicate_not_equal_object/4, |
| 29 | | kernel_call_predicate_not_element_of_wf/3, |
| 30 | | kernel_call/4, |
| 31 | | kernel_call_apply_to/6, |
| 32 | | |
| 33 | | kernel_call_predicate3/7, kernel_call_predicate2/6 |
| 34 | | ]). |
| 35 | | |
| 36 | | % new profiler |
| 37 | | %:- use_module('../extensions/profiler/profiler.pl'). |
| 38 | | %:- use_module('../extensions/profiler/profiler_te.pl'). |
| 39 | | %:- enable_profiling(must_succ_kernel_call/4). |
| 40 | | %:- enable_profiling(kernel_call_predicate/4). |
| 41 | | %:- enable_profiling(kernel_call/4). |
| 42 | | %:- enable_profiling(kernel_call_apply_to/5). |
| 43 | | %:- enable_profiling(kernel_call_or/5). |
| 44 | | |
| 45 | | % old profiler |
| 46 | | %:- use_module(covsrc(hit_profiler), [add_profile_hit/1,add_profile_hit/2]). |
| 47 | | |
| 48 | | :- use_module(tools). |
| 49 | | |
| 50 | | :- use_module(module_information,[module_info/2]). |
| 51 | | :- module_info(group,kernel). |
| 52 | | :- module_info(description,'This module translates AST constructs to calls in the ProB kernel.'). |
| 53 | | |
| 54 | | :- use_module(self_check). |
| 55 | | :- use_module(kernel_waitflags,[get_wait_flag0/2]). |
| 56 | | :- use_module(kernel_tools,[ground_value_check/2, ground_value_opt_check/3]). |
| 57 | | :- use_module(kernel_z). % compaction and bag_items |
| 58 | | |
| 59 | | :- meta_predicate kernel_call_or(0,*,*,*,*). |
| 60 | | :- meta_predicate kernel_call(0,*,*,*). |
| 61 | | |
| 62 | | |
| 63 | | |
| 64 | | unary_kernel_call(Module,KernelFunction,ESV1,Value,WF,Expr,Type,Span) :- |
| 65 | | (expects_waitflag_and_span(KernelFunction) |
| 66 | | -> KernelCall =.. [KernelFunction,ESV1,Value,Span,WF] |
| 67 | | ; expects_waitflag(KernelFunction) -> KernelCall =.. [KernelFunction,ESV1,Value,WF] |
| 68 | | ; KernelCall =.. [KernelFunction,ESV1,Value] |
| 69 | | ), |
| 70 | | (type_ok_for_wf0(Type) -> |
| 71 | ? | Module:KernelCall |
| 72 | | ; reversible_unary_function(KernelFunction) |
| 73 | | -> kernel_call_or(Module:KernelCall,ESV1,Value,WF,Expr) % if either value is bound it is ok to perform call |
| 74 | ? | ; must_succ_kernel_call(Module:KernelCall,ESV1,WF,Expr) |
| 75 | | ). |
| 76 | | |
| 77 | | % result is ok for wf0: no optimized AVL representation exists; we do not need to delay calling function |
| 78 | | type_ok_for_wf0(integer). |
| 79 | | type_ok_for_wf0(boolean). |
| 80 | | type_ok_for_wf0(global(_)). |
| 81 | | type_ok_for_wf0(string). |
| 82 | | |
| 83 | | |
| 84 | | binary_kernel_call(_,KernelFunction,ESV1,ESV2,Value,WF,_Expr,_Type,Span) :- |
| 85 | | determined_binary_integer_function(KernelFunction), |
| 86 | | !, |
| 87 | | get_wait_flag0(WF,WF0), |
| 88 | | call_determined_integer_function(KernelFunction,ESV1,ESV2,Value,WF0,WF,Span). |
| 89 | | %binary_kernel_call(kernel_objects,in_nat_range_wf,ESV1,ESV2,Value,WF,Expr,Type,Span) :- !, |
| 90 | | % in_nat_range_wf(ESV1,ESV2,Value,WF). % a common call; TO DO: provide optimized treatment |
| 91 | | binary_kernel_call(Module,KernelFunction,ESV1,ESV2,Value,WF,Expr,Type,Span) :- |
| 92 | | (expects_waitflag_and_span(KernelFunction) |
| 93 | | -> KernelCall =.. [KernelFunction,ESV1,ESV2,Value,Span,WF] |
| 94 | | ; expects_waitflag(KernelFunction) |
| 95 | | -> KernelCall =.. [KernelFunction,ESV1,ESV2,Value,WF] |
| 96 | | ; expects_waitflag_and_type(KernelFunction) |
| 97 | | -> KernelCall =.. [KernelFunction,ESV1,ESV2,Value,Type,WF] |
| 98 | | ; KernelCall =.. [KernelFunction,ESV1,ESV2,Value] |
| 99 | | ), |
| 100 | | special_propagate_binary_function(KernelFunction,ESV1,ESV2,Value,WF), |
| 101 | ? | must_succ_kernel_call(Module:KernelCall,(ESV1,ESV2),WF,Expr). |
| 102 | | |
| 103 | | % calls for El : BOP(SV1,SV2) where BOP is a binary operator |
| 104 | | binary_in_kernel_call(Module,Kernel_predicate,ElValue,SV1,SV2,WF,_Expr) :- |
| 105 | | get_wait_flag0(WF,WF0), |
| 106 | ? | binary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0). |
| 107 | | |
| 108 | | :- block binary_in_kernel_call2(?,?,-,?,?,?,-). % wait until either WF0 set or ElValue |
| 109 | | binary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0) :- nonvar(WF0),!, |
| 110 | ? | call(Module:Kernel_predicate,ElValue,SV1,SV2,WF). |
| 111 | | binary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0) :- |
| 112 | | not_symbolic_when_var(ElValue,WF0,EWait), |
| 113 | | % ensure that we do not call this in case ElValue is a closure which may need expanding |
| 114 | | binary_in_kernel_call3(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0,EWait). |
| 115 | | |
| 116 | | :- block binary_in_kernel_call3(?,?,?,?,?,?,-,-). |
| 117 | | binary_in_kernel_call3(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0,_EWait) :- nonvar(WF0),!, |
| 118 | ? | call(Module:Kernel_predicate,ElValue,SV1,SV2,WF). |
| 119 | | binary_in_kernel_call3(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0,EWait) :- |
| 120 | | ground_value_check(SV1,G1), |
| 121 | | ground_value_check(SV2,G2), |
| 122 | | % when((nonvar(WF0) ; ground(EWait), nonvar(G1), nonvar(G2)), |
| 123 | | call_nv4(Module:Kernel_predicate,ElValue,SV1,SV2,WF, WF0,EWait,G1,G2). |
| 124 | | |
| 125 | | % wait for either WF0 or all others |
| 126 | | :- block call_nv4(?,?,?,?,?,-,?,?,-),call_nv4(?,?,?,?,?,-,?,-,?),call_nv4(?,?,?,?,?,-,-,?,?). |
| 127 | | call_nv4(Call,A,B,C,D,_WF0,_,_G1,_G2) :- |
| 128 | | call(Call,A,B,C,D). |
| 129 | | |
| 130 | | % trigger WaitVariable before WF0 when first arg is not a symbolic closure and becomes ground |
| 131 | | :- block not_symbolic_when_var(-,-,?). |
| 132 | | not_symbolic_when_var(_,WF0,_) :- nonvar(WF0),!. % WV not required |
| 133 | | not_symbolic_when_var(closure(_,_,_),_,_) :- !. |
| 134 | | not_symbolic_when_var(X,WF0,WV) :- |
| 135 | | % initially used: value_variables(X,WV). % |
| 136 | | ground_value_opt_check(X,WF0,WV). |
| 137 | | % using ground_value_check instead of ground_value_opt_check means that co-routines can remain attached, |
| 138 | | % which means things like enumeration_only_fdvar will fail and lead to issues in tests 1924, 1925, 1492 |
| 139 | | |
| 140 | | unary_in_kernel_call(Module,Kernel_predicate,ElValue,SV1,WF,_Expr) :- |
| 141 | | %KernelCall =.. [Kernel_predicate,ElValue,SV1,WF], |
| 142 | | %kernel_call(Module:KernelCall,(ElValue,SV1),WF,Expr). |
| 143 | | get_wait_flag0(WF,WF0), |
| 144 | ? | unary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,WF,WF0). |
| 145 | | |
| 146 | | :- block unary_in_kernel_call2(?,?,-,?,?,-). % wait until either WF0 set or ElValue |
| 147 | | unary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,WF,WF0) :- nonvar(WF0),!, |
| 148 | ? | call(Module:Kernel_predicate,ElValue,SV1,WF). |
| 149 | | unary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,WF,WF0) :- |
| 150 | | not_symbolic_when_var(ElValue,WF0,EWait), |
| 151 | | % ensure that we do not call this in case ElValue is a closure which may need expanding; |
| 152 | | % then we should at least wait until WF0 is ground |
| 153 | | ground_value_opt_check(SV1,WF0,G1), |
| 154 | ? | call_nv3(Module:Kernel_predicate,ElValue,SV1,WF,WF0,EWait,G1). |
| 155 | | |
| 156 | | % wait for either WF0 or all others |
| 157 | | :- block call_nv3(?,?,?,?,-,?,-),call_nv3(?,?,?,?,-,-,?). |
| 158 | | call_nv3(Call,A,B,C,_WF0,_,_) :- |
| 159 | ? | call(Call,A,B,C). |
| 160 | | |
| 161 | | %must_succ_kernel_call(kernel_objects:equal_object_optimized(A,B),(A1,A2),WF,Expr) :- !, |
| 162 | | % Call = kernel_objects:equal_object_optimized(A,B), |
| 163 | | % kernel_call_or(Call,A1,A2,WF,Expr). |
| 164 | | must_succ_kernel_call(Call,HasToBeGround,WF,_Expr) :- |
| 165 | | get_wait_flag0(WF,WF0), |
| 166 | | (nonvar(WF0) |
| 167 | ? | -> call(Call) |
| 168 | | ; %hit_profiler:add_profile_hit(must_succ_kernel_call(Call,WF0),3), |
| 169 | | %ground_value_check(HasToBeGround,G1), % using this made test 1562 fail; probably because co-routines remain active after WF0 has been set, leading un bound variables preventing optimisations in kernel_objects |
| 170 | | ground_value_opt_check(HasToBeGround,WF0,VG1), |
| 171 | ? | call_nv(Call,WF0,VG1) |
| 172 | | ). |
| 173 | | |
| 174 | | %:- block must_succ_kernel_call2(?,-,-). |
| 175 | | %must_succ_kernel_call2(Call,_,_) :- call(Call). |
| 176 | | |
| 177 | | |
| 178 | | kernel_call_predicate(equal_object_optimized(A,B),kernel_objects,WF,_) :- !, |
| 179 | | get_wait_flag0(WF,WF0), |
| 180 | | equal_obj(A,B,WF0,WF). |
| 181 | | % equality is the only predicate that can generate AVL trees |
| 182 | | % OTHER CALLS: partition_wf, member of empty set or singleton set, CLPFD operators: TO DO add |
| 183 | | |
| 184 | | kernel_call_predicate(not_equal_object_wf(A,B,WF),kernel_objects,WF,Expr) :- !, |
| 185 | | get_wait_flag0(WF,WF0),not_eq_wf(A,B,WF,WF0,Expr). |
| 186 | | kernel_call_predicate(partition_wf(A,B,PWF),kernel_objects,WF,Expr) :- !, |
| 187 | | (nonvar(B),B=[B1|T],T==[] % just one set |
| 188 | | -> kernel_call_predicate(equal_object_optimized(A,B1),kernel_objects,WF,Expr) |
| 189 | ? | ; all_but_one_set_known([A|B],Known), |
| 190 | ? | kernel_call(kernel_objects:partition_wf(A,B,PWF),Known,WF,Expr)). |
| 191 | | kernel_call_predicate(less_than(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than(A,B). |
| 192 | | kernel_call_predicate(less_than_equal(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than_equal(A,B). |
| 193 | | kernel_call_predicate(greater_than(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than(B,A). |
| 194 | | kernel_call_predicate(greater_than_equal(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than_equal(B,A). |
| 195 | | kernel_call_predicate(check_element_of_wf(A,B,PWF),kernel_objects,WF,Expr) :- !, |
| 196 | | get_wait_flag0(WF,WF0), check_element_of_wf0(A,B,PWF,WF0,Expr). |
| 197 | | kernel_call_predicate(is_natural(A,WF),kernel_objects,WF,_Expr) :- !, kernel_objects:is_natural(A,WF). % see test 2092 |
| 198 | | kernel_call_predicate(is_natural1(A,WF),kernel_objects,WF,_Expr) :- !, kernel_objects:is_natural1(A,WF). |
| 199 | | kernel_call_predicate(is_not_natural(A),kernel_objects,_WF,_Expr) :- !, kernel_objects:is_not_natural(A). |
| 200 | | kernel_call_predicate(is_not_natural1(A),kernel_objects,_WF,_Expr) :- !, kernel_objects:is_not_natural1(A). |
| 201 | | kernel_call_predicate(Call,Module,WF,_Expr) :- get_wait_flag0(WF,WF0), |
| 202 | | %hit_profiler:add_profile_hit(kernel_call_predicate(Call,WF0),2), |
| 203 | ? | call_wf0(Module:Call,WF0). |
| 204 | | %kernel_call_predicate(Call,HasToBeGround,WF,Expr) :- kernel_call(Call,HasToBeGround,WF,Expr). |
| 205 | | |
| 206 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
| 207 | | :- if(environ(prob_use_timer,true)). |
| 208 | | :- block call_wf0(?,-). |
| 209 | | call_wf0(X,_) :- debug:timer_call(X). %debug:watch(10,X). |
| 210 | | :- else. |
| 211 | | :- block call_wf0(?,-). |
| 212 | ? | call_wf0(Call,_) :- call(Call). |
| 213 | | :- endif. |
| 214 | | |
| 215 | | % unfolded version of above (for efficiency): |
| 216 | | kernel_call_predicate_equal_object_optimized(A,B,WF) :- |
| 217 | ? | get_wait_flag0(WF,WF0),equal_obj(A,B,WF0,WF). |
| 218 | | kernel_call_predicate_check_element_of_wf(A,B,WF,Span) :- |
| 219 | ? | get_wait_flag0(WF,WF0), check_element_of_wf0(A,B,WF,WF0,Span). |
| 220 | | kernel_call_predicate_not_equal_object(A,B,WF,Expr) :- |
| 221 | | get_wait_flag0(WF,WF0),not_eq_wf(A,B,WF,WF0,Expr). |
| 222 | | kernel_call_predicate_not_element_of_wf(A,B,WF) :- |
| 223 | | get_wait_flag0(WF,WF0),not_element_of_wf0(A,B,WF,WF0). |
| 224 | | |
| 225 | | :- block not_element_of_wf0(?,?,?,-). |
| 226 | ? | not_element_of_wf0(ElemValue,SetValue,WF,_) :- kernel_objects:not_element_of_wf(ElemValue,SetValue,WF). |
| 227 | | |
| 228 | | kernel_call_predicate3(KernelCall,Arg1,Arg2,Arg3,Module,WF,_Expression) :- |
| 229 | | get_wait_flag0(WF,WF0), |
| 230 | ? | call_wf0_3(Module:KernelCall,Arg1,Arg2,Arg3,WF,WF0). |
| 231 | | :- block call_wf0_3(?, ?,?,?,?, -). |
| 232 | ? | call_wf0_3(Call,A1,A2,A3,WF,_) :- call(Call,A1,A2,A3,WF). |
| 233 | | |
| 234 | | kernel_call_predicate2(KernelCall,Arg1,Arg2,Module,WF,_Expression) :- |
| 235 | | get_wait_flag0(WF,WF0), |
| 236 | | call_wf0_2(Module:KernelCall,Arg1,Arg2,WF,WF0). |
| 237 | | :- block call_wf0_2(?, ?,?,?, -). |
| 238 | ? | call_wf0_2(Call,A1,A2,WF,_) :- call(Call,A1,A2,WF). |
| 239 | | |
| 240 | | :- use_module(custom_explicit_sets,[singleton_set/2]). |
| 241 | | :- block check_element_of_wf0(?,-,?,-,?). |
| 242 | | check_element_of_wf0(A,B,WF,_WF0,_) :- var(B),!, % means nonvar(WF0) |
| 243 | ? | kernel_objects:check_element_of_wf(A,B,WF). |
| 244 | | check_element_of_wf0(_A,B,_WF,_,_) :- B=[],!,fail. % nothing can be element of empty set; CAN PREVENT WD-ERRORS from being detected ! |
| 245 | | check_element_of_wf0(A,B,WF,_WF0,_) :- |
| 246 | | singleton_set(B,B1),!, /* also does var check */ |
| 247 | ? | equal_object_optimized_wf(A,B1,check_element_of_wf0,WF). %was equal_obj(A,B1,WF0) but as B1 is ground value will always call equal_object_optimized directly |
| 248 | | % below B must be nonvar |
| 249 | | check_element_of_wf0(A,global_set(GS),WF,_,Span) :- nonvar(A), |
| 250 | | !, % be sure that we check something like int(-1) : NATURAL |
| 251 | | %kernel_objects:check_element_of_wf(A,global_set(GS),WF). |
| 252 | | kernel_objects:element_of_global_set_wf(A,GS,WF,Span). % Span for enumeration warnings |
| 253 | | check_element_of_wf0(A,avl_set(AVL),WF,_,_) :- simple_ground_value(A), |
| 254 | | !, % we can already check this efficiently in phase 0 |
| 255 | | custom_explicit_sets:element_of_avl_set_wf(AVL,A,WF). % we could even call avl_fetch directly |
| 256 | | % kernel_objects:check_element_of_wf(A,avl_set(AVL),WF). |
| 257 | | check_element_of_wf0(A,B,WF,WF0,Span) :- |
| 258 | ? | check_element_of_wf0_aux(A,B,WF,WF0,Span). |
| 259 | | :- block check_element_of_wf0_aux(?,?,?,-,?). |
| 260 | | check_element_of_wf0_aux(A,global_set(GS),WF,_WF0,Span) :- !, |
| 261 | | kernel_objects:element_of_global_set_wf(A,GS,WF,Span). % Span for enumeration warnings |
| 262 | | check_element_of_wf0_aux(A,avl_set(AVL),_WF,_WF0,b(EE,TT,Span)) :- |
| 263 | | member(prob_annotation('ENUM'),Span),!, % force early enumeration via 'ENUM' external function annotation |
| 264 | | (debug:debug_mode(on) -> add_message(enum,'Early enumeration of: ',b(EE,TT,Span),Span) ; true), |
| 265 | | custom_explicit_sets:safe_avl_member(A,AVL). % TO DO: use avl_fetch if A known? + cover ENUM annotation also if set is known later |
| 266 | ? | check_element_of_wf0_aux(A,B,WF,_WF0,_Span) :- kernel_objects:check_element_of_wf(A,B,WF). |
| 267 | | |
| 268 | | simple_ground_value(A) :- nonvar(A), simple_ground_value_aux(A). |
| 269 | | simple_ground_value_aux(int(X)) :- number(X). |
| 270 | | simple_ground_value_aux(fd(X,_)) :- number(X). |
| 271 | | simple_ground_value_aux(string(S)) :- ground(S). |
| 272 | | simple_ground_value_aux((A,B)) :- simple_ground_value(A), simple_ground_value(B). |
| 273 | | simple_ground_value_aux(rec(F)) :- simple_ground_fields(F). |
| 274 | | simple_ground_value_aux([]). |
| 275 | | |
| 276 | | simple_ground_fields(Var) :- var(Var),!,fail. % TO DO: we could activate check as soon as it becomes ground |
| 277 | | simple_ground_fields([]). |
| 278 | | simple_ground_fields([field(N,V)|T]) :- nonvar(N),simple_ground_value(V),simple_ground_fields(T). |
| 279 | | |
| 280 | | :- assert_must_succeed( kernel_mappings:not_eq_wf(int(1),int(2),_,_,_) ). |
| 281 | | :- assert_must_succeed( kernel_mappings:not_eq_wf([int(1)],[int(2)],_,0,_) ). |
| 282 | | :- block not_eq_wf(-,?,?,-,?), not_eq_wf(?,-,?,-,?). |
| 283 | | not_eq_wf(A,B,WF,_,_) :- efficient_value(A),efficient_value(B),!, %tools_printing:print_term_summary(not_eq_wf(A,B)), |
| 284 | | kernel_objects:not_equal_object_wf(A,B,WF). |
| 285 | ? | not_eq_wf(A,B,WF,WF0,Expr) :- not_eq_wf0(A,B,WF,WF0,Expr). |
| 286 | | :- block not_eq_wf0(?,?,?,-,?). |
| 287 | | not_eq_wf0(A,B,WF,_,_Expr) :- |
| 288 | | %((var(A),var(B)) -> instantiate_argument(Expr,A) ; true), |
| 289 | ? | kernel_objects:not_equal_object_wf(A,B,WF). |
| 290 | | |
| 291 | | /* not required anymore ?! |
| 292 | | % instantiate argument according to type of expression to ensure not_equal_object (or other calls) are triggered and do not wait setting up dif constraints |
| 293 | | instantiate_argument(not_equal(AE,_),A) :- |
| 294 | | bsyntaxtree:get_texpr_type(AE,Type),!, print(instantiate(Type,A)),nl, |
| 295 | | instantiate_arg(Type,A). |
| 296 | | instantiate_argument(_,_). |
| 297 | | |
| 298 | | instantiate_arg(string,R) :- !, R=string(_). |
| 299 | | instantiate_arg(integer,R) :- !, R=int(_). |
| 300 | | % missing: more cases global(G),.... ? |
| 301 | | instantiate_arg(_,_). |
| 302 | | */ |
| 303 | | |
| 304 | | % check whether disequality can be efficiently checked (already in WF0 phase) |
| 305 | | efficient_value(X) :- var(X),!,fail. |
| 306 | | efficient_value(int(_)). |
| 307 | | efficient_value(avl_set(_)). |
| 308 | | efficient_value([]). |
| 309 | | efficient_value(fd(_,_)). |
| 310 | | efficient_value(string(_)). |
| 311 | | efficient_value((A,B)) :- nonvar(A),nonvar(B),efficient_value(A), efficient_value(B). |
| 312 | | efficient_value(pred_true). efficient_value(pred_false). |
| 313 | | efficient_value(term(_)). % will usually be floating: :- nonvar(X),X=floating(_). |
| 314 | | |
| 315 | | |
| 316 | | |
| 317 | | %:- meta_predicate kernel_call(0,*,*,*). |
| 318 | | kernel_call(Call,HasToBeGround,WF,_Expr) :- |
| 319 | | get_wait_flag0(WF,WF0), |
| 320 | | %hit_profiler:add_profile_hit(kernel_call(Call,WF),2), |
| 321 | | %print(kc(WF0,Call)),nl, |
| 322 | | (nonvar(WF0) |
| 323 | | -> call(Call) |
| 324 | | ; ground_value_opt_check(HasToBeGround,WF0,G1), |
| 325 | ? | call_nv(Call,WF0,G1) |
| 326 | | ). |
| 327 | | |
| 328 | | :- block call_nv(?,-,-). |
| 329 | | call_nv(Call,_,_) :- |
| 330 | | % ( (var(WF0) -> print('enter :'),tools_printing:print_term_summary(Call) ; true), |
| 331 | ? | call(Call). |
| 332 | | |
| 333 | | % optimized custom versions of kernel_call for performacne: |
| 334 | | :- use_module(bsets_clp,[apply_to/6]). |
| 335 | | kernel_call_apply_to(FValue,ArgValue,Res,FunctionType,Span,WF) :- |
| 336 | | %hit_profiler:add_profile_hit(kernel_call_apply_to(FValue,ArgValue,Res,WF)), |
| 337 | | get_wait_flag0(WF,WF0), |
| 338 | | (var(WF0) %(var(WF0), \+ ground(ArgValue), \+ ground(FValue)) |
| 339 | | -> ground_value_check((FValue,ArgValue),WF1), % often FValue is an avl_set, avoid pending co-routines later by checking it first for groundness |
| 340 | ? | call_apply_to(FValue,ArgValue,Res,FunctionType,Span,WF,WF0,WF1) |
| 341 | ? | ; apply_to(FValue,ArgValue,Res,FunctionType,Span,WF) |
| 342 | | ). |
| 343 | | % TO DO: maybe transmit Type information for using with element/3 |
| 344 | | |
| 345 | | :- block call_apply_to(?,?,?,?,?,?,-,-). |
| 346 | | call_apply_to(FValue,ArgValue,Res,FunctionType,Span,WF,_,_Gr) :- |
| 347 | | %discard_ground_value_check(Gr), |
| 348 | ? | bsets_clp:apply_to(FValue,ArgValue,Res,FunctionType,Span,WF). |
| 349 | | |
| 350 | | |
| 351 | | /* ------------------------------- */ |
| 352 | | |
| 353 | | :- use_module(kernel_objects,[equal_object_optimized_wf/4]). |
| 354 | | :- block equal_obj(-,-,-,?). |
| 355 | | |
| 356 | | equal_obj(A,B,WF0,WF) :- nonvar(WF0),!, |
| 357 | ? | equal_object_optimized_wf(A,B,equal_obj1,WF). |
| 358 | | equal_obj(A,B,WF0,WF) :- %hit_profiler:add_profile_hit(eq(A,B)), |
| 359 | | non_simple_ground_value_check(A,VA), |
| 360 | ? | (nonvar(VA) -> equal_object_optimized_wf(A,B,equal_obj2,WF) |
| 361 | | ; non_simple_ground_value_check(B,VB), |
| 362 | | (nonvar(VB) -> equal_object_optimized_wf(A,B,equal_obj3,WF) |
| 363 | | ; equal_obj_block(A,B,WF,WF0,VA,VB) |
| 364 | | ) |
| 365 | | ). |
| 366 | | :- block equal_obj_block(?,?,?,-,-,-). |
| 367 | | equal_obj_block(A,B,WF,_,_,_) :- |
| 368 | | equal_object_optimized_wf(A,B,equal_obj4,WF). |
| 369 | | |
| 370 | | % a version of ground_value_check that also returns [] in some cases where there is a variable but equal_object can be called |
| 371 | | non_simple_ground_value_check(V,Vars) :- var(V),!, Vars=[V]. |
| 372 | | non_simple_ground_value_check(pred_false,Vars) :- !, Vars=[]. |
| 373 | | non_simple_ground_value_check(pred_true,Vars) :- !, Vars=[]. |
| 374 | | non_simple_ground_value_check(int(_),Vars) :- !, Vars=[]. % may contain var; but we can unify nonetheless |
| 375 | | non_simple_ground_value_check(string(_),Vars) :- !, Vars=[]. % ditto |
| 376 | | non_simple_ground_value_check(fd(_,_),Vars) :- !, Vars=[]. % ditto |
| 377 | | non_simple_ground_value_check(A,Vars) :- !, ground_value_check(A,Vars). |
| 378 | | |
| 379 | | |
| 380 | | |
| 381 | | % used for reversible calls: if one argument is ground we can evaluate the call and compute the other one |
| 382 | | kernel_call_or(Call,HasToBeGround1,HasToBeGround2,WF,_Expr) :- |
| 383 | | get_wait_flag0(WF,WF0), |
| 384 | | (nonvar(WF0) -> call(Call) |
| 385 | | ; ground_value_check(HasToBeGround1,G1), |
| 386 | | (nonvar(G1) -> call(Call) |
| 387 | | ; ground_value_check(HasToBeGround2,G2), |
| 388 | | %hit_profiler:add_profile_hit(kernel_call_or(Call,WF0),2), |
| 389 | | call_nv_or3(Call,WF0,G1,G2) |
| 390 | | ) |
| 391 | | ). |
| 392 | | |
| 393 | | :- block call_nv_or3(?,-,-,-). |
| 394 | | call_nv_or3(Call,_,_,_) :- |
| 395 | ? | call(Call). |
| 396 | | |
| 397 | | |
| 398 | | % special case for calling binary integer functions: here we can use more efficient block declarations |
| 399 | | call_determined_integer_function(KF,V1,V2,Val,WF0,WF,Span) :- |
| 400 | | determined(V1,V2,Val,Determined,WF0), |
| 401 | | call_determined_integer_function2(KF,V1,V2,Val,WF0,Determined,WF,Span). |
| 402 | | :- block call_determined_integer_function2(?,?,?,?,-,-,?,?). |
| 403 | | %call_determined_integer_function2(KF,V1,V2,V,WF0,Det,_,_) :- |
| 404 | | % print(kernel_det_call(KF,V1,V2,V,WF0,Det)),nl,fail. |
| 405 | | call_determined_integer_function2(division,V1,V2,Val,_,_,WF,Span) :- |
| 406 | | kernel_objects:division(V1,V2,Val,Span,WF). |
| 407 | | call_determined_integer_function2(floored_division,V1,V2,Val,_,_,WF,Span) :- |
| 408 | | kernel_objects:floored_division(V1,V2,Val,Span,WF). |
| 409 | | call_determined_integer_function2(int_minus,V1,V2,Val,_,_,_WF,_Span) :- |
| 410 | | kernel_objects:int_minus(V1,V2,Val). |
| 411 | | call_determined_integer_function2(int_plus,V1,V2,Val,_,_,_WF,_Span) :- |
| 412 | | % kernel_call_determined(kernel_objects:int_plus(V1,V2,Val),V1,V2,Val,WF,integer). |
| 413 | ? | kernel_objects:int_plus(V1,V2,Val). |
| 414 | | call_determined_integer_function2(int_power,V1,V2,Val,_,_,WF,Span) :- |
| 415 | | kernel_objects:int_power(V1,V2,Val,Span,WF). |
| 416 | | call_determined_integer_function2(modulo,V1,V2,Val,_,_,WF,Span) :- |
| 417 | | kernel_objects:modulo(V1,V2,Val,Span,WF). |
| 418 | | call_determined_integer_function2(times,V1,V2,Val,_,_,_WF,_Span) :- |
| 419 | | kernel_objects:times(V1,V2,Val). |
| 420 | | |
| 421 | | % sets last argument to determined without instantiating its first three args |
| 422 | | % it is set when two integer values are known |
| 423 | | :- block determined(-,-,?,?,-), determined(-,?,-,?,-), determined(?,-,-,?,-). |
| 424 | | %:- block determined(-,-,?,?,?), determined(-,?,-,?,?), determined(?,-,-,?,?). |
| 425 | | %determined(Y,V,X,Det,WF0) :- print(determined(Y,V,X,Det,WF0)),nl,fail. |
| 426 | | determined(_X,_Y,_Z,Det,WF0) :- nonvar(WF0),!,Det=determined. |
| 427 | | % ((nonvar(_X),nonvar(_Y), \+ ground(_Y), var(_V)) -> trace ; true). |
| 428 | | determined(X,Y,V,Det,_) :- var(X),!, Y=int(YY),V=int(VV), %(YY=0 -> X=V ; true), |
| 429 | | determined2(X,YY,VV,Det). |
| 430 | | determined(Y,X,V,Det,_) :- var(X),!, Y=int(YY),V=int(VV), %(YY=0 -> X=V ; true), |
| 431 | | determined2(X,YY,VV,Det). |
| 432 | | determined(Y,V,X,Det,_) :- Y=int(YY),V=int(VV), %(YY=0 -> X=V ; VV=0 -> X=Y), |
| 433 | | determined2(X,YY,VV,Det). |
| 434 | | :- block determined2(-,-,?,?), determined2(-,?,-,?), determined2(?,-,-,?). |
| 435 | | %determined2(Y,V,X,Det) :- print(determined2(Y,V,X,Det)),nl,fail. |
| 436 | | determined2(X,_,_,Det) :- var(X),!,Det=determined. |
| 437 | | determined2(int(XX),YY,VV,Det) :- determined3(XX,YY,VV,Det). |
| 438 | | :- block determined3(-,-,?,?), determined3(-,?,-,?), determined3(?,-,-,?). |
| 439 | | %determined3(Y,V,X,Det) :- print(determined3(Y,V,X,Det)),nl,fail. |
| 440 | | determined3(_,_,_,determined). |
| 441 | | |
| 442 | | |
| 443 | | |
| 444 | | |
| 445 | | :- use_module(error_manager). |
| 446 | | |
| 447 | | invalid_call(X) :- \+ check_valid_kernel_call(X,_). |
| 448 | | check_valid_kernel_call(X,unary) :- unary_function(_,_,X). |
| 449 | | check_valid_kernel_call(X,binary) :- binary_function(_,_,X). |
| 450 | | check_valid_kernel_call(X,_) :- add_error(check_valid_kernel_call,'Illegal Kernel Call: ',X),fail. |
| 451 | | :- assert_must_fail((kernel_mappings:expects_waitflag_and_span(X), |
| 452 | | kernel_mappings:invalid_call(X))). |
| 453 | | |
| 454 | | expects_waitflag_and_span(first_sequence). |
| 455 | | expects_waitflag_and_span(last_sequence). |
| 456 | | expects_waitflag_and_span(tail_sequence). |
| 457 | | expects_waitflag_and_span(front_sequence). |
| 458 | | expects_waitflag_and_span(minimum_of_set). |
| 459 | | expects_waitflag_and_span(maximum_of_set). |
| 460 | | expects_waitflag_and_span(intersection_generalized_wf). |
| 461 | | |
| 462 | | expects_waitflag_and_span(division). |
| 463 | | expects_waitflag_and_span(floored_division). |
| 464 | | expects_waitflag_and_span(modulo). |
| 465 | | expects_waitflag_and_span(int_power). |
| 466 | | expects_waitflag_and_span(real_power_of_wf). |
| 467 | | expects_waitflag_and_span(singleton_set_element). |
| 468 | | expects_waitflag_and_span(real_division_wf). |
| 469 | | expects_waitflag_and_span(real_maximum_of_set). |
| 470 | | expects_waitflag_and_span(real_minimum_of_set). |
| 471 | | |
| 472 | | :- assert_must_fail((kernel_mappings:expects_waitflag(X), |
| 473 | | kernel_mappings:invalid_call(X))). |
| 474 | | :- assert_must_fail((kernel_mappings:expects_waitflag(X), |
| 475 | | kernel_mappings:expects_waitflag_and_span(X))). |
| 476 | | /* |
| 477 | | comment in if we want to ensure that all kernel predicates take at least the WF |
| 478 | | :- assert_must_fail((kernel_mappings:unary_function(_,_,X), |
| 479 | | \+ (kernel_mappings:expects_waitflag(X) ; |
| 480 | | kernel_mappings:expects_waitflag_and_span(X)), |
| 481 | | print(unary_no_waitflag(X)),nl )). |
| 482 | | :- assert_must_fail((kernel_mappings:binary_function(_,_,X), |
| 483 | | \+ (kernel_mappings:expects_waitflag(X) ; |
| 484 | | kernel_mappings:expects_waitflag_and_span(X)), |
| 485 | | print(binary_no_waitflag(X)),nl )). |
| 486 | | */ |
| 487 | | |
| 488 | | expects_waitflag(append_sequence). |
| 489 | | expects_waitflag(bag_items). |
| 490 | | expects_waitflag(cartesian_product_wf). |
| 491 | | expects_waitflag(compaction). |
| 492 | | expects_waitflag(concat_sequence). |
| 493 | | expects_waitflag(concatentation_of_sequences). |
| 494 | | expects_waitflag(difference_set_wf). |
| 495 | | expects_waitflag(direct_product_wf). |
| 496 | | expects_waitflag(parallel_product_wf). |
| 497 | | expects_waitflag(domain_restriction_wf). |
| 498 | | expects_waitflag(domain_subtraction_wf). |
| 499 | | expects_waitflag(domain_wf). |
| 500 | | expects_waitflag(finite_cardinality_as_int_wf). |
| 501 | | expects_waitflag(identity_relation_over_wf). |
| 502 | | expects_waitflag(image_wf). |
| 503 | | expects_waitflag(intersection). |
| 504 | | expects_waitflag(invert_relation_wf). |
| 505 | | expects_waitflag(relational_trans_closure_wf). |
| 506 | | expects_waitflag(override_relation). |
| 507 | | expects_waitflag(prefix_sequence_wf). |
| 508 | | expects_waitflag(prepend_sequence). |
| 509 | | expects_waitflag(range_restriction_wf). |
| 510 | | expects_waitflag(range_subtraction_wf). |
| 511 | | expects_waitflag(range_wf). |
| 512 | | expects_waitflag(real_addition_wf). |
| 513 | | %expects_waitflag(real_division_wf). |
| 514 | | expects_waitflag(real_multiplication_wf). |
| 515 | | expects_waitflag(real_subtraction_wf). |
| 516 | | expects_waitflag(real_unary_minus_wf). |
| 517 | | %expects_waitflag(rel_composition_wf). |
| 518 | | %expects_waitflag(rel_iterate_wf). |
| 519 | | expects_waitflag(rev_sequence). |
| 520 | | expects_waitflag(size_of_sequence). |
| 521 | | expects_waitflag(square). |
| 522 | | expects_waitflag(suffix_sequence). |
| 523 | | expects_waitflag(unary_minus_wf). |
| 524 | | expects_waitflag(union_generalized_wf). |
| 525 | | expects_waitflag(union_wf). |
| 526 | | |
| 527 | | expects_waitflag_and_type(rel_iterate_wf). |
| 528 | | expects_waitflag_and_type(rel_composition_wf). |
| 529 | | |
| 530 | | :- use_module(bsyntaxtree,[get_texpr_set_type/2]). |
| 531 | | % only used when not in CLPFD mode: |
| 532 | | special_binary_predicate(greater(b(card(X),integer,_),Y), kernel_objects:cardinality_greater,X,TypeX,Y,integer) :- |
| 533 | | get_texpr_set_type(X,TypeX). |
| 534 | | special_binary_predicate(less(Y,b(card(X),integer,_)), kernel_objects:cardinality_greater,X,TypeX,Y,integer) :- |
| 535 | | get_texpr_set_type(X,TypeX). |
| 536 | | special_binary_predicate(greater_equal(b(card(X),integer,_),Y), kernel_objects:cardinality_greater_equal,X,TypeX,Y,integer) :- |
| 537 | | get_texpr_set_type(X,TypeX). |
| 538 | | special_binary_predicate(less_equal(Y,b(card(X),integer,_)), kernel_objects:cardinality_greater_equal,X,TypeX,Y,integer) :- |
| 539 | | get_texpr_set_type(X,TypeX). |
| 540 | | |
| 541 | | |
| 542 | | |
| 543 | | /* EXPRESSIONS */ |
| 544 | | |
| 545 | | |
| 546 | | :- assert_must_fail((kernel_mappings:reversible_unary_function(X), |
| 547 | | kernel_mappings:invalid_call(X))). |
| 548 | | |
| 549 | | reversible_unary_function(invert_relation_wf). |
| 550 | | reversible_unary_function(rev_sequence). |
| 551 | | reversible_unary_function(unary_minus_wf). |
| 552 | | |
| 553 | | unary_function(reverse,bsets_clp,invert_relation_wf). |
| 554 | | unary_function(closure,bsets_clp,relational_trans_closure_wf). % this is closure1 |
| 555 | | %unary_function(reflexive_closure,bsets_clp,relational_reflexive_closure). % now done in ast_cleanup |
| 556 | | unary_function(domain,bsets_clp,domain_wf). |
| 557 | | unary_function(range,bsets_clp,range_wf). |
| 558 | | |
| 559 | | unary_function(general_union,kernel_objects,union_generalized_wf). |
| 560 | | unary_function(general_intersection,kernel_objects,intersection_generalized_wf). |
| 561 | | |
| 562 | | unary_function(first,bsets_clp,first_sequence). |
| 563 | | unary_function(size,bsets_clp,size_of_sequence). |
| 564 | | unary_function(front,bsets_clp,front_sequence). |
| 565 | | unary_function(tail,bsets_clp,tail_sequence). |
| 566 | | unary_function(rev,bsets_clp,rev_sequence). |
| 567 | | unary_function(last,bsets_clp,last_sequence). |
| 568 | | |
| 569 | | unary_function(card,kernel_cardinality_attr,finite_cardinality_as_int_wf). |
| 570 | | unary_function(pow_subset,kernel_objects,power_set). % not really necessary anymore, |
| 571 | | % because of symbolic_closure_unary_operator treatment, |
| 572 | | % except for empty set and singleton sets (see do_not_keep_symbolic_unary) |
| 573 | | unary_function(fin_subset,kernel_objects,power_set). % not really necessary anymore, ditto |
| 574 | | unary_function(pow1_subset,kernel_objects,non_empty_power_set). % not really necessary anymore |
| 575 | | unary_function(fin1_subset,kernel_objects,non_empty_power_set). % not really necessary anymore |
| 576 | | unary_function(identity,bsets_clp,identity_relation_over_wf). |
| 577 | | %unary_function(perm,bsets_clp,enumerate_permutation_sequence). |
| 578 | | % unary_function(iseq,bsets_clp,enumerate_injective_sequence). |
| 579 | | %unary_function(iseq1,bsets_clp,enumerate_non_empty_injective_sequence). |
| 580 | | %unary_function(seq,bsets_clp,enumerate_sequence). |
| 581 | | %unary_function(seq1,bsets_clp,enumerate_non_empty_sequence). |
| 582 | | %unary_function(struct,kernel_records,enumerate_records). |
| 583 | | |
| 584 | | unary_function(general_concat,bsets_clp,concatentation_of_sequences). % conc operator, mapped to STRING_CONC for strings |
| 585 | | unary_function(unary_minus,kernel_objects,unary_minus_wf). |
| 586 | | unary_function(unary_minus_real,kernel_reals,real_unary_minus_wf). |
| 587 | | unary_function(square_multiplication,kernel_objects,square). % artificial construct, detected when X*X is evaluated by interpreter; but square is directly called |
| 588 | | unary_function(max,kernel_objects,maximum_of_set). |
| 589 | | unary_function(max_real,kernel_reals,real_maximum_of_set). |
| 590 | | unary_function(min,kernel_objects,minimum_of_set). |
| 591 | | unary_function(min_real,kernel_reals,real_minimum_of_set). |
| 592 | | |
| 593 | | unary_function(first_of_pair,kernel_objects,first_of_pair). % prj1 for full types |
| 594 | | unary_function(second_of_pair,kernel_objects,second_of_pair). % prj2 for full types |
| 595 | | unary_function(mu,kernel_objects,singleton_set_element). % Z MU operator |
| 596 | | |
| 597 | | unary_function(compaction,kernel_z,compaction). |
| 598 | | unary_function(bag_items,kernel_z,bag_items). |
| 599 | | |
| 600 | | unary_function(convert_real,kernel_reals,convert_int_to_real). |
| 601 | | unary_function(convert_int_floor,kernel_reals,real_floor). |
| 602 | | unary_function(convert_int_ceiling,kernel_reals,real_ceiling). |
| 603 | | |
| 604 | | |
| 605 | | :- assert_must_fail((kernel_mappings:determined_binary_integer_function(X), |
| 606 | | kernel_mappings:invalid_call(X))). |
| 607 | | /* binary functions where 1 argument is determined from the other two */ |
| 608 | | determined_binary_integer_function(division). % isn't really determined X / 10 = 2 --> many possible values |
| 609 | | determined_binary_integer_function(int_minus). |
| 610 | | determined_binary_integer_function(int_plus). |
| 611 | | determined_binary_integer_function(int_power). |
| 612 | | determined_binary_integer_function(modulo). % isn't really determined; X mod 10 = 0 --> many possible values |
| 613 | | determined_binary_integer_function(times). |
| 614 | | |
| 615 | | %:- assert_must_fail((kernel_mappings:determined_binary_function(X), |
| 616 | | % kernel_mappings:invalid_call(X))). |
| 617 | | %determined_binary_function(nat_range). |
| 618 | | %determined_binary_function(concat_sequence). |
| 619 | | %determined_binary_function(prepend_sequence). |
| 620 | | %determined_binary_function(cartesian_product). |
| 621 | | |
| 622 | | % set up any special propagation rules which should trigger before Args1 and 2 are fully known: |
| 623 | | % we should probably move these rules down to kernel_objects, bsets_clp ... and validate them |
| 624 | | % maybe we can even store them in B format, prove them and read them in |
| 625 | | special_propagate_binary_function(union_wf,A,B,Res,WF) :- !, |
| 626 | | propagate_empty_set(Res,A,WF), % A\/B ={} => A={} |
| 627 | | propagate_empty_set(Res,B,WF). % A\/B ={} => B={} |
| 628 | | special_propagate_binary_function(override_relation,A,B,Res,WF) :- !, % used causes small slowdown for ticket 184?? |
| 629 | | propagate_empty_set(Res,A,WF), % A<+B ={} => A={} |
| 630 | | propagate_empty_set(Res,B,WF), % A<+B ={} => B={} |
| 631 | | propagate_empty_set_eq(A,B,Res,WF), % if A ={} => A <+ B = B |
| 632 | | propagate_empty_set_eq(B,A,Res,WF). % if B ={} => A <+ B = A |
| 633 | | special_propagate_binary_function(intersection,A,B,Res,WF) :- !, |
| 634 | | propagate_empty_set(A,Res,WF), % A={} => A /\ B = {} |
| 635 | | propagate_empty_set(B,Res,WF). % B={} => A /\ B = {} |
| 636 | | special_propagate_binary_function(difference_set_wf,A,B,Res,WF) :- !, |
| 637 | | propagate_empty_set(A,Res,WF), % A={} => A \ B = {} |
| 638 | | propagate_empty_set_eq(B,A,Res,WF). % B={} => A \ B = A |
| 639 | | special_propagate_binary_function(image_wf,A,B,Res,WF) :- !, |
| 640 | | propagate_empty_set(B,Res,WF), % B={} => A[B] = {} |
| 641 | | propagate_id_eq(A,B,Res,WF). % (A={} => A[B] = {}) & (A=id => A[B] = B) |
| 642 | | special_propagate_binary_function(domain_restriction_wf,S,_R,Res,WF) :- !, |
| 643 | | propagate_empty_set(S,Res,WF). % if S ={} => S <| R = {} |
| 644 | | special_propagate_binary_function(domain_subtraction_wf,S,R,Res,WF) :- !, |
| 645 | | propagate_empty_set_eq(S,R,Res,WF). % if S ={} => S <<| R = R |
| 646 | | special_propagate_binary_function(range_restriction_wf,_R,S,Res,WF) :- !, |
| 647 | | propagate_empty_set(S,Res,WF). % if S ={} => R |> S = {} |
| 648 | | special_propagate_binary_function(range_subtraction_wf,R,S,Res,WF) :- !, |
| 649 | | propagate_empty_set_eq(S,R,Res,WF). % if S ={} => R |>> S = R |
| 650 | | special_propagate_binary_function(_,_,_,_,_WF). % no propagators available |
| 651 | | :- block propagate_empty_set(-,?,?). |
| 652 | | propagate_empty_set([],A,WF) :- !, |
| 653 | | % (A==[] -> true ; print(prop_empty(A)),nl), %% |
| 654 | | kernel_objects:empty_set_wf(A,WF). |
| 655 | | propagate_empty_set(_,_,_). |
| 656 | | :- block propagate_empty_set_eq(-,?,?,?). |
| 657 | | propagate_empty_set_eq([],A,B,WF) :- !,kernel_objects:equal_object_wf(A,B,propagate_empty_set_eq,WF). |
| 658 | | propagate_empty_set_eq(_,_,_,_). |
| 659 | | :- block propagate_id_eq(-,?,?,?). |
| 660 | ? | propagate_id_eq([],_A,B,WF) :- !,kernel_objects:empty_set_wf(B,WF). |
| 661 | | propagate_id_eq(closure(Par,Types,Body),A,B,WF) :- custom_explicit_sets:is_full_id_closure(Par,Types,Body), |
| 662 | | % print(prop_id_eq(A,B)),nl, |
| 663 | | !,kernel_objects:equal_object_wf(A,B,propagate_id_eq,WF). |
| 664 | | propagate_id_eq(_,_,_,_). |
| 665 | | |
| 666 | | binary_function(concat,bsets_clp,concat_sequence). % ^ |
| 667 | | binary_function(insert_front,bsets_clp,prepend_sequence). |
| 668 | | binary_function(insert_tail,bsets_clp,append_sequence). |
| 669 | | binary_function(restrict_front,bsets_clp,prefix_sequence_wf). % s /|\ n |
| 670 | | binary_function(restrict_tail,bsets_clp,suffix_sequence). % WF |
| 671 | | binary_function(union,kernel_objects,union_wf). |
| 672 | | binary_function(intersection,kernel_objects,intersection). |
| 673 | | binary_function(set_subtraction,kernel_objects,difference_set_wf). |
| 674 | | binary_function(cartesian_product,kernel_objects,cartesian_product_wf). % always converted into closure |
| 675 | | binary_function(add,kernel_objects,int_plus). |
| 676 | | binary_function(add_real,kernel_reals,real_addition_wf). |
| 677 | | binary_function(multiplication,kernel_objects,times). |
| 678 | | binary_function(multiplication_real,kernel_reals,real_multiplication_wf). |
| 679 | | binary_function(minus,kernel_objects,int_minus). |
| 680 | | binary_function(minus_real,kernel_reals,real_subtraction_wf). |
| 681 | | binary_function(modulo,kernel_objects,modulo). |
| 682 | | binary_function(power_of,kernel_objects,int_power). |
| 683 | | binary_function(power_of_real,kernel_reals,real_power_of_wf). |
| 684 | | binary_function(div,kernel_objects,division). |
| 685 | | binary_function(div_real,kernel_reals,real_division_wf). |
| 686 | | binary_function(floored_div,kernel_objects,floored_division). |
| 687 | | %binary_function(interval,kernel_objects,nat_range). % always converted into closure, unless empty or singleton |
| 688 | | binary_function(image,bsets_clp,image_wf). |
| 689 | | %binary_function(function,apply_to). |
| 690 | | binary_function(domain_restriction,bsets_clp,domain_restriction_wf). |
| 691 | | binary_function(domain_subtraction,bsets_clp,domain_subtraction_wf). |
| 692 | | binary_function(range_subtraction,bsets_clp,range_subtraction_wf). |
| 693 | | binary_function(range_restriction,bsets_clp,range_restriction_wf). |
| 694 | | binary_function(overwrite,bsets_clp,override_relation). |
| 695 | | binary_function(composition,bsets_clp,rel_composition_wf). |
| 696 | | binary_function(iteration,bsets_clp,rel_iterate_wf). |
| 697 | | binary_function(direct_product,bsets_clp,direct_product_wf). |
| 698 | | binary_function(parallel_product,bsets_clp,parallel_product_wf). |
| 699 | | % functions below always converted into closure |
| 700 | | %binary_function(total_function,bsets_clp,enumerate_total_function). |
| 701 | | %binary_function(partial_function,bsets_clp,enumerate_partial_function). |
| 702 | | %binary_function(total_bijection,bsets_clp,enumerate_total_bijection). |
| 703 | | %binary_function(relations,bsets_clp,enumerate_relation). |
| 704 | | %binary_function(partial_injection,bsets_clp,enumerate_partial_injection). |
| 705 | | %binary_function(partial_surjection,bsets_clp,enumerate_partial_surjection). |
| 706 | | %binary_function(total_surjection,bsets_clp,enumerate_total_surjection). |
| 707 | | %binary_function(total_relation,bsets_clp,enumerate_total_relation). |
| 708 | | %binary_function(total_injection,bsets_clp,enumerate_total_injection). |
| 709 | | %binary_function(partial_bijection,bsets_clp,enumerate_partial_bijection). |
| 710 | | %binary_function(surjection_relation,bsets_clp,enumerate_surjection_relation). |
| 711 | | %binary_function(total_surjection_relation,bsets_clp,enumerate_total_surjection_relation). |
| 712 | | |
| 713 | | % check if the first argument determines the value of a binary_function: |
| 714 | | binary_arg1_determines_value(multiplication,A1,int(0)) :- zero(A1). |
| 715 | | binary_arg1_determines_value(intersection,A1,[]) :- A1==[]. |
| 716 | | binary_arg1_determines_value(set_subtraction,A1,[]) :- A1==[]. |
| 717 | | binary_arg1_determines_value(domain_restriction,A1,[]) :- A1==[]. % first arg is set |
| 718 | | binary_arg1_determines_value(range_subtraction,A1,[]) :- A1==[]. % first arg is rel |
| 719 | | binary_arg1_determines_value(range_restriction,A1,[]) :- A1==[]. % first arg is rel |
| 720 | | binary_arg1_determines_value(cartesian_product,A1,[]) :- A1==[]. |
| 721 | | binary_arg1_determines_value(composition,A1,[]) :- A1==[]. |
| 722 | | binary_arg1_determines_value(direct_product,A1,[]) :- A1==[]. |
| 723 | | binary_arg1_determines_value(parallel_product,A1,[]) :- A1==[]. |
| 724 | | |
| 725 | | |
| 726 | | zero(X) :- nonvar(X), X=int(X1),X1==0. |
| 727 | | |
| 728 | | /* add PartialBijection .... */ |
| 729 | | |
| 730 | | /* BOOLEAN EXPRESSIONS */ |
| 731 | | |
| 732 | | |
| 733 | | :- assert_must_succeed(kernel_mappings:symbolic_closure_binary_operator(partial_function)). |
| 734 | | :- assert_must_succeed(kernel_mappings:symbolic_closure_binary_operator(total_function)). |
| 735 | | |
| 736 | | symbolic_closure_binary_operator(Op) :- |
| 737 | | binary_in_boolean_type(Op,_), |
| 738 | | binary_not_in_boolean_type(Op,_), |
| 739 | | \+ not_symbolic_binary(Op). |
| 740 | | /* note every symbolic closure operator must be dealt with by a binary_in and |
| 741 | | a binary_not_in clause below, otherwise we have a problem */ |
| 742 | | |
| 743 | | %not_symbolic_binary(set_subtraction). % initially test 426 failed or runtime went from 6 to 12 secs ; now with do_not_keep_symbolic rules below it is fine and runtime is 3 secs |
| 744 | | %not_symbolic_binary(intersection). % seems to be ok to allow symbolic treatment |
| 745 | | not_symbolic_binary(range_subtraction). % important for test 1001 |
| 746 | | not_symbolic_binary(range_restriction). |
| 747 | | not_symbolic_binary(domain_subtraction). % important for test 1001 |
| 748 | | not_symbolic_binary(domain_restriction). |
| 749 | | not_symbolic_binary(composition). % for tests 525, 1001; there are quite a few rules to compute symbolic compositions |
| 750 | | % TO DO: see if we can remove the need for symbolic composition rules and just rely on in_composition_wf |
| 751 | | % this would also make this faster: 50 |-> res : ((f ; succ) ; succ) |
| 752 | | % where we have defined :let f = {x,y|x:1..50 & y : 1..250 & (x+y) mod 2 = 0} |
| 753 | | % currently 0 |-> res : (f ; (succ ; succ)) is fast (1 ms vs 21 ms) |
| 754 | | /* interval symbolic: because we often have expressions of the form a..b where b is > MAXINT */ |
| 755 | | |
| 756 | | % return true if a symbolic closure for a binary operator would be definitely empty: |
| 757 | | is_definitely_empty(interval,int(A),int(B)) :- number(A),number(B), A>B. |
| 758 | | is_definitely_empty(cartesian_product,A,B) :- (B==[]->true ; A==[]). % A==[] actually already checked in binary_arg1_determines_value |
| 759 | | is_definitely_empty(parallel_product,A,B) :- (A==[]->true ; B==[]). |
| 760 | | is_definitely_empty(total_relation,A,B) :- B==[], definitely_not_empty(A). |
| 761 | | is_definitely_empty(total_function,A,B) :- B==[], definitely_not_empty(A). % {} --> {} = {{}} |
| 762 | | is_definitely_empty(total_injection,A,B) :- B==[], definitely_not_empty(A). |
| 763 | | is_definitely_empty(total_surjection,A,B) :- B==[], definitely_not_empty(A). |
| 764 | | is_definitely_empty(total_bijection,A,B) :- B==[], definitely_not_empty(A). |
| 765 | | is_definitely_empty(intersection,A,B) :- (A==[] ; B==[]). |
| 766 | | is_definitely_empty(set_subtraction,A,B) :- |
| 767 | | (A==[] ; nonvar(B), custom_explicit_sets:is_definitely_maximal_set(B)). |
| 768 | | |
| 769 | | :- use_module(kernel_freetypes,[is_non_empty_freetype/1]). |
| 770 | | definitely_not_empty(X) :- nonvar(X), definitely_not_empty_aux(X). |
| 771 | | definitely_not_empty_aux([_|_]). |
| 772 | | definitely_not_empty_aux(avl_set(_)). |
| 773 | | definitely_not_empty_aux(global_set(_)). |
| 774 | | definitely_not_empty_aux(freetype(ID)) :- is_non_empty_freetype(ID). |
| 775 | | |
| 776 | | % check if it is worthwhile keeping a binary operator symbolic, if so: return value |
| 777 | | do_not_keep_symbolic(cartesian_product,Set1,Set2,Res,WF) :- %print(cart(Set1,Set2)),nl, |
| 778 | | (singleton_set(Set1,_) -> small_known_set(Set2) |
| 779 | | ; singleton_set(Set2,_) -> small_known_set(Set1) |
| 780 | | ), |
| 781 | | kernel_objects:cartesian_product_wf(Set1,Set2,Res,WF). |
| 782 | | do_not_keep_symbolic(interval,int(A),int(B),Res,_WF) :- |
| 783 | | (integer(A),nonvar(B),A=B % or B-A < some limit |
| 784 | | -> custom_explicit_sets:convert_to_avl([int(A)],Res)). |
| 785 | | do_not_keep_symbolic(parallel_product,Rel1,Rel2,Res,WF) :- |
| 786 | | not_closure(Rel1), not_closure(Rel2), |
| 787 | | bsets_clp:parallel_product_wf(Rel1,Rel2,Res,WF). |
| 788 | | %do_not_keep_symbolic(overwrite,Rel1,Rel2,Res,WF) :- |
| 789 | | % not_closure(Rel1), not_closure(Rel2), |
| 790 | | % bsets_clp:override_relation(Rel1,Rel2,Res,WF). |
| 791 | | do_not_keep_symbolic(intersection,Set1,Set2,Res,_WF) :- nonvar(Set1), nonvar(Set2), |
| 792 | | % only keep symbolic if at least one non-interval closure |
| 793 | | nonvar_non_interval_closure(Set1,Set2,R12), |
| 794 | | (R12=1 -> |
| 795 | | \+ small_known_set(Set2) % intersection with singleton set can always be computed |
| 796 | | ; R12=2 -> \+ small_known_set(Set1)), |
| 797 | | !, |
| 798 | | (same_closure(Set1,Set2) -> Res = Set1 % Set1 /\ Set1 = Set1 |
| 799 | | ; %% print(symbolic_intersection),nl, translate:print_bvalue(Set1),nl, translate:print_bvalue(Set2),nl,nl, %% |
| 800 | | fail). |
| 801 | | do_not_keep_symbolic(intersection,Set1,Set2,Res,WF) :- % otherwise: compute intersection normally |
| 802 | | Call=kernel_objects:intersection(Set1,Set2,Res,WF), |
| 803 | | must_succ_kernel_call(Call,[Set1,Set2],WF,Call). |
| 804 | | do_not_keep_symbolic(set_subtraction,Set1,Set2,Res,_WF) :- Set2 == [],!, |
| 805 | | Res = Set1. |
| 806 | | do_not_keep_symbolic(set_subtraction,Set1,Set2,Res,_WF) :- nonvar(Set1), |
| 807 | | % only keep symbolic if at least one non-interval closure |
| 808 | | nonvar_non_interval_closure(Set1,Set2,_), |
| 809 | | % check if we cannot construct a complement closure: |
| 810 | | \+ can_construct_complement_closure(Set1,Set2), |
| 811 | | \+ small_known_set(Set1), |
| 812 | | !, |
| 813 | | (same_closure(Set1,Set2) -> Res = [] % Set \ Set = {} |
| 814 | | ; %nl,print(symbolic_set_subtr(Set1,Set2)),nl,nl, %% |
| 815 | | fail). |
| 816 | | do_not_keep_symbolic(set_subtraction,Set1,Set2,Res,WF) :- % otherwise: compute difference normally |
| 817 | | Call=kernel_objects:difference_set_wf(Set1,Set2,Res,WF), % print(diff_set(Set1,Set2,Res)),nl, |
| 818 | | must_succ_kernel_call(Call,[Set1,Set2],WF,Call). |
| 819 | | |
| 820 | | % should succeed if we do not want to keep a unary operator symbolic |
| 821 | | do_not_keep_symbolic_unary(_,ArgValue) :- ArgValue==[],!. |
| 822 | | do_not_keep_symbolic_unary(closure,Set1) :- % this is closure1 |
| 823 | | very_small_known_avl_set(Set1). |
| 824 | | do_not_keep_symbolic_unary(pow_subset,Set1) :- singleton_set(Set1,_). |
| 825 | | do_not_keep_symbolic_unary(fin_subset,Set1) :- singleton_set(Set1,_). |
| 826 | | do_not_keep_symbolic_unary(pow1_subset,Set1) :- singleton_set(Set1,_). |
| 827 | | do_not_keep_symbolic_unary(fin1_subset,Set1) :- singleton_set(Set1,_). |
| 828 | | |
| 829 | | can_construct_complement_closure(Set1,Set2) :- |
| 830 | | nonvar(Set1), nonvar(Set2), Set2 = avl_set(_), |
| 831 | | custom_explicit_sets:is_very_large_maximal_global_set(Set1,_). |
| 832 | | |
| 833 | | nonvar_non_interval_closure(A,B,R) :- (nonvar_non_interval_closure(A) -> R=1 ; nonvar_non_interval_closure(B) -> R=2). |
| 834 | | nonvar_non_interval_closure(A) :- nonvar(A), A=closure(_,_,_), |
| 835 | | \+ custom_explicit_sets:is_interval_closure_or_integerset(A,_,_), |
| 836 | | \+ custom_explicit_sets:is_not_member_value_closure(A,_Type,_MS2). % there isn't full support for this for intersection yet ! TODO fix |
| 837 | | |
| 838 | | % happens quite often e.g. when expanding in state view |
| 839 | | same_closure(X,Y) :- (var(X);var(Y)),!,fail. |
| 840 | | same_closure(closure(P1,T1,B1),closure(P2,T2,B2)) :- |
| 841 | | custom_explicit_sets:same_closure_body(P1,T1, B1, P2,T2,B2). |
| 842 | | |
| 843 | | :- use_module(custom_explicit_sets,[quick_custom_explicit_set_approximate_size/2]). |
| 844 | | small_known_set(AVL) :- nonvar(AVL), AVL=avl_set(A),!, |
| 845 | | quick_custom_explicit_set_approximate_size(avl_set(A),Size), |
| 846 | | Size < 150. |
| 847 | | small_known_set(Closure) :- nonvar(Closure), |
| 848 | | % also accept small intervals; |
| 849 | | % useful e.g., for primes = {x | x>1 & ¬(∃y.(y>1 ∧ y<x ∧ x mod y=0))} ∧ res = primes /\ 1..50 |
| 850 | | custom_explicit_sets:is_interval_closure(Closure,From,To), integer(From), integer(To), |
| 851 | | 1+To-From < 150. |
| 852 | | |
| 853 | | very_small_known_avl_set(AVL) :- nonvar(AVL), AVL=avl_set(A), |
| 854 | | quick_custom_explicit_set_approximate_size(avl_set(A),Size), |
| 855 | | Size < 50. |
| 856 | | |
| 857 | | not_closure(X) :- nonvar(X), \+ functor(X,closure,3). %X \= closure(_,_,_). |
| 858 | | |
| 859 | | % explicit_set([]). explicit_set([_|_]). explicit_set(avl_set(_)). |
| 860 | | |
| 861 | | :- assert_must_fail((kernel_mappings:binary_in_boolean_type(Op,_), |
| 862 | | \+(kernel_mappings:binary_not_in_boolean_type(Op,_)))). |
| 863 | | :- assert_must_fail((kernel_mappings:binary_not_in_boolean_type(Op,_), |
| 864 | | \+(kernel_mappings:binary_in_boolean_type(Op,_)))). |
| 865 | | :- assert_must_fail((kernel_mappings:binary_in_boolean_type(Op,_), \+(kernel_mappings:binary_function(Op,_,_)), |
| 866 | | kernel_mappings:not_symbolic_binary(Op) )). |
| 867 | | |
| 868 | | binary_in_boolean_type(partial_function,bsets_clp:partial_function_wf). |
| 869 | | binary_in_boolean_type(total_function,bsets_clp:total_function_wf). |
| 870 | | binary_in_boolean_type(cartesian_product,kernel_objects:is_cartesian_pair_wf). |
| 871 | | binary_in_boolean_type(partial_surjection,bsets_clp:partial_surjection_wf). |
| 872 | | binary_in_boolean_type(partial_injection,bsets_clp:partial_injection_wf). |
| 873 | | binary_in_boolean_type(total_injection,bsets_clp:total_injection_wf). % >-> |
| 874 | | binary_in_boolean_type(partial_bijection,bsets_clp:partial_bijection_wf). |
| 875 | | binary_in_boolean_type(total_surjection,bsets_clp:total_surjection_wf). % -->> |
| 876 | | binary_in_boolean_type(total_bijection,bsets_clp:total_bijection_wf). % >->> |
| 877 | | binary_in_boolean_type(relations,bsets_clp:relation_over_wf). |
| 878 | | binary_in_boolean_type(total_relation,bsets_clp:total_relation_wf). |
| 879 | | binary_in_boolean_type(surjection_relation,bsets_clp:surjection_relation_wf). |
| 880 | | binary_in_boolean_type(total_surjection_relation,bsets_clp:total_surjection_relation_wf). |
| 881 | | binary_in_boolean_type(interval,kernel_objects:in_nat_range_wf). |
| 882 | | binary_in_boolean_type(parallel_product,bsets_clp:in_parallel_product_wf). |
| 883 | | binary_in_boolean_type(set_subtraction,kernel_objects:in_difference_set_wf). |
| 884 | | binary_in_boolean_type(intersection,kernel_objects:in_intersection_set_wf). |
| 885 | | %binary_in_boolean_type(union,bsets_clp:in_union_set_wf). % makes some CBC checks fail; TO DO: investigate |
| 886 | | binary_in_boolean_type(range_subtraction,bsets_clp:in_range_subtraction_wf). |
| 887 | | binary_in_boolean_type(range_restriction,bsets_clp:in_range_restriction_wf). |
| 888 | | binary_in_boolean_type(domain_subtraction,bsets_clp:in_domain_subtraction_wf). |
| 889 | | binary_in_boolean_type(domain_restriction,bsets_clp:in_domain_restriction_wf). |
| 890 | | %binary_in_boolean_type(overwrite,bsets_clp:in_override_relation_wf). % TO DO: add this, for a more principled symbolic treatment (see test 1491) |
| 891 | | binary_in_boolean_type(composition,bsets_clp:in_composition_wf). |
| 892 | | |
| 893 | | % check whether a binary operator is definitely true; irrespective of arguments |
| 894 | | binary_in_definitely_true(BOP,ValueOfEl) :- nonvar(ValueOfEl), |
| 895 | | binary_definitely_true_based_on_element_value(BOP,ValueOfEl). |
| 896 | | |
| 897 | | binary_definitely_true_based_on_element_value(partial_function,[]). % {} : A +-> B |
| 898 | | binary_definitely_true_based_on_element_value(partial_injection,[]). % {} : A >+> B |
| 899 | | binary_definitely_true_based_on_element_value(relations,[]). % {} : A <-> B |
| 900 | | |
| 901 | | % all make use of WF now: |
| 902 | | binary_not_in_boolean_type(interval,kernel_objects:not_in_nat_range_wf). |
| 903 | | binary_not_in_boolean_type(partial_function,bsets_clp:not_partial_function). |
| 904 | | binary_not_in_boolean_type(partial_surjection,bsets_clp:not_partial_surjection_wf). |
| 905 | | binary_not_in_boolean_type(total_surjection,bsets_clp:not_total_surjection_wf). |
| 906 | | binary_not_in_boolean_type(partial_injection,bsets_clp:not_partial_injection). |
| 907 | | binary_not_in_boolean_type(total_injection,bsets_clp:not_total_injection). |
| 908 | | binary_not_in_boolean_type(partial_bijection,bsets_clp:not_partial_bijection). |
| 909 | | binary_not_in_boolean_type(cartesian_product,kernel_objects:not_is_cartesian_pair). |
| 910 | | binary_not_in_boolean_type(relations,bsets_clp:not_relation_over). |
| 911 | | binary_not_in_boolean_type(total_function,bsets_clp:not_total_function). |
| 912 | | binary_not_in_boolean_type(total_bijection,bsets_clp:not_total_bijection). |
| 913 | | binary_not_in_boolean_type(total_relation,bsets_clp:not_total_relation_wf). |
| 914 | | binary_not_in_boolean_type(surjection_relation,bsets_clp:not_surjection_relation_wf). |
| 915 | | binary_not_in_boolean_type(total_surjection_relation,bsets_clp:not_total_surjection_relation_wf). |
| 916 | | binary_not_in_boolean_type(parallel_product,bsets_clp:not_in_parallel_product_wf). |
| 917 | | binary_not_in_boolean_type(set_subtraction,kernel_objects:not_in_difference_set_wf). |
| 918 | | binary_not_in_boolean_type(intersection,kernel_objects:not_in_intersection_set_wf). |
| 919 | | %binary_not_in_boolean_type(union,bsets_clp:not_in_union_set_wf). |
| 920 | | binary_not_in_boolean_type(range_subtraction,bsets_clp:not_in_range_subtraction_wf). |
| 921 | | binary_not_in_boolean_type(range_restriction,bsets_clp:not_in_range_restriction_wf). |
| 922 | | binary_not_in_boolean_type(domain_subtraction,bsets_clp:not_in_domain_subtraction_wf). |
| 923 | | binary_not_in_boolean_type(domain_restriction,bsets_clp:not_in_domain_restriction_wf). |
| 924 | | binary_not_in_boolean_type(composition,bsets_clp:not_in_composition_wf). |
| 925 | | %binary_not_in_boolean_type(overwrite,bsets_clp:not_in_override_relation_wf). |
| 926 | | % ex: not(f<+{TRUE |-> cT} : BOOL --> NATURAL) & f : BOOL --> NATURAL & cT:NATURAL |
| 927 | | |
| 928 | | |
| 929 | | symbolic_closure_unary_operator(Op) :- |
| 930 | | (unary_in_boolean_type(Op,_)), |
| 931 | | unary_not_in_boolean_type(Op,_), |
| 932 | | \+ not_symbolic_unary(Op). |
| 933 | | |
| 934 | | not_symbolic_unary(domain). |
| 935 | | %not_symbolic_unary(identity). % for Siemens Models |
| 936 | | |
| 937 | | :- assert_must_fail((kernel_mappings:unary_in_boolean_type(Op,_), |
| 938 | | \+(kernel_mappings:unary_not_in_boolean_type(Op,_)))). |
| 939 | | /* note every symbolic closure operator must be dealt with by a unary_in and |
| 940 | | a unary_not_in clause below, otherwise we have a problem */ |
| 941 | | :- assert_must_fail((kernel_mappings:unary_in_boolean_type(UnOp,_), |
| 942 | | \+ kernel_mappings:symbolic_closure_unary_operator(UnOp), |
| 943 | | \+ kernel_mappings:unary_function(UnOp,_,_) )). |
| 944 | | |
| 945 | | |
| 946 | | /* a waitflags version is available for these taking one extra argument (the waitflags): */ |
| 947 | | unary_in_boolean_type(pow_subset,kernel_objects:check_subset_of_wf). |
| 948 | | unary_in_boolean_type(fin_subset,kernel_objects:check_finite_subset_of_wf). |
| 949 | | unary_in_boolean_type(pow1_subset,kernel_objects:check_non_empty_subset_of_wf). |
| 950 | | unary_in_boolean_type(fin1_subset,kernel_objects:check_finite_non_empty_subset_of_wf). |
| 951 | | unary_in_boolean_type(struct,kernel_records:is_a_record_wf). |
| 952 | | unary_in_boolean_type(seq,bsets_clp:is_sequence_wf). /* last arg: basic type */ |
| 953 | | unary_in_boolean_type(iseq,bsets_clp:injective_sequence_wf). |
| 954 | | unary_in_boolean_type(perm,bsets_clp:permutation_sequence_wf). |
| 955 | | unary_in_boolean_type(domain, bsets_clp:in_domain_wf). |
| 956 | | unary_in_boolean_type(seq1,bsets_clp:finite_non_empty_sequence). |
| 957 | | unary_in_boolean_type(iseq1,bsets_clp:injective_non_empty_sequence). |
| 958 | | unary_in_boolean_type(identity,bsets_clp:in_identity). |
| 959 | | unary_in_boolean_type(closure,bsets_clp:in_closure1_wf). %element_of_closure1_wf). % this is closure1 |
| 960 | | %unary_in_boolean_type(reflexive_closure,bsets_clp:element_of_reflexive_closure_wf). % this is closure |
| 961 | | % we could add : inverse?, general_concat, .... ? range: in_range_wf |
| 962 | | |
| 963 | | |
| 964 | | % check whether a unary operator is definitely true; irrespective of arguments |
| 965 | | unary_in_definitely_true(BOP,ValueOfEl) :- nonvar(ValueOfEl), |
| 966 | | unary_definitely_true_based_on_element_value(BOP,ValueOfEl). |
| 967 | | |
| 968 | | unary_definitely_true_based_on_element_value(pow_subset,[]). |
| 969 | | unary_definitely_true_based_on_element_value(fin_subset,[]). |
| 970 | | unary_definitely_true_based_on_element_value(seq,[]). |
| 971 | | unary_definitely_true_based_on_element_value(iseq,[]). |
| 972 | | |
| 973 | | unary_not_in_boolean_type(domain, bsets_clp:not_in_domain_wf). |
| 974 | | unary_not_in_boolean_type(iseq,bsets_clp:not_injective_sequence). |
| 975 | | unary_not_in_boolean_type(struct,kernel_records:not_is_a_record_wf). |
| 976 | | unary_not_in_boolean_type(pow_subset,kernel_objects:not_subset_of_wf). |
| 977 | | unary_not_in_boolean_type(pow1_subset,kernel_objects:not_non_empty_subset_of_wf). |
| 978 | | unary_not_in_boolean_type(fin_subset,kernel_objects:not_finite_subset_of_wf). |
| 979 | | unary_not_in_boolean_type(fin1_subset,kernel_objects:not_non_empty_finite_subset_of_wf). |
| 980 | | unary_not_in_boolean_type(seq,bsets_clp:not_is_sequence_wf). |
| 981 | | unary_not_in_boolean_type(seq1,bsets_clp:not_is_non_empty_sequence_wf). |
| 982 | | unary_not_in_boolean_type(iseq1,bsets_clp:not_non_empty_injective_sequence). |
| 983 | | unary_not_in_boolean_type(perm,bsets_clp:not_permutation_sequence). |
| 984 | | unary_not_in_boolean_type(identity,bsets_clp:not_in_identity). |
| 985 | | unary_not_in_boolean_type(closure,bsets_clp:not_in_closure1_wf). %not_element_of_closure1_wf). % this is closure1 |
| 986 | | %unary_not_in_boolean_type(reflexive_closure,bsets_clp:not_element_of_reflexive_closure_wf). |
| 987 | | |
| 988 | | |
| 989 | | :- assert_must_fail(( kernel_mappings:cst_in_boolean_type(X,_), |
| 990 | | \+ kernel_mappings:cst_not_in_boolean_type(X,_) )). |
| 991 | | :- assert_must_fail(( kernel_mappings:cst_not_in_boolean_type(X,_), |
| 992 | | \+ kernel_mappings:cst_in_boolean_type(X,_) )). |
| 993 | | |
| 994 | | cst_in_boolean_type(string_set,kernel_objects:is_string). |
| 995 | | cst_in_boolean_type(real_set,kernel_reals:is_real_wf). |
| 996 | | cst_in_boolean_type(float_set,kernel_reals:is_float_wf). |
| 997 | | cst_in_boolean_type(integer_set(IntSet),Call) :- integerset_in_boolean_type(IntSet,Call). |
| 998 | | |
| 999 | | |
| 1000 | | :- assert_must_fail(( kernel_mappings:integerset_in_boolean_type(X,_), |
| 1001 | | \+ kernel_mappings:integerset_not_in_boolean_type(X,_) )). |
| 1002 | | :- assert_must_fail(( kernel_mappings:integerset_not_in_boolean_type(X,_), |
| 1003 | | \+ kernel_mappings:integerset_in_boolean_type(X,_) )). |
| 1004 | | |
| 1005 | | integerset_in_boolean_type('INTEGER',kernel_objects:is_integer). |
| 1006 | | integerset_in_boolean_type('NATURAL',kernel_objects:is_natural). |
| 1007 | | integerset_in_boolean_type('NATURAL1',kernel_objects:is_natural1). |
| 1008 | | integerset_in_boolean_type('INT',kernel_objects:is_implementable_int). |
| 1009 | | integerset_in_boolean_type('NAT',kernel_objects:is_implementable_nat). |
| 1010 | | integerset_in_boolean_type('NAT1',kernel_objects:is_implementable_nat1). |
| 1011 | | |
| 1012 | | cst_not_in_boolean_type(string_set,kernel_objects:is_not_string). |
| 1013 | | cst_not_in_boolean_type(real_set,kernel_reals:is_not_real). |
| 1014 | | cst_not_in_boolean_type(float_set,kernel_reals:is_not_float). |
| 1015 | | cst_not_in_boolean_type(integer_set(IntSet),Call) :- integerset_not_in_boolean_type(IntSet,Call). |
| 1016 | | |
| 1017 | | integerset_not_in_boolean_type('INTEGER',kernel_objects:is_not_integer). |
| 1018 | | integerset_not_in_boolean_type('NATURAL',kernel_objects:is_not_natural). |
| 1019 | | integerset_not_in_boolean_type('NATURAL1',kernel_objects:is_not_natural1). |
| 1020 | | integerset_not_in_boolean_type('INT',kernel_objects:is_not_implementable_int). |
| 1021 | | integerset_not_in_boolean_type('NAT',kernel_objects:is_not_implementable_nat). |
| 1022 | | integerset_not_in_boolean_type('NAT1',kernel_objects:is_not_implementable_nat1). |
| 1023 | | |
| 1024 | | % binary_boolean_operator(B-AST-NAME, Module:Predicate, WF_ENABLED) |
| 1025 | | %binary_boolean_operator(member,kernel_objects:element_of). /* not really used: interpreter deals with In explicitly */ |
| 1026 | | %binary_boolean_operator(not_member,kernel_objects:not_element_of_wf,yes). /* not really used: interpreter deals with In explicitly */ |
| 1027 | | binary_boolean_operator(not_equal,kernel_objects:not_equal_object_wf,yes). |
| 1028 | | binary_boolean_operator(equal,kernel_objects:equal_object_optimized,no). |
| 1029 | | binary_boolean_operator(less,kernel_objects:less_than,no). |
| 1030 | | binary_boolean_operator(less_equal,kernel_objects:less_than_equal,no). |
| 1031 | | binary_boolean_operator(less_real,kernel_reals:real_less_than_wf,yes). |
| 1032 | | binary_boolean_operator(less_equal_real,kernel_reals:real_less_than_equal_wf,yes). |
| 1033 | | binary_boolean_operator(greater,kernel_objects:greater_than,no). |
| 1034 | | binary_boolean_operator(greater_equal,kernel_objects:greater_than_equal,no). |
| 1035 | | binary_boolean_operator(subset,kernel_objects:check_subset_of_wf,yes). |
| 1036 | | binary_boolean_operator(subset_strict,kernel_objects:strict_subset_of_wf,yes). |
| 1037 | | binary_boolean_operator(not_subset_strict,kernel_objects:not_strict_subset_of_wf,yes). |
| 1038 | | binary_boolean_operator(not_subset,kernel_objects:not_subset_of_wf,yes). |
| 1039 | | |
| 1040 | | :- assert_must_fail(( kernel_mappings:binary_boolean_operator(X,_,_), |
| 1041 | | \+ kernel_mappings:negate_binary_boolean_operator(X,_), |
| 1042 | | \+ negate_binary_boolean_operator_swap(X,_) )). |
| 1043 | | :- assert_must_fail(( kernel_mappings:binary_boolean_operator(X,_,_), |
| 1044 | | kernel_mappings:negate_binary_boolean_operator(X,Y), Y=X )). |
| 1045 | | :- assert_must_fail(( kernel_mappings:negate_binary_boolean_operator(X,X) )). |
| 1046 | | |
| 1047 | | negate_binary_boolean_operator(X,Y) :- |
| 1048 | | ( negate_binary_boolean_operator2(X,Y) -> true |
| 1049 | ? | ; negate_binary_boolean_operator2(Y,X)). |
| 1050 | | negate_binary_boolean_operator2(member,not_member). |
| 1051 | | negate_binary_boolean_operator2(subset,not_subset). |
| 1052 | | negate_binary_boolean_operator2(subset_strict,not_subset_strict). |
| 1053 | | |
| 1054 | | negate_binary_boolean_operator2(equal,not_equal). |
| 1055 | | negate_binary_boolean_operator2(less,greater_equal). |
| 1056 | | negate_binary_boolean_operator2(less_equal,greater). |
| 1057 | | |
| 1058 | | % negate where we have to swap arguments |
| 1059 | | negate_binary_boolean_operator_swap(less_equal_real,less_real). |
| 1060 | | negate_binary_boolean_operator_swap(less_real,less_equal_real). |
| 1061 | | |
| 1062 | | |
| 1063 | | % input must be list of sets -> second argument set to true if all but one set is known |
| 1064 | | :- block all_but_one_set_known(-,?). |
| 1065 | | all_but_one_set_known([],true). |
| 1066 | | all_but_one_set_known([H|T],KNOWN) :- |
| 1067 | | (T==[] -> KNOWN=true |
| 1068 | ? | ; all_but_one(T,H,KNOWN)). |
| 1069 | | :- block all_but_one(-,?,?). |
| 1070 | | all_but_one([],_H,true). |
| 1071 | ? | all_but_one([H2|T],H1,KNOWN) :- known_value(H2,K2), known_value(H1,K1), all_but_one_wait(K1,K2,T,KNOWN). |
| 1072 | | |
| 1073 | | :- block all_but_one_wait(-,-,?,?), all_but_one_wait(?,?,-,?). |
| 1074 | | all_but_one_wait(K1,K2,[],true) :- K1=true,K2=true. |
| 1075 | | all_but_one_wait(K1,K2,[H3|T],KNOWN) :- known_value(H3,K3), |
| 1076 | ? | (var(K2) -> all_but_one_wait(K2,K3,T,KNOWN) ; all_but_one_wait(K1,K3,T,KNOWN)). |
| 1077 | | |
| 1078 | | :- block known_value(-,-). |
| 1079 | | known_value(_,T) :- T==true,!. |
| 1080 | | known_value(int(X),K) :- !, known_atomic(X,K). |
| 1081 | | known_value(pred_true /* bool_true */,K) :- !, K=true. |
| 1082 | | known_value(pred_false /* bool_false */,K) :- !, K=true. |
| 1083 | | known_value(string(X),K) :- !, known_atomic(X,K). |
| 1084 | | known_value([],K) :- !, K=true. |
| 1085 | | known_value(avl_set(_A),K) :- !, K=true. |
| 1086 | ? | known_value(global_set(X),K) :- !,known_atomic(X,K). |
| 1087 | | known_value(freetype(X),K) :- !,known_atomic(X,K). |
| 1088 | ? | known_value(A,K) :- when(ground(A),K=true). |
| 1089 | | |
| 1090 | | :- block known_atomic(-,?). |
| 1091 | | known_atomic(_,true). |
| 1092 | | |
| 1093 | | |
| 1094 | | % some code to automatically generate documentation for kernel predicates: |
| 1095 | | kernel_predicate(M,P,expression,1,BAST,BOP,WF) :- |
| 1096 | | unary_function(BAST,M,P), get_waitflag_info(P,WF), |
| 1097 | | (translate:unary_prefix(BAST,BOP,_) -> true |
| 1098 | | ; translate:unary_postfix(BAST,BOP,_) -> true |
| 1099 | | ; translate:function_like(BAST,BOP) -> true |
| 1100 | | ; BOP = '??'). |
| 1101 | | kernel_predicate(M,P,expression,2,BAST,BOP,WF) :- |
| 1102 | | binary_function(BAST,M,P), get_waitflag_info(P,WF), |
| 1103 | | (translate:binary_infix(BAST,BOP,_,_) -> true |
| 1104 | | ; translate:function_like(BAST,BOP) -> true ; BOP = '??'). |
| 1105 | | kernel_predicate(M,P,predicate,2,BAST,BOP,WF) :- |
| 1106 | | binary_boolean_operator(BAST,M:P,WF), |
| 1107 | | (translate:binary_infix(BAST,BOP,_,_) -> true |
| 1108 | | ; translate:function_like(BAST,BOP) -> true ; BOP = '??'). |
| 1109 | | |
| 1110 | | get_waitflag_info(P,WF) :- |
| 1111 | | (expects_waitflag_and_span(P) -> WF = wf_span ; |
| 1112 | | expects_waitflag_and_span(P) -> WF = yes ; |
| 1113 | | WF = no). |
| 1114 | | :- public generate_documentation/0. |
| 1115 | | generate_documentation :- |
| 1116 | | kernel_predicate(M,P,_T,ARITY,BAST,BOP,_WF), |
| 1117 | | ( symbolic_closure_unary_operator(BOP) -> Sym=' (symbolic_unary)' |
| 1118 | | ; symbolic_closure_binary_operator(BOP) -> Sym=' (symbolic_binary)' % these not printed as binary_function does not include them |
| 1119 | | ; Sym= ''), |
| 1120 | | format(' ~w (~w/~w) --> ~w:~w ~w~n',[BOP,BAST,ARITY,M,P,Sym]), |
| 1121 | | fail. |
| 1122 | | generate_documentation. |
| 1123 | | |
| 1124 | | :- use_module(library(codesio), [with_output_to_codes/2]). |
| 1125 | | :- assert_must_succeed((with_output_to_codes(kernel_mappings:generate_documentation, Codes), Codes \= [])). |
| 1126 | | |