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