diff options
Diffstat (limited to 'test/spass/tableau.h')
| -rw-r--r-- | test/spass/tableau.h | 292 |
1 files changed, 292 insertions, 0 deletions
diff --git a/test/spass/tableau.h b/test/spass/tableau.h new file mode 100644 index 0000000..f04a826 --- /dev/null +++ b/test/spass/tableau.h @@ -0,0 +1,292 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * TABLEAUS * */ +/* * * */ +/* * $Module: TABLEAU * */ +/* * * */ +/* * Copyright (C) 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: 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$ */ + +#ifndef _TABLEAU_ +#define _TABLEAU_ + + +#include "list.h" +#include "clause.h" + +typedef struct TABLEAU_HELP { + LIST Clauses; /* all clauses generated on the split level */ + CLAUSE SplitClause; /* this levels split clause */ + + CLAUSE LeftSplitClause; /* first clause generated by split */ + LIST RightSplitClauses; /* other clauses generated by split */ + + struct TABLEAU_HELP* LeftBranch; /* branch corresponding to first split clause */ + struct TABLEAU_HELP* RightBranch; /* branch corresponding to other split clauses */ + + int Label; +} TABLEAU_NODE, *TABLEAU; + + +typedef struct { + TABLEAU *Path; /* An array of tableaux */ + int Length; + int MaxLength; + +} TABPATH_NODE, *TABPATH; + +/* tableau output formats */ +typedef enum { DAVINCI, XVCG } GRAPHFORMAT; + + +TABPATH tab_PathCreate(int, TABLEAU); +void tab_PathDelete(TABPATH); +BOOL tab_PathContainsClause(TABPATH, CLAUSE); +void tab_AddClauseOnItsLevel(CLAUSE, TABPATH); +void tab_AddSplitAtCursor(TABPATH, BOOL); +BOOL tab_IsClosed(TABLEAU); +TABLEAU tab_PruneClosedBranches(TABLEAU, LIST*); +int tab_Depth(TABLEAU); +void tab_SetSplitLevels(TABLEAU T); +TABLEAU tab_RemoveIncompleteSplits(TABLEAU, LIST*); +void tab_PathDelete(TABPATH); +void tab_Delete(TABLEAU); +void tab_ToClauseList(TABLEAU, LIST*); +void tab_GetEarliestEmptyClauses(TABLEAU, LIST*); +void tab_WriteTableau(TABLEAU, const char*, GRAPHFORMAT); +void tab_CheckEmpties(TABLEAU); +void tab_GetAllEmptyClauses(TABLEAU, LIST*); +void tab_LabelNodes(TABLEAU); + +/* inline functions for tableau paths */ + +static __inline__ int tab_PathLength(TABPATH TabPath) +{ + return TabPath->Length; +} + +static __inline__ TABLEAU tab_PathNthNode(TABPATH TabPath, int n) +{ +#ifdef CHECK + if (n > TabPath->MaxLength) { + misc_StartErrorReport(); + misc_ErrorReport("\n In tab_PathNthNode:"); + misc_ErrorReport(" Path length is %d,", tab_PathLength(TabPath)); + misc_ErrorReport("\nnode %d was requested.\n", n); + misc_FinishErrorReport(); + } +#endif + + return TabPath->Path[n]; +} + +static __inline__ TABPATH tab_PathPush(TABLEAU Tab, TABPATH TabPath) +{ + TabPath->Length++; + TabPath->Path[TabPath->Length] = Tab; + +#ifdef CHECK + if (TabPath->Length > TabPath->MaxLength) { + misc_StartErrorReport(); + misc_ErrorReport("\n In tab_PathPush: Maximum path length %d exceeded\n", + TabPath->MaxLength); + misc_FinishErrorReport(); + } +#endif + + return TabPath; +} + +static __inline__ TABLEAU tab_EmptyTableau(void) +{ + return (TABLEAU)NULL; +} + +static __inline__ TABPATH tab_PathPop(TABPATH TabPath) +{ +#ifdef CHECK + if (TabPath->Length <= 0) { + misc_StartErrorReport(); + misc_ErrorReport("\n In tab_PathPop: Popping from empty path.\n"); + misc_FinishErrorReport(); + } +#endif + + TabPath->Path[TabPath->Length--] = tab_EmptyTableau(); + + return TabPath; +} + +static __inline__ BOOL tab_PathEmpty(TABPATH P) +{ + return (tab_PathLength(P) == 0); +} + +static __inline__ TABLEAU tab_CreateNode(void) +{ + TABLEAU Node; + + Node = (TABLEAU)memory_Malloc(sizeof(TABLEAU_NODE)); + Node->RightBranch = (TABLEAU)NULL; + Node->LeftBranch = (TABLEAU)NULL; + Node->SplitClause = (CLAUSE)NULL; + Node->LeftSplitClause = (CLAUSE)NULL; + Node->RightSplitClauses = list_Nil(); + + Node->Clauses = list_Nil(); + +#ifdef USE_LABEL + Node->Label = 0; +#endif + + return Node; +} + +static __inline__ TABPATH tab_PathPrefix(int Level, TABPATH TabPath) +{ + TabPath->Length = Level; + return TabPath; +} + +static __inline__ TABLEAU tab_PathTop(TABPATH Path) +{ + return tab_PathNthNode(Path, tab_PathLength(Path)); +} + + +static __inline__ BOOL tab_IsEmpty(TABLEAU Tab) +{ + return (Tab == tab_EmptyTableau()); +} + +static __inline__ TABLEAU tab_RightBranch(TABLEAU Tab) +{ + return Tab->RightBranch; +} + +static __inline__ TABLEAU tab_LeftBranch(TABLEAU Tab) +{ + return Tab->LeftBranch; +} + +static __inline__ void tab_SetRightBranch(TABLEAU Tab, TABLEAU SubTab) +{ + Tab->RightBranch = SubTab; +} + +static __inline__ void tab_SetLeftBranch(TABLEAU Tab, TABLEAU SubTab) +{ + Tab->LeftBranch = SubTab; +} + +static __inline__ BOOL tab_RightBranchIsEmpty(TABLEAU Tab) +{ + return (Tab->RightBranch == tab_EmptyTableau()); +} + +static __inline__ BOOL tab_LeftBranchIsEmpty(TABLEAU Tab) +{ + return (Tab->LeftBranch == tab_EmptyTableau()); +} + +static __inline__ CLAUSE tab_SplitClause(TABLEAU Tab) +{ + return Tab->SplitClause; +} + +static __inline__ void tab_SetSplitClause(TABLEAU Tab, CLAUSE C) +{ + Tab->SplitClause = C; +} + +static __inline__ BOOL tab_HasSplit(TABLEAU T) +{ + return (tab_SplitClause(T) != clause_Null()); +} + +static __inline__ void tab_AddClause(CLAUSE C,TABLEAU T) +{ + T->Clauses = list_Cons(C,T->Clauses); +} + +static __inline__ LIST tab_Clauses(TABLEAU T) +{ + return T->Clauses; +} + +static __inline__ void tab_SetClauses(TABLEAU T, LIST Clauses) +{ + T->Clauses = Clauses; +} + +static __inline__ CLAUSE tab_LeftSplitClause(TABLEAU T) +{ + return T->LeftSplitClause; +} + +static __inline__ void tab_SetLeftSplitClause(TABLEAU T, CLAUSE C) +{ + T->LeftSplitClause = C; +} + + +static __inline__ LIST tab_RightSplitClauses(TABLEAU T) +{ + return T->RightSplitClauses; +} + + +static __inline__ void tab_SetRightSplitClauses(TABLEAU T, LIST L) +{ + T->RightSplitClauses = L; +} + +static __inline__ void tab_AddRightSplitClause(TABLEAU T, CLAUSE C) +{ + T->RightSplitClauses = list_Cons(C, T->RightSplitClauses); +} + +static __inline__ BOOL tab_IsLeaf(TABLEAU T) +{ + return (tab_RightBranchIsEmpty(T) && tab_LeftBranchIsEmpty(T)); +} + +#endif |