disprover

check_negated(NegatedGoal,Hypotheses,_,FullOrigPredicate,Opts,ResultOut) :-
    create_negation(NegatedGoal,Goal),
    conjunct_predicates([Goal|Hypotheses],Predicate),
    %tools:print_bt_message(check_negated),
    debug_println(20,'Check whether we can also prove negation of goal'),
    solve_disprover_predicate(prob_check_negated_goal,Predicate,Opts,Result),
    %% tools:print_bt_message(solver_double_check_result(Result)),
    !,
    (Result = contradiction_found % proven both (H & not G) and (H & G)
    -> ResultOut = contradiction_in_hypotheses,
    translate:translate_bexpression_with_limit(NegatedGoal,GS),
    add_warning(disprover_inconsistent_hypotheses,
    'Disprover double check result: Contradiction in hypotheses (or Bug) detected for goal: ',
    GS), %% check_negated(NegatedGoal,Hypotheses))
    % translate:nested_print_bexpr_as_classicalb(Hypotheses),nl,nl,
    compute_unsat_core_if_requested(Predicate,Opts)
    % ; Result=solution(Bindings), format('Solution for negated goal:~n',[]), member(B,Bindings), print_binding(B),fail
    ; ResultOut = contradiction_found,
    compute_unsat_core_if_requested(FullOrigPredicate,Opts)
).

check_options([]) :- !.

check_options([O|T]) :- !, (valid_option(O) -> true ; add_warning(disprover,'Illegal disprover option: ',O)),
    check_options(T).

check_options(O) :- add_internal_error('Illegal disprover options: ',check_options(O)).

compute_unsat_core(Opts,Predicate) :-
    (member(unsat_core_algorithm/P,Opts)
    -> call_with_preference(compute_unsat_core_aux(Predicate,CorePredicate),unsat_core_algorithm,P)
    ; compute_unsat_core_aux(Predicate,CorePredicate)),
    !,
    print('UNSAT CORE: '),nl,print('--------'),nl,
    (member(disprover_option(unsat_core_as_machine),Opts)
    -> translate_predicate_into_machine(CorePredicate,'UnsatCore',ResultAtom),
    write(ResultAtom),nl
    ; nested_print_bexpr_as_classicalb(CorePredicate)),
    nl, print('--------'),nl.

compute_unsat_core_aux(Predicate,CorePredicate) :-
    print('Computing UNSAT CORE'),nl,
    unsat_core(Predicate,CorePredicate). % from unsat_cores

compute_unsat_core_if_requested(Predicate,Opts) :-
    (member(disprover_option(unsat_core),Opts) -> compute_unsat_core(Opts,Predicate) ; true).

disprove(Goal,AllHypotheses,SelectedHypotheses,Timeout,OutResult) :-
    get_disprover_default_opts(Opts),
    % Note: disprover_mode is always set to true
    disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,Timeout,Opts,OutResult).

disprove1(Goal,AllHypotheses,SelectedHypotheses,Opts,Result) :-
    catch(
    (disprove2(Goal,AllHypotheses,SelectedHypotheses,Opts,Result) -> true
    ; add_internal_error('Disprover failed on goal:',Goal),
    fail),
    type_errors(E),
    (add_all_perrors(E,[],disprover), Result=type_error)).

disprove2(Goal,AllHypotheses,SelectedHypotheses,Opts,ResultOut) :-
    (type_check_in_machine_context([Goal|AllHypotheses],[TGoal|TAllHypotheses]) -> true
    ; add_error_and_fail(disprover,'Disprover typechecking goal failed')),
    (type_check_in_machine_context(SelectedHypotheses,TSelectedHypotheses) -> true
    ; add_error_and_fail(disprover,'Disprover typechecking selected hyps failed')),
    disprove3(TGoal,TAllHypotheses,TSelectedHypotheses,Opts,ResultOut).

disprove3(TGoal,TAllHypotheses,TSelectedHypotheses,Opts,ResultOut) :-
    % build predicate H1 & H2 .... & not Goal
    create_negation(TGoal,NegatedGoal),
    %(debug_mode(on) -> write(NegatedGoal), nl ; true),
    (debug_mode(on) -> nl,write('Negated Goal:'), nl,
    translate:nested_print_bexpr_as_classicalb(NegatedGoal),
    write_hypothesis(TAllHypotheses)
    ; true),
    conjunct_predicates([NegatedGoal|TAllHypotheses],Predicate),
    %tools:print_bt_message(solving),
    ProofInfos = [disprover_result(final,all_and_selected,ResultOut),options(Opts)|PI1],
    ( get_alternate_prover_timeout(Opts,Prover,Timeout),
    Timeout>0,
    prove_using_alternative_prover(Prover,TGoal,TAllHypotheses,Opts,Timeout,ResultWithAll)
    % adds 5 extra PO proven in test 1800, and 4 more in test 1447
    -> % DISCHARGED by WD Prover
    (debug_mode(on) -> add_message(disprover,'Discharged by alternate prover: ',Prover:Timeout) ; true),
    PI1 = [disprover_result(Prover,all,ResultWithAll)|PI2]
    ; solve_disprover_predicate(prob_all_hyps,Predicate,Opts,ResultWithAll),
    PI1 = [disprover_result(prob,all,ResultWithAll)|PI2]
    ),
    %tools:print_bt_message(solver_result(CBCResult)),
    debug_println(10,disprover_result_with_all_hypotheses(ResultWithAll)),
    disprove_double_check(ResultWithAll,NegatedGoal,TAllHypotheses,TSelectedHypotheses,Predicate,Opts,ResultOut,PI2),
    (member(disprover_option(export_po_as_machine(File)),Opts)
    -> export_po_as_machine(File,TAllHypotheses,TSelectedHypotheses,TGoal,ProofInfos)
    ; true).

disprove_double_check(solution(X),NegatedGoal,_Hypotheses,_SelectedHypotheses,_,_,ResultOut,ProofInfos) :-
    predicate_identifiers(NegatedGoal,GoalIdentifiers),
    findall(binding(Id,Value,PP), get_binding_from_solution(X,GoalIdentifiers,0,Id,Value,PP), FilteredState),
    ResultOut = solution(FilteredState),
    ProofInfos = ['Counter example to all hypotheses found'].

disprove_double_check(no_solution_found(unfixed_deferred_sets),NegatedGoal,_Hypotheses,SelectedHypotheses,_,_,
    no_solution_found(unfixed_deferred_sets),ProofInfos) :-
    find_typed_identifier_uses(NegatedGoal,[],GoalIdentifiers),
    get_texpr_types(GoalIdentifiers,GoalTypes),
    find_typed_identifier_uses_l(SelectedHypotheses,[],HypIdentifiers),
    get_texpr_types(HypIdentifiers,HypTypes),
    append(GoalTypes,HypTypes,Types),
    % exclude all types that are not unfixed
    include(contains_unfixed_deferred_set,Types,UnfixedTypes),
    % see if an unfixed type is left
    UnfixedTypes = [_|_],
    !,
    ProofInfos = ['Goal or selected hypotheses contain unfixed deferred sets', unfixed(UnfixedTypes)],
    !.

disprove_double_check(contradiction_found,NegatedGoal,Hypotheses,SelectedHypotheses,FullPredicate,Opts,
    FinalResult,ProofInfos) :-
    ProofInfos = ['PO is proven using all hypotheses, no timeout or enumeration warning occured'],
    %add_hit(po_discharged,prob_all),
    (get_preference(double_evaluation_when_analysing,true)
    -> check_negated(NegatedGoal,Hypotheses,SelectedHypotheses,FullPredicate,Opts,FinalResult)
    ; FinalResult = contradiction_found).

disprove_double_check(Result,_NegatedGoal,Hypotheses,SelectedHypotheses,_,_Opts,ResultOut,ProofInfos) :-
    same_conjunction_list(Hypotheses,SelectedHypotheses),!,
    ProofInfos = ['Selected hypotheses identical to all hypotheses'],
    Result=ResultOut.

disprove_double_check(_OldResult,NegatedGoal,Hypotheses,SelectedHypotheses,_,Opts,ResultOut,ProofInfos) :-
    % No proof found with all hypotheses, now try selected ones only
    % reset existing enumeration warnings,
    % that might have been generated in a previous run
    reset_errors,
    (debug_mode(on)
    -> nl,write('Trying to use only selected hypotheses.\nNegated Goal:'), nl,
    translate:nested_print_bexpr_as_classicalb(NegatedGoal),
    write_hypothesis(SelectedHypotheses)
    ; true),
    conjunct_predicates([NegatedGoal|SelectedHypotheses],Predicate),
    %external_functions:observe_state(State),
    solve_disprover_predicate(prob_selected_hyps,Predicate,Opts,Result),
    ProofInfos = [disprover_result(prob,selected,Result)],
    !,
    disprove_triple_check(Result,NegatedGoal,Hypotheses,SelectedHypotheses,Predicate,Opts,ResultOut).

disprove_triple_check(contradiction_found,NegatedGoal,Hypotheses,SelectedHypotheses,FullPredicate,Opts,FinalResult) :-
    %add_hit(po_discharged,prob_selected),
    (get_preference(double_evaluation_when_analysing,true) % preference set by Rodin Disprover
    -> check_negated(NegatedGoal,Hypotheses,SelectedHypotheses,FullPredicate,Opts,FinalResult)
    ; FinalResult = contradiction_found,
    compute_unsat_core_if_requested(FullPredicate,Opts)
).

disprove_triple_check(solution(X),NegatedGoal,_,_,_FullPredicate,_,ResultOut) :-
    % Counter-Example to Goal for selected Hypotheses found
    predicate_identifiers(NegatedGoal,GoalIdentifiers),
    findall(binding(Id,Value,PP), get_binding_from_solution(X,GoalIdentifiers,10,Id,Value,PP), FilteredState),
    ResultOut = solution_on_selected_hypotheses(FilteredState).

disprove_triple_check(time_out,_,_,_,_,_,time_out). % TODO: We could try Kodkod here!

disprove_triple_check(no_solution_found(X),_,_,_,_,_,no_solution_found(X)). % Or here?

disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,Timeout,Opts,OutResult) :-
    check_options(Opts),
    temporary_set_preference(disprover_mode,true,DC),
    temporary_set_preference(time_out,Timeout,TC),
    start_ms_timer(Timer),
    user_interruptable_call_det(disprove1(Goal,AllHypotheses,SelectedHypotheses,Opts,Result),InterruptResult),
    %write(ir(InterruptResult)), nl,
    (InterruptResult = interrupted -> OutResult = interrupted ; OutResult = Result),
    %catch_internal_timeout(InterruptResult,Result,OutResult),
    (debug_mode(on) -> write(disprove_result(OutResult)),nl,stop_ms_timer(Timer),nl ; true),
    reset_temporary_preference(disprover_mode,DC),
    reset_temporary_preference(time_out,TC).

disprover_option(disprover_option(_)).

export_po_as_machine(Filename,THypothesesList,TSelectedHypothesesList,TGoal,Infos) :-
    %nested_print_sequent_as_classicalb(Stream,THypothesesList,TGoal,'ProofObligation_AllHyps',Infos),
    format(user_output,'Exporting selected hypotheses to B machine: ~w~n',[Filename]),
    safe_intelligent_open_file(Filename,write,Stream),
    nested_print_sequent_as_classicalb(Stream,TSelectedHypothesesList,TGoal,
    THypothesesList,'ProofObligation_SelectedHyps',Infos),
    close(Stream).

get_alternate_prover_timeout(Opts,Prover,Timeout) :-
    member(disprover_option(setlog_prover_timeout(TO)),Opts),!,
    (Prover=wd_prover,member(disprover_option(wd_prover_timeout(Timeout)),Opts) % try WD prover first
    ;
    Prover=setlog_prover, TO=Timeout).

get_alternate_prover_timeout(Opts,wd_prover,Timeout) :-
    member(disprover_option(wd_prover_timeout(Timeout)),Opts),!.

get_alternate_prover_timeout(_,wd_prover,WDTimeout) :-
    get_preference(time_out,GlobalTO),
    WDTimeout is 20 + GlobalTO // 100.

get_binding_from_solution(Solution,GoalIdentifiers,MaxIndexNonGoal,Id,Value,PP) :- MaxIndexNonGoal>=0,
    sort(GoalIdentifiers,SG),
    nth1(Nr,Solution,binding(Id,Value,PP)),
    (Nr =< MaxIndexNonGoal -> true ; ord_member(Id,SG)).

get_disprover_default_opts(Opts) :-
    (unavailable_extension(chr_extension,_Reason)
    -> CHR=false, format('Disabling CHR in disprover as extension not available~n',[]) ; CHR=true),
    % default options:
    Opts = [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/CHR].

print_prover_result_stats :-
    \+ \+ prover_stats(_,_,_,_), % at least one call made
    format('* Disprover statistics about individual prover calls and results:~n',[]),
    format('~w,~w,~w,~w,~w,~w~n',['Prover','Result','Calls','Runtime','TotRuntime','Walltime']),
    prover_stats(Prover,Result,Nr,timer(Runtime,TotRuntime,Walltime)),
    format('~w,~w,~w,~w,~w,~w~n',[Prover,Result,Nr,Runtime,TotRuntime,Walltime]),
    fail.

print_prover_result_stats.

prove_using_alternative_prover(setlog_prover,Goal,Hypotheses,Opts,TimeOutMs,Res) :-
    start_ms_timer(Timer),
    (prove_using_setlog(Goal,Hypotheses,Opts,TimeOutMs,Res)
    -> (Res = contradiction_found
    -> register_prover_result(setlog_prover,contradiction_found,Timer)
    ; register_prover_result(setlog_prover,Res,Timer),
    fail
    )
    ; register_prover_result(setlog_prover,failed,Timer),
    fail
).

prove_using_alternative_prover(wd_prover,Goal,Hypotheses,Opts,TimeOutMs,contradiction_found) :-
    % quite often 0 or 1 ms are enough for TimeOutMs
    (member(disprover_option(po_label(Label)),Opts) -> WDOpts=[po_label(Label)] ; WDOpts=[]),
    debug_format(19,'Starting WD Prover (timeout ~w ms) for \'~w\' ~n',[TimeOutMs,Label]),
    start_ms_timer(Timer),
    (safe_time_out(prove_sequent(proving,Goal,Hypotheses,WDOpts),TimeOutMs,TimeOutRes)
    -> (TimeOutRes=time_out
    -> format('Timeout in WD Prover (~w ms)~n',[TimeOutMs]),
    register_prover_result(wd_prover,time_out,Timer), fail
    ; register_prover_result(wd_prover,contradiction_found,Timer))
    ; register_prover_result(wd_prover,failed,Timer),
    fail
).

register_prover_result(Prover,Result,Timer) :-
    functor(Result,RF,_),
    (retract(prover_stats(Prover,RF,PrevNr,PrevTime)) -> true ; PrevNr=0, PrevTime=0),
    NewNr is PrevNr+1,
    get_elapsed_timer(Timer,DeltaTimer),
    combiner_timer(PrevTime,DeltaTimer,NewTimer),
    assert(prover_stats(Prover,RF,NewNr,NewTimer)),
    stop_ms_timer_with_debug_msg(Timer,prover_result(Prover,RF)).

same_conjunction_list(List1,List2) :-
    same_length(List1,List2,_), % avoid possibly expensive comparisons if lists clearly different
    % we could strip info field and the sort; but here we just want to catch the obvious case where the disprover is called with SelectedHyp = AllHyp
    maplist(same_texpr,List1,List2).

solve_disprover_predicate(ProverContext,Predicate,Opts,CBCResult) :-
    TimeoutFactor = 1,
    exclude(disprover_option,Opts,SOpts),
    (member(disprover_option(observe_state),Opts) -> observe_state(State) ; true),
    start_ms_timer(Timer),
    (solve_predicate(Predicate,State,TimeoutFactor,SOpts,CBCResult)
    -> register_prover_result(ProverContext,CBCResult,Timer)
    ; register_prover_result(ProverContext,failed,Timer),
    fail
).

valid_disprover_option(observe_state).

valid_disprover_option(unsat_core).

valid_disprover_option(unsat_core_as_machine).

valid_disprover_option(export_po_as_machine(_)).

valid_disprover_option(setlog_prover_timeout(_)).

valid_disprover_option(wd_prover_timeout(_)).

valid_disprover_option(po_label(_)).

valid_option(disprover_option(X)) :- !,valid_disprover_option(X).

valid_option(X) :- valid_solver_option(X).

write_hypothesis([]).

write_hypothesis([Hyp|Hyps]) :-
    write(' & /* Hypothesis: */ '), nl,
    %(debug_mode(on) -> write(Hyp), nl ; true),
    nested_print_bexpr_as_classicalb(Hyp),
    write_hypothesis(Hyps).