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