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		% WARNING (DEPRECATED) : it is planned to replace the debug_properties commands using the unsat_cores.pl predicates
6		% operation enabling code should be moved to a separate module
7
8		:- module(predicate_debugger,[tcltk_debug_properties/3,
9		tcltk_debug_properties_or_op/4, adapt_tcl_operation_name/2,
10		get_operation_propositional_guards/3, get_operation_propositional_guards/6,
11		get_operation_enabling_condition/7,
12		get_unsimplified_operation_guard/2,
13		get_unsimplified_operation_enabling_condition/5,
14		get_simplified_operation_enabling_condition/5,
15		tcltk_get_unsat_core_with_types/1]).
16
17		:- use_module(tools).
18
19		:- use_module(module_information,[module_info/2]).
20		:- module_info(group,misc).
21		:- module_info(description,'The predicate debugger adds conjuncts one by one until the predicate becomes unsatisfiable.').
22
23		:- use_module(debug).
24		:- use_module(self_check).
25		:- use_module(preferences).
26		:- use_module(error_manager).
27
28		:- use_module(translate).
29		:- use_module(b_interpreter).
30		:- use_module(bsyntaxtree).
31		:- use_module(b_ast_cleanup).
32
33		:- use_module(library(timeout)).
34		:- use_module(library(lists)).
35
36
37		:- meta_predicate maplist5(4,-,-,-,-).
38		maplist5(_P,[],[],[],[]).
39		maplist5(P,[H1|T1],[H2|T2],[H3|T3],[H4|T4]) :-
40		if(call(P,H1,H2,H3,H4),
41		maplist5(P,T1,T2,T3,T4),
42		(add_internal_error('Call fails: ',maplist5(P,H1,H2,H3,H4)),
43		fail)).
44
45		/* b_interpreter:b_debug_properties. */
46
47		:- volatile checked_property/1, last_checked_solution/2, failed_property/2, time_out_property/2, cur_conjunct_nr/1, projection_onto_component/1.
48		:- dynamic checked_property/1.
49		:- dynamic last_checked_solution/2.
50		:- dynamic failed_property/2.
51		:- dynamic time_out_property/2.
52		:- dynamic cur_conjunct_nr/1.
53		:- dynamic projection_onto_component/1.
54
55		reset_debug_properties :-
56		retractall(last_debug_info(_,_)),
57		retractall(checked_property(_)),
58		retractall(last_checked_solution(_,_)),
59		retractall(failed_property(_,_)),
60		retractall(time_out_property(_,_)),
61		retractall(cur_conjunct_nr(_)),
62		retractall(projection_onto_component(_)).
63
64		:- use_module(b_global_sets,[b_global_set/1, b_get_fd_type_bounds/3, unfixed_deferred_set/1]).
65		tcltk_debug_properties(RealRes,UnsatCore,Satisfiable) :-
66		tcltk_debug_properties_or_op('@PROPERTIES',UnsatCore,RealRes,Satisfiable).
67
68		% code below because names with $ cause problems in Tcl with eval
69		adapt_tcl_operation_name(X,R) :- var(X),!,R=X.
70		adapt_tcl_operation_name('@PROPERTIES','$setup_constants') :- !.
71		adapt_tcl_operation_name('@INITIALISATION','$initialise_machine') :- !.
72		adapt_tcl_operation_name(X,X).
73
74		tcltk_debug_properties_or_op(TclOpName,ComputeUnsatCore,list(RealRes),Satisfiable) :-
75		adapt_tcl_operation_name(TclOpName,OpName),
76		print(tcltk_debug_properties_or_op(OpName,ComputeUnsatCore,RealRes)),nl,
77		(ComputeUnsatCore==false ->
78		(OpName='$setup_constants' -> b_debug_properties
79		; OpName = '@GOAL' -> b_debug_goal
80		; b_debug_operation(OpName))
81		; set_fast_unsat_core(ComputeUnsatCore),
82		print('*** Finding Unsat Core : '), print(ComputeUnsatCore),nl,
83		(b_find_unsat_core
84		-> print('*** Finished '),nl
85		; add_error_fail(predicate_debugger,'Finding Unsat Core failed',OpName))
86		),
87		print(debugged(OpName)),nl,
88		findall(TP, (checked_property(P),
89		translate_bexpression_with_limit(P,TrP),
90		ajoin([TrP,' &\n'],TP)),
91		Res1),
92		(projection_onto_component(_SubNr)
93		-> Res1P = ['(only a sub-component was analysed)\n'|Res1] ; Res1P=Res1),
94		(Res1=[] -> R1=Res1P ;
95		R1=['\n ********\n\nSATISFIABLE CONSTRAINTS and PROPERTIES:\n'|Res1P]
96		),
97		findall(TP2,( ((failed_property(P,_),RES='false') ; (time_out_property(P,_),RES='time_out')),
98		translate_status(P,RES,TP2)),
99		Res2),
100		(Res2=[] -> R2=['\nNo unsatisfiable PROPERTY or CONSTRAINT'], Satisfiable=true
101		; R2=['\n ********\n\nFirst unsatisfiable PROPERTY or CONSTRAINT:\n'|Res2],
102		Satisfiable=false
103		),
104		findall(TP, (last_checked_solution(ConstantsState,_), % TO DO: Project on remaining variables !?
105		translate_equivalence(b(identifier('SOLUTION'),boolean,[]),ConstantsState,TP)),
106		Res12),
107		append(R2,['\n\n ********\n\nSolution for satisfiable part:\n'|Res12],R2Res12),
108		append(R1,R2Res12,Res),
109		findall(SetDescr,(b_global_set(Set),b_get_fd_type_bounds(Set,LowBnd,UpBnd), Card is 1+UpBnd-LowBnd,
110		create_texpr(identifier(Set),set(global(Set)),[],SetId),
111		create_texpr(card(SetId),integer,[],CardExpr),
112		create_texpr(value(int(Card)),integer,[],ValExpr),
113		create_texpr(equal(CardExpr,ValExpr),prop,[],EqualExpr),
114		translate_bexpression(EqualExpr,SetDescr1),
115		(unfixed_deferred_set(Set) -> Xtra = ' (assumed for deferred set)' ; Xtra=''),
116		ajoin([SetDescr1,Xtra,'\n'],SetDescr)), Sets),
117
118		append(['\nCardinalities of SETS:\n'|Sets],Res,SRes),
119		preferences:get_preference(minint,MININT),
120		preferences:get_preference(maxint,MAXINT),
121		clear_error_context,
122		ajoin(['MININT .. MAXINT = ',MININT,'..',MAXINT],MINMAX),
123		RealRes = ['SETTINGS:\n',MINMAX|SRes].
124		tcltk_debug_properties_or_op([],_,list(['Machine has no PROPERTIES']),true).
125
126		failed_or_time_out_property(P) :- failed_property(P,_) ; time_out_property(P,_).
127
128		:- use_module(library(codesio),[write_to_codes/2]).
129		:- use_module(tools,[ajoin/2]).
130		% use_module(probsrc(predicate_debugger)),predicate_debugger:print_unsat_core_with_types
131		tcltk_get_unsat_core_with_types(ResultCodes) :-
132		get_unsat_core(AllConj),
133		translate_predicate_into_machine(AllConj,ResultAtom),
134		write_to_codes(ResultAtom,ResultCodes).
135
136		get_unsat_core(AllConj) :- (checked_property(_) ; failed_or_time_out_property(_)), !,
137		findall(P,checked_property(P),Ps),
138		findall(UnsatP,failed_or_time_out_property(UnsatP),UPs),
139		append(Ps,UPs,All),
140		conjunct_predicates(All,AllConj).
141		get_unsat_core(Core) :- print('No predicate debugger analysis run'),nl,
142		print('Trying to extract from b_interpreter'),nl,
143		b_interpreter:get_unsat_component_predicate(_,Core,_Vars),!.
144		get_unsat_core(b(truth,pred,[])).
145
146
147		translate_equivalence(A,B,R) :-
148		translate_bexpression(A,TA),
149		translate_bstate(B,TB),
150		ajoin([TA,'\n == ',TB,'\n'],R).
151		:- use_module(translate,[translate_span/2]).
152		translate_status(A,Status,R) :-
153		translate_bexpression(A,TA),
154		(translate_span(A,ASpan)
155		-> ajoin([TA,'\n == ',Status,' ',ASpan],R)
156		; ajoin([TA,'\n == ',Status],R)).
157
158
159
160		:- use_module(bmachine).
161		b_debug_properties :- set_error_context(b_debug_properties),
162		reset_debug_properties,
163		%%b_extract_constants_and_properties(Constants,CstTypes,Properties),
164		%b_machine_has_constants_or_properties,
165		b_get_machine_constants(TypedConstants),
166		get_adapted_properties(TypedConstants,AProperties,ATypedConstants,AllowTimeout),
167		nr_of_conjuncts(AProperties,NrConj),
168		(b_debug_properties2(AProperties,ATypedConstants,[],NrConj,AllowTimeout) -> true ; true).
169
170		b_debug_goal :-
171		bmachine:b_get_machine_goal(Goal),
172		b_debug_predicate(Goal).
173		b_debug_predicate(FullPred) :- set_error_context(b_debug_predicate),
174		reset_debug_properties,
175		get_parameters(FullPred,Params,Pred),
176		get_current_state('@PRED',CurID,CurBState),
177		set_error_context(b_debug_predicate(CurID)),
178		nr_of_conjuncts(Pred,NrConj),
179		(b_debug_properties2(Pred,Params,CurBState,NrConj,allow_timeout) -> true ; true).
180
181		get_parameters(b(exists(Parameters,Pred),pred,_),Parameters,Pred) :- !.
182		get_parameters(Pred,[],Pred).
183
184		:- use_module(library(lists)).
185		get_adapted_properties(TypedConstants,Pred,CTypedConstants,do_not_allow_timeout) :-
186		%(b_interpreter:nr_of_components(NrC), NrC>1),
187		preferences:get_preference(partition_predicates,true),
188		b_interpreter:get_unsat_component_predicate(CompNr,Pred,Vars),!, % means there was no timeout
189		assert(projection_onto_component(CompNr)),
190		print(debugging_unsat_or_skipped_component(CompNr)),nl,
191		print(component_vars(Vars)),nl,
192		project_texpr_identifiers(TypedConstants,Vars,CTypedConstants).
193		get_adapted_properties(TypedConstants,Properties,TypedConstants,allow_timeout) :-
194		% TO DO determine whether timeout occured
195		b_get_properties_from_machine(Properties).
196
197
198		% only keep texpr_identifiers whose id is in the provided list
199		project_texpr_identifiers([],_,[]).
200		project_texpr_identifiers([TID|T],Vars,Res) :-
201		(get_texpr_id(TID,ID),member(ID,Vars)
202		-> Res = [TID|R2] ; Res=R2),
203		project_texpr_identifiers(T,Vars,R2).
204
205		:- use_module(specfile,[state_corresponds_to_initialised_b_machine/2, state_corresponds_to_set_up_constants/2]).
206		/* b_interpreter:tcltk_debug_properties_or_op(prog1,R)*/
207		b_debug_operation(OpName) :-
208		reset_debug_properties,
209		get_current_state(OpName,CurID,CurBState),
210		set_error_context(operation(OpName,CurID)),
211		(get_operation_enabling_condition(OpName,Parameters,EnablingCondition,BSVars,_,true,false) -> true
212		; add_error(b_debug_operation,'Operation does not exist or cannot determine enabling condition: ',OpName),fail),!,
213		print('Enabling: '), print_bexpr(EnablingCondition),nl,
214		flush_output(user),
215		nr_of_conjuncts(EnablingCondition,NrConj),
216		~~mnf(insert_before_substitution_variables(BSVars,[],CurBState,CurBState,NewCurBState)),
217		extract_exists_parameters(EnablingCondition,Parameters,NewCond,NewParas),
218		(b_debug_properties2(NewCond,NewParas,NewCurBState,NrConj,allow_timeout) -> true ; true).
219
220		:- use_module(state_space,[current_expression/2]).
221		get_current_state(OpName,CurID,CurBState) :-
222		(current_expression(CurID,CurState) -> true
223		; add_error(predicate_debugger,'Could not get current state',OpName),fail),
224		(state_corresponds_to_initialised_b_machine(CurState,CurBState) -> true
225		; (OpName=='$initialise_machine',
226		state_corresponds_to_set_up_constants(CurState,CurBState)) -> true
227		; add_error(b_debug_operation,'Machine not yet initialised! ',CurState),fail).
228
229
230		% Try to lift out existentially quantified variables to the outer level; to make the debugging more fine-grained
231		extract_exists_parameters(Pred,Parameters, NewPred, NewParas) :-
232		get_texpr_expr(Pred,exists(Vars,Body)),
233		disjoint_list_union(Parameters,Vars,Paras1), !, % also checks if no clash exists; otherwise we have to keep exists
234		print(augmented_paras(Paras1)),nl,
235		extract_exists_parameters(Body,Paras1,NewPred,NewParas).
236		extract_exists_parameters(Pred,Parameters, NewPred, NewParas) :-
237		get_texpr_expr(Pred,conjunct(LHS,RHS)),!,
238		extract_exists_parameters(LHS,Parameters, NewLHS, IntParas),
239		extract_exists_parameters(RHS,IntParas,NewRHS,NewParas),
240		conjunct_predicates([NewLHS,NewRHS],NewPred).
241		extract_exists_parameters(Pred,Par,Pred,Par).
242
243
244		:- dynamic obtain_action_enabling_conditions/0, simplify_enabling_condition/1.
245		obtain_action_enabling_conditions. simplify_enabling_condition(true).
246		set_obtain_action_enabling_conditions(true) :- !,
247		(obtain_action_enabling_conditions -> true ; assert(obtain_action_enabling_conditions)).
248		set_obtain_action_enabling_conditions(_) :- retractall(obtain_action_enabling_conditions).
249		set_simplify_enabling_condition(X) :- retractall(simplify_enabling_condition(_)),
250		assert(simplify_enabling_condition(X)).
251
252		:- use_module(b_interpreter_components,[construct_optimized_exists/3,construct_optimized_exists/4]).
253		:- use_module(specfile,[animation_minor_mode/1]).
254		:- use_module(external_functions,[external_subst_enabling_condition/3]).
255
256		get_unsimplified_operation_guard(OpName,Guard) :-
257		get_unsimplified_operation_enabling_condition(OpName,Parameters,EnablingCondition,_BecomesSuchVars,_Precise),
258		construct_optimized_exists(Parameters,EnablingCondition,Guard).
259
260		get_unsimplified_operation_enabling_condition(OpName,Parameters,EnablingCondition,BecomesSuchVars,Precise) :-
261	?	Simplify=false,
262	?	(animation_minor_mode(eventb) -> GetFromAction=false
263		; GetFromAction=true),
264	?	get_operation_enabling_condition(OpName,Parameters,EnablingCondition,BecomesSuchVars,Precise,GetFromAction,Simplify).
265
266		get_simplified_operation_enabling_condition(OpName,Parameters,EnablingCondition,BecomesSuchVars,Precise) :-
267		Simplify=true,
268		(animation_minor_mode(eventb) -> GetFromAction=false
269		; GetFromAction=true),
270		get_operation_enabling_condition(OpName,Parameters,EnablingCondition,BecomesSuchVars,Precise,GetFromAction,Simplify).
271
272		get_operation_enabling_condition(OpName,Parameters,EnablingCondition,BecomesSuchVars,IsPrecise,GetAct,Simplify) :-
273	?	set_obtain_action_enabling_conditions(GetAct), % specify whether we want also conditions stemming from actions, such as :() or ::
274	?	set_simplify_enabling_condition(Simplify), % specify whether we want to simplify the EnablingCondition if possible
275		%%nonvar(OpName), %% I am not sure why this test is here ??
276		%% print(getting_enabling(OpName,GetAct)),nl,%%
277	?	b_get_machine_operation_for_animation(OpName,_Results,Parameters,TBody,_OType,true),
278		get_operation_enabling_condition1(TBody,EnablingCondition,BecomesSuchVars,IsPreciseV),
279		(var(IsPreciseV) -> IsPrecise = precise ; IsPrecise = imprecise).
280
281		get_operation_enabling_condition1(TBody,EnablingCondition,BecomesSuchVars,IsPrecise) :-
282		get_texpr_expr(TBody,Body),
283		(get_operation_enabling_condition2(Body,EnablingCondition,BecomesSuchVars,IsPrecise) -> true
284		; add_internal_error('Getting enabling condition failed: ',Body),
285		%trace,get_operation_enabling_condition2(Body,EnablingCondition,BecomesSuchVars),
286		create_texpr(truth,pred,[],EnablingCondition),
287		BecomesSuchVars=[]).
288
289		/* TO DO: recursively expand the code below for more complicated SELECT,ANY,... */
290		get_operation_enabling_condition2(precondition(PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % PRE
291		get_operation_enabling_condition1(TBody,RC,BecomesSuchVars,IsPrecise),
292		~~mnf(conjunct_predicates([PreCond,RC],Res)).
293		get_operation_enabling_condition2(assertion(_PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % ASSERT
294		get_operation_enabling_condition1(TBody,Res,BecomesSuchVars,IsPrecise).
295		get_operation_enabling_condition2(block(TBody),Res,BecomesSuchVars,IsPrecise) :- !, % BEGIN ... END
296		get_operation_enabling_condition1(TBody,Res,BecomesSuchVars,IsPrecise).
297		get_operation_enabling_condition2(choice(ChoiceList),Res,BecomesSuchVars,IsPrecise) :- !, % CHOICE ... OR ...
298		get_disjunction_of_enabling_conditions(ChoiceList,Res,BecomesSuchVars,IsPrecise).
299		get_operation_enabling_condition2(var(_Parameters,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % VAR
300		% should the Parameters be added somewhere ? In principle the enabling condition should always be true, as we have a low-level construct
301		get_operation_enabling_condition1(TBody,Res,BecomesSuchVars,IsPrecise).
302		get_operation_enabling_condition2(sequence([TBody1|_]),Res,BecomesSuchVars,imprecise) :- !, % ;
303		(debug:debug_mode(on) -> print(ignoring_potential_enabling_condition_in_tail_of_sequence),nl ; true),
304		% TO DO: compute before-after predicate of TBody1 ? before_after_predicate_list_conjunct_with_equalities ?
305		% we ignore rest of sequence; cannot influence enabling condition; probably this should always return truth
306		get_operation_enabling_condition1(TBody1,Res,BecomesSuchVars,_IsPrecise).
307		get_operation_enabling_condition2(lazy_let_subst(ID,ExprOrPred,TBody),Res,BecomesSuchVars,IsPrecise) :- !,
308		Res = b(lazy_let_pred(ID,ExprOrPred,BodyRes),pred,[]),
309		get_operation_enabling_condition1(TBody,BodyRes,BecomesSuchVars,IsPrecise).
310		get_operation_enabling_condition2(let(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % LET
311		% for the moment: treat like ANY, but we could avoid introducing existential quantifier ?!
312		get_operation_enabling_condition2(any(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise).
313		get_operation_enabling_condition2(any(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % ANY
314		get_operation_enabling_condition1(TBody,RC,BecomesSuchVars,IsPrecise),
315		~~mnf(conjunct_predicates([PreCond,RC],Res1)),
316		simplify_enabling_condition(Simplify),
317		construct_optimized_exists(Parameters,Res1,Res,Simplify).
318		%get_operation_enabling_condition2(select([b(select_when(PreCond, TBody),_,_)]),Res,BecomesSuchVars) :- !,
319		% get_texpr_expr(TBody,Body),
320		% ~~mnf(get_operation_enabling_condition2(Body,RC,BecomesSuchVars)),
321		% ~~mnf(conjunct_predicates([PreCond,RC],Res)).
322		%get_operation_enabling_condition2(select([b(select_when(PreCond, TBody),_,_)],b(skip,_,_)),Res,BecomesSuchVars) :- !,
323		% get_texpr_expr(TBody,Body),
324		% ~~mnf(get_operation_enabling_condition2(Body,RC,BecomesSuchVars)),
325		% ~~mnf(conjunct_predicates([PreCond,RC],Res)).
326		get_operation_enabling_condition2(select_when(PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !,
327		get_operation_enabling_condition1(TBody,RC,BecomesSuchVars,IsPrecise),
328		~~mnf(conjunct_predicates([PreCond,RC],Res)).
329		get_operation_enabling_condition2(select(ListOfWhens),Res,BecomesSuchVars,IsPrecise) :- !,
330		get_disjunction_of_enabling_conditions(ListOfWhens,Res,BecomesSuchVars,IsPrecise).
331		get_operation_enabling_condition2(select(ListOfWhens,Else),Res,BecomesSuchVars,IsPrecise) :- !,
332		get_texpr_exprs(ListOfWhens,ListOfSelectWhens),
333		maplist(get_operation_enabling_condition3(IsPrecise),ListOfSelectWhens,Res1,BecomesSuchVars1),
334		get_operation_enabling_condition1(Else,ResElse,ElseBecomesSuchVars,IsPrecise),
335		~~mnf(disjunct_predicates([ResElse|Res1],Res)),
336		append([ElseBecomesSuchVars|BecomesSuchVars1],BecomesSuchVars).
337		get_operation_enabling_condition2(parallel([TH|T]),Res,BecomesSuchVars,IsPrecise) :- !,
338		get_operation_enabling_condition1(TH,E1,BecomesSuchVarsH,IsPrecise),
339		(T=[] -> Res=E1, BecomesSuchVarsH=BecomesSuchVars
340		; (~~mnf(get_operation_enabling_condition2(parallel(T),E2,BecomesSuchVarsT,IsPrecise)),
341		append(BecomesSuchVarsH,BecomesSuchVarsT,BecomesSuchVars),
342		conjunct_predicates([E1,E2],Res))).
343		get_operation_enabling_condition2(becomes_element_of(_LHS,RHS),Res,[],_Precise) :-
344		obtain_action_enabling_conditions,
345		get_texpr_expr(RHS,RHSExpr),get_texpr_type(RHS,Type),!,
346		(simplify_enabling_condition(true),
347		definitely_not_empty(RHSExpr,Type)
348		-> %print(def_not_empty(RHSExpr)),nl,
349		create_texpr(truth,pred,[],Res)
350		; create_texpr(empty_set,Type,[],EmptySet),
351		safe_create_texpr(not_equal(RHS,EmptySet),pred,Res2),
352		%print(not_equal_empty(RHSExpr,Type)),nl,
353		~~mnf(clean_up(Res2,[],Res))
354		).
355		get_operation_enabling_condition2(becomes_such(Vars,Condition),Res,Vars,_Precise) :- % Vars : (Condition)
356		% example x: (x$0 >= 1 & x=x$0+1)
357		obtain_action_enabling_conditions,!,
358		simplify_enabling_condition(Simplify),
359		construct_optimized_exists(Vars,Condition,Res1,Simplify),
360		%translate:print_bexpr(Res1),nl,
361		% e.g, for example above we have #x.(x$0 >= 1 & x=x$0+1) -> x$0 >= 1
362		% now rename $0 variables to act on current state to obtain the condition:
363		findall(rename(BeforeId,Id),
364		(member(b(identifier(Id),_,Infos),Vars),
365		member(before_substitution(_,BeforeId),Infos)),
366		RenameList),
367		rename_bt(Res1,RenameList,Res). % for example above: Res is x >= 1
368		get_operation_enabling_condition2(rlevent(_Name,_Section,_Status,_Params,Guard,_Theorems,Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents),Res,BecomesSuchVars,IsPrecise) :- !,
369		%print(actions(Actions)),nl,
370		% TO DO: have a look at get_full_eventb_guard. Do we want to recurse through the abstractions ?
371		(obtain_action_enabling_conditions
372		-> get_operation_enabling_for_event_b_actions(Actions,Guard,Res,BecomesSuchVars,IsPrecise)
373		; Res=Guard,BecomesSuchVars=[]).
374		get_operation_enabling_condition2(assign(_LHS,_RHS),Truth,[],_Precise) :- !,
375		create_texpr(truth,pred,[],Truth).
376		get_operation_enabling_condition2(assign_single_id(_IDE,_RHS),Truth,[],_Precise) :- !,
377		create_texpr(truth,pred,[],Truth).
378		get_operation_enabling_condition2(case(A,_,_),Truth,[],imprecise) :- !, % CASE is now translated to LET + IF-THEN-ELSE in b_ast_cleanup
379		print('Not computing enabling for CASE: '), translate:print_bexpr(A),nl,
380		create_texpr(truth,pred,[],Truth).
381		get_operation_enabling_condition2(while(_,_,_,_),Truth,[],imprecise) :- !,
382		debug:debug_println(9,enabling_for_while_assumed_true),
383		create_texpr(truth,pred,[],Truth).
384		get_operation_enabling_condition2(if(IfList),Res,BecomesSuchVars,IsPrecise) :- !,
385		maplist5(get_if_condition(IsPrecise),IfList,Tests,Conds,BecomesSuchVars1),
386		append(BecomesSuchVars1,BecomesSuchVars),
387	?	((member(X,Conds), \+ is_truth(X))
388		-> disjoin_ifs(Tests,Conds,[],L),
389		conjunct_predicates(L,Res)
390		; create_texpr(truth,pred,[],Res) % all branches have no enabling condition
391		).
392		get_operation_enabling_condition2(skip,Truth,[],_Prcise) :- !,
393		create_texpr(truth,pred,[],Truth).
394		get_operation_enabling_condition2(external_subst_call(Pred,Args),Res,[],_Precise) :-
395		external_subst_enabling_condition(Pred,Args,Cond),!, Res=Cond.
396		get_operation_enabling_condition2(operation_call(Operation,_OpCallResults,OpCallParas),Res,BecomeSuchVars,IsPrecise) :-
397		def_get_texpr_id(Operation,op(OperationName)),
398		b_get_machine_operation_for_animation(OperationName,_OpResults,OpParameters,Body,_OType,_TopLevel),
399		bsyntaxtree:replace_ids_by_exprs(Body,OpParameters,OpCallParas,Body2),
400		!,
401		%print(get_enabling_for_opcall),nl,translate:print_subst(Body2),nl,
402		get_operation_enabling_condition1(Body2,Res,BecomeSuchVars,IsPrecise).
403		get_operation_enabling_condition2(X,Truth,[],imprecise) :- %print(cannot_obtain(X)),nl,
404		(obtain_action_enabling_conditions
405		-> functor(X,F,A),debug_println(9,cannot_obtain_enabling(F/A,X)) ; true),
406		create_texpr(truth,pred,[],Truth).
407
408
409		get_if_condition(IsPrecise,b(if_elsif(Test,TBody),_,_),Test,Condition,BecomesSuchVars) :-
410		get_operation_enabling_condition1(TBody,Condition,BecomesSuchVars,IsPrecise).
411
412		:- use_module(bsyntaxtree, [create_implication/3]).
413		disjoin_ifs([],[],_,[]).
414		disjoin_ifs([Test|TT],[EnableCond|TC],NegSoFar,[Res1|TR]) :-
415		append(NegSoFar,[Test],L),
416		conjunct_predicates(L,BranchTest),
417		create_implication(BranchTest,EnableCond,Res1), % ELSEIF Test THEN Body ... ---> NegSoFar & Test => EnableCond
418		create_negation(Test,NTest),
419		append(NegSoFar,[NTest],NegSoFar1), % add negation of test as additional test for rest
420		disjoin_ifs(TT,TC,NegSoFar1,TR).
421
422
423		% for a list of substitutions: get enabling conditions and disjoin them
424		get_disjunction_of_enabling_conditions(ListOfWhens,Res,BecomesSuchVars,IsPrecise) :-
425		get_texpr_exprs(ListOfWhens,ListOfSelectWhens),
426		maplist(get_operation_enabling_condition3(IsPrecise),ListOfSelectWhens,Res1,BecomesSuchVars1),
427		~~mnf(disjunct_predicates(Res1,Res)),
428		append(BecomesSuchVars1,BecomesSuchVars).
429		get_operation_enabling_condition3(Precise,Exp,Res,BV) :- get_operation_enabling_condition2(Exp,Res,BV,Precise).
430
431		definitely_not_empty(bool_set,_).
432		definitely_not_empty(integer_set(_),_).
433		definitely_not_empty(identifier(X),set(global(X))).
434		definitely_not_empty(string_set,_).
435
436
437
438		% get operation enabling condition in context of an event-b action list:
439		get_operation_enabling_for_event_b_actions([],Res,Res,[],_Precise).
440		get_operation_enabling_for_event_b_actions([H|T],InRes,OutRes,BecomesSuchVars,IsPrecise) :-
441		get_operation_enabling_condition1(H,ResH,HBecomesSuchVars,IsPrecise),
442		~~mnf(conjunct_predicates([InRes,ResH],IntRes)),
443		get_operation_enabling_for_event_b_actions(T,IntRes,OutRes,TBecomesSuchVars,IsPrecise),
444		append(HBecomesSuchVars,TBecomesSuchVars,BecomesSuchVars).
445
446		% ---------------
447		:- use_module(bmachine,[b_top_level_operation/1]).
448		% LTSMIN style guards: a guard that does not depend on parameters
449		get_operation_propositional_guards(OpName,Guards,RestBody) :-
450		b_top_level_operation(OpName),
451		b_get_machine_operation_for_animation(OpName,TResults,TParameters,TBody,_OType,true), % requires bmachine to be precompiled
452		get_operation_propositional_guards(OpName,TResults,TParameters,TBody,Guards,RestBody).
453
454		:- use_module(translate,[print_bexpr/1]).
455		% the following can be called directly; does not require bmachine to be pre-compiled
456		get_operation_propositional_guards(OpName,TResults,TParameters,TBody,Guards,RestBody) :-
457		get_texpr_ids(TParameters,Ids1),
458		get_texpr_ids(TResults,Ids2),
459		append(Ids1,Ids2,Ids), sort(Ids,Parameters),
460		get_operation_guards_aux(TBody,Parameters,top,Guards,RestBody),
461		(debug:debug_mode(off) -> true
462		; format('OPERATION Guard Splitting ~w (~w)~n',[OpName,Parameters]),
463		print('LTSMin Guards: '), maplist(print_bexpr,Guards),nl,
464		print('LTSMin Body: '), translate:print_subst(RestBody),nl,nl
465		).
466
467		:- use_module(bsyntaxtree, [conjunction_to_list/2,find_identifier_uses/3]).
468
469
470		get_operation_guards_aux(Subst,Parameters,Top,Guards,OpBody) :-
471		get_guards(Subst,Top,TIds,Guard,InnerBody,Infos),
472		get_texpr_ids(TIds,Ids), sort(Ids,NewIds),
473		ord_union(Parameters,NewIds,Parameters2),
474		!,
475		get_parameter_independent_guards(Guard,Parameters2,Indep,Dep),
476		(Dep = []
477		-> OpBody = InnerOpBody % no need to keep b
478		; conjunct_predicates(Dep,DepCond),
479		construct_select(TIds,DepCond,InnerOpBody,Infos,OpBody) % we always produce a SELECT; even if we had a PRE as it will no longer be innermost ! we assume treat_outermost_pre_as_select is set to true for PRE (checked below)
480		),
481		get_operation_guards_aux(InnerBody,Parameters2,inner,InnerGuards,InnerOpBody),
482		append(Indep,InnerGuards,Guards).
483
484		get_operation_guards_aux(b(rlevent(Name,Sect,Status,Params,EvGuard,Theorems,Act,VWit,PWit,Unmod,AbsEvts),subst,Info),
485		Parameters,_,Guards,OpBody) :- !,
486		get_parameter_independent_guards(EvGuard,Parameters,InDepGuards,Dep),
487		(get_variant_pred(Status,VariantPred)
488		-> %print(op_variant(_Name)),nl,translate:print_bexpr(VariantPred),nl,
489		% we virtually include the Variant expression in the read info; ensure that LTS Min knows that this will be read by the Event-B interpreter
490		% TO DO: check if we need to add the witnesses as well !
491		Guards = [VariantPred|InDepGuards]
492		; Guards = InDepGuards),
493		conjunct_predicates(Dep,DepG),
494		OpBody = b(rlevent(Name,Sect,Status,Params,DepG,Theorems,Act,VWit,PWit,Unmod,AbsEvts),subst,Info).
495		get_operation_guards_aux(TB,_,_,[],TB).
496
497
498		:- use_module(bsyntaxtree, [safe_create_texpr/3]).
499		% we integrate the Variant check into the guard to ensure the correct read matrix is produced
500		% currently the Variant is checked upon event entry and for convergent events upon exit for decrease
501		% in principle this should be more of an assertion_predicate or assertion_expression
502		get_variant_pred(b(Status,status,_),Res) :- get_variant_pred_aux(Status,Res).
503		get_variant_pred_aux(anticipated(Variant),Res) :- NATURAL = b(integer_set('NATURAL'),set(integer),[]),
504		safe_create_texpr(member(Variant,NATURAL),pred,Res).
505		get_variant_pred_aux(convergent(Variant),Res) :- NATURAL1 = b(integer_set('NATURAL1'),set(integer),[]),
506		safe_create_texpr(member(Variant,NATURAL1),pred,Res).
507
508
509		get_guards(b(precondition(Guard,TBody),subst,Info), top, [],Guard, TBody, Info) :-
510		preferences:get_preference(treat_outermost_pre_as_select,true).
511		get_guards(b(select([b(select_when(Guard, TBody),subst,_Info1)]),subst,Info2), _, [],Guard, TBody, Info2).
512		% TO DO: for ANY try and extract propositional parts, e.g., for ANY pp WHERE pp:1..xx & z=1/yy THEN …
513		get_guards(b(any(TIds,Guard,TBody),subst,Info),_, TIds,Guard,TBody,Info).
514
515
516		construct_select([],Guard,TBody, Infos, Res) :- !,
517		Res = b(select([b(select_when(Guard, TBody),subst,Infos)]),subst,Infos).
518		construct_select(TIds,Guard,TBody,Infos, b(any(TIds,Guard,TBody),subst,Infos)).
519
520
521		get_parameter_independent_guards(Guard,Parameters,Indep,Dep) :-
522		conjunction_to_list(Guard,Gs),
523		l_get_parameter_independent_guards(Gs,Parameters,at_front,Indep,Dep).
524
525		:- use_module(library(ordsets)).
526		:- use_module(bsyntaxtree,[always_well_defined/1]).
527		l_get_parameter_independent_guards([],_,_,[],[]).
528		l_get_parameter_independent_guards([G|Gs],Parameters,AtFront,Indep,Dep) :-
529		find_identifier_uses(G,[],Ids),
530		((ord_disjoint(Ids,Parameters),
531		(AtFront=at_front -> true ; always_well_defined(G)))
532		-> Indep=[G|I1], Dep=D1, AtFront1=AtFront
533		; Indep=I1, Dep=[G|D1],
534		AtFront1=not_at_front % we have skipped one guard; the next guard is not guaranteed to be at the front (relevant for well-definedness)
535		),
536		l_get_parameter_independent_guards(Gs,Parameters,AtFront1,I1,D1).
537
538		% -----------------------------------------
539
540		:- use_module(library(timeout)).
541
542
543		nr_of_conjuncts(Pred,Nr) :-
544		is_a_conjunct(Pred,LHS,RHS),!,
545		nr_of_conjuncts(LHS,NrL),
546		nr_of_conjuncts(RHS,NrR),
547		Nr is NrL+NrR.
548		nr_of_conjuncts(_,1).
549
550		:- volatile last_debug_info/2.
551		:- dynamic last_debug_info/2.
552		b_debug_properties2(Pred,Constants,GlobalState,TotalNr,AllowTimeout) :-
553		create_texpr(truth,pred,[b_debug_properties],Truth),
554		retractall(last_debug_info(_,_)), assert(last_debug_info(Constants,GlobalState)),
555		(b_debug_find_first_unsat_property(Pred,Truth,Constants,GlobalState,TotalNr,AllowTimeout)
556		-> print('ALL PROPERTIES SATISFIABLE'),nl
557		; true % get_preference(debug_try_minimise,false) -> true ; b_find_unsat_core(Constants,GlobalState)
558		).
559
560		b_find_unsat_core :- /* assumes that b_debug_properties was run before */
561		% b_machine_has_constants_or_properties,
562		% b_get_machine_constants(TypedConstants),
563		% b_get_properties_from_machine(Properties),!,
564		% get_adapted_properties(TypedConstants,_AProperties,ATypedConstants),
565		%b_find_unsat_core(ATypedConstants,[]).
566		last_debug_info(Constants,GlobalState), b_find_unsat_core(Constants,GlobalState).
567		b_find_unsat_core(Constants,GlobalState) :-
568		print('TRYING TO MINIMISE UNSATISFIABLE PROPERTIES'),nl,
569		(last_checked_solution(_,Time)
570		-> print(' Time for last solution in ms: '), print(Time), nl ; true),
571		findall(P,checked_property(P),SatProps),
572		(failed_property(FailProp,USTime) -> true
573		; time_out_property(FailProp,USTime) -> true
574		; add_error_fail(b_find_unsat_core,'No failed or timed-out property:',SatProps)),
575		print(' Time for unsatisfiable conjuncts in ms: '), print(USTime), nl,
576		append(SatProps,[FailProp],Props),
577		length(SatProps,SL),
578		b_debug_try_remove_props(SatProps,Props,[],Constants,GlobalState,1,SL).
579		% TO DO: partition into components; try removing compnents without FailProp
580
581		b_debug_try_remove_props([],_,_,_,_,_,_) :- !.
582		b_debug_try_remove_props([],_,_,TypedConstants,GlobalState,Count,_) :- !, % for debug
583		format('~nFINISHED (~w); CHECKING CORE~n',[Count]),
584		get_unsat_core(Core),
585		nl,translate:print_bexpr(Core),nl,
586		(timeout_fast_check_property(unsat,Core,TypedConstants,_,GlobalState,TimeOutResC) -> true
587		; TimeOutResC = 'UNSAT'),
588		format('~nCORE RESULT: ~w~n',[TimeOutResC]).
589		b_debug_try_remove_props([H|TSat],[H|TUnsat],Required,TypedConstants,GlobalState,Count,Total) :-
590		append(Required,TSat,ConjunctsWithoutH),
591		conjunct_predicates(ConjunctsWithoutH,SatPred),
592		translate_bexpression(H,PT),
593		format('~nCHECKING REMOVAL(~w/~w) OF: ~w~n',[Count,Total,PT]),
594		(timeout_fast_check_property(sat,SatPred,TypedConstants,Sol,GlobalState,TimeOutResSat)
595		-> (\+ is_time_out_result(TimeOutResSat)
596		-> append(Required,TUnsat,ConjunctsWithoutH2),
597		conjunct_predicates(ConjunctsWithoutH2,UnsatPred),
598		((timeout_fast_check_property(unsat,UnsatPred,TypedConstants,_,GlobalState,TimeOutRes),
599		print(res(TimeOutRes)),nl,
600		(is_time_out_result(TimeOutRes) -> \+ time_out_property(_,_) ; true)
601		)
602		-> print('Required for inconsistency : '), print(TimeOutRes),nl,
603		append(Required,[H],NewRequired)
604		; /* H is not required for inconsistency/timeout */
605		print('NOT required for INCONSISTENCY !'),nl,
606		% print_bexpr(UnsatPred),nl,
607		Required=NewRequired,
608		% TO DO: update found solution
609		(retract(last_checked_solution(_,LastTime)) -> true
610		; print('*** Could not remove last_checked_solution'),nl,
611		preferences:get_computed_preference(debug_time_out,LastTime)
612		),
613		assert(last_checked_solution(Sol,LastTime)),
614		(retract(checked_property(H)) -> true
615		; print('*** Could not remove checked_property: '), print(H),nl
616		)
617		)
618		; print('Required for efficiency'),nl,
619		append(Required,[H],NewRequired)
620		)
621		; nl,print('*** INTERNAL ERROR: FAILED'),nl,nl,
622		append(Required,[H],NewRequired)
623		),
624		C1 is Count+1,
625		b_debug_try_remove_props(TSat,TUnsat,NewRequired,TypedConstants,GlobalState,C1,Total).
626
627		b_debug_find_first_unsat_property(Pred,Rest,Constants,GlobalState,TotalNr,AllowTimeout) :-
628		is_a_conjunct(Pred,LHS,RHS),!,
629		(b_debug_find_first_unsat_property(LHS,Rest,Constants,GlobalState,TotalNr,AllowTimeout)
630		-> conjunct_predicates([Rest,LHS],Rest2),
631		b_debug_find_first_unsat_property(RHS,Rest2,Constants,GlobalState,TotalNr,AllowTimeout)
632		; fail
633		).
634		b_debug_find_first_unsat_property(Prop,Rest,TypedConstants,GlobalState,TotalNr,AllowTimeout) :-
635		nl,nl,flush_output(user),
636		conjunct_predicates([Rest,Prop],Pred),
637		(retract(cur_conjunct_nr(CurNr)) -> true ; CurNr=1), CurNrP1 is CurNr+1,
638		assert(cur_conjunct_nr(CurNrP1)),
639		translate_bexpression(Prop,PT),
640		format('~nCHECKING (~w/~w) OF: ~w~n',[CurNr,TotalNr,PT]),
641		statistics(runtime,[Start,_]),
642		(timeout_check_property(Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes)
643		-> statistics(runtime,[Stop,_]), Time is Stop - Start,
644		print_time(TimeOutRes,Time),
645		format('~nINFO: ~w~n~n',[TimeOutRes]),
646		(((\+ last_checked_solution(_,_) % we haven't found a solution yet
647		; AllowTimeout=allow_timeout),
648		is_time_out_result(TimeOutRes))
649		-> assert(time_out_property(Prop,Time))
650		; is_time_out_failure(TimeOutRes)
651		-> assert(time_out_property(Prop,Time))
652		;
653		assert_checked_property(Prop,ConstantsState,Time) % could also be timeout
654		)
655		; statistics(runtime,[Stop,_]), Time is Stop - Start,
656		assert(failed_property(Prop,Time)),
657		print('No Solution Found !! ('),print(Time), print(' ms)'),nl, flush_output(user),
658		%print_bexpr(Pred),nl,
659		fail
660		).
661
662		is_time_out_failure(virtual_time_out(failure_enumeration_warning(_,_,_,_,_))).
663
664		print_time(TimeOutRes,Time) :- is_time_out_result(TimeOutRes),!,
665		(TimeOutRes=virtual_time_out(_) -> print('VIRTUAL ') ; true),
666		print('TIMEOUT !! ('),print(Time), print(' ms)'),nl, flush_output(user).
667		print_time(_TimeOutRes,Time) :-
668		print('OK ('), print(Time), print(' ms)'), flush_output(user).
669
670
671		last_unsat_time(Time) :- time_out_property(_,Time) -> true ; failed_property(_,Time).
672
673		set_fast_unsat_core(T) :- retractall(fast_unsat_core),
674		(T==fast -> assert(fast_unsat_core) ; true).
675		:- dynamic fast_unsat_core/0.
676		fast_unsat_core.
677
678		additional_time(301). % additional time given to account for variations in solving
679		%additional_time(1301).
680
681		get_timeout(sat,DebugTimeOut) :-
682		last_checked_solution(_,LTime),
683		!,
684		additional_time(AT),
685		DebugTimeOut is LTime+AT.
686		get_timeout(unsat,DebugTimeOut) :-
687		last_unsat_time(USTime),
688		last_checked_solution(_,LSTime),
689		(fast_unsat_core -> TT is min(USTime,LSTime) ; TT is max(USTime,LSTime)),
690		!,
691		additional_time(AT),
692		DebugTimeOut is TT+AT.
693		get_timeout(S,DebugTimeOut) :- print('*** Could not get TimeOut : '), print(S),nl,
694		preferences:get_preference(time_out,CurTO), DebugTimeOut is CurTO * 1.
695
696
697		timeout_fast_check_property(ExpectSat,Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes) :-
698		get_timeout(ExpectSat,DebugTimeOut),
699		% print(time_out_value(DebugTimeOut)),nl,
700		% print_bexpr(Pred),nl,
701		statistics(runtime,[Start,_]),
702		timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState,DebugTimeOut,TimeOutRes),
703		statistics(runtime,[Stop,_]), Time is Stop - Start, print(time(Time)),nl,
704		(is_time_out_result(TimeOutRes) -> print(time_out_occurred(Time,DebugTimeOut)),nl,
705		(debug:debug_mode(on) -> print_bexpr(Pred),nl ; true)
706		; true).
707
708		timeout_check_property(Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes) :-
709		preferences:get_computed_preference(debug_time_out,DebugTimeOut),
710		timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState,DebugTimeOut,TimeOutRes),
711		% Note: will translate failure with enumeration warning into virtual_timeout; see is_time_out_failure above
712		format('~nCHECKING RESULT is: ~w~n',[TimeOutRes]).
713
714		timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState, DebugTimeOut,TimeOutRes) :-
715		on_exception(E,
716		time_out_with_enum_warning_one_solution(
717		b_check_property_satisfiable(Pred,TypedConstants,ConstantsState,GlobalState),
718		DebugTimeOut,TimeOutRes),
719		TimeOutRes = virtual_time_out(exception(E))). % probably CLPFD overflow
720
721
722		assert_checked_property(P,ConstantsState,Time) :-
723		assert(checked_property(P)),
724		(var(ConstantsState) -> print('NO SOLUTION'),nl
725		; retractall(last_checked_solution(_,_)),
726		assert(last_checked_solution(ConstantsState,Time))).
727
728		:- use_module(kernel_waitflags).
729		:- use_module(b_enumerate).
730
731		% TO DO: call something which will use predicate_components
732
733		b_check_property_satisfiable(Properties,TypedConstants,ConstantsState,GlobalState) :-
734		b_ast_cleanup:clean_up_pred(Properties,[],Pred),
735		set_up_typed_localstate(TypedConstants,_FreshVars,TypedVals,[],ConstantsState,positive),
736		b_interpreter_components:reset_component_info(false),
737		append(ConstantsState,GlobalState,State),
738		b_interpreter_components:b_trace_test_components(Pred,State,TypedVals),
739		\+ b_interpreter_components:unsat_component_exists.
740
741
742
743		% ------------------------------------
744		% This code might be obsolete - replaced by unsat_cores module
745		% ------------------------------------
746
747		% NEW FIND UNSAT CORE
748
749		% Assumes predicate unsatisfiable without time-out to start with
750		% not yet finished
751
752		%:- use_module(bsyntaxtree, [conjunction_to_list/2,conjunct_predicates/2,find_identifier_uses/3]).
753
754		% :- use_module(predicate_debugger), predicate_debugger:unsat_core_goal.
755		%unsat_core_goal :-
756		% bmachine:b_get_machine_goal(Goal),
757		% unsat_core(Goal).
758		%unsat_core(FullPred) :-
759		% get_parameters(FullPred,Params,Conj),
760		% get_current_state('@PRED',CurID,CurBState),
761		% set_error_context(unsat_core(CurID)),
762		% conjunction_to_list(Conj,List),
763		% create_texpr(truth,pred,[],T), append(List,[T],ListT), % so that we also check full property
764		% unsat_core_list(ListT,[],Params,CurBState).
765
766		%remove_last(List,H,NewList) :- append(NewList,[H],List).
767
768		%unsat_core_list([],List,_Parameters,_CurBState) :-
769		% conjunct_predicates(List,Pred),
770		% print('UNSAT CORE: '), translate:print_bexpr(Pred),nl,
771		% find_identifier_uses(Pred,[],Used),
772		% print('USED IDENTIFIERS: '), print(Used),nl.
773		%unsat_core_list(List1,List2,Parameters,CurBState) :-
774		% remove_last(List1,H,NewList1),
775		% print('Checking removal of : '), translate:print_bexpr(H),nl,
776		% append(NewList1,List2,List),
777		% conjunct_predicates(List,Pred),
778		% print(' --> '),translate:print_bexpr(Pred),nl,
779		% preferences:get_preference(time_out,CurTO), DebugTimeOut is CurTO * 3,
780		% tools:start_ms_timer(TIMER),
781		% (time_out(b_check_property_satisfiable(Pred,Parameters,_ConstantsState,CurBState),
782		% DebugTimeOut,TimeOutRes)
783		% -> (TimeOutRes=time_out -> print('*** TIME OUT ***') ; print(' *** SAT ***')),nl,
784		% tools:stop_ms_timer(TIMER),
785		% unsat_core_list(NewList1,[H|List2],Parameters,CurBState)
786		% ; print(' --- STILL UNSAT (REMOVING CONJUNCT) ---'),nl,
787		% tools:stop_ms_timer(TIMER),
788		% unsat_core_list(NewList1,List2,Parameters,CurBState)
789		% ).
790