symmetry_reduction

get_equivalent_operators_post_symmetry_reduction(Solution,SymmetricComponents,LocationVarsOut,EquivalentOperatorsReduction) :-
    split_equivalent_components(SymmetricComponents,[],EquivalentComponents) ,
    maplist(get_equivalent_operators_post_symmetry_reduction_aux(Solution,LocationVarsOut),EquivalentComponents,EquivalentOperatorsReductions) ,
    conjunct_predicates(EquivalentOperatorsReductions,EquivalentOperatorsReduction).

get_equivalent_operators_post_symmetry_reduction_aux(Solution,LocationVarsOut,EquivalentComponents,EquivalentOperatorsReductions) :-
    findall((C1,C2),(member(C1,EquivalentComponents) , member(C2,EquivalentComponents) , C1 \= C2),EquivalentComponentPairs) ,
    get_equivalent_operators_post_symmetry_reduction_aux2(Solution,LocationVarsOut,EquivalentComponentPairs,EquivalentOperatorsReductions).

get_equivalent_operators_post_symmetry_reduction_aux2(Solution,LocationVarsOut,[EquivalentComponentPair|T],EquivalentOperatorsReductions) :-
    get_operators_post_symmetry_reduction_for_pair(EquivalentComponentPair,Solution,LocationVarsOut,PairReduction) ,
    get_equivalent_operators_post_symmetry_reduction_aux2(Solution,LocationVarsOut,T,PairReduction,EquivalentOperatorsReductions).

get_equivalent_operators_post_symmetry_reduction_aux2(_,_,[],Acc,Acc).

get_equivalent_operators_post_symmetry_reduction_aux2(Solution,LocationVarsOut,[EquivalentComponentPair|T],Acc,EquivalentOperatorsReductions) :-
    get_operators_post_symmetry_reduction_for_pair(EquivalentComponentPair,Solution,LocationVarsOut,PairReduction) ,
    create_texpr(conjunct(PairReduction,Acc),pred,[],NewAcc) ,
    get_equivalent_operators_post_symmetry_reduction_aux2(Solution,LocationVarsOut,T,NewAcc,EquivalentOperatorsReductions).

get_location_var_from_list(InternalName,ComponentType,LocationVars,LocationVar) :-
    member(LocationVar,LocationVars) ,
    get_texpr_info(LocationVar,Info) ,
    member(synthesis(InternalName,ComponentType),Info).

get_mapped_output_location(InputLocation,Solution,OutputLocation) :-
    member(binding(InputLocation,_,InputLocationValue),Solution) ,
    get_mapped_output_location_by_value(InputLocationValue,Solution,OutputLocation).

get_mapped_output_location_by_value(InputLocationValue,Solution,OutputLocation) :-
    member(binding(OutputLocation,_,InputLocationValue),Solution) ,
    (atom_concat(lo,_,OutputLocation) ; atom_concat(linput,_,OutputLocation)).

get_operator_symmetry_reduction(Components,LocationVarsOut,SymmetryReduction) :-
    split_equivalent_components(Components,[],EquivalentComponents) ,
    maplist(get_operator_symmetry_reduction_aux(LocationVarsOut,[]),EquivalentComponents,SymmetryExclusionList) ,
    conjunct_predicates(SymmetryExclusionList,SymmetryReduction).

get_operator_symmetry_reduction_aux(_,Acc,[],SymmetryReduction) :-
    conjunct_predicates(Acc,SymmetryReduction).

get_operator_symmetry_reduction_aux(LocationVarsOut,Acc,[Components|T],SymmetryReduction) :-
    % skip single components
    length(Components,Length) ,
    Length > 1 , !,
    get_operator_symmetry_reduction_aux2(Components,LocationVarsOut,[],OperatorReduction) ,
    get_operator_symmetry_reduction_aux(LocationVarsOut,[OperatorReduction|Acc],T,SymmetryReduction).

get_operator_symmetry_reduction_aux(LocationVarsOut,Acc,[_|T],SymmetryReduction) :-
    get_operator_symmetry_reduction_aux(LocationVarsOut,Acc,T,SymmetryReduction).

get_operator_symmetry_reduction_aux2([_],_,Acc,OperatorReduction) :-
    conjunct_predicates(Acc,OperatorReduction).

get_operator_symmetry_reduction_aux2([(_,InternalName1),(Name,InternalName2)|T],LocationVarsOut,Acc,OperatorReduction) :-
    get_location_var_from_list(InternalName1,output,LocationVarsOut,LocationVarOutComp1) ,
    get_location_var_from_list(InternalName2,output,LocationVarsOut,LocationVarOutComp2) ,
    NewAcc = [b(less_equal(LocationVarOutComp1,LocationVarOutComp2),pred,[])|Acc] ,
    get_operator_symmetry_reduction_aux2([(Name,InternalName2)|T],LocationVarsOut,NewAcc,OperatorReduction).

get_operators_post_symmetry_reduction_for_pair((ComponentName1,ComponentName2),Solution,LocationVarsOut,PairReduction) :-
    % get the output location variables that are mapped to left and right input of the component
    % the components are symmetric and thus have two inputs
    get_location_var_from_list(ComponentName1,left_input,LocationVarsOut,b(identifier(C1LeftLocationVarName),_,_)) ,
    get_mapped_output_location(C1LeftLocationVarName,Solution,C1LeftMappedOutputLocationName) ,
    get_location_var_from_list(ComponentName1,right_input,LocationVarsOut,b(identifier(C1RightLocationVarName),_,_)) ,
    get_mapped_output_location(C1RightLocationVarName,Solution,C1RightMappedOutputLocationName) ,
    C1LeftMappedOutputLocationName \= C1RightMappedOutputLocationName , % not the same operator mapped to both locations, otherwise we may loose solutions
    % create inequality with the input locations of the equivalent symmetric component
    get_location_var_from_list(ComponentName2,left_input,LocationVarsOut,C2LeftLocationVar) ,
    get_location_var_from_list(ComponentName2,right_input,LocationVarsOut,C2RightLocationVar) ,
    create_texpr(not_equal(b(identifier(C1LeftMappedOutputLocationName),integer,[]),C2RightLocationVar),pred,[],C1LOutC2RInReduction) ,
    create_texpr(not_equal(b(identifier(C1RightMappedOutputLocationName),integer,[]),C2LeftLocationVar),pred,[],C1ROutC2LInReduction) ,
    create_texpr(conjunct(C1LOutC2RInReduction,C1ROutC2LInReduction),pred,[],PairReduction).

get_operators_post_symmetry_reduction_for_pair(_,_,_,b(truth,pred,[])).

get_post_symmetry_reduction_constraint(Components,Solution,LocationVarsIn,LocationVarsOut,SymmetryReduction) :-
    get_symmetric_components(Components,SymmetricComponents) ,
    (SymmetricComponents = []
    -> ! , SymmetryReduction = b(truth,pred,[])
    ; get_post_symmetry_reduction_constraint_aux(SymmetricComponents,Solution,LocationVarsIn,LocationVarsOut,SymmetryReduction)).

get_post_symmetry_reduction_constraint_aux(SymmetricComponents,Solution,LocationVarsIn,LocationVarsOut,SymmetryReduction) :-
    get_single_operator_post_symmetry_reduction(SymmetricComponents,Solution,LocationVarsIn,LocationVarsOut,SingleOperatorReduction) ,
    get_equivalent_operators_post_symmetry_reduction(Solution,SymmetricComponents,LocationVarsOut,EquivalentOperatorsReduction) ,
    create_texpr(conjunct(SingleOperatorReduction,EquivalentOperatorsReduction),pred,[],SymmetryReduction).

get_preliminary_symmetry_reduction_constraint(Components,LocationVarsIn,LocationVarsOut,SymmetryReduction) :-
    get_symmetric_components(Components,SymmetricComponents) ,
    maplist(get_single_operand_symmetry_reduction(LocationVarsIn),SymmetricComponents,OperandExclusionList) ,
    get_operator_symmetry_reduction(Components,LocationVarsOut,OperatorReductionPredicate) ,
    conjunct_predicates([OperatorReductionPredicate|OperandExclusionList],SymmetryReduction).

get_single_operand_symmetry_reduction(LocationVarsIn,Expression,SymmetryReduction) :-
    Expression = (_,InternalName) ,
    get_location_var_from_list(InternalName,left_input,LocationVarsIn,LeftLocationVarIn) ,
    get_location_var_from_list(InternalName,right_input,LocationVarsIn,RightLocationVarIn) ,
    SymmetryReduction = b(less_equal(LeftLocationVarIn,RightLocationVarIn),pred,[]).

get_single_operator_post_symmetry_reduction([(_,InternalName)|T],Solution,LocationVarsIn,LocationVarsOut,SingleOperatorReductionConj) :-
    get_single_operator_post_symmetry_reduction_aux(InternalName,Solution,LocationVarsIn,LocationVarsOut,SingleOperatorReduction) ,
    get_single_operator_post_symmetry_reduction(T,Solution,LocationVarsIn,LocationVarsOut,SingleOperatorReduction,SingleOperatorReductionConj).

get_single_operator_post_symmetry_reduction([],_,_,_,Acc,Acc).

get_single_operator_post_symmetry_reduction([(_,InternalName)|T],Solution,LocationVarsIn,LocationVarsOut,Acc,SingleOperatorReductionConj) :-
    get_single_operator_post_symmetry_reduction_aux(InternalName,Solution,LocationVarsIn,LocationVarsOut,SingleOperatorReduction) ,
    create_texpr(conjunct(Acc,SingleOperatorReduction),pred,[],NewAcc) ,
    get_single_operator_post_symmetry_reduction(T,Solution,LocationVarsIn,LocationVarsOut,NewAcc,SingleOperatorReductionConj).

get_single_operator_post_symmetry_reduction_aux(InternalName,Solution,LocationVarsIn,_LocationVarsOut,SingleOperatorReduction) :-
    get_single_operator_post_symmetry_reduction_aux2(left_input,right_input,InternalName,Solution,LocationVarsIn,LRReduction) ,
    get_single_operator_post_symmetry_reduction_aux2(right_input,left_input,InternalName,Solution,LocationVarsIn,RLReduction) ,
    create_texpr(conjunct(LRReduction,RLReduction),pred,[],SingleOperatorReduction).

get_single_operator_post_symmetry_reduction_aux2(I1,I2,InternalName,Solution,LocationVarsIn,Reduction) :-
    get_location_var_from_list(InternalName,I1,LocationVarsIn,Input1LocationVar) ,
    Input1LocationVar = b(identifier(Input1LocationName),_,_) ,
    get_mapped_output_location(Input1LocationName,Solution,MappedOutputLocationName) ,
    get_location_var_from_list(InternalName,I2,LocationVarsIn,Input2LocationVar) ,
    create_texpr(not_equal(b(identifier(MappedOutputLocationName),integer,[]),Input2LocationVar),pred,[],Reduction).

get_symmetric_components(Components,SymmetricComponents) :-
    get_symmetric_components(Components,[],SymmetricComponents).

get_symmetric_components([],Acc,Acc).

get_symmetric_components([(Name,InternalName)|T],Acc,SymmetricComponents) :-
    Name \= constant-_ ,
    is_symmetric(Name) ,
    get_symmetric_components(T,[(Name,InternalName)|Acc],SymmetricComponents).

get_symmetric_components([_|T],Acc,SymmetricComponents) :-
    get_symmetric_components(T,Acc,SymmetricComponents).

is_symmetric(not_equal).

is_symmetric(equal).

is_symmetric(conjunct).

is_symmetric(disjunct).

is_symmetric(equivalence).

is_symmetric(add).

is_symmetric(multiplication).

is_symmetric(union).

is_symmetric(intersection).

split_equivalent_components([],Acc,Acc).

split_equivalent_components([(Name,InternalName)|T],Acc,EquivalentComponentsList) :-
    Name \= constant-_ ,
    findall(EquiInternalName,(member((_,EquiInternalName),T) , EquiInternalName = InternalName),EquivalentComponents) ,
    subtract(T,EquivalentComponents,NT) ,
    split_equivalent_components(NT,[(Name,InternalName)|Acc],EquivalentComponentsList).

split_equivalent_components([_|T],Acc,EquivalentComponentsList) :-
    split_equivalent_components(T,Acc,EquivalentComponentsList).