1		% (c) 2009-2026 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 (debug_properties DEPRECATED) :
6		% it is planned to replace the debug_properties commands using the unsat_cores.pl predicates
7		% operation enabling code should be moved to a separate module
8
9		:- module(predicate_debugger,[tcltk_debug_properties/3,
10		tcltk_debug_properties_or_op/4,
11		tcltk_get_unsat_core_with_types/1]).
12
13
14		:- use_module(probsrc(tools)).
15
16		:- use_module(probsrc(module_information),[module_info/2]).
17		:- module_info(group,misc).
18		:- module_info(description,'The predicate debugger adds conjuncts one by one until the predicate becomes unsatisfiable.').
19
20		:- use_module(probsrc(debug)).
21		:- use_module(probsrc(self_check)).
22		:- use_module(probsrc(preferences)).
23		:- use_module(probsrc(error_manager)).
24
25		:- use_module(probsrc(translate)).
26		:- use_module(probsrc(b_interpreter)).
27		:- use_module(probsrc(bsyntaxtree)).
28		:- use_module(probsrc(b_ast_cleanup)).
29
30		:- use_module(library(timeout)).
31		:- use_module(library(lists)).
32
33		:- use_module(probsrc(b_operation_guards),[get_operation_enabling_condition/7]).
34
35
36		/* b_interpreter:b_debug_properties. */
37
38		:- volatile checked_property/1, last_checked_solution/2, failed_property/2, time_out_property/2, cur_conjunct_nr/1, projection_onto_component/1.
39		:- dynamic checked_property/1.
40		:- dynamic last_checked_solution/2.
41		:- dynamic failed_property/2.
42		:- dynamic time_out_property/2.
43		:- dynamic cur_conjunct_nr/1.
44		:- dynamic projection_onto_component/1.
45
46		reset_debug_properties :-
47		retractall(last_debug_info(_,_)),
48		retractall(checked_property(_)),
49		retractall(last_checked_solution(_,_)),
50		retractall(failed_property(_,_)),
51		retractall(time_out_property(_,_)),
52		retractall(cur_conjunct_nr(_)),
53		retractall(projection_onto_component(_)).
54
55		:- use_module(probsrc(b_global_sets),[b_global_set/1, b_fd_card/2, unfixed_deferred_set/1]).
56		tcltk_debug_properties(RealRes,UnsatCore,Satisfiable) :-
57		tcltk_debug_properties_or_op('@PROPERTIES',UnsatCore,RealRes,Satisfiable).
58
59		% code below because names with $ cause problems in Tcl with eval
60		% code duplicated from tcltk_interface; but predicate debugger is deprecated anyway
61		adapt_tcl_operation_name(X,R) :- var(X),!,R=X.
62		adapt_tcl_operation_name('@PROPERTIES','$setup_constants') :- !.
63		adapt_tcl_operation_name('@INITIALISATION','$initialise_machine') :- !.
64		adapt_tcl_operation_name(X,X).
65
66		tcltk_debug_properties_or_op(TclOpName,ComputeUnsatCore,list(RealRes),Satisfiable) :-
67		adapt_tcl_operation_name(TclOpName,OpName),
68		print(tcltk_debug_properties_or_op(OpName,ComputeUnsatCore,RealRes)),nl,
69		(ComputeUnsatCore==false ->
70		(OpName='$setup_constants' -> b_debug_properties
71		; OpName = '@GOAL' -> b_debug_goal
72		; b_debug_operation(OpName))
73		; set_fast_unsat_core(ComputeUnsatCore),
74		print('*** Finding Unsat Core : '), print(ComputeUnsatCore),nl,
75		(b_find_unsat_core
76		-> print('*** Finished '),nl
77		; add_error_fail(predicate_debugger,'Finding Unsat Core failed',OpName))
78		),
79		print(debugged(OpName)),nl,
80		findall(TP, (checked_property(P),
81		translate_bexpression_with_limit(P,TrP),
82		ajoin([TrP,' &\n'],TP)),
83		Res1),
84		(projection_onto_component(_SubNr)
85		-> Res1P = ['(only a sub-component was analysed)\n'|Res1] ; Res1P=Res1),
86		(Res1=[] -> R1=Res1P ;
87		R1=['\n ********\n\nSATISFIABLE CONSTRAINTS and PROPERTIES:\n'|Res1P]
88		),
89		findall(TP2,( (failed_property(P,_),TRES='false' ; time_out_property(P,_),TRES='time_out'),
90		translate_status(P,TRES,TP2)),
91		Res2),
92		(Res2=[] -> R2=['\nNo unsatisfiable PROPERTY or CONSTRAINT'], Satisfiable=true
93		; R2=['\n ********\n\nFirst unsatisfiable PROPERTY or CONSTRAINT:\n'|Res2],
94		Satisfiable=false
95		),
96		findall(TP, (last_checked_solution(ConstantsState,_), % TO DO: Project on remaining variables !?
97		translate_equivalence(b(identifier('SOLUTION'),boolean,[]),ConstantsState,TP)),
98		Res12),
99		append(R2,['\n\n ********\n\nSolution for satisfiable part:\n'|Res12],R2Res12),
100		append(R1,R2Res12,Res),
101		findall(SetDescr,(b_global_set(Set),b_fd_card(Set,Card),
102		create_texpr(identifier(Set),set(global(Set)),[],SetId),
103		create_texpr(card(SetId),integer,[],CardExpr),
104		create_texpr(value(int(Card)),integer,[],ValExpr),
105		create_texpr(equal(CardExpr,ValExpr),prop,[],EqualExpr),
106		translate_bexpression(EqualExpr,SetDescr1),
107		(unfixed_deferred_set(Set) -> Xtra = ' (assumed for deferred set)' ; Xtra=''),
108		ajoin([SetDescr1,Xtra,'\n'],SetDescr)), Sets),
109
110		append(['\nCardinalities of SETS:\n'|Sets],Res,SRes),
111		preferences:get_preference(minint,MININT),
112		preferences:get_preference(maxint,MAXINT),
113		clear_error_context,
114		ajoin(['MININT .. MAXINT = ',MININT,'..',MAXINT],MINMAX),
115		RealRes = ['SETTINGS:\n',MINMAX|SRes].
116		tcltk_debug_properties_or_op([],_,list(['Machine has no PROPERTIES']),true).
117
118		failed_or_time_out_property(P) :- failed_property(P,_) ; time_out_property(P,_).
119
120		:- use_module(library(codesio),[write_to_codes/2]).
121		:- use_module(probsrc(tools),[ajoin/2]).
122		% use_module(probsrc(predicate_debugger)),predicate_debugger:print_unsat_core_with_types
123		tcltk_get_unsat_core_with_types(ResultCodes) :-
124		get_unsat_core(AllConj),
125		translate_predicate_into_machine(AllConj,'UnsatCore',ResultAtom),
126		write_to_codes(ResultAtom,ResultCodes).
127
128		get_unsat_core(AllConj) :- (checked_property(_) ; failed_or_time_out_property(_)), !,
129		findall(P,checked_property(P),Ps),
130		findall(UnsatP,failed_or_time_out_property(UnsatP),UPs),
131		append(Ps,UPs,All),
132		conjunct_predicates(All,AllConj).
133		get_unsat_core(Core) :- print('No predicate debugger analysis run'),nl,
134		print('Trying to extract from b_interpreter'),nl,
135		b_interpreter:get_unsat_component_predicate(_,Core,_Vars),!.
136		get_unsat_core(b(truth,pred,[])).
137
138
139		translate_equivalence(A,B,R) :-
140		translate_bexpression(A,TA),
141		translate_bstate(B,TB),
142		ajoin([TA,'\n == ',TB,'\n'],R).
143		:- use_module(probsrc(translate),[translate_span/2]).
144		translate_status(A,Status,R) :-
145		translate_bexpression(A,TA),
146		(translate_span(A,ASpan)
147		-> ajoin([TA,'\n == ',Status,' ',ASpan],R)
148		; ajoin([TA,'\n == ',Status],R)).
149
150
151
152		:- use_module(probsrc(bmachine)).
153		b_debug_properties :- set_error_context(b_debug_properties),
154		reset_debug_properties,
155		%%b_extract_constants_and_properties(Constants,CstTypes,Properties),
156		%b_machine_has_constants_or_properties,
157		b_get_machine_constants(TypedConstants),
158		get_adapted_properties(TypedConstants,AProperties,ATypedConstants,AllowTimeout),
159		nr_of_conjuncts(AProperties,NrConj),
160		(b_debug_properties2(AProperties,ATypedConstants,[],NrConj,AllowTimeout) -> true ; true).
161
162		b_debug_goal :-
163		bmachine:b_get_machine_goal(Goal),
164		b_debug_predicate(Goal).
165		b_debug_predicate(FullPred) :- set_error_context(b_debug_predicate),
166		reset_debug_properties,
167		get_parameters(FullPred,Params,Pred),
168		get_current_state('@PRED',CurID,CurBState),
169		set_error_context(b_debug_predicate(CurID)),
170		nr_of_conjuncts(Pred,NrConj),
171		(b_debug_properties2(Pred,Params,CurBState,NrConj,allow_timeout) -> true ; true).
172
173		get_parameters(b(exists(Parameters,Pred),pred,_),Parameters,Pred) :- !.
174		get_parameters(Pred,[],Pred).
175
176		:- use_module(library(lists)).
177		get_adapted_properties(TypedConstants,Pred,CTypedConstants,do_not_allow_timeout) :-
178		preferences:get_preference(partition_predicates,true),
179		b_interpreter:get_unsat_component_predicate(CompNr,Pred,Vars),!, % means there was no timeout
180		assertz(projection_onto_component(CompNr)),
181		print(debugging_unsat_or_skipped_component(CompNr)),nl,
182		print(component_vars(Vars)),nl,
183		project_texpr_identifiers(TypedConstants,Vars,CTypedConstants).
184		get_adapted_properties(TypedConstants,Properties,TypedConstants,allow_timeout) :-
185		% TO DO determine whether timeout occured
186		b_get_properties_from_machine(Properties).
187
188
189		% only keep texpr_identifiers whose id is in the provided list
190		project_texpr_identifiers([],_,[]).
191		project_texpr_identifiers([TID|T],Vars,Res) :-
192		(get_texpr_id(TID,ID),member(ID,Vars)
193		-> Res = [TID|R2] ; Res=R2),
194		project_texpr_identifiers(T,Vars,R2).
195
196		:- use_module(probsrc(specfile),[state_corresponds_to_initialised_b_machine/2, state_corresponds_to_set_up_constants/2]).
197		/* b_interpreter:tcltk_debug_properties_or_op(prog1,R)*/
198		b_debug_operation(OpName) :-
199		reset_debug_properties,
200		get_current_state(OpName,CurID,CurBState),
201		set_error_context(operation(OpName,CurID)),
202		(get_operation_enabling_condition(OpName,Parameters,EnablingCondition,BSVars,_,true,false) -> true
203		; add_error(b_debug_operation,'Operation does not exist or cannot determine enabling condition: ',OpName),fail),!,
204		print('Enabling: '), print_bexpr(EnablingCondition),nl,
205		flush_output(user),
206		nr_of_conjuncts(EnablingCondition,NrConj),
207		insert_before_substitution_variables(BSVars,[],CurBState,CurBState,NewCurBState),
208		extract_exists_parameters(EnablingCondition,Parameters,NewCond,NewParas),
209		(b_debug_properties2(NewCond,NewParas,NewCurBState,NrConj,allow_timeout) -> true ; true).
210
211		:- use_module(probsrc(state_space),[current_expression/2]).
212		get_current_state(OpName,CurID,CurBState) :-
213		(current_expression(CurID,CurState) -> true
214		; add_error(predicate_debugger,'Could not get current state',OpName),fail),
215		(state_corresponds_to_initialised_b_machine(CurState,CurBState) -> true
216		; (OpName=='$initialise_machine',
217		state_corresponds_to_set_up_constants(CurState,CurBState)) -> true
218		; add_error(b_debug_operation,'Machine not yet initialised! ',CurState),fail).
219
220
221		% Try to lift out existentially quantified variables to the outer level; to make the debugging more fine-grained
222		extract_exists_parameters(Pred,Parameters, NewPred, NewParas) :-
223		get_texpr_expr(Pred,exists(Vars,Body)),
224		disjoint_list_union(Parameters,Vars,Paras1), !, % also checks if no clash exists; otherwise we have to keep exists
225		extract_exists_parameters(Body,Paras1,NewPred,NewParas).
226		extract_exists_parameters(Pred,Parameters, NewPred, NewParas) :-
227		get_texpr_expr(Pred,conjunct(LHS,RHS)),!,
228		extract_exists_parameters(LHS,Parameters, NewLHS, IntParas),
229		extract_exists_parameters(RHS,IntParas,NewRHS,NewParas),
230		conjunct_predicates([NewLHS,NewRHS],NewPred).
231		extract_exists_parameters(Pred,Par,Pred,Par).
232
233		% -----------------------------------------
234
235		:- use_module(library(timeout)).
236
237
238		nr_of_conjuncts(Pred,Nr) :-
239		is_a_conjunct(Pred,LHS,RHS),!,
240		nr_of_conjuncts(LHS,NrL),
241		nr_of_conjuncts(RHS,NrR),
242		Nr is NrL+NrR.
243		nr_of_conjuncts(_,1).
244
245		:- volatile last_debug_info/2.
246		:- dynamic last_debug_info/2.
247		b_debug_properties2(Pred,Constants,GlobalState,TotalNr,AllowTimeout) :-
248		create_texpr(truth,pred,[b_debug_properties],Truth),
249		retractall(last_debug_info(_,_)), assertz(last_debug_info(Constants,GlobalState)),
250		(b_debug_find_first_unsat_property(Pred,Truth,Constants,GlobalState,TotalNr,AllowTimeout)
251		-> print('ALL PROPERTIES SATISFIABLE'),nl
252		; true % get_preference(debug_try_minimise,false) -> true ; b_find_unsat_core(Constants,GlobalState)
253		).
254
255		b_find_unsat_core :- /* assumes that b_debug_properties was run before */
256		% b_machine_has_constants_or_properties,
257		% b_get_machine_constants(TypedConstants),
258		% b_get_properties_from_machine(Properties),!,
259		% get_adapted_properties(TypedConstants,_AProperties,ATypedConstants),
260		%b_find_unsat_core(ATypedConstants,[]).
261		last_debug_info(Constants,GlobalState), b_find_unsat_core(Constants,GlobalState).
262		b_find_unsat_core(Constants,GlobalState) :-
263		print('TRYING TO MINIMISE UNSATISFIABLE PROPERTIES'),nl,
264		(last_checked_solution(_,Time)
265		-> print(' Time for last solution in ms: '), print(Time), nl ; true),
266		findall(P,checked_property(P),SatProps),
267		(failed_property(FailProp,USTime) -> true
268		; time_out_property(FailProp,USTime) -> true
269		; add_error_fail(b_find_unsat_core,'No failed or timed-out property:',SatProps)),
270		print(' Time for unsatisfiable conjuncts in ms: '), print(USTime), nl,
271		append(SatProps,[FailProp],Props),
272		length(SatProps,SL),
273		b_debug_try_remove_props(SatProps,Props,[],Constants,GlobalState,1,SL).
274		% TO DO: partition into components; try removing compnents without FailProp
275
276		b_debug_try_remove_props([],_,_,_,_,_,_) :- !.
277		b_debug_try_remove_props([],_,_,TypedConstants,GlobalState,Count,_) :- !, % for debug
278		format('~nFINISHED (~w); CHECKING CORE~n',[Count]),
279		get_unsat_core(Core),
280		nl,translate:print_bexpr(Core),nl,
281		(timeout_fast_check_property(unsat,Core,TypedConstants,_,GlobalState,TimeOutResC) -> true
282		; TimeOutResC = 'UNSAT'),
283		format('~nCORE RESULT: ~w~n',[TimeOutResC]).
284		b_debug_try_remove_props([H|TSat],[H|TUnsat],Required,TypedConstants,GlobalState,Count,Total) :-
285		append(Required,TSat,ConjunctsWithoutH),
286		conjunct_predicates(ConjunctsWithoutH,SatPred),
287		translate_bexpression(H,PT),
288		format('~nCHECKING REMOVAL(~w/~w) OF: ~w~n',[Count,Total,PT]),
289		(timeout_fast_check_property(sat,SatPred,TypedConstants,Sol,GlobalState,TimeOutResSat)
290		-> (\+ is_time_out_result(TimeOutResSat)
291		-> append(Required,TUnsat,ConjunctsWithoutH2),
292		conjunct_predicates(ConjunctsWithoutH2,UnsatPred),
293		((timeout_fast_check_property(unsat,UnsatPred,TypedConstants,_,GlobalState,TimeOutRes),
294		print(res(TimeOutRes)),nl,
295		(is_time_out_result(TimeOutRes) -> \+ time_out_property(_,_) ; true)
296		)
297		-> print('Required for inconsistency : '), print(TimeOutRes),nl,
298		append(Required,[H],NewRequired)
299		; /* H is not required for inconsistency/timeout */
300		print('NOT required for INCONSISTENCY !'),nl,
301		% print_bexpr(UnsatPred),nl,
302		Required=NewRequired,
303		% TO DO: update found solution
304		(retract(last_checked_solution(_,LastTime)) -> true
305		; print('*** Could not remove last_checked_solution'),nl,
306		preferences:get_computed_preference(debug_time_out,LastTime)
307		),
308		assertz(last_checked_solution(Sol,LastTime)),
309		(retract(checked_property(H)) -> true
310		; print('*** Could not remove checked_property: '), print(H),nl
311		)
312		)
313		; print('Required for efficiency'),nl,
314		append(Required,[H],NewRequired)
315		)
316		; nl,print('*** INTERNAL ERROR: FAILED'),nl,nl,
317		append(Required,[H],NewRequired)
318		),
319		C1 is Count+1,
320		b_debug_try_remove_props(TSat,TUnsat,NewRequired,TypedConstants,GlobalState,C1,Total).
321
322		b_debug_find_first_unsat_property(Pred,Rest,Constants,GlobalState,TotalNr,AllowTimeout) :-
323		is_a_conjunct(Pred,LHS,RHS),!,
324		(b_debug_find_first_unsat_property(LHS,Rest,Constants,GlobalState,TotalNr,AllowTimeout)
325		-> conjunct_predicates([Rest,LHS],Rest2),
326		b_debug_find_first_unsat_property(RHS,Rest2,Constants,GlobalState,TotalNr,AllowTimeout)
327		; fail
328		).
329		b_debug_find_first_unsat_property(Prop,Rest,TypedConstants,GlobalState,TotalNr,AllowTimeout) :-
330		nl,nl,flush_output(user),
331		conjunct_predicates([Rest,Prop],Pred),
332		(retract(cur_conjunct_nr(CurNr)) -> true ; CurNr=1), CurNrP1 is CurNr+1,
333		assertz(cur_conjunct_nr(CurNrP1)),
334		translate_bexpression(Prop,PT),
335		format('~nCHECKING (~w/~w) OF: ~w~n',[CurNr,TotalNr,PT]),
336		statistics(runtime,[Start,_]),
337		(timeout_check_property(Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes)
338		-> statistics(runtime,[Stop,_]), Time is Stop - Start,
339		print_time(TimeOutRes,Time),
340		format('~nINFO: ~w~n~n',[TimeOutRes]),
341		(((\+ last_checked_solution(_,_) % we haven't found a solution yet
342		; AllowTimeout=allow_timeout),
343		is_time_out_result(TimeOutRes))
344		-> assertz(time_out_property(Prop,Time))
345		; is_time_out_failure(TimeOutRes)
346		-> assertz(time_out_property(Prop,Time))
347		;
348		assert_checked_property(Prop,ConstantsState,Time) % could also be timeout
349		)
350		; statistics(runtime,[Stop,_]), Time is Stop - Start,
351		assertz(failed_property(Prop,Time)),
352		print('No Solution Found !! ('),print(Time), print(' ms)'),nl, flush_output(user),
353		%print_bexpr(Pred),nl,
354		fail
355		).
356
357		is_time_out_failure(virtual_time_out(failure_enumeration_warning(_,_,_,_,_))).
358
359		print_time(TimeOutRes,Time) :- is_time_out_result(TimeOutRes),!,
360		(TimeOutRes=virtual_time_out(_) -> print('VIRTUAL ') ; true),
361		print('TIMEOUT !! ('),print(Time), print(' ms)'),nl, flush_output(user).
362		print_time(_TimeOutRes,Time) :-
363		print('OK ('), print(Time), print(' ms)'), flush_output(user).
364
365
366		last_unsat_time(Time) :- time_out_property(_,Time) -> true ; failed_property(_,Time).
367
368		set_fast_unsat_core(T) :- retractall(fast_unsat_core),
369		(T==fast -> assertz(fast_unsat_core) ; true).
370		:- dynamic fast_unsat_core/0.
371		fast_unsat_core.
372
373		additional_time(301). % additional time given to account for variations in solving
374		%additional_time(1301).
375
376		get_timeout(sat,DebugTimeOut) :-
377		last_checked_solution(_,LTime),
378		!,
379		additional_time(AT),
380		DebugTimeOut is LTime+AT.
381		get_timeout(unsat,DebugTimeOut) :-
382		last_unsat_time(USTime),
383		last_checked_solution(_,LSTime),
384		(fast_unsat_core -> TT is min(USTime,LSTime) ; TT is max(USTime,LSTime)),
385		!,
386		additional_time(AT),
387		DebugTimeOut is TT+AT.
388		get_timeout(S,DebugTimeOut) :- print('*** Could not get TimeOut : '), print(S),nl,
389		preferences:get_preference(time_out,CurTO), DebugTimeOut is CurTO * 1.
390
391
392		timeout_fast_check_property(ExpectSat,Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes) :-
393		get_timeout(ExpectSat,DebugTimeOut),
394		% print(time_out_value(DebugTimeOut)),nl,
395		% print_bexpr(Pred),nl,
396		statistics(runtime,[Start,_]),
397		timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState,DebugTimeOut,TimeOutRes),
398		statistics(runtime,[Stop,_]), Time is Stop - Start, print(time(Time)),nl,
399		(is_time_out_result(TimeOutRes) -> print(time_out_occurred(Time,DebugTimeOut)),nl,
400		(debug:debug_mode(on) -> print_bexpr(Pred),nl ; true)
401		; true).
402
403		timeout_check_property(Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes) :-
404		preferences:get_computed_preference(debug_time_out,DebugTimeOut),
405		timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState,DebugTimeOut,TimeOutRes),
406		% Note: will translate failure with enumeration warning into virtual_timeout; see is_time_out_failure above
407		format('~nCHECKING RESULT is: ~w~n',[TimeOutRes]).
408
409		timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState, DebugTimeOut,TimeOutRes) :-
410		catch(
411		time_out_with_enum_warning_one_solution(
412		b_check_property_satisfiable(Pred,TypedConstants,ConstantsState,GlobalState),
413		DebugTimeOut,TimeOutRes),
414		E,
415		TimeOutRes = virtual_time_out(exception(E))). % probably CLPFD overflow
416
417
418		assert_checked_property(P,ConstantsState,Time) :-
419		assertz(checked_property(P)),
420		(var(ConstantsState) -> print('NO SOLUTION'),nl
421		; retractall(last_checked_solution(_,_)),
422		assertz(last_checked_solution(ConstantsState,Time))).
423
424		:- use_module(probsrc(kernel_waitflags)).
425		:- use_module(probsrc(b_enumerate)).
426
427		% TO DO: call something which will use predicate_components
428
429		b_check_property_satisfiable(Properties,TypedConstants,ConstantsState,GlobalState) :-
430		b_ast_cleanup:clean_up_pred(Properties,[],Pred),
431		set_up_typed_localstate(TypedConstants,_FreshVars,TypedVals,[],ConstantsState,positive),
432		b_interpreter_components:reset_component_info(false),
433		append(ConstantsState,GlobalState,State),
434		b_interpreter_components:b_trace_test_components(Pred,State,TypedVals),
435		\+ b_interpreter_components:unsat_component_exists.
436
437
438