| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * ST INDEXING * */ |
| /* * * */ |
| /* * $Module: ST * */ |
| /* * * */ |
| /* * 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$ */ |
| |
| #include "st.h" |
| |
| |
| /**************************************************************/ |
| /* Local Variables */ |
| /**************************************************************/ |
| |
| static st_RETRIEVAL_TYPE st_CURRENT_RETRIEVAL; |
| static st_WHERE_TYPE st_WHICH_CONTEXTS; |
| static CONTEXT st_INDEX_CONTEXT; |
| static st_MINMAX st_EXIST_MINMAX; |
| |
| /**************************************************************/ |
| /* Global Variables */ |
| /**************************************************************/ |
| |
| ST_STACK st_STACK; |
| int st_STACKPOINTER; |
| int st_STACKSAVE; |
| |
| |
| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * CREATION OF INDEX * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| st_INDEX st_IndexCreate(void) |
| /************************************************************** |
| INPUT: None. |
| RETURNS: A pointer to a new St-Index. |
| SUMMARY: Creates a new St-index. |
| ***************************************************************/ |
| { |
| st_INDEX StIndex; |
| |
| StIndex = st_Get(); |
| StIndex->subnodes = list_Nil(); |
| StIndex->entries = list_Nil(); |
| StIndex->subst = subst_Nil(); |
| st_SetMax(StIndex, 0); |
| st_SetMin(StIndex, 0); |
| |
| return StIndex; |
| } |
| |
| |
| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * CREATION OF INDEX NODES * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| static st_INDEX st_NodeAddLeaf(SUBST Subst, st_MINMAX MinMax, POINTER Pointer) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| st_INDEX NewLeaf; |
| |
| NewLeaf = st_Get(); |
| NewLeaf->subnodes = list_Nil(); |
| NewLeaf->entries = list_List(Pointer); |
| NewLeaf->subst = Subst; |
| st_SetMax(NewLeaf, MinMax); |
| st_SetMin(NewLeaf, MinMax); |
| |
| return NewLeaf; |
| } |
| |
| |
| static void st_NodeAddInner(st_INDEX StIndex, SUBST SubstOld, SUBST SubstNew, |
| SUBST ComGen, st_MINMAX MinMax, POINTER Pointer) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| st_INDEX OldIndexNode; |
| |
| OldIndexNode = st_Get(); |
| OldIndexNode->subst = SubstOld; |
| OldIndexNode->entries = StIndex->entries; |
| OldIndexNode->subnodes = StIndex->subnodes; |
| st_SetMax(OldIndexNode, st_Max(StIndex)); |
| st_SetMin(OldIndexNode, st_Min(StIndex)); |
| |
| subst_Delete(StIndex->subst); |
| |
| StIndex->subst = ComGen; |
| StIndex->entries = list_Nil(); |
| StIndex->subnodes = list_Cons(st_NodeAddLeaf(SubstNew, MinMax, Pointer), |
| list_List(OldIndexNode)); |
| |
| if (st_Max(StIndex) < MinMax) |
| st_SetMax(StIndex, MinMax); |
| else if (st_Min(StIndex) > MinMax) |
| st_SetMin(StIndex, MinMax); |
| } |
| |
| |
| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * MERGING OF INDEX NODES * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| static void st_NodeMergeWithSon(st_INDEX StIndex) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| st_INDEX SubNode; |
| |
| SubNode = (st_INDEX)list_Car(StIndex->subnodes); |
| |
| list_Delete(StIndex->subnodes); |
| |
| StIndex->subst = subst_Merge(SubNode->subst, StIndex->subst); |
| StIndex->entries = SubNode->entries; |
| StIndex->subnodes = SubNode->subnodes; |
| st_SetMax(StIndex, st_Max(SubNode)); |
| st_SetMin(StIndex, st_Min(SubNode)); |
| |
| subst_Delete(SubNode->subst); |
| |
| st_Free(SubNode); |
| } |
| |
| |
| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * VARIABLE HANDLING FOR TERMS AND SUBSTS. * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| static void st_CloseUsedVariables(const CONTEXT Context, LIST NodeList) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| for (; list_Exist(NodeList); NodeList = list_Cdr(NodeList)) { |
| SUBST Subst; |
| |
| for (Subst = ((st_INDEX)list_Car(NodeList))->subst; |
| subst_Exist(Subst); |
| Subst = subst_Next(Subst)) |
| if (!cont_VarIsUsed(Context, subst_Dom(Subst))) |
| cont_CreateClosedBinding(Context, subst_Dom(Subst)); |
| |
| if (!st_IsLeaf((st_INDEX)list_Car(NodeList))) |
| st_CloseUsedVariables(Context, ((st_INDEX)list_Car(NodeList))->subnodes); |
| } |
| } |
| |
| |
| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * HEURISTICS FOR INSERTION OF TERMS AND SUBSTS. * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| static st_INDEX st_FirstVariant(const CONTEXT Context, LIST Subnodes, st_INDEX* BestNonVariant) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| st_INDEX EmptyVariant; |
| |
| for (EmptyVariant = NULL, *BestNonVariant = NULL; |
| list_Exist(Subnodes); |
| Subnodes = list_Cdr(Subnodes)) { |
| st_INDEX CurrentNode; |
| |
| CurrentNode = (st_INDEX)list_Car(Subnodes); |
| |
| cont_StartBinding(); |
| |
| if (subst_Variation(Context, CurrentNode->subst)) { |
| if (subst_Exist(CurrentNode->subst)) { |
| subst_CloseVariables(Context, CurrentNode->subst); |
| |
| return CurrentNode; |
| } else |
| EmptyVariant = CurrentNode; |
| |
| } else if (*BestNonVariant == NULL) |
| if (subst_MatchTops(Context, CurrentNode->subst)) |
| *BestNonVariant = CurrentNode; |
| |
| cont_BackTrack(); |
| } |
| |
| return EmptyVariant; |
| } |
| |
| |
| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * INSERTION OF TERMS * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| void st_EntryCreate(st_INDEX StIndex, POINTER Pointer, TERM Term, const CONTEXT Context) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| st_INDEX Current; |
| st_INDEX BestNonVariant; |
| SYMBOL FirstDomain; |
| st_MINMAX MinMax; |
| |
| cont_Check(); |
| |
| MinMax = term_ComputeSize(Term); |
| |
| /* CREATE INITIAL BINDING AND INITIALIZE LOCAL VARIABLES */ |
| FirstDomain = cont_NextIndexVariable(Context); |
| cont_CreateBinding(Context, FirstDomain, Context, Term); |
| |
| Current = StIndex; |
| |
| if (st_Max(Current) < MinMax) |
| st_SetMax(Current, MinMax); |
| else if (st_Min(Current) > MinMax) |
| st_SetMin(Current, MinMax); |
| |
| /* FIND "LAST" VARIATION */ |
| while (!st_IsLeaf(Current) && |
| (Current = st_FirstVariant(Context, Current->subnodes, &BestNonVariant))) { |
| if (st_Max(Current) < MinMax) |
| st_SetMax(Current, MinMax); |
| else if (st_Min(Current) > MinMax) |
| st_SetMin(Current, MinMax); |
| |
| StIndex = Current; |
| } |
| |
| if (cont_BindingsSinceLastStart()==0 && Current && st_IsLeaf(Current)) { |
| |
| /* INSERT ENTRY EQUAL MODULO RENAMING */ |
| Current->entries = list_Cons(Pointer, Current->entries); |
| |
| } else if (BestNonVariant) { |
| |
| /* CREATE INNER NODE AND A NEW LEAF */ |
| SUBST ComGen, SubstOld, SubstNew; |
| |
| if (!st_IsLeaf(BestNonVariant)) |
| st_CloseUsedVariables(Context, BestNonVariant->subnodes); |
| |
| ComGen = subst_ComGen(Context, BestNonVariant->subst, &SubstOld, &SubstNew); |
| |
| st_NodeAddInner(BestNonVariant, |
| SubstOld, |
| subst_CloseOpenVariables(SubstNew), |
| ComGen, |
| MinMax, |
| Pointer); |
| |
| } else |
| |
| /* ADD A SINGLE LEAF NODE TO FATHER */ |
| StIndex->subnodes = |
| list_Cons(st_NodeAddLeaf(subst_CloseOpenVariables(subst_Nil()), MinMax, |
| Pointer), |
| StIndex->subnodes); |
| |
| cont_Reset(); |
| } |
| |
| |
| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * DELETION OF INDEX * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| void st_IndexDelete(st_INDEX StIndex) |
| /************************************************************** |
| INPUT: A pointer to an existing St-Index. |
| SUMMARY: Deletes the whole index structure. |
| ***************************************************************/ |
| { |
| if (StIndex == NULL) |
| return; |
| else if (st_IsLeaf(StIndex)) |
| list_Delete(StIndex->entries); |
| else |
| /* Recursion */ |
| list_DeleteWithElement(StIndex->subnodes, (void (*)(POINTER))st_IndexDelete); |
| |
| subst_Delete(StIndex->subst); |
| st_Free(StIndex); |
| } |
| |
| |
| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * DELETION OF ENTRY FOR TERMS * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| static st_INDEX st_EntryDeleteHelp(const CONTEXT Context, st_INDEX StIndex, POINTER Pointer, |
| BOOL* Found) |
| /************************************************************** |
| INPUT: The root of an abstraction tree (StIndex), a |
| pointer to a specific entry of the tree and |
| a query term. |
| RETURNS: Nothing. |
| SUMMARY: Uses Term in order to find Pointer in the tree. |
| EFFECTS: Will delete nodes of StIndex. |
| ***************************************************************/ |
| { |
| if (st_IsLeaf(StIndex)) { |
| |
| *Found = list_DeleteFromList(&(StIndex->entries), Pointer); |
| |
| if (list_Exist(StIndex->entries)) |
| return StIndex; |
| else { |
| subst_Delete(StIndex->subst); |
| st_Free(StIndex); |
| |
| return NULL; |
| } |
| |
| } else { |
| |
| LIST Subnodes; |
| |
| for (Subnodes = StIndex->subnodes; |
| list_Exist(Subnodes); |
| Subnodes = list_Cdr(Subnodes)) { |
| st_INDEX CurrentNode; |
| |
| CurrentNode = (st_INDEX)list_Car(Subnodes); |
| |
| cont_StartBinding(); |
| |
| if (subst_Variation(Context, CurrentNode->subst)) { |
| list_Rplaca(Subnodes, st_EntryDeleteHelp(Context, |
| CurrentNode, |
| Pointer, |
| Found)); |
| if (*Found) { |
| if (list_DeleteFromList(&(StIndex->subnodes), NULL)) |
| if (list_Empty(list_Cdr(StIndex->subnodes))) { |
| /* 'StIndex' has one subnode only. */ |
| st_NodeMergeWithSon(StIndex); |
| |
| return StIndex; |
| } |
| |
| /* Assertion: 'StIndex' is an inner node. */ |
| |
| CurrentNode = (st_INDEX)list_Car(StIndex->subnodes); |
| st_SetMax(StIndex, st_Max(CurrentNode)); |
| st_SetMin(StIndex, st_Min(CurrentNode)); |
| |
| for (Subnodes = list_Cdr(StIndex->subnodes); |
| list_Exist(Subnodes); |
| Subnodes = list_Cdr(Subnodes)) { |
| CurrentNode = (st_INDEX)list_Car(Subnodes); |
| |
| if (st_Max(CurrentNode) > st_Max(StIndex)) |
| st_SetMax(StIndex, st_Max(CurrentNode)); |
| |
| if (st_Min(CurrentNode) < st_Min(StIndex)) |
| st_SetMin(StIndex, st_Min(CurrentNode)); |
| } |
| |
| return StIndex; |
| } |
| } |
| |
| cont_BackTrack(); |
| } |
| |
| return StIndex; |
| } |
| } |
| |
| |
| BOOL st_EntryDelete(st_INDEX StIndex, POINTER Pointer, TERM Term, const CONTEXT Context) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| BOOL Found; |
| LIST Subnodes; |
| SYMBOL FirstDomain; |
| |
| cont_Check(); |
| |
| FirstDomain = symbol_FirstIndexVariable(); |
| cont_CreateBinding(Context, FirstDomain, Context, Term); |
| |
| for (Found = FALSE, Subnodes = StIndex->subnodes; |
| list_Exist(Subnodes); |
| Subnodes = list_Cdr(Subnodes)) { |
| st_INDEX CurrentNode; |
| |
| CurrentNode = (st_INDEX)list_Car(Subnodes); |
| |
| cont_StartBinding(); |
| |
| if (subst_Variation(Context, CurrentNode->subst)) { |
| list_Rplaca(Subnodes, st_EntryDeleteHelp(Context, CurrentNode, Pointer, &Found)); |
| |
| if (Found) { |
| StIndex->subnodes = list_PointerDeleteElement(StIndex->subnodes, NULL); |
| |
| if (list_Exist(StIndex->subnodes)) { |
| CurrentNode = (st_INDEX)list_Car(StIndex->subnodes); |
| st_SetMax(StIndex, st_Max(CurrentNode)); |
| st_SetMin(StIndex, st_Min(CurrentNode)); |
| |
| for (Subnodes = list_Cdr(StIndex->subnodes); |
| list_Exist(Subnodes); |
| Subnodes = list_Cdr(Subnodes)) { |
| CurrentNode = (st_INDEX)list_Car(Subnodes); |
| |
| if (st_Max(CurrentNode) > st_Max(StIndex)) |
| st_SetMax(StIndex, st_Max(CurrentNode)); |
| |
| if (st_Min(CurrentNode) < st_Min(StIndex)) |
| st_SetMin(StIndex, st_Min(CurrentNode)); |
| } |
| } else { |
| st_SetMax(StIndex, 0); |
| st_SetMin(StIndex, 0); |
| } |
| |
| break; |
| } |
| } |
| |
| cont_BackTrack(); |
| } |
| |
| cont_Reset(); |
| |
| return Found; |
| } |
| |
| |
| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * RETRIEVAL FOR TERMS * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| static LIST st_TraverseTreeUnifier(CONTEXT IndexContext, st_INDEX StIndex) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| int Save; |
| LIST Result, CurrentList; |
| st_INDEX CurrentNode; |
| |
| /* PREPARE TRAVERSAL */ |
| Save = stack_Bottom(); |
| |
| Result = list_Nil(); |
| CurrentList = StIndex->subnodes; |
| |
| cont_StartBinding(); |
| |
| for (;;) { |
| |
| /* BACKTRACK A BIG STEP */ |
| if (list_Empty(CurrentList)) { |
| cont_StopAndBackTrack(); |
| |
| if (stack_Empty(Save)) |
| return Result; |
| |
| CurrentList = stack_PopResult(); |
| } |
| |
| /* DESCENDING */ |
| for (CurrentNode = (st_INDEX)list_Car(CurrentList); |
| subst_Unify(IndexContext, CurrentNode->subst); |
| CurrentList = CurrentNode->subnodes, |
| CurrentNode = (st_INDEX)list_Car(CurrentList)) |
| if (st_IsLeaf(CurrentNode)) { |
| Result = list_Append(CurrentNode->entries, Result); |
| break; |
| } else if (list_Exist(list_Cdr(CurrentList))) { |
| stack_Push(list_Cdr(CurrentList)); |
| cont_StartBinding(); |
| } else |
| cont_StopAndStartBinding(); |
| |
| /* BACKTRACK LEAF OR INNER NODE */ |
| CurrentList = list_Cdr(CurrentList); |
| cont_BackTrackAndStart(); |
| } |
| } |
| |
| |
| static LIST st_TraverseTreeGen(CONTEXT IndexContext, st_INDEX StIndex) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| int Save; |
| LIST Result, CurrentList; |
| st_INDEX CurrentNode; |
| |
| /* PREPARE TRAVERSAL */ |
| Save = stack_Bottom(); |
| |
| Result = list_Nil(); |
| CurrentList = StIndex->subnodes; |
| |
| cont_StartBinding(); |
| |
| for (;;) { |
| |
| /* BACKTRACK A BIG STEP */ |
| if (list_Empty(CurrentList)) { |
| cont_StopAndBackTrack(); |
| |
| if (stack_Empty(Save)) |
| return Result; |
| |
| CurrentList = stack_PopResult(); |
| } |
| |
| /* DESCENDING */ |
| for (CurrentNode = (st_INDEX)list_Car(CurrentList); |
| subst_Match(IndexContext, CurrentNode->subst); |
| CurrentList = CurrentNode->subnodes, |
| CurrentNode = (st_INDEX)list_Car(CurrentList)) |
| if (st_IsLeaf(CurrentNode)) { |
| Result = list_Append(CurrentNode->entries, Result); |
| break; |
| } else if (list_Cdr(CurrentList)) { |
| stack_Push(list_Cdr(CurrentList)); |
| cont_StartBinding(); |
| } else |
| cont_StopAndStartBinding(); |
| |
| /* BACKTRACK LEAF OR INNER NODE */ |
| CurrentList = list_Cdr(CurrentList); |
| cont_BackTrackAndStart(); |
| } |
| } |
| |
| |
| static LIST st_TraverseTreeInstance(CONTEXT IndexContext, st_INDEX StIndex) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| int Save; |
| LIST Result, CurrentList; |
| st_INDEX CurrentNode; |
| |
| /* PREPARE TRAVERSAL */ |
| Save = stack_Bottom(); |
| |
| Result = list_Nil(); |
| CurrentList = StIndex->subnodes; |
| |
| cont_StartBinding(); |
| |
| for (;;) { |
| |
| /* BACKTRACK A BIG STEP */ |
| if (list_Empty(CurrentList)) { |
| cont_StopAndBackTrack(); |
| |
| if (stack_Empty(Save)) |
| return Result; |
| |
| CurrentList = stack_PopResult(); |
| } |
| |
| /* DESCENDING */ |
| for (CurrentNode = (st_INDEX)list_Car(CurrentList); |
| subst_MatchReverse(IndexContext, CurrentNode->subst); |
| CurrentList = CurrentNode->subnodes, |
| CurrentNode = (st_INDEX)list_Car(CurrentList)) |
| if (st_IsLeaf(CurrentNode)) { |
| Result = list_Append(CurrentNode->entries, Result); |
| break; |
| } else if (list_Cdr(CurrentList)) { |
| stack_Push(list_Cdr(CurrentList)); |
| cont_StartBinding(); |
| } else |
| cont_StopAndStartBinding(); |
| |
| /* BACKTRACK LEAF OR INNER NODE */ |
| CurrentList = list_Cdr(CurrentList); |
| cont_BackTrackAndStart(); |
| } |
| } |
| |
| |
| static LIST st_TraverseTreeGenPreTest(CONTEXT IndexContext, |
| st_INDEX StIndex, |
| st_MINMAX MinMax) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| int Save; |
| LIST Result, CurrentList; |
| st_INDEX CurrentNode; |
| |
| /* PREPARE TRAVERSAL */ |
| Save = stack_Bottom(); |
| |
| Result = list_Nil(); |
| CurrentList = StIndex->subnodes; |
| |
| cont_StartBinding(); |
| |
| for (;;) { |
| |
| /* BACKTRACK A BIG STEP */ |
| if (list_Empty(CurrentList)) { |
| cont_StopAndBackTrack(); |
| |
| if (stack_Empty(Save)) |
| return Result; |
| |
| CurrentList = stack_PopResult(); |
| } |
| |
| /* DESCENDING */ |
| for (CurrentNode = (st_INDEX)list_Car(CurrentList); |
| (MinMax >= st_Min(CurrentNode)) && |
| subst_Match(IndexContext, CurrentNode->subst); |
| CurrentList = CurrentNode->subnodes, |
| CurrentNode = (st_INDEX)list_Car(CurrentList)) |
| if (st_IsLeaf(CurrentNode)) { |
| Result = list_Append(CurrentNode->entries, Result); |
| break; |
| } else if (list_Cdr(CurrentList)) { |
| stack_Push(list_Cdr(CurrentList)); |
| cont_StartBinding(); |
| } else |
| cont_StopAndStartBinding(); |
| |
| /* BACKTRACK LEAF OR INNER NODE */ |
| CurrentList = list_Cdr(CurrentList); |
| cont_BackTrackAndStart(); |
| } |
| } |
| |
| |
| static LIST st_TraverseTreeInstancePreTest(CONTEXT IndexContext, st_INDEX StIndex, st_MINMAX MinMax) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| int Save; |
| LIST Result, CurrentList; |
| st_INDEX CurrentNode; |
| |
| /* PREPARE TRAVERSAL */ |
| Save = stack_Bottom(); |
| |
| Result = list_Nil(); |
| CurrentList = StIndex->subnodes; |
| |
| cont_StartBinding(); |
| |
| for (;;) { |
| |
| /* BACKTRACK A BIG STEP */ |
| if (list_Empty(CurrentList)) { |
| cont_StopAndBackTrack(); |
| |
| if (stack_Empty(Save)) |
| return Result; |
| |
| CurrentList = stack_PopResult(); |
| } |
| |
| /* DESCENDING */ |
| for (CurrentNode = (st_INDEX)list_Car(CurrentList); |
| (MinMax <= st_Max(CurrentNode)) && |
| subst_MatchReverse(IndexContext, CurrentNode->subst); |
| CurrentList = CurrentNode->subnodes, |
| CurrentNode = (st_INDEX)list_Car(CurrentList)) |
| if (st_IsLeaf(CurrentNode)) { |
| Result = list_Append(CurrentNode->entries, Result); |
| break; |
| } else if (list_Cdr(CurrentList)) { |
| stack_Push(list_Cdr(CurrentList)); |
| cont_StartBinding(); |
| } else |
| cont_StopAndStartBinding(); |
| |
| /* BACKTRACK LEAF OR INNER NODE */ |
| CurrentList = list_Cdr(CurrentList); |
| cont_BackTrackAndStart(); |
| } |
| } |
| |
| |
| LIST st_GetUnifier(CONTEXT IndexContext, st_INDEX StIndex, CONTEXT TermContext, TERM Term) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| LIST Result; |
| SYMBOL FirstDomain; |
| |
| cont_Check(); |
| |
| FirstDomain = symbol_FirstIndexVariable(); |
| cont_CreateBinding(IndexContext, FirstDomain, TermContext, Term); |
| |
| Result = st_TraverseTreeUnifier(IndexContext, StIndex); |
| |
| cont_Reset(); |
| |
| return Result; |
| } |
| |
| |
| LIST st_GetGen(CONTEXT IndexContext, st_INDEX StIndex, TERM Term) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| LIST Result; |
| SYMBOL FirstDomain; |
| |
| cont_Check(); |
| |
| FirstDomain = symbol_FirstIndexVariable(); |
| cont_CreateBinding(IndexContext, FirstDomain, cont_InstanceContext(), Term); |
| |
| Result = st_TraverseTreeGen(IndexContext, StIndex); |
| |
| cont_Reset(); |
| |
| return Result; |
| } |
| |
| |
| LIST st_GetGenPreTest(CONTEXT IndexContext, st_INDEX StIndex, TERM Term) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| LIST Result; |
| SYMBOL FirstDomain; |
| |
| cont_Check(); |
| |
| FirstDomain = symbol_FirstIndexVariable(); |
| cont_CreateBinding(IndexContext, FirstDomain, cont_InstanceContext(), Term); |
| |
| Result = st_TraverseTreeGenPreTest(IndexContext, StIndex, term_ComputeSize(Term)); |
| |
| cont_Reset(); |
| |
| return Result; |
| } |
| |
| |
| LIST st_GetInstance(CONTEXT IndexContext, st_INDEX StIndex, TERM Term) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| LIST Result; |
| SYMBOL FirstDomain; |
| |
| cont_Check(); |
| |
| FirstDomain = symbol_FirstIndexVariable(); |
| cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term); |
| |
| Result = st_TraverseTreeInstance(IndexContext, StIndex); |
| |
| cont_Reset(); |
| |
| return Result; |
| } |
| |
| |
| LIST st_GetInstancePreTest(CONTEXT IndexContext, st_INDEX StIndex, TERM Term) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| LIST Result; |
| SYMBOL FirstDomain; |
| |
| cont_Check(); |
| |
| FirstDomain = symbol_FirstIndexVariable(); |
| cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term); |
| |
| Result = st_TraverseTreeInstancePreTest(IndexContext, StIndex, term_ComputeSize(Term)); |
| |
| cont_Reset(); |
| |
| return Result; |
| } |
| |
| |
| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * INCREMENTAL RETRIEVAL * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| static POINTER st_TraverseForExistUnifier(CONTEXT IndexContext) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| LIST CurrentList; |
| st_INDEX CurrentNode; |
| |
| /* Caution: In case an entry is found |
| the procedure returns immediately |
| without backtracking the current bindings. */ |
| |
| CurrentList = list_Nil(); |
| |
| for (;;) { |
| |
| /* BACKTRACK A BIG STEP */ |
| if (list_Empty(CurrentList)) { |
| cont_StopAndBackTrack(); |
| |
| if (st_StackEmpty(st_STACKSAVE)) |
| return NULL; |
| |
| CurrentList = st_StackPopResult(); |
| } |
| |
| /* DESCENDING */ |
| for (CurrentNode = (st_INDEX)list_Car(CurrentList); |
| subst_Unify(IndexContext, CurrentNode->subst); |
| CurrentList = CurrentNode->subnodes, |
| CurrentNode = (st_INDEX)list_Car(CurrentList)) { |
| if (list_Exist(list_Cdr(CurrentList))) { |
| st_StackPush(list_Cdr(CurrentList)); |
| cont_StartBinding(); |
| } else |
| cont_StopAndStartBinding(); |
| |
| if (st_IsLeaf(CurrentNode)) { |
| st_StackPush(list_Cdr(CurrentNode->entries)); |
| return list_Car(CurrentNode->entries); |
| } |
| } |
| |
| /* BACKTRACK LEAF OR INNER NODE */ |
| CurrentList = list_Cdr(CurrentList); |
| cont_BackTrackAndStart(); |
| } |
| } |
| |
| |
| static POINTER st_TraverseForExistGen(CONTEXT IndexContext) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| LIST CurrentList; |
| st_INDEX CurrentNode; |
| |
| /* Caution: In case an entry is found |
| the procedure returns immediately |
| without backtracking the current bindings. */ |
| |
| CurrentList = list_Nil(); |
| |
| for (;;) { |
| |
| /* BACKTRACK A BIG STEP */ |
| if (list_Empty(CurrentList)) { |
| cont_StopAndBackTrack(); |
| |
| if (st_StackEmpty(st_STACKSAVE)) |
| return NULL; |
| |
| CurrentList = st_StackPopResult(); |
| } |
| |
| /* DESCENDING */ |
| for (CurrentNode = (st_INDEX)list_Car(CurrentList); |
| subst_Match(IndexContext, CurrentNode->subst); |
| CurrentList = CurrentNode->subnodes, |
| CurrentNode = (st_INDEX)list_Car(CurrentList)) { |
| if (list_Exist(list_Cdr(CurrentList))) { |
| st_StackPush(list_Cdr(CurrentList)); |
| cont_StartBinding(); |
| } else |
| cont_StopAndStartBinding(); |
| |
| if (st_IsLeaf(CurrentNode)) { |
| st_StackPush(list_Cdr(CurrentNode->entries)); |
| return list_Car(CurrentNode->entries); |
| } |
| } |
| |
| /* BACKTRACK LEAF OR INNER NODE */ |
| CurrentList = list_Cdr(CurrentList); |
| cont_BackTrackAndStart(); |
| } |
| } |
| |
| |
| static POINTER st_TraverseForExistGenPreTest(CONTEXT IndexContext) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| LIST CurrentList; |
| st_INDEX CurrentNode; |
| |
| /* Caution: In case an entry is found |
| the procedure returns immediately |
| without backtracking the current bindings. */ |
| |
| CurrentList = list_Nil(); |
| |
| for (;;) { |
| |
| /* BACKTRACK A BIG STEP */ |
| if (list_Empty(CurrentList)) { |
| cont_StopAndBackTrack(); |
| |
| if (st_StackEmpty(st_STACKSAVE)) |
| return NULL; |
| |
| CurrentList = st_StackPopResult(); |
| } |
| |
| /* DESCENDING */ |
| for (CurrentNode = (st_INDEX)list_Car(CurrentList); |
| (st_EXIST_MINMAX >= st_Min(CurrentNode)) && |
| subst_Match(IndexContext, CurrentNode->subst); |
| CurrentList = CurrentNode->subnodes, |
| CurrentNode = (st_INDEX)list_Car(CurrentList)) { |
| if (list_Exist(list_Cdr(CurrentList))) { |
| st_StackPush(list_Cdr(CurrentList)); |
| cont_StartBinding(); |
| } else |
| cont_StopAndStartBinding(); |
| |
| if (st_IsLeaf(CurrentNode)) { |
| st_StackPush(list_Cdr(CurrentNode->entries)); |
| return list_Car(CurrentNode->entries); |
| } |
| } |
| |
| /* BACKTRACK LEAF OR INNER NODE */ |
| CurrentList = list_Cdr(CurrentList); |
| cont_BackTrackAndStart(); |
| } |
| } |
| |
| |
| static POINTER st_TraverseForExistInstance(CONTEXT IndexContext) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| LIST CurrentList; |
| st_INDEX CurrentNode; |
| |
| /* Caution: In case an entry is found |
| the procedure returns immediately |
| without backtracking the current bindings. */ |
| |
| CurrentList = list_Nil(); |
| |
| for (;;) { |
| |
| /* BACKTRACK A BIG STEP */ |
| if (list_Empty(CurrentList)) { |
| cont_StopAndBackTrack(); |
| |
| if (st_StackEmpty(st_STACKSAVE)) |
| return NULL; |
| |
| CurrentList = st_StackPopResult(); |
| } |
| |
| /* DESCENDING */ |
| for (CurrentNode = (st_INDEX)list_Car(CurrentList); |
| subst_MatchReverse(IndexContext, CurrentNode->subst); |
| CurrentList = CurrentNode->subnodes, |
| CurrentNode = (st_INDEX)list_Car(CurrentList)) { |
| if (list_Exist(list_Cdr(CurrentList))) { |
| st_StackPush(list_Cdr(CurrentList)); |
| cont_StartBinding(); |
| } else |
| cont_StopAndStartBinding(); |
| |
| if (st_IsLeaf(CurrentNode)) { |
| st_StackPush(list_Cdr(CurrentNode->entries)); |
| return list_Car(CurrentNode->entries); |
| } |
| } |
| |
| /* BACKTRACK LEAF OR INNER NODE */ |
| CurrentList = list_Cdr(CurrentList); |
| cont_BackTrackAndStart(); |
| } |
| } |
| |
| |
| static POINTER st_TraverseForExistInstancePreTest(CONTEXT IndexContext) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| LIST CurrentList; |
| st_INDEX CurrentNode; |
| |
| /* Caution: In case an entry is found |
| the procedure returns immediately |
| without backtracking the current bindings. */ |
| |
| CurrentList = list_Nil(); |
| |
| for (;;) { |
| |
| /* BACKTRACK A BIG STEP */ |
| if (list_Empty(CurrentList)) { |
| cont_StopAndBackTrack(); |
| |
| if (st_StackEmpty(st_STACKSAVE)) |
| return NULL; |
| |
| CurrentList = st_StackPopResult(); |
| } |
| |
| /* DESCENDING */ |
| for (CurrentNode = (st_INDEX)list_Car(CurrentList); |
| (st_EXIST_MINMAX <= st_Max(CurrentNode)) && |
| subst_MatchReverse(IndexContext, CurrentNode->subst); |
| CurrentList = CurrentNode->subnodes, |
| CurrentNode = (st_INDEX)list_Car(CurrentList)) { |
| if (list_Exist(list_Cdr(CurrentList))) { |
| st_StackPush(list_Cdr(CurrentList)); |
| cont_StartBinding(); |
| } else |
| cont_StopAndStartBinding(); |
| |
| if (st_IsLeaf(CurrentNode)) { |
| st_StackPush(list_Cdr(CurrentNode->entries)); |
| return list_Car(CurrentNode->entries); |
| } |
| } |
| |
| /* BACKTRACK LEAF OR INNER NODE */ |
| CurrentList = list_Cdr(CurrentList); |
| cont_BackTrackAndStart(); |
| } |
| } |
| |
| |
| void st_CancelExistRetrieval(void) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| if (st_CURRENT_RETRIEVAL != st_NOP) { |
| |
| #ifdef CHECK |
| cont_CheckState(); |
| #endif |
| |
| st_StackSetBottom(st_STACKSAVE); |
| |
| switch (st_WHICH_CONTEXTS) { |
| |
| case st_STANDARD: |
| cont_Reset(); |
| break; |
| |
| case st_NOC: |
| break; |
| |
| default: |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_CancelExistRetrieval: Unknown context type.\n"); |
| misc_FinishErrorReport(); |
| } |
| |
| st_CURRENT_RETRIEVAL = st_NOP; |
| st_WHICH_CONTEXTS = st_NOC; |
| st_INDEX_CONTEXT = NULL; |
| st_EXIST_MINMAX = 0; |
| } |
| } |
| |
| |
| POINTER st_ExistUnifier(CONTEXT IndexContext, st_INDEX StIndex, CONTEXT TermContext, TERM Term) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| SYMBOL FirstDomain; |
| POINTER Result; |
| |
| #ifdef CHECK |
| if (!st_StackEmpty(st_STACKSAVE)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_ExistUnifier: ST-Stack not empty.\n"); |
| misc_FinishErrorReport(); |
| } else if (st_CURRENT_RETRIEVAL != st_NOP) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_ExistUnifier: %d Retrieval already in progress.\n", |
| st_CURRENT_RETRIEVAL); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| cont_Check(); |
| |
| if (st_Exist(StIndex)) { |
| |
| st_CURRENT_RETRIEVAL = st_UNIFIER; |
| st_WHICH_CONTEXTS = st_STANDARD; |
| st_INDEX_CONTEXT = IndexContext; |
| |
| st_STACKSAVE = st_StackBottom(); |
| |
| FirstDomain = symbol_FirstIndexVariable(); |
| cont_CreateBinding(IndexContext, FirstDomain, TermContext, Term); |
| |
| cont_StartBinding(); |
| st_StackPush(StIndex->subnodes); |
| cont_StartBinding(); |
| |
| Result = st_TraverseForExistUnifier(IndexContext); |
| |
| #ifdef CHECK |
| cont_SaveState(); |
| #endif |
| |
| if (Result == NULL) |
| st_CancelExistRetrieval(); |
| |
| return Result; |
| } else |
| return NULL; |
| } |
| |
| |
| POINTER st_ExistGen(CONTEXT IndexContext, st_INDEX StIndex, TERM Term) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| SYMBOL FirstDomain; |
| POINTER Result; |
| |
| #ifdef CHECK |
| if (!st_StackEmpty(st_STACKSAVE)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_ExistGen: ST-Stack not empty.\n"); |
| misc_FinishErrorReport(); |
| } |
| else |
| if (st_CURRENT_RETRIEVAL != st_NOP) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_ExistGen: %d Retrieval already in progress.\n", |
| st_CURRENT_RETRIEVAL); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| cont_Check(); |
| |
| if (st_Exist(StIndex)) { |
| |
| st_CURRENT_RETRIEVAL = st_GEN; |
| st_WHICH_CONTEXTS = st_STANDARD; |
| st_INDEX_CONTEXT = IndexContext; |
| |
| st_STACKSAVE = st_StackBottom(); |
| |
| FirstDomain = symbol_FirstIndexVariable(); |
| cont_CreateBinding(IndexContext, FirstDomain, cont_InstanceContext(), Term); |
| |
| cont_StartBinding(); |
| st_StackPush(StIndex->subnodes); |
| cont_StartBinding(); |
| |
| Result = st_TraverseForExistGen(IndexContext); |
| |
| #ifdef CHECK |
| cont_SaveState(); |
| #endif |
| |
| if (Result == NULL) |
| st_CancelExistRetrieval(); |
| |
| return Result; |
| } else |
| return NULL; |
| } |
| |
| |
| POINTER st_ExistGenPreTest(CONTEXT IndexContext, st_INDEX StIndex, TERM Term) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| SYMBOL FirstDomain; |
| POINTER Result; |
| |
| #ifdef CHECK |
| if (!st_StackEmpty(st_STACKSAVE)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_ExistGenPreTest: ST-Stack not empty.\n"); |
| misc_FinishErrorReport(); |
| } |
| else |
| if (st_CURRENT_RETRIEVAL != st_NOP) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_ExistGenPreTest: %d Retrieval already in progress.\n", |
| st_CURRENT_RETRIEVAL); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| cont_Check(); |
| |
| if (st_Exist(StIndex)) { |
| |
| st_CURRENT_RETRIEVAL = st_GENPRETEST; |
| st_WHICH_CONTEXTS = st_STANDARD; |
| st_INDEX_CONTEXT = IndexContext; |
| |
| st_STACKSAVE = st_StackBottom(); |
| |
| |
| FirstDomain = symbol_FirstIndexVariable(); |
| st_EXIST_MINMAX = term_ComputeSize(Term); |
| cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term); |
| |
| cont_StartBinding(); |
| st_StackPush(StIndex->subnodes); |
| cont_StartBinding(); |
| |
| Result = st_TraverseForExistGenPreTest(IndexContext); |
| |
| #ifdef CHECK |
| cont_SaveState(); |
| #endif |
| |
| if (Result == NULL) |
| st_CancelExistRetrieval(); |
| |
| return Result; |
| } else |
| return NULL; |
| } |
| |
| |
| POINTER st_ExistInstance(CONTEXT IndexContext, st_INDEX StIndex, TERM Term) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| SYMBOL FirstDomain; |
| POINTER Result; |
| |
| #ifdef CHECK |
| if (!st_StackEmpty(st_STACKSAVE)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_ExistInstance: ST-Stack not empty.\n"); |
| misc_FinishErrorReport(); |
| } |
| else |
| if (st_CURRENT_RETRIEVAL != st_NOP) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_ExistInstance: %d Retrieval already in progress.\n", |
| st_CURRENT_RETRIEVAL); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| cont_Check(); |
| |
| if (st_Exist(StIndex)) { |
| |
| st_CURRENT_RETRIEVAL = st_INSTANCE; |
| st_WHICH_CONTEXTS = st_STANDARD; |
| st_INDEX_CONTEXT = IndexContext; |
| |
| st_STACKSAVE = st_StackBottom(); |
| |
| FirstDomain = symbol_FirstIndexVariable(); |
| cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term); |
| |
| cont_StartBinding(); |
| st_StackPush(StIndex->subnodes); |
| cont_StartBinding(); |
| |
| Result = st_TraverseForExistInstance(IndexContext); |
| |
| #ifdef CHECK |
| cont_SaveState(); |
| #endif |
| |
| if (Result == NULL) |
| st_CancelExistRetrieval(); |
| |
| return Result; |
| } else |
| return NULL; |
| } |
| |
| |
| POINTER st_ExistInstancePreTest(CONTEXT IndexContext, st_INDEX StIndex, TERM Term) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| SYMBOL FirstDomain; |
| POINTER Result; |
| |
| #ifdef CHECK |
| if (!st_StackEmpty(st_STACKSAVE)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_ExistInstancePreTest: ST-Stack not empty.\n"); |
| misc_FinishErrorReport(); |
| } |
| else |
| if (st_CURRENT_RETRIEVAL != st_NOP) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_ExistInstancePreTest: %d Retrieval already in progress.\n", |
| st_CURRENT_RETRIEVAL); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| cont_Check(); |
| |
| if (st_Exist(StIndex)) { |
| |
| st_CURRENT_RETRIEVAL = st_INSTANCEPRETEST; |
| st_WHICH_CONTEXTS = st_STANDARD; |
| st_INDEX_CONTEXT = IndexContext; |
| |
| st_STACKSAVE = st_StackBottom(); |
| |
| FirstDomain = symbol_FirstIndexVariable(); |
| st_EXIST_MINMAX = term_ComputeSize(Term); |
| cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term); |
| |
| cont_StartBinding(); |
| st_StackPush(StIndex->subnodes); |
| cont_StartBinding(); |
| |
| Result = st_TraverseForExistInstancePreTest(IndexContext); |
| |
| #ifdef CHECK |
| cont_SaveState(); |
| #endif |
| |
| if (Result == NULL) |
| st_CancelExistRetrieval(); |
| |
| return Result; |
| } else |
| return NULL; |
| } |
| |
| |
| POINTER st_NextCandidate(void) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECTS: |
| ***************************************************************/ |
| { |
| LIST Result; |
| |
| #ifdef CHECK |
| if (st_StackEmpty(st_STACKSAVE)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_NextCandidate: ST-Stack empty.\n"); |
| misc_FinishErrorReport(); |
| } |
| else |
| if (st_CURRENT_RETRIEVAL == st_NOP) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_NextCandidate: No retrieval in progress.\n"); |
| misc_FinishErrorReport(); |
| } |
| |
| cont_CheckState(); |
| #endif |
| |
| Result = st_StackPopResult(); |
| |
| if (list_Exist(Result)) { |
| st_StackPush(list_Cdr(Result)); |
| #ifdef CHECK |
| cont_SaveState(); |
| #endif |
| return list_Car(Result); |
| } else { |
| POINTER NewResult; |
| |
| NewResult = NULL; |
| |
| if (st_WHICH_CONTEXTS == st_STANDARD) |
| switch (st_CURRENT_RETRIEVAL) { |
| |
| case st_UNIFIER: |
| NewResult = st_TraverseForExistUnifier(st_INDEX_CONTEXT); |
| break; |
| |
| case st_GEN: |
| NewResult = st_TraverseForExistGen(st_INDEX_CONTEXT); |
| break; |
| |
| case st_GENPRETEST: |
| NewResult = st_TraverseForExistGenPreTest(st_INDEX_CONTEXT); |
| break; |
| |
| case st_INSTANCE: |
| NewResult = st_TraverseForExistInstance(st_INDEX_CONTEXT); |
| break; |
| |
| case st_INSTANCEPRETEST: |
| NewResult = st_TraverseForExistInstancePreTest(st_INDEX_CONTEXT); |
| |
| default: |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_NextCandidate: Unknown retrieval type.\n"); |
| misc_FinishErrorReport(); |
| } |
| else { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In st_NextCandidate: Unknown context type.\n"); |
| misc_FinishErrorReport(); |
| } |
| |
| #ifdef CHECK |
| cont_SaveState(); |
| #endif |
| |
| if (NewResult == NULL) |
| st_CancelExistRetrieval(); |
| |
| return NewResult; |
| } |
| } |
| |
| |
| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * OUTPUT * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| static void st_PrintHelp(st_INDEX St, int Position, void (*Print)(POINTER)) |
| /************************************************************** |
| INPUT: A node of an St, an indention and a print |
| function for the entries. |
| SUMMARY: Prints an St starting at node St. |
| ***************************************************************/ |
| { |
| int i; |
| |
| if (St == (st_INDEX)NULL) |
| return; |
| |
| for (i = 0; i < Position; i++) |
| putchar(' '); |
| puts("|"); |
| |
| for (i = 0; i < Position; i++) |
| putchar(' '); |
| fputs("+-", stdout); |
| |
| printf(" Max: %d, Min: %d, ", st_Max(St), st_Min(St)); |
| subst_Print(St->subst); |
| putchar('\n'); |
| |
| if (st_IsLeaf(St)) { |
| |
| LIST Scan; |
| |
| for (i = 0; i < Position; i++) |
| putchar(' '); |
| fputs(" =>", stdout); |
| |
| if (Print) |
| for (Scan = St->entries; Scan != NULL; Scan = list_Cdr(Scan)) { |
| putchar(' '); |
| Print(list_Car(Scan)); |
| } |
| else |
| printf(" %d Entries", list_Length(St->entries)); |
| |
| putchar('\n'); |
| |
| } else { |
| LIST Scan; |
| |
| for (Scan = St->subnodes; Scan != NULL; Scan = list_Cdr(Scan)) |
| st_PrintHelp(list_Car(Scan), Position + 2, Print); |
| } |
| } |
| |
| |
| void st_Print(st_INDEX StIndex, void (*Print)(POINTER)) |
| /************************************************************** |
| INPUT: The root of an St. |
| SUMMARY: Prints a whole St. |
| ***************************************************************/ |
| { |
| LIST Scan; |
| |
| if (st_Empty(StIndex)) { |
| puts("\n\nIndex empty."); |
| return; |
| } |
| |
| fputs("\n\nroot: ", stdout); |
| printf(" Max: %d, Min: %d, ", st_Max(StIndex), st_Min(StIndex)); |
| subst_Print(StIndex->subst); |
| putchar('\n'); |
| if (st_IsLeaf(StIndex)) { |
| fputs(" =>", stdout); |
| |
| if (Print) |
| for (Scan = StIndex->entries; Scan != NULL; Scan = list_Cdr(Scan)) { |
| putchar(' '); |
| Print(list_Car(Scan)); |
| } |
| else |
| printf(" %d Entries", list_Length(StIndex->entries)); |
| |
| } else |
| for (Scan = StIndex->subnodes; Scan != NULL; Scan = list_Cdr(Scan)) |
| st_PrintHelp(list_Car(Scan),2, Print); |
| puts("\n"); |
| } |