b_synthesis

add_operation_parameter_values_to_examples(Input, Output, Actions, NewInput) :-
    Input = [Example|_],
    maplist(get_varname_from_node_info, Example, CurrentVarNames),
    maplist(parallel_to_conjunction, Actions, ActionPreds),
    add_operation_parameter_values_to_examples_aux(CurrentVarNames, ActionPreds, Input, Output, ParamValues),
    maplist(append, Input, ParamValues, NewInput).

add_operation_parameter_values_to_examples([], [], [], [], _, [], []).

add_operation_parameter_values_to_examples(PosInput, PosOutput, [], [], Actions, NewPosInput, []) :-
    add_operation_parameter_values_to_examples(PosInput, PosOutput, Actions, NewPosInput).

add_operation_parameter_values_to_examples([], [], NegInput, NegOutput, Actions, [], NewNegInput) :-
    add_operation_parameter_values_to_examples(NegInput, NegOutput, Actions, NewNegInput).

add_operation_parameter_values_to_examples(PosInput, PosOutput, NegInput, NegOutput, Actions, NewPosInput, NewNegInput) :-
    add_operation_parameter_values_to_examples(PosInput, PosOutput, Actions, NewPosInput),
    add_operation_parameter_values_to_examples(NegInput, NegOutput, Actions, NewNegInput).

add_operation_parameter_values_to_examples_aux(CurrentVarNames, ActionPreds, Input, Output, ParamValuesList) :-
    add_operation_parameter_values_to_examples_aux(CurrentVarNames, ActionPreds, Input, Output, [], ParamValuesList).

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

add_operation_parameter_values_to_examples_aux(CurrentVarNames, ActionPreds, [Input|IT], [Output|OT], Acc, ParamValuesList) :-
    create_before_after_equalities(Input, Output, BAEquality),
    member(ActionPred, ActionPreds),
    create_texpr(conjunct(ActionPred,BAEquality), pred, [], BeforeAfterWithEqualities),
    solve_predicate(BeforeAfterWithEqualities, _, Solution),
    Solution = solution(SolutionBindings),
    !,
    get_operation_parameter_values_from_before_after(CurrentVarNames, SolutionBindings, ParamValues),
    append(Acc, [ParamValues], NewAcc),
    add_operation_parameter_values_to_examples_aux(CurrentVarNames, ActionPreds, IT, OT, NewAcc, ParamValuesList).

add_operation_parameter_values_to_examples_aux(CurrentVarNames, ActionPreds, [Input|IT], [_|OT], Acc, ParamValuesList) :-
    % we may not find a solution for the operation parameters for negative examples
    create_equality_nodes_from_example(Input, BeforeEqualityList),
    conjunct_predicates(BeforeEqualityList, BeforeEquality),
    member(ActionPred, ActionPreds),
    create_texpr(conjunct(ActionPred,BeforeEquality), pred, [], BeforeAfterWithEqualities),
    solve_predicate(BeforeAfterWithEqualities, _, Solution),
    Solution = solution(SolutionBindings),
    !,
    get_operation_parameter_values_from_before_after(CurrentVarNames, SolutionBindings, ParamValues),
    append(Acc, [ParamValues], NewAcc),
    add_operation_parameter_values_to_examples_aux(CurrentVarNames, ActionPreds, IT, OT, NewAcc, ParamValuesList).

additional_machinevars([]).

assert_if_statement_var_names([]).

assert_if_statement_var_names(ConsiderIfVarNames) :-
    asserta(consider_if_var_names(ConsiderIfVarNames)).

assert_library_configuration_from_ui(Library) :-
    % either a list of manually selected components from the user or a term default:LibExpansion
    ( is_list(Library)
    ; Library = default:_LibExpansion
    ),
    retractall(library_from_ui(_)),
    asserta(library_from_ui(Library)).

assert_library_configuration_from_ui(_).

assert_synthesis_context(DistTransitionCache, NewDistStateCache, CurrentVars, PreCondVars, ValidInvariantsOrGuards, Type,
    Input, Output, Action) :-
    retractall(synthesis_context(_, _, _, _, _, Type, _, _, _)),
    asserta(synthesis_context(DistTransitionCache, NewDistStateCache, CurrentVars, PreCondVars, ValidInvariantsOrGuards, Type,
    Input, Output, Action)).

behavior_satisfied_or_extend_machine(Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized) :-
    PosInput = [Example|_],
    get_current_vars_from_example(Example, CurrentVars),
    check_transitions_against_machine_operations(CurrentVars, PosInput, PosOutput, Result),
    behavior_satisfied_or_extend_machine_aux(Result, Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized).

behavior_satisfied_or_extend_machine_aux((Operation,done), _, _, NegInput, _, _, operation_satisfied(Operation)) :-
    check_negative_inputs_against_operation_precondition(Operation, NegInput),
    !.

behavior_satisfied_or_extend_machine_aux((Operation,done), _, PosInput, NegInput, PosOutput, NegOutput, Synthesized) :-
    behavior_satisfied_or_extend_machine_aux2(guard, Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized).

behavior_satisfied_or_extend_machine_aux((Operation,guard), _, PosInput, NegInput, PosOutput, NegOutput, Synthesized) :-
    behavior_satisfied_or_extend_machine_aux2(guard, Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized).

behavior_satisfied_or_extend_machine_aux(no_match, Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized) :-
    behavior_satisfied_or_extend_machine_aux2(action, Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized).

behavior_satisfied_or_extend_machine_aux2(SynthesisType, Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized) :-
    start_specific_synthesis(Operation, SynthesisType, PosInput, NegInput, PosOutput, NegOutput, Synthesized),
    !,
    Synthesized \= none.

cache_operation_tuple_to_quadruple((_,b(operation(b(identifier(op(OperationName)),_,_),Res,Par,Body),_,_)), (OperationName,Res,Par,Body)).

create_before_after_equalities(In, Out, Equality) :-
    create_equality_nodes_from_example(In, EqIn),
    create_equality_nodes_from_example(Out, EqOut),
    maplist(prime_or_unprime_variables_in_ast(prime, []), EqOut, EqOutPrimed),
    append(EqIn, EqOutPrimed, Eqs),
    conjunct_predicates(Eqs, Equality),
    !.

create_machinevar(b(identifier(IdName),Type,Info)) :-
    member(synthesis(machinevar,IdName), Info),
    !,
    ( catch(additional_machinevars(AdditionalMachineVars), error(existence_error(_,_),_), fail) ->
    true
    ; AdditionalMachineVars = []
    ),
    ( \+ member(b(identifier(IdName),Type,Info), AdditionalMachineVars)
    ->
    create_machinevar_aux(b(identifier(IdName),Type,Info), AdditionalMachineVars)
    ; true
).

create_machinevar(b(_,Type,Info)) :-
    member(synthesis(machinevar,IdName), Info),
    create_machinevar(b(identifier(IdName),Type,Info)).

create_machinevar_aux(IdNode, AdditionalMachineVars) :-
    retractall(additional_machinevars(_)),
    asserta(additional_machinevars([IdNode|AdditionalMachineVars])).

distinguishing_state_or_synthesize_action(_, PreCondition, _, _, _, PreCondition) :-
    is_distinguishing(PreCondition).

distinguishing_state_or_synthesize_action(Operation, PreCondition, NewDistStateCache, (PosInput,PosOutput), (NegInput,NegOutput), Action) :-
    % assert the synthesized precondition to the currently suspended synthesis context of the action and restart it
    synthesis_context(DistTransitionCache, _, CurrentVars, PreCondVars, OldPreCond, action, Input, Output, _),
    new_or_old_precondition(OldPreCond, PreCondition, NewPreCond),
    retractall(synthesis_context(_, _, _, _, _, action, _, _, _)),
    asserta(synthesis_context(DistTransitionCache, NewDistStateCache, CurrentVars, PreCondVars, NewPreCond, action, Input, Output, _)),
    start_synthesis_from_ui_aux(Operation, action, (PosInput,PosOutput), (NegInput,NegOutput), Action).

find_further_solution(_, _, _, _, BehavioralConstraint, FurtherSolution, NewBehavioralConstraint) :-
    synthesis_mode(SynthesisMode),
    SynthesisMode == first_solution,
    !,
    FurtherSolution = none,
    NewBehavioralConstraint = BehavioralConstraint.

find_further_solution(ProgramAST, LocationVars, _, solution(SolutionBindings), BehavioralConstraint, FurtherSolution, NewBehavioralConstraint) :-
    get_new_behavioral_constraint(ProgramAST, LocationVars, solution(SolutionBindings), BehavioralConstraint, NewBehavioralConstraint),
    solve_using_selected_solver(NewBehavioralConstraint, TempSolution),
    find_further_solution_aux(TempSolution, FurtherSolution).

find_further_solution_aux(solution(S), Solution) :-
    !,
    Solution = solution(S).

find_further_solution_aux(_, none).

get_all_machine_sets(MachineSets) :-
    findall(MachineSet, b_get_machine_set(_, MachineSet), MachineSets).

get_asserted_constant_configuration(NotConsiderConstants) :-
    not_consider_constants(NotConsiderConstants),
    !.

get_asserted_constant_configuration(no).

get_asserted_if_statement_vars(ConsiderIfVarNames) :-
    consider_if_var_names(ConsiderIfVarNames),
    !.

get_asserted_if_statement_vars([]).

get_distinguishing_state_cache_from_operation_tuples(Operations, OperationName, (CachePos,CacheNeg), Operation) :-
    member(((CachePos,CacheNeg),Operation), Operations),
    Operation = b(operation(b(identifier(op(OperationName)),_,_),_,_,_),_,_).

get_operation_parameter_values_from_before_after(CurrentVarNames, SolutionBindings, ParamValues) :-
    % only for those operation parameter that are not part of the current examples
    findall(ParamBinding, ( member(ParamBinding, SolutionBindings),
    ParamBinding = binding(TempIdName,_,_),
    remove_prime(TempIdName, IdName),
    \+ member(IdName, CurrentVarNames)
    ), ParamBindings),
    get_operation_parameter_values_from_before_after_aux(ParamBindings, [], ParamValues).

get_operation_parameter_values_from_before_after_aux([], Acc, Acc).

get_operation_parameter_values_from_before_after_aux([binding(ParamName,_,Value)|T], Acc, ParamValues) :-
    parse_and_typecheck_value(Value, TempValueAst),
    add_texpr_infos(TempValueAst, [synthesis(initial_example),synthesis(machinevar,ParamName)], ValueAst),
    create_machinevar(ValueAst),
    get_operation_parameter_values_from_before_after_aux(T, [ValueAst|Acc], ParamValues).

get_positive_and_negative_examples_for_invariant_synthesis(PosInput, PosOutput, NegInput, NegOutput, Pos, Neg) :-
    % for synthesizing invariants we also need output states
    append(PosInput, PosOutput, TempPositive),
    append(NegInput, NegOutput, TempNegative),
    get_distinct_states(invariant, TempPositive, TempNegative, Positive, Negative),
    % don't use an example more than one time, only possible for invariant synthesis
    % because we split every transition in two examples (input,output)
    remove_dups(Positive, Pos),
    remove_dups(Negative, Neg).

is_distinguishing(transition(_,_)).

is_distinguishing(state(_)).

machine_operation_uses_parameters(OperationName, yes) :-
    b_get_machine_operation(OperationName, _, Params, _),
    Params \= [],
    !.

machine_operation_uses_parameters(_, no).

max_library_expansion(30).

new_or_old_precondition(OldPreCond, none, OldPreCond).

new_or_old_precondition(_, PreCond, PreCond) :-
    PreCond \= none.

post_synthesize_action(_, _, _, _, _, _, _, Synthesized, Synthesized) :-
    is_distinguishing(Synthesized),
    synthesis_log(solution(_,Synthesized)).

post_synthesize_action(Operation, _Vars, PosInput, PosOutput, NegInput, NegOutput, _NegDistInput, Synthesized, FinalAction) :-
    \+ is_distinguishing(Synthesized),
    Synthesized \= none,
    ( add_operation_parameter_values_to_examples(PosInput, PosOutput, NegInput, NegOutput, [Synthesized], NewPosInput, NewNegInput)
    ; PosInput = NewPosInput,
    NegInput = NewNegInput
    ),
    NewPosInput = [Example|_],
    maplist(get_varname_from_node_info, Example, VarNames),
    synthesize_guard_if_necessary(VarNames, NewPosInput, NewNegInput, Synthesized, Action),
    post_synthesize_action_aux(Operation, Action, FinalAction).

post_synthesize_action_aux(_, Distinguishing, Distinguishing) :-
    % synthesizing a guard afterwards returned a distinguishing state
    % the synthesized action is asserted in synthesis_context/9 and will be reused
    is_distinguishing(Distinguishing).

post_synthesize_action_aux(Operation, Action, FinalAction) :-
    % synthesizing a guard afterwards succeeded or has already been sufficient beforehand, i.e.,
    % a guard has been synthesized simultaneously when synthesizing the action
    \+ is_distinguishing(Action),
    finalize_synthesized_action(Operation, Action, FinalAction),
    synthesis_log(solution(action,FinalAction)).

post_synthesize_predicate(guard, Synthesized, NewPreCondition) :-
    find_typed_identifier_uses_with_info(Synthesized, TypedIdentifiers),
    get_operation_params_from_ids(TypedIdentifiers, Params),
    Params \= [],
    !,
    synthesis_util:set_operation_params_domain(Params, ParamTypeDefsPred),
    conjunct_predicates([ParamTypeDefsPred,Synthesized], NewPreCondition).

post_synthesize_predicate(_, Synthesized, Synthesized).

pre_library_setup(UseOperationParameters, Type, _, Example, Library) :-
    % either a specific default library is asserted (like default:1) or an explicit set of library
    % components selected by the user
    library_from_ui(LibraryFromUi),
    !,
    get_asserted_if_statement_vars(ConsiderIfVarNames),
    get_asserted_constant_configuration(NotConsiderConstants),
    get_all_machine_sets(MachineSets),
    library_setup(UseOperationParameters, MachineSets, ConsiderIfVarNames, NotConsiderConstants, LibraryFromUi, Type, Example, Library).

pre_library_setup(UseOperationParameters, Type, LibExpansion, Example, Library) :-
    get_asserted_if_statement_vars(ConsiderIfVarNames),
    get_asserted_constant_configuration(NotConsiderConstants),
    get_all_machine_sets(MachineSets),
    % default if no library is asserted, gets expanded in prolog using synthesis_callback/16
    library_setup(UseOperationParameters, MachineSets, ConsiderIfVarNames, NotConsiderConstants, default:LibExpansion, Type, Example, Library).

prepare_synthesis(Library, DoNotUseConstants, Solver, ConsiderIfVarNames, Positive, Negative, PosInput, PosOutput, NegInput, NegOutput) :-
    % retractall(current_library_lookahead(_)) ,
    % asserta(current_library_lookahead(0)) ,
    retractall(solver(_)),
    asserta(solver(Solver)),
    retractall(not_consider_constants(_)),
    asserta(not_consider_constants(DoNotUseConstants)),
    assert_library_configuration_from_ui(Library),
    assert_if_statement_var_names(ConsiderIfVarNames),
    % split examples that are tuples of input and output state
    split_input_output_tuples(Positive, PosInput, PosOutput),
    split_input_output_tuples(Negative, NegInput, NegOutput),
    !.

prepare_synthesis_of_action_by_examples(Operation, Input, Output, Library, ParameterAmount, M1, CurrentVars, BehavioralConstraint, LocationVars, Solution) :-
    !,
    Input = [Example|_],
    length(Example, ParameterAmount),
    pre_library_setup(yes, action, 1, Example, Library),
    get_current_vars_from_example(Example, CurrentVars),
    get_behavioral_constraint(Library, ([],_), Input, Output, BehavioralConstraint, LocationVars),
    % open('synthesis_constraint.eval',write,Stream) , tell(Stream) ,
    % translate:nested_print_bexpr_as_classicalb(BehavioralConstraint) , nl , nl, close(Stream) ,
    get_line_amount(Operation, Library, Example, M),
    M1 is M-1,
    solve_using_selected_solver(BehavioralConstraint, Solution).

prepare_synthesis_of_guard_by_examples(OperationUsesParameters, VarNames, (ValidGuards,Operation), TPositive, TNegative, Positive, Negative, Library, ParameterAmount, M1,
    CurrentVars, BehavioralConstraint, LocationVars, Solution) :-
    !,
    remove_dups(TPositive, TTPositive),
    remove_dups(TNegative, TTNegative),
    maplist(reduce_input_to_violating_vars(VarNames), TTPositive, TempPositive),
    maplist(reduce_input_to_violating_vars(VarNames), TTNegative, TempNegative),
    get_distinct_states(guard, TempPositive, TempNegative, Positive, Negative),
    % at least one negative example is given since an invariant is violated
    Negative = [Example|_],
    length(Example, ParameterAmount),
    pre_library_setup(OperationUsesParameters, guard, 1, Example, Library),
    get_current_vars_from_example(Example, CurrentVars),
    get_behavioral_constraint_from_input(Library, (ValidGuards,Operation), Positive, Negative, BehavioralConstraint, LocationVars),
    % open('synthesis_constraint.eval',write,Stream) , tell(Stream) ,
    % unsat_cores:unsat_core(BehavioralConstraint,UC) ,
    % translate:nested_print_bexpr_as_classicalb(BehavioralConstraint) , nl , nl, close(Stream) ,
    solve_using_selected_solver(BehavioralConstraint, Solution),
    get_line_amount(Operation, Library, Example, M),
    M1 is M-1.

reset_synthesis_context :-
    retractall(synthesis_context(_, _, _, _, _, _, _, _, _)),
    retractall(additional_machinevars(_)),
    asserta(additional_machinevars([])).

retract_context_if_solution(Distinguishing) :-
    ( Distinguishing = distinguishing(none)
    ; Distinguishing = none
    ),
    !,
    retractall(synthesis_context(_, _, _, _, _, _, _, _, _)),
    retractall(additional_machinevars(_)),
    asserta(additional_machinevars([])).

retract_context_if_solution(_).

set_synthesis_mode(SynthesisMode) :-
    retractall(synthesis_mode(_)),
    assertz(synthesis_mode(SynthesisMode)).

solve_using_selected_solver(Constraint, Solution) :-
    solver(z3),
    smt_solve_predicate(z3, Constraint, _, Solution).

solve_using_selected_solver(Constraint, Solution) :-
    solver(cdclt),
    cdclt_solve_predicate(Constraint, _, Solution).

solve_using_selected_solver(Constraint, Solution) :-
    \+ solver(z3),
    solver_interface:solve_predicate(Constraint, _, Solution).

solver(proB).

start_specific_synthesis(Operation, action, PosInput, NegInput, PosOutput, NegOutput, Action) :-
    set_preference(randomise_enumeration_order, true),
    % no context asserted
    \+ catch(synthesis_context(_, _, _, _, _, _, _, _, _), error(existence_error(_,_),_), fail),
    mark_examples_as_initial(PosInput, PosOutput, InitialInput, InitialOutput),
    prepare_synthesis_of_action_by_examples(Operation, InitialInput, InitialOutput, Library, ParameterAmount, M1, CurrentVars, BehavioralConstraint, LocationVars, Solution),
    % use the negative input states for the distinguishing state cache
    synthesis_from_examples(Operation, b(truth,pred,[]), ([],NegInput), Library, 1, CurrentVars, CurrentVars, any, action, InitialInput,
    InitialOutput, BehavioralConstraint, LocationVars, M1, ParameterAmount, Solution, Synthesized, (_,NegDistInput)),
    !,
    post_synthesize_action(Operation, CurrentVars, InitialInput, InitialOutput, NegInput, NegOutput, NegDistInput, Synthesized, Action).

start_specific_synthesis(Operation, action, PosInput, NegInput, PosOutput, _, Action) :-
    set_preference(randomise_enumeration_order, true),
    % context asserted, synthesis has been suspended
    catch(
    synthesis_context(DistTransitionCache, DistStateCache, CurrentVars, PreCondVars,
    ValidInvariantsOrGuards, action, OldInput, OldOutput, _),
    error(existence_error(_,_),_), fail),
    keep_asserted_initial_examples(PosInput, PosOutput, OldInput, OldOutput, NewPosInput, NewPosOutput),
    start_specific_synthesis_aux(Operation, action, NewPosInput, NegInput, NewPosOutput, _, DistTransitionCache, DistStateCache,
    CurrentVars, PreCondVars, ValidInvariantsOrGuards, Action).

start_specific_synthesis(null, invariant, PosInput, NegInput, PosOutput, NegOutput, SynthesizedInvariant) :-
    set_preference(randomise_enumeration_order, true),
    get_violated_and_valid_machine_invariants(PosOutput, _, _, ValidInvariants),
    get_positive_and_negative_examples_for_invariant_synthesis(PosInput, PosOutput, NegInput, NegOutput, Positive, Negative),
    Positive = [Example|_],
    maplist(get_varname_from_node_info, Example, VarNames),
    synthesis_log(involved_variables(VarNames)),
    pre_library_setup(no, invariant, 1, Example, Library),
    mark_examples_as_initial(Positive, Negative, InitialPositive, InitialNegative),
    get_behavioral_constraint_from_input(Library, ([],_), InitialPositive, InitialNegative, BehavioralConstraint, LocationVars),
    % open('synthesis_constraint_invariant.eval',write,Stream) , tell(Stream) ,
    % translate:nested_print_bexpr_as_classicalb(BehavioralConstraint) , nl , nl, close(Stream) ,
    solve_using_selected_solver(BehavioralConstraint, Solution),
    get_line_amount(_, Library, Example, M),
    M1 is M-1,
    length(Example, ParameterAmount),
    b_get_machinevars_with_operation_params(MachineVars),
    synthesis_from_examples(null, b(truth,pred,[]), ([],[]), Library, 1, MachineVars, MachineVars, ValidInvariants, invariant, InitialPositive,
    InitialNegative, BehavioralConstraint, LocationVars, M1, ParameterAmount, Solution, SynthesizedInvariant, _).

start_specific_synthesis(Operation, invariant, PosInput, NegInput, PosOutput, NegOutput, Synthesized) :-
    set_preference(randomise_enumeration_order, true),
    % use PosInput because at least one invariant violating state has been graduated as valid by the user
    get_violated_and_valid_machine_invariants(PosOutput, ViolatedInvariants, ViolatingVars, ValidInvariants),
    findall(Name, ( member(IDNode, ViolatingVars),
    IDNode = b(identifier(Name),_,_)
    ), VarNames),
    synthesis_log(involved_variables(VarNames)),
    get_positive_and_negative_examples_for_invariant_synthesis(PosInput, PosOutput, NegInput, NegOutput, Pos, Neg),
    maplist(reduce_input_to_violating_vars(VarNames), Pos, TRPositive),
    maplist(reduce_input_to_violating_vars(VarNames), Neg, RNegative),
    TRPositive = [Example|_],
    pre_library_setup(no, invariant, 1, Example, Library),
    get_valid_states(VarNames, 5, TValidStates),
    maplist(reduce_input_to_violating_vars(VarNames), TValidStates, ValidStates),
    append(TRPositive, ValidStates, RPositive),
    remove_dups(RPositive, NRPositive),
    % TODO: what about several invariant violating examples that are graduated to be valid?
    % get the example that violates an invariant but has been graduated to be valid by the user
    get_invariant_violating_example(ViolatedInvariants, PosInput, PosOutput, (In,Out)),
    % get counter example
    get_invariant_violating_transition(Operation, ViolatingVars, ViolatedInvariants, In, Out, Counter),
    start_specific_synthesis_aux(Operation, invariant, ValidInvariants, VarNames, NRPositive, RNegative, ViolatingVars, Library, Counter, Synthesized).

start_specific_synthesis(Operation, guard, PosInput, NegInput, _, NegOutput, SynthesizedGuard) :-
    set_preference(randomise_enumeration_order, true),
    get_guard_list_from_operation(Operation, Guards),
    get_involved_variables(Guards, PosInput, NegOutput, InvolvedVarNames),
    % filter partial guards that are valid for the examples, and thus, do not need to be relaxed,
    % these are conjuncted to the synthesized guard later on
    findall(ValidGuard, ( member(ValidGuard, Guards),
    find_identifier_uses(ValidGuard, [], UsedIDs),
    intersection(UsedIDs, InvolvedVarNames, [])
    ), ValidGuards),
    mark_examples_as_initial(PosInput, NegInput, InitialPosInput, InitialNegInput),
    % TODO: handle operation parameters
    % get_machinevars_by_name(InvolvedVarNames,InvolvedVarNodes) ,
    % get_valid_transitions_for_operation(InvolvedVarNodes,3,Operation,ValidInput,_) ,
    % append(InitialPosInput,ValidInput,ExtendedPosInput) ,
    machine_operation_uses_parameters(Operation, OperationUsesParameters),
    prepare_synthesis_of_guard_by_examples(OperationUsesParameters, InvolvedVarNames, (ValidGuards,Operation), InitialPosInput, InitialNegInput, Positive, Negative, Library,
    ParameterAmount, M1, CurrentVars, BehavioralConstraint, LocationVars, Solution),
    synthesis_from_examples(Operation, b(truth,pred,[]), ([],[]), Library, 1, CurrentVars, CurrentVars, ValidGuards, guard, Positive, Negative,
    BehavioralConstraint, LocationVars, M1, ParameterAmount, Solution, SynthesizedGuard, _),
    synthesis_log(solution(guard,SynthesizedGuard)).

start_specific_synthesis_aux(Operation, invariant, ValidInvariants, VarNames, Positive, TNegative, ViolatingVars, Library, (TCounterIn,TCounterOut), SynthesizedInvariant) :-
    maplist(reduce_input_to_violating_vars(VarNames), [TCounterIn,TCounterOut], [CounterIn,CounterOut]),
    % don't create contradiction by using the same example as positive and negative
    findall(Counter, ( member(Counter, [CounterIn,CounterOut]),
    \+ contains_equivalent_state(Counter, Positive, _)
    ), CounterStates),
    append(CounterStates, TNegative, Negative),
    mark_examples_as_initial(Positive, Negative, InitialPositive, InitialNegative),
    get_behavioral_constraint_from_input(Library, ([],_), InitialPositive, InitialNegative, BehavioralConstraint, LocationVars),
    solve_using_selected_solver(BehavioralConstraint, Solution),
    get_line_amount(Operation, Library, CounterIn, M),
    M1 is M-1,
    length(CounterIn, ParameterAmount),
    synthesis_from_examples(Operation, b(truth,pred,[]), ([],[]), Library, 1, ViolatingVars, ViolatingVars, ValidInvariants, invariant, InitialPositive,
    InitialNegative, BehavioralConstraint, LocationVars, M1, ParameterAmount, Solution, SynthesizedInvariant, _),
    synthesis_log(solution(invariant,SynthesizedInvariant)).

start_specific_synthesis_aux(_, invariant, [], _, _, _, _, _, _, b(truth,pred,[])) :-
    synthesis_log(solution(invariant,b(truth,pred,[]))).

start_specific_synthesis_aux(_, invariant, ValidInvariants, _, _, _, _, _, _, Invariant) :-
    conjunct_predicates(ValidInvariants, Invariant),
    synthesis_log(solution(invariant,Invariant)).

start_specific_synthesis_aux(Operation, action, NewPosInput, NegInput, NewPosOutput, NegOutput, DistTransitionCache, DistStateCache,
    CurrentVars, PreCondVars, _, Action) :-
    % synthesize guard if negative input states are given and synthesis has been suspended
    NegInput \= [],
    maplist(get_varname_from_id_node, PreCondVars, PreCondVarNames),
    DistStateCache = (PosDist,NegDist),
    append(NewPosInput, PosDist, GuardPositive),
    append(NegInput, NegDist, GuardNegative),
    % if neginput empty
    use_operation_parameters_for_current_synthesis_type(Operation, guard, OperationUsesParameters),
    prepare_synthesis_of_guard_by_examples(OperationUsesParameters, PreCondVarNames, ([],_), GuardPositive, GuardNegative, PrePositive, PreNegative,
    PreLibrary, PreParameterAmount, PreM1, _, PreBehavioralConstraint, PreLocationVars, Solution),
    synthesis_from_examples(Operation, b(truth,pred,[]), (PrePositive,PreNegative), PreLibrary, 1, PreCondVars, PreCondVars,
    any, guard, PrePositive, PreNegative, PreBehavioralConstraint, PreLocationVars, PreM1,
    PreParameterAmount, Solution, Guards, PreDistStateCache),
    ( is_distinguishing(Guards)
    ->
    Action = Guards
    ; prepare_synthesis_of_action_by_examples(Operation, NewPosInput, NewPosOutput, Library, ParameterAmount, M1, CurrentVars, BehavioralConstraint,
    LocationVars, Solution),
    prepare_synthesized_guards_for_action(Guards, GuardsForAction),
    synthesis_from_examples(Operation, DistTransitionCache, PreDistStateCache, Library, 1, CurrentVars, PreCondVars,
    GuardsForAction, action, NewPosInput, NewPosOutput, BehavioralConstraint, LocationVars,
    M1, ParameterAmount, Solution, Synthesized, (_,NegDistInput)),
    !,
    post_synthesize_action(Operation, CurrentVars, NewPosInput, NewPosOutput, NegInput, NegOutput, NegDistInput, Synthesized, Action)
).

start_specific_synthesis_aux(Operation, action, NewPosInput, [], NewPosOutput, _, DistTransitionCache, DistStateCache,
    CurrentVars, PreCondVars, ValidInvariantsOrGuards, Action) :-
    prepare_synthesis_of_action_by_examples(Operation, NewPosInput, NewPosOutput, Library, ParameterAmount, M1, CurrentVars, BehavioralConstraint,
    LocationVars, Solution),
    synthesis_from_examples(Operation, DistTransitionCache, DistStateCache, Library, 1, CurrentVars, PreCondVars,
    ValidInvariantsOrGuards, action, NewPosInput, NewPosOutput, BehavioralConstraint, LocationVars,
    M1, ParameterAmount, Solution, Synthesized, (_,NegDistInput)),
    !,
    post_synthesize_action(Operation, CurrentVars, NewPosInput, NewPosOutput, [], [], NegDistInput, Synthesized, Action).

start_synthesis_from_ui(SolverTimeOut, Library, DoNotUseConstants, Solver, ConsiderIfVarNames, Operation, SynthesisType, Positive, Negative, NewMachineAtom, Distinguishing) :-
    synthesis_mode(SynthesisMode),
    start_synthesis_from_ui(SynthesisMode, yes, SolverTimeOut, Library, DoNotUseConstants, Solver, ConsiderIfVarNames, Operation, SynthesisType, Positive, Negative, NewMachineAtom, Distinguishing).

start_synthesis_from_ui(SynthesisMode, AdaptMachineCode, SolverTimeOut, Library, DoNotUseConstants, Solver, ConsiderIfVarNames, Operation, SynthesisType, Positive, Negative, NewMachineAtom, Distinguishing) :-
    set_preference(time_out, SolverTimeOut),
    logging:enable_logging,
    set_synthesis_mode(SynthesisMode),
    prepare_synthesis(Library, DoNotUseConstants, Solver, ConsiderIfVarNames, Positive, Negative, PosInput, PosOutput, NegInput, NegOutput),
    start_synthesis_from_ui_aux(Operation, SynthesisType, (PosInput,PosOutput), (NegInput,NegOutput), (_,Synthesized)),
    !,
    prepare_solution(AdaptMachineCode, Operation, SynthesisType, Synthesized, NewMachineAtom, Distinguishing),
    retract_context_if_solution(Distinguishing).

start_synthesis_from_ui_aux(Operation, action, (PosInput,PosOutput), (NegInput,NegOutput), (DistStateCache,FinalAction)) :-
    % synthesizing the action already succeeded but synthesizing an appropriate guard afterwards has been suspended by
    % finding a distingushing state, the synthesized action is asserted and we just synthesize the guard here
    catch(synthesis_context(_, DistStateCache, _, PreCondVars, _, guard, OldPosInput, OldNegInput, Action),
    error(existence_error(_,_),_), fail),
    \+ catch(synthesis_context(_, _, _, _, _, action, _, _, _),
    error(existence_error(_,_),_), fail),
    Action \== temp(_),
    !,
    ( add_operation_parameter_values_to_examples(PosInput, PosOutput, NegInput, NegOutput, [Action], ExtendedPosInput, ExtendedNegInput)
    ; PosInput = ExtendedPosInput,
    NegInput = ExtendedNegInput
    ),
    keep_asserted_initial_examples(ExtendedPosInput, ExtendedNegInput, OldPosInput, OldNegInput, NewPosInput, NewNegInput),
    post_synthesize_action(Operation, PreCondVars, NewPosInput, PosOutput, NewNegInput, NegOutput, [], Action, FinalAction).

start_synthesis_from_ui_aux(Operation, action, (PosInput,PosOutput), (NegInput,NegOutput), (NewDistStateCache,FinalAction)) :-
    % synthesis type is action but the simultaneous generation of a guard has been suspended by finding a distinguishing state,
    % synthesizing the action has not succeeded yet
    catch(synthesis_context(_, PreDistStateCache, _, PreCondVars, ValidInvariantsOrGuards, guard, OldPosInput, OldNegInput, temp(Actions)),
    error(existence_error(_,_),_), fail),
    retractall(synthesis_context(_, _, _, _, ValidGuards, guard, _, _, _)),
    ( add_operation_parameter_values_to_examples(PosInput, PosOutput, NegInput, NegOutput, Actions, ExtendedPosInput, ExtendedNegInput)
    ; PosInput = ExtendedPosInput,
    NegInput = ExtendedNegInput
    ),
    keep_asserted_initial_examples(ExtendedPosInput, ExtendedNegInput, OldPosInput, OldNegInput, NewPosInput, NewNegInput),
    maplist(get_varname_from_id_node, PreCondVars, PreVarNames),
    % therefore we start/restart synthesis of a guard
    synthesized_operation_uses_parameters(Actions, OperationUsesParameters),
    prepare_synthesis_of_guard_by_examples(OperationUsesParameters, PreVarNames, (ValidGuards,Operation), NewPosInput, NewNegInput, PrePositive, PreNegative, PreLibrary,
    PreParameterAmount, PreM1, PreCurrentVars, PreBehavioralConstraint, PreLocationVars, PreSolution),
    synthesis_from_examples(Operation, b(truth,pred,[]), PreDistStateCache, PreLibrary, 1, PreCurrentVars, PreCurrentVars, ValidInvariantsOrGuards, guard, PrePositive, PreNegative,
    PreBehavioralConstraint, PreLocationVars, PreM1, PreParameterAmount, PreSolution, PreCondition, NewDistStateCache),
    distinguishing_state_or_synthesize_action(Operation, PreCondition, NewDistStateCache, (PosInput,PosOutput), (NegInput,NegOutput), FinalAction).

start_synthesis_from_ui_aux(Operation, action, (PosInput,PosOutput), (NegInput,NegOutput), (NewDistStateCache,FinalAction)) :-
    % synthesizing an action has been suspended by a distinguishing transition, but the user validated the distinguishing example to be negative
    \+ catch(synthesis_context(_, _, _, _, _, guard, _, _, _),
    error(existence_error(_,_),_), fail),
    catch(synthesis_context(_, DistStateCache, _, _, ValidInvariantsOrGuards, action, OldPosInput, OldNegInput, temp(Action)),
    error(existence_error(_,_),_), fail),
    length(OldPosInput, PLen),
    length(PosInput, PLen),
    length(OldNegInput, NLen),
    length(NegInput, NLen),
    NegInput \= [],
    !,
    ( add_operation_parameter_values_to_examples(PosInput, PosOutput, NegInput, NegOutput, [Action], ExtendedPosInput, ExtendedNegInput)
    ; PosInput = ExtendedPosInput,
    NegInput = ExtendedNegInput
    ),
    keep_asserted_initial_examples(ExtendedPosInput, ExtendedNegInput, OldPosInput, OldNegInput, NewPosInput, NewNegInput),
    ExtendedPosInput = [Example|_],
    maplist(get_varname_from_node_info, Example, PreVarNames),
    % therefore we start/restart synthesis of a guard
    synthesized_operation_uses_parameters([Action], OperationUsesParameters),
    prepare_synthesis_of_guard_by_examples(OperationUsesParameters, PreVarNames, (ValidInvariantsOrGuards,Operation), NewPosInput, NewNegInput, PrePositive, PreNegative, PreLibrary,
    PreParameterAmount, PreM1, PreCurrentVars, PreBehavioralConstraint, PreLocationVars, PreSolution),
    synthesis_from_examples(Operation, b(truth,pred,[]), DistStateCache, PreLibrary, 1, PreCurrentVars, PreCurrentVars, ValidInvariantsOrGuards, guard, PrePositive, PreNegative,
    PreBehavioralConstraint, PreLocationVars, PreM1, PreParameterAmount, PreSolution, PreCondition, NewDistStateCache),
    distinguishing_state_or_synthesize_action(Operation, PreCondition, NewDistStateCache, (PosInput,PosOutput), (NegInput,NegOutput), FinalAction).

start_synthesis_from_ui_aux(Operation, action, (PosInput,PosOutput), (NegInput,NegOutput), ((PosDistInput,NegDistInput),FinalAction)) :-
    % synthesizing an action has been suspended by a distinguishing transition, no guard
    \+ catch(synthesis_context(_, _, _, _, _, guard, _, _, _),
    error(existence_error(_,_),_), fail),
    catch(synthesis_context(DistTransitionCache, DistStateCache, _, PreCondVars, ValidGuards, action, OldPosInput, OldPosOutput, _),
    error(existence_error(_,_),_), fail),
    retractall(synthesis_context(_, _, _, _, _, action, _, _, _)),
    keep_asserted_initial_examples(PosInput, PosOutput, OldPosInput, OldPosOutput, NewPosInput, NewPosOutput),
    prepare_synthesis_of_action_by_examples(Operation, NewPosInput, NewPosOutput, Library, ParameterAmount, M1, CurrentVars, BehavioralConstraint, LocationVars, Solution),
    DistStateCache = (PosDist,NegDist),
    append(NegInput, NegDist, NewNegDist),
    synthesis_from_examples(Operation, DistTransitionCache, (PosDist,NewNegDist), Library, 1, CurrentVars, PreCondVars, ValidGuards, action,
    NewPosInput, NewPosOutput, BehavioralConstraint, LocationVars, M1, ParameterAmount, Solution, Synthesized, (PosDistInput,NegDistInput)),
    !,
    Synthesized \= none,
    post_synthesize_action(Operation, CurrentVars, NewPosInput, NewPosOutput, NegInput, NegOutput, NegDistInput, Synthesized, FinalAction).

start_synthesis_from_ui_aux(Operation, action, (PosInput,PosOutput), (NegInput,NegOutput), (DistStateCache,Synthesized)) :-
    % no context asserted, start new synthesis instance for type action,
    % check if the machine already satisfies the behavior and relax a guard or synthesize a new operation
    !,
    behavior_satisfied_or_extend_machine(Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized),
    ( catch(synthesis_context(_, DistStateCache, _, _, _, _, _, _, _), error(existence_error(_,_),_), fail)
    ->
    true
    ; DistStateCache = ([],[])
).

start_synthesis_from_ui_aux(Operation, SynthesisType, (PosInput,_), (NegInput,_), (DistStateCache,Synthesized)) :-
    SynthesisType \= action,
    % go on synthesizing the guard/invariant using the validated distinguishing state
    catch(synthesis_context(_, PreDistStateCache, _, PreCondVars, ValidInvariantsOrGuards, SynthesisType, OldPosInput, OldNegInput, _),
    error(existence_error(_,_),_), fail),
    retractall(synthesis_context(_, _, _, _, _, SynthesisType, _, _, _)),
    keep_asserted_initial_examples(PosInput, NegInput, OldPosInput, OldNegInput, NewPosInput, NewNegInput),
    maplist(get_varname_from_id_node, PreCondVars, PreVarNames),
    machine_operation_uses_parameters(Operation, OperationUsesParameters),
    prepare_synthesis_of_guard_by_examples(OperationUsesParameters, PreVarNames, (ValidInvariantsOrGuards,Operation), NewPosInput, NewNegInput, PrePositive, PreNegative, PreLibrary, PreParameterAmount, PreM1, PreCurrentVars,
    PreBehavioralConstraint, PreLocationVars, PreSolution),
    synthesis_from_examples(Operation, b(truth,pred,[]), PreDistStateCache, PreLibrary, 1, PreCurrentVars, PreCurrentVars, ValidInvariantsOrGuards, SynthesisType, PrePositive,
    PreNegative, PreBehavioralConstraint, PreLocationVars, PreM1, PreParameterAmount, PreSolution, TSynthesized, DistStateCache),
    TSynthesized \= none,
    post_synthesize_predicate(SynthesisType, TSynthesized, Synthesized).

start_synthesis_from_ui_aux(Operation, SynthesisType, (PosInput,PosOutput), (NegInput,NegOutput), (DistStateCache,Synthesized)) :-
    % no context asserted, we start a new synthesis instance
    \+ catch(synthesis_context(_, _, _, _, _, _, _, _, _),
    error(existence_error(_,_),_), fail),
    start_specific_synthesis(Operation, SynthesisType, PosInput, NegInput, PosOutput, NegOutput, TSynthesized),
    !,
    ( catch(synthesis_context(_, DistStateCache, _, _, _, _, _, _, _), error(existence_error(_,_),_), fail)
    ->
    true
    ; DistStateCache = ([],[])
    ),
    TSynthesized \= none,
    post_synthesize_predicate(SynthesisType, TSynthesized, Synthesized).

start_synthesis_single_operation_from_ui(SolverTimeOut, Operations, Library, DoNotUseConstants, Solver, Operation, action, Positive, Negative, CacheOperationTuple, Distinguishing) :-
    set_preference(time_out, SolverTimeOut),
    % TODO: consider the other examples to check against distinguishing examples, this is not essential though and works as is
    prepare_synthesis(Library, DoNotUseConstants, Solver, [], Positive, Negative, PosInput, PosOutput, NegInput, NegOutput),
    ( Operations = []
    ->
    Result = no_match
    ; maplist(cache_operation_tuple_to_quadruple, Operations, OperationQuadruples),
    PosInput = [Input],
    PosOutput = [Output],
    findall(UsedID, ( member(Value, Input),
    get_texpr_info(Value, Info),
    member(synthesis(machinevar,UsedID), Info)
    ), UsedIDs),
    get_machinevars_by_name(UsedIDs, UsedIDNodes),
    check_transition_against_machine_operations(OperationQuadruples, Input, Output, UsedIDNodes, Result)
    ),
    start_synthesis_single_operation_from_ui_aux(Result, Operations, Operation, PosInput, PosOutput, NegInput, NegOutput, CacheOperationTuple, Distinguishing),
    retract_context_if_solution(Distinguishing).

start_synthesis_single_operation_from_ui_aux((OperationName,done), _, _, _, _, _, _, done(OperationName,done), none).

start_synthesis_single_operation_from_ui_aux((OperationName,guard), Operations, _, PosInput, _, NegInput, _, FinalOperation, Distinguishing) :-
    get_distinguishing_state_cache_from_operation_tuples(Operations, OperationName, (CachePos,CacheNeg), Operation),
    append(PosInput, CachePos, Positive),
    append(NegInput, CacheNeg, Negative),
    start_synthesis_from_ui_aux(OperationName, guard, (Positive,_), (Negative,_), (_,SynthesizedGuard)),
    !,
    prepare_solution(yes, Operation, guard, SynthesizedGuard, _, Distinguishing),
    ( is_distinguishing(SynthesizedGuard) ->
    FinalOperation = none
    ; replace_precondition_of_operation(Operation, SynthesizedGuard, FinalOperation)
).

start_synthesis_single_operation_from_ui_aux(no_match, _, Operation, PosInput, PosOutput, NegInput, NegOutput, CacheOperationTuple, Distinguishing) :-
    start_synthesis_from_ui_aux(Operation, action, (PosInput,PosOutput), (NegInput,NegOutput), (DistStateCache,Synthesized)),
    !,
    prepare_solution(yes, Operation, action, Synthesized, _, Distinguishing),
    ( is_distinguishing(Synthesized) ->
    CacheOperationTuple = none
    ; CacheOperationTuple = (DistStateCache,Synthesized)
).

synthesis_callback(_, _, DistStateCache, _, _, NewLibExpansion, _, _, _, _, _, _, _, _, _, Synthesized, NewDistStateCache) :-
    % (subtract(NewLibrary,OldLibrary,[]) ;
    max_library_expansion(MaxLibExpansion),
    NewLibExpansion > MaxLibExpansion,
    !,
    Synthesized = none,
    NewDistStateCache = DistStateCache.

synthesis_callback(_, _, DistStateCache, _, _, _, _, _, _, _, _, _, _, _, _, Synthesized, NewDistStateCache) :-
    catch(library_from_ui(Library), error(existence_error(_,_),_), fail),
    Library \= default,
    !,
    Synthesized = none,
    NewDistStateCache = DistStateCache.

synthesis_callback(Operation, DistTransitionCache, DistStateCache, _, NewLibrary, NewLibExpansion, CurrentVars, PreCondVars,
    ValidInvariantsOrGuards, _, ParameterAmount, Type, NewLibrary, PosInput, NegInput, Synthesized, NewDistStateCache) :-
    synthesis_log(expand_library),
    get_behavioral_constraint_aux((ValidInvariantsOrGuards,Operation), Type, NewLibrary, PosInput, NegInput, NewBehavioralConstraint, NewLocationVars),
    solve_using_selected_solver(NewBehavioralConstraint, NewSolution),
    !,
    % compute the new amount of lines of the synthesized program using the expanded library
    PosInput = [Input|_],
    get_line_amount(Operation, NewLibrary, Input, M),
    NewM1 is M-1,
    synthesis_from_examples(Operation, DistTransitionCache, DistStateCache, NewLibrary, NewLibExpansion, CurrentVars, PreCondVars,
    ValidInvariantsOrGuards, Type, PosInput, NegInput, NewBehavioralConstraint, NewLocationVars,
    NewM1, ParameterAmount, NewSolution, Synthesized, NewDistStateCache).

synthesis_from_examples(Operation, DistTransitionCache, DistStateCache, Library, LibExpansion, CurrentVars, PreCondVars,
    ValidInvariantsOrGuards, Type, PosInput, NegInput, BehavioralConstraint, LocationVars,
    M1, ParameterAmount, Solution, Synthesized, NewDistStateCache) :-
    synthesis_log(start_synthesis_loop(DistTransitionCache,DistStateCache,Library,LibExpansion,CurrentVars,PreCondVars,
    ValidInvariantsOrGuards,Type,PosInput,NegInput,LocationVars,M1,ParameterAmount,Solution)),
    Solution = solution(SolutionBindings),
    set_preference(randomise_enumeration_order, true),
    location_vars_to_program(Library, Type, CurrentVars, LocationVars, M1, ParameterAmount, Solution, UsedLVars1, ProgramAST),
    % extend the BehavioralConstraint by a constraint excluding specific location mappings that
    % lead to just swapping equivalent components without changing the semantics
    get_prevent_component_swap_constraint(UsedLVars1, SolutionBindings, LocationVars, ComponentSwapExclusion),
    ExtendedBehavioralConstraint = b(conjunct(BehavioralConstraint,ComponentSwapExclusion),pred,[]),
    % In UsedLVars we have the used location variables from the synthesized solution, so we are able
    % to exclude those specific bindings when searching for a further solution (otherwise it would
    % be enough to just change some deadcode).
    find_further_solution(ProgramAST, LocationVars, UsedLVars1, Solution, ExtendedBehavioralConstraint, FurtherSolution, NewBehavioralConstraint),
    synthesis_log(defective_further_solution_and_fail(Type,NewBehavioralConstraint,FurtherSolution,Library,CurrentVars,
    PosInput,NegInput,LocationVars,M1,ParameterAmount)),
    !,
    add_distinguishing_states_from_cache(Type, DistStateCache, PosInput, NegInput, NewPosInput, NewPosOutput),
    synthesis_from_examples_aux1(Operation, DistTransitionCache, DistStateCache, Library, LibExpansion, CurrentVars, PreCondVars,
    ValidInvariantsOrGuards, Type, NewPosInput, NewPosOutput, ExtendedBehavioralConstraint, LocationVars,
    M1, ParameterAmount, Solution, FurtherSolution, NewBehavioralConstraint, Synthesized, NewDistStateCache).

synthesis_from_examples(Operation, DistTransitionCache, DistStateCache, OldLibrary, LibExpansion, CurrentVars, PreCondVars,
    ValidInvariantsOrGuards, Type, PosInput, NegInput, _, _, M1, ParameterAmount, Solution,
    Synthesized, NewDistStateCache) :-
    Solution \= solution(_),
    NewLibExpansion is LibExpansion+1,
    PosInput = [Example|_],
    use_operation_parameters_for_current_synthesis_type(Operation, Type, OperationUsesParameters),
    pre_library_setup(OperationUsesParameters, Type, NewLibExpansion, Example, NewLibrary),
    !,
    % library has changed
    synthesis_callback(Operation, DistTransitionCache, DistStateCache, OldLibrary, NewLibrary, NewLibExpansion,
    CurrentVars, PreCondVars, ValidInvariantsOrGuards, M1, ParameterAmount, Type, NewLibrary, PosInput,
    NegInput, Synthesized, NewDistStateCache).