predicate_handling

add_inner_inputs_to_op(Subst,Ids,SubstOut) :-
    get_texpr_expr(Subst,Expr),
    add_inner_inputs_to_op_aux(Expr,Ids,ExprOut), !,
    safe_create_texpr(ExprOut,pred,SubstOut).

add_inner_inputs_to_op(Subst,[],Subst).

add_inner_inputs_to_op_aux(conjunct(A,B),Ids,conjunct(NA,NB)) :- !,
    add_inner_inputs_to_op(A,AIds,NA),
    add_inner_inputs_to_op(B,BIds,NB),
    append(AIds,BIds,Ids).

add_inner_inputs_to_op_aux(disjunct(A,B),Ids,disjunct(NA,NB)) :- !,
    add_inner_inputs_to_op(A,AIds,NA),
    add_inner_inputs_to_op(B,BIds,NB),
    append(AIds,BIds,Ids).

add_inner_inputs_to_op_aux(member(A,B),[InputId],conjunct(b(member(A,B),pred,[]),Eq)) :- !,
    get_texpr_type(A,Type),
    unique_typed_id("_ic3_pi",Type,InputId),
    safe_create_texpr(equal(A,InputId),pred,Eq).

add_inner_inputs_to_op_aux(equal(A,B),[],equal(A,B)) :- !.

add_input_to_op(Op,IId,OpOut) :-
    unique_typed_id("_ic3_pi",integer,IId),
    safe_create_texpr(integer(1),integer,Int1),
    safe_create_texpr(equal(IId,Int1),pred,EqualToOne),
    add_inner_inputs_to_op(Op,_InnerIIds,Op2),
    conjunct_predicates([Op2,EqualToOne],OpOut).

add_primary_inputs(TIn,TOut) :-
    % transition is a disjunction
    % as a first step add an integer variable to each disjunct
    % + a constraint stating that the sum is 1
    disjunction_to_list(TIn,Disjuncts),
    maplist(add_input_to_op,Disjuncts,TopLevelIdentifiers,DisjunctsOut),
    sum_is_one(TopLevelIdentifiers,Constraint),
    disjunct_predicates(DisjunctsOut,Disjunction),
    conjunct_predicates([Disjunction,Constraint],TOut).

build_sum([Id],Id).

build_sum([Id|Ids],Sum) :-
    build_sum(Ids,SubSum),
    safe_create_texpr(add(Id,SubSum),integer,Sum).

create_constants_state_predicate(Solution,ConstantsStatePred) :-
    include(unprimed,Solution,UPSolution),
    b_get_machine_constants(Csts),
    include(filter_vars_and_constants(Csts),UPSolution,UPSolutionOnlyConstants),
    UPSolutionOnlyConstants \= [],
    create_state_predicate_aux(UPSolutionOnlyConstants,ConstantsStatePred).

create_negation_and_cleanup(P,NP) :-
    get_texpr_expr(P,implication(A,B)), !,
    create_negation_and_cleanup(B,NegB),
    safe_create_texpr(conjunct(A,NegB),pred,NP).

create_negation_and_cleanup(P,NP) :-
    create_negation(P,NP).

create_primary_inputs_predicate(Solution,InputsPred) :-
    exclude(primed,Solution,NoPrimes),
    include(primary_input,NoPrimes,NoPrimesNoState),
    maplist(create_single_assignment_predicate(NoPrimesNoState),NoPrimesNoState,SolutionPreds),
    conjunct_predicates(SolutionPreds,InputsPred).

create_single_assignment_predicate(VandC,binding(Name,Value,_PP),Pred) :-
    % fetch the type for the particular variable / constant
    member(b(identifier(Name),Type,Infos),VandC),
    Pred = b(equal(b(identifier(Name),Type,Infos),b(value(Value),Type,[])),pred,[]).

create_state_predicate(Solution,StatePredicate) :-
    include(unprimed,Solution,UPSolution),
    create_state_predicate_aux(UPSolution,StatePredicate).

create_state_predicate_aux(Solution,StatePredicate) :-
    b_get_machine_variables(Vars), b_get_machine_constants(Csts),
    append(Vars,Csts,VandC),
    include(filter_vars_and_constants(VandC),Solution,SolutionOnlyStateVars),
    maplist(create_single_assignment_predicate(VandC),SolutionOnlyStateVars,SolutionPreds),
    conjunct_predicates(SolutionPreds,StatePredicate).

create_succ_state_predicate(Solution,SStatePredicate) :-
    deprime_state(Solution,DePrimedState),
    create_state_predicate_aux(DePrimedState,SStatePredicate).

deprime_state(State,DeprimedState) :-
    include(primed,State,PSolution),
    maplist(remove_prime_from_binding,PSolution,DeprimedState).

do_not_prime_identifier(Id) :- b_global_set(Id).

do_not_prime_identifier(Id) :- lookup_global_constant(Id,_).

do_not_prime_identifier(Id) :- b_is_constant(Id,_).

filter_vars_and_constants(VandC,binding(Id,_,_)) :-
    member(b(identifier(Id),_,_),VandC).

get_initial_state_predicate(Init) :-
    % the initial state contains both the constants defined by the properties
    % and the variables set by the initialisation
    b_get_properties_from_machine(Properties),
    b_get_initialisation_from_machine(Initialisation,_),
    before_after_predicate_with_equalities(Initialisation,[],InitialisationPred),
    conjunct_predicates([Properties,InitialisationPred],PredWithPrimes),
    transform_bexpr(predicate_handling:remove_prime_from_expression,PredWithPrimes,Init).

get_single_transition_predicate(OpName,TP) :-
    b_get_machine_operation(OpName,_Results,_Parameters,Body),
    b_get_machine_variables(Variables),
    %b_get_machine_constants(Constants), append(Variables,Constants,VarsAndConsts),
    before_after_predicate_with_equalities(Body,Variables,TransitionPredicateNoInputs),
    add_primary_inputs(TransitionPredicateNoInputs,TP).

get_transition_predicate(TransitionPredicate) :-
    get_preference(use_po,false), !,
    findall(Body,b_get_machine_operation(_Name,_Results,_Parameters,Body),ListOfBodies),
    b_get_machine_variables(Variables),
    %b_get_machine_constants(Constants),append(Variables,Constants,VarsAndConsts),
    before_after_predicate_list_disjunct_with_equalities(ListOfBodies,Variables,TransitionPredicateNoInputs),
    add_primary_inputs(TransitionPredicateNoInputs,TransitionPredicate).

get_transition_predicate(TransitionPredicate) :-
    get_preference(use_po,true), !,
    findall(op(OpName,Pred),(before_after_predicate_for_operation(OpName,Pred)),Ops),
    maplist(op_to_transition,Ops,SingleSteps),
    disjunct_predicates(SingleSteps,TransitionPredicateNoInputs),
    add_primary_inputs(TransitionPredicateNoInputs,TransitionPredicate).

is_primed_codes(Codes) :- last(Codes,39).

is_primed_id_atom(Atom) :- atom_codes(Atom,Codes), is_primed_codes(Codes).

is_primed_typed_identifier(TExpr) :-
    get_texpr_id(TExpr,ID),
    is_primed_id_atom(ID).

op_to_transition(op(OpName,BaPred),StepConstraint) :-
    (get_proven_invariant(OpName,ProvenInvariant)
    -> true ; ProvenInvariant = b(truth,pred,[])),
    prime_predicate(ProvenInvariant,PrimedProvenInvariant),
    conjunct_predicates([BaPred,PrimedProvenInvariant],StepConstraint).

primary_input(binding(Id,_,_)) :- atom_codes(Id,Codes), prefix("_ic3_pi", Codes).

prime_expression(A,B) :-
    create_texpr(OExpr,Type,Info,A),
    (select(used_ids(Old),Info,Info2),
    maplist(prime_id_atom_if_necessary,Old,New), % also rename used_ids for exists/forall
    sort(New,SNew)
    -> NewInfo=[used_ids(SNew)|Info2]
    ; NewInfo=Info),
    create_texpr(NExpr,Type,NewInfo,B),
    prime_texpr(OExpr,Type,NExpr).

prime_id_atom(Old,New) :- atom_concat(Old,'\'',New). % code 39

prime_id_atom_if_necessary(Old,New) :- do_not_prime_identifier(Old),!,New=Old.

prime_id_atom_if_necessary(Old,New) :- prime_id_atom(Old,New).

prime_n_times(0,P,P) :- !.

prime_n_times(N,P,Primed) :-
    prime_predicate(P,T),
    N2 is N - 1,
    prime_n_times(N2,T,Primed).

prime_predicate(A,B) :-
    prime_expression(A,B),
    check_ast(B).

prime_texpr(identifier(Old),_Type,identifier(New)) :-
    % write(pt(Old,_Type)), nl,
    do_not_prime_identifier(Old), !,
    Old = New.

prime_texpr(identifier(Old),_Type,identifier(New)) :- !,
    prime_id_atom(Old,New).

prime_texpr(lazy_lookup_expr(Old),_,lazy_lookup_expr(New)) :-
    !, prime_id_atom(Old,New).

prime_texpr(lazy_lookup_pred(Old),_,lazy_lookup_pred(New)) :-
    !, prime_id_atom(Old,New).

prime_texpr(OExpr,_,NExpr) :-
    syntaxtransformation(OExpr,Subs,_TNames,NSubs,NExpr),
    prime_texpr_l(Subs,NSubs).

prime_texpr_l([],[]).

prime_texpr_l([Old|ORest],[New|NRest]) :-
    prime_expression(Old,New),
    prime_texpr_l(ORest,NRest).

prime_typed_identifier(b(identifier(Id),Type,Info),b(identifier(PId),Type,Info)) :-
    prime_id_atom(Id,PId).

primed(binding(Id,_,_)) :- atom_codes(Id,Codes), is_primed_codes(Codes).

remove_prime_from_binding(binding(Id,Res,PP),binding(NId,Res,PP)) :-
    remove_prime_id_atom(Id,NId).

remove_prime_from_expression(b(identifier(Id),Type,Infos),b(identifier(NId),Type,Infos)) :- !,
    remove_prime_id_atom(Id,NId).

remove_prime_from_expression(Expr,Expr).

remove_prime_id_atom(Id,NoPrimeId) :-
    atom_codes(Id,Codes),
    remove_primed_codes(Codes,NoPrimeIdCodes),
    !,
    atom_codes(NoPrimeId,NoPrimeIdCodes).

remove_prime_id_atom(Id,Id).

remove_prime_typed_identifier(b(identifier(Id),Type,Info),b(identifier(RemovedPrimeId),Type,Info)) :-
    remove_prime_id_atom(Id,RemovedPrimeId).

remove_primed_codes(Codes,NoPrimeIdCodes) :- append(NoPrimeIdCodes,[39],Codes).

sum_is_one(Identifiers,Constraint) :-
    build_sum(Identifiers,Sum),
    safe_create_texpr(integer(1),integer,Int1),
    safe_create_texpr(equal(Sum,Int1),pred,Constraint).

unprimed(binding(Id,_,_)) :- atom_codes(Id,Codes), \+ is_primed_codes(Codes).