| 1 | % (c) 2009-2019 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(ast_cleanup_for_smt, [clean_up/2]). | |
| 6 | ||
| 7 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 8 | :- module_info(group,smt_solvers). | |
| 9 | :- module_info(description,'This module implements transformations needed by the SMT-LIB translation.'). | |
| 10 | ||
| 11 | :- use_module(library(lists),[maplist/3, | |
| 12 | append/2, | |
| 13 | is_list/1, | |
| 14 | include/3]). | |
| 15 | ||
| 16 | :- use_module(probsrc(bsyntaxtree),[is_texpr/1, | |
| 17 | remove_bt/4, | |
| 18 | create_texpr/4, | |
| 19 | get_texpr_expr/2, | |
| 20 | get_texpr_type/2, | |
| 21 | create_negation/2, | |
| 22 | conjunct_predicates/2, | |
| 23 | create_forall/3, | |
| 24 | create_exists/3, | |
| 25 | create_implication/3, | |
| 26 | syntaxtransformation/5, | |
| 27 | unique_typed_id/3, | |
| 28 | is_just_type/1, | |
| 29 | find_typed_identifier_uses/2]). | |
| 30 | :- use_module(probsrc(error_manager), [add_internal_error/2, | |
| 31 | add_error_fail/3]). | |
| 32 | ||
| 33 | :- use_module(probsrc(b_ast_cleanup), [clean_up/3]). | |
| 34 | ||
| 35 | :- use_module(smt_common_predicates). | |
| 36 | :- use_module(seq_rewriter). | |
| 37 | ||
| 38 | clean_up(Expr,Out) :- | |
| 39 | clean_up(Expr,[],CleanExpr), | |
| 40 | rewrite_seq_to_set(CleanExpr,ExprWithoutSeq), | |
| 41 | internal_clean_up(ExprWithoutSeq,Out). | |
| 42 | ||
| 43 | internal_clean_up(ExprWithoutSeq,Out) :- | |
| 44 | % translate:translate_bexpression(ExprWithoutSeq,PPExpr), | |
| 45 | % write(before(PPExpr)),nl, | |
| 46 | %write(before(Expr)),nl, | |
| 47 | clean_up(ExprWithoutSeq,CExpr,[],AC,IDs), !, % do not backtrack and compute another "clean" version! | |
| 48 | %translate:translate_bexpression(CExpr,PPCExpr), | |
| 49 | %write(after(PPCExpr)),nl, | |
| 50 | combine_pred_and_ac(CExpr,AC,IDs,Out). | |
| 51 | %write(after(Out)),nl. | |
| 52 | ||
| 53 | clean_up(Expr,CExprOut,Path,ACOut,IDsOut) :- | |
| 54 | cleanups(pre,Expr,[],TPExpr,Path,ACPre,IDsPre), | |
| 55 | remove_bt(TPExpr,PExpr,LExpr,TLExpr), | |
| 56 | syntaxtransformation(PExpr,Subs,_,NewSubs,LExpr), | |
| 57 | functor(PExpr,F,N), | |
| 58 | % recursively clean up sub-expressions | |
| 59 | maplist(internal_clean_up,ACPre,ACPreClean), | |
| 60 | clean_up_l(Subs,NewSubs,F/N,1,Path,ACL,IDsL), | |
| 61 | maplist(internal_clean_up,ACL,ACLClean), | |
| 62 | cleanups(post,TLExpr,[],CExpr,Path,ACPost,IDsPost), | |
| 63 | maplist(internal_clean_up,ACPost,ACPostClean), | |
| 64 | append([ACPreClean,ACLClean,ACPostClean],AC), | |
| 65 | append([IDsPre,IDsL,IDsPost],IDs), | |
| 66 | (get_texpr_type(CExpr,pred) | |
| 67 | -> combine_pred_and_ac(CExpr,AC,IDs,CExprOut), IDsOut = [], ACOut = [] | |
| 68 | ; CExprOut = CExpr, ACOut = AC, IDsOut = IDs). | |
| 69 | ||
| 70 | combine_pred_and_ac(Pred,AC,IDs,Out) :- | |
| 71 | conjunct_predicates(AC,ACPred), | |
| 72 | conjunct_predicates([Pred,ACPred],OutInnerPred), | |
| 73 | create_exists(IDs,OutInnerPred,Out). | |
| 74 | ||
| 75 | clean_up_l([],[],_Functor,_Nr,_Path,[],[]). | |
| 76 | clean_up_l([Expr|Rest],[CExpr|CRest],Functor,ArgNr,Path,AC,IDs) :- | |
| 77 | clean_up(Expr,CExpr,[arg(Functor,ArgNr)|Path],ACC,IDsC), | |
| 78 | A1 is ArgNr+1, | |
| 79 | clean_up_l(Rest,CRest,Functor,A1,Path,ACL,IDsL), | |
| 80 | append(ACC,ACL,AC), | |
| 81 | append(IDsC,IDsL,IDs). | |
| 82 | ||
| 83 | cleanups(Phase,Expr,AppliedRules,Result,Path,ACS,IDs) :- | |
| 84 | assure_single_rules(AppliedRules,Rule), | |
| 85 | ( cleanup_phase(Phase,Expr,NExpr,Mode/Rule,Path,ACPhase,IDsPhase) -> % try to apply a rule (matching the current phase) | |
| 86 | ( Mode==single -> AppRules = [Rule|AppliedRules] % if the rule is marked as "single", we add to the list of already applied rules | |
| 87 | ; Mode==multi -> AppRules = AppliedRules % if "multi", we do not add it to the list, the rule might be applied more than once | |
| 88 | ; otherwise -> add_error_fail(ast_cleanup_for_smt,'Unexpected rule mode ',Mode)), | |
| 89 | cleanups(Phase,NExpr,AppRules,Result,Path,ACRec,IDsRec), % continue recursively with the new expression | |
| 90 | append(ACPhase,ACRec,ACS), append(IDsPhase,IDsRec,IDs) | |
| 91 | ; otherwise -> % if no rule matches anymore, | |
| 92 | Result = Expr, % we leave the expression unmodified | |
| 93 | ACS = [], IDs = [], | |
| 94 | Rule = none). % and unblock the co-routine (see assure_single_rules/2) | |
| 95 | ||
| 96 | assure_single_rules([],_Rule) :- !. | |
| 97 | assure_single_rules(AppliedRules,Rule) :- | |
| 98 | assure_single_rules2(AppliedRules,Rule). | |
| 99 | :- block assure_single_rules2(?,-). | |
| 100 | assure_single_rules2(_AppliedRules,none) :- !. | |
| 101 | assure_single_rules2(AppliedRules,Rule) :- | |
| 102 | \+ member(Rule, AppliedRules). | |
| 103 | ||
| 104 | cleanup_phase(Phase,OTExpr,NTExpr,Mode/Rule,Path,AC,IDs) :- | |
| 105 | create_texpr(OExpr,OType,OInfo,OTExpr), | |
| 106 | create_texpr(NExpr,NType,NInfo,NTExpr), | |
| 107 | cleanup_phase2(Phase,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path,AC,IDs). | |
| 108 | cleanup_phase2(pre,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,_Path,AC,IDs) :- | |
| 109 | cleanup_pre(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule,AC,IDs), | |
| 110 | (functor(Mode_Rule,'/',2) -> Mode_Rule = Mode/Rule | |
| 111 | ; add_internal_error('Illegal cleanup_pre rule, missing mode: ',Mode_Rule),fail). | |
| 112 | cleanup_phase2(post,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path,AC,IDs) :- | |
| 113 | cleanup_post_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule,Path,AC,IDs), | |
| 114 | (functor(Mode_Rule,'/',2) | |
| 115 | -> Mode_Rule = Mode/Rule %,format(' cleanup_post Rule: ~w/~w~n',[Mode,Rule]) | |
| 116 | ; add_internal_error('Illegal cleanup_post rule, missing mode: ',Mode_Rule),fail). | |
| 117 | ||
| 118 | % enforce well-definedness of division | |
| 119 | cleanup_pre(div(A,B),integer,I,div(A,B),integer,[smt_wd_added|I],multi/div_wd,[AC],[]) :- | |
| 120 | \+ member(smt_wd_added,I), !, | |
| 121 | create_texpr(not_equal(B,b(integer(0),integer,[])),pred,[],AC). | |
| 122 | % replace not_equal(..) by not(equal(..)) | |
| 123 | % and not_member(..) by not(member(..)) | |
| 124 | % and not_subset_strict(..) by not(subset_strict(..)) | |
| 125 | % and not_subset(..) by subset(..) | |
| 126 | cleanup_pre(not_equal(A,B),pred,I,negation(Equal),pred,[],multi/replace_not_equal,[],[]) :- | |
| 127 | create_texpr(equal(A,B),pred,I,Equal). | |
| 128 | cleanup_pre(not_member(A,B),pred,I,negation(Member),pred,[],multi/replace_not_member,[],[]) :- | |
| 129 | create_texpr(member(A,B),pred,I,Member). | |
| 130 | cleanup_pre(not_subset_strict(A,B),pred,I,negation(Subset),pred,[],multi/replace_not_subset_strict,[],[]) :- | |
| 131 | create_texpr(subset_strict(A,B),pred,I,Subset). | |
| 132 | cleanup_pre(not_subset(A,B),pred,I,negation(Subset),pred,[],multi/replace_not_subset,[],[]) :- | |
| 133 | create_texpr(subset(A,B),pred,I,Subset). | |
| 134 | % replace subset_strict by subset and not_equal | |
| 135 | cleanup_pre(subset_strict(A,B),pred,I,conjunct(NotEqual,Subset),pred,[],multi/replace_not_member,[],[]) :- | |
| 136 | create_texpr(subset(A,B),pred,I,Subset), | |
| 137 | create_texpr(not_equal(A,B),pred,I,NotEqual). | |
| 138 | % replace membership in struct by equalities to avoid powerset construction | |
| 139 | cleanup_pre(member(R,S),pred,I,POut,pred,I,multi/replace_struct,[],[]) :- | |
| 140 | get_texpr_expr(R,identifier(_)), | |
| 141 | get_texpr_expr(S,struct(Proto)), | |
| 142 | get_texpr_expr(Proto,rec(Fields)), | |
| 143 | maplist(rewrite_struct_ids(R),Fields,Constraints), | |
| 144 | conjunct_predicates(Constraints,Conj), | |
| 145 | get_texpr_expr(Conj,POut). | |
| 146 | cleanup_pre(member(E,S),pred,I,disjunct(M1,M2),pred,I,multi/split_union_in_member,[],[]) :- | |
| 147 | get_texpr_expr(S,union(S1,S2)), | |
| 148 | create_texpr(member(E,S1),pred,I,M1), | |
| 149 | create_texpr(member(E,S2),pred,I,M2). | |
| 150 | cleanup_pre(member(E,S),pred,I,conjunct(M1,M2),pred,I,multi/split_intersection_in_member,[],[]) :- | |
| 151 | get_texpr_expr(S,intersection(S1,S2)), | |
| 152 | create_texpr(member(E,S1),pred,I,M1), | |
| 153 | create_texpr(member(E,S2),pred,I,M2). | |
| 154 | cleanup_pre(member(E,S),pred,I,conjunct(M1,NotM2),pred,I,multi/split_set_subtraction_in_member,[],[]) :- | |
| 155 | get_texpr_expr(S,set_subtraction(S1,S2)), | |
| 156 | create_texpr(member(E,S1),pred,I,M1), | |
| 157 | create_texpr(member(E,S2),pred,I,M2), | |
| 158 | create_negation(M2,NotM2). | |
| 159 | cleanup_pre(member(E,F),pred,I,C,pred,I,multi/rewrite_member_of_function,[],[]) :- | |
| 160 | rewrite_member_of_function(E,F,C). | |
| 161 | cleanup_pre(member(E,S),pred,I,C,pred,I,multi/rewrite_member_to_disequalities,[],[]) :- | |
| 162 | get_texpr_type(E,integer), | |
| 163 | get_texpr_type(S,set(integer)), | |
| 164 | rewrite_member_to_ge_le(E,S,C). | |
| 165 | cleanup_pre(equal(S,GlobalIntSet),pred,I,C,pred,I,multi/rewrite_equal_to_disequalities,[],[]) :- | |
| 166 | get_texpr_type(S,set(integer)), | |
| 167 | get_texpr_expr(GlobalIntSet,integer_set(_)), | |
| 168 | rewrite_equal_to_ge_le(S,GlobalIntSet,C). | |
| 169 | cleanup_pre(subset(Sub,Super),pred,I,C,pred,I,multi/rewrite_subset_of_integer_set_or_interval,[],[]) :- | |
| 170 | get_texpr_type(Sub,set(integer)), | |
| 171 | (get_texpr_expr(Super,integer_set(_)) ; get_texpr_expr(Super,interval(_,_))), | |
| 172 | rewrite_subset_of_integer_set(Sub,Super,C). | |
| 173 | % if there are still interval nodes after the former rule, try to replace them by constants | |
| 174 | cleanup_pre(interval(From,To),set(integer),I,set_extension(L),set(integer),I,multi/rewrite_constant_interval,[],[]) :- | |
| 175 | get_texpr_expr(From,integer(FI)), | |
| 176 | get_texpr_expr(To,integer(TI)), !, | |
| 177 | constant_interval_as_list(FI,TI,L). | |
| 178 | % remaining intervals have to be rewritten to set comprehensions (introduced forall) | |
| 179 | cleanup_pre(interval(From,To),set(integer),I,comprehension_set([UIdD],Pred),set(integer),I,multi/rewrite_interval_to_set_comprehension,[],[]) :- | |
| 180 | unique_typed_id("_smt_tmp",integer,UIdD), | |
| 181 | create_texpr(greater_equal(UIdD,From),pred,[],Pred1), | |
| 182 | create_texpr(less_equal(UIdD,To),pred,[],Pred2), | |
| 183 | conjunct_predicates([Pred1,Pred2],Pred). | |
| 184 | % rewrite some operators to set comprehensions | |
| 185 | % later rules will rewrite them again and introduce foralls | |
| 186 | cleanup_pre(pow_subset(Set),set(set(T)),I,comprehension_set([UIdD],Pred),set(set(T)),I,multi/rewrite_pow_subset,[],[]) :- | |
| 187 | unique_typed_id("_smt_tmp",set(T),UIdD), | |
| 188 | create_texpr(subset(UIdD,Set),pred,[],Pred). | |
| 189 | cleanup_pre(pow1_subset(Set),set(set(T)),I,comprehension_set([UIdD],Pred),set(set(T)),I,multi/rewrite_pow1_subset,[],[]) :- | |
| 190 | unique_typed_id("_smt_tmp",set(T),UIdD), | |
| 191 | create_texpr(subset(UIdD,Set),pred,[],PredSubset), | |
| 192 | create_texpr(empty_set,set(T),[],EmptySet), | |
| 193 | create_texpr(not_equal(UIdD,EmptySet),pred,[],PredNotEqual), | |
| 194 | conjunct_predicates([PredSubset,PredNotEqual],Pred). | |
| 195 | cleanup_pre(fin_subset(Set),set(set(T)),I,comprehension_set([UIdD],Pred),set(set(T)),I,multi/rewrite_fin_subset,[],[]) :- | |
| 196 | unique_typed_id("_smt_tmp",set(T),UIdD), | |
| 197 | create_texpr(subset(UIdD,Set),pred,[],Pred1), | |
| 198 | create_texpr(finite(Set),pred,[],Pred2), | |
| 199 | conjunct_predicates([Pred1,Pred2],Pred). | |
| 200 | cleanup_pre(fin1_subset(Set),set(set(T)),I,comprehension_set([UIdD],Pred),set(set(T)),I,multi/rewrite_fin1_subset,[],[]) :- | |
| 201 | unique_typed_id("_smt_tmp",set(T),UIdD), | |
| 202 | create_texpr(subset(UIdD,Set),pred,[],PredSubset), | |
| 203 | create_texpr(empty_set,set(T),[],EmptySet), | |
| 204 | create_texpr(not_equal(UIdD,EmptySet),pred,[],PredNotEqual), | |
| 205 | create_texpr(finite(Set),pred,[],PredIsFinite), | |
| 206 | conjunct_predicates([PredSubset,PredNotEqual,PredIsFinite],Pred). | |
| 207 | cleanup_pre(direct_product(SetA,SetB),Type,I,comprehension_set([UIdE,UIdF,UIdG],Pred),Type,I,multi/rewrite_direct_product,[],[]) :- | |
| 208 | Type = set(couple(E,couple(F,G))), | |
| 209 | unique_typed_id("_smt_tmp",E,UIdE), | |
| 210 | unique_typed_id("_smt_tmp",F,UIdF), | |
| 211 | unique_typed_id("_smt_tmp",G,UIdG), | |
| 212 | create_texpr(couple(UIdE,UIdF),couple(E,F),[],CEF), | |
| 213 | create_texpr(couple(UIdE,UIdG),couple(E,G),[],CEG), | |
| 214 | create_texpr(member(CEF,SetA),pred,[],M1), | |
| 215 | create_texpr(member(CEG,SetB),pred,[],M2), | |
| 216 | conjunct_predicates([M1,M2],Pred). | |
| 217 | cleanup_pre(parallel_product(SetA,SetB),Type,I,comprehension_set([UIdE,UIdG,UIdF,UIdH],Pred),Type,I,multi/rewrite_parallel_product,[],[]) :- | |
| 218 | Type = set(couple(couple(E,G),couple(F,H))), | |
| 219 | unique_typed_id("_smt_tmp",E,UIdE), | |
| 220 | unique_typed_id("_smt_tmp",F,UIdF), | |
| 221 | unique_typed_id("_smt_tmp",G,UIdG), | |
| 222 | unique_typed_id("_smt_tmp",H,UIdH), | |
| 223 | create_texpr(couple(UIdE,UIdF),couple(E,F),[],CEF), | |
| 224 | create_texpr(couple(UIdG,UIdH),couple(G,H),[],CGH), | |
| 225 | create_texpr(member(CEF,SetA),pred,[],M1), | |
| 226 | create_texpr(member(CGH,SetB),pred,[],M2), | |
| 227 | conjunct_predicates([M1,M2],Pred). | |
| 228 | cleanup_pre(composition(Rel1,Rel2),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_composition,[],[]) :- | |
| 229 | get_texpr_type(Rel1,set(couple(TD,TI))), | |
| 230 | unique_typed_id("_smt_tmp",TD,UIdD), | |
| 231 | unique_typed_id("_smt_tmp",TR,UIdR), | |
| 232 | unique_typed_id("_smt_tmp",TI,UIdI), | |
| 233 | create_texpr(couple(UIdD,UIdI),couple(TD,TI),[],CoupleDomToI), | |
| 234 | create_texpr(couple(UIdI,UIdR),couple(TI,TR),[],CoupleIToRan), | |
| 235 | create_texpr(member(CoupleDomToI,Rel1),pred,[],Member1), | |
| 236 | create_texpr(member(CoupleIToRan,Rel2),pred,[],Member2), | |
| 237 | conjunct_predicates([Member1,Member2],Inner), | |
| 238 | create_exists([UIdI],Inner,Pred). | |
| 239 | cleanup_pre(domain_restriction(Set,Rel),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_domain_restriction,[],[]) :- | |
| 240 | unique_typed_id("_smt_tmp",TD,UIdD), | |
| 241 | unique_typed_id("_smt_tmp",TR,UIdR), | |
| 242 | create_texpr(couple(UIdD,UIdR),couple(TD,TR),[],Couple), | |
| 243 | create_texpr(member(Couple,Rel),pred,[],MemberOfRel), | |
| 244 | create_texpr(member(UIdD,Set),pred,[],MemberOfSet), | |
| 245 | conjunct_predicates([MemberOfRel,MemberOfSet],Pred). | |
| 246 | cleanup_pre(domain_subtraction(Set,Rel),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_domain_subtraction,[],[]) :- | |
| 247 | unique_typed_id("_smt_tmp",TD,UIdD), | |
| 248 | unique_typed_id("_smt_tmp",TR,UIdR), | |
| 249 | create_texpr(couple(UIdD,UIdR),couple(TD,TR),[],Couple), | |
| 250 | create_texpr(member(Couple,Rel),pred,[],MemberOfRel), | |
| 251 | create_texpr(member(UIdD,Set),pred,[],MemberOfSet), | |
| 252 | create_negation(MemberOfSet,NotMemberOfSet), | |
| 253 | conjunct_predicates([MemberOfRel,NotMemberOfSet],Pred). | |
| 254 | cleanup_pre(range_restriction(Rel,Set),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_range_restriction,[],[]) :- | |
| 255 | unique_typed_id("_smt_tmp",TD,UIdD), | |
| 256 | unique_typed_id("_smt_tmp",TR,UIdR), | |
| 257 | create_texpr(couple(UIdD,UIdR),couple(TD,TR),[],Couple), | |
| 258 | create_texpr(member(Couple,Rel),pred,[],MemberOfRel), | |
| 259 | create_texpr(member(UIdR,Set),pred,[],MemberOfSet), | |
| 260 | conjunct_predicates([MemberOfRel,MemberOfSet],Pred). | |
| 261 | cleanup_pre(range_subtraction(Rel,Set),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_range_subtraction,[],[]) :- | |
| 262 | unique_typed_id("_smt_tmp",TD,UIdD), | |
| 263 | unique_typed_id("_smt_tmp",TR,UIdR), | |
| 264 | create_texpr(couple(UIdD,UIdR),couple(TD,TR),[],Couple), | |
| 265 | create_texpr(member(Couple,Rel),pred,[],MemberOfRel), | |
| 266 | create_texpr(member(UIdR,Set),pred,[],MemberOfSet), | |
| 267 | create_negation(MemberOfSet,NotMemberOfSet), | |
| 268 | conjunct_predicates([MemberOfRel,NotMemberOfSet],Pred). | |
| 269 | cleanup_pre(overwrite(Set1,Set2),set(couple(TD,TR)),I,union(Set2,DomSub),set(couple(TD,TR)),I,multi/rewrite_overwrite,[],[]) :- | |
| 270 | create_texpr(domain(Set2),set(TD),[],DomainSet2), | |
| 271 | create_texpr(domain_subtraction(DomainSet2,Set1),set(couple(TD,TR)),[],DomSub). | |
| 272 | cleanup_pre(cartesian_product(SetA,SetB),set(couple(TR,TD)),I,comprehension_set([UIdR,UIdD],Pred),set(couple(TR,TD)),I,multi/cartesian_product_to_set_comprehension,[],[]) :- | |
| 273 | unique_typed_id("_smt_tmp",TD,UIdD), | |
| 274 | unique_typed_id("_smt_tmp",TR,UIdR), | |
| 275 | create_texpr(member(UIdR,SetA),pred,[],MemberOf1), | |
| 276 | create_texpr(member(UIdD,SetB),pred,[],MemberOf2), | |
| 277 | conjunct_predicates([MemberOf1,MemberOf2],Pred). | |
| 278 | cleanup_pre(Input,pred,I,C,pred,I2,multi/function_application_in_predicate_position_1,[],[]) :- | |
| 279 | Input =.. [Pred,E,Arg], | |
| 280 | \+ is_list(E), % avoids quantifiers | |
| 281 | is_texpr(E), is_texpr(Fun), | |
| 282 | get_texpr_expr(E,function(Fun,Elem)), | |
| 283 | get_texpr_type(Fun,set(couple(RanT,DomT))), | |
| 284 | unique_typed_id("_smt_tmp",DomT,UId), | |
| 285 | create_texpr(couple(Elem,UId),couple(RanT,DomT),[],Couple), | |
| 286 | create_texpr(member(Couple,Fun),pred,[],CoupleInFun), | |
| 287 | Output =.. [Pred,UId,Arg], | |
| 288 | create_texpr(Output,pred,I,UIdInS), | |
| 289 | conjunct_predicates([CoupleInFun,UIdInS],Inner), | |
| 290 | create_exists([UId],Inner,b(C,pred,I2)). | |
| 291 | cleanup_pre(Input,pred,I,C,pred,I2,multi/function_application_in_predicate_position_2,[],[]) :- | |
| 292 | Input =.. [Pred,E,Arg], | |
| 293 | \+ is_list(Arg), % avoids quantifiers | |
| 294 | is_texpr(Arg), is_texpr(Fun), | |
| 295 | get_texpr_expr(Arg,function(Fun,Elem)), | |
| 296 | get_texpr_type(Fun,set(couple(RanT,DomT))), | |
| 297 | unique_typed_id("_smt_tmp",DomT,UId), | |
| 298 | create_texpr(couple(Elem,UId),couple(RanT,DomT),[],Couple), | |
| 299 | create_texpr(member(Couple,Fun),pred,[],CoupleInFun), | |
| 300 | Output =.. [Pred,E,UId], | |
| 301 | create_texpr(Output,pred,I,UIdInS), | |
| 302 | conjunct_predicates([CoupleInFun,UIdInS],Inner), | |
| 303 | create_exists([UId],Inner,b(C,pred,I2)). | |
| 304 | % in case the former two rules have not removed a function/2 | |
| 305 | cleanup_pre(function(F,X),Type,I,UnwrappedId,Type,I,multi/function_application_to_membership,[AC],[UId]) :- | |
| 306 | unique_typed_id("_smt_tmp",Type,UId), | |
| 307 | get_texpr_expr(UId,UnwrappedId), | |
| 308 | get_texpr_type(F,set(FunType)), | |
| 309 | create_texpr(couple(X,UId),FunType,[],CoupleInFunction), | |
| 310 | create_texpr(member(CoupleInFunction,F),pred,[],AC). | |
| 311 | ||
| 312 | % ---------------------------------------------------------------------------- | |
| 313 | % the following rules introduce new identifiers and quantifiers to define them | |
| 314 | % thus, they should be the last rules executed and be avoided if possible | |
| 315 | % some of the expressions that are rewritten here can be removed if they | |
| 316 | % occur in another context, i.e. f(x) in the predicate f(x) : S | |
| 317 | % see rules above | |
| 318 | % ---------------------------------------------------------------------------- | |
| 319 | cleanup_pre(integer_set('INTEGER'),set(integer),I,UnwrappedId,set(integer),I,multi/rewrite_integer_set_if_above_fails,[AC],[UId]) :- | |
| 320 | % the integer set is replaced by an identifier (uid) | |
| 321 | unique_typed_id("_smt_tmp",set(integer),UId), | |
| 322 | get_texpr_expr(UId,UnwrappedId), | |
| 323 | ||
| 324 | % the identifer carries an additional constraint: | |
| 325 | % !(id).(id : uid) | |
| 326 | unique_typed_id("_smt_tmp",integer,IdToQuantify), | |
| 327 | ||
| 328 | create_texpr(member(IdToQuantify,UId),pred,[],MemberIn), | |
| 329 | ||
| 330 | create_forall([IdToQuantify],MemberIn,AC). | |
| 331 | cleanup_pre(min(Set),integer,I,UnwrappedId,integer,I,multi/min_to_definition,[AC1,AC2],[UId]) :- | |
| 332 | unique_typed_id("_smt_tmp",integer,UId), | |
| 333 | get_texpr_expr(UId,UnwrappedId), | |
| 334 | % two axioms: | |
| 335 | % !(x).(x : Set => uid <= x) | |
| 336 | % #(x).(x : Set & uid = x) | |
| 337 | ||
| 338 | unique_typed_id("_smt_tmp",integer,QuantifiedVar), | |
| 339 | ||
| 340 | create_texpr(less_equal(UId,QuantifiedVar),pred,[],LessEqual), | |
| 341 | create_texpr(equal(UId,QuantifiedVar),pred,[],Equal), | |
| 342 | create_texpr(member(QuantifiedVar,Set),pred,[],QuantifiedInSet), | |
| 343 | ||
| 344 | conjunct_predicates([QuantifiedInSet,Equal],ExistsInner), | |
| 345 | create_implication(QuantifiedInSet,LessEqual,ForallInner), | |
| 346 | ||
| 347 | create_exists([QuantifiedVar],ExistsInner,AC1), | |
| 348 | create_forall([QuantifiedVar],ForallInner,AC2). | |
| 349 | cleanup_pre(max(Set),integer,I,UnwrappedId,integer,I,multi/max_to_definition,[AC1,AC2],[UId]) :- | |
| 350 | unique_typed_id("_smt_tmp",integer,UId), | |
| 351 | get_texpr_expr(UId,UnwrappedId), | |
| 352 | % two axioms: | |
| 353 | % !(x).(x : Set => uid >= x) | |
| 354 | % #(x).(x : Set & uid = x) | |
| 355 | ||
| 356 | unique_typed_id("_smt_tmp",integer,QuantifiedVar), | |
| 357 | ||
| 358 | create_texpr(greater_equal(UId,QuantifiedVar),pred,[],GreaterEqual), | |
| 359 | create_texpr(equal(UId,QuantifiedVar),pred,[],Equal), | |
| 360 | create_texpr(member(QuantifiedVar,Set),pred,[],QuantifiedInSet), | |
| 361 | ||
| 362 | conjunct_predicates([QuantifiedInSet,Equal],ExistsInner), | |
| 363 | create_implication(QuantifiedInSet,GreaterEqual,ForallInner), | |
| 364 | ||
| 365 | create_exists([QuantifiedVar],ExistsInner,AC1), | |
| 366 | create_forall([QuantifiedVar],ForallInner,AC2). | |
| 367 | cleanup_pre(card(Set),integer,I,UnwrappedId,integer,I,multi/card_to_exists,[AC1,AC2],[UId]) :- | |
| 368 | unique_typed_id("_smt_tmp",integer,UId), | |
| 369 | get_texpr_expr(UId,UnwrappedId), | |
| 370 | get_texpr_type(Set,set(SetT)), | |
| 371 | unique_typed_id("_smt_tmp",set(couple(integer,SetT)),ForExists), | |
| 372 | create_texpr(interval(b(integer(1),integer,[]),UId),set(integer),[],Interval), | |
| 373 | create_texpr(total_bijection(Interval,Set),set(set(couple(integer,SetT))),[],Bijection), | |
| 374 | create_texpr(member(ForExists,Bijection),pred,[],MemberOf), | |
| 375 | create_exists([ForExists],MemberOf,AC1), | |
| 376 | % without the following constraint, the empty set could have any (negative) cardinality | |
| 377 | create_texpr(greater_equal(UId,b(integer(0),integer,[])),pred,[],AC2). | |
| 378 | cleanup_pre(finite(Set),pred,I,ForallExpr,pred,I,multi/finite_to_forall,[],[]) :- | |
| 379 | get_texpr_type(Set,set(ST)), | |
| 380 | unique_typed_id("_smt_tmp",integer,IDA), | |
| 381 | unique_typed_id("_smt_tmp",integer,IDB), | |
| 382 | create_texpr(interval(IDA,IDB),set(integer),[],IntervalAToB), | |
| 383 | unique_typed_id("_smt_tmp",set(couple(ST,integer)),IDFun), | |
| 384 | create_texpr(total_injection(Set,IntervalAToB),set(set(couple(ST,integer))),[],Functions), | |
| 385 | create_texpr(member(IDFun,Functions),pred,[],Member), | |
| 386 | create_exists([IDB,IDFun],Member,Exists), | |
| 387 | create_forall([IDA],Exists,ForallTExpr), | |
| 388 | get_texpr_expr(ForallTExpr,ForallExpr). | |
| 389 | cleanup_pre(comprehension_set(Identifiers,Pred),set(X),I,UnwrappedId,set(X),I,multi/comprehension_set_to_forall,[AC],[UId]) :- | |
| 390 | expr_list_to_couple_expr(Identifiers,X,IDCouple), | |
| 391 | % the set comprehension is replaced by an identifier (uid) | |
| 392 | unique_typed_id("_smt_tmp",set(X),UId), | |
| 393 | get_texpr_expr(UId,UnwrappedId), | |
| 394 | % the identifer carries an additional constraint: | |
| 395 | % !(id).(Pred(id) <-> id : uid) | |
| 396 | create_texpr(member(IDCouple,UId),pred,[],MemberInComprehension), | |
| 397 | create_implication(Pred,MemberInComprehension,Direction1), | |
| 398 | create_implication(MemberInComprehension,Pred,Direction2), | |
| 399 | % use two foralls instead of equivalence! | |
| 400 | create_forall(Identifiers,Direction1,AC1), | |
| 401 | create_forall(Identifiers,Direction2,AC2), | |
| 402 | conjunct_predicates([AC1,AC2],AC). | |
| 403 | cleanup_pre(identity(Set),set(couple(SetT,SetT)),I,UnwrappedId,set(couple(SetT,SetT)),I,multi/identity_to_forall,[AC],[UId]) :- | |
| 404 | % the identity is replaced by an identifier (uid) | |
| 405 | unique_typed_id("_smt_tmp",set(couple(SetT,SetT)),UId), | |
| 406 | get_texpr_expr(UId,UnwrappedId), | |
| 407 | % the identifer carries an additional constraint: | |
| 408 | % !(id).(id : set <-> (id,id) : uid) | |
| 409 | unique_typed_id("_smt_tmp",SetT,UIdInSet), | |
| 410 | create_texpr(couple(UIdInSet,UIdInSet),couple(SetT,SetT),[],IdCouple), | |
| 411 | create_texpr(member(UIdInSet,Set),pred,[],MemberInSet), | |
| 412 | create_texpr(member(IdCouple,UId),pred,[],MemberInIdentity), | |
| 413 | create_implication(MemberInIdentity,MemberInSet,Direction1), | |
| 414 | create_implication(MemberInSet,MemberInIdentity,Direction2), | |
| 415 | % use two foralls instead of equivalence! | |
| 416 | create_forall([UIdInSet],Direction1,AC1), | |
| 417 | create_forall([UIdInSet],Direction2,AC2), | |
| 418 | conjunct_predicates([AC1,AC2],AC). | |
| 419 | cleanup_pre(reverse(Set),set(couple(TA,TB)),I,UnwrappedId,set(couple(TA,TB)),I,multi/reverse_to_forall,[AC],[UId]) :- | |
| 420 | % the reverse is replaced by an identifier (uid) | |
| 421 | unique_typed_id("_smt_tmp",set(couple(TA,TB)),UId), | |
| 422 | get_texpr_expr(UId,UnwrappedId), | |
| 423 | % the identifer carries an additional constraint: | |
| 424 | % !(ida,idb).((ida,idb) : set <-> (idb,ida) : uid) | |
| 425 | unique_typed_id("_smt_tmp",TA,UIdA), | |
| 426 | unique_typed_id("_smt_tmp",TB,UIdB), | |
| 427 | create_texpr(couple(UIdA,UIdB),couple(TA,TB),[],CoupleAB), | |
| 428 | create_texpr(couple(UIdB,UIdA),couple(TB,TA),[],CoupleBA), | |
| 429 | ||
| 430 | create_texpr(member(CoupleAB,UId),pred,[],MemberA), | |
| 431 | create_texpr(member(CoupleBA,Set),pred,[],MemberB), | |
| 432 | create_implication(MemberA,MemberB,Direction1), | |
| 433 | create_implication(MemberB,MemberA,Direction2), | |
| 434 | % use two foralls instead of equivalence! | |
| 435 | create_forall([UIdA,UIdB],Direction1,AC1), | |
| 436 | create_forall([UIdA,UIdB],Direction2,AC2), | |
| 437 | conjunct_predicates([AC1,AC2],AC). | |
| 438 | cleanup_pre(domain(Set),set(TD),I,UnwrappedId,set(TD),I,multi/domain_to_forall,[AC],[UId]) :- | |
| 439 | % the domain is replaced by an identifier (uid) | |
| 440 | get_texpr_type(Set,set(couple(TD,TR))), | |
| 441 | unique_typed_id("_smt_tmp",set(TD),UId), | |
| 442 | get_texpr_expr(UId,UnwrappedId), | |
| 443 | % the identifer carries an additional constraint: | |
| 444 | % !(id).(id : uid <-> #(idr) : (id,idr) : set) | |
| 445 | unique_typed_id("_smt_tmp",TD,UIdInDomain), | |
| 446 | unique_typed_id("_smt_tmp",TR,UIdInRange), | |
| 447 | ||
| 448 | create_texpr(couple(UIdInDomain,UIdInRange),couple(TD,TR),[],CoupleDR), | |
| 449 | create_texpr(member(CoupleDR,Set),pred,[],CoupleInSet), | |
| 450 | create_exists([UIdInRange],CoupleInSet,ExistsRanElement), | |
| 451 | ||
| 452 | create_texpr(member(UIdInDomain,UId),pred,[],MemberInDomain), | |
| 453 | ||
| 454 | create_implication(ExistsRanElement,MemberInDomain,Direction1), | |
| 455 | create_implication(MemberInDomain,ExistsRanElement,Direction2), | |
| 456 | % use two foralls instead of equivalence! | |
| 457 | create_forall([UIdInDomain],Direction1,AC1), | |
| 458 | create_forall([UIdInDomain],Direction2,AC2), | |
| 459 | conjunct_predicates([AC1,AC2],AC). | |
| 460 | cleanup_pre(range(Set),set(TR),I,UnwrappedId,set(TR),I,multi/range_to_forall,[AC],[UId]) :- | |
| 461 | % the range is replaced by an identifier (uid) | |
| 462 | get_texpr_type(Set,set(couple(TD,TR))), | |
| 463 | unique_typed_id("_smt_tmp",set(TR),UId), | |
| 464 | get_texpr_expr(UId,UnwrappedId), | |
| 465 | % the identifer carries an additional constraint: | |
| 466 | % !(id).(id : uid <-> #(idd) : (idd,id) : set) | |
| 467 | unique_typed_id("_smt_tmp",TD,UIdInDomain), | |
| 468 | unique_typed_id("_smt_tmp",TR,UIdInRange), | |
| 469 | ||
| 470 | create_texpr(couple(UIdInDomain,UIdInRange),couple(TD,TR),[],CoupleDR), | |
| 471 | create_texpr(member(CoupleDR,Set),pred,[],CoupleInSet), | |
| 472 | create_exists([UIdInDomain],CoupleInSet,ExistsDomElement), | |
| 473 | ||
| 474 | create_texpr(member(UIdInRange,UId),pred,[],MemberInRange), | |
| 475 | create_implication(ExistsDomElement,MemberInRange,Direction1), | |
| 476 | create_implication(MemberInRange,ExistsDomElement,Direction2), | |
| 477 | % use two foralls instead of equivalence! | |
| 478 | create_forall([UIdInRange],Direction1,AC1), | |
| 479 | create_forall([UIdInRange],Direction2,AC2), | |
| 480 | conjunct_predicates([AC1,AC2],AC). | |
| 481 | cleanup_pre(image(Function,Set),set(TR),I,UnwrappedId,set(TR),I,multi/image_to_forall,[AC],[UId]) :- | |
| 482 | % the image is replaced by an identifier (uid) | |
| 483 | get_texpr_type(Function,set(couple(TD,TR))), | |
| 484 | unique_typed_id("_smt_tmp",set(TR),UId), | |
| 485 | get_texpr_expr(UId,UnwrappedId), | |
| 486 | % the identifer carries an additional constraint: | |
| 487 | % !(idr).(idr : uid <-> #(idd) : idd:set & (idd,idr) : function) | |
| 488 | unique_typed_id("_smt_tmp",TD,UIdInDomain), | |
| 489 | unique_typed_id("_smt_tmp",TR,UIdInRange), | |
| 490 | ||
| 491 | create_texpr(couple(UIdInDomain,UIdInRange),couple(TD,TR),[],CoupleDR), | |
| 492 | create_texpr(member(CoupleDR,Function),pred,[],CoupleInFunction), | |
| 493 | create_texpr(member(UIdInDomain,Set),pred,[],DomElementInSet), | |
| 494 | conjunct_predicates([CoupleInFunction,DomElementInSet],ExistsInner), | |
| 495 | create_exists([UIdInDomain],ExistsInner,RHS), | |
| 496 | ||
| 497 | create_texpr(member(UIdInRange,UId),pred,[],LHS), | |
| 498 | ||
| 499 | create_implication(LHS,RHS,Direction1), | |
| 500 | create_implication(RHS,LHS,Direction2), | |
| 501 | % use two foralls instead of equivalence! | |
| 502 | create_forall([UIdInRange],Direction1,AC1), | |
| 503 | create_forall([UIdInRange],Direction2,AC2), | |
| 504 | conjunct_predicates([AC1,AC2],AC). | |
| 505 | ||
| 506 | cleanup_post_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,_Path,[],[]) :- | |
| 507 | cleanup_post(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule). | |
| 508 | % remove membership / subset if only used for typing | |
| 509 | cleanup_post(subset(A,B),pred,I,truth,pred,[was(subset(A,B))|I],multi/remove_type_subset) :- | |
| 510 | is_just_type(B), !. | |
| 511 | cleanup_post(member(X,B),pred,I,truth,pred,[was(member(X,B))|I],multi/remove_type_member) :- | |
| 512 | is_just_type(B), !. | |
| 513 | cleanup_post(not_member(X,B),pred,I,falsity,pred,[was(not_member(X,B))|I],multi/remove_type_not_member) :- | |
| 514 | is_just_type(B), !. | |
| 515 | ||
| 516 | expr_list_to_couple_expr(Exprs,TypeOfCoupleExpr,Result) :- | |
| 517 | expr_list_to_couple_expr(Exprs,TypeOfCoupleExpr,[],Result). | |
| 518 | expr_list_to_couple_expr([T],_Type,[],R) :- !, T=R. | |
| 519 | expr_list_to_couple_expr([E|Es],couple(TA,TR),Rest,R) :- | |
| 520 | TA \= couple(_,_), !, | |
| 521 | expr_list_to_couple_expr(Es,TR,Rest,RHS), | |
| 522 | get_texpr_type(RHS,RHST), get_texpr_type(E,ET), | |
| 523 | create_texpr(couple(E,RHS),couple(ET,RHST),[],R). | |
| 524 | expr_list_to_couple_expr(Es,couple(TA,TR),Rest,R) :- !, | |
| 525 | TA = couple(SA,SB), | |
| 526 | expr_list_to_couple_expr(Es,SA,TRest,LHS), | |
| 527 | expr_list_to_couple_expr(TRest,SB,TRest2,RHS), | |
| 528 | get_texpr_type(RHS,RHST), get_texpr_type(LHS,LHST), | |
| 529 | create_texpr(couple(LHS,RHS),couple(LHST,RHST),[],R1), | |
| 530 | expr_list_to_couple_expr(TRest2,TR,Rest,R2), | |
| 531 | get_texpr_type(R1,R1T), get_texpr_type(R2,R2T), | |
| 532 | create_texpr(couple(R1,R2),couple(R1T,R2T),[],R). | |
| 533 | expr_list_to_couple_expr([T|Ts],_Type,Ts,R) :- !, T=R. | |
| 534 | ||
| 535 | rewrite_subset_of_integer_set(Sub,Super,COut) :- | |
| 536 | unique_typed_id("_smt_tmp",integer,ForAllVar), | |
| 537 | create_texpr(member(ForAllVar,Sub),pred,[],LHS), | |
| 538 | create_texpr(member(ForAllVar,Super),pred,[],RHS), % will be replaced by another rule | |
| 539 | create_implication(LHS,RHS,Inner), | |
| 540 | create_forall([ForAllVar],Inner,C), | |
| 541 | get_texpr_expr(C,COut). | |
| 542 | ||
| 543 | rewrite_struct_ids(Record,field(Id,Powerset),Constraint) :- | |
| 544 | get_texpr_type(Powerset,set(IdType)), | |
| 545 | create_texpr(record_field(Record,Id),IdType,[],TheField), | |
| 546 | create_texpr(member(TheField,Powerset),pred,[],Constraint). | |
| 547 | ||
| 548 | % relations | |
| 549 | rewrite_member_of_function(ID,Function,TypeConstraintOut) :- | |
| 550 | get_texpr_expr(Function,relations(Dom,Ran)), | |
| 551 | get_texpr_type(Function,set(set(couple(DomT,RanT)))), | |
| 552 | % relations: only typing constraint !(x,y).((x,y) : ID => x : Dom & y : Ran) | |
| 553 | unique_typed_id("_smt_tmp",DomT,UIdDom), | |
| 554 | unique_typed_id("_smt_tmp",RanT,UIdRan), | |
| 555 | create_texpr(couple(UIdDom,UIdRan),couple(DomT,RanT),[],UIdCouple), | |
| 556 | create_texpr(member(UIdCouple,ID),pred,[],LHS), | |
| 557 | create_texpr(member(UIdDom,Dom),pred,[],RHS1), | |
| 558 | create_texpr(member(UIdRan,Ran),pred,[],RHS2), | |
| 559 | conjunct_predicates([RHS1,RHS2],RHS), | |
| 560 | create_implication(LHS,RHS,TypeConsInner), | |
| 561 | create_forall([UIdDom,UIdRan],TypeConsInner,TypeConstraint), | |
| 562 | get_texpr_expr(TypeConstraint,TypeConstraintOut). | |
| 563 | rewrite_member_of_function(ID,Function,ConstraintOut) :- | |
| 564 | get_texpr_expr(Function,total_relation(Dom,Ran)), | |
| 565 | get_texpr_type(Function,set(set(couple(DomT,RanT)))), | |
| 566 | % total_relation: relation & !(x).(x : Dom => #(y).(y : Ran & (x,y):Id)) | |
| 567 | unique_typed_id("_smt_tmp",DomT,UIdDom), | |
| 568 | unique_typed_id("_smt_tmp",RanT,UIdRan), | |
| 569 | create_texpr(couple(UIdDom,UIdRan),couple(DomT,RanT),[],UIdCouple), | |
| 570 | create_texpr(member(UIdCouple,ID),pred,[],CoupleInID), | |
| 571 | create_exists([UIdRan],CoupleInID,RHS), | |
| 572 | create_texpr(member(UIdDom,Dom),pred,[],LHS), | |
| 573 | create_implication(LHS,RHS,FunConsInner), | |
| 574 | create_forall([UIdDom],FunConsInner,FunConstraint), | |
| 575 | create_texpr(relations(Dom,Ran),set(set(couple(DomT,RanT))),[],Relations), | |
| 576 | create_texpr(member(ID,Relations),pred,[],IsRelation), | |
| 577 | ConstraintOut = conjunct(IsRelation,FunConstraint). | |
| 578 | rewrite_member_of_function(ID,Function,ConstraintOut) :- | |
| 579 | get_texpr_expr(Function,surjection_relation(Dom,Ran)), | |
| 580 | get_texpr_type(Function,set(set(couple(DomT,RanT)))), | |
| 581 | % surjection_relation: relation & ran = T | |
| 582 | create_texpr(range(ID),set(RanT),[],Range), | |
| 583 | create_texpr(equal(Range,Ran),pred,[],FunConstraint), | |
| 584 | create_texpr(relations(Dom,Ran),set(set(couple(DomT,RanT))),[],Relations), | |
| 585 | create_texpr(member(ID,Relations),pred,[],IsRelation), | |
| 586 | ConstraintOut = conjunct(IsRelation,FunConstraint). | |
| 587 | rewrite_member_of_function(ID,Function,ConstraintOut) :- | |
| 588 | get_texpr_expr(Function,total_surjection_relation(Dom,Ran)), | |
| 589 | get_texpr_type(Function,set(set(couple(DomT,RanT)))), | |
| 590 | % total_surjection_relation: total_relation & surjection_relation | |
| 591 | create_texpr(total_relation(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalRelations), | |
| 592 | create_texpr(member(ID,TotalRelations),pred,[],IsTotalRelation), | |
| 593 | create_texpr(surjection_relation(Dom,Ran),set(set(couple(DomT,RanT))),[],SurjectionRelations), | |
| 594 | create_texpr(member(ID,SurjectionRelations),pred,[],IsSurjectionRelation), | |
| 595 | ConstraintOut = conjunct(IsTotalRelation,IsSurjectionRelation). | |
| 596 | % functions | |
| 597 | rewrite_member_of_function(ID,Function,ConstraintOut) :- | |
| 598 | get_texpr_expr(Function,partial_function(Dom,Ran)), | |
| 599 | get_texpr_type(Function,set(set(couple(DomT,RanT)))), | |
| 600 | % partial_function: relation & !(x,y,z).((x,y) : ID & (x,z) : ID => y = z) | |
| 601 | unique_typed_id("_smt_tmp",DomT,UIdDom), | |
| 602 | unique_typed_id("_smt_tmp",RanT,UIdRan), | |
| 603 | unique_typed_id("_smt_tmp",RanT,UIdRan2), | |
| 604 | create_texpr(couple(UIdDom,UIdRan),couple(DomT,RanT),[],UIdCouple), | |
| 605 | create_texpr(couple(UIdDom,UIdRan2),couple(DomT,RanT),[],UIdCouple2), | |
| 606 | create_texpr(member(UIdCouple,ID),pred,[],C1InID), | |
| 607 | create_texpr(member(UIdCouple2,ID),pred,[],C2InID), | |
| 608 | create_texpr(equal(UIdRan,UIdRan2),pred,[],RHS), | |
| 609 | conjunct_predicates([C1InID,C2InID],LHS), | |
| 610 | create_implication(LHS,RHS,FunConsInner), | |
| 611 | create_forall([UIdDom,UIdRan,UIdRan2],FunConsInner,FunConstraint), | |
| 612 | % add typing: is a relation | |
| 613 | create_texpr(relations(Dom,Ran),set(set(couple(DomT,RanT))),[],Relations), | |
| 614 | create_texpr(member(ID,Relations),pred,[],IsRelation), | |
| 615 | ConstraintOut = conjunct(IsRelation,FunConstraint). | |
| 616 | rewrite_member_of_function(ID,Function,ConstraintOut) :- | |
| 617 | get_texpr_expr(Function,total_function(Dom,Ran)), | |
| 618 | get_texpr_type(Function,set(set(couple(DomT,RanT)))), | |
| 619 | % total_function: partial_function & !(x).(x : Dom => #(y).(y : Ran & (x,y):Id)) | |
| 620 | unique_typed_id("_smt_tmp",DomT,UIdDom), | |
| 621 | unique_typed_id("_smt_tmp",RanT,UIdRan), | |
| 622 | create_texpr(couple(UIdDom,UIdRan),couple(DomT,RanT),[],UIdCouple), | |
| 623 | create_texpr(member(UIdCouple,ID),pred,[],CoupleInID), | |
| 624 | create_exists([UIdRan],CoupleInID,RHS), | |
| 625 | create_texpr(member(UIdDom,Dom),pred,[],LHS), | |
| 626 | create_implication(LHS,RHS,FunConsInner), | |
| 627 | create_forall([UIdDom],FunConsInner,FunConstraint), | |
| 628 | % add typing: is a partial_function | |
| 629 | create_texpr(partial_function(Dom,Ran),set(set(couple(DomT,RanT))),[],PFunctions), | |
| 630 | create_texpr(member(ID,PFunctions),pred,[],IsPFunction), | |
| 631 | ConstraintOut = conjunct(IsPFunction,FunConstraint). | |
| 632 | % injections | |
| 633 | rewrite_member_of_function(ID,Function,ConstraintOut) :- | |
| 634 | get_texpr_expr(Function,partial_injection(Dom,Ran)), | |
| 635 | get_texpr_type(Function,set(set(couple(DomT,RanT)))), | |
| 636 | % partial_injection: partial_function & !(x1,x2,y).((x1,y) : ID & (x2,y) : ID => x1 = x2) | |
| 637 | unique_typed_id("_smt_tmp",DomT,UIdDom1), | |
| 638 | unique_typed_id("_smt_tmp",DomT,UIdDom2), | |
| 639 | unique_typed_id("_smt_tmp",RanT,UIdRan), | |
| 640 | create_texpr(couple(UIdDom1,UIdRan),couple(DomT,RanT),[],UIdCouple), | |
| 641 | create_texpr(couple(UIdDom2,UIdRan),couple(DomT,RanT),[],UIdCouple2), | |
| 642 | create_texpr(member(UIdCouple,ID),pred,[],C1InID), | |
| 643 | create_texpr(member(UIdCouple2,ID),pred,[],C2InID), | |
| 644 | create_texpr(equal(UIdDom1,UIdDom2),pred,[],RHS), | |
| 645 | conjunct_predicates([C1InID,C2InID],LHS), | |
| 646 | create_implication(LHS,RHS,FunConsInner), | |
| 647 | create_forall([UIdDom1,UIdDom2,UIdRan],FunConsInner,FunConstraint), | |
| 648 | % add typing: is a partial_function | |
| 649 | create_texpr(partial_function(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialFunctions), | |
| 650 | create_texpr(member(ID,PartialFunctions),pred,[],IsPartialFunction), | |
| 651 | ConstraintOut = conjunct(IsPartialFunction,FunConstraint). | |
| 652 | rewrite_member_of_function(ID,Function,ConstraintOut) :- | |
| 653 | get_texpr_expr(Function,total_injection(Dom,Ran)), | |
| 654 | get_texpr_type(Function,set(set(couple(DomT,RanT)))), | |
| 655 | % total_injection: total_function & partial_injection | |
| 656 | create_texpr(total_function(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalFunctions), | |
| 657 | create_texpr(member(ID,TotalFunctions),pred,[],IsTotalFunction), | |
| 658 | create_texpr(partial_injection(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialInjections), | |
| 659 | create_texpr(member(ID,PartialInjections),pred,[],IsPartialInjection), | |
| 660 | ConstraintOut = conjunct(IsTotalFunction,IsPartialInjection). | |
| 661 | % surjections | |
| 662 | rewrite_member_of_function(ID,Function,ConstraintOut) :- | |
| 663 | get_texpr_expr(Function,partial_surjection(Dom,Ran)), | |
| 664 | get_texpr_type(Function,set(set(couple(DomT,RanT)))), | |
| 665 | % partial_surjection: partial_function & ran = T | |
| 666 | create_texpr(range(ID),set(RanT),[],Range), | |
| 667 | create_texpr(equal(Range,Ran),pred,[],FunConstraint), | |
| 668 | % add typing: is a partial_function | |
| 669 | create_texpr(partial_function(Dom,Ran),set(set(couple(DomT,RanT))),[],PFunctions), | |
| 670 | create_texpr(member(ID,PFunctions),pred,[],IsPFunction), | |
| 671 | ConstraintOut = conjunct(IsPFunction,FunConstraint). | |
| 672 | rewrite_member_of_function(ID,Function,ConstraintOut) :- | |
| 673 | get_texpr_expr(Function,total_surjection(Dom,Ran)), | |
| 674 | get_texpr_type(Function,set(set(couple(DomT,RanT)))), | |
| 675 | % total_surjection: total_function & partial_surjection | |
| 676 | create_texpr(total_function(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalFunctions), | |
| 677 | create_texpr(member(ID,TotalFunctions),pred,[],IsTotalFunction), | |
| 678 | create_texpr(partial_surjection(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialSurjections), | |
| 679 | create_texpr(member(ID,PartialSurjections),pred,[],IsPartialSurjection), | |
| 680 | ConstraintOut = conjunct(IsTotalFunction,IsPartialSurjection). | |
| 681 | % bijections | |
| 682 | rewrite_member_of_function(ID,Function,ConstraintOut) :- | |
| 683 | get_texpr_expr(Function,partial_bijection(Dom,Ran)), | |
| 684 | get_texpr_type(Function,set(set(couple(DomT,RanT)))), | |
| 685 | % partial_bijection: partial_surjection & partial_injection | |
| 686 | create_texpr(partial_surjection(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialSurjections), | |
| 687 | create_texpr(member(ID,PartialSurjections),pred,[],IsPartialSurjection), | |
| 688 | create_texpr(partial_injection(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialInjections), | |
| 689 | create_texpr(member(ID,PartialInjections),pred,[],IsPartialInjection), | |
| 690 | ConstraintOut = conjunct(IsPartialSurjection,IsPartialInjection). | |
| 691 | rewrite_member_of_function(ID,Function,ConstraintOut) :- | |
| 692 | get_texpr_expr(Function,total_bijection(Dom,Ran)), | |
| 693 | get_texpr_type(Function,set(set(couple(DomT,RanT)))), | |
| 694 | % total_bijection: total_surjection & total_injection | |
| 695 | create_texpr(total_surjection(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalSurjections), | |
| 696 | create_texpr(member(ID,TotalSurjections),pred,[],IsTotalSurjection), | |
| 697 | create_texpr(total_injection(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalInjections), | |
| 698 | create_texpr(member(ID,TotalInjections),pred,[],IsTotalInjection), | |
| 699 | ConstraintOut = conjunct(IsTotalSurjection,IsTotalInjection). | |
| 700 | ||
| 701 | rewrite_equal_to_ge_le(ID,GlobalSet,Constraint) :- | |
| 702 | unique_typed_id("_smt_tmp",integer,UId), | |
| 703 | create_texpr(member(UId,ID),pred,[],UIdInSet), | |
| 704 | rewrite_member_to_ge_le(UId,GlobalSet,GeLeConstraints), | |
| 705 | create_texpr(GeLeConstraints,pred,[],GeLeTexpr), | |
| 706 | create_implication(UIdInSet,GeLeTexpr,Direction1), | |
| 707 | create_implication(GeLeTexpr,UIdInSet,Direction2), | |
| 708 | create_forall([UId],Direction1,FA1), | |
| 709 | create_forall([UId],Direction2,FA2), | |
| 710 | Constraint = conjunct(FA1,FA2). | |
| 711 | ||
| 712 | rewrite_member_to_ge_le(ID,Set,Constraint) :- | |
| 713 | get_texpr_expr(Set,interval(Low,High)), | |
| 714 | create_texpr(greater_equal(ID,Low),pred,[],Lower), | |
| 715 | create_texpr(greater_equal(High,ID),pred,[],Higher), | |
| 716 | Constraint = conjunct(Lower,Higher). | |
| 717 | rewrite_member_to_ge_le(ID,Set,Constraint) :- | |
| 718 | get_texpr_expr(Set,integer_set(Kind)), % no cut here see rule below | |
| 719 | bzero(BZero), bone(BOne), bminint(MinInt), bmaxint(MaxInt), | |
| 720 | create_texpr(greater_equal(ID,LowerBound),pred,[],Lower), | |
| 721 | create_texpr(greater_equal(UpperBound,ID),pred,[],Higher), | |
| 722 | Constraint = conjunct(Lower,Higher), | |
| 723 | (Kind = 'NAT' -> LowerBound = BZero, UpperBound = MaxInt ; | |
| 724 | Kind = 'NAT1' -> LowerBound = BOne, UpperBound = MaxInt ; | |
| 725 | Kind = 'INT' -> LowerBound = MinInt, UpperBound = MaxInt). | |
| 726 | rewrite_member_to_ge_le(ID,Set,Constraint) :- | |
| 727 | get_texpr_expr(Set,integer_set(Kind)), !, | |
| 728 | bzero(BZero), bone(BOne), | |
| 729 | (Kind = 'NATURAL' -> Constraint = greater_equal(ID,BZero) ; | |
| 730 | Kind = 'NATURAL1' -> Constraint = greater_equal(ID,BOne)). | |
| 731 | ||
| 732 | bzero(b(integer(0),integer,[])). | |
| 733 | bone(b(integer(1),integer,[])). | |
| 734 | bminint(b(min_int,integer,[])). | |
| 735 | bmaxint(b(max_int,integer,[])). | |
| 736 | ||
| 737 | constant_interval_as_list(FI,TI,[]) :- | |
| 738 | FI > TI. | |
| 739 | constant_interval_as_list(FI,FI,[BI]) :- | |
| 740 | !, create_texpr(integer(FI), integer, [], BI). | |
| 741 | constant_interval_as_list(FI,TI,[BI|BIs]) :- | |
| 742 | create_texpr(integer(FI), integer, [], BI), | |
| 743 | NFI is FI + 1, | |
| 744 | constant_interval_as_list(NFI,TI,BIs). |