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 |