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