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 | | |