| 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 | | create_intersection([],typeset). % no constraints on identifier: use typeset |
| 987 | | create_intersection([A],Res) :- !, Res=A. |
| 988 | | create_intersection([A|T],intersection(A,Rest)) :- create_intersection(T,Rest). |
| 989 | | |
| 990 | | create_cartesian_product([Type],Res) :- !, Res=Type. |
| 991 | | create_cartesian_product([Type|T],Res) :- create_cartesian_product3(T,Type,Res). |
| 992 | | |
| 993 | | create_cartesian_product3([],Res,Res). |
| 994 | | create_cartesian_product3([Type|T],Acc,Res) :- |
| 995 | | create_cartesian_product3(T,cartesian_product(Acc,Type),Res). |
| 996 | | % Note: dom(%(x,y,z).(x:BOOL & y:1..2 & z:BOOL|1)) = (BOOL*(1..2))*BOOL |
| 997 | | |
| 998 | | % ------------------------ |
| 999 | | |
| 1000 | | % Partial Function Check: |
| 1001 | | |
| 1002 | | % check if Func : Domain +-> Range |
| 1003 | ? | check_is_partial_function_with_type(Func,_,_,Hyps,empty_set(PT)) :- check_equal_empty_set(Func,Hyps,PT),!. |
| 1004 | | check_is_partial_function_with_type(Func,Domain,Range,Hyps,pfun(PTD,PTR)) :- |
| 1005 | ? | check_is_partial_function(Func,Hyps),!, |
| 1006 | ? | (maximal_set(Domain,Hyps) -> PTD=maximal_domain ; check_is_subset(domain(Func),Domain,Hyps,PTD)),!, |
| 1007 | ? | (maximal_set(Range,Hyps) -> PTR=maximal_range ; check_is_subset(range(Func),Range,Hyps,PTR)). |
| 1008 | | |
| 1009 | | % various way to make a function smaller, related to subset |
| 1010 | | function_restriction(domain_subtraction(_,F),F). |
| 1011 | | function_restriction(domain_restriction(_,F),F). |
| 1012 | | function_restriction(range_subtraction(F,_),F). |
| 1013 | | function_restriction(range_restriction(F,_),F). |
| 1014 | | function_restriction(set_subtraction(F,_),F). |
| 1015 | | |
| 1016 | | % check if Func : DomTYPE +-> RanTYPE |
| 1017 | | % check if we can deduce from the Hypotheses that something is a partial function |
| 1018 | | check_is_partial_function(Func,Hyps) :- |
| 1019 | ? | avl_fetch_mem_or_struct(Func,Hyps,Function,Hyps1), |
| 1020 | | % also deals with function(_) f : _ +-> ( _ +-> _ ) => f(_) : _ +-> _ |
| 1021 | ? | is_partial_function_type(Function,Hyps1,_),!. |
| 1022 | | check_is_partial_function(reverse(Func),Hyps) :- |
| 1023 | ? | check_is_injective(Func,Hyps),!. |
| 1024 | | check_is_partial_function(value(avl_set(AVL)),_) :- !, |
| 1025 | | nonvar(AVL), |
| 1026 | | is_avl_partial_function(AVL). |
| 1027 | | check_is_partial_function(composition(F1,F2),Hyp) :- !, |
| 1028 | | % composition of two partial functions is a partial function |
| 1029 | ? | (check_is_partial_function(F1,Hyp) |
| 1030 | ? | -> check_is_partial_function(F2,Hyp) |
| 1031 | | ). |
| 1032 | | check_is_partial_function(overwrite(F1,F2),Hyp) :- !, |
| 1033 | | % overwrite of two partial functions is a partial function |
| 1034 | ? | (check_is_partial_function(F1,Hyp) |
| 1035 | | -> check_is_partial_function(F2,Hyp) |
| 1036 | | ). |
| 1037 | | check_is_partial_function(direct_product(F1,F2),Hyp) :- !, |
| 1038 | | % direct_product of two partial functions is a partial function a:A+->B & b:A+->C => a><b : A+->(B*C) |
| 1039 | | (check_is_partial_function(F1,Hyp) |
| 1040 | | -> check_is_partial_function(F2,Hyp) |
| 1041 | | ). |
| 1042 | | check_is_partial_function(identity(_),_Hyp) :- !. |
| 1043 | | check_is_partial_function(Func,Hyp) :- function_restriction(Func,LargerFunc), !, |
| 1044 | | check_is_partial_function(LargerFunc,Hyp). |
| 1045 | | check_is_partial_function(intersection(F1,F2),Hyp) :- !, |
| 1046 | | (check_is_partial_function(F1,Hyp) -> true ; check_is_partial_function(F2,Hyp)). |
| 1047 | | check_is_partial_function(sorted_set_extension(List),Hyp) :- !, |
| 1048 | | check_set_extension_is_partial_function(List,Hyp). |
| 1049 | | check_is_partial_function(set_extension(List),Hyp) :- !, |
| 1050 | | check_set_extension_is_partial_function(List,Hyp). |
| 1051 | | check_is_partial_function(Expr,_) :- |
| 1052 | ? | is_lambda_function(Expr),!. % also treats cartesian_product and sequence_extension |
| 1053 | | % check_is_partial_function(X,_Hyp) :- is_empty_set_direct(X),!. % covered by infer_sequence_type_of_expr below |
| 1054 | | check_is_partial_function(Expr,Hyps) :- |
| 1055 | ? | infer_sequence_type_of_expr(Expr,Hyps,_),!. % any sequence expression is a partial function; e.g. a <- b, front(.) |
| 1056 | ? | check_is_partial_function(Func,Hyps) :- rewrite_set_expression_exact(Func,Hyps,NewFunc,Hyps2),!, |
| 1057 | | check_is_partial_function(NewFunc,Hyps2). |
| 1058 | | check_is_partial_function(union(F1,F2),Hyps) :- |
| 1059 | | check_is_subset(F1,F2,Hyps,_),!, |
| 1060 | | check_is_partial_function(F2,Hyps). |
| 1061 | | check_is_partial_function(union(F1,F2),Hyps) :- |
| 1062 | | check_is_subset(F2,F1,Hyps,_),!, |
| 1063 | | check_is_partial_function(F1,Hyps). |
| 1064 | | check_is_partial_function(union(F1,F2),Hyps) :- !, |
| 1065 | | check_domain_disjoint(F1,F2,Hyps,Hyps2), % domain must be disjoint, not F1 and F2 |
| 1066 | | check_is_partial_function(F1,Hyps2), |
| 1067 | | check_is_partial_function(F2,Hyps2). |
| 1068 | | check_is_partial_function(Func,Hyps) :- % f<:g & g: A +-> B => f : A +-> B |
| 1069 | | (Op = equal ; Op = subset), |
| 1070 | ? | avl_fetch_binop_from_hyps(Func,Op,Hyps,Func2,Hyps1), |
| 1071 | | quick_not_occurs_check(Func,Func2), |
| 1072 | ? | check_is_partial_function(Func2,Hyps1). |
| 1073 | | %check_is_partial_function(Func,_) :- print(check_is_partial_function_failed(Func)),nl,fail. |
| 1074 | | |
| 1075 | | check_domain_disjoint(F1,F2,Hyps,Hyps2) :- |
| 1076 | | compute_exact_domain(F1,Hyps,DF1,Hyps2), |
| 1077 | | % example: :prove f:BOOL +-> BOOL & x /: dom(f) => f \/ {x|->TRUE} : BOOL +-> BOOL |
| 1078 | | is_set_extension(DF1,List1),!, |
| 1079 | | l_check_not_member_of_set(List1,domain(F2),Hyps2). % we could try and compute domain(F2) first |
| 1080 | | check_domain_disjoint(F2,F1,Hyps,Hyps2) :- |
| 1081 | | compute_exact_domain(F1,Hyps,DF1,Hyps2), |
| 1082 | | is_set_extension(DF1,List1),!, |
| 1083 | | l_check_not_member_of_set(List1,domain(F2),Hyps2). |
| 1084 | | check_domain_disjoint(F1,F2,Hyps,Hyps2) :- |
| 1085 | ? | get_domain_or_superset(F1,Hyps,DomFunc1,Hyps1), |
| 1086 | | get_domain_or_superset(F2,Hyps1,DomFunc2,Hyps2), |
| 1087 | | check_disjoint(DomFunc1,DomFunc2,Hyps2). |
| 1088 | | |
| 1089 | | |
| 1090 | | % check if this is a partial function type or something defined to be equal to a function type |
| 1091 | | :- if(environ(prob_safe_mode,true)). |
| 1092 | | is_partial_function_type(P,H,H1) :- nonvar(H1), |
| 1093 | | add_internal_error('Illegal hyps:',is_partial_function_type(P,H,H1)),fail. |
| 1094 | | :- endif. |
| 1095 | | is_partial_function_type(PF,Hyps,Hyps1) :- is_partial_function(PF,_,_),!,Hyps1=Hyps. |
| 1096 | | is_partial_function_type(range(Func),Hyps,Hyps2) :- |
| 1097 | ? | get_range_or_superset(Func,Hyps,RanFunc,Hyps1),!, |
| 1098 | | is_partial_function_type(RanFunc,Hyps1,Hyps2). |
| 1099 | | is_partial_function_type(domain(Func),Hyps,Hyps2) :- |
| 1100 | | get_domain_or_superset(Func,Hyps,DomFunc,Hyps1),!, |
| 1101 | | is_partial_function_type(DomFunc,Hyps1,Hyps2). |
| 1102 | | is_partial_function_type(sorted_set_extension(Funcs),Hyps,Hyps2) :- !, |
| 1103 | | is_partial_function_type(set_extension(Funcs),Hyps,Hyps2). |
| 1104 | | is_partial_function_type(set_extension(Funcs),Hyps,Hyps2) :- !, |
| 1105 | ? | (member(F,Funcs), \+ check_is_partial_function(F,Hyps) -> fail |
| 1106 | | ; Hyps2=Hyps). % all elements of Funcs are partial functions |
| 1107 | | is_partial_function_type(Func,Hyps,Hyps2) :- |
| 1108 | ? | get_superset(Func,Hyps,SuperSet,Hyps1),!, |
| 1109 | ? | is_partial_function_type(SuperSet,Hyps1,Hyps2). |
| 1110 | | is_partial_function_type(PF,Hyps,Hyps2) :- |
| 1111 | ? | avl_fetch_worthwhile_equal_from_hyps(PF,Hyps,PF2,Hyps1), % in case we have a definition like X = 1..n --> R |
| 1112 | ? | is_partial_function_type(PF2,Hyps1,Hyps2). |
| 1113 | | |
| 1114 | | % get worthwhile superset |
| 1115 | | get_superset(set_subtraction(A,_),Hyps,R,Hyps) :- !, R=A. |
| 1116 | | get_superset(intersection(A,B),Hyps,R,Hyps) :- !, (R=A ; R=B). |
| 1117 | | get_superset(CompSet,Hyps,Set,Hyps) :- is_comprehension_set(CompSet,[ID],Body),!, |
| 1118 | ? | get_parameter_superset_in_body(ID,[ID],Body,Set). |
| 1119 | | |
| 1120 | | is_partial_function(total_function(A,B),A,B). |
| 1121 | | is_partial_function(partial_function(A,B),A,B). |
| 1122 | | is_partial_function(total_injection(A,B),A,B). |
| 1123 | | is_partial_function(partial_injection(A,B),A,B). |
| 1124 | | is_partial_function(total_surjection(A,B),A,B). |
| 1125 | | is_partial_function(partial_surjection(A,B),A,B). |
| 1126 | | is_partial_function(total_bijection(A,B),A,B). |
| 1127 | | is_partial_function(partial_bijection(A,B),A,B). |
| 1128 | | is_partial_function(perm(A),'NATURAL1',A). |
| 1129 | | is_partial_function(seq(B),'NATURAL1',B). |
| 1130 | | is_partial_function(seq1(B),'NATURAL1',B). |
| 1131 | | is_partial_function(iseq(B),'NATURAL1',B). |
| 1132 | | is_partial_function(iseq1(B),'NATURAL1',B). |
| 1133 | | |
| 1134 | | % if First = f(1,GS) -> we can check if function is total; we could store summary of set_extension in hyps |
| 1135 | | check_set_extension_is_partial_function([_],_) :- !. % one element set extension is a function |
| 1136 | | check_set_extension_is_partial_function(List,Hyps) :- |
| 1137 | ? | maplist(get_explicit_dom_value(Hyps),List,VList),!, |
| 1138 | | sort(VList,SList), |
| 1139 | | SList = [couple(First,_)|TS], |
| 1140 | | check_set_ext_pf(TS,First,Hyps). |
| 1141 | | check_set_extension_is_partial_function([couple(A,_),couple(B,_)],Hyps) :- |
| 1142 | | check_not_equal(A,B,Hyps). % TO DO: all_different for longer lists |
| 1143 | | |
| 1144 | | check_set_ext_pf([],_,_). |
| 1145 | | check_set_ext_pf([couple(Next,_)|TS],Last,Hyp) :- |
| 1146 | | Next \= Last, |
| 1147 | | check_set_ext_pf(TS,Next,Hyp). |
| 1148 | | |
| 1149 | ? | get_explicit_dom_value(Hyps,couple(Val,RanVal),couple(Val2,RanVal)) :- get_explicit_value(Val,Hyps,Val2). |
| 1150 | | |
| 1151 | | get_explicit_value(couple(A,B),Hyps,couple(A2,B2)) :- !, |
| 1152 | | get_explicit_value(A,Hyps,A2), get_explicit_value(B,Hyps,B2). |
| 1153 | | get_explicit_value(rec(Fields),Hyps,rec(SFields2)) :- !, |
| 1154 | | maplist(get_field_value(Hyps),Fields,Fields2), |
| 1155 | | sort(Fields2,SFields2). |
| 1156 | ? | get_explicit_value(Val,Hyps,R) :- is_explicit_value(Val,AVal,Hyps),!,R=AVal. |
| 1157 | | get_explicit_value('$'(ID),Hyps,Res) :- |
| 1158 | ? | avl_fetch_equal_from_hyps('$'(ID),Hyps,Val2,Hyps2), |
| 1159 | | is_explicit_value(Val2,Res,Hyps2). % should we allow recursion through multiple equations? |
| 1160 | | |
| 1161 | | % is value which can be compared using Prolog equality |
| 1162 | | % cf. avl_can_fetch |
| 1163 | | is_explicit_value(boolean_true,pred_true,_). |
| 1164 | | is_explicit_value(boolean_false,pred_false,_). |
| 1165 | | is_explicit_value(Nr,Nr,_) :- number(Nr). % integers and floats |
| 1166 | | is_explicit_value(integer(Nr),Nr,_) :- integer(Nr). % normally already replaced by norm_expr2 |
| 1167 | | is_explicit_value(string(Atom),Atom,_). |
| 1168 | | is_explicit_value(real(Atom),Res,_) :- atom(Atom), |
| 1169 | | construct_real(Atom,term(floating(Res))). % c.f. is_real/1 in kernel_reals |
| 1170 | | is_explicit_value(couple(A,B),(AV,BV),Hyp) :- is_explicit_value(A,AV,Hyp), is_explicit_value(B,BV,Hyp). |
| 1171 | | is_explicit_value('$'(ID),'$'(ID),Hyp) :- is_global_constant_id(ID,Hyp). |
| 1172 | | is_explicit_value(value(R),Nr,_) :- nonvar(R), R=int(Nr), integer(Nr). % TODO: more values, strings, reals, ... |
| 1173 | | |
| 1174 | | |
| 1175 | | get_field_value(Hyps,field(Name,Val),field(Name,Val2)) :- get_explicit_value(Val,Hyps,Val2). |
| 1176 | | |
| 1177 | | :- use_module(probsrc(b_global_sets), [lookup_global_constant/2]). |
| 1178 | | % enumerated set element name |
| 1179 | | is_global_constant_id(ID,Hyp) :- |
| 1180 | | lookup_global_constant(ID,_), |
| 1181 | | \+ is_hyp_var(ID,Hyp). % global enumerated set constant visible |
| 1182 | | |
| 1183 | | is_enumerated_set(ID,Hyp) :- |
| 1184 | | enumerated_set(ID), |
| 1185 | | \+ is_hyp_var(ID,Hyp). % global enumerated set constant visible |
| 1186 | | |
| 1187 | | % Disjoint check: |
| 1188 | | check_disjoint(interval(Low1,Up1),interval(Low2,Up2),Hyps) :- !, |
| 1189 | | (check_less(Up1,Low2,Hyps) -> true ; check_less(Up2,Low1,Hyps) -> true |
| 1190 | | ; check_less(Up1,Low1,Hyps) -> true ; check_less(Up2,Low2,Hyps) -> true). |
| 1191 | | check_disjoint(A,B,Hyps) :- %print(disj(A,B)),nl, portray_hyps(Hyps),nl, |
| 1192 | ? | (check_disjoint_aux(A,B,Hyps) -> true ; check_disjoint_aux(B,A,Hyps)). |
| 1193 | | |
| 1194 | | check_disjoint_aux(S,_,Hyps) :- check_equal_empty_set(S,Hyps,_),!. |
| 1195 | | check_disjoint_aux(A,B,Hyps) :- |
| 1196 | | avl_fetch_from_hyps(equal(intersection(A,B),empty_set),Hyps),!. |
| 1197 | | check_disjoint_aux(domain_subtraction(A,_),B,Hyps) :- !, % A <<| f /\ B = {} if dom(B) <: A |
| 1198 | | get_domain_or_superset(B,Hyps,DomB,Hyps2), |
| 1199 | | check_is_subset(DomB,A,Hyps2,_). |
| 1200 | | check_disjoint_aux(set_subtraction(AA,A),B,Hyps) :- !, |
| 1201 | | (check_is_subset(B,A,Hyps,_) -> true % x \ A /\ B = {} if B <: A |
| 1202 | | ; check_disjoint(AA,B,Hyps) -> true). % AA-A /\ B ={} if AA /\ B = {} |
| 1203 | | check_disjoint_aux(set_extension(As),B,Hyps) :- !, l_check_not_member_of_set(As,B,Hyps). |
| 1204 | | check_disjoint_aux(sorted_set_extension(As),B,Hyps) :- !, l_check_not_member_of_set(As,B,Hyps). |
| 1205 | | check_disjoint_aux(domain(Func),B,Hyps) :- !, |
| 1206 | ? | get_domain_or_superset(Func,Hyps,DomFunc,Hyps2), |
| 1207 | | check_disjoint(DomFunc,B,Hyps2). |
| 1208 | | check_disjoint_aux(range(Func),B,Hyps) :- !, |
| 1209 | ? | get_range_or_superset(Func,Hyps,RanFunc,Hyps2), |
| 1210 | ? | check_disjoint(RanFunc,B,Hyps2). |
| 1211 | | check_disjoint_aux(A,B,Hyps) :- |
| 1212 | ? | avl_fetch_worthwhile_equal_from_hyps(A,Hyps,A1,Hyps1), |
| 1213 | ? | check_disjoint(A1,B,Hyps1). |
| 1214 | | % TO DO: move union of set_extension here? |
| 1215 | | |
| 1216 | | l_check_not_member_of_set([],_,_). |
| 1217 | | l_check_not_member_of_set([El|T],Set,Hyps) :- |
| 1218 | | check_not_member_of_set(Set,El,Hyps,_PT), |
| 1219 | | l_check_not_member_of_set(T,Set,Hyps). |
| 1220 | | |
| 1221 | | % Injective check: |
| 1222 | | |
| 1223 | | check_is_injective(Func,Hyps) :- |
| 1224 | ? | get_type_from_hyps(Func,Hyps,Function,Hyps1), |
| 1225 | | %print(check_rev_fun(Func,Function)),nl, |
| 1226 | | is_injective_function_type(Function,Hyps1,_). |
| 1227 | | check_is_injective(value(avl_set(AVL)),_) :- !, |
| 1228 | | nonvar(AVL), invert_explicit_set(avl_set(AVL),Inv), |
| 1229 | | Inv=avl_set(AVL2), is_avl_partial_function(AVL2). |
| 1230 | | check_is_injective(identity(_),_). |
| 1231 | | check_is_injective(Set,_) :- singleton_set(Set,_). % TO DO: extend to more than singleton set_extension |
| 1232 | | check_is_injective(sequence_extension([_]),_). % TO DO: check all elements are different |
| 1233 | | check_is_injective(Func, Hyps) :- |
| 1234 | ? | avl_fetch_equal_from_hyps(Func,Hyps,Value,Hyps2), |
| 1235 | | %print(check_inj_value(Func,Value)),nl, |
| 1236 | ? | check_is_injective(Value,Hyps2). |
| 1237 | | |
| 1238 | | % check if this is a partial function type or something defined to be equal to a function type |
| 1239 | | is_injective_function_type(PF,Hyps,Hyps1) :- is_injective(PF),!,Hyps1=Hyps. |
| 1240 | | is_injective_function_type(PF,Hyps,Hyps2) :- |
| 1241 | | avl_fetch_worthwhile_equal_from_hyps(PF,Hyps,PF2,Hyps1), % in case we have a definition like X = 1..n --> R |
| 1242 | | is_injective_function_type(PF2,Hyps1,Hyps2). |
| 1243 | | |
| 1244 | | is_injective(total_injection(_,_)). |
| 1245 | | is_injective(partial_injection(_,_)). |
| 1246 | | is_injective(total_bijection(_,_)). |
| 1247 | | is_injective(partial_bijection(_,_)). |
| 1248 | | is_injective(iseq(_)). |
| 1249 | | is_injective(iseq1(_)). |
| 1250 | | |
| 1251 | | % A /<: B <=> A/<<: B & A /= B |
| 1252 | | |
| 1253 | | check_not_subset(Sub,Super,Hyps,not_subset_interval) :- % R..S /<: X..Y |
| 1254 | | is_interval(Sub,Hyps,R,S), |
| 1255 | | is_interval(Super,Hyps,X,Y),!, |
| 1256 | | check_not_subset_interval(R,S,X,Y,Hyps). |
| 1257 | | check_not_subset(A,B,Hyps,PT) :- |
| 1258 | ? | check_not_is_subset_strict(A,B,Hyps,PT),!, |
| 1259 | | check_not_equal(A,B,Hyps). |
| 1260 | | |
| 1261 | | check_not_subset_interval(R,S,X,Y,Hyps) :- |
| 1262 | | check_not_empty_interval(R,S,Hyps), !, % empty set is always a subset |
| 1263 | | (check_less(Y,S,Hyps) -> true % interval extends right beyond Y |
| 1264 | | ; check_less(R,X,Hyps) -> true % interval extends left beyond X |
| 1265 | | ). |
| 1266 | | |
| 1267 | | check_not_empty_interval(Low,Up,Hyps) :- check_leq(Low,Up,Hyps). |
| 1268 | | |
| 1269 | | % check_not_is_subset_strict(A,B,Hyps,PT) check if A is not a strict subset of B |
| 1270 | | % not really used for WD proofs at the moment; mainly as top-level goal in prove_po |
| 1271 | | % (now used for proving set_subtraction is not empty; test 2469) |
| 1272 | | % probably quite a few more rules necessary to make it useful |
| 1273 | | check_not_is_subset_strict(A,B,Hyps,hyp) :- |
| 1274 | | avl_fetch_from_hyps(not_subset_strict(A,B),Hyps),!. % hyp; currently not marked as useful by default! |
| 1275 | | check_not_is_subset_strict(A,B,Hyps,hyp2) :- |
| 1276 | | avl_fetch_from_hyps(not_subset(A,B),Hyps),!. % not(A <: B) => not (A<<:B) |
| 1277 | | check_not_is_subset_strict(A,B,Hyps,equal_not_subset_strict) :- |
| 1278 | | check_equal(A,B,Hyps,_),!. % A=B => not (A<<:B) |
| 1279 | | check_not_is_subset_strict(_,B,Hyps,empty_set(PT)) :- % A /<<: {} |
| 1280 | ? | check_equal_empty_set(B,Hyps,PT). |
| 1281 | | check_not_is_subset_strict(Sub,Super,Hyps,not_subset_interval) :- % R..S /<: X..Y => R..S /<<: X..Y |
| 1282 | | is_interval(Sub,Hyps,R,S), |
| 1283 | | is_interval(Super,Hyps,X,Y),!, |
| 1284 | | check_not_subset_interval(R,S,X,Y,Hyps). |
| 1285 | | check_not_is_subset_strict(MAX,_,Hyps,maximal_set) :- % MAX /<<: B |
| 1286 | ? | maximal_set(MAX,Hyps),!. |
| 1287 | | check_not_is_subset_strict(A,B,Hyps,not_empty_singleton(PT)) :- % x <<: {A} <=> x={} |
| 1288 | | singleton_set(B,_),!, |
| 1289 | ? | check_not_equal_empty_set(A,Hyps,PT). |
| 1290 | | check_not_is_subset_strict(A,B,Hyps,infinite_sub(PT)) :- |
| 1291 | | infinite_integer_set(A,Hyps), % TODO: accept more infinite sets |
| 1292 | | check_finite(B,Hyps,PT),!. |
| 1293 | | check_not_is_subset_strict(A,B,Hyps,superset_eq1(PT)) :- |
| 1294 | | (Operator = equal ; Operator = superset), % A :> S2 & S2 /<<: B => A /<<: B |
| 1295 | ? | avl_fetch_binop_from_hyps(A,Operator,Hyps,S2,Hyps2), |
| 1296 | | rewrite_local_loop_check(A,check_not_is_subset_strict,S2,Hyps2,Hyps3), |
| 1297 | | check_not_is_subset_strict(S2,B,Hyps3,PT),!. |
| 1298 | | check_not_is_subset_strict(A,B,Hyps,subset_eq2(PT)) :- |
| 1299 | | (Operator = equal ; Operator = subset), % B <: S2 & A /<<: S2 => A /<<: B |
| 1300 | ? | avl_fetch_binop_from_hyps(B,Operator,Hyps,S2,Hyps2), |
| 1301 | | rewrite_local_loop_check(B,check_not_is_subset_strict,S2,Hyps2,Hyps3), |
| 1302 | | check_not_is_subset_strict(A,S2,Hyps3,PT),!. |
| 1303 | | %check_not_is_subset_strict(A,B,H,_) :- print(check_not_is_subset_strict_failed(A,B)),nl, portray_hyps(H),nl,fail. |
| 1304 | | |
| 1305 | | |
| 1306 | | check_is_subset_strict(A,B,Hyp,empty_singleton(PT)) :- % x <<: {A} <=> x={} |
| 1307 | | singleton_set(B,_),!, |
| 1308 | | check_equal_empty_set(A,Hyp,PT). |
| 1309 | | check_is_subset_strict(A,B,Hyp,PT) :- % A <<: B <=> A <: B & A /= B |
| 1310 | ? | check_is_subset(A,B,Hyp,PT),!, |
| 1311 | | check_not_equal(A,B,Hyp). |
| 1312 | | |
| 1313 | | % check if something is a subset of something else |
| 1314 | | check_is_subset(H,H,_,equal). |
| 1315 | | check_is_subset(A,B,Hyps,hyp) :- |
| 1316 | | avl_fetch_from_hyps(subset(A,B),Hyps),!. % hyp |
| 1317 | ? | check_is_subset(_,MAX,Hyps,maximal_set) :- maximal_set(MAX,Hyps),!. |
| 1318 | ? | check_is_subset(S,_,Hyps,empty_set(PT)) :- check_equal_empty_set(S,Hyps,PT),!. % {} <: B |
| 1319 | | check_is_subset(cartesian_product(A,B),cartesian_product(A2,B2),Hyps,cart(PTA,PTB)) :- !, |
| 1320 | | % A <: A2 & B <: B2 => (A*B) <: (A2*B2) |
| 1321 | ? | (check_is_subset(A,A2,Hyps,PTA) |
| 1322 | ? | -> check_is_subset(B,B2,Hyps,PTB)). |
| 1323 | | check_is_subset('NATURAL1','NATURAL',_,nat1_nat) :- !. |
| 1324 | ? | check_is_subset(interval(L,U),B,Hyps,interval(PT)) :- !, check_subset_interval(B,L,U,Hyps,PT). |
| 1325 | | check_is_subset(intersection(A,B),Super,Hyps,intersection(PT)) :- !, |
| 1326 | ? | ( check_is_subset(A,Super,Hyps,PT) -> true ; check_is_subset(B,Super,Hyps,PT)). |
| 1327 | | check_is_subset(union(A,B),Super,Hyps,union(PTA,PTB)) :- !, |
| 1328 | ? | ( check_is_subset(A,Super,Hyps,PTA) -> check_is_subset(B,Super,Hyps,PTB)). |
| 1329 | | check_is_subset(domain_subtraction(_,B),Super,Hyps,dom_sub(PT)) :- !,check_is_subset(B,Super,Hyps,PT). |
| 1330 | | check_is_subset(domain_restriction(_,B),Super,Hyps,dom_res(PT)) :- !,check_is_subset(B,Super,Hyps,PT). |
| 1331 | | check_is_subset(range_subtraction(A,_),Super,Hyps,ran_sub(PT)) :- !,check_is_subset(A,Super,Hyps,PT). |
| 1332 | ? | check_is_subset(range_restriction(A,_),Super,Hyps,ran_res(PT)) :- !,check_is_subset(A,Super,Hyps,PT). |
| 1333 | ? | check_is_subset(set_subtraction(A,_),Super,Hyps,set_sub(PT)) :- !,check_is_subset(A,Super,Hyps,PT). |
| 1334 | | check_is_subset(value(avl_set(AVL)),B,Hyps,avl) :- !,check_subset_avl(B,AVL,Hyps). |
| 1335 | | check_is_subset(A,B,Hyps,subset_eq(PT)) :- |
| 1336 | | (Operator = equal ; Operator = subset), % for subset_strict we also have subset in Hyps |
| 1337 | ? | avl_fetch_binop_from_hyps(A,Operator,Hyps,S2,Hyps2), |
| 1338 | | rewrite_local_loop_check(A,check_is_subset,S2,Hyps2,Hyps3), |
| 1339 | ? | check_is_subset(S2,B,Hyps3,PT),!. |
| 1340 | | check_is_subset(A,B,Hyps,subset_eq_r(PT)) :- |
| 1341 | ? | avl_fetch_binop_from_hyps(B,equal,Hyps,S2,Hyps2), % also superset? |
| 1342 | | rewrite_local_loop_check(B,check_is_subset,S2,Hyps2,Hyps3), |
| 1343 | ? | check_is_subset(A,S2,Hyps3,PT),!. |
| 1344 | | check_is_subset('$'(ID),B,Hyps,eq(ID,PT)) :- |
| 1345 | ? | get_type_from_hyps('$'(ID),Hyps,Set,Hyps2), |
| 1346 | | extract_element_super_set_type(Set,Hyps2,S2), |
| 1347 | | rewrite_local_loop_check(ID,check_is_subset,S2,Hyps2,Hyps3), |
| 1348 | ? | check_is_subset(S2,B,Hyps3,PT),!. |
| 1349 | | check_is_subset(domain(Func),B,Hyps,domain(PT)) :- |
| 1350 | ? | get_domain_or_superset(Func,Hyps,DomFunc,Hyps2), |
| 1351 | | %rewrite_local_loop_check(domain(Func),check_is_subset,DomFunc,Hyps2,Hyps3), |
| 1352 | ? | check_is_subset(DomFunc,B,Hyps2,PT),!. |
| 1353 | | check_is_subset(range(Func),B,Hyps,range(PT)) :- |
| 1354 | ? | get_range_or_superset(Func,Hyps,RanFunc,Hyps2), |
| 1355 | | %rewrite_local_loop_check(range(Func),check_is_subset,RanFunc,Hyps2,Hyps3), |
| 1356 | ? | check_is_subset(RanFunc,B,Hyps2,PT),!. |
| 1357 | | check_is_subset(function(Func,_),B,Hyps,function_range(PT)) :- !, |
| 1358 | ? | get_range_or_superset(Func,Hyps,RanFunc,Hyps2), % f : _ +-> POW(Ran) & Ran <: B => f(.) <: B |
| 1359 | | subset_transitivity_rule(RanFunc,pow_subset(B),A2,B2), % extract pow_subset from Range |
| 1360 | ? | check_is_subset(A2,B2,Hyps2,PT). |
| 1361 | | check_is_subset(image(Func,_),B,Hyps,image(PT)) :- % or B=range(Range) |
| 1362 | | (B = range(FuncB),check_equal(Func,FuncB,Hyps,_) -> !, PT=range_of_same_func % f[.] <: ran(f) |
| 1363 | ? | ; get_range_or_superset(Func,Hyps,Range,Hyps2) -> !, check_is_subset(Range,B,Hyps2,PT)). |
| 1364 | ? | check_is_subset(A,B,Hyps,transitivity(PT)) :- subset_transitivity_rule(A,B,A2,B2), |
| 1365 | | !, % unary subset rules like POW(A2) <: POW(B2) if A2 <: B2 |
| 1366 | ? | check_is_subset(A2,B2,Hyps,PT). |
| 1367 | ? | check_is_subset(A,B,Hyps,transitivity(PT1,PT2)) :- subset_bin_transitivity_rule(A,B,A1,A2,B1,B2), |
| 1368 | | !, % binary subset rules like A1+->B1 <: A2+->B2 if A1 <:B1 & A2 <: B2 |
| 1369 | ? | (check_is_subset(A1,B1,Hyps,PT1) -> check_is_subset(A2,B2,Hyps,PT2)). |
| 1370 | | check_is_subset(sorted_set_extension(List),B,Hyps,PT) :- !, |
| 1371 | ? | check_is_subset(set_extension(List),B,Hyps,PT). |
| 1372 | | check_is_subset(set_extension(List),B,Hyps,set_extension) :- |
| 1373 | | simplify_expr(B,Hyps,BS), % simplify expression once |
| 1374 | | %portray_hyps(Hyps),nl, |
| 1375 | | l_check_is_member(List,BS,Hyps). |
| 1376 | | check_is_subset(Sub,union(A,B),Hyps,sub_union(PT)) :- !, |
| 1377 | ? | ( check_is_subset(Sub,A,Hyps,PT) -> true ; check_is_subset(Sub,B,Hyps,PT)). |
| 1378 | | % get_set_of_possible_values; treat sequence_extension |
| 1379 | | check_is_subset(CompSet,B,Hyps,comprehension_set(PT)) :- |
| 1380 | | is_comprehension_set(CompSet,[ID],Pred), |
| 1381 | ? | get_conjunct(Pred,Conjunct), % TODO: also allow comprehension sets with multiple ids? |
| 1382 | | get_member(Conjunct,ID,A), |
| 1383 | | % we could do findall and then union |
| 1384 | | ID = $(ID1), \+ occurs(A,ID1), |
| 1385 | ? | check_is_subset(A,B,Hyps,PT). |
| 1386 | | % check_is_subset(A,B,_,_) :- print(check_is_subset_failed(A,B)),nl,nl,fail. |
| 1387 | | |
| 1388 | | get_member(member(LHS,RHS),LHS,RHS). |
| 1389 | | get_member(subset(LHS,RHS),LHS,pow_subset(RHS)). |
| 1390 | | get_member(subset_strict(LHS,RHS),LHS,pow_subset(RHS)). |
| 1391 | | |
| 1392 | | |
| 1393 | | l_check_is_member([],_,_). |
| 1394 | | l_check_is_member([El|T],B,Hyps) :- |
| 1395 | ? | check_member_of_set(B,El,Hyps,_ProofTree),!, |
| 1396 | | l_check_is_member(T,B,Hyps). |
| 1397 | | |
| 1398 | | % extract set type of the elements of a set: x: POW(A) ==> x<:A |
| 1399 | | extract_element_super_set_type(FuncType,Hyps,cartesian_product(A,B)) :- |
| 1400 | | get_possible_domain_of_func_or_rel_type(FuncType,Hyps,A,_),!, |
| 1401 | | get_possible_range_of_func_or_rel_type_direct(FuncType,B,_). |
| 1402 | | extract_element_super_set_type(fin_subset(A),_,A). |
| 1403 | | extract_element_super_set_type(fin1_subset(A),_,A). |
| 1404 | | extract_element_super_set_type(pow_subset(A),_,A). |
| 1405 | | extract_element_super_set_type(pow1_subset(A),_,A). |
| 1406 | | |
| 1407 | | |
| 1408 | | % simple not member of set check |
| 1409 | | check_not_member_of_set(Set,_,Hyps,empty_set) :- check_equal_empty_set(Set,Hyps,_),!. |
| 1410 | | check_not_member_of_set(Set,El,Hyps,hyp) :- |
| 1411 | | avl_fetch_from_hyps(not_member(El,Set),Hyps),!. % hyp |
| 1412 | | check_not_member_of_set(if_then_else(Pred,A,B),El,Hyps,if_then_else(PTA,PTB)) :- |
| 1413 | | push_and_rename_normalized_hyp(Pred,Hyps,Hyps1), |
| 1414 | | (hyps_inconsistent(Hyps1) -> true ; check_not_member_of_set(A,El,Hyps1,PTA) -> true), |
| 1415 | | push_and_rename_normalized_hyp(negation(Pred),Hyps,Hyps2), |
| 1416 | | (hyps_inconsistent(Hyps2) -> true ; check_not_member_of_set(B,El,Hyps2,PTB) -> true),!. |
| 1417 | | check_not_member_of_set(intersection(A,B),El,Hyps,inter(PT)) :- |
| 1418 | | (check_not_member_of_set(A,El,Hyps,PT) -> true ; check_not_member_of_set(B,El,Hyps,PT)),!. |
| 1419 | | check_not_member_of_set(set_subtraction(A,B),El,Hyps,inter(PT)) :- |
| 1420 | ? | (check_not_member_of_set(A,El,Hyps,PT) -> true ; check_member_of_set(B,El,Hyps,PT)),!. |
| 1421 | | check_not_member_of_set(union(A,B),El,Hyps,inter(PTA,PTB)) :- |
| 1422 | ? | (check_not_member_of_set(A,El,Hyps,PTA) -> check_not_member_of_set(B,El,Hyps,PTB)),!. |
| 1423 | | check_not_member_of_set(overwrite(A,B),El,Hyps,overwrite(PTA,PTB)) :- |
| 1424 | | (check_not_member_of_set(A,El,Hyps,PTA) -> check_not_member_of_set(B,El,Hyps,PTB)),!. |
| 1425 | | check_not_member_of_set('NATURAL1',El,Hyps,nat1) :- |
| 1426 | | check_leq(El,0,Hyps). |
| 1427 | | check_not_member_of_set('NATURAL',El,Hyps,nat1) :- |
| 1428 | | check_leq(El,-1,Hyps). |
| 1429 | | check_not_member_of_set(interval(From,To),El,Hyps,interval) :- |
| 1430 | | (check_leq(El,minus(From,1),Hyps) -> true |
| 1431 | | ; check_leq(add(To,1),El,Hyps) -> true). % TODO: or interval empty |
| 1432 | | check_not_member_of_set(domain(Func),El,Hyps,not_in_domain(PT)) :- |
| 1433 | ? | check_not_member_of_domain(Func,El,Hyps,PT),!. |
| 1434 | | check_not_member_of_set(range(Func),El,Hyps,not_in_range(PT)) :- |
| 1435 | | check_not_member_of_range(Func,El,Hyps,PT),!. |
| 1436 | | check_not_member_of_set(relations(A,B),closure(RX),Hyps,closure1_not_el_relations(PT)) :- !, |
| 1437 | | % rx : A <-> B <=> closure1(rx) : A <-> B |
| 1438 | | check_not_member_of_set(relations(A,B),RX,Hyps,PT). |
| 1439 | | check_not_member_of_set(Set,couple(From,_),Hyps,not_in_dom(PT)) :- |
| 1440 | | % x /: dom(f) => x|->y /: f |
| 1441 | | avl_fetch_binop_from_hyps(From,not_member,Hyps,Set2,Hyps2), |
| 1442 | | check_is_subset(domain(Set),Set2,Hyps2,PT), |
| 1443 | | !. |
| 1444 | | check_not_member_of_set(Set,couple(_,To),Hyps,not_in_range) :- |
| 1445 | | avl_fetch_from_hyps(not_member(To,range(Set)),Hyps), % y /: ran(f) => x|->y /: f |
| 1446 | | !. % TODO: generalise this rule somewhat, see domain above |
| 1447 | | check_not_member_of_set(A,El,Hyps,eq(ProofTree)) :- |
| 1448 | ? | avl_fetch_worthwhile_equal_from_hyps(A,Hyps,Value,Hyps2), |
| 1449 | | rewrite_local_loop_check(A,check_member_of_set,Value,Hyps2,Hyps3), |
| 1450 | ? | check_not_member_of_set(Value,El,Hyps3,ProofTree). |
| 1451 | | check_not_member_of_set(Set,El,Hyps,not_in_set_extension) :- |
| 1452 | | is_set_extension(Set,List), |
| 1453 | | check_not_member_of_list(List,El,Hyps). |
| 1454 | | %check_not_member_of_set(Set,El,Hyps,_) :- print(not_mem_failed(Set,El)),nl,fail. |
| 1455 | | % TO DO: process equalities, set_extension?, value(avl_set(AVL)), ... |
| 1456 | | |
| 1457 | | % check if an element is not in the domain of a function |
| 1458 | | check_not_member_of_domain(domain_subtraction(DS,Func),El,Hyps,not_dom_sub(PT)) :- |
| 1459 | | (check_member_of_set(DS,El,Hyps,PT) -> true |
| 1460 | | ; check_not_member_of_domain(Func,El,Hyps,PT)). |
| 1461 | | check_not_member_of_domain(domain_restriction(DS,Func),El,Hyps,not_dom_sub(PT)) :- |
| 1462 | | (check_not_member_of_set(DS,El,Hyps,PT) -> true |
| 1463 | | ; check_not_member_of_domain(Func,El,Hyps,PT)). |
| 1464 | | check_not_member_of_domain(Func,El,Hyps,PT) :- |
| 1465 | ? | get_domain_or_superset(Func,Hyps,DomFunc,Hyps1), |
| 1466 | | check_not_member_of_set(DomFunc,El,Hyps1,PT). |
| 1467 | | |
| 1468 | | % check if an element is not in the domain of a function |
| 1469 | | check_not_member_of_range(range_subtraction(Func,DS),El,Hyps,not_dom_sub(PT)) :- |
| 1470 | | (check_member_of_set(DS,El,Hyps,PT) -> true |
| 1471 | | ; check_not_member_of_range(Func,El,Hyps,PT)). |
| 1472 | | check_not_member_of_range(range_restriction(Func,DS),El,Hyps,not_dom_sub(PT)) :- |
| 1473 | | (check_not_member_of_set(DS,El,Hyps,PT) -> true |
| 1474 | | ; check_not_member_of_range(Func,El,Hyps,PT)). |
| 1475 | | check_not_member_of_range(Func,El,Hyps,PT) :- |
| 1476 | ? | get_range_or_superset(Func,Hyps,RanFunc,Hyps1),!, |
| 1477 | | check_not_member_of_set(RanFunc,El,Hyps1,PT). |
| 1478 | | |
| 1479 | | |
| 1480 | | |
| 1481 | | % check that an element does not occur in a list of values/expressions |
| 1482 | | check_not_member_of_list([],_,_). |
| 1483 | | check_not_member_of_list([H|T],El,Hyps) :- |
| 1484 | | check_not_equal(H,El,Hyps), |
| 1485 | | check_not_member_of_list(T,El,Hyps). |
| 1486 | | |
| 1487 | | is_set_extension(set_extension(List),List). |
| 1488 | | is_set_extension(sorted_set_extension(List),List). |
| 1489 | | |
| 1490 | | |
| 1491 | | % check_member_of_set(Set,Element,Hyps,ProofTree) |
| 1492 | | % check_member_of_set(A,B,_H,_ProofTree) :- print(check_member_of_set(A,B)),nl,fail. |
| 1493 | ? | check_member_of_set(Set,_,Hyps,maximal_set) :- maximal_set(Set,Hyps), !. |
| 1494 | | check_member_of_set(Set,if_then_else(Pred,A,B),Hyps,if(P1,P2)) :- !, % if-then-else expression |
| 1495 | | push_and_rename_normalized_hyp(Pred,Hyps,Hyps1), |
| 1496 | | (hyps_inconsistent(Hyps1) -> true ; check_member_of_set(Set,A,Hyps1,P1) -> true), |
| 1497 | | push_and_rename_normalized_hyp(negation(Pred),Hyps,Hyps2), |
| 1498 | | (hyps_inconsistent(Hyps2) -> true ; check_member_of_set(Set,B,Hyps2,P2) -> true). |
| 1499 | | check_member_of_set(Set,El,Hyps,hyp) :- |
| 1500 | | % we could do avl_fetch_binop_from_hyps(El,member,Hyps,Set2,Hyps2), and check_subset(Set2,Set) |
| 1501 | | avl_fetch_from_hyps(member(El,Set),Hyps),!. % hyp |
| 1502 | | % TO DO: sometimes value(El) stored ! |
| 1503 | | check_member_of_set(sorted_set_extension(List),El,Hyps,PT) :- !, % ordsets:ord_member(El,List),!. |
| 1504 | | check_member_of_set(set_extension(List),El,Hyps,PT). |
| 1505 | ? | check_member_of_set(set_extension(List),El,Hyps,set_extension) :- member(El2,List), |
| 1506 | ? | check_equal(El,El2,Hyps,_),!. % TO DO: avoid multiple equality rewriting of El for long lists ? |
| 1507 | | check_member_of_set(partial_function(T1,T2),El,Hyps,partial_function(PT)) :- |
| 1508 | | check_is_partial_function_with_type(El,T1,T2,Hyps,PT). |
| 1509 | | check_member_of_set(total_function(T1,T2),El,Hyps,total_function(PT,PTDom)) :- |
| 1510 | | check_is_partial_function_with_type(El,T1,T2,Hyps,PT),!, |
| 1511 | | simplify_expr(domain(El),Hyps,DomEl), |
| 1512 | ? | check_is_subset(T1,DomEl,Hyps,PTDom). |
| 1513 | | check_member_of_set(relations(A,B),closure(RX),Hyps,closure1_el_relations(PT)) :- !, |
| 1514 | | % rx : A <-> B <=> closure1(rx) : A <-> B |
| 1515 | | check_member_of_set(relations(A,B),RX,Hyps,PT). |
| 1516 | | check_member_of_set(range(Func),El,Hyps,mem_range(PT)) :- |
| 1517 | ? | check_member_of_range(El,Func,Hyps,PT),!. % check before function application below, can do symbolic range check |
| 1518 | | check_member_of_set(image(Func,Set),El,Hyps,mem_range_for_image(PT0,PT1)) :- |
| 1519 | | % El:ran(F) & dom(F) <: S => El:F[S] |
| 1520 | | check_member_of_set(range(Func),El,Hyps,PT0),!, |
| 1521 | | check_is_subset(domain(Func),Set,Hyps,PT1). |
| 1522 | | check_member_of_set(A,ElFunc,Hyps,typing_membership(PT)) :- |
| 1523 | ? | get_type_from_hyps(ElFunc,Hyps,Range,Hyps2), % !, % moving cut later proves on additional PO for test 2039 |
| 1524 | | % e.g. f(.) : A if ran(f) <: Range & Range <: A |
| 1525 | | %rewrite_local_loop_check(A,check_member_of_set,Range,Hyps2,Hyps3), |
| 1526 | ? | check_is_subset(Range,A,Hyps2,PT),!. |
| 1527 | | check_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_member_of_set(Value,El,Hyps3,ProofTree). |
| 1531 | ? | check_member_of_set(interval(L,U),El,Hyps,interval(PT)) :- !, check_in_interval(El,L,U,Hyps,PT). |
| 1532 | | check_member_of_set('NATURAL1',El,Hyps,nat1(PT)) :- !, check_subset_interval('NATURAL1',El,El,Hyps,PT). |
| 1533 | | check_member_of_set('NATURAL',El,Hyps,nat(PT)) :- !, check_subset_interval('NATURAL',El,El,Hyps,PT). |
| 1534 | | check_member_of_set(union(A,B),El,Hyps,union(PTA,PTB)) :- !, |
| 1535 | ? | (check_member_of_set(A,El,Hyps,PTA) -> true ; check_member_of_set(B,El,Hyps,PTB)). |
| 1536 | | check_member_of_set(intersection(A,B),El,Hyps,intersection(PTA,PTB)) :- !, |
| 1537 | | (check_member_of_set(A,El,Hyps,PTA) -> check_member_of_set(B,El,Hyps,PTB)). |
| 1538 | | check_member_of_set(set_subtraction(A,B),El,Hyps,set_subtraction(PTA,PTB)) :- !, |
| 1539 | ? | (check_member_of_set(A,El,Hyps,PTA) -> check_not_member_of_set(B,El,Hyps,PTB)). |
| 1540 | | check_member_of_set(pow_subset(T1),El,Hyps,pow(PT)) :- !, |
| 1541 | | check_is_subset(El,T1,Hyps,PT). |
| 1542 | | check_member_of_set(fin_subset(T1),El,Hyps,fin(PT1,PT2)) :- !, |
| 1543 | | check_is_subset(El,T1,Hyps,PT1),!, |
| 1544 | | check_finite(El,Hyps,PT2). |
| 1545 | | check_member_of_set(pow1_subset(T1),El,Hyps,pow1(PT)) :- !, |
| 1546 | ? | check_not_empty_set(El,Hyps),!, |
| 1547 | | check_is_subset(El,T1,Hyps,PT). |
| 1548 | | check_member_of_set(fin1_subset(T1),El,Hyps,fin1(PT1,PT2)) :- !, |
| 1549 | | check_not_empty_set(El,Hyps),!, |
| 1550 | | check_is_subset(El,T1,Hyps,PT1),!, |
| 1551 | | check_finite(El,Hyps,PT2). |
| 1552 | | check_member_of_set(seq(T1),El,Hyps,seq(PT)) :- !, |
| 1553 | | check_is_sequence(El,Hyps),!, |
| 1554 | | check_is_subset(range(El),T1,Hyps,PT). |
| 1555 | | check_member_of_set(seq1(T1),El,Hyps,seq1(PT)) :- !, |
| 1556 | | check_is_non_empty_sequence(El,Hyps),!, |
| 1557 | | check_is_subset(range(El),T1,Hyps,PT). |
| 1558 | | check_member_of_set(cartesian_product(T1,T2),couple(El1,El2),Hyps,cart(PT1,PT2)) :- !, |
| 1559 | ? | check_member_of_set(T1,El1,Hyps,PT1),!, |
| 1560 | ? | check_member_of_set(T2,El2,Hyps,PT2). |
| 1561 | | check_member_of_set(value(avl_set(AVL)),El,Hyps,PT) :- |
| 1562 | | (avl_can_fetch(El,BVal) -> !,PT=avl_fetch(El),avl_fetch(BVal,AVL) |
| 1563 | | ; avl_is_interval(AVL,Min,Max) -> !, PT=avl_interval(PT2), |
| 1564 | | % useful is El is not a number, but e.g. an arithmetic expression |
| 1565 | | % print(avl_interval(Min,Max,El)),nl, |
| 1566 | | check_integer(El,check_member_of_set_avl_interval), |
| 1567 | ? | check_in_interval(El,Min,Max,Hyps,PT2) |
| 1568 | | ). |
| 1569 | | check_member_of_set(A,El,Hyps,rewrite(PT)) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!, |
| 1570 | ? | check_member_of_set(A2,El,Hyps2,PT). |
| 1571 | | check_member_of_set(domain(Func),Index,Hyps,mem_domain(PT)) :- |
| 1572 | ? | check_member_of_domain(Index,Func,Hyps,PT),!. |
| 1573 | | check_member_of_set(Set,X,Hyps,value_set(PT)) :- |
| 1574 | ? | try_get_set_of_possible_values(X,Hyps,XSet,Hyps2), % also covers min(Set), max(Set), mu(Set), CHOOSE(Set) |
| 1575 | ? | check_is_subset(XSet,Set,Hyps2,PT),!. |
| 1576 | | %check_member_of_set(Set,X,Hyps,eq(PT)) :- Set = '$'(_), |
| 1577 | | % avl_fetch_equal_from_hyps(Set,Hyps,Set2,Hyps2), % maybe perform direct rewrite ancestor cycle check here |
| 1578 | | % check_member_of_set(Set2,X,Hyps2,PT),!. |
| 1579 | | check_member_of_set(Set,X,Hyps,trans(PT)) :- |
| 1580 | ? | avl_fetch_binop_from_hyps(Set,superset,Hyps,SubSet,Hyps2), % X:B & B <: A => X:A |
| 1581 | ? | check_member_of_set(SubSet,X,Hyps2,PT),!. |
| 1582 | | check_member_of_set(Set,ID,Hyps,member_subset(PT)) :- |
| 1583 | ? | avl_fetch_worthwhile_member_from_hyps(ID,Hyps,SubSet,Hyps2), %write(sub(ID,SubSet,Set)),nl, |
| 1584 | | check_is_subset(SubSet,Set,Hyps2,PT). |
| 1585 | | %check_member_of_set(A,B,_H,_ProofTree) :- write(check_member_of_set_failed(A,B)),nl,fail. |
| 1586 | | |
| 1587 | | |
| 1588 | | :- use_module(probsrc(kernel_reals),[construct_real/2]). |
| 1589 | | % check if we can fetch an expression as a B value (second arg) in an AVL set |
| 1590 | | avl_can_fetch(El,Res) :- number(El),!, Res=int(El). |
| 1591 | | avl_can_fetch(boolean_true,pred_true). |
| 1592 | | avl_can_fetch(boolean_false,pred_false). |
| 1593 | | avl_can_fetch(real(Atom),R) :- construct_real(Atom,R). |
| 1594 | | avl_can_fetch(string(S),string(S)) :- ground(S). |
| 1595 | | avl_can_fetch(couple(A,B),(VA,VB)) :- avl_can_fetch(A,VA), avl_can_fetch(B,VB). |
| 1596 | | |
| 1597 | | check_member_of_domain(El,reverse(Func2),Hyps,reverse(PT)) :- !, |
| 1598 | | check_member_of_range(El,Func2,Hyps,PT). |
| 1599 | | check_member_of_domain(El,Func,Hyps,hyp) :- |
| 1600 | | avl_fetch_from_hyps(member(El,domain(Func)),Hyps),!. % hyp, already checked in check_member_of_set |
| 1601 | | check_member_of_domain(Index,Func,Hyps,size_in_dom_seq) :- % x:seq1(T) => size(x) : dom(x) |
| 1602 | ? | index_in_non_empty_sequence(Index,Func,Hyps), |
| 1603 | | check_is_non_empty_sequence(Func,Hyps),!. |
| 1604 | | % TO DO: f~(x) : dom(f) ?? |
| 1605 | | check_member_of_domain(El,union(A,B),Hyps,dom_of_union(PT)) :- |
| 1606 | | check_member_of_union(domain(A),domain(B),El,Hyps,PT). |
| 1607 | | check_member_of_domain(El,overwrite(A,B),Hyps,dom_of_overwrite(PT)) :- |
| 1608 | ? | check_member_of_union(domain(A),domain(B),El,Hyps,PT). |
| 1609 | | check_member_of_domain(El,direct_product(A,B),Hyps,dom_of_direct_product(PT)) :- % dom(A >< B) = dom(A) /\ dom (B) |
| 1610 | | check_member_of_set(domain(A),El,Hyps,PT), |
| 1611 | | check_member_of_set(domain(B),El,Hyps,PT). |
| 1612 | | check_member_of_domain(El,A,Hyps,rewrite(PT)) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!, |
| 1613 | | check_member_of_domain(El,A2,Hyps2,PT). |
| 1614 | | check_member_of_domain(El,Func,Hyps,dom_of_subset(PT)) :- % Func2 <: Func & El:dom(Func2) => El:dom(Func) |
| 1615 | | % counter part of rule with superset for check_member_of_set |
| 1616 | | (Op = equal ; Op = superset), |
| 1617 | ? | avl_fetch_binop_from_hyps(Func,Op,Hyps,Func2,Hyps1), |
| 1618 | | rewrite_local_loop_check(Func,check_member_of_domain,Func2,Hyps1,Hyps2), |
| 1619 | | check_member_of_set(domain(Func2),El,Hyps2,PT). |
| 1620 | | check_member_of_domain(El,comprehension_set(IDS,Body),Hyps,dom_of_lambda(PTs)) :- |
| 1621 | ? | get_lambda_args_and_body(IDS,Body,_,_,Args,RestBodyList), |
| 1622 | | %nl,print(lambda(Args,El,RestBodyList)),nl, |
| 1623 | ? | generate_funapp_binding(Args,El,Subst), |
| 1624 | | % we rename the local variables of the comprehension set; no need to call add_new_hyp_any_vars |
| 1625 | | l_rename_and_prove_goals(RestBodyList,Subst,Hyps,PTs). |
| 1626 | | check_member_of_domain(El,restrict_front(_,K),Hyps,dom_of_restrict_front(PT)) :- |
| 1627 | | check_member_of_set(interval(1,K),El,Hyps,PT). % WD Condition requires K : 0..size(Seq) |
| 1628 | | check_member_of_domain(El,if_then_else(Pred,A,B),Hyps,if_then_else(PT1,PT2)) :- |
| 1629 | | push_and_rename_normalized_hyp(Pred,Hyps,Hyps1), |
| 1630 | | (hyps_inconsistent(Hyps1) -> true ; check_member_of_domain(El,A,Hyps1,PT1) -> true), |
| 1631 | | push_and_rename_normalized_hyp(negation(Pred),Hyps,Hyps2), |
| 1632 | | (hyps_inconsistent(Hyps2) -> true ; check_member_of_domain(El,B,Hyps2,PT2) -> true). |
| 1633 | | %check_member_of_domain(Index,Func,Hyps,_) :- write(check_member_of_domain_failed(Index,Func)),nl,fail. |
| 1634 | | |
| 1635 | | % we could do intersection, subtraction |
| 1636 | | |
| 1637 | | % check if an element is an element of a union of two sets |
| 1638 | | check_member_of_union(Set1,_,El,Hyps,PT) :- check_member_of_set(Set1,El,Hyps,PT),!. |
| 1639 | | check_member_of_union(_,Set2,El,Hyps,PT) :- check_member_of_set(Set2,El,Hyps,PT),!. |
| 1640 | | check_member_of_union(Set1,Set2,El,Hyps,union(PT1,PT2)) :- |
| 1641 | | % x : A \/ B & A <: S1 & B <: S2 => x : S1 \/ S2 |
| 1642 | ? | avl_fetch_mem_from_hyps(El,Hyps,union(A,B),Hyps2), % TO DO: other conditions ? |
| 1643 | | (check_is_subset(A,Set1,Hyps2,PT1) -> check_is_subset(B,Set2,Hyps2,PT2) |
| 1644 | ? | ; check_is_subset(A,Set2,Hyps2,PT1) -> check_is_subset(B,Set1,Hyps2,PT2)). |
| 1645 | | |
| 1646 | | generate_funapp_binding(['$'(X)],El,[rename(X,El)]). |
| 1647 | | generate_funapp_binding(['$'(X),'$'(Y)],couple(El1,El2),[rename(X,El1),rename(Y,El2)]). |
| 1648 | | generate_funapp_binding(['$'(X),'$'(Y),'$'(Z)],couple(couple(El1,El2),El3),[rename(X,El1),rename(Y,El2),rename(Z,El3)]). |
| 1649 | | % TO DO: create substitution for more arguments and other parameters |
| 1650 | | |
| 1651 | | |
| 1652 | ? | check_member_of_range(El,reverse(Func2),Hyps,reverse(PT)) :- !,check_member_of_domain(El,Func2,Hyps,PT). |
| 1653 | | check_member_of_range(El,Func,Hyps,hyp) :- |
| 1654 | | avl_fetch_from_hyps(member(El,range(Func)),Hyps),!. % hyp, already checked in check_member_of_set |
| 1655 | | check_member_of_range(El,A,Hyps,rewrite(PT)) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!, |
| 1656 | | check_member_of_range(El,A2,Hyps2,PT). |
| 1657 | | check_member_of_range('$'(ID),Func2,Hyps,PT) :- |
| 1658 | ? | avl_fetch_worthwhile_equal_from_hyps('$'(ID),Hyps,Value,Hyps2), |
| 1659 | ? | check_member_of_range(Value,Func2,Hyps2,PT). |
| 1660 | | check_member_of_range(function(Func1,_),Func2,Hyps,func_app_in_range) :- % f(.) : ran(f) |
| 1661 | | check_equal(Func1,Func2,Hyps,_). |
| 1662 | | check_member_of_range(El,if_then_else(Pred,A,B),Hyps,if_then_else(PT1,PT2)) :- |
| 1663 | | push_and_rename_normalized_hyp(Pred,Hyps,Hyps1), |
| 1664 | | (hyps_inconsistent(Hyps1) -> true ; check_member_of_range(El,A,Hyps1,PT1) -> true), |
| 1665 | | push_and_rename_normalized_hyp(negation(Pred),Hyps,Hyps2), |
| 1666 | | (hyps_inconsistent(Hyps2) -> true ; check_member_of_range(El,B,Hyps2,PT2) -> true). |
| 1667 | | |
| 1668 | | |
| 1669 | | % subset transitivity for unary operators: |
| 1670 | | subset_transitivity_rule(pow_subset(A),pow_subset(B),A,B). |
| 1671 | | |
| 1672 | | subset_transitivity_rule(pow1_subset(A),pow1_subset(B),A,B). |
| 1673 | | subset_transitivity_rule(pow1_subset(A),pow_subset(B),A,B). |
| 1674 | | |
| 1675 | | subset_transitivity_rule(fin_subset(A),fin_subset(B),A,B). |
| 1676 | | subset_transitivity_rule(fin_subset(A),pow_subset(B),A,B). |
| 1677 | | |
| 1678 | | subset_transitivity_rule(fin1_subset(A),fin1_subset(B),A,B). |
| 1679 | | subset_transitivity_rule(fin1_subset(A),fin_subset(B),A,B). |
| 1680 | | subset_transitivity_rule(fin1_subset(A),pow1_subset(B),A,B). |
| 1681 | | subset_transitivity_rule(fin1_subset(A),pow_subset(B),A,B). |
| 1682 | | |
| 1683 | | subset_transitivity_rule(seq(A),seq(B),A,B). |
| 1684 | | subset_transitivity_rule(seq(A),partial_function(typeset,B),A,B). |
| 1685 | | |
| 1686 | | subset_transitivity_rule(seq1(A),seq1(B),A,B). |
| 1687 | | subset_transitivity_rule(seq1(A),seq(B),A,B). |
| 1688 | | subset_transitivity_rule(seq1(A),partial_function(typeset,B),A,B). |
| 1689 | | |
| 1690 | | subset_transitivity_rule(iseq(A),iseq(B),A,B). |
| 1691 | | subset_transitivity_rule(iseq(A),seq(B),A,B). |
| 1692 | | subset_transitivity_rule(iseq(A),partial_function(typeset,B),A,B). |
| 1693 | | |
| 1694 | | subset_transitivity_rule(iseq1(A),iseq1(B),A,B). |
| 1695 | | subset_transitivity_rule(iseq1(A),iseq(B),A,B). |
| 1696 | | subset_transitivity_rule(iseq1(A),seq1(B),A,B). |
| 1697 | | subset_transitivity_rule(iseq1(A),seq(B),A,B). |
| 1698 | | subset_transitivity_rule(iseq1(A),partial_function(typeset,B),A,B). |
| 1699 | | |
| 1700 | | % subset_transitivity_rule(perm(A),perm(B),A,B). % this does not hold perm({}) = { [] }, perm({TRUE}) = {[TRUE]} |
| 1701 | | subset_transitivity_rule(perm(A),iseq(B),A,B). |
| 1702 | | subset_transitivity_rule(perm(A),seq(B),A,B). |
| 1703 | | subset_transitivity_rule(perm(A),partial_function(typeset,B),A,B). |
| 1704 | | |
| 1705 | | |
| 1706 | | subset_transitivity_rule(range(A),domain(reverse(B)),A,B). |
| 1707 | | subset_transitivity_rule(range(A),range(B),A,B). |
| 1708 | | subset_transitivity_rule(range(reverse(A)),domain(B),A,B). |
| 1709 | | subset_transitivity_rule(domain(reverse(A)),range(B),A,B). |
| 1710 | | subset_transitivity_rule(domain(A),domain(B),A,B). % dom(A) <: dom(B) if A <:B |
| 1711 | | subset_transitivity_rule(domain(A),range(reverse(B)),A,B). |
| 1712 | | subset_transitivity_rule(reverse(A),reverse(B),A,B). |
| 1713 | | subset_transitivity_rule(rev(A),rev(B),A,B). |
| 1714 | | subset_transitivity_rule(identity(A),identity(B),A,B). |
| 1715 | | |
| 1716 | | % TO DO: add rules for more binary operators, like surjective relations, ... |
| 1717 | | subset_bin_transitivity_rule(relations(A1,A2),relations(B1,B2),A1,A2,B1,B2). % <-> |
| 1718 | | subset_bin_transitivity_rule(total_relation(A1,A2),relations(B1,B2),A1,A2,B1,B2). % <<-> |
| 1719 | | subset_bin_transitivity_rule(total_relation(A1,A2),total_relation(B1,B2),A1,A2,B1,B2) :- A1=B1. |
| 1720 | | subset_bin_transitivity_rule(partial_function(A1,A2),relations(B1,B2),A1,A2,B1,B2). % +-> |
| 1721 | | subset_bin_transitivity_rule(partial_function(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). |
| 1722 | | subset_bin_transitivity_rule(partial_injection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % >+> |
| 1723 | | subset_bin_transitivity_rule(partial_injection(A1,A2),partial_injection(B1,B2),A1,A2,B1,B2). |
| 1724 | | subset_bin_transitivity_rule(partial_surjection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % -+>> |
| 1725 | | subset_bin_transitivity_rule(partial_surjection(A1,A2),partial_surjection(B1,B2),A1,A2,B1,B2) :- A2=B2. |
| 1726 | | subset_bin_transitivity_rule(partial_bijection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % >+>> |
| 1727 | | subset_bin_transitivity_rule(total_function(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % --> |
| 1728 | | subset_bin_transitivity_rule(total_function(A1,A2),total_function(B1,B2),A1,A2,B1,B2) :- A1=B1. |
| 1729 | | subset_bin_transitivity_rule(total_injection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % >-> |
| 1730 | | subset_bin_transitivity_rule(total_injection(A1,A2),total_function(B1,B2),A1,A2,B1,B2) :- A1=B1. |
| 1731 | | subset_bin_transitivity_rule(total_surjection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % -->> |
| 1732 | | subset_bin_transitivity_rule(total_surjection(A1,A2),total_function(B1,B2),A1,A2,B1,B2) :- A1=B1. |
| 1733 | | subset_bin_transitivity_rule(total_bijection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % >+>> |
| 1734 | | subset_bin_transitivity_rule(total_bijection(A1,A2),partial_injection(B1,B2),A1,A2,B1,B2). |
| 1735 | | subset_bin_transitivity_rule(total_bijection(A1,A2),partial_surjection(B1,B2),A1,A2,B1,B2) :- A2=B2. |
| 1736 | | subset_bin_transitivity_rule(total_bijection(A1,A2),total_function(B1,B2),A1,A2,B1,B2) :- A1=B1. |
| 1737 | | subset_bin_transitivity_rule(total_bijection(A1,A2),total_injection(B1,B2),A1,A2,B1,B2) :- A1=B1. |
| 1738 | | subset_bin_transitivity_rule(total_bijection(A1,A2),total_surjection(B1,B2),A1,A2,B1,B2) :- A1=B1, A2=B2. |
| 1739 | | subset_bin_transitivity_rule(image(A1,A2),image(B1,B2),A1,A2,B1,B2). % A1[A2] <: B1[B2] if A1 <: B1 & A2 <: B2 |
| 1740 | | 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 |
| 1741 | | subset_bin_transitivity_rule(range_restriction(A1,A2),range_restriction(B1,B2),A1,A2,B1,B2). |
| 1742 | | 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 |
| 1743 | | 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 |
| 1744 | | %subset_bin_transitivity_rule(A,B,A1,A2,B1,B2) :- write(subset_bin_transitivity_rule(A,B,A1,A2,B1,B2)),nl,fail. |
| 1745 | | % TO DO: add more |
| 1746 | | |
| 1747 | | % TO DO: instead of is_set_of_sequences_type |
| 1748 | | %subset_mixed_transitivity_rule(total_function(A1,A2),seq(B2),A2,B2) :- is_interval(A1). |
| 1749 | | |
| 1750 | | check_in_interval(El,Min,Max,Hyps,in_interval(PT1,PT2)) :- |
| 1751 | | expr_is_member_of_set(El,Set,PT1),!, % TODO: should we treat min/max as well here?? |
| 1752 | | check_is_subset(Set,interval(Min,Max),Hyps,PT2). |
| 1753 | | check_in_interval(El,Min,Max,Hyps,PT) :- |
| 1754 | ? | check_subset_interval(interval(Min,Max),El,El,Hyps,PT). % calls check_sub_intervals(Min,Max,El,El,Hyps) |
| 1755 | | |
| 1756 | | expr_is_member_of_set(mu(Set),Set,mu). |
| 1757 | | expr_is_member_of_set(external_function_call(Call,[Set]),Set,ext_call(Call)) :- |
| 1758 | | (Call = 'CHOOSE' -> true ; Call = 'MU'). |
| 1759 | | |
| 1760 | | % check if an interval is a subset of the first argument |
| 1761 | | check_subset_interval(union(A,B),L1,U1,Hyps,union(PT)) :- !, |
| 1762 | | % TO DO: try and merge A,B : union(interval(1,10),set_extension([11])) |
| 1763 | | (check_subset_interval(A,L1,U1,Hyps,PT) -> true ; check_subset_interval(B,L1,U1,Hyps,PT)). |
| 1764 | | check_subset_interval(sorted_set_extension(L),L1,U1,Hyps,PT) :- !, |
| 1765 | | check_subset_interval(set_extension(L),L1,U1,Hyps,PT). |
| 1766 | | check_subset_interval(set_extension(L),L1,U1,Hyps,set_extension(Nr)) :- !, |
| 1767 | | % TO DO: maybe merge L into an interval |
| 1768 | ? | nth1(Nr,L,El), check_sub_intervals(L1,U1,El,El,Hyps),!. |
| 1769 | | check_subset_interval(intersection(A,B),L1,U1,Hyps,inter(PTA,PTB)) :- !, |
| 1770 | | % L1..U1 <: A /\ B if L1..U1 <: A & L1..U1 <: B |
| 1771 | | (check_subset_interval(A,L1,U1,Hyps,PTA) -> check_subset_interval(B,L1,U1,Hyps,PTB)). |
| 1772 | | check_subset_interval(interval(L2,U2),L1,U1,Hyps,interval) :- |
| 1773 | ? | !,check_sub_intervals(L1,U1,L2,U2,Hyps). |
| 1774 | | check_subset_interval('NATURAL',L1,_,Hyps,nat) :- !, check_leq(0,L1,Hyps). |
| 1775 | | check_subset_interval('NATURAL1',L1,_,Hyps,nat1) :- !, check_leq(1,L1,Hyps). |
| 1776 | | check_subset_interval(value(avl_set(A)),L1,U1,Hyps,avl(PT)) :- !, |
| 1777 | | (number(L1), number(U1) |
| 1778 | | -> PT=in(L1,U1), |
| 1779 | ? | check_interval_in_custom_set(L1,U1,avl_set(A),no_wf_available) |
| 1780 | | ; avl_min(A,int(L2)), avl_max(A,int(U2)), PT=min_max(L2,U2,PT2), |
| 1781 | | check_subset_interval(interval(L2,U2),L1,U1,Hyps,PT2) |
| 1782 | | ). |
| 1783 | | check_subset_interval(A,L1,U1,Hyps,rewrite(PT)) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!, |
| 1784 | ? | check_subset_interval(A2,L1,U1,Hyps2,PT). |
| 1785 | | check_subset_interval(domain(Expr),Low,Up,Hyps,dom_seq1) :- % a special rule when using SEQ(1) rather than first(SEQ) |
| 1786 | | (check_leq(1,Low,Hyps), check_leq(Up,size(Expr),Hyps) % 1..size(s) <: dom(s) |
| 1787 | | -> check_is_sequence(Expr,Hyps) |
| 1788 | ? | ; index_in_non_empty_sequence(Low,Expr,Hyps), |
| 1789 | ? | index_in_non_empty_sequence(Up,Expr,Hyps) % 1..1 or size(s)..size(s) <: dom(s) if s:seq1(.) |
| 1790 | | -> check_is_non_empty_sequence(Expr,Hyps) |
| 1791 | | ). |
| 1792 | | check_subset_interval(range(reverse(Expr)),Low,Up,Hyps,PT) :- !, |
| 1793 | | check_subset_interval(domain(Expr),Low,Up,Hyps,PT). |
| 1794 | | check_subset_interval(A,Low,Up,Hyps,eq(PT)) :- |
| 1795 | ? | avl_fetch_worthwhile_equal_from_hyps(A,Hyps,A2,Hyps2), |
| 1796 | | rewrite_local_loop_check(A,check_subset_interval,A2,Hyps2,Hyps3), |
| 1797 | ? | check_subset_interval(A2,Low,Up,Hyps3,PT). |
| 1798 | | %check_subset_interval(A,L1,U1,_,_) :- print(check_subset_interval_failed(A,L1,U1)),nl,fail. |
| 1799 | | |
| 1800 | | % s:seq1(.) => 1:dom(s) & size(s):dom(s) |
| 1801 | | index_in_non_empty_sequence(1,_,_). |
| 1802 | | index_in_non_empty_sequence(card(E),E,_). |
| 1803 | | index_in_non_empty_sequence(size(E),E,_). |
| 1804 | | index_in_non_empty_sequence('$'(X),E,Hyps) :- |
| 1805 | ? | avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2), |
| 1806 | | rewrite_local_loop_check(X,index_in_non_empty_sequence,Y,Hyps2,Hyps3), |
| 1807 | ? | index_in_non_empty_sequence(Y,E,Hyps3). |
| 1808 | | index_in_non_empty_sequence(X,E,Hyps) :- \+ useful_value(X), % do not rewrite 10 to interval(10,10) |
| 1809 | ? | try_get_set_of_possible_values(X,Hyps,XSet,Hyps2), |
| 1810 | | rewrite_local_loop_check(X,index_in_non_empty_sequence,XSet,Hyps2,Hyps3), |
| 1811 | ? | all_in_non_empty_sequence(XSet,E,Hyps3). |
| 1812 | | |
| 1813 | | all_in_non_empty_sequence(interval(A,B),E,Hyps) :- |
| 1814 | ? | index_in_non_empty_sequence(A,E,Hyps), |
| 1815 | ? | index_in_non_empty_sequence(B,E,Hyps). |
| 1816 | | % TODO: avl_set, ... |
| 1817 | | |
| 1818 | | % check if L1..U1 <: L2..U2 |
| 1819 | | check_sub_intervals(L1,L1,L2,U2,Hyps) :- (L1=L2 ; L1=U2),!, |
| 1820 | ? | check_not_empty_set(interval(L2,U2),Hyps). |
| 1821 | | check_sub_intervals(L1,U1,L2,U2,Hyps) :- % L1..U1 <: L2..U2 if L2 <= L1 & U1 <= U2 |
| 1822 | ? | check_leq(L2,L1,Hyps),!, |
| 1823 | ? | check_leq(U1,U2,Hyps). |
| 1824 | | |
| 1825 | | |
| 1826 | | |
| 1827 | | % some exact rewrite steps |
| 1828 | ? | rewrite_set_expression_exact(domain(A),Hyps,Res,Hyps2) :- compute_exact_domain(A,Hyps,Dom,Hyps2),!, |
| 1829 | | %print(rewrote(domain(A))),nl, print(Dom),nl, |
| 1830 | | (A='$'(ID) -> not_occurs(Dom,ID) ; true), % prevent silly rewrites |
| 1831 | | Res=Dom. |
| 1832 | ? | rewrite_set_expression_exact(range(A),Hyps,Res,Hyps2) :- compute_exact_range(A,Hyps,Ran,Hyps2),!, |
| 1833 | | %print(rewrote(range(A))),nl, print(Ran),nl, |
| 1834 | | (A='$'(ID) -> not_occurs(Ran,ID) ; true), % prevent silly rewrites |
| 1835 | | Res=Ran. |
| 1836 | | rewrite_set_expression_exact(intersection(A,B),Hyps,Res,Hyps) :- |
| 1837 | | (is_empty_set_direct(A) -> Res=empty_set ; is_empty_set_direct(B) -> Res=empty_set). |
| 1838 | | rewrite_set_expression_exact(set_subtraction(A,B),Hyps,Res,Hyps) :- |
| 1839 | | (is_empty_set_direct(A) -> Res=empty_set ; is_empty_set_direct(B) -> Res=A). |
| 1840 | | rewrite_set_expression_exact(union(A,B),Hyps,Res,Hyps1) :- |
| 1841 | | (check_equal(A,B,Hyps,Hyps1) -> Res=A |
| 1842 | | ; Hyps1=Hyps, merge_set_extensions(union(A,B),List,[]), |
| 1843 | | construct_set_extension(List,Hyps,Res)). |
| 1844 | | rewrite_set_expression_exact(value(closure(P,T,B)),Hyps,Res,Hyps) :- nonvar(P), |
| 1845 | | is_normed_interval_closure(P,T,B,LOW,UP), number(LOW),number(UP),!, |
| 1846 | | Res = interval(LOW,UP). |
| 1847 | | rewrite_set_expression_exact(assertion_expression(_,_,Expr),Hyps,Res,Hyps2) :- % TO DO: add Predicate to Hyps ? |
| 1848 | | (rewrite_set_expression_exact(Expr,Hyps,Expr2,Hyps2) -> Res=Expr2 |
| 1849 | | ; Res=Expr, Hyps2=Hyps). |
| 1850 | | rewrite_set_expression_exact(Expr,Hyps,Res,Hyps) :- |
| 1851 | ? | eval_bvalue_from_norm_expr(Expr,Val,Hyps),!, Res=value(Val). |
| 1852 | | % Note one can have equalities like f = f~~ (in FunLawsWithLambda.mch); hence important to pass Hyps for cycle detection |
| 1853 | | |
| 1854 | | is_normed_interval_closure([P],[integer],B,LOW,UP) :- B = member(P,interval(LOW,UP)). |
| 1855 | | |
| 1856 | | % rewrite relational image operator; not used |
| 1857 | | rewrite_rel_image(Rel,Set,Hyps,value(ResVal),Hyps) :- write(rewr(Rel,Set)),nl, |
| 1858 | | get_bvalue_from_norm_expr(Rel,RelVal,Hyps), !, get_bvalue_from_norm_expr(Set,SetVal,Hyps), !, |
| 1859 | | eval_binary_operator(image,RelVal,SetVal,ResVal). |
| 1860 | | |
| 1861 | | |
| 1862 | | eval_unary_operator(reverse,Arg,Res) :- bsets_clp:invert_relation_wf(Arg,Res,no_wf_available). |
| 1863 | | eval_binary_operator(image,RelVal,SetVal,Res) :- bsets_clp:image_wf(RelVal,SetVal,Res,no_wf_available). |
| 1864 | | |
| 1865 | | :- use_module(probsrc(custom_explicit_sets),[construct_interval_closure/3]). |
| 1866 | | % try and convert a normed AST expression to a valid B value |
| 1867 | | get_bvalue_from_norm_expr(boolean_true,pred_true,_). |
| 1868 | | get_bvalue_from_norm_expr(boolean_false,pred_false,_). |
| 1869 | | get_bvalue_from_norm_expr(Nr,int(Nr),_) :- integer(Nr). |
| 1870 | | get_bvalue_from_norm_expr(value(V),V,_) :- !, value_can_be_computed(V). |
| 1871 | ? | get_bvalue_from_norm_expr(set_extension(List),Result,Hyps) :- !, l_get_bvalue_from_norm_expr(List,Result,Hyps). |
| 1872 | | get_bvalue_from_norm_expr(sorted_set_extension(List),Result,Hyps) :- !, l_get_bvalue_from_norm_expr(List,Result,Hyps). |
| 1873 | | get_bvalue_from_norm_expr(interval(Low,Up),Result,_) :- !, |
| 1874 | | number(Low),number(Up), construct_interval_closure(Low,Up,Result). |
| 1875 | | get_bvalue_from_norm_expr('$'(ID),Res,Hyps) :- !, |
| 1876 | ? | avl_fetch_equal_from_hyps('$'(ID),Hyps,E2,_Hyps1), E2 \= '$'(_), |
| 1877 | | get_bvalue_from_norm_expr(E2,Res,Hyps). |
| 1878 | | get_bvalue_from_norm_expr(Expr,Res,Hyps) :- eval_bvalue_from_norm_expr(Expr,Res,Hyps). |
| 1879 | | |
| 1880 | | l_get_bvalue_from_norm_expr([],[],_). |
| 1881 | ? | l_get_bvalue_from_norm_expr([H|T],[R|TR],Hyps) :- get_bvalue_from_norm_expr(H,R,Hyps), |
| 1882 | | l_get_bvalue_from_norm_expr(T,TR,Hyps). |
| 1883 | | |
| 1884 | ? | eval_bvalue_from_norm_expr(reverse(Rel),ResVal,Hyps) :- get_bvalue_from_norm_expr(Rel,RelVal,Hyps), |
| 1885 | | eval_unary_operator(reverse,RelVal,ResVal). |
| 1886 | ? | eval_bvalue_from_norm_expr(image(Rel,Set),ResVal,Hyps) :- get_bvalue_from_norm_expr(Rel,RelVal,Hyps),!, |
| 1887 | ? | get_bvalue_from_norm_expr(Set,SetVal,Hyps),!, |
| 1888 | | eval_binary_operator(image,RelVal,SetVal,ResVal). |
| 1889 | | |
| 1890 | | |
| 1891 | | % try and rewrite function applications for comprehension_sets |
| 1892 | | rewrite_function_application(CompSet,Arg,Hyps,Result,Hyps) :- |
| 1893 | | is_comprehension_set(CompSet,[$(PARA),$(LAMBDARES)],Body), |
| 1894 | | get_conjunct(Body,equal(A,B)), |
| 1895 | | sym_unify(A,B,$(LAMBDARES),RESEXPR), |
| 1896 | | \+ occurs(RESEXPR,LAMBDARES), |
| 1897 | | % TODO: support more than one argument and hadd rest of body to hyps |
| 1898 | | !, |
| 1899 | | rename_norm_term(RESEXPR,[rename(PARA,Arg)],Result). |
| 1900 | | rewrite_function_application(Function,Arg,Hyps,Result,Hyps2) :- |
| 1901 | ? | avl_fetch_binop_from_hyps(Function,equal,Hyps,Value,Hyps1), |
| 1902 | | rewrite_function_application(Value,Arg,Hyps1,Result,Hyps2). |
| 1903 | | |
| 1904 | | get_conjunct(conjunct(A,B),C) :- !, (get_conjunct(A,C) ; get_conjunct(B,C)). |
| 1905 | | get_conjunct(C,C). |
| 1906 | | |
| 1907 | | merge_set_extensions(empty_set) --> []. |
| 1908 | | merge_set_extensions(empty_sequence) --> []. |
| 1909 | | merge_set_extensions(set_extension(L)) --> L. |
| 1910 | | merge_set_extensions(sorted_set_extension(L)) --> L. |
| 1911 | | merge_set_extensions(union(A,B)) --> merge_set_extensions(A), merge_set_extensions(B). |
| 1912 | | |
| 1913 | | % check if AVL is a subset of the first argument |
| 1914 | | check_subset_avl(union(A,B),AVL1,Hyps) :- !, % TO DO: try and merge A,B |
| 1915 | ? | (check_subset_avl(A,AVL1,Hyps) -> true ; check_subset_avl(B,AVL1,Hyps)). |
| 1916 | | check_subset_avl(intersection(A,B),AVL1,Hyps) :- !, % AVL <: A /\ B if AVL <: A & AVL <: B |
| 1917 | | (check_subset_avl(A,AVL1,Hyps) -> check_subset_avl(B,AVL1,Hyps)). |
| 1918 | | check_subset_avl(interval(L2,U2),AVL,_) :- number(L2),number(U2),!, |
| 1919 | | check_avl_in_interval(AVL,L2,U2). |
| 1920 | | check_subset_avl(value(avl_set(AVL2)),AVL1,_) :- !, check_avl_subset(AVL1,AVL2). |
| 1921 | ? | check_subset_avl(seq(MAX),AVL,Hyps) :- maximal_set(MAX,Hyps), !, is_avl_set_of_sequences(AVL,seq). |
| 1922 | | check_subset_avl(seq1(MAX),AVL,Hyps) :- maximal_set(MAX,Hyps), !, is_avl_set_of_sequences(AVL,seq1). |
| 1923 | | check_subset_avl(seq(seq(MAX)),AVL,Hyps) :- maximal_set(MAX,Hyps), |
| 1924 | | % comes from general concat |
| 1925 | | custom_explicit_sets:is_one_element_avl(AVL,Element), % usually one value from try_get_set_of_possible_values |
| 1926 | | is_sequence(Element,seq), |
| 1927 | | expand_custom_set_to_list(Element,ListOfSeqs), |
| 1928 | | maplist(is_subsequence,ListOfSeqs). |
| 1929 | | check_subset_avl(A,AVL,Hyps) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!, |
| 1930 | | check_subset_avl(A2,AVL,Hyps2). |
| 1931 | | check_subset_avl(A,AVL,Hyps) :- |
| 1932 | ? | avl_fetch_worthwhile_equal_from_hyps(A,Hyps,A2,Hyps2), |
| 1933 | | rewrite_local_loop_check(A,check_subset_avl,A2,Hyps2,Hyps3), |
| 1934 | | check_subset_avl(A2,AVL,Hyps3). |
| 1935 | | %check_subset_avl(A,AVL,_) :- print(check_subset_avl_failed(A,AVL)),nl,fail. |
| 1936 | | |
| 1937 | | is_subsequence((int(_Index),Sequence)) :- is_sequence(Sequence,seq). |
| 1938 | | |
| 1939 | | is_sequence(avl_set(SeqAVL),_) :- safe_is_avl_sequence(SeqAVL). |
| 1940 | | is_sequence([],seq). |
| 1941 | | |
| 1942 | | % check if all elements of the AVL are sequences |
| 1943 | | is_avl_set_of_sequences(AVL,SeqType) :- avl_height(AVL,Height), Height<7, |
| 1944 | | expand_custom_set_to_list(avl_set(AVL),ListOfSeqs), |
| 1945 | | l_is_sequence(ListOfSeqs,SeqType). |
| 1946 | | l_is_sequence([],_). |
| 1947 | | l_is_sequence([S1|T],SeqType) :- is_sequence(S1,SeqType), l_is_sequence(T,SeqType). |
| 1948 | | |
| 1949 | | |
| 1950 | | :- use_module(probsrc(b_global_sets),[b_global_set/1]). |
| 1951 | | maximal_set('INTEGER',_). % integer_set('INTEGER') ? |
| 1952 | | maximal_set(real_set,_). |
| 1953 | | maximal_set(string_set,_). |
| 1954 | | maximal_set(bool_set,_). |
| 1955 | | maximal_set('typeset',_). |
| 1956 | | maximal_set(cartesian_product(A,B),Hyps) :- % SIMP_CPROD_EQUAL_TYPE |
| 1957 | ? | maximal_set(A,Hyps), maximal_set(B,Hyps). |
| 1958 | | maximal_set(relations(A,B),Hyps) :- % SIMP_TYPE_EQUAL_REL |
| 1959 | ? | maximal_set(A,Hyps), maximal_set(B,Hyps). |
| 1960 | | maximal_set(set_subtraction(A,B),Hyps) :- % SIMP_SETMINUS_EQUAL_TYPE |
| 1961 | ? | maximal_set(A,Hyps), check_equal_empty_set(B,Hyps,_). |
| 1962 | ? | maximal_set(pow_subset(A),Hyps) :- maximal_set(A,Hyps). |
| 1963 | ? | maximal_set('$'(ID),Hyps) :- is_global_set_id(ID,Hyps). |
| 1964 | | maximal_set(value(avl_set(AVL)),_) :- |
| 1965 | | quick_definitely_maximal_set_avl(AVL). |
| 1966 | | maximal_set(set_extension(A),Hyps) :- maximal_set_extension(A,Hyps). |
| 1967 | | % sorted_set_extension is never maximal |
| 1968 | | maximal_set(CompSet,_) :- is_comprehension_set(CompSet,_,truth). |
| 1969 | | %maximal_set(X,_) :- print(max_fail(X)),nl,fail. |
| 1970 | | |
| 1971 | | construct_set_extension([],_,Res) :- !, Res=empty_set. |
| 1972 | | construct_set_extension(L,Hyps,Res) :- maximal_set_extension(L,Hyps),!, Res='typeset'. |
| 1973 | | construct_set_extension(L,_,sorted_set_extension(SL)) :- |
| 1974 | | %length(L,Len), format('Construct set_extension ~w~n',[Len]), |
| 1975 | | sort(L,SL). |
| 1976 | | |
| 1977 | | maximal_set_extension([boolean_true|T],_) :- !, member(boolean_false,T). |
| 1978 | | maximal_set_extension([boolean_false|T],_) :- !, member(boolean_true,T). |
| 1979 | | maximal_set_extension(['$'(ID)|T],Hyps) :- |
| 1980 | | is_global_constant_id(ID,Hyps), |
| 1981 | | sort(['$'(ID)|T],Sorted), |
| 1982 | | maplist(is_glob_const_id(Hyps),Sorted), % all elements are global constants |
| 1983 | | lookup_global_constant(ID,fd(_,GlobalSet)), |
| 1984 | | enumerated_set(GlobalSet),b_global_set_cardinality(GlobalSet,Size), |
| 1985 | | length(Sorted,Size). |
| 1986 | | %maximal_set_extension(X,_) :- print(maximal_failed(X)),nl,fail. |
| 1987 | | |
| 1988 | | is_glob_const_id(Hyps,'$'(ID)) :- is_global_constant_id(ID,Hyps). |
| 1989 | | |
| 1990 | | |
| 1991 | | is_global_set_id(ID,Hyps) :- |
| 1992 | ? | b_global_set(ID), |
| 1993 | | \+ is_hyp_var(ID,Hyps). % global enumerated set visible |
| 1994 | | |
| 1995 | | % often called with 0 or 1 in first position |
| 1996 | | check_leq(I,I,_) :- !. |
| 1997 | | check_leq(if_then_else(Pred,A1,A2),B,Hyp) :- !, |
| 1998 | | push_and_rename_normalized_hyp(Pred,Hyp,Hyp1), |
| 1999 | | (hyps_inconsistent(Hyp1) -> true ; check_leq(A1,B,Hyp1) -> true), |
| 2000 | | push_and_rename_normalized_hyp(negation(Pred),Hyp,Hyp2), |
| 2001 | | (hyps_inconsistent(Hyp2) -> true ; check_leq(A2,B,Hyp2) -> true). |
| 2002 | | check_leq(N1,N2,_) :- number(N1), number(N2), !, N1 =< N2. |
| 2003 | | check_leq(N1,N2,hyp_rec(AVL,_)) :- |
| 2004 | | (avl_fetch(less_equal(N1,N2),AVL) |
| 2005 | | -> true |
| 2006 | | ; avl_fetch(equal(N1,N2),AVL)),!. |
| 2007 | | check_leq(min(List),N2,Hyps) :- !, |
| 2008 | | member(N1,List), check_leq(N1,N2,Hyps),!. |
| 2009 | | check_leq(min_int,N2,Hyps) :- !, % we could look up the value of MININT; but largest possible value is -1 |
| 2010 | | MININT is -1, |
| 2011 | | check_leq(MININT,N2,Hyps). |
| 2012 | | check_leq(N1,max_int,Hyps) :- !, % we could look up the value of MAXINT; but smallest possible value is 1 |
| 2013 | | MAXINT = 1, |
| 2014 | | check_leq(N1,MAXINT,Hyps). |
| 2015 | | check_leq(N1,N2,Hyps) :- |
| 2016 | ? | rewrite_integer(N2,Hyps,RN2,Hyps2),!, |
| 2017 | ? | check_leq(N1,RN2,Hyps2). |
| 2018 | | check_leq(add(N1,1),N2,Hyps) :- |
| 2019 | ? | check_not_equal(N1,N2,Hyps), |
| 2020 | | !, % N1+1 <= N2 if N1 <= N2 & N1 \= N2 ; happens quite often in array traversals |
| 2021 | ? | check_leq(N1,N2,Hyps). |
| 2022 | | check_leq(N1,minus(N2,1),Hyps) :- % variation of rule above |
| 2023 | ? | check_not_equal(N1,N2,Hyps), |
| 2024 | | !, % N1 <= N2-1 if N1 <= N2 & N1 \= N2 ; happens in array traversals |
| 2025 | | check_leq(N1,N2,Hyps). |
| 2026 | | check_leq(Nr,X,Hyps) :- |
| 2027 | | \+ number(X), |
| 2028 | ? | try_get_set_of_possible_values(X,Hyps,SetX,Hyps2), |
| 2029 | ? | check_all_values_geq_val(SetX,Nr,Hyps2),!. |
| 2030 | | check_leq(Nr,X,Hyps) :- number(Nr), !, |
| 2031 | ? | check_leq_nr(Nr,X,Hyps). |
| 2032 | | check_leq(N1,N2,Hyps) :- rewrite_integer(N1,Hyps,RN1,Hyps2),!, |
| 2033 | | check_leq(RN1,N2,Hyps2). |
| 2034 | | check_leq(Add,N2,Hyps) :- % A+N1 <= N2 <=> A <= N2-N1 |
| 2035 | | number(N2), |
| 2036 | | add_with_number(Add,A,N1),!, |
| 2037 | | N21 is N2-N1, |
| 2038 | | check_leq(A,N21,Hyps). |
| 2039 | | check_leq(Mul,N2,Hyps) :- % A*N1 <= N2 if A <= N2/N1 if N1>0 and N2 mod N1=0 |
| 2040 | | number(N2), |
| 2041 | | mul_with_number(Mul,Hyps,A,N1), |
| 2042 | | % symmetrical case to check_leq_nr(N1,Mul,Hyps), with N1=-N2 |
| 2043 | | !, |
| 2044 | | ( N1=0 -> check_leq(0,N2,Hyps) |
| 2045 | | ; N1>0 -> N21 is N2 div N1, % A <= 1.5 means we have to have A <= 1; |
| 2046 | | % A <= -1.5 means we have to have A <= -2 -3 div 2 =:= -2 |
| 2047 | | check_leq(A,N21,Hyps) |
| 2048 | | ; cdiv(N2,N1,N21), % A >= 1.5 means we have to have A >= 2 ; cdiv |
| 2049 | | check_leq(N21,A,Hyps) |
| 2050 | | ). |
| 2051 | | check_leq(div(A,N1),N2,Hyps) :- |
| 2052 | | number(N1),number(N2), N1>0, |
| 2053 | | !, |
| 2054 | | (N2=0 -> N12 is N2-1 % A/4 <= 0 <=> A <= 3 |
| 2055 | | ; N2 >= 0 -> N12 is (N2+1)*N1-1 % A/4 <= 10 <=> A <= 49 % A/N1 <= N2 <=> A <= (N1+1)*N2-1 |
| 2056 | | ; N12 is N2*N1 % A/4 <= -10 <=> A <= -40 |
| 2057 | | ), |
| 2058 | | check_leq(A,N12,Hyps). |
| 2059 | | check_leq(div(A1,N1),A2,Hyps) :- number(N1), N1>0, % A/N1 <= A if N1>0 & A>=0 |
| 2060 | | check_equal(A1,A2,Hyps,Hyps1),!, |
| 2061 | | check_leq(0,A1,Hyps1). |
| 2062 | | check_leq(modulo(A1,A2),B,Hyps) :- |
| 2063 | | \+ z_or_tla_minor_mode, % args to mod must be non-negative, modulo is between 0..A2-1 |
| 2064 | | ((number(A2),A21 is A2-1 -> check_leq(A21,B,Hyps) |
| 2065 | | ; B=minus(B1,1) -> check_leq(A2,B1,Hyps) |
| 2066 | | ; check_leq(A2,B,Hyps) |
| 2067 | | ) -> true |
| 2068 | | ; check_leq(A1,B,Hyps)). |
| 2069 | | % TO DO: modulo as RHS |
| 2070 | | check_leq(unary_minus(A),unary_minus(B),Hyps) :- !, % -A <= -B ---> A >= B |
| 2071 | | check_leq(B,A,Hyps). |
| 2072 | | check_leq(X,Nr,Hyps) :- \+ number(X), |
| 2073 | ? | try_get_set_of_possible_values(X,Hyps,SetX,Hyps2), |
| 2074 | ? | check_all_values_leq_val(SetX,Nr,Hyps2),!. % cut here; get set of possible values can give multiple solutions |
| 2075 | | check_leq(Minus,N2,Hyps) :- minus_with_number(Minus,N1,Nr), |
| 2076 | | Nr >= 0,!, % N1-Nr <= N2 if N1 <= N2 |
| 2077 | | % Both N1 and N2 are usually not numbers here |
| 2078 | | check_leq(N1,N2,Hyps). |
| 2079 | | check_leq(N1,Add,Hyps) :- |
| 2080 | | add_with_number(Add,N2,Nr),Nr >= 0,!, % N1 <= N2+Nr if N1 <= N2 |
| 2081 | | % Both N1 and N2 are usually not numbers here |
| 2082 | | check_leq(N1,N2,Hyps). |
| 2083 | | check_leq(add(A,B),E,Hyps) :- |
| 2084 | ? | decompose_floor(E,Hyps,X,Y), % e.g. divide a number E by 2 |
| 2085 | | check_leq(A,X,Hyps), % TO DO: other combinations like A <= 0, B <= Nr; or we could try_get_set_of_possible_values |
| 2086 | | check_leq(B,Y,Hyps). |
| 2087 | | check_leq('$'(X),N2,Hyps) :- |
| 2088 | ? | avl_fetch_binop_from_hyps('$'(X),less_equal,Hyps,Y,Hyps2), |
| 2089 | | (number(N2),avl_fetch_not_equal('$'(X),Y,Hyps) % as we know X and Y we can use regular avl_fetch |
| 2090 | | -> N21 is N2+1 % we have X<Y in the Hypotheses, we just require that Y <= N2+1 |
| 2091 | | ; N21=N2), |
| 2092 | | check_leq(Y,N21,Hyps2). |
| 2093 | | check_leq(Nr,'$'(X),Hyps) :- |
| 2094 | ? | ( avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2), |
| 2095 | | rewrite_local_loop_check(X,check_leq,Y,Hyps2,Hyps3), |
| 2096 | | check_leq(Nr,Y,Hyps3) -> true |
| 2097 | | % ; avl_fetch_binop_from_hyps('$'(X),greater,Hyps,Y,Hyps2), N1 is Nr-1, check_leq(N1,Y,Hyps2) -> true |
| 2098 | ? | ; avl_fetch_binop_from_hyps('$'(X),greater_equal,Hyps,Y,Hyps2), |
| 2099 | | % note: Nr is not a number, hence probably not useful to check not_equal in Hyps, as we cannot compute Nr-1 |
| 2100 | | check_leq(Nr,Y,Hyps2) |
| 2101 | | -> true |
| 2102 | | ), |
| 2103 | | !. |
| 2104 | | %check_leq(A,B,_H) :- print(check_leq_failed(A,B)),nl, portray_hyps(_H),nl,fail. |
| 2105 | | |
| 2106 | | % decompose an expression E into A and B so that A+B <= E |
| 2107 | ? | decompose_floor(X,Hyps,A,B) :- get_number(X,Hyps,Nr),!, |
| 2108 | | A is Nr div 2, B=A. % -11 div 2 -> -6, -1 div 2 = -1, 11 div 2 = 5 |
| 2109 | | decompose_floor(add(A,B),_Hyps,A,B). % TO DO: we could try other order |
| 2110 | | decompose_floor(Mul,Hyps,A,A) :- |
| 2111 | | mul_with_number(Mul,Hyps,A,Nr), |
| 2112 | | Nr>=2, % we could divide Nr by 2 |
| 2113 | | (Nr=2 -> true % we have exactly A+A = Mul |
| 2114 | | ; check_leq(0,A,Hyps)). % Note: -10/10 + -10/10 is not <= -10 |
| 2115 | | |
| 2116 | | % ceiling division utility |
| 2117 | | cdiv(N1,N2,Res) :- |
| 2118 | | (N1 mod N2 =:= 0 -> Res is N1//N2 |
| 2119 | | ; Res is (N1 div N2)+1). |
| 2120 | | |
| 2121 | | % Number <= Expression |
| 2122 | | check_leq_nr(N1,Add,Hyps) :- % N1 <= A+N2 <=> N1-N2 <= A |
| 2123 | | add_with_number(Add,A,N2), !, |
| 2124 | | N12 is N1-N2, |
| 2125 | | check_leq(N12,A,Hyps). |
| 2126 | | check_leq_nr(Nr,add(N1,N2),Hyps) :- !, % 0 <= A+B if 0 <= A & 0 <= B |
| 2127 | | % Both N1 and N2 are usually not numbers here |
| 2128 | | cdiv(Nr,2,Nr2), % Note: cdiv(-3,2) = 1, cdiv(3,2)=2 |
| 2129 | | check_leq(Nr2,N1,Hyps), |
| 2130 | | check_leq(Nr2,N2,Hyps). |
| 2131 | | check_leq_nr(N1,minus(N2,B),Hyps) :- % N1 <= N2-B <=> B <= N2-N1 |
| 2132 | | number(N2), !, |
| 2133 | | N21 is N2-N1, |
| 2134 | ? | check_leq(B,N21,Hyps). |
| 2135 | | check_leq_nr(N1,Mul,Hyps) :- % N1 <= A*N2 if N1/N2 <= A and N2>0 |
| 2136 | | mul_with_number(Mul,Hyps,A,N2), |
| 2137 | | !, |
| 2138 | | ( N2=0 -> check_leq(N1,0,Hyps) |
| 2139 | | ; N2>0 -> cdiv(N1,N2,N12), % cdiv |
| 2140 | | % if 1.5 <= A --> 2 <= A ; if -1.5 <= A --> -1 <= A |
| 2141 | | check_leq(N12,A,Hyps) |
| 2142 | | ; N12 is N1 div N2, |
| 2143 | | % if A <= 1.5 --> A <= 1 ; if -1.5 <= A --> -1 <= A |
| 2144 | | % A <= -1.5 means we have to have A <= -2 -3 div 2 =:= -2 |
| 2145 | | check_leq(A,N12,Hyps) |
| 2146 | | ). |
| 2147 | | check_leq_nr(0,multiplication(A,B),Hyps) :- !, % 0 <= A*B if A and B have same parity |
| 2148 | | (check_leq(0,A,Hyps) -> check_leq(0,B,Hyps) |
| 2149 | | ; check_leq(A,0,Hyps) -> check_leq(B,0,Hyps)). |
| 2150 | | check_leq_nr(N1,div(A,N2),Hyps) :- % N1 <= A/N2 <=> N1*N2 <= A |
| 2151 | | number(N2), N2>0, % TODO: case if N2<0 |
| 2152 | | !, |
| 2153 | | (N1 > 0 -> N12 is N1*N2 % 10 <= A/4 <=> 40 <= A |
| 2154 | | ; N1 = 0 -> N12 is 1-N2 % 0 <= A/4 <=> -3 <= A |
| 2155 | | ; N12 is (N1 - 1)*(N2)+1 % -10 <= A/4 <=> -49 <= A |
| 2156 | | ), |
| 2157 | | check_leq(N12,A,Hyps). |
| 2158 | | check_leq_nr(0,div(A,B),Hyps) :- !, % 0 <= A/B guaranteed if A and B have same parity |
| 2159 | | (check_leq(0,A,Hyps) -> check_leq(0,B,Hyps) % B \= 0 checked by other WD condition |
| 2160 | | ; check_leq(A,0,Hyps) -> check_leq(B,0,Hyps)). % ditto |
| 2161 | | % TODO: other solutions possible, e.g., -1/100 = 1/-100 = 0 |
| 2162 | | check_leq_nr(Nr,'$'(X),Hyps) :- |
| 2163 | ? | ( avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2), |
| 2164 | | rewrite_local_loop_check(X,check_leq,Y,Hyps2,Hyps3), |
| 2165 | | check_leq(Nr,Y,Hyps3) -> true |
| 2166 | | % ; avl_fetch_binop_from_hyps('$'(X),greater,Hyps,Y,Hyps2), N1 is Nr-1, check_leq(N1,Y,Hyps2) -> true |
| 2167 | ? | ; avl_fetch_binop_from_hyps('$'(X),greater_equal,Hyps,Y,Hyps2), |
| 2168 | | (avl_fetch_not_equal('$'(X),Y,Hyps2) % we have X < Y => sufficient to prove N-1 <= Y |
| 2169 | | -> N1 is Nr-1, check_leq(N1,Y,Hyps2) |
| 2170 | | ; check_leq(Nr,Y,Hyps2) |
| 2171 | | ) |
| 2172 | | ), |
| 2173 | | !. |
| 2174 | | 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 |
| 2175 | | (Nr =< 0 -> true % modulo always positive or 0 |
| 2176 | | ; % Nr <= A mod B if Nr <= A and A < B |
| 2177 | | check_leq_nr(Nr,A,Hyps), % Nr <= A |
| 2178 | | check_less(A,B,Hyps)). % and A < B so that modulo does not take effect |
| 2179 | | check_leq_nr(Nr,size(Seq),Hyps) :- check_leq_nr_size(Nr,Seq,Hyps). |
| 2180 | | check_leq_nr(1,power_of(A,_),Hyps) :- check_leq(1,A,Hyps). % Nr <= 1 <= x**y if x >= 1 |
| 2181 | | check_leq_nr(Nr,power_of(A,_),Hyps) :- number(Nr), Nr =< 0, |
| 2182 | | check_leq(0,A,Hyps). % 0 <= x**y if x >= 0 |
| 2183 | | %check_leq_nr(A,B,_H) :- print(check_leq_nr_failed(A,B)),nl,fail. |
| 2184 | | |
| 2185 | | check_less(A,B,Hyps) :- |
| 2186 | ? | check_leq(A,B,Hyps),!, |
| 2187 | | check_not_equal(A,B,Hyps). |
| 2188 | | |
| 2189 | | :- use_module(probsrc(specfile),[z_or_tla_minor_mode/0]). |
| 2190 | | |
| 2191 | | |
| 2192 | | check_leq_nr_size(Nr,restrict_front(_,RestrN),Hyps) :- !, % X <= size( Seq /|\ N) if X <= N as WD condition implies N : 0..size(Seq) |
| 2193 | | check_leq_nr(Nr,RestrN,Hyps). |
| 2194 | | check_leq_nr_size(1,Seq,Hyps) :- check_is_non_empty_sequence(Seq,Hyps). |
| 2195 | | |
| 2196 | | add_with_number(add(A,B),X,Nr) :- (number(A) -> Nr=A, X=B ; number(B) -> Nr=B, X=A). |
| 2197 | | add_with_number(minus(A,B),A,Nr) :- number(B), Nr is -B. |
| 2198 | | mul_with_number(multiplication(A,B),Hyps,X,Nr) :- |
| 2199 | | (get_number(A,Hyps,Nr) -> X=B ; get_number(B,Hyps,Nr) -> X=A). |
| 2200 | | mul_with_number(unary_minus(A),_Hyps,A,Nr) :- Nr is -1. |
| 2201 | | minus_with_number(add(A,B),A,Nr) :- number(B), Nr is -B. |
| 2202 | | minus_with_number(minus(A,Nr),A,Nr) :- number(Nr). |
| 2203 | | |
| 2204 | | |
| 2205 | | %get_possible_values('$'(X),Hyps,SetX,Hyps2) :- |
| 2206 | | % avl_fetch_binop_from_hyps('$'(X),member,Hyps,SetX,Hyps2). |
| 2207 | | |
| 2208 | | % a few rewrite rules for integer expressions |
| 2209 | | % addition/multiplication is dealt with in other places (and is usually done symbolically) |
| 2210 | | rewrite_integer(size(Seq),Hyps,Size,Hyps2) :- % can happen for sequence POs, like restrict_front,tail |
| 2211 | ? | compute_card_of_set(Seq,Hyps,Size,Hyps2),!. |
| 2212 | ? | rewrite_integer(card(Seq),Hyps,Size,Hyps2) :- !, rewrite_card_of_set(Seq,Hyps,Size,Hyps2). |
| 2213 | | rewrite_integer(assertion_expression(_,_,Expr),Hyps,Expr,Hyps). % TO DO: add Predicate to Hyps? |
| 2214 | | % the following may be done by ast_cleanup, but e.g., when applying functions no cleanup is run in l_rename_and_prove_goals |
| 2215 | | rewrite_integer(add(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1), number(A1), |
| 2216 | | (compute_integer(B,Hyps1,B1,Hyps2), number(B1) |
| 2217 | | -> Res is A1+B1 |
| 2218 | | ; A1=0 -> Res = B, Hyps2=Hyps1). |
| 2219 | | rewrite_integer(multiplication(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1), number(A1),!, |
| 2220 | | (A1=0 -> Res=0, Hyps2=Hyps1 |
| 2221 | | ; compute_integer(B,Hyps1,B1,Hyps2), number(B1) |
| 2222 | | -> Res is A1*B1 |
| 2223 | | ; A1=1 -> Res=B, Hyps2=Hyps1). |
| 2224 | | rewrite_integer(multiplication(A,B),Hyps,Res,Hyps2) :- |
| 2225 | | compute_integer(B,Hyps,B1,Hyps2), number(B1), |
| 2226 | | (B1=0 -> Res=0 |
| 2227 | | ; B1=1 -> Res = A). |
| 2228 | | rewrite_integer(unary_minus(A),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps2), number(A1), |
| 2229 | | Res is -A1. |
| 2230 | | rewrite_integer(minus(A,B),Hyps,Res,Hyps2) :- compute_integer(B,Hyps,B1,Hyps1), number(B1), |
| 2231 | | (compute_integer(A,Hyps1,A1,Hyps2), number(A1) |
| 2232 | | -> Res is A1-B1 |
| 2233 | | ; B1=0 -> Res = A, Hyps2=Hyps1). |
| 2234 | | rewrite_integer(power_of(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1), number(A1), |
| 2235 | | compute_integer(B,Hyps1,B1,Hyps2), number(B1), B1 >=0, |
| 2236 | | % check if not too large: |
| 2237 | | (abs(A1) < 2 -> true |
| 2238 | | ; A1=2 -> B1 =< 64 |
| 2239 | | ; A1 < 4294967296 -> B1 =< 2 |
| 2240 | | ; B1 =< 0 |
| 2241 | | ), |
| 2242 | | Res is A1 ^ B1. |
| 2243 | | rewrite_integer(modulo(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1),number(A1), |
| 2244 | | A1 >= 0, |
| 2245 | | compute_integer(B,Hyps1,B1,Hyps2), number(B1), B1 >0, |
| 2246 | | Res is A1 mod B1. |
| 2247 | | rewrite_integer(div(A,B),Hyps,Res,Hyps2) :- |
| 2248 | | compute_integer(B,Hyps,B1,Hyps1), number(B1), B1 \= 0, |
| 2249 | | (compute_integer(A,Hyps1,A1,Hyps2), number(A1) |
| 2250 | | -> Res is A1 // B1 % Prolog division corresponds to B division |
| 2251 | | ; B1=1 -> Res=A, Hyps2=Hyps1). |
| 2252 | | rewrite_integer(integer(X),Hyps,X,Hyps) :- integer(X), write(wd_unnormalised_integer(X)),nl. % should not happen |
| 2253 | | rewrite_integer(real(X),Hyps,Res,Hyps) :- atom(X), construct_real(X,term(floating(Res))). |
| 2254 | | rewrite_integer(convert_int_floor(RX),Hyps,X,Hyps1) :- |
| 2255 | | compute_integer(RX,Hyps,RX1,Hyps1), number(RX1), X is floor(RX1). %, print(rewr_floor(RX,X)),nl. |
| 2256 | | rewrite_integer(convert_int_ceiling(RX),Hyps,X,Hyps1) :- |
| 2257 | | compute_integer(RX,Hyps,RX1,Hyps1), number(RX1), X is ceiling(RX1). |
| 2258 | | rewrite_integer(convert_real(A),Hyps,RX,Hyps1) :- |
| 2259 | | compute_integer(A,Hyps,A1,Hyps1), integer(A1), RX is float(A1). |
| 2260 | | |
| 2261 | | rewrite_card_of_set(Set,Hyps,Size,Hyps2) :- |
| 2262 | ? | compute_card_of_set(Set,Hyps,Size,Hyps2),!. |
| 2263 | | rewrite_card_of_set(interval(1,Up),Hyps,Size,Hyps) :- !, % useful if Up is a symbolic expression |
| 2264 | | Size=Up. |
| 2265 | ? | rewrite_card_of_set(Set,Hyps,Size,Hyps2) :- rewrite_set_expression_exact(Set,Hyps,S2,Hyps1), |
| 2266 | | rewrite_card_of_set(S2,Hyps1,Size,Hyps2). |
| 2267 | | |
| 2268 | ? | compute_integer(A,Hyps,Res,Hyps) :- get_number(A,Hyps,Nr),!,Res=Nr. |
| 2269 | | compute_integer(A,H,Res,H2) :- rewrite_integer(A,H,Res,H2). |
| 2270 | | |
| 2271 | | get_number(A,_Hyps,Nr) :- number(A),!,Nr=A. |
| 2272 | | get_number('$'(ID),Hyps,Nr) :- Hyps \= nohyps, |
| 2273 | ? | avl_fetch_equal_from_hyps('$'(ID),Hyps,Nr,_Hyps1), number(Nr). |
| 2274 | | |
| 2275 | | |
| 2276 | | :- use_module(probsrc(b_global_sets), [enumerated_set/1, b_global_set_cardinality/2]). |
| 2277 | | compute_card_of_set(empty_set,Hyps,0,Hyps). |
| 2278 | | compute_card_of_set(empty_sequence,Hyps,0,Hyps). |
| 2279 | | compute_card_of_set(bool_set,Hyps,2,Hyps). |
| 2280 | | compute_card_of_set(interval(L,U),Hyps,Size,Hyps) :- number(L), number(U), Size is U+1-L. |
| 2281 | | compute_card_of_set(value(Val),Hyps,Size,Hyps) :- get_set_val_size(Val,Size). |
| 2282 | | compute_card_of_set(sequence_extension(List),Hyps,Size,Hyps) :- length(List,Size). |
| 2283 | | compute_card_of_set(set_extension([_]),Hyps,Size,Hyps) :- Size=1. % to do check if all elements definitely different |
| 2284 | | compute_card_of_set(sorted_set_extension([_]),Hyps,Size,Hyps) :- Size=1. % ditto |
| 2285 | | compute_card_of_set(rev(A),Hyps,Size,Hyps2) :- !, compute_card_of_set(A,Hyps,Size,Hyps2). |
| 2286 | | compute_card_of_set(front(A),Hyps,Size,Hyps2) :- !, compute_card_of_set(tail(A),Hyps,Size,Hyps2). |
| 2287 | | compute_card_of_set(tail(A),Hyps,Size,Hyps2) :- !, |
| 2288 | | compute_card_of_set(A,Hyps,Size1,Hyps2), number(Size1), Size1>0, |
| 2289 | | Size is Size1-1. |
| 2290 | | compute_card_of_set(concat(A,B),Hyps,Size,Hyps2) :- |
| 2291 | | compute_card_of_set(A,Hyps,SA,Hyps1),!, |
| 2292 | | compute_card_of_set(B,Hyps1,SB,Hyps2), |
| 2293 | | Size is SA+SB. |
| 2294 | | compute_card_of_set('$'(ID),Hyps,Size,Hyps) :- is_enumerated_set(ID,Hyps), |
| 2295 | | !, |
| 2296 | | b_global_set_cardinality(ID,Size). |
| 2297 | | compute_card_of_set('$'(ID),Hyps,Size,Hyps2) :- |
| 2298 | ? | avl_fetch_equal_from_hyps('$'(ID),Hyps,X2,Hyps1), |
| 2299 | | compute_card_of_set(X2,Hyps1,Size,Hyps2),!. |
| 2300 | | compute_card_of_set('$'(ID),Hyps,Size,Hyps4) :- % e.g., f:1..10 --> BOOL --> card(f) = 10 |
| 2301 | ? | avl_fetch_binop_from_hyps('$'(ID),member,Hyps,FunctionType,Hyps1), |
| 2302 | | is_partial_function_type(FunctionType,Hyps1,Hyps2), |
| 2303 | | get_exact_domain_of_func_or_rel_type(FunctionType,Hyps2,Dom,Hyps3), |
| 2304 | | compute_card_of_set(Dom,Hyps3,Size,Hyps4). |
| 2305 | | %compute_card_of_set(S,_,_,_) :- print(card_fail(S)),nl,fail. |
| 2306 | | |
| 2307 | | get_set_val_size([],0). |
| 2308 | | get_set_val_size(avl_set(AVL),Size) :- avl_size(AVL,Size). |
| 2309 | | |
| 2310 | | |
| 2311 | | check_all_values_geq_val(intersection(A,B),Nr,Hyps) :- |
| 2312 | | (check_all_values_geq_val(A,Nr,Hyps) -> true ; check_all_values_geq_val(B,Nr,Hyps)). |
| 2313 | | check_all_values_geq_val(union(A,B),Nr,Hyps) :- |
| 2314 | | (check_all_values_geq_val(A,Nr,Hyps) -> check_all_values_geq_val(B,Nr,Hyps)). |
| 2315 | | check_all_values_geq_val(set_subtraction(A,_),Nr,Hyps) :- |
| 2316 | | check_all_values_geq_val(A,Nr,Hyps). |
| 2317 | | check_all_values_geq_val(interval(From,_),Nr,Hyps) :- check_leq(Nr,From,Hyps). |
| 2318 | | check_all_values_geq_val(value(avl_set(AVL)),Nr,Hyps) :- avl_min(AVL,int(Min)), check_leq(Nr,Min,Hyps). |
| 2319 | | check_all_values_geq_val('NATURAL',Nr,Hyps) :- check_leq(Nr,0,Hyps). |
| 2320 | | check_all_values_geq_val('NATURAL1',Nr,Hyps) :- check_leq(Nr,1,Hyps). |
| 2321 | | check_all_values_geq_val(domain(Func),Nr,Hyps) :- |
| 2322 | ? | get_domain_or_superset(Func,Hyps,DomFunc,Hyps2), |
| 2323 | ? | check_all_values_geq_val(DomFunc,Nr,Hyps2). |
| 2324 | | check_all_values_geq_val(range(Func),Nr,Hyps) :- |
| 2325 | ? | get_range_or_superset(Func,Hyps,RanFunc,Hyps2), |
| 2326 | | check_all_values_geq_val(RanFunc,Nr,Hyps2). |
| 2327 | | check_all_values_geq_val(sorted_set_extension(L),Nr,Hyps) :- !, check_all_values_geq_val(set_extension(L),Nr,Hyps). |
| 2328 | | check_all_values_geq_val(set_extension(L),Nr,Hyps) :- |
| 2329 | ? | (member(Val,L), \+ check_leq(Nr,Val,Hyps) -> fail ; true). |
| 2330 | | check_all_values_geq_val('$'(X),Nr,Hyps) :- |
| 2331 | ? | avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2), |
| 2332 | | rewrite_local_loop_check(X,check_all_values_geq_val,Y,Hyps2,Hyps3), |
| 2333 | | check_all_values_geq_val(Y,Nr,Hyps3). |
| 2334 | | %check_all_values_geq_val(A,B,_) :- print(check_all_values_geq_val_failed(A,B)),nl,fail. |
| 2335 | | |
| 2336 | | check_all_values_neq_nr(intersection(A,B),Nr,Hyps) :- |
| 2337 | | (check_all_values_neq_nr(A,Nr,Hyps) -> true ; check_all_values_neq_nr(B,Nr,Hyps)). |
| 2338 | | check_all_values_neq_nr(union(A,B),Nr,Hyps) :- |
| 2339 | | (check_all_values_neq_nr(A,Nr,Hyps) -> check_all_values_neq_nr(B,Nr,Hyps)). |
| 2340 | | check_all_values_neq_nr(set_subtraction(A,_),Nr,Hyps) :- |
| 2341 | | check_all_values_neq_nr(A,Nr,Hyps). |
| 2342 | | check_all_values_neq_nr(interval(From,_),Nr,Hyps) :- number(From),F1 is From-1, check_leq(Nr,F1,Hyps). |
| 2343 | | check_all_values_neq_nr(interval(_,To),Nr,Hyps) :- number(To),T1 is To+1, check_leq(T1,Nr,Hyps). |
| 2344 | | check_all_values_neq_nr('NATURAL',Nr,Hyps) :- check_leq(Nr,-1,Hyps). |
| 2345 | | check_all_values_neq_nr('NATURAL1',Nr,Hyps) :- check_leq(Nr,0,Hyps). |
| 2346 | | check_all_values_neq_nr(sorted_set_extension(L),Nr,Hyps) :- !, check_all_values_neq_nr(set_extension(L),Nr,Hyps). |
| 2347 | | check_all_values_neq_nr(set_extension(L),Nr,Hyps) :- |
| 2348 | | (member(Val,L), \+ check_not_equal(Val,Nr,Hyps) -> fail ; true). |
| 2349 | | check_all_values_neq_nr('$'(X),Nr,Hyps) :- |
| 2350 | | avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2), |
| 2351 | | rewrite_local_loop_check(X,check_all_values_neq_nr,Y,Hyps2,Hyps3), |
| 2352 | | check_all_values_neq_nr(Y,Nr,Hyps3). |
| 2353 | | %check_all_values_neq_nr(A,B,_) :- print(check_all_values_neq_nr_failed(A,B)),nl,fail. |
| 2354 | | |
| 2355 | | |
| 2356 | | check_all_values_leq_val(intersection(A,B),Nr,Hyps) :- |
| 2357 | | (check_all_values_leq_val(A,Nr,Hyps) -> true ; check_all_values_leq_val(B,Nr,Hyps)). |
| 2358 | | check_all_values_leq_val(union(A,B),Nr,Hyps) :- |
| 2359 | | (check_all_values_leq_val(A,Nr,Hyps) -> check_all_values_leq_val(B,Nr,Hyps)). |
| 2360 | | check_all_values_leq_val(set_subtraction(A,_),Nr,Hyps) :- |
| 2361 | | check_all_values_leq_val(A,Nr,Hyps). |
| 2362 | | check_all_values_leq_val(interval(_,To),Nr,Hyps) :- check_leq(To,Nr,Hyps). |
| 2363 | | check_all_values_leq_val(value(avl_set(AVL)),Nr,Hyps) :- avl_max(AVL,int(Max)), check_leq(Max,Nr,Hyps). |
| 2364 | | check_all_values_leq_val(domain(Func),Nr,Hyps) :- |
| 2365 | | get_domain_or_superset(Func,Hyps,DomFunc,Hyps2), |
| 2366 | | check_all_values_leq_val(DomFunc,Nr,Hyps2). |
| 2367 | | check_all_values_leq_val(range(Func),Nr,Hyps) :- |
| 2368 | ? | get_range_or_superset(Func,Hyps,RanFunc,Hyps2), |
| 2369 | | check_all_values_leq_val(RanFunc,Nr,Hyps2). |
| 2370 | | check_all_values_leq_val(sorted_set_extension(L),Nr,Hyps) :- !, check_all_values_leq_val(set_extension(L),Nr,Hyps). |
| 2371 | | check_all_values_leq_val(set_extension(L),Nr,Hyps) :- |
| 2372 | ? | (member(Val,L), \+ check_leq(Val,Nr,Hyps) -> fail ; true). |
| 2373 | | check_all_values_leq_val('$'(X),Nr,Hyps) :- |
| 2374 | ? | avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2), |
| 2375 | | rewrite_local_loop_check(X,check_all_values_leq_val,Y,Hyps2,Hyps3), |
| 2376 | | check_all_values_leq_val(Y,Nr,Hyps3). |
| 2377 | | %check_all_values_leq_val(A,B,_) :- print(check_all_values_leq_val(A,B)),nl,fail. |
| 2378 | | |
| 2379 | | % check if two expressions are definitely different |
| 2380 | | % usually called for check_not_equal 0 or empty_set |
| 2381 | | check_not_equal(A,B,Hyp) :- |
| 2382 | ? | is_explicit_value(A,AV,Hyp), is_explicit_value(B,BV,Hyp), !, AV \= BV. |
| 2383 | ? | check_not_equal(X,Y,Hyp) :- sym_unify(X,Y,if_then_else(Pred,A1,A2),B),!, |
| 2384 | | push_and_rename_normalized_hyp(Pred,Hyp,Hyp1), |
| 2385 | ? | (hyps_inconsistent(Hyp1) -> true ; check_not_equal(A1,B,Hyp1) -> true), |
| 2386 | | push_and_rename_normalized_hyp(negation(Pred),Hyp,Hyp2), |
| 2387 | | (hyps_inconsistent(Hyp2) -> true ; check_not_equal(A2,B,Hyp2) -> true). |
| 2388 | | check_not_equal(N1,N2,Hyps) :- |
| 2389 | | avl_fetch_not_equal(N1,N2,Hyps),!. |
| 2390 | | check_not_equal(couple(A1,A2),couple(B1,B2),Hyps) :- !, |
| 2391 | | (check_not_equal(A1,B1,Hyps) -> true ; check_not_equal(A2,B2,Hyps)). |
| 2392 | | check_not_equal(X,B,Hyps) :- number(B), |
| 2393 | ? | try_get_set_of_possible_values(X,Hyps,SetX,Hyps2), |
| 2394 | ? | check_all_values_neq_nr(SetX,B,Hyps2),!. |
| 2395 | | % TO DO: compute also things like domain(...) for :wd s:perm(1..10) & x:dom(s) & res = 10/x |
| 2396 | ? | check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,unary_minus(A),B),number(B),!, BM is -B, |
| 2397 | | check_not_equal(A,BM,Hyps). |
| 2398 | ? | check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,multiplication(A,B),0),!, % A*B /= 0 if A/=0 & B/=0 |
| 2399 | | check_not_equal(A,0,Hyps),check_not_equal(B,0,Hyps). |
| 2400 | ? | check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,power_of(A,_),0),!, % A**B /= 0 if A/=0 |
| 2401 | | check_not_equal(A,0,Hyps). |
| 2402 | ? | check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,Add,B), |
| 2403 | | add_with_number(Add,A,Nr),!, |
| 2404 | | (Nr>0 -> check_leq(B,A,Hyps) % A >= B => A+Nr > B => A+Nr /= B |
| 2405 | | ; Nr=0 -> check_not_equal(A,B,Hyps) |
| 2406 | | ; check_leq(A,B,Hyps) |
| 2407 | | ). |
| 2408 | ? | check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,A,B),number(B),!, |
| 2409 | | B1 is B+1, |
| 2410 | ? | (check_leq(B1,A,Hyps) -> true % B < A |
| 2411 | | ; B2 is B-1, |
| 2412 | ? | check_leq(A,B2,Hyps)). % A < B |
| 2413 | ? | check_not_equal(XX,YY,Hyps) :- sym_unify(XX,YY,'$'(A),B), |
| 2414 | ? | avl_fetch_binop_from_hyps('$'(A),less_equal,Hyps,Y,Hyps2), |
| 2415 | | (number(B) -> (B1 is B-1, check_leq(Y,B1,Hyps2) -> true) |
| 2416 | | ; avl_fetch_not_equal('$'(A),Y,Hyps) % we have $(A) < Y => prove Y <= B |
| 2417 | | -> 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 |
| 2418 | | ). |
| 2419 | ? | check_not_equal(XX,YY,Hyps) :- sym_unify(XX,YY,'$'(A),B), |
| 2420 | ? | avl_fetch_binop_from_hyps('$'(A),greater_equal,Hyps,Y,Hyps2), |
| 2421 | | (number(B) -> (B1 is B+1, check_leq(B1,Y,Hyps2) -> true) |
| 2422 | | ; avl_fetch_not_equal('$'(A),Y,Hyps) % we have $(A) < Y => prove Y <= B |
| 2423 | | -> check_leq(B,Y,Hyps2) % see comments above |
| 2424 | | ). |
| 2425 | ? | check_not_equal(A,Empty,Hyp) :- is_empty_set_direct(Empty), !, check_not_empty_set(A,Hyp). |
| 2426 | | check_not_equal(Empty,A,Hyp) :- is_empty_set_direct(Empty), !, check_not_empty_set(A,Hyp). |
| 2427 | | check_not_equal(value(avl_set(A)),value(avl_set(B)),_) :- nonvar(A), nonvar(B),!, % nonvar should always be true |
| 2428 | | \+ equal_avl_tree(A,B). |
| 2429 | | check_not_equal(A,B,Hyps) :- |
| 2430 | | (A=set_extension(LA) -> check_not_equal_set_extension(B,LA,Hyps) |
| 2431 | | ; B=set_extension(LB) -> check_not_equal_set_extension(A,LB,Hyps)),!. |
| 2432 | | check_not_equal(A,B,Hyps) :- |
| 2433 | | (is_interval(A,Hyps,Low,Up) -> check_not_equal_interval(B,lhs,Low,Up,Hyps) |
| 2434 | ? | ; is_interval(B,Hyps,Low,Up) -> check_not_equal_interval(A,rhs,Low,Up,Hyps)),!. |
| 2435 | | check_not_equal(A,B,Hyps) :- |
| 2436 | ? | avl_fetch_worthwhile_equal_from_hyps(A,Hyps,Value,Hyps2),!, |
| 2437 | | check_not_equal(Value,B,Hyps2). |
| 2438 | | check_not_equal(A,B,Hyps) :- |
| 2439 | ? | avl_fetch_worthwhile_equal_from_hyps(B,Hyps,Value,Hyps2),!, |
| 2440 | | check_not_equal(A,Value,Hyps2). |
| 2441 | | %check_not_equal(A,B,Hyps) :- print(check_not_equal_failed(A,B)),nl,portray_hyps(Hyps),nl,fail. |
| 2442 | | |
| 2443 | | check_not_equal_interval(MaxSet,_,_,_,Hyps) :- infinite_integer_set(MaxSet,Hyps). |
| 2444 | | check_not_equal_interval(A,lhs,Low,Up,Hyps) :- is_interval(A,Hyps,LowA,UpA), |
| 2445 | | (check_not_empty_interval(Low,Up,Hyps) -> true ; check_not_empty_interval(LowA,UpA,Hyps)), |
| 2446 | | % if one of the intervals is non-empty then it is sufficient for one bound to be different |
| 2447 | | (check_not_equal(LowA,Low,Hyps) -> true |
| 2448 | | ; check_not_equal(UpA,Up,Hyps) -> true). |
| 2449 | | % TODO: other intervals, avl_set |
| 2450 | | |
| 2451 | | infinite_integer_set('INTEGER',_). |
| 2452 | | infinite_integer_set('NATURAL',_). |
| 2453 | | infinite_integer_set('NATURAL1',_). |
| 2454 | | |
| 2455 | | check_not_equal_set_extension(set_extension([B|TB]),[A|TA],Hyps) :- (TA=[];TB=[]),!, |
| 2456 | | check_not_equal(A,B,Hyps). % TO DO: we can generalize this treatment to find one element in one set not in the other |
| 2457 | | check_not_equal_set_extension(value(avl_set(AVL)),LA,Hyps) :- length(LA,MaxSizeA), |
| 2458 | | (avl_size(AVL,Sze),Sze>MaxSizeA -> true % AVL has at least one element more |
| 2459 | | ; is_one_element_avl(AVL,B), LA=[A|_], check_not_equal(A,B,Hyps)). |
| 2460 | | |
| 2461 | | avl_fetch_not_equal(N1,N2,hyp_rec(AVL,_)) :- |
| 2462 | | (avl_fetch(not_equal(N1,N2),AVL) -> true |
| 2463 | | ; avl_fetch(not_equal(N2,N1),AVL)). % we do not store both directions for not_equal |
| 2464 | | |
| 2465 | | % unify two variables with other two variables; useful for symmetric rules |
| 2466 | | sym_unify(A,B,A,B). |
| 2467 | | sym_unify(A,B,B,A). |
| 2468 | | |
| 2469 | | % TO DO: get equalities; maybe we should harmonise this for all rules |
| 2470 | | % we could add rules about min_int, max_int |
| 2471 | | |
| 2472 | | |
| 2473 | | % we should call this to check if something is the empty set: |
| 2474 | | % it does equality rewrites, but also calls check_empty_set/3 indirectly |
| 2475 | | check_equal_empty_set(Set,Hyps,PT) :- PT = check_equal, |
| 2476 | ? | check_equal(Set,empty_set,Hyps,_). % will also call this below: |
| 2477 | | |
| 2478 | | is_empty_set_direct(empty_set). |
| 2479 | | is_empty_set_direct(empty_sequence). |
| 2480 | | is_empty_set_direct(value(X)) :- X==[]. |
| 2481 | | |
| 2482 | | check_empty_set(Set,_,empty_set) :- is_empty_set_direct(Set),!. |
| 2483 | | check_empty_set(A,Hyps,hyp) :- avl_fetch_from_hyps(equal(A,empty_set),Hyps),!. |
| 2484 | | check_empty_set(set_subtraction(A,B),Hyp,subset(PT)) :- !, % see SIMP_SETMINUS_EQUAL_EMPTY Rodin proof rule |
| 2485 | | check_is_subset(A,B,Hyp,PT). |
| 2486 | | check_empty_set(intersection(A,B),Hyps,inter_disjoint) :- !, |
| 2487 | ? | check_disjoint(A,B,Hyps). |
| 2488 | | check_empty_set(union(A,B),Hyps,union_empty(P1,P2)) :- !, % SIMP_BUNION_EQUAL_EMPTY |
| 2489 | | check_equal_empty_set(A,Hyps,P1),!, |
| 2490 | | check_equal_empty_set(B,Hyps,P2). |
| 2491 | | check_empty_set(general_union(A),Hyp,general_union(PT)) :- !, % SIMP_KUNION_EQUAL_EMPTY |
| 2492 | | check_is_subset(A,set_extension([empty_set]),Hyp,PT). |
| 2493 | | check_empty_set(cartesian_product(A,B),Hyps,cart_empty(PT)) :- !, % SIMP_CPROD_EQUAL_EMPTY |
| 2494 | | (check_equal_empty_set(A,Hyps,PT) -> true ; check_equal_empty_set(B,Hyps,PT)). |
| 2495 | | check_empty_set(pow1_subset(A),Hyps,pow1_empty(PT)) :- !, % SIMP_POW1_EQUAL_EMPTY |
| 2496 | | check_equal_empty_set(A,Hyps,PT). |
| 2497 | | check_empty_set(interval(From,To),Hyps,interval_empty) :- !, % SIMP_UPTO_EQUAL_EMPTY |
| 2498 | | check_less(To,From,Hyps). |
| 2499 | | check_empty_set(domain(A),Hyps,domain_empty(PT)) :- !, % SIMP_DOM_EQUAL_EMPTY |
| 2500 | | check_equal_empty_set(A,Hyps,PT). |
| 2501 | | check_empty_set(range(A),Hyps,range_empty(PT)) :- !, % SIMP_RAN_EQUAL_EMPTY |
| 2502 | | check_equal_empty_set(A,Hyps,PT). |
| 2503 | | check_empty_set(reverse(A),Hyps,reverse_empty(PT)) :- !, % SIMP_CONVERSE_EQUAL_EMPTY (relational inverse) |
| 2504 | | check_equal_empty_set(A,Hyps,PT). |
| 2505 | | check_empty_set(total_relation(A,B),Hyp,trel_empty(PTA,PTB)) :- !, % SIMP_SPECIAL_EQUAL_RELDOM |
| 2506 | ? | check_not_equal_empty_set(A,Hyp,PTA), check_equal_empty_set(B,Hyp,PTB). |
| 2507 | | check_empty_set(total_function(A,B),Hyp,tfun_empty(PTA,PTB)) :- !, % SIMP_SPECIAL_EQUAL_RELDOM |
| 2508 | ? | check_not_equal_empty_set(A,Hyp,PTA), check_equal_empty_set(B,Hyp,PTB). |
| 2509 | | check_empty_set(composition(F,G),Hyp,fcomp_empty) :- !, % SIMP_FCOMP_EQUAL_EMPTY |
| 2510 | | check_disjoint(range(F),domain(G),Hyp). |
| 2511 | | check_empty_set(A,Hyps,subset_strict_singleton) :- |
| 2512 | ? | avl_fetch_binop_from_hyps(A,subset_strict,Hyps,B,_), % A <<: {Single} => A={} |
| 2513 | | singleton_set(B,_). |
| 2514 | | % TODO: add more rules inter(A,Singleton) SIMP_BINTER_SING_EQUAL_EMPTY |
| 2515 | | |
| 2516 | | % we should call this to check if something is not the empty set: |
| 2517 | | % it does equality rewrites, but also calls check_not_empty_set/2 indirectly |
| 2518 | | check_not_equal_empty_set(Set,Hyps,not_equal_empty_set) :- |
| 2519 | ? | check_not_equal(Set,empty_set,Hyps). |
| 2520 | | |
| 2521 | | check_not_empty_set(A,Hyps) :- avl_fetch_from_hyps(not_equal(A,empty_set),Hyps),!. |
| 2522 | | check_not_empty_set(A,Hyps) :- %Note: size(A) should be changed to card(A) in normalization |
| 2523 | | (CardA = card(A) ; CardA = size(A)), |
| 2524 | | (Op = equal ; Op = greater_equal), |
| 2525 | ? | avl_fetch_binop_from_hyps(CardA,Op,Hyps,Nr,Hyps2), %Nr \= 0, |
| 2526 | | check_leq(1,Nr,Hyps2),!. % cut here, relevant for test 2043 |
| 2527 | | check_not_empty_set(set_extension([_|_]),_Hyps). |
| 2528 | | check_not_empty_set(sorted_set_extension([_|_]),_Hyps). |
| 2529 | | check_not_empty_set(sequence_extension([_|_]),_Hyps). |
| 2530 | | check_not_empty_set(cartesian_product(A,B),Hyps) :- % SIMP_CPROD_EQUAL_EMPTY |
| 2531 | | (check_not_empty_set(A,Hyps) -> check_not_empty_set(B,Hyps)). |
| 2532 | | check_not_empty_set(interval(A,B),Hyps) :- check_leq(A,B,Hyps). |
| 2533 | | check_not_empty_set(value(avl_set(AVL)),_) :- AVL \= empty. |
| 2534 | ? | check_not_empty_set(union(A,B),Hyp) :- !, (check_not_empty_set(A,Hyp) -> true ; check_not_empty_set(B,Hyp)). |
| 2535 | | check_not_empty_set(general_union(A),Hyp) :- !, % SIMP_KUNION_EQUAL_EMPTY |
| 2536 | | check_not_subset(A,set_extension([empty_set]),Hyp,_PT). |
| 2537 | | check_not_empty_set(set_subtraction(A,B),Hyp) :- !, % see SIMP_SETMINUS_EQUAL_EMPTY Rodin proof rule |
| 2538 | | check_not_subset(A,B,Hyp,_PT). |
| 2539 | ? | check_not_empty_set(overwrite(A,B),Hyp) :- !, (check_not_empty_set(A,Hyp) -> true ; check_not_empty_set(B,Hyp)). |
| 2540 | | check_not_empty_set(domain(A),Hyp) :- !, % SIMP_DOM_EQUAL_EMPTY |
| 2541 | | check_not_empty_set(A,Hyp). |
| 2542 | | check_not_empty_set(range(A),Hyp) :- !, % SIMP_RAN_EQUAL_EMPTY |
| 2543 | | check_not_empty_set(A,Hyp). |
| 2544 | | check_not_empty_set(identity(A),Hyp) :- !, check_not_empty_set(A,Hyp). |
| 2545 | | check_not_empty_set(image(R,interval(L,U)),Hyp) :- !, |
| 2546 | ? | check_not_empty_set(interval(L,U),Hyp), |
| 2547 | | (check_member_of_set(domain(R),L,Hyp,_) -> true |
| 2548 | | ; check_member_of_set(domain(R),U,Hyp,_) |
| 2549 | | ). |
| 2550 | | check_not_empty_set(image(Func,set_extension([S1|_])),Hyp) :- !, |
| 2551 | | check_member_of_set(domain(Func),S1,Hyp,_). |
| 2552 | | check_not_empty_set(reverse(A),Hyp) :- !, % SIMP_CONVERSE_EQUAL_EMPTY (relational inverse) |
| 2553 | | check_not_empty_set(A,Hyp). |
| 2554 | | check_not_empty_set(rev(A),Hyp) :- !, check_not_empty_set(A,Hyp). |
| 2555 | | check_not_empty_set(concat(A,B),Hyp) :- !, (check_not_empty_set(A,Hyp) -> true ; check_not_empty_set(B,Hyp)). |
| 2556 | | check_not_empty_set(bool_set,_Hyp) :- !. |
| 2557 | | check_not_empty_set(float_set,_Hyp) :- !. |
| 2558 | | check_not_empty_set(real_set,_Hyp) :- !. |
| 2559 | | check_not_empty_set(string_set,_Hyp) :- !. |
| 2560 | | check_not_empty_set('NATURAL1',_Hyp) :- !. % SIMP_NATURAL1_EQUAL_EMPTY |
| 2561 | | check_not_empty_set('NATURAL',_Hyp) :- !. % SIMP_NATURAL_EQUAL_EMPTY |
| 2562 | | check_not_empty_set(typeset,_Hyp) :- !. % SIMP_TYPE_EQUAL_EMPTY, all basic sets are non empty in B and Event-B |
| 2563 | | check_not_empty_set(relations(_,_),_Hyp) :- !. % SIMP_SPECIAL_EQUAL_REL |
| 2564 | | check_not_empty_set(total_function(A,B),Hyp) :- !, % SIMP_SPECIAL_EQUAL_RELDOM |
| 2565 | | ( check_equal_empty_set(A,Hyp,_) -> true |
| 2566 | ? | ; check_not_equal_empty_set(B,Hyp,_) -> true |
| 2567 | | ; check_equal(A,B,Hyp,_)). % implicit proof by case distinction |
| 2568 | | check_not_empty_set(total_relation(A,B),Hyp) :- !, % SIMP_SPECIAL_EQUAL_RELDOM |
| 2569 | | check_not_empty_set(total_function(A,B),Hyp). |
| 2570 | | check_not_empty_set(if_then_else(Pred,A,B),Hyp) :- !, |
| 2571 | | push_and_rename_normalized_hyp(Pred,Hyp,Hyp1), |
| 2572 | | (hyps_inconsistent(Hyp1) -> true ; check_not_empty_set(A,Hyp1) -> true), |
| 2573 | | push_and_rename_normalized_hyp(negation(Pred),Hyp,Hyp2), |
| 2574 | | (hyps_inconsistent(Hyp2) -> true ; check_not_empty_set(B,Hyp2) -> true). |
| 2575 | | check_not_empty_set(Expr,Hyps) :- |
| 2576 | ? | is_lambda_function_with_domain(Expr,Domain),!, |
| 2577 | | check_not_empty_set(Domain,Hyps). |
| 2578 | | check_not_empty_set('$'(ID),Hyps) :- |
| 2579 | | enumerated_set(ID), |
| 2580 | | \+ is_hyp_var(ID,Hyps),!. % global enumerated set visible |
| 2581 | | check_not_empty_set(Eq,Hyps) :- |
| 2582 | | (Eq='$'(_) ; Eq=interval(_,_)), |
| 2583 | ? | avl_fetch_equal_from_hyps(Eq,Hyps,Value,Hyps2), |
| 2584 | | rewrite_local_loop_check(Eq,check_not_empty_set,Value,Hyps2,Hyps3), |
| 2585 | ? | check_not_empty_set(Value,Hyps3),!. |
| 2586 | ? | check_not_empty_set(Seq,Hyp) :- infer_sequence_type_of_expr(Seq,Hyp,seq1),!. |
| 2587 | | check_not_empty_set(Func,Hyps) :- Func = '$'(_), |
| 2588 | ? | avl_fetch_binop_from_hyps(Func,member,Hyps,FunctionType,Hyps2), % Func : . --> . |
| 2589 | ? | check_not_empty_elements(FunctionType,Hyps2),!. |
| 2590 | | check_not_empty_set(function(Func,Args),Hyps) :- |
| 2591 | ? | (get_range_or_superset(Func,Hyps,Range,Hyps2), |
| 2592 | | check_not_empty_elements(Range,Hyps2) -> !,true |
| 2593 | ? | ; rewrite_function_application(Func,Args,Hyps,Result,Hyps2), |
| 2594 | | check_not_empty_set(Result,Hyps2)). |
| 2595 | | check_not_empty_set(tail(A),Hyps) :- rewrite_card_of_set(A,Hyps,CardA,Hyps1),!, |
| 2596 | | check_leq(2,CardA,Hyps1). |
| 2597 | | check_not_empty_set(front(A),Hyps) :- rewrite_card_of_set(A,Hyps,CardA,Hyps1),!, |
| 2598 | | check_leq(2,CardA,Hyps1). |
| 2599 | | check_not_empty_set(A,Hyps) :- |
| 2600 | ? | avl_fetch_binop_from_hyps(A,not_subset_strict,Hyps,B,_), % A <<: {Single} <=> A={} |
| 2601 | | singleton_set(B,_),!. |
| 2602 | | check_not_empty_set(A,Hyps) :- |
| 2603 | | ( Lookup = A, Operator = superset |
| 2604 | | ; |
| 2605 | | (Lookup=domain(A) ; Lookup=range(A)), |
| 2606 | | (Operator = superset ; Operator = equal) |
| 2607 | | ), |
| 2608 | ? | avl_fetch_binop_from_hyps(Lookup,Operator,Hyps,B,Hyps2), % B /= {} & B <: A => A /= {} |
| 2609 | | rewrite_local_loop_check(A,check_not_empty_set,B,Hyps2,Hyps3), |
| 2610 | ? | check_not_empty_set(B,Hyps3),!. |
| 2611 | | % 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 |
| 2612 | | %check_not_empty_set(A,H) :- print(check_not_empty_set_failed(A)),nl,portray_hyps(H),nl,fail. |
| 2613 | | % TO DO: more rules for sequence operators; infer_sequence_type_of_expr does not look at values of ids |
| 2614 | | |
| 2615 | | |
| 2616 | | % check if elements of a function type or set are guaranteed to be not empty |
| 2617 | | |
| 2618 | | check_not_empty_elements(fin1_subset(_),_). |
| 2619 | | check_not_empty_elements(pow1_subset(_),_). |
| 2620 | | check_not_empty_elements(seq1(_),_). |
| 2621 | | check_not_empty_elements(iseq1(_),_). |
| 2622 | | check_not_empty_elements(perm(A),Hyps) :- check_not_empty_set(A,Hyps). |
| 2623 | ? | check_not_empty_elements(total_function(A,_),Hyps) :- check_not_empty_set(A,Hyps). |
| 2624 | | check_not_empty_elements(total_injection(A,_),Hyps) :- check_not_empty_set(A,Hyps). |
| 2625 | | check_not_empty_elements(total_surjection(A,B),Hyps) :- |
| 2626 | | (check_not_empty_set(A,Hyps) -> true ; check_not_empty_set(B,Hyps)). |
| 2627 | | check_not_empty_elements(total_bijection(A,B),Hyps) :- |
| 2628 | | (check_not_empty_set(A,Hyps) -> true ; check_not_empty_set(B,Hyps)). |
| 2629 | | check_not_empty_elements(total_relation(A,_),Hyps) :- check_not_empty_set(A,Hyps). |
| 2630 | | check_not_empty_elements(total_surjection_relation(A,_),Hyps) :- check_not_empty_set(A,Hyps). |
| 2631 | | check_not_empty_elements(partial_surjection(_,B),Hyps) :- check_not_empty_set(B,Hyps). |
| 2632 | | check_not_empty_elements(partial_bijection(_,B),Hyps) :- check_not_empty_set(B,Hyps). |
| 2633 | | check_not_empty_elements(surjection_relation(_,B),Hyps) :- check_not_empty_set(B,Hyps). |
| 2634 | | % more cases, set_extension,... |
| 2635 | | |
| 2636 | | :- use_module(probsrc(b_global_sets),[enumerated_set/1]). |
| 2637 | | % check if an expression is definitely finite |
| 2638 | | check_finite(bool_set,_,bool_set) :- !. |
| 2639 | | check_finite(empty_set,_,empty_set) :- !. |
| 2640 | | check_finite(empty_sequence,_,empty_sequence) :- !. |
| 2641 | | check_finite(float_set,_,float_set) :- !. |
| 2642 | | % check_finite(integer_set(X),_,bool_set) :- !. INT, NAT, NAT1 are translated to intervals |
| 2643 | | check_finite(set_extension(_),_,set_extension) :- !. |
| 2644 | | check_finite(sorted_set_extension(_),_,set_extension) :- !. |
| 2645 | | check_finite(sequence_extension(_),_,seq_extension) :- !. |
| 2646 | | check_finite(fin_subset(X),Hyps,fin(PT)) :- !, check_finite(X,Hyps,PT). |
| 2647 | | check_finite(fin1_subset(X),Hyps,fin1(PT)) :- !, check_finite(X,Hyps,PT). |
| 2648 | | check_finite(pow_subset(X),Hyps,pow(PT)) :- !, check_finite(X,Hyps,PT). |
| 2649 | | check_finite(pow1_subset(X),Hyps,pow1(PT)) :- !, check_finite(X,Hyps,PT). |
| 2650 | | check_finite(iseq(X),Hyps,iseq(PT)) :- !, check_finite(X,Hyps,PT). |
| 2651 | | check_finite(iseq1(X),Hyps,iseq1(PT)) :- !, check_finite(X,Hyps,PT). |
| 2652 | | check_finite(mu(Set),Hyps,mu) :- !, has_finite_elements(Set,Hyps). |
| 2653 | | check_finite(perm(X),Hyps,perm(PT)) :- !, check_finite(X,Hyps,PT). |
| 2654 | | check_finite(Set,Hyps,hyp) :- |
| 2655 | | avl_fetch_from_hyps(finite(Set),Hyps),!. |
| 2656 | | check_finite(domain(A),Hyp,dom(PT)) :- !, |
| 2657 | ? | (check_finite(A,Hyp,PT) -> true ; finite_domain(A,Hyp,PT)). |
| 2658 | | check_finite(range(A),Hyp,ran(PT)) :- !, |
| 2659 | ? | (check_finite(A,Hyp,PT) -> true ; finite_range(A,Hyp,PT)). |
| 2660 | ? | check_finite(reverse(A),Hyp,rev(PT)) :- !, check_finite(A,Hyp,PT). |
| 2661 | | check_finite(identity(A),Hyp,id(PT)) :- !,check_finite(A,Hyp,PT). % finite(id(A)) if finite(A) |
| 2662 | | check_finite(function(Func,Args),Hyps,function(PT)) :- !, |
| 2663 | ? | (get_range_or_superset(Func,Hyps,RanFunc,Hyps2), |
| 2664 | | has_finite_elements(RanFunc,Hyps2) -> PT = finite_elements |
| 2665 | | ; rewrite_function_application(Func,Args,Hyps,Result,Hyps2), |
| 2666 | | check_finite(Result,Hyps2,PT)). |
| 2667 | | check_finite(image(Func,B),Hyp,image(PT)) :- !, |
| 2668 | ? | (check_finite(Func,Hyp,PT) -> true % finite(Func[.]) <= finite(Func) |
| 2669 | | ; check_finite(B,Hyp,PTB) |
| 2670 | ? | -> PT = pfun(PTB), check_is_partial_function(Func,Hyp) % finite(Func[B]) <= finite(B) & Func : TD +-> TR |
| 2671 | | ). |
| 2672 | ? | check_finite(union(A,B),Hyp,union(PTA,PTB)) :- !, (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)). |
| 2673 | | check_finite(if_then_else(Pred,A,B),Hyps,if(PTA,PTB)) :- !, |
| 2674 | | push_and_rename_normalized_hyp(Pred,Hyps,Hyps1), |
| 2675 | | (hyps_inconsistent(Hyps1) -> true ; check_finite(A,Hyps1,PTA) -> true), |
| 2676 | | push_and_rename_normalized_hyp(negation(Pred),Hyps,Hyps2), |
| 2677 | | (hyps_inconsistent(Hyps2) -> true ; check_finite(B,Hyps2,PTB) -> true). |
| 2678 | | check_finite(intersection(A,B),Hyps,intersection(D,PT)) :- !, |
| 2679 | ? | (D=left,check_finite(A,Hyps,PT) -> true ; D=right,check_finite(B,Hyps,PT)). |
| 2680 | | check_finite(cartesian_product(A,B),Hyp,cart(PT)) :- |
| 2681 | | (check_finite(A,Hyp,PT) -> (check_equal_empty_set(A,Hyp,_PT2) -> true ; check_finite(B,Hyp,_PT2)) |
| 2682 | | ; check_equal_empty_set(B,Hyp,PT)). |
| 2683 | | check_finite(Rel,Hyp,rel(PTA,PTB)) :- is_relations_type(Rel,A,B),!, |
| 2684 | | (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)). % add other relations |
| 2685 | | check_finite(direct_product(A,B),Hyp,direct_product(PTA,PTB)) :- !, |
| 2686 | | (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)). |
| 2687 | | check_finite(parallel_product(A,B),Hyp,parallel_product(PTA,PTB)) :- !, |
| 2688 | | (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)). |
| 2689 | ? | check_finite(overwrite(A,B),Hyp,overwrite(PTA,PTB)) :- !, (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)). |
| 2690 | | check_finite(set_subtraction(A,_),Hyps,set_subtraction(PT)) :- !, check_finite(A,Hyps,PT). |
| 2691 | | check_finite(domain_restriction(A,BRel),Hyp,domain_restriction(PT)) :- !, |
| 2692 | ? | (check_finite(BRel,Hyp,PT) -> true |
| 2693 | | ; check_is_partial_function(BRel,Hyp), check_finite(A,Hyp,PT) |
| 2694 | | ; finite_range(BRel,Hyp,_) -> check_finite(A,Hyp,PT) % finite(a <| brel) if finite(a) & finite(ran(brel)) |
| 2695 | | ). |
| 2696 | ? | check_finite(domain_subtraction(_,B),Hyp,domain_subtraction(PT)) :- !, check_finite(B,Hyp,PT). |
| 2697 | | check_finite(range_restriction(ARel,B),Hyp,range_restriction(PT)) :- !, |
| 2698 | ? | (check_finite(ARel,Hyp,PT) -> true |
| 2699 | | ; check_is_injective(ARel,Hyp) -> check_finite(B,Hyp,PT) |
| 2700 | | ; finite_domain(ARel,Hyp,_) -> check_finite(B,Hyp,PT) % finite(arel |> b) if finite(b) & finite(dom(arel)) |
| 2701 | | ). |
| 2702 | | check_finite(range_subtraction(A,_),Hyp,range_subtraction(PT)) :- check_finite(A,Hyp,PT). |
| 2703 | | check_finite(interval(_,_),_,interval) :- !. |
| 2704 | | check_finite(value(V),_,empty_set_value) :- V==[], !. |
| 2705 | | check_finite(value(X),_,avl_set) :- nonvar(X),X=avl_set(_),!. |
| 2706 | | check_finite('$'(ID),Hyps,finite_type) :- |
| 2707 | | get_hyp_var_type(ID,Hyps,Type), %print(chk_fin(ID,Type)),nl, |
| 2708 | | (is_finite_type_for_wd(Type,Hyps) -> true |
| 2709 | | ; Type = set(couple(DomType,_)), % in principle an infinite relation type |
| 2710 | | is_finite_type_for_wd(DomType,Hyps), % we have something like set(couple(boolean,integer)) |
| 2711 | | % note: we treat this here in addition to the case is_partial_function below, as |
| 2712 | | % sometimes we loose the typing information in the term, e.g., in comprehension_set |
| 2713 | ? | avl_fetch_equal_from_hyps('$'(ID),Hyps,Func,_), |
| 2714 | ? | is_lambda_function(Func) % we have a function, it is finite if the domain is finite |
| 2715 | | ),!. |
| 2716 | | check_finite('$'(ID),Hyps,enumerated_set) :- |
| 2717 | | enumerated_set(ID), |
| 2718 | | \+ is_hyp_var(ID,Hyps),!. % global enumerated set visible |
| 2719 | | %check_finite('$'(ID),Hyp,partition) :- |
| 2720 | | % avl_fetch_binop_from_hyps('$'(ID),partition,Hyp,Values,Hyp2), % is now normalized |
| 2721 | | % not_occurs(Values,ID), |
| 2722 | | % l_check_finite(Values,Hyp2),!. |
| 2723 | | check_finite('$'(ID),Hyps,rewrite(Operator,PT)) :- |
| 2724 | | (Operator = equal ; Operator = subset), % for subset_strict we also have subset in Hyp |
| 2725 | ? | avl_fetch_binop_from_hyps('$'(ID),Operator,Hyps,Set2,Hyps2), |
| 2726 | | not_occurs(Set2,ID), % avoid silly, cyclic rewrites $x -> reverse(reverse($x)) (FunLawsStrings.mch) |
| 2727 | | % however, in SetLawsNatural this prevents proving 2 POs due to SS <: min(SS)..max(SS) |
| 2728 | | rewrite_local_loop_check(ID,check_finite,Set2,Hyps2,Hyps3), |
| 2729 | | check_finite(Set2,Hyps3,PT),!. |
| 2730 | | check_finite(Set,Hyp,finite_elements) :- id_or_record_field(Set), |
| 2731 | ? | avl_fetch_mem_or_struct(Set,Hyp,Set2,Hyp2), |
| 2732 | | Set2 \= Set, |
| 2733 | ? | has_finite_elements(Set2,Hyp2). |
| 2734 | | check_finite(Func,Hyp,pfun(PTA,PTB)) :- is_partial_function(Func,A,B),!, |
| 2735 | | % a set of partial functions from A to B is finite if both A and B are finite |
| 2736 | | (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)),!. |
| 2737 | ? | check_finite(Seq,Hyp,seq_type) :- infer_sequence_type_of_expr(Seq,Hyp,_),!. % a sequence is always finite |
| 2738 | | check_finite(struct(rec(Fields)),Hyp,struct) :- !, |
| 2739 | | maplist(check_finite_field(Hyp),Fields). |
| 2740 | | check_finite(general_union(SetOfSets),Hyp,general_union) :- !, |
| 2741 | ? | check_all_finite(SetOfSets,Hyp). |
| 2742 | | check_finite(general_intersection(SetOfSets),Hyp,general_intersection(PT)) :- !, |
| 2743 | | check_some_finite(SetOfSets,Hyp,PT). |
| 2744 | | check_finite(CompSet,Hyp,comprehension_set) :- is_comprehension_set(CompSet,Paras,Body), |
| 2745 | | finite_comprehension_set(Paras,Body,Hyp),!. |
| 2746 | | % TODO: is_lambda_function_with_domain; improve some proof trees above in style of intersection |
| 2747 | | %check_finite(F,Hyps,_) :- print(check_finite_failed(F)),nl,portray_hyps(Hyps),nl,fail. |
| 2748 | | |
| 2749 | | check_finite_field(Hyp,field(_,Set)) :- check_finite(Set,Hyp,_PT). |
| 2750 | | |
| 2751 | | % we could write a check_all meta_predicate |
| 2752 | | % check if we have a finite set of finite sets; used to determine if union(Sets) is finite |
| 2753 | | check_all_finite(empty_set,_). |
| 2754 | | check_all_finite(empty_sequence,_). |
| 2755 | | check_all_finite(value(avl_set(_AVL)),_Hyp) :- % currently avl_set can only contain finite values for normalisation |
| 2756 | | true. |
| 2757 | | check_all_finite(intersection(A,B),Hyps) :- |
| 2758 | | (check_all_finite(A,Hyps) -> true ; check_all_finite(B,Hyps)). |
| 2759 | | check_all_finite(union(A,B),Hyps) :- |
| 2760 | ? | (check_all_finite(A,Hyps) -> check_all_finite(B,Hyps)). |
| 2761 | | check_all_finite(sorted_set_extension(L),Hyps) :- !, check_all_finite(set_extension(L),Hyps). |
| 2762 | | check_all_finite(set_extension(L),Hyps) :- |
| 2763 | | (member(Val,L), \+ check_finite(Val,Hyps,_) -> fail % CHECK |
| 2764 | | ; true). |
| 2765 | | check_all_finite('$'(ID),Hyps) :- |
| 2766 | | (Operator = equal ; Operator = subset), % for subset_strict we also have subset in Hyp |
| 2767 | ? | avl_fetch_binop_from_hyps('$'(ID),Operator,Hyps,Set2,Hyps2), |
| 2768 | | not_occurs(Set2,ID), % avoid silly, cyclic rewrites |
| 2769 | | rewrite_local_loop_check(ID,check_finite,Set2,Hyps2,Hyps3), |
| 2770 | | check_all_finite(Set2,Hyps3),!. |
| 2771 | | check_all_finite(Op,Hyps) :- pow_subset_operator(Op,Set),!, |
| 2772 | | % if Set is finite then all subsets of it are finite and there are only finitely many |
| 2773 | | check_finite(Set,Hyps,_PT). |
| 2774 | | check_all_finite(Op,Hyps) :- iseq_operator(Op,Set),!, |
| 2775 | | % if Set is finite then all injective sequences of it are finite and there are only finitely many |
| 2776 | | check_finite(Set,Hyps,_PT). |
| 2777 | | |
| 2778 | | % check if some set of a set of sets is finite: |
| 2779 | | check_some_finite(sorted_set_extension(L),Hyps,PT) :- !, check_some_finite(set_extension(L),Hyps,PT). |
| 2780 | | check_some_finite(set_extension(L),Hyps,set_extension(PT)) :- |
| 2781 | | (member(Val,L), check_finite(Val,Hyps,PT) -> true). |
| 2782 | | check_some_finite('$'(ID),Hyps,rewrite_id(ID,PT)) :- |
| 2783 | | (Operator = equal ; Operator = superset), % Note: superset not subset as for check_all_finite |
| 2784 | | avl_fetch_binop_from_hyps('$'(ID),Operator,Hyps,Set2,Hyps2), |
| 2785 | | not_occurs(Set2,ID), % avoid silly, cyclic rewrites |
| 2786 | | rewrite_local_loop_check(ID,check_finite,Set2,Hyps2,Hyps3), |
| 2787 | | check_some_finite(Set2,Hyps3,PT),!. |
| 2788 | | %check_some_finite(intersection(A,B),Hyps) :- fail. % Note: the intersection could be empty! |
| 2789 | | check_some_finite(union(A,B),Hyps,union(PT)) :- |
| 2790 | | (check_some_finite(A,Hyps,PT) -> true ; check_some_finite(B,Hyps,PT)). |
| 2791 | | % for pow_subset_operator iseq_operator we would still need to check that the sets are not empty |
| 2792 | | % we cannot currently :prove x<:POW1(INT) & inter({NATURAL}\/x) : FIN(inter({NATURAL}\/x)) |
| 2793 | | |
| 2794 | | |
| 2795 | | pow_subset_operator(fin_subset(X),X). |
| 2796 | | pow_subset_operator(fin1_subset(X),X). |
| 2797 | | pow_subset_operator(pow_subset(X),X). |
| 2798 | | pow_subset_operator(pow1_subset(X),X). |
| 2799 | | iseq_operator(perm(Set),Set). |
| 2800 | | iseq_operator(iseq(Set),Set). |
| 2801 | | iseq_operator(iseq1(Set),Set). |
| 2802 | | |
| 2803 | | |
| 2804 | | is_comprehension_set(comprehension_set(Paras,Body),Paras,Body). |
| 2805 | | is_comprehension_set(value(V),Paras,Body) :- nonvar(V), |
| 2806 | | V=closure(P,_T,Body), % Note: norm_value normalises Body of closures |
| 2807 | | create_dollar_ids(P,Paras). |
| 2808 | | |
| 2809 | | create_dollar_ids([],[]). |
| 2810 | | create_dollar_ids([ID|T],['$'(ID)|TD]) :- create_dollar_ids(T,TD). |
| 2811 | | |
| 2812 | | % Note: lambdas already treated in is_partial_function check above |
| 2813 | | finite_comprehension_set(Paras,Body,Hyp) :- |
| 2814 | | % first exclude the parameters which can be proven finite on their own |
| 2815 | | % 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) |
| 2816 | | finite_comprehension_set_rest(Paras,Body,Hyp,[],Rest), |
| 2817 | | Rest \= Paras, |
| 2818 | | 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} |
| 2819 | | |
| 2820 | | finite_comprehension_set_rest([],_,_,_,[]). |
| 2821 | | % finite_comprehension_set(['$'(ID)|TID],Body,Hyp) :- finite_type ! |
| 2822 | | finite_comprehension_set_rest([ParaID1|TID],Body,Hyp,UnProven,Rest) :- |
| 2823 | ? | get_parameter_superset_in_body(ParaExpr,[ParaID1|TID],Body,Values), |
| 2824 | | l_not_occurs(Values,UnProven), % do not rely on not yet finitely proven paras; e.g. for {x,y|x:INTEGER & y=x} |
| 2825 | ? | match_parameter(ParaExpr,ParaID1), |
| 2826 | | check_finite(Values,Hyp,_PT),!, |
| 2827 | | finite_comprehension_set_rest(TID,Body,Hyp,UnProven,Rest). |
| 2828 | | finite_comprehension_set_rest([ParaID1|TID],Body,Hyp,UnProven,[ParaID1|Rest]) :- |
| 2829 | | finite_comprehension_set_rest(TID,Body,Hyp,[ParaID1|UnProven],Rest). |
| 2830 | | |
| 2831 | | % match_parameter(Expr,ID) -> ID occurs in Expr and finite number of values for Expr implies finite values for ID |
| 2832 | | match_parameter(ParaID,ParaID). |
| 2833 | | match_parameter(couple(ParaID,_),ParaID). % x|->y : Values finite implies finitely many values for x |
| 2834 | | match_parameter(couple(_,ParaID),ParaID). |
| 2835 | | match_parameter(set_extension(Ext),ParaID) :- |
| 2836 | ? | member(El,Ext), match_parameter(El,ParaID). % {x,..} : Values finite implies finitely many values for x |
| 2837 | | match_parameter(sorted_set_extension(Ext),ParaID) :- match_parameter(set_extension(Ext),ParaID). |
| 2838 | ? | match_parameter(sequence_extension(Ext),ParaID) :- member(ParaID,Ext). |
| 2839 | ? | match_parameter(rev(RF),ParaID) :- match_parameter(RF,ParaID). |
| 2840 | | match_parameter(reverse(RF),ParaID) :- match_parameter(RF,ParaID). |
| 2841 | | match_parameter(unary_minus(RF),ParaID) :- match_parameter(RF,ParaID). |
| 2842 | ? | match_parameter(concat(RF1,RF2),ParaID) :- (match_parameter(RF1,ParaID) -> true ; match_parameter(RF2,ParaID)). |
| 2843 | | match_parameter(union(RF1,RF2),ParaID) :- (match_parameter(RF1,ParaID) -> true ; match_parameter(RF2,ParaID)). |
| 2844 | ? | match_parameter(overwrite(_,RF),ParaID) :- match_parameter(RF,ParaID). % f <+ RF = (... <<| f ) \/ RF |
| 2845 | ? | match_parameter(Add,ParaID) :- add_with_number(Add,A,_Number), match_parameter(A,ParaID). |
| 2846 | ? | match_parameter(Mul,ParaID) :- mul_with_number(Mul,nohyps,A,Number), Number \= 0, match_parameter(A,ParaID). |
| 2847 | | % TO DO: more injective functions where a solution determines the ParaID, identity? direct_product, ... |
| 2848 | | % cartesian_product : only if other set not empty |
| 2849 | | |
| 2850 | | get_parameter_superset_in_body(ParaID,AllParas,Body,Values) :- |
| 2851 | ? | ( member_in_norm_conjunction(Body,member(ParaID,Values)) |
| 2852 | ? | ; member_in_norm_conjunction(Body,subset(ParaID,Values)) % there are only finitely many subsets of a finite set |
| 2853 | | ; member_in_norm_conjunction(Body,subset_strict(ParaID,Values)) |
| 2854 | ? | ; member_in_norm_conjunction(Body,equal(X,Y)), |
| 2855 | ? | sym_unify(X,Y,ParaID,Value), Values=set_extension([Value]) ), |
| 2856 | | l_not_occurs(Values,AllParas). % as an alternative: check for finite_type of set elements; e.g., detect ID=bool(...) |
| 2857 | | |
| 2858 | | |
| 2859 | | :- use_module(probsrc(bsyntaxtree),[is_set_type/2]). |
| 2860 | | %we suppose this has already failed: finite_domain(A,Hyp) :- check_finite(A,Hyp,PT). |
| 2861 | | finite_domain('$'(ID),Hyps,finite_type) :- |
| 2862 | | get_hyp_var_type(ID,Hyps,Type), |
| 2863 | | is_set_type(Type,couple(DomType,_)), |
| 2864 | | is_finite_type_for_wd(DomType,Hyps),!. |
| 2865 | | finite_domain(domain_restriction(A,Rel),Hyps,domain_restriction(PT)) :- !, |
| 2866 | | (check_finite(A,Hyps,PT) -> true ; finite_domain(Rel,Hyps,PT)). |
| 2867 | ? | finite_domain(A,Hyp,PT) :- get_domain_or_superset(A,Hyp,DA,Hyp2), check_finite(DA,Hyp2,PT). |
| 2868 | | |
| 2869 | | finite_range('$'(ID),Hyps,finite_type) :- |
| 2870 | | get_hyp_var_type(ID,Hyps,Type), |
| 2871 | | is_set_type(Type,couple(_,RanType)), |
| 2872 | | is_finite_type_for_wd(RanType,Hyps),!. |
| 2873 | ? | finite_range(A,Hyp,PT) :- get_range_or_superset(A,Hyp,RA,Hyp2),!, check_finite(RA,Hyp2,PT). |
| 2874 | | |
| 2875 | | l_check_finite([],_). |
| 2876 | | l_check_finite([H|T],Hyp) :- (check_finite(H,Hyp,_) -> l_check_finite(T,Hyp)). |
| 2877 | | |
| 2878 | | % is a set containing only finite sets |
| 2879 | | has_finite_elements(fin_subset(_),_) :- !. |
| 2880 | | has_finite_elements(fin1_subset(_),_) :- !. |
| 2881 | | has_finite_elements(pow_subset(X),Hyps) :- !, check_finite(X,Hyps,_). |
| 2882 | | has_finite_elements(pow1_subset(X),Hyps) :- !, check_finite(X,Hyps,_). |
| 2883 | | has_finite_elements(seq(_),_) :- !. % every sequence is always finite (of finite length) |
| 2884 | | has_finite_elements(seq1(_),_) :- !. |
| 2885 | | has_finite_elements(iseq(_),_) :- !. |
| 2886 | | has_finite_elements(iseq1(_),_) :- !. |
| 2887 | | has_finite_elements(perm(_),_) :- !. |
| 2888 | | has_finite_elements(union(A,B),Hyps) :- !, has_finite_elements(A,Hyps), has_finite_elements(B,Hyps). |
| 2889 | | has_finite_elements(intersection(A,B),Hyps) :- !, (has_finite_elements(A,Hyps) -> true ; has_finite_elements(B,Hyps)). |
| 2890 | | has_finite_elements(set_subtraction(A,_),Hyps) :- !, has_finite_elements(A,Hyps). |
| 2891 | | has_finite_elements(sorted_set_extension(L),Hyps) :- !, l_check_finite(L,Hyps). |
| 2892 | | has_finite_elements(set_extension(L),Hyps) :- !, l_check_finite(L,Hyps). |
| 2893 | | has_finite_elements(S,_) :- is_empty_set_direct(S),!. % has no elements |
| 2894 | | has_finite_elements(Func,Hyps) :- is_partial_function(Func,A,B),!, |
| 2895 | ? | (check_finite(A,Hyps,_) -> true ; is_injective(Func), check_finite(B,Hyps,_)). |
| 2896 | ? | has_finite_elements(Rel,Hyps) :- is_relations_type(Rel,A,B),!,check_finite(A,Hyps,_),check_finite(B,Hyps,_). |
| 2897 | | %has_finite_elements(F,Hs) :- print(has_finite_elements_failed(F)),nl, portray_hyps(Hs),fail. |
| 2898 | | |
| 2899 | | |
| 2900 | | is_relations_type(relations(A,B),A,B). |
| 2901 | | is_relations_type(surjection_relation(A,B),A,B). |
| 2902 | | is_relations_type(total_relation(A,B),A,B). |
| 2903 | | is_relations_type(total_surjection_relation(A,B),A,B). |
| 2904 | | |
| 2905 | | % TO DO: more rules for functions |
| 2906 | | % ------------------------------ |
| 2907 | | |
| 2908 | | :- use_module(probsrc(avl_tools),[avl_fetch_bin/4]). |
| 2909 | | |
| 2910 | | % fetch member(Ground,Free) construct |
| 2911 | | %avl_fetch_mem(Key, AVL ,Res) :- avl_fetch_bin(Key, member, AVL ,Res). |
| 2912 | | %avl_fetch_equal(Key, AVL ,Res) :- avl_fetch_bin(Key, equal, AVL ,Res). |
| 2913 | | |
| 2914 | | |
| 2915 | | avl_fetch_mem_from_hyps(ID,Hyps,Value,Hyps2) :- |
| 2916 | ? | avl_fetch_binop_from_hyps(ID,member,Hyps,Value,Hyps2). |
| 2917 | | |
| 2918 | | avl_fetch_worthwhile_mem_from_hyps(ID,Hyps,Value,Hyps2) :- |
| 2919 | ? | avl_fetch_binop_from_hyps(ID,member,Hyps,Value,Hyps2), |
| 2920 | | \+ maximal_set(Value,Hyps2). |
| 2921 | | |
| 2922 | | avl_fetch_equal_from_hyps(ID,Hyps,Value,Hyps2) :- |
| 2923 | ? | avl_fetch_binop_from_hyps(ID,equal,Hyps,Value,Hyps2). |
| 2924 | | |
| 2925 | | avl_fetch_worthwhile_equal_from_hyps(ID,Hyps,Value,Hyps2) :- |
| 2926 | | worth_rewriting_with_equal(ID), |
| 2927 | ? | avl_fetch_binop_from_hyps(ID,equal,Hyps,Value,Hyps2), |
| 2928 | | quick_not_occurs_check(ID,Value). |
| 2929 | | |
| 2930 | | avl_fetch_worthwhile_member_from_hyps(ID,Hyps,Value,Hyps2) :- |
| 2931 | | worth_rewriting_with_equal(ID), |
| 2932 | ? | avl_fetch_binop_from_hyps(ID,member,Hyps,Value,Hyps2). |
| 2933 | | |
| 2934 | | % fetch member predicate or indirect member via record fields |
| 2935 | | avl_fetch_mem_or_struct(Func,Hyps,Function,Hyps1) :- |
| 2936 | ? | get_type_from_hyps(Func,Hyps,Function,Hyps1). |
| 2937 | | avl_fetch_mem_or_struct(record_field(Rec,Field),Hyps,FieldType,Hyps2) :- |
| 2938 | ? | get_record_type_fields(Rec,Fields,Hyps,Hyps2), |
| 2939 | ? | (member(field(Field,FieldType),Fields) -> true). |
| 2940 | | |
| 2941 | | % find record type and extract fields for a given expression |
| 2942 | | get_record_type_fields(function(Func,_),Fields,Hyps,Hyps2) :- |
| 2943 | ? | get_range_or_superset(Func,Hyps,Range,Hyps1), |
| 2944 | ? | check_equal_pattern(Range,struct(rec(Fields)),Hyps1,Hyps2). |
| 2945 | | get_record_type_fields(Rec,Fields,Hyps,Hyps2) :- |
| 2946 | ? | get_type_from_hyps(Rec,Hyps,RecType,Hyps1), |
| 2947 | ? | check_equal_pattern(RecType,struct(rec(Fields)),Hyps1,Hyps2). |
| 2948 | | |
| 2949 | | % get type from hyps x:XType or x:ran(F) with F : A->B |
| 2950 | | get_type_from_hyps(X,Hyps,XType,Hyps2) :- |
| 2951 | ? | avl_fetch_mem_from_hyps(X,Hyps,XSet,Hyps1), |
| 2952 | ? | get_type2(XSet,Hyps1,XType,Hyps2). |
| 2953 | | get_type_from_hyps(function(Func2,_),Hyps,Range,Hyps2) :- |
| 2954 | | % f : _ +-> ( _ >-> _ ) => f(_) : _ >-> _ |
| 2955 | ? | get_range_or_superset(Func2,Hyps,Range,Hyps2). |
| 2956 | | get_type_from_hyps(second_of_pair(X),Hyps,Type,Hyps2) :- %prj2 |
| 2957 | ? | get_type_from_hyps(X,Hyps,XType,Hyps1), |
| 2958 | | check_equal_pattern(XType,cartesian_product(_,Type),Hyps1,Hyps2). |
| 2959 | | get_type_from_hyps(first_of_pair(X),Hyps,Type,Hyps2) :- %prj1 |
| 2960 | ? | get_type_from_hyps(X,Hyps,XType,Hyps1), |
| 2961 | | check_equal_pattern(XType,cartesian_product(Type,_),Hyps1,Hyps2). |
| 2962 | | get_type_from_hyps(assertion_expression(_,_,X),Hyps,XType,Hyps1) :- |
| 2963 | ? | get_type_from_hyps(X,Hyps,XType,Hyps1). |
| 2964 | | |
| 2965 | | get_type2(domain(Func),Hyps,XType,Hyps2) :- !, |
| 2966 | ? | get_domain_or_superset(Func,Hyps,XType,Hyps2). |
| 2967 | | get_type2(range(Func),Hyps,XType,Hyps2) :- !, |
| 2968 | ? | get_range_or_superset(Func,Hyps,XType,Hyps2). |
| 2969 | | get_type2(Type,Hyps,Type,Hyps). |
| 2970 | | |
| 2971 | | id_or_record_field('$'(_)). |
| 2972 | | id_or_record_field(record_field(_,_)). |
| 2973 | | |
| 2974 | | % perform occurs check if first arg is an identifier: |
| 2975 | | quick_not_occurs_check('$'(ID),Value) :- !, not_occurs(Value,ID). |
| 2976 | | quick_not_occurs_check(_,_). |
| 2977 | | |
| 2978 | | % worth rewriting with equality hyps |
| 2979 | | worth_rewriting_with_equal('$'(_)). |
| 2980 | | worth_rewriting_with_equal(record_field('$'(_),_)). |
| 2981 | | worth_rewriting_with_equal(couple(_,_)). |
| 2982 | | worth_rewriting_with_equal(size(_)). |
| 2983 | | worth_rewriting_with_equal(card(_)). |
| 2984 | | worth_rewriting_with_equal(function(_,_)). |
| 2985 | | |
| 2986 | | % utility to fetch fully ground term from hyp avl |
| 2987 | | avl_fetch_from_hyps(Term,hyp_rec(AVL,_)) :- avl_fetch(Term,AVL). |
| 2988 | | |
| 2989 | | % a version without loop check; can be used if processing is finished afterwards |
| 2990 | | avl_fetch_binop_from_hyps_no_loop_check(ID,BinOp,hyp_rec(AVL,_),Value) :- |
| 2991 | ? | avl_fetch_bin(ID,BinOp,AVL,Value). |
| 2992 | | |
| 2993 | | % lookup a hypothesis ID BinOp Value in logarithmic time; ID and BinOp must be known |
| 2994 | | avl_fetch_binop_from_hyps(ID,BinOp,hyp_rec(AVL,HInfos),Value,hyp_rec(AVL,HInfos2)) :- |
| 2995 | ? | avl_fetch_bin(ID,BinOp,AVL,Value), |
| 2996 | | (avl_fetch(prevent_cycle_count,HInfos,CycleCount) % avoid cycles x=y, y=x |
| 2997 | | -> (CycleCount < 5 -> true ; % print(prevented_cycle(ID,CycleCount)),nl, |
| 2998 | | % in test 2018: :wd target = [2,1,1,2,1] & n=size(target) & i:1..n & target(i)=res requires cycle count < 5 |
| 2999 | | !, fail), |
| 3000 | | C1 is CycleCount+1 |
| 3001 | | ; C1 is 1 |
| 3002 | | ), |
| 3003 | | avl_store(prevent_cycle_count,HInfos,C1,HInfos2). |
| 3004 | | % detect local loops; should not be used where Hyps are passed to unrelated goals or one has to reset_local_loop_check |
| 3005 | | rewrite_local_loop_check(_,_,Value,HI,HI1) :- useful_value(Value),!,HI1=HI. |
| 3006 | | rewrite_local_loop_check(Term,ProverPredicate,_,Hyps,_) :- var(Hyps),!, |
| 3007 | | add_internal_error('Var hyps: ',rewrite_local_loop_check(Term,ProverPredicate,_,Hyps,_)),fail. |
| 3008 | | rewrite_local_loop_check(Term,ProverPredicate,_,hyp_rec(AVL,HInfos),hyp_rec(AVL,HInfos1)) :- !, |
| 3009 | | (Term='$'(ID) -> true ; ID=Term), |
| 3010 | | %(avl_fetch(rewritten(Term,ProverPredicate),HInfos) -> print(loop(Term,ProverPredicate)),nl,fail ; true), |
| 3011 | | \+ avl_fetch(rewritten(ID,ProverPredicate),HInfos), |
| 3012 | | avl_store(rewritten(ID,ProverPredicate),HInfos,true,HInfos1). |
| 3013 | | % :wd a : 1 .. sz --> INTEGER & sz=5 & p : perm(dom(a)) & i : 1 .. sz - 1 & res= p(i) % sz rewritten multiple times |
| 3014 | | % :wd f: BOOL --> 1..10 & g : 0..20 --> BOOL & bb:BOOL & (f;g)(bb)=res |
| 3015 | | |
| 3016 | | %reset_local_loop_check() |
| 3017 | | |
| 3018 | | % values where there is no risk of looping when rewriting to: |
| 3019 | | useful_value(Value) :- number(Value). |
| 3020 | | useful_value(interval(A,B)) :- number(A), number(B). |
| 3021 | | useful_value(value(_)). |
| 3022 | | |
| 3023 | | |
| 3024 | | % rename and prove a list of goals |
| 3025 | | l_rename_and_prove_goals([],_,_,[]). |
| 3026 | | l_rename_and_prove_goals([H|T],Subst,Hyps,[PTH|PTT]) :- |
| 3027 | | rename_norm_term(H,Subst,RH),!, |
| 3028 | ? | prove_po(RH,Hyps,PTH),!, % TO DO: use version of prove_po that does not print info |
| 3029 | | l_rename_and_prove_goals(T,Subst,Hyps,PTT). |
| 3030 | | |
| 3031 | | |
| 3032 | | % small utility for sanity checking |
| 3033 | | check_integer(A,PP) :- not_integer(A),!, add_error(PP,'Not an integer: ',A),fail. |
| 3034 | | check_integer(_,_). |
| 3035 | | not_integer(empty_set). |
| 3036 | | not_integer(empty_sequence). |
| 3037 | | not_integer(interval(_,_)). |
| 3038 | | not_integer(couple(_,_)). |
| 3039 | | not_integer(union(_,_)). |
| 3040 | | not_integer(intersection(_,_)). |
| 3041 | | not_integer(domain(_)). |
| 3042 | | not_integer(range(_)). |
| 3043 | | % TO DO: extend |
| 3044 | | |
| 3045 | | |
| 3046 | | % ---------------- |
| 3047 | | |
| 3048 | | % small REPL to inspect hyps |
| 3049 | | :- public hyp_repl/1. |
| 3050 | | hyp_repl(Hyps) :- hyp_repl_prompt(Hyps),read(Term), !, hyp_repl(Term,Hyps). |
| 3051 | | hyp_repl(_). |
| 3052 | | |
| 3053 | | hyp_repl(end_of_file,_). |
| 3054 | | hyp_repl(quit,_). |
| 3055 | | hyp_repl(exit,_). |
| 3056 | | hyp_repl(help,Hyps) :- write('Use quit to exit, print to portray_hyps, or type an identifier to lookup in hyps'),nl, |
| 3057 | | hyp_repl(Hyps). |
| 3058 | | hyp_repl(print,Hyps) :- portray_hyps(Hyps), hyp_repl(Hyps). |
| 3059 | | hyp_repl(ID,Hyps) :- avl_fetch_equal_from_hyps($(ID),Hyps,Value,_), |
| 3060 | | format('Value for ~w:~n ~w~n',[ID,Value]), |
| 3061 | | hyp_repl(Hyps). |
| 3062 | | |
| 3063 | | hyp_repl_prompt(hyp_rec(AVL,HInfos)) :- |
| 3064 | | avl_size(AVL,Size), |
| 3065 | | avl_size(HInfos,ISize),!, |
| 3066 | | format('hyp_rec(#~w,#~w) >>>',[Size,ISize]). |
| 3067 | | hyp_repl_prompt(_) :- write('ILLEGAL HYP_REC >>>'). |