MODULE ClassTwo EXPORTS Main;

IMPORT Wr, Thread, Fmt, Random, Word;
FROM Stdio IMPORT stderr;
FROM JMGraph IMPORT 
  N, M, TN, D, Msg, WriteGraph,
  Vertex, Subgraph, Edge, Graph;

CONST
  MaxGraphs = 10;        (* Max number of graphs to output *)

PROCEDURE DoIt() =
  VAR coins: Random.T := Random.New();
  BEGIN
    Msg("num vertices = " & Fmt.Int(N));
    Msg("max degree = " & Fmt.Int(D));
    EnumSmoothClassTwoGraphs(coins);
    Msg("Done.");
  END DoIt;
  
PROCEDURE IsClassOne(READONLY g: Graph): BOOLEAN =
  (* TRUE iff the edges of g can be colored with only D colors. *)
  
  VAR edge: ARRAY [0..M-1] OF Edge;
      color: ARRAY [0..M-1] OF [0..D-1];
      nedges: CARDINAL;
      used: ARRAY Vertex OF ARRAY [0..D-1] OF BOOLEAN; (* Colors used at each vertex *)
  
  PROCEDURE CollectEdges() =
    BEGIN
      nedges := 0;
      FOR u := 0 TO N-2 DO 
       FOR v := u+1 TO N-1 DO 
         IF g[u,v] THEN 
           edge[nedges] := Edge{u,v}; 
           INC(nedges)
         END
       END
      END
    END CollectEdges;
    
  PROCEDURE ClearUsedTable() =
    BEGIN
      FOR u := 0 TO N-1 DO
        FOR c := 0 TO D-1 DO 
          used[u,c] := FALSE
        END
      END
    END ClearUsedTable;

  PROCEDURE DColorable(k: CARDINAL): BOOLEAN =
    (* 
      TRUE if edges edge[k..nedges-1] can be colored using only D colors,
      given the current colors of edge[0..k-1]
    *)
    BEGIN
      IF k >= nedges THEN
        (* Msc('*'); *)
        RETURN TRUE
      ELSE
        (* Msc('('); *)
        WITH 
          e = edge[k],
          u = e.org,
          v = e.dst
        DO
          <* ASSERT g[u,v] *>
          WITH usu = used[u], usv = used[v] DO
            FOR c := 0 TO D-1 DO
              IF NOT (usu[c] OR usv[c]) THEN
                color[k] := c;
                (* Msc(VAL(ORD('0') + c, CHAR)); *)
                used[u,c] := TRUE;
                used[v,c] := TRUE;
                IF DColorable(k+1) THEN
                  (* Msc(')'); *)
                  RETURN TRUE
                END;
                used[u,c] := FALSE;
                used[v,c] := FALSE;
              END
            END;
          END
        END;
        (* Msc(')'); *)
        RETURN FALSE
      END
    END DColorable;
  
  BEGIN
    (* Msg("  coloring edges: ", FALSE); *)
    CollectEdges();
    ClearUsedTable();
    WITH
      r = DColorable(0)
    DO
      (* Msc(' '); *)
      (* IF r THEN Msg(" - class one") ELSE Msg(" - class two") END; *)
      RETURN r
    END
  END IsClassOne;
  
PROCEDURE EnumSmoothClassTwoGraphs (coins: Random.T) =

  VAR 
    (* Adjacency matrix: *)
    g: Graph;
    (* Invariant: 
         /\ g[u,v] = TRUE iff there is an edge from vertex u to vertex v
         /\ g[u,u] = FALSE
         /\ g[u,v] = g[v,u]
    *)

    (* Degree table: *)
    deg: ARRAY Vertex OF CARDINAL;     
    (* Invariant: 
        /\ deg[v] = SUM_{u IN [0..NV-1]} g[u,v]
        /\ deg[v] <= D
    *)

    (* Induced subgraph tables: *)
    ne: ARRAY Subgraph OF CARDINAL;   (* Current number of edges in subgraph s *)
    nv: ARRAY Subgraph OF CARDINAL;   (* Number of vertices in subgraph s *)
    maxe: ARRAY Subgraph OF CARDINAL; (* Max num of edges allowed in subgraph s *) 
    (* 
      "Subgraph s" means the subgraph of g induced by the set of vertices
      whose indices are the bit positions of the "1" bits in the binary 
      representation of integer s (with bit 0 in the units place).  Thus,
      for example, subgraph 0 is the empty graph, and subgraph TN-1 is
      g itself.

      Note that nv[s] is simply the number of "1" bits in the binary representation
      of s.

      Invariant:
        s SUBSETOF [0..N-1] ==> 
          /\ nv[s] = CARDINALITY(s)
          /\ maxe[s] = D * (nv[s] DIV 2)
          /\ ne[s] = SUM_{u,v IN s} g[u,v]
          /\ ne[s] <= maxe[s]
    *)

    (* Candidate edge list: *)
    edge: ARRAY [0..M-1] OF Edge;
    (* Invariant: 
        /\ 0 <= edge[k].org < edge[k].dst < N
        /\ (edge[i] = edge[j]) = (i = j)
    *)

  PROCEDURE InitializeGraph() =
    (* Initializes g  deg, ne, nv, maxe, edge: *)
    VAR k: CARDINAL := 0;
    BEGIN
      FOR u := 0 TO N-1 DO
        g[u,u] := FALSE;
        deg[u] := 0;
        FOR v := u+1 TO N-1 DO
          g[u,v] := FALSE; g[v,u] := FALSE;
          edge[k] := Edge{u,v};
          INC(k);
        END
      END;
      <* ASSERT k = M *>
      (* Initialize subgraph tables: *)
      nv[0] := 0;  ne[0] := 0; maxe[0] := 0;
      FOR s := 1 TO TN-1 DO 
        nv[s] := nv[s DIV 2] + (s MOD 2);
        ne[s] := 0;
        maxe[s] := D * (nv[s] DIV 2);
      END;
    END InitializeGraph;
    
  PROCEDURE IsEdgeGood(u, v: Vertex): BOOLEAN =
    (*
      TRUE if adding the missing edge (u,v) to the graph g
      will neither cause deg[v] to exceed D for any vertex v, nor
      cause ne[s] to exceed maxe[s] for any vertex subset s.
    *)
    BEGIN
      <* ASSERT u < v *>
      <* ASSERT NOT g[u,v] *>
      (* Msg("  considering edge " & FE(u, v) & " ... ", FALSE); *)
      IF deg[u] = D THEN 
        (* Msg("bad - vertex " & FV(u) & " saturated"); *)
        RETURN FALSE
      END;
      IF deg[v] = D THEN 
        (* Msg("bad - vertex " & FV(v) & " saturated"); *)
        RETURN FALSE
      END;
      WITH 
        muv = Word.Or(Word.Shift(1, u), Word.Shift(1, v))
      DO
        FOR s := 0 TO TN-1 DO 
          IF Word.And(muv, s) = muv AND ne[s] = maxe[s] THEN 
            (* Msg("bad - subgraph " & FS(s) & " full"); *)
            RETURN FALSE
          END
        END
      END;
      (* Msg("good"); *)
      RETURN TRUE
    END IsEdgeGood;

  PROCEDURE AddEdge(u, v: Vertex) =
    BEGIN
      <* ASSERT u < v AND v < N *>
      <* ASSERT (NOT g[u, v]) AND (NOT g[v,u]) *>
      g[u,v] := TRUE; g[v,u] := TRUE;
      (* Msg("  added edge " & FE(u, v)); *)
      <* ASSERT deg[u] < D *>
      INC(deg[u]);
      <* ASSERT deg[v] < D *>
      INC(deg[v]);
      WITH 
        muv = Word.Or(Word.Shift(1, u), Word.Shift(1, v))
      DO
        FOR s := 0 TO TN-1 DO 
          IF Word.And(muv, s) = muv THEN 
            <* ASSERT ne[s] < maxe[s] *>
            INC(ne[s])
          END
        END
      END
    END AddEdge;

  PROCEDURE RemoveEdge(u, v: Vertex) =
    BEGIN
      <* ASSERT u < v AND v < N *>
      (* Msg("  removed edge " & FE(u, v)); *)
      WITH 
        muv = Word.Or(Word.Shift(1, u), Word.Shift(1, v))
      DO
        FOR s := 0 TO TN-1 DO 
          IF Word.And(muv, s) = muv THEN 
            <* ASSERT ne[s] > 0 *>
            DEC(ne[s])
          END
        END
      END;
      <* ASSERT deg[u] > 0 *>
      DEC(deg[u]);
      <* ASSERT deg[v] > 0 *>
      DEC(deg[v]);
      <* ASSERT g[u, v] AND g[v,u] *>
      g[u,v] := FALSE; g[v,u] := FALSE;
    END RemoveEdge;

  PROCEDURE MaxDegree(): CARDINAL =
    VAR d := 0;
    BEGIN
      FOR u := 0 TO N-1 DO IF deg[u] > d THEN d := deg[u] END END;
      RETURN d
    END MaxDegree;
    
  VAR ngtried: CARDINAL := 0; (* Number of maximal D-NSO graphs tested *)
      ngfound: CARDINAL := 0; (* Number of D-NSO D-M C2 graphs found *)
    
  PROCEDURE DoEnum(k: CARDINAL) =
    (*
      Enumerates all Non-D-Subgraph-Overfull graphs (D-NSO)
      with max degree = D (D-M) which are class 2 (C2), and
      which have the status of edges edge[0..k-1] fixed as 
      specified by g.
    *)
    BEGIN
      IF ngfound >= MaxGraphs THEN
        RETURN 
      ELSIF k >= M THEN
        (* Msg("--------------------------------------------------------------"); *)
        INC(ngtried);
        Msg("graph " & Fmt.Int(ngtried) & ": ", FALSE);
        IF MaxDegree() < D THEN
          Msg("max degree too low")
        ELSIF IsClassOne(g) THEN
          Msg("class one")
        ELSE
          Msg("class two", FALSE);
          INC(ngfound);
          WriteGraph(g, ngfound);
        END;
        (* Msg("--------------------------------------------------------------"); *)
      ELSE
        (* Pick a random non-fixed edge: *)
        WITH i = Random.Subrange(coins, k, M-1) DO
          VAR t := edge[k]; BEGIN edge[k] := edge[i]; edge[i] := t END
        END;
        WITH e = edge[k], u = e.org, v = e.dst DO
          IF IsEdgeGood(u,v) THEN
            (* Enumerate graphs WITH edge[k]: *)
            AddEdge(u, v);
            DoEnum(k+1);
            RemoveEdge(u, v);
          END;
          (* Enumerate graphs WITHOUT edge[k]: *)
          DoEnum(k+1)
        END
      END
    END DoEnum;    

  BEGIN
    InitializeGraph();
    DoEnum(0)
  END EnumSmoothClassTwoGraphs;

<*UNUSED*>
PROCEDURE Msc(c: CHAR) =
  <* FATAL Wr.Failure, Thread.Alerted *>
  BEGIN
    Wr.PutChar(stderr, c);
  END Msc;

BEGIN
  DoIt()
END ClassTwo.