1
/**************************************************************/
2
/* ********************************************************** */
8
/* * Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001 * */
9
/* * MPI fuer Informatik * */
11
/* * This program is free software; you can redistribute * */
12
/* * it and/or modify it under the terms of the FreeBSD * */
15
/* * This program is distributed in the hope that it will * */
16
/* * be useful, but WITHOUT ANY WARRANTY; without even * */
17
/* * the implied warranty of MERCHANTABILITY or FITNESS * */
18
/* * FOR A PARTICULAR PURPOSE. See the LICENCE file * */
19
/* * for more details. * */
22
/* $Revision: 1.3 $ * */
24
/* $Date: 2010-02-22 14:09:59 $ * */
25
/* $Author: weidenb $ * */
28
/* * Christoph Weidenbach * */
29
/* * MPI fuer Informatik * */
30
/* * Stuhlsatzenhausweg 85 * */
31
/* * 66123 Saarbruecken * */
32
/* * Email: spass@mpi-inf.mpg.de * */
35
/* ********************************************************** */
36
/**************************************************************/
39
/* $RCSfile: st.c,v $ */
44
/**************************************************************/
46
/**************************************************************/
48
static st_RETRIEVAL_TYPE st_CURRENT_RETRIEVAL;
49
static st_WHERE_TYPE st_WHICH_CONTEXTS;
50
static CONTEXT st_INDEX_CONTEXT;
51
static st_MINMAX st_EXIST_MINMAX;
53
/**************************************************************/
54
/* Global Variables */
55
/**************************************************************/
62
/**************************************************************/
63
/* ********************************************************** */
65
/* * CREATION OF INDEX * */
67
/* ********************************************************** */
68
/**************************************************************/
71
st_INDEX st_IndexCreate(void)
72
/**************************************************************
74
RETURNS: A pointer to a new St-Index.
75
SUMMARY: Creates a new St-index.
76
***************************************************************/
81
StIndex->subnodes = list_Nil();
82
StIndex->entries = list_Nil();
83
StIndex->subst = subst_Nil();
84
st_SetMax(StIndex, 0);
85
st_SetMin(StIndex, 0);
91
/**************************************************************/
92
/* ********************************************************** */
94
/* * CREATION OF INDEX NODES * */
96
/* ********************************************************** */
97
/**************************************************************/
100
static st_INDEX st_NodeAddLeaf(SUBST Subst, st_MINMAX MinMax, POINTER Pointer)
101
/**************************************************************
105
***************************************************************/
110
NewLeaf->subnodes = list_Nil();
111
NewLeaf->entries = list_List(Pointer);
112
NewLeaf->subst = Subst;
113
st_SetMax(NewLeaf, MinMax);
114
st_SetMin(NewLeaf, MinMax);
120
static void st_NodeAddInner(st_INDEX StIndex, SUBST SubstOld, SUBST SubstNew,
121
SUBST ComGen, st_MINMAX MinMax, POINTER Pointer)
122
/**************************************************************
126
***************************************************************/
128
st_INDEX OldIndexNode;
130
OldIndexNode = st_Get();
131
OldIndexNode->subst = SubstOld;
132
OldIndexNode->entries = StIndex->entries;
133
OldIndexNode->subnodes = StIndex->subnodes;
134
st_SetMax(OldIndexNode, st_Max(StIndex));
135
st_SetMin(OldIndexNode, st_Min(StIndex));
137
subst_Delete(StIndex->subst);
139
StIndex->subst = ComGen;
140
StIndex->entries = list_Nil();
141
StIndex->subnodes = list_Cons(st_NodeAddLeaf(SubstNew, MinMax, Pointer),
142
list_List(OldIndexNode));
144
if (st_Max(StIndex) < MinMax)
145
st_SetMax(StIndex, MinMax);
146
else if (st_Min(StIndex) > MinMax)
147
st_SetMin(StIndex, MinMax);
151
/**************************************************************/
152
/* ********************************************************** */
154
/* * MERGING OF INDEX NODES * */
156
/* ********************************************************** */
157
/**************************************************************/
160
static void st_NodeMergeWithSon(st_INDEX StIndex)
161
/**************************************************************
165
***************************************************************/
169
SubNode = (st_INDEX)list_Car(StIndex->subnodes);
171
list_Delete(StIndex->subnodes);
173
StIndex->subst = subst_Merge(SubNode->subst, StIndex->subst);
174
StIndex->entries = SubNode->entries;
175
StIndex->subnodes = SubNode->subnodes;
176
st_SetMax(StIndex, st_Max(SubNode));
177
st_SetMin(StIndex, st_Min(SubNode));
179
subst_Delete(SubNode->subst);
185
/**************************************************************/
186
/* ********************************************************** */
188
/* * VARIABLE HANDLING FOR TERMS AND SUBSTS. * */
190
/* ********************************************************** */
191
/**************************************************************/
194
static void st_CloseUsedVariables(const CONTEXT Context, LIST NodeList)
195
/**************************************************************
199
***************************************************************/
201
for (; list_Exist(NodeList); NodeList = list_Cdr(NodeList)) {
204
for (Subst = ((st_INDEX)list_Car(NodeList))->subst;
206
Subst = subst_Next(Subst))
207
if (!cont_VarIsUsed(Context, subst_Dom(Subst)))
208
cont_CreateClosedBinding(Context, subst_Dom(Subst));
210
if (!st_IsLeaf((st_INDEX)list_Car(NodeList)))
211
st_CloseUsedVariables(Context, ((st_INDEX)list_Car(NodeList))->subnodes);
216
/**************************************************************/
217
/* ********************************************************** */
219
/* * HEURISTICS FOR INSERTION OF TERMS AND SUBSTS. * */
221
/* ********************************************************** */
222
/**************************************************************/
225
static st_INDEX st_FirstVariant(const CONTEXT Context, LIST Subnodes, st_INDEX* BestNonVariant)
226
/**************************************************************
230
***************************************************************/
232
st_INDEX EmptyVariant;
234
for (EmptyVariant = NULL, *BestNonVariant = NULL;
235
list_Exist(Subnodes);
236
Subnodes = list_Cdr(Subnodes)) {
237
st_INDEX CurrentNode;
239
CurrentNode = (st_INDEX)list_Car(Subnodes);
243
if (subst_Variation(Context, CurrentNode->subst)) {
244
if (subst_Exist(CurrentNode->subst)) {
245
subst_CloseVariables(Context, CurrentNode->subst);
249
EmptyVariant = CurrentNode;
251
} else if (*BestNonVariant == NULL)
252
if (subst_MatchTops(Context, CurrentNode->subst))
253
*BestNonVariant = CurrentNode;
262
/**************************************************************/
263
/* ********************************************************** */
265
/* * INSERTION OF TERMS * */
267
/* ********************************************************** */
268
/**************************************************************/
271
void st_EntryCreate(st_INDEX StIndex, POINTER Pointer, TERM Term, const CONTEXT Context)
272
/**************************************************************
276
***************************************************************/
279
st_INDEX BestNonVariant;
285
MinMax = term_ComputeSize(Term);
286
BestNonVariant = (st_INDEX)NULL;
288
/* CREATE INITIAL BINDING AND INITIALIZE LOCAL VARIABLES */
289
FirstDomain = cont_NextIndexVariable(Context);
290
cont_CreateBinding(Context, FirstDomain, Context, Term);
294
if (st_Max(Current) < MinMax)
295
st_SetMax(Current, MinMax);
296
else if (st_Min(Current) > MinMax)
297
st_SetMin(Current, MinMax);
299
/* FIND "LAST" VARIATION */
300
while (!st_IsLeaf(Current) &&
301
(Current = st_FirstVariant(Context, Current->subnodes, &BestNonVariant))) {
302
if (st_Max(Current) < MinMax)
303
st_SetMax(Current, MinMax);
304
else if (st_Min(Current) > MinMax)
305
st_SetMin(Current, MinMax);
310
if (cont_BindingsSinceLastStart()==0 && Current && st_IsLeaf(Current)) {
312
/* INSERT ENTRY EQUAL MODULO RENAMING */
313
Current->entries = list_Cons(Pointer, Current->entries);
315
} else if (BestNonVariant) {
317
/* CREATE INNER NODE AND A NEW LEAF */
318
SUBST ComGen, SubstOld, SubstNew;
320
if (!st_IsLeaf(BestNonVariant))
321
st_CloseUsedVariables(Context, BestNonVariant->subnodes);
323
ComGen = subst_ComGen(Context, BestNonVariant->subst, &SubstOld, &SubstNew);
325
st_NodeAddInner(BestNonVariant,
327
subst_CloseOpenVariables(SubstNew),
334
/* ADD A SINGLE LEAF NODE TO FATHER */
336
list_Cons(st_NodeAddLeaf(subst_CloseOpenVariables(subst_Nil()), MinMax,
344
/**************************************************************/
345
/* ********************************************************** */
347
/* * DELETION OF INDEX * */
349
/* ********************************************************** */
350
/**************************************************************/
352
void st_IndexDeleteWithElement(st_INDEX StIndex)
353
/**************************************************************
354
INPUT: A pointer to an existing St-Index.
355
SUMMARY: Deletes the whole index structure and
356
the terms contained in the index
357
***************************************************************/
361
else if (st_IsLeaf(StIndex))
362
list_DeleteWithElement(StIndex->entries, (void (*) (POINTER)) term_Delete);
365
list_DeleteWithElement(StIndex->subnodes,
366
(void(*)(POINTER)) st_IndexDeleteWithElement);
368
subst_Delete(StIndex->subst);
373
void st_IndexDelete(st_INDEX StIndex)
374
/**************************************************************
375
INPUT: A pointer to an existing St-Index.
376
SUMMARY: Deletes the whole index structure.
377
***************************************************************/
381
else if (st_IsLeaf(StIndex))
382
list_Delete(StIndex->entries);
385
list_DeleteWithElement(StIndex->subnodes, (void (*)(POINTER))st_IndexDelete);
387
subst_Delete(StIndex->subst);
392
/**************************************************************/
393
/* ********************************************************** */
395
/* * DELETION OF ENTRY FOR TERMS * */
397
/* ********************************************************** */
398
/**************************************************************/
401
static st_INDEX st_EntryDeleteHelp(const CONTEXT Context, st_INDEX StIndex, POINTER Pointer,
403
/**************************************************************
404
INPUT: The root of an abstraction tree (StIndex), a
405
pointer to a specific entry of the tree and
408
SUMMARY: Uses Term in order to find Pointer in the tree.
409
EFFECTS: Will delete nodes of StIndex.
410
***************************************************************/
412
if (st_IsLeaf(StIndex)) {
414
*Found = list_DeleteFromList(&(StIndex->entries), Pointer);
416
if (list_Exist(StIndex->entries))
419
subst_Delete(StIndex->subst);
429
for (Subnodes = StIndex->subnodes;
430
list_Exist(Subnodes);
431
Subnodes = list_Cdr(Subnodes)) {
432
st_INDEX CurrentNode;
434
CurrentNode = (st_INDEX)list_Car(Subnodes);
438
if (subst_Variation(Context, CurrentNode->subst)) {
439
list_Rplaca(Subnodes, st_EntryDeleteHelp(Context,
444
if (list_DeleteFromList(&(StIndex->subnodes), NULL))
445
if (list_Empty(list_Cdr(StIndex->subnodes))) {
446
/* 'StIndex' has one subnode only. */
447
st_NodeMergeWithSon(StIndex);
452
/* Assertion: 'StIndex' is an inner node. */
454
CurrentNode = (st_INDEX)list_Car(StIndex->subnodes);
455
st_SetMax(StIndex, st_Max(CurrentNode));
456
st_SetMin(StIndex, st_Min(CurrentNode));
458
for (Subnodes = list_Cdr(StIndex->subnodes);
459
list_Exist(Subnodes);
460
Subnodes = list_Cdr(Subnodes)) {
461
CurrentNode = (st_INDEX)list_Car(Subnodes);
463
if (st_Max(CurrentNode) > st_Max(StIndex))
464
st_SetMax(StIndex, st_Max(CurrentNode));
466
if (st_Min(CurrentNode) < st_Min(StIndex))
467
st_SetMin(StIndex, st_Min(CurrentNode));
482
BOOL st_EntryDelete(st_INDEX StIndex, POINTER Pointer, TERM Term, const CONTEXT Context)
483
/**************************************************************
487
***************************************************************/
495
FirstDomain = symbol_FirstIndexVariable();
496
cont_CreateBinding(Context, FirstDomain, Context, Term);
498
for (Found = FALSE, Subnodes = StIndex->subnodes;
499
list_Exist(Subnodes);
500
Subnodes = list_Cdr(Subnodes)) {
501
st_INDEX CurrentNode;
503
CurrentNode = (st_INDEX)list_Car(Subnodes);
507
if (subst_Variation(Context, CurrentNode->subst)) {
508
list_Rplaca(Subnodes, st_EntryDeleteHelp(Context, CurrentNode, Pointer, &Found));
511
StIndex->subnodes = list_PointerDeleteElement(StIndex->subnodes, NULL);
513
if (list_Exist(StIndex->subnodes)) {
514
CurrentNode = (st_INDEX)list_Car(StIndex->subnodes);
515
st_SetMax(StIndex, st_Max(CurrentNode));
516
st_SetMin(StIndex, st_Min(CurrentNode));
518
for (Subnodes = list_Cdr(StIndex->subnodes);
519
list_Exist(Subnodes);
520
Subnodes = list_Cdr(Subnodes)) {
521
CurrentNode = (st_INDEX)list_Car(Subnodes);
523
if (st_Max(CurrentNode) > st_Max(StIndex))
524
st_SetMax(StIndex, st_Max(CurrentNode));
526
if (st_Min(CurrentNode) < st_Min(StIndex))
527
st_SetMin(StIndex, st_Min(CurrentNode));
530
st_SetMax(StIndex, 0);
531
st_SetMin(StIndex, 0);
547
/**************************************************************/
548
/* ********************************************************** */
550
/* * RETRIEVAL FOR TERMS * */
552
/* ********************************************************** */
553
/**************************************************************/
556
static LIST st_TraverseTreeUnifier(CONTEXT IndexContext, st_INDEX StIndex)
557
/**************************************************************
561
***************************************************************/
564
LIST Result, CurrentList;
565
st_INDEX CurrentNode;
567
/* PREPARE TRAVERSAL */
568
Save = stack_Bottom();
571
CurrentList = StIndex->subnodes;
577
/* BACKTRACK A BIG STEP */
578
if (list_Empty(CurrentList)) {
579
cont_StopAndBackTrack();
581
if (stack_Empty(Save))
584
CurrentList = stack_PopResult();
588
for (CurrentNode = (st_INDEX)list_Car(CurrentList);
589
subst_Unify(IndexContext, CurrentNode->subst);
590
CurrentList = CurrentNode->subnodes,
591
CurrentNode = (st_INDEX)list_Car(CurrentList))
592
if (st_IsLeaf(CurrentNode)) {
593
Result = list_Append(CurrentNode->entries, Result);
595
} else if (list_Exist(list_Cdr(CurrentList))) {
596
stack_Push(list_Cdr(CurrentList));
599
cont_StopAndStartBinding();
601
/* BACKTRACK LEAF OR INNER NODE */
602
CurrentList = list_Cdr(CurrentList);
603
cont_BackTrackAndStart();
608
static LIST st_TraverseTreeGen(CONTEXT IndexContext, st_INDEX StIndex)
609
/**************************************************************
613
***************************************************************/
616
LIST Result, CurrentList;
617
st_INDEX CurrentNode;
619
/* PREPARE TRAVERSAL */
620
Save = stack_Bottom();
623
CurrentList = StIndex->subnodes;
629
/* BACKTRACK A BIG STEP */
630
if (list_Empty(CurrentList)) {
631
cont_StopAndBackTrack();
633
if (stack_Empty(Save))
636
CurrentList = stack_PopResult();
640
for (CurrentNode = (st_INDEX)list_Car(CurrentList);
641
subst_Match(IndexContext, CurrentNode->subst);
642
CurrentList = CurrentNode->subnodes,
643
CurrentNode = (st_INDEX)list_Car(CurrentList))
644
if (st_IsLeaf(CurrentNode)) {
645
Result = list_Append(CurrentNode->entries, Result);
647
} else if (list_Cdr(CurrentList)) {
648
stack_Push(list_Cdr(CurrentList));
651
cont_StopAndStartBinding();
653
/* BACKTRACK LEAF OR INNER NODE */
654
CurrentList = list_Cdr(CurrentList);
655
cont_BackTrackAndStart();
660
static LIST st_TraverseTreeInstance(CONTEXT IndexContext, st_INDEX StIndex)
661
/**************************************************************
665
***************************************************************/
668
LIST Result, CurrentList;
669
st_INDEX CurrentNode;
671
/* PREPARE TRAVERSAL */
672
Save = stack_Bottom();
675
CurrentList = StIndex->subnodes;
681
/* BACKTRACK A BIG STEP */
682
if (list_Empty(CurrentList)) {
683
cont_StopAndBackTrack();
685
if (stack_Empty(Save))
688
CurrentList = stack_PopResult();
692
for (CurrentNode = (st_INDEX)list_Car(CurrentList);
693
subst_MatchReverse(IndexContext, CurrentNode->subst);
694
CurrentList = CurrentNode->subnodes,
695
CurrentNode = (st_INDEX)list_Car(CurrentList))
696
if (st_IsLeaf(CurrentNode)) {
697
Result = list_Append(CurrentNode->entries, Result);
699
} else if (list_Cdr(CurrentList)) {
700
stack_Push(list_Cdr(CurrentList));
703
cont_StopAndStartBinding();
705
/* BACKTRACK LEAF OR INNER NODE */
706
CurrentList = list_Cdr(CurrentList);
707
cont_BackTrackAndStart();
712
static LIST st_TraverseTreeGenPreTest(CONTEXT IndexContext,
715
/**************************************************************
719
***************************************************************/
722
LIST Result, CurrentList;
723
st_INDEX CurrentNode;
725
/* PREPARE TRAVERSAL */
726
Save = stack_Bottom();
729
CurrentList = StIndex->subnodes;
735
/* BACKTRACK A BIG STEP */
736
if (list_Empty(CurrentList)) {
737
cont_StopAndBackTrack();
739
if (stack_Empty(Save))
742
CurrentList = stack_PopResult();
746
for (CurrentNode = (st_INDEX)list_Car(CurrentList);
747
(MinMax >= st_Min(CurrentNode)) &&
748
subst_Match(IndexContext, CurrentNode->subst);
749
CurrentList = CurrentNode->subnodes,
750
CurrentNode = (st_INDEX)list_Car(CurrentList))
751
if (st_IsLeaf(CurrentNode)) {
752
Result = list_Append(CurrentNode->entries, Result);
754
} else if (list_Cdr(CurrentList)) {
755
stack_Push(list_Cdr(CurrentList));
758
cont_StopAndStartBinding();
760
/* BACKTRACK LEAF OR INNER NODE */
761
CurrentList = list_Cdr(CurrentList);
762
cont_BackTrackAndStart();
767
static LIST st_TraverseTreeInstancePreTest(CONTEXT IndexContext, st_INDEX StIndex, st_MINMAX MinMax)
768
/**************************************************************
772
***************************************************************/
775
LIST Result, CurrentList;
776
st_INDEX CurrentNode;
778
/* PREPARE TRAVERSAL */
779
Save = stack_Bottom();
782
CurrentList = StIndex->subnodes;
788
/* BACKTRACK A BIG STEP */
789
if (list_Empty(CurrentList)) {
790
cont_StopAndBackTrack();
792
if (stack_Empty(Save))
795
CurrentList = stack_PopResult();
799
for (CurrentNode = (st_INDEX)list_Car(CurrentList);
800
(MinMax <= st_Max(CurrentNode)) &&
801
subst_MatchReverse(IndexContext, CurrentNode->subst);
802
CurrentList = CurrentNode->subnodes,
803
CurrentNode = (st_INDEX)list_Car(CurrentList))
804
if (st_IsLeaf(CurrentNode)) {
805
Result = list_Append(CurrentNode->entries, Result);
807
} else if (list_Cdr(CurrentList)) {
808
stack_Push(list_Cdr(CurrentList));
811
cont_StopAndStartBinding();
813
/* BACKTRACK LEAF OR INNER NODE */
814
CurrentList = list_Cdr(CurrentList);
815
cont_BackTrackAndStart();
820
LIST st_GetUnifier(CONTEXT IndexContext, st_INDEX StIndex, CONTEXT TermContext, TERM Term)
821
/**************************************************************
825
***************************************************************/
832
FirstDomain = symbol_FirstIndexVariable();
833
cont_CreateBinding(IndexContext, FirstDomain, TermContext, Term);
835
Result = st_TraverseTreeUnifier(IndexContext, StIndex);
843
LIST st_GetGen(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
844
/**************************************************************
848
***************************************************************/
855
FirstDomain = symbol_FirstIndexVariable();
856
cont_CreateBinding(IndexContext, FirstDomain, cont_InstanceContext(), Term);
858
Result = st_TraverseTreeGen(IndexContext, StIndex);
866
LIST st_GetGenPreTest(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
867
/**************************************************************
871
***************************************************************/
878
FirstDomain = symbol_FirstIndexVariable();
879
cont_CreateBinding(IndexContext, FirstDomain, cont_InstanceContext(), Term);
881
Result = st_TraverseTreeGenPreTest(IndexContext, StIndex, term_ComputeSize(Term));
889
LIST st_GetInstance(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
890
/**************************************************************
894
***************************************************************/
901
FirstDomain = symbol_FirstIndexVariable();
902
cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term);
904
Result = st_TraverseTreeInstance(IndexContext, StIndex);
912
LIST st_GetInstancePreTest(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
913
/**************************************************************
917
***************************************************************/
924
FirstDomain = symbol_FirstIndexVariable();
925
cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term);
927
Result = st_TraverseTreeInstancePreTest(IndexContext, StIndex, term_ComputeSize(Term));
935
/**************************************************************/
936
/* ********************************************************** */
938
/* * INCREMENTAL RETRIEVAL * */
940
/* ********************************************************** */
941
/**************************************************************/
944
static POINTER st_TraverseForExistUnifier(CONTEXT IndexContext)
945
/**************************************************************
949
***************************************************************/
952
st_INDEX CurrentNode;
954
/* Caution: In case an entry is found
955
the procedure returns immediately
956
without backtracking the current bindings. */
958
CurrentList = list_Nil();
962
/* BACKTRACK A BIG STEP */
963
if (list_Empty(CurrentList)) {
964
cont_StopAndBackTrack();
966
if (st_StackEmpty(st_STACKSAVE))
969
CurrentList = st_StackPopResult();
973
for (CurrentNode = (st_INDEX)list_Car(CurrentList);
974
subst_Unify(IndexContext, CurrentNode->subst);
975
CurrentList = CurrentNode->subnodes,
976
CurrentNode = (st_INDEX)list_Car(CurrentList)) {
977
if (list_Exist(list_Cdr(CurrentList))) {
978
st_StackPush(list_Cdr(CurrentList));
981
cont_StopAndStartBinding();
983
if (st_IsLeaf(CurrentNode)) {
984
st_StackPush(list_Cdr(CurrentNode->entries));
985
return list_Car(CurrentNode->entries);
989
/* BACKTRACK LEAF OR INNER NODE */
990
CurrentList = list_Cdr(CurrentList);
991
cont_BackTrackAndStart();
996
static POINTER st_TraverseForExistGen(CONTEXT IndexContext)
997
/**************************************************************
1001
***************************************************************/
1004
st_INDEX CurrentNode;
1006
/* Caution: In case an entry is found
1007
the procedure returns immediately
1008
without backtracking the current bindings. */
1010
CurrentList = list_Nil();
1014
/* BACKTRACK A BIG STEP */
1015
if (list_Empty(CurrentList)) {
1016
cont_StopAndBackTrack();
1018
if (st_StackEmpty(st_STACKSAVE))
1021
CurrentList = st_StackPopResult();
1025
for (CurrentNode = (st_INDEX)list_Car(CurrentList);
1026
subst_Match(IndexContext, CurrentNode->subst);
1027
CurrentList = CurrentNode->subnodes,
1028
CurrentNode = (st_INDEX)list_Car(CurrentList)) {
1029
if (list_Exist(list_Cdr(CurrentList))) {
1030
st_StackPush(list_Cdr(CurrentList));
1031
cont_StartBinding();
1033
cont_StopAndStartBinding();
1035
if (st_IsLeaf(CurrentNode)) {
1036
st_StackPush(list_Cdr(CurrentNode->entries));
1037
return list_Car(CurrentNode->entries);
1041
/* BACKTRACK LEAF OR INNER NODE */
1042
CurrentList = list_Cdr(CurrentList);
1043
cont_BackTrackAndStart();
1048
static POINTER st_TraverseForExistGenPreTest(CONTEXT IndexContext)
1049
/**************************************************************
1053
***************************************************************/
1056
st_INDEX CurrentNode;
1058
/* Caution: In case an entry is found
1059
the procedure returns immediately
1060
without backtracking the current bindings. */
1062
CurrentList = list_Nil();
1066
/* BACKTRACK A BIG STEP */
1067
if (list_Empty(CurrentList)) {
1068
cont_StopAndBackTrack();
1070
if (st_StackEmpty(st_STACKSAVE))
1073
CurrentList = st_StackPopResult();
1077
for (CurrentNode = (st_INDEX)list_Car(CurrentList);
1078
(st_EXIST_MINMAX >= st_Min(CurrentNode)) &&
1079
subst_Match(IndexContext, CurrentNode->subst);
1080
CurrentList = CurrentNode->subnodes,
1081
CurrentNode = (st_INDEX)list_Car(CurrentList)) {
1082
if (list_Exist(list_Cdr(CurrentList))) {
1083
st_StackPush(list_Cdr(CurrentList));
1084
cont_StartBinding();
1086
cont_StopAndStartBinding();
1088
if (st_IsLeaf(CurrentNode)) {
1089
st_StackPush(list_Cdr(CurrentNode->entries));
1090
return list_Car(CurrentNode->entries);
1094
/* BACKTRACK LEAF OR INNER NODE */
1095
CurrentList = list_Cdr(CurrentList);
1096
cont_BackTrackAndStart();
1101
static POINTER st_TraverseForExistInstance(CONTEXT IndexContext)
1102
/**************************************************************
1106
***************************************************************/
1109
st_INDEX CurrentNode;
1111
/* Caution: In case an entry is found
1112
the procedure returns immediately
1113
without backtracking the current bindings. */
1115
CurrentList = list_Nil();
1119
/* BACKTRACK A BIG STEP */
1120
if (list_Empty(CurrentList)) {
1121
cont_StopAndBackTrack();
1123
if (st_StackEmpty(st_STACKSAVE))
1126
CurrentList = st_StackPopResult();
1130
for (CurrentNode = (st_INDEX)list_Car(CurrentList);
1131
subst_MatchReverse(IndexContext, CurrentNode->subst);
1132
CurrentList = CurrentNode->subnodes,
1133
CurrentNode = (st_INDEX)list_Car(CurrentList)) {
1134
if (list_Exist(list_Cdr(CurrentList))) {
1135
st_StackPush(list_Cdr(CurrentList));
1136
cont_StartBinding();
1138
cont_StopAndStartBinding();
1140
if (st_IsLeaf(CurrentNode)) {
1141
st_StackPush(list_Cdr(CurrentNode->entries));
1142
return list_Car(CurrentNode->entries);
1146
/* BACKTRACK LEAF OR INNER NODE */
1147
CurrentList = list_Cdr(CurrentList);
1148
cont_BackTrackAndStart();
1153
static POINTER st_TraverseForExistInstancePreTest(CONTEXT IndexContext)
1154
/**************************************************************
1158
***************************************************************/
1161
st_INDEX CurrentNode;
1163
/* Caution: In case an entry is found
1164
the procedure returns immediately
1165
without backtracking the current bindings. */
1167
CurrentList = list_Nil();
1171
/* BACKTRACK A BIG STEP */
1172
if (list_Empty(CurrentList)) {
1173
cont_StopAndBackTrack();
1175
if (st_StackEmpty(st_STACKSAVE))
1178
CurrentList = st_StackPopResult();
1182
for (CurrentNode = (st_INDEX)list_Car(CurrentList);
1183
(st_EXIST_MINMAX <= st_Max(CurrentNode)) &&
1184
subst_MatchReverse(IndexContext, CurrentNode->subst);
1185
CurrentList = CurrentNode->subnodes,
1186
CurrentNode = (st_INDEX)list_Car(CurrentList)) {
1187
if (list_Exist(list_Cdr(CurrentList))) {
1188
st_StackPush(list_Cdr(CurrentList));
1189
cont_StartBinding();
1191
cont_StopAndStartBinding();
1193
if (st_IsLeaf(CurrentNode)) {
1194
st_StackPush(list_Cdr(CurrentNode->entries));
1195
return list_Car(CurrentNode->entries);
1199
/* BACKTRACK LEAF OR INNER NODE */
1200
CurrentList = list_Cdr(CurrentList);
1201
cont_BackTrackAndStart();
1206
void st_CancelExistRetrieval(void)
1207
/**************************************************************
1211
***************************************************************/
1213
if (st_CURRENT_RETRIEVAL != st_NOP) {
1219
st_StackSetBottom(st_STACKSAVE);
1221
switch (st_WHICH_CONTEXTS) {
1231
misc_StartErrorReport();
1232
misc_ErrorReport("\n In st_CancelExistRetrieval: Unknown context type.\n");
1233
misc_FinishErrorReport();
1236
st_CURRENT_RETRIEVAL = st_NOP;
1237
st_WHICH_CONTEXTS = st_NOC;
1238
st_INDEX_CONTEXT = NULL;
1239
st_EXIST_MINMAX = 0;
1244
POINTER st_ExistUnifier(CONTEXT IndexContext, st_INDEX StIndex, CONTEXT TermContext, TERM Term)
1245
/**************************************************************
1249
***************************************************************/
1255
if (!st_StackEmpty(st_STACKSAVE)) {
1256
misc_StartErrorReport();
1257
misc_ErrorReport("\n In st_ExistUnifier: ST-Stack not empty.\n");
1258
misc_FinishErrorReport();
1259
} else if (st_CURRENT_RETRIEVAL != st_NOP) {
1260
misc_StartErrorReport();
1261
misc_ErrorReport("\n In st_ExistUnifier: %d Retrieval already in progress.\n",
1262
st_CURRENT_RETRIEVAL);
1263
misc_FinishErrorReport();
1269
if (st_Exist(StIndex)) {
1271
st_CURRENT_RETRIEVAL = st_UNIFIER;
1272
st_WHICH_CONTEXTS = st_STANDARD;
1273
st_INDEX_CONTEXT = IndexContext;
1275
st_STACKSAVE = st_StackBottom();
1277
FirstDomain = symbol_FirstIndexVariable();
1278
cont_CreateBinding(IndexContext, FirstDomain, TermContext, Term);
1280
cont_StartBinding();
1281
st_StackPush(StIndex->subnodes);
1282
cont_StartBinding();
1284
Result = st_TraverseForExistUnifier(IndexContext);
1291
st_CancelExistRetrieval();
1299
POINTER st_ExistGen(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
1300
/**************************************************************
1304
***************************************************************/
1310
if (!st_StackEmpty(st_STACKSAVE)) {
1311
misc_StartErrorReport();
1312
misc_ErrorReport("\n In st_ExistGen: ST-Stack not empty.\n");
1313
misc_FinishErrorReport();
1316
if (st_CURRENT_RETRIEVAL != st_NOP) {
1317
misc_StartErrorReport();
1318
misc_ErrorReport("\n In st_ExistGen: %d Retrieval already in progress.\n",
1319
st_CURRENT_RETRIEVAL);
1320
misc_FinishErrorReport();
1326
if (st_Exist(StIndex)) {
1328
st_CURRENT_RETRIEVAL = st_GEN;
1329
st_WHICH_CONTEXTS = st_STANDARD;
1330
st_INDEX_CONTEXT = IndexContext;
1332
st_STACKSAVE = st_StackBottom();
1334
FirstDomain = symbol_FirstIndexVariable();
1335
cont_CreateBinding(IndexContext, FirstDomain, cont_InstanceContext(), Term);
1337
cont_StartBinding();
1338
st_StackPush(StIndex->subnodes);
1339
cont_StartBinding();
1341
Result = st_TraverseForExistGen(IndexContext);
1348
st_CancelExistRetrieval();
1356
POINTER st_ExistGenPreTest(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
1357
/**************************************************************
1361
***************************************************************/
1367
if (!st_StackEmpty(st_STACKSAVE)) {
1368
misc_StartErrorReport();
1369
misc_ErrorReport("\n In st_ExistGenPreTest: ST-Stack not empty.\n");
1370
misc_FinishErrorReport();
1373
if (st_CURRENT_RETRIEVAL != st_NOP) {
1374
misc_StartErrorReport();
1375
misc_ErrorReport("\n In st_ExistGenPreTest: %d Retrieval already in progress.\n",
1376
st_CURRENT_RETRIEVAL);
1377
misc_FinishErrorReport();
1383
if (st_Exist(StIndex)) {
1385
st_CURRENT_RETRIEVAL = st_GENPRETEST;
1386
st_WHICH_CONTEXTS = st_STANDARD;
1387
st_INDEX_CONTEXT = IndexContext;
1389
st_STACKSAVE = st_StackBottom();
1392
FirstDomain = symbol_FirstIndexVariable();
1393
st_EXIST_MINMAX = term_ComputeSize(Term);
1394
cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term);
1396
cont_StartBinding();
1397
st_StackPush(StIndex->subnodes);
1398
cont_StartBinding();
1400
Result = st_TraverseForExistGenPreTest(IndexContext);
1407
st_CancelExistRetrieval();
1415
POINTER st_ExistInstance(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
1416
/**************************************************************
1420
***************************************************************/
1426
if (!st_StackEmpty(st_STACKSAVE)) {
1427
misc_StartErrorReport();
1428
misc_ErrorReport("\n In st_ExistInstance: ST-Stack not empty.\n");
1429
misc_FinishErrorReport();
1432
if (st_CURRENT_RETRIEVAL != st_NOP) {
1433
misc_StartErrorReport();
1434
misc_ErrorReport("\n In st_ExistInstance: %d Retrieval already in progress.\n",
1435
st_CURRENT_RETRIEVAL);
1436
misc_FinishErrorReport();
1442
if (st_Exist(StIndex)) {
1444
st_CURRENT_RETRIEVAL = st_INSTANCE;
1445
st_WHICH_CONTEXTS = st_STANDARD;
1446
st_INDEX_CONTEXT = IndexContext;
1448
st_STACKSAVE = st_StackBottom();
1450
FirstDomain = symbol_FirstIndexVariable();
1451
cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term);
1453
cont_StartBinding();
1454
st_StackPush(StIndex->subnodes);
1455
cont_StartBinding();
1457
Result = st_TraverseForExistInstance(IndexContext);
1464
st_CancelExistRetrieval();
1472
POINTER st_ExistInstancePreTest(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
1473
/**************************************************************
1477
***************************************************************/
1483
if (!st_StackEmpty(st_STACKSAVE)) {
1484
misc_StartErrorReport();
1485
misc_ErrorReport("\n In st_ExistInstancePreTest: ST-Stack not empty.\n");
1486
misc_FinishErrorReport();
1489
if (st_CURRENT_RETRIEVAL != st_NOP) {
1490
misc_StartErrorReport();
1491
misc_ErrorReport("\n In st_ExistInstancePreTest: %d Retrieval already in progress.\n",
1492
st_CURRENT_RETRIEVAL);
1493
misc_FinishErrorReport();
1499
if (st_Exist(StIndex)) {
1501
st_CURRENT_RETRIEVAL = st_INSTANCEPRETEST;
1502
st_WHICH_CONTEXTS = st_STANDARD;
1503
st_INDEX_CONTEXT = IndexContext;
1505
st_STACKSAVE = st_StackBottom();
1507
FirstDomain = symbol_FirstIndexVariable();
1508
st_EXIST_MINMAX = term_ComputeSize(Term);
1509
cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term);
1511
cont_StartBinding();
1512
st_StackPush(StIndex->subnodes);
1513
cont_StartBinding();
1515
Result = st_TraverseForExistInstancePreTest(IndexContext);
1522
st_CancelExistRetrieval();
1530
POINTER st_NextCandidate(void)
1531
/**************************************************************
1535
***************************************************************/
1540
if (st_StackEmpty(st_STACKSAVE)) {
1541
misc_StartErrorReport();
1542
misc_ErrorReport("\n In st_NextCandidate: ST-Stack empty.\n");
1543
misc_FinishErrorReport();
1546
if (st_CURRENT_RETRIEVAL == st_NOP) {
1547
misc_StartErrorReport();
1548
misc_ErrorReport("\n In st_NextCandidate: No retrieval in progress.\n");
1549
misc_FinishErrorReport();
1555
Result = st_StackPopResult();
1557
if (list_Exist(Result)) {
1558
st_StackPush(list_Cdr(Result));
1562
return list_Car(Result);
1568
if (st_WHICH_CONTEXTS == st_STANDARD)
1569
switch (st_CURRENT_RETRIEVAL) {
1572
NewResult = st_TraverseForExistUnifier(st_INDEX_CONTEXT);
1576
NewResult = st_TraverseForExistGen(st_INDEX_CONTEXT);
1580
NewResult = st_TraverseForExistGenPreTest(st_INDEX_CONTEXT);
1584
NewResult = st_TraverseForExistInstance(st_INDEX_CONTEXT);
1587
case st_INSTANCEPRETEST:
1588
NewResult = st_TraverseForExistInstancePreTest(st_INDEX_CONTEXT);
1591
misc_StartErrorReport();
1592
misc_ErrorReport("\n In st_NextCandidate: Unknown retrieval type.\n");
1593
misc_FinishErrorReport();
1596
misc_StartErrorReport();
1597
misc_ErrorReport("\n In st_NextCandidate: Unknown context type.\n");
1598
misc_FinishErrorReport();
1605
if (NewResult == NULL)
1606
st_CancelExistRetrieval();
1613
/**************************************************************/
1614
/* ********************************************************** */
1618
/* ********************************************************** */
1619
/**************************************************************/
1622
static void st_PrintHelp(st_INDEX St, int Position, void (*Print)(POINTER))
1623
/**************************************************************
1624
INPUT: A node of an St, an indention and a print
1625
function for the entries.
1626
SUMMARY: Prints an St starting at node St.
1627
***************************************************************/
1631
if (St == (st_INDEX)NULL)
1634
for (i = 0; i < Position; i++)
1638
for (i = 0; i < Position; i++)
1640
fputs("+-", stdout);
1642
printf(" Max: %d, Min: %d, ", st_Max(St), st_Min(St));
1643
subst_Print(St->subst);
1646
if (st_IsLeaf(St)) {
1650
for (i = 0; i < Position; i++)
1652
fputs(" =>", stdout);
1655
for (Scan = St->entries; Scan != NULL; Scan = list_Cdr(Scan)) {
1657
Print(list_Car(Scan));
1660
printf(" %d Entries", list_Length(St->entries));
1667
for (Scan = St->subnodes; Scan != NULL; Scan = list_Cdr(Scan))
1668
st_PrintHelp(list_Car(Scan), Position + 2, Print);
1673
void st_Print(st_INDEX StIndex, void (*Print)(POINTER))
1674
/**************************************************************
1675
INPUT: The root of an St.
1676
SUMMARY: Prints a whole St.
1677
***************************************************************/
1681
if (st_Empty(StIndex)) {
1682
puts("\n\nIndex empty.");
1686
fputs("\n\nroot: ", stdout);
1687
printf(" Max: %d, Min: %d, ", st_Max(StIndex), st_Min(StIndex));
1688
subst_Print(StIndex->subst);
1690
if (st_IsLeaf(StIndex)) {
1691
fputs(" =>", stdout);
1694
for (Scan = StIndex->entries; Scan != NULL; Scan = list_Cdr(Scan)) {
1696
Print(list_Car(Scan));
1699
printf(" %d Entries", list_Length(StIndex->entries));
1702
for (Scan = StIndex->subnodes; Scan != NULL; Scan = list_Cdr(Scan))
1703
st_PrintHelp(list_Car(Scan),2, Print);