constraints

accumulate_location_var(b(identifier(LocationVarName),integer,Info),InAcc,OutAcc,[b(identifier(LocationVarName),integer,Info)|InAcc],OutAcc) :-
    atom_concat(li,_,LocationVarName).

accumulate_location_var(b(identifier(LocationVarName),integer,Info),InAcc,OutAcc,InAcc,[b(identifier(LocationVarName),integer,Info)|OutAcc]) :-
    atom_concat(lo,_,LocationVarName).

accumulate_location_var(_,InAcc,OutAcc,InAcc,OutAcc).

accumulate_used_location_var(Info,LocationVars,LocationAcc,OpAcc,NewLocationAcc,[Op|OpAcc]) :-
    member(synthesis(Op,output),Info) ,
    \+member(Op,OpAcc) ,
    member(b(identifier(_),integer,IdInfo),LocationVars) ,
    member(synthesis(Op,output),IdInfo) ,
    accumulate_used_location_var_aux(Op,LocationVars,LocationAcc,NewLocationAcc).

accumulate_used_location_var(_,_,LocationAcc,OpAcc,LocationAcc,OpAcc).

accumulate_used_location_var_aux(Operator,LocationVars,Acc,NewAcc) :-
    findall(LocationVar,(member(LocationVar,LocationVars) , LocationVar = b(_,_,Info) ,
    member(synthesis(Operator,LocationType),Info) ,
    (LocationType = left_input ; LocationType = right_input)),InputLocationVars) ,
    append(Acc,InputLocationVars,NewAcc).

atom_number_concat(Atom,Number,Concatenation) :-
    number_codes(Number,NumberCodes) ,
    atom_codes(Atom,AtomCodes) ,
    append(AtomCodes,NumberCodes,ConcatCodes) ,
    atom_codes(Concatenation,ConcatCodes).

create_fixed_constant_for_set_and_machine_var_type(InnerType,(MachineVarName,InnerType),MachineVar) :-
    b_get_machine_variables(MachineVars) ,
    member(MachineVar,MachineVars) ,
    get_texpr_id(MachineVar,IdName) , IdName = MachineVarName.

create_fixed_constant_for_set_and_machine_var_type(set(InnerType),NonSetTypeTuple,b(set_extension([PartialFixedConstant]),set(InnerType),[])) :-
    create_fixed_constant_for_set_and_machine_var_type(InnerType,NonSetTypeTuple,PartialFixedConstant).

create_fixed_constants_to_insert_to_sets(InputValues,FixedSetConstantsConstraint) :-
    findall((MachineVarName,Type),(member(InputValue,InputValues) , get_texpr_info(InputValue,Info) ,
    member(synthesis(type,Type),Info) , member(synthesis(machinevar,MachineVarName),Info)),MachineVarNameTypeTuples) ,
    create_fixed_constants_to_insert_to_sets_aux(MachineVarNameTypeTuples,FixedSetConstantsConstraint).

create_fixed_constants_to_insert_to_sets_aux(MachineVarNameTypeTuples,b(truth,pred,[])) :-
    retractall(additional_set_constants(_)) ,
    assertz(additional_set_constants([])) ,
    \+member((_,set(_)),MachineVarNameTypeTuples) , !.

create_fixed_constants_to_insert_to_sets_aux(MachineVarNameTypeTuples,FixedSetConstantsConstraint) :-
    get_set_types(MachineVarNameTypeTuples,TempSetTypes) ,
    findall(NonSetTypeTuple,(member(NonSetTypeTuple,MachineVarNameTypeTuples) , NonSetTypeTuple = (_,Type) , \+member(Type,TempSetTypes)),NonSetTypeTupleTuples) ,
    remove_dups(TempSetTypes,SetTypes) , % we only need one constant for an arbitrary amount of sets of this specific type, like one constant c = {i} for several sets of type integer
    maplist(create_fixed_constants_to_insert_to_sets_aux2(SetTypes,[]),NonSetTypeTupleTuples,TempFixedSetConstantsConstraintList) ,
    findall(FixedConstraint,(member(FixedConstraint,TempFixedSetConstantsConstraintList) , FixedConstraint \= []),FixedSetConstantsConstraintList) ,
    retractall(additional_set_constants(_)) ,
    assertz(additional_set_constants(FixedSetConstantsConstraintList)) ,
    conjunct_predicates(FixedSetConstantsConstraintList,FixedSetConstantsConstraint).

create_fixed_constants_to_insert_to_sets_aux2([],[],_,[]). % do not use conjunct_predicates if Acc is an empty list since this create b(truth,pred,[])

create_fixed_constants_to_insert_to_sets_aux2([],Acc,_,FixedSetConstantsConstraint) :-
    conjunct_predicates(Acc,FixedSetConstantsConstraint).

create_fixed_constants_to_insert_to_sets_aux2([SetType|T],Acc,NonSetTypeTuple,FixedSetConstantsConstraint) :-
    create_fixed_constant_for_set_and_machine_var_type(SetType,NonSetTypeTuple,FixedConstantValue) , ! ,
    unique_typed_id("o",SetType,TempOut) ,
    get_texpr_id(TempOut,OutId) ,
    add_texpr_infos(TempOut,[synthesis(OutId,output),synthesis(type,SetType),synthesis(machineconstant,FixedConstantValue)],Out) ,
    create_texpr(equal(Out,FixedConstantValue),pred,[],FixedConstant) ,
    create_fixed_constants_to_insert_to_sets_aux2(T,[FixedConstant|Acc],NonSetTypeTuple,FixedSetConstantsConstraint).

create_fixed_constants_to_insert_to_sets_aux2([_|T],Acc,NonSetTypeTuple,FixedSetConstantsConstraint) :-
    % skip: the set type does not match the machine var type, that is, NonSetTypeTuple
    create_fixed_constants_to_insert_to_sets_aux2(T,Acc,NonSetTypeTuple,FixedSetConstantsConstraint).

create_typing_predicate_from_info(Node,b(member(Node,TypeAst),pred,[])) :-
    get_texpr_info(Node,Info) ,
    member(synthesis(type,Type),Info) ,
    Type \= pred , ! ,
    get_type_ast(Type,TypeAst).

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

create_typing_predicates_from_info([],b(truth,pred,[])).

create_typing_predicates_from_info([Node|T],TypingPredicatesConj) :-
    create_typing_predicate_from_info(Node,TypingPredicate) ,
    create_typing_predicates_from_info(T,TypingPredicate,TypingPredicatesConj).

create_typing_predicates_from_info([],Acc,Acc).

create_typing_predicates_from_info([Node|T],Acc,TypingPredicatesConj) :-
    create_typing_predicate_from_info(Node,TypingPredicate) ,
    create_texpr(conjunct(Acc,TypingPredicate),pred,[],NewAcc) ,
    create_typing_predicates_from_info(T,NewAcc,TypingPredicatesConj).

enumerate_inputs_and_outputs(ExampleCount,InputValues,StateType,InputNodes) :-
    enumerate_inputs_and_outputs(ExampleCount,InputValues,StateType,0,InputNodes).

enumerate_inputs_and_outputs(_,[],_,_,[]).

enumerate_inputs_and_outputs(ExampleCount,[b(Node,Type,Info)|R],input,C,[b(Node,Type,[synthesis(input(C)),synthesis(example(ExampleCount)),synthesis(type,Type)|Info])|T]) :-
    C1 is C + 1 ,
    enumerate_inputs_and_outputs(ExampleCount,R,input,C1,T).

enumerate_inputs_and_outputs(ExampleCount,[b(Node,Type,Info)|R],output,C,[b(Node,Type,[synthesis(output(C)),synthesis(example(ExampleCount)),synthesis(type,Type)|Info])|T]) :-
    C1 is C + 1 ,
    enumerate_inputs_and_outputs(ExampleCount,R,output,C1,T).

enumerated_sets_constraint(EnumeratedSetsConstraint) :-
    findall(SetName,b_get_machine_set(SetName),EnumeratedSets) ,
    full_b_machine(BMachine) ,
    get_section(enumerated_elements,BMachine,Elems),
    enumerated_sets_constraint_aux(Elems,EnumeratedSets,TEnumeratedSetsConstraint) ,
    conjunct_predicates(TEnumeratedSetsConstraint,EnumeratedSetsConstraint).

enumerated_sets_constraint_aux(_,[],[]).

enumerated_sets_constraint_aux(Elems,[SetName|T],[b(conjunct(Equality,DistinctConstraint),pred,[])|NT]) :-
    findall(b(identifier(N),global(SetName),[]),member(b(identifier(N),global(SetName),_),Elems),EElems) ,
    EElems \== [] , ! ,
    Equality = b(equal(b(identifier(SetName),set(global(SetName)),[]),b(set_extension(EElems),set(global(SetName)),[])),pred,[]) ,
    get_consistency_constraint(EElems,DistinctConstraint) ,
    enumerated_sets_constraint_aux(Elems,T,NT).

enumerated_sets_constraint_aux(Elems,[_|T],NT) :-
    enumerated_sets_constraint_aux(Elems,T,NT).

exclude_output_to_input_mapping_for_constant_aux(LocationVars,_,ConstantLocation,MappedInputLocationName,Exclusion) :-
    member(MappedInputLocationVar,LocationVars) , MappedInputLocationVar = b(identifier(MappedInputLocationName),_,_) ,
    create_texpr(not_equal(ConstantLocation,MappedInputLocationVar),pred,[],Exclusion).

exclude_output_to_input_mapping_for_operator(LocationVars,SolutionBindings,OperatorName,Exclusion) :-
    atom_concat(constant,_,OperatorName) , ! ,
    get_location_var_node_by_info_term(LocationVars,synthesis(OperatorName,output),ConstantLocation) ,
    ConstantLocation = b(identifier(ConstantLocationName),integer,_) ,
    get_binding_for_name_or_value(SolutionBindings,ConstantLocationName,LocationValue) ,
    get_binding_for_name_or_value(SolutionBindings,MappedInputLocationName,LocationValue) ,
    MappedInputLocationName \= ConstantLocationName ,
    % exclude connection for all constants to prevent swapping with other constants of the same type
    findall(E,(member(ConstantNode,LocationVars) , is_constant(ConstantNode) , ConstantNode = b(identifier(CName),_,_) ,
    get_binding_for_name_or_value(SolutionBindings,CName,LValue) ,
    ConstantLocationName \= CName ,
    exclude_output_to_input_mapping_for_constant_aux(LocationVars,LValue,ConstantLocation,CName,E)),TExclusions) ,
    flatten(TExclusions,Exclusions) ,
    exclude_output_to_input_mapping_for_constant_aux(LocationVars,LocationValue,ConstantLocation,MappedInputLocationName,TExclusion) ,
    conjunct_predicates([TExclusion|Exclusions],Exclusion).

exclude_output_to_input_mapping_for_operator(LocationVars,SolutionBindings,OperatorName,Exclusion) :-
    get_location_var_node_by_info_term(LocationVars,synthesis(OperatorName,output),ConstantLocation) ,
    ConstantLocation = b(identifier(ConstantLocationName),integer,_) ,
    get_binding_for_name_or_value(SolutionBindings,ConstantLocationName,LocationValue) ,
    get_binding_for_name_or_value(SolutionBindings,MappedInputLocationName,LocationValue) ,
    MappedInputLocationName \= ConstantLocationName ,
    exclude_output_to_input_mapping_for_constant_aux(LocationVars,LocationValue,ConstantLocation,MappedInputLocationName,Exclusion).

exclude_output_to_input_mapping_for_operator(LocationVars,SolutionBindings,OperatorName,Exclusion) :-
    get_input_location_nodes_for_operator_name(OperatorName,LocationVars,[],InputLocations) , InputLocations \= [] ,
    maplist(exclude_specific_input_output_mapping(LocationVars,SolutionBindings),InputLocations,InputOutputExclusions) ,
    disjunct_predicates(InputOutputExclusions,Exclusion).

exclude_solution_for_further_search(UsedOperatorNames,LocationVars,SolutionBindings,Exclusion) :-
    maplist(exclude_output_to_input_mapping_for_operator(LocationVars,SolutionBindings),UsedOperatorNames,TExclusionList) ,
    remove_dups(TExclusionList,ExclusionList) ,
    disjunct_predicates(ExclusionList,TempExclusion) ,
    exclude_solution_for_further_search_aux(TempExclusion,Exclusion).

exclude_solution_for_further_search_aux(b(falsity,_,_),b(truth,pred,[])) :- !.

exclude_solution_for_further_search_aux(Exclusion,Exclusion).

exclude_specific_input_output_mapping(LocationVars,SolutionBindings,b(identifier(Id),integer,Info),Exclusion) :-
    get_binding_for_name_or_value(SolutionBindings,Id,LocationValue) ,
    get_output_location_for_location_value(LocationVars,SolutionBindings,LocationValue,OutputLocationVar) ,
    create_texpr(not_equal(b(identifier(Id),integer,Info),OutputLocationVar),pred,[],Exclusion).

exclude_specific_input_output_mapping(_,_,_,b(falsity,pred,[])).

exclude_swapping_for_component(SolutionBindings,LocationVars,(OutLVar,InLVars),ExclusionConstraint) :-
    maplist(get_lvar_name_and_input_type,InLVars,InLVarNames,InLVarTypes) ,
    % get the location values the inputs of OutLVar are mapped to
    maplist(get_binding_for_name_or_value(SolutionBindings),InLVarNames,InLVarValues) ,
    % create tuples of (lvar,lvalue)
    zip(InLVarNames,InLVarValues,VarValueTuples) ,
    zip(InLVarNames,InLVarTypes,VarTypeTuples) ,
    % then, get the output locations those inputs are mapped to
    maplist(get_corresponding_mapped_location(SolutionBindings,LocationVars),VarValueTuples,CorrespondingLocations) ,
    % and create tuples of output locations and the type of the input they are mapped to, i.e.,
    % either left_input or right_input
    findall((OutLVarName,InputType),(member((InLVar,OutLVarName),CorrespondingLocations) ,
    member((InLVar,InputType),VarTypeTuples)),OutLVarInTypeTuples) ,
    exclude_swapping_for_component_aux(LocationVars,(OutLVar,OutLVarInTypeTuples),ExclusionConstraint).

exclude_swapping_for_component_aux(LocationVars,(OutLVarName,OutLVarInTypeTuples),ExclusionConstraint) :-
    get_equivalent_input_location_nodes(OutLVarName,LocationVars,EquivalentInputLocations) ,
    % find pairs of output and input location that correspond (are mapped) to the same input type, i.e.
    % either left_input, right_input or input
    findall(Exclusion,(member((CorOutLVarName,InputType),OutLVarInTypeTuples) ,
    get_location_var_node_by_name(CorOutLVarName,LocationVars,OutLVarNode) ,
    member((InLVarNode,InputType),EquivalentInputLocations) ,
    create_texpr(not_equal(OutLVarNode,InLVarNode),pred,[],Exclusion)),Exclusions) ,
    conjunct_predicates(Exclusions,ExclusionConstraint).

get_acyclic_constraint(LocationVarsIn,LocationVarsOut,Constraint) :-
    get_acyclic_constraint_list(LocationVarsIn,LocationVarsOut,ConstraintList) ,
    conjunct_predicates(ConstraintList,Constraint).

get_acyclic_constraint_list(_,[],[]).

get_acyclic_constraint_list(LocationVarsIn,[Out|ROut],[Constraint|ConstraintList]) :-
    get_texpr_info(Out,Info) , member(synthesis(ComponentID,output),Info) ,
    get_location_var_node_by_info_term(LocationVarsIn,synthesis(ComponentID,left_input),In1) ,
    get_location_var_node_by_info_term(LocationVarsIn,synthesis(ComponentID,right_input),In2) ,
    create_texpr(less(In1,Out),pred,[],Node1) ,
    create_texpr(less(In2,Out),pred,[],Node2) ,
    conjunct_predicates([Node1,Node2],Constraint) ,
    get_acyclic_constraint_list(LocationVarsIn,ROut,ConstraintList).

get_acyclic_constraint_list(LocationVarsIn,[Out|ROut],[Constraint|ConstraintList]) :-
    get_texpr_info(Out,Info) , member(synthesis(ComponentID,output),Info) ,
    get_location_var_node_by_info_term(LocationVarsIn,synthesis(ComponentID,input),In) ,
    create_texpr(less(In,Out),pred,[],Constraint) ,
    get_acyclic_constraint_list(LocationVarsIn,ROut,ConstraintList).

get_acyclic_constraint_list(LocationVarsIn,[_|ROut],ConstraintList) :-
    get_acyclic_constraint_list(LocationVarsIn,ROut,ConstraintList).

get_behavioral_constraint(Library,(ValidGuards,Operation),InputExamples,OutputExamples,BehavioralConstraint,LocationVars) :-
    % lists of currently used components, necessary if a library is used several times
    retractall(used_library(_)) ,
    asserta(used_library([])) ,
    InputExamples = [InputValues|_] ,
    % create library constraint separated from the funtional constraint
    % to make sure to just obtain one set of location variables
    get_library_constraint(InputValues,Library,(ValidGuards,Operation),LibConstraint,InputVars,OutputVars,EnumeratedConstants) ,
    % set the temporary location variables with prefix "l"
    maplist(get_location_var_from_ast_node,InputVars,LocationVarsIn) ,
    maplist(get_location_var_from_ast_node,OutputVars,LocationVarsOut) ,
    % tuples of raw component name and internal component name like (add,add1)
    used_library(Components) ,
    get_preliminary_symmetry_reduction_constraint(Components,LocationVarsIn,LocationVarsOut,SymmetryReductionPred) ,
    conjunct_predicates([LibConstraint,SymmetryReductionPred],ExtendedLibConstraint) ,
   
    % get some information needed for well-definedness constraint
    get_line_amount(Operation,Library,InputValues,M) ,
    length(InputValues,VarAmount) ,
    % create well-definedness constraint separated from function constraints
    get_well_definedness_constraint(VarAmount,LocationVarsIn,LocationVarsOut,M,WellDefinednessConstraint) ,
    get_max_cardinality_from_examples(InputExamples,MaxCard) ,
    get_range_of_integer_nodes_from_examples(MaxCard,InputExamples,InMin,InMax) ,
    % create upper and lower bound for input values (kodkod warning) and constants
    create_texpr(integer(InMin),integer,[],IntLowerBound) ,
    create_texpr(integer(InMax),integer,[],IntUpperBound) ,
    create_texpr(integer(MaxCard),integer,[],CardUpperBound) , ! ,
    map_get_function_constraint(Operation,0,Library,ExtendedLibConstraint,InputVars,OutputVars,InputExamples,OutputExamples,FunctionConstraints,ProgramInLocationVars) ,
    enumerated_sets_constraint(EnumeratedSetsConstraint) ,
    append(OutputVars,EnumeratedConstants,ConstantsAndOutputs) ,
    % restrict domains outside of the existential quantifiers
    restrict_constant_domains(IntLowerBound,IntUpperBound,CardUpperBound,ConstantsAndOutputs,ConstantRestrictionList) ,
    % and create typing predicates for constants and input output values of components
    create_typing_predicates_from_info(ConstantsAndOutputs,TypingPredicatesConj) ,
    conjunct_predicates(ConstantRestrictionList,ConstantRestrictions) ,
    findall(InputRestriction,(member(In,InputVars) , get_bounds_for_node(In,IntLowerBound,IntUpperBound,CardUpperBound,InputRestriction)),TempInputRestrictions) ,
    conjunct_predicates(TempInputRestrictions,InputRestrictions) ,
    conjunct_predicates([EnumeratedSetsConstraint,WellDefinednessConstraint,TypingPredicatesConj,ConstantRestrictions,InputRestrictions|FunctionConstraints],BehavioralConstraint) ,
    append([LocationVarsIn,LocationVarsOut,ProgramInLocationVars],LocationVars).

get_behavioral_constraint_aux((ValidGuards,Operation),action,Library,PosInput,PosOutput,BehavioralConstraint,LocationVars) :-
    get_behavioral_constraint(Library,(ValidGuards,Operation),PosInput,PosOutput,BehavioralConstraint,LocationVars).

get_behavioral_constraint_aux((ValidInvariantsOrGuards,Operation),_,Library,PosInput,PosOutput,BehavioralConstraint,LocationVars) :-
    get_behavioral_constraint_from_input(Library,(ValidInvariantsOrGuards,Operation),PosInput,PosOutput,BehavioralConstraint,LocationVars).

get_behavioral_constraint_from_input(Library,(ValidGuards,Operation),PosInput,NegInput,BehavioralConstraint,LocationVars) :-
    % get output values
    length(PosInput,PosLength) , length(NegInput,NegLength) ,
    % create empty lists
    length(TempPosOutput,PosLength) , length(TempNegOutput,NegLength) ,
    % for our task to repair invariant violations output is either "true" or "false" (interpreted as pred_true/pred_false (synthesis(type,pred))
    % but implemented as boolean_true/boolean_false, we set options each node's info representing the type which can differ from the ast node's type)
    findall(In,(member(In,TempPosOutput) , In = [b(boolean_true,boolean,[synthesis(type,pred)])]),PosOutput) ,
    findall(In,(member(In,TempNegOutput) , In = [b(boolean_false,boolean,[synthesis(type,pred)])]),NegOutput) ,
    append(PosInput,NegInput,Input) ,
    append(PosOutput,NegOutput,Output) ,
    get_behavioral_constraint(Library,(ValidGuards,Operation),Input,Output,BehavioralConstraint,LocationVars).

get_bounds_for_node(Node,LowerIntBound,UpperIntBound,_,Restriction) :-
    Node = b(_,integer,_) ,
    Restriction = b(member(Node,b(interval(LowerIntBound,UpperIntBound),set(integer),[])),pred,[]).

get_bounds_for_node(Node,LowerIntBound,UpperIntBound,CardUpperBound,Restriction) :-
    Node = b(_,Type,_) ,
    Type = set(integer) ,
    % we restrict the cardinality of sets of integers as well as the domain of their elements
    Restriction = b(conjunct(b(less_equal(b(card(Node),integer,[]),CardUpperBound),pred,[]),
    b(member(Node,b(pow_subset(b(interval(LowerIntBound,UpperIntBound),set(integer),[])),set(set(integer)),[])),pred,[])),pred,[]).

get_bounds_for_node(Node,_LowerIntBound,_UpperIntBound,CardUpperBound,Restriction) :-
    Node = b(_,Type,_) ,
    Type = seq(integer) ,
    % we restrict the size of seqs of integers
    % TODO: restrict domain of elements of seq(integer)
    Restriction = b(less_equal(b(card(Node),integer,[]),CardUpperBound),pred,[]).

get_bounds_for_node(Node,_,_,CardUpperBound,Restriction) :-
    Node = b(_,Type,_) ,
    % either card or size for sets or sequences
    (Type = set(InnerType) , Functor = card ; Type = seq(InnerType) , Functor = size) ,
    InnerType \= integer ,
    RestrNode =.. [Functor,Node] ,
    % we restrict cardinality/size of sets/seqs with an other type than integer
    Restriction = b(less_equal(b(RestrNode,integer,[]),CardUpperBound),pred,[]).

get_connectivity_constraint(InputExampleNodes,OutputExampleNodes,InputVars,OutputVars,ConnectivityConstraint) :-
    append([InputVars,OutputVars,InputExampleNodes,OutputExampleNodes],SetOfVars) ,
    findall((X,Y),(member(X,SetOfVars) , member(Y,SetOfVars) , X \= Y , nth0(I1,SetOfVars,X) , nth0(I2,SetOfVars,Y) , I1 < I2),ListOfVarPairs) ,
    maplist(get_single_connectivity_constraint,ListOfVarPairs,ConstraintList) ,
    conjunct_predicates(ConstraintList,ConnectivityConstraint).

get_consistency_constraint(LocationVarsOut,Constraint) :-
    % find all pairs of location variables (not redundant) and create "not_equal"-Node for each pair
    get_consistency_constraint_aux(LocationVarsOut,TConstraint) ,
    %findall(InequalityNode,
    % (member(L1,LocationVarsOut) , member(L2,LocationVarsOut) ,
    % L1 \= L2 , nth0(I1,LocationVarsOut,L1) , nth0(I2,LocationVarsOut,L2) ,
    % I1 < I2 , create_texpr(not_equal(L1,L2),pred,[],InequalityNode)),InequalityList) ,
    conjunct_predicates(TConstraint,Constraint).

get_consistency_constraint_aux([],[]).

get_consistency_constraint_aux([LocationVarOut|T],[Inequality|NT]) :-
    findall(b(not_equal(LocationVarOut,LVar),pred,[]),member(LVar,T),InequalityList) ,
    conjunct_predicates(InequalityList,Inequality) ,
    get_consistency_constraint_aux(T,NT).

get_corresponding_mapped_location(SolutionBindings,_,(LVarName,LVarValue),(LVarName,LVarName2)) :-
    get_binding_for_name_or_value(SolutionBindings,LVarName2,LVarValue) ,
    delete_numbers_from_atom(LVarName2,RawName) ,
    RawName \= constant ,
    LVarName \= LVarName2.

get_equivalent_input_location_nodes(LocationVarName,LocationVars,InputLocations) :-
    delete_numbers_from_atom(LocationVarName,RawName) ,
    get_equivalent_input_location_nodes_aux(LocationVarName,RawName,LocationVars,[],InputLocations).

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

get_equivalent_input_location_nodes_aux(LocationVarName,RawName,[LocationVar|T],Acc,InputLocations) :-
    get_texpr_info(LocationVar,Info) ,
    member(synthesis(LVarName,InputType),Info) ,
    (InputType = left_input ; InputType = right_input ; InputType = input) ,
    delete_numbers_from_atom(LVarName,RawLVarName) ,
    RawLVarName = RawName ,
    % not exactly the same location
    LVarName \= LocationVarName ,
    \+member((LocationVar,InputType),Acc) , % no duplicates
    get_equivalent_input_location_nodes_aux(LocationVarName,RawName,T,[(LocationVar,InputType)|Acc],InputLocations).

get_equivalent_input_location_nodes_aux(LocationVarName,RawName,[_|T],Acc,InputLocations) :-
    get_equivalent_input_location_nodes_aux(LocationVarName,RawName,T,Acc,InputLocations).

get_fn_types(seq(Type),integer,Type).

get_fn_types(set(couple(A,B)),A,B).

get_function_constraint(Operation,ExampleCount,Library,LibConstraint,InputVars,OutputVars,InputValues,OutputValues,FunctionConstraint,LocationVars) :-
    % add a predicate setting equalities to the machine variables for the current example, since we possibly consider additional set constants like c = {i}, where i is a machine variable
    synthesis_util:create_equality_nodes_from_example(InputValues,InputEqualityList) ,
    % in this context, we have to add the invariants setting the types of the machine variables
    conjunct_predicates(InputEqualityList,InputEquality) ,
    b_get_machine_variables(MachineVars) ,
    findall(MachineVar,(member(InputValue,InputValues) , get_texpr_info(InputValue,Info) , member(synthesis(machinevar,CurrentVarName),Info) ,
    member(MachineVar,MachineVars) , get_texpr_id(MachineVar,CurrentVarName)),CurrentVars) ,
    b_get_typing_predicate_for_vars(CurrentVars,TypingMachineVarsPredicate) ,
    get_line_amount(Operation,Library,InputValues,M) ,
    % enumerate input/output values
    enumerate_inputs_and_outputs(ExampleCount,InputValues,input,InputValueNodes) ,
    enumerate_inputs_and_outputs(ExampleCount,OutputValues,output,OutputValueNodes) ,
    get_connectivity_constraint(InputValueNodes,OutputValueNodes,InputVars,OutputVars,ConnectivityConstraint) ,
    set_input_location_vars(InputValueNodes,InputLocationConstraint) ,
    set_output_location_vars(OutputValueNodes,M,OutputLocationConstraint,OutputLocationVars) ,
    conjunct_predicates([TypingMachineVarsPredicate,InputEquality,OutputLocationConstraint,InputLocationConstraint,LibConstraint,ConnectivityConstraint],ExistsBody) ,
    % get all used identifier as ast nodes
    find_typed_identifier_uses_with_info(ExistsBody,TListOfIDNodes) ,
    remove_dup_id_nodes(TListOfIDNodes,ListOfIDNodes) ,
    get_temporary_ids(ListOfIDNodes,TempTemporaryIDs) ,
    append(TempTemporaryIDs,CurrentVars,TemporaryIDs) , % the machine variables are local to the exists quantifier which are used within the equalities to the machine variables
    findall(LocationVar,(member(LocationVar,ListOfIDNodes) , LocationVar = b(identifier(Name),integer,_) , atom_concat(l,_,Name)),TempListOfLVarNodes) ,
    append(TempListOfLVarNodes,OutputLocationVars,LocationVars) ,
    % and their corresponding identifier names
    maplist(get_texpr_id,ListOfIDNodes,UsedIDs) ,
    ( unfold_existential_quantification(true)
    -> set_unique_temporary_id_names(ExampleCount,TemporaryIDs,ExistsBody,FunctionConstraint)
    ; FunctionConstraint = b(exists(TemporaryIDs,ExistsBody),pred,[used_ids(UsedIDs)])
).

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

get_input_location_nodes_for_operator_name(OperatorName,[LocationVar|T],Acc,InputLocations) :-
    LocationVar = b(identifier(_),integer,Info) ,
    member(synthesis(OperatorName,LocationType),Info) ,
    LocationType \= output , ! ,
    get_input_location_nodes_for_operator_name(OperatorName,T,[LocationVar|Acc],InputLocations).

get_input_location_nodes_for_operator_name(OperatorName,[_|T],Acc,InputLocations) :-
    get_input_location_nodes_for_operator_name(OperatorName,T,Acc,InputLocations).

get_input_location_vars_for_outputs(UsedLVars,LocationVars,OutputInputsTuples) :-
    % create tuples of component and an empty list to use as an accumulator
    findall((Component,[]),(member(OutLVar,UsedLVars) , get_texpr_info(OutLVar,Info) ,
    member(synthesis(Component,output),Info)),Acc) ,
    get_input_location_vars_for_outputs_aux(LocationVars,Acc,OutputInputsTuples).

get_input_location_vars_for_outputs_aux([],Acc,Acc).

get_input_location_vars_for_outputs_aux([LocationVar|T],Acc,OutputInputsTuples) :-
    get_texpr_info(LocationVar,Info) ,
    (member(synthesis(Component,left_input),Info) ; member(synthesis(Component,right_input),Info) ; member(synthesis(Component,input),Info)) ,
    member((Component,Inputs),Acc) ,
    delete(Acc,(Component,Inputs),TempAcc) ,
    remove_dups([LocationVar|Inputs],InputLVars),
    NewTuple = (Component,InputLVars) ,
    \+member(NewTuple,Acc) , % no duplicates
    get_input_location_vars_for_outputs_aux(T,[NewTuple|TempAcc],OutputInputsTuples).

get_input_location_vars_for_outputs_aux([_|T],Acc,OutputInputsTuples) :-
    get_input_location_vars_for_outputs_aux(T,Acc,OutputInputsTuples).

get_input_type_from_info(Info,left_input) :-
    member(synthesis(_,left_input),Info).

get_input_type_from_info(Info,right_input) :-
    member(synthesis(_,right_input),Info).

get_input_type_from_info(Info,input) :-
    member(synthesis(_,input),Info).

get_library_constraint(InputValues,Components,(ValidGuards,Operation),Constraint,InputVars,OutputVars,EnumeratedConstants) :-
    create_fixed_constants_to_insert_to_sets(InputValues,FixedSetConstantsConstraint) ,
    maplist(get_single_component_constraint,Components,ConstraintList) ,
    get_machine_constants_constraint(MachineConstantsConstraint) ,
    get_operation_parameters_constraint(ValidGuards,Operation,OperationParametersConstraint) ,
    conjunct_predicates([OperationParametersConstraint,FixedSetConstantsConstraint,MachineConstantsConstraint|ConstraintList],TConstraint) ,
    find_typed_identifier_uses_with_info(TConstraint,ListOfIDNodes) ,
    % split used identifier by input and output
    findall(I,(member(I,ListOfIDNodes) , get_texpr_id(I,IName) , is_component_input(I) , atom_concat(i,_,IName)),InputVars) ,
    findall(O,(member(O,ListOfIDNodes) , get_texpr_id(O,OName) , is_component_output(O) , atom_concat(o,_,OName)),OutputVars) ,
    findall(C,(member(C,ListOfIDNodes) , is_enumerated_constant(C)),EnumeratedConstants) ,
    get_library_wd_constraints(ListOfIDNodes,ListOfIDNodes,[],WDConstraintList) ,
    conjunct_predicates([TConstraint|WDConstraintList],Constraint).

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

get_library_wd_constraints(ListOfIDNodes,[b(Node,Type,Info)|T],Acc,WDConstraintList) :-
    \+member(synthesis(_,output),Info) ,
    member(synthesis(OpName,_),Info) ,
    get_library_wd_constraints_aux(ListOfIDNodes,OpName,b(Node,Type,Info),AccWDConstraint) ,
    get_library_wd_constraints(ListOfIDNodes,T,[AccWDConstraint|Acc],WDConstraintList).

get_library_wd_constraints(ListOfIDNodes,[_|T],Acc,WDConstraintList) :-
    get_library_wd_constraints(ListOfIDNodes,T,Acc,WDConstraintList).

get_library_wd_constraints_aux(ListOfIDNodes,OpName,_,b(less_equal(LeftInput,RightInput),pred,[])) :-
    % left input of interval is smaller or equal than the right input
    delete_numbers_from_atom(OpName,RawOpName) ,
    RawOpName = interval ,
    get_var_node_by_info_term(ListOfIDNodes,synthesis(OpName,left_input),LeftInput) ,
    get_var_node_by_info_term(ListOfIDNodes,synthesis(OpName,right_input),RightInput).

get_library_wd_constraints_aux(ListOfIDNodes,OpName,_,b(conjunct(b(greater(LeftInput,b(integer(-1),integer,[])),pred,[]),b(greater(RightInput,b(integer(-1),integer,[])),pred,[])),pred,[])) :-
    % modulo only for positive numbers
    delete_numbers_from_atom(OpName,RawOpName) ,
    RawOpName = modulo ,
    get_var_node_by_info_term(ListOfIDNodes,synthesis(OpName,left_input),LeftInput) ,
    get_var_node_by_info_term(ListOfIDNodes,synthesis(OpName,right_input),RightInput).

get_library_wd_constraints_aux(ListOfIDNodes,OpName,_,b(not_equal(LeftInput,RightInput),pred,[])) :-
    % prohibit the same inputs for subset/subset_strict like 's <<: s'
    delete_numbers_from_atom(OpName,RawOpName) ,
    member(RawOpName,[subset]) , % subset_strict (union and intersection is too restrictive here)
    get_var_node_by_info_term(ListOfIDNodes,synthesis(OpName,left_input),LeftInput) ,
    get_var_node_by_info_term(ListOfIDNodes,synthesis(OpName,right_input),RightInput).

get_library_wd_constraints_aux(_,OpName,Node,b(not_equal(Node,b(integer(0),integer,[])),pred,[])) :-
    % to only check division by zero we would need to check that the variable is the right input, thus the denominator,
    % but we also want to prevent 0/c since this is just the constant value 0
    delete_numbers_from_atom(OpName,div).

get_library_wd_constraints_aux(ListOfIDNodes,OpName,_,b(member(RightInput,b(interval(b(integer(0),integer,[]),b(integer(10),integer,[])),set(integer),[])),pred,[])) :-
    % the exponent of power_of has to be positive and we furthermore restrict the exponent to be less or equal to 10
    delete_numbers_from_atom(OpName,RawOpName) ,
    RawOpName = power_of ,
    get_var_node_by_info_term(ListOfIDNodes,synthesis(OpName,right_input),RightInput).

get_library_wd_constraints_aux(_,OpName,Node,b(greater(b(card(Node),integer,[]),b(integer(0),integer,[])),pred,[])) :-
    delete_numbers_from_atom(OpName,RawOpName) ,
    member(RawOpName,[max,min,front,tail,first,last,perm,general_intersection]).

get_line_amount(Operation,Components,InputVars,M) :-
    additional_set_constants(AdditionalSetConstants) ,
    length(AdditionalSetConstants,AC) ,
    length(InputVars,I) ,
    length(Components,N) ,
    b_get_machine_constants(MachineConstants) ,
    % if the operation exists consider the amount of operation parameters for that we consider synthesis constants
    (ground(Operation) , b_get_machine_operation(Operation,_,OperationParameters,_)
    -> length(OperationParameters,OperationParameterAmount)
    ; OperationParameterAmount = 0) ,
    length(MachineConstants,AmountOfMachineConstants) ,
    M is I + N + AmountOfMachineConstants + AC + OperationParameterAmount.

get_location_constraint(LocationVars,A,B,RestrictionNode) :-
    maplist(get_single_location_constraint(A,B),LocationVars,RestrictionList) ,
    conjunct_predicates(RestrictionList,RestrictionNode).

get_location_var_from_ast_node(b(identifier(Name),_,Info),b(identifier(LocationName),integer,Info)) :-
    ! , atom_concat(l,Name,LocationName).

get_location_var_from_ast_node(b(_,Type,Info),b(identifier(LocationName),integer,Info)) :-
    get_location_var_from_ast_node_aux(Type,ValueCode) ,
    % set input/output enumeration as prefix to get unique name
    % output location names are like 'lovalue0boolean_true'
    member(synthesis(example(ExampleCount)),Info) ,
    number_codes(ExampleCount,ExampleCountCode) ,
    (member(synthesis(input(C)),Info)
    -> number_codes(C,NC) ,
    append([[105,110,112,117,116],NC,ExampleCountCode],CCode)
    ; member(synthesis(output(C)),Info) ,
    number_codes(C,NumberCodes) ,
    append([[111,118,97,108,117,101],NumberCodes,ExampleCountCode],CCode)) ,
    append(CCode,ValueCode,Codes) ,
    atom_codes(LocationName,[108|Codes]).

get_location_var_from_ast_node_aux(Type,ValueCode) :-
    functor(Type, Functor, _),
    atom_codes(Functor,ValueCode).

get_logical_constraint(implication,In1,In2,Out,Truth,Falsity) :-
    Truth = b(conjunct(b(disjunct(
    b(equal(In1,b(boolean_false,boolean,[])),pred,[]),
    b(equal(In2,b(boolean_true,boolean,[])),pred,[])),pred,[]),
    b(equal(Out,b(boolean_true,boolean,[])),pred,[])),pred,[]) ,
    Falsity = b(conjunct(b(conjunct(
    b(equal(In1,b(boolean_true,boolean,[])),pred,[]),
    b(equal(In2,b(boolean_false,boolean,[])),pred,[])),pred,[]),
    b(equal(Out,b(boolean_false,boolean,[])),pred,[])),pred,[]).

get_logical_constraint(equivalence,In1,In2,Out,Truth,Falsity) :-
    get_logical_constraint(implication,In1,In2,Out,TruthImpl1,FalsityImpl1) ,
    get_logical_constraint(implication,In2,In1,Out,TruthImpl2,FalsityImpl2) ,
    Truth = b(conjunct(TruthImpl1,TruthImpl2),pred,[]) ,
    Falsity = b(disjunct(FalsityImpl1,FalsityImpl2),pred,[]).

get_logical_constraint(conjunct,In1,In2,Out,Truth,Falsity) :-
    Truth = b(conjunct(b(conjunct(
    b(equal(In1,b(boolean_true,boolean,[])),pred,[]),
    b(equal(In2,b(boolean_true,boolean,[])),pred,[])),pred,[]),
    b(equal(Out,b(boolean_true,boolean,[])),pred,[])),pred,[]) ,
    Falsity = b(conjunct(b(disjunct(
    b(equal(In1,b(boolean_false,boolean,[])),pred,[]),
    b(equal(In2,b(boolean_false,boolean,[])),pred,[])),pred,[]),
    b(equal(Out,b(boolean_false,boolean,[])),pred,[])),pred,[]).

get_logical_constraint(disjunct,In1,In2,Out,Truth,Falsity) :-
    Truth = b(conjunct(b(disjunct(
    b(equal(In1,b(boolean_true,boolean,[])),pred,[]),
    b(equal(In2,b(boolean_true,boolean,[])),pred,[])),pred,[]),
    b(equal(Out,b(boolean_true,boolean,[])),pred,[])),pred,[]) ,
    Falsity = b(conjunct(b(conjunct(
    b(equal(In1,b(boolean_false,boolean,[])),pred,[]),
    b(equal(In2,b(boolean_false,boolean,[])),pred,[])),pred,[]),
    b(equal(Out,b(boolean_false,boolean,[])),pred,[])),pred,[]).

get_lvar_name_and_input_type(b(identifier(LVarName),integer,Info),LVarName,InputType) :-
    get_input_type_from_info(Info,InputType).

get_machine_constants_constraint(MachineConstantsConstraint) :-
    b_get_machine_constants(MachineConstants) ,
    get_machine_constants_constraint_aux(MachineConstants,[],ConstraintList) ,
    conjunct_predicates(ConstraintList,MachineConstantsConstraint).

get_machine_constants_constraint_aux([],Acc,[MachineProperties|Acc]) :-
    % append the machine properties defining the machine constants
    b_get_properties_from_machine(MachineProperties).

get_machine_constants_constraint_aux([MachineConstant|T],Acc,ConstraintList) :-
    get_texpr_type(MachineConstant,ConstantType) ,
    get_texpr_id(MachineConstant,ConstantName) ,
    unique_typed_id("o",ConstantType,TempOut) ,
    add_texpr_infos(TempOut,[synthesis(ConstantName,output),synthesis(type,ConstantType),synthesis(machineconstant,MachineConstant)],Out) ,
    create_texpr(equal(Out,MachineConstant),pred,[],Constraint) ,
    get_machine_constants_constraint_aux(T,[Constraint|Acc],ConstraintList).

get_max_cardinality_from_examples(InputExamples,MaxCard) :-
    flatten(InputExamples,InputSet) ,
    findall(SetOrSeqNode,(member(SetOrSeqNode,InputSet) , get_texpr_type(SetOrSeqNode,Type) , (Type = set(_) ; Type = seq(_)) ,
    get_texpr_info(SetOrSeqNode,Info) , member(synthesis(initial_example),Info)),SetOrSeqNodes) ,
    SetOrSeqNodes \= [] , ! ,
    findall(Card,(member(Node,SetOrSeqNodes) , b_compute_expression_nowf_no_bindings(b(card(Node),integer,[]),Card)),Cards) ,
    (Cards = []
    -> MaxCardExamples = 0
    ; b_compute_expression_nowf_no_bindings(b(max(b(value(Cards),set(integer),[])),integer,[]),Res) , Res = int(MaxCardExamples)) ,
    % subjectively add a limit of MaxCard + 3
    MaxCard is MaxCardExamples + 3.

get_max_cardinality_from_examples(_,0).

get_new_behavioral_constraint(ProgramAST,LocationVars,solution(SolutionBindings),BehavioralConstraint,NewBehavioralConstraint) :-
    % get the used operators output location variables to exclude from the further solution
    get_used_location_vars_and_op_names(ProgramAST,LocationVars,[],[],_,UsedOperatorNames) ,
    exclude_solution_for_further_search(UsedOperatorNames,LocationVars,SolutionBindings,Exclusion) ,
    split_input_output_location_vars(LocationVars,LocationVarsIn,LocationVarsOut) ,
    used_library(Components) ,
    %findall(Component,(member(Component,AllComponents) , Component = (_,Name) , member(Name,UsedOperatorNames)),UsedComponents) ,
    get_post_symmetry_reduction_constraint(Components,SolutionBindings,LocationVarsIn,LocationVarsOut,SymmetryReduction) ,
    conjunct_predicates([BehavioralConstraint,Exclusion,SymmetryReduction],NewBehavioralConstraint).

get_operation_parameters_constraint(ValidGuards,Operation,OperationParametersConstraint) :-
    b_get_machine_operation(Operation,_,OperationParameters,_) , ValidGuards \= [] , ! ,
    get_operation_parameters_constraint_aux(OperationParameters,[],ConstraintList) ,
    get_operation_parameters_constraint_aux2(ValidGuards,ConstraintList,OperationParametersConstraint).

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

get_operation_parameters_constraint_aux([],Acc,Acc).

get_operation_parameters_constraint_aux([OperationParameter|T],Acc,ConstraintList) :-
    get_texpr_type(OperationParameter,ParameterType) ,
    get_texpr_id(OperationParameter,ParameterName) ,
    unique_typed_id("o",ParameterType,TempOut) ,
    add_texpr_infos(TempOut,[synthesis(ParameterName,output),synthesis(type,ParameterType),synthesis(operationparameter,OperationParameter)],Out) ,
    create_texpr(equal(Out,OperationParameter),pred,[],Constraint) ,
    get_machine_constants_constraint_aux(T,[Constraint|Acc],ConstraintList).

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

get_operation_parameters_constraint_aux2(ValidGuards,ConstraintList,OperationParametersConstraint) :-
    append(ValidGuards,ConstraintList,NewConstraintList) ,
    conjunct_predicates(NewConstraintList,OperationParametersConstraint).

get_output_location_for_location_value(LocationVars,SolutionBindings,LocationValue,OutputLocationVar) :-
    get_binding_for_name_or_value(SolutionBindings,OutputLocationName,LocationValue) ,
    atom_concat(lo,_,OutputLocationName) , ! ,
    member(OutputLocationVar,LocationVars) , OutputLocationVar = b(identifier(OutputLocationName),integer,_).

get_output_location_for_location_value(_,_,int(Value),b(integer(Value),integer,[])).

get_perm_component_output_type(set(CoupleType),set(seq(CoupleType))) :-
    CoupleType = couple(integer,_).

get_perm_component_output_type(seq(InnerType),set(seq(couple(integer,InnerType)))).

get_prevent_component_swap_constraint(UsedLVars,SolutionBindings,LocationVars,Constraint) :-
    get_input_location_vars_for_outputs(UsedLVars,LocationVars,OutputInputsTuples) ,
    maplist(exclude_swapping_for_component(SolutionBindings,LocationVars),OutputInputsTuples,TExclusions) ,
    remove_dups(TExclusions,Exclusions) ,
    conjunct_predicates(Exclusions,Constraint).

get_range_of_integer_nodes_from_examples(_,InputExamples,InMin,InMax) :-
    flatten(InputExamples,InputSet) ,
    get_values_of_integer_nodes(InputSet,[],IntegerValues) ,
    IntegerValues \= [] , ! ,
    min_member(TInMin,IntegerValues) , max_member(TInMax,IntegerValues) ,
    InMin is TInMin - 10 , InMax is TInMax + 10.

get_range_of_integer_nodes_from_examples(MaxCard,_,0,NMaxCard) :- % at least MaxCard + 5, e.g. card(x) > 5 but no integer is given
    NMaxCard is MaxCard + 5.

get_set_types(MachineVarNameTypeTuples,SetTypes) :-
    get_set_types_aux(MachineVarNameTypeTuples,[],SetTypes).