unsat_cores

add_fixed_conj(Options,P,Res) :- member(fixed_conjuncts(FixedList),Options),!,
    (append(FixedList,P,FP) -> Res=FP
    ; add_internal_error('Illegal fixed list: ',FixedList), Res=P).

add_fixed_conj(_,P,P).

add_uc_info(SolverRes, C, IC2) :-
    ( ( ground(SolverRes),
    SolverRes = solution(_), Labels = [],
    UCInfo = [description('definitely in unsat core (solution)')])
    ; ( SolverRes == error, Labels = ['WD'],
    UCInfo = [description('definitely in unsat core (kept to prevent WD error)')])
    ; ( SolverRes == time_out, Labels = ['TO'], % pretty printed as @TO
    UCInfo = [description('possibly in unsat core (kept to prevent timeout)')])
    ; ( ground(SolverRes), Labels = ['VTO'],
    SolverRes = no_solution_found(enumeration_warning(_,_,_,_,_)),
    UCInfo = [description('possibly in unsat core (kept to prevent virtual timeout)')])
    ; ( SolverRes == no_solution_found(unfixed_deferred_sets), Labels = ['DEFSETS'],
    UCInfo = [description('definitely in unsat core (kept to fix deferred sets)')])
    ; ( ground(SolverRes), Labels = ['UNKNOWN'],
    SolverRes = no_solution_found(_),
    UCInfo = [description('possibly in unsat core (kept to prevent unknown solver result)')])
    ), !,
    add_texpr_infos(C, UCInfo, IC1),
    add_labels_to_texpr(IC1,Labels,IC2).

add_warn(Conjunct) :-
    add_warning(unsat_cores,'This is part of an unsatisfiable core of the PROPERTIES clause: ',Conjunct,Conjunct).

can_be_further_decomposed(TE,A,B) :- can_be_further_decomposed(TE,positive,A,B).

can_be_further_decomposed(b(E,pred,Info),NegPos,A,B) :- can_be_further_decomposed_aux(E,Info,NegPos,A,B).

can_be_further_decomposed_aux(conjunct(A,B),_,positive,A,B).

can_be_further_decomposed_aux(disjunct(A,B),_,negative,A,B).

can_be_further_decomposed_aux(disjunct(A,B),_,positive,D1,D2) :-
    get_preference(unsat_core_algorithm,linear_greedy_decompose),!, % can blow up number of cases
    (can_be_further_decomposed(A,positive,A1,A2) % here we could try divide conjuncts in middle
    -> disjunct_predicates([A1,B],D1),
    disjunct_predicates([A2,B],D2)
    ; can_be_further_decomposed(B,positive,B1,B2)
    -> disjunct_predicates([A,B1],D1),
    disjunct_predicates([A,B2],D2)
).

can_be_further_decomposed_aux(implication(A,B),_,positive,I1,I2) :-
    (can_be_further_decomposed(B,positive,B1,B2) % A=>B1&B2 <--> A=>B1 & A=>B2
    -> create_implication(A,B1,I1),
    create_implication(A,B2,I2)
    ; can_be_further_decomposed(A,negative,A1,A2) % (A1 or A2) => B <--> A1 => B & A2 => B
    -> create_implication(A1,B,I1),
    create_implication(A2,B,I2)).

can_be_further_decomposed_aux(implication(A,B),_,negative,NA,B) :- % A=>B <--> not(A) or B
    create_negation(A,NA).

can_be_further_decomposed_aux(negation(D),_,NegPos,NA,NB) :- neg_context(NegPos,PosNeg),
    can_be_further_decomposed(D,PosNeg,A,B), % not(A &/or B) <--> not(A) or/& not(B)
    create_negation(A,NA),
    create_negation(B,NB).

can_be_further_decomposed_aux(let_predicate(V,E,P),Info,NegPos,LEA,LEB) :-
    can_be_further_decomposed(P,NegPos,A,B),
    LEA = b(let_predicate(V,E,A),pred,Info), % used_ids could be wrong; TO DO: think about exists
    LEB = b(let_predicate(V,E,B),pred,Info).

can_be_further_decomposed_aux(lazy_let_pred(V,E,P),Info,NegPos,LEA,LEB) :-
    can_be_further_decomposed(P,NegPos,A,B),
    LEA = b(lazy_let_pred(V,E,A),pred,Info),
    LEB = b(lazy_let_pred(V,E,B),pred,Info).

compare_length(P1,P2) :- length(P1,L1), length(P2,L2),
    (L1<L2 -> true
    ; L1=L2 ->
    term_size(P1, T1),
    term_size(P2, T2),
    T1 < T2
).

compute_core_linear_loop([], _,DefinitelyInCore, _Options, _, DefinitelyInCore,[],[]).

compute_core_linear_loop([C|Cs], Counter,DefinitelyInCore, Options, GlobalRes, CorePreds,NotInCore,AllPreds) :-
    % remove C and check for satisfiability
    append(DefinitelyInCore,Cs,LL0), add_fixed_conj(Options,LL0,LL),
    conjunct_predicates(LL, ConjunctionToCheck),
    % print('TRY TO REMOVE: '), translate:print_bexpr(C),nl,
    solve_core_pred(ConjunctionToCheck, 1, Options, Res),
    debug_println(4, solve_predicate_result(Res)),
    progress_info(Res),
    must_keep_conjunct(Res,GlobalRes,Options), % a solution has been found or a time-out occured - C can not be removed;
    % normally corresponds to solve_result: contradiction_found or no_solution_found(unfixed_deferred_sets)
    !,
    % print('KEEPING: '), translate:print_bexpr(C),nl,
    % TO DO: when looking for minimal unsat core we could provide an upper-bound for the length
    increase_core_counter(Counter,Options,IncCtr),
    (can_be_further_decomposed(C, CA, CB),
    (member(inspect_nested_conjuncts(INC),Options) -> INC=true ; true)
    -> % print('% Split: '), translate:print_bexpr(CA),nl, print('% '),translate:print_bexpr(CB),nl,
    compute_core_linear_loop([CA,CB|Cs], Counter,DefinitelyInCore, Options, GlobalRes, CorePreds,NotInCore,AllPreds)
    ; add_uc_info(Res, C, IC), AllPreds = [C|TAP],
    append(DefinitelyInCore,[IC],NewDefInCore), % TODO: use DCG
    compute_core_linear_loop(Cs, IncCtr,NewDefInCore, Options, GlobalRes, CorePreds,NotInCore,TAP)
).

compute_core_linear_loop([C|Cs], Ctr, DefinitelyInCore, Options, GlobalRes, CorePreds,NotInCore,[C|AllPreds]) :-
    % format('CAN BE REMOVED (~w): ',[GlobalRes]), translate:print_bexpr(C),nl,
    % C can be removed - we no longer introduce a choice point to not remove C; further cores are found by restarting
    NotInCore = [C|RestNotInCore],
    compute_core_linear_loop(Cs, Ctr, DefinitelyInCore, Options, GlobalRes, CorePreds,RestNotInCore,AllPreds).

compute_cores_linear(RPredicateList, Options, GlobalRes, CorePreds) :-
    compute_core_linear_loop(RPredicateList, 0, [], Options, GlobalRes, InCore,NotInCore,AllPreds),!,
    ( CorePreds = InCore
    ; % find more cores:
    debug_print('R'),
    restart_core_linear(InCore,NotInCore,AllPreds,Options,GlobalRes,CorePreds)
).

contradiction_check(N,ProcessedList,Options,CoreList,Res) :-
    select_core_target(N,ProcessedList,CoreList),
    conjunct_predicates(CoreList,Core),
    %nl,translate:print_bexpr(Core),nl,nl,
    solve_core_pred(Core, 0.02, Options, Res),
    progress_info(Res),
    contradiction_result(Res,Options).

contradiction_result(contradiction_found,_).

contradiction_result(no_solution_found(unfixed_deferred_sets),Options) :-
    member(allow_unfixed_deferred_sets,Options).

definite_prob_result(solution(_),_).

definite_prob_result(Res,Options) :- contradiction_result(Res,Options).

explain_no_sol(solver_answered_unknown, 'UNKNOWN').

explain_no_sol(unfixed_deferred_sets,'FALSE (DEFERRED SETS)').

explain_no_sol(enumeration_warning(_,_,_,_,_), 'UNKNOWN (ENUMERATION WARNING)').

explain_no_sol(_, 'UNKNOWN').

explain_result(time_out,'UNKNOWN (TIME_OUT)').

explain_result(error,'UNKNOWN (ERROR)').

explain_result(clpfd_overflow,'UNKNOWN (CLPFD OVERFLOW)').

explain_result(no_solution_found(E),R) :- explain_no_sol(E,R).

explain_result(contradiction_found,'FALSE').

explain_result(solution(_),'TRUE').

explain_result(_,'UNKNOWN').

get_time_out_for_comp_pred(Predicate,Nr,SubPred,TimeToFindContradiction,Options,Res) :- % partition
    temporary_set_preference(partition_predicates_inline_equalities,false,OldValueOfPref), % avoid inlining equalities
    % TO DO: maybe provide an option for this
    call_cleanup(predicate_components(Predicate,Components),
    reset_temporary_preference(partition_predicates_inline_equalities, OldValueOfPref)),
    if( (nth1(Nr,Components,component(SubPred,Ids)), % select component via backtracking
    debug_println(19,examining_component(Nr,Ids)),
    get_time_out_for_pred(SubPred,TimeToFindContradiction,Options,Res),
    progress_info(Res),
    %print(sol_comp(Nr,Res)),nl,
    % TODO: if translation_or_setup_failed and target is contradiction_found: filter predicate to that part that can be translated
    \+ solution_found(Res)),
    % we have found a sub-component that has a contradiction
    true,
    (SubPred=Predicate,
    get_time_out_for_pred(SubPred,TimeToFindContradiction,Options,Res)
)
).

get_time_out_for_pred(Predicate,TimeToFindContradiction,Options,Res) :-
    silent_mode(CurMode), set_silent_mode(on),
    statistics(walltime,[T1,_]),
    solve_core_pred(Predicate, 2, Options, Res),
    statistics(walltime,[T2,_]), TimeToFindContradiction is T2-T1,
    set_silent_mode(CurMode), !.

has_common_ids(UsedIdsSoFar,conj(_,_,_,UsedIdsN)) :- ord_intersect(UsedIdsSoFar,UsedIdsN).

increase_core_counter(Cur,Options,_) :- max_core_size(Max), Cur >= Max,
    member(branch_and_bound,Options),!,format('B~w',[Max]),fail.

increase_core_counter(Cur,_,C1) :- C1 is Cur+1.

minimum_unsat_core(Predicate,CorePredicate) :-
    minimum_unsat_core_with_fixed_conjuncts(Predicate,[],CorePredicate).

minimum_unsat_core_with_fixed_conjuncts(Predicate,FixedConjuncts,CorePredicate) :-
    Options = [branch_and_bound,fixed_conjuncts(FixedConjuncts)],
    findall(CoreList,
    unsat_core_list(Predicate,Options,no_solution_found,CoreList),
    Cores),
    reset_max_core_size,
    min_member(compare_length,MinCs,Cores),
    conjunct_predicates(MinCs,CorePredicate).

must_keep_conjunct(solution(_),_,_) :- !.

must_keep_conjunct(X,X,_) :- !,fail. % same result as global result, e.g., WD error or time_out

must_keep_conjunct(_,_,Options) :- member(keep_exact_result,Options),!.

must_keep_conjunct(contradiction_found,_,_) :- !,fail.

must_keep_conjunct(no_solution_found(X),GlobalRes,_) :- !,
    must_keep_no_sol_found(X,GlobalRes).

must_keep_conjunct(_,_,_).

must_keep_no_sol_found(enumeration_warning(_,_,_,_,critical),_).

must_keep_no_sol_found(solver_answered_unknown,_Global). % Global typically contradiction_found

neg_context(positive,negative). neg_context(negative,positive).

neg_context(positive,negative). neg_context(negative,positive).

pred_has_unsat_core_label(Pred,Label) :- get_texpr_label(Pred,Label), uc_label(Label).

preprocess_conjuncts([],_,_,[]).

preprocess_conjuncts([Conj|T],Nr,Options,ListResult) :-
    format(' ==> Pre-processing conjunct ~w and checking for individual inconsistency~n',[Nr]),
    %translate:print_bexpr(Conj),nl,
    % we could =remove try_prob_solver_first(_) from Options, if we want to filter non-translatable conjuncts!
    solve_core_pred(Conj, 0.02, Options, Res),
    (explain_result(Res,Expl) -> debug_format(19,'Result for conjunct ~w: ~w (~w)~n',[Nr,Expl,Res])),
    N1 is Nr+1,
    (should_remove_conjunct(Res)
    -> % remove this conjunct; it can only disturb finding a core for a contradiction
    preprocess_conjuncts(T,N1,Options,ListResult)
    ; find_identifier_uses(Conj,[],UsedIds),
    ListResult = [conj(Nr,Conj,Res,UsedIds)|PT],
    (contradiction_result(Res,Options)
    -> PT=[] % stop processing, we have found an unsat core of a single conjunct
    ; preprocess_conjuncts(T,N1,Options,PT))
).

progress_info(ARes) :- progress_info_aux(ARes),!,flush_output(user_output).

progress_info_aux(time_out) :- progress_print('T').

progress_info_aux(error) :- progress_print('WD').

progress_info_aux(no_solution_found(E)) :- progress_info_no_sol_found_aux(E).

progress_info_aux(contradiction_found) :- progress_print('-').

progress_info_aux(translation_or_setup_failed) :- progress_print('FAILED'). % Z3 or cvc4 translation failed

progress_info_aux(solution(_)) :- progress_print('+').

progress_info_aux(clpfd_overflow) :- progress_print('O').

progress_info_aux(UNKNOWN) :- debug_format(5, '*~w*', [UNKNOWN]).

progress_info_no_sol_found_aux(unfixed_deferred_sets) :- progress_print('-').

progress_info_no_sol_found_aux(solver_answered_unknown) :- progress_print('U').

progress_info_no_sol_found_aux(enumeration_warning(_,_,_,_,_)) :- progress_print('U(ENUM)').

progress_info_no_sol_found_aux(UNKNOWN) :- debug_format(5, '*~w*', [UNKNOWN]).

progress_print(C) :- debug_print(C).

quick_bup_core(Predicate,Options,CoreList,Result) :-
    uc_conjunction_to_list(Predicate,Options,List),
    preprocess_conjuncts(List,1,Options,ProcessedList),
    (last(ProcessedList,conj(_,Last,LR,_)),
    contradiction_result(LR,Options)
    -> CoreList = [Last], Result=LR
    ; (member(maximum_core_size(MaxN),Options) -> true ; MaxN=3),
    between(2,MaxN,N),
    format(' ==> Finding cores of length ~w~n',[N]),
    contradiction_check(N,ProcessedList,Options,CoreList,Result) -> true
).

quick_bup_core_up_to(Typed,MaxSize,CoreList,Result) :-
    quick_bup_core(Typed,[use_smt_solver(z3axm),
    maximum_core_size(MaxSize),
    try_prob_solver_first(fixed_time_out(5))],
    CoreList,Result).

remove_conjunct(C,RPredicateList,NewRPredicateList) :-
    select(CC,RPredicateList,NewRPredicateList), % TO DO: remember position of C and use nth1
    same_texpr(C,CC),!.

remove_conjunct(C,RPredicateList,New) :-
    add_internal_error('Could not find conjunct from unsat core: ',remove_conjunct(C,RPredicateList,New)),fail.

reset_max_core_size :- retractall(max_core_size(_)).

restart_core_linear([C|Cs],Keep,AllPreds,Options,GlobalRes,CorePreds) :-
    append(Keep,Cs,LL0), add_fixed_conj(Options,LL0,LL),
    conjunct_predicates(LL, ConjunctionToCheck),
    % print('TRY TO REMOVE CORE CONJUNCT FOR RESTART: '), translate:print_bexpr(C),nl,
    solve_core_pred(ConjunctionToCheck, 1, Options, Res),
    progress_info(Res),
    must_keep_conjunct(Res,GlobalRes,Options),!,
    % we need to keep C in PredicateList for restart; otherwise we change global result
    restart_core_linear(Cs,[C|Keep],AllPreds,Options,GlobalRes,CorePreds).

restart_core_linear([C|_],_,AllPreds,Options,GlobalRes,CorePreds) :-
    % we can remove C from the global list
    (\+ get_preference(unsat_core_algorithm,divide_and_conquer) -> ! ; true), % linear_greedy
    remove_conjunct(C,AllPreds,NewAllPreds), % remove C, keeping original order
    debug_print('C'),
    compute_cores_linear(NewAllPreds, Options, GlobalRes, CorePreds).

restart_core_linear([C|Cs],Keep,AllPreds,Options,GlobalRes,CorePreds) :-
    % try to remove another conjunct; we may find the same core multiple times
    restart_core_linear(Cs,[C|Keep],AllPreds,Options,GlobalRes,CorePreds).

select_core_target(N,List,Res) :-
    append(_,[conj(Nr,ConjN,_,UsedIdsN)|Rest],List), % now only use conjuncts to the right of ConjN
    format(' ==> finding (~w-ary) conflicts with conjunct ~w: ',[N,Nr]),translate:print_bexpr(ConjN),nl,
    N1 is N-1,
    select_core_target(N1,Rest,[ConjN],UsedIdsN,Res).

select_core_target(0,_,Core,_,Res) :- !, Res=Core.

select_core_target(N,List,CoreSoFar,UsedIdsSoFar,Res) :- %print(n(N,UsedIdsSoFar)),nl,
    split_list(has_common_ids(UsedIdsSoFar),List,CommonList,DisjList),
    append(_,[conj(_Nr,ConjN,_,UsedIdsN)|Rest],CommonList), % only choose conjuncts with common ids larger than Nr
    %print(selected_conj(_Nr)),nl, translate:print_bexpr(ConjN),nl,
    append(Rest,DisjList,RestList),
    ord_union(UsedIdsN,UsedIdsSoFar,New),
    N1 is N-1,
    select_core_target(N1,RestList,[ConjN|CoreSoFar],New,Res).

set_max_core_size(Max) :- retractall(max_core_size(_)), assertz(max_core_size(Max)).

should_remove_conjunct(no_solution_found(translation_failed)).

solution_found(Res) :-
    Res \= contradiction_found,
    Res \= no_solution_found(_),
    Res \= time_out,
    Res \= error,
    Res \= clpfd_overflow.

solve_core_pred(BPred,_TOFactor,Options,Res) :- % translate:print_bexpr(BPred),nl,
    memberchk(try_prob_solver_first(TimeoutFactor),Options),
    solve_predicate(BPred,_State,TimeoutFactor,Res),
    formatsilent('ProB solve_predicate result : ~w~n',[Res]),
    definite_prob_result(Res,Options), !.

solve_core_pred(BPred,TOFactor,Options,Res) :- % print(' --> Z3 SOLVE: '), translate:print_bexpr(BPred),nl,
    member(use_smt_solver(Solver),Options),!,
    Opts = [smt_time_out_factor(TOFactor), check_sat_skeleton(10), instantiate_quantifier_limit(5)],
    %formatsilent('Starting SMT solver ~w with ~w~n',[Solver,Opts]),
    smt_solve_predicate(Solver,Opts,BPred,_,Res),
    formatsilent('~w solve_predicate result : ~w~n',[Solver,Res]).

solve_core_pred(BPred,_TOFactor,Options,Res) :-
    member(use_cdclt_solver,Options),!, % TODO: pass TOFactor to cdclt
    (cdclt_solve_predicate(BPred,_,Res) -> true
    ; Res= contradiction_found,
    add_internal_error('Solver call failed:',cdclt_solve_predicate(BPred,_,Res))
).

solve_core_pred(BPred,TOFactor,Options,Res) :-
    (member(use_smt_mode/SMT,Options) -> true ; SMT=true),
    (member(use_clpfd_solver/CLPFD,Options) -> true ; CLPFD=true),
    (member(use_chr_solver/CHR,Options) -> T=[use_chr_solver/CHR] ; T=[]),
    solve_predicate(BPred,_BState,TOFactor,[use_smt_mode/SMT,use_clpfd_solver/CLPFD,ignore_wd_errors|T],Res).

split_in_half(C, A, B) :-
    length(C,L),
    Half is L // 2,
    length(A, Half),
    append(A, B, C).

tcltk_unsat_core_properties(list(CorePredStrings),HasUCLabels,StrRes) :-
    % TO DO: transmit runtime from Runtime to FINALISE SETUP_CONSTANTS to avoid re-checking Properties
    unsat_core_of_properties(CorePredicates,[],StrRes),
    set_unicode_mode,
    call_cleanup(maplist(translate:translate_bexpression,CorePredicates,CorePredStrings),
    unset_unicode_mode),
    (member(CP,CorePredicates), pred_has_unsat_core_label(CP,_) -> HasUCLabels=true ; HasUCLabels=false),
    maplist(add_warn,CorePredicates). % so that we see the spans of the unsat core in the edit window

temporary_set_timeout(TimeToFindContradiction,CHNG1) :-
    number(TimeToFindContradiction), TimeToFindContradiction>=0,
    NewTimeOut is round(TimeToFindContradiction+10), % in case we have 0; just add a few ms
    temporary_set_preference(time_out,NewTimeOut,CHNG1).

uc_conjunction_to_list(b(exists(_V,Pred),pred,_), Options, List) :-
    member(inspect_quantifiers(true), Options),
    !,
    conjunction_to_list(Pred, List).

uc_conjunction_to_list(Pred, _, List) :- conjunction_to_list(Pred, List).

uc_label('WD').

uc_label('TO').

uc_label('VTO').

uc_label('DEFSETS').

unsat_chr_core_list_with_auto_time_limit(Predicate,MaxTime,Options,GlobalRes,CorePredicates) :-
    temporary_set_preference(use_chr_solver,true,CHNG1),
    call_cleanup(unsat_core_wth_auto_time_limit(Predicate,MaxTime,Options,GlobalRes,CorePredicates),
    reset_temporary_preference(use_chr_solver,CHNG1)).

unsat_chr_core_with_fixed_conjuncts_auto_time_limit(Predicate,FixedConjuncts,MaxTimeLimit,CorePredicate) :-
    temporary_set_preference(use_chr_solver,true,CHNG1), % TODO: put into options ?
    Options = [],
    call_cleanup(unsat_core_with_fixed_conjuncts_auto_time_limit(Predicate,FixedConjuncts,MaxTimeLimit,Options,CorePredicate),
    reset_temporary_preference(use_chr_solver,CHNG1)).

unsat_core(Predicate,CorePredicate) :-
    unsat_core(Predicate,no_solution_found,CorePredicate).

unsat_core(Predicate,GlobalResult,CorePredicate) :-
    unsat_core_list(Predicate,[],GlobalResult,CorePreds),
    conjunct_predicates(CorePreds,CorePredicate).

unsat_core_fixed_conjuncts_lists_divide_and_conquer([],_,_,_,_) :- !, fail. % we split too far!

unsat_core_fixed_conjuncts_lists_divide_and_conquer([C],_FixedConjuncts,_GlobalResult,_Options,[C]) :-
    !. % if there is only one conjunct left, it has to belong to the core

unsat_core_fixed_conjuncts_lists_divide_and_conquer(Clauses,FixedConjuncts,GlobalResult,Options,Core) :-
    split_in_half(Clauses,A,B),
    % print('SPLIT: '), print(A),nl,print(B),nl,
    unsat_core_fixed_conjuncts_lists_divide_and_conquer_split(A,B,FixedConjuncts,GlobalResult,Options,Core).

unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur1(ARealRes,A,_B,FixedConjuncts,GlobalResult,Options,Core) :-
    \+ must_keep_conjunct(ARealRes,GlobalResult,[]), % A is (virtually / effectively) unsat. Recur on A.
    unsat_core_fixed_conjuncts_lists_divide_and_conquer(A,FixedConjuncts,GlobalResult,Options,Core).

unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur1(ARealRes,A,B,FixedConjuncts,GlobalResult,Options,Core) :-
    append(B,FixedConjuncts,AllConjuncts),
    conjunct_predicates(AllConjuncts,BPred),
    % print('SOLVING RHS: '), translate:print_bexpr(BPred),nl,
    solve_core_pred(BPred,1,Options,BRealRes),
    progress_info(BRealRes),
    % print(result(BRealRes)),nl,
    !,
    unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur2(ARealRes,BRealRes,A,B,FixedConjuncts,GlobalResult,Options,Core).

unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur2(_ARealRes,BRealRes,_A,B,FixedConjuncts,GlobalResult,Options,Core) :-
    \+ must_keep_conjunct(BRealRes,GlobalResult,[]), % B is (virtually / effectively) unsat. Recur on B.
    !,
    unsat_core_fixed_conjuncts_lists_divide_and_conquer(B,FixedConjuncts,GlobalResult,Options,Core).

unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur2(ARealRes,BRealRes,A,B,FixedConjuncts,GlobalResult,Options,Core) :-
    % the interesting case: if both are sat
    must_keep_conjunct(ARealRes,GlobalResult,[]),
    must_keep_conjunct(BRealRes,GlobalResult,[]),
    % minimize A assuming usat core includes B
    append(B,FixedConjuncts,FixedAndB),
    unsat_core_fixed_conjuncts_lists_divide_and_conquer(A,FixedAndB,GlobalResult,Options,ACore),
    % now ACore & B is unsat and minimal but not minimum core
    % minimize B assuming ACore
    append(ACore,FixedConjuncts,FixedAndA),
    unsat_core_fixed_conjuncts_lists_divide_and_conquer(B,FixedAndA,GlobalResult,Options,BCore),
    append(ACore,BCore,Core).

unsat_core_fixed_conjuncts_lists_divide_and_conquer_split(A,B,FixedConjuncts,GlobalResult,Options,Core) :-
    append(A,FixedConjuncts,AllConjuncts),
    conjunct_predicates(AllConjuncts,APred),
    % print('SOLVING LHS: '), translate:print_bexpr(APred),nl,
    solve_core_pred(APred, 1, Options, ARealRes),
    progress_info(ARealRes),
    % print(result(ARealRes)),nl,
    !, % do not backtrack into solving or multiple results can be found leading to duplicated cores
    unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur1(ARealRes,A,B,FixedConjuncts,GlobalResult,Options,Core).

unsat_core_list(Predicate,Options,GlobalResult,CorePreds) :-
    %print('COMPUTING CORE:'),nl,translate:nested_print_bexpr(Predicate),nl,
    %(member(fixed_conjuncts(FL),Options) -> print('FIXED CONJ:'),nl,translate:nested_print_bexpr(FL),nl ; true),nl,
    uc_conjunction_to_list(Predicate,Options,PredicateList),
    length(PredicateList,OrigLen),
    silent_mode(CurMode), set_silent_mode(on),
    call_cleanup(unsat_core_with_options_lists(PredicateList,Options,GlobalResult,CorePreds),
    set_silent_mode(CurMode)),
    ( CurMode = on
    -> true
    ; length(CorePreds,NewLen),
    debug_format(5, '~nFound core with ~w/~w conjuncts.~n', [NewLen,OrigLen])
).

unsat_core_list_with_time_limit(Predicate,TimeToFindContradiction,Options,GlobalRes, CorePredicates) :-
    temporary_set_timeout(TimeToFindContradiction,CHNG1),
    % this time will be multiplied by 2 below
    call_cleanup(unsat_core_list(Predicate,Options,GlobalRes,CorePredicates),
    reset_temporary_preference(time_out,CHNG1)).

unsat_core_of_properties(CorePredicates,Options,StrRes) :-
    bmachine:b_get_properties_from_machine(Properties), % TO DO: also provide for unsat component
    debug_print('Computing (efficient) unsat core for PROPERTIES'),nl,
    unsat_chr_core_list_with_auto_time_limit(Properties,5000,Options,GlobalResult,CorePredicates),
    (explain_result(GlobalResult,Explanation) -> StrRes=Explanation ; StrRes='**UNKNOWN**').

unsat_core_properties_table(list([list([PropsHeader,'Source'])|ResList])) :-
    get_preference(translation_limit_for_table_commands,Limit),
    get_specification_description(properties,PROPS),
    unsat_core_of_properties(CorePredicates,[no_warning_if_sol_found],StrRes),
    ajoin([PROPS,' : ',StrRes],PropsHeader),
    set_unicode_mode,
    call_cleanup(findall(list([TS,PosInfo]),
    (member(CP,CorePredicates), translate_bexpression_with_limit(CP,Limit,TS),
    get_tk_table_position_info(CP,PosInfo)),ResList),
    unset_unicode_mode).

unsat_core_with_fixed_conjuncts(P,FC,Core) :- unsat_core_with_fixed_conjuncts(P,FC,no_solution_found,Core).

unsat_core_with_fixed_conjuncts(Predicate,FixedPreds,GlobalRes,CorePredicate) :-
    conjunction_to_list(FixedPreds,FixedList),
    Options = [fixed_conjuncts(FixedList)], % should we set inspect_nested_conjuncts(false) ?
    unsat_core_list(Predicate,Options,GlobalRes,CorePreds),
    conjunct_predicates(CorePreds,CorePredicate).

unsat_core_with_fixed_conjuncts_auto_time_limit(Predicate,FixedConjuncts,MaxTimeLimit,Options,CorePredicate) :-
    is_truth(FixedConjuncts),!,
    Options=[],
    unsat_core_wth_auto_time_limit(Predicate,MaxTimeLimit,Options,_,CorePreds),
    conjunct_predicates(CorePreds,CorePredicate).

unsat_core_with_fixed_conjuncts_auto_time_limit(Predicate,FixedConjuncts,MaxTimeLimit,Options,CorePredicate) :-
    conjunct_predicates([Predicate,FixedConjuncts],FullPred),
    get_time_out_for_pred(FullPred,TimeToFindContradiction,Options,GlobalRes), % we cannot use component version due to FixedConjuncts
    progress_info(GlobalRes),
    (solution_found(GlobalRes)
    -> add_warning(unsat_cores,'Predicate has a solution, unsat core cannot be computed: ',Predicate,Predicate),
    CorePredicate=Predicate
    ; Limit is min((TimeToFindContradiction*110/100),MaxTimeLimit),
    temporary_set_timeout(Limit,CHNG1),
    call_cleanup(unsat_core_with_fixed_conjuncts(Predicate,FixedConjuncts,GlobalRes,CorePredicate),
    reset_temporary_preference(time_out,CHNG1))
).

unsat_core_with_options_linear(PredicateList,Options, GlobalRes, CorePreds) :-
    reverse(PredicateList, RPredicateList), % so that we properly treat WD we start removing from the back
    compute_cores_linear(RPredicateList, Options, GlobalRes, CorePreds).

unsat_core_with_options_lists(PredicateList,Options,GlobalResult,CorePreds) :-
    get_preference(unsat_core_algorithm,divide_and_conquer), !, % TO DO: pass GlobalResult
    temporary_set_preference(allow_enumeration_of_infinite_types,false,OldValueOfPref),
    (member(fixed_conjuncts(FixedList),Options) -> true ; FixedList=[]),
    call_cleanup(unsat_core_fixed_conjuncts_lists_divide_and_conquer(PredicateList,FixedList,GlobalResult,Options,CorePreds),
    reset_temporary_preference(allow_enumeration_of_infinite_types,OldValueOfPref)).

unsat_core_with_options_lists(PredicateList,Options,GlobalResult,CorePreds) :-
    reset_max_core_size,
    temporary_set_preference(allow_enumeration_of_infinite_types,true, OldValueOfPref),
    %print('START: '),nl,translate:nested_print_bexpr(RPredicateList),nl,
    call_cleanup(unsat_core_with_options_linear(PredicateList,Options, GlobalResult, CorePreds),
    reset_temporary_preference(allow_enumeration_of_infinite_types, OldValueOfPref)),
    (member(branch_and_bound,Options) -> length(CorePreds,Len), set_max_core_size(Len) ; true).

unsat_core_wth_auto_time_limit(Predicate,MaxTime,Options,GlobalRes,CorePredicates) :-
    % TODO: if unsat_core_target(.) provided and fixed time-out then we do not need to compute this:
    get_time_out_for_comp_pred(Predicate,_Nr,CompPred,TimeToFindContradiction,Options,GlobalRes),
    progress_info(GlobalRes),
    (solution_found(GlobalRes)
    -> ( member(no_warning_if_sol_found,Options)
    -> add_message(unsat_cores,'Predicate has a solution, unsat core cannot be computed: ',Predicate,Predicate)
    ; member(ignore_if_sol_found,Options)
    -> true
    ; add_warning(unsat_cores,'Predicate has a solution, unsat core cannot be computed: ',Predicate,Predicate)
    ),
    CorePredicates=[Predicate]
    ; (member(auto_time_out_factor(Factor),Options) -> true ; Factor=120),
    Limit0 is min(((TimeToFindContradiction*Factor)/100),MaxTime), %print(time_limit(Limit)),nl,
    (member(min_time_out(MinTime),Options) -> true ; MinTime = 5),
    Limit is max(MinTime,Limit0),
    (member(unsat_core_target(Target),Options) -> true ; Target = GlobalRes),
    % with unsat_core_target(contradiction_found) we can look for real contradictions even if the whole predicate has a time-out or translation error
    debug_format(19,'Time out: ~w ms, target for unsat core: ~w~n',[Limit,Target]),
    unsat_core_list_with_time_limit(CompPred,Limit,Options,Target,CorePredicates)
).