diff options
Diffstat (limited to 'test/spass/table.h')
-rw-r--r-- | test/spass/table.h | 101 |
1 files changed, 101 insertions, 0 deletions
diff --git a/test/spass/table.h b/test/spass/table.h new file mode 100644 index 00000000..e0024a40 --- /dev/null +++ b/test/spass/table.h @@ -0,0 +1,101 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * SIGNATURE TABLE * */ +/* * * */ +/* * $Module: TABLE * */ +/* * * */ +/* * Copyright (C) 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: 21527 $ * */ +/* $State$ * */ +/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $ * */ +/* $Author: duraid $ * */ +/* * * */ +/* * Contact: * */ +/* * Christoph Weidenbach * */ +/* * MPI fuer Informatik * */ +/* * Stuhlsatzenhausweg 85 * */ +/* * 66123 Saarbruecken * */ +/* * Email: weidenb@mpi-sb.mpg.de * */ +/* * Germany * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + +/* module manages signature tables i. e. tables of terms (including the empty */ +/* term NULL) where the lookup key is the tuple of top symbol index and */ +/* arguments' equivalence classes with respect to a partition p, the */ +/* _p-signature_ (sigtab_Index(top symbol), [arg 1] , ..., [arg n] ) */ +/* p p */ + +#ifndef _TABLE_ +#define _TABLE_ + + +/**************************************************************/ +/* Includes */ +/**************************************************************/ + +#include "term.h" +#include "partition.h" + + +/**************************************************************/ +/* Basic types */ +/**************************************************************/ + +typedef struct termarray { + TERM term; + int stamp; + struct termarray *child; +} *TERMARRAY; + +typedef struct table { + TERMARRAY ta, *pos; + int *posstamp, stampcounter, opbound, varbound, termbound; +} +*TABLE; + +/* a signature table is an "array of terms allocated by need" (i. e. a tree */ +/* where the nodes of the same layer represent array entries with the same */ +/* dimension), an array of positions in this "array", stamps for the */ +/* positions, the stamp counter and bounds for the operator symbol, variable */ +/* and term indices of the terms to be stored in the signature table (i. e. */ +/* for every such term its top symbol index has to be in [1, opbound] and the */ +/* term numbers of its arguments in [0, termbound] - or its variable index in */ +/* [1, varbound] if it is a variable) */ + + +/**************************************************************/ +/* Prototypes */ +/**************************************************************/ + +TABLE table_Null(void); +TABLE table_Create(int, int, int); +void table_Free(TABLE); +TABLE table_Init(TABLE, int, int, int); +TERM table_QueryAndEnter(TABLE, PARTITION, TERM); +TABLE table_Delete(TABLE, TERM); + + +#endif + |