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