| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * 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$ * */ |
| /* $State$ * */ |
| /* $Date$ * */ |
| /* $Author$ * */ |
| /* * * */ |
| /* * Contact: * */ |
| /* * Christoph Weidenbach * */ |
| /* * MPI fuer Informatik * */ |
| /* * Stuhlsatzenhausweg 85 * */ |
| /* * 66123 Saarbruecken * */ |
| /* * Email: weidenb@mpi-sb.mpg.de * */ |
| /* * Germany * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| /**************************************************************/ |
| /* Includes */ |
| /**************************************************************/ |
| |
| #include "table.h" |
| |
| |
| /**************************************************************/ |
| /* Inline functions */ |
| /**************************************************************/ |
| |
| static __inline__ int table_Index(SYMBOL symbol) |
| { |
| if (symbol_IsVariable(symbol)) |
| return -(int) symbol; |
| else |
| return symbol_Index(symbol); |
| } |
| |
| |
| static __inline__ TERM table_GetTerm(TERMARRAY ta) |
| { |
| return ta->term; |
| } |
| |
| |
| static __inline__ TERMARRAY table_SetTerm(TERMARRAY ta, TERM term) |
| { |
| ta->term = term; |
| return ta; |
| } |
| |
| |
| static __inline__ int table_GetStamp(TERMARRAY ta) |
| { |
| return ta->stamp; |
| } |
| |
| |
| static __inline__ TERMARRAY table_SetStamp(TERMARRAY ta, int stamp) |
| { |
| ta->stamp = stamp; |
| return ta; |
| } |
| |
| |
| static __inline__ TERMARRAY table_GetChild(TERMARRAY ta) |
| { |
| return ta->child; |
| } |
| |
| |
| static __inline__ TERMARRAY table_SetChild(TERMARRAY ta, TERMARRAY child) |
| { |
| ta->child = child; |
| return ta; |
| } |
| |
| |
| static __inline__ TERMARRAY table_GetTermarray(TABLE table) |
| { |
| return table->ta; |
| } |
| |
| |
| static __inline__ TABLE table_SetTermarray(TABLE table, TERMARRAY ta) |
| { |
| table->ta = ta; |
| return table; |
| } |
| |
| |
| static __inline__ TERMARRAY *table_GetPoss(TABLE table) |
| { |
| return table->pos; |
| } |
| |
| |
| static __inline__ TERMARRAY table_GetPos(TABLE table, int index) |
| { |
| return table_GetPoss(table)[index]; |
| } |
| |
| |
| static __inline__ TABLE table_SetPoss(TABLE table, TERMARRAY *ref) |
| { |
| table->pos = ref; |
| return table; |
| } |
| |
| |
| static __inline__ TABLE table_SetPos(TABLE table, int index, TERMARRAY ta) |
| { |
| table_GetPoss(table)[index] = ta; |
| return table; |
| } |
| |
| |
| static __inline__ int *table_GetPosstamps(TABLE table) |
| { |
| return table->posstamp; |
| } |
| |
| |
| static __inline__ int table_GetPosstamp(TABLE table, int index) |
| { |
| return table_GetPosstamps(table)[index]; |
| } |
| |
| |
| static __inline__ TABLE table_SetPosstamps(TABLE table, int *ref) |
| { |
| table->posstamp = ref; |
| return table; |
| } |
| |
| |
| static __inline__ TABLE table_SetPosstamp(TABLE table, int index, int stamp) |
| { |
| table_GetPosstamps(table)[index] = stamp; |
| return table; |
| } |
| |
| |
| static __inline__ int table_GetStampcounter(TABLE table) |
| { |
| return table->stampcounter; |
| } |
| |
| |
| static __inline__ TABLE table_SetStampcounter(TABLE table, int stampcounter) |
| { |
| table->stampcounter = stampcounter; |
| return table; |
| } |
| |
| |
| static __inline__ int table_GetOpbound(TABLE table) |
| { |
| return table->opbound; |
| } |
| |
| |
| static __inline__ TABLE table_SetOpbound(TABLE table, int opbound) |
| { |
| table->opbound = opbound; |
| return table; |
| } |
| |
| |
| static __inline__ int table_GetVarbound(TABLE table) |
| { |
| return table->varbound; |
| } |
| |
| |
| static __inline__ TABLE table_SetVarbound(TABLE table, int varbound) |
| { |
| table->varbound = varbound; |
| return table; |
| } |
| |
| |
| static __inline__ int table_GetTermbound(TABLE table) |
| { |
| return table->termbound; |
| } |
| |
| |
| static __inline__ TABLE table_SetTermbound(TABLE table, int termbound) |
| { |
| table->termbound = termbound; |
| return table; |
| } |
| |
| |
| static __inline__ BOOL table_LegalPosIndex(TABLE table, int index) |
| { |
| return 0 <= index && index <= table_GetTermbound(table); |
| } |
| |
| |
| static __inline__ BOOL table_Stamped(TABLE table, TERMARRAY ta) |
| { |
| return table_GetStamp(ta) == table_GetStampcounter(table); |
| } |
| |
| |
| static __inline__ TERMARRAY table_DelayedInit(TABLE table, TERMARRAY ta) |
| /*************************************************************** |
| INPUT: a table and a termarray |
| RETURNS: the (now stamped) termarray |
| EFFECT: partially initializes table by setting the |
| termarray's entry to the empty term |
| ***************************************************************/ |
| { |
| if (!table_Stamped(table, ta)) { |
| table_SetTerm(ta, term_Null()); |
| table_SetStamp(ta, table_GetStampcounter(table)); |
| } |
| return ta; |
| } |
| |
| |
| static __inline__ BOOL table_PosStamped(TABLE table, int index) |
| { |
| return table_GetPosstamp(table, index) == table_GetStampcounter(table); |
| } |
| |
| |
| static __inline__ int table_DelayedPosInit(TABLE table, int index) |
| /*************************************************************** |
| INPUT: a table and a position index |
| RETURNS: the (now stamped) position index |
| EFFECT: partially initializes table by setting the indexed |
| position to the empty pointer, which means that the |
| term with this index is not stored in table |
| ***************************************************************/ |
| { |
| if (!table_PosStamped(table, index)) { |
| table_SetPos(table, index, (TERMARRAY) NULL); |
| table_SetPosstamp(table, index, table_GetStampcounter(table)); |
| } |
| return index; |
| } |
| |
| |
| /**************************************************************/ |
| /* Functions */ |
| /**************************************************************/ |
| |
| TABLE table_Null(void) |
| { |
| return (TABLE) NULL; |
| } |
| |
| |
| TABLE table_Create(int opbound, int varbound, int termbound) |
| /*************************************************************** |
| INPUT: 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) |
| RETURNS: a new (and empty) signature table |
| ***************************************************************/ |
| { |
| TABLE result; |
| |
| #ifdef CHECK |
| if (opbound < 0) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In table_Create: negative opbound."); |
| misc_FinishErrorReport(); |
| } |
| if (varbound < 0) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In table_Create: negative varbound."); |
| misc_FinishErrorReport(); |
| } |
| if (termbound < 0) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In table_Create: negative termbound."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| result = (TABLE) memory_Malloc(sizeof(struct table)); |
| table_SetTermarray(result, (TERMARRAY) memory_Calloc ( |
| opbound + varbound + 1, |
| sizeof(struct termarray) |
| ) + varbound); |
| /* move pointer to the middle of the array to allow negative indices */ |
| table_SetPoss( |
| result, |
| (TERMARRAY*) memory_Malloc((termbound + 1) * sizeof(TERMARRAY)) |
| ); |
| table_SetPosstamps(result, (int*) memory_Calloc(termbound + 1, sizeof(int))); |
| table_SetOpbound(result, opbound); |
| table_SetVarbound(result, varbound); |
| table_SetTermbound(result, termbound); |
| table_SetStampcounter(result, 1); |
| return result; |
| } |
| |
| |
| static void table_FreeTermarray(TERMARRAY ta, int size) |
| /*************************************************************** |
| INPUT: the termarray to free and its size |
| EFFECT: recursively frees the tree structure allocated for the |
| signature array |
| ***************************************************************/ |
| { |
| int i; |
| |
| if (ta) { |
| for (i = 0; i < size; i++) |
| table_FreeTermarray(table_GetChild(ta + i), size); |
| memory_Free(ta, size * sizeof(struct termarray)); |
| } |
| } |
| |
| |
| void table_Free(TABLE table) |
| { |
| int i; |
| |
| if (table != table_Null()) { |
| for (i = -table_GetVarbound(table); i <= table_GetOpbound(table); i++) |
| table_FreeTermarray( |
| table_GetChild(table_GetTermarray(table) + i), |
| table_GetTermbound(table) + 1 |
| ); |
| memory_Free( |
| table_GetTermarray(table) - table_GetVarbound(table), |
| (table_GetOpbound(table) + table_GetVarbound(table) + 1) * sizeof(struct |
| termarray) |
| ); |
| memory_Free( |
| table_GetPoss(table), |
| (table_GetTermbound(table) + 1) * sizeof(TERMARRAY) |
| ); |
| memory_Free( |
| table_GetPosstamps(table), |
| (table_GetTermbound(table) + 1) * sizeof(int) |
| ); |
| memory_Free(table, sizeof(struct table)); |
| } |
| } |
| |
| |
| TABLE table_Init(TABLE table, int opbound, int varbound, int termbound) |
| /*************************************************************** |
| INPUT: the table to recycle 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) |
| RETURNS: a cleaned up signature table |
| CAUTION: potentially frees the old table, therefore must be |
| called inside of an assignment like: |
| table = table_Init(table, ...) |
| ***************************************************************/ |
| { |
| int opmax, varmax, termmax, i; |
| TERMARRAY old; |
| |
| #ifdef CHECK |
| if (opbound < 0) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In table_Init: negative opbound."); |
| misc_FinishErrorReport(); |
| } |
| if (varbound < 0) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In table_Init: negative varbound."); |
| misc_FinishErrorReport(); |
| } |
| if (termbound < 0) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In table_Init: negative termbound."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| opmax = table_GetOpbound(table) > opbound ? table_GetOpbound(table) : |
| opbound; |
| varmax = table_GetVarbound(table) > varbound ? table_GetVarbound(table) : |
| varbound; |
| termmax = table_GetTermbound(table) > termbound ? table_GetTermbound(table) : |
| termbound; |
| table_SetStampcounter(table, table_GetStampcounter(table) + 1); |
| |
| /* in case of stamp overflow or too small termarray nodes get a new table: */ |
| if (table_GetStampcounter(table)<=0 || termbound>table_GetTermbound(table)) { |
| table_Free(table); |
| return table_Create(opmax, varmax, termmax); |
| } |
| |
| /* if only the top layer of the tree is too small get a larger top layer: */ |
| else if (opbound+varbound > table_GetOpbound(table)+table_GetVarbound(table)){ |
| old = table_GetTermarray(table); |
| table_SetTermarray(table, (TERMARRAY) memory_Calloc( |
| opmax + varmax + 1, |
| sizeof(struct termarray) |
| ) + varmax); |
| for (i = -table_GetVarbound(table); i <= table_GetOpbound(table); i++) |
| table_SetChild(table_GetTermarray(table) + i, table_GetChild(old + i)); |
| memory_Free( |
| old - table_GetVarbound(table), |
| (table_GetOpbound(table) + table_GetVarbound(table) + 1) * sizeof(struct |
| termarray) |
| ); |
| table_SetOpbound(table, opmax); |
| table_SetVarbound(table, varmax); |
| return table; |
| } |
| |
| else { |
| |
| /* move pointer to termarray's new middle: */ |
| table_SetTermarray( |
| table, |
| table_GetTermarray(table) + table_GetOpbound(table) - opbound |
| ); |
| |
| table_SetVarbound( |
| table, |
| table_GetOpbound(table) + table_GetVarbound(table) - opbound |
| ); |
| table_SetOpbound(table, opbound); |
| return table; |
| } |
| } |
| |
| |
| TERM table_QueryAndEnter(TABLE table, PARTITION p, TERM term) |
| /*************************************************************** |
| RETURNS: a term with the same p-signature (sigtab_Index(top |
| symbol), [arg 1] , ..., [arg n] ) as term - or the |
| p p |
| empty term if no such term exists |
| EFFECT: term enters table in the latter case |
| ***************************************************************/ |
| { |
| TERMARRAY ta; |
| LIST terms; |
| |
| #ifdef CHECK |
| if (part_Size(p) - 1 > table_GetTermbound(table)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In table_QueryAndEnter: partition not suitable."); |
| misc_FinishErrorReport(); |
| } |
| if (table_Index(term_TopSymbol(term)) > table_GetOpbound(table)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport |
| ("\n In table_QueryAndEnter: term's operation symbol out of bounds."); |
| misc_FinishErrorReport(); |
| } |
| if (table_Index(term_TopSymbol(term)) < -table_GetVarbound(table)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In table_QueryAndEnter: variable out of bounds."); |
| misc_FinishErrorReport(); |
| } |
| if (!table_LegalPosIndex(table, term_Size(term))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In table_QueryAndEnter: term out of bounds."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| ta = table_GetTermarray(table) + table_Index(term_TopSymbol(term)); |
| for (terms = term_ArgumentList(term); !list_Empty(terms); terms = |
| list_Cdr(terms)) { |
| if (!table_GetChild(ta)) |
| table_SetChild(ta, (TERMARRAY) memory_Calloc ( |
| table_GetTermbound(table) + 1, |
| sizeof(struct termarray) |
| )); |
| ta = table_GetChild(ta) + part_Find(p, term_Size(list_Car(terms))); |
| } |
| table_DelayedInit(table, ta); |
| if (table_GetTerm(ta)) |
| return table_GetTerm(ta); |
| else { |
| table_SetTerm(ta, term); |
| table_SetPos(table, table_DelayedPosInit(table, term_Size(term)), ta); |
| return term_Null(); |
| } |
| } |
| |
| |
| TABLE table_Delete(TABLE table, TERM term) |
| /*************************************************************** |
| EFFECT: if term has entered table before, it is deleted |
| ***************************************************************/ |
| { |
| int no; |
| |
| #ifdef CHECK |
| if (!table_LegalPosIndex(table, term_Size(term))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In table_Delete: illegal table access."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| no = term_Size(term); |
| table_DelayedPosInit(table, no); |
| if (table_GetPos(table, no)) { |
| |
| #ifdef CHECK |
| if (!table_Stamped(table, table_GetPos(table, no))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In table_Delete: table corrupted."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| table_SetTerm(table_GetPos(table, no), term_Null()); |
| table_SetPos(table, no, (TERMARRAY) NULL); |
| } |
| return table; |
| } |
| |