#include "semcheck.h"

//#define DEBUG

int SCC_MAX(DemNumber* n1, DemNumber *n2)
{
   if (n1->get_val() > n2->get_val())
      return(n1->get_val());
   else
      return(n2->get_val());
 }

void Cd_graphs::SCC(Cd_graphs *iCd_graphs)
{

   this->SCC_INIT_STRUCT();
   cd_graphs->SCC();
   this->SCC_COLLECT(iCd_graphs);
 }


void Cd_graph_List::SCC()
{
   Cd_graph_list_iterator next_arg(*this);
   Cd_graph_ each_arg;

   while (each_arg = next_arg())
      each_arg->SCC();
}

void Cd_graph::SCCStart()
{
   this->SCC_INIT_STRUCT();
   this->SCC();
}

void Cd_graph::SCC()
{
   adjacencies->SCC(dfs_n, current_component, stack);
}


void Adjacency_Nlist::SCC(DemNumber *dfs_n,
                         DemNumber *current_component,
                         Adjacency_List *stack)
{
   Adjacency_list_iterator next_arg(*this);
   Adjacency_ each_arg;

   while (each_arg = next_arg())
      each_arg->SCC(dfs_n, current_component, stack, this);
 }


void Adjacency::SCC(DemNumber *dfs_n,
                    DemNumber *current_component,
                    Adjacency_List *stack,
                    Adjacency_Nlist *adjacencies)
{
   Vertex_Comma_list *iVertex_Comma_list = new Vertex_Comma_list();
   Adjacency *iAdjacency;
   DemNumber *wDFS;
   int idfs = dfs_n->get_val();
   int curr_comp;

   if (dfs->get_val() == 0) {
      dfs->rset_val(idfs);
      high->rset_val(idfs--);
      dfs_n->rset_val(idfs);
      stack->insert(this);
   
      ns->SCC_GET_NS_VERTEX(iVertex_Comma_list);

#ifdef DEBUG
      cout << "ADJACENCY: ";
      this->pp();
      cout << "\n";
#endif

      while (iVertex_Comma_list->list_length())
         if(iAdjacency=adjacencies->SCC_GET_ADJACENCY(iVertex_Comma_list->get())) {
            wDFS = iAdjacency->get_dfs();
            if (wDFS->get_val() == 0) {
               iAdjacency->SCC(dfs_n, current_component, stack, adjacencies);
               high->rset_val(SCC_MAX(high,iAdjacency->get_high()));
               }
            else if ((wDFS->get_val() > dfs->get_val()) &&
                    ((iAdjacency->get_scc())->get_val() == 0))
            high->rset_val(SCC_MAX(high,wDFS));
	    }
         
      if (high->g_equal(dfs)) {
         curr_comp = current_component->get_val();
         current_component->rset_val(++curr_comp);
         do {
            iAdjacency = stack->get();
            (iAdjacency->get_scc())->rset_val(curr_comp);
            }
            while(!(this->SCC_VERTEX_EQUAL(iAdjacency->get_source())));
         }
      }
   }

void Cd_graphs::SCC_INIT_STRUCT()
{
   cd_graphs->SCC_INIT_STRUCT();
 }


void Cd_graph_List::SCC_INIT_STRUCT()
{
   Cd_graph_list_iterator next_arg(*this);
   Cd_graph_ each_arg;

   while (each_arg = next_arg())
      each_arg->SCC_INIT_STRUCT();
 }


void Cd_graph::SCC_INIT_STRUCT()
{
   this->rset_dfs_n(new DemNumber(adjacencies->list_length()));
   this->rset_current_component(new DemNumber(0));
   stack = new Adjacency_List();

   adjacencies->SCC_INIT_STRUCT();
 }


void Adjacency_Nlist::SCC_INIT_STRUCT()
{
   Adjacency_list_iterator next_arg(*this);
   Adjacency_ each_arg;

   while (each_arg = next_arg())
      each_arg->SCC_INIT_STRUCT();
 }


void Adjacency::SCC_INIT_STRUCT()
{
   this->rset_dfs(new DemNumber(0));
   this->rset_high(new DemNumber(0));
   this->rset_scc(new DemNumber(0));
 }

void Neighbors::SCC_GET_NS_VERTEX(Vertex_Comma_list *iVertex_Comma_list)
{
} 

//Neighbors_wc:
void Neighbors_wc::SCC_GET_NS_VERTEX(Vertex_Comma_list *iVertex_Comma_list)
{
   construct_ns->SCC_GET_NS_VERTEX(iVertex_Comma_list);
 }

//Repetit_n:
void Repetit_n::SCC_GET_NS_VERTEX(Vertex_Comma_list *iVertex_Comma_list)
{
   sandwiched->SCC_GET_NS_VERTEX(iVertex_Comma_list);
 }

void Kernel_Sandwich::SCC_GET_NS_VERTEX(Vertex_Comma_list *iVertex_Comma_list)
{
   inner->SCC_GET_NS_VERTEX(iVertex_Comma_list);
 }

void Kernel::SCC_GET_NS_VERTEX(Vertex_Comma_list *iVertex_Comma_list)
{
   if (nonempty)
      iVertex_Comma_list->append(nonempty->SCC_GET_NS_VERTEX());
 }


// Alternation:

void Alternat_ns::SCC_GET_NS_VERTEX(Vertex_Comma_list *iVertex_Comma_list)
{
   Any_vertex_List *construct_ns;

   alternat_ns->SCC_GET_NS_VERTEX(iVertex_Comma_list);
   if (construct_ns = this->get_construct_ns())
      construct_ns->SCC_GET_NS_VERTEX(iVertex_Comma_list);
 }

void Term_Bar_list::SCC_GET_NS_VERTEX(Vertex_Comma_list *iVertex_Comma_list)
{
   Term_list_iterator next_arg(*this);
   Term_ each_arg;

   while (each_arg = next_arg())
      iVertex_Comma_list->append(each_arg->SCC_GET_NS_VERTEX());
 }


//Construction:
void Any_vertex_List::SCC_GET_NS_VERTEX(Vertex_Comma_list *iVertex_Comma_list)
{
   Any_vertex_list_iterator next_arg(*this);
   Any_vertex_ each_arg;
   Vertex *iVertex;

   while (each_arg = next_arg())
      if (iVertex = each_arg->SCC_GET_NS_VERTEX())
         iVertex_Comma_list->append(iVertex);
 }


Vertex *Any_vertex::SCC_GET_NS_VERTEX()
{
    return NULL;
}

Vertex *Opt_labeled_term::SCC_GET_NS_VERTEX()
{
   return(this->get_vertex()->SCC_GET_NS_VERTEX());
 }

Vertex *Term::SCC_GET_NS_VERTEX()
{
   return(vertex);
 }

Adjacency *Adjacency_Nlist::SCC_GET_ADJACENCY(Vertex *iVertex)
{
   Adjacency_list_iterator next_arg(*this);
   Adjacency_ each_arg;

   while (each_arg = next_arg())
      if (each_arg->SCC_VERTEX_EQUAL(iVertex))
         return(each_arg);

   return((Adjacency *)NULL);
 }


int Adjacency::SCC_VERTEX_EQUAL(Vertex *iVertex)
{
   return(source->SCC_VERTEX_EQUAL(iVertex));
 }


int Vertex::SCC_VERTEX_EQUAL(Vertex *iVertex)
{
   if (!iVertex) return 0;
   if (!this->get_vertex_name())
   {
       cout << "\n this Vertex name : NULL !" << endl;
       exit(-1);
   }
   if (!iVertex->get_vertex_name())
   {
       cout << "\n iVertex name : NULL !" << endl;
       exit(-1);
   }
   return((this->get_vertex_name())->g_equal(iVertex->get_vertex_name()));
 }

void Cd_graphs::SCC_COLLECT(Cd_graphs *iCd_graphs)
{
   iCd_graphs->rset_cd_graphs(cd_graphs->SCC_COLLECT());
 }


Cd_graph_List *Cd_graph_List::SCC_COLLECT()
{
   Cd_graph_list_iterator next_arg(*this);
   Cd_graph_ each_arg;
   Cd_graph_List *iCd_graph_List = new Cd_graph_List();

   (each_arg = next_arg())->SCC_COLLECT(iCd_graph_List);

   return(iCd_graph_List);
 }


void Cd_graph::SCC_COLLECT(Cd_graph_List *iCd_graph_List)
{
   int i, curr_comp = current_component->get_val();
   
   for (i = 1; i <= curr_comp; i++)
   {
      Cd_graph * iCd_graph = new Cd_graph();
      iCd_graph->set_adjacencies(adjacencies->SCC_COLLECT(i));
      iCd_graph_List->append(iCd_graph);
   }
 }


Adjacency_Nlist *Adjacency_Nlist::SCC_COLLECT(int iSCC)
{
   Adjacency_list_iterator next_arg(*this);
   Adjacency_ each_arg;
   Adjacency_Nlist *iAdjacency_Nlist = new Adjacency_Nlist();

   while (each_arg = next_arg())
      if (each_arg->SCC_COLLECT(iSCC))
         iAdjacency_Nlist->append(each_arg);

   return (iAdjacency_Nlist);
 }


int Adjacency::SCC_COLLECT(int iSCC)
{
   if (iSCC == scc->get_val())
      return(1);
   else
      return(0);
 }

void Cd_graphs::SCC_PRINT()
{
   cd_graphs->SCC_PRINT();
 }

void Cd_graph_List::SCC_PRINT()
{
   Cd_graph_list_iterator next_arg(*this);
   Cd_graph_ each_arg;
   int i = 1;

   cout << "\n\nITS SCC-COMPONENTS:" << endl;
   cout << "==================\n";
   while (each_arg = next_arg()) {
      cout << form("\nSCC %3d:\n", i++);
      cout << "=======" << endl;
      each_arg->SCC_PRINT();
      }
 }

void Cd_graph::SCC_PRINT()
{
   adjacencies->SCC_PRINT();
}

void Adjacency_Nlist::SCC_PRINT()
{
   Adjacency_list_iterator next_arg(*this);
   Adjacency_ each_arg;
   int counter = 1;

   cout << "        ";
   while (each_arg = next_arg())
   {
      each_arg->get_source()->pp(cout);
      counter++;
      if (counter==6)
      {
	  counter=1;
	  cout << endl;
	  cout << "        ";
      }
   }
   cout << endl;
}

void Adjacency::SCC_PRINT()
{
   source->pp();
   ns->pp();
   cout << "." << endl;
 }

void Cd_graphs::SCC_INPUT_PRINT()
{
   cd_graphs->SCC_INPUT_PRINT();
 }

void Cd_graph_List::SCC_INPUT_PRINT()
{
   Cd_graph_list_iterator next_arg(*this);
   Cd_graph_ each_arg;

   while (each_arg = next_arg())
      each_arg->SCC_INPUT_PRINT();
 }

void Cd_graph::SCC_INPUT_PRINT()
{
   adjacencies->SCC_INPUT_PRINT();
 }

void Adjacency_Nlist::SCC_INPUT_PRINT()
{
   Adjacency_list_iterator next_arg(*this);
   Adjacency_ each_arg;

   cout << "\n// --------------------------------------------------------" << endl;
   cout << "INPUT CD_GRAPH:\n";
   cout << "==============\n";

   while (each_arg = next_arg()) {
      each_arg->pp();
      cout << "" << endl;
      }
 }