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_hyps, [empty_hyps/1,
6 portray_hyps/1,
7 get_hyp_vars/2,
8 get_hyp_var_type/3,
9 push_hyp/4, push_hyps/4,
10 push_hyps_wo_renaming/4,
11 %push_normalized_hyp/3,
12 add_new_hyp_variables/3,
13 add_new_hyp_any_vars/3,
14 copy_hyp_variables/3,
15 is_hyp_var/2,
16 get_clash_renaming_subst/2,
17 get_renamed_expression/3,
18 get_normalized_and_renamed_predicate/4,
19 negate_hyp/2,
20 negate_op/2,
21 is_finite_type_for_wd/2
22 ]).
23
24 :- use_module(probsrc(module_information),[module_info/2]).
25 :- module_info(group,well_def_prover).
26 :- module_info(description,'This module provides hypotheses stack management.').
27
28
29
30 :- use_module(wdsrc(well_def_tools), [not_occurs/2]).
31 :- use_module(probsrc(error_manager)).
32 :- use_module(probsrc(debug)).
33 :- use_module(library(avl)).
34 :- use_module(library(ordsets)).
35
36 % ------------------------------
37
38 % Hypotheses stack management:
39
40
41 % create an empty hyp stack
42 empty_hyps(hyp_rec(E,HI2)) :- empty_avl(E),
43 avl_store(hyp_typed_vars,E,[],HI1), % typed variables of the hypotheses (implicitly universally quantified)
44 avl_store(hyp_clash_vars,HI1,clash_rec(0,E),HI2). % variables which are currently in clash
45
46 :- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2]).
47 % display the hypotheses stack:
48 portray_hyps(hyp_rec(AVL,HInfos)) :- fetch_hyp_vars(HInfos,Vars),
49 get_clashed_vars(HInfos,CVars),
50 (debug_mode(on) -> portray_hyp_vars(hyp_rec(AVL,HInfos)),nl ; true),
51 %b_global_sets:portray_global_sets,
52 !,
53 format('Hypotheses over ~w (clashes: ~w):~n',[Vars,CVars]),
54 %avl_domain(AVL,D), lists:maplist(well_def_hyps:println_nhyp,D),
55 avl_range(AVL,Hyp),
56 conjunct_predicates(Hyp,HypC),
57 translate:nested_print_bexpr(HypC),nl,nl.
58 portray_hyps(H) :- !, format('** ILLEGAL Hypotheses: ~w~n',[H]).
59
60 print_tvar(b(identifier(ID),Type,_)) :- format(' ~w : ~w~n',[ID,Type]).
61 :- use_module(library(lists),[maplist/2]).
62 portray_hyp_vars(hyp_rec(_,HInfos)) :- fetch_hyp_typed_vars(HInfos,TVars),!,
63 length(TVars,Len),
64 format('Typed vars in hyps (~w):~n',[Len]),
65 maplist(print_tvar,TVars).
66 portray_hyp_vars(H) :- !, format('** ILLEGAL Hypotheses: ~w~n',[H]).
67
68
69 %println_nhyp(NH) :- format(' --> ~w~n',[NH]).
70
71
72 % ---------------------
73
74 % for debugging:
75 :- public hyp_portray_hook/1.
76 hyp_portray_hook(X) :- nonvar(X), X= hyp_rec(AVL,HInfos),
77 avl_size(AVL,Size),
78 avl_size(HInfos,ISize),
79 format('hyp_rec(#~w,#~w)',[Size,ISize]).
80
81 :- public install_hyp_portray_hook/0.
82 install_hyp_portray_hook :- % mainly for the Prolog debugger
83 assertz(( user:portray(X) :- well_def_hyps:hyp_portray_hook(X) )).
84
85 %:- install_hyp_portray_hook.
86
87
88 % ------------------------
89
90 % get the variable ids currently in scope
91 get_hyp_vars(hyp_rec(_,HInfos),Res) :- get_hyp_vars(HInfos,Vars),!,Res=Vars.
92 get_hyp_vars(H,R) :- add_internal_error('Illegal hyps: ',get_hyp_vars(H,R)), R=[].
93
94 :- use_module(probsrc(bsyntaxtree), [def_get_texpr_ids/2]).
95 fetch_hyp_vars(HInfos,Vars) :- avl_fetch(hyp_typed_vars,HInfos,TVars),
96 def_get_texpr_ids(TVars,Vars).
97 fetch_hyp_typed_vars(HInfos,Vars) :-
98 avl_fetch(hyp_typed_vars,HInfos,Vars).
99 get_clashed_vars(HInfos,Vars) :- avl_fetch(hyp_clash_vars,HInfos,clash_rec(_,AVL)),
100 avl_domain(AVL,Vars).
101 get_clash_renaming(HInfos,Renamings) :- avl_fetch(hyp_clash_vars,HInfos,clash_rec(_,AVL)),
102 findall(rename(ID,FreshID), avl_member(ID,AVL,FreshID), Renamings).
103
104 % check if a variable id is currently in the scope of the hypotheses
105 % if not, it is a global identifier (e.g., enumerated or deferred set)
106 is_hyp_var(Var,hyp_rec(_,HInfos)) :- atomic(Var), nonvar(HInfos),!,
107 fetch_hyp_vars(HInfos,Vars),
108 ord_member(Var,Vars).
109 is_hyp_var(V,H) :- add_internal_error('Illegal call: ',is_hyp_var(V,H)),fail.
110
111 :- use_module(probsrc(tools_lists),[ord_member_nonvar_chk/2]).
112 get_hyp_var_type(Var,hyp_rec(_,HInfos),Type) :- atomic(Var),!,
113 fetch_hyp_typed_vars(HInfos,TVars),
114 TVar = b(identifier(Var),Type,_),
115 ord_member_nonvar_chk(TVar,TVars).
116 get_hyp_var_type(V,H,T) :- add_internal_error('Illegal call: ',is_hyp_var_type(V,H,T)),fail.
117
118 :- use_module(probsrc(bsyntaxtree), [conjunction_to_list/2]).
119 % push a new Hypothesis H on the hyp stack
120 push_hyp(Hyps,H,Options,NewHyps) :-
121 check_hyp_rec(Hyps,push_hyp),
122 conjunction_to_list(H,Hs),
123 push_hyps(Hyps,Hs,Options,NewHyps).
124
125 check_hyp_rec(Hyps,PP) :- var(Hyps),!, add_internal_error('Illegal variable hyp_rec: ',check_hyp_rec(Hyps,PP)),fail.
126 check_hyp_rec(Hyps,PP) :- Hyps \= hyp_rec(_,_),!, add_internal_error('Illegal hyp_rec: ',check_hyp_rec(Hyps,PP)),fail.
127 check_hyp_rec(_,_).
128
129 % push a list of hypotheses
130 push_hyps(hyp_rec(NHyps,HInfos),Hs,Options,hyp_rec(NewNHyps,HInfos)) :- !,
131 get_clash_renaming(HInfos,ClashRenaming),
132 push_hyp_aux(Hs,ClashRenaming,Options,NHyps,NewNHyps).
133 push_hyps(A,B,C,D) :- add_internal_error('Illegal call: ', push_hyps(A,B,C,D)),fail.
134
135 % useful if renaming done outside, e.g., for treating x:=x-1 in WD analyser
136 push_hyps_wo_renaming(hyp_rec(NHyps,HInfos),Hs,Options,hyp_rec(NewNHyps,HInfos)) :- !, ClashRenaming=[],
137 push_hyp_aux(Hs,ClashRenaming,Options,NHyps,NewNHyps).
138 push_hyps_wo_renaming(A,B,C,D) :- add_internal_error('Illegal call: ', push_hyps(A,B,C,D)),fail.
139
140 push_hyp_aux(Hyps,_,_,_,_) :- var(Hyps),!, add_internal_error('Unbound hyps: ',push_hyps(Hyps)),fail.
141 push_hyp_aux([],_,_,NH,NH).
142 push_hyp_aux([H|T],ClashRenaming,Options,NHyps,NewNHyps) :-
143 ((var(NHyps) ; NHyps=hyp_rec(_,_)) -> add_internal_error('Illegal AVL: ',NHyps),fail ; true),
144 push_individual_hyp(H,ClashRenaming,Options,NHyps,NHyps3),
145 push_hyp_aux(T,ClashRenaming,Options,NHyps3,NewNHyps).
146
147 % sometimes we still have conjuncts in the list of hypotheses (e.g., coming from Rodin)
148 push_individual_hyp(b(conjunct(H1,H2),_,_),ClashRenaming,Options,NHyps,NHyps3) :- !,
149 push_individual_hyp(H1,ClashRenaming,Options,NHyps,NHyps2),
150 push_individual_hyp(H2,ClashRenaming,Options,NHyps2,NHyps3).
151 push_individual_hyp(H,ClashRenaming,Options,NHyps,NHyps3) :-
152 normalize_and_rename_predicate(ClashRenaming,H,RenH,NH),
153 % print('PUSH: '),nl, debug:print_quoted_with_max_depth(NH,6), print(' '), error_manager:print_message_span(H),nl,
154 push_normalized_hyp_aux(NH,RenH,Options,NHyps,NHyps3).
155
156 % utility: used to push already normalized and renamed hyp from within prover for normalized sub-goals
157 %push_normalized_hyp(NH,hyp_rec(NHyps,I),hyp_rec(NHyps3,I)) :- norm_aux(NH,NormPred),
158 % push_normalized_hyp_aux(NormPred,unknown,[],NHyps,NHyps3).
159
160 push_normalized_hyp_aux(NH,RenH,Options,NHyps,NHyps3) :-
161 ((useful_hyp(NH) ; safe_ord_member(create_full_po,Options)
162 ; potentially_useful_for_hyp_rule(NH), safe_ord_member(push_more_hyps,Options)
163 )
164 -> avl_store(NH,NHyps,RenH,NHyps2)
165 ; NHyps2=NHyps % hypothesis not used by prover
166 %,functor(NH,FF,NN), print(not_pushing(FF,NN)),nl
167 ),
168 ( commute_bin_op(NH,_) % somehow faster than using findall directly
169 -> findall(NH3,commute_bin_op(NH,NH3),NH3s),
170 %length(NH3s,Len),hit_profiler:add_profile_hit(hyp(NH,Len)),
171 l_avl_store_nhyps(NH3s,NHyps2,RenH,NHyps3)
172 ; NHyps3=NHyps2
173 ).
174
175 safe_ord_member(El,List) :- var(List),!, add_internal_error('Illegal call: ',safe_ord_member(El,List)),fail.
176 safe_ord_member(El,List) :- ord_member(El,List).
177
178 l_avl_store_nhyps([],NHyps,_,NHyps).
179 l_avl_store_nhyps([NH1|TNH],NHyps1,RenH,NHyps3) :-
180 avl_store_if_new(NH1,NHyps1,RenH,NHyps2),
181 l_avl_store_nhyps(TNH,NHyps2,RenH,NHyps3).
182
183 avl_store_if_new(NH,H,_,H2) :- avl_fetch(NH,H),!, H2=H.
184 avl_store_if_new(NH,H,RH,H2) :- avl_store(NH,H,RH,H2).
185
186 :- use_module(probsrc(bsyntaxtree), [rename_bt/3]).
187 normalize_and_rename_predicate(_,H,_,_) :- var(H),!,
188 add_internal_error('Unbound predicate: ',normalize_and_rename_predicate(H)),fail.
189 normalize_and_rename_predicate([],H,RenH,NH) :- !, RenH=H,
190 normalize_predicate(H,NH).
191 normalize_and_rename_predicate(ClashRenaming,H,RenH,NH) :- !,
192 %format('Rename Hyp: ~w ',[ClashRenaming]),translate:print_bexpr(H),nl,
193 rename_bt(H,ClashRenaming,RenH),
194 %print(' > renamed Hyp: '),translate:print_bexpr(RenH),nl,
195 normalize_predicate(RenH,NH).
196
197 normalize_predicate(Pred,NormPred) :-
198 b_interpreter_check:norm_pred_check(Pred,NP),
199 norm_aux(NP,NormPred).
200
201 % put identifiers first, so that we can more efficiently do lookups;
202 % hence we try and replace less/greater by less_equal/greater_equal when possible
203 norm_aux(equal(Val,'$'(ID)),Res) :- Val \= '$'(_), !, Res=equal('$'(ID),Val).
204 norm_aux(greater(Val,Nr),greater_equal(Val,N1)) :- integer(Nr),!, N1 is Nr+1.
205 norm_aux(greater(Nr,Val),greater_equal(N1,Val)) :- integer(Nr),!, N1 is Nr-1.
206 norm_aux(greater(A,B),less(B,A)) :- !. % we only look up less (when both args are known)
207 norm_aux(less(Val,Nr),less_equal(Val,N1)) :- integer(Nr),!, N1 is Nr-1.
208 norm_aux(less(Nr,Val),less_equal(N1,Val)) :- integer(Nr),!, N1 is Nr+1.
209 norm_aux(not_equal(Val,EMPTY),not_equal(Val,empty_set)) :- is_empty_set_alternative(EMPTY),!.
210 norm_aux(not_equal(EMPTY,Val),not_equal(Val,empty_set)) :- is_empty_set_alternative(EMPTY),!.
211 norm_aux(negation(Pred),NormPred) :- negate_op(Pred,NP),!, norm_aux(NP,NormPred).
212 %norm_aux(Term,NormPred) :- print(Term),nl,functor(Term,union,2),flatten(Term,union,List,[]), print(union(List)),nl,
213 % sort(List,SL),print(sorted(SL)),nl,fail.
214 norm_aux(V,V).
215 % TO DO: subset_strict -> subset and not_equal
216 % TO DO: normalize value(X) terms -> value(int(Nr)) -> Nr, ...
217 % TO DO: maybe process a few rules here x<: dom(f) or x = dom(f) - other
218
219 % TO DO: flatten and sort union and possibly other operators:
220 %flatten(Term,BOP) --> {functor(Term,BOP,2), arg(1,Term,B1), arg(2,Term,B2)},!,
221 % flatten(B1,BOP), flatten(B2,BOP).
222 %flatten(Term,_) --> [Term].
223
224 is_empty_set_alternative(empty_sequence).
225 is_empty_set_alternative(value(V)) :- V==[]. % should now be handled in norm_expr / norm_value
226
227 negate_op(truth,falsity).
228 negate_op(falsity,truth).
229 negate_op(equal(A,B),not_equal(A,B)).
230 negate_op(not_equal(A,B),equal(A,B)).
231 negate_op(less(A,B),less_equal(B,A)).
232 negate_op(greater(A,B),less_equal(A,B)).
233 negate_op(less_equal(A,B),less(B,A)).
234 negate_op(greater_equal(A,B),less(A,B)).
235 negate_op(less_real(A,B),less_equal_real(B,A)).
236 negate_op(less_equal_real(A,B),less_real(B,A)).
237 negate_op(negation(P),P).
238 negate_op(not_member(A,B),member(A,B)).
239 negate_op(member(A,B),not_member(A,B)). % should we do this?
240 negate_op(not_subset(A,B),subset(A,B)).
241 negate_op(subset(A,B),not_subset(A,B)).
242 negate_op(not_subset_strict(A,B),subset_strict(A,B)).
243 negate_op(subset_strict(A,B),not_subset_strict(A,B)).
244 % should we negate_op(conjunct ...), we also treat negation in prove_po/prove_negated_po
245
246 % for commutative binary operators: also store commutative version to enable lookup on either argument
247 commute_bin_op(equal(A,B),Pred) :- compute_bin_op_equal(A,B,Pred).
248 % not_equal: no need to reverse: we always know both values when doing a lookup
249 commute_bin_op(greater_equal(A,B),less_equal(B,A)) :- can_be_used_for_lookups(B).
250 commute_bin_op(greater(A,B),Pred) :- compute_bin_op_less(B,A,Pred).
251 commute_bin_op(less_equal(A,B),Pred) :- compute_bin_op_less_equal(A,B,Pred).
252 commute_bin_op(less(A,B),Pred) :- compute_bin_op_less(A,B,Pred).
253 commute_bin_op(less_real(A,B),not_equal(A,B)). % TO DO: extend
254 commute_bin_op(subset_strict(A,B),Pred) :- gen_subset(A,B,Pred).
255 commute_bin_op(subset(A,B),superset(B,A)) :- % new operator, for efficient lookups !
256 can_be_used_for_lookups(B).
257 commute_bin_op(not_subset(A,B),not_equal(A,B)).
258 commute_bin_op(member(_,Set),not_equal(Set,empty_set)).
259 commute_bin_op(member(couple(A,B),C),NewHyp) :-
260 ( NewHyp = member(A,domain(C)) % A|->B : C ==> A : dom(C)
261 ; NewHyp = member(B,range(C)) ). % A|->B : C ==> B : ran(C)
262 commute_bin_op(member(X,interval(Low,Up)),NewHyp) :-
263 (NewHyp = less_equal(Low,Up) % x : Low..Up => Low <= Up
264 ; NewHyp = less_equal(Low,X) % Low <= X if X: Low..UP
265 ; can_be_used_for_lookups(X), NewHyp = greater_equal(X,Low)
266 ; NewHyp = less_equal(X,Up) % X <= UP if X: Low..UP
267 ; can_be_used_for_lookups(Up), NewHyp = greater_equal(Up,X)
268 ).
269 commute_bin_op(member(X,Rel),NewHyp) :- is_total_relation(Rel,Domain),
270 % we cannot efficiently lookup this info from Domain
271 can_be_used_for_lookups(Domain),
272 NewHyp = equal(Domain,domain(X)).
273 commute_bin_op(member(X,Rel),NewHyp) :- is_surjective_relation(Rel,Range),
274 % we cannot efficiently lookup this info from Range
275 can_be_used_for_lookups(Range),
276 NewHyp = equal(Range,range(X)).
277 commute_bin_op(member(card(X),_),NewHyp) :- can_be_used_for_lookups(X),
278 NewHyp=finite(X).
279 commute_bin_op(disjunct(LHS,RHS),NewHyp) :- get_member_pred(LHS,X,A), get_member_pred(RHS,X,B),
280 NewHyp = member(X,union(A,B)).
281 commute_bin_op(disjunct(LHS,RHS),NewHyp) :- get_subset_pred(LHS,X,A), get_subset_pred(RHS,X,B),
282 NewHyp = subset(X,union(A,B)).
283 commute_bin_op(partition(A,List),equal(A,UNION)) :- gen_union(List,UNION).
284 % TO DO: is there a use in the all_disjoint feature?
285 commute_bin_op(forall(['$'(X)],LHSPred,RHSPred), Pred) :-
286 get_member_lhs(LHSPred,'$'(X),Set),
287 get_member_rhs(RHSPred,'$'(X),SET2),
288 useful_forall_superset(SET2),
289 % !x.(x:SET => x:dom(F)) => SET <: dom(F)
290 % !x.(x:SET => x:SET2) => SET <: SET2
291 not_occurs(Set,X),
292 not_occurs(SET2,X), %print(subset1(Set,SET2)),nl,
293 gen_subset(Set,SET2,Pred).
294 commute_bin_op(forall(['$'(X),'$'(Y)],LHSPred,RHSPred), Pred) :- % TO DO: generalise
295 get_member_lhs(LHSPred,couple('$'(X),'$'(Y)),Set), %TO DO: generalise -> domain/range
296 get_member_rhs(RHSPred,'$'(X),SET2),
297 useful_forall_superset(SET2),
298 % !x,y.(x|->y:SET => x:dom(F)) => dom(SET) <: dom(F)
299 % !x,y.(x|->y:SET => x:SET2) => dom(SET) <: SET2
300 not_occurs(Set,X),
301 not_occurs(Set,Y),
302 not_occurs(SET2,X), %print(subset2(Set,SET2)),nl,
303 gen_subset(domain(Set),SET2,Pred).
304 commute_bin_op(not_equal(A,B),equal(A,NB)) :- negate_boolean_like_value(B,NB).
305 commute_bin_op(not_equal(intersection(Set1,Set2),empty_set), Pred) :-
306 % Set /\ {a} /= {} => a : Set
307 (Set1=set_extension([A]),B=Set2 -> true ; Set2=set_extension([A]),B=Set1),
308 Pred = member(A,B).
309 %commute_bin_op(X,_) :- print(binop(X)),nl,fail.
310
311 % extract a membership predicate
312 get_member_pred(member(X,A),X,A).
313 get_member_pred(equal(X,A),X,set_extension([A])).
314 get_member_pred(equal(A,X),X,set_extension([A])).
315 get_member_pred(disjunct(LHS,RHS),X,union(A,B)) :- get_member_pred(LHS,X,A), get_member_pred(RHS,X,B).
316 % TO DO: same for subset?
317 get_subset_pred(subset(X,A),X,A).
318 get_subset_pred(subset_strict(X,A),X,A).
319 %get_subset_pred(member(X,power_set(A)),X,A).
320 get_subset_pred(disjunct(LHS,RHS),X,union(A,B)) :- get_subset_pred(LHS,X,A), get_subset_pred(RHS,X,B).
321
322 % for which supersets is it useful to derive informations from forall quantifier:
323 useful_forall_superset(domain(_)).
324 useful_forall_superset(range(_)).
325 useful_forall_superset(finite(_)).
326 useful_forall_superset(seq(_)).
327 useful_forall_superset(seq1(_)).
328 useful_forall_superset(iseq(_)).
329 useful_forall_superset(iseq1(_)).
330 useful_forall_superset(perm(_)).
331 useful_forall_superset(partial_function(_,_)).
332 useful_forall_superset(total_function(_,_)).
333 useful_forall_superset(total_injection(_,_)).
334 useful_forall_superset(total_surjection(_,_)).
335 useful_forall_superset('$'(_)).
336 useful_forall_superset(pow1_subset(_)). % not empty
337 useful_forall_superset(fin1_subset(_)). % not empty and finite
338 useful_forall_superset(fin_subset(_)). % finite info
339 % TO DO: more
340
341 is_total_relation(total_function(A,_),A).
342 is_total_relation(total_injection(A,_),A).
343 is_total_relation(total_surjection(A,_),A).
344 is_total_relation(total_bijection(A,_),A).
345 is_total_relation(total_surjection_relation(A,_),A).
346
347
348 is_surjective_relation(partial_surjection(_,B),B).
349 is_surjective_relation(surjection_relation(_,B),B).
350 is_surjective_relation(total_surjection(_,B),B).
351 is_surjective_relation(total_bijection(_,B),B).
352 is_surjective_relation(total_surjection_relation(_,B),B).
353 is_surjective_relation(perm(B),B).
354
355 negate_boolean_like_value(boolean_true,boolean_false).
356 negate_boolean_like_value(boolean_false,boolean_true).
357 % TO DO: also treat enumerated sets with exactly two values
358
359 % must match completely
360 get_member_lhs(member(X,Set),X,Set).
361 get_member_lhs(truth,_,typeset).
362
363 % must be an conjunct in rhs
364 get_member_rhs(member(X,Set),X,Set).
365 get_member_rhs(conjunct(A,B),X,Set) :- get_member_rhs(A,X,Set) ; get_member_rhs(B,X,Set).
366 get_member_rhs(not_equal(empty_set,X),X,pow1_subset(typeset)).
367 get_member_rhs(not_equal(X,empty_set),X,pow1_subset(typeset)).
368 get_member_rhs(finite(X),X,fin_subset(typeset)).
369
370
371 compute_bin_op_less_equal(A,B,greater_equal(B,A)) :- can_be_used_for_lookups(B).
372 compute_bin_op_less_equal(card(X),_,finite(X)) :- can_be_used_for_lookups(X).
373
374 compute_bin_op_less(A,B,less_equal(A,B)).
375 compute_bin_op_less(A,B,greater_equal(B,A)) :- can_be_used_for_lookups(B). % we do not lookup greater
376 compute_bin_op_less(A,B,not_equal(A,B)). % for not_equal we only need to store one direction
377 compute_bin_op_less(card(X),_,finite(X)) :- can_be_used_for_lookups(X). % actually card(X)>1 also implies finite(X)
378
379 compute_bin_op_equal(A,B,equal(B,A)) :-
380 can_be_used_for_lookups(B).
381 compute_bin_op_equal(A,B,falsity) :- % sometimes we have FALSE=TRUE as an alternative to falsity
382 is_explicit_value(A,VA),
383 is_explicit_value(B,VB),
384 VA \= VB.
385 compute_bin_op_equal(Set,A,Pred) :-
386 % e.g., A = B \ C => A <: B, useful for examples/B/Alstom/etcs/actions_scn_f6_372_bis.mch
387 derive_superset(Set,B), B \= A,
388 gen_superset(B,A,Pred). % only generate superset rule; for subset there are rules to treat set_subtraction
389 compute_bin_op_equal(A,Set,Pred) :- % interchange args
390 derive_superset(Set,B), B \= A,
391 gen_superset(B,A,Pred).
392 compute_bin_op_equal(A,Set,subset(B,A)) :- % A = B \/ C => B <: A ; useful to allow lookups of B
393 derive_subset(Set,B),
394 can_be_used_for_lookups(B), B \= A.
395 compute_bin_op_equal(A,Add,Res) :- is_add_with_nr(Add,B,Nr),
396 % A = B+Nr => B < A
397 (Nr>0 -> compute_bin_op_less(B,A,Res)
398 ; Nr<0 -> compute_bin_op_less(A,B,Res)
399 ; Res = equal(A,B)).
400 compute_bin_op_equal(A,B,finite(X)) :-
401 (A=card(X);B=card(X)), can_be_used_for_lookups(X). % actually: if any sub-expression uses card(.) we could add it?
402
403 % cf is_explicit_value/3 in well_def_prover
404 % explicit value that can be compared using Prolog unification:
405 is_explicit_value(boolean_true,pred_true).
406 is_explicit_value(boolean_false,pred_false).
407 is_explicit_value(string(A),A).
408 is_explicit_value(Nr,Nr) :- number(Nr).
409
410 is_add_with_nr(add(A,B),X,Nr) :- (number(B) -> (X,Nr)=(A,B) ; number(A) -> (X,Nr)=(B,A)).
411 is_add_with_nr(minus(A,B),A,Nr) :- number(B), Nr is -B.
412
413 derive_superset(set_subtraction(B,_),B). % B \ C <: B
414 derive_superset(intersection(B,_),B). % B /\ C <: B
415 derive_superset(intersection(_,C),C). % B /\ C <: C
416
417 derive_subset(union(B,_),B). % B <: B \/ C
418 derive_subset(union(_,C),C). % C <: B /\ C
419
420 gen_subset(A,B,subset(A,B)) :- can_be_used_for_lookups(A).
421 gen_subset(A,B,superset(B,A)) :- can_be_used_for_lookups(B).
422
423 gen_superset(A,B,superset(A,B)) :- can_be_used_for_lookups(A).
424
425 gen_union([],emptyset).
426 gen_union([X],R) :- !, R=X.
427 gen_union([X|T],union(X,UT)) :- gen_union(T,UT).
428
429 % true if we are likely to need looking up these kinds of terms
430 can_be_used_for_lookups('$'(_)).
431 %can_be_used_for_lookups(Nr) :- number(Nr).
432 can_be_used_for_lookups(domain(_)). % lookup domain of a function
433 can_be_used_for_lookups(range(_)).
434 can_be_used_for_lookups(card(_)).
435 can_be_used_for_lookups(size(_)). % TO DO: normalize size to card, we assume hyps are WD; so no difference
436 can_be_used_for_lookups(interval(_,_)).
437 % ADD: records,...
438
439 useful_hyp(finite(_)).
440 %useful_hyp(partition(_,_)). % now rewritten
441 useful_hyp(member(_,_)).
442 useful_hyp(subset(_,_)).
443 useful_hyp(equal(_,_)).
444 useful_hyp(greater_equal(_,_)).
445 useful_hyp(less_equal(_,_)).
446 useful_hyp(less_equal_real(_,_)).
447 %useful_hyp(less(_,_)). % less is now no longer looked up; we look up not_equal
448 useful_hyp(not_equal(_,_)).
449 useful_hyp(not_member(_,_)). % used in check_not_member_of_set
450 %useful_hyp(equal(A,B)) :- check if A is ID which occurs in B; e.g, x = x*1 not useful
451
452 % a few more binary operations that are potentially useful for :prove, particularly if negation in goal
453 potentially_useful_for_hyp_rule(less(_,_)).
454 potentially_useful_for_hyp_rule(less_real(_,_)).
455 potentially_useful_for_hyp_rule(not_subset(_,_)).
456 potentially_useful_for_hyp_rule(not_subset_strict(_,_)).
457 potentially_useful_for_hyp_rule(subset_strict(_,_)).
458 potentially_useful_for_hyp_rule(partition(_,_)).
459
460 get_clash_renaming_subst(hyp_rec(_,HInfos),ClashRenaming) :- !,
461 get_clash_renaming(HInfos,ClashRenaming).
462 get_clash_renaming_subst(H,R) :- add_internal_error('Illegal hyps:',get_clash_renaming_subst(H,R)),fail.
463
464 % rename an expression or predicate given the current variable clashes
465 get_renamed_expression(Expr,Hyps,RenExpr) :-
466 get_clash_renaming_subst(Hyps,ClashRenaming),
467 rename_bt(Expr,ClashRenaming,RenExpr).
468
469 get_normalized_and_renamed_predicate(Pred,Hyps,RenPred,NormPred) :-
470 get_clash_renaming_subst(Hyps,ClashRenaming),
471 normalize_and_rename_predicate(ClashRenaming,Pred,RenPred,NormPred).
472
473 :- use_module(library(lists),[maplist/3]).
474 % add new quantified $ untyped variables to the hyp stack
475 create_any_type($(ID),b(identifier(ID),any,[])).
476 add_new_hyp_any_vars(H,DollarIDs,H2) :-
477 maplist(create_any_type,DollarIDs,TVars),!,
478 add_new_hyp_variables(H,TVars,H2).
479 add_new_hyp_any_vars(H,I,H2) :- add_internal_error('Illegal Ids:',add_new_hyp_any_vars(H,I,H)),
480 H2=H.
481
482 % add new quantified typed variables to the hyp stack
483 add_new_hyp_variables(H,[],R) :- !, R=H.
484 add_new_hyp_variables(hyp_rec(NH,HInfos1),NewAddedTVars,hyp_rec(NH,HInfos3)) :-
485 fetch_hyp_typed_vars(HInfos1,TVars),
486 list_to_ord_set(NewAddedTVars,SortedNewTVars),
487 add_new_hyp_vars(SortedNewTVars,TVars,NewTVars2,ClashTVars),
488 (ClashTVars=[] -> HInfos2=HInfos1, NewTVars3=NewTVars2
489 ; (debug_mode(off) -> true
490 ; add_message(well_def_analyser,'Variable clash, will rename future predicates: ', ClashTVars,ClashTVars)
491 ),
492 avl_fetch(hyp_clash_vars,HInfos1,clash_rec(GenSymCount,OldClashAVL)),
493 ren_clash_variables(ClashTVars,RenClashTVars,GenSymCount,NewGSC,OldClashAVL,NewClashAVL),
494 avl_store(hyp_clash_vars,HInfos1,clash_rec(NewGSC,NewClashAVL),HInfos2),
495 list_to_ord_set(RenClashTVars,SRenClashTVars),
496 ord_union(SRenClashTVars,NewTVars2,NewTVars3)
497 ),
498 avl_store(hyp_typed_vars,HInfos2,NewTVars3,HInfos3).
499
500 % add_new_typed_vars(AddedTVars,OldTVars,NewTVars,ClashVars)
501 add_new_hyp_vars([],TVars,NewTVars,[]) :- !, NewTVars=TVars.
502 add_new_hyp_vars(AddedTVars,[],NewTVars,[]) :- !,NewTVars=AddedTVars.
503 add_new_hyp_vars([b(identifier(ID1),Type1,I1)|T1],[b(identifier(ID2),Type2,I2)|T2],NewTVars,Clash) :- !,
504 (ID1 @> ID2
505 -> NewTVars = [b(identifier(ID2),Type2,I2)|NewT],
506 add_new_hyp_vars([b(identifier(ID1),Type1,I1)|T1],T2,NewT,Clash)
507 ; ID1 @< ID2
508 -> NewTVars = [b(identifier(ID1),Type1,I1)|NewT],
509 add_new_hyp_vars(T1,[b(identifier(ID2),Type2,I2)|T2],NewT,Clash)
510 ; NewTVars = [b(identifier(ID2),Type2,I2)|NewT],
511 Clash = [b(identifier(ID1),Type1,I1)|NewClash],
512 add_new_hyp_vars(T1,T2,NewT,NewClash)
513 ).
514 add_new_hyp_vars(T1,T2,_,_) :- add_internal_error('Illegal call: ',add_new_hyp_vars(T1,T2,_,_)),fail.
515
516 % add clash ids and their renaming to the clash AVL
517 ren_clash_variables([],[],C,C,Avl,Avl).
518 ren_clash_variables([b(identifier(ID1),Type1,I1)|T1],
519 [b(identifier(RenamedID),Type1,[was(ID1)|I1])|T2], Cin,Cout,AvlIn,AvlOut) :-
520 number_codes(Cin,NC), atom_codes(Ain,NC),
521 atom_concat('$wd_rename_',Ain,RenamedID), % print(rename(ID,RenamedID)),nl,
522 C1 is Cin+1,
523 avl_store(ID1,AvlIn,RenamedID,Avl2),
524 ren_clash_variables(T1,T2,C1,Cout,Avl2,AvlOut).
525
526 % make a fresh copy of existing variables (the variables are not typed but atomic ids)
527 copy_hyp_variables(hyp_rec(NH,HInfos1),ExistingVars,Hyp2) :-
528 fetch_hyp_typed_vars(HInfos1,TVars),
529 list_to_ord_set(ExistingVars,SortedIds),
530 get_existing_tids(SortedIds,TVars,ResTVars),
531 add_new_hyp_variables(hyp_rec(NH,HInfos1),ResTVars,Hyp2).
532
533 get_existing_tids([],_,[]).
534 get_existing_tids([ID|TI],TIDs,Res) :- get_aux(TIDs,ID,TI,Res).
535 :- use_module(probsrc(bsyntaxtree), [get_texpr_id/2]).
536 get_aux([],ID,_,Res) :- add_internal_error('Cannot find existing hyp variable:',ID), Res=[].
537 get_aux([TID|TT],ID,TI,Res) :-
538 (get_texpr_id(TID,ID) -> Res=[TID|ResT], get_existing_tids(TI,TT,ResT)
539 ; get_aux(TT,ID,TI,Res)
540 ).
541
542
543 % similar to create_negation in bsyntaxtree but more rules adapted for hypotheses and WD prover
544
545 :- use_module(probsrc(bsyntaxtree),[extract_info/2]).
546 negate_hyp(b(P,pred,I),Res) :- create_negation_aux(P,I,R),!,Res=R.
547 negate_hyp(Pred,b(negation(Pred),pred,Infos)) :-
548 extract_info(Pred,Infos).
549
550 create_negation_aux(truth,I,R) :- !, R=b(falsity,pred,I).
551 create_negation_aux(falsity,I,R) :- !, R=b(truth,pred,I).
552 create_negation_aux(disjunct(A,B),I,R) :- !,
553 negate_hyp(A,NA), negate_hyp(B,NB), R = b(conjunct(NA,NB),pred,I).
554 create_negation_aux(implication(A,B),I,R) :- !, % not(A=>B) <===> A & not(B)
555 negate_hyp(B,NB), R = b(conjunct(A,NB),pred,I).
556 create_negation_aux(negation(Pred),_,R) :- !, R=Pred.
557 create_negation_aux(BOP,I,R) :- negate_op_aux(BOP,NBOP), R=b(NBOP,pred,I).
558 % no rule for conjunct(A,B)
559
560 % TODO: should we use negate_op ??
561 negate_op_aux(equal(A,B),not_equal(A,B)).
562 negate_op_aux(not_equal(A,B),equal(A,B)).
563 negate_op_aux(less(A,B),greater_equal(A,B)).
564 negate_op_aux(less_equal(A,B),greater(A,B)).
565 negate_op_aux(greater(A,B),less_equal(A,B)).
566 negate_op_aux(greater_equal(A,B),less(A,B)).
567
568 % --------------------
569
570 :- use_module(probsrc(preferences), [get_preference/2]).
571 :- use_module(probsrc(typing_tools),[is_finite_type_in_context/2]).
572 is_finite_type_for_wd(Type,_) :-
573 get_preference(wd_analysis_for_animation,true),!,
574 is_finite_type_in_context(animation,Type).
575 is_finite_type_for_wd(Type,_Hyps) :-
576 is_finite_type_in_context(proving,Type).
577
578
579