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