/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *                    ST INDEXING                         * */
/* *                                                        * */
/* *  $Module:   ST                                         * */ 
/* *                                                        * */
/* *  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$ */

#ifndef _ST_
#define _ST_

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

#include "foldfg.h"
#include "term.h"
#include "symbol.h"
#include "list.h"

#include "subst.h"
#include "unify.h"

/**************************************************************/
/* Data Structures                                            */
/**************************************************************/

typedef enum {st_NOP,             st_UNIFIER,    st_GEN,
	      st_GENPRETEST,      st_INSTANCE,   st_INSTANCEPRETEST
}  st_RETRIEVAL_TYPE;

typedef enum {st_STANDARD, st_NOC} st_WHERE_TYPE;

typedef unsigned short int st_MINMAX;


/**************************************************************/
/* Type st_INDEX and Inline Functions                         */
/**************************************************************/

typedef struct st {
  SUBST     subst;
  LIST      subnodes;
  LIST      entries;
  st_MINMAX max, min;
} st_INDEX_NODE, *st_INDEX;


static __inline__ st_INDEX st_Get(void)
{
  return (st_INDEX) memory_Malloc(sizeof(st_INDEX_NODE));
}

static __inline__ void st_Free(st_INDEX ST)
{
  memory_Free(ST, sizeof(st_INDEX_NODE));
}

static __inline__ SUBST st_Subst(st_INDEX ST)
{
  return ST->subst;
}

static __inline__ LIST st_Entries(st_INDEX ST)
{
  return ST->entries;
}

static __inline__ LIST st_Subnodes(st_INDEX ST)
{
  return ST->subnodes;
}

static __inline__ st_MINMAX st_Max(st_INDEX ST)
{
  return ST->max;
}

static __inline__ void st_SetMax(st_INDEX ST, st_MINMAX Value)
{
  ST->max = Value;
}

static __inline__ st_MINMAX st_Min(st_INDEX ST)
{
  return ST->min;
}

static __inline__ void st_SetMin(st_INDEX ST, st_MINMAX Value)
{
  ST->min = Value;
}

static __inline__ BOOL st_IsLeaf(st_INDEX ST)
{
  return !list_Empty(st_Entries(ST));
}

static __inline__ BOOL st_IsInner(st_INDEX ST)
{
  return !list_Empty(st_Subnodes(ST));
}

static __inline__ BOOL st_Empty(st_INDEX ST)
{
  return (ST == NULL || (!st_IsLeaf(ST) && !st_IsInner(ST)));
}

static __inline__ BOOL st_Exist(st_INDEX ST)
{
  return (ST != NULL && (st_IsLeaf(ST) || st_IsInner(ST)));
}

static __inline__ void st_SetNode(st_INDEX Index, SUBST Subst,
				  LIST Subnodes, LIST Entries)
{
  Index->subst    = Subst;
  Index->subnodes = Subnodes;
  Index->entries  = Entries;
}

static __inline__ st_INDEX st_CreateNode(SUBST Subst, LIST Subnodes,
					 LIST Entries)
{
  st_INDEX index;

  index = st_Get();
  st_SetNode(index, Subst, Subnodes, Entries);

  return index;
}


typedef enum {st_EMPTY = 1, st_FCT, st_CONST, st_VAR,
	      st_STAR, st_FIRST} NODETYPE;


/**************************************************************/
/* A special ST-Stack for sequential retrieval operations     */
/**************************************************************/

#define st_STACKSIZE 1000

typedef POINTER ST_STACK[st_STACKSIZE];

extern ST_STACK st_STACK;
extern int      st_STACKPOINTER;
extern int      st_STACKSAVE;

/* Stack operations */

static __inline__ void st_StackInit(void)
{
  st_STACKPOINTER = 0;
}

static __inline__ void st_StackPush(POINTER Entry)
{
#ifdef CHECK
  if (st_STACKPOINTER >= st_STACKSIZE) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In st_StackPush: ST-Stack Overflow!\n");
    misc_FinishErrorReport();
  }
#endif
  
  st_STACK[st_STACKPOINTER++] = Entry;
}

static __inline__ void st_StackPop(void)
{
  --st_STACKPOINTER;
}

static __inline__ POINTER st_StackPopResult(void)
{
  return st_STACK[--st_STACKPOINTER];
}

static __inline__ void st_StackNPop(int N)
{
  st_STACKPOINTER -= N;
}

static __inline__ POINTER st_StackTop(void)
{
  return st_STACK[st_STACKPOINTER - 1];
}

static __inline__ POINTER st_StackNthTop(int N)
{
  return st_STACK[st_STACKPOINTER - (1 + N)];
}

static __inline__ void st_StackRplacTop(POINTER Entry)
{
  st_STACK[st_STACKPOINTER - 1] = Entry;
}

static __inline__ void st_StackRplacNthTop(int N, POINTER Entry)
{
  st_STACK[st_STACKPOINTER - (1 + N)] = Entry;
}

static __inline__ void st_StackRplacNth(int N, POINTER Entry)
{
  st_STACK[N] = Entry;
}

static __inline__ int st_StackBottom(void)
{
  return st_STACKPOINTER;
}

static __inline__ void st_StackSetBottom(int Pointer)
{
  st_STACKPOINTER = Pointer;
}

static __inline__ BOOL st_StackEmpty(int Pointer)
{
  return st_STACKPOINTER == Pointer;
}


/**************************************************************/
/* Functions for Creation and Deletion of an st_INDEX         */
/**************************************************************/

st_INDEX st_IndexCreate(void); 
void     st_IndexDelete(st_INDEX);

/**************************************************************/
/* Add and Remove Entries to an st_INDEX                      */
/**************************************************************/

void     st_EntryCreate(st_INDEX, POINTER, TERM, const CONTEXT);
BOOL     st_EntryDelete(st_INDEX, POINTER, TERM, const CONTEXT);

/**************************************************************/
/* Functions for Retrieval in the Index                       */
/**************************************************************/

LIST     st_GetUnifier(CONTEXT, st_INDEX, CONTEXT, TERM);
LIST     st_GetGen(CONTEXT, st_INDEX, TERM);
LIST     st_GetGenPreTest(CONTEXT, st_INDEX, TERM);
LIST     st_GetInstance(CONTEXT, st_INDEX, TERM);
LIST     st_GetInstancePreTest(CONTEXT, st_INDEX, TERM);

void     st_CancelExistRetrieval(void);

POINTER  st_ExistUnifier(CONTEXT, st_INDEX, CONTEXT, TERM);
POINTER  st_ExistGen(CONTEXT, st_INDEX, TERM);
POINTER  st_ExistGenPreTest(CONTEXT, st_INDEX, TERM);
POINTER  st_ExistInstance(CONTEXT, st_INDEX, TERM);
POINTER  st_ExistInstancePreTest(CONTEXT, st_INDEX, TERM);

POINTER  st_NextCandidate(void);

/**************************************************************/
/* Function for Output                                        */
/**************************************************************/

void     st_Print(st_INDEX, void (*)(POINTER));

#endif