well_def_analyser

adapt_info(Info,Subs,NewInfo) :- subs_contain_wd_condition(Subs),!,NewInfo=Info.

adapt_info(Info,_,[discharged_wd_po|NewInfo]) :-
    NewInfo=Info, memberchk(contains_wd_condition,Info).

add_modified_vars_to_hyp(Hyps,TLHS,Hyps2) :-
    (get_accessed_vars(TLHS,[],ModifiedVars,_Read) -> true
    ; add_error(well_def_analyser,'Could not obtain modified vars:',TLHS,TLHS), ModifiedVars=[]
    ),
    maplist(construct_typed_var(Hyps),ModifiedVars,TModVars),
    add_new_hyp_variables(Hyps,TModVars,Hyps2).

analyse_invariants_for_machine(UnchangedNr,ProvenNr,UnProvenNr,TotPOsNr,Options) :-
    findall(Proven,prove_invariant_preservation(_Op,_,Proven,Options),Ls),
    count_occurences(Ls,Res),
    (member(proven-ProvenNr,Res) -> true ; ProvenNr=0),
    (member(unchanged-UnchangedNr,Res) -> true ; UnchangedNr=0),
    (member(unproven-UnProvenNr,Res) -> true ; UnProvenNr=0),
    TotPOsNr is UnchangedNr + ProvenNr + UnProvenNr.

analyse_wd_for_expr(TExpr,_,_) :-
    analyse_wd_for_expr(TExpr,_,_,silent).

analyse_wd_for_expr(TExpr,_,_,MsgLevel) :-
    reset_stats,
    formatsilent('WD Proof Obligations:~n',[]),
    %empty_hyps(OriginalHyps),
    push_properties_invariant_hyps([],OriginalHyps),
    list_to_ord_set([create_full_po,create_not_discharged_msg(MsgLevel),discharge_po,ignore_wd_infos
    %,minimize_full_po
    %,prove_with_z3 % comment in to double-check with Z3
    ],Options),
    compute_wd(TExpr,OriginalHyps,Options,PO),
    (silent_mode(on) -> true ; translate:nested_print_bexpr(PO),nl),
    fail.

analyse_wd_for_expr(TExpr,ResStr,AllDischarged,MsgLevel) :-
    formatsilent('----~n',[]),
    print_stats,
    get_discharged_result(ResStr,_,_,AllDischarged),
    empty_hyps(OriginalHyps),
    transform_wd(TExpr,OriginalHyps,[discharge_po],NewTExpr),
    (silent_mode(on) -> true
    ; MsgLevel = silent -> true
    ; format('Annotated formula:~n',[]),
    nested_print_wd_bexpr(NewTExpr)
).

analyse_wd_for_machine(NrDischarged,NrTot,Discharged) :-
    Options = [create_not_discharged_msg(warning),discharge_po,ignore_wd_infos,reorder_conjuncts],
    analyse_wd_for_machine(NrDischarged,NrTot,Discharged,Options).

analyse_wd_for_machine(NrDischarged,NrTot,Discharged,UnsortedOptions) :- reset_stats,
    list_to_ord_set(UnsortedOptions,Options),
    %list_to_ord_set([discharge_po,reorder_conjuncts],Options),
    statistics(walltime,[Start,_]),
    ( get_machine_wd_po(Options,_PO,_),
    fail
    ;
    statistics(walltime,[Stop,_]), Delta is Stop-Start,
    formatsilent('Analysis walltime: ~w ms~n',[Delta]),
    print_stats,
    get_discharged_result(_ResStr,NrDischarged,NrTot,Discharged)
).

analyse_wd_for_machine_with_double_check(NrDischarged,NrTot,Discharged) :-
    Options = [create_not_discharged_msg(warning),discharge_po,ignore_wd_infos,reorder_conjuncts,
    create_full_po, prove_with_z3],
    analyse_wd_for_machine(NrDischarged,NrTot,Discharged,Options).

annotate_wd(TExpr,AnnotatedTExpr) :-
    reset_stats,
    %empty_hyps(EH),
    push_properties_invariant_hyps([],EH),
    Options = [discharge_po],
    transform_wd(TExpr,EH,Options,AnnotatedTExpr),
    print_bexpr_with_wd_info(AnnotatedTExpr).

check_if_po_expected(PO,TExpr,Infos) :-
    ( memberchk(contains_wd_condition,Infos) -> true
    ; get_texpr_info(PO,POInfo), POInfo=[discharged(true,_)|_] -> true
    % Note: Sigma currently gets no contains_wd_condition, but has finiteness WD constraint
    ; add_error(well_def_analyser,'Unexpected WD-PO for expression marked to have no WD condition:',PO,TExpr)
).

check_top_level_wd(conj,Expr,Type,Info,Hyps,Options, _NSubs, NewInfo) :-
    Discharged=false,
    create_top_level_wd_po_conj_like(Expr,Type,Info,Hyps,Options,_PO,Discharged),!, % PO not proven; keep Info as is
    %write(-), flush_output, %print(not_discharged(PO)),nl,
    NewInfo=Info.

check_top_level_wd(other,Expr,Type,Info,Hyps,Options, _NSubs, NewInfo) :-
    Discharged=false,
    create_top_level_wd_po(Expr,Type,Info,Hyps,Options,_PO,Discharged),
    !, % PO not proven; keep Info as is
    %write(-), flush_output, print(not_discharged(_PO)),nl,
    NewInfo=Info.

check_top_level_wd(_,_Expr,_Type,Info,_Hyps,_Options, NSubs, NewInfo) :- % no top-level PO or PO proven
    adapt_info(Info,NSubs,NewInfo).

cnf_negate(implication(A,B),conjunct(A,NotB)) :- create_negation(B,NotB).

cnf_negate(equivalence(A,B),conjunct(b(implication(A,NotB),pred,[]),
    b(implication(NotA,B),pred,[]))) :-
    % not( A <=> B ) <----> A=> not(B) & not(A) => B
    create_negation(A,NotA),
    create_negation(B,NotB).

cnf_negate(disjunct(A,B),conjunct(NotA,NotB)) :- create_negation(A,NotA), create_negation(B,NotB).

cnf_negate(conjunct(A,B),disjunct(NotA,NotB)) :- create_negation(A,NotA), create_negation(B,NotB).

cnf_negate(NegA,A) :- negate_op(NegA,A). % deals with negation(A) -> A, truth->falsity, ...

compute_all_wd_pos(TExpr,OriginalHyps,Options,POs) :-
    findall(PO, compute_wd(TExpr,OriginalHyps,Options,PO), POs).

compute_wd(TExpr,Hypotheses,Options,PO) :-
    syntaxtraversion(TExpr,Expr,Type,Infos,Subs,TNames),
    (ord_member(ignore_wd_infos,Options) -> true ; memberchk(contains_wd_condition,Infos) -> true),
    %(print(Expr),nl ; print(backtrack(Expr)),nl,fail),
    (get_info_labels(Infos,Label) -> ord_add_element(Options,po_label(Label),Opt2) ; Opt2=Options),
    compute_wd_aux(Expr,Type,Infos,Subs,TNames,Hypotheses,Opt2,PO),
    true. %check_if_po_expected(PO,TExpr,Infos).

compute_wd_assign(Hyps,Options,PO,LHS,RHS) :- LHS=b(function(F,X),_,_),
    !,
    % special case for f(X) := RHS
    ( compute_wd(F,Hyps,Options,PO) % ?
    ; compute_wd(X,Hyps,Options,PO)
    ; compute_wd(RHS,Hyps,Options,PO) ).

compute_wd_assign(Hyps,Options,PO,_,RHS) :- % LHS must be an identifier
    compute_wd(RHS,Hyps,Options,PO).

compute_wd_aux(assign(LHSList,RHSList),_,_,_,[],Hypotheses,Options,PO) :-
    !,
    maplist(compute_wd_assign(Hypotheses,Options,PO),LHSList,RHSList).

compute_wd_aux(Expr,_,_,Subs,TNames,Hypotheses,Options,PO) :-
    wd_transparent(Expr),!,
    % cut: only look at WD condition of all sub-arguments
    add_new_hyp_variables(Hypotheses,TNames,Hyps2),
    member(Sub,Subs),
    compute_wd(Sub,Hyps2,Options,PO).

compute_wd_aux(conjunct(A,B),_,_,_,_,Hypotheses,Options,PO) :- !,
    flatten_conjunct(A,B,List), % avoid re-pushing hyps if A is nested conjunct
    compute_wd_conjuncts(List,Hypotheses,Options,PO).

compute_wd_aux(sequence(List),subst,_,_,_,Hypotheses,Options,PO) :- % sequential composition
    !,
    sequence_compute_wd(List,Options,Hypotheses,PO).

compute_wd_aux(while(COND,STMT,INV,VARIANT),_,Infos,_,_,Hypotheses,Options,PO) :- !,
    (member(modifies(VarsModified),Infos) -> debug_println(9,computed_wd_while(VarsModified))
    ; add_error(well_def_analyser,'While does not contain modifies info:',Infos,Infos),
    VarsModified=[]
    ),
    copy_hyp_variables(Hypotheses,VarsModified,Hyps2), % we can no longer make any assumption about the modified vars
    % this corresponds to a universal quantification
    ( compute_wd(INV,Hyps2,Options,PO) % Invariant must hold before and after WHILE loop
    ;
    push_hyp(Hyps2,INV,Options,Hyps3), % add INV to the hypotheses now for the other parts of the WHILE
    (
    compute_wd(COND,Hyps3,Options,PO)
    ;
    compute_wd(VARIANT,Hyps3,Options,PO) % NAT proof rule for While must also hold if P is false according to Atelier-B handbook (otherwise we could have pushed COND onto the stack)
    ;
    push_hyp(Hyps3,COND,Options,Hyps4),
    compute_wd(STMT,Hyps4,Options,PO) % Statement is only executed if COND is true; INV is checked
)
).

compute_wd_aux(Expr,Type,Infos,Subs,TNames,Hypotheses,Options,PO) :-
    wd_like_conjunction(Expr,_,A,B),!,
    add_new_hyp_variables(Hypotheses,TNames,Hyps2),
    ( create_top_level_wd_po_conj_like(Expr,Type,Infos,Hyps2,Options,PO,_Discharged) % e.g., for assertion_expression
    ;
    compute_wd_aux(conjunct(A,B),Type,Infos,Subs,TNames,Hyps2,Options,PO)
).

compute_wd_aux(if_then_else(A,B,C),_,_,_,_,Hypotheses,Options,PO) :- !,
    (compute_wd(A,Hypotheses,Options,PO)
    ;
    push_hyp(Hypotheses,A,Options,NewHyp),
    compute_wd(B,NewHyp,Options,PO)
    ;
    negate_hyp(A,NA),
    push_hyp(Hypotheses,NA,Options,NewHyp),
    compute_wd(C,NewHyp,Options,PO)).

compute_wd_aux(if(List),_,_,_,_,Hypotheses,Options,PO) :- !,
    list_compute_if_elsif_wd(List,Hypotheses,Options,PO).

compute_wd_aux(disjunct(A,B),_,_,_,_,Hypotheses,Options,PO) :- !,
    (compute_wd(A,Hypotheses,Options,PO)
    ;
    negate_hyp(A,NA),
    push_hyp(Hypotheses,NA,Options,NewHyp),
    compute_wd(B,NewHyp,Options,PO)).

compute_wd_aux(general_sum(Ids,P,E),Type,Infos,_,_,Hypotheses,Options,PO) :- !, % SIGMA, real or integer
    ( % first the sub arguments
    add_new_hyp_variables(Hypotheses,Ids,Hyps2),
    ( compute_wd(P,Hyps2,Options,PO)
    ;
    push_hyp(Hyps2,P,Options,NewHyp),
    compute_wd(E,NewHyp,Options,PO)
    )
    ; % now the PO of general_sum itself
    create_top_level_wd_po(general_sum(Ids,P,E),Type,Infos,Hypotheses,Options,PO,_Discharged)
).

compute_wd_aux(general_product(Ids,P,E),Type,Infos,Subs,TNames,Hypotheses,Options,PO) :- !, % PI
    compute_wd_aux(general_sum(Ids,P,E),Type,Infos,Subs,TNames,Hypotheses,Options,PO).

compute_wd_aux(rlevent(_Name,_Sect,_Status,_Params,Guard,Theorems,Actions,VWit,PWit,_Unmod,_AbstractEvents),
    _,_Infos,_Subs,TNames,Hypotheses,Options,PO) :- !,
    add_new_hyp_variables(Hypotheses,TNames,Hyps2),
    % TO DO: treat nested lists VWit,...
    Act = b(parallel(Actions),subst,[]),
    append([[Guard],Theorems,VWit,PWit,[Act]],List),
    list_compute_wd(List,Options,Hyps2,PO).

compute_wd_aux(recursive_let(_ID,Body),_,_,_,_,Hypotheses,Options,PO) :- !,
    % the ID does not have to be added to hypothesis stack !
    compute_wd(Body,Hypotheses,Options,PO).

compute_wd_aux(_,_,_,Subs,TNames,Hypotheses,Options,PO) :-
    add_new_hyp_variables(Hypotheses,TNames,Hyp2),
    % look at WD condition of all sub-arguments independently
    member(Sub,Subs),
    compute_wd(Sub,Hyp2,Options,PO).

compute_wd_aux(Expr,Type,Infos,_,_,Hypotheses,Options,PO) :-
    create_top_level_wd_po(Expr,Type,Infos,Hypotheses,Options,PO,_Discharged).

compute_wd_conjuncts([A|T],Hypotheses,Options,PO) :-
    (compute_wd(A,Hypotheses,Options,PO)
    ;
    T \= [],
    push_hyp(Hypotheses,A,Options,NewHyp),
    compute_wd_conjuncts(T,NewHyp,Options,PO)).

compute_wd_with_reordering(TExpr,Hypotheses,Options,PO) :- \+ ord_member(reorder_conjuncts,Options),!,
    compute_wd(TExpr,Hypotheses,Options,PO).

compute_wd_with_reordering(TExpr,Hypotheses,Options,PO) :-
    conjunction_to_list(TExpr,Conjuncts),
    split_list(is_well_defined_conjunct,Conjuncts,Conj1,Conj2),
    Conj2 \= [], % otherwise no WD condition anyway
    (ord_member(ignore_wd_infos,Options)
    -> append(Conj1,Conj2,Conj12),
    list_compute_wd(Conj12,Options,Hypotheses,PO)
    ; push_hyps(Hypotheses,Conj1,Options,Hyps2), % push the Hypotheses without WD checking
    list_compute_wd(Conj2,Options,Hyps2,PO)
).

construct_eq(TID,E,EqPred) :- safe_create_texpr(equal(TID,E),pred,EqPred).

construct_equal(TID,RenExpr, b(equal(TID,RenExpr),pred,[])) :- get_texpr_id(TID,_),!.

construct_equal(_,_,b(truth,pred,[])). % TO DO: deal with more complex assignments f(i) := E -> f' = f <+ {i|->E}

construct_let_eq_pred(Ids,E,Pred) :-
    (ground(Pred)
    -> conjunction_to_list(Pred,Ps), % enable predicate to be used both ways
    maplist(deconstruct_eq,Ids,E,Ps)
    ; maplist(construct_eq,Ids,E,Ps),
    conjunct_predicates(Ps,Pred)
    ),!.

construct_let_eq_pred(Ids,E,Pred) :- add_internal_error('Call failed: ',construct_let_eq_pred(Ids,E,Pred)),fail.

construct_typed_var(Hyps,ID,b(identifier(ID),Type,[])) :-
    (get_hyp_var_type(ID,Hyps,Type) -> true
    ; add_internal_error('Unknown identifier in hyps:',ID), Type=any).

create_partial_fun_target(A,Target) :-
    % see create_function_check in bvisual2
    get_texpr_type(A,TA), is_set_type(TA,couple(TDom,TRan)),
    create_type_set(TDom,TDT), % we could also use create_maximal_type_set/2
    create_type_set(TRan,TRT),
    safe_create_texpr(partial_function(TDT,TRT),set(TA),[],PF),
    safe_create_texpr(member(A,PF),pred,[],Target).

create_po(H,Target,Infos,Options,PO) :- create_po(H,Target,Infos,Options,PO,_).

create_po(H,Target,Infos,Options,PO,D) :- (var(H) ; H \= hyp_rec(_,_) ; var(Options)),!,
    add_internal_error('Illegal hypotheses or options: ', create_po(H,Target,Infos,Options,PO,D)),fail.

create_po(Hyps,Target,Infos,Options,PO,Discharged) :-
    get_normalized_and_renamed_predicate(Target,Hyps,RenTarget,NT),
    (get_current_po_label(POLabel,Options) -> true ; POLabel = ''),
    (ord_member(print_goal,Options) -> translate:print_bexpr(RenTarget),nl ; true),
    (ord_member(discharge_po,Options)
    -> (%nl,add_message(well_def_analyser,'Proving ',Target,Infos),
    prove_proof_obligation(POLabel,Target,NT,Hyps,ProofTree)
    -> debug_format(19,'PO ~w discharged: ~w~n',[POLabel,ProofTree]), %debug:nl_time,
    inc_counter(discharged_po),
    Discharged=true
    ; inc_counter(not_discharged_po),
    Discharged=false,
    (ord_member_nonvar_chk(create_not_discharged_msg(MsgType),Options)
    -> (prove_po(negation(NT),Hyps,_NegProofTree)
    -> NegProfStatus = ' (goal provably false)'
    % Negation can be proven; i.e., PO cannot be proven unless there is a contradiction in Hyps
    ; NegProfStatus = ''
    ),
    (POLabel = '' -> ajoin(['WD-PO not discharged', NegProfStatus, ': '],Msg)
    ; ajoin(['WD-PO [',POLabel,'] not discharged', NegProfStatus, ': '],Msg)
    ),
    ( MsgType=message -> add_message(well_def_analyser,Msg,Target,Infos)
    ; MsgType=warning -> add_warning(well_def_analyser,Msg,Target,Infos)
    ; MsgType=silent -> formatsilent('~w~w~n',[Msg,Target])
    ; add_error(well_def_analyser,Msg,Target,Infos)
    ),
    debug_format(19,' Normalized Proof Target: ~w~n',[NT])
    %,(debug_level_active_for(5) -> portray_hyps(Hyps) ; true) % hyps can be shown with create_full_po
    ; true
    )
    )
    ; Discharged=false % no discharging of POs
    ),
    extract_pos_infos(Infos,PosInfos),
    (ord_member(create_full_po,Options)
    -> Hyps = hyp_rec(AvlNH,_),
    avl_range(AvlNH,Hyp),
    (Discharged=true, ord_member(minimize_full_po,Options)
    -> minimize_hyps(Hyp,RenTarget,Options,NecHyps) % only show minimum core of hyps necessary for proving
    ; NecHyps=Hyp
    ),
    %length(NecHyps,Len), print(hyps(Len)),nl,
    conjunct_predicates(NecHyps,HypC),
    safe_create_texpr(implication(HypC,RenTarget),pred,[discharged(Discharged,POLabel)|PosInfos],PO),
    %nl,translate:print_bexpr(PO),nl, prove_po_with_atelierb(POLabel,[ml],PO,_),
    % terms:term_hash(PO,Hash), print(Hash),nl,
    %(ord_member(check_ast,Options) -> bsyntaxtree:check_ast(PO) ; true),
    (ord_member(prove_with_z3,Options)
    -> prove_po_with_smt(POLabel,z3,PO,Res),double_check(Discharged,z3,Res) ; true),
    (ord_member(prove_with_ml,Options) -> prove_po_with_atelierb(POLabel,[ml],PO,_) ; true),
    (ord_member(prove_with_pp,Options) -> prove_po_with_atelierb(POLabel,[pp],PO,_) ; true)
    ; RenTarget = b(POE,POT,POI),
    append([discharged(Discharged,POLabel)|PosInfos],POI,POInfos),
    PO = b(POE,POT,POInfos)
).

create_seq1_type_expr(Seq,Sequences) :-
    get_texpr_type(Seq,ST),
    is_set_type(ST,couple(_,TRan)),
    create_type_set(TRan,TRT),
    safe_create_texpr(seq1(TRT),set(ST),[],Sequences).

create_seq_interval_target(S,N,Target) :-
    create_texpr(integer(0),integer,[],Zero),
    safe_create_texpr(size(S),integer,[contains_wd_condition],MaxIdx),
    safe_create_texpr(interval(Zero,MaxIdx),set(integer),[],ValidIdxs),
    safe_create_texpr(member(N,ValidIdxs),pred,[],Target).

create_seq_seq_target(S,Target) :-
    create_seq_seq_type_expr(S,SeqSeq),
    extract_pos_infos(S,PosInfos),
    safe_create_texpr(member(S,SeqSeq),pred,PosInfos,Target).

create_seq_seq_type_expr(SeqSeq,SequencesOfSequences) :-
    get_texpr_type(SeqSeq,SST),
    is_set_type(SST,couple(_,SeqT)), % SeqT = type of the inner sequences
    is_set_type(SeqT,couple(_,TRan)), % TRan is type elements in the inner sequence
    create_type_set(TRan,TRT1),
    safe_create_texpr(seq(TRT1),set(SeqT),[],Sequences),
    safe_create_texpr(seq(Sequences),set(SST),[],SequencesOfSequences).

create_seq_type_expr(Seq,Sequences) :-
    get_texpr_type(Seq,ST),
    is_set_type(ST,couple(_,TRan)),
    create_type_set(TRan,TRT),
    safe_create_texpr(seq(TRT),set(ST),[],Sequences).

create_sequence1_target(S,Target) :-
    create_seq1_type_expr(S,Sequences),
    extract_pos_infos(S,PosInfos),
    safe_create_texpr(member(S,Sequences),pred,PosInfos,Target).

create_sequence_target(S,Target) :-
    create_seq_type_expr(S,Sequences),
    extract_pos_infos(S,PosInfos),
    safe_create_texpr(member(S,Sequences),pred,PosInfos,Target).

create_top_level_wd_po(function(A,B),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    (get_texpr_type(B,TB),
    safe_create_texpr(domain(A),set(TB),[],DomA),
    safe_create_texpr(member(B,DomA),pred,[],Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
    %, tools_printing:print_term_summary(created_function_po(Target,PO))
    ;
    create_partial_fun_target(A,Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
).

create_top_level_wd_po(div(_,B),integer,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_texpr(integer(0),integer,[],Zero),
    safe_create_texpr(not_equal(B,Zero),pred,[],Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(div_real(_,B),real,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_texpr(real('0.0'),real,[],Zero),
    safe_create_texpr(not_equal(B,Zero),pred,[],Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(floored_div(_,B),integer,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_texpr(integer(0),integer,[],Zero),
    safe_create_texpr(not_equal(B,Zero),pred,[],Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(modulo(A,B),integer,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_texpr(integer(0),integer,[],Zero),
    ( safe_create_texpr(greater(B,Zero),pred,[],Target), % does TLA require this to be positive??
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
    ; \+ z_or_tla_minor_mode,
    safe_create_texpr(greater_equal(A,Zero),pred,[],Target), % in B A must be positive
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
).

create_top_level_wd_po(power_of(A,B),integer,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_texpr(integer(0),integer,[],Zero),
    ( AB=B, % B >= 0 must hold in B and Event-B
    safe_create_texpr(greater_equal(AB,Zero),pred,[],Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
    ; eventb_mode, % TO DO: what happens in Z and TLA+?
    AB=A, % A >= 0 must hold in Event-B
    safe_create_texpr(greater_equal(AB,Zero),pred,[],Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
).

create_top_level_wd_po(power_of_real(A,B),real,Infos,Hypotheses,Options,PO,Discharged) :- !,
    % power_of_real has a WD condition, real ** integer has not
    create_texpr(real('0.0'),real,[],Zero),
    ( % A < 0 => real(floor(B))=B
    safe_create_texpr(less_real(A,Zero),pred,[],LHS),
    safe_create_texpr(convert_int_floor(B),integer,[],FloorB),
    safe_create_texpr(convert_real(FloorB),real,[],BB),
    safe_create_texpr(equal(B,BB),pred,[],RHS),
    safe_create_texpr(implication(LHS,RHS),pred,[],Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
    ; % A = 0 => B >= 0
    safe_create_texpr(equal(A,Zero),pred,[],LHS),
    safe_create_texpr(less_equal_real(Zero,B),pred,[],RHS),
    safe_create_texpr(implication(LHS,RHS),pred,[],Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
).

create_top_level_wd_po(iteration(_Rel,Index),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_texpr(integer(0),integer,[],Zero),
    safe_create_texpr(greater_equal(Index,Zero),pred,[],Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(card(S),integer,Infos,Hypotheses,Options,PO,Discharged) :-
    !,
    \+ skip_finite_pos(Options),
    safe_create_texpr(finite(S),pred,[contains_wd_condition],Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(max(S),integer,Infos,Hypotheses,Options,PO,Discharged) :- !,
    get_texpr_type(S,TS),
    safe_create_texpr(not_equal(S,b(empty_set,TS,[])),pred,[],Target1),
    ( skip_finite_pos(Options)
    -> Target = Target1
    ; safe_create_texpr(finite(S),pred,[contains_wd_condition],Target2),
    conjunct_predicates([Target1,Target2],Target) % this is a sufficient condition, not a necessary one
    ),
    % create a single PO, because of use in check_top_level_wd
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(min(S),integer,Infos,Hypotheses,Options,PO,Discharged) :- !,
    get_texpr_type(S,TS),
    safe_create_texpr(not_equal(S,b(empty_set,TS,[])),pred,[],Target1),
    ( skip_finite_pos(Options)
    -> Target = Target1
    ; safe_create_texpr(finite(S),pred,[contains_wd_condition],Target2),
    conjunct_predicates([Target1,Target2],Target) % this is a sufficient condition, not a necessary one
    ),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(max_real(S),real,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_top_level_wd_po(max(S),integer,Infos,Hypotheses,Options,PO,Discharged). % create same PO as for integer max

create_top_level_wd_po(min_real(S),real,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_top_level_wd_po(min(S),integer,Infos,Hypotheses,Options,PO,Discharged). % ditto

create_top_level_wd_po(general_intersection(A),TA,Infos,Hypotheses,Options,PO,Discharged) :- !, % inter
    safe_create_texpr(not_equal(A,b(empty_set,set(TA),[])),pred,[],Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(size(S),integer,Infos,Hypotheses,Options,PO,Discharged) :- !,
    % we do not have to create a finite PO: sequences are by construction finite
    create_sequence_target(S,Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(insert_tail(S,_),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_sequence_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(insert_front(_,S),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    % page 174 of Abrial's book just requires that S is a partial function NATURAL1 +-> TYPE
    create_sequence_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(rev(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_sequence_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(concat(S1,S2),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    (create_sequence_target(S1,Target) ; create_sequence_target(S2,Target)),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(general_concat(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_seq_seq_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(first(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_sequence1_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(last(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_sequence1_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(front(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_sequence1_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(tail(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_sequence1_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(restrict_front(S,N),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    ( create_sequence_target(S,Target) ; create_seq_interval_target(S,N,Target) ),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(restrict_tail(S,N),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    ( create_sequence_target(S,Target) ; create_seq_interval_target(S,N,Target) ),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(mu(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !, % Z MU Operator
    get_texpr_type(S,TS),
    safe_create_texpr(not_equal(S,b(empty_set,TS,[])),pred,[],Target1),
    create_texpr(integer(1),integer,[],One),
    safe_create_texpr(card(S),integer,[contains_wd_condition],CardS),
    safe_create_texpr(less_equal(CardS,One),pred,[],Target2),
    ( skip_finite_pos(Options)
    -> conjunct_predicates([Target1,Target2],Target)
    ; safe_create_texpr(finite(S),pred,[contains_wd_condition],Target3),
    conjunct_predicates([Target1,Target3,Target2],Target)
    ),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(external_function_call('MU',[S]),T,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_top_level_wd_po(mu(S),T,Infos,Hypotheses,Options,PO,Discharged).

create_top_level_wd_po(external_function_call('CHOOSE',[A]),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    get_texpr_type(A,TA),
    safe_create_texpr(not_equal(A,b(empty_set,set(TA),[])),pred,[],Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(external_function_call('SQUASH',[A]),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_partial_fun_target(A,Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(external_function_call(C,_),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    % external_fun_has_wd_condition is true
    get_preference(wd_ignore_external_funs,false),
    create_po(Hypotheses,b(unknown_truth_value(C),pred,[]),Infos,Options,PO,Discharged).

create_top_level_wd_po(external_subst_call(C,_),_,Infos,Hypotheses,Options,PO,Discharged) :- !, % ditto
    get_preference(wd_ignore_external_funs,false),
    create_po(Hypotheses,b(unknown_truth_value(C),pred,[]),Infos,Options,PO,Discharged).

create_top_level_wd_po(external_pred_call(C,_),_,Infos,Hypotheses,Options,PO,Discharged) :- !, % ditto
    get_preference(wd_ignore_external_funs,false),
    create_po(Hypotheses,b(unknown_truth_value(C),pred,[]),Infos,Options,PO,Discharged).

create_top_level_wd_po(general_product(Ids,P,E),Type,Infos,Hypotheses,Options,PO,Discharged) :- !,
    create_top_level_wd_po(general_sum(Ids,P,E),Type,Infos,Hypotheses,Options,PO,Discharged).

create_top_level_wd_po(general_sum(Ids,P,_E),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    \+ skip_finite_pos(Options),
    create_comprehension_set(Ids,P,[],TS),
    safe_create_texpr(finite(TS),pred,[contains_wd_condition],Target),
    create_po(Hypotheses,Target,Infos,Options,PO,Discharged).

create_top_level_wd_po(Expr,T,I,Hypotheses,Options,PO,Discharged) :-
    functor(Expr,F,N),
    ajoin(['Unsupported expression ',F,'/',N,': '],Msg),
    (ord_member_nonvar_chk(create_not_discharged_msg(MsgType),Options)
    -> (MsgType=silent -> true ; add_message(well_def_analyser,Msg,Expr,I)) % we create warning below
    ; known_to_be_unsupported(F,N)
    -> add_warning(well_def_analyser,Msg,Expr,I)
    ; wd_transparent(Expr)
    -> add_error(well_def_analyser,Msg,'transparent operator has no top-level WD condition',I)
    ; (wd_like_conjunction(Expr,_,_,_) ; Expr=disjunct(_,_))
    -> add_error(well_def_analyser,Msg,'operator has no top-level WD condition',I)
    ; add_internal_error(Msg,create_top_level_wd_po(Expr,T,I,_,Options,PO,Discharged))
    ),
    inc_counter(unsupported),
    create_po(Hypotheses,b(unknown_truth_value(F),pred,[wd(Expr)]),I,Options,PO,Discharged).

create_top_level_wd_po_conj_like(assertion_expression(A,_Msg,_),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
    Target = A,
    ord_add_element(Options,po_label('ASSERT'),Options2),
    create_po(Hypotheses,Target,Infos,Options2,PO,Discharged).

create_type_set(boolean,Res) :- !, Res=b(bool_set,set(boolean),[]). % custom rule not necessary

create_type_set(integer,Res) :- !, Res=b(integer_set('INTEGER'),set(integer),[]).

create_type_set(string,Res) :- !, Res=b(string_set,set(string),[]).

create_type_set(Type,Res) :- create_texpr(typeset,set(Type),[],Res).

decompose_po(b(implication(Hyps,Goal),pred,_),Hyps,Goal) :- !.

decompose_po(Goal,b(truth,pred,[]),Goal).

deconstruct_eq(TID,E,b(equal(TID,E),pred,_)).

double_check(true,Solver,solution(S)) :- !,
    add_error(Solver,'Double check of discharged PO failed, counter-example: ',S).

double_check(_,_,_).

find_inconsistent_axiom(LOpt,Axiom,NecHyps) :-
    reset_stats,
    get_fresh_hyps_for_constants(OriginalHyps),
    b_get_properties_from_machine(Properties),
    list_to_ord_set([push_more_hyps|LOpt],Options),
    push_hyp(OriginalHyps,Properties,Options,Hyps1),
    member_in_conjunction(Axiom,Properties),
    (debug_mode(on) -> print(' checking for contradiction with ==> '),translate:print_bexpr(Axiom),nl ; true),
    NegAxiom = b(negation(Axiom),pred,[]),
    prove_sequent_goal(NegAxiom,Hyps1,Options),
    print('INCONSISTENCY FOUND, negation of axiom can be proven: '),
    translate:print_bexpr(Axiom),nl,
    % ord_member(minimize_full_po,Options),
    print('Finding NECESSARY Hypotheses:'),nl,
    minimize_necessary_hyps(Hyps1,NegAxiom,Options,NecHyps),
    (debug_mode(on) -> translate:nested_print_bexpr(NecHyps),nl ; true).

flatten_conjunct(ConjA,ConjB,List) :-
    flatten_conjunct_dl(ConjA,List,[ConjB]). % Tail not flattened; not necessary for performance

flatten_conjunct_dl(b(conjunct(A,B),_,_)) --> !, flatten_conjunct_dl(A), flatten_conjunct_dl(B).

flatten_conjunct_dl(X) --> [X].

get_assigned_id(function(F,_),F).

get_assigned_id(record_field(R,_),R).

get_assigned_ids(b(Expr,_,_),TID) :- get_assigned_id(Expr,F), !,get_assigned_ids(F,TID).

get_assigned_ids(TID,TID).

get_current_po_label(POLabel,Options) :-
    findall(Label,get_label(Label,Options),Labels),
    Labels \= [],
    ajoin_with_sep(Labels,'/',POLabel).

get_discharged_result(ResStr,D,Tot,AllDischarged) :- counter(not_discharged_po,ND),
    counter(discharged_po,D), Tot is ND+D,
    ajoin([D,'/',Tot,' DISCHARGED'],ResStr),
    (ND=0 -> AllDischarged='TRUE' ; AllDischarged='FALSE').

get_fresh_hyps_for_constants(OriginalHyps) :-
    empty_hyps(E),
    b_get_machine_all_constants(Csts),
    add_new_hyp_variables(E,Csts,OriginalHyps).

get_hyps_for_top_level_operations(Options,Hyps) :-
    push_properties_invariant_hyps(Options,Hyps).

get_label(Label,Options) :- member(po_label(L),Options),
    (L = [_|_] -> member(Label,L) ; Label=L).

get_machine_wd_po(LOpt,PO,PO_Name) :-
    reset_stats,
    list_to_ord_set(LOpt,Options),
    b_get_properties_from_machine(Properties),
    % TO DO: move Conjuncts without WD condition to front in first pass
    get_fresh_hyps_for_constants(OriginalHyps),
    ( PO_Name = 'AXM',
    debug_format(19,'Checking WD of PROPERTIES~n',[]),
    ord_add_element(Options,po_label(PO_Name),Opt2),
    compute_wd_with_reordering(Properties,OriginalHyps,Opt2,PO)
   
    %debug:time(well_def_analyser:transform_wd(Properties,OriginalHyps,Opt2,NewProperties)),nl,fail)
   
    ; % TO DO: for transform: only use assertions if assertion checking is on!?
   
    push_hyp(OriginalHyps,Properties,Options,Hyps1),
    b_get_static_assertions_from_machine(StaticAssertions),
   
    ( PO_Name = 'THM-AXM',
    ord_add_element(Options,po_label(PO_Name),Opt2),
    conjunct_predicates(StaticAssertions,SAssPred),
    compute_wd(SAssPred,Hyps1,Opt2,PO)
    ;
    push_hyps(Hyps1,StaticAssertions,Options,Hyps2),
    %portray_hyps(Hyps2),nl,
    b_get_machine_variables(Vars),
    add_new_hyp_variables(Hyps2,Vars,Hyps3),
    b_get_invariant_from_machine(Invariant),
    ( PO_Name = 'INV',
    debug_format(19,'Checking WD of INVARIANT~n',[]),
    ord_add_element(Options,po_label(PO_Name),Opt2),
    compute_wd_with_reordering(Invariant,Hyps3,Opt2,PO)
    ;
    push_hyp(Hyps3,Invariant,Options,Hyps4),
    b_get_dynamic_assertions_from_machine(DynAssertions),
    ( PO_Name = 'THM-INV',
    debug_format(19,'Checking WD of ASSERTIONS~n',[]),
    ord_add_element(Options,po_label(PO_Name),Opt2),
    conjunct_predicates(DynAssertions,AssPred),
    compute_wd(AssPred,Hyps4,Opt2,PO)
    % TO DO: use assertions for operations
    ; push_hyps(Hyps4,DynAssertions,Options,Hyps5),
    (
    b_get_initialisation_from_machine(Body,_OType),
    PO_Name = 'INIT',
    debug_format(19,'Checking WD of INITIALISATION~n',[]),
    ord_add_element(Options,po_label(PO_Name),Opt2),
    compute_wd(Body,Hyps5,Opt2,PO)
    ; b_get_machine_operation(OpName,OpResults,OpFormalParameters,Body,_OType,_TopLevel),
    PO_Name = OpName,
    debug_format(19,'Checking WD of OPERATION ~w~n',[OpName]),
    ord_add_element(Options,po_label(PO_Name),Opt2),
    add_new_hyp_variables(Hyps5,OpFormalParameters,Hyps6),
    add_new_hyp_variables(Hyps6,OpResults,Hyps7),
    compute_wd(Body,Hyps7,Opt2,PO)
    )
    )
    )
    )
    ),
    inc_counter(PO_Name).