library_setup

add_constants(UserLibrary,Int,Bool,SetTypes,SeqTypes,IndependentTypes,ConstantComponents) :-
    length(IntConstants,Int) ,
    findall(IntConstant,(member(IntConstant,IntConstants) , IntConstant = constant-integer),IntConstants) ,
    length(BoolConstants,Bool) ,
    findall(BoolConstant = constant-boolean,(member(BoolConstant,BoolConstants)),BoolConstants) ,
    findall(constant-SetType,member(SetType,SetTypes),SetConstants) ,
    findall(constant-SeqType,member(SeqType,SeqTypes),SeqConstants) ,
    findall(constant-IndependentType,member(IndependentType,IndependentTypes),IndConstants) ,
    findall(constant-set(IndependentType),member(IndependentType,IndependentTypes),SetIndConstants) ,
    append([IntConstants,BoolConstants,SetConstants,SeqConstants,IndConstants,SetIndConstants],TempConstantComponents) ,
    add_set_constants_for_seq_relations(UserLibrary,SeqTypes,TempConstantComponents,ConstantComponents).

add_set_constants_as_op_params_for_independent_types(MachineSets,SetConstants) :-
    add_set_constants_as_op_params_for_independent_types(MachineSets,[],SetConstants).

add_set_constants_as_op_params_for_independent_types([],Acc,Acc).

add_set_constants_as_op_params_for_independent_types([MachineSet|T],Acc,SetConstants) :-
    MachineSet = b(_,set(global(IndependentType)),_) ,
    add_set_constants_as_op_params_for_independent_types(T,[param_constant-set(global(IndependentType)),param_constant-global(IndependentType)|Acc],SetConstants).

add_set_constants_for_seq_relations(UserLibrary,SeqTypes,TempConstantComponents,ConstantComponents) :-
    member(relations(Relations),UserLibrary) ,
    length(Relations,RelationAmount) ,
    add_set_constants_for_seq_relations_aux(RelationAmount,SeqTypes,[],SetConstants) ,
    append(TempConstantComponents,SetConstants,ConstantComponents).

add_set_constants_for_seq_relations(_,_,ConstantComponents,ConstantComponents).

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

add_set_constants_for_seq_relations_aux(RelationAmount,[SeqType|T],Acc,SetConstants) :-
    length(Constants,RelationAmount) ,
    SeqType = seq(InnerType) ,
    findall(Constant,(member(Constant,Constants) , Constant = constant-set(InnerType)),Constants) ,
    append(Constants,Acc,NewAcc) ,
    add_set_constants_for_seq_relations_aux(RelationAmount,T,NewAcc,SetConstants).

add_skip_components(action,TComponents,Int,Bool,SetTypes,SeqTypes,IndependentTypes,Components) :-
    length(IntDummies,Int) ,
    findall(Skip,(member(Skip,IntDummies) , Skip = skip-integer),SkipInts) ,
    length(BoolDummies,Bool) ,
    findall(Skip,(member(Skip,BoolDummies) , Skip = skip-boolean),SkipBools) ,
    findall(Skip,(member(SetType,SetTypes) , Skip = skip-SetType),SkipSets) ,
    findall(Skip,(member(SeqType,SeqTypes) , Skip = skip-SeqType),SkipSeqs) ,
    findall(Skip,(member(IndependentType,IndependentTypes) , Skip = skip-IndependentType),SkipInd) ,
    append([TComponents,SkipInts,SkipBools,SkipSets,SkipSeqs,SkipInd],Components).

add_skip_components(SynthesisType,Components,_,_,_,_,_,Components) :-
    SynthesisType \= action.

count_var_types(Example,LInt,LBool,(LSet,SetTypes),(LSeq,SeqTypes),(LIndependent,IndependentTypes)) :-
    findall(Val,member(b(Val,integer,_),Example),Int) ,
    findall(Val,member(b(Val,boolean,_),Example),Bool) ,
    findall(Type,(member(b(Node,Type,_),Example) , Type = seq(_)),SeqTypes) ,
    findall(Type,(member(b(Node,Type,_),Example) , Type = set(_)),SetTypes) ,
    findall(Type,(member(b(Node,Type,_),Example) , Type = global(_)),IndependentTypes) ,
    length(Int,LInt) , length(Bool,LBool) , length(SetTypes,LSet) , length(SeqTypes,LSeq) , length(IndependentTypes,LIndependent).

encode_component_type(integer,intOp).

encode_component_type(bool,boolOp).

encode_component_type(set(Type),setOp-set(Type)).

encode_component_type(seq(Type),seqOp-seq(Type)).

extend_components_to_consider_if_statements([],_,_,Components,Components).

extend_components_to_consider_if_statements([ConsiderIfVarName|T],NotConsiderConstants,LibExpansion,Components,ExtendedComponents) :-
    get_machinevars_by_name([ConsiderIfVarName],[MachineVar]) ,
    get_texpr_type(MachineVar,MachineVarType) ,
    encode_component_type(MachineVarType,ComponentType) ,
    % besides adding the if_then_else component itself we need to consider appropriate operators for the condition
    % TODO: assume that initially all if-statements have the same condition to reduce the overhead of considering too much preciates in addition to expressions needed for synthesizing the substitution
    % therefore, implement an own library expansion for the condition of if-statements relaxing this assumption successively
    library_add_component_aux(guard,NotConsiderConstants,LibExpansion,ComponentType,[],ConditionComponents) ,
    append(Components,[if_then_else-MachineVarType|ConditionComponents],NewComponents) ,
    extend_components_to_consider_if_statements(T,NotConsiderConstants,LibExpansion,NewComponents,ExtendedComponents).

get_larger_sublist(Sub1,Sub2,Sub1) :-
    length(Sub1,L1) , length(Sub2,L2) ,
    L1 > L2.

get_larger_sublist(_,Sub2,Sub2).

library_add_arithmetic_components(action,C,Acc,[add,minus|Acc]) :- C = 1 ; C = 2.

library_add_arithmetic_components(action,C,Acc,[multiplication,power_of|Acc]) :- C = 3 ; C = 4.

library_add_arithmetic_components(action,C,Acc,[multiplication,div|Acc]) :- C = 5 ; C = 6.

library_add_arithmetic_components(action,C,Acc,[multiplication,div,add|Acc]) :- C = 7 ; C = 8.

library_add_arithmetic_components(action,C,Acc,[div,modulo|Acc]) :- C = 9 ; C = 10.

library_add_arithmetic_components(action,C,Acc,[multiplication,div,modulo|Acc]) :- C = 11 ; C = 12.

library_add_arithmetic_components(action,C,Acc,[multiplication,div|Acc]) :- C = 13 ; C = 14.

library_add_arithmetic_components(action,_,Acc,[add,minus,multiplication,div,modulo,power_of|Acc]).

library_add_arithmetic_components(_,C,Acc,Acc) :- C = 1 ; C = 2.

library_add_arithmetic_components(_,C,Acc,[add,minus|Acc]) :- C = 3 ; C = 4.

library_add_arithmetic_components(_,C,Acc,[multiplication,power_of|Acc]) :- C = 5 ; C = 6.

library_add_arithmetic_components(_,C,Acc,[multiplication,div|Acc]) :- C = 7 ; C = 8.

library_add_arithmetic_components(_,C,Acc,[multiplication,div,add|Acc]) :- C = 9 ; C = 10.

library_add_arithmetic_components(_,C,Acc,[div,modulo|Acc]) :- C = 11 ; C = 12.

library_add_arithmetic_components(_,C,Acc,[multiplication,div,modulo|Acc]) :- C = 13 ; C = 14.

library_add_arithmetic_components(_,C,Acc,[multiplication,div|Acc]) :- C = 15 ; C = 16.

library_add_arithmetic_components(_,_,Acc,[add,minus,multiplication,div,modulo,power_of|Acc]).

library_add_boolean_components(action,1,Acc,[convert_bool,subset-set(integer),skip-boolean|Acc]).

library_add_boolean_components(_,1,Acc,[equal-boolean|Acc]).

library_add_boolean_components(_,_,Acc,[equal-boolean,convert_bool,subset-set(integer)|Acc]).

library_add_component_aux(_,_,_,_-[],Acc,Acc).

library_add_component_aux(SynthesisType,NotConsiderConstants,LibExpansion,independent-Type,Acc,NewAcc) :-
    library_add_indepentend_type_components(SynthesisType,LibExpansion,Type,Acc,TempAcc) ,
    (NotConsiderConstants = no -> NewAcc = [constant-Type|TempAcc] ; NewAcc = TempAcc).

library_add_component_aux(SynthesisType,NotConsiderConstants,LibExpansion,intOp,Acc,NewAcc) :-
    library_add_integer_components(SynthesisType,LibExpansion,Acc,TempAcc),
    (NotConsiderConstants = no -> NewAcc = [constant-integer|TempAcc] ; NewAcc = TempAcc).

library_add_component_aux(SynthesisType,NotConsiderConstants,LibExpansion,boolOp,Acc,NewAcc) :-
    library_add_boolean_components(SynthesisType,LibExpansion,Acc,TempAcc) ,
    ((NotConsiderConstants = no) , (SynthesisType \= action) -> NewAcc = [constant-boolean|TempAcc] ; NewAcc = TempAcc).

library_add_component_aux(SynthesisType,NotConsiderConstants,LibExpansion,arithmetic,Acc,NewAcc) :-
    library_add_arithmetic_components(SynthesisType,LibExpansion,Acc,TempAcc) ,
    (NotConsiderConstants = no -> NewAcc = [constant-integer|TempAcc] ; NewAcc = TempAcc).

library_add_component_aux(SynthesisType,NotConsiderConstants,LibExpansion,setOp-SetType,Acc,NewAcc) :-
    library_add_set_components(SynthesisType,LibExpansion,SetType,Acc,TempAcc) ,
    (NotConsiderConstants = no
    -> (SynthesisType = action -> NewAcc = [constant-SetType|TempAcc] ; NewAcc = [constant-SetType,constant-integer|TempAcc]) % integer constant for card(_) > _
    ; NewAcc = TempAcc).

library_add_component_aux(SynthesisType,NotConsiderConstants,LibExpansion,seqOp-SeqType,Acc,NewAcc) :-
    (SeqType = seq(_) ; SeqType = set(couple(integer,_))) ,
    library_add_seq_components(SynthesisType,LibExpansion,SeqType,TLibrary) ,
    % use constant of type seq(_)
    append([TLibrary,Acc],TempAcc) ,
    SeqType = seq(InnerType) , % add set constant for components like domain_restriction
    (NotConsiderConstants = no
    -> (SynthesisType = action -> NewAcc = [constant-SeqType,constant-set(InnerType)|TempAcc] ; NewAcc = [constant-SeqType,constant-integer|TempAcc])
    ; NewAcc = TempAcc).

library_add_components(Type,_,0,arithmetic,_,Acc,Acc) :-
    (Type = guard ; Type = invariant) , !.

library_add_components(_,_,_,_,0,Acc,Acc).

library_add_components(Type,NotConsiderConstants,LibExpansion,OpType,VarAmount,Acc,Library) :-
    NVarAmount is VarAmount - 1 ,
    (OpType = TOp-[ExactType|RTypes]
    % get the type from the list of set/seq/independent types
    -> Op = TOp-ExactType ,
    NOpType = TOp-RTypes
    ; Op = OpType ,
    NOpType = OpType) ,
    library_add_component_aux(Type,NotConsiderConstants,LibExpansion,Op,Acc,Operators) ,
    library_add_components(Type,NotConsiderConstants,LibExpansion,NOpType,NVarAmount,Operators,Library).

library_add_conn(action,_,_,[],[]).

library_add_conn(_,LibExpansion,Example,Or,And) :-
    length(Example,VarAmount) ,
    (LibExpansion mod 2 =\= 0 , VarAmount > 2 -> Div = 3 ; Div = 2) ,
    %C is round(VarAmount/2) ,
    TempC is VarAmount / Div ,
    (TempC = 0.5 -> C = 0 ; C is floor(TempC)) ,
    library_add_conn_aux(C,Or,And).

library_add_conn_aux(C,Or,And) :-
    length(And,C) , length(Or,C) ,
    findall(A,(member(A,And), A = conjunct),And) ,
    findall(O,(member(O,Or), O = disjunct),Or).

library_add_indepentend_type_components(action,_,Type,Acc,[skip-Type|Acc]).

library_add_indepentend_type_components(SynthesisType,_,Type,Acc,[equal-Type,not_equal-Type|Acc]) :-
    SynthesisType \= action.

library_add_integer_components(action,_,Acc,[skip-integer|Acc]).

library_add_integer_components(_,C,Acc,[greater|Acc]) :- C = 1 ; C = 2.

library_add_integer_components(_,_,Acc,[greater,equal-integer|Acc]).

library_add_seq_components(action,C,SeqType,[concat-SeqType,skip-SeqType]) :- C = 1 ; C = 2.

library_add_seq_components(action,C,SeqType,[overwrite-SeqType,concat-SeqType,skip-SeqType]) :- C = 3 ; C = 4.

library_add_seq_components(action,C,SeqType,[insert_tail-SeqType,domain-SeqType,domain_restriction-SeqType,skip-SeqType]) :- C = 5 ; C = 6.

library_add_seq_components(action,C,SeqType,[insert_front-SeqType,insert_tail-SeqType,domain-SeqType,domain_restriction-SeqType,range_restriction-SeqType,skip-SeqType]) :- C = 7 ; C = 8.

library_add_seq_components(action,C,SeqType,[concat-SeqType,first-SeqType,last-SeqType,skip-SeqType]) :- C = 9 ; C = 10.

library_add_seq_components(action,C,SeqType,[concat-SeqType,domain_restriction-SeqType,range_restriction-SeqType,domain_subtraction-SeqType,domain_restriction-SeqType,skip-SeqType]) :- C = 11 ; C = 12.

library_add_seq_components(action,_,SeqType,[overwrite-SeqType,concat-SeqType,insert_tail-SeqType,insert_front-SeqType,first-SeqType,last-SeqType,domain_restriction-SeqType,range_restriction-SeqType,domain_subtraction-SeqType,domain_restriction-SeqType,skip-SeqType]).

library_add_seq_components(_,C,SeqType,[card-SeqType,greater,equal-integer]) :- C = 1 ; C = 2. % member-set(seq(integer)),seq-integer_set

library_add_seq_components(_,C,SeqType,[card-SeqType,greater,equal-integer,range-SeqType,domain-SeqType,equal-SeqType]) :- C = 3 ; C = 4.

library_add_seq_components(_,C,SeqType,[range-SeqType,domain-SeqType,image-SeqType,reverse-SeqType,equal-SeqType]) :- C = 5 ; C = 6.

library_add_seq_components(_,C,SeqType,[range_restriction-SeqType,range_subtraction-SeqType,domain_restriction-SeqType,domain_subtraction-SeqType,
    equal-SeqType]) :- C = 7 ; C = 8.

library_add_seq_components(_,_,SeqType,[restrict_front-SeqType,restrict_tail-SeqType,range_restriction-SeqType,range_subtraction-SeqType,
    domain_restriction-SeqType,domain_subtraction-SeqType,range-SeqType,domain-SeqType,image-SeqType,equal-SeqType,
    first-SeqType,last-SeqType,union-SeqType,equal-SeqType]).

library_add_set_components(action,C,SetType,Acc,[union-SetType,skip-SetType|Acc]) :-
    SetType = set(set(_)) , C = 1 ; C = 2.

library_add_set_components(action,C,SetType,Acc,[set_subtraction-SetType,skip-SetType|Acc]) :-
    SetType = set(set(_)) , C = 3 ; C = 4.

library_add_set_components(action,C,SetType,Acc,[intersection-SetType,skip-SetType|Acc]) :-
    SetType = set(set(_)) , C = 5 ; C = 6.

library_add_set_components(action,C,SetType,Acc,[general_union-SetType,skip-SetType|Acc]) :-
    SetType = set(set(_)) , C = 7 ; C = 8.

library_add_set_components(action,C,SetType,Acc,[general_intersection-SetType,skip-SetType|Acc]) :-
    SetType = set(set(_)) , C = 9 ; C = 10.

library_add_set_components(action,C,SetType,Acc,[union-SetType,set_subtraction-SetType,general_union-SetType,general_intersection-SetType,skip-SetType|Acc]) :-
    SetType = set(set(_)) , C = 11 ; C = 12.

library_add_set_components(action,C,SetType,Acc,[union-SetType,intersection-SetType,set_subtraction-SetType,skip-SetType|Acc]) :-
    SetType = set(set(_)) , C = 13 ; C = 14.

library_add_set_components(action,_,SetType,Acc,[cartesian_product-SetType,union-SetType,set_subtraction-SetType,intersection-SetType,general_union-SetType,general_intersection-SetType,skip-SetType|Acc]) :-
    SetType = set(set(_)).

library_add_set_components(action,C,SetType,Acc,[union-SetType,skip-SetType|Acc]) :-
    SetType \= set(set(_)) , C = 1 ; C = 2.

library_add_set_components(action,C,SetType,Acc,[set_subtraction-SetType,skip-SetType|Acc]) :-
    SetType \= set(set(_)) , C = 3 ; C = 4.

library_add_set_components(action,C,SetType,Acc,[intersection-SetType,skip-SetType|Acc]) :-
    SetType \= set(set(_)) , C = 5 ; C = 6.

library_add_set_components(action,C,SetType,Acc,[union-SetType,set_subtraction-SetType,skip-SetType|Acc]) :-
    SetType \= set(set(_)) , C = 7 ; C = 8.

library_add_set_components(action,C,SetType,Acc,[union-SetType,intersection-SetType,skip-SetType|Acc]) :-
    SetType \= set(set(_)) , C = 9 ; C = 10.

library_add_set_components(action,C,SetType,Acc,[set_subtraction-SetType,intersection-SetType,skip-SetType|Acc]) :-
    SetType \= set(set(_)) , C = 11 ; C = 12.

library_add_set_components(action,C,SetType,Acc,[union-SetType,set_subtraction-SetType,intersection-SetType,skip-SetType,max,min|Acc]) :-
    SetType = set(integer) , C = 13 ; C = 14.

library_add_set_components(action,C,SetType,Acc,[union-SetType,set_subtraction-SetType,intersection-SetType,skip-SetType|Acc]) :-
    SetType \= set(set(_)) , C = 13 ; C = 14.

library_add_set_components(action,C,SetType,Acc,[union-SetType,intersection-SetType,cartesian_product-SetType,skip-SetType|Acc]) :-
    SetType \= set(set(_)) , C = 15 ; C = 16.

library_add_set_components(action,C,SetType,Acc,[union-SetType,set_subtraction-SetType,intersection-SetType,cartesian_product-SetType,skip-SetType|Acc]) :-
    SetType \= set(set(_)) , C = 17 ; C = 18.

library_add_set_components(action,_,SetType,Acc,[union-SetType,set_subtraction-SetType,cartesian_product-SetType,intersection-SetType,skip-SetType,max,min|Acc]) :-
    SetType = set(integer).

library_add_set_components(_,C,SetType,Acc,[member-SetType,not_member-SetType|Acc]) :- C = 1 ; C = 2.

library_add_set_components(_,C,SetType,Acc,[not_equal-SetType,equal-SetType|Acc]) :- C = 3 ; C = 4.

library_add_set_components(_,C,SetType,Acc,[member-SetType,not_equal-SetType|Acc]) :- C = 5 ; C = 6.

library_add_set_components(_,C,SetType,Acc,[member-SetType,equal-SetType|Acc]) :- C = 7 ; C = 8.

library_add_set_components(_,C,SetType,Acc,[not_member-SetType,not_equal-SetType|Acc]) :- C = 9 ; C = 10.

library_add_set_components(_,C,SetType,Acc,[not_member-SetType,equal-SetType|Acc]) :- C = 11 ; C = 12.

library_add_set_components(_,C,SetType,Acc,[member-SetType,not_member-SetType,equal-SetType,not_equal-SetType|Acc]) :- C = 13 ; C = 14.

library_add_set_components(_,C,SetType,Acc,[member-SetType,not_member-SetType,equal-SetType,not_equal-SetType,union-SetType,intersection-SetType,set_subtraction-SetType|Acc]) :- C = 15 ; C = 16.

library_add_set_components(_,C,SetType,Acc,[card-SetType,greater,equal-integer|Acc]) :- C = 17 ; C = 18.

library_add_set_components(_,C,SetType,Acc,[union-SetType,intersection-SetType,equal-SetType|Acc]) :- C = 19 ; C = 20.

library_add_set_components(_,C,SetType,Acc,[union-SetType,intersection-SetType,not_equal-SetType|Acc]) :- C = 21 ; C = 22.

library_add_set_components(_,C,SetType,Acc,[intersection-SetType,union-SetType,equal-SetType,not_equal-SetType|Acc]) :- C = 23 ; C = 24.

library_add_set_components(_,C,SetType,Acc,[intersection-SetType,union-SetType,set_subtraction-SetType,equal-SetType,not_equal-SetType|Acc]) :- C = 25 ; C = 26.

library_add_set_components(_,C,SetType,Acc,[member-SetType,not_member-SetType,card-SetType,greater,equal-integer,union-SetType|Acc]) :- C = 27 ; C = 28.

library_add_set_components(_,C,SetType,Acc,[member-SetType,not_member-SetType,card-SetType,greater,equal-integer,union-SetType,intersection-SetType,set_subtraction-SetType|Acc]) :- C = 29 ; C = 30.

library_add_set_components(_,C,SetType,Acc,[equal-SetType,member-SetType,subset-SetType,subset_strict-SetType,negation|Acc]) :- C = 31 ; C = 32.

library_add_set_components(_,C,SetType,Acc,[card-SetType,greater,equal-integer,member-SetType,subset_strict-SetType,subset-SetType,negation|Acc]) :-
    SetType \= set(integer) , C = 33 ; C = 34.

library_add_set_components(_,C,SetType,Acc,[card-SetType,max,min,greater,equal-integer,member-SetType,subset_strict-SetType,subset-SetType,negation|Acc]) :-
    SetType = set(integer) , C = 33 ; C = 34.

library_add_set_components(_,_,SetType,Acc,[max,min,card-SetType,greater,equal-integer,equal-SetType,not_equal-SetType,subset-SetType,subset_strict-SetType,general_union-SetType,general_intersection-SetType,set_subtraction-SetType,member-SetType,negation,not_member-SetType|Acc]) :-
    SetType = set(integer).

library_add_set_components(_,_,SetType,Acc,[card-SetType,greater,equal-integer,equal-SetType,not_equal-SetType,subset-SetType,subset_strict-SetType,general_union-SetType,general_intersection-SetType,set_subtraction-SetType,member-SetType,negation,not_member-SetType|Acc]) :-
    SetType = set(set(_)).

library_add_set_components(_,_,SetType,Acc,[card-SetType,greater,equal-integer,equal-SetType,not_equal-SetType,subset-SetType,subset_strict-SetType,union-SetType,intersection-SetType,set_subtraction-SetType,member-SetType,negation|Acc]) :-
    SetType \= set(set(_)).

library_setup(UseOperationParameters,MachineSets,ConsiderIfVarNames,NotConsiderConstants,default:LibExpansion,SynthesisType,Example,ExtendedComponents) :-
    count_var_types(Example,Int,Bool,(_,SetTypes),(_,SeqTypes),(Ind,IndependentTypes)) ,
    try_minimized_types_first(LibExpansion,Int,Bool,SetTypes,SeqTypes,NewInt,NewBool,NewSetTypes,NewSeqTypes) ,
    findall(set(IT),member(IT,IndependentTypes),IndependentSetTypes) ,
    length(SetTypes,Set) ,
    length(SeqTypes,Seq) ,
    append([NewSetTypes,IndependentSetTypes],NewSetTypes2),
    library_add_components(SynthesisType,NotConsiderConstants,LibExpansion,intOp,NewInt,[],TLib1) ,
    library_add_components(SynthesisType,NotConsiderConstants,LibExpansion,boolOp,NewBool,TLib1,TLib2) ,
    library_add_components(SynthesisType,NotConsiderConstants,LibExpansion,setOp-NewSetTypes2,Set,TLib2,TLib3) ,
    library_add_components(SynthesisType,NotConsiderConstants,LibExpansion,seqOp-NewSeqTypes,Seq,TLib3,TLib4) ,
    library_add_components(SynthesisType,NotConsiderConstants,LibExpansion,independent-IndependentTypes,Ind,TLib4,TOperators) ,
    library_add_conn(SynthesisType,LibExpansion,Example,Or,And) ,
    append([Or,And,TOperators],Operators) ,
    library_add_components(SynthesisType,NotConsiderConstants,LibExpansion,arithmetic,Int,[],Arithmetic) ,
    append(Operators,Arithmetic,TempComponents) ,
    randomize_library_configuration(TempComponents,RandomComponents) ,
    (UseOperationParameters = yes
    -> add_set_constants_as_op_params_for_independent_types(MachineSets,SetConstants) ,
    append(RandomComponents,SetConstants,Components)
    ; RandomComponents = Components) ,
    extend_components_to_consider_if_statements(ConsiderIfVarNames,NotConsiderConstants,LibExpansion,Components,ExtendedComponents).

library_setup(UseOperationParameters,MachineSets,ConsiderIfVarNames,NotConsiderConstants,UserLibrary,SynthesisType,Example,ExtendedComponents) :-
    UserLibrary \= default:_ ,
    setup_user_library(UserLibrary,NotConsiderConstants,SynthesisType,Example,TempComponents) ,
    (UseOperationParameters == yes
    -> add_set_constants_as_op_params_for_independent_types(MachineSets,SetConstants) ,
    append(TempComponents,SetConstants,Components)
    ; TempComponents = Components) ,
    extend_components_to_consider_if_statements(ConsiderIfVarNames,NotConsiderConstants,SynthesisType,Components,ExtendedComponents).

randomize_library_configuration(Components,Components) :-
    length(Components,L) ,
    L =< 20.

randomize_library_configuration(Components,RandomComponents) :-
    random_subseq(Components,Sub1,Sub2) ,
    get_larger_sublist(Sub1,Sub2,RandomComponents).

setup_typed_expressions(Components,Types,Acc,FinalComponents) :-
    remove_dups(Types,NTypes) ,
    setup_typed_expressions_aux(Components,NTypes,Acc,FinalComponents).

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

setup_typed_expressions_aux([Component|T],Types,Acc,FinalComponents) :-
    findall(TypedComponent,(member(Type,Types) , TypedComponent = Component-Type),TypedComponents) ,
    append(TypedComponents,Acc,NAcc) ,
    setup_typed_expressions_aux(T,Types,NAcc,FinalComponents).

setup_typed_predicates([],_,_,_,_,_,[]).

setup_typed_predicates(Predicates,Int,Bool,(Sets,SetTypes),(Seqs,SeqTypes),(IndT,IndependentTypes),TypedPredicates) :-
    setup_typed_predicates_aux(Predicates,Int,integer,IntPredicates) ,
    setup_typed_predicates_aux(Predicates,Bool,boolean,BoolPredicates) ,
    setup_typed_predicates_aux(Predicates,Sets,SetTypes,SetPredicates) ,
    setup_typed_predicates_aux(Predicates,Seqs,SeqTypes,SeqPredicates) ,
    setup_typed_predicates_aux(Predicates,IndT,IndependentTypes,IndPredicates) ,
    append([IntPredicates,BoolPredicates,SetPredicates,SeqPredicates,IndPredicates],TypedPredicates).

setup_typed_predicates_aux(_,0,_,[]).

setup_typed_predicates_aux(Predicates,Amount,Type,TypedPredicates) :-
    % single type
    Amount \= 0 , \+ is_list(Type) ,
    findall(Equal,(member(Op,[equal,not_equal]) , member(Op,Predicates) , Equal = Op-Type),TypedPredicates).

setup_typed_predicates_aux(_,_,[],[]).

setup_typed_predicates_aux(Predicates,Amount,Types,TypedPredicates) :-
    % list of types, e.g., different types of sets
    Amount \= 0 , is_list(Types) , Types \= [] ,
    findall(Equal,(member(Op,[equal,not_equal]) , member(Op,Predicates) , member(Type,Types) , Equal = Op-Type),TypedPredicates).

setup_user_library(UserLibrary,NotConsiderConstants,SynthesisType,Example,Components) :-
    % TODO: consider independent types
    count_var_types(Example,Int,Bool,(Set,SetTypes),(Seq,SeqTypes),(IndT,IndependentTypes)) ,
    setup_user_library_aux(UserLibrary,Int,Bool,(Set,SetTypes),(Seq,SeqTypes),(IndT,IndependentTypes),SelectedComponents) ,
    (NotConsiderConstants == no
    -> add_constants(UserLibrary,Int,Bool,SetTypes,SeqTypes,IndependentTypes,ConstantComponents)
    ; ConstantComponents = []) ,
    append(SelectedComponents,ConstantComponents,TComponents) ,
    add_skip_components(SynthesisType,TComponents,Int,Bool,SetTypes,SeqTypes,IndependentTypes,Components).

setup_user_library_aux(UserLibrary,Int,Bool,(SetAmount,SetTypes),(SeqAmount,SeqTypes),(IndT,IndependentTypes),Components) :-
    member(predicates(Predicates),UserLibrary) ,
    split_typed_and_untyped_predicates(Predicates,PredicatesToBeTyped,UntypedPredicates) ,
    setup_typed_predicates(PredicatesToBeTyped,Int,Bool,(SetAmount,SetTypes),(SeqAmount,SeqTypes),(IndT,IndependentTypes),TypedPredicates) ,
    member(numbers(Numbers),UserLibrary) ,
    member(relations(Relations),UserLibrary) ,
    member(sequences(Sequences),UserLibrary) ,
    append(Sequences,Relations,SequencesAndRelations) , % components in Relations refer to sequences
    setup_typed_expressions(SequencesAndRelations,SeqTypes,[],TypedSequences) ,
    member(sets(Sets),UserLibrary) ,
    findall(set(IT),member(IT,IndependentTypes),IndependentTypes2) ,
    append([SetTypes,IndependentTypes2],SetTypes2) ,
    setup_typed_expressions(Sets,SetTypes2,[],TypedSets) ,
    member(substitutions(Substitutions),UserLibrary) ,
    append([UntypedPredicates,TypedPredicates,Numbers,TypedSequences,TypedSets,Substitutions],Components).

split_typed_and_untyped_predicates(Predicates,TypedPredicates,UntypedPredicates) :-
    findall(UntypedPredicate,(member(UntypedPredicate,Predicates) , UntypedPredicate \= equal , UntypedPredicate \= not_equal),UntypedPredicates) ,
    subtract(Predicates,UntypedPredicates,TypedPredicates).

try_minimized_types_first(LibExpansion,Int,Bool,SetTypes,SeqTypes,NewInt,NewBool,NewSetTypes,NewSeqTypes) :-
    LibExpansion mod 2 =\= 0 , ! , % odd lib expansion
    try_minimized_types_first_aux(Int,NewInt) ,
    try_minimized_types_first_aux(Bool,NewBool) ,
    try_minimized_types_first_aux(SetTypes,NewSetTypes) ,
    try_minimized_types_first_aux(SeqTypes,NewSeqTypes).

try_minimized_types_first(_,Int,Bool,SetTypes,SeqTypes,Int,Bool,SetTypes,SeqTypes).

try_minimized_types_first_aux(IntOrBoolTypes,1) :-
    integer(IntOrBoolTypes) ,
    IntOrBoolTypes > 0.

try_minimized_types_first_aux(0,0).

try_minimized_types_first_aux(SetOrSeqTypes,NewTypes) :-
    is_list(SetOrSeqTypes) ,
    remove_dups(SetOrSeqTypes,NewTypes).