1 % (c) 2020-2026 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 push_and_rename_normalized_hyp/3,
13 hyps_inconsistent/1,
14 add_new_hyp_variables/3,
15 add_new_hyp_any_vars/3,
16 copy_hyp_variables/3,
17 is_hyp_var/2,
18 get_clash_renaming_subst/2,
19 get_renamed_expression/3,
20 get_normalized_and_renamed_predicate/4,
21 translate_norm_expr/2, translate_norm_expr_with_limit/3,
22 negate_hyp/2,
23 negate_op/2,
24 is_finite_type_for_wd/2,
25
26 normalize_expression/2, normalize_predicate/2,
27 convert_norm_expr_to_raw/2,
28 extract_assert_predicate/2
29 ]).
30
31 :- use_module(probsrc(module_information),[module_info/2]).
32 :- module_info(group,well_def_prover).
33 :- module_info(description,'This module provides hypotheses stack management.').
34
35
36
37 :- use_module(wdsrc(well_def_tools), [not_occurs/2]).
38 :- use_module(probsrc(error_manager)).
39 :- use_module(probsrc(debug)).
40 :- use_module(library(avl)).
41 :- use_module(library(ordsets)).
42 :- use_module(probsrc(avl_tools),[avl_fetch_bin/4, avl_fetch_term/2]).
43
44 % ------------------------------
45
46 % Hypotheses stack management:
47
48
49 % create an empty hyp stack
50 empty_hyps(hyp_rec(E,HI2)) :- empty_avl(E),
51 avl_store(hyp_typed_vars,E,[],HI1), % typed variables of the hypotheses (implicitly universally quantified)
52 avl_store(hyp_clash_vars,HI1,clash_rec(0,E),HI2). % variables which are currently in clash
53
54 hyps_inconsistent(hyp_rec(AVL,_)) :- avl_fetch(falsity,AVL).
55
56 :- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2]).
57 % display the hypotheses stack:
58 portray_hyps(H) :- var(H), !, format('** ILLEGAL VAR Hypotheses: ~w~n',[H]).
59 portray_hyps(hyp_rec(AVL,HInfos)) :- fetch_hyp_vars(HInfos,Vars),
60 get_clashed_vars(HInfos,CVars),
61 (debug_mode(on) -> portray_hyp_vars(hyp_rec(AVL,HInfos)),nl ; true),
62 %b_global_sets:portray_global_sets,
63 !,
64 format('Hypotheses over ~w (clashes: ~w):~n',[Vars,CVars]),
65 %avl_domain(AVL,D), lists:maplist(well_def_hyps:println_nhyp,D),
66 portray_hyp_avl(AVL).
67 portray_hyps(H) :- !, format('** ILLEGAL Hypotheses: ~w~n',[H]).
68
69 portray_hyp_avl(AVL) :-
70 avl_range(AVL,Hyp),
71 conjunct_predicates(Hyp,HypC),
72 translate:nested_print_bexpr(HypC),nl,nl.
73
74 print_tvar(b(identifier(ID),Type,_)) :- format(' ~w : ~w~n',[ID,Type]).
75 :- use_module(library(lists),[maplist/2]).
76 portray_hyp_vars(hyp_rec(_,HInfos)) :- fetch_hyp_typed_vars(HInfos,TVars),!,
77 length(TVars,Len),
78 format('Typed vars in hyps (~w):~n',[Len]),
79 maplist(print_tvar,TVars).
80 portray_hyp_vars(H) :- !, format('** ILLEGAL Hypotheses: ~w~n',[H]).
81
82
83 %println_nhyp(NH) :- format(' --> ~w~n',[NH]).
84
85
86 % ---------------------
87
88 % for debugging:
89 :- public hyp_portray_hook/1.
90 hyp_portray_hook(X) :- nonvar(X), X= hyp_rec(AVL,HInfos),
91 avl_size(AVL,Size),
92 avl_size(HInfos,ISize),
93 format('hyp_rec(#~w,#~w)',[Size,ISize]).
94
95 :- public install_hyp_portray_hook/0.
96 install_hyp_portray_hook :- % mainly for the Prolog debugger
97 assertz(( user:portray(X) :- well_def_hyps:hyp_portray_hook(X) )).
98
99 %:- install_hyp_portray_hook.
100
101
102 % ------------------------
103
104 % get the variable ids currently in scope
105 get_hyp_vars(hyp_rec(_,HInfos),Res) :- get_hyp_vars(HInfos,Vars),!,Res=Vars.
106 get_hyp_vars(H,R) :- add_internal_error('Illegal hyps: ',get_hyp_vars(H,R)), R=[].
107
108 :- use_module(probsrc(bsyntaxtree), [def_get_texpr_ids/2]).
109 fetch_hyp_vars(HInfos,Vars) :- avl_fetch(hyp_typed_vars,HInfos,TVars),
110 def_get_texpr_ids(TVars,Vars).
111 fetch_hyp_typed_vars(HInfos,Vars) :-
112 avl_fetch(hyp_typed_vars,HInfos,Vars).
113 get_clashed_vars(HInfos,Vars) :- avl_fetch(hyp_clash_vars,HInfos,clash_rec(_,AVL)),
114 avl_domain(AVL,Vars).
115 get_clash_renaming(HInfos,Renamings) :- avl_fetch(hyp_clash_vars,HInfos,clash_rec(_,AVL)),
116 findall(rename(ID,FreshID), avl_member(ID,AVL,FreshID), Renamings).
117
118 % check if a variable id is currently in the scope of the hypotheses
119 % if not, it is a global identifier (e.g., enumerated or deferred set)
120 is_hyp_var(Var,hyp_rec(_,HInfos)) :- atomic(Var), nonvar(HInfos),!,
121 fetch_hyp_vars(HInfos,Vars),
122 ord_member(Var,Vars).
123 is_hyp_var(V,H) :- add_internal_error('Illegal call: ',is_hyp_var(V,H)),fail.
124
125 :- use_module(probsrc(tools_lists),[ord_member_nonvar_chk/2]).
126 get_hyp_var_type(Var,hyp_rec(_,HInfos),Type) :- atomic(Var),!,
127 fetch_hyp_typed_vars(HInfos,TVars),
128 TVar = b(identifier(Var),Type,_),
129 ord_member_nonvar_chk(TVar,TVars).
130 get_hyp_var_type(V,H,T) :- add_internal_error('Illegal call: ',is_hyp_var_type(V,H,T)),fail.
131
132 :- use_module(probsrc(bsyntaxtree), [conjunction_to_list/2]).
133 % push a new Hypothesis H on the hyp stack
134 push_hyp(Hyps,H,Options,NewHyps) :-
135 check_valid_hyp_rec(Hyps,push_hyp),
136 conjunction_to_list(H,Hs),
137 push_hyps(Hyps,Hs,Options,NewHyps).
138
139 check_valid_hyp_rec(Hyps,PP) :- var(Hyps),!,
140 add_internal_error('Illegal variable hyp_rec: ',check_hyp_rec(Hyps,PP)),fail.
141 check_valid_hyp_rec(Hyps,PP) :- Hyps \= hyp_rec(_,_),!,
142 add_internal_error('Illegal hyp_rec: ',check_valid_hyp_rec(Hyps,PP)),fail.
143 check_valid_hyp_rec(_,_).
144
145 % push a list of hypotheses
146 push_hyps(hyp_rec(NHyps,HInfos),Hs,Options,hyp_rec(NewNHyps,HInfos)) :- !,
147 get_clash_renaming(HInfos,ClashRenaming),
148 push_hyp_aux(Hs,ClashRenaming,Options,NHyps,NewNHyps).
149 push_hyps(A,B,C,D) :- add_internal_error('Illegal call: ', push_hyps(A,B,C,D)),fail.
150
151 % useful if renaming done outside, e.g., for treating x:=x-1 in WD analyser
152 push_hyps_wo_renaming(hyp_rec(NHyps,HInfos),Hs,Options,hyp_rec(NewNHyps,HInfos)) :- !, ClashRenaming=[],
153 push_hyp_aux(Hs,ClashRenaming,Options,NHyps,NewNHyps).
154 push_hyps_wo_renaming(A,B,C,D) :- add_internal_error('Illegal call: ', push_hyps(A,B,C,D)),fail.
155
156 push_hyp_aux(Hyps,_,_,_,_) :- var(Hyps),!, add_internal_error('Unbound hyps: ',push_hyps(Hyps)),fail.
157 push_hyp_aux([],_,_,NH,NH).
158 push_hyp_aux([H|T],ClashRenaming,Options,NHyps,NewNHyps) :-
159 ((var(NHyps) ; NHyps=hyp_rec(_,_)) -> add_internal_error('Illegal AVL: ',NHyps),fail ; true),
160 push_individual_hyp(H,ClashRenaming,Options,NHyps,NHyps3),
161 push_hyp_aux(T,ClashRenaming,Options,NHyps3,NewNHyps).
162
163 % sometimes we still have conjuncts in the list of hypotheses (e.g., coming from Rodin)
164 push_individual_hyp(b(conjunct(H1,H2),_,_),ClashRenaming,Options,NHyps,NHyps3) :- !,
165 push_individual_hyp(H1,ClashRenaming,Options,NHyps,NHyps2),
166 push_individual_hyp(H2,ClashRenaming,Options,NHyps2,NHyps3).
167 push_individual_hyp(H,ClashRenaming,Options,NHyps,NHyps3) :-
168 normalize_and_rename_predicate(ClashRenaming,H,RenH,NH),
169 % print('PUSH: '),nl, debug:print_quoted_with_max_depth(NH,6), print(' '), error_manager:print_message_span(H),nl,
170 push_normalized_hyp_aux(NH,RenH,Options,NHyps,NHyps3).
171
172 % utility: used to push already normalized and renamed hyp from within prover for normalized sub-goals
173 % should normally be renamed with get_clash_renaming_subst result
174 push_normalized_hyp(NH,hyp_rec(NHyps,I),hyp_rec(NHyps3,I)) :-
175 norm_aux(NH,NormPred),
176 unknown_source_term(NormPred,CorrespondingTExpr),
177 push_normalized_hyp_aux(NormPred,CorrespondingTExpr,[],NHyps,NHyps3).
178
179
180 push_normalized_hyp_aux(NH0,RenH,Options,NHyps,NHyps2) :-
181 simplify_hyp(NH0,NHyps,NH),
182 ((useful_hyp(NH) ; safe_ord_member(create_full_po,Options)
183 ; potentially_useful_for_hyp_rule(NH), safe_ord_member(push_more_hyps,Options)
184 ; useful_implication(NH,Options),
185 true %safe_ord_member(push_more_hyps,Options) % seems useful for Event-B benchmark models, enable by default?
186 )
187 -> avl_store_with_commutes_if_new(NH,NHyps,RenH,NHyps2,Options)
188 %write(pushing_hyp(NH)),nl, portray_hyp_avl(NHyps2),nl
189 ; push_commutative_hyps(NH,RenH,Options,NHyps,NHyps2)
190 % hypothesis not directly used by prover, but there could be alternatives e.g., for disjunct
191 %,functor(NH,FF,NN), print(not_pushing(FF,NN)),nl
192 ).
193
194 :- use_module(wdsrc(well_def_tools), [rename_norm_term/3]).
195 % rename and push an already normalized hyp; also splitting conjuncts
196 push_and_rename_normalized_hyp(Pred,Hyps,NewHyps) :-
197 get_clash_renaming_subst(Hyps,Renaming),
198 rename_norm_term(Pred,Renaming,RenamedPred), %write(push(RenamedPred)),nl,
199 push_conj(RenamedPred,Hyps,NewHyps).
200 push_conj(conjunct(A,B),Hyps,NewHyps) :-
201 push_conj(A,Hyps,Hyps1), push_conj(B,Hyps1,NewHyps).
202 push_conj(A,Hyps,NewHyps) :- push_normalized_hyp(A,Hyps,NewHyps).
203
204
205 % push equivalent or implied hypotheses on the stack:
206 push_commutative_hyps(NH,RenH,Options,NHyps1,NHyps2) :-
207 commute_bin_op(NH,_,Options), % somehow faster than using findall directly
208 !,
209 findall(NH3,commute_bin_op(NH,NH3,Options),NH3s),
210 l_avl_store_nhyps(NH3s,NHyps1,RenH,NHyps2,Options).
211 push_commutative_hyps(_,_,_,NHyps,NHyps).
212
213 safe_ord_member(El,List) :- var(List),!, add_internal_error('Illegal call: ',safe_ord_member(El,List)),fail.
214 safe_ord_member(El,List) :- ord_member(El,List).
215
216 l_avl_store_nhyps([],NHyps,_,NHyps,_Options).
217 l_avl_store_nhyps([NH1|TNH],NHyps1,RenH,NHyps3,Options) :-
218 simplify_hyp(NH1,NHyps1,NH1s),
219 avl_store_if_new(NH1s,NHyps1,RenH,NHyps2,Options),
220 l_avl_store_nhyps(TNH,NHyps2,RenH,NHyps3,Options).
221
222 % store a hypothesis if new (without storing commutative versions of it)
223 avl_store_if_new(NH,H,_,H2,_) :- avl_fetch(NH,H),!, H2=H.
224 avl_store_if_new(NH,H1,RH,H3,Options) :- %write(prop_new(NH)),nl, avl_domain(H1,H1D), write(H1D),nl,nl,
225 propagate_resolution_with_hyp(NH,H1,H2,Options),
226 avl_store(NH,H2,RH,H3).
227
228 % propagate new hyp by applying (simple) resolution: Hyp & not(Hyp) -> add false as hypothesis
229 % also propagates implications Hyp => Q -> add Q as hypothesis
230 propagate_resolution_with_hyp(NormHyp,Hyps,H2,_) :- negate_norm_op(NormHyp,NegNormHyp),
231 avl_fetch(NegNormHyp,Hyps),!,
232 debug_println(9,contradiction_found_in_hypotheses(NormHyp)),
233 avl_store(falsity,Hyps,b(falsity,pred,[neg_hyp]),H2). % false_hyp rule can later trigger
234 propagate_resolution_with_hyp(NH,Hyps,H3,Options) :-
235 %write(fetch_impl(NH)),nl, avl_domain(Hyps,D), write(hyps(D)),nl,
236 % first find implications whose LHS match exactly the new hypothesis NH
237 findall(imp(NH,NRHS),avl_fetch_bin(NH,implication,Hyps,NRHS),TriggeredImplications),
238 propagate_implications(TriggeredImplications,Hyps,H2,Options),
239 % now find implications which do not match exactly, but where we can efficiently lookup variations/weaker versions
240 findall(imp(TLHS,TRHS),get_weakened_impl_trigger(NH,Hyps,TLHS,TRHS),TriggeredImp2),
241 propagate_implications(TriggeredImp2,H2,H3,Options).
242
243 % get triggered implications by weakening added hypothesis first
244 get_weakened_impl_trigger(NH,Hyps,TriggeredLHS,TriggeredRHS) :-
245 weaken_hyp(NH,TriggeredLHS,Condition),
246 Term = implication(TriggeredLHS,TriggeredRHS),
247 avl_fetch_term(Term,Hyps),
248 call(Condition).
249
250 % find weaker hypotheses to look for in LHS of implications which can be triggered
251 % we want to generalise in such a way that we can use avl_fetch_term for efficient logarithmic lookup
252 %weaken_hyp(greater(Term,Nr),greater(Term,int(N1)), safe_less(N1,Nr)) :- number(Nr).
253 weaken_hyp(greater_equal(Term,Nr),greater_equal(Term,N1), safe_less(N1,Nr)) :- number(Nr).
254 weaken_hyp(greater_equal(Nr,Term),less_equal(Term,N1), safe_less(Nr,N1)) :- number(Nr).
255 weaken_hyp(less_equal(Term,Nr),less_equal(Term,N1), safe_less(Nr,N1)) :- number(Nr).
256 weaken_hyp(less_equal(Nr,Term),greater_equal(Term,N1), safe_less(N1,Nr)) :- number(Nr).
257 weaken_hyp(less(Term,Nr),less(Term,N1), safe_less(Nr,N1)) :- number(Nr).
258 weaken_hyp(less_equal_real(Term,Nr),less_equal_real(Term,N1), safe_less(Nr,N1)) :- number(Nr).
259
260 safe_less(X,Y) :- number(X), number(Y), X<Y.
261
262 % add variation of LHS of implementation as hyps, so that later weaken_hyp can find triggered implications:
263 % idea is to move ids or other lookup terms first to be able to use avl_fetch_term
264 variation_useful_for_implementation_triggering(less_equal(Nr,Term),greater_equal(Term,Nr)) :-
265 number(Nr), can_be_used_for_lookups(Term).
266 variation_useful_for_implementation_triggering(greater_equal(Nr,Term),less_equal(Term,Nr)) :-
267 number(Nr), can_be_used_for_lookups(Term).
268 % ----------------------
269
270 negate_norm_op(NormHyp,NegNormHyp) :- negate_op(NormHyp,NegNH),
271 norm_aux(NegNH,NegNormHyp).
272
273 propagate_implications([],Hyps,Hyps,_).
274 propagate_implications([imp(NLHS,NRHS)|TR],NHyps1,NHyps4,Options) :-
275 (avl_delete(implication(NLHS,NRHS),NHyps1,TE,NHyps2)
276 -> % write('propagate : '),translate:print_bexpr(TE),nl,
277 (TE=b(implication(_,RHS),_,_) -> true
278 ; TE=b(disjunct(_,RHS),_,_) -> true
279 ; unknown_source_term(NRHS,RHS),
280 true %add_warning(wd_prover,'Unexpected un-normalised hyp: ',TE)
281 ),
282 simplify_hyp(NRHS,NHyps2,NRHS2),
283 avl_store_with_commutes_if_new(NRHS2,NHyps2,RHS,NHyps3,Options)
284 ; % implication has already been triggered by processing a previous NRHS in the list
285 NHyps3=NHyps1
286 ),
287 propagate_implications(TR,NHyps3,NHyps4,Options).
288
289 unknown_source_term(NormPred,b(unknown_truth_value(NormPred),pred,[trigger_implication])).
290
291 avl_store_with_commutes_if_new(NH,H,_,H2,_) :- avl_fetch(NH,H),!, H2=H.
292 avl_store_with_commutes_if_new(conjunct(NH1,NH2),H0,TE,H2,Options) :- !,
293 (TE=b(conjunct(TE1,TE2),_,_) -> true ; unknown_source_term(NH1,TE1), unknown_source_term(NH2,TE2)),
294 simplify_hyp(NH1,H0,SNH1),
295 avl_store_with_commutes_if_new(SNH1,H0,TE1,H1,Options),
296 simplify_hyp(NH2,H1,SNH2),
297 avl_store_with_commutes_if_new(SNH2,H1,TE2,H2,Options).
298 avl_store_with_commutes_if_new(NH,H0,RH,H3,Options) :- %write(prop_new(NH)),nl, avl_domain(H,H1D), write(H1D),nl,nl,
299 avl_store(NH,H0,RH,H1),
300 propagate_resolution_with_hyp(NH,H1,H2,Options),
301 push_commutative_hyps(NH,RH,Options,H2,H3).
302
303 normalize_expression(Expr,NormExpr) :-
304 (Expr \= b(_,pred,_) -> true ; add_error(well_def_hyps,'Expected expression, but got predicate')),
305 b_interpreter_check:norm_expr_check(Expr,NormExpr).
306
307 :- use_module(probsrc(bsyntaxtree), [rename_bt/3]).
308 normalize_and_rename_predicate(_,H,_,_) :- var(H),!,
309 add_internal_error('Unbound predicate: ',normalize_and_rename_predicate(H)),fail.
310 normalize_and_rename_predicate([],H,RenH,NH) :- !, RenH=H,
311 normalize_predicate(H,NH).
312 normalize_and_rename_predicate(ClashRenaming,H,RenH,NH) :- !,
313 %format('Rename Hyp: ~w ',[ClashRenaming]),translate:print_bexpr(H),nl,
314 rename_bt(H,ClashRenaming,RenH),
315 %print(' > renamed Hyp: '),translate:print_bexpr(RenH),nl,
316 normalize_predicate(RenH,NH).
317
318 % :- use_module(probsrc(bsyntaxtree),[expand_all_lets/2]).
319 % TO DO: expand lets; but can be very expensive; e.g., B/Tickets/Schneider3_Trees/NewSolver_v2.mch -wd-check
320 normalize_predicate(Pred,NormPred) :-
321 b_interpreter_check:norm_pred_check(Pred,NP),
322 norm_aux(NP,NormPred).
323
324
325 % put identifiers first, so that we can more efficiently do lookups;
326 % hence we try and replace less/greater by less_equal/greater_equal when possible
327 norm_aux(equal(A,B),equal(NA,NB)) :- !, norm_equal(A,B,NA,NB).
328 norm_aux(greater(Val,Nr),Res) :- integer(Nr),!, N1 is Nr+1, norm_aux(greater_equal(Val,N1),Res).
329 norm_aux(greater(Nr,Val),Res) :- integer(Nr),!, N1 is Nr-1, norm_aux(greater_equal(N1,Val),Res).
330 norm_aux(greater(A,B),less(B,A)) :- !. % we only look up less (when both args are known)
331 norm_aux(less(Val,Nr),Res) :- integer(Nr),!, N1 is Nr-1, norm_aux(less_equal(Val,N1),Res).
332 norm_aux(less(Nr,Val),Res) :- integer(Nr),!, N1 is Nr+1, norm_aux(less_equal(N1,Val),Res).
333 norm_aux(less_equal(A,Nr),less_equal(A2,Nr2)) :-
334 integer(Nr), peel_constant_offset(A,A2,Offset),!, Nr2 is Nr-Offset.
335 norm_aux(less_equal(Nr,A),less_equal(Nr2,A2)) :-
336 integer(Nr), peel_constant_offset(A,A2,Offset),!, Nr2 is Nr-Offset.
337 norm_aux(greater_equal(A,Nr),greater_equal(A2,Nr2)) :-
338 integer(Nr), peel_constant_offset(A,A2,Offset),!, Nr2 is Nr-Offset.
339 norm_aux(greater_equal(Nr,A),greater_equal(Nr2,A2)) :-
340 integer(Nr), peel_constant_offset(A,A2,Offset),!, Nr2 is Nr-Offset.
341 norm_aux(not_equal(Val,EMPTY),not_equal(Val,empty_set)) :- is_empty_set_alternative(EMPTY),!.
342 norm_aux(not_equal(EMPTY,Val),not_equal(Val,empty_set)) :- is_empty_set_alternative(EMPTY),!.
343 norm_aux(negation(Pred),NormPred) :- negate_op(Pred,NP),!, norm_aux(NP,NormPred).
344 norm_aux(if_predicate(Test,A,B),NormPred) :- !,
345 norm_implication(Test,A,Imp1),
346 negate_op(Test,NTest),norm_implication(NTest,B,Imp2),
347 NormPred = conjunct(Imp1,Imp2). % TODO: separate into distinct conjuncts ?
348 norm_aux(implication(Pred1,Pred2),NormPred) :- !,
349 norm_implication(Pred1,Pred2,NormPred).
350 norm_aux(disjunct(Pred1,Pred2),disjunct(NormPred1,NormPred2)) :- !,
351 norm_aux(Pred1,NormPred1),norm_aux(Pred2,NormPred2).
352 norm_aux(equivalence(Pred1,Pred2),equivalence(NormPred1,NormPred2)) :- !,
353 norm_aux(Pred1,NormPred1),norm_aux(Pred2,NormPred2).
354 %norm_aux(Term,NormPred) :- print(Term),nl,functor(Term,union,2),flatten(Term,union,List,[]), print(union(List)),nl,
355 % sort(List,SL),print(sorted(SL)),nl,fail.
356 norm_aux(external_pred_call('ASSERT_TRUE',[BOOL_EXPR,_ErrString]),NormPred) :-
357 extract_assert_predicate(BOOL_EXPR,Pred), !,
358 normalize_predicate(Pred,NormPred).
359 norm_aux(V,V).
360 % TO DO: subset_strict -> subset and not_equal
361 % TO DO: normalize value(X) terms -> value(int(Nr)) -> Nr, ...
362 % TO DO: maybe process a few rules here x<: dom(f) or x = dom(f) - other
363 % TO DO: what about negation of ASSERT_TRUE, treat ASSERT_EXPR
364
365 % translate boolean expression argument of ASSERT_TRUE, ... into a predicate that must be true
366 extract_assert_predicate(b(convert_bool(Pred),_,_),Res) :- !, Res=Pred.
367 extract_assert_predicate(BOOL_EXPR,b(equal(BOOL_EXPR,b(boolean_true,boolean,[])),pred,[])).
368
369 norm_equal(A,B,RA,RB) :- peel_eq(A,B,SA,SB),
370 (SB='$'(_), SA \= '$'(_) -> RA=SB,RB=SA ; RA=SA, RB=SB).
371
372 % peel constant +/- offsets used for less_equal/greater_equal normalisation:
373 peel_constant_offset(add(X,Y),Res,Offset) :- ((X,Y)=(A,Nr) ; (X,Y)=(Nr,A)), integer(Nr),!,
374 peel_constant_offset(A,Res,OffsetA), Offset is Nr+OffsetA.
375 peel_constant_offset(minus(X,Y),Res,Offset) :- ((X,Y)=(A,Nr) ; (X,Y)=(Nr,A)), integer(Nr),!,
376 peel_constant_offset(A,Res,OffsetA), Offset is OffsetA-Nr.
377 peel_constant_offset(A,A,0).
378
379 peel_eq(reverse(A),reverse(B),SA,SB) :- !, peel_eq(A,B,SA,SB).
380 % TODO: add other injective/reversible operators; also cf. simplify_hyp
381 peel_eq(A,B,A,B).
382
383 norm_implication(conjunct(A,B),Pred2,Implication) :- !,
384 % A & B => C ---> A => (B => C) (so that we can use avl_fetch on LHS of implication)
385 norm_implication(B,Pred2,Implication2),
386 norm_implication(A,Implication2,Implication).
387 norm_implication(Pred1,Pred2,implication(NormPred1,NormPred2)) :-
388 norm_aux(Pred1,NormPred1),norm_aux(Pred2,NormPred2).
389
390
391 % TO DO: flatten and sort union and possibly other operators:
392 %flatten(Term,BOP) --> {functor(Term,BOP,2), arg(1,Term,B1), arg(2,Term,B2)},!,
393 % flatten(B1,BOP), flatten(B2,BOP).
394 %flatten(Term,_) --> [Term].
395
396 is_empty_set_alternative(empty_sequence).
397 is_empty_set_alternative(value(V)) :- V==[]. % should now be handled in norm_expr / norm_value
398
399 negate_op(truth,falsity).
400 negate_op(falsity,truth).
401 negate_op(equal(A,B),not_equal(A,B)).
402 negate_op(not_equal(A,B),equal(A,B)).
403 negate_op(less(A,B),less_equal(B,A)).
404 negate_op(greater(A,B),less_equal(A,B)).
405 negate_op(less_equal(A,B),less(B,A)).
406 negate_op(greater_equal(A,B),less(A,B)).
407 negate_op(less_real(A,B),less_equal_real(B,A)).
408 negate_op(less_equal_real(A,B),less_real(B,A)).
409 negate_op(negation(P),P).
410 negate_op(not_member(A,B),member(A,B)).
411 negate_op(member(A,B),not_member(A,B)). % should we do this?
412 negate_op(not_subset(A,B),subset(A,B)).
413 negate_op(subset(A,B),not_subset(A,B)).
414 negate_op(not_subset_strict(A,B),subset_strict(A,B)).
415 negate_op(subset_strict(A,B),not_subset_strict(A,B)).
416 % should we negate_op(conjunct ...), we also treat negation in prove_po/prove_negated_po
417
418 % for commutative binary operators: also store commutative version to enable lookup on either argument
419 commute_bin_op(OpTerm,CommutativeOrDerivedVersion,_Options) :-
420 commute_bin_op(OpTerm,CommutativeOrDerivedVersion).
421 commute_bin_op(OpTerm,CommutativeOrDerivedVersion,Options) :-
422 safe_ord_member(push_more_hyps,Options),
423 commute_bin_op_aggressive(OpTerm,CommutativeOrDerivedVersion,Options).
424
425 commute_bin_op(equal(A,B),Pred) :- compute_bin_op_equal(A,B,Pred).
426 % not_equal: no need to reverse: we always know both values when doing a lookup
427 commute_bin_op(greater_equal(A,B),less_equal(B,A)) :- can_be_used_for_lookups(B).
428 commute_bin_op(greater(A,B),Pred) :- compute_bin_op_less(B,A,Pred).
429 commute_bin_op(less_equal(A,B),Pred) :- compute_bin_op_less_equal(A,B,Pred).
430 commute_bin_op(less(A,B),Pred) :- compute_bin_op_less(A,B,Pred).
431 commute_bin_op(less_real(A,B),not_equal(A,B)). % TO DO: extend
432 commute_bin_op(subset_strict(A,B),Pred) :- gen_subset(A,B,Pred).
433 commute_bin_op(subset_strict(A,B),not_equal(A,B)).
434 commute_bin_op(subset(A,B),superset(B,A)) :- % new operator, for efficient lookups !
435 can_be_used_for_lookups(B).
436 commute_bin_op(subset(A,cartesian_product(Dom,Ran)),member(A,relations(Dom,Ran))) :-
437 can_be_used_for_lookups(A).
438 commute_bin_op(subset_strict(A,cartesian_product(Dom,Ran)),member(A,relations(Dom,Ran))) :-
439 can_be_used_for_lookups(A).
440 commute_bin_op(not_subset(A,B),not_equal(A,B)). % also implies not_subset_strict
441 commute_bin_op(member(_,Set),not_equal(Set,empty_set)). % x:Set ==> Set /= {}
442 commute_bin_op(member(couple(A,B),C),NewHyp) :-
443 ( NewHyp = member(A,domain(C)) % A|->B : C ==> A : dom(C)
444 ; NewHyp = member(B,range(C)) ). % A|->B : C ==> B : ran(C)
445 commute_bin_op(member(X,interval(Low,Up)),NewHyp) :-
446 (NewHyp = less_equal(Low,Up) % x : Low..Up => Low <= Up
447 ; NewHyp = less_equal(Low,X) % Low <= X if X: Low..UP
448 ; can_be_used_for_lookups(X), NewHyp = greater_equal(X,Low)
449 ; NewHyp = less_equal(X,Up) % X <= UP if X: Low..UP
450 ; can_be_used_for_lookups(Up), NewHyp = greater_equal(Up,X)
451 ).
452 commute_bin_op(member(X,Rel),NewHyp) :- is_total_relation(Rel,Domain),
453 % we cannot efficiently lookup this info from Domain
454 can_be_used_for_lookups(Domain),
455 NewHyp = equal(Domain,domain(X)).
456 commute_bin_op(member(X,Rel),NewHyp) :- is_surjective_relation(Rel,Range),
457 % we cannot efficiently lookup this info from Range
458 can_be_used_for_lookups(Range),
459 NewHyp = equal(Range,range(X)).
460 commute_bin_op(member(card(X),_),NewHyp) :- can_be_used_for_lookups(X),
461 NewHyp=finite(X).
462 commute_bin_op(member(X,union(A,B)),NewHyp) :- can_be_used_for_lookups(X),
463 (NewHyp=implication(not_member(X,A),member(X,B)) % x:A\/B & x/:A => x:B
464 ; NewHyp=implication(not_member(X,B),member(X,A))). % ditto for B
465 commute_bin_op(member(X,set_subtraction(A,B)),NewHyp) :- can_be_used_for_lookups(X),
466 NewHyp=implication(not_member(X,B),member(X,A)). % x:A\B & x/:B => x:A
467 commute_bin_op(member(X,intersection(A,B)),NewHyp) :- can_be_used_for_lookups(X),
468 (NewHyp=member(X,A) ; NewHyp=member(X,B)).
469 commute_bin_op(disjunct(LHS,RHS),NewHyp) :- get_member_pred(LHS,X,A), get_member_pred(RHS,X,B),
470 NewHyp = member(X,union(A,B)).
471 commute_bin_op(disjunct(LHS,RHS),NewHyp) :- get_subset_pred(LHS,X,A), get_subset_pred(RHS,X,B),
472 NewHyp = subset(X,union(A,B)).
473 commute_bin_op(partition(A,List),equal(A,UNION)) :- gen_union(List,UNION).
474 % TO DO: is there a use in the all_disjoint feature?
475 commute_bin_op(forall(['$'(X)],LHSPred,RHSPred), Pred) :-
476 get_member_lhs(LHSPred,'$'(X),Set),
477 get_member_rhs(RHSPred,'$'(X),SET2),
478 useful_forall_superset(SET2),
479 % !x.(x:SET => x:dom(F)) => SET <: dom(F)
480 % !x.(x:SET => x:SET2) => SET <: SET2
481 not_occurs(Set,X),
482 not_occurs(SET2,X), %print(subset1(Set,SET2)),nl,
483 gen_subset(Set,SET2,Pred).
484 commute_bin_op(forall(['$'(X),'$'(Y)],LHSPred,RHSPred), Pred) :- % TO DO: generalise
485 get_member_lhs(LHSPred,couple('$'(X),'$'(Y)),Set), %TO DO: generalise -> domain/range
486 get_member_rhs(RHSPred,'$'(X),SET2),
487 useful_forall_superset(SET2),
488 % !x,y.(x|->y:SET => x:dom(F)) => dom(SET) <: dom(F)
489 % !x,y.(x|->y:SET => x:SET2) => dom(SET) <: SET2
490 not_occurs(Set,X),
491 not_occurs(Set,Y),
492 not_occurs(SET2,X), %print(subset2(Set,SET2)),nl,
493 gen_subset(domain(Set),SET2,Pred).
494 commute_bin_op(equal(A,reverse(B)),equal(B,reverse(A))).
495 commute_bin_op(not_equal(A,B),equal(A,NB)) :- negate_boolean_like_value(B,NB).
496 commute_bin_op(not_equal(intersection(Set1,Set2),empty_set), Pred) :-
497 % Set /\ {a} /= {} => a : Set
498 (Set1=set_extension([A]),B=Set2 -> true ; Set2=set_extension([A]),B=Set1),
499 Pred = member(A,B).
500 commute_bin_op(implication(A,B),implication(VA,B)) :-
501 variation_useful_for_implementation_triggering(A,VA).
502 %commute_bin_op(X,_) :- print(binop(X)),nl,fail.
503
504 % transform disjuncts/equivalences/... into implications that we propagate:
505 commute_bin_op_aggressive(disjunct(LHS,RHS),implication(NegLHS,RHS),Options) :-
506 negate_norm_op(LHS,NegLHS), useful_hyp_or_imp(RHS,Options).
507 commute_bin_op_aggressive(disjunct(RHS,LHS),implication(NegLHS,RHS),Options) :-
508 negate_norm_op(LHS,NegLHS), useful_hyp_or_imp(RHS,Options).
509 commute_bin_op_aggressive(implication(LHS,RHS),implication(NegRHS,NegLHS),_) :- % contra-positive implication
510 negate_norm_op(LHS,NegLHS),
511 negate_norm_op(RHS,NegRHS).
512 commute_bin_op_aggressive(equivalence(LHS,RHS),implication(LHS,RHS),Options) :-
513 useful_hyp_or_imp(RHS,Options).
514 commute_bin_op_aggressive(equivalence(RHS,LHS),implication(LHS,RHS),Options) :-
515 useful_hyp_or_imp(RHS,Options).
516
517 % extract a membership predicate
518 get_member_pred(member(X,A),X,A).
519 get_member_pred(equal(X,A),X,set_extension([A])).
520 get_member_pred(equal(A,X),X,set_extension([A])).
521 get_member_pred(disjunct(LHS,RHS),X,union(A,B)) :- get_member_pred(LHS,X,A), get_member_pred(RHS,X,B).
522 % TO DO: same for subset?
523 get_subset_pred(subset(X,A),X,A).
524 get_subset_pred(subset_strict(X,A),X,A).
525 %get_subset_pred(member(X,power_set(A)),X,A).
526 get_subset_pred(disjunct(LHS,RHS),X,union(A,B)) :- get_subset_pred(LHS,X,A), get_subset_pred(RHS,X,B).
527
528 % for which supersets is it useful to derive informations from forall quantifier:
529 useful_forall_superset(domain(_)).
530 useful_forall_superset(range(_)).
531 useful_forall_superset(finite(_)).
532 useful_forall_superset(seq(_)).
533 useful_forall_superset(seq1(_)).
534 useful_forall_superset(iseq(_)).
535 useful_forall_superset(iseq1(_)).
536 useful_forall_superset(perm(_)).
537 useful_forall_superset(partial_function(_,_)).
538 useful_forall_superset(total_function(_,_)).
539 useful_forall_superset(total_injection(_,_)).
540 useful_forall_superset(total_surjection(_,_)).
541 useful_forall_superset('$'(_)).
542 useful_forall_superset(pow1_subset(_)). % not empty
543 useful_forall_superset(fin1_subset(_)). % not empty and finite
544 useful_forall_superset(fin_subset(_)). % finite info
545 % TO DO: more
546
547 is_total_relation(total_function(A,_),A).
548 is_total_relation(total_injection(A,_),A).
549 is_total_relation(total_surjection(A,_),A).
550 is_total_relation(total_bijection(A,_),A).
551 is_total_relation(total_surjection_relation(A,_),A).
552
553
554 is_surjective_relation(partial_surjection(_,B),B).
555 is_surjective_relation(surjection_relation(_,B),B).
556 is_surjective_relation(total_surjection(_,B),B).
557 is_surjective_relation(total_bijection(_,B),B).
558 is_surjective_relation(total_surjection_relation(_,B),B).
559 is_surjective_relation(perm(B),B).
560
561 negate_boolean_like_value(boolean_true,boolean_false).
562 negate_boolean_like_value(boolean_false,boolean_true).
563 % TO DO: also treat enumerated sets with exactly two values
564
565 % must match completely
566 get_member_lhs(member(X,Set),X,Set).
567 get_member_lhs(truth,_,typeset).
568
569 % must be an conjunct in rhs
570 get_member_rhs(member(X,Set),X,Set).
571 get_member_rhs(conjunct(A,B),X,Set) :- get_member_rhs(A,X,Set) ; get_member_rhs(B,X,Set).
572 get_member_rhs(not_equal(empty_set,X),X,pow1_subset(typeset)).
573 get_member_rhs(not_equal(X,empty_set),X,pow1_subset(typeset)).
574 get_member_rhs(finite(X),X,fin_subset(typeset)).
575
576
577 compute_bin_op_less_equal(A,B,greater_equal(B,A)) :- can_be_used_for_lookups(B).
578 compute_bin_op_less_equal(card(X),_,finite(X)) :- can_be_used_for_lookups(X).
579
580 compute_bin_op_less(A,B,less_equal(A,B)).
581 compute_bin_op_less(A,B,greater_equal(B,A)) :- can_be_used_for_lookups(B). % we do not lookup greater
582 compute_bin_op_less(A,B,not_equal(A,B)). % for not_equal we only need to store one direction
583 compute_bin_op_less(card(X),_,finite(X)) :- can_be_used_for_lookups(X). % actually card(X)>1 also implies finite(X)
584
585 compute_bin_op_equal(A,B,equal(B,A)) :-
586 can_be_used_for_lookups(B).
587 compute_bin_op_equal(A,B,falsity) :- % sometimes we have FALSE=TRUE as an alternative to falsity
588 is_explicit_value(A,VA),
589 is_explicit_value(B,VB),
590 VA \= VB.
591 compute_bin_op_equal(Set,A,Pred) :-
592 % e.g., A = B \ C => A <: B, useful for examples/B/Alstom/etcs/actions_scn_f6_372_bis.mch
593 derive_superset(Set,B), B \= A,
594 gen_superset(B,A,Pred). % only generate superset rule; for subset there are rules to treat set_subtraction
595 compute_bin_op_equal(A,Set,Pred) :- % interchange args
596 derive_superset(Set,B), B \= A,
597 gen_superset(B,A,Pred).
598 compute_bin_op_equal(A,Set,subset(B,A)) :- % A = B \/ C => B <: A ; useful to allow lookups of B
599 derive_subset(Set,B),
600 can_be_used_for_lookups(B), B \= A.
601 compute_bin_op_equal(A,Add,Res) :- is_add_with_nr(Add,B,Nr),
602 % A = B+Nr => B < A
603 (Nr>0 -> compute_bin_op_less(B,A,Res)
604 ; Nr<0 -> compute_bin_op_less(A,B,Res)
605 ; Res = equal(A,B)).
606 compute_bin_op_equal(A,B,finite(X)) :-
607 (A=card(X);B=card(X)), can_be_used_for_lookups(X). % actually: if any sub-expression uses card(.) we could add it?
608
609 % cf is_explicit_value/3 in well_def_prover
610 % explicit value that can be compared using Prolog unification:
611 is_explicit_value(boolean_true,pred_true).
612 is_explicit_value(boolean_false,pred_false).
613 is_explicit_value(string(A),A).
614 is_explicit_value(Nr,Nr) :- number(Nr).
615
616 is_add_with_nr(add(A,B),X,Nr) :- (number(B) -> (X,Nr)=(A,B) ; number(A) -> (X,Nr)=(B,A)).
617 is_add_with_nr(minus(A,B),A,Nr) :- number(B), Nr is -B.
618
619 derive_superset(set_subtraction(B,_),B). % B \ C <: B
620 derive_superset(intersection(B,_),B). % B /\ C <: B
621 derive_superset(intersection(_,C),C). % B /\ C <: C
622
623 derive_subset(union(B,_),B). % B <: B \/ C
624 derive_subset(union(_,C),C). % C <: B /\ C
625
626 gen_subset(A,B,subset(A,B)) :- can_be_used_for_lookups(A).
627 gen_subset(A,B,superset(B,A)) :- can_be_used_for_lookups(B).
628
629 gen_superset(A,B,superset(A,B)) :- can_be_used_for_lookups(A).
630
631 gen_union([],emptyset).
632 gen_union([X],R) :- !, R=X.
633 gen_union([X|T],union(X,UT)) :- gen_union(T,UT).
634
635 % true if we are likely to need looking up these kinds of terms
636 can_be_used_for_lookups('$'(_)).
637 %can_be_used_for_lookups(Nr) :- number(Nr).
638 can_be_used_for_lookups(domain(_)). % lookup domain of a function
639 can_be_used_for_lookups(range(_)).
640 can_be_used_for_lookups(card(_)).
641 can_be_used_for_lookups(size(_)). % TO DO: normalize size to card, we assume hyps are WD; so no difference
642 can_be_used_for_lookups(interval(_,_)).
643 % ADD: records,...
644
645 useful_hyp(finite(_)).
646 %useful_hyp(partition(_,_)). % now rewritten
647 useful_hyp(member(_,_)).
648 useful_hyp(subset(_,_)).
649 useful_hyp(equal(_,_)).
650 useful_hyp(greater_equal(_,_)).
651 useful_hyp(less_equal(_,_)).
652 useful_hyp(less_equal_real(_,_)).
653 %useful_hyp(less(_,_)). % less is now no longer looked up; we look up not_equal
654 useful_hyp(not_equal(_,_)).
655 useful_hyp(not_member(_,_)). % used in check_not_member_of_set
656 %useful_hyp(equal(A,B)) :- check if A is ID which occurs in B; e.g, x = x*1 not useful
657
658 useful_implication(implication(_,RHS),Options) :-
659 useful_hyp_or_imp(RHS,Options).
660 useful_hyp_or_imp(RHS,Options) :-
661 (useful_hyp(RHS) -> true
662 ; useful_implication_body(RHS,Options)). % useful upon pushing hyps in propagate_resolution_with_hyp
663
664 % implication or similar which could be useful (i.e., triggered so that it produces a really useful hypothesis)
665 useful_implication_body(implication(_,RHS),Options) :-
666 useful_hyp_or_imp(RHS,Options).
667 useful_implication_body(equivalence(_,_),Options) :- safe_ord_member(push_more_hyps,Options).
668 useful_implication_body(disjunct(_,_),Options) :- safe_ord_member(push_more_hyps,Options).
669 useful_implication_body(conjunct(LHS,RHS),Options) :-
670 (useful_hyp_or_imp(LHS,Options) -> true ; useful_hyp_or_imp(RHS,Options)).
671
672 % check if we can simplify the hypothesis
673 simplify_hyp(implication(LHS,RHS),Hyps,Res) :- % true => RHS --> RHS
674 %write(check_imp_lhs_hyp(LHS)),nl, avl_domain(Hyps,D), write(dom(D)),nl,
675 avl_fetch(LHS,Hyps),!, % LHS is in the hyps
676 %write(simplify_imp(LHS,RHS)),nl,
677 simplify_hyp(RHS,Hyps,Res).
678 % TODO: disjunction, ...
679 simplify_hyp(Hyp,_,Hyp).
680
681
682 % a few more binary operations that are potentially useful for :prove, particularly if negation in goal
683 potentially_useful_for_hyp_rule(less(_,_)).
684 potentially_useful_for_hyp_rule(less_real(_,_)).
685 potentially_useful_for_hyp_rule(not_subset(_,_)).
686 potentially_useful_for_hyp_rule(not_subset_strict(_,_)).
687 potentially_useful_for_hyp_rule(subset_strict(_,_)).
688 potentially_useful_for_hyp_rule(partition(_,_)).
689
690 get_clash_renaming_subst(hyp_rec(_,HInfos),ClashRenaming) :- !,
691 get_clash_renaming(HInfos,ClashRenaming).
692 get_clash_renaming_subst(H,R) :- add_internal_error('Illegal hyps:',get_clash_renaming_subst(H,R)),fail.
693
694 % rename an expression or predicate given the current variable clashes
695 get_renamed_expression(Expr,Hyps,RenExpr) :-
696 get_clash_renaming_subst(Hyps,ClashRenaming),
697 rename_bt(Expr,ClashRenaming,RenExpr).
698
699 get_normalized_and_renamed_predicate(Pred,Hyps,RenPred,NormPred) :-
700 get_clash_renaming_subst(Hyps,ClashRenaming),
701 normalize_and_rename_predicate(ClashRenaming,Pred,RenPred,NormPred).
702
703 :- use_module(library(lists),[maplist/3]).
704 % add new quantified $ untyped variables to the hyp stack
705 create_any_type($(ID),b(identifier(ID),any,[])).
706 add_new_hyp_any_vars(H,DollarIDs,H2) :-
707 maplist(create_any_type,DollarIDs,TVars),!,
708 add_new_hyp_variables(H,TVars,H2).
709 add_new_hyp_any_vars(H,I,H2) :- add_internal_error('Illegal Ids:',add_new_hyp_any_vars(H,I,H)),
710 H2=H.
711
712 % add new quantified typed variables to the hyp stack
713 add_new_hyp_variables(H,[],R) :- !, R=H.
714 add_new_hyp_variables(hyp_rec(NH,HInfos1),NewAddedTVars,hyp_rec(NH,HInfos3)) :-
715 fetch_hyp_typed_vars(HInfos1,TVars),
716 list_to_ord_set(NewAddedTVars,SortedNewTVars),
717 add_new_hyp_vars(SortedNewTVars,TVars,NewTVars2,ClashTVars),
718 (ClashTVars=[] -> HInfos2=HInfos1, NewTVars3=NewTVars2
719 ; (debug_mode(off) -> true
720 ; add_message(well_def_analyser,'Variable clash, will rename future predicates: ', ClashTVars,ClashTVars)
721 ),
722 avl_fetch(hyp_clash_vars,HInfos1,clash_rec(GenSymCount,OldClashAVL)),
723 ren_clash_variables(ClashTVars,RenClashTVars,GenSymCount,NewGSC,OldClashAVL,NewClashAVL),
724 avl_store(hyp_clash_vars,HInfos1,clash_rec(NewGSC,NewClashAVL),HInfos2),
725 list_to_ord_set(RenClashTVars,SRenClashTVars),
726 ord_union(SRenClashTVars,NewTVars2,NewTVars3)
727 ),
728 avl_store(hyp_typed_vars,HInfos2,NewTVars3,HInfos3).
729
730 % add_new_typed_vars(AddedTVars,OldTVars,NewTVars,ClashVars)
731 add_new_hyp_vars([],TVars,NewTVars,[]) :- !, NewTVars=TVars.
732 add_new_hyp_vars(AddedTVars,[],NewTVars,[]) :- !,NewTVars=AddedTVars.
733 add_new_hyp_vars([b(identifier(ID1),Type1,I1)|T1],[b(identifier(ID2),Type2,I2)|T2],NewTVars,Clash) :- !,
734 (ID1 @> ID2
735 -> NewTVars = [b(identifier(ID2),Type2,I2)|NewT],
736 add_new_hyp_vars([b(identifier(ID1),Type1,I1)|T1],T2,NewT,Clash)
737 ; ID1 @< ID2
738 -> NewTVars = [b(identifier(ID1),Type1,I1)|NewT],
739 add_new_hyp_vars(T1,[b(identifier(ID2),Type2,I2)|T2],NewT,Clash)
740 ; NewTVars = [b(identifier(ID2),Type2,I2)|NewT],
741 Clash = [b(identifier(ID1),Type1,I1)|NewClash],
742 add_new_hyp_vars(T1,T2,NewT,NewClash)
743 ).
744 add_new_hyp_vars(T1,T2,_,_) :- add_internal_error('Illegal call: ',add_new_hyp_vars(T1,T2,_,_)),fail.
745
746 % add clash ids and their renaming to the clash AVL
747 ren_clash_variables([],[],C,C,Avl,Avl).
748 ren_clash_variables([b(identifier(ID1),Type1,I1)|T1],
749 [b(identifier(RenamedID),Type1,[was(ID1)|I1])|T2], Cin,Cout,AvlIn,AvlOut) :-
750 number_codes(Cin,NC), atom_codes(Ain,NC),
751 atom_concat('$wd_rename_',Ain,RenamedID), % print(rename(ID,RenamedID)),nl,
752 C1 is Cin+1,
753 avl_store(ID1,AvlIn,RenamedID,Avl2),
754 ren_clash_variables(T1,T2,C1,Cout,Avl2,AvlOut).
755
756 % make a fresh copy of existing variables (the variables are not typed but atomic ids)
757 copy_hyp_variables(hyp_rec(NH,HInfos1),ExistingVars,Hyp2) :-
758 fetch_hyp_typed_vars(HInfos1,TVars),
759 list_to_ord_set(ExistingVars,SortedIds),
760 get_existing_tids(SortedIds,TVars,ResTVars),
761 add_new_hyp_variables(hyp_rec(NH,HInfos1),ResTVars,Hyp2).
762
763 get_existing_tids([],_,[]).
764 get_existing_tids([ID|TI],TIDs,Res) :- get_aux(TIDs,ID,TI,Res).
765 :- use_module(probsrc(bsyntaxtree), [get_texpr_id/2]).
766 get_aux([],ID,_,Res) :- add_internal_error('Cannot find existing hyp variable:',ID), Res=[].
767 get_aux([TID|TT],ID,TI,Res) :-
768 (get_texpr_id(TID,ID) -> Res=[TID|ResT], get_existing_tids(TI,TT,ResT)
769 ; get_aux(TT,ID,TI,Res)
770 ).
771
772
773 % similar to create_negation in bsyntaxtree but more rules adapted for hypotheses and WD prover
774
775 :- use_module(probsrc(bsyntaxtree),[extract_info/2]).
776 negate_hyp(b(P,pred,I),Res) :- create_negation_aux(P,I,R),!,Res=R.
777 negate_hyp(Pred,b(negation(Pred),pred,Infos)) :-
778 extract_info(Pred,Infos).
779
780 create_negation_aux(truth,I,R) :- !, R=b(falsity,pred,I).
781 create_negation_aux(falsity,I,R) :- !, R=b(truth,pred,I).
782 create_negation_aux(disjunct(A,B),I,R) :- !,
783 negate_hyp(A,NA), negate_hyp(B,NB), R = b(conjunct(NA,NB),pred,I).
784 create_negation_aux(implication(A,B),I,R) :- !, % not(A=>B) <===> A & not(B)
785 negate_hyp(B,NB), R = b(conjunct(A,NB),pred,I).
786 create_negation_aux(negation(Pred),_,R) :- !, R=Pred.
787 create_negation_aux(if_predicate(Test,A,B),I,R) :- !,
788 %not(Test=>A & not(Test)=>B) <===> Test & not(A) or not(Test) & not(B)
789 negate_hyp(A,NA), D1 = b(conjunct(Test,NA),pred,I),
790 negate_hyp(Test,NTest), negate_hyp(B,NB), D2 = b(conjunct(NTest,NB),pred,I),
791 R = b(conjunct(D1,D2),pred,I).
792 create_negation_aux(BOP,I,R) :- negate_op_aux(BOP,NBOP), R=b(NBOP,pred,I).
793 % no rule for conjunct(A,B)
794
795 % TODO: should we use negate_op ??
796 negate_op_aux(equal(A,B),not_equal(A,B)).
797 negate_op_aux(not_equal(A,B),equal(A,B)).
798 negate_op_aux(less(A,B),greater_equal(A,B)).
799 negate_op_aux(less_equal(A,B),greater(A,B)).
800 negate_op_aux(greater(A,B),less_equal(A,B)).
801 negate_op_aux(greater_equal(A,B),less(A,B)).
802
803 % --------------------
804
805 :- use_module(probsrc(preferences), [get_preference/2]).
806 :- use_module(probsrc(typing_tools),[is_finite_type_in_context/2]).
807 is_finite_type_for_wd(Type,_) :-
808 get_preference(wd_analysis_for_animation,true),!,
809 is_finite_type_in_context(animation,Type).
810 is_finite_type_for_wd(Type,_Hyps) :-
811 is_finite_type_in_context(proving,Type).
812
813
814 % -------------------
815
816 % convert a normalized expression to a raw expression (e.g., for pretty printing translate:print_raw_bexpr
817 % or translate:transform_raw)
818
819 :- use_module(library(lists),[is_list/1]).
820 convert_norm_expr_to_raw('$'(ID),Res) :- !, Res=identifier(unknown,ID).
821 convert_norm_expr_to_raw(Int,Res) :- integer(Int),!,Res=integer(unknown,Int).
822 convert_norm_expr_to_raw(Nr,Res) :- float(Nr),!,Res=real(unknown,Nr).
823 convert_norm_expr_to_raw(X,Res) :- integer_set_name_to_raw(X,Res), !.
824 convert_norm_expr_to_raw(set_extension(List),Res) :- !,
825 Res = set_extension(unknown,RList),
826 l_convert_norm(List,RList).
827 convert_norm_expr_to_raw(sequence_extension(List),Res) :- !,
828 Res = sequence_extension(unknown,RList),
829 l_convert_norm(List,RList).
830 convert_norm_expr_to_raw(Term,Res) :-
831 Term =.. [Functor,List,LHS,RHS],
832 ? member(Functor, [forall,event_b_comprehension_set,quantified_union,quantified_intersection]),!,
833 Res =.. [Functor,unknown,RList,RLHS,RRHS],
834 l_convert_norm(List,RList),
835 convert_norm_expr_to_raw(LHS,RLHS),
836 convert_norm_expr_to_raw(RHS,RRHS).
837 convert_norm_expr_to_raw(exists(List,Pred),Res) :- !,
838 Res = exists(unknown,RList,RPred),
839 l_convert_norm(List,RList),
840 convert_norm_expr_to_raw(Pred,RPred).
841 convert_norm_expr_to_raw(function(Functor,Args),Res) :- !,
842 Res = function(unknown,RFunctor,RList),
843 (is_list(Args) -> List=Args ; List=[Args]),
844 l_convert_norm(List,RList),
845 convert_norm_expr_to_raw(Functor,RFunctor).
846 convert_norm_expr_to_raw(partition(Set,Args),Res) :- !,
847 Res = partition(unknown,RSet,RArgs),
848 l_convert_norm(Args,RArgs),
849 convert_norm_expr_to_raw(Set,RSet).
850 % TODO: more special cases where generic code below does not work:
851 convert_norm_expr_to_raw(Term,Res) :- Term =.. [Functor|Args],
852 l_convert_norm(Args,RawArgs),
853 Res =.. [Functor,unknown|RawArgs].
854
855 l_convert_norm([],[]).
856 l_convert_norm([H|T],[RH|RT]) :- convert_norm_expr_to_raw(H,RH), l_convert_norm(T,RT).
857
858 integer_set_name_to_raw('INTEGER',integer_set(unknown)).
859 integer_set_name_to_raw('NATURAL',natural_set(unknown)).
860 integer_set_name_to_raw('NATURAL1',natural1_set(unknown)).
861 integer_set_name_to_raw('INT',int_set(unknown)).
862 integer_set_name_to_raw('NAT',nat_set(unknown)).
863 integer_set_name_to_raw('NAT1',nat1_set(unknown)).
864
865 :- use_module(probsrc(translate),[translate_raw_bexpr/2,translate_raw_bexpr_with_limit/3]).
866 translate_norm_expr(NormExpr,Str) :-
867 (convert_norm_expr_to_raw(NormExpr,RawExpr)
868 -> translate_raw_bexpr(RawExpr,Str)
869 ; add_error(translate_norm_expr,'Cannot translate norm expression:',NormExpr),
870 Str = '???'
871 ).
872 translate_norm_expr_with_limit(NormExpr,Limit,Str) :-
873 (convert_norm_expr_to_raw(NormExpr,RawExpr)
874 -> translate_raw_bexpr_with_limit(RawExpr,Limit,Str)
875 ; add_error(translate_norm_expr,'Cannot translate norm expression:',NormExpr),
876 Str = '???'
877 ).