~ubuntu-branches/ubuntu/quantal/spass/quantal

« back to all changes in this revision

Viewing changes to SPASS/st.c

  • Committer: Bazaar Package Importer
  • Author(s): Roland Stigge
  • Date: 2010-06-27 18:59:28 UTC
  • mfrom: (1.1.1 upstream)
  • Revision ID: james.westby@ubuntu.com-20100627185928-kdjuqghv04rxyqmc
Tags: 3.7-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
 
1
/**************************************************************/
 
2
/* ********************************************************** */
 
3
/* *                                                        * */
 
4
/* *                    ST INDEXING                         * */
 
5
/* *                                                        * */
 
6
/* *  $Module:   ST                                         * */ 
 
7
/* *                                                        * */
 
8
/* *  Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001      * */
 
9
/* *  MPI fuer Informatik                                   * */
 
10
/* *                                                        * */
 
11
/* *  This program is free software; you can redistribute   * */
 
12
/* *  it and/or modify it under the terms of the FreeBSD    * */
 
13
/* *  Licence.                                              * */
 
14
/* *                                                        * */
 
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.                                     * */
 
20
/* *                                                        * */
 
21
/* *                                                        * */
 
22
/* $Revision: 1.3 $                                         * */
 
23
/* $State: Exp $                                            * */
 
24
/* $Date: 2010-02-22 14:09:59 $                             * */
 
25
/* $Author: weidenb $                                       * */
 
26
/* *                                                        * */
 
27
/* *             Contact:                                   * */
 
28
/* *             Christoph Weidenbach                       * */
 
29
/* *             MPI fuer Informatik                        * */
 
30
/* *             Stuhlsatzenhausweg 85                      * */
 
31
/* *             66123 Saarbruecken                         * */
 
32
/* *             Email: spass@mpi-inf.mpg.de                * */
 
33
/* *             Germany                                    * */
 
34
/* *                                                        * */
 
35
/* ********************************************************** */
 
36
/**************************************************************/
 
37
 
 
38
 
 
39
/* $RCSfile: st.c,v $ */
 
40
 
 
41
#include "st.h"
 
42
 
 
43
 
 
44
/**************************************************************/
 
45
/* Local Variables                                            */
 
46
/**************************************************************/
 
47
 
 
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;
 
52
 
 
53
/**************************************************************/
 
54
/* Global Variables                                           */
 
55
/**************************************************************/
 
56
 
 
57
ST_STACK st_STACK;
 
58
int      st_STACKPOINTER;
 
59
int      st_STACKSAVE;
 
60
 
 
61
 
 
62
/**************************************************************/
 
63
/* ********************************************************** */
 
64
/* *                                                        * */
 
65
/* *  CREATION OF INDEX                                     * */
 
66
/* *                                                        * */
 
67
/* ********************************************************** */
 
68
/**************************************************************/
 
69
 
 
70
 
 
71
st_INDEX st_IndexCreate(void)
 
72
/**************************************************************
 
73
  INPUT:   None.
 
74
  RETURNS: A pointer to a new St-Index.
 
75
  SUMMARY: Creates a new St-index.
 
76
***************************************************************/
 
77
{
 
78
  st_INDEX StIndex;
 
79
 
 
80
  StIndex           = st_Get();
 
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);
 
86
 
 
87
  return StIndex;
 
88
}
 
89
 
 
90
 
 
91
/**************************************************************/
 
92
/* ********************************************************** */
 
93
/* *                                                        * */
 
94
/* *  CREATION OF INDEX NODES                               * */
 
95
/* *                                                        * */
 
96
/* ********************************************************** */
 
97
/**************************************************************/
 
98
 
 
99
 
 
100
static st_INDEX st_NodeAddLeaf(SUBST Subst, st_MINMAX MinMax, POINTER Pointer)
 
101
/**************************************************************
 
102
  INPUT:   
 
103
  RETURNS: 
 
104
  EFFECTS: 
 
105
***************************************************************/
 
106
 
107
  st_INDEX NewLeaf;
 
108
 
 
109
  NewLeaf           = st_Get();
 
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);
 
115
 
 
116
  return NewLeaf;
 
117
}
 
118
 
 
119
 
 
120
static void st_NodeAddInner(st_INDEX StIndex, SUBST SubstOld, SUBST SubstNew,
 
121
                            SUBST ComGen, st_MINMAX MinMax, POINTER Pointer)
 
122
/**************************************************************
 
123
  INPUT:   
 
124
  RETURNS: 
 
125
  EFFECTS: 
 
126
***************************************************************/
 
127
{
 
128
  st_INDEX OldIndexNode;
 
129
 
 
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));
 
136
 
 
137
  subst_Delete(StIndex->subst);
 
138
 
 
139
  StIndex->subst         = ComGen;
 
140
  StIndex->entries       = list_Nil();
 
141
  StIndex->subnodes      = list_Cons(st_NodeAddLeaf(SubstNew, MinMax, Pointer),
 
142
                                     list_List(OldIndexNode));
 
143
 
 
144
  if (st_Max(StIndex) < MinMax)
 
145
    st_SetMax(StIndex, MinMax);
 
146
  else if (st_Min(StIndex) > MinMax)
 
147
    st_SetMin(StIndex, MinMax);
 
148
}
 
149
 
 
150
 
 
151
/**************************************************************/
 
152
/* ********************************************************** */
 
153
/* *                                                        * */
 
154
/* *  MERGING OF INDEX NODES                                * */
 
155
/* *                                                        * */
 
156
/* ********************************************************** */
 
157
/**************************************************************/
 
158
 
 
159
 
 
160
static void st_NodeMergeWithSon(st_INDEX StIndex)
 
161
/**************************************************************
 
162
  INPUT:   
 
163
  RETURNS: 
 
164
  EFFECTS: 
 
165
***************************************************************/
 
166
{
 
167
  st_INDEX SubNode;
 
168
 
 
169
  SubNode = (st_INDEX)list_Car(StIndex->subnodes);
 
170
 
 
171
  list_Delete(StIndex->subnodes);
 
172
 
 
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));
 
178
 
 
179
  subst_Delete(SubNode->subst);
 
180
 
 
181
  st_Free(SubNode);
 
182
}
 
183
 
 
184
 
 
185
/**************************************************************/
 
186
/* ********************************************************** */
 
187
/* *                                                        * */
 
188
/* *  VARIABLE HANDLING FOR TERMS AND SUBSTS.               * */
 
189
/* *                                                        * */
 
190
/* ********************************************************** */
 
191
/**************************************************************/
 
192
 
 
193
 
 
194
static void st_CloseUsedVariables(const CONTEXT Context, LIST NodeList)
 
195
/**************************************************************
 
196
  INPUT:   
 
197
  RETURNS: 
 
198
  EFFECTS: 
 
199
***************************************************************/
 
200
{
 
201
  for (; list_Exist(NodeList); NodeList = list_Cdr(NodeList)) {
 
202
    SUBST Subst;
 
203
 
 
204
    for (Subst = ((st_INDEX)list_Car(NodeList))->subst;
 
205
         subst_Exist(Subst);
 
206
         Subst = subst_Next(Subst))
 
207
      if (!cont_VarIsUsed(Context, subst_Dom(Subst)))
 
208
        cont_CreateClosedBinding(Context, subst_Dom(Subst));
 
209
 
 
210
    if (!st_IsLeaf((st_INDEX)list_Car(NodeList)))
 
211
      st_CloseUsedVariables(Context, ((st_INDEX)list_Car(NodeList))->subnodes);
 
212
  }
 
213
}
 
214
 
 
215
 
 
216
/**************************************************************/
 
217
/* ********************************************************** */
 
218
/* *                                                        * */
 
219
/* *  HEURISTICS FOR INSERTION OF TERMS AND SUBSTS.         * */
 
220
/* *                                                        * */
 
221
/* ********************************************************** */
 
222
/**************************************************************/
 
223
 
 
224
 
 
225
static st_INDEX st_FirstVariant(const CONTEXT Context, LIST Subnodes, st_INDEX* BestNonVariant)
 
226
/**************************************************************
 
227
  INPUT:   
 
228
  RETURNS: 
 
229
  EFFECTS: 
 
230
***************************************************************/
 
231
{
 
232
  st_INDEX EmptyVariant;
 
233
 
 
234
  for (EmptyVariant = NULL, *BestNonVariant = NULL;
 
235
       list_Exist(Subnodes);
 
236
       Subnodes = list_Cdr(Subnodes)) {
 
237
    st_INDEX CurrentNode;
 
238
 
 
239
    CurrentNode = (st_INDEX)list_Car(Subnodes);
 
240
 
 
241
    cont_StartBinding();
 
242
 
 
243
    if (subst_Variation(Context, CurrentNode->subst)) {
 
244
      if (subst_Exist(CurrentNode->subst)) {    
 
245
        subst_CloseVariables(Context, CurrentNode->subst);
 
246
 
 
247
        return CurrentNode;
 
248
      } else
 
249
        EmptyVariant = CurrentNode;
 
250
 
 
251
    } else if (*BestNonVariant == NULL)
 
252
      if (subst_MatchTops(Context, CurrentNode->subst))
 
253
        *BestNonVariant = CurrentNode;
 
254
 
 
255
    cont_BackTrack();
 
256
  }
 
257
 
 
258
  return EmptyVariant;
 
259
}
 
260
 
 
261
 
 
262
/**************************************************************/
 
263
/* ********************************************************** */
 
264
/* *                                                        * */
 
265
/* *  INSERTION OF TERMS                                    * */
 
266
/* *                                                        * */
 
267
/* ********************************************************** */
 
268
/**************************************************************/
 
269
 
 
270
 
 
271
void st_EntryCreate(st_INDEX StIndex, POINTER Pointer, TERM Term, const CONTEXT Context)
 
272
/**************************************************************
 
273
  INPUT:   
 
274
  RETURNS: 
 
275
  EFFECTS: 
 
276
***************************************************************/
 
277
{
 
278
  st_INDEX  Current;
 
279
  st_INDEX  BestNonVariant;
 
280
  SYMBOL    FirstDomain;
 
281
  st_MINMAX MinMax;
 
282
 
 
283
  cont_Check();
 
284
 
 
285
  MinMax         = term_ComputeSize(Term);
 
286
  BestNonVariant = (st_INDEX)NULL;
 
287
 
 
288
  /* CREATE INITIAL BINDING AND INITIALIZE LOCAL VARIABLES */
 
289
  FirstDomain = cont_NextIndexVariable(Context);
 
290
  cont_CreateBinding(Context, FirstDomain, Context, Term);
 
291
 
 
292
  Current = StIndex;
 
293
 
 
294
  if (st_Max(Current) < MinMax)
 
295
    st_SetMax(Current, MinMax);
 
296
  else if (st_Min(Current) > MinMax)
 
297
    st_SetMin(Current, MinMax);
 
298
 
 
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);
 
306
    
 
307
    StIndex = Current;
 
308
  }
 
309
 
 
310
  if (cont_BindingsSinceLastStart()==0 && Current && st_IsLeaf(Current)) {
 
311
    
 
312
    /* INSERT ENTRY EQUAL MODULO RENAMING */
 
313
    Current->entries = list_Cons(Pointer, Current->entries);
 
314
  
 
315
  } else if (BestNonVariant) {
 
316
    
 
317
    /* CREATE INNER NODE AND A NEW LEAF */
 
318
    SUBST ComGen, SubstOld, SubstNew;
 
319
 
 
320
    if (!st_IsLeaf(BestNonVariant))
 
321
      st_CloseUsedVariables(Context, BestNonVariant->subnodes);
 
322
 
 
323
    ComGen = subst_ComGen(Context, BestNonVariant->subst, &SubstOld, &SubstNew);
 
324
 
 
325
    st_NodeAddInner(BestNonVariant,
 
326
                    SubstOld,
 
327
                    subst_CloseOpenVariables(SubstNew),
 
328
                    ComGen,
 
329
                    MinMax,
 
330
                    Pointer);
 
331
    
 
332
  } else
 
333
    
 
334
    /* ADD A SINGLE LEAF NODE TO FATHER */
 
335
    StIndex->subnodes =
 
336
      list_Cons(st_NodeAddLeaf(subst_CloseOpenVariables(subst_Nil()), MinMax,
 
337
                               Pointer),
 
338
                StIndex->subnodes);
 
339
 
 
340
  cont_Reset();
 
341
}
 
342
 
 
343
 
 
344
/**************************************************************/
 
345
/* ********************************************************** */
 
346
/* *                                                        * */
 
347
/* *  DELETION OF INDEX                                     * */
 
348
/* *                                                        * */
 
349
/* ********************************************************** */
 
350
/**************************************************************/
 
351
 
 
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
 ***************************************************************/
 
358
{
 
359
        if (StIndex == NULL)
 
360
                return;
 
361
        else if (st_IsLeaf(StIndex))
 
362
                list_DeleteWithElement(StIndex->entries, (void (*) (POINTER)) term_Delete);
 
363
        else
 
364
                /* Recursion */
 
365
                list_DeleteWithElement(StIndex->subnodes,
 
366
                                (void(*)(POINTER)) st_IndexDeleteWithElement);
 
367
 
 
368
        subst_Delete(StIndex->subst);
 
369
        st_Free(StIndex);
 
370
 
 
371
}
 
372
 
 
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
***************************************************************/
 
378
{
 
379
  if (StIndex == NULL)
 
380
    return;
 
381
  else if (st_IsLeaf(StIndex))
 
382
    list_Delete(StIndex->entries);
 
383
  else
 
384
    /* Recursion */
 
385
    list_DeleteWithElement(StIndex->subnodes, (void (*)(POINTER))st_IndexDelete);
 
386
 
 
387
  subst_Delete(StIndex->subst);
 
388
  st_Free(StIndex);
 
389
}
 
390
 
 
391
 
 
392
/**************************************************************/
 
393
/* ********************************************************** */
 
394
/* *                                                        * */
 
395
/* *  DELETION OF ENTRY FOR TERMS                           * */
 
396
/* *                                                        * */
 
397
/* ********************************************************** */
 
398
/**************************************************************/
 
399
 
 
400
 
 
401
static st_INDEX st_EntryDeleteHelp(const CONTEXT Context, st_INDEX StIndex, POINTER Pointer,
 
402
                                   BOOL* Found)
 
403
/**************************************************************
 
404
  INPUT:   The root of an abstraction tree (StIndex), a
 
405
           pointer to a specific entry of the tree and
 
406
           a query term.
 
407
  RETURNS: Nothing.
 
408
  SUMMARY: Uses Term in order to find Pointer in the tree.
 
409
  EFFECTS: Will delete nodes of StIndex.
 
410
***************************************************************/
 
411
{
 
412
  if (st_IsLeaf(StIndex)) {
 
413
 
 
414
    *Found = list_DeleteFromList(&(StIndex->entries), Pointer);
 
415
 
 
416
    if (list_Exist(StIndex->entries))
 
417
      return StIndex;
 
418
    else {
 
419
      subst_Delete(StIndex->subst);
 
420
      st_Free(StIndex);
 
421
 
 
422
      return NULL;
 
423
    }
 
424
 
 
425
  } else {
 
426
 
 
427
    LIST Subnodes;
 
428
 
 
429
    for (Subnodes = StIndex->subnodes;
 
430
         list_Exist(Subnodes);
 
431
         Subnodes = list_Cdr(Subnodes)) {
 
432
      st_INDEX CurrentNode;
 
433
 
 
434
      CurrentNode = (st_INDEX)list_Car(Subnodes);
 
435
 
 
436
      cont_StartBinding();
 
437
 
 
438
      if (subst_Variation(Context, CurrentNode->subst)) {
 
439
        list_Rplaca(Subnodes, st_EntryDeleteHelp(Context,
 
440
                                                 CurrentNode,
 
441
                                                 Pointer,
 
442
                                                 Found));
 
443
        if (*Found) {
 
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);
 
448
          
 
449
              return StIndex;
 
450
            }
 
451
 
 
452
          /* Assertion: 'StIndex' is an inner node. */
 
453
 
 
454
          CurrentNode      = (st_INDEX)list_Car(StIndex->subnodes);
 
455
          st_SetMax(StIndex, st_Max(CurrentNode));
 
456
          st_SetMin(StIndex, st_Min(CurrentNode));
 
457
 
 
458
          for (Subnodes = list_Cdr(StIndex->subnodes);
 
459
               list_Exist(Subnodes);
 
460
               Subnodes = list_Cdr(Subnodes)) {
 
461
            CurrentNode = (st_INDEX)list_Car(Subnodes);
 
462
 
 
463
            if (st_Max(CurrentNode) > st_Max(StIndex))
 
464
              st_SetMax(StIndex, st_Max(CurrentNode));
 
465
 
 
466
            if (st_Min(CurrentNode) < st_Min(StIndex))
 
467
              st_SetMin(StIndex, st_Min(CurrentNode));
 
468
          }
 
469
 
 
470
          return StIndex;
 
471
        }
 
472
      }
 
473
 
 
474
      cont_BackTrack();
 
475
    }
 
476
 
 
477
    return StIndex;
 
478
  }
 
479
}
 
480
 
 
481
 
 
482
BOOL st_EntryDelete(st_INDEX StIndex, POINTER Pointer, TERM Term, const CONTEXT Context)
 
483
/**************************************************************
 
484
  INPUT:   
 
485
  RETURNS: 
 
486
  EFFECTS: 
 
487
***************************************************************/
 
488
 
489
  BOOL   Found;
 
490
  LIST   Subnodes;
 
491
  SYMBOL FirstDomain;
 
492
 
 
493
  cont_Check();
 
494
 
 
495
  FirstDomain = symbol_FirstIndexVariable();
 
496
  cont_CreateBinding(Context, FirstDomain, Context, Term);
 
497
 
 
498
  for (Found = FALSE, Subnodes = StIndex->subnodes;
 
499
       list_Exist(Subnodes);
 
500
       Subnodes = list_Cdr(Subnodes)) {
 
501
    st_INDEX CurrentNode;
 
502
 
 
503
    CurrentNode = (st_INDEX)list_Car(Subnodes);
 
504
 
 
505
    cont_StartBinding();
 
506
 
 
507
    if (subst_Variation(Context, CurrentNode->subst)) {
 
508
      list_Rplaca(Subnodes, st_EntryDeleteHelp(Context, CurrentNode, Pointer, &Found));
 
509
 
 
510
      if (Found) {
 
511
        StIndex->subnodes = list_PointerDeleteElement(StIndex->subnodes, NULL);
 
512
 
 
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));
 
517
 
 
518
          for (Subnodes = list_Cdr(StIndex->subnodes);
 
519
               list_Exist(Subnodes);
 
520
               Subnodes = list_Cdr(Subnodes)) {
 
521
            CurrentNode = (st_INDEX)list_Car(Subnodes);
 
522
 
 
523
            if (st_Max(CurrentNode) > st_Max(StIndex))
 
524
              st_SetMax(StIndex, st_Max(CurrentNode));
 
525
 
 
526
            if (st_Min(CurrentNode) < st_Min(StIndex))
 
527
              st_SetMin(StIndex, st_Min(CurrentNode));
 
528
          }
 
529
        } else {
 
530
          st_SetMax(StIndex, 0);
 
531
          st_SetMin(StIndex, 0);
 
532
        }
 
533
 
 
534
        break;
 
535
      }
 
536
    }
 
537
 
 
538
    cont_BackTrack();
 
539
  }
 
540
 
 
541
  cont_Reset();
 
542
 
 
543
  return Found;
 
544
}
 
545
 
 
546
 
 
547
/**************************************************************/
 
548
/* ********************************************************** */
 
549
/* *                                                        * */
 
550
/* *  RETRIEVAL FOR TERMS                                   * */
 
551
/* *                                                        * */
 
552
/* ********************************************************** */
 
553
/**************************************************************/
 
554
 
 
555
 
 
556
static LIST st_TraverseTreeUnifier(CONTEXT IndexContext, st_INDEX StIndex)
 
557
/**************************************************************
 
558
  INPUT:   
 
559
  RETURNS: 
 
560
  EFFECTS: 
 
561
***************************************************************/
 
562
{
 
563
  int      Save;
 
564
  LIST     Result, CurrentList;
 
565
  st_INDEX CurrentNode;
 
566
 
 
567
  /* PREPARE TRAVERSAL */
 
568
  Save = stack_Bottom();
 
569
 
 
570
  Result      = list_Nil();
 
571
  CurrentList = StIndex->subnodes;
 
572
  
 
573
  cont_StartBinding();
 
574
 
 
575
  for (;;) {
 
576
    
 
577
    /* BACKTRACK A BIG STEP */
 
578
    if (list_Empty(CurrentList)) {
 
579
      cont_StopAndBackTrack();
 
580
 
 
581
      if (stack_Empty(Save))
 
582
        return Result;
 
583
 
 
584
      CurrentList = stack_PopResult();
 
585
    }
 
586
    
 
587
    /* DESCENDING */
 
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);
 
594
        break;
 
595
      } else if (list_Exist(list_Cdr(CurrentList))) {
 
596
        stack_Push(list_Cdr(CurrentList));
 
597
        cont_StartBinding();
 
598
      } else
 
599
        cont_StopAndStartBinding();
 
600
    
 
601
    /* BACKTRACK LEAF OR INNER NODE */
 
602
    CurrentList = list_Cdr(CurrentList);
 
603
    cont_BackTrackAndStart();
 
604
  }
 
605
}
 
606
 
 
607
 
 
608
static LIST st_TraverseTreeGen(CONTEXT IndexContext, st_INDEX StIndex)
 
609
/**************************************************************
 
610
  INPUT:   
 
611
  RETURNS: 
 
612
  EFFECTS: 
 
613
***************************************************************/
 
614
{
 
615
  int      Save;
 
616
  LIST     Result, CurrentList;
 
617
  st_INDEX CurrentNode;
 
618
 
 
619
  /* PREPARE TRAVERSAL */
 
620
  Save = stack_Bottom();
 
621
 
 
622
  Result      = list_Nil();
 
623
  CurrentList = StIndex->subnodes;
 
624
 
 
625
  cont_StartBinding();
 
626
  
 
627
  for (;;) {
 
628
    
 
629
    /* BACKTRACK A BIG STEP */
 
630
    if (list_Empty(CurrentList)) {
 
631
      cont_StopAndBackTrack();
 
632
 
 
633
      if (stack_Empty(Save))
 
634
        return Result;
 
635
 
 
636
      CurrentList = stack_PopResult();
 
637
    }
 
638
    
 
639
    /* DESCENDING */
 
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);
 
646
        break;
 
647
      } else if (list_Cdr(CurrentList)) {
 
648
        stack_Push(list_Cdr(CurrentList));
 
649
        cont_StartBinding();
 
650
      } else
 
651
        cont_StopAndStartBinding();
 
652
    
 
653
    /* BACKTRACK LEAF OR INNER NODE */
 
654
    CurrentList = list_Cdr(CurrentList);
 
655
    cont_BackTrackAndStart();
 
656
  }
 
657
}
 
658
 
 
659
 
 
660
static LIST st_TraverseTreeInstance(CONTEXT IndexContext, st_INDEX StIndex)
 
661
/**************************************************************
 
662
  INPUT:   
 
663
  RETURNS: 
 
664
  EFFECTS: 
 
665
***************************************************************/
 
666
{
 
667
  int      Save;
 
668
  LIST     Result, CurrentList;
 
669
  st_INDEX CurrentNode;
 
670
 
 
671
  /* PREPARE TRAVERSAL */
 
672
  Save = stack_Bottom();
 
673
 
 
674
  Result      = list_Nil();
 
675
  CurrentList = StIndex->subnodes;
 
676
 
 
677
  cont_StartBinding();
 
678
 
 
679
  for (;;) {
 
680
    
 
681
    /* BACKTRACK A BIG STEP */
 
682
    if (list_Empty(CurrentList)) {
 
683
      cont_StopAndBackTrack();
 
684
 
 
685
      if (stack_Empty(Save))
 
686
        return Result;
 
687
 
 
688
      CurrentList = stack_PopResult();
 
689
    }
 
690
    
 
691
    /* DESCENDING */
 
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);
 
698
        break;
 
699
      } else if (list_Cdr(CurrentList)) {
 
700
        stack_Push(list_Cdr(CurrentList));
 
701
        cont_StartBinding();
 
702
      } else
 
703
        cont_StopAndStartBinding();
 
704
    
 
705
    /* BACKTRACK LEAF OR INNER NODE */
 
706
    CurrentList = list_Cdr(CurrentList);
 
707
    cont_BackTrackAndStart();
 
708
  }
 
709
}
 
710
 
 
711
 
 
712
static LIST st_TraverseTreeGenPreTest(CONTEXT IndexContext,
 
713
                                      st_INDEX StIndex,
 
714
                                      st_MINMAX MinMax)
 
715
/**************************************************************
 
716
  INPUT:   
 
717
  RETURNS: 
 
718
  EFFECTS: 
 
719
***************************************************************/
 
720
{
 
721
  int      Save;
 
722
  LIST     Result, CurrentList;
 
723
  st_INDEX CurrentNode;
 
724
 
 
725
  /* PREPARE TRAVERSAL */
 
726
  Save = stack_Bottom();
 
727
 
 
728
  Result      = list_Nil();
 
729
  CurrentList = StIndex->subnodes;
 
730
 
 
731
  cont_StartBinding();
 
732
 
 
733
  for (;;) {
 
734
    
 
735
    /* BACKTRACK A BIG STEP */
 
736
    if (list_Empty(CurrentList)) {
 
737
      cont_StopAndBackTrack();
 
738
 
 
739
      if (stack_Empty(Save))
 
740
        return Result;
 
741
 
 
742
      CurrentList = stack_PopResult();
 
743
    }
 
744
    
 
745
    /* DESCENDING */
 
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);
 
753
        break;
 
754
      } else if (list_Cdr(CurrentList)) {
 
755
        stack_Push(list_Cdr(CurrentList));
 
756
        cont_StartBinding();
 
757
      } else
 
758
        cont_StopAndStartBinding();
 
759
 
 
760
    /* BACKTRACK LEAF OR INNER NODE */
 
761
    CurrentList = list_Cdr(CurrentList);
 
762
    cont_BackTrackAndStart();
 
763
  }
 
764
}
 
765
 
 
766
 
 
767
static LIST st_TraverseTreeInstancePreTest(CONTEXT IndexContext, st_INDEX StIndex, st_MINMAX MinMax)
 
768
/**************************************************************
 
769
  INPUT:   
 
770
  RETURNS: 
 
771
  EFFECTS: 
 
772
***************************************************************/
 
773
{
 
774
  int      Save;
 
775
  LIST     Result, CurrentList;
 
776
  st_INDEX CurrentNode;
 
777
 
 
778
  /* PREPARE TRAVERSAL */
 
779
  Save = stack_Bottom();
 
780
 
 
781
  Result      = list_Nil();
 
782
  CurrentList = StIndex->subnodes;
 
783
 
 
784
  cont_StartBinding();
 
785
 
 
786
  for (;;) {
 
787
    
 
788
    /* BACKTRACK A BIG STEP */
 
789
    if (list_Empty(CurrentList)) {
 
790
      cont_StopAndBackTrack();
 
791
 
 
792
      if (stack_Empty(Save))
 
793
        return Result;
 
794
 
 
795
      CurrentList = stack_PopResult();
 
796
    }
 
797
    
 
798
    /* DESCENDING */
 
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);
 
806
        break;
 
807
      } else if (list_Cdr(CurrentList)) {
 
808
        stack_Push(list_Cdr(CurrentList));
 
809
        cont_StartBinding();
 
810
      } else
 
811
        cont_StopAndStartBinding();
 
812
 
 
813
    /* BACKTRACK LEAF OR INNER NODE */
 
814
    CurrentList = list_Cdr(CurrentList);
 
815
    cont_BackTrackAndStart();
 
816
  }
 
817
}
 
818
 
 
819
 
 
820
LIST st_GetUnifier(CONTEXT IndexContext, st_INDEX StIndex, CONTEXT TermContext, TERM Term)
 
821
/**************************************************************
 
822
  INPUT:   
 
823
  RETURNS: 
 
824
  EFFECTS: 
 
825
***************************************************************/
 
826
{
 
827
  LIST   Result;
 
828
  SYMBOL FirstDomain;
 
829
 
 
830
  cont_Check();
 
831
 
 
832
  FirstDomain = symbol_FirstIndexVariable();
 
833
  cont_CreateBinding(IndexContext, FirstDomain, TermContext, Term);
 
834
 
 
835
  Result = st_TraverseTreeUnifier(IndexContext, StIndex);
 
836
 
 
837
  cont_Reset();
 
838
  
 
839
  return Result;
 
840
}
 
841
 
 
842
 
 
843
LIST st_GetGen(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
 
844
/**************************************************************
 
845
  INPUT:   
 
846
  RETURNS: 
 
847
  EFFECTS: 
 
848
***************************************************************/
 
849
{
 
850
  LIST   Result;
 
851
  SYMBOL FirstDomain;
 
852
 
 
853
  cont_Check();
 
854
 
 
855
  FirstDomain = symbol_FirstIndexVariable();
 
856
  cont_CreateBinding(IndexContext, FirstDomain, cont_InstanceContext(), Term);
 
857
 
 
858
  Result = st_TraverseTreeGen(IndexContext, StIndex);
 
859
 
 
860
  cont_Reset();
 
861
  
 
862
  return Result;
 
863
}
 
864
 
 
865
 
 
866
LIST st_GetGenPreTest(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
 
867
/**************************************************************
 
868
  INPUT:   
 
869
  RETURNS: 
 
870
  EFFECTS: 
 
871
***************************************************************/
 
872
{
 
873
  LIST   Result;
 
874
  SYMBOL FirstDomain;
 
875
 
 
876
  cont_Check();
 
877
 
 
878
  FirstDomain = symbol_FirstIndexVariable();
 
879
  cont_CreateBinding(IndexContext, FirstDomain, cont_InstanceContext(), Term);
 
880
 
 
881
  Result = st_TraverseTreeGenPreTest(IndexContext, StIndex, term_ComputeSize(Term));
 
882
 
 
883
  cont_Reset();
 
884
  
 
885
  return Result;
 
886
}
 
887
 
 
888
 
 
889
LIST st_GetInstance(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
 
890
/**************************************************************
 
891
  INPUT:   
 
892
  RETURNS: 
 
893
  EFFECTS: 
 
894
***************************************************************/
 
895
{
 
896
  LIST   Result;
 
897
  SYMBOL FirstDomain;
 
898
 
 
899
  cont_Check();
 
900
 
 
901
  FirstDomain = symbol_FirstIndexVariable();
 
902
  cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term);
 
903
 
 
904
  Result = st_TraverseTreeInstance(IndexContext, StIndex);
 
905
 
 
906
  cont_Reset();
 
907
  
 
908
  return Result;
 
909
}
 
910
 
 
911
 
 
912
LIST st_GetInstancePreTest(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
 
913
/**************************************************************
 
914
  INPUT:   
 
915
  RETURNS: 
 
916
  EFFECTS: 
 
917
***************************************************************/
 
918
{
 
919
  LIST   Result;
 
920
  SYMBOL FirstDomain;
 
921
 
 
922
  cont_Check();
 
923
 
 
924
  FirstDomain = symbol_FirstIndexVariable();
 
925
  cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term);
 
926
 
 
927
  Result = st_TraverseTreeInstancePreTest(IndexContext, StIndex, term_ComputeSize(Term));
 
928
 
 
929
  cont_Reset();
 
930
  
 
931
  return Result;
 
932
}
 
933
 
 
934
 
 
935
/**************************************************************/
 
936
/* ********************************************************** */
 
937
/* *                                                        * */
 
938
/* *  INCREMENTAL RETRIEVAL                                 * */
 
939
/* *                                                        * */
 
940
/* ********************************************************** */
 
941
/**************************************************************/
 
942
 
 
943
 
 
944
static POINTER st_TraverseForExistUnifier(CONTEXT IndexContext)
 
945
/**************************************************************
 
946
  INPUT:   
 
947
  RETURNS: 
 
948
  EFFECTS: 
 
949
***************************************************************/
 
950
{
 
951
  LIST     CurrentList;
 
952
  st_INDEX CurrentNode;
 
953
 
 
954
  /* Caution: In case an entry is found
 
955
     the procedure returns immediately
 
956
     without backtracking the current bindings. */
 
957
 
 
958
  CurrentList = list_Nil();
 
959
  
 
960
  for (;;) {
 
961
    
 
962
    /* BACKTRACK A BIG STEP */
 
963
    if (list_Empty(CurrentList)) {
 
964
      cont_StopAndBackTrack();
 
965
 
 
966
      if (st_StackEmpty(st_STACKSAVE))
 
967
        return NULL;
 
968
 
 
969
      CurrentList = st_StackPopResult();
 
970
    }
 
971
    
 
972
    /* DESCENDING */
 
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));
 
979
        cont_StartBinding();
 
980
      } else
 
981
        cont_StopAndStartBinding();
 
982
    
 
983
      if (st_IsLeaf(CurrentNode)) {
 
984
        st_StackPush(list_Cdr(CurrentNode->entries));
 
985
        return list_Car(CurrentNode->entries);
 
986
      }
 
987
    }
 
988
    
 
989
    /* BACKTRACK LEAF OR INNER NODE */
 
990
    CurrentList = list_Cdr(CurrentList);
 
991
    cont_BackTrackAndStart();
 
992
  }
 
993
}
 
994
 
 
995
 
 
996
static POINTER st_TraverseForExistGen(CONTEXT IndexContext)
 
997
/**************************************************************
 
998
  INPUT:   
 
999
  RETURNS: 
 
1000
  EFFECTS: 
 
1001
***************************************************************/
 
1002
{
 
1003
  LIST     CurrentList;
 
1004
  st_INDEX CurrentNode;
 
1005
 
 
1006
  /* Caution: In case an entry is found
 
1007
     the procedure returns immediately
 
1008
     without backtracking the current bindings. */
 
1009
 
 
1010
  CurrentList = list_Nil();
 
1011
  
 
1012
  for (;;) {
 
1013
    
 
1014
    /* BACKTRACK A BIG STEP */
 
1015
    if (list_Empty(CurrentList)) {
 
1016
      cont_StopAndBackTrack();
 
1017
 
 
1018
      if (st_StackEmpty(st_STACKSAVE))
 
1019
        return NULL;
 
1020
 
 
1021
      CurrentList = st_StackPopResult();
 
1022
    }
 
1023
    
 
1024
    /* DESCENDING */
 
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();
 
1032
      } else
 
1033
        cont_StopAndStartBinding();
 
1034
 
 
1035
      if (st_IsLeaf(CurrentNode)) {
 
1036
        st_StackPush(list_Cdr(CurrentNode->entries));
 
1037
        return list_Car(CurrentNode->entries);
 
1038
      }
 
1039
    }
 
1040
    
 
1041
    /* BACKTRACK LEAF OR INNER NODE */
 
1042
    CurrentList = list_Cdr(CurrentList);
 
1043
    cont_BackTrackAndStart();
 
1044
  }
 
1045
}
 
1046
 
 
1047
 
 
1048
static POINTER st_TraverseForExistGenPreTest(CONTEXT IndexContext)
 
1049
/**************************************************************
 
1050
  INPUT:   
 
1051
  RETURNS: 
 
1052
  EFFECTS: 
 
1053
***************************************************************/
 
1054
{
 
1055
  LIST     CurrentList;
 
1056
  st_INDEX CurrentNode;
 
1057
 
 
1058
  /* Caution: In case an entry is found
 
1059
     the procedure returns immediately
 
1060
     without backtracking the current bindings. */
 
1061
 
 
1062
  CurrentList = list_Nil();
 
1063
  
 
1064
  for (;;) {
 
1065
    
 
1066
    /* BACKTRACK A BIG STEP */
 
1067
    if (list_Empty(CurrentList)) {
 
1068
      cont_StopAndBackTrack();
 
1069
 
 
1070
      if (st_StackEmpty(st_STACKSAVE))
 
1071
        return NULL;
 
1072
 
 
1073
      CurrentList = st_StackPopResult();
 
1074
    }
 
1075
    
 
1076
    /* DESCENDING */
 
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();
 
1085
      } else
 
1086
        cont_StopAndStartBinding();
 
1087
 
 
1088
      if (st_IsLeaf(CurrentNode)) {
 
1089
        st_StackPush(list_Cdr(CurrentNode->entries));
 
1090
        return list_Car(CurrentNode->entries);
 
1091
      }
 
1092
    }
 
1093
    
 
1094
    /* BACKTRACK LEAF OR INNER NODE */
 
1095
    CurrentList = list_Cdr(CurrentList);
 
1096
    cont_BackTrackAndStart();
 
1097
  }
 
1098
}
 
1099
 
 
1100
 
 
1101
static POINTER st_TraverseForExistInstance(CONTEXT IndexContext)
 
1102
/**************************************************************
 
1103
  INPUT:   
 
1104
  RETURNS: 
 
1105
  EFFECTS: 
 
1106
***************************************************************/
 
1107
{
 
1108
  LIST     CurrentList;
 
1109
  st_INDEX CurrentNode;
 
1110
 
 
1111
  /* Caution: In case an entry is found
 
1112
     the procedure returns immediately
 
1113
     without backtracking the current bindings. */
 
1114
 
 
1115
  CurrentList = list_Nil();
 
1116
  
 
1117
  for (;;) {
 
1118
    
 
1119
    /* BACKTRACK A BIG STEP */
 
1120
    if (list_Empty(CurrentList)) {
 
1121
      cont_StopAndBackTrack();
 
1122
 
 
1123
      if (st_StackEmpty(st_STACKSAVE))
 
1124
        return NULL;
 
1125
 
 
1126
      CurrentList = st_StackPopResult();
 
1127
    }
 
1128
    
 
1129
    /* DESCENDING */
 
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();
 
1137
      } else
 
1138
        cont_StopAndStartBinding();
 
1139
 
 
1140
      if (st_IsLeaf(CurrentNode)) {
 
1141
        st_StackPush(list_Cdr(CurrentNode->entries));
 
1142
        return list_Car(CurrentNode->entries);
 
1143
      }
 
1144
    }
 
1145
    
 
1146
    /* BACKTRACK LEAF OR INNER NODE */
 
1147
    CurrentList = list_Cdr(CurrentList);
 
1148
    cont_BackTrackAndStart();
 
1149
  }
 
1150
}
 
1151
 
 
1152
 
 
1153
static POINTER st_TraverseForExistInstancePreTest(CONTEXT IndexContext)
 
1154
/**************************************************************
 
1155
  INPUT:   
 
1156
  RETURNS: 
 
1157
  EFFECTS: 
 
1158
***************************************************************/
 
1159
{
 
1160
  LIST     CurrentList;
 
1161
  st_INDEX CurrentNode;
 
1162
 
 
1163
  /* Caution: In case an entry is found
 
1164
     the procedure returns immediately
 
1165
     without backtracking the current bindings. */
 
1166
 
 
1167
  CurrentList = list_Nil();
 
1168
  
 
1169
  for (;;) {
 
1170
    
 
1171
    /* BACKTRACK A BIG STEP */
 
1172
    if (list_Empty(CurrentList)) {
 
1173
      cont_StopAndBackTrack();
 
1174
 
 
1175
      if (st_StackEmpty(st_STACKSAVE))
 
1176
        return NULL;
 
1177
 
 
1178
      CurrentList = st_StackPopResult();
 
1179
    }
 
1180
    
 
1181
    /* DESCENDING */
 
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();
 
1190
      } else
 
1191
        cont_StopAndStartBinding();
 
1192
 
 
1193
      if (st_IsLeaf(CurrentNode)) {
 
1194
        st_StackPush(list_Cdr(CurrentNode->entries));
 
1195
        return list_Car(CurrentNode->entries);
 
1196
      }
 
1197
    }
 
1198
    
 
1199
    /* BACKTRACK LEAF OR INNER NODE */
 
1200
    CurrentList = list_Cdr(CurrentList);
 
1201
    cont_BackTrackAndStart();
 
1202
  }
 
1203
}
 
1204
 
 
1205
 
 
1206
void st_CancelExistRetrieval(void)
 
1207
/**************************************************************
 
1208
  INPUT:   
 
1209
  RETURNS: 
 
1210
  EFFECTS: 
 
1211
***************************************************************/
 
1212
{
 
1213
  if (st_CURRENT_RETRIEVAL != st_NOP) {
 
1214
 
 
1215
#ifdef CHECK
 
1216
    cont_CheckState();
 
1217
#endif
 
1218
 
 
1219
    st_StackSetBottom(st_STACKSAVE);
 
1220
 
 
1221
    switch (st_WHICH_CONTEXTS) {
 
1222
 
 
1223
    case st_STANDARD:
 
1224
      cont_Reset();
 
1225
      break;
 
1226
 
 
1227
    case st_NOC:
 
1228
      break;
 
1229
 
 
1230
    default:
 
1231
      misc_StartErrorReport();
 
1232
      misc_ErrorReport("\n In st_CancelExistRetrieval: Unknown context type.\n");
 
1233
      misc_FinishErrorReport();
 
1234
    }
 
1235
 
 
1236
    st_CURRENT_RETRIEVAL = st_NOP;
 
1237
    st_WHICH_CONTEXTS    = st_NOC;
 
1238
    st_INDEX_CONTEXT     = NULL;
 
1239
    st_EXIST_MINMAX      = 0;
 
1240
  }
 
1241
}
 
1242
 
 
1243
 
 
1244
POINTER st_ExistUnifier(CONTEXT IndexContext, st_INDEX StIndex, CONTEXT TermContext, TERM Term)
 
1245
/**************************************************************
 
1246
  INPUT:   
 
1247
  RETURNS: 
 
1248
  EFFECTS: 
 
1249
***************************************************************/
 
1250
{
 
1251
  SYMBOL  FirstDomain;
 
1252
  POINTER Result;
 
1253
 
 
1254
#ifdef CHECK
 
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();
 
1264
  }
 
1265
#endif
 
1266
 
 
1267
  cont_Check();
 
1268
 
 
1269
  if (st_Exist(StIndex)) {
 
1270
 
 
1271
    st_CURRENT_RETRIEVAL = st_UNIFIER;
 
1272
    st_WHICH_CONTEXTS    = st_STANDARD;
 
1273
    st_INDEX_CONTEXT     = IndexContext;
 
1274
 
 
1275
    st_STACKSAVE = st_StackBottom();
 
1276
 
 
1277
    FirstDomain = symbol_FirstIndexVariable();
 
1278
    cont_CreateBinding(IndexContext, FirstDomain, TermContext, Term);
 
1279
 
 
1280
    cont_StartBinding();
 
1281
    st_StackPush(StIndex->subnodes);
 
1282
    cont_StartBinding();
 
1283
 
 
1284
    Result = st_TraverseForExistUnifier(IndexContext);
 
1285
 
 
1286
#ifdef CHECK
 
1287
    cont_SaveState();
 
1288
#endif
 
1289
 
 
1290
    if (Result == NULL)
 
1291
      st_CancelExistRetrieval();
 
1292
 
 
1293
    return Result;
 
1294
  } else
 
1295
    return NULL;
 
1296
}
 
1297
 
 
1298
 
 
1299
POINTER st_ExistGen(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
 
1300
/**************************************************************
 
1301
  INPUT:   
 
1302
  RETURNS: 
 
1303
  EFFECTS: 
 
1304
***************************************************************/
 
1305
{
 
1306
  SYMBOL  FirstDomain;
 
1307
  POINTER Result;
 
1308
 
 
1309
#ifdef CHECK
 
1310
  if (!st_StackEmpty(st_STACKSAVE)) {
 
1311
    misc_StartErrorReport();
 
1312
    misc_ErrorReport("\n In st_ExistGen: ST-Stack not empty.\n");
 
1313
    misc_FinishErrorReport();
 
1314
  } 
 
1315
  else 
 
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();
 
1321
    }
 
1322
#endif
 
1323
 
 
1324
  cont_Check();
 
1325
 
 
1326
  if (st_Exist(StIndex)) {
 
1327
 
 
1328
    st_CURRENT_RETRIEVAL = st_GEN;
 
1329
    st_WHICH_CONTEXTS    = st_STANDARD;
 
1330
    st_INDEX_CONTEXT     = IndexContext;
 
1331
  
 
1332
    st_STACKSAVE = st_StackBottom();
 
1333
 
 
1334
    FirstDomain = symbol_FirstIndexVariable();
 
1335
    cont_CreateBinding(IndexContext, FirstDomain, cont_InstanceContext(), Term);
 
1336
 
 
1337
    cont_StartBinding();
 
1338
    st_StackPush(StIndex->subnodes);
 
1339
    cont_StartBinding();
 
1340
 
 
1341
    Result = st_TraverseForExistGen(IndexContext);
 
1342
 
 
1343
#ifdef CHECK
 
1344
    cont_SaveState();
 
1345
#endif
 
1346
 
 
1347
    if (Result == NULL)
 
1348
      st_CancelExistRetrieval();
 
1349
 
 
1350
    return Result;
 
1351
  } else
 
1352
    return NULL;
 
1353
}
 
1354
 
 
1355
 
 
1356
POINTER st_ExistGenPreTest(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
 
1357
/**************************************************************
 
1358
  INPUT:   
 
1359
  RETURNS: 
 
1360
  EFFECTS: 
 
1361
***************************************************************/
 
1362
{
 
1363
  SYMBOL  FirstDomain;
 
1364
  POINTER Result;
 
1365
 
 
1366
#ifdef CHECK
 
1367
  if (!st_StackEmpty(st_STACKSAVE)) {
 
1368
    misc_StartErrorReport();
 
1369
    misc_ErrorReport("\n In st_ExistGenPreTest: ST-Stack not empty.\n");
 
1370
    misc_FinishErrorReport();
 
1371
  } 
 
1372
  else 
 
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();
 
1378
    }
 
1379
#endif
 
1380
 
 
1381
  cont_Check();
 
1382
 
 
1383
  if (st_Exist(StIndex)) {
 
1384
 
 
1385
    st_CURRENT_RETRIEVAL = st_GENPRETEST;
 
1386
    st_WHICH_CONTEXTS    = st_STANDARD;
 
1387
    st_INDEX_CONTEXT     = IndexContext;
 
1388
  
 
1389
    st_STACKSAVE = st_StackBottom();
 
1390
 
 
1391
 
 
1392
    FirstDomain     = symbol_FirstIndexVariable();
 
1393
    st_EXIST_MINMAX = term_ComputeSize(Term);
 
1394
    cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term);
 
1395
 
 
1396
    cont_StartBinding();
 
1397
    st_StackPush(StIndex->subnodes);
 
1398
    cont_StartBinding();
 
1399
 
 
1400
    Result = st_TraverseForExistGenPreTest(IndexContext);
 
1401
 
 
1402
#ifdef CHECK
 
1403
    cont_SaveState();
 
1404
#endif
 
1405
 
 
1406
    if (Result == NULL)
 
1407
      st_CancelExistRetrieval();
 
1408
 
 
1409
    return Result;
 
1410
  } else
 
1411
    return NULL;
 
1412
}
 
1413
 
 
1414
 
 
1415
POINTER st_ExistInstance(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
 
1416
/**************************************************************
 
1417
  INPUT:   
 
1418
  RETURNS: 
 
1419
  EFFECTS: 
 
1420
***************************************************************/
 
1421
{
 
1422
  SYMBOL  FirstDomain;
 
1423
  POINTER Result;
 
1424
 
 
1425
#ifdef CHECK
 
1426
  if (!st_StackEmpty(st_STACKSAVE)) {
 
1427
    misc_StartErrorReport();
 
1428
    misc_ErrorReport("\n In st_ExistInstance: ST-Stack not empty.\n");
 
1429
    misc_FinishErrorReport();
 
1430
  } 
 
1431
  else 
 
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();
 
1437
    }
 
1438
#endif
 
1439
 
 
1440
  cont_Check();
 
1441
 
 
1442
  if (st_Exist(StIndex)) {
 
1443
 
 
1444
    st_CURRENT_RETRIEVAL = st_INSTANCE;
 
1445
    st_WHICH_CONTEXTS    = st_STANDARD;
 
1446
    st_INDEX_CONTEXT     = IndexContext;
 
1447
 
 
1448
    st_STACKSAVE = st_StackBottom();
 
1449
 
 
1450
    FirstDomain = symbol_FirstIndexVariable();
 
1451
    cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term);
 
1452
 
 
1453
    cont_StartBinding();
 
1454
    st_StackPush(StIndex->subnodes);
 
1455
    cont_StartBinding();
 
1456
 
 
1457
    Result = st_TraverseForExistInstance(IndexContext);
 
1458
 
 
1459
#ifdef CHECK
 
1460
    cont_SaveState();
 
1461
#endif
 
1462
 
 
1463
    if (Result == NULL)
 
1464
      st_CancelExistRetrieval();
 
1465
 
 
1466
    return Result;
 
1467
  } else
 
1468
    return NULL;
 
1469
}
 
1470
 
 
1471
 
 
1472
POINTER st_ExistInstancePreTest(CONTEXT IndexContext, st_INDEX StIndex, TERM Term)
 
1473
/**************************************************************
 
1474
  INPUT:   
 
1475
  RETURNS: 
 
1476
  EFFECTS: 
 
1477
***************************************************************/
 
1478
{
 
1479
  SYMBOL  FirstDomain;
 
1480
  POINTER Result;
 
1481
 
 
1482
#ifdef CHECK
 
1483
  if (!st_StackEmpty(st_STACKSAVE)) {
 
1484
    misc_StartErrorReport();
 
1485
    misc_ErrorReport("\n In st_ExistInstancePreTest: ST-Stack not empty.\n");
 
1486
    misc_FinishErrorReport();
 
1487
  } 
 
1488
  else 
 
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();
 
1494
    }
 
1495
#endif
 
1496
 
 
1497
  cont_Check();
 
1498
 
 
1499
  if (st_Exist(StIndex)) {
 
1500
 
 
1501
    st_CURRENT_RETRIEVAL = st_INSTANCEPRETEST;
 
1502
    st_WHICH_CONTEXTS    = st_STANDARD;
 
1503
    st_INDEX_CONTEXT     = IndexContext;
 
1504
 
 
1505
    st_STACKSAVE = st_StackBottom();
 
1506
 
 
1507
    FirstDomain     = symbol_FirstIndexVariable();
 
1508
    st_EXIST_MINMAX = term_ComputeSize(Term);
 
1509
    cont_CreateBinding(IndexContext, FirstDomain, IndexContext, Term);
 
1510
 
 
1511
    cont_StartBinding();
 
1512
    st_StackPush(StIndex->subnodes);
 
1513
    cont_StartBinding();
 
1514
 
 
1515
    Result = st_TraverseForExistInstancePreTest(IndexContext);
 
1516
 
 
1517
#ifdef CHECK
 
1518
    cont_SaveState();
 
1519
#endif
 
1520
 
 
1521
    if (Result == NULL)
 
1522
      st_CancelExistRetrieval();
 
1523
 
 
1524
    return Result;
 
1525
  } else
 
1526
    return NULL;
 
1527
}
 
1528
 
 
1529
 
 
1530
POINTER st_NextCandidate(void)
 
1531
/**************************************************************
 
1532
  INPUT:   
 
1533
  RETURNS: 
 
1534
  EFFECTS: 
 
1535
***************************************************************/
 
1536
{
 
1537
  LIST Result;
 
1538
 
 
1539
#ifdef CHECK
 
1540
  if (st_StackEmpty(st_STACKSAVE)) {
 
1541
    misc_StartErrorReport();
 
1542
    misc_ErrorReport("\n In st_NextCandidate: ST-Stack empty.\n");
 
1543
    misc_FinishErrorReport();
 
1544
  } 
 
1545
  else 
 
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();
 
1550
    }
 
1551
 
 
1552
  cont_CheckState();
 
1553
#endif
 
1554
 
 
1555
  Result = st_StackPopResult();
 
1556
 
 
1557
  if (list_Exist(Result)) {
 
1558
    st_StackPush(list_Cdr(Result));
 
1559
#ifdef CHECK
 
1560
    cont_SaveState();
 
1561
#endif
 
1562
    return list_Car(Result);
 
1563
  } else {
 
1564
    POINTER NewResult;
 
1565
 
 
1566
    NewResult = NULL;
 
1567
 
 
1568
    if (st_WHICH_CONTEXTS == st_STANDARD)
 
1569
      switch (st_CURRENT_RETRIEVAL) {
 
1570
 
 
1571
      case st_UNIFIER:
 
1572
        NewResult = st_TraverseForExistUnifier(st_INDEX_CONTEXT);
 
1573
        break;
 
1574
 
 
1575
      case st_GEN:
 
1576
        NewResult = st_TraverseForExistGen(st_INDEX_CONTEXT);
 
1577
        break;
 
1578
 
 
1579
      case st_GENPRETEST:
 
1580
        NewResult = st_TraverseForExistGenPreTest(st_INDEX_CONTEXT);
 
1581
        break;
 
1582
 
 
1583
      case st_INSTANCE:
 
1584
        NewResult = st_TraverseForExistInstance(st_INDEX_CONTEXT);
 
1585
        break;
 
1586
 
 
1587
      case st_INSTANCEPRETEST:
 
1588
        NewResult = st_TraverseForExistInstancePreTest(st_INDEX_CONTEXT);
 
1589
 
 
1590
      default:
 
1591
        misc_StartErrorReport();
 
1592
        misc_ErrorReport("\n In st_NextCandidate: Unknown retrieval type.\n");
 
1593
        misc_FinishErrorReport();
 
1594
      }
 
1595
    else {
 
1596
      misc_StartErrorReport();
 
1597
      misc_ErrorReport("\n In st_NextCandidate: Unknown context type.\n");
 
1598
      misc_FinishErrorReport();
 
1599
    }
 
1600
 
 
1601
#ifdef CHECK
 
1602
    cont_SaveState();
 
1603
#endif
 
1604
 
 
1605
    if (NewResult == NULL)
 
1606
      st_CancelExistRetrieval();
 
1607
 
 
1608
    return NewResult;
 
1609
  }
 
1610
}
 
1611
 
 
1612
 
 
1613
/**************************************************************/
 
1614
/* ********************************************************** */
 
1615
/* *                                                        * */
 
1616
/* *  OUTPUT                                                * */
 
1617
/* *                                                        * */
 
1618
/* ********************************************************** */
 
1619
/**************************************************************/
 
1620
 
 
1621
 
 
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
***************************************************************/
 
1628
{
 
1629
  int i;
 
1630
  
 
1631
  if (St == (st_INDEX)NULL)
 
1632
    return;
 
1633
  
 
1634
  for (i = 0; i < Position; i++)
 
1635
    putchar(' ');
 
1636
  puts("|");
 
1637
  
 
1638
  for (i = 0; i < Position; i++)
 
1639
    putchar(' ');
 
1640
  fputs("+-", stdout);
 
1641
 
 
1642
  printf(" Max: %d, Min: %d, ", st_Max(St), st_Min(St));
 
1643
  subst_Print(St->subst);
 
1644
  putchar('\n');
 
1645
 
 
1646
  if (st_IsLeaf(St)) {
 
1647
 
 
1648
    LIST Scan;
 
1649
 
 
1650
    for (i = 0; i < Position; i++)
 
1651
      putchar(' ');
 
1652
    fputs("  =>", stdout);
 
1653
 
 
1654
    if (Print)
 
1655
      for (Scan = St->entries; Scan != NULL; Scan = list_Cdr(Scan)) {
 
1656
        putchar(' ');
 
1657
        Print(list_Car(Scan));
 
1658
      }
 
1659
    else
 
1660
      printf(" %d Entries", list_Length(St->entries));
 
1661
 
 
1662
    putchar('\n');
 
1663
    
 
1664
  } else {
 
1665
    LIST Scan;
 
1666
 
 
1667
    for (Scan = St->subnodes; Scan != NULL; Scan = list_Cdr(Scan))
 
1668
      st_PrintHelp(list_Car(Scan), Position + 2, Print);
 
1669
  }
 
1670
}
 
1671
 
 
1672
 
 
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
***************************************************************/
 
1678
{
 
1679
  LIST Scan;
 
1680
 
 
1681
  if (st_Empty(StIndex)) {
 
1682
    puts("\n\nIndex empty.");
 
1683
    return;
 
1684
  }
 
1685
 
 
1686
  fputs("\n\nroot: ", stdout);
 
1687
  printf(" Max: %d, Min: %d, ", st_Max(StIndex), st_Min(StIndex));
 
1688
  subst_Print(StIndex->subst);
 
1689
  putchar('\n');
 
1690
  if (st_IsLeaf(StIndex)) {
 
1691
    fputs("  =>", stdout);
 
1692
 
 
1693
    if (Print)
 
1694
      for (Scan = StIndex->entries; Scan != NULL; Scan = list_Cdr(Scan)) {
 
1695
        putchar(' ');
 
1696
        Print(list_Car(Scan));
 
1697
      }
 
1698
    else
 
1699
      printf(" %d Entries", list_Length(StIndex->entries));
 
1700
 
 
1701
  } else
 
1702
    for (Scan = StIndex->subnodes; Scan != NULL; Scan = list_Cdr(Scan))
 
1703
      st_PrintHelp(list_Car(Scan),2, Print);
 
1704
  puts("\n");
 
1705
}