/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *                ANALYSIS OF CLAUSE SETS                 * */
/* *                                                        * */
/* *  $Module:   ANALYZE                                    * */ 
/* *                                                        * */
/* *  Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001      * */
/* *  MPI fuer Informatik                                   * */
/* *                                                        * */
/* *  This program is free software; you can redistribute   * */
/* *  it and/or modify it under the terms of the GNU        * */
/* *  General Public License as published by the Free       * */
/* *  Software Foundation; either version 2 of the License, * */
/* *  or (at your option) any later version.                * */
/* *                                                        * */
/* *  This program is distributed in the hope that it will  * */
/* *  be useful, but WITHOUT ANY WARRANTY; without even     * */
/* *  the implied warranty of MERCHANTABILITY or FITNESS    * */
/* *  FOR A PARTICULAR PURPOSE.  See the GNU General Public * */
/* *  License for more details.                             * */
/* *                                                        * */
/* *  You should have received a copy of the GNU General    * */
/* *  Public License along with this program; if not, write * */
/* *  to the Free Software Foundation, Inc., 59 Temple      * */
/* *  Place, Suite 330, Boston, MA  02111-1307  USA         * */
/* *                                                        * */
/* $Revision$                                        * */
/* $State$                                            * */
/* $Date$                             * */
/* $Author$                                       * */
/* *                                                        * */
/* *             Contact:                                   * */
/* *             Christoph Weidenbach                       * */
/* *             MPI fuer Informatik                        * */
/* *             Stuhlsatzenhausweg 85                      * */
/* *             66123 Saarbruecken                         * */
/* *             Email: weidenb@mpi-sb.mpg.de               * */
/* *             Germany                                    * */
/* *                                                        * */
/* ********************************************************** */
/**************************************************************/


/* $RCSfile$ */

#include <stdio.h>

#include "analyze.h"

static LIST ana_CalculatePredicatePrecedence(LIST, LIST);
static LIST ana_CalculateFunctionPrecedence(LIST, LIST, FLAGSTORE);

/**************************************************************/
/* Global Variables                                           */
/**************************************************************/

LIST ana_FINITEMONADICPREDICATES;  /* List of monadic predicates with finite extension */

BOOL ana_EQUATIONS;                /* Problem contains any equations at all */
static BOOL ana_PEQUATIONS;        /* Problem contains positive equations */
static BOOL ana_NEQUATIONS;        /* Problem contains negative equations */
static BOOL ana_FUNCTIONS;         /* Problem contains non-constant function symbols */
static BOOL ana_PROP;              /* Problem contains propositional variables */
static BOOL ana_GROUND;            /* Problem contains non-propositional, non-equational ground atoms */
static BOOL ana_NONUNIT;           /* Problem contains non-unit clauses */
static BOOL ana_MONADIC;           /* Problem contains non-ground monadic predicates */
static BOOL ana_NONMONADIC;        /* Problem contains non-ground n-place predicates, n>1, not equality */
BOOL ana_SORTRES;                  /* Problem contains literal not(S(x)) for some S */
BOOL ana_USORTRES;                 /* Problem contains literal not(S(t)) for some S */
static BOOL ana_FINDOMAIN;         /* Problem contains clause implying a finite domain */
static BOOL ana_NONTRIVDOMAIN;     /* Problem contains clause implying a domain of size greater one */
static BOOL ana_CONGROUND;         /* Conjecture is ground */

static BOOL ana_PUREEQUATIONAL;    /* Problem is purely equational */
static BOOL ana_PUREPROPOSITIONAL; /* Problem is purely propositional */

BOOL ana_SORTDECEQUATIONS;         /* True if all positive equations are sort decreasing with respect to
                                      the static sort theory contained in the problem */
static BOOL ana_SORTMANYEQUATIONS;  /* True if all positive equations have the
				       same sort on left and right hand side with
				       respect to the static sort theory
				       contained in the problem */

static NAT  ana_AXIOMCLAUSES;      /* Number of axiom clauses */
static NAT  ana_CONCLAUSES;        /* Number of conjecture clauses */
static NAT  ana_NONHORNCLAUSES;    /* Number of Non-Horn clauses */


/**************************************************************/
/* Functions                                                  */
/**************************************************************/

void ana_AnalyzeProblem(PROOFSEARCH Search, LIST Clauses)
/**************************************************************
  INPUT:   A proofsearch object and a list of clauses.
  RETURNS: Void.
  EFFECT:  Analyzes the clauses and sets the analyze variables.
           Recomputes the weight for the clauses.
	   <Search> is modified according to clauses: non trivial domain number
	   is set
***************************************************************/
{
  CLAUSE Clause;

  ana_EQUATIONS       = FALSE;  
  ana_PEQUATIONS      = FALSE;             /* Defaults for properties */
  ana_NEQUATIONS      = FALSE; 
  ana_FUNCTIONS       = FALSE;
  ana_FINDOMAIN       = FALSE;
  ana_NONTRIVDOMAIN   = FALSE;
  ana_MONADIC         = FALSE;
  ana_NONMONADIC      = FALSE;
  ana_PROP            = FALSE;
  ana_GROUND          = FALSE;
  ana_SORTRES         = FALSE;
  ana_USORTRES        = FALSE;
  ana_NONUNIT         = FALSE;
  ana_CONGROUND       = TRUE;

  ana_AXIOMCLAUSES    = 0; 
  ana_CONCLAUSES      = 0;
  ana_NONHORNCLAUSES  = 0;

  list_Delete(ana_FINITEMONADICPREDICATES);
  ana_FINITEMONADICPREDICATES = list_Nil();

  if (list_Empty(Clauses))
    return;

  ana_FINITEMONADICPREDICATES = clause_FiniteMonadicPredicates(Clauses);

  while (!list_Empty(Clauses)) {
    Clause = (CLAUSE)list_Car(Clauses);
    clause_UpdateWeight(Clause, prfs_Store(Search));

    if (clause_GetFlag(Clause,CONCLAUSE))
      ana_CONCLAUSES++;
    else
      ana_AXIOMCLAUSES++;

    if (clause_NumOfSuccLits(Clause) > 1)
      ana_NONHORNCLAUSES++;

    if (ana_CONGROUND && clause_GetFlag(Clause,CONCLAUSE) &&
	clause_MaxVar(Clause) != symbol_GetInitialStandardVarCounter())
      ana_CONGROUND = FALSE;
    if (!ana_PEQUATIONS && clause_ContainsPositiveEquations(Clause)) {
      ana_PEQUATIONS = TRUE;
    }
    if (!ana_NEQUATIONS && clause_ContainsNegativeEquations(Clause)) {
      ana_NEQUATIONS = TRUE;
    }
    if (!ana_MONADIC || !ana_NONMONADIC || !ana_PROP || !ana_GROUND)
      clause_ContainsFolAtom(Clause,&ana_PROP,&ana_GROUND,&ana_MONADIC,&ana_NONMONADIC);

    if (!ana_FUNCTIONS && clause_ContainsFunctions(Clause)) {
      ana_FUNCTIONS = TRUE;
    }
    if (!ana_FINDOMAIN && clause_ImpliesFiniteDomain(Clause)) {
      ana_FINDOMAIN = TRUE;
    }
    if (!ana_NONTRIVDOMAIN && clause_ImpliesNonTrivialDomain(Clause)) {
      prfs_SetNonTrivClauseNumber(Search, clause_Number(Clause));
      ana_NONTRIVDOMAIN =  TRUE;
    }
    if (!ana_NONUNIT && clause_Length(Clause) > 1) {
      ana_NONUNIT = TRUE;
    }
    if (!ana_SORTRES || !ana_USORTRES) 
      clause_ContainsSortRestriction(Clause,&ana_SORTRES,&ana_USORTRES);
    
    Clauses = list_Cdr(Clauses);
  }

  ana_PUREEQUATIONAL    = ((ana_PEQUATIONS || ana_NEQUATIONS) && !ana_MONADIC &&
			   !ana_NONMONADIC && !ana_PROP && !ana_GROUND);
  ana_EQUATIONS         = (ana_PEQUATIONS || ana_NEQUATIONS);
  ana_PUREPROPOSITIONAL = (!ana_PEQUATIONS && !ana_NEQUATIONS &&!ana_MONADIC &&
			   !ana_NONMONADIC && ana_PROP);
}


void ana_AnalyzeSortStructure(LIST Clauses, FLAGSTORE Flags,
			      PRECEDENCE Precedence)
/**************************************************************
  INPUT:   A list of clauses, a flag store and a precedence.
  RETURNS: Nothing.
  EFFECT:  The sort structure with respect to equations is analyzed.
           It is detected whether all equations are many sorted or
	   sort decreasing.
***************************************************************/
{
  if (ana_PEQUATIONS && ana_SORTRES) {
    STR Result;
    Result                = sort_AnalyzeSortStructure(Clauses,Flags,Precedence);
    ana_SORTMANYEQUATIONS = (Result == SORTEQMANY);
    ana_SORTDECEQUATIONS  = (Result == SORTEQMANY || Result == SORTEQDECR);
  }
}


void ana_Print(FLAGSTORE Flags, PRECEDENCE Precedence)
/**************************************************************
  INPUT:   A flag store and a precedence.
  RETURNS: Nothing.
  EFFECT:  The results of an analysis stored in the module variables
           is printed to stdout.
***************************************************************/
{
  const char* Horn;

  if (ana_NONHORNCLAUSES == 0)
    Horn = "Horn";
  else
    Horn = "Non-Horn";
  
  if (ana_MONADIC && !ana_NONMONADIC) {
    printf("\n This is a monadic %s problem",Horn);
    if (ana_PEQUATIONS || ana_NEQUATIONS)
      fputs(" with equality.", stdout);
    else
      fputs(" without equality.", stdout);
  }
  else
    if (ana_PEQUATIONS || ana_NEQUATIONS) {
      if (ana_NONMONADIC || ana_MONADIC || ana_PROP)
	printf("\n This is a first-order %s problem containing equality.",Horn);
      else
	if (ana_NONUNIT)
	  printf("\n This is a pure equality %s problem.",Horn);
	else
	  fputs("\n This is a unit equality problem.", stdout);
    }
    else
      if (ana_NONMONADIC || ana_MONADIC)
	printf("\n This is a first-order %s problem without equality.",Horn);

  if (ana_PUREPROPOSITIONAL)
    printf("\n This is a propositional %s problem.",Horn);
  else
    if (ana_FINDOMAIN || !ana_FUNCTIONS) {
      fputs("\n This is a problem that has, if any, a finite domain model.",
	    stdout);
      if (ana_FINDOMAIN)
	fputs("\n There is a finite domain clause.", stdout);
      if (!ana_FUNCTIONS)
	fputs("\n There are no function symbols.", stdout);
    }

  if (ana_NONTRIVDOMAIN)
    fputs("\n This is a problem that has, if any, a non-trivial domain model.",
	  stdout);
      
  
  if (ana_SORTRES) {
    fputs("\n This is a problem that contains sort information.", stdout);
    if (ana_PEQUATIONS) {
      if (ana_SORTMANYEQUATIONS)
	fputs("\n All equations are many sorted.", stdout);
      else {
	if (ana_SORTDECEQUATIONS)
	  fputs("\n All equations are sort-decreasing.", stdout);
      }
    }
  }

  if (ana_CONCLAUSES > 0 && ana_CONGROUND && !ana_PUREPROPOSITIONAL)
    fputs("\n The conjecture is ground.", stdout);

  if (!list_Empty(ana_FINITEMONADICPREDICATES)) {
    LIST Scan;
    fputs("\n The following monadic predicates have finite extensions: ", stdout);
    for (Scan=ana_FINITEMONADICPREDICATES;!list_Empty(Scan);Scan=list_Cdr(Scan)) {
      symbol_Print((SYMBOL)list_Car(Scan));
      if (!list_Empty(list_Cdr(Scan)))
	fputs(", ", stdout);
    }
    putchar('.');
  }

  printf("\n Axiom clauses: %d Conjecture clauses: %d",ana_AXIOMCLAUSES,ana_CONCLAUSES);

  flag_PrintInferenceRules(Flags);
  flag_PrintReductionRules(Flags);
  fputs("\n Extras    : ", stdout);
  if (flag_GetFlagValue(Flags, flag_SATINPUT))
    fputs("Input Saturation, ", stdout);
  else
    fputs("No Input Saturation, ", stdout);
  if (flag_GetFlagValue(Flags, flag_SELECT) == flag_SELECTOFF)
    fputs("No Selection, ", stdout);
  else
    if (flag_GetFlagValue(Flags, flag_SELECT) == flag_SELECTIFSEVERALMAXIMAL)
      fputs("Dynamic Selection, ", stdout);
    else
      fputs("Always Selection, ", stdout);
  if (flag_GetFlagValue(Flags, flag_SPLITS) == flag_SPLITSUNLIMITED)
    fputs("Full Splitting, ", stdout);
  else
    if (flag_GetFlagValue(Flags, flag_SPLITS) == flag_SPLITSOFF)
      fputs("No Splitting, ", stdout);
    else
      printf("Maximum of %d Splits, ",flag_GetFlagValue(Flags, flag_SPLITS));
  if (flag_GetFlagValue(Flags, flag_FULLRED))
    fputs("Full Reduction, ", stdout);
  else
    fputs("Lazy Reduction, ", stdout);
  printf(" Ratio: %d, FuncWeight: %d, VarWeight: %d",
	 flag_GetFlagValue(Flags, flag_WDRATIO),
	 flag_GetFlagValue(Flags, flag_FUNCWEIGHT),
	 flag_GetFlagValue(Flags, flag_VARWEIGHT));
  fputs("\n Precedence: ", stdout);
  fol_PrintPrecedence(Precedence);
  fputs("\n Ordering  : ", stdout);
  fputs(flag_GetFlagValue(Flags, flag_ORD) == flag_ORDKBO ? "KBO" : "RPOS",
	stdout);
}


void ana_AutoConfiguration(LIST Clauses, FLAGSTORE Flags,
			   PRECEDENCE Precedence)
/**************************************************************
  INPUT:   A list of clauses, a flag store and a precedence.
  RETURNS: Nothing.
  EFFECT:  Based on the values of the ana analysis module, an appropriate
           complete configuration of inference, reduction rules and other
	   settings is established.
***************************************************************/
{
  LIST Scan, Functions, Predicates, Constants;

  Functions  = symbol_GetAllFunctions();
  Predicates = fol_GetNonFOLPredicates();

  /* Set precedence */
  Predicates = ana_CalculatePredicatePrecedence(Predicates, Clauses);
  Functions  = ana_CalculateFunctionPrecedence(Functions, Clauses, Flags);
  Constants  = list_Nil();

  for (Scan=Functions; !list_Empty(Scan); Scan=list_Cdr(Scan))
    if (symbol_IsConstant((SYMBOL)list_Car(Scan)))
      Constants = list_Cons(list_Car(Scan),Constants);
  Functions = list_NPointerDifference(Functions,Constants);
  Constants = list_NReverse(Constants);

  for ( ; !list_Empty(Functions); Functions = list_Pop(Functions))
    symbol_SetIncreasedOrdering(Precedence, (SYMBOL)list_Car(Functions));
  /* Predicates < Functions */
  for ( ; !list_Empty(Predicates); Predicates = list_Pop(Predicates))
    symbol_SetIncreasedOrdering(Precedence, (SYMBOL)list_Car(Predicates));
  /* Constants < Predicates */
  /* Predicates < Functions */
  for ( ; !list_Empty(Constants); Constants = list_Pop(Constants))
    symbol_SetIncreasedOrdering(Precedence, (SYMBOL)list_Car(Constants));

  flag_ClearInferenceRules(Flags);
  flag_ClearReductionRules(Flags);

  flag_SetFlagValue(Flags, flag_ROBV,    flag_ROBVON);
  flag_SetFlagValue(Flags, flag_RTAUT,   flag_RTAUTSYNTACTIC);
  flag_SetFlagValue(Flags, flag_RFSUB,   flag_RFSUBON);
  flag_SetFlagValue(Flags, flag_RBSUB,   flag_RBSUBON);
  flag_SetFlagValue(Flags, flag_RFMRR,   flag_RFMRRON);
  flag_SetFlagValue(Flags, flag_RBMRR,   flag_RBMRRON);
  flag_SetFlagValue(Flags, flag_RUNC,    flag_RUNCON);
  flag_SetFlagValue(Flags, flag_FULLRED, flag_FULLREDON);
  /*flag_SetFlagValue(Flags, flag_FUNCWEIGHT,1);
  flag_SetFlagValue(Flags, flag_VARWEIGHT,1);*/
  flag_SetFlagValue(Flags, flag_WDRATIO,5);

  if (ana_NEQUATIONS) {
    flag_SetFlagValue(Flags, flag_IEQR, flag_EQUALITYRESOLUTIONON);
    if (ana_NONUNIT) {
      if (ana_NONTRIVDOMAIN)
	flag_SetFlagValue(Flags, flag_RAED, flag_RAEDPOTUNSOUND);
      else
	flag_SetFlagValue(Flags, flag_RAED, flag_RAEDSOUND);
    }
  }

  if (ana_PEQUATIONS) {
    flag_SetFlagValue(Flags, flag_ISPR, flag_SUPERPOSITIONRIGHTON);
    flag_SetFlagValue(Flags, flag_ISPL, flag_SUPERPOSITIONLEFTON);
    if (ana_NONHORNCLAUSES > 0)
      flag_SetFlagValue(Flags, flag_IEQF, flag_EQUALITYFACTORINGON);
    if (ana_NONUNIT) 
      flag_SetFlagValue(Flags, flag_RCON, flag_RCONON);
    flag_SetFlagValue(Flags, flag_RFREW, flag_RFREWON);
    flag_SetFlagValue(Flags, flag_RBREW, flag_RBREWON);
    flag_SetFlagValue(Flags, flag_RFCRW, flag_RFCRWOFF); /* Here we could activate contextual rewriting */
    flag_SetFlagValue(Flags, flag_RBCRW, flag_RBCRWOFF);
  }
  
  if (ana_SORTRES) {
    flag_SetFlagValue(Flags, flag_SORTS, flag_SORTSMONADICWITHVARIABLE);
    flag_SetFlagValue(Flags, flag_IEMS,  flag_EMPTYSORTON);
    flag_SetFlagValue(Flags, flag_ISOR,  flag_SORTRESOLUTIONON);
    flag_SetFlagValue(Flags, flag_RSSI, flag_RSSION);
    if (!ana_PEQUATIONS || ana_SORTMANYEQUATIONS)
      flag_SetFlagValue(Flags, flag_RSST, flag_RSSTON);
  }
  else
    flag_SetFlagValue(Flags, flag_SORTS, flag_SORTSOFF);

  if (ana_MONADIC || ana_NONMONADIC) { /* Problem contains real predicates */
    flag_SetFlagValue(Flags, flag_IORE, flag_ORDEREDRESOLUTIONNOEQUATIONS);
    if (ana_NONHORNCLAUSES > 0)
      flag_SetFlagValue(Flags, flag_IOFC, flag_FACTORINGONLYRIGHT);
    if (ana_NONUNIT) 
      flag_SetFlagValue(Flags, flag_RCON, flag_RCONON);
  }


  if (!ana_FUNCTIONS)
    flag_SetFlagValue(Flags, flag_SELECT, flag_SELECTALWAYS);
  else
    if (ana_NONUNIT)
      flag_SetFlagValue(Flags, flag_SELECT, flag_SELECTIFSEVERALMAXIMAL);
    else
      flag_SetFlagValue(Flags, flag_SELECT, flag_SELECTOFF);

  if (ana_CONCLAUSES < ana_AXIOMCLAUSES || (ana_CONGROUND && !ana_PUREPROPOSITIONAL))
    flag_SetFlagValue(Flags, flag_SATINPUT, flag_SATINPUTON);
  else
    flag_SetFlagValue(Flags, flag_SATINPUT, flag_SATINPUTOFF);

  if (ana_NONHORNCLAUSES > 0)
    flag_SetFlagValue(Flags, flag_SPLITS, flag_SPLITSUNLIMITED);
  else
    flag_SetFlagValue(Flags, flag_SPLITS, flag_SPLITSOFF);
}


void ana_ExploitSortAnalysis(FLAGSTORE Flags)
/**************************************************************
  INPUT:   A flag store.
  EFFECT:  If all equations are many sorted and or no positive
           equations occur at all and the problem contains sort
	   information, static soft typing is activated.
***************************************************************/
{
  if (ana_SORTRES && (!ana_PEQUATIONS || ana_SORTMANYEQUATIONS))
    flag_SetFlagValue(Flags, flag_RSST, flag_RSSTON);
}


static LIST ana_CalculatePredicatePrecedence(LIST Predicates, LIST Clauses)
/**************************************************************
  INPUT:   A list of predicates and a list of clauses.
  RETURNS: A list of predicate symbols, which should be used
           for setting the symbol precedence. The list is sorted
           in descending order, that means predicates with highest
           precedence come first.
  EFFECT:  Analyze the clause list to build a directed graph G where
           the predicates are vertices. There's an edge (P,Q) in
           G iff a clause exists where P is a negative literal
           and Q is a positive literal and P != Q. Apply DFS to
           find the strongly connected components of this graph.
	   The <Predicates> list is deleted.
  CAUTION: The predicate list must contain ALL predicates
           occurring in the clause list!
***************************************************************/
{
  GRAPH  graph;
  LIST   result, scan;
  int    i, j;
  NAT    count;
  SYMBOL s;

  /* clause_ListPrint(Clauses); DBG */

  if (list_Empty(Predicates)) {
    return Predicates;
  }

  graph = graph_Create();

  /* First create the nodes: one node for every predicate symbol. */
  for ( ; !list_Empty(Predicates); Predicates = list_Pop(Predicates))
    graph_AddNode(graph, symbol_Index((SYMBOL)list_Car(Predicates)));

  /* Now scan the clause clause list to create the edges */
  /* An edge (P,Q) means P is smaller than Q */
  for (scan = Clauses; !list_Empty(scan); scan = list_Cdr(scan)) {
    CLAUSE c = list_Car(scan);

    for (i = clause_FirstLitIndex(); i < clause_FirstSuccedentLitIndex(c); i++) {
      SYMBOL negPred = term_TopSymbol(clause_GetLiteralAtom(c, i));
      if (!symbol_Equal(negPred, fol_Equality())) { /* negative predicate */
	for (j = clause_FirstSuccedentLitIndex(c); j < clause_Length(c); j++) {
	  SYMBOL posPred = term_TopSymbol(clause_GetLiteralAtom(c, j));
	  if (!symbol_Equal(posPred, fol_Equality()) && /* positive predicate */
	      negPred != posPred) {  /* No self loops! */
	    graph_AddEdge(graph_GetNode(graph, symbol_Index(negPred)),
			  graph_GetNode(graph, symbol_Index(posPred)));
	  }
	}
      }
    }
  }

  /* graph_Print(graph); fflush(stdout); DBG */

  /* Calculate the strongly connected components of the graph */
  count = graph_StronglyConnectedComponents(graph);

  /* Now create the precedence list by scanning the nodes.        */
  /* If there's a link between two strongly connected components  */
  /* c1 and c2 then component_num(c1) > component_num(c2), so the */
  /* following code creates a valid precedence list in descending */
  /* order.                                                       */
  result = list_Nil();
  for (i = count - 1; i >= 0; i--) {
    for (scan = graph_Nodes(graph); !list_Empty(scan); scan = list_Cdr(scan)) {
      GRAPHNODE n = list_Car(scan);
      if (graph_NodeCompNum(n) == i) {
	/* The symbol represented by the node <<n> belongs to component <i> */
	s = symbol_GetSigSymbol(graph_NodeNumber(n));
	result = list_Cons((POINTER)s, result);
      }
    }
  }

  /* putchar('\n');
     for (scan = result; !list_Empty(scan); scan = list_Cdr(scan)) {
     s = (SYMBOL) list_Car(scan);
     symbol_Print(s);
     putchar(' ');
     }
     putchar('\n'); fflush(stdout); DBG */

  graph_Delete(graph);

  return result;
}


/* We use the node info to store the degree of the node */
static __inline__ NAT ana_NodeDegree(GRAPHNODE Node)
{
  return (NAT)graph_NodeInfo(Node);
}


static __inline__ void ana_IncNodeDegree(GRAPHNODE Node)
{
  graph_NodeSetInfo(Node, (POINTER)(ana_NodeDegree(Node)+1));
}

static BOOL ana_NodeGreater(GRAPHNODE N1, GRAPHNODE N2)
/**************************************************************
  INPUT:   Two graph nodes.
  RETURNS: TRUE, if N1 is greater than N2.
  EFFECT:  This function is used to sort the node list
           of the graph in ana_CalculateFunctionPrecedence.
***************************************************************/
{
  return (symbol_Arity(symbol_GetSigSymbol(graph_NodeNumber(N1))) >
	  symbol_Arity(symbol_GetSigSymbol(graph_NodeNumber(N2))));
}


static BOOL ana_BidirectionalDistributivity(LIST SymbolPairs)
/**************************************************************
  INPUT:   A list of symbol pairs defining distributivity.
  RETURNS: TRUE, if the list contains two pairs (s1, s2) and (s2, s1)
           FALSE otherwise.
  EFFECT:  This function is used to detect symbols that are distributive
           in both directions, logical OR and AND for example.
***************************************************************/
{
  LIST scan, actPair, nextPair;

  for ( ; !list_Empty(SymbolPairs); SymbolPairs = list_Cdr(SymbolPairs)) {
    actPair = list_Car(SymbolPairs);
    /* If actPair = (s1, s2), check whether there's a pair (s2, s1) in list */
    for (scan = list_Cdr(SymbolPairs); !list_Empty(scan); scan = list_Cdr(scan)) {
      nextPair = list_Car(scan);
      if (symbol_Equal((SYMBOL)list_PairFirst(actPair),(SYMBOL)list_PairSecond(nextPair)) &&
	  symbol_Equal((SYMBOL)list_PairSecond(actPair),(SYMBOL)list_PairFirst(nextPair)))
	return TRUE;
    }
  }
  return FALSE;
}


static LIST ana_CalculateFunctionPrecedence(LIST Functions, LIST Clauses,
					    FLAGSTORE Flags)
/**************************************************************
  INPUT:   A list of functions, a list of clauses and 
           a flag store.
  RETURNS: A list of function symbols, which should be used
           for setting the symbol precedence. The list is sorted
           in descending order, that means function with highest
           precedence come first.
  EFFECT:  Analyzes the clauses to build a directed graph G with
           function symbol as nodes. An edge (f,g) or in G means
           f should have lower precedence than g.
           An edge (f,g) or (g,f) is created if there's an equation
           equal(f(...), g(...)) in the clause list.
	   The direction of the edge depends on the degree of the
           nodes and the symbol arity.
	   Then find the strongly connected components of this
           graph.
           The "Ordering" flag will be set in the flag store.
  CAUTION: The value of "ana_PEQUATIONS" must be up to date.
***************************************************************/
{
  GRAPH     graph;
  GRAPHNODE n1, n2;
  LIST      result, scan, scan2, distrPairs;
  NAT       i, j;
  SYMBOL    s, Add, Mult;

  if (list_Empty(Functions))
    return Functions;   /* Problem contains no functions */
  else if (!ana_PEQUATIONS) {
    Functions = list_NumberSort(Functions, (NAT (*)(POINTER)) symbol_PositiveArity);
    return Functions;
  }

  graph = graph_Create();
  /* First create the nodes: one node for every function symbol. */
  for (; !list_Empty(Functions); Functions = list_Pop(Functions))
    graph_AddNode(graph, symbol_Index((SYMBOL)list_Car(Functions)));

  /* Now sort the node list wrt descending symbol arity. */
  graph_SortNodes(graph, ana_NodeGreater);

  /* A list of pairs (add, multiply) of distributive symbols */
  distrPairs = list_Nil();

  /* Now add undirected edges: there's an undirected edge between  */
  /* two nodes if the symbols occur as top symbols in a positive   */
  /* equation. */
  for (scan = Clauses; !list_Empty(scan); scan = list_Cdr(scan)) {
    CLAUSE c = list_Car(scan);
    for (i = clause_FirstSuccedentLitIndex(c);
	 i <= clause_LastSuccedentLitIndex(c); i++) {
      if (clause_LiteralIsEquality(clause_GetLiteral(c, i))) {
	/* Consider only positive equations */
	TERM t1, t2;

	if (fol_DistributiveEquation(clause_GetLiteralAtom(c,i), &Add, &Mult)) {
	  /* Add a pair (Add, Mult) to <distrTerms> */
	  distrPairs = list_Cons(list_PairCreate((POINTER)Add, (POINTER)Mult),
				 distrPairs);
	  /*fputs("\nDISTRIBUTIVITY: ", stdout);
	    term_PrintPrefix(clause_GetLiteralAtom(c,i));
	    fputs(" Add=", stdout); symbol_Print(Add);
	    fputs(" Mult=", stdout); symbol_Print(Mult); fflush(stdout); DBG */
	}

	t1 = term_FirstArgument(clause_GetLiteralAtom(c, i));
	t2 = term_SecondArgument(clause_GetLiteralAtom(c, i));

	if  (!term_IsVariable(t1) && !term_IsVariable(t2) &&
	     !term_EqualTopSymbols(t1, t2) &&  /* No self loops! */
	     !term_HasSubterm(t1, t2) &&       /* No subterm property */
	     !term_HasSubterm(t2, t1)) {
	  n1 = graph_GetNode(graph, symbol_Index(term_TopSymbol(t1)));
	  n2 = graph_GetNode(graph, symbol_Index(term_TopSymbol(t2)));
	  /* Create an undirected edge by adding two directed edges */
	  graph_AddEdge(n1, n2);
	  graph_AddEdge(n2, n1);
	  /* Use the node info for the degree of the node */
	  ana_IncNodeDegree(n1);
	  ana_IncNodeDegree(n2);
	}
      }
    }
  }
  
  /* putchar('\n');
     for (scan = graph_Nodes(graph); !list_Empty(scan); scan = list_Cdr(scan)) {
     n1 = list_Car(scan);
     printf("(%s,%d,%u), ",
     symbol_Name(symbol_GetSigSymbol(graph_NodeNumber(n1))),
     graph_NodeNumber(n1), ana_NodeDegree(n1));
     }
     graph_Print(graph); fflush(stdout); DBG */

  graph_DeleteDuplicateEdges(graph);
  
  /* Transform the undirected graph into a directed graph. */
  for (scan = graph_Nodes(graph); !list_Empty(scan); scan = list_Cdr(scan)) {
    n1 = list_Car(scan);
    result = list_Nil(); /* Collect edges from n1 that shall be deleted */ 
    for (scan2 = graph_NodeNeighbors(n1); !list_Empty(scan2);
	 scan2 = list_Cdr(scan2)) {
      int a1, a2;
      n2 = list_Car(scan2);
      /* Get the node degrees in the undirected graph with multiple edges */
      i  = ana_NodeDegree(n1);
      j  = ana_NodeDegree(n2);
      a1 = symbol_Arity(symbol_GetSigSymbol(graph_NodeNumber(n1)));
      a2 = symbol_Arity(symbol_GetSigSymbol(graph_NodeNumber(n2)));

      if (i > j || (i==j && a1 >= a2)) {
	/* symbol2 <= symbol1, so remove edge n1 -> n2 */
	result = list_Cons(n2, result);
      }
      if (i < j || (i==j && a1 <= a2)) {
	/* symbol1 <= symbol2, so remove edge n2 -> n1 */
	graph_DeleteEdge(n2, n1);
      }
      /* NOTE: If (i==j && a1==a2) both edges are deleted! */
    }
    /* Now delete edges from n1 */
    for ( ; !list_Empty(result); result = list_Pop(result))
      graph_DeleteEdge(n1, list_Car(result));
  }

  if (!list_Empty(distrPairs) && !ana_BidirectionalDistributivity(distrPairs)) {
    /* Enable RPO ordering, otherwise the default KBO will be used. */
    flag_SetFlagValue(Flags, flag_ORD, flag_ORDRPOS);
  }

  /* Now examine the list of distribute symbols */
  /* since they've highest priority.                  */
  for ( ; !list_Empty(distrPairs); distrPairs = list_Pop(distrPairs)) {
    scan = list_Car(distrPairs); /* A pair (Add, Mult) */
    /* Addition */
    n1 = graph_GetNode(graph,
		       symbol_Index((SYMBOL)list_PairFirst(scan)));
    /* Multiplication */
    n2 = graph_GetNode(graph, 
		       symbol_Index((SYMBOL)list_PairSecond(scan)));
    /* Remove any edges between n1 and n2 */
    graph_DeleteEdge(n1, n2);
    graph_DeleteEdge(n2, n1);
    /* Add one edge Addition -> Multiplication */
    graph_AddEdge(n1, n2);
    list_PairFree(scan);
  }

  /* fputs("\n------------------------",stdout);
     graph_Print(graph); fflush(stdout); DBG */

  /* Calculate the strongly connected components of the graph. */
  /* <i> is the number of SCCs. */
  i = graph_StronglyConnectedComponents(graph);

  /* Now create the precedence list by scanning the nodes.        */
  /* If there's a link between two strongly connected components  */
  /* c1 and c2 then component_num(c1) > component_num(c2), so the */
  /* following code creates a valid precedence list in descending */
  /* order.                                                       */
  result = list_Nil();
  while (i-- > 0) {   /* for i = numberOfSCCs -1 dowto 0 */
    for (scan = graph_Nodes(graph); !list_Empty(scan); scan = list_Cdr(scan)) {
      n1 = list_Car(scan);
      if (graph_NodeCompNum(n1) == i) {
	/* The symbol represented by the node <n> belongs to component <i> */
	s = symbol_GetSigSymbol(graph_NodeNumber(n1));
	result = list_Cons((POINTER)s, result);
      }
    }
  }

  /* putchar('\n');
     for (scan = result; !list_Empty(scan); scan = list_Cdr(scan)) {
     s = (SYMBOL) list_Car(scan);
     symbol_Print(s);
     fputs(" > ", stdout);
     }
     putchar('\n'); fflush(stdout); DBG */

  graph_Delete(graph);

  return result;
}