graph_iso_nauty

add_nauty_graph([],Exists) :- !,
    prob_start_graph(1), prob_set_colour_of_node(0,0),
    prob_exists_graph(Exists).

add_nauty_graph(SG,Exists) :-
    get_graph_info(SG, _Cols,AVLRange, NrLabelCols,
    Nodes,AVLNodes,NrNodesPerLevel,TotalNodes,TSG),
    %% format('% LabelColors=~w=Levels, Nodes/Level=~w\n',[NrLabelCols,NrNodesPerLevel]),
    % nr_of_node_colours_per_level(NrOfNodeColours),
    % print(prob_get_number_of_colours(NrOfNodeColours)),nl,
    % prob_get_number_of_colours(NrOfNodeColours),
    %% nl,nl,print(prob_start_graph(TotalNodes)),nl,
    prob_start_graph(TotalNodes),
    add_nodes(AVLRange,Nodes,AVLNodes,NrNodesPerLevel,NrLabelCols,TSG),
    %print(prob_exists_graph(Exists)),nl,
    prob_exists_graph(Exists)
.%,print(added_graph(SG,Exists)),nl,nl.

add_nodes(AVLRange,Nodes,AVLNodes,NrNodesPerLevel,TotalNrLabelCols,TSG) :-
    %% print(add_nodes(AVLRange,Nodes,AVLNodes,NrNodesPerLevel,TotalNrLabelCols,TSG)),nl,
    %% portray_avl(AVLNodes),nl,
    total_nr_of_node_colours(MaxNrOfNodeColours),
    get_node(AVLRange,Nodes,AVLNodes,NrNodesPerLevel,
    TotalNrLabelCols,TSG, NrOfLabelColour,Node,ID,Successors),
    (get_colour_of_node(Node,Colour) -> true
    ; add_error(add_nodes,'Call failed: ',get_colour_of_node(Node,Colour)),Colour=0),
    %% print(node(Node,Colour)),nl,
    RealColour is (Colour*TotalNrLabelCols + NrOfLabelColour-1),
    (RealColour >= MaxNrOfNodeColours
    -> (RealColour2 is RealColour mod MaxNrOfNodeColours,
    (colour_overflow -> true
    ; (assertz(colour_overflow),
    add_error(graph_iso_nauty,'Warning: Colour overflow in Nauty Symmetry Library. Some symmetry classes may not be explored!!! Try and increase MAXINT.',RealColour))
    ))
    ; RealColour2 = RealColour
    ), %print(prob_set_colour_of_node(ID,RealColour,nodec(Colour),level(NrOfLabelColour),nroflabelcolours(TotalNrLabelCols))),nl, flush_output(user),
    prob_set_colour_of_node(ID,RealColour2),
    member(DestID,Successors),
    %% print(prob_add_edge(ID,DestID)),nl, flush_output(user),
    prob_add_edge(ID,DestID),
    fail.

add_nodes(_AVLRange,_Nodes,_AVLNodes,_NrNodes,_TotalNrLabelCols,_TSG).

add_state_graph_to_nauty(StateExpression,Exists) :-
    (state_graph(StateExpression,SG)
    -> add_nauty_graph(SG,Exists)
    ; add_error(graph_canon,'Could not compute state_graph: ',StateExpression),fail).

compute_label_colours :-
    retractall(computed_label_colours(_,_,_,_)),
    b_get_machine_variables(TypedVarList),
    b_get_machine_constants(TypedCstList),
    append(TypedCstList,TypedVarList,TL),
    convert_typed_varlist(TL,Cols,_Types),
    retractall(cst_var_colournr(_,_)), retractall(colornr_used(_)),
    generate_col_keylist(TL,3,KL,TotalNrLabelCols), % start at 3, because of $from and $to_el
    % TO DO: check if $from and $to_el are really required given types of variables,constants !
    debug_println(19,label_colours(Cols,KL,TotalNrLabelCols)),
    list_to_avl(['$from'-1,'$to_el'-2|KL],AVLCols), %%print(AVLCols),nl,
    avl_range(AVLCols,AVLRange),
    assertz(computed_label_colours(Cols,AVLCols,AVLRange,TotalNrLabelCols)).

convert_typed_varlist([],[],[]).

convert_typed_varlist([b(identifier(ID),Type,_)|T],[ID|IT],[Type|TT]) :-
    convert_typed_varlist(T,IT,TT).

find_existing_colour(Type,Nr) :- /* check whether an existing colour number can be used for a variable/constant with type Type */
    colornr_used(Nr),
    \+ find_incompatible_type(Type,Nr).

find_incompatible_type(Type,Nr) :- cst_var_colournr(Type2,Nr),
    incompatible_type(Type,Type2).

generate_col_keylist([],N,[],TotalNrLabelCols) :- TotalNrLabelCols is N-1.

generate_col_keylist([b(identifier(ID),Type,_)|T],N,[ID-IDNr|KT],TotalNrLabelCols) :-
    (find_existing_colour(Type,IDNr) -> N1=N /* we can reuse an existing colour nr without conflict */
    ; IDNr=N,N1 is N+1,
    assertz(colornr_used(IDNr)) /* we need to use a new colour number; entailing a new level */
    ), assertz(cst_var_colournr(Type,IDNr)),
    generate_col_keylist(T,N1,KT,TotalNrLabelCols).

get_colour_of_node(X,C) :- var(X), !,
    add_error(get_colour_of_node,'Argument is var: ',get_colour_of_node(X,C)),
    fail.

get_colour_of_node(sg_root,C) :- !, C=0.

get_colour_of_node([],C) :- !, C=1.

get_colour_of_node(pred_true /* bool_true */,Colour) :- !, Colour = 3.

get_colour_of_node(pred_false /* bool_false */,Colour) :- !, Colour = 2.

get_colour_of_node(abs_cn(_,AbsCol),Colour) :- !, Colour is 4 + (AbsCol mod 4). %% TO DO: make more flexible

get_colour_of_node(fd(Nr,Type),Colour) :- !, node_fd_colour(Type,Nr,Colour).

get_colour_of_node(int(Nr),Colour) :- !, colour_for_int0(Max), /* + number of cn's !!! */
    (Nr>=0 -> Colour is Max+Nr*2
    ; Colour is Max-1-(Nr*2)
).

get_colour_of_node(string(S),C) :- !, print(strings_not_supported_in_nauty(S)),nl, C=0.

get_colour_of_node((_A,_B),Col) :- !, Col = 4. /* internal node; just like abs_cn(_,_) */

get_colour_of_node(avl_set(A),Col) :- !, print(avl_set_as_node(A)),nl, Col = 1. /* should be handled in state graph ! */

get_colour_of_node(Node,0) :- print(unknown_node(Node)),nl.

get_graph_info(StateGraph,Cols,AVLRange,TotalNrLabelCols,
    Nodes,AVLNodes,NrNodesPerLevel,TotalNodes,TranslatedStateGraph) :-
    get_label_colours(StateGraph,Cols,AVLCols,AVLRange,TotalNrLabelCols),
    get_nodes(StateGraph,Nodes,AVLNodes),
    length(Nodes,NrNodesPerLevel),
    TotalNodes is NrNodesPerLevel*TotalNrLabelCols,
    translate_state_graph(StateGraph,AVLCols,AVLNodes,TranslatedStateGraph),!.

get_graph_info(StateGraph,_,_,_,_,_,_,_,_) :-
    add_error(graph_iso_nauty,'get_graph_info failed: ',StateGraph),fail.

get_label_colours(SG,Cols,AVLCols,AVLRange,TotalNrLabelCols) :-
    (computed_label_colours(Cols,AVLCols,AVLRange,TotalNrLabelCols) -> true
    ; add_error_fail(graph_iso_nauty,'Could not get label colours',SG)).

get_node(AVLRange,_Nodes,AVLNodes,NrNodesPerLevel,TotalNrLabelCols,TSG,
    NrofLabelColour,Node,NodeID,Successors) :-
    avl_member(Node,AVLNodes,NrN),
    restrict_sg_for_node(TSG,NrN,RestrictedTSG),
    member(NrofLabelColour,AVLRange),
    % print(nr(NrN,NrofLabelColour)),nl,
   
    NodeID is (NrofLabelColour-1)*NrNodesPerLevel+NrN-1,
    (NrofLabelColour>1
    -> N1 is (NrofLabelColour-2)*NrNodesPerLevel+NrN-1, Successors = [N1|S2]
    /* add link to layer above */
    ; Successors=S2),
   
    % S2=S3, /* add no link to layer above; seems to be much slower ! */
    (NrofLabelColour<TotalNrLabelCols
    -> N2 is (NrofLabelColour)*NrNodesPerLevel+NrN-1, S2 = [N2|S3]
    /* add link to layer above */
    ; S2=S3),
   
    findall( DestID, (member((NrN,NrofLabelColour,DestNr),RestrictedTSG),
    DestID is (NrofLabelColour-1)*NrNodesPerLevel+DestNr-1), S3).

get_nodes(SG,Nodes,AVLNodes) :-
    findall(N,(sg_arc(Orig,_C,Dest,SG),(N=Orig;N=Dest)),Ns),
    sort(Ns,Nodes),
    slist_to_avl(Nodes,AVLNodes).

incompatible_type(T,T).

incompatible_type(T,set(T)). %% membership arrow could conflict with = arrow; but only at top-level ??

incompatible_type(set(T),T).

initialise_node_colours :- retractall(nr_of_node_colours_per_level(_)), retractall(node_fd_colour(_,_,_)),
    assertz(nr_of_node_colours_per_level(8)), % start off with number 8 ( last abs_cn colour is 7)
    is_used_b_global_constant(Type,Nr,_Cst),
    retract(nr_of_node_colours_per_level(NC)),
    NC1 is NC+1,
    assertz(nr_of_node_colours_per_level(NC1)),
    assertz(node_fd_colour(Type,Nr,NC)),
    %% print(enum_colour(Type,Nr,NC,_Cst)),nl,
    fail.

initialise_node_colours :-
    b_partially_deferred_set(Type),
    retract(nr_of_node_colours_per_level(NC)),
    NC1 is NC+1,
    assertz(nr_of_node_colours_per_level(NC1)),
    is_unused_b_global_constant(Type,Nr),
    assertz(node_fd_colour(Type,Nr,NC)),
    %% print(partial_enum_colour(Type,Nr,NC)),nl,
    fail.

initialise_node_colours :-
    b_global_deferred_set(Type),
    retract(nr_of_node_colours_per_level(NC)),
    NC1 is NC+1,
    assertz(nr_of_node_colours_per_level(NC1)),
    assertz(node_fd_colour(Type,_,NC)),
    %% print(node_fd_colour(Type,'ANY',NC)),nl,
    fail.

initialise_node_colours :- nr_of_node_colours_per_level(C),
    get_preference(minint,MININT),
    get_preference(maxint,MAXINT),
    CNew is C + MAXINT+1-MININT,
    CNewIncreased is CNew + 14, /* to allow numbers which are greater than MAXINT or smaller than MININT */
    retract(nr_of_node_colours_per_level(_)),
    assertz(nr_of_node_colours_per_level(CNewIncreased)),
    retractall(colour_for_int0(_)),
    assertz(colour_for_int0(C)),
    (debug_mode(off) -> true ; print('Colours initialised: '), print(CNewIncreased),nl, flush_output(user)).

max_nr_of_label_colours(Nr) :-
    b_get_machine_constants(C),
    length(C,NrOfConstants),
    b_get_machine_variables(V),
    length(V,NrOfVars),
    NrOfExtraArrows = 2, /* '$from', '$to_el'*/
    Nr is NrOfConstants+NrOfVars + NrOfExtraArrows.

nauty_clear :-
    retractall(colour_overflow),
    retractall(total_nr_of_node_colours(_)),
    retractall(computed_label_colours(_,_,_,_)).

nauty_init :- %%print(nauty_init),nl,
    initialise_node_colours,
    % nauty_use_module,
    (nauty_initialised -> debug_println(19,prob_free_storage), prob_free_storage
    ; assertz(nauty_initialised) ),
    %% print(graphiso_init),nl,
    catch(graphiso_init, Exception,
    (add_error(nauty_init,'Exception during graphiso_init: ',Exception),
    reraise_important_exception(Exception),fail)),
    nr_of_node_colours_per_level(NrOfNodeColours),
    max_nr_of_label_colours(MaxNrOfLabelColours),
    MaxNrOfNodeColours is NrOfNodeColours * MaxNrOfLabelColours,
    %% print(prob_get_number_of_colours(MaxNrOfNodeColours,NrOfNodeColours)),nl, flush_output(user),
    nauty_clear,
    prob_get_number_of_colours(MaxNrOfNodeColours),
    assertz(total_nr_of_node_colours(MaxNrOfNodeColours)),
    %print(done),nl,flush_output(user),
    compute_label_colours.

nauty_reset :-
    get_preference(symmetry_mode,SymMode),
    ( SymMode=nauty ->
    (nauty_init -> true ; set_preference(symmetry_mode,off))
    ; nauty_clear).

nr_of_node_colours_per_level(5).

restrict_sg_for_node([],_,[]).

restrict_sg_for_node([(Nr,Col,Dest)|T],NodeNr,Res) :-
    (Nr = NodeNr -> Res = [(Nr,Col,Dest)|TR] ; Res=TR),
    restrict_sg_for_node(T,NodeNr,TR).

sg_arc(Orig,ArcColour,Dest, StateGraph) :-
    member((Orig,ArcColour,Dest),StateGraph).

slist_to_avl(List,AVL) :-
    sorted_list_to_keylist(List,1,KL), % assign each element a number, starting at 1
    list_to_avl(KL,AVL).

sorted_list_to_keylist([],_,[]).

sorted_list_to_keylist([H|T],N,[H-N|KT]) :- N1 is N+1, sorted_list_to_keylist(T,N1,KT).

total_nr_of_node_colours(5).

translate_state_graph([],_AVLCols,_AVLNodes,[]).

translate_state_graph([(Node,Col,Dest)|T],AVLCols,AVLNodes,[(NrN,NrC,NrD)|TT]) :-
    avl_member(Node,AVLNodes,NrN),
    (avl_member(Col,AVLCols,NrC) -> true
    ; add_error(translate_state_graph,'Unknown Label: ',Col:AVLCols),NrC=1),
    avl_member(Dest,AVLNodes,NrD),
    translate_state_graph(T,AVLCols,AVLNodes,TT).