← Back to branch summary

~ubuntu-branches/ubuntu/oneiric/spass/oneiric

« back to all changes in this revision

Viewing changes to SPASS/search.h

  • 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:
SPASS/search.h
 
1
/**************************************************************/
 
2
/* ********************************************************** */
 
3
/* *                                                        * */
 
4
/* *          REPRESENTATION OF PROOF SEARCH                * */
 
5
/* *                                                        * */
 
6
/* *  $Module:   PROOF SEARCH                               * */ 
 
7
/* *                                                        * */
 
8
/* *  Copyright (C) 1997, 1998, 1999, 2000                  * */
 
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.7 $                                         * */
 
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: search.h,v $ */
 
40
 
 
41
#ifndef _PROOFSEARCH_
 
42
#define _PROOFSEARCH_
 
43
 
 
44
#include "clause.h"
 
45
#include "sort.h"
 
46
 
 
47
/**************************************************************/
 
48
/* Data Structures and Constants                              */
 
49
/**************************************************************/
 
50
 
 
51
/* <isleft>:         true iff the split is a left branch         */
 
52
/* <blockedClauses>: list of (unshared) clauses containing the   */
 
53
/*                   "remainder" of the clause splitted at this  */
 
54
/*                   level and the negation of the first branch  */
 
55
/*                   if this branch created a ground clause.     */ 
 
56
/*                   The right clause has clause number 0, and   */
 
57
/*                   the negation clauses have number -1.        */
 
58
/* <deletedClauses>: list of (unshared) clauses made redundant   */
 
59
/*                   by a clause of this level. The split level  */
 
60
/*                   of these clauses may be above or below the  */
 
61
/*                   current level, but not equal to the current */
 
62
/*                   level.                                      */
 
63
/* <father>:         the unshared clause that was splitted.      */
 
64
/* <leftSplitfield>: the used splits of the left branch          */
 
65
/*                   corresponding to current split if it is a   */
 
66
/*                   right branch; not used for left splits      */
 
67
/* <rightSplitfield>: the used splits of the current split if it */
 
68
/*                   is a right branch; not used for left splits */
 
69
typedef struct {
 
70
  /* == 0 -> TOPLEVEL, 1,2,... */
 
71
  int     splitlevel;
 
72
  BOOL    isleft;
 
73
  BOOL    used;
 
74
  LIST    blockedClauses, deletedClauses;
 
75
  CLAUSE  father;
 
76
  SPLITFIELD leftSplitfield, rightSplitfield;
 
77
  unsigned leftSplitfield_length, rightSplitfield_length;
 
78
} *SPLIT, SPLIT_NODE;
 
79
 
 
80
 
 
81
typedef struct PROOFSEARCH_HELP {
 
82
  LIST            definitions;
 
83
  LIST            emptyclauses;
 
84
  LIST            usedemptyclauses;
 
85
  LIST            finmonpreds;
 
86
  SHARED_INDEX    woindex;
 
87
  LIST            wolist;
 
88
  SHARED_INDEX    usindex;
 
89
  LIST            uslist;
 
90
  SORTTHEORY      astatic;
 
91
  SORTTHEORY      adynamic;
 
92
  SORTTHEORY      dynamic;
 
93
  SHARED_INDEX    dpindex;
 
94
  LIST            dplist;
 
95
  PRECEDENCE      precedence;
 
96
  FLAGSTORE       store;
 
97
  LIST            stack;
 
98
  int             validlevel;
 
99
  int             lastbacktrack;
 
100
  int             splitcounter;
 
101
  int             keptclauses;
 
102
  int             derivedclauses;
 
103
  int             loops;
 
104
  int             backtracked;
 
105
  NAT             nontrivclausenumber;
 
106
} PROOFSEARCH_NODE,*PROOFSEARCH;
 
107
 
 
108
/* There are two sets of clauses with their respective clause list: worked-off clauses   */
 
109
/* contained in <woindex>, <wolist> and usable clauses, contained in <usindex>,<uslist>. */
 
110
/* The assoc list <finitepreds> is a list of pairs (<pred>.(<gterm1>,...,<gtermn>))      */
 
111
/* where <pred> (monadic) has (at most) the extension <gterm1>,...,<gtermn>              */
 
112
/* Three sort theories: <astatic> is the static overall approximation, only available    */
 
113
/* in a non-equality setting, <adynamic> is the dynamic approximation only considering   */
 
114
/* maximal declarations, and <dynamic> is the (not approximated) dynamic sort theory of  */
 
115
/* all maximal declarations. Clauses that are no longer needed for the search, but for   */
 
116
/* proof documentation are stored in <dpindex>, <dplist>. If <dpindex> is NULL, then     */
 
117
/* this means that no proof documentation is required.                                   */
 
118
/* A search is also heavily influenced by the used <precedence> and flag values in       */
 
119
/* store.                                                                                */
 
120
/* The next components deal with splitting: the split stack, the current level           */
 
121
/* of splitting, the last backtrack level (for branch condensing) and the overall number */
 
122
/* of splittings stored in <splitcounter>.                                               */
 
123
/* Finally some statistics is stored: the number of kept, derived clauses ...            */
 
124
/* and the clause number of some clause that implies a non-trivial domain .               */
 
125
 
 
126
/**************************************************************/
 
127
/* Inline Functions                                           */
 
128
/**************************************************************/
 
129
 
 
130
static __inline__ LIST prfs_EmptyClauses(PROOFSEARCH Prf)
 
131
{
 
132
  return Prf->emptyclauses;
 
133
}
 
134
 
 
135
static __inline__ void prfs_SetEmptyClauses(PROOFSEARCH Prf, LIST Clauses)
 
136
{
 
137
  Prf->emptyclauses = Clauses;
 
138
}
 
139
 
 
140
static __inline__ LIST prfs_Definitions(PROOFSEARCH Prf)
 
141
{
 
142
  return Prf->definitions;
 
143
}
 
144
 
 
145
static __inline__ void prfs_SetDefinitions(PROOFSEARCH Prf, LIST Definitions)
 
146
{
 
147
  Prf->definitions = Definitions;
 
148
}
 
149
 
 
150
static __inline__ LIST prfs_UsedEmptyClauses(PROOFSEARCH Prf)
 
151
{
 
152
  return Prf->usedemptyclauses;
 
153
}
 
154
 
 
155
static __inline__ void prfs_SetUsedEmptyClauses(PROOFSEARCH Prf, LIST Clauses)
 
156
{
 
157
  Prf->usedemptyclauses = Clauses;
 
158
}
 
159
 
 
160
 
 
161
static __inline__ LIST prfs_WorkedOffClauses(PROOFSEARCH Prf)
 
162
{
 
163
  return Prf->wolist;
 
164
}
 
165
 
 
166
static __inline__ void prfs_SetWorkedOffClauses(PROOFSEARCH Prf, LIST Clauses)
 
167
{
 
168
  Prf->wolist = Clauses;
 
169
}
 
170
 
 
171
static __inline__ SHARED_INDEX prfs_WorkedOffSharingIndex(PROOFSEARCH Prf)
 
172
{
 
173
  return Prf->woindex;
 
174
}
 
175
 
 
176
static __inline__ LIST prfs_UsableClauses(PROOFSEARCH Prf)
 
177
{
 
178
  return Prf->uslist;
 
179
}
 
180
 
 
181
static __inline__ void prfs_SetUsableClauses(PROOFSEARCH Prf, LIST Clauses)
 
182
{
 
183
  Prf->uslist = Clauses;
 
184
}
 
185
 
 
186
static __inline__ SHARED_INDEX prfs_UsableSharingIndex(PROOFSEARCH Prf)
 
187
{
 
188
  return Prf->usindex;
 
189
}
 
190
 
 
191
static __inline__ LIST prfs_DocProofClauses(PROOFSEARCH Prf)
 
192
{
 
193
  return Prf->dplist;
 
194
}
 
195
 
 
196
static __inline__ void prfs_SetDocProofClauses(PROOFSEARCH Prf, LIST Clauses)
 
197
{
 
198
  Prf->dplist = Clauses;
 
199
}
 
200
 
 
201
static __inline__ SHARED_INDEX prfs_DocProofSharingIndex(PROOFSEARCH Prf)
 
202
{
 
203
  return Prf->dpindex;
 
204
}
 
205
 
 
206
static __inline__ void prfs_AddDocProofSharingIndex(PROOFSEARCH Prf)
 
207
{
 
208
  Prf->dpindex  = sharing_IndexCreate();
 
209
}
 
210
 
 
211
static __inline__ LIST prfs_GetFinMonPreds(PROOFSEARCH Prf)
 
212
{
 
213
  return Prf->finmonpreds;
 
214
}
 
215
 
 
216
static __inline__ void prfs_SetFinMonPreds(PROOFSEARCH Prf, LIST Preds)
 
217
{
 
218
  Prf->finmonpreds = Preds;
 
219
}
 
220
 
 
221
static __inline__ void prfs_DeleteFinMonPreds(PROOFSEARCH Prf)
 
222
{
 
223
  list_DeleteAssocListWithValues(Prf->finmonpreds,
 
224
                                 (void (*)(POINTER)) term_DeleteTermList);
 
225
  prfs_SetFinMonPreds(Prf, list_Nil());
 
226
}
 
227
 
 
228
static __inline__ SORTTHEORY prfs_StaticSortTheory(PROOFSEARCH Prf)
 
229
{
 
230
  return Prf->astatic;
 
231
}
 
232
 
 
233
static __inline__ void prfs_SetStaticSortTheory(PROOFSEARCH Prf, SORTTHEORY Theory)
 
234
{
 
235
  Prf->astatic = Theory;
 
236
}
 
237
 
 
238
static __inline__ SORTTHEORY prfs_DynamicSortTheory(PROOFSEARCH Prf)
 
239
{
 
240
  return Prf->dynamic;
 
241
}
 
242
 
 
243
static __inline__ void prfs_SetDynamicSortTheory(PROOFSEARCH Prf, SORTTHEORY Theory)
 
244
{
 
245
  Prf->dynamic = Theory;
 
246
}
 
247
 
 
248
static __inline__ SORTTHEORY prfs_ApproximatedDynamicSortTheory(PROOFSEARCH Prf)
 
249
{
 
250
  return Prf->adynamic;
 
251
}
 
252
 
 
253
static __inline__ void prfs_SetApproximatedDynamicSortTheory(PROOFSEARCH Prf, SORTTHEORY Theory)
 
254
{
 
255
  Prf->adynamic = Theory;
 
256
}
 
257
 
 
258
static __inline__ PRECEDENCE prfs_Precedence(PROOFSEARCH Prf)
 
259
{
 
260
  return Prf->precedence;
 
261
}
 
262
 
 
263
static __inline__ FLAGSTORE prfs_Store(PROOFSEARCH Prf)
 
264
{
 
265
  return Prf->store;
 
266
}
 
267
 
 
268
static __inline__ BOOL prfs_SplitLevelCondition(NAT OriginLevel, NAT RedundantLevel, NAT BacktrackLevel)
 
269
{
 
270
  /*return (OriginLevel != RedundantLevel && OriginLevel != 0);*/
 
271
  /*return OriginLevel != 0;*/
 
272
  return (OriginLevel > RedundantLevel);
 
273
}
 
274
 
 
275
static __inline__ BOOL prfs_IsClauseValid(CLAUSE C, int Level)
 
276
{
 
277
  return clause_SplitLevel(C) <= Level;
 
278
}
 
279
 
 
280
static __inline__ SPLIT prfs_GetSplitOfLevel(int L, PROOFSEARCH Prf)
 
281
{
 
282
  LIST Scan;
 
283
  Scan = Prf->stack; 
 
284
  while (!list_Empty(Scan) &&
 
285
         (((SPLIT)list_Car(Scan))->splitlevel != L))
 
286
    Scan = list_Cdr(Scan);
 
287
 
 
288
  if (list_Empty(Scan)) {
 
289
    return (SPLIT) NULL;
 
290
  } else {
 
291
    return (SPLIT) list_Car(Scan);
 
292
  }
 
293
}
 
294
 
 
295
static __inline__ LIST prfs_SplitStack(PROOFSEARCH Prf)
 
296
{
 
297
  return Prf->stack;
 
298
}
 
299
 
 
300
static __inline__ SPLIT prfs_SplitStackTop(PROOFSEARCH Prf)
 
301
{
 
302
  return (SPLIT) list_Car(Prf->stack);
 
303
}
 
304
 
 
305
static __inline__ void prfs_SplitStackPop(PROOFSEARCH Prf)
 
306
{
 
307
  Prf->stack = list_Pop(Prf->stack);
 
308
}
 
309
 
 
310
static __inline__ void prfs_SplitStackPush(PROOFSEARCH Prf, SPLIT S)
 
311
{
 
312
  Prf->stack = list_Cons(S, Prf->stack);
 
313
}
 
314
 
 
315
static __inline__ BOOL prfs_SplitStackEmpty(PROOFSEARCH Prf)
 
316
{
 
317
  return list_StackEmpty(prfs_SplitStack(Prf));
 
318
}
 
319
 
 
320
static __inline__ int prfs_TopLevel(void) 
 
321
{
 
322
  return 0;
 
323
}
 
324
 
 
325
static __inline__ int prfs_ValidLevel(PROOFSEARCH Prf)
 
326
{
 
327
  return Prf->validlevel;
 
328
}
 
329
 
 
330
static __inline__ void prfs_SetValidLevel(PROOFSEARCH Prf, int Value)
 
331
{
 
332
  Prf->validlevel = Value;
 
333
}
 
334
 
 
335
static __inline__ void prfs_IncValidLevel(PROOFSEARCH Prf)
 
336
{
 
337
  (Prf->validlevel)++;
 
338
}
 
339
 
 
340
static __inline__ void prfs_DecValidLevel(PROOFSEARCH Prf)
 
341
{
 
342
  (Prf->validlevel)--;
 
343
}
 
344
 
 
345
static __inline__ int prfs_LastBacktrackLevel(PROOFSEARCH Prf)
 
346
{
 
347
  return Prf->lastbacktrack;
 
348
}
 
349
 
 
350
static __inline__ void prfs_SetLastBacktrackLevel(PROOFSEARCH Prf, int Value)
 
351
{
 
352
  Prf->lastbacktrack = Value;
 
353
}
 
354
 
 
355
static __inline__ int prfs_SplitCounter(PROOFSEARCH Prf)
 
356
{
 
357
  return Prf->splitcounter;
 
358
}
 
359
 
 
360
static __inline__ void prfs_SetSplitCounter(PROOFSEARCH Prf, int c)
 
361
{
 
362
  Prf->splitcounter = c;
 
363
}
 
364
 
 
365
static __inline__ void prfs_IncSplitCounter(PROOFSEARCH Prf)
 
366
{
 
367
  (Prf->splitcounter)++;
 
368
}
 
369
 
 
370
static __inline__ int prfs_KeptClauses(PROOFSEARCH Prf)
 
371
{
 
372
  return Prf->keptclauses;
 
373
}
 
374
 
 
375
static __inline__ void prfs_IncKeptClauses(PROOFSEARCH Prf)
 
376
{
 
377
  Prf->keptclauses++;
 
378
}
 
379
 
 
380
static __inline__ int prfs_DerivedClauses(PROOFSEARCH Prf)
 
381
{
 
382
  return Prf->derivedclauses;
 
383
}
 
384
 
 
385
static __inline__ void prfs_IncDerivedClauses(PROOFSEARCH Prf, int k)
 
386
{
 
387
  Prf->derivedclauses += k;
 
388
}
 
389
 
 
390
static __inline__ int prfs_Loops(PROOFSEARCH Prf)
 
391
{
 
392
  return Prf->loops;
 
393
}
 
394
 
 
395
static __inline__ void prfs_SetLoops(PROOFSEARCH Prf, int k)
 
396
{
 
397
  Prf->loops = k;
 
398
}
 
399
 
 
400
static __inline__ void prfs_DecLoops(PROOFSEARCH Prf)
 
401
{
 
402
  Prf->loops--;
 
403
}
 
404
 
 
405
static __inline__ int prfs_BacktrackedClauses(PROOFSEARCH Prf)
 
406
{
 
407
  return Prf->backtracked;
 
408
}
 
409
 
 
410
static __inline__ void prfs_SetBacktrackedClauses(PROOFSEARCH Prf, int k)
 
411
{
 
412
  Prf->backtracked = k;
 
413
}
 
414
 
 
415
static __inline__ void prfs_IncBacktrackedClauses(PROOFSEARCH Prf, int k)
 
416
{
 
417
  Prf->backtracked += k;
 
418
}
 
419
 
 
420
static __inline__ NAT prfs_NonTrivClauseNumber(PROOFSEARCH Prf)
 
421
{
 
422
  return Prf->nontrivclausenumber;
 
423
}
 
424
 
 
425
static __inline__ void prfs_SetNonTrivClauseNumber(PROOFSEARCH Prf, NAT Number)
 
426
{
 
427
  Prf->nontrivclausenumber = Number;
 
428
}
 
429
 
 
430
 
 
431
/**************************************************************/
 
432
/* Functions for accessing SPLIT objects                      */
 
433
/**************************************************************/
 
434
 
 
435
static __inline__ void prfs_SplitFree(SPLIT Sp)
 
436
{
 
437
  memory_Free(Sp, sizeof(SPLIT_NODE));
 
438
}
 
439
 
 
440
static __inline__ void prfs_SplitDelete(SPLIT S)
 
441
/**************************************************************
 
442
  INPUT:   A split 
 
443
  RETURNS: Nothing.
 
444
  MEMORY:  Deletes blocked and deleted clauses. Frees the split.
 
445
***************************************************************/
 
446
{
 
447
  clause_DeleteClauseList(S->blockedClauses);
 
448
  clause_DeleteClauseList(S->deletedClauses);
 
449
  if (S->father != (CLAUSE)NULL)
 
450
    clause_Delete(S->father);
 
451
  if (S->leftSplitfield != NULL) {
 
452
    memory_Free(S->leftSplitfield,
 
453
                sizeof(SPLITFIELDENTRY) * S->leftSplitfield_length);
 
454
    S->leftSplitfield = NULL;
 
455
  }
 
456
  if (S->rightSplitfield != NULL) {
 
457
    memory_Free(S->rightSplitfield,
 
458
                sizeof(SPLITFIELDENTRY) * S->rightSplitfield_length);
 
459
    S->rightSplitfield = NULL;
 
460
  }
 
461
  prfs_SplitFree(S);
 
462
}
 
463
 
 
464
 
 
465
static __inline__ LIST prfs_SplitBlockedClauses(SPLIT S)
 
466
{
 
467
  return S->blockedClauses;
 
468
}
 
469
 
 
470
static __inline__ void prfs_SplitAddBlockedClause(SPLIT S, CLAUSE C)
 
471
{
 
472
  S->blockedClauses = list_Cons(C,S->blockedClauses);
 
473
}
 
474
 
 
475
static __inline__ void prfs_SplitSetBlockedClauses(SPLIT S, LIST L)
 
476
{
 
477
  S->blockedClauses = L;
 
478
}
 
479
 
 
480
static __inline__ LIST prfs_SplitDeletedClauses(SPLIT S)
 
481
{
 
482
  return S->deletedClauses;
 
483
}
 
484
 
 
485
static __inline__ void prfs_SplitSetDeletedClauses(SPLIT S, LIST L)
 
486
{
 
487
  S->deletedClauses = L;
 
488
}
 
489
 
 
490
static __inline__ int prfs_SplitSplitLevel(SPLIT S)
 
491
{
 
492
  return S->splitlevel;
 
493
}
 
494
 
 
495
static __inline__ BOOL prfs_SplitIsLeft(SPLIT S)
 
496
{
 
497
  return S->isleft;
 
498
}
 
499
 
 
500
static __inline__ void prfs_SplitSetLeft(SPLIT S)
 
501
{
 
502
  S->isleft = TRUE;
 
503
}
 
504
 
 
505
static __inline__ void prfs_SplitSetRight(SPLIT S)
 
506
{
 
507
  S->isleft = FALSE;
 
508
}
 
509
 
 
510
static __inline__ BOOL prfs_SplitIsUsed(SPLIT S)
 
511
{
 
512
  return S->used;
 
513
}
 
514
 
 
515
static __inline__ BOOL prfs_SplitIsUnused(SPLIT S)
 
516
{
 
517
  return !S->used;
 
518
}
 
519
 
 
520
static __inline__ void prfs_SplitSetUsed(SPLIT S)
 
521
{
 
522
  S->used = TRUE;
 
523
}
 
524
 
 
525
static __inline__ CLAUSE prfs_SplitFatherClause(SPLIT S) 
 
526
{
 
527
  return S->father;
 
528
}
 
529
 
 
530
static __inline__ void prfs_SplitSetFatherClause(SPLIT S, CLAUSE C)
 
531
{
 
532
  S->father = C;
 
533
}
 
534
 
 
535
static __inline__ SPLITFIELD prfs_LeftSplitfield(SPLIT S, unsigned *Length)
 
536
{
 
537
  *Length = S->leftSplitfield_length;
 
538
  return S->leftSplitfield;
 
539
}
 
540
 
 
541
static __inline__ SPLITFIELD prfs_RightSplitfield(SPLIT S, unsigned *Length)
 
542
{
 
543
  *Length = S->rightSplitfield_length;
 
544
  return S->rightSplitfield;
 
545
}
 
546
 
 
547
static __inline void prfs_SplitFreeSplitfields(SPLIT S)
 
548
{
 
549
  if (S->leftSplitfield != NULL) {
 
550
    memory_Free(S->leftSplitfield,
 
551
                sizeof(SPLITFIELDENTRY) * S->leftSplitfield_length);
 
552
    S->leftSplitfield = NULL;
 
553
  }
 
554
  if (S->rightSplitfield != NULL) {
 
555
    memory_Free(S->rightSplitfield,
 
556
                sizeof(SPLITFIELDENTRY) * S->rightSplitfield_length);
 
557
    S->rightSplitfield = NULL;
 
558
  }
 
559
}
 
560
 
 
561
 
 
562
static __inline__ BOOL prfs_ExistsSplitOfLevel(int L, PROOFSEARCH PS)
 
563
{
 
564
  LIST Scan;
 
565
  Scan = PS->stack;
 
566
 
 
567
  while (!list_Empty(Scan) &&
 
568
   (((SPLIT)list_Car(Scan))->splitlevel != L  || ((SPLIT)list_Car(Scan))->used))
 
569
    Scan = list_Cdr(Scan);
 
570
 
 
571
  if (list_Empty(Scan)) {
 
572
    return FALSE;
 
573
  } else {
 
574
    return TRUE;
 
575
  }
 
576
}
 
577
 
 
578
static __inline__ BOOL prfs_SplitsAvailable(PROOFSEARCH PS, FLAGSTORE Store)
 
579
{
 
580
  return (flag_GetFlagIntValue(Store, flag_SPLITS) < 0 ||
 
581
          prfs_SplitCounter(PS) < flag_GetFlagIntValue(Store, flag_SPLITS));
 
582
}
 
583
 
 
584
 
 
585
/**************************************************************/
 
586
/* Functions                                                  */
 
587
/**************************************************************/
 
588
 
 
589
PROOFSEARCH prfs_Create(void);
 
590
BOOL        prfs_Check(PROOFSEARCH);
 
591
void        prfs_CopyIndices(PROOFSEARCH, PROOFSEARCH);
 
592
void        prfs_Delete(PROOFSEARCH);
 
593
void        prfs_DeleteDocProof(PROOFSEARCH);
 
594
void        prfs_Clean(PROOFSEARCH);
 
595
void        prfs_Print(PROOFSEARCH);
 
596
void        prfs_PrintSplit(SPLIT);
 
597
void        prfs_PrintSplitStack(PROOFSEARCH);
 
598
void        prfs_InsertWorkedOffClause(PROOFSEARCH,CLAUSE);
 
599
void        prfs_InsertUsableClause(PROOFSEARCH,CLAUSE);
 
600
void        prfs_InsertDocProofClause(PROOFSEARCH,CLAUSE);
 
601
void        prfs_MoveUsableWorkedOff(PROOFSEARCH, CLAUSE);
 
602
void        prfs_MoveWorkedOffDocProof(PROOFSEARCH, CLAUSE);
 
603
void        prfs_MoveUsableDocProof(PROOFSEARCH, CLAUSE);
 
604
void        prfs_ExtractWorkedOff(PROOFSEARCH, CLAUSE);
 
605
void        prfs_DeleteWorkedOff(PROOFSEARCH, CLAUSE);
 
606
void        prfs_ExtractUsable(PROOFSEARCH, CLAUSE);
 
607
void        prfs_DeleteUsable(PROOFSEARCH, CLAUSE);
 
608
void        prfs_ExtractDocProof(PROOFSEARCH, CLAUSE);
 
609
void        prfs_DeleteDocProofClause(PROOFSEARCH, CLAUSE);
 
610
void        prfs_MoveInvalidClausesDocProof(PROOFSEARCH);
 
611
void        prfs_SwapIndexes(PROOFSEARCH);
 
612
 
 
613
void        prfs_InstallFiniteMonadicPredicates(PROOFSEARCH, LIST, LIST);
 
614
 
 
615
CLAUSE      prfs_PerformSplitting(PROOFSEARCH, CLAUSE);
 
616
CLAUSE      prfs_DoSplitting(PROOFSEARCH, CLAUSE, LIST);
 
617
NAT         prfs_GetNumberOfInstances(PROOFSEARCH, LITERAL, BOOL);
 
618
 
 
619
void        prfs_SetLeftSplitfield(SPLIT, SPLITFIELD, unsigned);
 
620
void        prfs_SetRightSplitfield(SPLIT, SPLITFIELD, unsigned);
 
621
BOOL        prfs_SplitfieldContainsLevel(SPLITFIELD, unsigned, NAT);
 
622
NAT         prfs_SplitfieldHighestLevel(SPLITFIELD, unsigned);
 
623
void        prfs_AddLevelToSplitfield(SPLITFIELD*, unsigned*, NAT);
 
624
void        prfs_RemoveLevelFromSplitfield(SPLITFIELD*, unsigned*, NAT);
 
625
BOOL        prfs_SplitfieldIsSubset(SPLITFIELD, unsigned, SPLITFIELD, unsigned);
 
626
SPLITFIELD  prfs_SplitfieldUnion(SPLITFIELD, unsigned, SPLITFIELD, unsigned, unsigned*);
 
627
SPLITFIELD  prfs_SplitfieldIntersection(SPLITFIELD, unsigned, SPLITFIELD, unsigned, unsigned*);
 
628
SPLITFIELD  prfs_CombineSplitfields(SPLITFIELD, unsigned, SPLITFIELD, unsigned, NAT, unsigned*);
 
629
 
 
630
#endif
 
631