predicate_analysis

add_all([],In,In).

add_all([E|Rest],([E|In],Infonodes),Out) :-
    add_all(Rest,(In,Infonodes),Out).

add_all_to_constraint_tree([],_,Tree,Tree).

add_all_to_constraint_tree([Node|NRest],Constraint,InTree,OutTree) :-
    ( avl_change(Node,InTree,Old,InterTree,[Constraint|Old]) ->
    true
    ;
    avl_store(Node,InTree,[Constraint],InterTree)),
    add_all_to_constraint_tree(NRest,Constraint,InterTree,OutTree).

add_existing_constraints(Info,NodeId,In,Out) :-
    memberchk(analysis(Analysis),Info),!,
    findall( constraint([],[Scope:NodeId],constant(Value)),
    member(Scope:Value,Analysis),
    Constraints),
    add_all(Constraints,In,Out).

add_existing_constraints(_Info,_NodeId,In,In).

add_id_basic_constraint(NodeEnv,Identifier,In,Out) :-
    get_texpr_id(Identifier,Id),
    identifier_node_lookup(Id,NodeEnv,_NodeId,Nodes,_Mode),
    add_type_constraints(Identifier,Nodes,In,Out).

add_info([],Old,Old) :- !.

add_info(Info,Old,[analysis(Info)|Old]).

add_node_infos(OldInfo,NodeId,NewInfos,
    (Constraints,[infonode(NodeId,NewInfos,OldInfo)|Out]),
    (Constraints,Out)).

add_type_constraints(TExpr,Nodes,In,Out) :-
    get_texpr_type(TExpr,Type),
    findall(C, type_constraint(Type,Nodes,C), Constraints),
    add_all(Constraints,In,Out).

addition_constraint(A,B,R,[A,B],[R],add).

addition_constraint(A,B,R,[R,B],[A],sub).

addition_constraint(A,B,R,[R,A],[B],sub).

all_nodes_ignored([]).

all_nodes_ignored([_:ignored|Rest]) :-
    all_nodes_ignored(Rest).

append_arguments(Orig,Args,Result) :-
    Orig =.. FA,
    append_arguments2(FA,Args,AllArgs),
    Result =.. AllArgs.

append_arguments2([F|FA],Args,AllArgs) :-
    multi_rule(F),!,
    append([F|FA],[Args],AllArgs).

append_arguments2(FA,Args,AllArgs) :-
    append(FA,Args,AllArgs).

apply_output([],[],Changed,Changed,Values,Values).

apply_output([Node|NRest],[Value|VRest],Cin,Cout,Vin,Vout) :-
    ( Node = _:ignored ->
    Vin = Vinter, Cin=Cinter
    ;
    avl_change(Node,Vin,OldValue,Vinter,NewValue),
    info_conjunct(OldValue,Value,NewValue),
    ( has_more_information(NewValue,OldValue) ->
    Cin = [Node|Cinter]
    ;
    Cin = Cinter)),
    apply_output(NRest,VRest,Cinter,Cout,Vinter,Vout).

apply_start_constraints(Constraints,ChangedNodes,In,Out) :-
    find_start_constraints(Constraints,Start),
    writetodot(1,[],Start,In),
    compute_constraints(Start,ChangedNodes1,[],In,Out),
    list_to_ord_set(ChangedNodes1,ChangedNodes).

call_rule(Rule,InValues,OutValues) :-
    append_arguments(Rule,InValues,CallRule),
    if(rule(CallRule,OutValues), true,
    (add_warning(predicate_analysis,'No rule for: ',CallRule),fail)).

choose_one([],[],[],[]).

choose_one([List1|L1Rest],[List2|L2Rest],[Elem1|E1Rest],[Elem2|E2Rest]) :-
    choose_one2(List1,List2,Elem1,Elem2),
    choose_one(L1Rest,L2Rest,E1Rest,E2Rest).

choose_one2(NodeList,NodeListRO,Elem,ElemRO) :-
    (Elem == (*) -> true ; nth1(N,NodeList,Elem), nth1(N,NodeListRO,ElemRO)).

compset_constraint(left(Scope),NodeLists,Node) :- !,
    last(Begin,_,NodeLists),
    compset_constraint(Scope,Begin,Node).

compset_constraint(right(Scope),NodeLists,Node) :- !,
    last(_,Last,NodeLists),
    compset_constraint(Scope,[Last],Node).

compset_constraint(Scope,[Nodes],Scope:NodeId) :-
    memberchk(Scope:NodeId,Nodes).

compset_constraints(SetNodes,Ids,NodeEnv,Constraints) :-
    lookup_identifier_nodes(Ids,NodeEnv,NodeLists),
    findall( C,
    (SetNode=elem(Scope):_SetNodeId, member(SetNode,SetNodes),
    compset_constraint(Scope,NodeLists,ElemNode),
    member(C, [constraint([SetNode],[ElemNode],id),
    constraint([ElemNode],[SetNode],id)])),
    Constraints).

compute_constraint(constraint(Input,Output,Rule),Cin,Cout,Vin,Vout) :-
    get_input_values(Input,Vin,InValues),
    same_length(Output,OutValues),
    call_rule(Rule,InValues,OutValues),
    apply_output(Output,OutValues,Cin,Cout,Vin,Vout).

compute_constraints([],Changed,Changed,Values,Values).

compute_constraints([Constraint|CRest],Cin,Cout,Vin,Vout) :-
    compute_constraint(Constraint,Cin,Cinter,Vin,Vinter),
    compute_constraints(CRest,Cinter,Cout,Vinter,Vout).

compute_expression(Expr,Type,Result) :-
    empty_state(Empty),
    create_texpr(Expr,Type,[],BExpr),
    b_compute_expression_nowf(BExpr,Empty,Empty,Result,'predicate analysis',0).

compute_integer(Expr,Result) :-
    compute_expression(Expr,integer,int(Result)).

compute_integer_set('INTEGER',-inf,inf).

compute_integer_set('NATURAL',0,inf).

compute_integer_set('NATURAL1',1,inf).

compute_integer_set('INT',Min,Max) :-
    get_preference(minint,Min),
    get_preference(maxint,Max).

compute_integer_set('NAT',0,Max) :-
    get_preference(maxint,Max).

compute_integer_set('NAT1',1,Max) :-
    get_preference(maxint,Max).

compute_maximum_iterations(Nodes,MaxIter) :-
    length(Nodes,N), MaxIter is N*10.

construct_scope([],Scope,Scope).

construct_scope([F|Rest],Base,Scope) :-
    functor(Scope,F,1),arg(1,Scope,Subscope),
    construct_scope(Rest,Base,Subscope).

couple_pathes(TExpr,Path,Constant,TIdentifiers) -->
    {get_texpr_ids(TIdentifiers,Identifiers)},
    couple_pathes2(TExpr,Path,Constant,Identifiers).

couple_pathes2(TExpr,Path,Constant,Identifiers) -->
    {get_texpr_expr(TExpr,Expr)},couple_pathes3(Expr,TExpr,Path,Constant,Identifiers).

couple_pathes3(identifier(Id),_,Path,Constant,Identifiers) -->
    {memberchk(Id,Identifiers),!},[Id-ref(Path,Constant)].

couple_pathes3(couple(A,B),_,Path,Constant,Identifiers) --> !,
    {append(Path,[left],PathA),append(Path,[right],PathB)},
    couple_pathes2(A,PathA,Constant,Identifiers),
    couple_pathes2(B,PathB,Constant,Identifiers).

couple_pathes3(_,TExpr,_Path,_Constant,_Identifiers,_,_) :-
    translate_bexpression(TExpr,String),
    atom_concat('Expected quantified identifier or couple in test specification, but was: ',
    String,Msg),
    throw(junit(Msg)).

create_add_list_constraints([],_Result,Constraints) :- !,Constraints=[].

create_add_list_constraints([Node],Result,Constraints) :- !,
    Constraints = [constraint([Node],[Result],id),constraint([Result],[Node],id)].

create_add_list_constraints(Nodes,Result,Constraints) :- !,
    create_add_list_constraints2(Nodes,Result,Constraints,[]).

create_add_list_constraints2([A,B],Result) --> !,
    findall(constraint(I,O,C),addition_constraint(A,B,Result,I,O,C)).

create_add_list_constraints2([A|Nodes],Result) -->
    {new_node_scope(integer,NodeId,_Nodes)},
    findall(constraint(I,O,C),addition_constraint(A,interval:NodeId,Result,I,O,C)),
    create_add_list_constraints2(Nodes,interval:NodeId).

create_constraint_tree(Constraints,Nodes,Tree) :-
    empty_avl(EmptyTree),
    sort(Constraints,SConstraints), % for SAT_Generator sorting reduces runtime from 22 sec to 18 sec for n=8; TO DO: investigate
    (debug:debug_mode(on) -> length(Constraints,Len), format('Processing ~w constraints~n',[Len]) ; true),
    create_constraint_tree1(SConstraints,[],UnsortedNodes,EmptyTree,Tree),
    (debug:debug_mode(on) -> length(UnsortedNodes,Len2), format('Sorting ~w nodes~n',[Len2]) ; true),
    sort(UnsortedNodes,Nodes),
    (debug:debug_mode(on) -> length(Nodes,Len3), format('Done sorting ~w nodes~n',[Len3]) ; true).

create_constraint_tree1([],Nodes,Nodes,Tree,Tree).

create_constraint_tree1([C|CRest],InNodes,OutNodes,InTree,OutTree) :-
    create_constraint_tree2(C,InNodes,InterNodes,InTree,InterTree),
    create_constraint_tree1(CRest,InterNodes,OutNodes,InterTree,OutTree).

create_constraint_tree2(Constraint,InNodes,OutNodes,InTree,OutTree) :-
    Constraint = constraint(Input,Output,_Rule),
    ( all_nodes_ignored(Output) ->
    InTree = OutTree, InNodes=OutNodes
    ;
    add_all_to_constraint_tree(Input,Constraint,InTree,OutTree),
    %ord_union(Input,InNodes,Nodes),ord_union(Output,Nodes,OutNodes) % this can be very expensive !
    append(Input,InNodes,Nodes), append(Output,Nodes,OutNodes) % just append the nodes and sort them later
).

create_identifier_nodes2([],[],Env,Env,Info,Info).

create_identifier_nodes2([TId|Rest],[NTId|NRest],In,Out,IIn,IOut) :-
    create_identifier_nodes3(TId,NTId,In,Inter,IIn,IInter),
    create_identifier_nodes2(Rest,NRest,Inter,Out,IInter,IOut).

create_identifier_nodes3(TId,NTId,In,Out,IIn,IOut) :-
    get_texpr_id(TId,Id),
    get_texpr_type(TId,Type),
    new_node_scope(Type,NodeId,Nodes),
    avl_store(Id,In,nodes(NodeId,Nodes,rw),Out),
    texpr_add_node_infos(TId,NodeId,NTId,IIn,IOut).

create_info_lookup_table(Values,Nodes) :-
    avl_to_list(Values,ValueList),
    empty_avl(Empty),
    create_info_lookup_table2(ValueList,Empty,Nodes).

create_info_lookup_table2([],Nodes,Nodes).

create_info_lookup_table2([(Scope:Node)-I|Rest],In,Out) :-
    (avl_fetch(Node,In,Old) -> true ; Old = []),
    avl_store(Node,In,[Scope:I|Old],Inter),
    create_info_lookup_table2(Rest,Inter,Out).

create_initial_information(Nodes,InitEnv) :-
    empty_avl(Empty),
    foldl(create_initial_information2,Nodes,Empty,InitEnv).

create_initial_information2(Scope:Node,In,Out) :-
    get_scope_top(Scope,Top),
    avl_store(Scope:Node,In,Top,Out).

create_node_environment(ROIdentifiers,Identifiers,NewIdentifiers,NodeEnv,Infos) :-
    initial_node_env(InitNodeEnv),
    create_identifier_nodes2(ROIdentifiers,_,InitNodeEnv,RONodeEnv1,Infos1,([],[])),
    identifier_nodes_readonly(RONodeEnv1,RONodeEnv),
    create_identifier_nodes2(Identifiers,NewIdentifiers,RONodeEnv,NodeEnv,Infos2,Infos1),
    foldl(add_id_basic_constraint(NodeEnv),Identifiers,Infos,Infos2).

div_rule(Am,AM2,Bm,BM2,MinC,MaxC) :- number(Bm), Bm >= 0,!, % division by positive number
    (Am = -inf -> MinC = -inf
    ; Am < 0, Bm=0 -> MinC = Am % if try_find_abort is true we could set MinC to -inf; here we suppose division by 0 will not occur or not produce a value
    ; Am < 0 -> MinC is Am // Bm % a possible lowest value is obtained by the largest absolute (neg) value
    ; BM2=inf -> MinC is 0 % Am is positive ; we can divide Am by an arbitrarily large number to reach 0
    ; MinC is Am // BM2 % minimum is dividing min of A by maximum of B
    ),
    (AM2 = inf -> MaxC = inf
    ; BM2=inf, AM2<0 -> MinC is 0 % Am is positive ; we can divide Am by an arbitrarily large number to reach 0
    ; AM2 < 0 -> MaxC is AM2 // BM2 % a possible max value is obtained by the smallest absolute (neg) value
    ; Bm=0 -> MaxC = AM2 % if try_find_abort is true we could set MaxC to inf
    ; MaxC is AM2 // Bm % maximum is dividing max of A by min of B
).

div_rule(Am,AM2,_Bm,_BM2,MinC,MaxC) :- number(Am),number(AM2), !, % TODO: improve and check
    M is max(abs(Am),abs(AM2)), % if try_find_abort is true we could divide by 0 and set to -inf .. inf
    MinC is -M, MaxC = M.

div_rule(_,_,_,_,-inf,inf).

do_analysis([],Counter,_MaxIter,_CTree,Values,Values) :-
    !,writetodot(Counter,[],[],Values).

do_analysis([ChangedNode|CNRest],Counter,MaxIter,CTree,In,Out) :-
    Counter < MaxIter,!,
    (avl_fetch(ChangedNode,CTree,Constraints) -> true ; Constraints = []),
    writetodot(Counter,[ChangedNode|CNRest],Constraints,In),
    compute_constraints(Constraints,ChangedNodes1,[],In,Inter),
    list_to_ord_set(ChangedNodes1,ChangedNodes),
    ord_union(CNRest,ChangedNodes,NewChangedNodes),
    Counter2 is Counter+1,
    do_analysis(NewChangedNodes,Counter2,MaxIter,CTree,Inter,Out).

do_analysis(_ChangedNodes,Counter,MaxIter,_CTree,Values,Values) :-
    Counter >= MaxIter.

expected_value_is_top(ExpectedValue,Scope,true) :-
    ground(ExpectedValue),get_scope_top(Scope,ExpectedValue),!.

expected_value_is_top(_ExpectedValue,_Scope,false).

extract(Expr,R,X,Y,Op) :-
    extract_symmetric(Expr,R,X1,Y1,Op1),
    symmetric_constraint(Op1,Op2),
    ( Op=Op1,X=X1,Y=Y1
    ; Op=Op2,X=Y1,Y=X1).

extract(integer(I),R,[],[interval:R],constant(irange(I,I))).

extract(value(IV),R,[],[interval:R],constant(irange(I,I))) :- nonvar(IV), IV = int(I). % TO DO: other vals

extract(interval(interval:A,interval:B),R,[interval:A,interval:B],[card:R],interval_card).

extract(member(S:A,elem(S):B),_,[elem(S):B],[S:A],id).

extract(subset(elem(S):A,elem(S):B),_,[elem(S):B],[elem(S):A],id).

extract(subset_strict(elem(S):A,elem(S):B),_,[elem(S):B],[elem(S):A],id).

extract(add(interval:A,interval:B),R,I,O,C) :- addition_constraint(interval:A,interval:B,interval:R,I,O,C).

extract(minus(interval:A,interval:B),R,I,O,C) :- addition_constraint(interval:B,interval:R,interval:A,I,O,C).

extract(minus(interval:A,interval:B),R,[interval:R,interval:B],[interval:A],add).

extract(minus(interval:A,interval:B),R,[interval:A,interval:R],[interval:B],sub).

extract(multiplication(interval:A,interval:B),R,[interval:A,interval:B],[interval:R],mult).

extract(div(interval:A,interval:B),R,[interval:A,interval:B],[interval:R],divrange).

extract(floored_div(interval:A,interval:B),R,[interval:A,interval:B],[interval:R],divrange). % TO DO: provide proper treatment of floored_div

extract(modulo(*,interval:B),R,[interval:B],[interval:R],lt).

extract(modulo(*,*),R,[],[interval:R],constant(irange(0,inf))).

extract(power_of(interval:Base,interval:Exp),R,[interval:Base,interval:Exp],[interval:R],power).

extract(integer_set(Set),R,[],[elem(interval):R],constant(irange(Min,Max))) :-
    compute_integer_set(Set,Min,Max).

extract(bool_set,R,[],[card:R],constant(irange(2,2))).

extract(pow1_subset(*),R,[],[elem(card):R],constant(irange(1,inf))).

extract(fin_subset(A),R,AL,RL,Op) :- extract(pow_subset(A),R,AL,RL,Op).

extract(fin1_subset(A),R,AL,RL,Op) :- extract(pow1_subset(A),R,AL,RL,Op).

extract(partial_function(A,B),R,AL,RL,Op) :- extract(relations(A,B),R,AL,RL,Op).

extract(total_function(A,B),R,AL,RL,Op) :- extract(relations(A,B),R,AL,RL,Op).

extract(partial_injection(A,B),R,AL,RL,Op) :- extract(partial_function(A,B),R,AL,RL,Op).

extract(total_injection(A,B),R,AL,RL,Op) :- extract(total_function(A,B),R,AL,RL,Op).

extract(partial_surjection(A,B),R,AL,RL,Op) :- extract(partial_function(A,B),R,AL,RL,Op).

extract(total_surjection(A,B),R,AL,RL,Op) :- extract(total_function(A,B),R,AL,RL,Op).

extract(total_bijection(A,B),R,AL,RL,Op) :- extract(total_function(A,B),R,AL,RL,Op).

extract(partial_bijection(A,B),R,AL,RL,Op) :- extract(partial_function(A,B),R,AL,RL,Op).

extract(cartesian_product(card:A,card:B),R,[card:A,card:B],[card:R],mult).

extract(cartesian_product(card:A,card:B),R,[card:R,card:A],[card:B],cart_div).

extract(cartesian_product(card:A,card:B),R,[card:R,card:B],[card:A],cart_div).

extract(set_subtraction(elem(S):A,*),R,[elem(S):A],[elem(S):R],id).

extract(image(elem(right(S)):A,*),R,[elem(right(S)):A],[elem(S):R],id).

extract(intersection(S:A,*),R,I,O,C) :- is_subset_extract(S:R,S:A,I,O,C).

extract(intersection(*,S:B),R,I,O,C) :- is_subset_extract(S:R,S:B,I,O,C).

extract(union(elem(S):A,elem(S):B),R,[elem(S):A,elem(S):B],[elem(S):R],union).

extract(union(S:A,*),R,I,O,C) :- is_subset_extract(S:A,S:R,I,O,C).

extract(union(*,S:B),R,I,O,C) :- is_subset_extract(S:B,S:R,I,O,C).

extract(domain_restriction(S:A,*),R,I,O,C) :- is_subset_extract(left(S):R,S:A,I,O,C). % ALWAYS FAILS !!!!! SOMETHING IS WRONG HERE; TODO: fix

extract(domain_restriction(*,S:B),R,I,O,C) :- is_subset_extract(S:R,S:B,I,O,C).

extract(domain_subtraction(*,S:B),R,I,O,C) :- is_subset_extract(S:R,S:B,I,O,C).

extract(range_restriction(*,S:B),R,I,O,C) :- is_subset_extract(right(S):R,S:B,I,O,C). % ALWAYS FAILS !!!!!

extract(range_restriction(S:A,*),R,I,O,C) :- is_subset_extract(S:R,S:A,I,O,C).

extract(range_subtraction(S:A,*),R,I,O,C) :- is_subset_extract(S:R,S:A,I,O,C).

extract(closure(elem(S):A),R,[elem(S):A],[elem(S):R],id).

extract(composition(elem(left(S)):A,*),R,I,O,C) :- is_subset_extract(elem(left(S)):R,elem(left(S)):A,I,O,C).

extract(composition(*,elem(right(S)):B),R,I,O,C) :- is_subset_extract(elem(right(S)):R,elem(right(S)):B,I,O,C).

extract(function(elem(right(S)):A,*),R,[elem(right(S)):A],[S:R],id).

extract(concat(card:A,card:B),R,I,O,C) :- addition_constraint(card:A,card:B,card:R,I,O,C).

extract(concat(Right:A,Right:B),R,[Right:A,Right:B],[Right:R],union) :- Right=elem(right(_)).

extract(concat(S:A,*),R,I,O,C) :- S=elem(right(_)),is_subset_extract(S:A,S:R,I,O,C).

extract(concat(*,S:B),R,I,O,C) :- S=elem(right(_)),is_subset_extract(S:B,S:R,I,O,C).

extract(concat(LI:A,LI:B),R,[LI:A,LI:B],[LI:R],concat_index) :- LI=elem(left(interval)). % TODO: More rules like addition

extract(seq(*),R,[],[elem(elem(left(interval))):R],constant(irange(1,inf))).

extract(seq1(A),R,I,O,C) :- extract(seq(A),R,I,O,C).

extract(seq1(*),R,[],[elem(card):R],constant(irange(1,inf))).

extract(size(A),R,I,O,C) :- extract(card(A),R,I,O,C).

extract_analysis(Id,Constants,Scope,FoundValue,IsTop) :-
    get_texpr_id(Constant,Id),
    ( memberchk(Constant,Constants) ->
    get_texpr_info(Constant,Info),
    (memberchk(analysis(Analysis),Info) -> true ; Analysis=[]),
    ( memberchk(Scope:FoundValue,Analysis) -> true
    ; IsTop == true -> get_scope_top(Scope,FoundValue) /* no information expected */
    ;
    ajoin(['No analysis information found for constant ',Id,', scope ',Scope],Msg),
    print(extract_analysis(Id,Constants,Scope,FoundValue,IsTop)),nl,
    throw(junit(Msg)))
    ;
    ajoin(['Constant ',Id,' not found'],Msg),
    throw(junit(Msg))).

extract_constraint_for_value(Type,Value,LocalNodes,constraint([],[NodeType:NodeId],Constant)) :-
    extract_constraint_for_value2(Type,Value,NodeType,Constant),
    memberchk(NodeType:NodeId,LocalNodes).

extract_constraint_for_value2(set(_Type),Value,card,Constant) :-
    compute_integer(card(Value),Card),
    Constant = constant(irange(Card,Card)).

extract_constraint_for_value2(set(integer),Value,elem(interval),constant(irange(Min,Max))) :-
    compute_integer(min(Value),Min),
    compute_integer(max(Value),Max).

extract_constraint_for_value2(set(couple(TA,_)),Value,elem(left(DN)),Constant) :-
    compute_expression(domain(Value),set(TA),Dom),
    create_texpr(value(Dom),set(TA),[],BDom),
    extract_constraint_for_value2(set(TA),BDom,elem(DN),Constant).

extract_constraint_for_value2(set(couple(_,TB)),Value,elem(right(RN)),Constant) :-
    compute_expression(range(Value),set(TB),Ran),
    create_texpr(value(Ran),set(TB),[],BRan),
    extract_constraint_for_value2(set(TB),BRan,elem(RN),Constant).

extract_ext_nodes2([],_ElemNodes,[]).

extract_ext_nodes2([Scope|Srest],ElemNodes,Constraints) :-
    extract_ext_nodes3(Scope,ElemNodes,C1),
    append(C1,C2,Constraints),
    extract_ext_nodes2(Srest,ElemNodes,C2).

extract_ext_nodes3(n(Scope,SeqNode),ElemNodes,[Union|Constraints]) :-
    findall(Scope:E,
    ( member(NodeList,ElemNodes), memberchk(Scope:E,NodeList)),
    AllElemNodes),
    Union = constraint(AllElemNodes,[SeqNode],union),
    % for set extensions like { min(0..7) } this generates an empty list AllElemenNodes; TO DO: fix
    findall(constraint([SeqNode],[E],id), member(E,AllElemNodes), Constraints).

extract_extension_nodes([],_NodeEnv,[],[],X,X).

extract_extension_nodes([Elem|Rest],NodeEnv,[ElemNodes|RestNodes],[NElem|NRest],In,Out) :-
    extract_nodes(Elem,NodeEnv,ElemNodes,_Mode,NElem,In,Inter),
    extract_extension_nodes(Rest,NodeEnv,RestNodes,NRest,Inter,Out).

extract_integer(Spec,Value) :-
    ( get_texpr_expr(Spec,integer(Value)) -> true
    ; get_texpr_expr(Spec,unary_minus(Spec2)) ->
    extract_integer(Spec2,Value2),Value is -Value2
    ;
    throw(junit('Integer value expected in right side of assertion'))).

extract_nodes(TExpr,NodeEnv,Nodes,Mode,NTExpr,In,Out) :-
    get_texpr_expr(TExpr,Expr),
    extract_nodes2(Expr,TExpr,NodeEnv,Nodes,Mode,NTExpr,In,Inter),
    add_type_constraints(TExpr,Nodes,Inter,Out),
    store_debug_info(Nodes,TExpr).

extract_nodes2(identifier(Id),TExpr,NodeEnv,Nodes,Mode,NTExpr,In,Out) :- !,
    identifier_node_lookup(Id,NodeEnv,NodeId,Nodes,Mode),!,
    texpr_add_node_infos(TExpr,NodeId,NTExpr,In,Out).

extract_nodes2(conjunct(A,B),TExpr,NodeEnv,[],rw,NTExpr,In,Out) :- !,
    get_texpr_info(TExpr,Infos),
    create_texpr(conjunct(NA,NB),pred,Infos,NTExpr),
    extract_nodes(A,NodeEnv,_NodesA,_ModeA,NA,In,Inter),
    extract_nodes(B,NodeEnv,_NodesB,_ModeB,NB,Inter,Out).

extract_nodes2(forall(Ids,Pre,Cond),TExpr,NodeEnv,[],rw,NTExpr,In,Out) :- !,
    get_texpr_info(TExpr,Info),
    create_texpr(forall(NIds,NPre,NCond),pred,Info,NTExpr),
    identifier_nodes_readonly(NodeEnv,SubEnv1),
    create_identifier_nodes2(Ids,NIds,SubEnv1,SubEnv,In,Inter1),
    extract_nodes(Pre,SubEnv,_NodesPre,_ModePre,NPre,Inter1,Inter2),
    identifier_nodes_readonly(SubEnv,ROEnv),
    extract_nodes(Cond,ROEnv,_NodesCond,_ModeCond,NCond,Inter2,Out).

extract_nodes2(exists(Ids,Cond),TExpr,NodeEnv,[],rw,NTExpr,In,Out) :- !,
    get_texpr_info(TExpr,Info),
    create_texpr(exists(NIds,NCond),pred,Info,NTExpr),
    create_identifier_nodes2(Ids,NIds,NodeEnv,SubEnv,In,Inter1),
    extract_nodes(Cond,SubEnv,_NodesCond,_ModeCond,NCond,Inter1,Out).

extract_nodes2(general_sum([TId],TPred,TExpr),TSigma,NodeEnv,Nodes,rw,NTSigma,In,Out) :- !,
    nodes_for_general_sum_or_mult(mult,TId,TPred,TExpr,TSigma,NodeEnv,Nodes,NTSigma,In,Out).

extract_nodes2(general_product([TId],TPred,TExpr),TSigma,NodeEnv,Nodes,rw,NTSigma,In,Out) :- !,
    nodes_for_general_sum_or_mult(power_rule,TId,TPred,TExpr,TSigma,NodeEnv,Nodes,NTSigma,In,Out).

extract_nodes2(comprehension_set(Ids,Cond),TExpr,NodeEnv,Nodes,rw,NTExpr,In,Out) :- !,
    get_texpr_info(TExpr,Info),
    get_texpr_type(TExpr,Type),
    identifier_nodes_readonly(NodeEnv,SubEnv1),
    create_identifier_nodes2(Ids,NIds,SubEnv1,SubEnv,In,Inter1),
    extract_nodes(Cond,SubEnv,_NodesCond,_ModeCond,NCond,Inter1,Inter2),
    new_node_scope(Type,NodeId,Nodes),
    compset_constraints(Nodes,Ids,SubEnv,Constraints),
    add_all(Constraints,Inter2,Inter3),
    add_node_infos(Info,NodeId,NInfo,Inter3,Out),
    create_texpr(comprehension_set(NIds,NCond),Type,NInfo,NTExpr).

extract_nodes2(set_extension(L),TExpr,NodeEnv,LocalNodes,rw,NTExpr,In,Out) :- !,
    get_texpr_info(TExpr,Info),
    get_texpr_type(TExpr,Type),
    new_node_scope(Type,NodeId,LocalNodes),
    extract_set_extension(L,NodeEnv,LocalNodes,NTSubs,In,Inter1),
    CardNode = card:_, memberchk(CardNode,LocalNodes),
    length(L,MaxCard),
    add_all([constraint([],[CardNode],constant(irange(1,MaxCard)))],
    Inter1,Inter2),
    add_node_infos(Info,NodeId,NewInfo,Inter2,Out),
    create_texpr(set_extension(NTSubs),Type,NewInfo,NTExpr).

extract_nodes2(value(Value),TExpr,NodeEnv,LocalNodes,RW,NTExpr,In,Out) :-
    get_texpr_info(TExpr,Infos), member(was_identifier(ID),Infos),
    \+ ground(Value),!,
    %print(treating_value_as_id(Value,ID)),nl,
    extract_nodes2(identifier(ID),TExpr,NodeEnv,LocalNodes,RW,NTExpr,In,Out).

extract_nodes2(value(Value),TExpr,_NodeEnv,LocalNodes,rw,NTExpr,In,Out) :- nonvar(Value),
    !,
    get_texpr_info(TExpr,Info),
    get_texpr_type(TExpr,Type),
    new_node_scope(Type,NodeId,LocalNodes),
    findall(C,extract_constraint_for_value(Type,TExpr,LocalNodes,C),Constraints),
    add_all(Constraints,In,Inter),
    add_node_infos(Info,NodeId,NewInfo,Inter,Out),
    create_texpr(value(Value),Type,NewInfo,NTExpr).

extract_nodes2(partition(S,Es),TExpr,NodeEnv,[],rw,NTExpr,In,Out) :- !,
    extract_nodes_l([S|Es],NodeEnv,[SNodes|EsNodeLists],_Modes,[NS|NEs],In,Inter1),
    % subset constraints
    findall(constraint(CI,CO,CC),
    (member(Scope:SId,SNodes),
    member(NodeList,EsNodeLists),member(Scope:Elem,NodeList),
    is_subset_extract(Scope:Elem,Scope:SId,CI,CO,CC)),
    SubsetConstraints),
    add_all(SubsetConstraints,Inter1,Inter2),
    % cardinality constraints
    memberchk(card:SNodeId,SNodes),
    findall(card:Elem2,(member(NodeList2,EsNodeLists),member(card:Elem2,NodeList2)),
    CardNodes),
    create_add_list_constraints(CardNodes,card:SNodeId,CardConstraints),
    add_all(CardConstraints,Inter2,Inter3),
    % union constraints
    findall(constraint(ElemNodes,[elem(Scope3):SId3],union),
    ( member(elem(Scope3):SId3,SNodes),
    findall(elem(Scope3):Elem3,
    (member(NodeList3,EsNodeLists),member(elem(Scope3):Elem3,NodeList3)),
    ElemNodes)),
    UnionConstraints),
    add_all(UnionConstraints,Inter3,Out),
    get_texpr_info(TExpr,Info),
    create_texpr(partition(NS,NEs),pred,Info,NTExpr).

extract_nodes2(sequence_extension(L),TExpr,NodeEnv,LocalNodes,rw,NTExpr,In,Out) :- !,
    get_texpr_info(TExpr,Info),
    get_texpr_type(TExpr,Type),
    new_node_scope(Type,NodeId,LocalNodes),
    extract_seq_extension(L,NodeEnv,LocalNodes,NTSubs,In,Inter1),
    CardNode = card:_, memberchk(CardNode,LocalNodes),
    DomNode = elem(left(interval)):_, memberchk(DomNode,LocalNodes),
    length(L,Card),
    add_all([constraint([],[CardNode],constant(irange(Card,Card))),
    constraint([],[DomNode], constant(irange(1, Card)))],
    Inter1,Inter2),
    add_node_infos(Info,NodeId,NewInfo,Inter2,Out),
    create_texpr(sequence_extension(NTSubs),Type,NewInfo,NTExpr).

extract_nodes2(empty_set,TExpr,_NodeEnv,Nodes,rw,NTExpr,In,Out) :- !,
    get_texpr_type(TExpr,Type), new_node_scope(Type,NodeId,Nodes),
    texpr_add_node_infos(TExpr,NodeId,NTExpr,In,Inter),
    get_type_scopes(Type,Scopes),
    findall(constraint([],[elem(S):NodeId],constant(Bottom)),
    (member(elem(S),Scopes),get_scope_bottom(S,Bottom)),
    Bottoms),
    add_all([constraint([],[card:NodeId],constant(irange(0,0)))|Bottoms],Inter,Out).

extract_nodes2(Expr,TExpr,NodeEnv,Nodes,rw,NTExpr,In,Out) :-
    same_functor(Expr,Tmp),
    extract(Tmp,_,_,_,_),!,
    syntaxtransformation(Expr,Subs,[],NSubs,NExpr),
    copy_term((NSubs,NExpr),(NSubsRO,NExprRO)),
    copy_term((NSubs,NExpr),(NewSubs,NewExpr)),
    extract_nodes_l(Subs,NodeEnv,SubNodeLists,Modes,NewSubs,In,Inter),
    ignore_readonly_nodes(Modes,SubNodeLists,SubNodeListsRO),
    get_texpr_info(TExpr,Info),
    get_texpr_type(TExpr,Type),
    new_node_scope(Type,NodeId,Nodes),
    add_node_infos(Info,NodeId,NewInfos,Inter,Inter2),
    create_texpr(NewExpr,Type,NewInfos,NTExpr),
    findall(constraint(InputNodes,OutputNodes,Transition),
    ( extract(NExpr,NodeId,InputNodes,OrigOutputNodes,Transition),
    copy_term(extract(NExpr,NodeId,InputNodes,OrigOutputNodes,Transition),
    extract(NExprRO,NodeId,_,OutputNodes,Transition)),
    choose_one(SubNodeLists,SubNodeListsRO,NSubs,NSubsRO)),
    Constraints),
    %error_manager:print_error_span(TExpr),nl,print(Constraints),nl,
    add_all(Constraints,Inter2,Out).

extract_nodes2(Expr,TExpr,NodeEnv,[],rw,NTExpr,In,Out) :-
    remove_bt(TExpr,_,NExpr,NTExpr),
    syntaxtransformation(Expr,Subs,Names,NSubs,NExpr),
    identifier_nodes_readonly(NodeEnv,SubEnv1),
    create_identifier_nodes2(Names,_NIds,SubEnv1,SubEnv,In,Inter1),!,
    extract_nodes_l(Subs,SubEnv,_SubNodeLists,_Modes,NSubs,Inter1,Out).

extract_nodes2(_,TExpr,_,_,_,_,_,_) :-
    throw(failed_analysis(TExpr)).