unsat_core_generalization

unsat_core_generalization(TransitionPredicate,HIn,N,Frames,State,Inputs,[SuccState|SuccStates],HOut) :-
    in_solver_on_level(N,Frames,IS),
    unsat_core_generalization_aux(TransitionPredicate,IS,State,Inputs,SuccState,Core), !,
    add_to_heap(HIn,N,obligation(Core,TransitionPredicate,Inputs,[SuccState|SuccStates]),HOut).

unsat_core_generalization_aux(TransitionPredicate,IS,State,Inputs,SuccState,Core) :-
    prime_predicate(SuccState,TPrime),
    create_negation(TPrime,NotTPrime),
    conjunct_predicates([NotTPrime,Inputs,TransitionPredicate|IS],Conjunction),
   
    % verify that the query is actually unsat
    conjunct_predicates([State,Conjunction],VerifyQuery),
    solve(VerifyQuery,Result),
    Result = contradiction_found(_), !,
   
    %debug output
    translate_bexpression(Conjunction,PPConj),
    translate_bexpression(State,PPState),
    translate_bexpression(Inputs,PPInputs),
    format('unsat core generalization: generalizing~n~w~nby computing unsat core of it with fixed conjuncts~n~w~nand inputs~n~w~n.',[PPState,PPConj,PPInputs]),
   
    % the unsat core is a lifting to a partial assignment
    unsat_core_with_fixed_conjuncts(State,Conjunction,Core),
    translate_bexpression(Core,PPCore),
    format('unsat core is~n~w~n',[PPCore]).

unsat_core_generalization_aux(_TP,_IS,State,_Inputs,_SuccState,Core) :-
    add_error(unsat_core_generalization, 'unsat core generalization failed. query is not unsat!'),
    Core = State.