b_slicing

construct_property_machine(Constants,Properties,Machine) :-
    full_b_machine(Orig),
    erase_unnecessary_mparts(Orig,Clean),
    write_section(abstract_constants,Constants,Clean,M1),
    write_section(properties,Properties,M1,Machine).

contains_equation(Id,Predicates,Expression,Equation,RPred) :-
    get_texpr_id(IdExpr,Id),
    create_texpr(equal(A,B),pred,_,Equation),
    select(Equation,Predicates,RPred),
    ( A=IdExpr,B=Expression
    ; B=IdExpr,A=Expression).

do_simple_statistics(IncludedIds,IncludedPred,ExcludedIds,ExcludedPred,
    statistics(NIncludedIds,NExcludedIds,NIncludedPreds,NExcludedPreds)) :-
    predicate_length(IncludedPred,NIncludedPreds),
    predicate_length(ExcludedPred,NExcludedPreds),
    length(IncludedIds,NIncludedIds),
    length(ExcludedIds,NExcludedIds).

equation_slicing(Selected,Predicate,Identifiers,IncludedIds,IncludedPred,ExcludedIds,ExcludedPred) :-
    conjunction_to_list(Predicate,Predicates),
    % first just use the equations for slicing
    equation_slicing2(Selected,Predicates,Identifiers,[],UsedIds,OtherIds,RestPredicates,Equations),
    conjunct_predicates(RestPredicates,RestPredicate),
    % For the ids that have been encountered but are not defined by equations, we use the
    % slicing by predicate partitions
    predicate_slicing(OtherIds,RestPredicate,IncludedIds1,IncludedPred1,ExcludedIds,ExcludedPred),
    list_to_ord_set(UsedIds,IncludedIds2),
    ord_union(IncludedIds1,IncludedIds2,IncludedIds),
    conjunct_predicates([IncludedPred1|Equations],IncludedPred).

equation_slicing2([],Predicates,_Identifiers,Used,Used,[],Predicates,[]).

equation_slicing2([Sel|Srest],Predicates,Identifiers,UsedOld,UsedNew,NEE,SP,Eq) :-
    ( memberchk(Sel,UsedOld) -> % identifier was already processed
    equation_slicing2(Srest,Predicates,Identifiers,UsedOld,UsedNew,NEE,SP,Eq)
    ; nonmember(Sel,Identifiers) -> % an id that is not relevant for us (e.g. an enumerated set element)
    equation_slicing2(Srest,Predicates,Identifiers,UsedOld,UsedNew,NEE,SP,Eq)
    ; contains_equation(Sel,Predicates,Expression,Equation,RestPredicates) -> % we found an equation!
    Eq = [Equation|Erest], % store it
    find_identifier_uses(Expression,UsedOld,NewIds), % extract all used identifiers in the equation
    append(NewIds,Srest,NewSelected), % and continue with all found identifiers recursively
    equation_slicing2(NewSelected,RestPredicates,Identifiers,[Sel|UsedOld],UsedNew,NEE,SP,Erest)
    ; % we encountered an identifier that seems to be relevant but is not defined by an equation
    NEE = [Sel|Nrest], % we just store it for later use
    equation_slicing2(Srest,Predicates,Identifiers,[Sel|UsedOld],UsedNew,Nrest,SP,Eq)).

erase_unnecessary_mparts(Orig,Clean) :-
    write_section(abstract_variables,[],Orig,M1),
    write_section(concrete_variables,[],M1,M2),
    write_section(concrete_constants,[],M2,M3),
    write_section(promoted,[],M3,M4),
    write_section(unpromoted,[],M4,M5),
   
    create_texpr(truth,pred,[],Truth),
    write_section(invariant,Truth,M5,M6),
    write_section(assertions,[],M6,M7),
   
    write_section(initialisation,[],M7,M8),
    write_section(operation_bodies,[],M8,M9),
   
    write_section(definitions,[],M9,Clean).

get_component_id(component(_,I),I).

get_component_pred(component(P,_),P).

is_interesting_component(SelectedIds,component(_Pred,UIds)) :-
    list_to_ord_set(UIds,Ids),
    ord_intersect(SelectedIds,Ids).

join_components(Components,Ids,Predicate) :-
    maplist(get_component_pred, Components, Predicates),
    conjunct_predicates(Predicates,Predicate),
   
    maplist(get_component_id, Components, IdLists),
    append(IdLists,Ids).

predicate_length(Pred,NPreds) :-
    conjunction_to_list(Pred,Ps),length(Ps,NPreds).

predicate_slicing(UIdentifiers,Predicate,IncludedIds,IncludedPred,ExcludedIds,ExcludedPred) :-
    list_to_ord_set(UIdentifiers,Identifiers),
    predicate_components(Predicate,Components),
    split_list(is_interesting_component(Identifiers),Components,Included,Excluded),
    join_components(Included,IncludedIds,IncludedPred),
    join_components(Excluded,ExcludedIds,ExcludedPred).

slice_machine_properties_by_constants(Selected,Statistics,Machine) :-
    b_get_properties_from_machine(Predicate),
    b_get_machine_constants(Constants),get_texpr_ids(Constants,CIds),
    %predicate_slicing(Selected,Predicate,IncludedIds,IncludedPred,ExcludedIds,ExcludedPred),
    equation_slicing(Selected,Predicate,CIds,IncludedIds,IncludedPred,ExcludedIds,ExcludedPred),
    do_simple_statistics(IncludedIds,IncludedPred,ExcludedIds,ExcludedPred,Statistics),
    construct_property_machine(IncludedIds,IncludedPred,Machine).