| 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 | ||
| 6 | :- module(kodkod,[apply_kodkod/3, apply_kodkod/4, | |
| 7 | replace_by_kodkod/3, | |
| 8 | current_solver_is_not_incremental/0, | |
| 9 | kodkod_request/5, | |
| 10 | apply_kodkod_to_counterexample_search/5, | |
| 11 | kodkod_reset/0]). | |
| 12 | ||
| 13 | :- use_module(library(lists)). | |
| 14 | :- use_module(library(avl)). | |
| 15 | ||
| 16 | :- use_module(probsrc(tools)). | |
| 17 | :- use_module(probsrc(bmachine)). | |
| 18 | :- use_module(probsrc(self_check)). | |
| 19 | :- use_module(probsrc(bsyntaxtree)). | |
| 20 | :- use_module(probsrc(translate)). | |
| 21 | :- use_module(probsrc(predicate_analysis)). | |
| 22 | :- use_module(probsrc(btypechecker)). | |
| 23 | :- use_module(probsrc(b_global_sets),[b_global_set/1,lookup_global_constant/2]). | |
| 24 | :- use_module(probsrc(preferences),[get_preference/2]). | |
| 25 | ||
| 26 | :- use_module(kodkod_translate). | |
| 27 | :- use_module(kodkod_tools). | |
| 28 | :- use_module(kodkod_rewrite). | |
| 29 | :- use_module(kodkod2). | |
| 30 | :- use_module(kodkod_typing). | |
| 31 | :- use_module(kodkod_process). | |
| 32 | ||
| 33 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 34 | :- module_info(group,kodkod). | |
| 35 | :- module_info(description,'This is the central module of the B to Kodkod translation (still experimental).'). | |
| 36 | ||
| 37 | %:- dynamic kodkod_error/1. | |
| 38 | ||
| 39 | kodkod_reset :- | |
| 40 | ( stop_kodkod -> true; true). | |
| 41 | ||
| 42 | % Signum is either pos (when we want the predicate to succeed) or neg (when we want the predicate to be false) | |
| 43 | kodkod_request(Id,Signum,LocalState,State,LWF) :- | |
| 44 | % MaxNrOfSols is the maximum number of solutions found in one go by Kodkod | |
| 45 | get_max_nr_of_solutions(MaxNrOfSols), | |
| 46 | kodkod_request(Id,Signum,MaxNrOfSols,LocalState,State,LWF). | |
| 47 | ||
| 48 | get_max_nr_of_solutions(MaxNrOfSols) :- | |
| 49 | current_solver_is_not_incremental,!, | |
| 50 | MaxNrOfSols = 1. | |
| 51 | get_max_nr_of_solutions(MaxNrOfSols) :- | |
| 52 | get_preference(kodkod_max_nr_solutions,MaxNrOfSols). % TO DO: we could look at kodkod_for_components and maxNrOfInitialisations preference | |
| 53 | ||
| 54 | current_solver_is_not_incremental :- | |
| 55 | get_preference(kodkod_sat_solver,Solver), | |
| 56 | not_incremental(Solver). | |
| 57 | not_incremental(lingeling). | |
| 58 | ||
| 59 | :- use_module(probsrc(error_manager)). | |
| 60 | ||
| 61 | :- block kodkod_request(?,?,?,?,?,-). | |
| 62 | kodkod_request(Id,Signum,MaxNrOfSols,LocalState,State,_LWF) :- | |
| 63 | on_exception(error(system_error,system_error(E)), % often SPIO_E_NET_CONNRESET | |
| 64 | kodkod_request_intern(Id,Signum,MaxNrOfSols,LocalState,State), | |
| 65 | (add_internal_error('System Error while processing Kodkod request: ',E), | |
| 66 | fail | |
| 67 | )). | |
| 68 | ||
| 69 | ||
| 70 | ||
| 71 | apply_kodkod(Identifier,Predicate,NewPredicate) :- | |
| 72 | get_preference(try_kodkod_on_load,true), | |
| 73 | replace_by_kodkod(Identifier,Predicate,NewPredicate),!. | |
| 74 | apply_kodkod(_Identifier,Predicate,Predicate). | |
| 75 | ||
| 76 | create_id(Id,Type,b(identifier(Id),Type,[])). | |
| 77 | ||
| 78 | % a version which takes ids and types list: | |
| 79 | apply_kodkod(Ids,Types,Predicate,NewPredicate) :- | |
| 80 | get_preference(try_kodkod_on_load,true), | |
| 81 | maplist(create_id,Ids,Types,Identifiers), | |
| 82 | replace_by_kodkod(Identifiers,Predicate,NewPredicate),!. | |
| 83 | apply_kodkod(_Identifier,_Types,Predicate,Predicate). | |
| 84 | ||
| 85 | % | |
| 86 | :- use_module(probsrc(b_expression_sharing),[expand_cse_lazy_lets_if_cse_enabled/2]). | |
| 87 | replace_by_kodkod(Constants,Predicate,NewPredicate) :- | |
| 88 | % Remove any CSE lazy_lets as Kodkod translation cannot deal with them yet | |
| 89 | expand_cse_lazy_lets_if_cse_enabled(Predicate,Predicate0), | |
| 90 | % The Predicate may already contain Kodkod calls, replace | |
| 91 | % them by their original B predicate | |
| 92 | undo_kodkod_replacements(Predicate0,Predicate1), | |
| 93 | % first we do a predicate analysis to determine ranges for integers | |
| 94 | try_predicate_analysis_with_global_sets(Predicate1,Constants,TaggedConstants,TaggedPredicate), | |
| 95 | replace_by_kodkod2(TaggedConstants,TaggedPredicate,NewPredicate). | |
| 96 | ||
| 97 | :- use_module(probsrc(preferences),[temporary_set_preference/3,reset_temporary_preference/2]). | |
| 98 | replace_by_kodkod2(Constants,_Predicate,NewPredicate) :- | |
| 99 | % If the static analysis states that there is no possible solution for one | |
| 100 | % of the identifiers, we just say "false" | |
| 101 | somechk(is_inconsistent_expression,Constants),!, | |
| 102 | write('kodkod: Static analysis detected inconsistencies, new predicate is "false"'),nl, | |
| 103 | create_texpr(falsity,pred,[],NewPredicate). | |
| 104 | replace_by_kodkod2(Constants,Predicate,NewPredicate) :- | |
| 105 | temporary_set_preference(partition_predicates_inline_equalities,false,CHNG), | |
| 106 | split_predicates(Predicate,PList), % will split into components if KODKOD_ONLY_FULL = FALSE | |
| 107 | reset_temporary_preference(partition_predicates_inline_equalities,CHNG), | |
| 108 | % we try to translate each predicate alone | |
| 109 | try_apply_transformation_l(PList,Constants,1,Result), | |
| 110 | print_results(Result), | |
| 111 | % split the result into two lists: the successfull translatable predicates (ToKodkod) | |
| 112 | % and those which were not translatable (StayProb) | |
| 113 | filter_translatable(Result,ToKodkod,StayProb), | |
| 114 | %%print('Stay ProB: '), conjunct_predicates(StayProb,StayPred), translate:print_bexpr(StayPred),nl, | |
| 115 | % fail if there are no translatable predicates | |
| 116 | ToKodkod = [_|_], | |
| 117 | % now, translate all translatable predicates in one run | |
| 118 | apply_transformation(Constants,ToKodkod,KPred), | |
| 119 | % the new | |
| 120 | %%print('For Kodkod: '), translate:print_bexpr(KPred),nl, | |
| 121 | conjunct_predicates([KPred|StayProb],NewPredicate). | |
| 122 | ||
| 123 | apply_kodkod_to_counterexample_search(Variables,Assumption,Assertion,KPred,Rest) :- | |
| 124 | get_preference(try_kodkod_on_load,true), | |
| 125 | % The predicates may already contain Kodkod calls, replace | |
| 126 | % them by their original B predicate | |
| 127 | undo_kodkod_replacements(Assumption,Assumption1), | |
| 128 | undo_kodkod_replacements(Assertion,Assertion1), | |
| 129 | % first we do a predicate analysis to determine ranges for integers | |
| 130 | analysis_for_counterexample(Variables,Assumption1,Assertion1, | |
| 131 | TaggedVariables,TaggedAssumption,TaggedAssertions), | |
| 132 | ||
| 133 | % analyse assumptions | |
| 134 | split_assumptions(TaggedAssumption,TaggedVariables, | |
| 135 | TAssumptions,NTAssumptions,AssumptionsComponents), | |
| 136 | ||
| 137 | % analyse assertions | |
| 138 | translate_assertions(TaggedAssertions,TaggedVariables,TAssumptions,NTAssumptions, | |
| 139 | UsedAssumptionNumbers,TAssertions,NTAssertions,UsedVariables), | |
| 140 | ||
| 141 | % if we do not find a translatalbe assertion, fail and do not apply Kodkod at all | |
| 142 | TAssertions = [_|_], | |
| 143 | ||
| 144 | findall( UP, | |
| 145 | (member(N,UsedAssumptionNumbers),nth1(N,AssumptionsComponents,component(UP,_))), | |
| 146 | UsedAssumptions), | |
| 147 | findall( UP, | |
| 148 | (nth1(N,AssumptionsComponents,component(UP,_)),nonmember(N,UsedAssumptionNumbers)), | |
| 149 | UnusedAssumptions), | |
| 150 | ||
| 151 | conjunct_predicates(TAssertions,TAssertion), | |
| 152 | create_texpr(negation(TAssertion),pred,[],Negation), | |
| 153 | append(UsedAssumptions,[Negation],ToTranslate), | |
| 154 | apply_transformation(UsedVariables,ToTranslate,KPred), | |
| 155 | ||
| 156 | ( NTAssertions = [] -> | |
| 157 | conjunct_predicates(UnusedAssumptions,Rest) | |
| 158 | ; otherwise -> | |
| 159 | conjunct_predicates(NTAssertions,RestAssertion), | |
| 160 | create_texpr(negate(RestAssertion),pred,[],RestNegated), | |
| 161 | conjunct_predicates([Assumption,RestNegated],Rest)). | |
| 162 | ||
| 163 | split_assumptions(Assumption,Variables,Translatable,NotTranslated,AssumptionsComponents) :- | |
| 164 | predicate_components(Assumption,AssumptionsComponents), | |
| 165 | try_apply_transformation_to_components(AssumptionsComponents,Variables,1,AssumptionResults), | |
| 166 | map_ids_to_assumption(AssumptionResults,Translatable,NotTranslated). | |
| 167 | ||
| 168 | translate_assertions(Assertion,Variables,TAssumptions,NTAssumptions,UsedAssumptions, | |
| 169 | Translatable,NotTranslated,UsedVariables) :- | |
| 170 | conjunction_to_list(Assertion,Assertions), | |
| 171 | translate_assertions2(Assertions,Variables,TAssumptions,NTAssumptions,Unsorted, | |
| 172 | Translatable,NotTranslated,UIds), | |
| 173 | sort(Unsorted,UsedAssumptions), | |
| 174 | sort(UIds,Ids), | |
| 175 | findall(V,(member(V,Variables),get_texpr_id(V,I),memberchk(I,Ids)),UsedVariables). | |
| 176 | translate_assertions2([],_Variables,_TAssumptions,_NTAssumptions,[],[],[],[]). | |
| 177 | translate_assertions2([Assertion|Arest],Variables,TAssumptions,NTAssumptions, | |
| 178 | UsedAssumptions,Translatable,NotTranslated,Ids) :- | |
| 179 | ( translate_assertion(Assertion,Variables,TAssumptions,NTAssumptions,LUsedAssumptions,LUsedIds) -> | |
| 180 | append(LUsedAssumptions,Urest,UsedAssumptions), | |
| 181 | append(LUsedIds,Irest,Ids), | |
| 182 | Translatable = [Assertion|Trest], NotTranslated = NTrest | |
| 183 | ; otherwise -> | |
| 184 | UsedAssumptions = Urest, | |
| 185 | Ids = Irest, | |
| 186 | Translatable = Trest, NotTranslated = [Assertion|NTrest]), | |
| 187 | translate_assertions2(Arest,Variables,TAssumptions,NTAssumptions,Urest,Trest,NTrest,Irest). | |
| 188 | translate_assertion(Assertion,Variables,TAssumptions,NTAssumptions,UsedAssumptions,Ids) :- | |
| 189 | find_identifier_uses(Assertion,[],Ids), | |
| 190 | find_used_predicates(Ids,TAssumptions,NTAssumptions,UsedAssumptions), | |
| 191 | try_apply_transformation(Assertion,Variables,1,R), | |
| 192 | functor(R,ok,_). | |
| 193 | find_used_predicates(Ids,TAssumptions,NTAssumptions,UsedAssumptions) :- | |
| 194 | maplist(find_predicate(TAssumptions,NTAssumptions),Ids,AssumptionsL), | |
| 195 | append(AssumptionsL,Assumptions), | |
| 196 | sort(Assumptions,UsedAssumptions). | |
| 197 | ||
| 198 | find_predicate(_TAssumptions,NTAssumptions,Id,_UsedAssumption) :- | |
| 199 | % if the assertion uses an ID that is also used by a non-translatable | |
| 200 | % assumption, we do not translate the assumption | |
| 201 | avl_fetch(Id,NTAssumptions),!,fail. | |
| 202 | find_predicate(TAssumptions,_NTAssumptions,Id,UsedAssumptions) :- | |
| 203 | ( avl_fetch(Id,TAssumptions,UsedAssumption) -> | |
| 204 | UsedAssumptions = [UsedAssumption] | |
| 205 | ; otherwise -> | |
| 206 | UsedAssumptions = []). | |
| 207 | ||
| 208 | map_ids_to_assumption(AssumptionResults,AssumptionIds,NotTranslated) :- | |
| 209 | findall( Id-N, | |
| 210 | ( nth1(N,AssumptionResults,ok(Ids,_,_,_)), | |
| 211 | member(Id,Ids)), | |
| 212 | Ids1), | |
| 213 | list_to_avl(Ids1,AssumptionIds), | |
| 214 | findall( N, | |
| 215 | ( nth1(N,AssumptionResults,failure(Ids,_,_,_,_)), | |
| 216 | member(Id,Ids)), | |
| 217 | Ids2), | |
| 218 | list_to_avl(Ids2,NotTranslated). | |
| 219 | ||
| 220 | analysis_for_counterexample(Variables,Assumption,Assertion, | |
| 221 | TaggedVariables,TaggedAssumption,TaggedAssertion) :- | |
| 222 | create_texpr(negation(Assertion),pred,[],NAssertion), | |
| 223 | create_texpr(conjunct(Assumption,NAssertion),pred,[],Conj), | |
| 224 | try_predicate_analysis_with_global_sets(Conj,Variables,TaggedVariables,TaggedConj), | |
| 225 | create_texpr(conjunct(TaggedAssumption,TaggedNAssertion),pred,_,TaggedConj), | |
| 226 | create_texpr(negation(TaggedAssertion),pred,_,TaggedNAssertion). | |
| 227 | ||
| 228 | split_predicates(Predicate,Parts) :- | |
| 229 | get_preference(kodkod_for_components,true),!, | |
| 230 | predicate_components(Predicate,Components), | |
| 231 | findall(P,member(component(P,_),Components),Parts). | |
| 232 | split_predicates(Predicate,Parts) :- | |
| 233 | conjunction_to_list(Predicate,Parts). | |
| 234 | ||
| 235 | split_simple_equalities(InPredicate,Equalities,Rest) :- | |
| 236 | conjunction_to_list(InPredicate,InPredicates), | |
| 237 | split_list(is_simple_equality,InPredicates,EqualitiesL,RestL), | |
| 238 | conjunct_predicates(EqualitiesL,Equalities), | |
| 239 | conjunct_predicates(RestL,Rest). | |
| 240 | ||
| 241 | is_simple_equality(TExpr) :- | |
| 242 | get_texpr_expr(TExpr,equal(A,B)), | |
| 243 | ( get_texpr_id(A,_),is_base_expression(B) | |
| 244 | ; get_texpr_id(B,_),is_base_expression(A)),!. | |
| 245 | ||
| 246 | is_base_expression(TExpr) :- | |
| 247 | get_texpr_expr(TExpr,Expr), | |
| 248 | is_base_expression2(Expr). | |
| 249 | is_base_expression2(identifier(Id)) :- b_global_set(Id),!. % a deferred set | |
| 250 | is_base_expression2(identifier(Id)) :- lookup_global_constant(Id,_). % an enumerated set element | |
| 251 | is_base_expression2(integer(_)). | |
| 252 | is_base_expression2(couple(A,B)) :- is_base_expression(A),is_base_expression(B). | |
| 253 | is_base_expression2(set_extension(L)) :- maplist(is_base_expression,L). | |
| 254 | is_base_expression2(value(_)). | |
| 255 | is_base_expression2(boolean_true). | |
| 256 | is_base_expression2(boolean_false). | |
| 257 | is_base_expression2(empty_set). | |
| 258 | is_base_expression2(bool_set). | |
| 259 | is_base_expression2(add(A,B)) :- is_base_expression(A),is_base_expression(B). | |
| 260 | is_base_expression2(minus(A,B)) :- is_base_expression(A),is_base_expression(B). | |
| 261 | is_base_expression2(unary_minus(A)) :- is_base_expression(A). | |
| 262 | is_base_expression2(multiplication(A,B)) :- is_base_expression(A),is_base_expression(B). | |
| 263 | is_base_expression2(div(A,B)) :- is_base_expression(A),is_base_expression(B). | |
| 264 | is_base_expression2(floored_div(A,B)) :- is_base_expression(A),is_base_expression(B). | |
| 265 | is_base_expression2(modulo(A,B)) :- is_base_expression(A),is_base_expression(B). | |
| 266 | is_base_expression2(power_of(A,B)) :- is_base_expression(A),is_base_expression(B). | |
| 267 | ||
| 268 | ||
| 269 | undo_kodkod_replacements(Old,New) :- | |
| 270 | contains_kodkod_call(Old),!, | |
| 271 | undo_kodkod_replacements2(Old,New). | |
| 272 | undo_kodkod_replacements(Old,Old). | |
| 273 | undo_kodkod_replacements2(TOld,TNew) :- | |
| 274 | get_texpr_expr(TOld,Old), | |
| 275 | undo_kodkod_replacements3(Old,TOld,TNew). | |
| 276 | undo_kodkod_replacements3(conjunct(A,B),_TOld,TNew) :- | |
| 277 | !,create_texpr(conjunct(NewA,NewB),pred,[],TNew), | |
| 278 | undo_kodkod_replacements2(A,NewA), | |
| 279 | undo_kodkod_replacements2(B,NewB). | |
| 280 | undo_kodkod_replacements3(kodkod(Id,_),_TOld,Orig) :- | |
| 281 | !,get_original_problem(Id,Orig). | |
| 282 | undo_kodkod_replacements3(_Old,TOld,TOld). | |
| 283 | ||
| 284 | contains_kodkod_call(TExpr) :- | |
| 285 | get_texpr_expr(TExpr,Expr), | |
| 286 | contains_kodkod_call2(Expr),!. | |
| 287 | contains_kodkod_call2(kodkod(_,_)). | |
| 288 | contains_kodkod_call2(conjunct(A,_)) :- contains_kodkod_call(A). | |
| 289 | contains_kodkod_call2(conjunct(_,B)) :- contains_kodkod_call(B). | |
| 290 | ||
| 291 | ||
| 292 | try_predicate_analysis_with_global_sets(Predicate,Constants,TaggedConstants,TaggedPredicate) :- | |
| 293 | catch(predicate_analysis_with_global_sets(Predicate,[],Constants,TaggedConstants,TaggedPredicate), | |
| 294 | failed_analysis(Expr), | |
| 295 | ( write('kodkod fail: predicate analysis failed on expression '), | |
| 296 | translate_bexpression_with_limit(Expr,80,Msg), | |
| 297 | write(Msg),nl,fail)), | |
| 298 | !. | |
| 299 | try_predicate_analysis_with_global_sets(_Predicate,_Constants,_TaggedConstants,_TaggedPredicate) :- | |
| 300 | write('kodkod fail: predicate analysis failed.\n'), | |
| 301 | fail. | |
| 302 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 303 | ||
| 304 | :- meta_predicate try_call(-,-,0). | |
| 305 | ||
| 306 | try_apply_transformation(Predicate,Constants,Index,Result) :- | |
| 307 | %%print('TRY KODKOD ON: '), translate:print_bexpr(Predicate),nl, | |
| 308 | Log = log(Predicate,Result,Index,Ints,Bits), | |
| 309 | try_call( 'applying rewriting rules', Log, | |
| 310 | apply_rewriting_rules(Predicate,Rewritten)), | |
| 311 | %%print('REWRITTEN: '), translate:print_bexpr(Rewritten),nl, | |
| 312 | try_call( 'extracting used types', Log, | |
| 313 | extract_used_types(Rewritten,Types,Ints,Bits)), | |
| 314 | try_call( 'creating Kodkod atoms for types', Log, | |
| 315 | create_atoms_for_types(Types,Ints,Bits,Typemap,Idmap1,_Valuemap)), | |
| 316 | try_call( 'translate and type Kodkod formula', Log, | |
| 317 | typed_translation(Constants,Predicate,Bits,Typemap,Idmap1,_Idmap,Rewritten,_KExpr)), | |
| 318 | finalize_result(Log). | |
| 319 | try_call(_Msg,log(_Predicate,Result,_Index,_,_),_Call) :- | |
| 320 | nonvar(Result),!. | |
| 321 | try_call(Msg,log(Predicate,Result,Index,_,_),Call) :- | |
| 322 | %%format('Try ~w ~n',[Msg]), | |
| 323 | ( catch(Call, | |
| 324 | kodkod(T), | |
| 325 | ( %%format('Exception: ~w~n',[T]), | |
| 326 | Result = failure(Index,Predicate,Msg,kodkod_exception(T))) | |
| 327 | ) -> true | |
| 328 | ; otherwise -> | |
| 329 | %%format('Failure for: ~w~n',[Msg]), | |
| 330 | Result = failure(Index,Predicate,Msg,failed) | |
| 331 | ). | |
| 332 | finalize_result(log(Predicate,Result,Index,Ints,Bits)) :- | |
| 333 | var(Result),!,Result=ok(Index,Predicate,Ints,Bits). | |
| 334 | finalize_result(_). | |
| 335 | ||
| 336 | ||
| 337 | typed_translation(Constants,Predicate,Bits,Typemap,Idmap1,Idmap,Rewritten,KExpr) :- | |
| 338 | % Create the relations for the constants that are actually used | |
| 339 | restrict_to_used_constants(Constants,Predicate,UsedConstants), | |
| 340 | create_identifier_relations(UsedConstants,Typemap,Bits,Idmap1,Idmap), | |
| 341 | % translate the formula in two steps: | |
| 342 | kodkod_translate(Rewritten,Typemap,Idmap,Formula), | |
| 343 | kodkod_insert_casts(Formula,Typemap,Idmap,KExpr), | |
| 344 | !. | |
| 345 | ||
| 346 | restrict_to_used_constants(Constants,Predicate,UsedConstants) :- | |
| 347 | find_identifier_uses(Predicate,['$examine_value_was_identifier_info'],UsedIds), % flag says: also get value(_) with was_identifier(_) field | |
| 348 | include(constant_is_used(UsedIds),Constants,UsedConstants). | |
| 349 | constant_is_used(UsedIds,C) :- | |
| 350 | get_texpr_id(C,Id),memberchk(Id,UsedIds). | |
| 351 | ||
| 352 | try_apply_transformation_l([],_Constants,_,[]). | |
| 353 | try_apply_transformation_l([Predicate|Prest],Constants,I,[Result|Rrest]) :- | |
| 354 | try_apply_transformation(Predicate,Constants,I,Result), | |
| 355 | I2 is I+1, | |
| 356 | try_apply_transformation_l(Prest,Constants,I2,Rrest). | |
| 357 | ||
| 358 | try_apply_transformation_to_components([],_Vars,_,[]). | |
| 359 | try_apply_transformation_to_components([component(Predicate,Ids)|Crest],Vars,I,[Result|Rrest]) :- | |
| 360 | try_apply_transformation(Predicate,Vars,I,Result1), | |
| 361 | Result1 =.. [Functor|Args], | |
| 362 | Result =.. [Functor,Ids|Args], | |
| 363 | I2 is I+1, | |
| 364 | try_apply_transformation_to_components(Crest,Vars,I2,Rrest). | |
| 365 | ||
| 366 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 367 | ||
| 368 | filter_translatable([],[],[]). | |
| 369 | filter_translatable([Res|Rrest],ToKodkod,StayProb) :- | |
| 370 | ( Res = ok(_,P,_,_) -> ToKodkod=[P|Krest], StayProb=Prest | |
| 371 | ; Res = failure(_,P,_,_) -> ToKodkod=Krest, StayProb=[P|Prest]), | |
| 372 | filter_translatable(Rrest,Krest,Prest). | |
| 373 | ||
| 374 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 375 | :- use_module(probsrc(error_manager),[add_warning/3,add_warning/4]). | |
| 376 | :- use_module(probsrc(debug),[debug_mode/1,silent_mode/1,nls/0]). | |
| 377 | ||
| 378 | apply_transformation(AllConstants,PredicateList,Result) :- | |
| 379 | conjunct_predicates(PredicateList,Predicate1), | |
| 380 | (debug_mode(on) -> print('TRANSLATING FOR KODKOD: '),nl,translate:print_bexpr(Predicate1),nl ; true), | |
| 381 | apply_transformation2(AllConstants,Predicate1,Result). | |
| 382 | ||
| 383 | apply_transformation2(AllConstants,Predicate1,Result) :- | |
| 384 | split_simple_equalities(Predicate1,Equalities,Predicate), | |
| 385 | (debug_mode(on) -> print('Equalities: '), translate:print_bexpr(Equalities),nl ; true), | |
| 386 | (is_truth(Predicate) -> debug:debug_println('Only equalities'),fail | |
| 387 | ; apply_transformation3(AllConstants,Predicate,Equalities,Result) | |
| 388 | -> (debug_mode(on) -> print('RESULT: '),nl,translate:print_bexpr(Result),nl ; true) | |
| 389 | ; add_warning(kodkod,'Kodkod Transformation Failed: ',AllConstants), | |
| 390 | %trace, apply_transformation3(AllConstants,Predicate,Equalities,Result), | |
| 391 | fail). | |
| 392 | ||
| 393 | apply_transformation3(AllConstants,Predicate,Equalities,Result) :- | |
| 394 | restrict_to_used_constants(AllConstants,Predicate,Constants), | |
| 395 | apply_rewriting_rules(Predicate,Rewritten), | |
| 396 | extract_used_types(Rewritten,Types,Ints,Bits), | |
| 397 | create_atoms_for_types(Types,Ints,Bits,Typemap,Idmap1,Valuemap), | |
| 398 | % check if any types are used, if not Kodkod would exit with an | |
| 399 | % empty universe exception (or something similar) | |
| 400 | \+ empty_avl(Typemap), | |
| 401 | typed_translation(Constants,Predicate,Bits,Typemap,Idmap1,Idmap,Rewritten,KExpr), | |
| 402 | ||
| 403 | register_problem(Constants,KExpr,Idmap,Typemap,Valuemap,Predicate,ProblemNr), | |
| 404 | create_texpr(kodkod(ProblemNr,Constants),pred,[],KPred), | |
| 405 | conjunct_predicates([Equalities,KPred],Result). | |
| 406 | ||
| 407 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 408 | ||
| 409 | print_results([]). | |
| 410 | print_results([R|Rrest]) :- | |
| 411 | print_result(R),nls, | |
| 412 | print_results(Rrest). | |
| 413 | print_result(ok(_Ids,Index,P,Ints,Bits)) :- | |
| 414 | print_result(ok(Index,P,Ints,Bits)). | |
| 415 | print_result(ok(_Index,P,Ints,Bits)) :- | |
| 416 | (silent_mode(on) -> true | |
| 417 | ; write('kodkod ok: '),print_bexpr_with_limit(P,50), | |
| 418 | write(' ints: '),write(Ints),write(', intatoms: '),write(Bits) | |
| 419 | ). | |
| 420 | print_result(failure(_Ids,Index,P,Msg,Reason)) :- | |
| 421 | print_result(failure(Index,P,Msg,Reason)). | |
| 422 | print_result(failure(_Index,P,Msg,Reason)) :- | |
| 423 | write('kodkod fail: '), | |
| 424 | translate_bexpression_with_limit(P,50,PS), write(PS), | |
| 425 | write(' , reason: '),write_reason(Reason),write(' while '),write(Msg), | |
| 426 | (get_preference(kodkod_raise_warnings,true) | |
| 427 | -> add_warning(kodkod,'Cannot translate predicate for Kodkod: ',PS,P) | |
| 428 | ; true). | |
| 429 | write_reason(kodkod_exception(KE)) :- | |
| 430 | write_reason2(KE),!. | |
| 431 | write_reason(E) :- write(E). | |
| 432 | ||
| 433 | write_reason2(unsupported_type(T)) :- | |
| 434 | pretty_type(T,PT), | |
| 435 | write('unsupported type '),write(PT). | |
| 436 | write_reason2(unsupported_expression(TE)) :- | |
| 437 | get_texpr_expr(TE,T), | |
| 438 | functor(T,Functor,Arity), | |
| 439 | translate_bexpression(TE,PE), | |
| 440 | format('unsupported expression ~w/~w: ~w',[Functor,Arity,PE]). | |
| 441 | write_reason2(unsupported_int(Msg)) :- | |
| 442 | write(Msg). | |
| 443 | write_reason2(side_condition(Msg,PPExpr)) :- | |
| 444 | format('~w: ~w',[Msg,PPExpr]). | |
| 445 | ||
| 446 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 447 | ||
| 448 | :- public pdebug/0. | |
| 449 | pdebug :- | |
| 450 | install_b_portray_hook, | |
| 451 | assert(( user:portray(X) :- is_avl(X),!,portray_avl(X) )). |