predicate_debugger

adapt_tcl_operation_name(X,R) :- var(X),!,R=X.

adapt_tcl_operation_name('@PROPERTIES','$setup_constants') :- !.

adapt_tcl_operation_name('@INITIALISATION','$initialise_machine') :- !.

adapt_tcl_operation_name(X,X).

additional_time(301). % additional time given to account for variations in solving

assert_checked_property(P,ConstantsState,Time) :-
    assertz(checked_property(P)),
    (var(ConstantsState) -> print('NO SOLUTION'),nl
    ; retractall(last_checked_solution(_,_)),
    assertz(last_checked_solution(ConstantsState,Time))).

b_check_property_satisfiable(Properties,TypedConstants,ConstantsState,GlobalState) :-
    b_ast_cleanup:clean_up_pred(Properties,[],Pred),
    set_up_typed_localstate(TypedConstants,_FreshVars,TypedVals,[],ConstantsState,positive),
    b_interpreter_components:reset_component_info(false),
    append(ConstantsState,GlobalState,State),
    b_interpreter_components:b_trace_test_components(Pred,State,TypedVals),
    \+ b_interpreter_components:unsat_component_exists.

b_debug_find_first_unsat_property(Pred,Rest,Constants,GlobalState,TotalNr,AllowTimeout) :-
    is_a_conjunct(Pred,LHS,RHS),!,
    (b_debug_find_first_unsat_property(LHS,Rest,Constants,GlobalState,TotalNr,AllowTimeout)
    -> conjunct_predicates([Rest,LHS],Rest2),
    b_debug_find_first_unsat_property(RHS,Rest2,Constants,GlobalState,TotalNr,AllowTimeout)
    ; fail
).

b_debug_find_first_unsat_property(Prop,Rest,TypedConstants,GlobalState,TotalNr,AllowTimeout) :-
    nl,nl,flush_output(user),
    conjunct_predicates([Rest,Prop],Pred),
    (retract(cur_conjunct_nr(CurNr)) -> true ; CurNr=1), CurNrP1 is CurNr+1,
    assertz(cur_conjunct_nr(CurNrP1)),
    translate_bexpression(Prop,PT),
    format('~nCHECKING (~w/~w) OF: ~w~n',[CurNr,TotalNr,PT]),
    statistics(runtime,[Start,_]),
    (timeout_check_property(Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes)
    -> statistics(runtime,[Stop,_]), Time is Stop - Start,
    print_time(TimeOutRes,Time),
    format('~nINFO: ~w~n~n',[TimeOutRes]),
    (((\+ last_checked_solution(_,_) % we haven't found a solution yet
    ; AllowTimeout=allow_timeout),
    is_time_out_result(TimeOutRes))
    -> assertz(time_out_property(Prop,Time))
    ; is_time_out_failure(TimeOutRes)
    -> assertz(time_out_property(Prop,Time))
    ;
    assert_checked_property(Prop,ConstantsState,Time) % could also be timeout
    )
    ; statistics(runtime,[Stop,_]), Time is Stop - Start,
    assertz(failed_property(Prop,Time)),
    print('No Solution Found !! ('),print(Time), print(' ms)'),nl, flush_output(user),
    %print_bexpr(Pred),nl,
    fail
).

b_debug_goal :-
    bmachine:b_get_machine_goal(Goal),
    b_debug_predicate(Goal).

b_debug_operation(OpName) :-
    reset_debug_properties,
    get_current_state(OpName,CurID,CurBState),
    set_error_context(operation(OpName,CurID)),
    (get_operation_enabling_condition(OpName,Parameters,EnablingCondition,BSVars,_,true,false) -> true
    ; add_error(b_debug_operation,'Operation does not exist or cannot determine enabling condition: ',OpName),fail),!,
    print('Enabling: '), print_bexpr(EnablingCondition),nl,
    flush_output(user),
    nr_of_conjuncts(EnablingCondition,NrConj),
    insert_before_substitution_variables(BSVars,[],CurBState,CurBState,NewCurBState),
    extract_exists_parameters(EnablingCondition,Parameters,NewCond,NewParas),
    (b_debug_properties2(NewCond,NewParas,NewCurBState,NrConj,allow_timeout) -> true ; true).

b_debug_predicate(FullPred) :- set_error_context(b_debug_predicate),
    reset_debug_properties,
    get_parameters(FullPred,Params,Pred),
    get_current_state('@PRED',CurID,CurBState),
    set_error_context(b_debug_predicate(CurID)),
    nr_of_conjuncts(Pred,NrConj),
    (b_debug_properties2(Pred,Params,CurBState,NrConj,allow_timeout) -> true ; true).

b_debug_properties :- set_error_context(b_debug_properties),
    reset_debug_properties,
    %%b_extract_constants_and_properties(Constants,CstTypes,Properties),
    %b_machine_has_constants_or_properties,
    b_get_machine_constants(TypedConstants),
    get_adapted_properties(TypedConstants,AProperties,ATypedConstants,AllowTimeout),
    nr_of_conjuncts(AProperties,NrConj),
    (b_debug_properties2(AProperties,ATypedConstants,[],NrConj,AllowTimeout) -> true ; true).

b_debug_properties2(Pred,Constants,GlobalState,TotalNr,AllowTimeout) :-
    create_texpr(truth,pred,[b_debug_properties],Truth),
    retractall(last_debug_info(_,_)), assertz(last_debug_info(Constants,GlobalState)),
    (b_debug_find_first_unsat_property(Pred,Truth,Constants,GlobalState,TotalNr,AllowTimeout)
    -> print('ALL PROPERTIES SATISFIABLE'),nl
    ; true % get_preference(debug_try_minimise,false) -> true ; b_find_unsat_core(Constants,GlobalState)
).

b_debug_try_remove_props([],_,_,_,_,_,_) :- !.

b_debug_try_remove_props([],_,_,TypedConstants,GlobalState,Count,_) :- !, % for debug
    format('~nFINISHED (~w); CHECKING CORE~n',[Count]),
    get_unsat_core(Core),
    nl,translate:print_bexpr(Core),nl,
    (timeout_fast_check_property(unsat,Core,TypedConstants,_,GlobalState,TimeOutResC) -> true
    ; TimeOutResC = 'UNSAT'),
    format('~nCORE RESULT: ~w~n',[TimeOutResC]).

b_debug_try_remove_props([H|TSat],[H|TUnsat],Required,TypedConstants,GlobalState,Count,Total) :-
    append(Required,TSat,ConjunctsWithoutH),
    conjunct_predicates(ConjunctsWithoutH,SatPred),
    translate_bexpression(H,PT),
    format('~nCHECKING REMOVAL(~w/~w) OF: ~w~n',[Count,Total,PT]),
    (timeout_fast_check_property(sat,SatPred,TypedConstants,Sol,GlobalState,TimeOutResSat)
    -> (\+ is_time_out_result(TimeOutResSat)
    -> append(Required,TUnsat,ConjunctsWithoutH2),
    conjunct_predicates(ConjunctsWithoutH2,UnsatPred),
    ((timeout_fast_check_property(unsat,UnsatPred,TypedConstants,_,GlobalState,TimeOutRes),
    print(res(TimeOutRes)),nl,
    (is_time_out_result(TimeOutRes) -> \+ time_out_property(_,_) ; true)
    )
    -> print('Required for inconsistency : '), print(TimeOutRes),nl,
    append(Required,[H],NewRequired)
    ; /* H is not required for inconsistency/timeout */
    print('NOT required for INCONSISTENCY !'),nl,
    % print_bexpr(UnsatPred),nl,
    Required=NewRequired,
    % TO DO: update found solution
    (retract(last_checked_solution(_,LastTime)) -> true
    ; print('*** Could not remove last_checked_solution'),nl,
    preferences:get_computed_preference(debug_time_out,LastTime)
    ),
    assertz(last_checked_solution(Sol,LastTime)),
    (retract(checked_property(H)) -> true
    ; print('*** Could not remove checked_property: '), print(H),nl
    )
    )
    ; print('Required for efficiency'),nl,
    append(Required,[H],NewRequired)
    )
    ; nl,print('*** INTERNAL ERROR: FAILED'),nl,nl,
    append(Required,[H],NewRequired)
    ),
    C1 is Count+1,
    b_debug_try_remove_props(TSat,TUnsat,NewRequired,TypedConstants,GlobalState,C1,Total).

b_find_unsat_core :- /* assumes that b_debug_properties was run before */
    % b_machine_has_constants_or_properties,
    % b_get_machine_constants(TypedConstants),
    % b_get_properties_from_machine(Properties),!,
    % get_adapted_properties(TypedConstants,_AProperties,ATypedConstants),
    %b_find_unsat_core(ATypedConstants,[]).
    last_debug_info(Constants,GlobalState), b_find_unsat_core(Constants,GlobalState).

b_find_unsat_core(Constants,GlobalState) :-
    print('TRYING TO MINIMISE UNSATISFIABLE PROPERTIES'),nl,
    (last_checked_solution(_,Time)
    -> print(' Time for last solution in ms: '), print(Time), nl ; true),
    findall(P,checked_property(P),SatProps),
    (failed_property(FailProp,USTime) -> true
    ; time_out_property(FailProp,USTime) -> true
    ; add_error_fail(b_find_unsat_core,'No failed or timed-out property:',SatProps)),
    print(' Time for unsatisfiable conjuncts in ms: '), print(USTime), nl,
    append(SatProps,[FailProp],Props),
    length(SatProps,SL),
    b_debug_try_remove_props(SatProps,Props,[],Constants,GlobalState,1,SL).

extract_exists_parameters(Pred,Parameters, NewPred, NewParas) :-
    get_texpr_expr(Pred,exists(Vars,Body)),
    disjoint_list_union(Parameters,Vars,Paras1), !, % also checks if no clash exists; otherwise we have to keep exists
    extract_exists_parameters(Body,Paras1,NewPred,NewParas).

extract_exists_parameters(Pred,Parameters, NewPred, NewParas) :-
    get_texpr_expr(Pred,conjunct(LHS,RHS)),!,
    extract_exists_parameters(LHS,Parameters, NewLHS, IntParas),
    extract_exists_parameters(RHS,IntParas,NewRHS,NewParas),
    conjunct_predicates([NewLHS,NewRHS],NewPred).

extract_exists_parameters(Pred,Par,Pred,Par).

failed_or_time_out_property(P) :- failed_property(P,_) ; time_out_property(P,_).

fast_unsat_core.

get_adapted_properties(TypedConstants,Pred,CTypedConstants,do_not_allow_timeout) :-
    %(b_interpreter:nr_of_components(NrC), NrC>1),
    preferences:get_preference(partition_predicates,true),
    b_interpreter:get_unsat_component_predicate(CompNr,Pred,Vars),!, % means there was no timeout
    assertz(projection_onto_component(CompNr)),
    print(debugging_unsat_or_skipped_component(CompNr)),nl,
    print(component_vars(Vars)),nl,
    project_texpr_identifiers(TypedConstants,Vars,CTypedConstants).

get_adapted_properties(TypedConstants,Properties,TypedConstants,allow_timeout) :-
    % TO DO determine whether timeout occured
    b_get_properties_from_machine(Properties).

get_current_state(OpName,CurID,CurBState) :-
    (current_expression(CurID,CurState) -> true
    ; add_error(predicate_debugger,'Could not get current state',OpName),fail),
    (state_corresponds_to_initialised_b_machine(CurState,CurBState) -> true
    ; (OpName=='$initialise_machine',
    state_corresponds_to_set_up_constants(CurState,CurBState)) -> true
    ; add_error(b_debug_operation,'Machine not yet initialised! ',CurState),fail).

get_parameters(b(exists(Parameters,Pred),pred,_),Parameters,Pred) :- !.

get_parameters(Pred,[],Pred).

get_timeout(sat,DebugTimeOut) :-
    last_checked_solution(_,LTime),
    !,
    additional_time(AT),
    DebugTimeOut is LTime+AT.

get_timeout(unsat,DebugTimeOut) :-
    last_unsat_time(USTime),
    last_checked_solution(_,LSTime),
    (fast_unsat_core -> TT is min(USTime,LSTime) ; TT is max(USTime,LSTime)),
    !,
    additional_time(AT),
    DebugTimeOut is TT+AT.

get_timeout(S,DebugTimeOut) :- print('*** Could not get TimeOut : '), print(S),nl,
    preferences:get_preference(time_out,CurTO), DebugTimeOut is CurTO * 1.

get_unsat_core(AllConj) :- (checked_property(_) ; failed_or_time_out_property(_)), !,
    findall(P,checked_property(P),Ps),
    findall(UnsatP,failed_or_time_out_property(UnsatP),UPs),
    append(Ps,UPs,All),
    conjunct_predicates(All,AllConj).

get_unsat_core(Core) :- print('No predicate debugger analysis run'),nl,
    print('Trying to extract from b_interpreter'),nl,
    b_interpreter:get_unsat_component_predicate(_,Core,_Vars),!.

get_unsat_core(b(truth,pred,[])).

is_time_out_failure(virtual_time_out(failure_enumeration_warning(_,_,_,_,_))).

last_unsat_time(Time) :- time_out_property(_,Time) -> true ; failed_property(_,Time).

nr_of_conjuncts(Pred,Nr) :-
    is_a_conjunct(Pred,LHS,RHS),!,
    nr_of_conjuncts(LHS,NrL),
    nr_of_conjuncts(RHS,NrR),
    Nr is NrL+NrR.

nr_of_conjuncts(_,1).

print_time(TimeOutRes,Time) :- is_time_out_result(TimeOutRes),!,
    (TimeOutRes=virtual_time_out(_) -> print('VIRTUAL ') ; true),
    print('TIMEOUT !! ('),print(Time), print(' ms)'),nl, flush_output(user).

print_time(_TimeOutRes,Time) :-
    print('OK ('), print(Time), print(' ms)'), flush_output(user).

project_texpr_identifiers([],_,[]).

project_texpr_identifiers([TID|T],Vars,Res) :-
    (get_texpr_id(TID,ID),member(ID,Vars)
    -> Res = [TID|R2] ; Res=R2),
    project_texpr_identifiers(T,Vars,R2).

reset_debug_properties :-
    retractall(last_debug_info(_,_)),
    retractall(checked_property(_)),
    retractall(last_checked_solution(_,_)),
    retractall(failed_property(_,_)),
    retractall(time_out_property(_,_)),
    retractall(cur_conjunct_nr(_)),
    retractall(projection_onto_component(_)).

set_fast_unsat_core(T) :- retractall(fast_unsat_core),
    (T==fast -> assertz(fast_unsat_core) ; true).

tcltk_debug_properties(RealRes,UnsatCore,Satisfiable) :-
    tcltk_debug_properties_or_op('@PROPERTIES',UnsatCore,RealRes,Satisfiable).

tcltk_debug_properties_or_op(TclOpName,ComputeUnsatCore,list(RealRes),Satisfiable) :-
    adapt_tcl_operation_name(TclOpName,OpName),
    print(tcltk_debug_properties_or_op(OpName,ComputeUnsatCore,RealRes)),nl,
    (ComputeUnsatCore==false ->
    (OpName='$setup_constants' -> b_debug_properties
    ; OpName = '@GOAL' -> b_debug_goal
    ; b_debug_operation(OpName))
    ; set_fast_unsat_core(ComputeUnsatCore),
    print('*** Finding Unsat Core : '), print(ComputeUnsatCore),nl,
    (b_find_unsat_core
    -> print('*** Finished '),nl
    ; add_error_fail(predicate_debugger,'Finding Unsat Core failed',OpName))
    ),
    print(debugged(OpName)),nl,
    findall(TP, (checked_property(P),
    translate_bexpression_with_limit(P,TrP),
    ajoin([TrP,' &\n'],TP)),
    Res1),
    (projection_onto_component(_SubNr)
    -> Res1P = ['(only a sub-component was analysed)\n'|Res1] ; Res1P=Res1),
    (Res1=[] -> R1=Res1P ;
    R1=['\n ********\n\nSATISFIABLE CONSTRAINTS and PROPERTIES:\n'|Res1P]
    ),
    findall(TP2,( (failed_property(P,_),TRES='false' ; time_out_property(P,_),TRES='time_out'),
    translate_status(P,TRES,TP2)),
    Res2),
    (Res2=[] -> R2=['\nNo unsatisfiable PROPERTY or CONSTRAINT'], Satisfiable=true
    ; R2=['\n ********\n\nFirst unsatisfiable PROPERTY or CONSTRAINT:\n'|Res2],
    Satisfiable=false
    ),
    findall(TP, (last_checked_solution(ConstantsState,_), % TO DO: Project on remaining variables !?
    translate_equivalence(b(identifier('SOLUTION'),boolean,[]),ConstantsState,TP)),
    Res12),
    append(R2,['\n\n ********\n\nSolution for satisfiable part:\n'|Res12],R2Res12),
    append(R1,R2Res12,Res),
    findall(SetDescr,(b_global_set(Set),b_fd_card(Set,Card),
    create_texpr(identifier(Set),set(global(Set)),[],SetId),
    create_texpr(card(SetId),integer,[],CardExpr),
    create_texpr(value(int(Card)),integer,[],ValExpr),
    create_texpr(equal(CardExpr,ValExpr),prop,[],EqualExpr),
    translate_bexpression(EqualExpr,SetDescr1),
    (unfixed_deferred_set(Set) -> Xtra = ' (assumed for deferred set)' ; Xtra=''),
    ajoin([SetDescr1,Xtra,'\n'],SetDescr)), Sets),
   
    append(['\nCardinalities of SETS:\n'|Sets],Res,SRes),
    preferences:get_preference(minint,MININT),
    preferences:get_preference(maxint,MAXINT),
    clear_error_context,
    ajoin(['MININT .. MAXINT = ',MININT,'..',MAXINT],MINMAX),
    RealRes = ['SETTINGS:\n',MINMAX|SRes].

tcltk_debug_properties_or_op([],_,list(['Machine has no PROPERTIES']),true).

tcltk_get_unsat_core_with_types(ResultCodes) :-
    get_unsat_core(AllConj),
    translate_predicate_into_machine(AllConj,'UnsatCore',ResultAtom),
    write_to_codes(ResultAtom,ResultCodes).

timeout_check_property(Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes) :-
    preferences:get_computed_preference(debug_time_out,DebugTimeOut),
    timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState,DebugTimeOut,TimeOutRes),
    % Note: will translate failure with enumeration warning into virtual_timeout; see is_time_out_failure above
    format('~nCHECKING RESULT is: ~w~n',[TimeOutRes]).

timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState, DebugTimeOut,TimeOutRes) :-
    catch(
    time_out_with_enum_warning_one_solution(
    b_check_property_satisfiable(Pred,TypedConstants,ConstantsState,GlobalState),
    DebugTimeOut,TimeOutRes),
    E,
    TimeOutRes = virtual_time_out(exception(E))). % probably CLPFD overflow

timeout_fast_check_property(ExpectSat,Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes) :-
    get_timeout(ExpectSat,DebugTimeOut),
    % print(time_out_value(DebugTimeOut)),nl,
    % print_bexpr(Pred),nl,
    statistics(runtime,[Start,_]),
    timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState,DebugTimeOut,TimeOutRes),
    statistics(runtime,[Stop,_]), Time is Stop - Start, print(time(Time)),nl,
    (is_time_out_result(TimeOutRes) -> print(time_out_occurred(Time,DebugTimeOut)),nl,
    (debug:debug_mode(on) -> print_bexpr(Pred),nl ; true)
    ; true).

translate_equivalence(A,B,R) :-
    translate_bexpression(A,TA),
    translate_bstate(B,TB),
    ajoin([TA,'\n == ',TB,'\n'],R).

translate_status(A,Status,R) :-
    translate_bexpression(A,TA),
    (translate_span(A,ASpan)
    -> ajoin([TA,'\n == ',Status,' ',ASpan],R)
    ; ajoin([TA,'\n == ',Status],R)).