diff options
Diffstat (limited to 'test/spass/component.c')
-rw-r--r-- | test/spass/component.c | 266 |
1 files changed, 266 insertions, 0 deletions
diff --git a/test/spass/component.c b/test/spass/component.c new file mode 100644 index 00000000..def8e30c --- /dev/null +++ b/test/spass/component.c @@ -0,0 +1,266 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * COMPONENTS OF CLAUSES * */ +/* * * */ +/* * $Module: COMPONENT * */ +/* * * */ +/* * Copyright (C) 1996, 1998, 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 * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +/* $RCSfile$ */ + +#include "term.h" +#include "component.h" + + +CLITERAL literal_Create(BOOL used, int index, LIST varlist) +/********************************************************** + INPUT: A boolean used, an integer index and a list varlist. + RETURNS: A LITERAL is created. + MEMORY: The boolean, integer and varlist are no copies. +*** ********************************************************/ +{ + CLITERAL literal; + + literal = (CLITERAL)memory_Malloc(sizeof(CLITERAL_NODE)); + literal_PutUsed(literal,used); + literal_PutLitIndex(literal,index); + literal_PutLitVarList(literal,varlist); + + return literal; +} + + +void literal_Delete(CLITERAL literal) +/********************************************************** + INPUT: A literal. + RETURNS: None. + MEMORY: Deletes the LITERAL and frees the storage. +***********************************************************/ +{ + list_Delete(literal_GetLitVarList(literal)); + literal_Free(literal); +} + + +LITPTR litptr_Create(LIST Indexlist, LIST Termsymblist) +/********************************************************** + INPUT: A list indexes and a list of terms, i.e. a list of integers. + RETURNS: A LITPTR structure is created. + MEMORY: The integers in the created structure are the integers + in indexList, no copies. +***********************************************************/ +{ + LITPTR lit_ptr; + LIST Scan,varlist; + CLITERAL literal; + int index,n,k; + + n = list_Length(Indexlist); + + lit_ptr = (LITPTR)memory_Malloc(sizeof(LITPTR_NODE)); + litptr_SetLength(lit_ptr, n); + + if (n > 0) { + lit_ptr->litptr = (CLITERAL *)memory_Malloc(n * sizeof(CLITERAL)); + + k = 0; + for (Scan = Indexlist; !list_Empty(Scan); Scan = list_Cdr(Scan)) { + index = (int)list_Car(Scan); + varlist = (LIST)list_Car(Termsymblist); + Termsymblist = list_Cdr(Termsymblist); + literal = literal_Create(FALSE,index,varlist); + + litptr_SetLiteral(lit_ptr, k, literal); + + k++; + } + } else + lit_ptr->litptr = NULL; + + return lit_ptr; +} + + +void litptr_Delete(LITPTR lit_ptr) +/********************************************************** + INPUT: A pointer to LITPTR. + MEMORY: Deletes the LITPTR and frees the storage. +***********************************************************/ +{ + int n,i; + + n = litptr_Length(lit_ptr); + + if (n > 0) { + for (i = 0; i < n; i++) + literal_Delete(litptr_Literal(lit_ptr,i)); + + memory_Free(lit_ptr->litptr, sizeof(CLITERAL) * n); + memory_Free(lit_ptr, sizeof(LITPTR_NODE)); + } else + memory_Free(lit_ptr, sizeof(LITPTR_NODE)); +} + + +void litptr_Print(LITPTR lit_ptr) +/************************************************************** + INPUT: A term. + RETURNS: void. + SUMMARY: Prints any term to stdout. + CAUTION: Uses the other term_Output functions. +***************************************************************/ +{ + int i,n; + + n = litptr_Length(lit_ptr); + /*n = lit_ptr->length;*/ + + if (n > 0) { + printf("\nlength of LITPTR: %d\n",n); + for (i = 0; i < n; i++) { + printf("Entries of literal %d : \n",i); + puts("----------------------"); + fputs("used:\t\t", stdout); + + if (literal_GetUsed(litptr_Literal(lit_ptr,i))) + /*if (lit_ptr->litptr[i]->used)*/ + puts("TRUE"); + else + puts("FALSE"); + printf("litindex:\t%d\n", + literal_GetLitIndex(litptr_Literal(lit_ptr,i))); + fputs("litvarlist:\t", stdout); + list_Apply((void (*)(POINTER)) symbol_Print, + literal_GetLitVarList(litptr_Literal(lit_ptr,i))); + puts("\n"); + } + }else + puts("No entries in litptr structure"); +} + + +BOOL litptr_AllUsed(LITPTR lit_ptr) +/************************************************************** + INPUT: A LITPTR. + RETURNS: TRUE if every literal in the LITPTR is used and + FALSE otherwise. +***************************************************************/ +{ + int n,i; + + n = litptr_Length(lit_ptr); + + for (i = 0; i < n; i++) + if (!(literal_GetUsed(litptr_Literal(lit_ptr,i)))) + return FALSE; + + return TRUE; +} + + +LIST subs_CompList(LITPTR litptr) +/********************************************************** + INPUT: A pointer litptr. + RETURNS: A list with indexes which represents the first component of + with respect to the actual bindings and to litptr. + CAUTION: The structure to which litptr points to + is changed destructively in the used slot. +***********************************************************/ +{ + BOOL found,hasinter; + LIST scan,complist,compindexlist; + int n,i,j,lit; + + compindexlist = list_Nil(); /* the result will be placed into this list */ + complist = list_Nil(); /* added afterwards */ + n = litptr_Length(litptr); + + if (n > 0) { + for (j = 0; j < n; j++) { + printf("\nj = %d\n",j); + if (!literal_GetUsed(litptr_Literal(litptr,j))){ + complist = list_Nil(); + complist = list_Cons((POINTER)j,complist); + compindexlist = list_Cons((POINTER)(litptr->litptr[j]->litindex), + compindexlist); + literal_PutUsed(litptr_Literal(litptr,j), TRUE); + j = n+1; + printf("\nj == %d\n",j); + } + } + + if (j == n){ + list_Delete(complist); /* There is no more component */ + return compindexlist; /* should be empty here */ + } + + found = TRUE; + while (found) { + found = FALSE; + for (scan = complist; !list_Empty(scan); scan = list_Cdr(scan)) { + lit = (int)list_Car(scan); + for (i = 0; i < n; i++) { + if (!literal_GetUsed(litptr_Literal(litptr,i))) { + printf("lit = %d\n",lit); + printf("i = %d\n",i); + + hasinter = list_HasIntersection(litptr->litptr[lit]->litvarlist, + litptr->litptr[i]->litvarlist); + + if (hasinter) { + puts("hasinter = TRUE"); + complist = list_Cons((POINTER)i,complist); + compindexlist = list_Cons((POINTER)(litptr->litptr[i]->litindex),compindexlist); + literal_PutUsed(litptr_Literal(litptr,i), TRUE); + found = TRUE; + } + } + } + } + + if (!found) { /* one component is finished */ + list_Delete(complist); + found = FALSE; + } + } + } + + return compindexlist; +} |