synthesis_util

accumulate_input_output_if_non_empty([], Acc, Acc).

accumulate_input_output_if_non_empty(Asts, Acc, [Asts|Acc]) :-
    Asts \= [].

adapt_machine_code_for_operations(Operations, NewMachineAtom) :-
    full_b_machine(Machine),
    adapt_machine_code_for_operations_aux(Operations, Machine, TempNewMachine),
    % type invariants which may have been optimized by ProB
    b_get_invariant_from_machine(Invariant),
    apply_solution_to_machine_and_type_invariant(TempNewMachine, _, invariant, Invariant, NewMachineAst),
    translate_machine(NewMachineAst, Codes, _),
    atom_codes(NewMachineAtom, Codes).

adapt_machine_code_for_operations_aux([], MachineCode, MachineCode).

adapt_machine_code_for_operations_aux([Operation|T], MachineCode, NewMachineCode) :-
    apply_solution_to_machine(MachineCode, _, action, Operation, TempNewMachine),
    adapt_machine_code_for_operations_aux(T, TempNewMachine, NewMachineCode).

add_distinguishing_states_from_cache(action, _, PosInput, NegInput, PosInput, NegInput) :-
    !.

add_distinguishing_states_from_cache(_, (DistIn,DistOut), PosInput, NegInput, NewPosInput, NewNegInput) :-
    append(DistIn, PosInput, TempPosInput),
    append(DistOut, NegInput, TempNegInput),
    remove_dups(TempPosInput, NewPosInput),
    remove_dups(TempNegInput, NewNegInput).

add_invariant_to_machine_content([linking_invariant/OperationBodies|T], Invariant, [invariant/Invariant,linking_invariant/OperationBodies|T]).

add_invariant_to_machine_content([ContentType/Content|T], Invariant, [ContentType/Content|NewContent]) :-
    ContentType \= operation_bodies,
    add_invariant_to_machine_content(T, Invariant, NewContent).

apply_solution_to_machine(Machine, _, _, none, Machine).

apply_solution_to_machine(machine(MachineName,Content), _, action, Synthesized, NewMachine) :-
    member(operation_bodies/OperationBodies, Content),
    subtract(Content, [operation_bodies/_], TempContent),
    apply_solution_to_machine_aux(action, OperationBodies, Synthesized, NewOperationBodies),
    append(TempContent, [operation_bodies/NewOperationBodies], NewContent),
    NewMachine = machine(MachineName,NewContent).

apply_solution_to_machine(machine(MachineName,Content), Operation, guard, Synthesized, NewMachine) :-
    member(operation_bodies/OperationBodies, Content),
    subtract(Content, [operation_bodies/_], TempContent),
    apply_solution_to_machine_aux(guard, Operation, Synthesized, OperationBodies, NewOperationBodies),
    append(TempContent, [operation_bodies/NewOperationBodies], NewContent),
    NewMachine = machine(MachineName,NewContent).

apply_solution_to_machine(machine(MachineName,Content), _, invariant, Synthesized, NewMachine) :-
    subtract(Content, [invariant/_], TempContent),
    conjunction_to_list(Synthesized, SynthesizedList),
    % split synthesized code from previous invariants that have been valid beforehand
    findall(SynthesizedCode, ( member(SynthesizedCode, SynthesizedList),
    get_texpr_info(SynthesizedCode, Info),
    member(synthesized_code, Info)
    ), SynthesizedCodeList),
    conjunct_predicates(SynthesizedCodeList, TempSynthesizedCode),
    find_typed_identifier_uses(TempSynthesizedCode, UsedVars),
    % create typing invariants only for variables that are involved in the synthesized code, the other typing invariants have already been conjuncted in ValidInvariants
    % we hereby want to avoid redundancy and conflicts in typing invariants, like the valid invariant has been i : NATURAL but generate_typing_predicates creates i : INTEGER afterwards
    % whilst i has not even been affected by the invariant violation
    b_get_typing_predicate_for_vars(UsedVars, TypingPredicate),
    conjunct_predicates([TypingPredicate,Synthesized], TypedSynthesizedInvariant),
    add_invariant_to_machine_content(TempContent, TypedSynthesizedInvariant, NewContent),
    NewMachine = machine(MachineName,NewContent).

apply_solution_to_machine_and_type_invariant(Machine, Operation, Type, Synthesized, NewMachine) :-
    Type \= invariant,
    apply_solution_to_machine(Machine, Operation, Type, Synthesized, TempNewMachine),
    % the invariant has not been changed but typing predicates may be removed by the solver optimization,
    % therefore, we add typing predicates for each machine variable at the beginning of the invariant
    b_get_invariant_from_machine(Invariant),
    apply_solution_to_machine(TempNewMachine, _, invariant, Invariant, NewMachine).

apply_solution_to_machine_and_type_invariant(Machine, Operation, invariant, SynthesizedInvariant, NewMachine) :-
    apply_solution_to_machine(Machine, Operation, invariant, SynthesizedInvariant, NewMachine).

apply_solution_to_machine_aux(action, OperationBodies, Synthesized, NewOperationBodies) :-
    is_list(Synthesized),
    maplist(get_name_from_operation_ast, Synthesized, OperationNames),
    remove_operations_from_list(OperationBodies, OperationNames, [], UninvoledOperations),
    append(Synthesized, UninvoledOperations, NewOperationBodies).

apply_solution_to_machine_aux(action, OperationBodies, Synthesized, [Synthesized|UninvoledOperations]) :-
    \+ is_list(Synthesized),
    get_name_from_operation_ast(Synthesized, OperationName),
    remove_operations_from_list(OperationBodies, [OperationName], [], UninvoledOperations).

apply_solution_to_machine_aux(guard, OperationName, Synthesized, [Operation|T], [NewOperation|T]) :-
    replace_precondition_if_operation_fits(OperationName, Operation, Synthesized, NewOperation),
    !.

apply_solution_to_machine_aux(guard, OperationName, Synthesized, [Operation|T], [Operation|NT]) :-
    apply_solution_to_machine_aux(guard, OperationName, Synthesized, T, NT).

b_compute_expression_nowf_no_bindings(Expression, Result) :-
    find_identifier_uses(Expression, [], UsedIdNames),
    findall(bind(UsedIdName,_), member(UsedIdName, UsedIdNames), Bindings),
    b_compute_expression_nowf(Expression, [], Bindings, Result,'synthesis',0).

b_get_machine_enumerated_sets_with_names(SetNamesTuples) :-
    findall((SetName,SetNode), b_get_machine_set(SetName, SetNode), NameNodeTuples),
    findall((SetName,ElmNames), b_get_named_machine_set(SetName, ElmNames), NameElmsTuples),
    findall((SetNode,ElmNames), ( member((SetName,SetNode), NameNodeTuples),
    member((SetName,ElmNames), NameElmsTuples)
    ), SetNamesTuples).

b_get_machinevars_with_operation_params(MachineVarsWithParams) :-
    b_get_machine_variables(MachineVars),
    b_get_machinevars_with_operation_params_aux(MachineVars, MachineVarsWithParams).

b_get_machinevars_with_operation_params_aux(MachineVars, MachineVarsWithParams) :-
    % TODO: fix this spider warning, do not access dynamic additional_machinevars/1 in this module
    catch(b_synthesis:additional_machinevars(AdditionalMachineVars), error(existence_error(_,_),_), fail),
    !,
    append(MachineVars, AdditionalMachineVars, MachineVarsWithParams).

b_get_machinevars_with_operation_params_aux(MachineVars, MachineVars).

b_get_typed_invariant_from_machine(TypedInvariant) :-
    b_get_typing_predicate(TypingPredicate),
    b_get_invariant_from_machine(Invariant),
    conjunct_predicates([TypingPredicate,Invariant], TypedInvariant).

b_get_typing_predicate(TypingPredicate) :-
    b_get_machinevars_with_operation_params(MachineVars),
    findall(NonSeq, ( member(NonSeq, MachineVars),
    NonSeq \= b(_,seq(_),_)
    ), NonSeqMachineVars),
    b_get_typing_predicate_for_vars(NonSeqMachineVars, TypingPredicate).

b_get_typing_predicate_for_vars(CurrentVars, TypingPredicate) :-
    generate_typing_predicates(CurrentVars, TypingPredicatesList),
    conjunct_predicates(TypingPredicatesList, TypingPredicate).

b_test_boolean_expression_wf_no_bindings(BooleanExpr, Result) :-
    find_identifier_uses(BooleanExpr, [], UsedIdNames),
    findall(bind(UsedIdName,_), member(UsedIdName, UsedIdNames), Bindings),
    b_test_boolean_expression_cs(BooleanExpr, Bindings, Result,'synthesis',0).

check_invariant_on_state(Input, Output, InvariantAst) :-
    create_equality_nodes_from_examples(Input, Output, EqualityNodes),
    conjunct_predicates([InvariantAst|EqualityNodes], InvariantTransitionPred),
    b_test_boolean_expression_wf_no_bindings(InvariantTransitionPred, _).

check_negative_inputs_against_operation_precondition(_, []). % no negative input states are present

check_negative_inputs_against_operation_precondition(Operation, NegInput) :-
    NegInput \= [],
    b_get_machine_operation(Operation, _, _, OpBody),
    OpBody = b(precondition(PreCondition,_),_,_),
    check_negative_inputs_against_operation_precondition_aux(PreCondition, NegInput).

check_negative_inputs_against_operation_precondition_aux(_, []).

check_negative_inputs_against_operation_precondition_aux(PreCondition, [NegState|T]) :-
    create_equality_nodes_from_example(NegState, EqualityNodes),
    conjunct_predicates([PreCondition|EqualityNodes], EqualityPred),
    \+ b_test_boolean_expression_wf_no_bindings(EqualityPred, _),
    check_negative_inputs_against_operation_precondition_aux(PreCondition, T).

check_states_on_guard([], _).

check_states_on_guard([StateEquality|T], Guard) :-
    conjunct_predicates([Guard|StateEquality], CheckGuard),
    b_test_boolean_expression_wf_no_bindings(CheckGuard, []),
    !,
    check_states_on_guard(T, Guard).

check_states_on_guards(State, Guards, ViolatedGuards) :-
    maplist(create_equality_nodes_from_example, State, StateEqualities),
    findall(Guard, ( member(Guard, Guards),
    check_states_on_guard(StateEqualities, Guard)
    ), ValidGuards),
    subtract(Guards, ValidGuards, ViolatedGuards).

check_transition_against_machine_operations(VarNodes, Input, Output, Result) :-
    findall((Op,Res,Par,Body), b_get_machine_operation(Op, Res, Par, Body), Operations),
    check_transition_against_machine_operations(Operations, Input, Output, VarNodes, Result).

check_transition_against_machine_operations([], _, _, _, no_match).

check_transition_against_machine_operations([(_,_,_,b(skip,subst,_))|T], Input, Output, VarNodes, Result) :-
    check_transition_against_machine_operations(T, Input, Output, VarNodes, Result).

check_transition_against_machine_operations([(_,_,_,OpBody)|T], Input, Output, VarNodes, Result) :-
    find_identifier_uses(OpBody, [], BodyIDs),
    findall(Name, member(b(identifier(Name),_,_), VarNodes), VarNames),
    % find distinguishing variables
    findall(DistName, ( member(DistName, BodyIDs),
    \+ member(DistName, VarNames)
    ), DistNames),
    DistNames \= [],
    !,
    check_transition_against_machine_operations(T, Input, Output, VarNodes, Result).

check_transition_against_machine_operations([(OpName,_,_,OpBody)|T], Input, Output, VarNodes, Result) :-
    b_get_machinevars_with_operation_params(MachineVars),
    before_after_predicate_with_equalities(OpBody, MachineVars, BABody),
    find_identifier_uses(OpBody, [], BodyIDs),
    create_equality_nodes_from_examples(BodyIDs, Input, Output, VarNodes, NodeList),
    b_get_typed_invariant_from_machine(Invariant),
    conjunct_predicates([BABody,Invariant|NodeList], BABodyPred),
    check_transition_against_machine_operations_aux(BABodyPred, NodeList, [(OpName,_,_,OpBody)|T], Input, Output, VarNodes, Result).

check_transition_against_machine_operations_aux(BABodyPred, _, [(OpName,_,_,_)|_], _, _, _, (OpName,done)) :-
    solve_predicate(BABodyPred, _, solution(_)),
    !.

check_transition_against_machine_operations_aux(_, NodeList, [(OpName,_,_,OpBody)|_], _, _, _, (OpName,guard)) :-
    b_get_machinevars_with_operation_params(MachineVars),
    % remove guard and try if action itself supports the missing state
    OpBody = b(precondition(_PreCondition,Action),_,_),
    before_after_predicate_with_equalities(Action, MachineVars, BAAction),
    conjunct_predicates([BAAction|NodeList], BAActionPred),
    solve_predicate(BAActionPred, _, solution(_)),
    !.

check_transition_against_machine_operations_aux(_, _, [_|T], Input, Output, VarNodes, Result) :-
    check_transition_against_machine_operations(T, Input, Output, VarNodes, Result).

check_transitions_against_machine_operations(VarNodes, InputExamples, OutputExamples, Result) :-
    % check each example againt the existing machine operations
    maplist(check_transition_against_machine_operations(VarNodes), InputExamples, OutputExamples, SingleResults),
    check_transitions_against_machine_operations_aux(SingleResults, Result),
    !.

check_transitions_against_machine_operations_aux(SingleResults, Result) :-
    % an operation satisifies the transition but its guard needs to be relaxed
    member((OpName,guard), SingleResults),
    % and all other example transitions are also satisfied by this operation,
    maplist(operation_match(OpName), SingleResults),
    % therefore we synthesize a relaxed guard
    Result = (OpName,guard).

check_transitions_against_machine_operations_aux(SingleResults, Result) :-
    % an operation satisifies all transitions, and thus, we don't have to synthesize anything
    member((OpName,done), SingleResults),
    maplist('='((OpName,done)), SingleResults),
    Result = (OpName,done).

check_transitions_against_machine_operations_aux(_, no_match).

conjunct_previous_invariant_or_guard_if_necessary(invariant, ValidInvariants, ProgramAST, SolutionAST) :-
    !,
    % mark synthesized invariants in the info to be able to split synthesized invariants from those that have already been valid beforehand
    % we want to avoid redundancy when generating typing invariants later on
    conjunction_to_list(ProgramAST, ProgramASTList),
    findall(MarkedConjunct, ( member(Conjunct, ProgramASTList),
    add_texpr_infos(Conjunct, [synthesized_code], MarkedConjunct)
    ), MarkedConjunctList),
    conjunct_predicates(MarkedConjunctList, MarkedProgramAst),
    append(ValidInvariants, [MarkedProgramAst], InvariantsList), % ValidInvariants prior to synthesized ones since they may contain typing invariants
    conjunct_predicates(InvariantsList, SolutionAST).

conjunct_previous_invariant_or_guard_if_necessary(guard, Guards, ProgramAST, SolutionAST) :-
    Guards \= any,
    !,
    % search for valid guards that are already given by the machine ( NewPreCond => OldPreCond )
    find_typed_identifier_uses(ProgramAST, [], ProgIDs),
    findall(Pre, ( member(Pre, Guards),
    find_typed_identifier_uses(Pre, PreIDs),
    append(ProgIDs, PreIDs, TIDs),
    remove_dups(TIDs, IDs),
    b_test_boolean_expression_wf_no_bindings(b(forall(IDs,ProgramAST,Pre),pred,[used_ids([])]), [])
    ), InvalidPreConds),
    sets:subtract(Guards, InvalidPreConds, ValidPreConds),
    append(ValidPreConds, [ProgramAST], PreCondsList), % ValidPreConds prior to synthesized ones since they may contain predicates setting the type of operation parameters
    conjunct_predicates(PreCondsList, SolutionAST).

conjunct_previous_invariant_or_guard_if_necessary(action, Guard, ProgramAST, SolutionAST) :-
    \+ member(Guard, [any,none]),
    !,
    SolutionAST = b(precondition(Guard,ProgramAST),subst,[]).

conjunct_previous_invariant_or_guard_if_necessary(_, _, ProgramAST, ProgramAST).

contains_equivalent_state(State, States, EquivalentState) :-
    length(State, VarAmount),
    contains_equivalent_state(VarAmount, State, States, EquivalentState).

contains_equivalent_state(_, _, [], _) :-
    !,
    fail.

contains_equivalent_state(VarAmount, State, [ExampleState|_], EquivalentState) :-
    length(ExampleState, ExampleVarAmount),
    VarAmount = ExampleVarAmount,
    create_equality_nodes_from_example(State, StateEqualityNodes),
    create_equality_nodes_from_example(ExampleState, ExampleStateEqualityNodes),
    get_distinct_independent_types_constraint_for_enums(DistinctEnumSetsConstraint),
    ( DistinctEnumSetsConstraint == b(truth,pred,[])
    ->
    append([StateEqualityNodes,ExampleStateEqualityNodes], EqualityNodes)
    ; append([DistinctEnumSetsConstraint,StateEqualityNodes,ExampleStateEqualityNodes], EqualityNodes)
    ),
    conjunct_predicates(EqualityNodes, Equality),
    solve_predicate(Equality, _, Solution),
    Solution = solution(_),
    !,
    EquivalentState = ExampleState.

contains_equivalent_state(VarAmount, State, [_|T], EquivalentState) :-
    contains_equivalent_state(VarAmount, State, T, EquivalentState).

create_equality_nodes_from_example(ExampleState, EqualityNodes) :-
    create_equality_nodes_from_example(ExampleState, [], EqualityNodes).

create_equality_nodes_from_example([], Acc, Acc).

create_equality_nodes_from_example([ValueAst|T], Acc, EqualityNodes) :-
    get_varname_from_node_info(ValueAst, VarName),
    ValueAst = b(_,VarType,_),
    % note: following enforces variables to be real machine variables
    % (we consider operation parameters to be part of our I/O "state" in synthesis by marking them with machinevar/1 in AST info)
    %get_machinevars_by_name([VarName], [MachineVar]),
    Var = b(identifier(VarName),VarType,[]),
    Equality = b(equal(Var,ValueAst),pred,[]),
    create_equality_nodes_from_example(T, [Equality|Acc], EqualityNodes).

create_equality_nodes_from_examples(Input, Output, EqualityNodes) :-
    b_get_machinevars_with_operation_params(MachineVars),
    maplist(get_varname_from_node_info, Input, CurrentIDs),
    create_equality_nodes_from_examples(CurrentIDs, Input, Output, MachineVars, EqualityNodes).

create_equality_nodes_from_examples([], _, _, _, []).

create_equality_nodes_from_examples([VarName|T], Input, Output, VarNodes, [Node1,Node2|NodeList]) :-
    member(VarNode, VarNodes),
    VarNode = b(identifier(VarName),_,_),
    member(InputNode, Input),
    get_varname_from_node_info(InputNode, VarName),
    member(OutputNode, Output),
    get_varname_from_node_info(OutputNode, VarName),
    Node1 = b(equal(VarNode,InputNode),pred,[]),
    prime_identifier(VarNode, PrimedVarNode),
    Node2 = b(equal(PrimedVarNode,OutputNode),pred,[]),
    create_equality_nodes_from_examples(T, Input, Output, VarNodes, NodeList).

create_equality_predicate_from_example(ExampleState, EqualityPredicate) :-
    create_equality_nodes_from_example(ExampleState, EqualityNodes),
    conjunct_predicates(EqualityNodes, EqualityPredicate).

delete_numbers_from_atom(NumberAtom, Atom) :-
    atom_codes(NumberAtom, Codes),
    delete_numbers_from_codelist(Codes, NewCodes),
    atom_codes(Atom, NewCodes).

delete_numbers_from_codelist([], []).

delete_numbers_from_codelist([Code|R], [Code|NR]) :-
    ( Code > 57
    ; Code < 48
    ),
    !,
    delete_numbers_from_codelist(R, NR).

delete_numbers_from_codelist([_|R], NR) :-
    delete_numbers_from_codelist(R, NR).

equality_to_assignment(b(equal(Primed,Assignment),pred,Info), b(assign_single_id(Primed,Assignment),subst,Info)).

example_bindings_to_ast_nodes([], []).

example_bindings_to_ast_nodes([Binding|T], [Ast|NT]) :-
    ( Binding = binding(TVarName,In,_)
    ; Binding = bind(TVarName,In)
    ),
    value_to_ast(In, TAst),
    remove_prime(TVarName, VarName),
    add_texpr_infos(TAst, [synthesis(machinevar,VarName)], TTAst),
    set_type_if_necessary(TTAst, Ast),
    !,
    example_bindings_to_ast_nodes(T, NT).

examples_already_reduced(Examples) :-
    Examples = [Example|_],
    length(Example, VarAmount),
    b_get_machinevars_with_operation_params(MachineVars),
    length(MachineVars, MachineVarAmount),
    VarAmount < MachineVarAmount.

exclude_accumulated_states(_, [], Acc, Exclusion) :-
    conjunct_predicates(Acc, Exclusion).

exclude_accumulated_states(CurrentVars, [BeforeState|T], Acc, Exclusion) :-
    maplist(exclude_variable_state(CurrentVars), BeforeState, ExclusionList),
    conjunct_predicates(ExclusionList, Inequalities),
    exclude_accumulated_states(CurrentVars, T, [Inequalities|Acc], Exclusion).

exclude_transition_constraint(Input, Output, CurrentVars, b(negation(EqualityConjunction),pred,[])) :-
    b_get_machinevars_with_operation_params(MachineVars),
    maplist(get_varname_from_id_node, CurrentVars, CurrentIDs),
    create_equality_nodes_from_examples(CurrentIDs, Input, Output, MachineVars, EqualityNodes),
    conjunct_predicates(EqualityNodes, EqualityConjunction).

exclude_variable_state(MachineVars, b(Node,Type,Info), Inequality) :-
    member(synthesis(machinevar,VarName), Info),
    member(b(identifier(VarName),MachineVarType,MachineVarInfo), MachineVars),
    create_texpr(not_equal(b(Node,Type,Info),b(identifier(VarName),MachineVarType,MachineVarInfo)), pred, [], Inequality).

expand_state_cache_if_guard_and_solution(guard, solution(_), (UsedPositives,UsedNegatives), PosInput,
    NegInput, (PositiveStates,NegativeStates)) :-
    append(UsedPositives, PosInput, TPositiveStates),
    append(UsedNegatives, NegInput, TNegativeStates),
    remove_dups(TPositiveStates, PositiveStates),
    remove_dups(TNegativeStates, NegativeStates).

expand_state_cache_if_guard_and_solution(_, _, DistStateCache, _, _, DistStateCache).

expand_transition_cache_if_solution(action, DistTransitionCache, CurrentVars, solution(Solution), NewDistTransitionCache) :-
    !,
    get_input_output_nodes_from_bindings(Solution, Input, Output),
    exclude_transition_constraint(Input, Output, CurrentVars, Exclusion),
    NewDistTransitionCache = b(conjunct(DistTransitionCache,Exclusion),pred,[]).

expand_transition_cache_if_solution(action, DistTransitionCache, _, _, DistTransitionCache).

expand_transition_cache_if_solution(Type, DistTransitionCache, _, _, DistTransitionCache) :-
    Type \= action.

finalize_synthesized_action(_, none, none).

finalize_synthesized_action(OperationName, b(precondition(PreCondition,Substitutions),subst,[]),
    b(operation(OpNameId,_,Params,b(precondition(NewPreCondition,UnprimedSubstitutions),subst,[])),subst,[])) :-
    OpNameId = b(identifier(op(OperationName)),op([],[]),[]),
    find_typed_identifier_uses_with_info(Substitutions, TypedIdentifiers),
    get_operation_params_from_ids(TypedIdentifiers, Params),
    Params \= [],
    !,
    set_operation_params_domain(Params, ParamTypeDefsPred),
    conjunct_predicates([ParamTypeDefsPred,PreCondition], NewPreCondition),
    prime_or_unprime_variables_in_ast(unprime, [], Substitutions, UnprimedSubstitutions).

finalize_synthesized_action(OperationName, b(precondition(PreCondition,Substitutions),subst,[]),
    b(operation(OpNameId,_,_,b(precondition(PreCondition,UnprimedSubstitutions),subst,[])),subst,[])) :-
    OpNameId = b(identifier(op(OperationName)),op([],[]),[]),
    prime_or_unprime_variables_in_ast(unprime, [], Substitutions, UnprimedSubstitutions).

finalize_synthesized_action(OperationName, Action, b(operation(OpNameId,_,Params,b(precondition(ParamTypeDefsPred,UnprimedAction),subst,[])),subst,[])) :-
    OpNameId = b(identifier(op(OperationName)),op([],[]),[]),
    find_typed_identifier_uses_with_info(Action, TypedIdentifiers),
    get_operation_params_from_ids(TypedIdentifiers, Params),
    Params \= [],
    !,
    set_operation_params_domain(Params, ParamTypeDefsPred),
    prime_or_unprime_variables_in_ast(unprime, [], Action, UnprimedAction).

finalize_synthesized_action(OperationName, Action, b(operation(OpNameId,_,_,UnprimedAction),subst,[])) :-
    OpNameId = b(identifier(op(OperationName)),op([],[]),[]),
    prime_or_unprime_variables_in_ast(unprime, [], Action, UnprimedAction).

find_typed_identifier_uses_with_info(AST, UsedIDs) :-
    find_typed_identifier_uses_with_info_aux(AST, TempUsedIDs),
    remove_dups(TempUsedIDs, UsedIDs),
    !.

find_typed_identifier_uses_with_info_aux(List, IDs) :-
    is_list(List),
    findall(ID, ( member(ID, List),
    ID = b(identifier(_),_,_)
    ), IDs).

find_typed_identifier_uses_with_info_aux(b(identifier(IDName),Type,Info), [b(identifier(IDName),Type,Info)]).

find_typed_identifier_uses_with_info_aux(b(Node,_,_), UsedIDs) :-
    Node =.. [Name,List],
    ( Name = set_extension
    ; Name = parallel
    ),
    maplist(find_typed_identifier_uses_with_info_aux, List, UsedIDsNested),
    tools:flatten(UsedIDsNested, UsedIDs).

find_typed_identifier_uses_with_info_aux(b(assign_single_id(_ID,Ast),_,_), UsedIDs) :-
    find_typed_identifier_uses_with_info_aux(Ast, UsedIDs).

find_typed_identifier_uses_with_info_aux(b(Node,_,_), UsedIDs) :-
    Node = if_then_else(Condition,TrueOut,FalseOut),
    find_typed_identifier_uses_with_info_aux(Condition, ConditionIDs),
    find_typed_identifier_uses_with_info_aux(TrueOut, TrueOutIDs),
    find_typed_identifier_uses_with_info_aux(FalseOut, FalseOutIDs),
    append([ConditionIDs,TrueOutIDs,FalseOutIDs], UsedIDs).

find_typed_identifier_uses_with_info_aux(b(Node,_,_), UsedIDs) :-
    Node = forall(_Ids,Left,Right),
    find_typed_identifier_uses_with_info_aux(Left, LeftIDs),
    find_typed_identifier_uses_with_info_aux(Right, RightIDs),
    append([LeftIDs,RightIDs], UsedIDs).

find_typed_identifier_uses_with_info_aux(b(Node,_,_), UsedIDs) :-
    Node =.. [_,Arg],
    find_typed_identifier_uses_with_info_aux(Arg, UsedIDs).

find_typed_identifier_uses_with_info_aux(b(Node,_,_), UsedIDs) :-
    Node =.. [_,Arg1,Arg2],
    find_typed_identifier_uses_with_info_aux(Arg1, UsedIDs1),
    find_typed_identifier_uses_with_info_aux(Arg2, UsedIDs2),
    append(UsedIDs1, UsedIDs2, UsedIDs).

find_typed_identifier_uses_with_info_aux(b(Node,_,_), UsedIDs) :-
    functor(Node, Functor, Arity),
    Functor = rlevent,
    Arity = 5,
    arg(5, Node, Body),
    find_typed_identifier_uses_with_info_aux(Body, UsedIDs).

find_typed_identifier_uses_with_info_aux(_, []).

get_binding_for_name_or_value(SolutionBindings, VarName, Value) :-
    ( member(binding(VarName,Value,_), SolutionBindings)
    ;
    member(bind(VarName,Value), SolutionBindings)
).

get_constant_node_or_id(string_set, b(string_set,set(string),[])).

get_constant_node_or_id(bool_set, b(bool_set,set(boolean),[])).

get_constant_node_or_id(integer_set, b(integer_set('INTEGER'),set(integer),[])).

get_constant_node_or_id(integer_set_min_max, b(integer_set('INT'),set(integer),[])).

get_constant_node_or_id(natural1, b(integer_set('NATURAL1'),set(integer),[])).

get_constant_node_or_id(natural, b(integer_set('NATURAL'),set(integer),[])).

get_constant_node_or_id(implementable_natural1, b(integer_set('NAT1'),set(integer),[])).

get_constant_node_or_id(implementable_natural, b(integer_set('NAT'),set(integer),[])).

get_constant_node_or_id(constant-Type, Constant) :-
    unique_typed_id("constant", Type, TempConstant),
    add_texpr_infos(TempConstant, [synthesis(enumerated_constant),synthesis(type,Type)], Constant).

get_current_vars_from_example(Example, CurrentVars) :-
    b_get_machinevars_with_operation_params(MachineVars),
    findall(VarName, ( member(Node, Example),
    get_varname_from_node_info(Node, VarName)
    ), CurrentVarNames),
    findall(VarNode, ( member(VarNode, MachineVars),
    VarNode = b(identifier(VarName),_,_),
    member(VarName, CurrentVarNames)
    ), CurrentVars).

get_distinct_independent_types_constraint_for_enums(Constraint) :-
    findall(MachineSetName, b_get_machine_set(MachineSetName), MachineSetNames),
    get_distinct_independent_types_constraint_for_enums(MachineSetNames, [], ConstraintList),
    conjunct_predicates(ConstraintList, Constraint).

get_distinct_independent_types_constraint_for_enums([], Acc, Acc).

get_distinct_independent_types_constraint_for_enums([MachineSetName|T], Acc, ConstraintList) :-
    b_get_named_machine_set(MachineSetName, SetValues),
    findall(SetValueNode, ( member(SetValue, SetValues),
    SetValueNode = b(identifier(SetValue),global(MachineSetName),[])
    ), SetValueNodes),
    findall(Inequality, ( member(Node1, SetValueNodes),
    member(Node2, SetValueNodes),
    Node1 \= Node2,
    Inequality = b(not_equal(Node1,Node2),pred,[])
    ), Inequalities),
    get_distinct_independent_types_constraint_for_enums(T, [Inequalities|Acc], ConstraintList).

get_distinct_states(invariant, Positive, TempNegative, Positive, Negative) :-
    get_distinct_states(Positive, TempNegative, Negative).

get_distinct_states(guard, TempPositive, Negative, Positive, Negative) :-
    get_distinct_states(Negative, TempPositive, Positive).

get_distinct_states(Examples1, TempExamples2, Examples2) :-
    findall(E, ( member(E, TempExamples2),
    \+ contains_equivalent_state(E, Examples1, _)
    ), Examples2).

get_distinguishing_state_or_trans(DistTransitionCache, CurrentVars, Type, ValidInvariantsOrGuards, AST1,
    AST2, NewDistTransitionCache, Distinguishing) :-
    % add typing of machine variables to the invariant for consistency with AtelierB and to find a solution referring to
    % all machine variables
    b_get_typed_invariant_from_machine(TypedInvariant),
    % add WD-constraints for sequences
    find_typed_identifier_uses(AST1, AST1Nodes),
    find_typed_identifier_uses(AST2, AST2Nodes),
    findall(Seq, ( member(Seq, AST1Nodes),
    is_seq(Seq)
    ), Seq1),
    findall(Seq, ( member(Seq, AST2Nodes),
    is_seq(Seq)
    ), Seq2),
    append(Seq1, Seq2, TSequences),
    remove_dups(TSequences, Sequences),
    maplist(sequence_well_definedness_constraint, Sequences, SeqConstraintList),
    conjunct_predicates(SeqConstraintList, SeqConstraints),
    get_distinct_independent_types_constraint_for_enums(DistinctEnumSetsConstraint),
    preferences:set_preference(randomise_enumeration_order, true),
    get_distinguishing_state_or_trans_aux(DistinctEnumSetsConstraint, DistTransitionCache, Type, ValidInvariantsOrGuards,
    b(conjunct(SeqConstraints,b(conjunct(b(negation(
    b(equivalence(AST1,AST2),pred,[])),pred,[]),TypedInvariant),pred,[])),pred,[]), Distinguishing),
    expand_transition_cache_if_solution(Type, DistTransitionCache, CurrentVars, Distinguishing, NewDistTransitionCache),
    synthesis_log(distinguishing_transition_cache_changed(DistTransitionCache,NewDistTransitionCache)).

get_distinguishing_state_or_trans_aux(DistinctEnumSetsConstraint, DistTransitionCache, action, ValidInvariantsOrGuards, Constraint, Distinguishing) :-
    ValidInvariantsOrGuards \= any,
    ValidInvariantsOrGuards \= none,
    !,
    DistConstraint = b(conjunct(DistinctEnumSetsConstraint,b(conjunct(b(conjunct(Constraint,ValidInvariantsOrGuards),pred,[]),DistTransitionCache),pred,[])),pred,[]),
    synthesis_log(distinguishing_constraint(action,DistConstraint)),
    solve_distinguishing_constraint_with_fallback(DistConstraint, TDistinguishing),
    get_solution_or_none(TDistinguishing, Distinguishing).

get_distinguishing_state_or_trans_aux(DistinctEnumSetsConstraint, DistTransitionCache, action, _, Constraint, Distinguishing) :-
    !,
    DistConstraint = b(conjunct(DistinctEnumSetsConstraint,b(conjunct(Constraint,DistTransitionCache),pred,[])),pred,[]),
    synthesis_log(distinguishing_constraint(action,Constraint)),
    solve_distinguishing_constraint_with_fallback(DistConstraint, TDistinguishing),
    get_solution_or_none(TDistinguishing, Distinguishing).

get_distinguishing_state_or_trans_aux(DistinctEnumSetsConstraint, _, Type, _, Constraint, Distinguishing) :-
    synthesis_log(distinguishing_constraint(Type,Constraint)),
    solve_distinguishing_constraint_with_fallback(b(conjunct(DistinctEnumSetsConstraint,Constraint),pred,[]), TDistinguishing),
    get_solution_or_none(TDistinguishing, Distinguishing).

get_guard_list_from_operation(Operation, ListOfGuards) :-
    b_get_machine_operation(Operation, _, OperationParameters, OpBody),
    get_guard_list_from_operation_aux(Operation, OpBody, GuardList),
    recreate_guards_for_operation_parameters(OperationParameters, OperationParameterGuards),
    append(GuardList, OperationParameterGuards, ListOfGuards).

get_guard_list_from_operation(_, any).

get_guard_list_from_operation_aux(Operation, OpBody, GuardList) :-
    get_guard_list_from_operation_aux2(Operation, OpBody, Guard),
    conjunction_to_list(Guard, GuardList).

get_guard_list_from_operation_aux(_, _, []).

get_guard_list_from_operation_aux2(_, b(precondition(Guard,_),_,_), Guard).

get_guard_list_from_operation_aux2(Operation, b(rlevent(Operation,_,_,_,Guard,_,_,_,_,_,_),_,_), Guard).

get_guard_list_from_operation_aux2(_, b(any(_,Guard,_),subst,_), Guard).

get_input_nodes_from_bindings(Solution, Input) :-
    findall(Binding, ( member(Binding, Solution),
    get_varname_from_binding(Binding, VarName),
    \+ is_primed_id(VarName)
    ), Bindings),
    example_bindings_to_ast_nodes(Bindings, Input).

get_input_output_nodes_from_bindings(Solution, Input, Output) :-
    get_input_nodes_from_bindings(Solution, Input),
    get_output_nodes_from_bindings(Solution, Output).

get_invalid_state_equalities_for_operation(OperationName, MachineVars, Amount, b(precondition(Precondition,_),subst,_), InvalidEqualities) :-
    !,
    % additionally consider the machine properties since a precondition may access machine constants
    b_get_properties_from_machine(MachineProperties),
    % filter predicates that set the types of operation parameters from the actual preconditions, since we do not want to negate the typing of operation parameters in the following
    b_get_machine_operation(OperationName, _, OperationParams, _),
    split_typing_predicates_from_precondition(OperationParams, Precondition, TypingPredicates, PreconditionPredicate),
    conjunct_predicates([MachineProperties,TypingPredicates,b(negation(PreconditionPredicate),pred,[])], NegatedPrecondition),
    get_invalid_state_equalities_for_operation_aux(MachineVars, Amount, NegatedPrecondition, [], InvalidStates),
    maplist(create_equality_predicate_from_example, InvalidStates, InvalidEqualities).

get_invalid_state_equalities_for_operation(_, _, _, _, []).

get_invalid_state_equalities_for_operation_aux(_, 0, _, Acc, Acc).

get_invalid_state_equalities_for_operation_aux(MachineVars, Amount, PreconditionWithProperties, Acc, InvalidStates) :-
    exclude_accumulated_states(MachineVars, Acc, [], TExclusion),
    ( TExclusion = [] ->
    Exclusion = b(truth,pred,[])
    ; Exclusion = TExclusion
    ),
    create_texpr(conjunct(Exclusion,PreconditionWithProperties), pred, [], Predicate),
    solve_predicate(Predicate, _, Solution),
    Solution = solution(SolutionBindings),
    !,
    % solutions may also refer to machine constants that we do not want to consider here since we search for machine states
    findall(Binding, ( member(Binding, SolutionBindings),
    Binding = binding(Name,_,_),
    member(b(identifier(Name),_,_), MachineVars)
    ), MachineVarBindings),
    example_bindings_to_ast_nodes(MachineVarBindings, InvalidState),
    NAmount is Amount-1,
    get_invalid_state_equalities_for_operation_aux(MachineVars, NAmount, PreconditionWithProperties, [InvalidState|Acc], InvalidStates).

get_invalid_state_equalities_for_operation_aux(_, _, _, Acc, Acc).