| 1 | % (c) 2020-2026 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(well_def_prover, [prove_po/3]). | |
| 6 | ||
| 7 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 8 | :- module_info(group,well_def_prover). | |
| 9 | :- module_info(description,'This module proves WD POs.'). | |
| 10 | ||
| 11 | :- use_module(library(avl)). | |
| 12 | :- use_module(library(lists)). | |
| 13 | ||
| 14 | :- use_module(wdsrc(well_def_hyps),[get_hyp_var_type/3, portray_hyps/1, get_clash_renaming_subst/2, | |
| 15 | is_hyp_var/2, is_finite_type_for_wd/2, add_new_hyp_any_vars/3, negate_op/2, | |
| 16 | hyps_inconsistent/1, | |
| 17 | push_normalized_hyp/3, push_and_rename_normalized_hyp/3]). | |
| 18 | ||
| 19 | :- use_module(wdsrc(well_def_tools), [rename_norm_term/3, member_in_norm_conjunction/2, not_occurs/2, occurs/2]). | |
| 20 | :- use_module(probsrc(debug)). | |
| 21 | :- use_module(probsrc(error_manager),[add_error/3, add_internal_error/2]). | |
| 22 | ||
| 23 | :- use_module(probsrc(custom_explicit_sets),[domain_of_explicit_set_wf/3, equal_avl_tree/2, | |
| 24 | range_of_explicit_set_wf/3, | |
| 25 | invert_explicit_set/2,check_interval_in_custom_set/4, | |
| 26 | check_avl_in_interval/3, check_avl_subset/2, is_one_element_avl/2, | |
| 27 | avl_is_interval/3, | |
| 28 | expand_custom_set_to_list/2, quick_definitely_maximal_set_avl/1, | |
| 29 | expand_and_convert_to_avl_set/4, safe_is_avl_sequence/1, is_avl_partial_function/1]). | |
| 30 | ||
| 31 | :- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
| 32 | ||
| 33 | % PROVING: | |
| 34 | % -------- | |
| 35 | ||
| 36 | ||
| 37 | % some more rules are covered in process_sequent_aux of prove_sequent/3 | |
| 38 | prove_po(truth,_,truth). | |
| 39 | prove_po(_NormTarget,Hyps,false_hyp) :- hyps_inconsistent(Hyps). | |
| 40 | prove_po(NormTarget,hyp_rec(AVL,_),hyp) :- avl_fetch(NormTarget,AVL). | |
| 41 | prove_po(member(X,Y),Hyps,mem(PT)) :- % Y is usually domain(Func) | |
| 42 | simplify_expr_loop(Y,Hyps,SY), | |
| 43 | simplify_expr_loop(X,Hyps,SX), | |
| 44 | check_member_of_set(SY,SX,Hyps,PT). | |
| 45 | prove_po(not_member(X,Y),Hyps,mem(PT)) :- | |
| 46 | simplify_expr_loop(Y,Hyps,SY), | |
| 47 | simplify_expr_loop(X,Hyps,SX), | |
| 48 | check_not_member_of_set(SY,SX,Hyps,PT). | |
| 49 | prove_po(finite(Set),Hyp,finite_set(PT)) :- check_finite(Set,Hyp,PT). | |
| 50 | prove_po(not_equal(A,B),Hyp,not_equal) :- | |
| 51 | simplify_expr_loop(A,Hyp,SA), | |
| 52 | simplify_expr_loop(B,Hyp,SB), | |
| 53 | check_not_equal(SA,SB,Hyp). | |
| 54 | prove_po(equal(A,B),Hyp,equal) :- % not generated by our POG | |
| 55 | simplify_expr_loop(A,Hyp,SA), | |
| 56 | simplify_expr_loop(B,Hyp,SB), | |
| 57 | check_equal(SA,SB,Hyp,_). | |
| 58 | prove_po(greater(A,B),Hyp,PT) :- prove_po(less(B,A),Hyp,PT). | |
| 59 | prove_po(greater_equal(A,B),Hyp,greater_equal) :- % print(check_leq(B,A)),nl, | |
| 60 | check_leq(B,A,Hyp). | |
| 61 | prove_po(less_equal(A,B),Hyp,less_equal) :- | |
| 62 | check_leq(A,B,Hyp). | |
| 63 | %prove_po(less_equal_real(A,B),Hyp,less_equal_real) :- | |
| 64 | % check_leq(A,B,Hyp). % TODO: check that all proof rules are sound for reals, ditto for less | |
| 65 | prove_po(less(A,B),Hyp,less) :- | |
| 66 | check_leq(A,B,Hyp),!, | |
| 67 | check_not_equal(A,B,Hyp). | |
| 68 | prove_po(subset(A,B),Hyp,PT) :- | |
| 69 | simplify_expr_loop(A,Hyp,SA), simplify_expr_loop(B,Hyp,SB), | |
| 70 | check_is_subset(SA,SB,Hyp,PT). | |
| 71 | prove_po(subset_strict(A,B),Hyp,subset_strict(PT)) :- | |
| 72 | simplify_expr_loop(A,Hyp,SA), simplify_expr_loop(B,Hyp,SB), | |
| 73 | check_is_subset_strict(SA,SB,Hyp,PT). | |
| 74 | prove_po(not_subset_strict(A,B),Hyp,not_subset_strict(PT)) :- | |
| 75 | simplify_expr_loop(A,Hyp,SA), simplify_expr_loop(B,Hyp,SB), | |
| 76 | check_not_is_subset_strict(SA,SB,Hyp,PT). | |
| 77 | prove_po(not_subset(A,B),Hyp,not_subset(PT)) :- | |
| 78 | simplify_expr_loop(A,Hyp,SA), simplify_expr_loop(B,Hyp,SB), | |
| 79 | check_not_subset(SA,SB,Hyp,PT). | |
| 80 | prove_po(conjunct(A,B),Hyp,conj(T1,T2)) :- % generated by Rodin | |
| 81 | prove_po(A,Hyp,T1), | |
| 82 | !, | |
| 83 | prove_po(B,Hyp,T2). | |
| 84 | prove_po(disjunct(A,B),Hyp,conj(T1,T2)) :- % could be generated by Rodin | |
| 85 | (% push_normalized_hyp(NotB,Hyp,Hyp2), % % OR_R rule allows to add not(B) as hypothesis | |
| 86 | prove_po(A,Hyp,T1) -> true | |
| 87 | ; prove_po(B,Hyp,T2)). % OR_R rule allows to add not(A) as hypothesis, this is done in prove_sequent_goal | |
| 88 | prove_po(implication(A,B),Hyp,imply(T2)) :- % generated by Rodin; now treated in prove_sequent_goal | |
| 89 | % also generated for power_of_real | |
| 90 | (prove_negated_po(A,Hyp,PT) -> T2=false_lhs(PT) | |
| 91 | ; debug_println(19,not_pushing_lhs_for_implication(A)), | |
| 92 | %push_normalized_hyp(A,Hyp,Hyp2), % TODO: activate this | |
| 93 | prove_po(B,Hyp,T2) | |
| 94 | ). | |
| 95 | prove_po(exists([$(B0)],forall([$(X)],member($(X),Set),less_equal($(X),$(B0)))),Hyp,finite_max(PT)) :- X \= B0, | |
| 96 | % generated by Rodin for max(Set) | |
| 97 | debug_println(19,checking_finite_for_max(Set)), | |
| 98 | check_finite(Set,Hyp,PT). | |
| 99 | prove_po(exists([$(B0)],forall([$(X)],member($(X),Set),less_equal($(B0),$(X)))),Hyp,finite_min(PT)) :- X \= B0, | |
| 100 | % generated by Rodin for min(Set) | |
| 101 | debug_println(19,checking_finite_for_min(Set)), | |
| 102 | check_finite(Set,Hyp,PT). | |
| 103 | prove_po(negation(Goal),Hyp,negation(PT)) :- prove_negated_po(Goal,Hyp,PT). | |
| 104 | %prove_po(NT,_,_) :- format('Unproven by WD Prover: ~w~n~n',[NT]),fail. | |
| 105 | ||
| 106 | % some redundancy wrt negate_hyp; but negate_hyp currently does not go inside conjunction | |
| 107 | prove_negated_po(falsity,_,falsity) :- !. | |
| 108 | prove_negated_po(disjunct(A,B),Hyp,negdisj(T1,T2)) :- !, | |
| 109 | (prove_negated_po(A,Hyp,T1) -> prove_negated_po(B,Hyp,T2)). | |
| 110 | prove_negated_po(conjunct(A,B),Hyp,negconj(T1,T2)) :- !, % could be generated by Rodin | |
| 111 | (prove_negated_po(A,Hyp,T1) -> true | |
| 112 | ; prove_negated_po(B,Hyp,T2)). % we could add not(A) as hypothesis, | |
| 113 | prove_negated_po(negation(Goal),Hyp,negation(PT)) :-!, prove_po(Goal,Hyp,PT). | |
| 114 | prove_negated_po(OP,Hyp,negated_op(PT)) :- negate_op(OP,NOP), prove_po(NOP,Hyp,PT). | |
| 115 | ||
| 116 | ||
| 117 | simple_value(Nr) :- number(Nr). | |
| 118 | simple_value('$'(_)). | |
| 119 | simple_value(boolean_true). | |
| 120 | simple_value(boolean_false). | |
| 121 | simple_value(record_field('$'(_),_)). | |
| 122 | simple_value(value(_)). | |
| 123 | simple_value(string(_)). | |
| 124 | simple_value(function(F,_)) :- simple_value(F). | |
| 125 | simple_value(couple(A,B)) :- simple_value(A), simple_value(B). | |
| 126 | ||
| 127 | %get_set_of_possible_values(X,Hyps,XSet) :- | |
| 128 | % if(try_get_set_of_possible_values(X,Hyps,R), XSet=R, | |
| 129 | % XSet=set_extension([X])). % was typeset | |
| 130 | ||
| 131 | try_get_set_of_possible_values(Nr,Hyps,R,Hyps) :- number(Nr),!,R=interval(Nr,Nr). | |
| 132 | try_get_set_of_possible_values(X,Hyps,R,Hyps) :- | |
| 133 | avl_fetch_binop_from_hyps_no_loop_check(X,equal,Hyps,Nr), number(Nr),!, % TODO: also treat is_explicit_value | |
| 134 | R=interval(Nr,Nr). | |
| 135 | try_get_set_of_possible_values(X,Hyps,XSet,Hyps2) :- | |
| 136 | avl_fetch_worthwhile_mem_from_hyps(X,Hyps,XSet1,Hyps1), | |
| 137 | (improve_integer_set_precision(X,XSet1,Hyps1,XSet,Hyps2) | |
| 138 | -> true ; Hyps2=Hyps1, XSet=XSet1). | |
| 139 | try_get_set_of_possible_values(X,Hyps,Res,Hyps3) :- | |
| 140 | avl_fetch_equal_from_hyps(X,Hyps,X2,Hyps1), | |
| 141 | quick_not_occurs_check(X,X2), | |
| 142 | rewrite_local_loop_check(X,try_get_set_of_possible_values,X2,Hyps1,Hyps2), | |
| 143 | (X2='$'(_) -> X = '$'(_) ; true), % avoid rewriting x -> card(...) -> x; TO DO: better cyclic equality prevention | |
| 144 | try_get_set_of_possible_values(X2,Hyps2,Res,Hyps3), !. | |
| 145 | try_get_set_of_possible_values(function(Func,Args),Hyps,RangeSet,Hyps2) :- !, | |
| 146 | (get_range_or_superset(Func,Hyps,RangeSet,Hyps2) -> true | |
| 147 | ; rewrite_function_application(Func,Args,Hyps,Result,Hyps1), % maybe put this first? | |
| 148 | try_get_set_of_possible_values(Result,Hyps1,RangeSet,Hyps2)). | |
| 149 | try_get_set_of_possible_values(first(Seq),Hyps,RangeSet,Hyps2) :- !, % first(S) === S(1) | |
| 150 | get_range_or_superset(Seq,Hyps,RangeSet,Hyps2). | |
| 151 | try_get_set_of_possible_values(last(Seq),Hyps,RangeSet,Hyps2) :- !, % last(S) === S(size(S)) | |
| 152 | get_range_or_superset(Seq,Hyps,RangeSet,Hyps2). | |
| 153 | % TO DO other sequence operations | |
| 154 | try_get_set_of_possible_values(couple(A,B),Hyps,cartesian_product(SA,SB),Hyps2) :- !, | |
| 155 | try_get_set_of_possible_values(A,Hyps,SA,Hyps1), | |
| 156 | try_get_set_of_possible_values(B,Hyps1,SB,Hyps2). | |
| 157 | try_get_set_of_possible_values(max(set_extension([V1,V2|_])),H,'NATURAL',H) :- % max({x,-x}) >= 0 | |
| 158 | ( V1 = unary_minus(V2), \+ number(V1) -> true | |
| 159 | ; V2 = unary_minus(V1), \+ number(V2) -> true), !. % instead of NATURAL we could try and infer values for V1/V2 | |
| 160 | try_get_set_of_possible_values(max(Set),H,Set,H). | |
| 161 | try_get_set_of_possible_values(min(Set),H,Set,H). | |
| 162 | try_get_set_of_possible_values(mu(Set),H,Set,H). | |
| 163 | try_get_set_of_possible_values(external_function_call(Call,Args),H,Set,H) :- | |
| 164 | external_function_possible_vals(Call,Args,Set). % treats CHOOSE, MU, ABS, LCM, GCD, ... | |
| 165 | try_get_set_of_possible_values(max_int,H,'NATURAL1',H). | |
| 166 | % TO DO: min_int | |
| 167 | try_get_set_of_possible_values(value(avl_set(A1)),Hyps,value(avl_set(A2)),Hyps) :- !, | |
| 168 | expand_and_convert_to_avl_set([avl_set(A1)],A2,get_set_of_possible_values,'WD(?)'). | |
| 169 | try_get_set_of_possible_values(add(X,Y),Hyps,Set,Hyps2) :- | |
| 170 | add_with_number(add(X,Y),A,Nr), | |
| 171 | try_get_set_of_possible_values(A,Hyps,ValA,Hyps2), | |
| 172 | add_to_value_set(ValA,Nr,Set),!. | |
| 173 | try_get_set_of_possible_values(minus(A,Nr),Hyps,Set,Hyps2) :- number(Nr), Nr1 is -Nr, | |
| 174 | try_get_set_of_possible_values(A,Hyps,ValA,Hyps2), | |
| 175 | add_to_value_set(ValA,Nr1,Set),!. | |
| 176 | % TO DO : add unary_minus, multiplication with nr | |
| 177 | try_get_set_of_possible_values(Seq,Hyps,Set,Hyps) :- | |
| 178 | infer_sequence_type_of_expr(Seq,Hyps,SeqType),!, | |
| 179 | (SeqType=seq1 -> Set=seq1(typeset) ; Set=seq(typeset)). % TO DO: examine type of list elements | |
| 180 | try_get_set_of_possible_values(X,Hyps,XSet,Hyps2) :- | |
| 181 | avl_fetch_binop_from_hyps(X,greater_equal,Hyps,Low,Hyps1), !, | |
| 182 | (avl_fetch_binop_from_hyps(X,less_equal,Hyps1,Up,Hyps2) -> XSet = interval(Low,Up) | |
| 183 | ; Low=0 -> XSet = 'NATURAL', Hyps2=Hyps1 | |
| 184 | ; number(Low),Low>0 -> XSet= 'NATURAL1', Hyps2=Hyps1). % TO DO: improve precision | |
| 185 | try_get_set_of_possible_values(X,Hyps,XSet,Hyps2) :- | |
| 186 | rewrite_integer(X,Hyps,X2,Hyps1),!, | |
| 187 | try_get_set_of_possible_values(X2,Hyps1,XSet,Hyps2). | |
| 188 | try_get_set_of_possible_values(size(A),Hyps,XSet,Hyps) :- | |
| 189 | (check_not_empty_set(A,Hyps) -> XSet = 'NATURAL1' ; XSet='NATURAL'). | |
| 190 | try_get_set_of_possible_values(card(A),Hyps,XSet,Hyps) :- | |
| 191 | (check_not_empty_set(A,Hyps) -> XSet = 'NATURAL1' ; XSet='NATURAL'). | |
| 192 | try_get_set_of_possible_values(if_then_else(_,A,B),Hyps,R,Hyps) :- | |
| 193 | (try_get_set_of_possible_values(A,Hyps,AV,Hyps1) | |
| 194 | -> try_get_set_of_possible_values(B,Hyps1,BV,Hyps2)), | |
| 195 | construct_union(AV,BV,Hyps2,R). | |
| 196 | try_get_set_of_possible_values(modulo(A,B),Hyps1,XSet,Hyps2) :- | |
| 197 | number(B), B>0, | |
| 198 | B1 is B-1, | |
| 199 | XSet1 = interval(0,B1), % value of A mod B must be in 0..B1 | |
| 200 | % note: this also holds in z_or_tla_minor_mode, we have (-3) mod 2 = 1 | |
| 201 | (try_get_set_of_possible_values(A,Hyps1,XSet2,Hyps2), | |
| 202 | maximal_value(XSet2,Up) | |
| 203 | -> intersect_sets(XSet1,interval(0,Up),XSet) | |
| 204 | % we were able to reduce the interval further by finding possible upper-bound for A | |
| 205 | % we could call improve_upper_bound | |
| 206 | ; Hyps2=Hyps1, XSet=XSet1). | |
| 207 | try_get_set_of_possible_values(external_function_call(Name,Args),Hyps,R,Hyps) :- | |
| 208 | external_function_returns_sequence_type(Name,Args,Hyps,_,R). | |
| 209 | ||
| 210 | %try_get_set_of_possible_values(X,_,_,_) :- print(try_get_set_of_possible_values_failed(X)),nl,fail. | |
| 211 | % TO DO: more precise representation of open-ended intervals interval(Low,'$infinity')) | |
| 212 | % TO DO: intersect multiple solutions; e.g., intervals and >=, <= constraints | |
| 213 | ||
| 214 | maximal_value(interval(_,Up),Up). | |
| 215 | maximal_value(value(avl_set(A)),Up) :- avl_max(A,int(Up)). | |
| 216 | % TO DO: add avl_set | |
| 217 | ||
| 218 | ||
| 219 | is_integer_set(interval(_,_)). | |
| 220 | is_integer_set('NATURAL'). | |
| 221 | is_integer_set('NATURAL1'). | |
| 222 | is_integer_set('INTEGER'). | |
| 223 | % TO DO: add avl_set | |
| 224 | ||
| 225 | % detect sets which can profit from narrowing down: | |
| 226 | is_infinite__or_large_integer_set('NATURAL',0,inf). | |
| 227 | is_infinite__or_large_integer_set('NATURAL1',1,inf). | |
| 228 | %is_infinite__or_large_integer_set('INTEGER',-inf,inf). | |
| 229 | is_infinite__or_large_integer_set(interval(Low,max_int),Low,max_int). % one cannot prove a lot with max_int anyway!? | |
| 230 | ||
| 231 | % try and improve precision of integer set | |
| 232 | % limitation: only looks for one other hypotheses; maybe we should do this in well_defs_hyps.pl | |
| 233 | improve_integer_set_precision(X,XSet1,Hyps1,NewSet,Hyps3) :- | |
| 234 | is_integer_set(XSet1), | |
| 235 | avl_fetch_worthwhile_mem_from_hyps(X,Hyps1,XSet2,Hyps2), | |
| 236 | XSet2 \= XSet1, | |
| 237 | !, | |
| 238 | intersect_sets(XSet1,XSet2,XSet12), | |
| 239 | try_improve_interval(XSet12,X,Hyps2,NewSet,Hyps3). % TO DO: we could try and find another member | |
| 240 | % TO DO: also look at less_equal, greater_equal constraints | |
| 241 | improve_integer_set_precision(X,XSet1,Hyps1,NewSet,Hyps3) :- | |
| 242 | is_infinite__or_large_integer_set(XSet1,Low,LargeUp), | |
| 243 | avl_fetch_binop_from_hyps(X,less_equal,Hyps1,Up,Hyps2), | |
| 244 | Up \= LargeUp, % we really improve upon earlier value | |
| 245 | !, | |
| 246 | try_improve_interval(interval(Low,Up),X,Hyps2,NewSet,Hyps3). | |
| 247 | improve_integer_set_precision(X,XSet1,Hyps1,NewSet,Hyps2) :- | |
| 248 | try_improve_interval(XSet1,X,Hyps1,NewSet,Hyps2). | |
| 249 | ||
| 250 | try_improve_interval(interval(OldLow,OldUp),X,Hyps1,interval(NewLow,NewUp),Hyps2) :- !, | |
| 251 | improve_interval(X,OldLow,OldUp,Hyps1,NewLow,NewUp,Hyps2). | |
| 252 | try_improve_interval(Set,_,Hyps,Set,Hyps). | |
| 253 | ||
| 254 | % phase 1: try improve upper bound | |
| 255 | improve_interval(X,OldLow,OldUp,Hyps1,NewLow,NewUp,Hyps3) :- | |
| 256 | improve_upper_bound(X,OldUp,Hyps1,NewUp1,Hyps2),!, | |
| 257 | improve_interval(X,OldLow,NewUp1,Hyps2,NewLow,NewUp,Hyps3). | |
| 258 | improve_interval(X,OldLow,Up,Hyps1,NewLow,Up,Hyps2) :- | |
| 259 | improve_interval2(X,OldLow,Hyps1,NewLow,Hyps2). | |
| 260 | % | |
| 261 | improve_upper_bound(X,OldUp,Hyps1,NewUp,Hyps2) :- | |
| 262 | avl_fetch_binop_from_hyps(X,less_equal,Hyps1,Up,Hyps2), | |
| 263 | order_values(OldUp,Up,NewUp,OldUp), | |
| 264 | NewUp \= OldUp. | |
| 265 | ||
| 266 | % now try and improve lower bound: | |
| 267 | improve_interval2(X,OldLow,Hyps1,NewLow,Hyps3) :- | |
| 268 | improve_lower_bound(X,OldLow,Hyps1,Low1,Hyps2),!, | |
| 269 | improve_interval2(X,Low1,Hyps2,NewLow,Hyps3). | |
| 270 | improve_interval2(_,Low,Hyps,Low,Hyps). | |
| 271 | % | |
| 272 | improve_lower_bound(X,OldLow,Hyps1,NewLow,Hyps2) :- | |
| 273 | avl_fetch_binop_from_hyps(X,greater_equal,Hyps1,Low,Hyps2), | |
| 274 | order_values(Low,OldLow,OldLow,NewLow), | |
| 275 | NewLow \= OldLow. | |
| 276 | ||
| 277 | ||
| 278 | % try and intersect two sets: | |
| 279 | intersect_sets(interval(L1,U1),B,Res) :- !, intersect_interval(B,L1,U1,Res). | |
| 280 | intersect_sets(B,interval(L1,U1),Res) :- intersect_interval(B,L1,U1,Res). | |
| 281 | intersect_sets('NATURAL1','NATURAL','NATURAL1'). | |
| 282 | intersect_sets('NATURAL','NATURAL1','NATURAL1'). | |
| 283 | % TODO: support avl_set | |
| 284 | ||
| 285 | intersect_interval(interval(L2,U2),L1,U1,interval(L3,U3)) :- | |
| 286 | order_values(L1,L2,_,L3), % choose larger value as lower bound | |
| 287 | order_values(U1,U2,U3,_). % choose smaller value as upper bound | |
| 288 | intersect_interval('NATURAL1',L1,U1,interval(L3,U1)) :- order_values(L1,1,L3,_). | |
| 289 | intersect_interval('NATURAL',L1,U1,interval(L3,U1)) :- order_values(L1,0,L3,_). | |
| 290 | ||
| 291 | % order values for interval intersection | |
| 292 | order_values(N1,N2,R1,R2) :- number(N1),!, order_aux_nr(N2,N1,R1,R2). | |
| 293 | order_values(N1,N2,R1,R2) :- number(N2),!, order_aux_nr(N1,N2,R1,R2). | |
| 294 | order_values(min_int,N2,R1,R2) :- !, R1=min_int,R2=N2. | |
| 295 | order_values(max_int,N2,R1,R2) :- !, R1=N2,R2=max_int. | |
| 296 | order_values(N1,N2,N1,N2). % just choose N1 | |
| 297 | ||
| 298 | order_aux_nr(N2,N1,R1,R2) :- number(N2),!, | |
| 299 | (N2>N1 -> R1=N1,R2=N2 ; R1=N2,R2=N1). | |
| 300 | order_aux_nr(max_int,N1,R1,R2) :- N1 < 1, !, R1=N1, R2=max_int. | |
| 301 | order_aux_nr(_N2,N1,N1,N1). % choose the number as the bound | |
| 302 | ||
| 303 | ||
| 304 | ||
| 305 | add_to_value_set(interval(L,U),Nr,interval(L2,U2)) :- | |
| 306 | add_nr(L,Nr,L2), | |
| 307 | (add_nr(U,Nr,U2) -> true ; Nr =< 0, U2=U). % e.g., if U = size(x) we create an over-approximation | |
| 308 | add_to_value_set('NATURAL',1,'NATURAL1'). % TO DO: extend | |
| 309 | %add_to_value_set(value(avl_set(A1),Nr,value(avl_set(A2)) :- TO DO: add Nr to all values in A2 | |
| 310 | ||
| 311 | % adding a known number to an arithmetic expression; could be extended | |
| 312 | % this is mainly for dealing with index arithmetic for arrays | |
| 313 | add_nr(Nr1,ToAdd,Nr2) :- number(Nr1),!, Nr2 is Nr1+ToAdd. | |
| 314 | add_nr(minus(Expr,Nr1),ToAdd,Res) :- number(Nr1),!, Nr2 is Nr1-ToAdd, | |
| 315 | (Nr2=0 -> Res=Expr ; Res= minus(Expr,Nr2)). | |
| 316 | add_nr(add(Expr,Nr1),ToAdd,Res) :- number(Nr1),!, Nr2 is Nr1+ToAdd, | |
| 317 | (Nr2=0 -> Res=Expr ; Res= add(Expr,Nr2)). | |
| 318 | add_nr(add(Nr1,Expr),ToAdd,Res) :- number(Nr1),!, Nr2 is Nr1+ToAdd, | |
| 319 | (Nr2=0 -> Res=Expr ; Res= add(Expr,Nr2)). | |
| 320 | ||
| 321 | ||
| 322 | % check if an expression is a sequence | |
| 323 | check_is_sequence(El,Hyps) :- check_is_sequence(El,Hyps,_). | |
| 324 | check_is_non_empty_sequence(El,Hyps) :- check_is_sequence(El,Hyps,seq1). | |
| 325 | ||
| 326 | check_is_sequence(S,_,seq) :- is_empty_set_direct(S),!. | |
| 327 | check_is_sequence(El,Hyps,RequiredType) :- | |
| 328 | infer_sequence_type_of_expr(El,Hyps,Type), | |
| 329 | (Type=seq1 -> true ; RequiredType=seq -> true | |
| 330 | ; check_not_equal_empty_set(El,Hyps,_)), !. | |
| 331 | check_is_sequence(A,Hyps,RequiredType) :- | |
| 332 | avl_fetch_worthwhile_equal_from_hyps(A,Hyps,Value,Hyps2), | |
| 333 | check_is_sequence(Value,Hyps2,RequiredType), !. | |
| 334 | check_is_sequence(domain_restriction(Dom,S),Hyps,Res) :- !, | |
| 335 | is_interval(Dom,Hyps,1,N), | |
| 336 | check_is_sequence(S,Hyps,SeqType), | |
| 337 | (SeqType=seq1, check_leq(1,N,Hyps) -> Res=seq1 ; Res=seq). | |
| 338 | check_is_sequence(El,Hyps,RequiredType) :- | |
| 339 | avl_fetch_mem_or_struct(El,Hyps,Set,Hyps2), | |
| 340 | is_set_of_sequences_type(Set,Hyps2,Type), % should we move this to subset? dealt with in subset_transitivity_rule | |
| 341 | % required for :wd Right:seq(BOOL) & (Right/=[] => tail(Right)=res) in test 2018 | |
| 342 | (Type=seq1 -> true ; RequiredType=seq -> true | |
| 343 | ; check_not_equal_empty_set(El,Hyps2,_)), | |
| 344 | !. | |
| 345 | check_is_sequence(X,Hyps,RequiredType) :- try_get_set_of_possible_values(X,Hyps,XSet,Hyps2), | |
| 346 | (RequiredType==seq1 -> check_is_subset(XSet,seq1(typeset),Hyps2,_PT) | |
| 347 | ; check_is_subset(XSet,seq(typeset),Hyps2,_PT)). | |
| 348 | % check if something is an interval | |
| 349 | is_interval(Expr,Hyps,A,B) :- simplify_expr_loop(Expr,Hyps,SE), is_interval_aux(SE,A,B). | |
| 350 | is_interval_aux(interval(A,B),A,B). | |
| 351 | is_interval_aux(value(CS),A,B) :- nonvar(CS), CS= avl_set(AVL), avl_is_interval(AVL,A,B). | |
| 352 | ||
| 353 | is_set_of_sequences_type(seq1(_),_,seq1) :- !. | |
| 354 | is_set_of_sequences_type(seq(_),_,seq) :- !. | |
| 355 | is_set_of_sequences_type(iseq(_),_,seq) :- !. | |
| 356 | is_set_of_sequences_type(iseq1(_),_,seq) :- !. | |
| 357 | is_set_of_sequences_type(perm(A),Hyps,Type) :- !, | |
| 358 | (check_not_equal_empty_set(A,Hyps,_) -> Type=seq1 ; Type=seq). | |
| 359 | is_set_of_sequences_type(Func,Hyps,Type) :- % a total function 1..Up --> Range is a sequence | |
| 360 | get_exact_domain_of_func_or_rel_type(Func,Hyps,Dom,Hyps1), | |
| 361 | check_equal_pattern(Dom,interval(1,Up),Hyps1,Hyps2), | |
| 362 | % we could call check_equal for Low; relevant for :wd BV=16 & II=1 & BIdx = II..BV & s:BIdx --> BOOL & res=size(s) | |
| 363 | is_partial_function_type(Func,Hyps2,_), | |
| 364 | (number(Up), Up>0 % we could call check_leq | |
| 365 | -> Type=seq1 ; Type=seq). | |
| 366 | ||
| 367 | % a simple equality check | |
| 368 | check_equal_pattern(A,Target,Hyps,Hyps1) :- | |
| 369 | check_equal_h(A,Target,not_ground,[],Hyps,Hyps1). | |
| 370 | check_equal(A,Target,Hyps,Hyps1) :- | |
| 371 | check_equal_h(A,Target,ground,[],Hyps,Hyps1). | |
| 372 | ||
| 373 | % TargetGround=ground means Target is a ground, fully known expressions and not a pattern with variables | |
| 374 | check_equal_h(A,Target,_,_,Hyps,Hyps1) :- %write(check_eq(A,Target)),nl, | |
| 375 | A=Target,!, Hyps1=Hyps. | |
| 376 | check_equal_h(BOP1,BOP2,TGr,History,Hyps,Hyps2) :- | |
| 377 | commutative_bin_op(BOP1,F,A1,A2), commutative_bin_op(BOP2,F,B1,B2), | |
| 378 | (check_equal_h(A1,B1,TGr,History,Hyps,Hyps1) | |
| 379 | -> !, check_equal_h(A2,B2,TGr,History,Hyps1,Hyps2) | |
| 380 | ; check_equal_h(A1,B2,TGr,History,Hyps,Hyps1) | |
| 381 | -> !, check_equal_h(A2,B1,TGr,History,Hyps1,Hyps2) | |
| 382 | ). | |
| 383 | check_equal_h(BOP1,BOP2,TGr,History,Hyps,Hyps2) :- | |
| 384 | non_commutative_bin_op(BOP1,F,A1,A2), non_commutative_bin_op(BOP2,F,B1,B2), | |
| 385 | check_equal_h(A1,B1,TGr,History,Hyps,Hyps1),!, | |
| 386 | check_equal_h(A2,B2,TGr,History,Hyps1,Hyps2). | |
| 387 | check_equal_h(UNOP1,UNOP2,TGr,History,Hyps,Hyps1) :- | |
| 388 | unary_op(UNOP1,F,A1), unary_op(UNOP2,F,B1), | |
| 389 | check_equal_h(A1,B1,TGr,History,Hyps,Hyps1),!. | |
| 390 | % TO DO: records, ... | |
| 391 | check_equal_h(A,Target,TGr,History,Hyps,Hyps2) :- | |
| 392 | avl_fetch_equal_from_hyps(A,Hyps,A2,Hyps1), nonmember(A2,History), | |
| 393 | check_equal_h(A2,Target,TGr,[A|History],Hyps1,Hyps2). | |
| 394 | check_equal_h(A,Target,TGr,History,Hyps,Hyps2) :- Target = '$'(_), | |
| 395 | avl_fetch_equal_from_hyps(Target,Hyps,T2,Hyps1), nonmember(T2,History), | |
| 396 | check_equal_h(A,T2,TGr,[A|History],Hyps1,Hyps2). | |
| 397 | check_equal_h(A,Target,ground,_,Hyps,Hyps) :- | |
| 398 | avl_fetch_from_hyps(subset(A,Target),Hyps), | |
| 399 | avl_fetch_from_hyps(subset(Target,A),Hyps). | |
| 400 | check_equal_h(A,Empty,ground,_,Hyps,Hyps) :- is_empty_set_direct(Empty), !, check_empty_set(A,Hyps,_). | |
| 401 | check_equal_h(Empty,A,ground,_,Hyps,Hyps) :- is_empty_set_direct(Empty), !, check_empty_set(A,Hyps,_). | |
| 402 | check_equal_h(interval(Min,Max),Val,ground,History,Hyps1,Hyps3) :- !, | |
| 403 | check_equal_h_interval(Val,Min,Max,History,Hyps1,Hyps3). | |
| 404 | check_equal_h(Val,interval(Min,Max),ground,History,Hyps1,Hyps3) :- | |
| 405 | check_equal_h_interval(Val,Min,Max,History,Hyps1,Hyps3). | |
| 406 | %check_equal_h(A,Target,_,_,Hyps,Hyps1) :- write(check_eq_failed(A,Target)),nl,fail. | |
| 407 | ||
| 408 | check_equal_h_interval(Val,Min,Max,History,Hyps1,Hyps3) :- | |
| 409 | is_interval(Val,Hyps1,Min2,Max2),!, | |
| 410 | check_equal_h(Min,Min2,ground,History,Hyps1,Hyps2),!, | |
| 411 | check_equal_h(Max,Max2,ground,History,Hyps2,Hyps3). | |
| 412 | % case when Min>Max and Val is empty set is covered elsewhere !? see test 2560 | |
| 413 | ||
| 414 | commutative_bin_op(add(X,Y),add,X,Y). | |
| 415 | commutative_bin_op(intersection(X,Y),intersection,X,Y). | |
| 416 | commutative_bin_op(multiplication(X,Y),multiplication,X,Y). | |
| 417 | commutative_bin_op(union(X,Y),union,X,Y). | |
| 418 | ||
| 419 | non_commutative_bin_op(cartesian_product(X,Y),cartesian_product,X,Y). % TODO: better rule | |
| 420 | non_commutative_bin_op(concat(X,Y),concat,X,Y). | |
| 421 | non_commutative_bin_op(couple(X,Y),couple,X,Y). | |
| 422 | non_commutative_bin_op(direct_product(X,Y),direct_product,X,Y). | |
| 423 | non_commutative_bin_op(domain_restriction(X,Y),domain_restriction,X,Y). | |
| 424 | non_commutative_bin_op(domain_subtraction(X,Y),domain_subtraction,X,Y). | |
| 425 | non_commutative_bin_op(div(X,Y),div,X,Y). | |
| 426 | non_commutative_bin_op(image(X,Y),image,X,Y). | |
| 427 | non_commutative_bin_op(interval(X,Y),interval,X,Y). % TODO: better rule, see check_not_equal_interval | |
| 428 | non_commutative_bin_op(iteration(X,Y),iteration,X,Y). | |
| 429 | non_commutative_bin_op(minus(X,Y),minus,X,Y). | |
| 430 | non_commutative_bin_op(modulo(X,Y),modulo,X,Y). | |
| 431 | non_commutative_bin_op(parallel_product(X,Y),parallel_product,X,Y). | |
| 432 | non_commutative_bin_op(power_of(X,Y),power_of,X,Y). | |
| 433 | non_commutative_bin_op(range_restriction(X,Y),range_restriction,X,Y). | |
| 434 | non_commutative_bin_op(range_subtraction(X,Y),range_subtraction,X,Y). | |
| 435 | non_commutative_bin_op(restrict_front(X,Y),restrict_front,X,Y). | |
| 436 | non_commutative_bin_op(restrict_tail(X,Y),restrict_tail,X,Y). | |
| 437 | non_commutative_bin_op(set_subtraction(X,Y),set_subtraction,X,Y). | |
| 438 | ||
| 439 | unary_op(closure(X),closure,X). | |
| 440 | unary_op(card(X),card,X). | |
| 441 | unary_op(domain(X),domain,X). | |
| 442 | unary_op(identity(X),identity,X). | |
| 443 | unary_op(fin_subset(X),fin_subset,X). | |
| 444 | unary_op(fin1_subset(X),fin1_subset,X). | |
| 445 | unary_op(first(X),first,X). | |
| 446 | unary_op(first_of_pair(X),first_of_pair,X). | |
| 447 | unary_op(front(X),front,X). | |
| 448 | unary_op(iseq(X),iseq,X). | |
| 449 | unary_op(iseq1(X),iseq1,X). | |
| 450 | unary_op(last(X),last,X). | |
| 451 | unary_op(max(X),max,X). | |
| 452 | unary_op(min(X),min,X). | |
| 453 | unary_op(perm(X),perm,X). | |
| 454 | unary_op(pow_subset(X),pow_subset,X). | |
| 455 | unary_op(pow1_subset(X),pow1_subset,X). | |
| 456 | unary_op(range(X),range,X). | |
| 457 | unary_op(reflexive_closure(X),reflexive_closure,X). | |
| 458 | unary_op(rev(X),rev,X). | |
| 459 | unary_op(reverse(X),reverse,X). | |
| 460 | unary_op(second_of_pair(X),second_of_pair,X). | |
| 461 | unary_op(seq(X),seq,X). | |
| 462 | unary_op(seq1(X),seq1,X). | |
| 463 | unary_op(size(X),size,X). | |
| 464 | unary_op(tail(X),tail,X). | |
| 465 | unary_op(unary_minus(X),unary_minus,X). | |
| 466 | ||
| 467 | ||
| 468 | infer_sequence_type_of_expr(sequence_extension([_|_]),_,seq1). | |
| 469 | infer_sequence_type_of_expr(sorted_set_extension(SList),_,seq1) :- | |
| 470 | sorted_set_extension_is_seq(SList,1). | |
| 471 | infer_sequence_type_of_expr(set_extension(List),_,seq1) :- sort(List,SList), | |
| 472 | sorted_set_extension_is_seq(SList,1). | |
| 473 | infer_sequence_type_of_expr(insert_tail(_,_),_,seq1). | |
| 474 | % we do not need to check Seq is a sequence; this will be checked in its own PO, ditto for operators below | |
| 475 | infer_sequence_type_of_expr(insert_front(_,_),_,seq1). | |
| 476 | infer_sequence_type_of_expr(concat(A,B),Hyps,R) :- | |
| 477 | ( infer_sequence_type_of_expr(A,Hyps,seq1) -> R=seq1 | |
| 478 | ; infer_sequence_type_of_expr(B,Hyps,seq1) -> R=seq1 | |
| 479 | ; R=seq). | |
| 480 | infer_sequence_type_of_expr(restrict_front(_,_),_,seq). | |
| 481 | infer_sequence_type_of_expr(restrict_tail(_,_),_,seq). | |
| 482 | infer_sequence_type_of_expr(rev(A),Hyps,R) :- | |
| 483 | (infer_sequence_type_of_expr(A,Hyps,seq1) -> R=seq1 ; R=seq). | |
| 484 | infer_sequence_type_of_expr(front(_),_,seq). % we could call check_not_empty_set(front(A),Hyps) | |
| 485 | infer_sequence_type_of_expr(tail(_),_,seq). % ditto | |
| 486 | infer_sequence_type_of_expr(general_concat(_),_,seq). | |
| 487 | infer_sequence_type_of_expr(value(avl_set(SeqAVL)),_,seq1) :- !, SeqAVL \= empty, | |
| 488 | safe_is_avl_sequence(SeqAVL). | |
| 489 | infer_sequence_type_of_expr(if_then_else(Pred,A,B),Hyps,Type) :- !, | |
| 490 | push_and_rename_normalized_hyp(Pred,Hyps,Hyps1), | |
| 491 | (hyps_inconsistent(Hyps1) | |
| 492 | -> push_and_rename_normalized_hyp(negation(Pred),Hyps,Hyps2), | |
| 493 | infer_sequence_type_of_expr(B,Hyps2,Type) | |
| 494 | ; infer_sequence_type_of_expr(A,Hyps1,S1), | |
| 495 | push_and_rename_normalized_hyp(negation(Pred),Hyps,Hyps2), | |
| 496 | (hyps_inconsistent(Hyps2) -> Type=S1 | |
| 497 | ; infer_sequence_type_of_expr(B,Hyps2,S2), lub_seq(S1,S2,Type)) | |
| 498 | ). | |
| 499 | infer_sequence_type_of_expr(external_function_call(Name,Args),Hyps,R) :- | |
| 500 | external_function_returns_sequence_type(Name,Args,Hyps,R,_). | |
| 501 | infer_sequence_type_of_expr(S,_,seq) :- is_empty_set_direct(S). | |
| 502 | infer_sequence_type_of_expr(Expr,Hyps,R) :- | |
| 503 | is_lambda_function_with_domain(Expr,Domain), | |
| 504 | Domain = interval(1,N), | |
| 505 | (check_leq(1,N,Hyps) -> R = seq1 ; R=seq). | |
| 506 | % TO DO: rule for composition | |
| 507 | ||
| 508 | lub_seq(seq1,seq1,seq1). | |
| 509 | lub_seq(seq1,seq,seq). | |
| 510 | lub_seq(seq,seq1,seq). | |
| 511 | lub_seq(seq,seq,seq). | |
| 512 | ||
| 513 | external_function_possible_vals('CHOOSE',[Set],Set). | |
| 514 | external_function_possible_vals('MU',[Set],Set). | |
| 515 | external_function_possible_vals('ABS',_,'NATURAL'). | |
| 516 | external_function_possible_vals('LCM',_,'NATURAL'). | |
| 517 | external_function_possible_vals('GCD',_,'NATURAL1'). | |
| 518 | external_function_possible_vals('SIGN',_,interval(-1,1)). | |
| 519 | ||
| 520 | external_function_returns_sequence_type('STRING_CHARS',[Arg],Hyps,Type,FullType) :- !, | |
| 521 | (check_not_equal(Arg,string(''),Hyps) -> Type=seq1, FullType=seq1(string) ; Type=seq, FullType=seq(string)). | |
| 522 | external_function_returns_sequence_type('STRING_CODES',[Arg],Hyps,Type,FullType) :- !, | |
| 523 | (check_not_equal(Arg,string(''),Hyps) -> Type=seq1, FullType=seq1(integer) ; Type=seq, FullType=seq(integer)). | |
| 524 | external_function_returns_sequence_type(Name,_Args,_Hyps,Type,FullType) :- | |
| 525 | external_function_returns_sequence_type(Name,Type,FullType). | |
| 526 | ||
| 527 | :- use_module(probsrc(external_functions), [external_fun_type/3, performs_io/1]). | |
| 528 | % external functions which return sequences | |
| 529 | external_function_returns_sequence_type('STRING_SPLIT',Type,FullType) :- !, Type=seq1, FullType=seq1(string). | |
| 530 | external_function_returns_sequence_type(Name,seq,seq(Type)) :- external_fun_type(Name,_,List), | |
| 531 | last(List,ReturnType), nonvar(ReturnType), ReturnType=seq(RType), | |
| 532 | (ground(RType) -> Type = ReturnType ; Type=typeset). % 'REGEX_SEARCH_ALL', 'REGEX_ISEARCH_ALL', ... | |
| 533 | % TODO: use hyps, e.g., for STRING_CHARS(X) we have type seq1 if X/="" | |
| 534 | ||
| 535 | % check if a sorted set extension represent a proper sequence | |
| 536 | sorted_set_extension_is_seq([],_). | |
| 537 | sorted_set_extension_is_seq([couple(Nr,_)|T],Nr) :- N1 is Nr+1, sorted_set_extension_is_seq(T,N1). | |
| 538 | ||
| 539 | % -------- | |
| 540 | % DOMAIN | |
| 541 | ||
| 542 | % compute exact domain | |
| 543 | % currently there can be multiple solutions for $(_) case below; first one is usually more precise | |
| 544 | %compute_exact_domain(Value,Hyps2,Res) :- debug:print_quoted_with_max_depth(compute_exact_domain(Value,Hyps2,Res),4),nl,fail. | |
| 545 | ||
| 546 | ||
| 547 | compute_exact_domain(assertion_expression(_,_,Func),Hyps,Res,Hyps2) :- !, | |
| 548 | compute_exact_domain(Func,Hyps,Res,Hyps2). | |
| 549 | compute_exact_domain(closure(Func),Hyps,Res,Hyps2) :- !, % this is closure1, dom(closure1(R)) = dom(R) | |
| 550 | compute_exact_domain(Func,Hyps,Res,Hyps2). | |
| 551 | compute_exact_domain(reverse(Func),Hyps,Res,Hyps2) :- !, | |
| 552 | compute_exact_range(Func,Hyps,Res,Hyps2). | |
| 553 | compute_exact_domain(rev(Func),Hyps,Res,Hyps2) :- !, % reverse of a sequence; domain identical | |
| 554 | compute_exact_domain(Func,Hyps,Res,Hyps2). | |
| 555 | compute_exact_domain(identity(Domain),Hyps,Res,Hyps2) :- !, Hyps2=Hyps, Res=Domain. | |
| 556 | compute_exact_domain(cartesian_product(A,B),Hyps,Res,Hyps) :- | |
| 557 | check_not_empty_set(B,Hyps), !, Res = A. % B/= {} => dom(A * B) = A | |
| 558 | %compute_exact_domain(restrict_front(_Seq,N),Hyps,Res,Hyps2) :- !, | |
| 559 | % % WD Condition requires N : 0..size(Seq); | |
| 560 | % w/o it we loose the info that 1..N is a subset of dom(Seq); hence we comment this out, see test 2471 | |
| 561 | % Hyps2=Hyps, Res = interval(1,N). % TODO: similar rule for restrict_tail | |
| 562 | compute_exact_domain(Func,Hyps,Res,Hyps2) :- | |
| 563 | compute_exact_domain_direct(Func,Hyps,Res,Hyps2),!. % No recursive application of equal or hyp | |
| 564 | compute_exact_domain(Func,Hyps,Domain,Hyps2) :- | |
| 565 | avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1), | |
| 566 | compute_exact_domain(Func2,Hyps1,Domain,Hyps2). | |
| 567 | %compute_exact_domain(Expr,_,Domain,_) :- print(compute_exact_domain_failed(Expr,_,Domain)),nl,fail. | |
| 568 | ||
| 569 | ||
| 570 | compute_exact_domain_direct(Func,Hyps,Res,Hyps2) :- | |
| 571 | avl_fetch_mem_or_struct(Func,Hyps,Function,Hyps1), % look for Func : Res --> Range ; e.g. Func:perm(1..10) -> DomSet=1..10 | |
| 572 | % f : _ +-> ( Dom --> _ ) & x:Dom ==> x:dom(f(_)) | |
| 573 | % f : _ +-> ( Dom --> _ ) => dom(f(_)) = Dom | |
| 574 | get_exact_domain_of_func_or_rel_type(Function,Hyps1,Res,Hyps2),!. % is thus also minimal domain | |
| 575 | compute_exact_domain_direct(Func,Hyps,Res,Hyps3) :- Func = '$'(_), % Look for Func = Value definition | |
| 576 | avl_fetch_equal_from_hyps(Func,Hyps,Value,Hyps2), | |
| 577 | compute_exact_domain(Value,Hyps2,Res,Hyps3). | |
| 578 | compute_exact_domain_direct(value(CS),Hyps,value(Res),Hyps) :- value_can_be_computed(CS),!, | |
| 579 | domain_of_explicit_set_wf(CS,Res,no_wf_available). | |
| 580 | compute_exact_domain_direct(overwrite(F1,F2),Hyps,D12,Hyps2) :- !, % dom(F1 <+ F2) = dom(F1) \/ dom(F2) | |
| 581 | compute_exact_domain(F1,Hyps,D1,Hyps1), compute_exact_domain(F2,Hyps1,D2,Hyps2), | |
| 582 | construct_union(D1,D2,Hyps2,D12). | |
| 583 | compute_exact_domain_direct(domain_restriction(S,F),Hyps,intersection(S,D),Hyps2) :- !, % dom(S <| F) = S /\ dom(F) | |
| 584 | compute_exact_domain(F,Hyps,D,Hyps2). % SIMP_MULTI_DOM_DOMRES | |
| 585 | compute_exact_domain_direct(domain_subtraction(S,F),Hyps,set_subtraction(D,S),Hyps2) :- !, % dom(S <<| F) = dom(F) - S | |
| 586 | compute_exact_domain(F,Hyps,D,Hyps2). % SIMP_MULTI_DOM_DOMSUB | |
| 587 | compute_exact_domain_direct(direct_product(F,G),Hyps,intersection(DF,DG),Hyps2) :- !, % dom(F><G) = dom(F) /\ dom(G) | |
| 588 | compute_exact_domain(F,Hyps,DF,Hyps1), | |
| 589 | compute_exact_domain(G,Hyps1,DG,Hyps2). | |
| 590 | compute_exact_domain_direct(composition(F1,F2),Hyps,Domain,Hyps4) :- !, % dom((F1;F2)) = dom(F1) if ran(F1) <: dom(F2) | |
| 591 | compute_exact_domain(F1,Hyps,Domain,Hyps2), | |
| 592 | compute_exact_domain(F2,Hyps2,D2,Hyps3), % or_subset would also be ok | |
| 593 | (maximal_set(D2,Hyps3) -> Hyps4=Hyps3 | |
| 594 | ; get_range_or_superset(F1,Hyps3,R1,Hyps4), | |
| 595 | check_is_subset(R1,D2,Hyps4,_PT) | |
| 596 | ). | |
| 597 | compute_exact_domain_direct(union(F,G),Hyps,UnionDFDG,Hyps2) :- !, % dom(F \/ G) = dom(F) \/ dom(G) | |
| 598 | compute_exact_domain(F,Hyps,DF,Hyps1), | |
| 599 | compute_exact_domain(G,Hyps1,DG,Hyps2), | |
| 600 | construct_union(DF,DG,Hyps2,UnionDFDG). | |
| 601 | compute_exact_domain_direct(sorted_set_extension(List),Hyps,Res,Hyps2) :- !, | |
| 602 | compute_exact_domain_direct(set_extension(List),Hyps,Res,Hyps2). | |
| 603 | compute_exact_domain_direct(set_extension(List),Hyps,Res,Hyps) :- !, maplist(get_dom_el,List,Domain), | |
| 604 | construct_set_extension(Domain,Hyps,Res). | |
| 605 | compute_exact_domain_direct(Expr,Hyps,Domain,Hyps) :- is_lambda_function_with_domain(Expr,Domain),!. | |
| 606 | compute_exact_domain_direct(Func,Hyps,Domain,Hyps2) :- | |
| 607 | avl_fetch_equal_from_hyps(domain(Func),Hyps,Domain,Hyps2). | |
| 608 | ||
| 609 | value_can_be_computed(CS) :- nonvar(CS), | |
| 610 | CS \= closure(_,_,_). % norm_value normalises Body of closures; leading to errors | |
| 611 | % Note: this does not check if we have a couple/record/set with closures inside | |
| 612 | ||
| 613 | % get domain element of a couple | |
| 614 | get_dom_el(couple(A,_),A). | |
| 615 | % get range element of a couple | |
| 616 | get_ran_el(couple(_,B),B). | |
| 617 | ||
| 618 | % construct union term with a few optimisations | |
| 619 | construct_union(empty_set,B,_Hyps,Res) :- !,Res=B. | |
| 620 | construct_union(set_extension(A),set_extension(B),Hyps,Res) :- !, | |
| 621 | append(A,B,AB), | |
| 622 | construct_set_extension(AB,Hyps,Res). | |
| 623 | construct_union(A,empty_set,_,Res) :- !,Res=A. | |
| 624 | construct_union(A,B,_,union(A,B)). | |
| 625 | ||
| 626 | % get maximal domain of a function (i.e., domain or superset thereof) | |
| 627 | :- if(environ(prob_safe_mode,true)). | |
| 628 | get_domain_or_superset(F,H,R,H2) :- nonvar(H2), | |
| 629 | add_internal_error('Instantiated hyps:',get_domain_or_superset(F,H,R,H2)),fail. | |
| 630 | :- endif. | |
| 631 | get_domain_or_superset(reverse(Func),Hyps,Res,Hyps2) :- !, | |
| 632 | get_range_or_superset(Func,Hyps,Res,Hyps2). | |
| 633 | get_domain_or_superset(domain(F),Hyps,Res,Hyps2) :- | |
| 634 | get_domain_or_superset(F,Hyps,DomF,Hyps1), | |
| 635 | get_domain_or_superset(DomF,Hyps1,Res,Hyps2). | |
| 636 | get_domain_or_superset(range(F),Hyps,Res,Hyps2) :- | |
| 637 | get_range_or_superset(F,Hyps,RanF,Hyps1), | |
| 638 | get_domain_or_superset(RanF,Hyps1,Res,Hyps2). | |
| 639 | get_domain_or_superset(CompSet,Hyps,comprehension_set(NewIds,Pred2),Hyps) :- | |
| 640 | is_comprehension_set(CompSet,Ids,Pred), | |
| 641 | append(NewIds,['$'(LastID)],Ids), % we project away last identifier | |
| 642 | NewIds \= [], % otherwise first and unique id is a pair | |
| 643 | conj_to_list(Pred,Preds,[]), | |
| 644 | exclude(uses_id(LastID),Preds,Preds2), % filter out all conjuncts using removed variable | |
| 645 | Preds2 \= [], % otherwise we simply have truth as body | |
| 646 | list_to_conj(Preds2,Pred2). | |
| 647 | get_domain_or_superset(Func,Hyps,Res,Hyps3) :- % sometimes rewrites terms to variables | |
| 648 | compute_exact_domain_direct(Func,Hyps,Res,Hyps2), | |
| 649 | rewrite_local_loop_check(Func,get_domain_or_superset,Res,Hyps2,Hyps3), | |
| 650 | !. | |
| 651 | get_domain_or_superset(domain_restriction(A,_),Hyps,Res,Hyps) :- Res=A. % in case compute_exact_domain_direct fails | |
| 652 | get_domain_or_superset(Func,Hyps,Res,Hyps1) :- | |
| 653 | function_restriction(Func,LargerFunc), | |
| 654 | get_domain_or_superset(LargerFunc,Hyps,Res,Hyps1). | |
| 655 | get_domain_or_superset(composition(F1,_),Hyps,Res,Hyps1) :- get_domain_or_superset(F1,Hyps,Res,Hyps1). | |
| 656 | get_domain_or_superset(cartesian_product(A,_),Hyps,Res,Hyps) :- !, Res=A. % dom(A*B) <: A | |
| 657 | get_domain_or_superset(direct_product(A,B),Hyps,Res,Hyps2) :- % dom(A >< B) = dom(A) /\ dom (B) | |
| 658 | (get_domain_or_superset(A,Hyps,Res,Hyps2) -> true | |
| 659 | ; get_domain_or_superset(B,Hyps,Res,Hyps2) -> true). | |
| 660 | get_domain_or_superset(tail(Seq),Hyps,Res,Hyps2) :- !, % dom(tail(S)) <: dom(S) | |
| 661 | get_domain_or_superset(Seq,Hyps,Res,Hyps2). | |
| 662 | get_domain_or_superset(front(Seq),Hyps,Res,Hyps2) :- !, % dom(front(S)) <: dom(S) | |
| 663 | get_domain_or_superset(Seq,Hyps,Res,Hyps2). | |
| 664 | get_domain_or_superset(restrict_front(Seq,K),Hyps,Res,Hyps2) :- !, % dom(S /|\ k) <: dom(S) | |
| 665 | (get_domain_or_superset(Seq,Hyps,Res,Hyps2) | |
| 666 | ; Res = interval(1,K), Hyps2=Hyps % WD Condition requires K : 0..size(Seq) | |
| 667 | ). | |
| 668 | get_domain_or_superset(restrict_tail(Seq,_),Hyps,Res,Hyps2) :- !, % dom(S \|/ k) <: dom(S) | |
| 669 | get_domain_or_superset(Seq,Hyps,Res,Hyps2). | |
| 670 | get_domain_or_superset(Func,Hyps,DomSet,Hyps2) :- simple_value(Func), | |
| 671 | avl_fetch_mem_or_struct(Func,Hyps,FunctionType,Hyps1), | |
| 672 | get_domain_or_superset_of_func_or_rel_type(FunctionType,Hyps1,DomSet,Hyps2), | |
| 673 | \+ maximal_set(DomSet,Hyps2). % inference useless | |
| 674 | get_domain_or_superset(Func,Hyps,Domain,Hyps2) :- | |
| 675 | avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1), | |
| 676 | get_domain_or_superset(Func2,Hyps1,Domain,Hyps2). | |
| 677 | get_domain_or_superset(Func,Hyps,DomSuperSet,Hyps2) :- | |
| 678 | avl_fetch_binop_from_hyps(domain(Func),subset,Hyps,DomSuperSet,Hyps2). | |
| 679 | ||
| 680 | uses_id(ID,Expr) :- occurs(Expr,ID). | |
| 681 | ||
| 682 | % get exact (thus also minimal) domain of a function type | |
| 683 | :- if(environ(prob_safe_mode,true)). | |
| 684 | get_exact_domain_of_func_or_rel_type(F,H,R,H2) :- | |
| 685 | nonvar(H2), add_internal_error('Instantiated hyps:',get_exact_domain_of_func_or_rel_type(F,H,R,H2)),fail. | |
| 686 | :- endif. | |
| 687 | get_exact_domain_of_func_or_rel_type(FunType,Hyps,A,Hyps) :- | |
| 688 | get_possible_domain_of_func_or_rel_type(FunType,Hyps,A,exact),!. | |
| 689 | get_exact_domain_of_func_or_rel_type(FunType,Hyps,Domain,Hyps2) :- | |
| 690 | avl_fetch_worthwhile_equal_from_hyps(FunType,Hyps,FunType2,Hyps1), % in case we have a definition like X = 1..n --> R | |
| 691 | get_exact_domain_of_func_or_rel_type(FunType2,Hyps1,Domain,Hyps2). | |
| 692 | get_exact_domain_of_func_or_rel_type(sorted_set_extension(F),Hyps,Domain,Hyps2) :- !, | |
| 693 | get_exact_domain_of_func_or_rel_type(set_extension(F),Hyps,Domain,Hyps2). | |
| 694 | get_exact_domain_of_func_or_rel_type(set_extension([Func|TF]),Hyps,Domain,Hyps2) :- | |
| 695 | compute_exact_domain(Func,Hyps,Domain,Hyps2), % now check that all other functions have the same domain | |
| 696 | (member(Func2,TF), \+ compute_exact_domain(Func2,Hyps2,Domain,_) -> fail | |
| 697 | ; true). | |
| 698 | ||
| 699 | get_possible_domain_of_func_or_rel_type(iseq(_),_,'NATURAL1',subset). | |
| 700 | get_possible_domain_of_func_or_rel_type(iseq1(_),_,'NATURAL1',subset). | |
| 701 | get_possible_domain_of_func_or_rel_type(partial_bijection(A,_),_,A,subset). | |
| 702 | get_possible_domain_of_func_or_rel_type(partial_function(A,_),_,A,subset). | |
| 703 | get_possible_domain_of_func_or_rel_type(partial_injection(A,_),_,A,subset). | |
| 704 | get_possible_domain_of_func_or_rel_type(partial_surjection(A,_),_,A,subset). | |
| 705 | get_possible_domain_of_func_or_rel_type(perm(A),Hyps,Domain,Type) :- | |
| 706 | (compute_card_of_set(A,Hyps,CardA,_) % we could do check_finite and use card(A) instead of CardA | |
| 707 | -> Domain = interval(1,CardA), Type=exact | |
| 708 | ; check_finite(A,Hyps,_) -> Domain = interval(1,card(A)), Type=exact | |
| 709 | ; %print(could_not_compute_card_for_perm(A)),nl, | |
| 710 | Domain = 'NATURAL1', Type=subset | |
| 711 | ). | |
| 712 | get_possible_domain_of_func_or_rel_type(relations(A,_),_,A,subset). | |
| 713 | get_possible_domain_of_func_or_rel_type(pow_subset(cartesian_product(A,_)),_,A,subset). | |
| 714 | get_possible_domain_of_func_or_rel_type(pow1_subset(cartesian_product(A,_)),_,A,subset). | |
| 715 | get_possible_domain_of_func_or_rel_type(fin_subset(cartesian_product(A,_)),_,A,subset). | |
| 716 | get_possible_domain_of_func_or_rel_type(fin1_subset(cartesian_product(A,_)),_,A,subset). | |
| 717 | get_possible_domain_of_func_or_rel_type(seq(_),_,'NATURAL1',subset). | |
| 718 | get_possible_domain_of_func_or_rel_type(seq1(_),_,'NATURAL1',subset). | |
| 719 | get_possible_domain_of_func_or_rel_type(surjection_relation(A,_),_,A,subset). | |
| 720 | get_possible_domain_of_func_or_rel_type(total_bijection(A,_),_,A,exact). | |
| 721 | get_possible_domain_of_func_or_rel_type(total_function(A,_),_,A,exact). | |
| 722 | get_possible_domain_of_func_or_rel_type(total_injection(A,_),_,A,exact). | |
| 723 | get_possible_domain_of_func_or_rel_type(total_relation(A,_),_,A,exact). | |
| 724 | get_possible_domain_of_func_or_rel_type(total_surjection_relation(A,_),_,A,exact). | |
| 725 | get_possible_domain_of_func_or_rel_type(total_surjection(A,_),_,A,exact). | |
| 726 | ||
| 727 | ||
| 728 | % variation of get_possible_domain_of_func_or_rel_type, which uses Hyps and can deal with set_extensions | |
| 729 | :- if(environ(prob_safe_mode,true)). | |
| 730 | get_domain_or_superset_of_func_or_rel_type(F,H,R,H2) :- nonvar(H2), | |
| 731 | add_internal_error('Instantiated hyps:',get_domain_or_superset_of_func_or_rel_type(F,H,R,H2)),fail. | |
| 732 | :- endif. | |
| 733 | get_domain_or_superset_of_func_or_rel_type(sorted_set_extension(List),Hyps,Dom,Hyps2) :- !, | |
| 734 | get_domain_or_superset_of_func_or_rel_type(set_extension(List),Hyps,Dom,Hyps2). | |
| 735 | get_domain_or_superset_of_func_or_rel_type(set_extension(List),Hyps,Dom,Hyps2) :- !, | |
| 736 | % if we have f: {f1,f2,...} => dom(f) <: dom(f1) \/ dom(f2) \/ ... | |
| 737 | merge_possible_domains_of_list(List,Hyps,empty_set,Dom,Hyps2). | |
| 738 | get_domain_or_superset_of_func_or_rel_type(Func,Hyps,Res,Hyps) :- | |
| 739 | get_possible_domain_of_func_or_rel_type(Func,Hyps,D,_),!,Res=D. | |
| 740 | ||
| 741 | % merge domains of a list of possible functions | |
| 742 | merge_possible_domains_of_list([],Hyps,Acc,Acc,Hyps). | |
| 743 | merge_possible_domains_of_list([H|T],Hyps,Acc,Res,Hyps2) :- | |
| 744 | get_domain_or_superset(H,Hyps,Domain,Hyps1),!, | |
| 745 | construct_union(Acc,Domain,Hyps1,Acc1), | |
| 746 | merge_possible_domains_of_list(T,Hyps1,Acc1,Res,Hyps2). | |
| 747 | ||
| 748 | % RANGE | |
| 749 | % ----- | |
| 750 | ||
| 751 | % compute range or subset thereof | |
| 752 | ||
| 753 | compute_exact_range(assertion_expression(_,_,Func),Hyps,Res,Hyps2) :- !, | |
| 754 | compute_exact_range(Func,Hyps,Res,Hyps2). | |
| 755 | compute_exact_range(closure(Func),Hyps,Res,Hyps2) :- !, % this is closure1, range(closure1(R)) = ran(R) | |
| 756 | compute_exact_range(Func,Hyps,Res,Hyps2). | |
| 757 | compute_exact_range(reverse(Func),Hyps,Res,Hyps2) :- | |
| 758 | compute_exact_domain(Func,Hyps,Res,Hyps2). | |
| 759 | compute_exact_range(rev(Func),Hyps,Res,Hyps2) :- % reverse of a sequence: same range | |
| 760 | compute_exact_range(Func,Hyps,Res,Hyps2). | |
| 761 | compute_exact_range(identity(Domain),Hyps,Res,Hyps2) :- !, Hyps2=Hyps, Res=Domain. | |
| 762 | compute_exact_range(Func,Hyps,Res,Hyps2) :- | |
| 763 | compute_exact_range_direct(Func,Hyps,Res,Hyps2),!. % No recursive application of equal or hyp | |
| 764 | compute_exact_range(Func,Hyps,Res,Hyps2) :- Func = '$'(_), | |
| 765 | avl_fetch_mem_or_struct(Func,Hyps,FunctionType,Hyps2), % Func : _ --> Res | |
| 766 | get_exact_range_of_func_type_direct(FunctionType,Res). | |
| 767 | compute_exact_range(Func,Hyps,Range,Hyps2) :- | |
| 768 | avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1), | |
| 769 | compute_exact_range(Func2,Hyps1,Range,Hyps2). | |
| 770 | %compute_exact_range(Expr,H,Domain) :- nl,portray_hyps(H),nl,print(compute_range_failed(Expr,_,Domain)),nl,fail. | |
| 771 | % TO DO: rule for composition (exact case) | |
| 772 | ||
| 773 | ||
| 774 | compute_exact_range_direct(S,Hyps,empty_set,Hyps) :- is_empty_set_direct(S),!. | |
| 775 | compute_exact_range_direct(function(Func2,_),Hyps,Res,Hyps2) :- | |
| 776 | % f : _ +-> ( _ --> Ran ) & x:Ran ==> x:ran(f(_)) | |
| 777 | % f : _ +-> ( _ -->> Ran ) => ran(f(_)) = Ran | |
| 778 | get_range_or_superset(Func2,Hyps,Range,Hyps2), | |
| 779 | get_exact_range_of_func_type_direct(Range,Res). % is thus also minimal domain | |
| 780 | compute_exact_range_direct(value(CS),Hyps,value(Res),Hyps) :- !, | |
| 781 | value_can_be_computed(CS), % TO DO: maybe only if small enough | |
| 782 | range_of_explicit_set_wf(CS,Res,no_wf_available). | |
| 783 | compute_exact_range_direct(sequence_extension(L),Hyps,Res,Hyps) :- !, | |
| 784 | construct_set_extension(L,Hyps,Res). | |
| 785 | compute_exact_range_direct(union(F,G),Hyps,UnionRFRG,Hyps2) :- !, % ran(F \/ G) = ran(F) \/ ran(G) | |
| 786 | compute_exact_range(F,Hyps,RF,Hyps1), | |
| 787 | compute_exact_range(G,Hyps1,RG,Hyps2), | |
| 788 | construct_union(RF,RG,Hyps2,UnionRFRG). | |
| 789 | compute_exact_range_direct(cartesian_product(A,B),Hyps,Res,Hyps) :- | |
| 790 | check_not_empty_set(A,Hyps),!, Res=B. % A/={} => ran(A * B) = B | |
| 791 | compute_exact_range_direct(sorted_set_extension(List),Hyps,Res,Hyps2) :- !, | |
| 792 | compute_exact_range_direct(set_extension(List),Hyps,Res,Hyps2). | |
| 793 | compute_exact_range_direct(set_extension(List),Hyps,Res,Hyps) :- !, maplist(get_ran_el,List,Domain), | |
| 794 | construct_set_extension(Domain,Hyps,Res). | |
| 795 | compute_exact_range_direct(Func,Hyps,Range,Hyps2) :- | |
| 796 | avl_fetch_equal_from_hyps(range(Func),Hyps,Range,Hyps2). | |
| 797 | ||
| 798 | % get maximal range of a function (i.e., range or superset thereof) | |
| 799 | :- if(environ(prob_safe_mode,true)). | |
| 800 | get_range_or_superset(P,H,R,H1) :- nonvar(H1), add_internal_error('Illegal hyps:',get_range_or_superset(P,H,R,H1)),fail. | |
| 801 | :- endif. | |
| 802 | get_range_or_superset(reverse(Func),Hyps,Res,Hyps2) :- !, | |
| 803 | get_domain_or_superset(Func,Hyps,Res,Hyps2). | |
| 804 | get_range_or_superset(domain(F),Hyps,Res,Hyps2) :- | |
| 805 | get_domain_or_superset(F,Hyps,DomF,Hyps1), | |
| 806 | get_range_or_superset(DomF,Hyps1,Res,Hyps2). | |
| 807 | get_range_or_superset(range(F),Hyps,Res,Hyps2) :- | |
| 808 | get_range_or_superset(F,Hyps,RanF,Hyps1), | |
| 809 | get_range_or_superset(RanF,Hyps1,Res,Hyps2). | |
| 810 | get_range_or_superset(Func,Hyps,Res,Hyps3) :- | |
| 811 | compute_exact_range_direct(Func,Hyps,Res,Hyps2), | |
| 812 | rewrite_local_loop_check(Func,get_range_or_superset,Res,Hyps2,Hyps3), | |
| 813 | !. % can be a loop dom(f) = ran(g) | |
| 814 | get_range_or_superset(function(Func2,_),Hyps,Res,Hyps2) :- | |
| 815 | % f2 : _ +-> ( _ --> Res ) ==> ran(f2(.)) <: Res | |
| 816 | get_range_or_superset(Func2,Hyps,Range,Hyps1), | |
| 817 | get_possible_range_of_func_or_rel_type(Range,Hyps1,Res,_,Hyps2). | |
| 818 | % TODO: try rewrite_function_application(Func,Args,Hyps,Result,Hyps2) ? | |
| 819 | get_range_or_superset(range_restriction(_,B),Hyps,Res,Hyps) :- Res=B. % in case compute_exact_range_direct fails | |
| 820 | get_range_or_superset(Func,Hyps,Res,Hyps1) :- | |
| 821 | function_restriction(Func,LargerFunc), | |
| 822 | get_range_or_superset(LargerFunc,Hyps,Res,Hyps1). | |
| 823 | get_range_or_superset(Func,Hyps,RangeSet,Hyps2) :- simple_value(Func), | |
| 824 | avl_fetch_mem_or_struct(Func,Hyps,FunctionType,Hyps1), | |
| 825 | get_possible_range_of_func_or_rel_type(FunctionType,Hyps1,RangeSet,_,Hyps2), | |
| 826 | \+ maximal_set(RangeSet,Hyps2). % inference useless. | |
| 827 | get_range_or_superset(tail(Seq),Hyps,Res,Hyps2) :- !, % ran(tail(S)) <: ran(S) | |
| 828 | get_range_or_superset(Seq,Hyps,Res,Hyps2). | |
| 829 | get_range_or_superset(front(Seq),Hyps,Res,Hyps2) :- !, % ran(front(S)) <: ran(S) | |
| 830 | get_range_or_superset(Seq,Hyps,Res,Hyps2). | |
| 831 | get_range_or_superset(restrict_front(Seq,_),Hyps,Res,Hyps2) :- !, % /|\ | |
| 832 | get_range_or_superset(Seq,Hyps,Res,Hyps2). | |
| 833 | get_range_or_superset(restrict_tail(Seq,_),Hyps,Res,Hyps2) :- !, | |
| 834 | get_range_or_superset(Seq,Hyps,Res,Hyps2). | |
| 835 | get_range_or_superset(concat(Seq1,Seq2),Hyps,Res12,Hyps2) :- !, % ran(S1^S2) = ran(S1) \/ ran(S2) | |
| 836 | get_range_or_superset(Seq1,Hyps,Res1,Hyps2), | |
| 837 | get_range_or_superset(Seq2,Hyps,Res2,Hyps2), | |
| 838 | construct_union(Res1,Res2,Hyps2,Res12). | |
| 839 | get_range_or_superset(composition(_,Func2),Hyps,Res2,Hyps2) :- !, % ran((F1;F2)) <: ran(F2) | |
| 840 | get_range_or_superset(Func2,Hyps,Res2,Hyps2). | |
| 841 | get_range_or_superset(cartesian_product(_,B),Hyps,Res,Hyps) :- !, Res=B. % ran(A*B) <: B | |
| 842 | get_range_or_superset(Func,Hyps,Range,Hyps2) :- | |
| 843 | avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1), | |
| 844 | get_range_or_superset(Func2,Hyps1,Range,Hyps2). | |
| 845 | get_range_or_superset(Func,Hyps,RangeSuperSet,Hyps2) :- | |
| 846 | avl_fetch_binop_from_hyps(range(Func),subset,Hyps,RangeSuperSet,Hyps2). | |
| 847 | get_range_or_superset(CompSet,Hyps,RangeSuperSet,Hyps2) :- | |
| 848 | is_comprehension_set(CompSet,IDS,Body), | |
| 849 | get_lambda_args_and_body(IDS,Body,_,Expr,RestIDs,RestBodyList), | |
| 850 | add_new_hyp_any_vars(Hyps,RestIDs,Hyps0), % do not infer anything about lambda vars | |
| 851 | get_clash_renaming_subst(Hyps0,Renaming), | |
| 852 | l_push_normalized_hyp(RestBodyList,Renaming,Hyps0,Hyps1), | |
| 853 | (hyps_inconsistent(Hyps1) -> RangeSuperSet = empty_set, Hyps2=Hyps | |
| 854 | ; rename_norm_term(Expr,Renaming,RNExpr), | |
| 855 | try_get_set_of_possible_values(RNExpr,Hyps1,RangeSuperSet,Hyps2) | |
| 856 | ). | |
| 857 | % get_range_or_superset(Func,_,_,_) :- print(get_range_or_superset_failed(Func)),nl,fail. | |
| 858 | % to do: more sequence operations: insert_front, insert_tail | |
| 859 | ||
| 860 | l_push_normalized_hyp([],_,Hyp,Hyp). | |
| 861 | l_push_normalized_hyp([H|T],Renaming,Hyp0,Hyp2) :- | |
| 862 | rename_norm_term(H,Renaming,RenamedH), | |
| 863 | push_normalized_hyp(RenamedH,Hyp0,Hyp1), | |
| 864 | l_push_normalized_hyp(T,Renaming,Hyp1,Hyp2). | |
| 865 | ||
| 866 | % get exact range without equality rewrites | |
| 867 | get_exact_range_of_func_type_direct(Func,R) :- | |
| 868 | get_possible_range_of_func_or_rel_type_direct(Func,R,exact). | |
| 869 | % TO DO: maybe do same treatment for set_extension as in get_exact_domain_of_func_or_rel_type | |
| 870 | ||
| 871 | % get possible range with equality rewrites | |
| 872 | get_possible_range_of_func_or_rel_type(Func,Hyps,Range,ResType,Hyps2) :- | |
| 873 | get_possible_range_of_func_or_rel_type_direct(Func,Range,Type),!, ResType=Type,Hyps2=Hyps. | |
| 874 | get_possible_range_of_func_or_rel_type(Func,Hyps,Range,ResType,Hyps2) :- | |
| 875 | avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1), | |
| 876 | get_possible_range_of_func_or_rel_type(Func2,Hyps1,Range,ResType,Hyps2). | |
| 877 | ||
| 878 | % get possible range without equality rewrites | |
| 879 | get_possible_range_of_func_or_rel_type_direct(total_function(_,B),B,subset). | |
| 880 | get_possible_range_of_func_or_rel_type_direct(total_injection(_,B),B,subset). | |
| 881 | get_possible_range_of_func_or_rel_type_direct(total_surjection(_,B),B,exact). | |
| 882 | get_possible_range_of_func_or_rel_type_direct(total_bijection(_,B),B,exact). | |
| 883 | get_possible_range_of_func_or_rel_type_direct(total_relation(_,B),B,subset). | |
| 884 | get_possible_range_of_func_or_rel_type_direct(total_surjection_relation(_,B),B,exact). | |
| 885 | get_possible_range_of_func_or_rel_type_direct(partial_function(_,B),B,subset). | |
| 886 | get_possible_range_of_func_or_rel_type_direct(partial_injection(_,B),B,subset). | |
| 887 | get_possible_range_of_func_or_rel_type_direct(partial_surjection(_,B),B,exact). | |
| 888 | get_possible_range_of_func_or_rel_type_direct(partial_bijection(_,B),B,exact). | |
| 889 | get_possible_range_of_func_or_rel_type_direct(perm(B),B,exact). | |
| 890 | get_possible_range_of_func_or_rel_type_direct(iseq(B),B,subset). | |
| 891 | get_possible_range_of_func_or_rel_type_direct(iseq1(B),B,subset). | |
| 892 | get_possible_range_of_func_or_rel_type_direct(seq(B),B,subset). | |
| 893 | get_possible_range_of_func_or_rel_type_direct(seq1(B),B,subset). | |
| 894 | get_possible_range_of_func_or_rel_type_direct(relations(_,B),B,subset). | |
| 895 | get_possible_range_of_func_or_rel_type_direct(surjection_relation(_,B),B,exact). | |
| 896 | get_possible_range_of_func_or_rel_type_direct(pow_subset(cartesian_product(_,B)),B,subset). | |
| 897 | get_possible_range_of_func_or_rel_type_direct(pow1_subset(cartesian_product(_,B)),B,subset). | |
| 898 | get_possible_range_of_func_or_rel_type_direct(fin_subset(cartesian_product(_,B)),B,subset). | |
| 899 | get_possible_range_of_func_or_rel_type_direct(fin1_subset(cartesian_product(_,B)),B,subset). | |
| 900 | ||
| 901 | ||
| 902 | % EXACT REWRITING/SIMPLIFICATION RULES | |
| 903 | ||
| 904 | % simplifier, useful rules independent of context | |
| 905 | simplify_expr(A,Hyps,Res) :- | |
| 906 | simplify_expr(A,Hyps,1,Res). % no repeated applications of rule | |
| 907 | simplify_expr_loop(A,Hyps,Res) :- | |
| 908 | simplify_expr(A,Hyps,3,Res). % which value to use here? | |
| 909 | simplify_expr(A,Hyps,MaxLoop,Res) :- | |
| 910 | rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!, | |
| 911 | simplify_iter(A2,Hyps2,MaxLoop,Res). | |
| 912 | simplify_expr(A,Hyps,MaxLoop,Res) :- | |
| 913 | rewrite_integer(A,Hyps,A2,Hyps2),!, | |
| 914 | simplify_iter(A2,Hyps2,MaxLoop,Res). | |
| 915 | simplify_expr(record_field(rec(Fields),Field),Hyps,MaxLoop,SExpr) :- | |
| 916 | member(field(Field,Expr),Fields),!, | |
| 917 | simplify_expr(Expr,Hyps,MaxLoop,SExpr). | |
| 918 | simplify_expr(domain(A),Hyps,MaxLoop,Res) :- | |
| 919 | simplify_domain(A,SA),!,simplify_expr(SA,Hyps,MaxLoop,Res). | |
| 920 | simplify_expr(range(A),Hyps,MaxLoop,Res) :- | |
| 921 | simplify_range(A,SA),!,simplify_expr(SA,Hyps,MaxLoop,Res). | |
| 922 | simplify_expr(E,_,_,E). | |
| 923 | ||
| 924 | simplify_iter(A,Hyps,MaxLoop,Res) :- MaxLoop > 1,!, | |
| 925 | M1 is MaxLoop-1, simplify_expr(A,Hyps,M1,Res). | |
| 926 | simplify_iter(A,_,_,A). | |
| 927 | ||
| 928 | simplify_domain(reverse(A),range(A)). | |
| 929 | simplify_domain(closure(A),domain(A)). % rx : A <-> B <=> closure1(rx) : A <-> B | |
| 930 | simplify_range(reverse(A),domain(A)). | |
| 931 | simplify_range(closure(A),range(A)). % rx : A <-> B <=> closure1(rx) : A <-> B | |
| 932 | ||
| 933 | get_lambda_args_and_body(IDS,Body,LambdaID,LambdaExpr,RestArgs,RestBodyList) :- | |
| 934 | LambdaID='$'(Lambda), | |
| 935 | append(RestArgs,[LambdaID],IDS), % TO DO: pass lambda info from typed unnormalized expression! | |
| 936 | conj_to_list(Body,BodyList,[]), | |
| 937 | select(equal(A,B),BodyList,RestBodyList), | |
| 938 | ( A=LambdaID, not_occurs(B,Lambda), LambdaExpr=B | |
| 939 | ; B=LambdaID, not_occurs(A,Lambda), LambdaExpr=A | |
| 940 | ). | |
| 941 | ||
| 942 | % just check if something is a lambda function or similar, without computing exact domain | |
| 943 | is_lambda_function(CompSet) :- is_comprehension_set(CompSet,IDS,Body), !, | |
| 944 | get_lambda_args_and_body(IDS,Body,_,_,_,_). | |
| 945 | is_lambda_function(Expr) :- is_lambda_function_with_domain(Expr,_). | |
| 946 | ||
| 947 | % determine if something is a lambda function and determines exact domain: | |
| 948 | is_lambda_function_with_domain(CompSet,Set) :- | |
| 949 | is_comprehension_set(CompSet,IDS,Body), !, | |
| 950 | get_lambda_args_and_body(IDS,Body,_,_,Args,RestBodyList), | |
| 951 | get_argument_types(Args,Args,RestBodyList,ArgTypes), | |
| 952 | create_cartesian_product(ArgTypes,Set). | |
| 953 | is_lambda_function_with_domain(cartesian_product(Domain,Set),Domain) :- | |
| 954 | singleton_set(Set,_). | |
| 955 | is_lambda_function_with_domain(set_extension([couple(El,_)]),set_extension([El])). | |
| 956 | is_lambda_function_with_domain(Set,singleton_set([El])) :- singleton_set(Set,couple(El,_)). % TO DO: longer lists and check no multiple domain elements | |
| 957 | is_lambda_function_with_domain(sequence_extension(List),interval(1,Len)) :- length(List,Len). | |
| 958 | % we could treat domain_restriction, domain_subtraction here | |
| 959 | ||
| 960 | singleton_set(set_extension([El]),El). | |
| 961 | singleton_set(sorted_set_extension([El]),El). | |
| 962 | ||
| 963 | conj_to_list(conjunct(A,B)) --> !, conj_to_list(A),conj_to_list(B). | |
| 964 | conj_to_list(X) --> [X]. | |
| 965 | ||
| 966 | list_to_conj([],truth). | |
| 967 | list_to_conj([X],Res) :- !, Res=X. | |
| 968 | list_to_conj([H|T],conjunct(H,R)) :- list_to_conj(T,R). | |
| 969 | ||
| 970 | :- use_module(probsrc(tools),[map_split_list/4]). | |
| 971 | % we support Arg:Set and we support an argument not appearing at all (equivalent to Arg:typeset) | |
| 972 | get_argument_types([],_,[],[]). % no other conjuncts remain in body | |
| 973 | get_argument_types(['$'(ID1)|T],AllArgs,BodyList,[Set1|TS]) :- | |
| 974 | map_split_list(typing_predicate_for(ID1,AllArgs),BodyList,TypingSetList,RestBody), | |
| 975 | create_intersection(TypingSetList,Set1), | |
| 976 | get_argument_types(T,AllArgs,RestBody,TS). | |
| 977 | ||
| 978 | % check if we have a typing predicate for a given identifier | |
| 979 | typing_predicate_for(ID1,AllArgs,member('$'(ID1),Set1),Set1) :- l_not_occurs(Set1,AllArgs). | |
| 980 | typing_predicate_for(ID1,AllArgs,subset('$'(ID1),SSet1),pow_subset(SSet1)) :- l_not_occurs(SSet1,AllArgs). | |
| 981 | ||
| 982 | % check if any argument appears in expression; if so we have a link between arguments and no proper type | |
| 983 | l_not_occurs(Expr,AllArgs) :- member('$'(ID),AllArgs), occurs(Expr,ID),!,fail. | |
| 984 | l_not_occurs(_,_). | |
| 985 | ||
| 986 | % check that #Vars.Conjuncts holds by repeatedly removing a conjunct C(V) about a variable V of Vars, | |
| 987 | % where V occurs in no other conjunct and #V.C(V) holds for all values of the other variables: | |
| 988 | % then #V.(C(V) & Rest) <=> Rest; the Vars are added as unconstrained hyp variables | |
| 989 | check_satisfiable_conjuncts(Conjuncts,Vars,Hyps) :- | |
| 990 | add_new_hyp_any_vars(Hyps,Vars,Hyps1), % do not infer anything about the quantified variables | |
| 991 | get_clash_renaming_subst(Hyps1,Renaming0), | |
| 992 | maplist(dollar_renaming,Renaming0,Renaming), % rename_norm_term replaces '$'(ID) by the new term | |
| 993 | maplist(rename_conjunct(Renaming),Conjuncts,RConjuncts), | |
| 994 | maplist(rename_conjunct(Renaming),Vars,RVars), | |
| 995 | all_satisfiable(RConjuncts,RVars,Hyps1). | |
| 996 | rename_conjunct(Renaming,C,RC) :- rename_norm_term(C,Renaming,RC). | |
| 997 | dollar_renaming(rename(ID,FreshID),rename(ID,'$'(FreshID))). | |
| 998 | ||
| 999 | % check all conjuncts constrain exactly one variable in a satisfiable manner | |
| 1000 | % TODO: can have quadratic complexity | |
| 1001 | all_satisfiable([],_,_) :- !. | |
| 1002 | all_satisfiable(Conjuncts,Vars,Hyps) :- | |
| 1003 | select(C,Conjuncts,Rest), % we may not want to pick the first conjunct; see {y|#a.(a : 1 .. 3 & y <: {a,a + 1})} | |
| 1004 | (C=truth -> Hyps1=Hyps | |
| 1005 | ; satisfiable_for_var(C,V,Hyps), memberchk('$'(V),Vars), | |
| 1006 | \+ (member(C2,Rest), occurs(C2,V)), | |
| 1007 | push_normalized_hyp(C,Hyps,Hyps1) | |
| 1008 | ), | |
| 1009 | !, | |
| 1010 | all_satisfiable(Rest,Vars,Hyps1). | |
| 1011 | ||
| 1012 | % satisfiable_for_var(C,V,Hyps): V does not occur in C's other argument and #V.C holds | |
| 1013 | satisfiable_for_var(Pred,V,Hyps) :- var_binop(Pred,Op,V,E), not_occurs(E,V), | |
| 1014 | satisfiable_binop(Op,E,Hyps). | |
| 1015 | ||
| 1016 | var_binop(Pred,Op,V,E) :- Pred =.. [Op,A,B], | |
| 1017 | (A='$'(V), E=B ; B='$'(V), E=A, Op \= member, Op \= subset, Op \= subset_strict). | |
| 1018 | ||
| 1019 | satisfiable_binop(equal,_,_). % one-point rule | |
| 1020 | satisfiable_binop(subset,_,_). % V={} is a witness | |
| 1021 | satisfiable_binop(subset_strict,S,Hyps) :- check_not_empty_set(S,Hyps). % V={} is a witness if S/={} | |
| 1022 | satisfiable_binop(member,S,Hyps) :- check_not_empty_set(S,Hyps). | |
| 1023 | satisfiable_binop(less,_,_). % the integers and reals are unbounded | |
| 1024 | satisfiable_binop(less_equal,_,_). | |
| 1025 | satisfiable_binop(greater,_,_). | |
| 1026 | satisfiable_binop(greater_equal,_,_). | |
| 1027 | satisfiable_binop(less_real,_,_). | |
| 1028 | satisfiable_binop(less_equal_real,_,_). | |
| 1029 | satisfiable_binop(not_equal,E,Hyps) :- type_has_two_elements(E,Hyps). | |
| 1030 | ||
| 1031 | % check if the type of an expression has at least two elements | |
| 1032 | type_has_two_elements(Nr,_) :- number(Nr),!. % infinitely many values | |
| 1033 | type_has_two_elements(E,_) :- functor(E,F,N), two_element_type_functor(F,N),!. | |
| 1034 | type_has_two_elements('$'(ID),Hyps) :- get_hyp_var_type(ID,Hyps,Type),!, two_element_type(Type). | |
| 1035 | type_has_two_elements(couple(A,B),Hyps) :- (type_has_two_elements(A,Hyps) -> true ; type_has_two_elements(B,Hyps)). | |
| 1036 | ||
| 1037 | two_element_type(Type) :- var(Type),!,fail. | |
| 1038 | two_element_type(integer). | |
| 1039 | two_element_type(real). | |
| 1040 | two_element_type(string). | |
| 1041 | two_element_type(boolean). | |
| 1042 | two_element_type(set(_)). | |
| 1043 | two_element_type(couple(A,B)) :- (two_element_type(A) -> true ; two_element_type(B)). | |
| 1044 | % TODO: global; check minimum two values | |
| 1045 | ||
| 1046 | two_element_type_functor(boolean_true,0). | |
| 1047 | two_element_type_functor(boolean_false,0). | |
| 1048 | two_element_type_functor(string,1). | |
| 1049 | two_element_type_functor(real,1). | |
| 1050 | two_element_type_functor(integer,1). | |
| 1051 | two_element_type_functor(add,2). | |
| 1052 | two_element_type_functor(minus,2). | |
| 1053 | two_element_type_functor(multiplication,2). | |
| 1054 | two_element_type_functor(unary_minus,1). | |
| 1055 | two_element_type_functor(card,1). | |
| 1056 | two_element_type_functor(size,1). | |
| 1057 | two_element_type_functor(empty_set,0). % all set types POW(T) contain {} and T; no type in B is empty | |
| 1058 | two_element_type_functor(set_extension,1). | |
| 1059 | two_element_type_functor(interval,2). | |
| 1060 | two_element_type_functor(union,2). | |
| 1061 | two_element_type_functor(intersection,2). | |
| 1062 | two_element_type_functor(set_subtraction,2). | |
| 1063 | two_element_type_functor(domain,1). | |
| 1064 | two_element_type_functor(range,1). | |
| 1065 | ||
| 1066 | create_intersection([],typeset). % no constraints on identifier: use typeset | |
| 1067 | create_intersection([A],Res) :- !, Res=A. | |
| 1068 | create_intersection([A|T],intersection(A,Rest)) :- create_intersection(T,Rest). | |
| 1069 | ||
| 1070 | create_cartesian_product([Type],Res) :- !, Res=Type. | |
| 1071 | create_cartesian_product([Type|T],Res) :- create_cartesian_product3(T,Type,Res). | |
| 1072 | ||
| 1073 | create_cartesian_product3([],Res,Res). | |
| 1074 | create_cartesian_product3([Type|T],Acc,Res) :- | |
| 1075 | create_cartesian_product3(T,cartesian_product(Acc,Type),Res). | |
| 1076 | % Note: dom(%(x,y,z).(x:BOOL & y:1..2 & z:BOOL|1)) = (BOOL*(1..2))*BOOL | |
| 1077 | ||
| 1078 | % ------------------------ | |
| 1079 | ||
| 1080 | % Partial Function Check: | |
| 1081 | ||
| 1082 | % check if Func : Domain +-> Range | |
| 1083 | check_is_partial_function_with_type(Func,_,_,Hyps,empty_set(PT)) :- check_equal_empty_set(Func,Hyps,PT),!. | |
| 1084 | check_is_partial_function_with_type(Func,Domain,Range,Hyps,pfun(PTD,PTR)) :- | |
| 1085 | check_is_partial_function(Func,Hyps),!, | |
| 1086 | (maximal_set(Domain,Hyps) -> PTD=maximal_domain ; check_is_subset(domain(Func),Domain,Hyps,PTD)),!, | |
| 1087 | (maximal_set(Range,Hyps) -> PTR=maximal_range ; check_is_subset(range(Func),Range,Hyps,PTR)). | |
| 1088 | ||
| 1089 | % various way to make a function smaller, related to subset | |
| 1090 | function_restriction(domain_subtraction(_,F),F). | |
| 1091 | function_restriction(domain_restriction(_,F),F). | |
| 1092 | function_restriction(range_subtraction(F,_),F). | |
| 1093 | function_restriction(range_restriction(F,_),F). | |
| 1094 | function_restriction(set_subtraction(F,_),F). | |
| 1095 | ||
| 1096 | % check if Func : DomTYPE +-> RanTYPE | |
| 1097 | % check if we can deduce from the Hypotheses that something is a partial function | |
| 1098 | check_is_partial_function(Func,Hyps) :- | |
| 1099 | avl_fetch_mem_or_struct(Func,Hyps,Function,Hyps1), | |
| 1100 | % also deals with function(_) f : _ +-> ( _ +-> _ ) => f(_) : _ +-> _ | |
| 1101 | is_partial_function_type(Function,Hyps1,_),!. | |
| 1102 | check_is_partial_function(reverse(Func),Hyps) :- | |
| 1103 | check_is_injective(Func,Hyps),!. | |
| 1104 | check_is_partial_function(value(avl_set(AVL)),_) :- !, | |
| 1105 | nonvar(AVL), | |
| 1106 | is_avl_partial_function(AVL). | |
| 1107 | check_is_partial_function(composition(F1,F2),Hyp) :- !, | |
| 1108 | % composition of two partial functions is a partial function | |
| 1109 | (check_is_partial_function(F1,Hyp) | |
| 1110 | -> check_is_partial_function(F2,Hyp) | |
| 1111 | ). | |
| 1112 | check_is_partial_function(overwrite(F1,F2),Hyp) :- !, | |
| 1113 | % overwrite of two partial functions is a partial function | |
| 1114 | (check_is_partial_function(F1,Hyp) | |
| 1115 | -> check_is_partial_function(F2,Hyp) | |
| 1116 | ). | |
| 1117 | check_is_partial_function(direct_product(F1,F2),Hyp) :- !, | |
| 1118 | % direct_product of two partial functions is a partial function a:A+->B & b:A+->C => a><b : A+->(B*C) | |
| 1119 | (check_is_partial_function(F1,Hyp) | |
| 1120 | -> check_is_partial_function(F2,Hyp) | |
| 1121 | ). | |
| 1122 | check_is_partial_function(identity(_),_Hyp) :- !. | |
| 1123 | check_is_partial_function(Func,Hyp) :- function_restriction(Func,LargerFunc), !, | |
| 1124 | check_is_partial_function(LargerFunc,Hyp). | |
| 1125 | check_is_partial_function(intersection(F1,F2),Hyp) :- !, | |
| 1126 | (check_is_partial_function(F1,Hyp) -> true ; check_is_partial_function(F2,Hyp)). | |
| 1127 | check_is_partial_function(sorted_set_extension(List),Hyp) :- !, | |
| 1128 | check_set_extension_is_partial_function(List,Hyp). | |
| 1129 | check_is_partial_function(set_extension(List),Hyp) :- !, | |
| 1130 | check_set_extension_is_partial_function(List,Hyp). | |
| 1131 | check_is_partial_function(Expr,_) :- | |
| 1132 | is_lambda_function(Expr),!. % also treats cartesian_product and sequence_extension | |
| 1133 | % check_is_partial_function(X,_Hyp) :- is_empty_set_direct(X),!. % covered by infer_sequence_type_of_expr below | |
| 1134 | check_is_partial_function(Expr,Hyps) :- | |
| 1135 | infer_sequence_type_of_expr(Expr,Hyps,_),!. % any sequence expression is a partial function; e.g. a <- b, front(.) | |
| 1136 | check_is_partial_function(Func,Hyps) :- rewrite_set_expression_exact(Func,Hyps,NewFunc,Hyps2),!, | |
| 1137 | check_is_partial_function(NewFunc,Hyps2). | |
| 1138 | check_is_partial_function(union(F1,F2),Hyps) :- | |
| 1139 | check_is_subset(F1,F2,Hyps,_),!, | |
| 1140 | check_is_partial_function(F2,Hyps). | |
| 1141 | check_is_partial_function(union(F1,F2),Hyps) :- | |
| 1142 | check_is_subset(F2,F1,Hyps,_),!, | |
| 1143 | check_is_partial_function(F1,Hyps). | |
| 1144 | check_is_partial_function(union(F1,F2),Hyps) :- !, | |
| 1145 | check_domain_disjoint(F1,F2,Hyps,Hyps2), % domain must be disjoint, not F1 and F2 | |
| 1146 | check_is_partial_function(F1,Hyps2), | |
| 1147 | check_is_partial_function(F2,Hyps2). | |
| 1148 | check_is_partial_function(Func,Hyps) :- % f<:g & g: A +-> B => f : A +-> B | |
| 1149 | (Op = equal ; Op = subset), | |
| 1150 | avl_fetch_binop_from_hyps(Func,Op,Hyps,Func2,Hyps1), | |
| 1151 | quick_not_occurs_check(Func,Func2), | |
| 1152 | check_is_partial_function(Func2,Hyps1). | |
| 1153 | %check_is_partial_function(Func,_) :- print(check_is_partial_function_failed(Func)),nl,fail. | |
| 1154 | ||
| 1155 | check_domain_disjoint(F1,F2,Hyps,Hyps2) :- | |
| 1156 | compute_exact_domain(F1,Hyps,DF1,Hyps2), | |
| 1157 | % example: :prove f:BOOL +-> BOOL & x /: dom(f) => f \/ {x|->TRUE} : BOOL +-> BOOL | |
| 1158 | is_set_extension(DF1,List1),!, | |
| 1159 | l_check_not_member_of_set(List1,domain(F2),Hyps2). % we could try and compute domain(F2) first | |
| 1160 | check_domain_disjoint(F2,F1,Hyps,Hyps2) :- | |
| 1161 | compute_exact_domain(F1,Hyps,DF1,Hyps2), | |
| 1162 | is_set_extension(DF1,List1),!, | |
| 1163 | l_check_not_member_of_set(List1,domain(F2),Hyps2). | |
| 1164 | check_domain_disjoint(F1,F2,Hyps,Hyps2) :- | |
| 1165 | get_domain_or_superset(F1,Hyps,DomFunc1,Hyps1), | |
| 1166 | get_domain_or_superset(F2,Hyps1,DomFunc2,Hyps2), | |
| 1167 | check_disjoint(DomFunc1,DomFunc2,Hyps2). | |
| 1168 | ||
| 1169 | ||
| 1170 | % check if this is a partial function type or something defined to be equal to a function type | |
| 1171 | :- if(environ(prob_safe_mode,true)). | |
| 1172 | is_partial_function_type(P,H,H1) :- nonvar(H1), | |
| 1173 | add_internal_error('Illegal hyps:',is_partial_function_type(P,H,H1)),fail. | |
| 1174 | :- endif. | |
| 1175 | is_partial_function_type(PF,Hyps,Hyps1) :- is_partial_function(PF,_,_),!,Hyps1=Hyps. | |
| 1176 | is_partial_function_type(range(Func),Hyps,Hyps2) :- | |
| 1177 | get_range_or_superset(Func,Hyps,RanFunc,Hyps1),!, | |
| 1178 | is_partial_function_type(RanFunc,Hyps1,Hyps2). | |
| 1179 | is_partial_function_type(domain(Func),Hyps,Hyps2) :- | |
| 1180 | get_domain_or_superset(Func,Hyps,DomFunc,Hyps1),!, | |
| 1181 | is_partial_function_type(DomFunc,Hyps1,Hyps2). | |
| 1182 | is_partial_function_type(sorted_set_extension(Funcs),Hyps,Hyps2) :- !, | |
| 1183 | is_partial_function_type(set_extension(Funcs),Hyps,Hyps2). | |
| 1184 | is_partial_function_type(set_extension(Funcs),Hyps,Hyps2) :- !, | |
| 1185 | (member(F,Funcs), \+ check_is_partial_function(F,Hyps) -> fail | |
| 1186 | ; Hyps2=Hyps). % all elements of Funcs are partial functions | |
| 1187 | is_partial_function_type(Func,Hyps,Hyps2) :- | |
| 1188 | get_superset(Func,Hyps,SuperSet,Hyps1),!, | |
| 1189 | is_partial_function_type(SuperSet,Hyps1,Hyps2). | |
| 1190 | is_partial_function_type(PF,Hyps,Hyps2) :- | |
| 1191 | avl_fetch_worthwhile_equal_from_hyps(PF,Hyps,PF2,Hyps1), % in case we have a definition like X = 1..n --> R | |
| 1192 | is_partial_function_type(PF2,Hyps1,Hyps2). | |
| 1193 | ||
| 1194 | % get worthwhile superset | |
| 1195 | get_superset(set_subtraction(A,_),Hyps,R,Hyps) :- !, R=A. | |
| 1196 | get_superset(intersection(A,B),Hyps,R,Hyps) :- !, (R=A ; R=B). | |
| 1197 | get_superset(CompSet,Hyps,Set,Hyps) :- is_comprehension_set(CompSet,[ID],Body),!, | |
| 1198 | get_parameter_superset_in_body(ID,[ID],Body,Set). | |
| 1199 | ||
| 1200 | is_partial_function(total_function(A,B),A,B). | |
| 1201 | is_partial_function(partial_function(A,B),A,B). | |
| 1202 | is_partial_function(total_injection(A,B),A,B). | |
| 1203 | is_partial_function(partial_injection(A,B),A,B). | |
| 1204 | is_partial_function(total_surjection(A,B),A,B). | |
| 1205 | is_partial_function(partial_surjection(A,B),A,B). | |
| 1206 | is_partial_function(total_bijection(A,B),A,B). | |
| 1207 | is_partial_function(partial_bijection(A,B),A,B). | |
| 1208 | is_partial_function(perm(A),'NATURAL1',A). | |
| 1209 | is_partial_function(seq(B),'NATURAL1',B). | |
| 1210 | is_partial_function(seq1(B),'NATURAL1',B). | |
| 1211 | is_partial_function(iseq(B),'NATURAL1',B). | |
| 1212 | is_partial_function(iseq1(B),'NATURAL1',B). | |
| 1213 | ||
| 1214 | % if First = f(1,GS) -> we can check if function is total; we could store summary of set_extension in hyps | |
| 1215 | check_set_extension_is_partial_function([_],_) :- !. % one element set extension is a function | |
| 1216 | check_set_extension_is_partial_function(List,Hyps) :- | |
| 1217 | maplist(get_explicit_dom_value(Hyps),List,VList),!, | |
| 1218 | sort(VList,SList), | |
| 1219 | SList = [couple(First,_)|TS], | |
| 1220 | check_set_ext_pf(TS,First,Hyps). | |
| 1221 | check_set_extension_is_partial_function([couple(A,_),couple(B,_)],Hyps) :- | |
| 1222 | check_not_equal(A,B,Hyps). % TO DO: all_different for longer lists | |
| 1223 | ||
| 1224 | check_set_ext_pf([],_,_). | |
| 1225 | check_set_ext_pf([couple(Next,_)|TS],Last,Hyp) :- | |
| 1226 | Next \= Last, | |
| 1227 | check_set_ext_pf(TS,Next,Hyp). | |
| 1228 | ||
| 1229 | get_explicit_dom_value(Hyps,couple(Val,RanVal),couple(Val2,RanVal)) :- get_explicit_value(Val,Hyps,Val2). | |
| 1230 | ||
| 1231 | get_explicit_value(couple(A,B),Hyps,couple(A2,B2)) :- !, | |
| 1232 | get_explicit_value(A,Hyps,A2), get_explicit_value(B,Hyps,B2). | |
| 1233 | get_explicit_value(rec(Fields),Hyps,rec(SFields2)) :- !, | |
| 1234 | maplist(get_field_value(Hyps),Fields,Fields2), | |
| 1235 | sort(Fields2,SFields2). | |
| 1236 | get_explicit_value(Val,Hyps,R) :- is_explicit_value(Val,AVal,Hyps),!,R=AVal. | |
| 1237 | get_explicit_value('$'(ID),Hyps,Res) :- | |
| 1238 | avl_fetch_equal_from_hyps('$'(ID),Hyps,Val2,Hyps2), | |
| 1239 | is_explicit_value(Val2,Res,Hyps2). % should we allow recursion through multiple equations? | |
| 1240 | ||
| 1241 | % is value which can be compared using Prolog equality | |
| 1242 | % cf. avl_can_fetch | |
| 1243 | is_explicit_value(boolean_true,pred_true,_). | |
| 1244 | is_explicit_value(boolean_false,pred_false,_). | |
| 1245 | is_explicit_value(Nr,Nr,_) :- number(Nr). % integers and floats | |
| 1246 | is_explicit_value(integer(Nr),Nr,_) :- integer(Nr). % normally already replaced by norm_expr2 | |
| 1247 | is_explicit_value(string(Atom),Atom,_). | |
| 1248 | is_explicit_value(real(Atom),Res,_) :- atom(Atom), | |
| 1249 | construct_real(Atom,term(floating(Res))). % c.f. is_real/1 in kernel_reals | |
| 1250 | is_explicit_value(couple(A,B),(AV,BV),Hyp) :- is_explicit_value(A,AV,Hyp), is_explicit_value(B,BV,Hyp). | |
| 1251 | is_explicit_value('$'(ID),'$'(ID),Hyp) :- is_global_constant_id(ID,Hyp). | |
| 1252 | is_explicit_value(value(R),Nr,_) :- nonvar(R), R=int(Nr), integer(Nr). % TODO: more values, strings, reals, ... | |
| 1253 | ||
| 1254 | ||
| 1255 | get_field_value(Hyps,field(Name,Val),field(Name,Val2)) :- get_explicit_value(Val,Hyps,Val2). | |
| 1256 | ||
| 1257 | :- use_module(probsrc(b_global_sets), [lookup_global_constant/2]). | |
| 1258 | % enumerated set element name | |
| 1259 | is_global_constant_id(ID,Hyp) :- | |
| 1260 | lookup_global_constant(ID,_), | |
| 1261 | \+ is_hyp_var(ID,Hyp). % global enumerated set constant visible | |
| 1262 | ||
| 1263 | is_enumerated_set(ID,Hyp) :- | |
| 1264 | enumerated_set(ID), | |
| 1265 | \+ is_hyp_var(ID,Hyp). % global enumerated set constant visible | |
| 1266 | ||
| 1267 | % Disjoint check: | |
| 1268 | check_disjoint(interval(Low1,Up1),interval(Low2,Up2),Hyps) :- !, | |
| 1269 | (check_less(Up1,Low2,Hyps) -> true ; check_less(Up2,Low1,Hyps) -> true | |
| 1270 | ; check_less(Up1,Low1,Hyps) -> true ; check_less(Up2,Low2,Hyps) -> true). | |
| 1271 | check_disjoint(A,B,Hyps) :- %print(disj(A,B)),nl, portray_hyps(Hyps),nl, | |
| 1272 | (check_disjoint_aux(A,B,Hyps) -> true ; check_disjoint_aux(B,A,Hyps)). | |
| 1273 | ||
| 1274 | check_disjoint_aux(S,_,Hyps) :- check_equal_empty_set(S,Hyps,_),!. | |
| 1275 | check_disjoint_aux(A,B,Hyps) :- | |
| 1276 | avl_fetch_from_hyps(equal(intersection(A,B),empty_set),Hyps),!. | |
| 1277 | check_disjoint_aux(domain_subtraction(A,_),B,Hyps) :- !, % A <<| f /\ B = {} if dom(B) <: A | |
| 1278 | get_domain_or_superset(B,Hyps,DomB,Hyps2), | |
| 1279 | check_is_subset(DomB,A,Hyps2,_). | |
| 1280 | check_disjoint_aux(set_subtraction(AA,A),B,Hyps) :- !, | |
| 1281 | (check_is_subset(B,A,Hyps,_) -> true % x \ A /\ B = {} if B <: A | |
| 1282 | ; check_disjoint(AA,B,Hyps) -> true). % AA-A /\ B ={} if AA /\ B = {} | |
| 1283 | check_disjoint_aux(set_extension(As),B,Hyps) :- !, l_check_not_member_of_set(As,B,Hyps). | |
| 1284 | check_disjoint_aux(sorted_set_extension(As),B,Hyps) :- !, l_check_not_member_of_set(As,B,Hyps). | |
| 1285 | check_disjoint_aux(domain(Func),B,Hyps) :- !, | |
| 1286 | get_domain_or_superset(Func,Hyps,DomFunc,Hyps2), | |
| 1287 | check_disjoint(DomFunc,B,Hyps2). | |
| 1288 | check_disjoint_aux(range(Func),B,Hyps) :- !, | |
| 1289 | get_range_or_superset(Func,Hyps,RanFunc,Hyps2), | |
| 1290 | check_disjoint(RanFunc,B,Hyps2). | |
| 1291 | check_disjoint_aux(A,B,Hyps) :- | |
| 1292 | avl_fetch_worthwhile_equal_from_hyps(A,Hyps,A1,Hyps1), | |
| 1293 | check_disjoint(A1,B,Hyps1). | |
| 1294 | % TO DO: move union of set_extension here? | |
| 1295 | ||
| 1296 | l_check_not_member_of_set([],_,_). | |
| 1297 | l_check_not_member_of_set([El|T],Set,Hyps) :- | |
| 1298 | check_not_member_of_set(Set,El,Hyps,_PT), | |
| 1299 | l_check_not_member_of_set(T,Set,Hyps). | |
| 1300 | ||
| 1301 | % Injective check: | |
| 1302 | ||
| 1303 | check_is_injective(Func,Hyps) :- | |
| 1304 | get_type_from_hyps(Func,Hyps,Function,Hyps1), | |
| 1305 | %print(check_rev_fun(Func,Function)),nl, | |
| 1306 | is_injective_function_type(Function,Hyps1,_). | |
| 1307 | check_is_injective(value(avl_set(AVL)),_) :- !, | |
| 1308 | nonvar(AVL), invert_explicit_set(avl_set(AVL),Inv), | |
| 1309 | Inv=avl_set(AVL2), is_avl_partial_function(AVL2). | |
| 1310 | check_is_injective(identity(_),_). | |
| 1311 | check_is_injective(Set,_) :- singleton_set(Set,_). % TO DO: extend to more than singleton set_extension | |
| 1312 | check_is_injective(sequence_extension([_]),_). % TO DO: check all elements are different | |
| 1313 | check_is_injective(Func, Hyps) :- | |
| 1314 | avl_fetch_equal_from_hyps(Func,Hyps,Value,Hyps2), | |
| 1315 | %print(check_inj_value(Func,Value)),nl, | |
| 1316 | check_is_injective(Value,Hyps2). | |
| 1317 | ||
| 1318 | % check if this is a partial function type or something defined to be equal to a function type | |
| 1319 | is_injective_function_type(PF,Hyps,Hyps1) :- is_injective(PF),!,Hyps1=Hyps. | |
| 1320 | is_injective_function_type(PF,Hyps,Hyps2) :- | |
| 1321 | avl_fetch_worthwhile_equal_from_hyps(PF,Hyps,PF2,Hyps1), % in case we have a definition like X = 1..n --> R | |
| 1322 | is_injective_function_type(PF2,Hyps1,Hyps2). | |
| 1323 | ||
| 1324 | is_injective(total_injection(_,_)). | |
| 1325 | is_injective(partial_injection(_,_)). | |
| 1326 | is_injective(total_bijection(_,_)). | |
| 1327 | is_injective(partial_bijection(_,_)). | |
| 1328 | is_injective(iseq(_)). | |
| 1329 | is_injective(iseq1(_)). | |
| 1330 | ||
| 1331 | % A /<: B <=> A/<<: B & A /= B | |
| 1332 | ||
| 1333 | check_not_subset(Sub,Super,Hyps,not_subset_interval) :- % R..S /<: X..Y | |
| 1334 | is_interval(Sub,Hyps,R,S), | |
| 1335 | is_interval(Super,Hyps,X,Y),!, | |
| 1336 | check_not_subset_interval(R,S,X,Y,Hyps). | |
| 1337 | check_not_subset(A,B,Hyps,PT) :- | |
| 1338 | check_not_is_subset_strict(A,B,Hyps,PT),!, | |
| 1339 | check_not_equal(A,B,Hyps). | |
| 1340 | ||
| 1341 | check_not_subset_interval(R,S,X,Y,Hyps) :- | |
| 1342 | check_not_empty_interval(R,S,Hyps), !, % empty set is always a subset | |
| 1343 | (check_less(Y,S,Hyps) -> true % interval extends right beyond Y | |
| 1344 | ; check_less(R,X,Hyps) -> true % interval extends left beyond X | |
| 1345 | ). | |
| 1346 | ||
| 1347 | check_not_empty_interval(Low,Up,Hyps) :- check_leq(Low,Up,Hyps). | |
| 1348 | ||
| 1349 | % check_not_is_subset_strict(A,B,Hyps,PT) check if A is not a strict subset of B | |
| 1350 | % not really used for WD proofs at the moment; mainly as top-level goal in prove_po | |
| 1351 | % (now used for proving set_subtraction is not empty; test 2469) | |
| 1352 | % probably quite a few more rules necessary to make it useful | |
| 1353 | check_not_is_subset_strict(A,B,Hyps,hyp) :- | |
| 1354 | avl_fetch_from_hyps(not_subset_strict(A,B),Hyps),!. % hyp; currently not marked as useful by default! | |
| 1355 | check_not_is_subset_strict(A,B,Hyps,hyp2) :- | |
| 1356 | avl_fetch_from_hyps(not_subset(A,B),Hyps),!. % not(A <: B) => not (A<<:B) | |
| 1357 | check_not_is_subset_strict(A,B,Hyps,equal_not_subset_strict) :- | |
| 1358 | check_equal(A,B,Hyps,_),!. % A=B => not (A<<:B) | |
| 1359 | check_not_is_subset_strict(_,B,Hyps,empty_set(PT)) :- % A /<<: {} | |
| 1360 | check_equal_empty_set(B,Hyps,PT). | |
| 1361 | check_not_is_subset_strict(Sub,Super,Hyps,not_subset_interval) :- % R..S /<: X..Y => R..S /<<: X..Y | |
| 1362 | is_interval(Sub,Hyps,R,S), | |
| 1363 | is_interval(Super,Hyps,X,Y),!, | |
| 1364 | check_not_subset_interval(R,S,X,Y,Hyps). | |
| 1365 | check_not_is_subset_strict(MAX,_,Hyps,maximal_set) :- % MAX /<<: B | |
| 1366 | maximal_set(MAX,Hyps),!. | |
| 1367 | check_not_is_subset_strict(A,B,Hyps,not_empty_singleton(PT)) :- % x <<: {A} <=> x={} | |
| 1368 | singleton_set(B,_),!, | |
| 1369 | check_not_equal_empty_set(A,Hyps,PT). | |
| 1370 | check_not_is_subset_strict(A,B,Hyps,infinite_sub(PT)) :- | |
| 1371 | infinite_integer_set(A,Hyps), % TODO: accept more infinite sets | |
| 1372 | check_finite(B,Hyps,PT),!. | |
| 1373 | check_not_is_subset_strict(A,B,Hyps,superset_eq1(PT)) :- | |
| 1374 | (Operator = equal ; Operator = superset), % A :> S2 & S2 /<<: B => A /<<: B | |
| 1375 | avl_fetch_binop_from_hyps(A,Operator,Hyps,S2,Hyps2), | |
| 1376 | rewrite_local_loop_check(A,check_not_is_subset_strict,S2,Hyps2,Hyps3), | |
| 1377 | check_not_is_subset_strict(S2,B,Hyps3,PT),!. | |
| 1378 | check_not_is_subset_strict(A,B,Hyps,subset_eq2(PT)) :- | |
| 1379 | (Operator = equal ; Operator = subset), % B <: S2 & A /<<: S2 => A /<<: B | |
| 1380 | avl_fetch_binop_from_hyps(B,Operator,Hyps,S2,Hyps2), | |
| 1381 | rewrite_local_loop_check(B,check_not_is_subset_strict,S2,Hyps2,Hyps3), | |
| 1382 | check_not_is_subset_strict(A,S2,Hyps3,PT),!. | |
| 1383 | %check_not_is_subset_strict(A,B,H,_) :- print(check_not_is_subset_strict_failed(A,B)),nl, portray_hyps(H),nl,fail. | |
| 1384 | ||
| 1385 | ||
| 1386 | check_is_subset_strict(A,B,Hyp,empty_singleton(PT)) :- % x <<: {A} <=> x={} | |
| 1387 | singleton_set(B,_),!, | |
| 1388 | check_equal_empty_set(A,Hyp,PT). | |
| 1389 | check_is_subset_strict(A,B,Hyp,PT) :- % A <<: B <=> A <: B & A /= B | |
| 1390 | check_is_subset(A,B,Hyp,PT),!, | |
| 1391 | check_not_equal(A,B,Hyp). | |
| 1392 | ||
| 1393 | % check if something is a subset of something else | |
| 1394 | check_is_subset(H,H,_,equal). | |
| 1395 | check_is_subset(A,B,Hyps,hyp) :- | |
| 1396 | avl_fetch_from_hyps(subset(A,B),Hyps),!. % hyp | |
| 1397 | check_is_subset(_,MAX,Hyps,maximal_set) :- maximal_set(MAX,Hyps),!. | |
| 1398 | check_is_subset(S,_,Hyps,empty_set(PT)) :- check_equal_empty_set(S,Hyps,PT),!. % {} <: B | |
| 1399 | check_is_subset(cartesian_product(A,B),cartesian_product(A2,B2),Hyps,cart(PTA,PTB)) :- !, | |
| 1400 | % A <: A2 & B <: B2 => (A*B) <: (A2*B2) | |
| 1401 | (check_is_subset(A,A2,Hyps,PTA) | |
| 1402 | -> check_is_subset(B,B2,Hyps,PTB)). | |
| 1403 | check_is_subset('NATURAL1','NATURAL',_,nat1_nat) :- !. | |
| 1404 | check_is_subset(interval(L,U),B,Hyps,interval(PT)) :- !, check_subset_interval(B,L,U,Hyps,PT). | |
| 1405 | check_is_subset(intersection(A,B),Super,Hyps,intersection(PT)) :- !, | |
| 1406 | ( check_is_subset(A,Super,Hyps,PT) -> true ; check_is_subset(B,Super,Hyps,PT)). | |
| 1407 | check_is_subset(union(A,B),Super,Hyps,union(PTA,PTB)) :- !, | |
| 1408 | ( check_is_subset(A,Super,Hyps,PTA) -> check_is_subset(B,Super,Hyps,PTB)). | |
| 1409 | check_is_subset(domain_subtraction(_,B),Super,Hyps,dom_sub(PT)) :- !,check_is_subset(B,Super,Hyps,PT). | |
| 1410 | check_is_subset(domain_restriction(_,B),Super,Hyps,dom_res(PT)) :- !,check_is_subset(B,Super,Hyps,PT). | |
| 1411 | check_is_subset(range_subtraction(A,_),Super,Hyps,ran_sub(PT)) :- !,check_is_subset(A,Super,Hyps,PT). | |
| 1412 | check_is_subset(range_restriction(A,_),Super,Hyps,ran_res(PT)) :- !,check_is_subset(A,Super,Hyps,PT). | |
| 1413 | check_is_subset(set_subtraction(A,_),Super,Hyps,set_sub(PT)) :- !,check_is_subset(A,Super,Hyps,PT). | |
| 1414 | check_is_subset(value(avl_set(AVL)),B,Hyps,avl) :- !,check_subset_avl(B,AVL,Hyps). | |
| 1415 | check_is_subset(A,B,Hyps,subset_eq(PT)) :- | |
| 1416 | (Operator = equal ; Operator = subset), % for subset_strict we also have subset in Hyps | |
| 1417 | avl_fetch_binop_from_hyps(A,Operator,Hyps,S2,Hyps2), | |
| 1418 | rewrite_local_loop_check(A,check_is_subset,S2,Hyps2,Hyps3), | |
| 1419 | check_is_subset(S2,B,Hyps3,PT),!. | |
| 1420 | check_is_subset(A,B,Hyps,subset_eq_r(PT)) :- | |
| 1421 | avl_fetch_binop_from_hyps(B,equal,Hyps,S2,Hyps2), % also superset? | |
| 1422 | rewrite_local_loop_check(B,check_is_subset,S2,Hyps2,Hyps3), | |
| 1423 | check_is_subset(A,S2,Hyps3,PT),!. | |
| 1424 | check_is_subset('$'(ID),B,Hyps,eq(ID,PT)) :- | |
| 1425 | get_type_from_hyps('$'(ID),Hyps,Set,Hyps2), | |
| 1426 | extract_element_super_set_type(Set,Hyps2,S2), | |
| 1427 | rewrite_local_loop_check(ID,check_is_subset,S2,Hyps2,Hyps3), | |
| 1428 | check_is_subset(S2,B,Hyps3,PT),!. | |
| 1429 | check_is_subset(domain(Func),B,Hyps,domain(PT)) :- | |
| 1430 | get_domain_or_superset(Func,Hyps,DomFunc,Hyps2), | |
| 1431 | %rewrite_local_loop_check(domain(Func),check_is_subset,DomFunc,Hyps2,Hyps3), | |
| 1432 | check_is_subset(DomFunc,B,Hyps2,PT),!. | |
| 1433 | check_is_subset(range(Func),B,Hyps,range(PT)) :- | |
| 1434 | get_range_or_superset(Func,Hyps,RanFunc,Hyps2), | |
| 1435 | %rewrite_local_loop_check(range(Func),check_is_subset,RanFunc,Hyps2,Hyps3), | |
| 1436 | check_is_subset(RanFunc,B,Hyps2,PT),!. | |
| 1437 | check_is_subset(function(Func,_),B,Hyps,function_range(PT)) :- !, | |
| 1438 | get_range_or_superset(Func,Hyps,RanFunc,Hyps2), % f : _ +-> POW(Ran) & Ran <: B => f(.) <: B | |
| 1439 | subset_transitivity_rule(RanFunc,pow_subset(B),A2,B2), % extract pow_subset from Range | |
| 1440 | check_is_subset(A2,B2,Hyps2,PT). | |
| 1441 | check_is_subset(image(Func,_),B,Hyps,image(PT)) :- % or B=range(Range) | |
| 1442 | (B = range(FuncB),check_equal(Func,FuncB,Hyps,_) -> !, PT=range_of_same_func % f[.] <: ran(f) | |
| 1443 | ; get_range_or_superset(Func,Hyps,Range,Hyps2) -> !, check_is_subset(Range,B,Hyps2,PT)). | |
| 1444 | check_is_subset(A,B,Hyps,transitivity(PT)) :- subset_transitivity_rule(A,B,A2,B2), | |
| 1445 | !, % unary subset rules like POW(A2) <: POW(B2) if A2 <: B2 | |
| 1446 | check_is_subset(A2,B2,Hyps,PT). | |
| 1447 | check_is_subset(A,B,Hyps,transitivity(PT1,PT2)) :- subset_bin_transitivity_rule(A,B,A1,A2,B1,B2), | |
| 1448 | !, % binary subset rules like A1+->B1 <: A2+->B2 if A1 <:B1 & A2 <: B2 | |
| 1449 | (check_is_subset(A1,B1,Hyps,PT1) -> check_is_subset(A2,B2,Hyps,PT2)). | |
| 1450 | check_is_subset(sorted_set_extension(List),B,Hyps,PT) :- !, | |
| 1451 | check_is_subset(set_extension(List),B,Hyps,PT). | |
| 1452 | check_is_subset(set_extension(List),B,Hyps,set_extension) :- | |
| 1453 | simplify_expr(B,Hyps,BS), % simplify expression once | |
| 1454 | %portray_hyps(Hyps),nl, | |
| 1455 | l_check_is_member(List,BS,Hyps). | |
| 1456 | check_is_subset(Sub,union(A,B),Hyps,sub_union(PT)) :- !, | |
| 1457 | ( check_is_subset(Sub,A,Hyps,PT) -> true ; check_is_subset(Sub,B,Hyps,PT)). | |
| 1458 | % get_set_of_possible_values; treat sequence_extension | |
| 1459 | check_is_subset(CompSet,B,Hyps,comprehension_set(PT)) :- | |
| 1460 | is_comprehension_set(CompSet,[ID],Pred), | |
| 1461 | get_conjunct(Pred,Conjunct), % TODO: also allow comprehension sets with multiple ids? | |
| 1462 | get_member(Conjunct,ID,A), | |
| 1463 | % we could do findall and then union | |
| 1464 | ID = $(ID1), \+ occurs(A,ID1), | |
| 1465 | check_is_subset(A,B,Hyps,PT). | |
| 1466 | % check_is_subset(A,B,_,_) :- print(check_is_subset_failed(A,B)),nl,nl,fail. | |
| 1467 | ||
| 1468 | get_member(member(LHS,RHS),LHS,RHS). | |
| 1469 | get_member(subset(LHS,RHS),LHS,pow_subset(RHS)). | |
| 1470 | get_member(subset_strict(LHS,RHS),LHS,pow_subset(RHS)). | |
| 1471 | ||
| 1472 | ||
| 1473 | l_check_is_member([],_,_). | |
| 1474 | l_check_is_member([El|T],B,Hyps) :- | |
| 1475 | check_member_of_set(B,El,Hyps,_ProofTree),!, | |
| 1476 | l_check_is_member(T,B,Hyps). | |
| 1477 | ||
| 1478 | % extract set type of the elements of a set: x: POW(A) ==> x<:A | |
| 1479 | extract_element_super_set_type(FuncType,Hyps,cartesian_product(A,B)) :- | |
| 1480 | get_possible_domain_of_func_or_rel_type(FuncType,Hyps,A,_),!, | |
| 1481 | get_possible_range_of_func_or_rel_type_direct(FuncType,B,_). | |
| 1482 | extract_element_super_set_type(fin_subset(A),_,A). | |
| 1483 | extract_element_super_set_type(fin1_subset(A),_,A). | |
| 1484 | extract_element_super_set_type(pow_subset(A),_,A). | |
| 1485 | extract_element_super_set_type(pow1_subset(A),_,A). | |
| 1486 | ||
| 1487 | ||
| 1488 | % simple not member of set check | |
| 1489 | check_not_member_of_set(Set,_,Hyps,empty_set) :- check_equal_empty_set(Set,Hyps,_),!. | |
| 1490 | check_not_member_of_set(Set,El,Hyps,hyp) :- | |
| 1491 | avl_fetch_from_hyps(not_member(El,Set),Hyps),!. % hyp | |
| 1492 | check_not_member_of_set(if_then_else(Pred,A,B),El,Hyps,if_then_else(PTA,PTB)) :- | |
| 1493 | push_and_rename_normalized_hyp(Pred,Hyps,Hyps1), | |
| 1494 | (hyps_inconsistent(Hyps1) -> true ; check_not_member_of_set(A,El,Hyps1,PTA) -> true), | |
| 1495 | push_and_rename_normalized_hyp(negation(Pred),Hyps,Hyps2), | |
| 1496 | (hyps_inconsistent(Hyps2) -> true ; check_not_member_of_set(B,El,Hyps2,PTB) -> true),!. | |
| 1497 | check_not_member_of_set(intersection(A,B),El,Hyps,inter(PT)) :- | |
| 1498 | (check_not_member_of_set(A,El,Hyps,PT) -> true ; check_not_member_of_set(B,El,Hyps,PT)),!. | |
| 1499 | check_not_member_of_set(set_subtraction(A,B),El,Hyps,inter(PT)) :- | |
| 1500 | (check_not_member_of_set(A,El,Hyps,PT) -> true ; check_member_of_set(B,El,Hyps,PT)),!. | |
| 1501 | check_not_member_of_set(union(A,B),El,Hyps,inter(PTA,PTB)) :- | |
| 1502 | (check_not_member_of_set(A,El,Hyps,PTA) -> check_not_member_of_set(B,El,Hyps,PTB)),!. | |
| 1503 | check_not_member_of_set(overwrite(A,B),El,Hyps,overwrite(PTA,PTB)) :- | |
| 1504 | (check_not_member_of_set(A,El,Hyps,PTA) -> check_not_member_of_set(B,El,Hyps,PTB)),!. | |
| 1505 | check_not_member_of_set('NATURAL1',El,Hyps,nat1) :- | |
| 1506 | check_leq(El,0,Hyps). | |
| 1507 | check_not_member_of_set('NATURAL',El,Hyps,nat1) :- | |
| 1508 | check_leq(El,-1,Hyps). | |
| 1509 | check_not_member_of_set(interval(From,To),El,Hyps,interval) :- | |
| 1510 | (check_leq(El,minus(From,1),Hyps) -> true | |
| 1511 | ; check_leq(add(To,1),El,Hyps) -> true). % TODO: or interval empty | |
| 1512 | check_not_member_of_set(domain(Func),El,Hyps,not_in_domain(PT)) :- | |
| 1513 | check_not_member_of_domain(Func,El,Hyps,PT),!. | |
| 1514 | check_not_member_of_set(range(Func),El,Hyps,not_in_range(PT)) :- | |
| 1515 | check_not_member_of_range(Func,El,Hyps,PT),!. | |
| 1516 | check_not_member_of_set(relations(A,B),closure(RX),Hyps,closure1_not_el_relations(PT)) :- !, | |
| 1517 | % rx : A <-> B <=> closure1(rx) : A <-> B | |
| 1518 | check_not_member_of_set(relations(A,B),RX,Hyps,PT). | |
| 1519 | check_not_member_of_set(Set,couple(From,_),Hyps,not_in_dom(PT)) :- | |
| 1520 | % x /: dom(f) => x|->y /: f | |
| 1521 | avl_fetch_binop_from_hyps(From,not_member,Hyps,Set2,Hyps2), | |
| 1522 | check_is_subset(domain(Set),Set2,Hyps2,PT), | |
| 1523 | !. | |
| 1524 | check_not_member_of_set(Set,couple(_,To),Hyps,not_in_range) :- | |
| 1525 | avl_fetch_from_hyps(not_member(To,range(Set)),Hyps), % y /: ran(f) => x|->y /: f | |
| 1526 | !. % TODO: generalise this rule somewhat, see domain above | |
| 1527 | check_not_member_of_set(A,El,Hyps,eq(ProofTree)) :- | |
| 1528 | avl_fetch_worthwhile_equal_from_hyps(A,Hyps,Value,Hyps2), | |
| 1529 | rewrite_local_loop_check(A,check_member_of_set,Value,Hyps2,Hyps3), | |
| 1530 | check_not_member_of_set(Value,El,Hyps3,ProofTree). | |
| 1531 | check_not_member_of_set(Set,El,Hyps,not_in_set_extension) :- | |
| 1532 | is_set_extension(Set,List), | |
| 1533 | check_not_member_of_list(List,El,Hyps). | |
| 1534 | %check_not_member_of_set(Set,El,Hyps,_) :- print(not_mem_failed(Set,El)),nl,fail. | |
| 1535 | % TO DO: process equalities, set_extension?, value(avl_set(AVL)), ... | |
| 1536 | ||
| 1537 | % check if an element is not in the domain of a function | |
| 1538 | check_not_member_of_domain(domain_subtraction(DS,Func),El,Hyps,not_dom_sub(PT)) :- | |
| 1539 | (check_member_of_set(DS,El,Hyps,PT) -> true | |
| 1540 | ; check_not_member_of_domain(Func,El,Hyps,PT)). | |
| 1541 | check_not_member_of_domain(domain_restriction(DS,Func),El,Hyps,not_dom_sub(PT)) :- | |
| 1542 | (check_not_member_of_set(DS,El,Hyps,PT) -> true | |
| 1543 | ; check_not_member_of_domain(Func,El,Hyps,PT)). | |
| 1544 | check_not_member_of_domain(Func,El,Hyps,PT) :- | |
| 1545 | get_domain_or_superset(Func,Hyps,DomFunc,Hyps1), | |
| 1546 | check_not_member_of_set(DomFunc,El,Hyps1,PT). | |
| 1547 | ||
| 1548 | % check if an element is not in the domain of a function | |
| 1549 | check_not_member_of_range(range_subtraction(Func,DS),El,Hyps,not_dom_sub(PT)) :- | |
| 1550 | (check_member_of_set(DS,El,Hyps,PT) -> true | |
| 1551 | ; check_not_member_of_range(Func,El,Hyps,PT)). | |
| 1552 | check_not_member_of_range(range_restriction(Func,DS),El,Hyps,not_dom_sub(PT)) :- | |
| 1553 | (check_not_member_of_set(DS,El,Hyps,PT) -> true | |
| 1554 | ; check_not_member_of_range(Func,El,Hyps,PT)). | |
| 1555 | check_not_member_of_range(Func,El,Hyps,PT) :- | |
| 1556 | get_range_or_superset(Func,Hyps,RanFunc,Hyps1),!, | |
| 1557 | check_not_member_of_set(RanFunc,El,Hyps1,PT). | |
| 1558 | ||
| 1559 | ||
| 1560 | ||
| 1561 | % check that an element does not occur in a list of values/expressions | |
| 1562 | check_not_member_of_list([],_,_). | |
| 1563 | check_not_member_of_list([H|T],El,Hyps) :- | |
| 1564 | check_not_equal(H,El,Hyps), | |
| 1565 | check_not_member_of_list(T,El,Hyps). | |
| 1566 | ||
| 1567 | is_set_extension(set_extension(List),List). | |
| 1568 | is_set_extension(sorted_set_extension(List),List). | |
| 1569 | ||
| 1570 | ||
| 1571 | % check_member_of_set(Set,Element,Hyps,ProofTree) | |
| 1572 | % check_member_of_set(A,B,_H,_ProofTree) :- print(check_member_of_set(A,B)),nl,fail. | |
| 1573 | check_member_of_set(Set,_,Hyps,maximal_set) :- maximal_set(Set,Hyps), !. | |
| 1574 | check_member_of_set(Set,if_then_else(Pred,A,B),Hyps,if(P1,P2)) :- !, % if-then-else expression | |
| 1575 | push_and_rename_normalized_hyp(Pred,Hyps,Hyps1), | |
| 1576 | (hyps_inconsistent(Hyps1) -> true ; check_member_of_set(Set,A,Hyps1,P1) -> true), | |
| 1577 | push_and_rename_normalized_hyp(negation(Pred),Hyps,Hyps2), | |
| 1578 | (hyps_inconsistent(Hyps2) -> true ; check_member_of_set(Set,B,Hyps2,P2) -> true). | |
| 1579 | check_member_of_set(Set,El,Hyps,hyp) :- | |
| 1580 | % we could do avl_fetch_binop_from_hyps(El,member,Hyps,Set2,Hyps2), and check_subset(Set2,Set) | |
| 1581 | avl_fetch_from_hyps(member(El,Set),Hyps),!. % hyp | |
| 1582 | % TO DO: sometimes value(El) stored ! | |
| 1583 | check_member_of_set(sorted_set_extension(List),El,Hyps,PT) :- !, % ordsets:ord_member(El,List),!. | |
| 1584 | check_member_of_set(set_extension(List),El,Hyps,PT). | |
| 1585 | check_member_of_set(set_extension(List),El,Hyps,set_extension) :- member(El2,List), | |
| 1586 | check_equal(El,El2,Hyps,_),!. % TO DO: avoid multiple equality rewriting of El for long lists ? | |
| 1587 | check_member_of_set(partial_function(T1,T2),El,Hyps,partial_function(PT)) :- | |
| 1588 | check_is_partial_function_with_type(El,T1,T2,Hyps,PT). | |
| 1589 | check_member_of_set(total_function(T1,T2),El,Hyps,total_function(PT,PTDom)) :- | |
| 1590 | check_is_partial_function_with_type(El,T1,T2,Hyps,PT),!, | |
| 1591 | simplify_expr(domain(El),Hyps,DomEl), | |
| 1592 | check_is_subset(T1,DomEl,Hyps,PTDom). | |
| 1593 | check_member_of_set(relations(A,B),closure(RX),Hyps,closure1_el_relations(PT)) :- !, | |
| 1594 | % rx : A <-> B <=> closure1(rx) : A <-> B | |
| 1595 | check_member_of_set(relations(A,B),RX,Hyps,PT). | |
| 1596 | check_member_of_set(range(Func),El,Hyps,mem_range(PT)) :- | |
| 1597 | check_member_of_range(El,Func,Hyps,PT),!. % check before function application below, can do symbolic range check | |
| 1598 | check_member_of_set(image(Func,Set),El,Hyps,mem_range_for_image(PT0,PT1)) :- | |
| 1599 | % El:ran(F) & dom(F) <: S => El:F[S] | |
| 1600 | check_member_of_set(range(Func),El,Hyps,PT0),!, | |
| 1601 | check_is_subset(domain(Func),Set,Hyps,PT1). | |
| 1602 | check_member_of_set(A,ElFunc,Hyps,typing_membership(PT)) :- | |
| 1603 | get_type_from_hyps(ElFunc,Hyps,Range,Hyps2), % !, % moving cut later proves on additional PO for test 2039 | |
| 1604 | % e.g. f(.) : A if ran(f) <: Range & Range <: A | |
| 1605 | %rewrite_local_loop_check(A,check_member_of_set,Range,Hyps2,Hyps3), | |
| 1606 | check_is_subset(Range,A,Hyps2,PT),!. | |
| 1607 | check_member_of_set(A,El,Hyps,eq(ProofTree)) :- | |
| 1608 | avl_fetch_worthwhile_equal_from_hyps(A,Hyps,Value,Hyps2), | |
| 1609 | rewrite_local_loop_check(A,check_member_of_set,Value,Hyps2,Hyps3), | |
| 1610 | check_member_of_set(Value,El,Hyps3,ProofTree). | |
| 1611 | check_member_of_set(interval(L,U),El,Hyps,interval(PT)) :- !, check_in_interval(El,L,U,Hyps,PT). | |
| 1612 | check_member_of_set('NATURAL1',El,Hyps,nat1(PT)) :- !, check_subset_interval('NATURAL1',El,El,Hyps,PT). | |
| 1613 | check_member_of_set('NATURAL',El,Hyps,nat(PT)) :- !, check_subset_interval('NATURAL',El,El,Hyps,PT). | |
| 1614 | check_member_of_set(union(A,B),El,Hyps,union(PTA,PTB)) :- !, | |
| 1615 | (check_member_of_set(A,El,Hyps,PTA) -> true ; check_member_of_set(B,El,Hyps,PTB)). | |
| 1616 | check_member_of_set(intersection(A,B),El,Hyps,intersection(PTA,PTB)) :- !, | |
| 1617 | (check_member_of_set(A,El,Hyps,PTA) -> check_member_of_set(B,El,Hyps,PTB)). | |
| 1618 | check_member_of_set(set_subtraction(A,B),El,Hyps,set_subtraction(PTA,PTB)) :- !, | |
| 1619 | (check_member_of_set(A,El,Hyps,PTA) -> check_not_member_of_set(B,El,Hyps,PTB)). | |
| 1620 | check_member_of_set(pow_subset(T1),El,Hyps,pow(PT)) :- !, | |
| 1621 | check_is_subset(El,T1,Hyps,PT). | |
| 1622 | check_member_of_set(fin_subset(T1),El,Hyps,fin(PT1,PT2)) :- !, | |
| 1623 | check_is_subset(El,T1,Hyps,PT1),!, | |
| 1624 | check_finite(El,Hyps,PT2). | |
| 1625 | check_member_of_set(pow1_subset(T1),El,Hyps,pow1(PT)) :- !, | |
| 1626 | check_not_empty_set(El,Hyps),!, | |
| 1627 | check_is_subset(El,T1,Hyps,PT). | |
| 1628 | check_member_of_set(fin1_subset(T1),El,Hyps,fin1(PT1,PT2)) :- !, | |
| 1629 | check_not_empty_set(El,Hyps),!, | |
| 1630 | check_is_subset(El,T1,Hyps,PT1),!, | |
| 1631 | check_finite(El,Hyps,PT2). | |
| 1632 | check_member_of_set(seq(T1),El,Hyps,seq(PT)) :- !, | |
| 1633 | check_is_sequence(El,Hyps),!, | |
| 1634 | check_is_subset(range(El),T1,Hyps,PT). | |
| 1635 | check_member_of_set(seq1(T1),El,Hyps,seq1(PT)) :- !, | |
| 1636 | check_is_non_empty_sequence(El,Hyps),!, | |
| 1637 | check_is_subset(range(El),T1,Hyps,PT). | |
| 1638 | check_member_of_set(cartesian_product(T1,T2),couple(El1,El2),Hyps,cart(PT1,PT2)) :- !, | |
| 1639 | check_member_of_set(T1,El1,Hyps,PT1),!, | |
| 1640 | check_member_of_set(T2,El2,Hyps,PT2). | |
| 1641 | check_member_of_set(value(avl_set(AVL)),El,Hyps,PT) :- | |
| 1642 | (avl_can_fetch(El,BVal) -> !,PT=avl_fetch(El),avl_fetch(BVal,AVL) | |
| 1643 | ; avl_is_interval(AVL,Min,Max) -> !, PT=avl_interval(PT2), | |
| 1644 | % useful is El is not a number, but e.g. an arithmetic expression | |
| 1645 | % print(avl_interval(Min,Max,El)),nl, | |
| 1646 | check_integer(El,check_member_of_set_avl_interval), | |
| 1647 | check_in_interval(El,Min,Max,Hyps,PT2) | |
| 1648 | ). | |
| 1649 | check_member_of_set(A,El,Hyps,rewrite(PT)) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!, | |
| 1650 | check_member_of_set(A2,El,Hyps2,PT). | |
| 1651 | check_member_of_set(domain(Func),Index,Hyps,mem_domain(PT)) :- | |
| 1652 | check_member_of_domain(Index,Func,Hyps,PT),!. | |
| 1653 | check_member_of_set(Set,X,Hyps,value_set(PT)) :- | |
| 1654 | try_get_set_of_possible_values(X,Hyps,XSet,Hyps2), % also covers min(Set), max(Set), mu(Set), CHOOSE(Set) | |
| 1655 | check_is_subset(XSet,Set,Hyps2,PT),!. | |
| 1656 | %check_member_of_set(Set,X,Hyps,eq(PT)) :- Set = '$'(_), | |
| 1657 | % avl_fetch_equal_from_hyps(Set,Hyps,Set2,Hyps2), % maybe perform direct rewrite ancestor cycle check here | |
| 1658 | % check_member_of_set(Set2,X,Hyps2,PT),!. | |
| 1659 | check_member_of_set(Set,X,Hyps,trans(PT)) :- | |
| 1660 | avl_fetch_binop_from_hyps(Set,superset,Hyps,SubSet,Hyps2), % X:B & B <: A => X:A | |
| 1661 | check_member_of_set(SubSet,X,Hyps2,PT),!. | |
| 1662 | check_member_of_set(Set,ID,Hyps,member_subset(PT)) :- | |
| 1663 | avl_fetch_worthwhile_member_from_hyps(ID,Hyps,SubSet,Hyps2), %write(sub(ID,SubSet,Set)),nl, | |
| 1664 | check_is_subset(SubSet,Set,Hyps2,PT). | |
| 1665 | %check_member_of_set(A,B,_H,_ProofTree) :- write(check_member_of_set_failed(A,B)),nl,fail. | |
| 1666 | ||
| 1667 | ||
| 1668 | :- use_module(probsrc(kernel_reals),[construct_real/2]). | |
| 1669 | % check if we can fetch an expression as a B value (second arg) in an AVL set | |
| 1670 | avl_can_fetch(El,Res) :- number(El),!, Res=int(El). | |
| 1671 | avl_can_fetch(boolean_true,pred_true). | |
| 1672 | avl_can_fetch(boolean_false,pred_false). | |
| 1673 | avl_can_fetch(real(Atom),R) :- construct_real(Atom,R). | |
| 1674 | avl_can_fetch(string(S),string(S)) :- ground(S). | |
| 1675 | avl_can_fetch(couple(A,B),(VA,VB)) :- avl_can_fetch(A,VA), avl_can_fetch(B,VB). | |
| 1676 | ||
| 1677 | check_member_of_domain(El,reverse(Func2),Hyps,reverse(PT)) :- !, | |
| 1678 | check_member_of_range(El,Func2,Hyps,PT). | |
| 1679 | check_member_of_domain(El,Func,Hyps,hyp) :- | |
| 1680 | avl_fetch_from_hyps(member(El,domain(Func)),Hyps),!. % hyp, already checked in check_member_of_set | |
| 1681 | check_member_of_domain(Index,Func,Hyps,size_in_dom_seq) :- % x:seq1(T) => size(x) : dom(x) | |
| 1682 | index_in_non_empty_sequence(Index,Func,Hyps), | |
| 1683 | check_is_non_empty_sequence(Func,Hyps),!. | |
| 1684 | % TO DO: f~(x) : dom(f) ?? | |
| 1685 | check_member_of_domain(El,union(A,B),Hyps,dom_of_union(PT)) :- | |
| 1686 | check_member_of_union(domain(A),domain(B),El,Hyps,PT). | |
| 1687 | check_member_of_domain(El,overwrite(A,B),Hyps,dom_of_overwrite(PT)) :- | |
| 1688 | check_member_of_union(domain(A),domain(B),El,Hyps,PT). | |
| 1689 | check_member_of_domain(El,direct_product(A,B),Hyps,dom_of_direct_product(PT)) :- % dom(A >< B) = dom(A) /\ dom (B) | |
| 1690 | check_member_of_set(domain(A),El,Hyps,PT), | |
| 1691 | check_member_of_set(domain(B),El,Hyps,PT). | |
| 1692 | check_member_of_domain(El,A,Hyps,rewrite(PT)) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!, | |
| 1693 | check_member_of_domain(El,A2,Hyps2,PT). | |
| 1694 | check_member_of_domain(El,Func,Hyps,dom_of_subset(PT)) :- % Func2 <: Func & El:dom(Func2) => El:dom(Func) | |
| 1695 | % counter part of rule with superset for check_member_of_set | |
| 1696 | (Op = equal ; Op = superset), | |
| 1697 | avl_fetch_binop_from_hyps(Func,Op,Hyps,Func2,Hyps1), | |
| 1698 | rewrite_local_loop_check(Func,check_member_of_domain,Func2,Hyps1,Hyps2), | |
| 1699 | check_member_of_set(domain(Func2),El,Hyps2,PT). | |
| 1700 | check_member_of_domain(El,comprehension_set(IDS,Body),Hyps,dom_of_lambda(PTs)) :- | |
| 1701 | get_lambda_args_and_body(IDS,Body,_,_,Args,RestBodyList), | |
| 1702 | %nl,print(lambda(Args,El,RestBodyList)),nl, | |
| 1703 | generate_funapp_binding(Args,El,Subst), | |
| 1704 | % we rename the local variables of the comprehension set; no need to call add_new_hyp_any_vars | |
| 1705 | l_rename_and_prove_goals(RestBodyList,Subst,Hyps,PTs). | |
| 1706 | check_member_of_domain(El,restrict_front(_,K),Hyps,dom_of_restrict_front(PT)) :- | |
| 1707 | check_member_of_set(interval(1,K),El,Hyps,PT). % WD Condition requires K : 0..size(Seq) | |
| 1708 | check_member_of_domain(El,if_then_else(Pred,A,B),Hyps,if_then_else(PT1,PT2)) :- | |
| 1709 | push_and_rename_normalized_hyp(Pred,Hyps,Hyps1), | |
| 1710 | (hyps_inconsistent(Hyps1) -> true ; check_member_of_domain(El,A,Hyps1,PT1) -> true), | |
| 1711 | push_and_rename_normalized_hyp(negation(Pred),Hyps,Hyps2), | |
| 1712 | (hyps_inconsistent(Hyps2) -> true ; check_member_of_domain(El,B,Hyps2,PT2) -> true). | |
| 1713 | %check_member_of_domain(Index,Func,Hyps,_) :- write(check_member_of_domain_failed(Index,Func)),nl,fail. | |
| 1714 | ||
| 1715 | % we could do intersection, subtraction | |
| 1716 | ||
| 1717 | % check if an element is an element of a union of two sets | |
| 1718 | check_member_of_union(Set1,_,El,Hyps,PT) :- check_member_of_set(Set1,El,Hyps,PT),!. | |
| 1719 | check_member_of_union(_,Set2,El,Hyps,PT) :- check_member_of_set(Set2,El,Hyps,PT),!. | |
| 1720 | check_member_of_union(Set1,Set2,El,Hyps,union(PT1,PT2)) :- | |
| 1721 | % x : A \/ B & A <: S1 & B <: S2 => x : S1 \/ S2 | |
| 1722 | avl_fetch_mem_from_hyps(El,Hyps,union(A,B),Hyps2), % TO DO: other conditions ? | |
| 1723 | (check_is_subset(A,Set1,Hyps2,PT1) -> check_is_subset(B,Set2,Hyps2,PT2) | |
| 1724 | ; check_is_subset(A,Set2,Hyps2,PT1) -> check_is_subset(B,Set1,Hyps2,PT2)). | |
| 1725 | ||
| 1726 | generate_funapp_binding(['$'(X)],El,[rename(X,El)]). | |
| 1727 | generate_funapp_binding(['$'(X),'$'(Y)],couple(El1,El2),[rename(X,El1),rename(Y,El2)]). | |
| 1728 | generate_funapp_binding(['$'(X),'$'(Y),'$'(Z)],couple(couple(El1,El2),El3),[rename(X,El1),rename(Y,El2),rename(Z,El3)]). | |
| 1729 | % TO DO: create substitution for more arguments and other parameters | |
| 1730 | ||
| 1731 | ||
| 1732 | check_member_of_range(El,reverse(Func2),Hyps,reverse(PT)) :- !,check_member_of_domain(El,Func2,Hyps,PT). | |
| 1733 | check_member_of_range(El,Func,Hyps,hyp) :- | |
| 1734 | avl_fetch_from_hyps(member(El,range(Func)),Hyps),!. % hyp, already checked in check_member_of_set | |
| 1735 | check_member_of_range(El,A,Hyps,rewrite(PT)) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!, | |
| 1736 | check_member_of_range(El,A2,Hyps2,PT). | |
| 1737 | check_member_of_range('$'(ID),Func2,Hyps,PT) :- | |
| 1738 | avl_fetch_worthwhile_equal_from_hyps('$'(ID),Hyps,Value,Hyps2), | |
| 1739 | check_member_of_range(Value,Func2,Hyps2,PT). | |
| 1740 | check_member_of_range(function(Func1,_),Func2,Hyps,func_app_in_range) :- % f(.) : ran(f) | |
| 1741 | check_equal(Func1,Func2,Hyps,_). | |
| 1742 | check_member_of_range(El,if_then_else(Pred,A,B),Hyps,if_then_else(PT1,PT2)) :- | |
| 1743 | push_and_rename_normalized_hyp(Pred,Hyps,Hyps1), | |
| 1744 | (hyps_inconsistent(Hyps1) -> true ; check_member_of_range(El,A,Hyps1,PT1) -> true), | |
| 1745 | push_and_rename_normalized_hyp(negation(Pred),Hyps,Hyps2), | |
| 1746 | (hyps_inconsistent(Hyps2) -> true ; check_member_of_range(El,B,Hyps2,PT2) -> true). | |
| 1747 | ||
| 1748 | ||
| 1749 | % subset transitivity for unary operators: | |
| 1750 | subset_transitivity_rule(pow_subset(A),pow_subset(B),A,B). | |
| 1751 | ||
| 1752 | subset_transitivity_rule(pow1_subset(A),pow1_subset(B),A,B). | |
| 1753 | subset_transitivity_rule(pow1_subset(A),pow_subset(B),A,B). | |
| 1754 | ||
| 1755 | subset_transitivity_rule(fin_subset(A),fin_subset(B),A,B). | |
| 1756 | subset_transitivity_rule(fin_subset(A),pow_subset(B),A,B). | |
| 1757 | ||
| 1758 | subset_transitivity_rule(fin1_subset(A),fin1_subset(B),A,B). | |
| 1759 | subset_transitivity_rule(fin1_subset(A),fin_subset(B),A,B). | |
| 1760 | subset_transitivity_rule(fin1_subset(A),pow1_subset(B),A,B). | |
| 1761 | subset_transitivity_rule(fin1_subset(A),pow_subset(B),A,B). | |
| 1762 | ||
| 1763 | subset_transitivity_rule(seq(A),seq(B),A,B). | |
| 1764 | subset_transitivity_rule(seq(A),partial_function(typeset,B),A,B). | |
| 1765 | ||
| 1766 | subset_transitivity_rule(seq1(A),seq1(B),A,B). | |
| 1767 | subset_transitivity_rule(seq1(A),seq(B),A,B). | |
| 1768 | subset_transitivity_rule(seq1(A),partial_function(typeset,B),A,B). | |
| 1769 | ||
| 1770 | subset_transitivity_rule(iseq(A),iseq(B),A,B). | |
| 1771 | subset_transitivity_rule(iseq(A),seq(B),A,B). | |
| 1772 | subset_transitivity_rule(iseq(A),partial_function(typeset,B),A,B). | |
| 1773 | ||
| 1774 | subset_transitivity_rule(iseq1(A),iseq1(B),A,B). | |
| 1775 | subset_transitivity_rule(iseq1(A),iseq(B),A,B). | |
| 1776 | subset_transitivity_rule(iseq1(A),seq1(B),A,B). | |
| 1777 | subset_transitivity_rule(iseq1(A),seq(B),A,B). | |
| 1778 | subset_transitivity_rule(iseq1(A),partial_function(typeset,B),A,B). | |
| 1779 | ||
| 1780 | % subset_transitivity_rule(perm(A),perm(B),A,B). % this does not hold perm({}) = { [] }, perm({TRUE}) = {[TRUE]} | |
| 1781 | subset_transitivity_rule(perm(A),iseq(B),A,B). | |
| 1782 | subset_transitivity_rule(perm(A),seq(B),A,B). | |
| 1783 | subset_transitivity_rule(perm(A),partial_function(typeset,B),A,B). | |
| 1784 | ||
| 1785 | ||
| 1786 | subset_transitivity_rule(range(A),domain(reverse(B)),A,B). | |
| 1787 | subset_transitivity_rule(range(A),range(B),A,B). | |
| 1788 | subset_transitivity_rule(range(reverse(A)),domain(B),A,B). | |
| 1789 | subset_transitivity_rule(domain(reverse(A)),range(B),A,B). | |
| 1790 | subset_transitivity_rule(domain(A),domain(B),A,B). % dom(A) <: dom(B) if A <:B | |
| 1791 | subset_transitivity_rule(domain(A),range(reverse(B)),A,B). | |
| 1792 | subset_transitivity_rule(reverse(A),reverse(B),A,B). | |
| 1793 | subset_transitivity_rule(rev(A),rev(B),A,B). | |
| 1794 | subset_transitivity_rule(identity(A),identity(B),A,B). | |
| 1795 | ||
| 1796 | % TO DO: add rules for more binary operators, like surjective relations, ... | |
| 1797 | subset_bin_transitivity_rule(relations(A1,A2),relations(B1,B2),A1,A2,B1,B2). % <-> | |
| 1798 | subset_bin_transitivity_rule(total_relation(A1,A2),relations(B1,B2),A1,A2,B1,B2). % <<-> | |
| 1799 | subset_bin_transitivity_rule(total_relation(A1,A2),total_relation(B1,B2),A1,A2,B1,B2) :- A1=B1. | |
| 1800 | subset_bin_transitivity_rule(partial_function(A1,A2),relations(B1,B2),A1,A2,B1,B2). % +-> | |
| 1801 | subset_bin_transitivity_rule(partial_function(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). | |
| 1802 | subset_bin_transitivity_rule(partial_injection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % >+> | |
| 1803 | subset_bin_transitivity_rule(partial_injection(A1,A2),partial_injection(B1,B2),A1,A2,B1,B2). | |
| 1804 | subset_bin_transitivity_rule(partial_surjection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % -+>> | |
| 1805 | subset_bin_transitivity_rule(partial_surjection(A1,A2),partial_surjection(B1,B2),A1,A2,B1,B2) :- A2=B2. | |
| 1806 | subset_bin_transitivity_rule(partial_bijection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % >+>> | |
| 1807 | subset_bin_transitivity_rule(total_function(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % --> | |
| 1808 | subset_bin_transitivity_rule(total_function(A1,A2),total_function(B1,B2),A1,A2,B1,B2) :- A1=B1. | |
| 1809 | subset_bin_transitivity_rule(total_injection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % >-> | |
| 1810 | subset_bin_transitivity_rule(total_injection(A1,A2),total_function(B1,B2),A1,A2,B1,B2) :- A1=B1. | |
| 1811 | subset_bin_transitivity_rule(total_surjection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % -->> | |
| 1812 | subset_bin_transitivity_rule(total_surjection(A1,A2),total_function(B1,B2),A1,A2,B1,B2) :- A1=B1. | |
| 1813 | subset_bin_transitivity_rule(total_bijection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % >+>> | |
| 1814 | subset_bin_transitivity_rule(total_bijection(A1,A2),partial_injection(B1,B2),A1,A2,B1,B2). | |
| 1815 | subset_bin_transitivity_rule(total_bijection(A1,A2),partial_surjection(B1,B2),A1,A2,B1,B2) :- A2=B2. | |
| 1816 | subset_bin_transitivity_rule(total_bijection(A1,A2),total_function(B1,B2),A1,A2,B1,B2) :- A1=B1. | |
| 1817 | subset_bin_transitivity_rule(total_bijection(A1,A2),total_injection(B1,B2),A1,A2,B1,B2) :- A1=B1. | |
| 1818 | subset_bin_transitivity_rule(total_bijection(A1,A2),total_surjection(B1,B2),A1,A2,B1,B2) :- A1=B1, A2=B2. | |
| 1819 | subset_bin_transitivity_rule(image(A1,A2),image(B1,B2),A1,A2,B1,B2). % A1[A2] <: B1[B2] if A1 <: B1 & A2 <: B2 | |
| 1820 | subset_bin_transitivity_rule(domain_restriction(A1,A2),domain_restriction(B1,B2),A1,A2,B1,B2). % A1 <| A2 <: B1 <| B2 if A1 <: B1 & A2 <: B2 | |
| 1821 | subset_bin_transitivity_rule(range_restriction(A1,A2),range_restriction(B1,B2),A1,A2,B1,B2). | |
| 1822 | subset_bin_transitivity_rule(domain_subtraction(A1,A2),domain_subtraction(B1,B2),B1,A2,A1,B2). % A1 <<| A2 <: B1 <<| B2 if B1 <: A1 & A2 <: B2 | |
| 1823 | subset_bin_transitivity_rule(range_subtraction(A1,A2),range_subtraction(B1,B2),A1,B2,A2,B1). % A1 |>> A2 <: B1|>> B2 if A1 <: B1 & B2 <: A2 | |
| 1824 | %subset_bin_transitivity_rule(A,B,A1,A2,B1,B2) :- write(subset_bin_transitivity_rule(A,B,A1,A2,B1,B2)),nl,fail. | |
| 1825 | % TO DO: add more | |
| 1826 | ||
| 1827 | % TO DO: instead of is_set_of_sequences_type | |
| 1828 | %subset_mixed_transitivity_rule(total_function(A1,A2),seq(B2),A2,B2) :- is_interval(A1). | |
| 1829 | ||
| 1830 | check_in_interval(El,Min,Max,Hyps,in_interval(PT1,PT2)) :- | |
| 1831 | expr_is_member_of_set(El,Set,PT1),!, % TODO: should we treat min/max as well here?? | |
| 1832 | check_is_subset(Set,interval(Min,Max),Hyps,PT2). | |
| 1833 | check_in_interval(El,Min,Max,Hyps,PT) :- | |
| 1834 | check_subset_interval(interval(Min,Max),El,El,Hyps,PT). % calls check_sub_intervals(Min,Max,El,El,Hyps) | |
| 1835 | ||
| 1836 | expr_is_member_of_set(mu(Set),Set,mu). | |
| 1837 | expr_is_member_of_set(external_function_call(Call,[Set]),Set,ext_call(Call)) :- | |
| 1838 | (Call = 'CHOOSE' -> true ; Call = 'MU'). | |
| 1839 | ||
| 1840 | % check if an interval is a subset of the first argument | |
| 1841 | check_subset_interval(union(A,B),L1,U1,Hyps,union(PT)) :- !, | |
| 1842 | % TO DO: try and merge A,B : union(interval(1,10),set_extension([11])) | |
| 1843 | (check_subset_interval(A,L1,U1,Hyps,PT) -> true ; check_subset_interval(B,L1,U1,Hyps,PT)). | |
| 1844 | check_subset_interval(sorted_set_extension(L),L1,U1,Hyps,PT) :- !, | |
| 1845 | check_subset_interval(set_extension(L),L1,U1,Hyps,PT). | |
| 1846 | check_subset_interval(set_extension(L),L1,U1,Hyps,set_extension(Nr)) :- !, | |
| 1847 | % TO DO: maybe merge L into an interval | |
| 1848 | nth1(Nr,L,El), check_sub_intervals(L1,U1,El,El,Hyps),!. | |
| 1849 | check_subset_interval(intersection(A,B),L1,U1,Hyps,inter(PTA,PTB)) :- !, | |
| 1850 | % L1..U1 <: A /\ B if L1..U1 <: A & L1..U1 <: B | |
| 1851 | (check_subset_interval(A,L1,U1,Hyps,PTA) -> check_subset_interval(B,L1,U1,Hyps,PTB)). | |
| 1852 | check_subset_interval(interval(L2,U2),L1,U1,Hyps,interval) :- | |
| 1853 | !,check_sub_intervals(L1,U1,L2,U2,Hyps). | |
| 1854 | check_subset_interval('NATURAL',L1,_,Hyps,nat) :- !, check_leq(0,L1,Hyps). | |
| 1855 | check_subset_interval('NATURAL1',L1,_,Hyps,nat1) :- !, check_leq(1,L1,Hyps). | |
| 1856 | check_subset_interval(value(avl_set(A)),L1,U1,Hyps,avl(PT)) :- !, | |
| 1857 | (number(L1), number(U1) | |
| 1858 | -> PT=in(L1,U1), | |
| 1859 | check_interval_in_custom_set(L1,U1,avl_set(A),no_wf_available) | |
| 1860 | ; avl_min(A,int(L2)), avl_max(A,int(U2)), PT=min_max(L2,U2,PT2), | |
| 1861 | check_subset_interval(interval(L2,U2),L1,U1,Hyps,PT2) | |
| 1862 | ). | |
| 1863 | check_subset_interval(A,L1,U1,Hyps,rewrite(PT)) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!, | |
| 1864 | check_subset_interval(A2,L1,U1,Hyps2,PT). | |
| 1865 | check_subset_interval(domain(Expr),Low,Up,Hyps,dom_seq1) :- % a special rule when using SEQ(1) rather than first(SEQ) | |
| 1866 | (check_leq(1,Low,Hyps), check_leq(Up,size(Expr),Hyps) % 1..size(s) <: dom(s) | |
| 1867 | -> check_is_sequence(Expr,Hyps) | |
| 1868 | ; index_in_non_empty_sequence(Low,Expr,Hyps), | |
| 1869 | index_in_non_empty_sequence(Up,Expr,Hyps) % 1..1 or size(s)..size(s) <: dom(s) if s:seq1(.) | |
| 1870 | -> check_is_non_empty_sequence(Expr,Hyps) | |
| 1871 | ). | |
| 1872 | check_subset_interval(range(reverse(Expr)),Low,Up,Hyps,PT) :- !, | |
| 1873 | check_subset_interval(domain(Expr),Low,Up,Hyps,PT). | |
| 1874 | check_subset_interval(A,Low,Up,Hyps,eq(PT)) :- | |
| 1875 | avl_fetch_worthwhile_equal_from_hyps(A,Hyps,A2,Hyps2), | |
| 1876 | rewrite_local_loop_check(A,check_subset_interval,A2,Hyps2,Hyps3), | |
| 1877 | check_subset_interval(A2,Low,Up,Hyps3,PT). | |
| 1878 | %check_subset_interval(A,L1,U1,_,_) :- print(check_subset_interval_failed(A,L1,U1)),nl,fail. | |
| 1879 | ||
| 1880 | % s:seq1(.) => 1:dom(s) & size(s):dom(s) | |
| 1881 | index_in_non_empty_sequence(1,_,_). | |
| 1882 | index_in_non_empty_sequence(card(E),E,_). | |
| 1883 | index_in_non_empty_sequence(size(E),E,_). | |
| 1884 | index_in_non_empty_sequence('$'(X),E,Hyps) :- | |
| 1885 | avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2), | |
| 1886 | rewrite_local_loop_check(X,index_in_non_empty_sequence,Y,Hyps2,Hyps3), | |
| 1887 | index_in_non_empty_sequence(Y,E,Hyps3). | |
| 1888 | index_in_non_empty_sequence(X,E,Hyps) :- \+ useful_value(X), % do not rewrite 10 to interval(10,10) | |
| 1889 | try_get_set_of_possible_values(X,Hyps,XSet,Hyps2), | |
| 1890 | rewrite_local_loop_check(X,index_in_non_empty_sequence,XSet,Hyps2,Hyps3), | |
| 1891 | all_in_non_empty_sequence(XSet,E,Hyps3). | |
| 1892 | ||
| 1893 | all_in_non_empty_sequence(interval(A,B),E,Hyps) :- | |
| 1894 | index_in_non_empty_sequence(A,E,Hyps), | |
| 1895 | index_in_non_empty_sequence(B,E,Hyps). | |
| 1896 | % TODO: avl_set, ... | |
| 1897 | ||
| 1898 | % check if L1..U1 <: L2..U2 | |
| 1899 | check_sub_intervals(L1,L1,L2,U2,Hyps) :- (L1=L2 ; L1=U2),!, | |
| 1900 | check_not_empty_set(interval(L2,U2),Hyps). | |
| 1901 | check_sub_intervals(L1,U1,L2,U2,Hyps) :- % L1..U1 <: L2..U2 if L2 <= L1 & U1 <= U2 | |
| 1902 | check_leq(L2,L1,Hyps),!, | |
| 1903 | check_leq(U1,U2,Hyps). | |
| 1904 | ||
| 1905 | ||
| 1906 | ||
| 1907 | % some exact rewrite steps | |
| 1908 | rewrite_set_expression_exact(domain(A),Hyps,Res,Hyps2) :- compute_exact_domain(A,Hyps,Dom,Hyps2),!, | |
| 1909 | %print(rewrote(domain(A))),nl, print(Dom),nl, | |
| 1910 | (A='$'(ID) -> not_occurs(Dom,ID) ; true), % prevent silly rewrites | |
| 1911 | Res=Dom. | |
| 1912 | rewrite_set_expression_exact(range(A),Hyps,Res,Hyps2) :- compute_exact_range(A,Hyps,Ran,Hyps2),!, | |
| 1913 | %print(rewrote(range(A))),nl, print(Ran),nl, | |
| 1914 | (A='$'(ID) -> not_occurs(Ran,ID) ; true), % prevent silly rewrites | |
| 1915 | Res=Ran. | |
| 1916 | rewrite_set_expression_exact(intersection(A,B),Hyps,Res,Hyps) :- | |
| 1917 | (is_empty_set_direct(A) -> Res=empty_set ; is_empty_set_direct(B) -> Res=empty_set). | |
| 1918 | rewrite_set_expression_exact(set_subtraction(A,B),Hyps,Res,Hyps) :- | |
| 1919 | (is_empty_set_direct(A) -> Res=empty_set ; is_empty_set_direct(B) -> Res=A). | |
| 1920 | rewrite_set_expression_exact(union(A,B),Hyps,Res,Hyps1) :- | |
| 1921 | (check_equal(A,B,Hyps,Hyps1) -> Res=A | |
| 1922 | ; Hyps1=Hyps, merge_set_extensions(union(A,B),List,[]), | |
| 1923 | construct_set_extension(List,Hyps,Res)). | |
| 1924 | rewrite_set_expression_exact(value(closure(P,T,B)),Hyps,Res,Hyps) :- nonvar(P), | |
| 1925 | is_normed_interval_closure(P,T,B,LOW,UP), number(LOW),number(UP),!, | |
| 1926 | Res = interval(LOW,UP). | |
| 1927 | rewrite_set_expression_exact(assertion_expression(_,_,Expr),Hyps,Res,Hyps2) :- % TO DO: add Predicate to Hyps ? | |
| 1928 | (rewrite_set_expression_exact(Expr,Hyps,Expr2,Hyps2) -> Res=Expr2 | |
| 1929 | ; Res=Expr, Hyps2=Hyps). | |
| 1930 | rewrite_set_expression_exact(Expr,Hyps,Res,Hyps) :- | |
| 1931 | eval_bvalue_from_norm_expr(Expr,Val,Hyps),!, Res=value(Val). | |
| 1932 | % Note one can have equalities like f = f~~ (in FunLawsWithLambda.mch); hence important to pass Hyps for cycle detection | |
| 1933 | ||
| 1934 | :- use_module(probsrc(custom_explicit_sets),[is_interval_closure/5]). | |
| 1935 | is_normed_interval_closure([P],[integer],B,LOW,UP) :- | |
| 1936 | B = member(P,interval(LOW,UP)). % norm_value(closure(P,T,B),R) -> normalises some values | |
| 1937 | is_normed_interval_closure(P,T,B,LOW,UP) :- % relevant for test 2039 | |
| 1938 | is_interval_closure(P,T,B,LOW,UP). % some values are computed here explicitly, without being normalised | |
| 1939 | ||
| 1940 | % rewrite relational image operator; not used | |
| 1941 | %rewrite_rel_image(Rel,Set,Hyps,value(ResVal),Hyps) :- | |
| 1942 | % get_bvalue_from_norm_expr(Rel,RelVal,Hyps), !, get_bvalue_from_norm_expr(Set,SetVal,Hyps), !, | |
| 1943 | % eval_binary_operator(image,RelVal,SetVal,ResVal). | |
| 1944 | ||
| 1945 | ||
| 1946 | eval_unary_operator(reverse,Arg,Res) :- bsets_clp:invert_relation_wf(Arg,Res,no_wf_available). | |
| 1947 | eval_binary_operator(image,RelVal,SetVal,Res) :- bsets_clp:image_wf(RelVal,SetVal,Res,no_wf_available). | |
| 1948 | ||
| 1949 | :- use_module(probsrc(custom_explicit_sets),[construct_interval_closure/3]). | |
| 1950 | % try and convert a normed AST expression to a valid B value | |
| 1951 | get_bvalue_from_norm_expr(boolean_true,pred_true,_). | |
| 1952 | get_bvalue_from_norm_expr(boolean_false,pred_false,_). | |
| 1953 | get_bvalue_from_norm_expr(Nr,int(Nr),_) :- integer(Nr). | |
| 1954 | get_bvalue_from_norm_expr(value(V),V,_) :- !, value_can_be_computed(V). | |
| 1955 | get_bvalue_from_norm_expr(set_extension(List),Result,Hyps) :- !, l_get_bvalue_from_norm_expr(List,Result,Hyps). | |
| 1956 | get_bvalue_from_norm_expr(sorted_set_extension(List),Result,Hyps) :- !, l_get_bvalue_from_norm_expr(List,Result,Hyps). | |
| 1957 | get_bvalue_from_norm_expr(interval(Low,Up),Result,_) :- !, | |
| 1958 | number(Low),number(Up), construct_interval_closure(Low,Up,Result). | |
| 1959 | get_bvalue_from_norm_expr('$'(ID),Res,Hyps) :- !, | |
| 1960 | avl_fetch_equal_from_hyps('$'(ID),Hyps,E2,_Hyps1), E2 \= '$'(_), | |
| 1961 | get_bvalue_from_norm_expr(E2,Res,Hyps). | |
| 1962 | get_bvalue_from_norm_expr(Expr,Res,Hyps) :- eval_bvalue_from_norm_expr(Expr,Res,Hyps). | |
| 1963 | ||
| 1964 | l_get_bvalue_from_norm_expr([],[],_). | |
| 1965 | l_get_bvalue_from_norm_expr([H|T],[R|TR],Hyps) :- get_bvalue_from_norm_expr(H,R,Hyps), | |
| 1966 | l_get_bvalue_from_norm_expr(T,TR,Hyps). | |
| 1967 | ||
| 1968 | eval_bvalue_from_norm_expr(reverse(Rel),ResVal,Hyps) :- get_bvalue_from_norm_expr(Rel,RelVal,Hyps), | |
| 1969 | eval_unary_operator(reverse,RelVal,ResVal). | |
| 1970 | eval_bvalue_from_norm_expr(image(Rel,Set),ResVal,Hyps) :- get_bvalue_from_norm_expr(Rel,RelVal,Hyps),!, | |
| 1971 | get_bvalue_from_norm_expr(Set,SetVal,Hyps),!, | |
| 1972 | eval_binary_operator(image,RelVal,SetVal,ResVal). | |
| 1973 | ||
| 1974 | ||
| 1975 | % try and rewrite function applications for comprehension_sets | |
| 1976 | rewrite_function_application(CompSet,Arg,Hyps,Result,Hyps) :- | |
| 1977 | is_comprehension_set(CompSet,[$(PARA),$(LAMBDARES)],Body), | |
| 1978 | get_conjunct(Body,equal(A,B)), | |
| 1979 | sym_unify(A,B,$(LAMBDARES),RESEXPR), | |
| 1980 | \+ occurs(RESEXPR,LAMBDARES), | |
| 1981 | % TODO: support more than one argument and hadd rest of body to hyps | |
| 1982 | !, | |
| 1983 | rename_norm_term(RESEXPR,[rename(PARA,Arg)],Result). | |
| 1984 | rewrite_function_application(Function,Arg,Hyps,Result,Hyps2) :- | |
| 1985 | avl_fetch_binop_from_hyps(Function,equal,Hyps,Value,Hyps1), | |
| 1986 | rewrite_function_application(Value,Arg,Hyps1,Result,Hyps2). | |
| 1987 | ||
| 1988 | get_conjunct(conjunct(A,B),C) :- !, (get_conjunct(A,C) ; get_conjunct(B,C)). | |
| 1989 | get_conjunct(C,C). | |
| 1990 | ||
| 1991 | merge_set_extensions(empty_set) --> []. | |
| 1992 | merge_set_extensions(empty_sequence) --> []. | |
| 1993 | merge_set_extensions(set_extension(L)) --> L. | |
| 1994 | merge_set_extensions(sorted_set_extension(L)) --> L. | |
| 1995 | merge_set_extensions(union(A,B)) --> merge_set_extensions(A), merge_set_extensions(B). | |
| 1996 | ||
| 1997 | % check if AVL is a subset of the first argument | |
| 1998 | check_subset_avl(union(A,B),AVL1,Hyps) :- !, % TO DO: try and merge A,B | |
| 1999 | (check_subset_avl(A,AVL1,Hyps) -> true ; check_subset_avl(B,AVL1,Hyps)). | |
| 2000 | check_subset_avl(intersection(A,B),AVL1,Hyps) :- !, % AVL <: A /\ B if AVL <: A & AVL <: B | |
| 2001 | (check_subset_avl(A,AVL1,Hyps) -> check_subset_avl(B,AVL1,Hyps)). | |
| 2002 | check_subset_avl(interval(L2,U2),AVL,_) :- number(L2),number(U2),!, | |
| 2003 | check_avl_in_interval(AVL,L2,U2). | |
| 2004 | check_subset_avl(value(avl_set(AVL2)),AVL1,_) :- !, check_avl_subset(AVL1,AVL2). | |
| 2005 | check_subset_avl(seq(MAX),AVL,Hyps) :- maximal_set(MAX,Hyps), !, is_avl_set_of_sequences(AVL,seq). | |
| 2006 | check_subset_avl(seq1(MAX),AVL,Hyps) :- maximal_set(MAX,Hyps), !, is_avl_set_of_sequences(AVL,seq1). | |
| 2007 | check_subset_avl(seq(seq(MAX)),AVL,Hyps) :- maximal_set(MAX,Hyps), | |
| 2008 | % comes from general concat | |
| 2009 | custom_explicit_sets:is_one_element_avl(AVL,Element), % usually one value from try_get_set_of_possible_values | |
| 2010 | is_sequence(Element,seq), | |
| 2011 | expand_custom_set_to_list(Element,ListOfSeqs), | |
| 2012 | maplist(is_subsequence,ListOfSeqs). | |
| 2013 | check_subset_avl(A,AVL,Hyps) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!, | |
| 2014 | check_subset_avl(A2,AVL,Hyps2). | |
| 2015 | check_subset_avl(A,AVL,Hyps) :- | |
| 2016 | avl_fetch_worthwhile_equal_from_hyps(A,Hyps,A2,Hyps2), | |
| 2017 | rewrite_local_loop_check(A,check_subset_avl,A2,Hyps2,Hyps3), | |
| 2018 | check_subset_avl(A2,AVL,Hyps3). | |
| 2019 | %check_subset_avl(A,AVL,_) :- print(check_subset_avl_failed(A,AVL)),nl,fail. | |
| 2020 | ||
| 2021 | is_subsequence((int(_Index),Sequence)) :- is_sequence(Sequence,seq). | |
| 2022 | ||
| 2023 | is_sequence(avl_set(SeqAVL),_) :- safe_is_avl_sequence(SeqAVL). | |
| 2024 | is_sequence([],seq). | |
| 2025 | ||
| 2026 | % check if all elements of the AVL are sequences | |
| 2027 | is_avl_set_of_sequences(AVL,SeqType) :- avl_height(AVL,Height), Height<7, | |
| 2028 | expand_custom_set_to_list(avl_set(AVL),ListOfSeqs), | |
| 2029 | l_is_sequence(ListOfSeqs,SeqType). | |
| 2030 | l_is_sequence([],_). | |
| 2031 | l_is_sequence([S1|T],SeqType) :- is_sequence(S1,SeqType), l_is_sequence(T,SeqType). | |
| 2032 | ||
| 2033 | ||
| 2034 | :- use_module(probsrc(b_global_sets),[b_global_set/1]). | |
| 2035 | maximal_set('INTEGER',_). % integer_set('INTEGER') ? | |
| 2036 | maximal_set(real_set,_). | |
| 2037 | maximal_set(string_set,_). | |
| 2038 | maximal_set(bool_set,_). | |
| 2039 | maximal_set('typeset',_). | |
| 2040 | maximal_set(cartesian_product(A,B),Hyps) :- % SIMP_CPROD_EQUAL_TYPE | |
| 2041 | maximal_set(A,Hyps), maximal_set(B,Hyps). | |
| 2042 | maximal_set(relations(A,B),Hyps) :- % SIMP_TYPE_EQUAL_REL | |
| 2043 | maximal_set(A,Hyps), maximal_set(B,Hyps). | |
| 2044 | maximal_set(set_subtraction(A,B),Hyps) :- % SIMP_SETMINUS_EQUAL_TYPE | |
| 2045 | maximal_set(A,Hyps), check_equal_empty_set(B,Hyps,_). | |
| 2046 | maximal_set(pow_subset(A),Hyps) :- maximal_set(A,Hyps). | |
| 2047 | maximal_set('$'(ID),Hyps) :- is_global_set_id(ID,Hyps). | |
| 2048 | maximal_set(value(avl_set(AVL)),_) :- | |
| 2049 | quick_definitely_maximal_set_avl(AVL). | |
| 2050 | maximal_set(set_extension(A),Hyps) :- maximal_set_extension(A,Hyps). | |
| 2051 | % sorted_set_extension is never maximal | |
| 2052 | maximal_set(CompSet,_) :- is_comprehension_set(CompSet,_,truth). | |
| 2053 | %maximal_set(X,_) :- print(max_fail(X)),nl,fail. | |
| 2054 | ||
| 2055 | construct_set_extension([],_,Res) :- !, Res=empty_set. | |
| 2056 | construct_set_extension(L,Hyps,Res) :- maximal_set_extension(L,Hyps),!, Res='typeset'. | |
| 2057 | construct_set_extension(L,_,sorted_set_extension(SL)) :- | |
| 2058 | %length(L,Len), format('Construct set_extension ~w~n',[Len]), | |
| 2059 | sort(L,SL). | |
| 2060 | ||
| 2061 | maximal_set_extension([boolean_true|T],_) :- !, member(boolean_false,T). | |
| 2062 | maximal_set_extension([boolean_false|T],_) :- !, member(boolean_true,T). | |
| 2063 | maximal_set_extension(['$'(ID)|T],Hyps) :- | |
| 2064 | is_global_constant_id(ID,Hyps), | |
| 2065 | sort(['$'(ID)|T],Sorted), | |
| 2066 | maplist(is_glob_const_id(Hyps),Sorted), % all elements are global constants | |
| 2067 | lookup_global_constant(ID,fd(_,GlobalSet)), | |
| 2068 | enumerated_set(GlobalSet),b_global_set_cardinality(GlobalSet,Size), | |
| 2069 | length(Sorted,Size). | |
| 2070 | %maximal_set_extension(X,_) :- print(maximal_failed(X)),nl,fail. | |
| 2071 | ||
| 2072 | is_glob_const_id(Hyps,'$'(ID)) :- is_global_constant_id(ID,Hyps). | |
| 2073 | ||
| 2074 | ||
| 2075 | is_global_set_id(ID,Hyps) :- | |
| 2076 | b_global_set(ID), | |
| 2077 | \+ is_hyp_var(ID,Hyps). % global enumerated set visible | |
| 2078 | ||
| 2079 | % often called with 0 or 1 in first position | |
| 2080 | check_leq(I,I,_) :- !. | |
| 2081 | check_leq(if_then_else(Pred,A1,A2),B,Hyp) :- !, | |
| 2082 | push_and_rename_normalized_hyp(Pred,Hyp,Hyp1), | |
| 2083 | (hyps_inconsistent(Hyp1) -> true ; check_leq(A1,B,Hyp1) -> true), | |
| 2084 | push_and_rename_normalized_hyp(negation(Pred),Hyp,Hyp2), | |
| 2085 | (hyps_inconsistent(Hyp2) -> true ; check_leq(A2,B,Hyp2) -> true). | |
| 2086 | check_leq(N1,N2,_) :- number(N1), number(N2), !, N1 =< N2. | |
| 2087 | check_leq(N1,N2,hyp_rec(AVL,_)) :- | |
| 2088 | (avl_fetch(less_equal(N1,N2),AVL) | |
| 2089 | -> true | |
| 2090 | ; avl_fetch(equal(N1,N2),AVL)),!. | |
| 2091 | check_leq(min(List),N2,Hyps) :- !, | |
| 2092 | member(N1,List), check_leq(N1,N2,Hyps),!. | |
| 2093 | check_leq(min_int,N2,Hyps) :- !, % we could look up the value of MININT; but largest possible value is -1 | |
| 2094 | MININT is -1, | |
| 2095 | check_leq(MININT,N2,Hyps). | |
| 2096 | check_leq(N1,max_int,Hyps) :- !, % we could look up the value of MAXINT; but smallest possible value is 1 | |
| 2097 | MAXINT = 1, | |
| 2098 | check_leq(N1,MAXINT,Hyps). | |
| 2099 | check_leq(N1,N2,Hyps) :- | |
| 2100 | rewrite_integer(N2,Hyps,RN2,Hyps2),!, | |
| 2101 | check_leq(N1,RN2,Hyps2). | |
| 2102 | check_leq(add(N1,1),N2,Hyps) :- | |
| 2103 | check_not_equal(N1,N2,Hyps), | |
| 2104 | !, % N1+1 <= N2 if N1 <= N2 & N1 \= N2 ; happens quite often in array traversals | |
| 2105 | check_leq(N1,N2,Hyps). | |
| 2106 | check_leq(N1,minus(N2,1),Hyps) :- % variation of rule above | |
| 2107 | check_not_equal(N1,N2,Hyps), | |
| 2108 | !, % N1 <= N2-1 if N1 <= N2 & N1 \= N2 ; happens in array traversals | |
| 2109 | check_leq(N1,N2,Hyps). | |
| 2110 | check_leq(Nr,X,Hyps) :- | |
| 2111 | \+ number(X), | |
| 2112 | try_get_set_of_possible_values(X,Hyps,SetX,Hyps2), | |
| 2113 | check_all_values_geq_val(SetX,Nr,Hyps2),!. | |
| 2114 | check_leq(Nr,X,Hyps) :- number(Nr), !, | |
| 2115 | check_leq_nr(Nr,X,Hyps). | |
| 2116 | check_leq(N1,N2,Hyps) :- rewrite_integer(N1,Hyps,RN1,Hyps2),!, | |
| 2117 | check_leq(RN1,N2,Hyps2). | |
| 2118 | check_leq(Add,N2,Hyps) :- % A+N1 <= N2 <=> A <= N2-N1 | |
| 2119 | number(N2), | |
| 2120 | add_with_number(Add,A,N1),!, | |
| 2121 | N21 is N2-N1, | |
| 2122 | check_leq(A,N21,Hyps). | |
| 2123 | check_leq(Mul,N2,Hyps) :- % A*N1 <= N2 if A <= N2/N1 if N1>0 and N2 mod N1=0 | |
| 2124 | number(N2), | |
| 2125 | mul_with_number(Mul,Hyps,A,N1), | |
| 2126 | % symmetrical case to check_leq_nr(N1,Mul,Hyps), with N1=-N2 | |
| 2127 | !, | |
| 2128 | ( N1=0 -> check_leq(0,N2,Hyps) | |
| 2129 | ; N1>0 -> N21 is N2 div N1, % A <= 1.5 means we have to have A <= 1; | |
| 2130 | % A <= -1.5 means we have to have A <= -2 -3 div 2 =:= -2 | |
| 2131 | check_leq(A,N21,Hyps) | |
| 2132 | ; cdiv(N2,N1,N21), % A >= 1.5 means we have to have A >= 2 ; cdiv | |
| 2133 | check_leq(N21,A,Hyps) | |
| 2134 | ). | |
| 2135 | check_leq(div(A,N1),N2,Hyps) :- | |
| 2136 | number(N1),number(N2), N1>0, | |
| 2137 | !, | |
| 2138 | (N2=0 -> N12 is N2-1 % A/4 <= 0 <=> A <= 3 | |
| 2139 | ; N2 >= 0 -> N12 is (N2+1)*N1-1 % A/4 <= 10 <=> A <= 49 % A/N1 <= N2 <=> A <= (N1+1)*N2-1 | |
| 2140 | ; N12 is N2*N1 % A/4 <= -10 <=> A <= -40 | |
| 2141 | ), | |
| 2142 | check_leq(A,N12,Hyps). | |
| 2143 | check_leq(div(A1,N1),A2,Hyps) :- number(N1), N1>0, % A/N1 <= A if N1>0 & A>=0 | |
| 2144 | check_equal(A1,A2,Hyps,Hyps1),!, | |
| 2145 | check_leq(0,A1,Hyps1). | |
| 2146 | check_leq(modulo(A1,A2),B,Hyps) :- | |
| 2147 | \+ z_or_tla_minor_mode, % args to mod must be non-negative, modulo is between 0..A2-1 | |
| 2148 | ((number(A2),A21 is A2-1 -> check_leq(A21,B,Hyps) | |
| 2149 | ; B=minus(B1,1) -> check_leq(A2,B1,Hyps) | |
| 2150 | ; check_leq(A2,B,Hyps) | |
| 2151 | ) -> true | |
| 2152 | ; check_leq(A1,B,Hyps)). | |
| 2153 | % TO DO: modulo as RHS | |
| 2154 | check_leq(unary_minus(A),unary_minus(B),Hyps) :- !, % -A <= -B ---> A >= B | |
| 2155 | check_leq(B,A,Hyps). | |
| 2156 | check_leq(X,Nr,Hyps) :- \+ number(X), | |
| 2157 | try_get_set_of_possible_values(X,Hyps,SetX,Hyps2), | |
| 2158 | check_all_values_leq_val(SetX,Nr,Hyps2),!. % cut here; get set of possible values can give multiple solutions | |
| 2159 | check_leq(Minus,N2,Hyps) :- minus_with_number(Minus,N1,Nr), | |
| 2160 | Nr >= 0,!, % N1-Nr <= N2 if N1 <= N2 | |
| 2161 | % Both N1 and N2 are usually not numbers here | |
| 2162 | check_leq(N1,N2,Hyps). | |
| 2163 | check_leq(N1,Add,Hyps) :- | |
| 2164 | add_with_number(Add,N2,Nr),Nr >= 0,!, % N1 <= N2+Nr if N1 <= N2 | |
| 2165 | % Both N1 and N2 are usually not numbers here | |
| 2166 | check_leq(N1,N2,Hyps). | |
| 2167 | check_leq(add(A,B),E,Hyps) :- | |
| 2168 | decompose_floor(E,Hyps,X,Y), % e.g. divide a number E by 2 | |
| 2169 | check_leq(A,X,Hyps), % TO DO: other combinations like A <= 0, B <= Nr; or we could try_get_set_of_possible_values | |
| 2170 | check_leq(B,Y,Hyps). | |
| 2171 | check_leq('$'(X),N2,Hyps) :- | |
| 2172 | avl_fetch_binop_from_hyps('$'(X),less_equal,Hyps,Y,Hyps2), | |
| 2173 | (number(N2),avl_fetch_not_equal('$'(X),Y,Hyps) % as we know X and Y we can use regular avl_fetch | |
| 2174 | -> N21 is N2+1 % we have X<Y in the Hypotheses, we just require that Y <= N2+1 | |
| 2175 | ; N21=N2), | |
| 2176 | check_leq(Y,N21,Hyps2). | |
| 2177 | check_leq(Nr,'$'(X),Hyps) :- | |
| 2178 | ( avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2), | |
| 2179 | rewrite_local_loop_check(X,check_leq,Y,Hyps2,Hyps3), | |
| 2180 | check_leq(Nr,Y,Hyps3) -> true | |
| 2181 | % ; avl_fetch_binop_from_hyps('$'(X),greater,Hyps,Y,Hyps2), N1 is Nr-1, check_leq(N1,Y,Hyps2) -> true | |
| 2182 | ; avl_fetch_binop_from_hyps('$'(X),greater_equal,Hyps,Y,Hyps2), | |
| 2183 | % note: Nr is not a number, hence probably not useful to check not_equal in Hyps, as we cannot compute Nr-1 | |
| 2184 | check_leq(Nr,Y,Hyps2) | |
| 2185 | -> true | |
| 2186 | ), | |
| 2187 | !. | |
| 2188 | %check_leq(A,B,_H) :- print(check_leq_failed(A,B)),nl, portray_hyps(_H),nl,fail. | |
| 2189 | ||
| 2190 | % decompose an expression E into A and B so that A+B <= E | |
| 2191 | decompose_floor(X,Hyps,A,B) :- get_number(X,Hyps,Nr),!, | |
| 2192 | A is Nr div 2, B=A. % -11 div 2 -> -6, -1 div 2 = -1, 11 div 2 = 5 | |
| 2193 | decompose_floor(add(A,B),_Hyps,A,B). % TO DO: we could try other order | |
| 2194 | decompose_floor(Mul,Hyps,A,A) :- | |
| 2195 | mul_with_number(Mul,Hyps,A,Nr), | |
| 2196 | Nr>=2, % we could divide Nr by 2 | |
| 2197 | (Nr=2 -> true % we have exactly A+A = Mul | |
| 2198 | ; check_leq(0,A,Hyps)). % Note: -10/10 + -10/10 is not <= -10 | |
| 2199 | ||
| 2200 | % ceiling division utility | |
| 2201 | cdiv(N1,N2,Res) :- | |
| 2202 | (N1 mod N2 =:= 0 -> Res is N1//N2 | |
| 2203 | ; Res is (N1 div N2)+1). | |
| 2204 | ||
| 2205 | % Number <= Expression | |
| 2206 | check_leq_nr(N1,Add,Hyps) :- % N1 <= A+N2 <=> N1-N2 <= A | |
| 2207 | add_with_number(Add,A,N2), !, | |
| 2208 | N12 is N1-N2, | |
| 2209 | check_leq(N12,A,Hyps). | |
| 2210 | check_leq_nr(Nr,add(N1,N2),Hyps) :- !, % 0 <= A+B if 0 <= A & 0 <= B | |
| 2211 | % Both N1 and N2 are usually not numbers here | |
| 2212 | cdiv(Nr,2,Nr2), % Note: cdiv(-3,2) = 1, cdiv(3,2)=2 | |
| 2213 | check_leq(Nr2,N1,Hyps), | |
| 2214 | check_leq(Nr2,N2,Hyps). | |
| 2215 | check_leq_nr(N1,minus(N2,B),Hyps) :- % N1 <= N2-B <=> B <= N2-N1 | |
| 2216 | number(N2), !, | |
| 2217 | N21 is N2-N1, | |
| 2218 | check_leq(B,N21,Hyps). | |
| 2219 | check_leq_nr(N1,Mul,Hyps) :- % N1 <= A*N2 if N1/N2 <= A and N2>0 | |
| 2220 | mul_with_number(Mul,Hyps,A,N2), | |
| 2221 | !, | |
| 2222 | ( N2=0 -> check_leq(N1,0,Hyps) | |
| 2223 | ; N2>0 -> cdiv(N1,N2,N12), % cdiv | |
| 2224 | % if 1.5 <= A --> 2 <= A ; if -1.5 <= A --> -1 <= A | |
| 2225 | check_leq(N12,A,Hyps) | |
| 2226 | ; N12 is N1 div N2, | |
| 2227 | % if A <= 1.5 --> A <= 1 ; if -1.5 <= A --> -1 <= A | |
| 2228 | % A <= -1.5 means we have to have A <= -2 -3 div 2 =:= -2 | |
| 2229 | check_leq(A,N12,Hyps) | |
| 2230 | ). | |
| 2231 | check_leq_nr(0,multiplication(A,B),Hyps) :- !, % 0 <= A*B if A and B have same parity | |
| 2232 | (check_leq(0,A,Hyps) -> check_leq(0,B,Hyps) | |
| 2233 | ; check_leq(A,0,Hyps) -> check_leq(B,0,Hyps)). | |
| 2234 | check_leq_nr(N1,div(A,N2),Hyps) :- % N1 <= A/N2 <=> N1*N2 <= A | |
| 2235 | number(N2), N2>0, % TODO: case if N2<0 | |
| 2236 | !, | |
| 2237 | (N1 > 0 -> N12 is N1*N2 % 10 <= A/4 <=> 40 <= A | |
| 2238 | ; N1 = 0 -> N12 is 1-N2 % 0 <= A/4 <=> -3 <= A | |
| 2239 | ; N12 is (N1 - 1)*(N2)+1 % -10 <= A/4 <=> -49 <= A | |
| 2240 | ), | |
| 2241 | check_leq(N12,A,Hyps). | |
| 2242 | check_leq_nr(0,div(A,B),Hyps) :- !, % 0 <= A/B guaranteed if A and B have same parity | |
| 2243 | (check_leq(0,A,Hyps) -> check_leq(0,B,Hyps) % B \= 0 checked by other WD condition | |
| 2244 | ; check_leq(A,0,Hyps) -> check_leq(B,0,Hyps)). % ditto | |
| 2245 | % TODO: other solutions possible, e.g., -1/100 = 1/-100 = 0 | |
| 2246 | check_leq_nr(Nr,'$'(X),Hyps) :- | |
| 2247 | ( avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2), | |
| 2248 | rewrite_local_loop_check(X,check_leq,Y,Hyps2,Hyps3), | |
| 2249 | check_leq(Nr,Y,Hyps3) -> true | |
| 2250 | % ; avl_fetch_binop_from_hyps('$'(X),greater,Hyps,Y,Hyps2), N1 is Nr-1, check_leq(N1,Y,Hyps2) -> true | |
| 2251 | ; avl_fetch_binop_from_hyps('$'(X),greater_equal,Hyps,Y,Hyps2), | |
| 2252 | (avl_fetch_not_equal('$'(X),Y,Hyps2) % we have X < Y => sufficient to prove N-1 <= Y | |
| 2253 | -> N1 is Nr-1, check_leq(N1,Y,Hyps2) | |
| 2254 | ; check_leq(Nr,Y,Hyps2) | |
| 2255 | ) | |
| 2256 | ), | |
| 2257 | !. | |
| 2258 | check_leq_nr(Nr,modulo(A,B),Hyps) :- \+ z_or_tla_minor_mode, % A and B must be non-negative, modulo is between 0..B-1 | |
| 2259 | (Nr =< 0 -> true % modulo always positive or 0 | |
| 2260 | ; % Nr <= A mod B if Nr <= A and A < B | |
| 2261 | check_leq_nr(Nr,A,Hyps), % Nr <= A | |
| 2262 | check_less(A,B,Hyps)). % and A < B so that modulo does not take effect | |
| 2263 | check_leq_nr(Nr,size(Seq),Hyps) :- check_leq_nr_size(Nr,Seq,Hyps). | |
| 2264 | check_leq_nr(1,power_of(A,_),Hyps) :- check_leq(1,A,Hyps). % Nr <= 1 <= x**y if x >= 1 | |
| 2265 | check_leq_nr(Nr,power_of(A,_),Hyps) :- number(Nr), Nr =< 0, | |
| 2266 | check_leq(0,A,Hyps). % 0 <= x**y if x >= 0 | |
| 2267 | %check_leq_nr(A,B,_H) :- print(check_leq_nr_failed(A,B)),nl,fail. | |
| 2268 | ||
| 2269 | check_less(A,B,Hyps) :- | |
| 2270 | check_leq(A,B,Hyps),!, | |
| 2271 | check_not_equal(A,B,Hyps). | |
| 2272 | ||
| 2273 | :- use_module(probsrc(specfile),[z_or_tla_minor_mode/0]). | |
| 2274 | ||
| 2275 | ||
| 2276 | check_leq_nr_size(Nr,restrict_front(_,RestrN),Hyps) :- !, % X <= size( Seq /|\ N) if X <= N as WD condition implies N : 0..size(Seq) | |
| 2277 | check_leq_nr(Nr,RestrN,Hyps). | |
| 2278 | check_leq_nr_size(1,Seq,Hyps) :- check_is_non_empty_sequence(Seq,Hyps). | |
| 2279 | ||
| 2280 | add_with_number(add(A,B),X,Nr) :- (number(A) -> Nr=A, X=B ; number(B) -> Nr=B, X=A). | |
| 2281 | add_with_number(minus(A,B),A,Nr) :- number(B), Nr is -B. | |
| 2282 | mul_with_number(multiplication(A,B),Hyps,X,Nr) :- | |
| 2283 | (get_number(A,Hyps,Nr) -> X=B ; get_number(B,Hyps,Nr) -> X=A). | |
| 2284 | mul_with_number(unary_minus(A),_Hyps,A,Nr) :- Nr is -1. | |
| 2285 | minus_with_number(add(A,B),A,Nr) :- number(B), Nr is -B. | |
| 2286 | minus_with_number(minus(A,Nr),A,Nr) :- number(Nr). | |
| 2287 | ||
| 2288 | ||
| 2289 | %get_possible_values('$'(X),Hyps,SetX,Hyps2) :- | |
| 2290 | % avl_fetch_binop_from_hyps('$'(X),member,Hyps,SetX,Hyps2). | |
| 2291 | ||
| 2292 | % a few rewrite rules for integer expressions | |
| 2293 | % addition/multiplication is dealt with in other places (and is usually done symbolically) | |
| 2294 | rewrite_integer(size(Seq),Hyps,Size,Hyps2) :- % can happen for sequence POs, like restrict_front,tail | |
| 2295 | compute_card_of_set(Seq,Hyps,Size,Hyps2),!. | |
| 2296 | rewrite_integer(card(Seq),Hyps,Size,Hyps2) :- !, rewrite_card_of_set(Seq,Hyps,Size,Hyps2). | |
| 2297 | rewrite_integer(assertion_expression(_,_,Expr),Hyps,Expr,Hyps). % TO DO: add Predicate to Hyps? | |
| 2298 | % the following may be done by ast_cleanup, but e.g., when applying functions no cleanup is run in l_rename_and_prove_goals | |
| 2299 | rewrite_integer(add(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1), number(A1), | |
| 2300 | (compute_integer(B,Hyps1,B1,Hyps2), number(B1) | |
| 2301 | -> Res is A1+B1 | |
| 2302 | ; A1=0 -> Res = B, Hyps2=Hyps1). | |
| 2303 | rewrite_integer(multiplication(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1), number(A1),!, | |
| 2304 | (A1=0 -> Res=0, Hyps2=Hyps1 | |
| 2305 | ; compute_integer(B,Hyps1,B1,Hyps2), number(B1) | |
| 2306 | -> Res is A1*B1 | |
| 2307 | ; A1=1 -> Res=B, Hyps2=Hyps1). | |
| 2308 | rewrite_integer(multiplication(A,B),Hyps,Res,Hyps2) :- | |
| 2309 | compute_integer(B,Hyps,B1,Hyps2), number(B1), | |
| 2310 | (B1=0 -> Res=0 | |
| 2311 | ; B1=1 -> Res = A). | |
| 2312 | rewrite_integer(unary_minus(A),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps2), number(A1), | |
| 2313 | Res is -A1. | |
| 2314 | rewrite_integer(minus(A,B),Hyps,Res,Hyps2) :- compute_integer(B,Hyps,B1,Hyps1), number(B1), | |
| 2315 | (compute_integer(A,Hyps1,A1,Hyps2), number(A1) | |
| 2316 | -> Res is A1-B1 | |
| 2317 | ; B1=0 -> Res = A, Hyps2=Hyps1). | |
| 2318 | rewrite_integer(power_of(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1), number(A1), | |
| 2319 | compute_integer(B,Hyps1,B1,Hyps2), number(B1), B1 >=0, | |
| 2320 | % check if not too large: | |
| 2321 | (abs(A1) < 2 -> true | |
| 2322 | ; A1=2 -> B1 =< 64 | |
| 2323 | ; A1 < 4294967296 -> B1 =< 2 | |
| 2324 | ; B1 =< 0 | |
| 2325 | ), | |
| 2326 | Res is A1 ^ B1. | |
| 2327 | rewrite_integer(modulo(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1),number(A1), | |
| 2328 | A1 >= 0, | |
| 2329 | compute_integer(B,Hyps1,B1,Hyps2), number(B1), B1 >0, | |
| 2330 | Res is A1 mod B1. | |
| 2331 | rewrite_integer(div(A,B),Hyps,Res,Hyps2) :- | |
| 2332 | compute_integer(B,Hyps,B1,Hyps1), number(B1), B1 \= 0, | |
| 2333 | (compute_integer(A,Hyps1,A1,Hyps2), number(A1) | |
| 2334 | -> Res is A1 // B1 % Prolog division corresponds to B division | |
| 2335 | ; B1=1 -> Res=A, Hyps2=Hyps1). | |
| 2336 | rewrite_integer(integer(X),Hyps,X,Hyps) :- integer(X), write(wd_unnormalised_integer(X)),nl. % should not happen | |
| 2337 | rewrite_integer(real(X),Hyps,Res,Hyps) :- atom(X), construct_real(X,term(floating(Res))). | |
| 2338 | rewrite_integer(convert_int_floor(RX),Hyps,X,Hyps1) :- | |
| 2339 | compute_integer(RX,Hyps,RX1,Hyps1), number(RX1), X is floor(RX1). %, print(rewr_floor(RX,X)),nl. | |
| 2340 | rewrite_integer(convert_int_ceiling(RX),Hyps,X,Hyps1) :- | |
| 2341 | compute_integer(RX,Hyps,RX1,Hyps1), number(RX1), X is ceiling(RX1). | |
| 2342 | rewrite_integer(convert_real(A),Hyps,RX,Hyps1) :- | |
| 2343 | compute_integer(A,Hyps,A1,Hyps1), integer(A1), RX is float(A1). | |
| 2344 | ||
| 2345 | rewrite_card_of_set(Set,Hyps,Size,Hyps2) :- | |
| 2346 | compute_card_of_set(Set,Hyps,Size,Hyps2),!. | |
| 2347 | rewrite_card_of_set(interval(1,Up),Hyps,Size,Hyps) :- !, % useful if Up is a symbolic expression | |
| 2348 | Size=Up. | |
| 2349 | rewrite_card_of_set(Set,Hyps,Size,Hyps2) :- rewrite_set_expression_exact(Set,Hyps,S2,Hyps1), | |
| 2350 | rewrite_card_of_set(S2,Hyps1,Size,Hyps2). | |
| 2351 | ||
| 2352 | compute_integer(A,Hyps,Res,Hyps) :- get_number(A,Hyps,Nr),!,Res=Nr. | |
| 2353 | compute_integer(A,H,Res,H2) :- rewrite_integer(A,H,Res,H2). | |
| 2354 | ||
| 2355 | get_number(A,_Hyps,Nr) :- number(A),!,Nr=A. | |
| 2356 | get_number('$'(ID),Hyps,Nr) :- Hyps \= nohyps, | |
| 2357 | avl_fetch_equal_from_hyps('$'(ID),Hyps,Nr,_Hyps1), number(Nr). | |
| 2358 | ||
| 2359 | ||
| 2360 | :- use_module(probsrc(b_global_sets), [enumerated_set/1, b_global_set_cardinality/2]). | |
| 2361 | compute_card_of_set(empty_set,Hyps,0,Hyps). | |
| 2362 | compute_card_of_set(empty_sequence,Hyps,0,Hyps). | |
| 2363 | compute_card_of_set(bool_set,Hyps,2,Hyps). | |
| 2364 | compute_card_of_set(interval(L,U),Hyps,Size,Hyps) :- number(L), number(U), Size is U+1-L. | |
| 2365 | compute_card_of_set(value(Val),Hyps,Size,Hyps) :- get_set_val_size(Val,Size). | |
| 2366 | compute_card_of_set(sequence_extension(List),Hyps,Size,Hyps) :- length(List,Size). | |
| 2367 | compute_card_of_set(set_extension([_]),Hyps,Size,Hyps) :- Size=1. % to do check if all elements definitely different | |
| 2368 | compute_card_of_set(sorted_set_extension([_]),Hyps,Size,Hyps) :- Size=1. % ditto | |
| 2369 | compute_card_of_set(rev(A),Hyps,Size,Hyps2) :- !, compute_card_of_set(A,Hyps,Size,Hyps2). | |
| 2370 | compute_card_of_set(front(A),Hyps,Size,Hyps2) :- !, compute_card_of_set(tail(A),Hyps,Size,Hyps2). | |
| 2371 | compute_card_of_set(tail(A),Hyps,Size,Hyps2) :- !, | |
| 2372 | compute_card_of_set(A,Hyps,Size1,Hyps2), number(Size1), Size1>0, | |
| 2373 | Size is Size1-1. | |
| 2374 | compute_card_of_set(concat(A,B),Hyps,Size,Hyps2) :- | |
| 2375 | compute_card_of_set(A,Hyps,SA,Hyps1),!, | |
| 2376 | compute_card_of_set(B,Hyps1,SB,Hyps2), | |
| 2377 | Size is SA+SB. | |
| 2378 | compute_card_of_set('$'(ID),Hyps,Size,Hyps) :- is_enumerated_set(ID,Hyps), | |
| 2379 | !, | |
| 2380 | b_global_set_cardinality(ID,Size). | |
| 2381 | compute_card_of_set('$'(ID),Hyps,Size,Hyps2) :- | |
| 2382 | avl_fetch_equal_from_hyps('$'(ID),Hyps,X2,Hyps1), | |
| 2383 | compute_card_of_set(X2,Hyps1,Size,Hyps2),!. | |
| 2384 | compute_card_of_set('$'(ID),Hyps,Size,Hyps4) :- % e.g., f:1..10 --> BOOL --> card(f) = 10 | |
| 2385 | avl_fetch_binop_from_hyps('$'(ID),member,Hyps,FunctionType,Hyps1), | |
| 2386 | is_partial_function_type(FunctionType,Hyps1,Hyps2), | |
| 2387 | get_exact_domain_of_func_or_rel_type(FunctionType,Hyps2,Dom,Hyps3), | |
| 2388 | compute_card_of_set(Dom,Hyps3,Size,Hyps4). | |
| 2389 | %compute_card_of_set(S,_,_,_) :- print(card_fail(S)),nl,fail. | |
| 2390 | ||
| 2391 | get_set_val_size([],0). | |
| 2392 | get_set_val_size(avl_set(AVL),Size) :- avl_size(AVL,Size). | |
| 2393 | ||
| 2394 | ||
| 2395 | check_all_values_geq_val(intersection(A,B),Nr,Hyps) :- | |
| 2396 | (check_all_values_geq_val(A,Nr,Hyps) -> true ; check_all_values_geq_val(B,Nr,Hyps)). | |
| 2397 | check_all_values_geq_val(union(A,B),Nr,Hyps) :- | |
| 2398 | (check_all_values_geq_val(A,Nr,Hyps) -> check_all_values_geq_val(B,Nr,Hyps)). | |
| 2399 | check_all_values_geq_val(set_subtraction(A,_),Nr,Hyps) :- | |
| 2400 | check_all_values_geq_val(A,Nr,Hyps). | |
| 2401 | check_all_values_geq_val(interval(From,_),Nr,Hyps) :- check_leq(Nr,From,Hyps). | |
| 2402 | check_all_values_geq_val(value(avl_set(AVL)),Nr,Hyps) :- avl_min(AVL,int(Min)), check_leq(Nr,Min,Hyps). | |
| 2403 | check_all_values_geq_val('NATURAL',Nr,Hyps) :- check_leq(Nr,0,Hyps). | |
| 2404 | check_all_values_geq_val('NATURAL1',Nr,Hyps) :- check_leq(Nr,1,Hyps). | |
| 2405 | check_all_values_geq_val(domain(Func),Nr,Hyps) :- | |
| 2406 | get_domain_or_superset(Func,Hyps,DomFunc,Hyps2), | |
| 2407 | check_all_values_geq_val(DomFunc,Nr,Hyps2). | |
| 2408 | check_all_values_geq_val(range(Func),Nr,Hyps) :- | |
| 2409 | get_range_or_superset(Func,Hyps,RanFunc,Hyps2), | |
| 2410 | check_all_values_geq_val(RanFunc,Nr,Hyps2). | |
| 2411 | check_all_values_geq_val(sorted_set_extension(L),Nr,Hyps) :- !, check_all_values_geq_val(set_extension(L),Nr,Hyps). | |
| 2412 | check_all_values_geq_val(set_extension(L),Nr,Hyps) :- | |
| 2413 | (member(Val,L), \+ check_leq(Nr,Val,Hyps) -> fail ; true). | |
| 2414 | check_all_values_geq_val('$'(X),Nr,Hyps) :- | |
| 2415 | avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2), | |
| 2416 | rewrite_local_loop_check(X,check_all_values_geq_val,Y,Hyps2,Hyps3), | |
| 2417 | check_all_values_geq_val(Y,Nr,Hyps3). | |
| 2418 | %check_all_values_geq_val(A,B,_) :- print(check_all_values_geq_val_failed(A,B)),nl,fail. | |
| 2419 | ||
| 2420 | check_all_values_neq_nr(intersection(A,B),Nr,Hyps) :- | |
| 2421 | (check_all_values_neq_nr(A,Nr,Hyps) -> true ; check_all_values_neq_nr(B,Nr,Hyps)). | |
| 2422 | check_all_values_neq_nr(union(A,B),Nr,Hyps) :- | |
| 2423 | (check_all_values_neq_nr(A,Nr,Hyps) -> check_all_values_neq_nr(B,Nr,Hyps)). | |
| 2424 | check_all_values_neq_nr(set_subtraction(A,_),Nr,Hyps) :- | |
| 2425 | check_all_values_neq_nr(A,Nr,Hyps). | |
| 2426 | check_all_values_neq_nr(interval(From,_),Nr,Hyps) :- number(From),F1 is From-1, check_leq(Nr,F1,Hyps). | |
| 2427 | check_all_values_neq_nr(interval(_,To),Nr,Hyps) :- number(To),T1 is To+1, check_leq(T1,Nr,Hyps). | |
| 2428 | check_all_values_neq_nr('NATURAL',Nr,Hyps) :- check_leq(Nr,-1,Hyps). | |
| 2429 | check_all_values_neq_nr('NATURAL1',Nr,Hyps) :- check_leq(Nr,0,Hyps). | |
| 2430 | check_all_values_neq_nr(sorted_set_extension(L),Nr,Hyps) :- !, check_all_values_neq_nr(set_extension(L),Nr,Hyps). | |
| 2431 | check_all_values_neq_nr(set_extension(L),Nr,Hyps) :- | |
| 2432 | (member(Val,L), \+ check_not_equal(Val,Nr,Hyps) -> fail ; true). | |
| 2433 | check_all_values_neq_nr('$'(X),Nr,Hyps) :- | |
| 2434 | avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2), | |
| 2435 | rewrite_local_loop_check(X,check_all_values_neq_nr,Y,Hyps2,Hyps3), | |
| 2436 | check_all_values_neq_nr(Y,Nr,Hyps3). | |
| 2437 | %check_all_values_neq_nr(A,B,_) :- print(check_all_values_neq_nr_failed(A,B)),nl,fail. | |
| 2438 | ||
| 2439 | ||
| 2440 | check_all_values_leq_val(intersection(A,B),Nr,Hyps) :- | |
| 2441 | (check_all_values_leq_val(A,Nr,Hyps) -> true ; check_all_values_leq_val(B,Nr,Hyps)). | |
| 2442 | check_all_values_leq_val(union(A,B),Nr,Hyps) :- | |
| 2443 | (check_all_values_leq_val(A,Nr,Hyps) -> check_all_values_leq_val(B,Nr,Hyps)). | |
| 2444 | check_all_values_leq_val(set_subtraction(A,_),Nr,Hyps) :- | |
| 2445 | check_all_values_leq_val(A,Nr,Hyps). | |
| 2446 | check_all_values_leq_val(interval(_,To),Nr,Hyps) :- check_leq(To,Nr,Hyps). | |
| 2447 | check_all_values_leq_val(value(avl_set(AVL)),Nr,Hyps) :- avl_max(AVL,int(Max)), check_leq(Max,Nr,Hyps). | |
| 2448 | check_all_values_leq_val(domain(Func),Nr,Hyps) :- | |
| 2449 | get_domain_or_superset(Func,Hyps,DomFunc,Hyps2), | |
| 2450 | check_all_values_leq_val(DomFunc,Nr,Hyps2). | |
| 2451 | check_all_values_leq_val(range(Func),Nr,Hyps) :- | |
| 2452 | get_range_or_superset(Func,Hyps,RanFunc,Hyps2), | |
| 2453 | check_all_values_leq_val(RanFunc,Nr,Hyps2). | |
| 2454 | check_all_values_leq_val(sorted_set_extension(L),Nr,Hyps) :- !, check_all_values_leq_val(set_extension(L),Nr,Hyps). | |
| 2455 | check_all_values_leq_val(set_extension(L),Nr,Hyps) :- | |
| 2456 | (member(Val,L), \+ check_leq(Val,Nr,Hyps) -> fail ; true). | |
| 2457 | check_all_values_leq_val('$'(X),Nr,Hyps) :- | |
| 2458 | avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2), | |
| 2459 | rewrite_local_loop_check(X,check_all_values_leq_val,Y,Hyps2,Hyps3), | |
| 2460 | check_all_values_leq_val(Y,Nr,Hyps3). | |
| 2461 | %check_all_values_leq_val(A,B,_) :- print(check_all_values_leq_val(A,B)),nl,fail. | |
| 2462 | ||
| 2463 | % check if two expressions are definitely different | |
| 2464 | % usually called for check_not_equal 0 or empty_set | |
| 2465 | check_not_equal(A,B,Hyp) :- | |
| 2466 | is_explicit_value(A,AV,Hyp), is_explicit_value(B,BV,Hyp), !, AV \= BV. | |
| 2467 | check_not_equal(X,Y,Hyp) :- sym_unify(X,Y,if_then_else(Pred,A1,A2),B),!, | |
| 2468 | push_and_rename_normalized_hyp(Pred,Hyp,Hyp1), | |
| 2469 | (hyps_inconsistent(Hyp1) -> true ; check_not_equal(A1,B,Hyp1) -> true), | |
| 2470 | push_and_rename_normalized_hyp(negation(Pred),Hyp,Hyp2), | |
| 2471 | (hyps_inconsistent(Hyp2) -> true ; check_not_equal(A2,B,Hyp2) -> true). | |
| 2472 | check_not_equal(N1,N2,Hyps) :- | |
| 2473 | avl_fetch_not_equal(N1,N2,Hyps),!. | |
| 2474 | check_not_equal(couple(A1,A2),couple(B1,B2),Hyps) :- !, | |
| 2475 | (check_not_equal(A1,B1,Hyps) -> true ; check_not_equal(A2,B2,Hyps)). | |
| 2476 | check_not_equal(X,B,Hyps) :- number(B), | |
| 2477 | try_get_set_of_possible_values(X,Hyps,SetX,Hyps2), | |
| 2478 | check_all_values_neq_nr(SetX,B,Hyps2),!. | |
| 2479 | % TO DO: compute also things like domain(...) for :wd s:perm(1..10) & x:dom(s) & res = 10/x | |
| 2480 | check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,unary_minus(A),B),number(B),!, BM is -B, | |
| 2481 | check_not_equal(A,BM,Hyps). | |
| 2482 | check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,multiplication(A,B),0),!, % A*B /= 0 if A/=0 & B/=0 | |
| 2483 | check_not_equal(A,0,Hyps),check_not_equal(B,0,Hyps). | |
| 2484 | check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,power_of(A,_),0),!, % A**B /= 0 if A/=0 | |
| 2485 | check_not_equal(A,0,Hyps). | |
| 2486 | check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,Add,B), | |
| 2487 | add_with_number(Add,A,Nr),!, | |
| 2488 | (Nr>0 -> check_leq(B,A,Hyps) % A >= B => A+Nr > B => A+Nr /= B | |
| 2489 | ; Nr=0 -> check_not_equal(A,B,Hyps) | |
| 2490 | ; check_leq(A,B,Hyps) | |
| 2491 | ). | |
| 2492 | check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,A,B),number(B),!, | |
| 2493 | B1 is B+1, | |
| 2494 | (check_leq(B1,A,Hyps) -> true % B < A | |
| 2495 | ; B2 is B-1, | |
| 2496 | check_leq(A,B2,Hyps)). % A < B | |
| 2497 | check_not_equal(XX,YY,Hyps) :- sym_unify(XX,YY,'$'(A),B), | |
| 2498 | avl_fetch_binop_from_hyps('$'(A),less_equal,Hyps,Y,Hyps2), | |
| 2499 | (number(B) -> (B1 is B-1, check_leq(Y,B1,Hyps2) -> true) | |
| 2500 | ; avl_fetch_not_equal('$'(A),Y,Hyps) % we have $(A) < Y => prove Y <= B | |
| 2501 | -> check_leq(Y,B,Hyps2) % we can prove x<y & y<=z => x<z but we cannot yet prove x<=y & y<z => x<z | |
| 2502 | ). | |
| 2503 | check_not_equal(XX,YY,Hyps) :- sym_unify(XX,YY,'$'(A),B), | |
| 2504 | avl_fetch_binop_from_hyps('$'(A),greater_equal,Hyps,Y,Hyps2), | |
| 2505 | (number(B) -> (B1 is B+1, check_leq(B1,Y,Hyps2) -> true) | |
| 2506 | ; avl_fetch_not_equal('$'(A),Y,Hyps) % we have $(A) < Y => prove Y <= B | |
| 2507 | -> check_leq(B,Y,Hyps2) % see comments above | |
| 2508 | ). | |
| 2509 | check_not_equal(A,Empty,Hyp) :- is_empty_set_direct(Empty), !, check_not_empty_set(A,Hyp). | |
| 2510 | check_not_equal(Empty,A,Hyp) :- is_empty_set_direct(Empty), !, check_not_empty_set(A,Hyp). | |
| 2511 | check_not_equal(value(avl_set(A)),value(avl_set(B)),_) :- nonvar(A), nonvar(B),!, % nonvar should always be true | |
| 2512 | \+ equal_avl_tree(A,B). | |
| 2513 | check_not_equal(A,B,Hyps) :- | |
| 2514 | (A=set_extension(LA) -> check_not_equal_set_extension(B,LA,Hyps) | |
| 2515 | ; B=set_extension(LB) -> check_not_equal_set_extension(A,LB,Hyps)),!. | |
| 2516 | check_not_equal(A,B,Hyps) :- | |
| 2517 | (is_interval(A,Hyps,Low,Up) -> check_not_equal_interval(B,lhs,Low,Up,Hyps) | |
| 2518 | ; is_interval(B,Hyps,Low,Up) -> check_not_equal_interval(A,rhs,Low,Up,Hyps)),!. | |
| 2519 | check_not_equal(A,B,Hyps) :- | |
| 2520 | avl_fetch_worthwhile_equal_from_hyps(A,Hyps,Value,Hyps2),!, | |
| 2521 | check_not_equal(Value,B,Hyps2). | |
| 2522 | check_not_equal(A,B,Hyps) :- | |
| 2523 | avl_fetch_worthwhile_equal_from_hyps(B,Hyps,Value,Hyps2),!, | |
| 2524 | check_not_equal(A,Value,Hyps2). | |
| 2525 | %check_not_equal(A,B,Hyps) :- print(check_not_equal_failed(A,B)),nl,portray_hyps(Hyps),nl,fail. | |
| 2526 | ||
| 2527 | check_not_equal_interval(MaxSet,_,_,_,Hyps) :- infinite_integer_set(MaxSet,Hyps). | |
| 2528 | check_not_equal_interval(A,lhs,Low,Up,Hyps) :- is_interval(A,Hyps,LowA,UpA), | |
| 2529 | (check_not_empty_interval(Low,Up,Hyps) -> true ; check_not_empty_interval(LowA,UpA,Hyps)), | |
| 2530 | % if one of the intervals is non-empty then it is sufficient for one bound to be different | |
| 2531 | (check_not_equal(LowA,Low,Hyps) -> true | |
| 2532 | ; check_not_equal(UpA,Up,Hyps) -> true). | |
| 2533 | % TODO: other intervals, avl_set | |
| 2534 | ||
| 2535 | infinite_integer_set('INTEGER',_). | |
| 2536 | infinite_integer_set('NATURAL',_). | |
| 2537 | infinite_integer_set('NATURAL1',_). | |
| 2538 | ||
| 2539 | check_not_equal_set_extension(set_extension([B|TB]),[A|TA],Hyps) :- (TA=[];TB=[]),!, | |
| 2540 | check_not_equal(A,B,Hyps). % TO DO: we can generalize this treatment to find one element in one set not in the other | |
| 2541 | check_not_equal_set_extension(value(avl_set(AVL)),LA,Hyps) :- length(LA,MaxSizeA), | |
| 2542 | (avl_size(AVL,Sze),Sze>MaxSizeA -> true % AVL has at least one element more | |
| 2543 | ; is_one_element_avl(AVL,B), LA=[A|_], check_not_equal(A,B,Hyps)). | |
| 2544 | ||
| 2545 | avl_fetch_not_equal(N1,N2,hyp_rec(AVL,_)) :- | |
| 2546 | (avl_fetch(not_equal(N1,N2),AVL) -> true | |
| 2547 | ; avl_fetch(not_equal(N2,N1),AVL)). % we do not store both directions for not_equal | |
| 2548 | ||
| 2549 | % unify two variables with other two variables; useful for symmetric rules | |
| 2550 | sym_unify(A,B,A,B). | |
| 2551 | sym_unify(A,B,B,A). | |
| 2552 | ||
| 2553 | % TO DO: get equalities; maybe we should harmonise this for all rules | |
| 2554 | % we could add rules about min_int, max_int | |
| 2555 | ||
| 2556 | ||
| 2557 | % we should call this to check if something is the empty set: | |
| 2558 | % it does equality rewrites, but also calls check_empty_set/3 indirectly | |
| 2559 | check_equal_empty_set(Set,Hyps,PT) :- PT = check_equal, | |
| 2560 | check_equal(Set,empty_set,Hyps,_). % will also call this below: | |
| 2561 | ||
| 2562 | is_empty_set_direct(empty_set). | |
| 2563 | is_empty_set_direct(empty_sequence). | |
| 2564 | is_empty_set_direct(value(X)) :- X==[]. | |
| 2565 | ||
| 2566 | check_empty_set(Set,_,empty_set) :- is_empty_set_direct(Set),!. | |
| 2567 | check_empty_set(A,Hyps,hyp) :- avl_fetch_from_hyps(equal(A,empty_set),Hyps),!. | |
| 2568 | check_empty_set(set_subtraction(A,B),Hyp,subset(PT)) :- !, % see SIMP_SETMINUS_EQUAL_EMPTY Rodin proof rule | |
| 2569 | check_is_subset(A,B,Hyp,PT). | |
| 2570 | check_empty_set(intersection(A,B),Hyps,inter_disjoint) :- !, | |
| 2571 | check_disjoint(A,B,Hyps). | |
| 2572 | check_empty_set(union(A,B),Hyps,union_empty(P1,P2)) :- !, % SIMP_BUNION_EQUAL_EMPTY | |
| 2573 | check_equal_empty_set(A,Hyps,P1),!, | |
| 2574 | check_equal_empty_set(B,Hyps,P2). | |
| 2575 | check_empty_set(general_union(A),Hyp,general_union(PT)) :- !, % SIMP_KUNION_EQUAL_EMPTY | |
| 2576 | check_is_subset(A,set_extension([empty_set]),Hyp,PT). | |
| 2577 | check_empty_set(cartesian_product(A,B),Hyps,cart_empty(PT)) :- !, % SIMP_CPROD_EQUAL_EMPTY | |
| 2578 | (check_equal_empty_set(A,Hyps,PT) -> true ; check_equal_empty_set(B,Hyps,PT)). | |
| 2579 | check_empty_set(pow1_subset(A),Hyps,pow1_empty(PT)) :- !, % SIMP_POW1_EQUAL_EMPTY | |
| 2580 | check_equal_empty_set(A,Hyps,PT). | |
| 2581 | check_empty_set(interval(From,To),Hyps,interval_empty) :- !, % SIMP_UPTO_EQUAL_EMPTY | |
| 2582 | check_less(To,From,Hyps). | |
| 2583 | check_empty_set(domain(A),Hyps,domain_empty(PT)) :- !, % SIMP_DOM_EQUAL_EMPTY | |
| 2584 | check_equal_empty_set(A,Hyps,PT). | |
| 2585 | check_empty_set(range(A),Hyps,range_empty(PT)) :- !, % SIMP_RAN_EQUAL_EMPTY | |
| 2586 | check_equal_empty_set(A,Hyps,PT). | |
| 2587 | check_empty_set(reverse(A),Hyps,reverse_empty(PT)) :- !, % SIMP_CONVERSE_EQUAL_EMPTY (relational inverse) | |
| 2588 | check_equal_empty_set(A,Hyps,PT). | |
| 2589 | check_empty_set(total_relation(A,B),Hyp,trel_empty(PTA,PTB)) :- !, % SIMP_SPECIAL_EQUAL_RELDOM | |
| 2590 | check_not_equal_empty_set(A,Hyp,PTA), check_equal_empty_set(B,Hyp,PTB). | |
| 2591 | check_empty_set(total_function(A,B),Hyp,tfun_empty(PTA,PTB)) :- !, % SIMP_SPECIAL_EQUAL_RELDOM | |
| 2592 | check_not_equal_empty_set(A,Hyp,PTA), check_equal_empty_set(B,Hyp,PTB). | |
| 2593 | check_empty_set(composition(F,G),Hyp,fcomp_empty) :- !, % SIMP_FCOMP_EQUAL_EMPTY | |
| 2594 | check_disjoint(range(F),domain(G),Hyp). | |
| 2595 | check_empty_set(A,Hyps,subset_strict_singleton) :- | |
| 2596 | avl_fetch_binop_from_hyps(A,subset_strict,Hyps,B,_), % A <<: {Single} => A={} | |
| 2597 | singleton_set(B,_). | |
| 2598 | % TODO: add more rules inter(A,Singleton) SIMP_BINTER_SING_EQUAL_EMPTY | |
| 2599 | ||
| 2600 | % we should call this to check if something is not the empty set: | |
| 2601 | % it does equality rewrites, but also calls check_not_empty_set/2 indirectly | |
| 2602 | check_not_equal_empty_set(Set,Hyps,not_equal_empty_set) :- | |
| 2603 | check_not_equal(Set,empty_set,Hyps). | |
| 2604 | ||
| 2605 | check_not_empty_set(A,Hyps) :- avl_fetch_from_hyps(not_equal(A,empty_set),Hyps),!. | |
| 2606 | check_not_empty_set(A,Hyps) :- %Note: size(A) should be changed to card(A) in normalization | |
| 2607 | (CardA = card(A) ; CardA = size(A)), | |
| 2608 | (Op = equal ; Op = greater_equal), | |
| 2609 | avl_fetch_binop_from_hyps(CardA,Op,Hyps,Nr,Hyps2), %Nr \= 0, | |
| 2610 | check_leq(1,Nr,Hyps2),!. % cut here, relevant for test 2043 | |
| 2611 | check_not_empty_set(set_extension([_|_]),_Hyps). | |
| 2612 | check_not_empty_set(sorted_set_extension([_|_]),_Hyps). | |
| 2613 | check_not_empty_set(sequence_extension([_|_]),_Hyps). | |
| 2614 | check_not_empty_set(cartesian_product(A,B),Hyps) :- % SIMP_CPROD_EQUAL_EMPTY | |
| 2615 | (check_not_empty_set(A,Hyps) -> check_not_empty_set(B,Hyps)). | |
| 2616 | check_not_empty_set(interval(A,B),Hyps) :- check_leq(A,B,Hyps). | |
| 2617 | check_not_empty_set(value(avl_set(AVL)),_) :- AVL \= empty. | |
| 2618 | check_not_empty_set(union(A,B),Hyp) :- !, (check_not_empty_set(A,Hyp) -> true ; check_not_empty_set(B,Hyp)). | |
| 2619 | check_not_empty_set(general_union(A),Hyp) :- !, % SIMP_KUNION_EQUAL_EMPTY | |
| 2620 | check_not_subset(A,set_extension([empty_set]),Hyp,_PT). | |
| 2621 | check_not_empty_set(set_subtraction(A,B),Hyp) :- !, % see SIMP_SETMINUS_EQUAL_EMPTY Rodin proof rule | |
| 2622 | check_not_subset(A,B,Hyp,_PT). | |
| 2623 | check_not_empty_set(overwrite(A,B),Hyp) :- !, (check_not_empty_set(A,Hyp) -> true ; check_not_empty_set(B,Hyp)). | |
| 2624 | check_not_empty_set(domain(A),Hyp) :- !, % SIMP_DOM_EQUAL_EMPTY | |
| 2625 | check_not_empty_set(A,Hyp). | |
| 2626 | check_not_empty_set(range(A),Hyp) :- !, % SIMP_RAN_EQUAL_EMPTY | |
| 2627 | check_not_empty_set(A,Hyp). | |
| 2628 | check_not_empty_set(identity(A),Hyp) :- !, check_not_empty_set(A,Hyp). | |
| 2629 | check_not_empty_set(image(R,interval(L,U)),Hyp) :- !, | |
| 2630 | check_not_empty_set(interval(L,U),Hyp), | |
| 2631 | (check_member_of_set(domain(R),L,Hyp,_) -> true | |
| 2632 | ; check_member_of_set(domain(R),U,Hyp,_) | |
| 2633 | ). | |
| 2634 | check_not_empty_set(image(Func,set_extension([S1|_])),Hyp) :- !, | |
| 2635 | check_member_of_set(domain(Func),S1,Hyp,_). | |
| 2636 | check_not_empty_set(reverse(A),Hyp) :- !, % SIMP_CONVERSE_EQUAL_EMPTY (relational inverse) | |
| 2637 | check_not_empty_set(A,Hyp). | |
| 2638 | check_not_empty_set(rev(A),Hyp) :- !, check_not_empty_set(A,Hyp). | |
| 2639 | check_not_empty_set(concat(A,B),Hyp) :- !, (check_not_empty_set(A,Hyp) -> true ; check_not_empty_set(B,Hyp)). | |
| 2640 | check_not_empty_set(bool_set,_Hyp) :- !. | |
| 2641 | check_not_empty_set(float_set,_Hyp) :- !. | |
| 2642 | check_not_empty_set(real_set,_Hyp) :- !. | |
| 2643 | check_not_empty_set(string_set,_Hyp) :- !. | |
| 2644 | check_not_empty_set('NATURAL1',_Hyp) :- !. % SIMP_NATURAL1_EQUAL_EMPTY | |
| 2645 | check_not_empty_set('NATURAL',_Hyp) :- !. % SIMP_NATURAL_EQUAL_EMPTY | |
| 2646 | check_not_empty_set(typeset,_Hyp) :- !. % SIMP_TYPE_EQUAL_EMPTY, all basic sets are non empty in B and Event-B | |
| 2647 | check_not_empty_set(relations(_,_),_Hyp) :- !. % SIMP_SPECIAL_EQUAL_REL | |
| 2648 | check_not_empty_set(total_function(A,B),Hyp) :- !, % SIMP_SPECIAL_EQUAL_RELDOM | |
| 2649 | ( check_equal_empty_set(A,Hyp,_) -> true | |
| 2650 | ; check_not_equal_empty_set(B,Hyp,_) -> true | |
| 2651 | ; check_equal(A,B,Hyp,_)). % implicit proof by case distinction | |
| 2652 | check_not_empty_set(total_relation(A,B),Hyp) :- !, % SIMP_SPECIAL_EQUAL_RELDOM | |
| 2653 | check_not_empty_set(total_function(A,B),Hyp). | |
| 2654 | check_not_empty_set(if_then_else(Pred,A,B),Hyp) :- !, | |
| 2655 | push_and_rename_normalized_hyp(Pred,Hyp,Hyp1), | |
| 2656 | (hyps_inconsistent(Hyp1) -> true ; check_not_empty_set(A,Hyp1) -> true), | |
| 2657 | push_and_rename_normalized_hyp(negation(Pred),Hyp,Hyp2), | |
| 2658 | (hyps_inconsistent(Hyp2) -> true ; check_not_empty_set(B,Hyp2) -> true). | |
| 2659 | check_not_empty_set(Expr,Hyps) :- | |
| 2660 | is_lambda_function_with_domain(Expr,Domain),!, | |
| 2661 | check_not_empty_set(Domain,Hyps). | |
| 2662 | check_not_empty_set(CompSet,Hyps) :- % {Ps | #Ids.P} /= {} <=> #(Ps,Ids).P | |
| 2663 | is_comprehension_set(CompSet,Paras,Body), | |
| 2664 | (Body = exists(Ids,Pred) -> append(Paras,Ids,Vars) ; Vars=Paras, Pred=Body), | |
| 2665 | conj_to_list(Pred,Conjuncts,[]), | |
| 2666 | check_satisfiable_conjuncts(Conjuncts,Vars,Hyps),!. | |
| 2667 | check_not_empty_set('$'(ID),Hyps) :- | |
| 2668 | enumerated_set(ID), | |
| 2669 | \+ is_hyp_var(ID,Hyps),!. % global enumerated set visible | |
| 2670 | check_not_empty_set(Eq,Hyps) :- | |
| 2671 | (Eq='$'(_) ; Eq=interval(_,_)), | |
| 2672 | avl_fetch_equal_from_hyps(Eq,Hyps,Value,Hyps2), | |
| 2673 | rewrite_local_loop_check(Eq,check_not_empty_set,Value,Hyps2,Hyps3), | |
| 2674 | check_not_empty_set(Value,Hyps3),!. | |
| 2675 | check_not_empty_set(Seq,Hyp) :- infer_sequence_type_of_expr(Seq,Hyp,seq1),!. | |
| 2676 | check_not_empty_set(Func,Hyps) :- Func = '$'(_), | |
| 2677 | avl_fetch_binop_from_hyps(Func,member,Hyps,FunctionType,Hyps2), % Func : . --> . | |
| 2678 | check_not_empty_elements(FunctionType,Hyps2),!. | |
| 2679 | check_not_empty_set(function(Func,Args),Hyps) :- | |
| 2680 | (get_range_or_superset(Func,Hyps,Range,Hyps2), | |
| 2681 | check_not_empty_elements(Range,Hyps2) -> !,true | |
| 2682 | ; rewrite_function_application(Func,Args,Hyps,Result,Hyps2), | |
| 2683 | check_not_empty_set(Result,Hyps2)). | |
| 2684 | check_not_empty_set(tail(A),Hyps) :- rewrite_card_of_set(A,Hyps,CardA,Hyps1),!, | |
| 2685 | check_leq(2,CardA,Hyps1). | |
| 2686 | check_not_empty_set(front(A),Hyps) :- rewrite_card_of_set(A,Hyps,CardA,Hyps1),!, | |
| 2687 | check_leq(2,CardA,Hyps1). | |
| 2688 | check_not_empty_set(A,Hyps) :- | |
| 2689 | avl_fetch_binop_from_hyps(A,not_subset_strict,Hyps,B,_), % A <<: {Single} <=> A={} | |
| 2690 | singleton_set(B,_),!. | |
| 2691 | check_not_empty_set(A,Hyps) :- | |
| 2692 | ( Lookup = A, Operator = superset | |
| 2693 | ; | |
| 2694 | (Lookup=domain(A) ; Lookup=range(A)), | |
| 2695 | (Operator = superset ; Operator = equal) | |
| 2696 | ), | |
| 2697 | avl_fetch_binop_from_hyps(Lookup,Operator,Hyps,B,Hyps2), % B /= {} & B <: A => A /= {} | |
| 2698 | rewrite_local_loop_check(A,check_not_empty_set,B,Hyps2,Hyps3), | |
| 2699 | check_not_empty_set(B,Hyps3),!. | |
| 2700 | % TO DO: rule for dom(r)<:A and r not empty implies A not empty; problem: we need lookup for A=dom(r), or dom(r)<:A, could be of form: r:A+->B | |
| 2701 | %check_not_empty_set(A,H) :- print(check_not_empty_set_failed(A)),nl,portray_hyps(H),nl,fail. | |
| 2702 | % TO DO: more rules for sequence operators; infer_sequence_type_of_expr does not look at values of ids | |
| 2703 | ||
| 2704 | ||
| 2705 | % check if elements of a function type or set are guaranteed to be not empty | |
| 2706 | ||
| 2707 | check_not_empty_elements(fin1_subset(_),_). | |
| 2708 | check_not_empty_elements(pow1_subset(_),_). | |
| 2709 | check_not_empty_elements(seq1(_),_). | |
| 2710 | check_not_empty_elements(iseq1(_),_). | |
| 2711 | check_not_empty_elements(perm(A),Hyps) :- check_not_empty_set(A,Hyps). | |
| 2712 | check_not_empty_elements(total_function(A,_),Hyps) :- check_not_empty_set(A,Hyps). | |
| 2713 | check_not_empty_elements(total_injection(A,_),Hyps) :- check_not_empty_set(A,Hyps). | |
| 2714 | check_not_empty_elements(total_surjection(A,B),Hyps) :- | |
| 2715 | (check_not_empty_set(A,Hyps) -> true ; check_not_empty_set(B,Hyps)). | |
| 2716 | check_not_empty_elements(total_bijection(A,B),Hyps) :- | |
| 2717 | (check_not_empty_set(A,Hyps) -> true ; check_not_empty_set(B,Hyps)). | |
| 2718 | check_not_empty_elements(total_relation(A,_),Hyps) :- check_not_empty_set(A,Hyps). | |
| 2719 | check_not_empty_elements(total_surjection_relation(A,_),Hyps) :- check_not_empty_set(A,Hyps). | |
| 2720 | check_not_empty_elements(partial_surjection(_,B),Hyps) :- check_not_empty_set(B,Hyps). | |
| 2721 | check_not_empty_elements(partial_bijection(_,B),Hyps) :- check_not_empty_set(B,Hyps). | |
| 2722 | check_not_empty_elements(surjection_relation(_,B),Hyps) :- check_not_empty_set(B,Hyps). | |
| 2723 | % more cases, set_extension,... | |
| 2724 | ||
| 2725 | :- use_module(probsrc(b_global_sets),[enumerated_set/1]). | |
| 2726 | % check if an expression is definitely finite | |
| 2727 | check_finite(bool_set,_,bool_set) :- !. | |
| 2728 | check_finite(empty_set,_,empty_set) :- !. | |
| 2729 | check_finite(empty_sequence,_,empty_sequence) :- !. | |
| 2730 | check_finite(float_set,_,float_set) :- !. | |
| 2731 | % check_finite(integer_set(X),_,bool_set) :- !. INT, NAT, NAT1 are translated to intervals | |
| 2732 | check_finite(set_extension(_),_,set_extension) :- !. | |
| 2733 | check_finite(sorted_set_extension(_),_,set_extension) :- !. | |
| 2734 | check_finite(sequence_extension(_),_,seq_extension) :- !. | |
| 2735 | check_finite(fin_subset(X),Hyps,fin(PT)) :- !, check_finite(X,Hyps,PT). | |
| 2736 | check_finite(fin1_subset(X),Hyps,fin1(PT)) :- !, check_finite(X,Hyps,PT). | |
| 2737 | check_finite(pow_subset(X),Hyps,pow(PT)) :- !, check_finite(X,Hyps,PT). | |
| 2738 | check_finite(pow1_subset(X),Hyps,pow1(PT)) :- !, check_finite(X,Hyps,PT). | |
| 2739 | check_finite(iseq(X),Hyps,iseq(PT)) :- !, check_finite(X,Hyps,PT). | |
| 2740 | check_finite(iseq1(X),Hyps,iseq1(PT)) :- !, check_finite(X,Hyps,PT). | |
| 2741 | check_finite(mu(Set),Hyps,mu) :- !, has_finite_elements(Set,Hyps). | |
| 2742 | check_finite(perm(X),Hyps,perm(PT)) :- !, check_finite(X,Hyps,PT). | |
| 2743 | check_finite(Set,Hyps,hyp) :- | |
| 2744 | avl_fetch_from_hyps(finite(Set),Hyps),!. | |
| 2745 | check_finite(domain(A),Hyp,dom(PT)) :- !, | |
| 2746 | (check_finite(A,Hyp,PT) -> true ; finite_domain(A,Hyp,PT)). | |
| 2747 | check_finite(range(A),Hyp,ran(PT)) :- !, | |
| 2748 | (check_finite(A,Hyp,PT) -> true ; finite_range(A,Hyp,PT)). | |
| 2749 | check_finite(reverse(A),Hyp,rev(PT)) :- !, check_finite(A,Hyp,PT). | |
| 2750 | check_finite(identity(A),Hyp,id(PT)) :- !,check_finite(A,Hyp,PT). % finite(id(A)) if finite(A) | |
| 2751 | check_finite(function(Func,Args),Hyps,function(PT)) :- !, | |
| 2752 | (get_range_or_superset(Func,Hyps,RanFunc,Hyps2), | |
| 2753 | has_finite_elements(RanFunc,Hyps2) -> PT = finite_elements | |
| 2754 | ; rewrite_function_application(Func,Args,Hyps,Result,Hyps2), | |
| 2755 | check_finite(Result,Hyps2,PT)). | |
| 2756 | check_finite(image(Func,B),Hyp,image(PT)) :- !, | |
| 2757 | (check_finite(Func,Hyp,PT) -> true % finite(Func[.]) <= finite(Func) | |
| 2758 | ; check_finite(B,Hyp,PTB) | |
| 2759 | -> PT = pfun(PTB), check_is_partial_function(Func,Hyp) % finite(Func[B]) <= finite(B) & Func : TD +-> TR | |
| 2760 | ). | |
| 2761 | check_finite(union(A,B),Hyp,union(PTA,PTB)) :- !, (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)). | |
| 2762 | check_finite(if_then_else(Pred,A,B),Hyps,if(PTA,PTB)) :- !, | |
| 2763 | push_and_rename_normalized_hyp(Pred,Hyps,Hyps1), | |
| 2764 | (hyps_inconsistent(Hyps1) -> true ; check_finite(A,Hyps1,PTA) -> true), | |
| 2765 | push_and_rename_normalized_hyp(negation(Pred),Hyps,Hyps2), | |
| 2766 | (hyps_inconsistent(Hyps2) -> true ; check_finite(B,Hyps2,PTB) -> true). | |
| 2767 | check_finite(intersection(A,B),Hyps,intersection(D,PT)) :- !, | |
| 2768 | (D=left,check_finite(A,Hyps,PT) -> true ; D=right,check_finite(B,Hyps,PT)). | |
| 2769 | check_finite(cartesian_product(A,B),Hyp,cart(PT)) :- | |
| 2770 | (check_finite(A,Hyp,PT) -> (check_equal_empty_set(A,Hyp,_PT2) -> true ; check_finite(B,Hyp,_PT2)) | |
| 2771 | ; check_equal_empty_set(B,Hyp,PT)). | |
| 2772 | check_finite(Rel,Hyp,rel(PTA,PTB)) :- is_relations_type(Rel,A,B),!, | |
| 2773 | (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)). % add other relations | |
| 2774 | check_finite(direct_product(A,B),Hyp,direct_product(PTA,PTB)) :- !, | |
| 2775 | (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)). | |
| 2776 | check_finite(parallel_product(A,B),Hyp,parallel_product(PTA,PTB)) :- !, | |
| 2777 | (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)). | |
| 2778 | check_finite(overwrite(A,B),Hyp,overwrite(PTA,PTB)) :- !, (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)). | |
| 2779 | check_finite(set_subtraction(A,_),Hyps,set_subtraction(PT)) :- !, check_finite(A,Hyps,PT). | |
| 2780 | check_finite(domain_restriction(A,BRel),Hyp,domain_restriction(PT)) :- !, | |
| 2781 | (check_finite(BRel,Hyp,PT) -> true | |
| 2782 | ; check_is_partial_function(BRel,Hyp), check_finite(A,Hyp,PT) | |
| 2783 | ; finite_range(BRel,Hyp,_) -> check_finite(A,Hyp,PT) % finite(a <| brel) if finite(a) & finite(ran(brel)) | |
| 2784 | ). | |
| 2785 | check_finite(domain_subtraction(_,B),Hyp,domain_subtraction(PT)) :- !, check_finite(B,Hyp,PT). | |
| 2786 | check_finite(range_restriction(ARel,B),Hyp,range_restriction(PT)) :- !, | |
| 2787 | (check_finite(ARel,Hyp,PT) -> true | |
| 2788 | ; check_is_injective(ARel,Hyp) -> check_finite(B,Hyp,PT) | |
| 2789 | ; finite_domain(ARel,Hyp,_) -> check_finite(B,Hyp,PT) % finite(arel |> b) if finite(b) & finite(dom(arel)) | |
| 2790 | ). | |
| 2791 | check_finite(range_subtraction(A,_),Hyp,range_subtraction(PT)) :- check_finite(A,Hyp,PT). | |
| 2792 | check_finite(interval(_,_),_,interval) :- !. | |
| 2793 | check_finite(value(V),_,empty_set_value) :- V==[], !. | |
| 2794 | check_finite(value(X),_,avl_set) :- nonvar(X),X=avl_set(_),!. | |
| 2795 | check_finite('$'(ID),Hyps,finite_type) :- | |
| 2796 | get_hyp_var_type(ID,Hyps,Type), %print(chk_fin(ID,Type)),nl, | |
| 2797 | (is_finite_type_for_wd(Type,Hyps) -> true | |
| 2798 | ; Type = set(couple(DomType,_)), % in principle an infinite relation type | |
| 2799 | is_finite_type_for_wd(DomType,Hyps), % we have something like set(couple(boolean,integer)) | |
| 2800 | % note: we treat this here in addition to the case is_partial_function below, as | |
| 2801 | % sometimes we loose the typing information in the term, e.g., in comprehension_set | |
| 2802 | avl_fetch_equal_from_hyps('$'(ID),Hyps,Func,_), | |
| 2803 | is_lambda_function(Func) % we have a function, it is finite if the domain is finite | |
| 2804 | ),!. | |
| 2805 | check_finite('$'(ID),Hyps,enumerated_set) :- | |
| 2806 | enumerated_set(ID), | |
| 2807 | \+ is_hyp_var(ID,Hyps),!. % global enumerated set visible | |
| 2808 | %check_finite('$'(ID),Hyp,partition) :- | |
| 2809 | % avl_fetch_binop_from_hyps('$'(ID),partition,Hyp,Values,Hyp2), % is now normalized | |
| 2810 | % not_occurs(Values,ID), | |
| 2811 | % l_check_finite(Values,Hyp2),!. | |
| 2812 | check_finite('$'(ID),Hyps,rewrite(Operator,PT)) :- | |
| 2813 | (Operator = equal ; Operator = subset), % for subset_strict we also have subset in Hyp | |
| 2814 | avl_fetch_binop_from_hyps('$'(ID),Operator,Hyps,Set2,Hyps2), | |
| 2815 | not_occurs(Set2,ID), % avoid silly, cyclic rewrites $x -> reverse(reverse($x)) (FunLawsStrings.mch) | |
| 2816 | % however, in SetLawsNatural this prevents proving 2 POs due to SS <: min(SS)..max(SS) | |
| 2817 | rewrite_local_loop_check(ID,check_finite,Set2,Hyps2,Hyps3), | |
| 2818 | check_finite(Set2,Hyps3,PT),!. | |
| 2819 | check_finite(Set,Hyp,finite_elements) :- id_or_record_field(Set), | |
| 2820 | avl_fetch_mem_or_struct(Set,Hyp,Set2,Hyp2), | |
| 2821 | Set2 \= Set, | |
| 2822 | has_finite_elements(Set2,Hyp2). | |
| 2823 | check_finite(Func,Hyp,pfun(PTA,PTB)) :- is_partial_function(Func,A,B),!, | |
| 2824 | % a set of partial functions from A to B is finite if both A and B are finite | |
| 2825 | (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)),!. | |
| 2826 | check_finite(Seq,Hyp,seq_type) :- infer_sequence_type_of_expr(Seq,Hyp,_),!. % a sequence is always finite | |
| 2827 | check_finite(struct(rec(Fields)),Hyp,struct) :- !, | |
| 2828 | maplist(check_finite_field(Hyp),Fields). | |
| 2829 | check_finite(general_union(SetOfSets),Hyp,general_union) :- !, | |
| 2830 | check_all_finite(SetOfSets,Hyp). | |
| 2831 | check_finite(general_intersection(SetOfSets),Hyp,general_intersection(PT)) :- !, | |
| 2832 | check_some_finite(SetOfSets,Hyp,PT). | |
| 2833 | check_finite(CompSet,Hyp,comprehension_set) :- is_comprehension_set(CompSet,Paras,Body), | |
| 2834 | finite_comprehension_set(Paras,Body,Hyp),!. | |
| 2835 | % TODO: is_lambda_function_with_domain; improve some proof trees above in style of intersection | |
| 2836 | %check_finite(F,Hyps,_) :- print(check_finite_failed(F)),nl,portray_hyps(Hyps),nl,fail. | |
| 2837 | ||
| 2838 | check_finite_field(Hyp,field(_,Set)) :- check_finite(Set,Hyp,_PT). | |
| 2839 | ||
| 2840 | % we could write a check_all meta_predicate | |
| 2841 | % check if we have a finite set of finite sets; used to determine if union(Sets) is finite | |
| 2842 | check_all_finite(empty_set,_). | |
| 2843 | check_all_finite(empty_sequence,_). | |
| 2844 | check_all_finite(value(avl_set(_AVL)),_Hyp) :- % currently avl_set can only contain finite values for normalisation | |
| 2845 | true. | |
| 2846 | check_all_finite(intersection(A,B),Hyps) :- | |
| 2847 | (check_all_finite(A,Hyps) -> true ; check_all_finite(B,Hyps)). | |
| 2848 | check_all_finite(union(A,B),Hyps) :- | |
| 2849 | (check_all_finite(A,Hyps) -> check_all_finite(B,Hyps)). | |
| 2850 | check_all_finite(sorted_set_extension(L),Hyps) :- !, check_all_finite(set_extension(L),Hyps). | |
| 2851 | check_all_finite(set_extension(L),Hyps) :- | |
| 2852 | (member(Val,L), \+ check_finite(Val,Hyps,_) -> fail % CHECK | |
| 2853 | ; true). | |
| 2854 | check_all_finite('$'(ID),Hyps) :- | |
| 2855 | (Operator = equal ; Operator = subset), % for subset_strict we also have subset in Hyp | |
| 2856 | avl_fetch_binop_from_hyps('$'(ID),Operator,Hyps,Set2,Hyps2), | |
| 2857 | not_occurs(Set2,ID), % avoid silly, cyclic rewrites | |
| 2858 | rewrite_local_loop_check(ID,check_finite,Set2,Hyps2,Hyps3), | |
| 2859 | check_all_finite(Set2,Hyps3),!. | |
| 2860 | check_all_finite(Op,Hyps) :- pow_subset_operator(Op,Set),!, | |
| 2861 | % if Set is finite then all subsets of it are finite and there are only finitely many | |
| 2862 | check_finite(Set,Hyps,_PT). | |
| 2863 | check_all_finite(Op,Hyps) :- iseq_operator(Op,Set),!, | |
| 2864 | % if Set is finite then all injective sequences of it are finite and there are only finitely many | |
| 2865 | check_finite(Set,Hyps,_PT). | |
| 2866 | ||
| 2867 | % check if some set of a set of sets is finite: | |
| 2868 | check_some_finite(sorted_set_extension(L),Hyps,PT) :- !, check_some_finite(set_extension(L),Hyps,PT). | |
| 2869 | check_some_finite(set_extension(L),Hyps,set_extension(PT)) :- | |
| 2870 | (member(Val,L), check_finite(Val,Hyps,PT) -> true). | |
| 2871 | check_some_finite('$'(ID),Hyps,rewrite_id(ID,PT)) :- | |
| 2872 | (Operator = equal ; Operator = superset), % Note: superset not subset as for check_all_finite | |
| 2873 | avl_fetch_binop_from_hyps('$'(ID),Operator,Hyps,Set2,Hyps2), | |
| 2874 | not_occurs(Set2,ID), % avoid silly, cyclic rewrites | |
| 2875 | rewrite_local_loop_check(ID,check_finite,Set2,Hyps2,Hyps3), | |
| 2876 | check_some_finite(Set2,Hyps3,PT),!. | |
| 2877 | %check_some_finite(intersection(A,B),Hyps) :- fail. % Note: the intersection could be empty! | |
| 2878 | check_some_finite(union(A,B),Hyps,union(PT)) :- | |
| 2879 | (check_some_finite(A,Hyps,PT) -> true ; check_some_finite(B,Hyps,PT)). | |
| 2880 | % for pow_subset_operator iseq_operator we would still need to check that the sets are not empty | |
| 2881 | % we cannot currently :prove x<:POW1(INT) & inter({NATURAL}\/x) : FIN(inter({NATURAL}\/x)) | |
| 2882 | ||
| 2883 | ||
| 2884 | pow_subset_operator(fin_subset(X),X). | |
| 2885 | pow_subset_operator(fin1_subset(X),X). | |
| 2886 | pow_subset_operator(pow_subset(X),X). | |
| 2887 | pow_subset_operator(pow1_subset(X),X). | |
| 2888 | iseq_operator(perm(Set),Set). | |
| 2889 | iseq_operator(iseq(Set),Set). | |
| 2890 | iseq_operator(iseq1(Set),Set). | |
| 2891 | ||
| 2892 | ||
| 2893 | is_comprehension_set(comprehension_set(Paras,Body),Paras,Body). | |
| 2894 | is_comprehension_set(value(V),Paras,Body) :- nonvar(V), | |
| 2895 | V=closure(P,_T,Body), % Note: norm_value normalises Body of closures | |
| 2896 | create_dollar_ids(P,Paras). | |
| 2897 | ||
| 2898 | create_dollar_ids([],[]). | |
| 2899 | create_dollar_ids([ID|T],['$'(ID)|TD]) :- create_dollar_ids(T,TD). | |
| 2900 | ||
| 2901 | % Note: lambdas already treated in is_partial_function check above | |
| 2902 | finite_comprehension_set(Paras,Body,Hyp) :- | |
| 2903 | % first exclude the parameters which can be proven finite on their own | |
| 2904 | % now deal with the rest; we do not pass AllParas as second arg; as all references to excluded IDs is ok (only finitely many values possible) | |
| 2905 | finite_comprehension_set_rest(Paras,Body,Hyp,[],Rest), | |
| 2906 | Rest \= Paras, | |
| 2907 | finite_comprehension_set_rest(Rest,Body,Hyp,[],[]). % do a second pass, e.g., for {x,y|x:{y,y+1} & y:1..2 & x:INTEGER} | |
| 2908 | ||
| 2909 | finite_comprehension_set_rest([],_,_,_,[]). | |
| 2910 | % finite_comprehension_set(['$'(ID)|TID],Body,Hyp) :- finite_type ! | |
| 2911 | finite_comprehension_set_rest([ParaID1|TID],Body,Hyp,UnProven,Rest) :- | |
| 2912 | get_parameter_superset_in_body(ParaExpr,[ParaID1|TID],Body,Values), | |
| 2913 | l_not_occurs(Values,UnProven), % do not rely on not yet finitely proven paras; e.g. for {x,y|x:INTEGER & y=x} | |
| 2914 | match_parameter(ParaExpr,ParaID1), | |
| 2915 | check_finite(Values,Hyp,_PT),!, | |
| 2916 | finite_comprehension_set_rest(TID,Body,Hyp,UnProven,Rest). | |
| 2917 | finite_comprehension_set_rest([ParaID1|TID],Body,Hyp,UnProven,[ParaID1|Rest]) :- | |
| 2918 | finite_comprehension_set_rest(TID,Body,Hyp,[ParaID1|UnProven],Rest). | |
| 2919 | ||
| 2920 | % match_parameter(Expr,ID) -> ID occurs in Expr and finite number of values for Expr implies finite values for ID | |
| 2921 | match_parameter(ParaID,ParaID). | |
| 2922 | match_parameter(couple(ParaID,_),ParaID). % x|->y : Values finite implies finitely many values for x | |
| 2923 | match_parameter(couple(_,ParaID),ParaID). | |
| 2924 | match_parameter(set_extension(Ext),ParaID) :- | |
| 2925 | member(El,Ext), match_parameter(El,ParaID). % {x,..} : Values finite implies finitely many values for x | |
| 2926 | match_parameter(sorted_set_extension(Ext),ParaID) :- match_parameter(set_extension(Ext),ParaID). | |
| 2927 | match_parameter(sequence_extension(Ext),ParaID) :- member(ParaID,Ext). | |
| 2928 | match_parameter(rev(RF),ParaID) :- match_parameter(RF,ParaID). | |
| 2929 | match_parameter(reverse(RF),ParaID) :- match_parameter(RF,ParaID). | |
| 2930 | match_parameter(unary_minus(RF),ParaID) :- match_parameter(RF,ParaID). | |
| 2931 | match_parameter(concat(RF1,RF2),ParaID) :- (match_parameter(RF1,ParaID) -> true ; match_parameter(RF2,ParaID)). | |
| 2932 | match_parameter(union(RF1,RF2),ParaID) :- (match_parameter(RF1,ParaID) -> true ; match_parameter(RF2,ParaID)). | |
| 2933 | match_parameter(overwrite(_,RF),ParaID) :- match_parameter(RF,ParaID). % f <+ RF = (... <<| f ) \/ RF | |
| 2934 | match_parameter(Add,ParaID) :- add_with_number(Add,A,_Number), match_parameter(A,ParaID). | |
| 2935 | match_parameter(Mul,ParaID) :- mul_with_number(Mul,nohyps,A,Number), Number \= 0, match_parameter(A,ParaID). | |
| 2936 | % TO DO: more injective functions where a solution determines the ParaID, identity? direct_product, ... | |
| 2937 | % cartesian_product : only if other set not empty | |
| 2938 | ||
| 2939 | get_parameter_superset_in_body(ParaID,AllParas,Body,Values) :- | |
| 2940 | ( member_in_norm_conjunction(Body,member(ParaID,Values)) | |
| 2941 | ; member_in_norm_conjunction(Body,subset(ParaID,Values)) % there are only finitely many subsets of a finite set | |
| 2942 | ; member_in_norm_conjunction(Body,subset_strict(ParaID,Values)) | |
| 2943 | ; member_in_norm_conjunction(Body,equal(X,Y)), | |
| 2944 | sym_unify(X,Y,ParaID,Value), Values=set_extension([Value]) ), | |
| 2945 | l_not_occurs(Values,AllParas). % as an alternative: check for finite_type of set elements; e.g., detect ID=bool(...) | |
| 2946 | ||
| 2947 | ||
| 2948 | :- use_module(probsrc(bsyntaxtree),[is_set_type/2]). | |
| 2949 | %we suppose this has already failed: finite_domain(A,Hyp) :- check_finite(A,Hyp,PT). | |
| 2950 | finite_domain('$'(ID),Hyps,finite_type) :- | |
| 2951 | get_hyp_var_type(ID,Hyps,Type), | |
| 2952 | is_set_type(Type,couple(DomType,_)), | |
| 2953 | is_finite_type_for_wd(DomType,Hyps),!. | |
| 2954 | finite_domain(domain_restriction(A,Rel),Hyps,domain_restriction(PT)) :- !, | |
| 2955 | (check_finite(A,Hyps,PT) -> true ; finite_domain(Rel,Hyps,PT)). | |
| 2956 | finite_domain(A,Hyp,PT) :- get_domain_or_superset(A,Hyp,DA,Hyp2), check_finite(DA,Hyp2,PT). | |
| 2957 | ||
| 2958 | finite_range('$'(ID),Hyps,finite_type) :- | |
| 2959 | get_hyp_var_type(ID,Hyps,Type), | |
| 2960 | is_set_type(Type,couple(_,RanType)), | |
| 2961 | is_finite_type_for_wd(RanType,Hyps),!. | |
| 2962 | finite_range(A,Hyp,PT) :- get_range_or_superset(A,Hyp,RA,Hyp2),!, check_finite(RA,Hyp2,PT). | |
| 2963 | ||
| 2964 | l_check_finite([],_). | |
| 2965 | l_check_finite([H|T],Hyp) :- (check_finite(H,Hyp,_) -> l_check_finite(T,Hyp)). | |
| 2966 | ||
| 2967 | % is a set containing only finite sets | |
| 2968 | has_finite_elements(fin_subset(_),_) :- !. | |
| 2969 | has_finite_elements(fin1_subset(_),_) :- !. | |
| 2970 | has_finite_elements(pow_subset(X),Hyps) :- !, check_finite(X,Hyps,_). | |
| 2971 | has_finite_elements(pow1_subset(X),Hyps) :- !, check_finite(X,Hyps,_). | |
| 2972 | has_finite_elements(seq(_),_) :- !. % every sequence is always finite (of finite length) | |
| 2973 | has_finite_elements(seq1(_),_) :- !. | |
| 2974 | has_finite_elements(iseq(_),_) :- !. | |
| 2975 | has_finite_elements(iseq1(_),_) :- !. | |
| 2976 | has_finite_elements(perm(_),_) :- !. | |
| 2977 | has_finite_elements(union(A,B),Hyps) :- !, has_finite_elements(A,Hyps), has_finite_elements(B,Hyps). | |
| 2978 | has_finite_elements(intersection(A,B),Hyps) :- !, (has_finite_elements(A,Hyps) -> true ; has_finite_elements(B,Hyps)). | |
| 2979 | has_finite_elements(set_subtraction(A,_),Hyps) :- !, has_finite_elements(A,Hyps). | |
| 2980 | has_finite_elements(sorted_set_extension(L),Hyps) :- !, l_check_finite(L,Hyps). | |
| 2981 | has_finite_elements(set_extension(L),Hyps) :- !, l_check_finite(L,Hyps). | |
| 2982 | has_finite_elements(S,_) :- is_empty_set_direct(S),!. % has no elements | |
| 2983 | has_finite_elements(Func,Hyps) :- is_partial_function(Func,A,B),!, | |
| 2984 | (check_finite(A,Hyps,_) -> true ; is_injective(Func), check_finite(B,Hyps,_)). | |
| 2985 | has_finite_elements(Rel,Hyps) :- is_relations_type(Rel,A,B),!,check_finite(A,Hyps,_),check_finite(B,Hyps,_). | |
| 2986 | %has_finite_elements(F,Hs) :- print(has_finite_elements_failed(F)),nl, portray_hyps(Hs),fail. | |
| 2987 | ||
| 2988 | ||
| 2989 | is_relations_type(relations(A,B),A,B). | |
| 2990 | is_relations_type(surjection_relation(A,B),A,B). | |
| 2991 | is_relations_type(total_relation(A,B),A,B). | |
| 2992 | is_relations_type(total_surjection_relation(A,B),A,B). | |
| 2993 | ||
| 2994 | % TO DO: more rules for functions | |
| 2995 | % ------------------------------ | |
| 2996 | ||
| 2997 | :- use_module(probsrc(avl_tools),[avl_fetch_bin/4]). | |
| 2998 | ||
| 2999 | % fetch member(Ground,Free) construct | |
| 3000 | %avl_fetch_mem(Key, AVL ,Res) :- avl_fetch_bin(Key, member, AVL ,Res). | |
| 3001 | %avl_fetch_equal(Key, AVL ,Res) :- avl_fetch_bin(Key, equal, AVL ,Res). | |
| 3002 | ||
| 3003 | ||
| 3004 | avl_fetch_mem_from_hyps(ID,Hyps,Value,Hyps2) :- | |
| 3005 | avl_fetch_binop_from_hyps(ID,member,Hyps,Value,Hyps2). | |
| 3006 | ||
| 3007 | avl_fetch_worthwhile_mem_from_hyps(ID,Hyps,Value,Hyps2) :- | |
| 3008 | avl_fetch_binop_from_hyps(ID,member,Hyps,Value,Hyps2), | |
| 3009 | \+ maximal_set(Value,Hyps2). | |
| 3010 | ||
| 3011 | avl_fetch_equal_from_hyps(ID,Hyps,Value,Hyps2) :- | |
| 3012 | avl_fetch_binop_from_hyps(ID,equal,Hyps,Value,Hyps2). | |
| 3013 | ||
| 3014 | avl_fetch_worthwhile_equal_from_hyps(ID,Hyps,Value,Hyps2) :- | |
| 3015 | worth_rewriting_with_equal(ID), | |
| 3016 | avl_fetch_binop_from_hyps(ID,equal,Hyps,Value,Hyps2), | |
| 3017 | quick_not_occurs_check(ID,Value). | |
| 3018 | ||
| 3019 | avl_fetch_worthwhile_member_from_hyps(ID,Hyps,Value,Hyps2) :- | |
| 3020 | worth_rewriting_with_equal(ID), | |
| 3021 | avl_fetch_binop_from_hyps(ID,member,Hyps,Value,Hyps2). | |
| 3022 | ||
| 3023 | % fetch member predicate or indirect member via record fields | |
| 3024 | avl_fetch_mem_or_struct(Func,Hyps,Function,Hyps1) :- | |
| 3025 | get_type_from_hyps(Func,Hyps,Function,Hyps1). | |
| 3026 | avl_fetch_mem_or_struct(record_field(Rec,Field),Hyps,FieldType,Hyps2) :- | |
| 3027 | get_record_type_fields(Rec,Fields,Hyps,Hyps2), | |
| 3028 | (member(field(Field,FieldType),Fields) -> true). | |
| 3029 | ||
| 3030 | % find record type and extract fields for a given expression | |
| 3031 | get_record_type_fields(function(Func,_),Fields,Hyps,Hyps2) :- | |
| 3032 | get_range_or_superset(Func,Hyps,Range,Hyps1), | |
| 3033 | check_equal_pattern(Range,struct(rec(Fields)),Hyps1,Hyps2). | |
| 3034 | get_record_type_fields(Rec,Fields,Hyps,Hyps2) :- | |
| 3035 | get_type_from_hyps(Rec,Hyps,RecType,Hyps1), | |
| 3036 | check_equal_pattern(RecType,struct(rec(Fields)),Hyps1,Hyps2). | |
| 3037 | ||
| 3038 | % get type from hyps x:XType or x:ran(F) with F : A->B | |
| 3039 | get_type_from_hyps(X,Hyps,XType,Hyps2) :- | |
| 3040 | avl_fetch_mem_from_hyps(X,Hyps,XSet,Hyps1), | |
| 3041 | get_type2(XSet,Hyps1,XType,Hyps2). | |
| 3042 | get_type_from_hyps(function(Func2,_),Hyps,Range,Hyps2) :- | |
| 3043 | % f : _ +-> ( _ >-> _ ) => f(_) : _ >-> _ | |
| 3044 | get_range_or_superset(Func2,Hyps,Range,Hyps2). | |
| 3045 | get_type_from_hyps(second_of_pair(X),Hyps,Type,Hyps2) :- %prj2 | |
| 3046 | get_type_from_hyps(X,Hyps,XType,Hyps1), | |
| 3047 | check_equal_pattern(XType,cartesian_product(_,Type),Hyps1,Hyps2). | |
| 3048 | get_type_from_hyps(first_of_pair(X),Hyps,Type,Hyps2) :- %prj1 | |
| 3049 | get_type_from_hyps(X,Hyps,XType,Hyps1), | |
| 3050 | check_equal_pattern(XType,cartesian_product(Type,_),Hyps1,Hyps2). | |
| 3051 | get_type_from_hyps(assertion_expression(_,_,X),Hyps,XType,Hyps1) :- | |
| 3052 | get_type_from_hyps(X,Hyps,XType,Hyps1). | |
| 3053 | ||
| 3054 | get_type2(domain(Func),Hyps,XType,Hyps2) :- !, | |
| 3055 | get_domain_or_superset(Func,Hyps,XType,Hyps2). | |
| 3056 | get_type2(range(Func),Hyps,XType,Hyps2) :- !, | |
| 3057 | get_range_or_superset(Func,Hyps,XType,Hyps2). | |
| 3058 | get_type2(Type,Hyps,Type,Hyps). | |
| 3059 | ||
| 3060 | id_or_record_field('$'(_)). | |
| 3061 | id_or_record_field(record_field(_,_)). | |
| 3062 | ||
| 3063 | % perform occurs check if first arg is an identifier: | |
| 3064 | quick_not_occurs_check('$'(ID),Value) :- !, not_occurs(Value,ID). | |
| 3065 | quick_not_occurs_check(_,_). | |
| 3066 | ||
| 3067 | % worth rewriting with equality hyps | |
| 3068 | worth_rewriting_with_equal('$'(_)). | |
| 3069 | worth_rewriting_with_equal(record_field('$'(_),_)). | |
| 3070 | worth_rewriting_with_equal(couple(_,_)). | |
| 3071 | worth_rewriting_with_equal(size(_)). | |
| 3072 | worth_rewriting_with_equal(card(_)). | |
| 3073 | worth_rewriting_with_equal(function(_,_)). | |
| 3074 | ||
| 3075 | % utility to fetch fully ground term from hyp avl | |
| 3076 | avl_fetch_from_hyps(Term,hyp_rec(AVL,_)) :- avl_fetch(Term,AVL). | |
| 3077 | ||
| 3078 | % a version without loop check; can be used if processing is finished afterwards | |
| 3079 | avl_fetch_binop_from_hyps_no_loop_check(ID,BinOp,hyp_rec(AVL,_),Value) :- | |
| 3080 | avl_fetch_bin(ID,BinOp,AVL,Value). | |
| 3081 | ||
| 3082 | % lookup a hypothesis ID BinOp Value in logarithmic time; ID and BinOp must be known | |
| 3083 | avl_fetch_binop_from_hyps(ID,BinOp,hyp_rec(AVL,HInfos),Value,hyp_rec(AVL,HInfos2)) :- | |
| 3084 | avl_fetch_bin(ID,BinOp,AVL,Value), | |
| 3085 | (avl_fetch(prevent_cycle_count,HInfos,CycleCount) % avoid cycles x=y, y=x | |
| 3086 | -> (CycleCount < 5 -> true ; % print(prevented_cycle(ID,CycleCount)),nl, | |
| 3087 | % in test 2018: :wd target = [2,1,1,2,1] & n=size(target) & i:1..n & target(i)=res requires cycle count < 5 | |
| 3088 | !, fail), | |
| 3089 | C1 is CycleCount+1 | |
| 3090 | ; C1 is 1 | |
| 3091 | ), | |
| 3092 | avl_store(prevent_cycle_count,HInfos,C1,HInfos2). | |
| 3093 | % detect local loops; should not be used where Hyps are passed to unrelated goals or one has to reset_local_loop_check | |
| 3094 | rewrite_local_loop_check(_,_,Value,HI,HI1) :- useful_value(Value),!,HI1=HI. | |
| 3095 | rewrite_local_loop_check(Term,ProverPredicate,_,Hyps,_) :- var(Hyps),!, | |
| 3096 | add_internal_error('Var hyps: ',rewrite_local_loop_check(Term,ProverPredicate,_,Hyps,_)),fail. | |
| 3097 | rewrite_local_loop_check(Term,ProverPredicate,_,hyp_rec(AVL,HInfos),hyp_rec(AVL,HInfos1)) :- !, | |
| 3098 | (Term='$'(ID) -> true ; ID=Term), | |
| 3099 | %(avl_fetch(rewritten(Term,ProverPredicate),HInfos) -> print(loop(Term,ProverPredicate)),nl,fail ; true), | |
| 3100 | \+ avl_fetch(rewritten(ID,ProverPredicate),HInfos), | |
| 3101 | avl_store(rewritten(ID,ProverPredicate),HInfos,true,HInfos1). | |
| 3102 | % :wd a : 1 .. sz --> INTEGER & sz=5 & p : perm(dom(a)) & i : 1 .. sz - 1 & res= p(i) % sz rewritten multiple times | |
| 3103 | % :wd f: BOOL --> 1..10 & g : 0..20 --> BOOL & bb:BOOL & (f;g)(bb)=res | |
| 3104 | ||
| 3105 | %reset_local_loop_check() | |
| 3106 | ||
| 3107 | % values where there is no risk of looping when rewriting to: | |
| 3108 | useful_value(Value) :- number(Value). | |
| 3109 | useful_value(interval(A,B)) :- number(A), number(B). | |
| 3110 | useful_value(value(_)). | |
| 3111 | ||
| 3112 | ||
| 3113 | % rename and prove a list of goals | |
| 3114 | l_rename_and_prove_goals([],_,_,[]). | |
| 3115 | l_rename_and_prove_goals([H|T],Subst,Hyps,[PTH|PTT]) :- | |
| 3116 | rename_norm_term(H,Subst,RH),!, | |
| 3117 | prove_po(RH,Hyps,PTH),!, % TO DO: use version of prove_po that does not print info | |
| 3118 | l_rename_and_prove_goals(T,Subst,Hyps,PTT). | |
| 3119 | ||
| 3120 | ||
| 3121 | % small utility for sanity checking | |
| 3122 | check_integer(A,PP) :- not_integer(A),!, add_error(PP,'Not an integer: ',A),fail. | |
| 3123 | check_integer(_,_). | |
| 3124 | not_integer(empty_set). | |
| 3125 | not_integer(empty_sequence). | |
| 3126 | not_integer(interval(_,_)). | |
| 3127 | not_integer(couple(_,_)). | |
| 3128 | not_integer(union(_,_)). | |
| 3129 | not_integer(intersection(_,_)). | |
| 3130 | not_integer(domain(_)). | |
| 3131 | not_integer(range(_)). | |
| 3132 | % TO DO: extend | |
| 3133 | ||
| 3134 | ||
| 3135 | % ---------------- | |
| 3136 | ||
| 3137 | % small REPL to inspect hyps | |
| 3138 | :- public hyp_repl/1. | |
| 3139 | hyp_repl(Hyps) :- hyp_repl_prompt(Hyps),read(Term), !, hyp_repl(Term,Hyps). | |
| 3140 | hyp_repl(_). | |
| 3141 | ||
| 3142 | hyp_repl(end_of_file,_). | |
| 3143 | hyp_repl(quit,_). | |
| 3144 | hyp_repl(exit,_). | |
| 3145 | hyp_repl(help,Hyps) :- write('Use quit to exit, print to portray_hyps, or type an identifier to lookup in hyps'),nl, | |
| 3146 | hyp_repl(Hyps). | |
| 3147 | hyp_repl(print,Hyps) :- portray_hyps(Hyps), hyp_repl(Hyps). | |
| 3148 | hyp_repl(ID,Hyps) :- avl_fetch_equal_from_hyps($(ID),Hyps,Value,_), | |
| 3149 | format('Value for ~w:~n ~w~n',[ID,Value]), | |
| 3150 | hyp_repl(Hyps). | |
| 3151 | ||
| 3152 | hyp_repl_prompt(hyp_rec(AVL,HInfos)) :- | |
| 3153 | avl_size(AVL,Size), | |
| 3154 | avl_size(HInfos,ISize),!, | |
| 3155 | format('hyp_rec(#~w,#~w) >>>',[Size,ISize]). | |
| 3156 | hyp_repl_prompt(_) :- write('ILLEGAL HYP_REC >>>'). |