proz

add_errors([]).

add_errors([T|Rest]) :-
    add_error(proz,'Z conversion testcase failed: ', T),
    add_errors(Rest).

add_locals(IdentifiersL,LocalsIn,LocalsOut) :-
    append(IdentifiersL,Identifiers),
    get_texpr_ids(Identifiers,UIds),sort(UIds,Ids),
    ord_union(LocalsIn,Ids,LocalsOut).

all_members([],_).

all_members([FirstMember|Members], List) :-
    member(FirstMember, List),!,
    all_members(Members, List).

append_gif(Name,Gif) :- atom_concat(Name,'.gif',Gif).

classify_init_state(Deps,'Init',State) :-
    findall(S,member(dep('Init',S),Deps),[State]).

classify_init_state(Deps,SchemaName,State) :-
    % see if we can find another Schema with Init in its name, which references exactly one other atomic Schema
    member(dep(SchemaName,_),Deps),
    atom_codes(SchemaName,SCodes),
    atom_codes('Init',InitCodes1), atom_codes('init',InitCodes2),
    (sublist(SCodes,InitCodes1,_,_,_) -> true ; sublist(SCodes,InitCodes2,_,_,_)),
    findall(S,member(dep(SchemaName,S),Deps),[State]), % we should check that State is not Delta or Xi state schema
    add_message(proz,'Did not find Init Schema; assuming following schema to define the initialisation: ',SchemaName).

classify_schema(fschema('Scope',_,ScopeVars,_), AllSchemas, _, _, State, scope) :-
    member(fschema(State,_,StateVars,_),AllSchemas),
    all_members(ScopeVars,StateVars),!.

classify_schema(fschema('ProZ_Goal',_,ScopeVars,_), AllSchemas, _, _, State, goal) :-
    member(fschema(State,_,StateVars,_),AllSchemas),
    all_members(ScopeVars,StateVars),!.

classify_schema(fschema('ProZ_Settings',_,_,_), _AllSchemas, _, _, _State, settings) :- !.

classify_schema(fschema('Invariant',_,InvVars,_), AllSchemas, _, _, State, inv) :-
    member(fschema(State,_,StateVars,_),AllSchemas),
    all_members(InvVars,StateVars),!.

classify_schema(Schema, AllSchemas, Deps, Init, State, op) :-
    Schema = fschema(Id,_,_,_),
    Id \= State, Id \= Init,
    is_operation(AllSchemas, Deps, Schema, State),
    !.

classify_schemas(Schemas,Deps,[cls(init,Init),cls(state,State)|Operations]) :-
    ( classify_init_state(Deps, Init, State) -> true
    ; Deps= [] ->
    add_error(proz,'This Z specification has no schema and cannot be initialised.'),fail
    ;
    %debug:print_quoted(Deps),nl,
    ajoin(['Was not able to identify Z state schema.\n',
    'Please check if there is a schema called Init that\n',
    'references exactly one other schema (the state) in its\n',
    'declaration part.'], Msg),
    add_error(proz,Msg),fail),
    classify_schemas(Schemas, Schemas, Deps, Init, State, Operations).

classify_schemas([], _, _, _, _, []).

classify_schemas([Schema|SRest], AllSchemas, Deps, Init, State, [cls(Class,Id)|CRest]) :-
    classify_schema(Schema, AllSchemas, Deps, Init, State, Class),
    !,Schema = fschema(Id,_,_,_),
    classify_schemas(SRest, AllSchemas, Deps, Init, State, CRest).

classify_schemas([_|SRest], AllSchemas, Deps, Init, State, CRest) :-
    classify_schemas(SRest, AllSchemas, Deps, Init, State, CRest).

clean_up_machine(Machine,Clean) :-
    clean_up_sections([concrete_constants,properties,
    abstract_variables,invariant,
    promoted,initialisation,operation_bodies],
    Machine,Clean).

clean_up_section(Section,In,Out) :-
    select_section_texprs(Section,Old,New,In,Out),
    clean_up_l_with_optimizations(Old,[],New,Section).

clean_up_sections([],M,M).

clean_up_sections([Section|Rest],In,Out) :-
    clean_up_section(Section,In,M),
    clean_up_sections(Rest,M,Out).

construct_any(any(Vars,Types,ZConds,LHS,RHS),Locals1,TExpr) :-
    % Translate the guard to B:
    z_translate(ZConds,BConds),conjunct_predicates(BConds,BCond),
    % Translate local variables to B:
    z_translate_typed_identifiers(Vars,Types,[],Identifiers),
    add_locals([Identifiers],Locals1,Locals),
    % Determine which variables have been used by the guard:
    find_identifier_uses(BCond,Locals,GuardReads),
    % Construct inner substitution:
    construct_substitution(LHS,RHS,Locals,InnerSubst,Writes,SubstReads),
    % Construct ANY or SELECT:
    ord_union(GuardReads,SubstReads,AllReads),
    Info = [modifies(Writes),reads(AllReads)],
    construct_any_or_select(Identifiers,BCond,Info,InnerSubst,AnyOrSelect),
    create_texpr(AnyOrSelect,subst,Info,TExpr).

construct_any_or_select([],BCond,Info,InnerSubst,select([When])) :- !,
    create_texpr(select_when(BCond,InnerSubst),subst,Info,When).

construct_any_or_select(Identifiers,BCond,_Info,InnerSubst,any(Identifiers,BCond,InnerSubst)).

construct_init(Schemas,Classification,Any) :-
    member(cls(init,Init),Classification),
    member(fschema(Init,Def,_,_),Schemas),
   
    member(cls(state,State),Classification),
    member(fschema(State,_,StateVars,StateTypes),Schemas),!,
   
    (translate_initialisation(Def,StateVars,StateTypes,Any) -> true
    ; add_error(proz,'Internal error while translating initialisation'),fail).

construct_operations(Schemas,Classification,Operations) :-
    member(cls(state,State),Classification),
    member(fschema(State,_,StateVars,StateTypes),Schemas),!,
    findall(Op,member(cls(op,Op),Classification),Ops),
    construct_operations2(Ops,Schemas,StateVars,StateTypes,Operations).

construct_operations2([],_,_,_,[]).

construct_operations2([Op|ORest],Schemas,StateVars,StateTypes,[Operation|OpRest]) :-
    member(fschema(Op,Def,Vars,Types),Schemas),!,
    ( translate_operation(Op,Def,Vars,Types,StateVars,StateTypes,Params,ParaTypes,Results,ResultTypes,Any) ->
    Operation = op(Op,Params,Results,Any,ParaTypes,ResultTypes),
    OpArgs =.. [Op|Params],printsilent('Z operation: '),printsilent(OpArgs),nls
    ;
    add_error(proz,'Internal error while translating operation', Op)
    ),
    construct_operations2(ORest,Schemas,StateVars,StateTypes,OpRest).

construct_substitution(LHS,RHS,Locals,TExpr,Writes,Reads) :-
    create_texpr(Subst,subst,[modifies(Writes),reads(Reads)],TExpr),
    construct_substitution2(LHS,RHS,Locals,Subst,Writes,Reads).

construct_substitution2([],[],_Locals,skip,[],[]) :- !.

construct_substitution2(LHS,RHS,Locals,assign(LHS,RHS),Writes,Reads) :-
    get_texpr_ids(LHS,UWrites),sort(UWrites,Writes1),
    ord_subtract(Writes1,Locals,Writes),
    find_identifier_uses_l(RHS,Locals,Reads).

copy_result_vars([],[]).

copy_result_vars([name(Name,Deco)|Rest],[name(Name,NewDeco)|NRest]) :-
    z_counter(Deco,NewDeco),
    copy_result_vars(Rest,NRest).

create_b_identifiers([],[],[]).

create_b_identifiers([Name|Nrest],[Type|Trest],[Id|Irest]) :-
    create_texpr(identifier(Name),Type,[],Id),
    create_b_identifiers(Nrest,Trest,Irest).

create_disjoint(B, let_predicate([D],[Domain],Forall)) :-
    get_texpr_type(B,set(couple(integer,set(ElemType)))),
    create_texpr(identifier('__d'),set(integer),[],D),
    create_texpr(identifier('__i'),integer,[],I),
    create_texpr(identifier('__j'),integer,[],J),
    create_texpr(domain(B),set(integer),[],Domain),
    create_texpr(forall([I,J],Pre,IsDisjunct),pred,[],Forall),
    create_texpr(member(I,D),pred,[],M1),
    create_texpr(member(J,D),pred,[],M2),
    create_texpr(less(I,J),pred,[],Less),
    conjunct_predicates([M1,M2,Less],Pre),
    create_texpr(function(B,I),set(ElemType),[],SetA),
    create_texpr(function(B,J),set(ElemType),[],SetB),
    create_texpr(intersection(SetA,SetB),set(ElemType),[],Intersection),
    create_texpr(empty_set,set(ElemType),[],Empty),
    create_texpr(equal(Intersection,Empty),pred,[],IsDisjunct).

create_enum_elements([],_,[]).

create_enum_elements([Id|IRest],Type,[TId|TRest]) :-
    create_texpr(identifier(Id),Type,[enumerated_set_element],TId ),
    create_enum_elements(IRest,Type,TRest).

create_fields_for_binding([],[]).

create_fields_for_binding([BindingTi|ZRest],
    [field(BField,BExpr)|BRest]) :-
    ti_expr(BindingTi,bindfield(Name,ZExpr)),
    z_translate_identifier(Name,BField),
    z_translate(ZExpr,BExpr),
    create_fields_for_binding(ZRest,BRest).

create_in_sequence(Za,Zb,BExpr) :-
    z_translate(Za,Ba),z_translate(Zb,Bb),
    get_texpr_type(Ba,BSeqType), BSeqType = set(couple(integer,BElemType)),
    ti_type(Za,ZSeqType), ZSeqType = set(tuple([num,ZElemType])),
    translate_basetype(ZElemType,BaseSet),
    create_texpr(identifier('__card'),integer,[],C),
    create_texpr(identifier('__i'),integer,[],I),
    create_texpr(identifier('__la'),BSeqType,[],La),
    create_texpr(identifier('__lb'),BSeqType,[],Lb),
    create_texpr(identifier('__offset'),integer,[],Offset),
    create_texpr(let_predicate([La,Lb],[Ba,Bb],Conjunction),pred,[],TypedBExpr),
    create_texpr(seq(BaseSet),set(BSeqType),[],Sequences),
    create_texpr(member(La,Sequences),pred,[],Asequence),
    create_texpr(member(Lb,Sequences),pred,[],Bsequence),
    create_texpr(card(La),integer,[],CardA),
    create_texpr(card(Lb),integer,[],CardB),
    create_texpr(minus(CardB,CardA),integer,[],Diff),
    create_texpr(let_predicate([C],[Diff],Exists),pred,[],Let),
    create_texpr(integer(0),integer,[],Zero),
    create_texpr(interval(Zero,Diff),integer,[],Interval),
    create_texpr(member(Offset,Interval),pred,[],InInterval),
    create_texpr(conjunct(InInterval,Forall),pred,[],Pred),
    create_texpr(forall([I],InDomain,Equal),pred,[],Forall),
    create_texpr(domain(Ba),integer,[],Domain),
    create_texpr(member(I,Domain),pred,[],InDomain),
    create_texpr(equal(ElemA,ElemB),pred,[],Equal),
    create_texpr(function(Ba,I),BElemType,[],ElemA),
    create_texpr(add(I,Offset),integer,[],I2),
    create_texpr(function(Bb,I2),BElemType,[],ElemB),
    create_exists([Offset],Pred,Exists),
    conjunct_predicates([Asequence,Bsequence,Let],Conjunction),
    get_texpr_expr(TypedBExpr,BExpr).

create_partition(Za,Zb,let_predicate([Seq],[Ba],Conjunct)) :-
    z_translate(Za,Ba),
    z_translate(Zb,Bb),
    % print('Z Partition : '), translate:print_bexpr(Ba),nl, translate:print_bexpr(Bb),nl,
    get_texpr_type(Ba,SeqType),
    get_texpr_type(Bb,set(Type)),
    create_texpr(identifier('__sets'),SeqType,[],Seq),
    create_disjoint(Seq,Disjoint1), create_texpr(Disjoint1,pred,[],Disjoint),
    create_texpr(general_union(Range),set(Type),[],Union),
    create_texpr(range(Seq),set(Type),[],Range),
    create_texpr(equal(Union,Bb),pred,[],Unification),
    create_texpr(conjunct(Disjoint, Unification),pred,[],Conjunct).

create_renamings([],[],[]).

create_renamings([L|LRest],[R|RRest],[rename(name(LN,LD),name(RN,RD))|Rest]) :-
    get_texpr_info(L,LInfos),member(zname(LN,LD),LInfos),
    get_texpr_info(R,RInfos),member(zname(RN,RD),RInfos),!,
    create_renamings(LRest,RRest,Rest).

create_typed_bexpr(symbolic_comprehension_set(Ids, Lhs),BType,Res) :- !,
    Res = b(comprehension_set(Ids, Lhs),BType,[prob_annotation('SYMBOLIC')]).

create_typed_bexpr(BExpr,BType,b(BExpr,BType,[])).

create_z_machine(Filename, TypedSpecification, InitAny, Ops, Schemas, Classification, Settings, BMachine) :-
    create_machine(Filename,Empty),
   
    /* register new data types */
    set_given_sets(TypedSpecification,Empty,MSets),
    set_freetypes(TypedSpecification,MSets,MFreetypes),
   
    /* register initialisation and operations */
    set_init(InitAny,MFreetypes,MInit),
    set_operations(Ops,MInit,MOps),
   
    set_variables(Schemas,Classification,MOps,MVars),
    /* register_scope(Schemas,Classification), */
    set_constants(TypedSpecification,MVars,MConstants),
   
    set_settings(Settings, MConstants, MSettings),
   
    b_global_sets:b_clear_global_set_type_definitions, % TO DO: do the full pre-compiling before cleaning up !?!?
    % cleanup will need to get deferred sets, ...
   
    clean_up_machine(MSettings,BMachine).

exists_to_anys(anys(OldInitAny,OldOps),anys(NewInitAny,NewOps)) :-
    exists_to_anys2(OldInitAny,NewInitAny),
    exists_to_anys_ops(OldOps,NewOps).

exists_to_anys2(any(Vars,Types,[ti(exists(Body,Pred),bool)],LHS,RHS),NewAny) :-
    !,Body=ti(body(_,Wheres),set(schema(ZFields))),
    append(Wheres,[Pred],NPreds1),
    clean_wheret(NPreds1,NPreds),
    % todo: not safe with name clashes
    zfields2b(ZFields,EVars,ETypes),
    append(Vars,EVars,NVars),
    append(Types,ETypes,NTypes),
    exists_to_anys2(any(NVars,NTypes,NPreds,LHS,RHS),NewAny).

exists_to_anys2(Any,Any).

exists_to_anys_ops([],[]).

exists_to_anys_ops([op(Op,Params,Results,OldAny,ParaTypes,ResultTypes)|ORest],
    [op(Op,Params,Results,NewAny,ParaTypes,ResultTypes)|NRest]) :-
    exists_to_anys2(OldAny,NewAny),
    exists_to_anys_ops(ORest,NRest).

extract_cases_from_arms([],[]).

extract_cases_from_arms([ArmTi|RestArms],[case(CaseId,Type)|RestCases]) :-
    ti_expr(ArmTi,arm(Case,SwitchTi)),
    z_translate_identifier(Case,CaseId),
    ti_expr(SwitchTi,Switch),
    ( Switch = just(ExprTi) ->
    ti_type(ExprTi,set(ZType)),internal2b(ZType,Type)
    ;
    Type = constant([CaseId])
    ),
    extract_cases_from_arms(RestArms,RestCases).

extract_constants2([],[],[],[]).

extract_constants2([Def|Rest], Constants, Types, Properties) :-
    extract_constants3(Def, LocalConstants, LocalTypes, ZPropertiesTi),
    !,
    z_translate(ZPropertiesTi,LocalProperties),
    append(LocalConstants, RestConstants, Constants),
    append(LocalTypes, RestTypes, Types),
    append(LocalProperties, RestProperties, Properties),
    extract_constants2(Rest, RestConstants, RestTypes, RestProperties).

extract_constants2([_|Rest], Constants, Types, Properties) :-
    extract_constants2(Rest, Constants, Types, Properties).

extract_constants3(Axdef, Constants, Types, Predicates) :-
    ti_expr(Axdef,axdef(BodyTi)),!,
    extract_btypes(Axdef,Constants,Types),
    ti_expr(BodyTi,body(_,Predicates)).

extract_constants3(PredTi, [], [], [Predicate]) :-
    ti_expr(PredTi, pred(Predicate)).

extract_def_by_equality(ZDef,Name,Type,BExpr) :-
    get_equality(ZDef,ti(ref(name(Name,''),[]),Type),ZExpr),
    z_translate(ZExpr,BExpr1),
    clean_up(BExpr1,[],BExpr).

extract_image_filenames(given(IName),TypedSpecification,Images) :-
    memberchk(ti(namedset(IName,Elements),_),TypedSpecification),
    z_translate_identifiers(Elements,PImages),
    maplist(append_gif,PImages,Images).

filter_preds([],_,_,[]).

filter_preds([Old|ORest],OpPreds,Renamings,NewPreds) :-
    rename_variablest(Old,Renamings,Comparable),
    (exists_equalt(OpPreds,Comparable) ->
    NewPreds = [Old|PRest];
    NewPreds = PRest),
    filter_preds(ORest,OpPreds,Renamings,PRest).

filter_vars_by_deco([],[],_,[],[]).

filter_vars_by_deco([V|VRest],[T|TRest],Deco,Param,ParamTypes) :-
    ( V = name(_,Deco) ->
    (Param,ParamTypes) = ([V|PRest],[T|PTRest])
    ;
    (Param,ParamTypes) = (PRest, PTRest)),
    filter_vars_by_deco(VRest,TRest,Deco,PRest,PTRest).

findtests(Z,Tests) :-
    findall(Name,getschema(Z,Name,_),Schemas),
    findall(test(N,T),(member(T,Schemas),testmark(T,N),member(N,Schemas)),Tests).

fuzzschemas([],[]).

fuzzschemas([Def|Rest],FSchemas) :-
    ( schema_id_body(Def,Id,Body) ->
    FSchemas = [fschema(Id, Body, Vars, Types)|FRest],
    extract_btypes(Def,Vars,Types)
    ;
    FSchemas = FRest),
    fuzzschemas(Rest,FRest).

get_equality(ti(body(_,ZWhere),_),Name,Equal) :-
    !,member(A,ZWhere),get_equality(A,Name,Equal),!.

get_equality(ti(equal(X,Y),_),TName,Equal) :-
    ( X=TName -> Equal=Y
    ; Y=TName -> Equal=X).

get_freetype(Freetype,ArmsTi,freetype(FreetypeId,Cases)) :-
    extract_cases_from_arms(ArmsTi,Cases),
    z_translate_identifier(Freetype,FreetypeId),
    print_message(freetype(FreetypeId)).

get_freetypes([],[]).

get_freetypes([ExprTi|Rest],Freetypes) :-
    ( ti_expr(ExprTi,data(Freetype,Arms)) ->
    get_freetype(Freetype,Arms,BFreetype),
    Freetypes = [BFreetype|FRest]
    ;
    Freetypes = FRest),
    get_freetypes(Rest,FRest).

get_given_sets([],[]).

get_given_sets([Setname|Rest],[BSet|Brest]) :-
    z_translate_identifier(Setname, Setid),
    print_message(given_set(Setid)),
    create_texpr(identifier(Setid),set(global(Setid)),[given_set],BSet),
    get_given_sets(Rest,Brest).

get_named_sets([],[],[]).

get_named_sets([namedset(Setname,Members)|Rest],[BSet|BSetRest],Enumerated) :-
    z_translate_identifier(Setname,Setid),
    create_texpr(identifier(Setid),set(global(Setid)),[given_set],BSet),
    z_translate_identifiers(Members,Memberids),
    create_enum_elements(Memberids,global(Setid),LocalEnumerated),
    append(LocalEnumerated,RestEnumerated,Enumerated),
    get_named_sets(Rest,BSetRest,RestEnumerated).

get_operation(op(Op,Params,Results,Any,ParaTypes,ResultTypes),TOp,OpId) :-
    OpType = op(ResultTypes,ParaTypes),
    create_texpr(identifier(op(Op)),OpType,[],OpId),
    create_b_identifiers(Params,ParaTypes,BParams),
    create_b_identifiers(Results,ResultTypes,BResults),
    create_texpr(operation(OpId,BResults,BParams,Statement),OpType,OpInfo,TOp), % [] == Info ?? extract from Statement ??
    add_locals([BParams,BResults],[],Locals),
    construct_any(Any,Locals,Statement),
    get_texpr_info(Statement,StmtInfo),
    include(is_operation_info,StmtInfo,OpInfo).

get_operations([],[],[]).

get_operations([Operation|ORest],[BOperation|Brest],[Promoted|PromotedRest]) :-
    get_operation(Operation,BOperation,Promoted),
    get_operations(ORest,Brest,PromotedRest).

get_proz_expr_setting(ZDef,_ZVars,_ZTypes,TypedSpecification,animation_function(BAnim,BDefaultAnim,Images)) :-
    ( extract_def_by_equality(ZDef,'animation_function',AFType,BAnim) ->
    (extract_def_by_equality(ZDef,'animation_function_default',DFType,BDefaultAnim) -> true ; BDefaultAnim = none)
    ; extract_def_by_equality(ZDef,'animation_function_default',DFType,BDefaultAnim) ->
    BAnim = none),
    (AFType = DFType -> true ; add_error(proz,'animation_function and animation_function_default should be of the same type')),
    ( AFType = set(tuple([tuple([_,_]),ImageType])) ->
    ( extract_image_filenames(ImageType,TypedSpecification,Images) -> true
    ; add_error(proz,'Unable to map animation function to images'))
    ;
    add_error(proz,'Unexpected type of animation_function'),fail).

get_proz_setting(Schemas,Classification,_Filename,TypedSpecification,Setting) :-
    get_schema_by_class(settings,Classification,Schemas,ZDef,ZVars,ZTypes),
    get_proz_expr_setting(ZDef,ZVars,ZTypes,TypedSpecification,Setting).

get_proz_setting(Schemas,Classification,_Filename,_TypedSpecification,goal(BGoal)) :-
    get_schema_by_class(goal,Classification,Schemas,ZDef,_,_),
    ti_expr(ZDef,body(_,ZGoals)),
    z_translate(ZGoals,BGoals1),
    clean_up_l_wo_optimizations(BGoals1,[],BGoals,schemas),
    conjunct_predicates(BGoals,BGoal).

get_proz_setting(_Schemas,_Classification,_Filename,_TypedSpecification,[]).

get_proz_settings(Schemas,Classification,Filename,TypedSpecification,Settings) :-
    findall(Setting,
    get_proz_setting(Schemas,Classification,Filename,TypedSpecification,Setting),
    Settings).

get_schema_by_class(Cls,Classification,Schemas,Def,Vars,Types) :-
    memberchk(cls(Cls,Name),Classification),
    memberchk(fschema(Name,Def,Vars,Types),Schemas).

get_z_filename(File,Filename) :-
    get_tail_filename(File,Filename1),
    (split_filename(Filename1,Filename,_) -> true ; Filename1 = Filename).

getschema(Z,Name,Def) :- member(sdef(shead(Name,[]),Def),Z).

getschema(Z,Name,Def) :- member(defeq(shead(Name,[]),Def),Z).

getschemat(Z,Name,Def) :- member(ti(sdef(shead(Name,[]),Def),_),Z).

getschemat(Z,Name,Def) :- member(ti(defeq(shead(Name,[]),Def),_),Z).

global_predicates(InitAny,Ops,GlobalPreds) :-
    pred_init(InitAny,InitPreds),
    findall(OpAny,member(op(_,_,_,OpAny,_,_),Ops),OpAnies),
    pred_ops(OpAnies,InitPreds,GlobalPreds).

init_fuzz_mode(Filename,BMachine) :-
    typed_specification(Dependencies,TypedSpecification),
   
    /* initialise the z schemas */
    fuzzschemas(TypedSpecification,Schemas),
    classify_schemas(Schemas, Dependencies, Classification),
   
    /* construct any statements for initialisation and operations */
    construct_init(Schemas,Classification,InitAny),
    construct_operations(Schemas,Classification,Ops),
   
    optimize_anys(anys(InitAny,Ops),anys(InitAny2,Ops2)),
   
    get_proz_settings(Schemas,Classification,Filename,TypedSpecification,Settings),
   
    create_z_machine(Filename,TypedSpecification,InitAny2,Ops2,Schemas,Classification,Settings,BMachine).

is_a_negative_number(ZExpr,N) :-
    ti_expr(ZExpr,apply(Ref,Num)),
    ti_expr(Ref,ref(name('(-)',''),[])),
    is_a_number(Num,N).

is_a_number(ZExpr,N) :-
    ti_expr(ZExpr,number(N)).

is_binary_op(OpName) :- z_binary_op(OpName,_).

is_operation(AllSchemas, Deps, fschema(Id,_,OpVars,_), State) :-
    \+ member(dep(_,Id),Deps), % not included by other schema
    %format('Try operation ~w with OpVars ~w and State schema is ~w~n',[Id,OpVars,State]),
    member(fschema(State,_,StateVars,_),AllSchemas), % get the variables of the state schema
    !,
    decorate_vars(StateVars,'\'',AfterStateVars),
    append(StateVars,AfterStateVars,NeededVars),
    (all_members(NeededVars,OpVars) -> true
    ; %format('~nSchema not recognised as operation: ~w over state variables ~w~n',[Id,StateVars]),
    OpVars \= [],
    list_to_ord_set(StateVars,SVS),
    list_to_ord_set(OpVars,OVS),
    primed_unprimed_ok(OVS,SVS), % check that all variables that are referenced occur with and without prime
    ord_subtract(SVS,OVS,Unchanged),
    formatsilent('Promoting Schema ~w to Z Operation by adding unchanged variables: ~w~n',[Id,Unchanged]),
    % TO DO: in test 1094 for System.fuzz the InitSystem operation is also recognised
    assertz(unchanged_vars_for_partial_zoperation(Id,Unchanged))
).

is_operation_info(modifies(_)).

is_operation_info(reads(_)).

is_symbolic_set_comprehension([TID],_) :-
    get_texpr_id(TID,ID),
    atom_codes(ID,C),
    append("rec__",_,C). % rec__ are special variables introduced in ztransformations:removesexpr2 for Schema fields

is_unary_op(OpName) :- z_unary_operator(OpName,_).

load_and_simplify(File,Tests,Specification) :-
    load_fuzzfile(File),
    get_z_definitions(Z),
    findtests(Z,Tests),
    simplify_untyped(Z,Z2),!,
    global_environment(Z2,_,Z3),!,
    simplify_typed(Z3,Specification).

open_proz_file(File,BMachine) :-
    reset_proz,
    load_fuzzfile(File),
    get_z_filename(File,Filename),
    init_fuzz_mode(Filename,BMachine).

optimize_anys -->
    exists_to_anys,
    optimize_global_predicates.

optimize_global_predicates(anys(InitAny,OldOps),anys(InitAny,NewOps)) :-
    global_predicates(InitAny,OldOps,GlobalPredicates),
    remove_global_predicates(OldOps,GlobalPredicates,NewOps).

pred_init(any(_,_,Preds,Lhs,Rhs),GPreds) :-
    create_renamings(Lhs,Rhs,Renamings),
    rename_variablest(Preds,Renamings,GPreds).

pred_ops([],GPreds,GPreds).

pred_ops([any(_,_,OpPreds,Lhs,Rhs)|ORest],OldPreds,GPreds) :-
    create_renamings(Rhs,Lhs,Renamings),
    filter_preds(OldPreds,OpPreds,Renamings,NewPreds),
    pred_ops(ORest,NewPreds,GPreds).

primed_unprimed_ok([],_).

primed_unprimed_ok([name(ID,''),name(ID,'\'')|T],SVS) :- !,primed_unprimed_ok(T,SVS).

primed_unprimed_ok([NAME|T],SVS) :- \+ ord_member(NAME,SVS),primed_unprimed_ok(T,SVS).

remove_global_predicates(Ops,[],Ops) :- !.

remove_global_predicates(Ops,GlobalPredicates,NewOps) :-
    remove_globalpreds(Ops,GlobalPredicates,NewOps).

remove_globalpreds([],_,[]).

remove_globalpreds([op(Op,Param,Results,Any,ParaTypes,ResultTypes)|ORest],GlobalPredicates,
    [op(Op,Param,Results,NewAny,ParaTypes,ResultTypes)|NRest]) :-
    remove_globalpreds2(Any,GlobalPredicates,NewAny),
    remove_globalpreds(ORest,GlobalPredicates,NRest).

remove_globalpreds2(any(Vars,Types,Old,LHS,RHS),GlobalPredicates,
    any(Vars,Types,New,LHS,RHS)) :-
    remove_globalpreds3(Old,GlobalPredicates,New).

remove_globalpreds3([],_,[]).

remove_globalpreds3([Pred|ORest],GlobalPredicates,New) :-
    ( exists_equalt(GlobalPredicates,Pred) ->
    New = NRest
    ;
    New = [Pred|NRest]),
    remove_globalpreds3(ORest,GlobalPredicates,NRest).

remove_var([],[],_,[],[]) :- !.

remove_var([Var|Orig],[_|OrigTypes],Var,ResVars,ResTypes) :-
    remove_var(Orig,OrigTypes,Var,ResVars,ResTypes).

remove_var([Var|Orig],[Type|OrigTypes],OtherVar,[Var|ResVars],[Type|ResTypes]) :-
    Var \= OtherVar,
    remove_var(Orig,OrigTypes,OtherVar,ResVars,ResTypes).