| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * SORTED REASONING * */ |
| /* * * */ |
| /* * $Module: SORT * */ |
| /* * * */ |
| /* * 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 _SORT_ |
| #define _SORT_ |
| |
| #include "clause.h" |
| #include "unify.h" |
| #include "hash.h" |
| #include "subsumption.h" |
| |
| |
| /**************************************************************/ |
| /* Data Structures and Constants */ |
| /**************************************************************/ |
| |
| /* Objects of type SORT are used to store the sort information */ |
| /* for terms. SORT is a list of NODE's */ |
| |
| typedef LIST SORT; |
| /* List of sort nodes */ |
| |
| typedef LIST SOJU; |
| /* Pair: First Component Sort, Second Component Condition */ |
| |
| typedef enum {SORTEQNONE=1, SORTEQDECR=2, SORTEQMANY=3} STR; |
| /* The overall result of an sort theory analysis with respect to equations */ |
| |
| typedef struct CONDITION_HELP { |
| SYMBOL var; |
| LIST constraint; |
| LIST antecedent; |
| LIST succedent; |
| LIST clauses; |
| } CONDITION_NODE,*CONDITION; |
| |
| /* This data structure collects the conditions from conditioned subsort clauses */ |
| /* The constraint, antecedent, succedent lists contain lists of atoms used to */ |
| /* derive the subsort relationship that come from clauses. */ |
| |
| |
| typedef struct NODE_HELP { |
| LIST links; |
| NAT mark; |
| NAT start; |
| NAT extra; |
| LIST conditions; |
| SYMBOL symbol; |
| } NODE_NODE,*NODE; |
| |
| /* This is a node from the subsort graph with outgoing links the represented */ |
| /* sort symbol and a mark indicating whether the node is already visited,i.e, */ |
| /* it is TRUE. Whereas start indicates whether the node was put true right */ |
| /* from the beginning. Conditions contains a list of conditions needed to set */ |
| /* the node true. */ |
| |
| typedef struct SLINK_HELP { |
| LIST input; |
| NODE output; |
| int card; |
| int fire; |
| LIST constraint; |
| LIST antecedent; |
| LIST succedent; |
| SYMBOL var; |
| CLAUSE clause; |
| } SLINK_NODE,*SLINK; |
| |
| /* This is a link in the subsort graph, with a list of input nodes that have */ |
| /* to become true in order to fire the link and set the output node TRUE */ |
| /* constraint, antecedent, succedent literals are the extra literals of */ |
| /* <clause> and <var> is the subsort variable. It is always assumed that the */ |
| /* subsort variable is the maximal variable with respect to the constraint, */ |
| /* antecedent and succedent literals. */ |
| |
| typedef struct SORTTHEORY_HELP { |
| st_INDEX index; |
| NODE basesorttable[symbol__MAXSIGNATURE]; |
| LIST suborigcls; |
| LIST termorigcls; |
| NAT mark; |
| } SORTTHEORY_NODE,*SORTTHEORY; |
| |
| /* The index contains the term declarations mapped to their possibly */ |
| /* approximated term declarations of inserted clauses. The subsort declarations*/ |
| /* are handled by a specific graph initiated over the base sorts. There is */ |
| /* one node in the graph for every base sort (basesorttable) and links */ |
| /* correspond to subsort declaration clauses */ |
| /* The mark is used in the subsort graph to detect already visited nodes. */ |
| /* The lists suborigcls and termorigcls map original clauses to sort theory */ |
| /* clauses to links/terms respectively. They contain triples of this kind */ |
| |
| |
| |
| /**************************************************************/ |
| /* Extern */ |
| /**************************************************************/ |
| |
| void sort_ConditionDelete(CONDITION); |
| CONDITION sort_ConditionCopy(CONDITION); |
| |
| |
| /**************************************************************/ |
| /* Macros */ |
| /**************************************************************/ |
| |
| static __inline__ SORT sort_TopSort(void) |
| { |
| return list_Nil(); |
| } |
| |
| static __inline__ BOOL sort_IsTopSort(SORT S) |
| { |
| return list_Empty(S); |
| } |
| |
| static __inline__ SORT sort_Copy(SORT S) |
| { |
| return list_Copy(S); |
| } |
| |
| static __inline__ void sort_DeleteOne(SORT S) |
| { |
| list_Delete(S); |
| } |
| |
| static __inline__ SORT sort_Intersect(SORT S1, SORT S2) |
| { |
| return list_Nconc(S1, S2); |
| } |
| |
| static __inline__ SORT sort_DeleteBaseNode(SORT S, NODE N) |
| { |
| return list_PointerDeleteElement(S,N); |
| } |
| |
| static __inline__ SORT sort_AddBaseNode(SORT S, NODE N) |
| { |
| return list_Cons(N,S); |
| } |
| |
| static __inline__ void sort_NodeFree(NODE N) |
| { |
| memory_Free(N,sizeof(NODE_NODE)); |
| } |
| |
| static __inline__ BOOL sort_NodeEqual(NODE N1, NODE N2) |
| { |
| return (N1 == N2); |
| } |
| |
| static __inline__ void sort_DeleteConditionList(LIST List) |
| { |
| list_DeleteWithElement(List, (void (*)(POINTER)) sort_ConditionDelete); |
| } |
| |
| static __inline__ void sort_NodeDelete(NODE N) |
| { |
| list_Delete(N->links); |
| N->links = list_Nil(); |
| sort_DeleteConditionList(N->conditions); |
| N->conditions = list_Nil(); |
| sort_NodeFree(N); |
| } |
| |
| static __inline__ LIST sort_NodeLinks(NODE N) |
| { |
| return N->links; |
| } |
| |
| static __inline__ BOOL sort_NodeValue(SORTTHEORY S, NODE N) |
| { |
| return (N->mark == S->mark); |
| } |
| |
| static __inline__ BOOL sort_NodeExtraValue(SORTTHEORY S, NODE N) |
| { |
| return (N->extra == S->mark); |
| } |
| |
| static __inline__ BOOL sort_NodeStartValue(SORTTHEORY S, NODE N) |
| { |
| return (N->start == S->mark); |
| } |
| |
| static __inline__ NAT sort_NodeMark(NODE N) |
| { |
| return N->mark; |
| } |
| |
| static __inline__ NAT sort_NodeStart(NODE N) |
| { |
| return N->start; |
| } |
| |
| static __inline__ SYMBOL sort_NodeSymbol(NODE N) |
| { |
| return N->symbol; |
| } |
| |
| static __inline__ LIST sort_NodeConditions(NODE N) |
| { |
| return N->conditions; |
| } |
| |
| static __inline__ void sort_PutNodeMark(NODE N, NAT M) |
| { |
| N->mark = M; |
| } |
| |
| static __inline__ void sort_PutNodeExtra(NODE N, NAT M) |
| { |
| N->extra = M; |
| } |
| |
| static __inline__ void sort_PutNodeStart(NODE N, NAT S) |
| { |
| N->start = S; |
| } |
| |
| static __inline__ void sort_PutNodeSymbol(NODE N, SYMBOL S) |
| { |
| N->symbol = S; |
| } |
| |
| static __inline__ void sort_PutNodeLinks(NODE N, LIST C) |
| { |
| N->links = C; |
| } |
| |
| static __inline__ void sort_PutNodeConditions(NODE N, LIST C) |
| { |
| N->conditions = C; |
| } |
| |
| static __inline__ void sort_PutNodeTrue(SORTTHEORY S, NODE N) |
| { |
| N->mark = S->mark; |
| } |
| |
| static __inline__ void sort_PutNodeExtraTrue(SORTTHEORY S, NODE N) |
| { |
| N->extra = S->mark; |
| } |
| |
| static __inline__ void sort_PutNodeStartTrue(SORTTHEORY S, NODE N) |
| { |
| N->start = S->mark; |
| } |
| |
| static __inline__ LIST sort_LinkInput(SLINK S) |
| { |
| return S->input; |
| } |
| |
| static __inline__ NODE sort_LinkOutput(SLINK S) |
| { |
| return S->output; |
| } |
| |
| static __inline__ int sort_LinkFire(SLINK S) |
| { |
| return S->fire; |
| } |
| |
| static __inline__ int sort_LinkVar(SLINK S) |
| { |
| return S->var; |
| } |
| |
| static __inline__ LIST sort_LinkConstraint(SLINK S) |
| { |
| return S->constraint; |
| } |
| |
| static __inline__ LIST sort_LinkAntecedent(SLINK S) |
| { |
| return S->antecedent; |
| } |
| |
| static __inline__ LIST sort_LinkSuccedent(SLINK S) |
| { |
| return S->succedent; |
| } |
| |
| static __inline__ CLAUSE sort_LinkClause(SLINK S) |
| { |
| return S->clause; |
| } |
| |
| static __inline__ int sort_LinkCard(SLINK S) |
| { |
| return S->card; |
| } |
| |
| static __inline__ void sort_PutLinkInput(SLINK S, LIST T) |
| { |
| S->input = T; |
| } |
| |
| static __inline__ void sort_PutLinkVar(SLINK S, SYMBOL V) |
| { |
| S->var = V; |
| } |
| |
| static __inline__ void sort_PutLinkConstraint(SLINK S, LIST T) |
| { |
| S->constraint = T; |
| } |
| |
| static __inline__ void sort_PutLinkAntecedent(SLINK S, LIST T) |
| { |
| S->antecedent = T; |
| } |
| |
| static __inline__ void sort_PutLinkSuccedent(SLINK S, LIST T) |
| { |
| S->succedent = T; |
| } |
| |
| static __inline__ void sort_PutLinkOutput(SLINK S,NODE H) |
| { |
| S->output = H; |
| } |
| |
| static __inline__ void sort_PutLinkClause(SLINK S, CLAUSE C) |
| { |
| S->clause = C; |
| } |
| |
| static __inline__ void sort_PutLinkCard(SLINK S,int L) |
| { |
| S->card = L; |
| } |
| |
| static __inline__ void sort_LinkResetFire(SLINK S) { |
| S->fire = S->card; |
| } |
| |
| static __inline__ int sort_LinkDecrementFire(SLINK S) |
| { |
| --(S->fire); |
| return S->fire; |
| } |
| |
| static __inline__ void sort_LinkFree(SLINK S) |
| { |
| memory_Free(S,sizeof(SLINK_NODE)); |
| } |
| |
| static __inline__ void sort_LinkDelete(SLINK S) |
| { |
| LIST Scan; |
| for (Scan=sort_LinkInput(S); !list_Empty(Scan); Scan=list_Cdr(Scan)) |
| sort_PutNodeLinks(list_Car(Scan),list_PointerDeleteElement(sort_NodeLinks(list_Car(Scan)),S)); |
| list_Delete(sort_LinkInput(S)); |
| term_DeleteTermList(sort_LinkConstraint(S)); |
| term_DeleteTermList(sort_LinkAntecedent(S)); |
| term_DeleteTermList(sort_LinkSuccedent(S)); |
| sort_LinkFree(S); |
| } |
| |
| static __inline__ SYMBOL sort_ConditionVar(CONDITION C) |
| { |
| return C->var; |
| } |
| |
| static __inline__ LIST sort_ConditionConstraint(CONDITION C) |
| { |
| return C->constraint; |
| } |
| |
| static __inline__ LIST sort_ConditionAntecedent(CONDITION C) |
| { |
| return C->antecedent; |
| } |
| |
| static __inline__ LIST sort_ConditionSuccedent(CONDITION C) |
| { |
| return C->succedent; |
| } |
| |
| static __inline__ LIST sort_ConditionClauses(CONDITION C) |
| { |
| return C->clauses; |
| } |
| |
| static __inline__ void sort_ConditionPutVar(CONDITION C, SYMBOL Var) |
| { |
| C->var = Var; |
| } |
| |
| static __inline__ void sort_ConditionPutConstraint(CONDITION C, LIST Constr) |
| { |
| C->constraint = Constr; |
| } |
| |
| static __inline__ void sort_ConditionPutAntecedent(CONDITION C, LIST Ante) |
| { |
| C->antecedent = Ante; |
| } |
| |
| static __inline__ void sort_ConditionPutSuccedent(CONDITION C, LIST Succ) |
| { |
| C->succedent = Succ; |
| } |
| |
| static __inline__ void sort_ConditionPutClauses(CONDITION C, LIST Clauses) |
| { |
| C->clauses = Clauses; |
| } |
| |
| static __inline__ void sort_ConditionFree(CONDITION C) |
| { |
| memory_Free(C, sizeof(CONDITION_NODE)); |
| } |
| |
| static __inline__ BOOL sort_ConditionNoResidues(CONDITION C) |
| { |
| return (list_Empty(sort_ConditionConstraint(C)) && |
| list_Empty(sort_ConditionAntecedent(C)) && |
| list_Empty(sort_ConditionSuccedent(C))); |
| } |
| |
| |
| |
| static __inline__ BOOL sort_LinkNoResidues(SLINK S) |
| { |
| return (list_Empty(sort_LinkConstraint(S)) && |
| list_Empty(sort_LinkAntecedent(S)) && |
| list_Empty(sort_LinkSuccedent(S))); |
| } |
| |
| static __inline__ BOOL sort_HasEqualSort(SORT S1, SORT S2) |
| { |
| return S1 == S2; |
| } |
| |
| |
| static __inline__ POINTER sort_PairSort(LIST Pair) |
| { |
| return list_PairFirst(Pair); |
| } |
| |
| static __inline__ POINTER sort_PairCondition(LIST Pair) |
| { |
| return list_PairSecond(Pair); |
| } |
| |
| static __inline__ LIST sort_PairCreate(SORT S , CONDITION Just) |
| { |
| return list_PairCreate((POINTER)S, Just); |
| } |
| |
| static __inline__ void sort_PairFree(LIST Pair) |
| { |
| list_PairFree(Pair); |
| } |
| |
| static __inline__ void sort_PairDelete(LIST Pair) |
| { |
| sort_DeleteOne(sort_PairSort(Pair)); |
| sort_ConditionDelete(sort_PairCondition(Pair)); |
| list_PairFree(Pair); |
| } |
| |
| static __inline__ LIST sort_PairCopy(LIST Pair) |
| { |
| return sort_PairCreate(sort_Copy(sort_PairSort(Pair)), |
| sort_ConditionCopy(sort_PairCondition(Pair))); |
| } |
| |
| static __inline__ NODE sort_TheoryNode(SORTTHEORY Theory, SYMBOL S) |
| { |
| return Theory->basesorttable[symbol_Index(S)]; |
| } |
| |
| static __inline__ NAT sort_TheoryMark(SORTTHEORY Theory) |
| { |
| return Theory->mark; |
| } |
| |
| static __inline__ LIST sort_TheorySuborigcls(SORTTHEORY Theory) |
| { |
| return Theory->suborigcls; |
| } |
| |
| static __inline__ LIST sort_TheoryTermorigcls(SORTTHEORY Theory) |
| { |
| return Theory->termorigcls; |
| } |
| |
| static __inline__ void sort_TheoryIncrementMark(SORTTHEORY Theory) |
| { |
| if (Theory->mark == NAT_MAX) { |
| int i; |
| NODE Node; |
| for (i = 0; i < symbol__MAXSIGNATURE; i++) { |
| Node = Theory->basesorttable[i]; |
| Node->mark = 0; |
| Node->extra = 0; |
| Node->start = 0; |
| } |
| Theory->mark = 0; |
| } |
| ++(Theory->mark); |
| } |
| |
| static __inline__ st_INDEX sort_TheoryIndex(SORTTHEORY Theory) |
| { |
| return Theory->index; |
| } |
| |
| |
| /**************************************************************/ |
| /* Functions */ |
| /**************************************************************/ |
| |
| void sort_Init(void); |
| void sort_Free(void); |
| |
| void sort_Delete(SORT); |
| BOOL sort_Eq(SORT, SORT); |
| void sort_DeleteSortPair(SOJU); |
| |
| void sort_Print(SORT); |
| void sort_PairPrint(SOJU); |
| |
| LIST sort_GetSymbolsFromSort(SORT); |
| BOOL sort_ContainsSymbol(SORT, SYMBOL); |
| BOOL sort_IsSort(SORT); |
| |
| |
| SORTTHEORY sort_ApproxStaticSortTheory(LIST, FLAGSTORE, PRECEDENCE); |
| SORTTHEORY sort_ApproxDynamicSortTheory(LIST); |
| |
| |
| SORTTHEORY sort_TheoryCreate(void); |
| void sort_TheoryDelete(SORTTHEORY); |
| void sort_TheoryPrint(SORTTHEORY); |
| void sort_TheoryInsertClause(SORTTHEORY, CLAUSE, CLAUSE, LITERAL); |
| void sort_TheoryDeleteClause(SORTTHEORY, CLAUSE); |
| SORT sort_TheorySortOfSymbol(SORTTHEORY, SYMBOL); |
| BOOL sort_TheorySortEqual(SORTTHEORY,SORT,SORT); |
| CONDITION sort_TheoryIsSubsortOfNoResidues(SORTTHEORY, SORT, SORT); |
| BOOL sort_TheoryIsSubsortOf(SORTTHEORY, SORT, SORT); |
| BOOL sort_TheoryIsSubsortOfExtra(SORTTHEORY , SORT , SORT , SORT); |
| LIST sort_TheoryComputeAllSubsortHits(SORTTHEORY, SORT, SORT); |
| SOJU sort_ComputeSortNoResidues(SORTTHEORY,TERM, CLAUSE, int, FLAGSTORE, PRECEDENCE); |
| LIST sort_ApproxMaxDeclClauses(CLAUSE, FLAGSTORE, PRECEDENCE); |
| STR sort_AnalyzeSortStructure(LIST, FLAGSTORE, PRECEDENCE); |
| |
| |
| #endif |