#include "semcheck.h"

/*int Cd_graph::CYCLE_FREE_SUBGRAPH_START(Cd_graph *cd_graph)*/
int Cd_graph::CYCLE_FREE_SUBGRAPH_START()
{
   cout << "\nChecking the Inductiveness Axiom..." << endl;
   Cd_graphs *sccCd_graphs = new Cd_graphs();
   Cd_graphs *violationCd_graphs = new Cd_graphs();

   Cd_graph  *icd_graph = (Cd_graph*)this->g_copy();
   Cd_graphs *iCd_graphs= new Cd_graphs();

   iCd_graphs->CYCLE_FREE_SUBGRAPH_APPEND(icd_graph);

#ifdef DEBUG
iCd_graphs->CYCLE_FREE_SUBGRAPH_INPUT_PRINT();
#endif
   iCd_graphs->SCC(sccCd_graphs);
#ifdef DEBUG
sccCd_graphs->SCC_PRINT();
#endif
   sccCd_graphs->CYCLE_FREE_SUBGRAPH(violationCd_graphs);
   violationCd_graphs->CYCLE_FREE_SUBGRAPH_PRINT();

   if (violationCd_graphs->get_cd_graphs())
       if (violationCd_graphs->get_cd_graphs()->list_length()>0)
           return (FALSE);
   return (TRUE);
}


void Cd_graphs::CYCLE_FREE_SUBGRAPH(Cd_graphs *violationCd_graphs)
{
   cd_graphs->CYCLE_FREE_SUBGRAPH(violationCd_graphs);
 }

void Cd_graph_List::CYCLE_FREE_SUBGRAPH(Cd_graphs *violationCd_graphs)
{
   Cd_graph_list_iterator next_arg(*this);
   Cd_graph_ each_arg;

   if (this->list_length() == 1)
      next_arg()->CYCLE_FREE_SUBGRAPH_CHECK(violationCd_graphs);
   else
      while (each_arg = next_arg())
         each_arg->CYCLE_FREE_SUBGRAPH(violationCd_graphs);
 }

void Cd_graph::CYCLE_FREE_SUBGRAPH(Cd_graphs *violationCd_graphs)
{
   Cd_graphs *sccCd_graphs = new Cd_graphs();
   Cd_graph * iCd_graph = new Cd_graph();
   iCd_graph->set_adjacencies(adjacencies->CYCLE_FREE_SUBGRAPH_REDUCE());
   Cd_graphs *iCd_graphs   =
                new Cd_graphs
                 ( new Cd_graph_List( iCd_graph ));

   iCd_graphs->SCC(sccCd_graphs);
   sccCd_graphs->CYCLE_FREE_SUBGRAPH(violationCd_graphs);
 }

Adjacency_Nlist *Adjacency_Nlist::CYCLE_FREE_SUBGRAPH_REDUCE()
{
   Adjacency_list_iterator next_arg(*this);
   Adjacency_ each_arg;
   Adjacency_Nlist *iAdjacency_Nlist = new Adjacency_Nlist();

   while (each_arg = next_arg()) {
      each_arg->CYCLE_FREE_SUBGRAPH_REDUCE(this);
      iAdjacency_Nlist->append(each_arg);
      }
   return(iAdjacency_Nlist);
 }

void Adjacency::CYCLE_FREE_SUBGRAPH_REDUCE(Adjacency_Nlist *iAdjacency_Nlist)
{
   ns->CYCLE_FREE_SUBGRAPH_REDUCE(iAdjacency_Nlist);
 }

void Neighbors::CYCLE_FREE_SUBGRAPH_REDUCE(Adjacency_Nlist *iAdjacency_Nlist)
{
}

void Repetit_n::CYCLE_FREE_SUBGRAPH_REDUCE(Adjacency_Nlist *iAdjacency_Nlist)
{
   sandwiched->CYCLE_FREE_SUBGRAPH_REDUCE(iAdjacency_Nlist);
 }

void Kernel_Sandwich::CYCLE_FREE_SUBGRAPH_REDUCE(Adjacency_Nlist *iAdjacency_Nlist)
{
   inner->CYCLE_FREE_SUBGRAPH_REDUCE(iAdjacency_Nlist);
 }

void Kernel::CYCLE_FREE_SUBGRAPH_REDUCE(Adjacency_Nlist *iAdjacency_Nlist)
{
   if (nonempty)
      if (nonempty->CYCLE_FREE_SUBGRAPH_REDUCE(iAdjacency_Nlist) == 0)
         this->rset_nonempty((Term *)NULL);
 }


//
void Neighbors_wc::CYCLE_FREE_SUBGRAPH_REDUCE(Adjacency_Nlist *iAdjacency_Nlist)
{
   construct_ns->CYCLE_FREE_SUBGRAPH_REDUCE(iAdjacency_Nlist);
 }


//Alternation:
void Alternat_ns::CYCLE_FREE_SUBGRAPH_REDUCE(Adjacency_Nlist *iAdjacency_Nlist)
{
   this->rset_alternat_ns(alternat_ns->CYCLE_FREE_SUBGRAPH_REDUCE(iAdjacency_Nlist));
 }

Term_Bar_list *Term_Bar_list::CYCLE_FREE_SUBGRAPH_REDUCE(Adjacency_Nlist *iAdjacency_Nlist)
{

   Term_list_iterator next_arg(*this);
   Term_ each_arg;

   while (each_arg = next_arg())
      if (each_arg->CYCLE_FREE_SUBGRAPH_REDUCE(iAdjacency_Nlist) == 0)
         return   each_arg->CYCLE_FREE_SUBGRAPH_REDUCE_NEW();
   return(this);
 }


Term_Bar_list *Term::CYCLE_FREE_SUBGRAPH_REDUCE_NEW()
{
	return NULL;
}

Term_Bar_list *Normal::CYCLE_FREE_SUBGRAPH_REDUCE_NEW()
{
   Term_Bar_list * termbarlist  = new Term_Bar_list();
   Normal * anormal = new Normal ();
   Vertex * avertex = new Vertex (new DemIdent ("EMPTY_ALTERNATION"));
   anormal->rset_vertex(avertex);
   termbarlist->append(anormal);
   return termbarlist;
}



Term_Bar_list *CppTerm::CYCLE_FREE_SUBGRAPH_REDUCE_NEW()
{
   Term_Bar_list * termbarlist  = new Term_Bar_list();
   CppTerm * acplusplustype = new CppTerm();
   Vertex * avertex = new Vertex (new DemIdent ("EMPTY_ALTERNATION"));
   acplusplustype->rset_vertex(avertex);
   termbarlist->append(acplusplustype);
   return termbarlist;

}

//Construction:
void Any_vertex_List::CYCLE_FREE_SUBGRAPH_REDUCE(Adjacency_Nlist *iAdjacency_Nlist)
{
   int length = this->list_length();
   Any_vertex *iAny_vertex;

   while (length--) {
      iAny_vertex = this->get();
      if (iAny_vertex->CYCLE_FREE_SUBGRAPH_REDUCE(iAdjacency_Nlist))
         this->append(iAny_vertex);
      }
}

int Any_vertex::CYCLE_FREE_SUBGRAPH_REDUCE(Adjacency_Nlist *iAdjacency_Nlist)
{
	return 0;
}

// Syntax_vertex:
int Syntax_vertex::CYCLE_FREE_SUBGRAPH_REDUCE(Adjacency_Nlist *iAdjacency_Nlist)
{
   return(0);
 }

// Optional_term:
int Optional_term::CYCLE_FREE_SUBGRAPH_REDUCE(Adjacency_Nlist *iAdjacency_Nlist)
{
//   return(opt->CYCLE_FREE_SUBGRAPH_REDUCE(iAdjacency_Nlist));
   return(0);
 }

// Opt_labeled_term:
int Opt_labeled_term::CYCLE_FREE_SUBGRAPH_REDUCE(Adjacency_Nlist *iAdjacency_Nlist)
{
   return(this->get_vertex()->CYCLE_FREE_SUBGRAPH_REDUCE(iAdjacency_Nlist));
 }

int Term::CYCLE_FREE_SUBGRAPH_REDUCE(Adjacency_Nlist *iAdjacency_Nlist)
{
   if (iAdjacency_Nlist->SCC_GET_ADJACENCY(vertex))
      return(1);
   else
      return(0);
 }

void Cd_graph::CYCLE_FREE_SUBGRAPH_CHECK(Cd_graphs *violationCd_graphs)
{
   if (adjacencies->list_length() > 1)
      violationCd_graphs->CYCLE_FREE_SUBGRAPH_APPEND(this);
   else if (adjacencies->CYCLE_FREE_SUBGRAPH_CHECK())
      violationCd_graphs->CYCLE_FREE_SUBGRAPH_APPEND(this);
 }

int Adjacency_Nlist::CYCLE_FREE_SUBGRAPH_CHECK()
{
   Adjacency_list_iterator next_arg(*this);

   return(next_arg()->CYCLE_FREE_SUBGRAPH_CHECK());
 }

int Adjacency::CYCLE_FREE_SUBGRAPH_CHECK()
{
   int length;
   Vertex_Comma_list *iVertex_Comma_list = new Vertex_Comma_list();

   ns->SCC_GET_NS_VERTEX(iVertex_Comma_list);
   length = iVertex_Comma_list->list_length();

   while (length--)
      if (source->SCC_VERTEX_EQUAL(iVertex_Comma_list->get()))
         return(1);

   return(0);
 }

void Cd_graphs::CYCLE_FREE_SUBGRAPH_APPEND(Cd_graph *iCd_graph)
{
   if (cd_graphs)
      cd_graphs->append(iCd_graph);
   else
      this->rset_cd_graphs(new Cd_graph_List(iCd_graph));
 }

void Cd_graphs::CYCLE_FREE_SUBGRAPH_PRINT()
{
   if (cd_graphs)
      cd_graphs->CYCLE_FREE_SUBGRAPH_PRINT();
}

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

   int numberofav = this->list_length();
   int count = 1;

    if (numberofav>1)
      cout << "\nWarning: There are " << numberofav << "  violations of the Inductiveness Axiom." << endl;
    else
      cout << "\nWarning: there is one violation of the Inductiveness Axiom." << endl;
    while (each_arg = next_arg()) {
      cout << "\n        There are no non-cylic objects for the following classes:\n"
	   << endl;
      each_arg->SCC_PRINT();
    }
}
void Cd_graph_List::CYCLE_FREE_SUBGRAPH_INPUT_PRINT()
{
   Cd_graph_list_iterator next_arg(*this);
   Cd_graph_ each_arg;

    while (each_arg = next_arg()) {
      cout << "\n     INPUT  GRAPH" << endl;
      cout << "\n======================================" << endl;
      each_arg->SCC_PRINT();
      }
    cout << "\n======================================" << endl;
}