/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *                     SYMBOLS                            * */
/* *                                                        * */
/* *  $Module:   SYMBOL                                     * */ 
/* *                                                        * */
/* *  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 FreeBSD    * */
/* *  Licence.                                              * */
/* *                                                        * */
/* *  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 LICENCE file       * */ 
/* *  for more details.                                     * */
/* *                                                        * */
/* *                                                        * */
/* $Revision: 1.10 $                                         * */
/* $State: Exp $                                            * */
/* $Date: 2010-02-22 14:09:59 $                             * */
/* $Author: weidenb $                                       * */
/* *                                                        * */
/* *             Contact:                                   * */
/* *             Christoph Weidenbach                       * */
/* *             MPI fuer Informatik                        * */
/* *             Stuhlsatzenhausweg 85                      * */
/* *             66123 Saarbruecken                         * */
/* *             Email: spass@mpi-inf.mpg.de                * */
/* *             Germany                                    * */
/* *                                                        * */
/* ********************************************************** */
/**************************************************************/


/* $RCSfile: symbol.h,v $ */


#ifndef _SYMBOL_
#define _SYMBOL_

/**************************************************************/
/* Includes                                                   */
/**************************************************************/

#include "list.h"
#include "strings.h"
#include "hashmap.h"

/**************************************************************/
/* Data Structures and Constants                              */
/**************************************************************/

/* Critical values: the maximum length of a symbol string and the */
/* maximum number of different variables (in one term, clause)    */
/* CAUTION: symbol__MAXVARIABLES is the overall number of         */
/*          variables + 1 to provide safe allocation of contexts  */
/*          ... because the first var begins with 1 instead of 0. */

#define symbol__SYMBOLVARMAXLEN 7  

#define symbol__NOOFSTANDARDVAR 2000
#define symbol__NOOFINDEXVAR    2000

#define symbol__MAXSTANDARDVAR  symbol__NOOFSTANDARDVAR
#define symbol__MAXINDEXVAR     (symbol__NOOFSTANDARDVAR + symbol__NOOFINDEXVAR)

#define symbol__NOOFVARIABLES (symbol__NOOFSTANDARDVAR + symbol__NOOFINDEXVAR)
#define symbol__MAXVARIABLES  (symbol__NOOFVARIABLES + 1)

/* Symbol Types, Symbols are represented as integers. In case of */
/* constants, functions, predicates, junctors, the two least     */
/* significant bits encode the type. Variables are just          */
/* positive integers, all other symbols negative integers        */
/* The third least significant bit encodes the status of         */
/* function symbols (lexicographic or multiset)                  */

extern const int symbol_MASK;
extern const int symbol_TYPEMASK;
extern const int symbol_STATMASK;
extern const int symbol_TYPESTATMASK;

extern const int symbol_ARBITRARYARITY;

extern const int symbol_TYPEBITS;
extern const int symbol_STATBITS;
extern const int symbol_TYPESTATBITS;

extern const int symbol_SIGTYPES;

#define symbol_CONSTANT  0 
#define symbol_FUNCTION  1
#define symbol_PREDICATE 2
#define symbol_JUNCTOR   3

#define symbol_STATLEX   0 
#define symbol_STATMUL   1

/* For constants, functions, predicates, junctors, is a special */
/* symbol table available, containing the arity, status and the */
/* print name.                                                  */

typedef int SYMBOL;
typedef int *PRECEDENCE;

typedef struct signature {
  char   *name;         /* The name of the symbol as a string */
  NAT    length;        /* The length of the name. Needed for efficient printing */
  unsigned hash;        /* The speedup hash of the name. Needed for efficient hashing */
  int    weight;        /* The weight of the symbol for ordering purposes */
  int    arity;         /* The arity of the symbol */
  NAT    props;         /* Special Properties of the symbol, e.g. AC, Skolem,... */
  SYMBOL info;          /* 2 LSB denote Type and 3rd LSB denotes status */
  LIST   generatedBy;
  BOOL   fixed;         /* used when parsing to decide, whether the type of the given symbol has already been fixed*/
} SIGNATURE_NODE, *SIGNATURE;

typedef enum {SKOLEM=1,    CUMMUTATIVE=2, ASSOCIATIVE=4, ORDRIGHT=8, ORDMUL=16,
	      DECLSORT=32, DOMPRED=64, ISDEF=128, FREELY=256, GENERATED=512, SELECTED=1024,
	      PREDEFINED=2048
} SPROPERTY;


#define symbol__MAXSIGNATURE 400000

extern SIGNATURE *symbol_SIGNATURE;

extern SYMBOL symbol_STANDARDVARCOUNTER;
extern SYMBOL symbol_INDEXVARCOUNTER;

extern int symbol_ACTINDEX;
extern int symbol_ACTSKOLEMFINDEX;
extern int symbol_ACTSKOLEMCINDEX;
extern int symbol_ACTSKOLEMPINDEX;
extern int symbol_ACTSKOLEMAINDEX;

/* For matching of signature symbols */
extern SYMBOL symbol_CONTEXT[symbol__MAXSIGNATURE];


/**************************************************************/
/* Specials                                                   */
/**************************************************************/

NAT             symbol_MaxStringLength(void);

void            symbol_ReinitGenericNameCounters(void);

int             symbol_GetIncreasedOrderingCounter(void);

void            symbol_Delete(SYMBOL);
BOOL            symbol_IsSymbol(SYMBOL);
BOOL            symbol_IsFreed(SYMBOL);
void            symbol_Dump(PRECEDENCE);

LIST            symbol_SortByPrecedence(LIST, PRECEDENCE);
void            symbol_RearrangePrecedence(PRECEDENCE, LIST);

void            symbol_LowerSignature(void);

LIST            symbol_GetAllSymbols(void);
LIST            symbol_GetAllPredicates(void);
LIST            symbol_GetAllFunctions(void);
LIST            symbol_GetAllSymbolsWithProperty(SPROPERTY Property);

void            symbol_SetCount(SYMBOL, unsigned long);
unsigned long   symbol_GetCount(SYMBOL);

int             symbol_Ordering(PRECEDENCE, SYMBOL);

void            symbol_CheckIndexInRange(int);
void            symbol_CheckNoVariable(SYMBOL);

/**************************************************************/
/* Symbol Comparisons                                         */
/**************************************************************/

static __inline__ BOOL symbol_Equal(SYMBOL A, SYMBOL B)
{
  return A==B;
}

static __inline__ BOOL symbol_IsSignature(SYMBOL S)
{
  return S < 0;
}

static __inline__ int symbol_Type(SYMBOL ActSymbol)
{
  symbol_CheckNoVariable(ActSymbol);
  return (-ActSymbol) & symbol_TYPEMASK;
}

static __inline__ BOOL symbol_IsJunctor(SYMBOL S)
{
  return (symbol_IsSignature(S) && symbol_Type(S) == symbol_JUNCTOR);
}

static __inline__ BOOL symbol_IsFunction(SYMBOL S)
{
  return (symbol_IsSignature(S) &&
	  (symbol_Type(S) == symbol_FUNCTION ||
	   symbol_Type(S) == symbol_CONSTANT));
}

static __inline__ BOOL symbol_IsConstant(SYMBOL S)
{
  return (symbol_IsSignature(S) && symbol_Type(S) == symbol_CONSTANT);
}

static __inline__ BOOL symbol_IsPredicate(SYMBOL S)
{
  return (symbol_IsSignature(S) && symbol_Type(S) == symbol_PREDICATE);
}

static __inline__ BOOL symbol_IsVariable(SYMBOL S)
{
  return S > 0;
}

static __inline__ BOOL symbol_IsStandardVariable(SYMBOL S)
{
  return symbol_IsVariable(S) && (S <= symbol__MAXSTANDARDVAR);
}

static __inline__ BOOL symbol_IsIndexVariable(SYMBOL S)
{
  return (S > symbol__MAXSTANDARDVAR) && (S <= symbol__MAXINDEXVAR);
}

static __inline__ BOOL symbol_IsComplex(SYMBOL S)
{
  return (!symbol_IsVariable(S) && !symbol_IsConstant(S));
}

static __inline__ BOOL symbol_IsSuccessor(SYMBOL S, SYMBOL P)
{
  return S > P;
}


/**************************************************************/
/* Symbol Manipulation                                        */
/**************************************************************/

static __inline__ int symbol_GetInitialStandardVarCounter(void)
{
  return 0;
}

static __inline__ int symbol_GetInitialIndexVarCounter(void)
{
  return symbol__MAXSTANDARDVAR;
}

static __inline__ int symbol_FirstIndexVariable(void)
{
  return symbol__MAXSTANDARDVAR + 1;
}

static __inline__ int symbol_LastIndexVariable(void)
{
  return symbol_INDEXVARCOUNTER;
}

/* Special predefined symbols            */

#define symbol__NULL 0

static __inline__ int symbol_MaxVars(void)
{
  return symbol__MAXVARIABLES;
}

static __inline__ int symbol_MaxConsts(void)
{
  return symbol__MAXSIGNATURE;
}

static __inline__ int symbol_MaxBaseSorts(void)
{
  return symbol__MAXSIGNATURE;
}

static __inline__ int symbol_TypeBits(void)
{
  return symbol_TYPEBITS;
}

static __inline__ int symbol_Null(void)
{
  return 0;
}

static __inline__ int symbol_ActIndex(void)
{
  return symbol_ACTINDEX;
}

static __inline__ void symbol_ResetSkolemIndex(void)
{
  symbol_ACTSKOLEMFINDEX = 0;
  symbol_ACTSKOLEMCINDEX = 0;
  symbol_ACTSKOLEMPINDEX = 0;
  symbol_ACTSKOLEMAINDEX = 0;
}


/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *  MEMORY MANAGEMENT                                     * */
/* *                                                        * */
/* ********************************************************** */
/**************************************************************/

static __inline__ SIGNATURE symbol_GetSignature(void)
{
  return (SIGNATURE) memory_Malloc(sizeof(SIGNATURE_NODE));
} 


/**************************************************************/
/* Symbol Creation                                            */
/**************************************************************/

static __inline__ SYMBOL symbol_CreateStandardVariable(void)
/***************************************************************
  INPUT:   None
  RETURNS: A new symbol for a new standard variable numbered according to
           symbol_STANDARDVARCOUNTER
  SUMMARY: Creates a new standard variable symbol.
  EFFECTS: None
****************************************************************/
{
#ifdef CHECK
  if (symbol_STANDARDVARCOUNTER >= symbol__MAXSTANDARDVAR) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In symbol_CreateStandardVariable: Number of standard variables exceeded.\n");
    misc_FinishErrorReport();
   }
#endif

  return (++symbol_STANDARDVARCOUNTER);
}


static __inline__ SYMBOL symbol_CreateIndexVariable(void)
/***************************************************************
  INPUT:   None
  RETURNS: A new symbol for a new index variable numbered according to
           symbol_INDEXVARCOUNTER
  SUMMARY: Creates a new index variable symbol.
  EFFECTS: None
****************************************************************/
{

  if (symbol_INDEXVARCOUNTER >= symbol__MAXINDEXVAR) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In symbol_CreateIndexVariable: Number of index variables exceeded.\n");
    misc_FinishErrorReport();
  }

  return (++symbol_INDEXVARCOUNTER);
}


static __inline__ SYMBOL symbol_NextIndexVariable(SYMBOL Variable)
{
#ifdef CHECK
  if ((Variable != symbol_GetInitialIndexVarCounter() &&
       !symbol_IsIndexVariable(Variable)) ||
      Variable == symbol__MAXINDEXVAR) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In symbol_NextVariable: Illegal input.\n");
    misc_FinishErrorReport();
  }
#endif

  return (Variable + 1);
}


static __inline__ void symbol_SetStandardVarCounter(SYMBOL Variable)
{
#ifdef CHECK
  if (Variable != symbol_GetInitialStandardVarCounter() &&
      !symbol_IsStandardVariable(Variable)) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In symbol_SetStandardVarCounter: Illegal input.\n");
    misc_FinishErrorReport();
  } 
  else 
    if (Variable >= symbol__MAXSTANDARDVAR) {
      misc_StartErrorReport();
      misc_ErrorReport("\n In symbol_SetStandardVarCounter: Number of standard variables exceeded.\n");
      misc_FinishErrorReport();
    }
#endif

  symbol_STANDARDVARCOUNTER = Variable;
}

static __inline__ SYMBOL symbol_FirstVariable(void)
{
  return 1;
}

static __inline__ BOOL symbol_GreaterVariable(SYMBOL Var1, SYMBOL Var2)
{
  return Var1 > Var2;
}

static __inline__ void symbol_ResetStandardVarCounter(void)
{
  symbol_STANDARDVARCOUNTER = symbol_GetInitialStandardVarCounter();
}

void   symbol_Init(BOOL);
BOOL   symbol_SignatureExists(void);
void   symbol_FreeAllSymbols(void);
void   symbol_SeparateVariableSymbolNames(void);
SYMBOL symbol_CreateFunction(const char*, int, int, PRECEDENCE);
SYMBOL symbol_CreateSkolemFunction(int, PRECEDENCE);
SYMBOL symbol_CreateSkolemPredicate(int, PRECEDENCE);
SYMBOL symbol_CreatePredicate(const char*, int, int, PRECEDENCE);
SYMBOL symbol_CreateJunctor(const char*, int, int, PRECEDENCE);

/**************************************************************/
/* Symbol Access                                              */
/**************************************************************/

SYMBOL symbol_Lookup(const char*);

static __inline__ int symbol_VarIndex(SYMBOL ActSymbol)
{
  return ActSymbol;
}

static __inline__ int symbol_NormVar(SYMBOL ActSymbol)
{
  /* Normalization of variables s.t. the index of the variable
     is normalized starting always with 1:
     Standard variables are already normalized.
     Index variables are decreased by the number of the
     underlying standard variables. */
  return (ActSymbol <= symbol__MAXSTANDARDVAR) ? ActSymbol : (ActSymbol - symbol__MAXSTANDARDVAR);
}

/* The name, index and arity macros are only defined for signature   */
/* elements not for variables. The type of the symbol is not checked */
/* by the macros.                                                    */

static __inline__ int symbol_Index(SYMBOL ActSymbol)
{
  symbol_CheckNoVariable(ActSymbol);
  return (-ActSymbol) >> symbol_TYPESTATBITS;
}

static __inline__ SYMBOL symbol_SignatureSymbol(int ActIndex, int Type, int Status)
{
  return -((ActIndex << symbol_TYPESTATBITS)
	   | (Status << symbol_TYPEBITS)
	   | Type);
}

static __inline__ SIGNATURE symbol_Signature(int Index)
  /* Returns the signature of the symbol with <Index> or NULL */
  /* if the symbol was deleted */
{
  symbol_CheckIndexInRange(Index);
  return symbol_SIGNATURE[Index];
}

static __inline__ SYMBOL symbol_GetSigSymbol(int Index)
{
  return symbol_Signature(Index)->info;
}

static __inline__ int symbol_Stat(SYMBOL ActSymbol)
{
  symbol_CheckNoVariable(ActSymbol);
  return ((-ActSymbol) & symbol_STATMASK) >> symbol_TYPEBITS;
}

static __inline__ SYMBOL symbol_ChangeType(SYMBOL S, int Type)
/**************************************************************
  INPUT:   A symbol and a new type for that symbols.
  RETURNS: A new symbol that is the old symbol with type changed to <Type>,
           therefore the return value is different from <S>.
  EFFECT:  Uses the signature memory of the input symbol.
  CAUTION: Usage only allowed by the parsing modules!!!
***************************************************************/
{
  SIGNATURE Sig;
  symbol_CheckNoVariable(S);
  Sig = symbol_Signature(symbol_Index(S));
  S   = symbol_SignatureSymbol(symbol_Index(S), Type, symbol_Stat(S));
  Sig->info = S;
  return S;
}

static __inline__ int symbol_Arity(SYMBOL ActSymbol)
{
  return symbol_Signature(symbol_Index(ActSymbol))->arity;
}

static __inline__ NAT symbol_PositiveArity(SYMBOL ActSymbol)
{
  int arity = symbol_Arity(ActSymbol);
  if (arity < 0)
    return NAT_MAX;
  else
    return arity;
}

static __inline__ void symbol_SetArity(SYMBOL ActSymbol, int Arity)
{
  symbol_Signature(symbol_Index(ActSymbol))->arity = Arity;
}

static __inline__ BOOL symbol_Fixed(SYMBOL ActSymbol)
{
  return symbol_Signature(symbol_Index(ActSymbol))->fixed;
}

static __inline__ void symbol_SetFixed(SYMBOL ActSymbol, BOOL fixed)
{
  symbol_Signature(symbol_Index(ActSymbol))->fixed = fixed;
}

static __inline__ int symbol_ArbitraryArity(void)
{
  return -1;
}

static __inline__ const char* symbol_Name(SYMBOL ActSymbol)
{
  return symbol_Signature(symbol_Index(ActSymbol))->name;
}

static __inline__ NAT symbol_NameLength(SYMBOL ActSymbol)
{
  return symbol_Signature(symbol_Index(ActSymbol))->length;
}

static __inline__ int symbol_Info(SYMBOL ActSymbol)
{
  return symbol_Signature(symbol_Index(ActSymbol))->info;
}

static __inline__ int symbol_Weight(SYMBOL ActSymbol)
{
  return symbol_Signature(symbol_Index(ActSymbol))->weight;
}

static __inline__ void symbol_SetWeight(SYMBOL ActSymbol, int Weight)
{
  symbol_Signature(symbol_Index(ActSymbol))->weight = Weight;
}

void symbol_SetName(SYMBOL, char*);

static __inline__ LIST symbol_GeneratedBy(SYMBOL S)
{
  return symbol_Signature(symbol_Index(S))->generatedBy;
}

static __inline__ BOOL symbol_IsGeneratedBy(SYMBOL S1, SYMBOL S2)
{
  return list_PointerMember(symbol_GeneratedBy(S1), (POINTER)S2);
}

static __inline__ void symbol_SetGeneratedBy(SYMBOL S, LIST SymbolList)
{
  symbol_Signature(symbol_Index(S))->generatedBy = SymbolList;
}

static __inline__ void symbol_SetOrdering(PRECEDENCE P, SYMBOL ActSymbol,
					  int Ordering)
{
  int Index;

  Index = symbol_Index(ActSymbol);
  symbol_CheckIndexInRange(Index);
  P[Index] = Ordering;
}

static __inline__ void symbol_SetIncreasedOrdering(PRECEDENCE P, SYMBOL S)
{
  symbol_SetOrdering(P, S, symbol_GetIncreasedOrderingCounter());
}


static __inline__ BOOL symbol_PrecedenceGreater(PRECEDENCE P, SYMBOL S1, SYMBOL S2)
{
  return symbol_Ordering(P, S1) < symbol_Ordering(P, S2);
}

static __inline__ BOOL symbol_HasProperty(SYMBOL ActSymbol, SPROPERTY Property)
{
  return (symbol_Signature(symbol_Index(ActSymbol))->props & Property);
}

static __inline__ void symbol_AddProperty(SYMBOL ActSymbol, SPROPERTY Property)
{
  SIGNATURE S = symbol_Signature(symbol_Index(ActSymbol));
  S->props    = S->props | Property;
}

static __inline__ void symbol_RemoveProperty(SYMBOL ActSymbol, SPROPERTY Property)
{
  SIGNATURE S = symbol_Signature(symbol_Index(ActSymbol));
  if (S->props & Property)
    S->props = S->props - Property;
}

static __inline__ BOOL symbol_IsPredefined(SYMBOL Symbol)
{
  return (symbol_HasProperty(Symbol, PREDEFINED));
}

static __inline__ BOOL symbol_IsPredefinedPred(SYMBOL Symbol)
{
  return symbol_IsPredicate(Symbol) && symbol_IsPredefined(Symbol);	
}

static __inline__ BOOL symbol_IsBaseSort(SYMBOL Symbol)
{
  return (symbol_Arity(Symbol) == 1);
}

static __inline__ void symbol_ClearPrecedence(PRECEDENCE P)
{
  int i;
  const int clear = -42; /* Some negative number */

  for (i = 0; i < symbol__MAXSIGNATURE; i++)
    P[i] = clear;        
}

static __inline__ PRECEDENCE symbol_CreatePrecedence(void)
{
  PRECEDENCE P;

  P = memory_Malloc(sizeof(int[symbol__MAXSIGNATURE]));
  symbol_ClearPrecedence(P);
  return P;
}

static __inline__ void symbol_DeletePrecedence(PRECEDENCE P)
{
  memory_Free(P, sizeof(int[symbol__MAXSIGNATURE]));
}

static __inline__ void symbol_TransferPrecedence(PRECEDENCE Source,
						 PRECEDENCE Target)
  /* Copy settings from one precedence object to another */
{
  int i;

  for (i = 0; i < symbol__MAXSIGNATURE; i++)
    Target[i] = Source[i];
}

static __inline__ LIST symbol_DeleteSymbolFromList(LIST Symbols, SYMBOL S)
  /* Deletes all occurrences of <S> from the list */
{
  return list_DeleteElement(Symbols, (POINTER) S, 
			    (BOOL (*)(POINTER, POINTER)) symbol_Equal);
}

static __inline__ void symbol_DeleteSymbolList(LIST Symbols)
  /* The list AND the symbols within are deleted */
{
  list_DeleteWithElement(Symbols, (void (*)(POINTER))symbol_Delete);
}

/**************************************************************/
/* Symbol CONTEXT                                             */
/**************************************************************/

static __inline__ BOOL symbol_ContextIsClean(void)
{
  int i;
  for (i = 0; i < symbol__MAXSIGNATURE; i++)
    if (symbol_CONTEXT[i] != (SYMBOL)0)
      return FALSE;
  return TRUE;
}

static __inline__ void symbol_ContextClean(void)
{
  int i;
  for (i = 0; i < symbol__MAXSIGNATURE; i++)
    symbol_CONTEXT[i] = (SYMBOL)0;
}

static __inline__ BOOL symbol_ContextIsMapped(SYMBOL Symbol)
{
  int i;
  for (i = 0; i < symbol__MAXSIGNATURE; i++)
    if (symbol_Equal(symbol_CONTEXT[i],Symbol))
      return TRUE;
  return FALSE;
}

static __inline__ SYMBOL symbol_ContextGetValue(SYMBOL Symbol)
{
  int Index;

  Index = symbol_Index(Symbol);
  symbol_CheckIndexInRange(Index);
  return symbol_CONTEXT[Index];
}

static __inline__ void symbol_ContextSetValue(SYMBOL Symbol, SYMBOL Value)
{
  int Index;

  Index = symbol_Index(Symbol);
  symbol_CheckIndexInRange(Index);
  symbol_CONTEXT[Index] = Value;
}

static __inline__ void symbol_ContextClearValue(SYMBOL Symbol)
{
  symbol_ContextSetValue(Symbol, (SYMBOL)0);
}

static __inline__ BOOL symbol_ContextIsBound(SYMBOL Symbol)
{
  return (symbol_ContextGetValue(Symbol) != (SYMBOL)0);
}

/**************************************************************/
/* Symbol Output                                              */
/**************************************************************/

void   symbol_Print(SYMBOL);
void   symbol_PrintPrecedence(PRECEDENCE);
void   symbol_FPrintPrecedence(FILE*, PRECEDENCE);
void   symbol_FPrintDFGSignature(FILE*);
void   symbol_FPrint(FILE*, SYMBOL);
void   symbol_FPrintOtter(FILE*, SYMBOL);
void   symbol_PrintLn(SYMBOL);
void   symbol_PrintAll(void);

#endif