1 | | % (c) 2009-2015 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(cbc_refinement_checks, [cbc_refinement_check/2]). |
6 | | |
7 | | :- use_module(module_information,[module_info/2]). |
8 | | :- module_info(group,cbc). |
9 | | :- module_info(description,'This module provides constraint-based checking of B and Event-B refinements.'). |
10 | | |
11 | | :- use_module(library(lists)). |
12 | | :- use_module(library(sets), [subtract/3]). |
13 | | |
14 | | :- use_module(solver_interface, [solve_predicate/3]). |
15 | | |
16 | | :- use_module(specfile, [animation_minor_mode/1]). |
17 | | :- use_module(bmachine, [full_b_machine/1, |
18 | | b_get_refined_machine/1, |
19 | | b_get_machine_operation/6, |
20 | | b_get_invariant_from_machine/1, |
21 | | b_get_linking_invariant_from_machine/1, |
22 | | b_get_properties_from_machine/1, |
23 | | b_get_machine_variables/1, |
24 | | b_get_machine_constants/1, |
25 | | b_machine_name/1]). |
26 | | |
27 | | :- use_module(translate, [nested_print_bexpr/1]). |
28 | | :- use_module(bsyntaxtree, [get_texpr_expr/2,get_texpr_info/2, |
29 | | get_texpr_id/2, |
30 | | get_rodin_name/2, |
31 | | conjunct_predicates/2, |
32 | | conjunction_to_list/2, |
33 | | create_texpr/4, safe_create_texpr/3, |
34 | | rename_bt/3]). |
35 | | :- use_module(b_interpreter_components, [construct_optimized_exists/3]). |
36 | | :- use_module(bmachine_structure, [get_section/3]). |
37 | | :- use_module(bmachine_eventb, [prime_variables/2]). |
38 | | :- use_module(bsyntaxtree, [create_negation/2]). |
39 | | :- use_module(weakest_preconditions, [weakest_precondition/3, |
40 | | set_reference_machine/1, |
41 | | delete_reference_machine/0]). |
42 | | :- use_module(before_after_predicates, [before_after_predicate_with_equalities/3, |
43 | | before_after_predicate_list_conjunct_with_equalities/3, |
44 | | list_renamings_to_primed_vars/2]). |
45 | | :- use_module(preferences,[get_preference/2]). |
46 | | :- use_module(tools_strings, [ajoin/2]). |
47 | | |
48 | | cbc_refinement_check(List,ViolationFound) :- |
49 | | (animation_minor_mode(eventb) |
50 | | -> eventb_refinement_check(List,ViolationFound) |
51 | | ; classical_refinement_check(List,ViolationFound)). |
52 | | |
53 | | % ------------------------------------------- |
54 | | % eventb po generation |
55 | | % ------------------------------------------- |
56 | | |
57 | | eventb_refinement_check(ResultList,ViolationFound) :- |
58 | | % fetch Axioms and Invariant/properties first |
59 | | full_b_machine(Machine), |
60 | | (get_section(axioms,Machine,Axioms) -> true ; Axioms = []), |
61 | | b_get_invariant_from_machine(Invariant), |
62 | | b_get_properties_from_machine(Properties), |
63 | | % evt/p/WFIS |
64 | | witness_feasibility(Axioms,Invariant,Properties,ListWF,V1), |
65 | | % evt/grd/GRD proof obligations |
66 | | guard_strengthening(Axioms,Invariant,Properties,ListGS,V2), |
67 | | % evt/act/SIM |
68 | | action_simulation(Axioms,Invariant,Properties,ListAS,V3), |
69 | | append([ListWF,['\n'],ListGS,['\n'],ListAS],ResultList), |
70 | | merge_violation_found([V1,V2,V3],ViolationFound). |
71 | | |
72 | | witness_feasibility(Axioms,Invariant,Properties,['Witness Feasibility:'|FlatResults],ViolationFound) :- |
73 | | % action simulation: |
74 | | % A & I & J & H & W & Tau => Q_i |
75 | | % find all candidates for evt/act/SIM proof obligations |
76 | | findall(RLEVENT, |
77 | | (b_get_machine_operation(_Name,_R,_P,Body,_OType,_OpPos), |
78 | | get_texpr_expr(Body,RLEVENT)), |
79 | | ListOfOperations), |
80 | | maplist(witness_feasibility_aux(Axioms,Invariant,Properties),ListOfOperations,Results,SubViolationFound), |
81 | | append(Results,FlatResults), |
82 | | merge_violation_found(SubViolationFound,ViolationFound). |
83 | | |
84 | | witness_feasibility_aux(Axioms,Invariant,Properties, |
85 | | rlevent(Name,_Section,_Stat,Parameters,Guards,_Thm,_Actions,_VWit,PWit,_Unmod,AbsEvents), |
86 | | ResultsParameters,ViolationFound) :- |
87 | | % feasibility for parameters - the abstract events have a parameter |
88 | | % that is not a parameter of the concrete events |
89 | | all_abstract_parameters(AbsEvents,AllAbsParameters), |
90 | | subtract(AllAbsParameters,Parameters,ParametersForWfisPos), |
91 | | |
92 | | conjunct_predicates([Invariant,Properties,Guards|Axioms],LHSPred), |
93 | | |
94 | | % map over all abstract events |
95 | | maplist(witness_feasibility_parameters(Name,LHSPred,PWit),ParametersForWfisPos,ResultsParameters,SubViolationFound), |
96 | | merge_violation_found(SubViolationFound,ViolationFound). |
97 | | |
98 | | witness_feasibility_parameters(Name,LHSPred,PWit,Parameter,Result,ViolationFound) :- |
99 | | % find matching witness - same identifier |
100 | | get_texpr_id(Parameter,Identifier), |
101 | | member(Witness,PWit), get_texpr_expr(Witness,witness(WitnessIdentifier,Pred)), |
102 | | get_texpr_id(WitnessIdentifier,Identifier), !, |
103 | | |
104 | | % set up PO: A & I & J & H => exists p : W_p |
105 | | construct_optimized_exists([Parameter],Pred,ExistsPred), |
106 | | create_negation(ExistsPred,NegatedExistsPred), |
107 | | conjunct_predicates([LHSPred,NegatedExistsPred],CounterExamplePred), |
108 | | |
109 | | solve_predicate(CounterExamplePred,State,Res), |
110 | | assign_violation_found(Res,ViolationFound), |
111 | | |
112 | | % result string |
113 | | ajoin([Name,'/',Identifier,'/WFIS: ','Counter-Example found: ', Res],Result), |
114 | | % print |
115 | | write(Result), nl, nested_print_bexpr(Pred), |
116 | | write(State),nl. |
117 | | |
118 | | action_simulation(Axioms,Invariant,Properties,['Action Simulation:'|ResultsFlat],ViolationFound) :- |
119 | | % action simulation: |
120 | | % A & I & J & H & W & Tau => Q_i |
121 | | % find all candidates for evt/act/SIM proof obligations |
122 | | findall(RLEVENT, |
123 | | (b_get_machine_operation(_Name,_R,_P,Body,_OType,_), |
124 | | get_texpr_expr(Body,RLEVENT)), |
125 | | ListOfOperations), |
126 | | maplist(action_simulation(Axioms,Invariant,Properties),ListOfOperations,Results,SubViolationFound), |
127 | | merge_violation_found(SubViolationFound,ViolationFound), |
128 | | append(Results,ResultsFlat). |
129 | | |
130 | | action_simulation(Axioms,Invariant,Properties, |
131 | | rlevent(Name,_Section,_Stat,_Parameters,Guards,_Thm,Actions,VWit,PWit,_Unmod,AbsEvents), |
132 | | ResultsFlat,ViolationFound) :- |
133 | | % concrete before-after-predicate |
134 | | b_get_machine_variables(Vars), |
135 | | b_get_machine_constants(Consts), |
136 | | append(Vars,Consts,Both), |
137 | | before_after_predicate_list_conjunct_with_equalities(Actions,Both,Tau), |
138 | | maplist(extract_witness_predicate,VWit,VWitPreds), |
139 | | maplist(extract_witness_predicate,PWit,PWitPreds), |
140 | | append([Axioms,[Invariant,Properties,Guards,Tau],VWitPreds,PWitPreds],LHSPreds), |
141 | | conjunct_predicates(LHSPreds,LHS), |
142 | | |
143 | | % map over all abstract events |
144 | | maplist(action_simulation2(Name,LHS),AbsEvents,Results,SubViolationFound), |
145 | | merge_violation_found(SubViolationFound,ViolationFound), |
146 | | append(Results,ResultsFlat). |
147 | | |
148 | | action_simulation2(Name,LHS,AbsEvent,Result,ViolationFound) :- |
149 | | get_texpr_expr(AbsEvent,rlevent(_AbsName,_Section,_Stat,_AbsParameters,_Guards,_Thm,Actions,_VWit,_PWit,_Unmod,_AbsEvents)), |
150 | | % map over all abstract actions |
151 | | maplist(action_simulation3(Name,LHS),Actions,Result,SubViolationFound), |
152 | | merge_violation_found(SubViolationFound,ViolationFound). |
153 | | |
154 | | action_simulation3(Name,LHS,Action,Result,ViolationFound) :- |
155 | | modifies_concrete_var(Action), !, |
156 | | get_rodin_name(Action,ActionName), |
157 | | |
158 | | % before after predicate of abstract action, negate, solve |
159 | | % trace, |
160 | | b_get_machine_variables(AllVars), |
161 | | exclude(is_concrete_var,AllVars,AbstractVars), |
162 | | before_after_predicate_with_equalities(Action,AbstractVars,BAPred), |
163 | | create_negation(BAPred,NegatedBAPred), |
164 | | conjunct_predicates([NegatedBAPred,LHS],Pred), |
165 | | |
166 | | solve_predicate(Pred,State,Res), |
167 | | assign_violation_found(Res,ViolationFound), |
168 | | |
169 | | % result string |
170 | | ajoin([Name,'/',ActionName,'/SIM: ','Counter-Example found: ', Res],Result), |
171 | | % print |
172 | | write(Result), nl, translate:nested_print_bexpr(Pred), |
173 | | write(State),nl. |
174 | | |
175 | | % abstract action does not modify a concrete variable -> no PO |
176 | | action_simulation3(_Name,_LHS,_Action,[],false). |
177 | | |
178 | | guard_strengthening(Axioms,Invariant,Properties,['Guard Strengthening:'|ResultsFlat],ViolationFound) :- |
179 | | % guard strengthening: |
180 | | % A & I & J & H & W => G_i |
181 | | % guard strengthening (merge): |
182 | | % A & I & J & H & W & Tau => G_1 or ... or G_n |
183 | | % find all candidates for evt/grd/GRD proof obligations |
184 | | findall(RLEVENT, |
185 | | (b_get_machine_operation(_Name,_R,_P,Body,_OType,_), |
186 | | get_texpr_expr(Body,RLEVENT)), |
187 | | ListOfOperations), |
188 | | maplist(guard_strengthening_aux(Axioms,Invariant,Properties),ListOfOperations,Results,SubViolationFound), |
189 | | append(Results,ResultsFlat), |
190 | | merge_violation_found(SubViolationFound,ViolationFound). |
191 | | |
192 | | % guard_strengthening: not a refinement |
193 | | guard_strengthening_aux(_Axioms,_Invariant,_Properties, |
194 | | rlevent(_Name,_Section,_Stat,_Parameters,_Guards,_Thm,_Actions,_VWit,_PWit,_Unmod,[]), |
195 | | [],false) :- !. % nothing to check |
196 | | |
197 | | % guard_strengthening: refining only one event |
198 | | guard_strengthening_aux(Axioms,Invariant,Properties, |
199 | | rlevent(Name,_Section,_Stat,_Parameters,Guards,_Thm,_Actions,VWit,PWit,_Unmod,[AbsEvent]), |
200 | | Results,ViolationFound) :- !, |
201 | | get_texpr_expr(AbsEvent,ABSRLEVENT), |
202 | | ABSRLEVENT = rlevent(_AbsName,_Absection,_AbsStat,_AbsParameters,AbsGrds,_AbsThm,_AbsAct,_AbsVWit,_AbsPWit,_AbsUnmod,_AbsEvents), |
203 | | conjunction_to_list(AbsGrds,AbsGrdsList), |
204 | | % map over all abstract guards |
205 | | maplist(guard_strengthening_single_event(Name,Axioms,Invariant,Properties,VWit,PWit,Guards),AbsGrdsList,Results,SubViolationFound), |
206 | | merge_violation_found(SubViolationFound,ViolationFound). |
207 | | |
208 | | % guard_strengthening: refining multiple events |
209 | | guard_strengthening_aux(Axioms,Invariant,Properties, |
210 | | rlevent(Name,_Section,_Stat,_Parameters,Guards,_Thm,Actions,VWit,PWit,_Unmod,AbsEvents), |
211 | | [Result],ViolationFound) :- |
212 | | % concrete before-after-predicate |
213 | | b_get_machine_variables(Vars), |
214 | | b_get_machine_constants(Consts), |
215 | | append(Vars,Consts,Both), |
216 | | before_after_predicate_list_conjunct_with_equalities(Actions,Both,Tau), |
217 | | % collect all abstract guards G_i and negate |
218 | | findall(AbsGrds, |
219 | | (member(Evt,AbsEvents), |
220 | | get_texpr_expr(Evt,rlevent(_AbsName,_AbsSection,_AbsStat,_AbsParams,AbsGrds,_AbsThm,_AbsAct,_AbsVWit,_AbsPWit,_AbsUnmod,_AbsAbsEvents))), |
221 | | ListOfAbstractGuards), |
222 | | maplist(create_negation,ListOfAbstractGuards,NegatedAbstractGuards), |
223 | | |
224 | | % build up predicate A & I & J & H & W & Tau => G_1 or ... or G_n |
225 | | maplist(extract_witness_predicate,VWit,VWitPreds), |
226 | | maplist(extract_witness_predicate,PWit,PWitPreds), |
227 | | |
228 | | append([Axioms,[Invariant,Properties,Guards,Tau],VWitPreds,PWitPreds,NegatedAbstractGuards],LHSPred), |
229 | | conjunct_predicates(LHSPred,Pred), |
230 | | solve_predicate(Pred,State,Res), |
231 | | |
232 | | assign_violation_found(Res,ViolationFound), |
233 | | |
234 | | % result string and print |
235 | | ajoin([Name,'/MRG: ','Counter-Example found: ', Res],Result), |
236 | | write(Result), nl, translate:nested_print_bexpr(Pred), |
237 | | write(State),nl. |
238 | | |
239 | | guard_strengthening_single_event(OpName,_Axioms,_Invariant,_Properties,_VWit,_PWit,_Guards,AbsGrd,Result,false) :- |
240 | | get_rodin_name(AbsGrd,GuardName), |
241 | | format('~nChecking single event guard strengthening for: ~w of ~w~n',[GuardName,OpName]), |
242 | | b_machine_name(MainMachineName), % we assume that we prove the guard strengthening for the main machine ! |
243 | | bmachine:discharged_guard_strengthening(MainMachineName,AbstractEvent,GuardName,OpName), |
244 | | format('Guard ~w of ~w is already proven for event ~w:~w !~n',[GuardName,AbstractEvent,MainMachineName,OpName]), |
245 | | preferences:get_preference(use_po,true), |
246 | | !, |
247 | | ajoin([OpName,'/',GuardName,'/GRD: ','already proven'],Result). |
248 | | guard_strengthening_single_event(OpName,Axioms,Invariant,Properties,VWit,PWit,Guards,AbsGrd,Result,ViolationFound) :- |
249 | | get_rodin_name(AbsGrd,GuardName), |
250 | | % build up predicate and check |
251 | | maplist(extract_witness_predicate,VWit,VWitPreds), |
252 | | maplist(extract_witness_predicate,PWit,PWitPreds), |
253 | | create_negation(AbsGrd,NegAbsGrd), |
254 | | |
255 | | append([Axioms,[Invariant,Properties,Guards,NegAbsGrd],VWitPreds,PWitPreds],Predicates), |
256 | | conjunct_predicates(Predicates,Pred), |
257 | | |
258 | | solve_predicate(Pred,State,Res), |
259 | | assign_violation_found(Res,ViolationFound), |
260 | | |
261 | | % result string and print |
262 | | ajoin([OpName,'/',GuardName,'/GRD: ','Counter-Example found: ', Res],Result), |
263 | | write(Result), nl, translate:nested_print_bexpr(Pred), |
264 | | write(State),nl. |
265 | | |
266 | | extract_witness_predicate(Witness,Pred) :- |
267 | | get_texpr_expr(Witness,witness(_Id,Pred)). |
268 | | |
269 | | modifies_concrete_var(Action) :- |
270 | | get_texpr_info(Action,Info), |
271 | | member(modifies(ListOfVars), Info), |
272 | | some(is_concrete_var,ListOfVars). |
273 | | |
274 | | is_concrete_var(b(identifier(Name),_,_)) :- !, |
275 | | is_concrete_var(Name). |
276 | | is_concrete_var(VarName) :- |
277 | | b_get_machine_variables(Variables), |
278 | | b_machine_name(TopLevelName), |
279 | | member(b(identifier(VarName),_Type,Infos),Variables), |
280 | | member(occurrences(Machines),Infos), |
281 | | member(TopLevelName,Machines). |
282 | | |
283 | | all_abstract_parameters([],[]). |
284 | | all_abstract_parameters([Event|FurtherEvents],ParametersOut) :- |
285 | | get_texpr_expr(Event,rlevent(_Name,_Section,_Stat,Parameters,_Guards,_Thm,_Actions,_VWit,_PWit,_Unmod,_AbsEvents)), |
286 | | all_abstract_parameters(FurtherEvents,FurtherParameters), append(Parameters,FurtherParameters,ParametersOut). |
287 | | |
288 | | % ------------------------------------------- |
289 | | % classical b po generation |
290 | | % ------------------------------------------- |
291 | | |
292 | | classical_refinement_check(ResultList,ViolationFound) :- |
293 | | % fetch Axioms and Invariant/properties first |
294 | | full_b_machine(Machine), |
295 | | b_get_refined_machine(AbsMachine) |
296 | | -> b_get_invariant_from_machine(Invariant), |
297 | | b_get_linking_invariant_from_machine(LinkingInvariant), |
298 | | % check initialisation po |
299 | | initialisation_pos(LinkingInvariant,Machine,AbsMachine,IniPos,V1), |
300 | | % check all operation pos |
301 | | get_all_operations_from_machine(Machine,ConcreteOperations), |
302 | | get_all_operations_from_machine(AbsMachine,AbstractOperations), |
303 | | operations_pos(ConcreteOperations,Invariant,LinkingInvariant,AbsMachine,AbstractOperations,ListOpPos,V2), |
304 | | append([[IniPos],['\n'],ListOpPos],ResultList), |
305 | | merge_violation_found([V1,V2],ViolationFound) |
306 | | ; ResultList = ['Not a Refinement Machine']. |
307 | | |
308 | | get_all_operations_from_machine(Machine,Operations) :- |
309 | | get_section(operation_bodies,Machine,Ops), |
310 | | findall(operation(Name,Results,Parameters,Body), |
311 | | (get_texpr_expr(Op,operation(TId,Results,Parameters,Body)), |
312 | | get_texpr_id(TId,op(Name)),member(Op,Ops)), |
313 | | Operations). |
314 | | |
315 | | initialisation_pos(LinkingInvariant,Machine,AbsMachine,Result,ViolationFound) :- |
316 | | % get the two initialisations |
317 | | get_section(initialisation,Machine,ConcreteInitialisation), |
318 | | get_section(initialisation,AbsMachine,AbstractInitialisation), |
319 | | |
320 | | % set up proof obligation [T1] not [T] not J (Schneider p.222) |
321 | | create_negation(LinkingInvariant,NegLinkingInvariant), |
322 | | |
323 | | set_reference_machine(AbsMachine), |
324 | | weakest_precondition(AbstractInitialisation,NegLinkingInvariant,TempPred), |
325 | | delete_reference_machine, |
326 | | |
327 | | create_negation(TempPred,NotTNotJ), |
328 | | weakest_precondition(ConcreteInitialisation,NotTNotJ,PO), |
329 | | create_negation(PO,CounterExPO), |
330 | | |
331 | | solve_predicate(CounterExPO,State,Res), |
332 | | assign_violation_found(Res,ViolationFound), |
333 | | |
334 | | % result string and print |
335 | | ajoin(['Initialisation [T1] not [T] not J: Counter-Example found: ', Res],Result), |
336 | | write(Result), nl, translate:nested_print_bexpr(CounterExPO), |
337 | | write(State),nl. |
338 | | |
339 | | operations_pos([],_I,_LI,_AM,_A,[],false). |
340 | | operations_pos([operation(Name,Results,_Parameters,_Body)|FurtherOps],Invariant,LinkingInvariant,AbsMachine,AbstractOperations,Results,ViolationFound) :- |
341 | | % there might be no abstract operation with the same name (includes, etc.) |
342 | | \+ (member(operation(Name,_AbsResults,_AbsParameters,_AbsBody),AbstractOperations)), !, |
343 | | operations_pos(FurtherOps,Invariant,LinkingInvariant,AbsMachine,AbstractOperations,Results,ViolationFound). |
344 | | operations_pos([operation(Name,Results,_Parameters,Body)|FurtherOps],Invariant,LinkingInvariant,AbsMachine,AbstractOperations,[PreRefPoResult,RefPoResult|ListOpPos],ViolationFound) :- |
345 | | % first find the matching abstract operation |
346 | | member(operation(Name,_AbsResults,_AbsParameters,AbsBody),AbstractOperations), |
347 | | |
348 | | % check if we have preconditions - otherwise we assume true |
349 | | (get_texpr_expr(Body,precondition(Precondition,RealBody)) -> true ; RealBody=Body, create_texpr(truth,pred,[],Precondition)), |
350 | | (get_texpr_expr(AbsBody,precondition(AbsPrecondition,AbsRealBody)) -> true ; AbsRealBody=AbsBody, create_texpr(truth,pred,[],AbsPrecondition)), |
351 | | |
352 | | % refinement po for the preconditions |
353 | | create_negation(AbsPrecondition,NegAbsPrecondition), |
354 | | conjunct_predicates([Invariant,LinkingInvariant,Precondition,NegAbsPrecondition],PreRefPo), |
355 | | solve_predicate(PreRefPo,State,PreRefPoRes), |
356 | | |
357 | | % result string and print |
358 | | ajoin([Name, ' Precondition Refinement I & J & P => P1: Counter-Example found: ', PreRefPoRes],PreRefPoResult), |
359 | | write(PreRefPoResult), nl, translate:nested_print_bexpr(PreRefPo), |
360 | | write(State),nl, |
361 | | |
362 | | % for the refinement of operations, we need to rename existing output variables (i.e. prime them) |
363 | | prime_variables(Results,PrimedResults), |
364 | | list_renamings_to_primed_vars(Results,Renamings), |
365 | | rename_bt(RealBody,Renamings,RealBodyWithPrimedVariables), |
366 | | create_equals(Results,PrimedResults,EqualResultsPred), |
367 | | |
368 | | % refinement po for the operation |
369 | | % I & J & P => [S1[out'/out]] not S not (J & out'=out) |
370 | | conjunct_predicates([LinkingInvariant|EqualResultsPred],RHS), |
371 | | create_negation(RHS,NegRHS), |
372 | | |
373 | | set_reference_machine(AbsMachine), |
374 | | weakest_precondition(AbsRealBody,NegRHS,RHS2), |
375 | | delete_reference_machine, |
376 | | |
377 | | create_negation(RHS2,NegRHS2), |
378 | | weakest_precondition(RealBodyWithPrimedVariables,NegRHS2,RHS3), |
379 | | create_negation(RHS3,NegRHS3), |
380 | | conjunct_predicates([Invariant,LinkingInvariant,Precondition,NegRHS3],RefPo), |
381 | | |
382 | | solve_predicate(RefPo,State2,RefPoRes), |
383 | | % result string and print |
384 | | ajoin([Name, ' Refinement I & J & P => S1 not S not J: Counter-Example found: ', RefPoRes],RefPoResult), |
385 | | write(RefPoResult), nl, translate:nested_print_bexpr(RefPo), |
386 | | write(State2),nl, |
387 | | |
388 | | operations_pos(FurtherOps,Invariant,LinkingInvariant,AbsMachine,AbstractOperations,ListOpPos,SubViolationFound), |
389 | | assign_violation_found(RefPoRes,V1), |
390 | | assign_violation_found(PreRefPoRes,V2), |
391 | | merge_violation_found([V1,V2,SubViolationFound],ViolationFound). |
392 | | |
393 | | create_equals([],[],[]). |
394 | | create_equals([Id|Ids],[Expr|Exprs],[TPred|SubPreds]) :- |
395 | | safe_create_texpr(equal(Id,Expr),pred,TPred), |
396 | | create_equals(Ids,Exprs,SubPreds). |
397 | | |
398 | | merge_violation_found(L,true) :- |
399 | | some('=='(true),L), !. |
400 | | merge_violation_found(L,R) :- |
401 | | some('=='(time_out),L), !, R=time_out. |
402 | | merge_violation_found(_,false). |
403 | | |
404 | | assign_violation_found(solution(_),true) :- !. |
405 | | assign_violation_found(time_out,R) :- !, R= time_out. |
406 | | assign_violation_found(_,false). |