« back to all changes in this revision
Viewing changes to SPASS/subsumption.c
- browse files at revision 4
- compare with another revision
- compare with revision 1
- download diff
- download tarball
- view history from revision 4
- 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
- files added:
- .pc
- .pc/debian-changes-3.7-1
- .pc/debian-changes-3.7-1/doc
- .pc/debian-changes-3.7-1/doc/man
- .pc/debian-changes-3.7-1/doc/texinfo
- SPASS
- debian/patches
- debian/source
- doc
- doc/handbook
- doc/html
- doc/man
- doc/syntax
- doc/texinfo
- doc/tutorial
- examples
- lib
- m4
- scripts
- files removed:
- debian/SPASS.1
- files modified:
- debian/changelog
added
removed
SPASS/subsumption.c
1
/**************************************************************/
2
/* ********************************************************** */
3
/* * * */
4
/* * SUBSUMPTION * */
5
/* * * */
6
/* * $Module: SUBSUMPTION * */
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: subsumption.c,v $ */
40
41
42
#include "subsumption.h"
43
44
static NAT *multvec_i;
45
static NAT *multvec_j;
46
static NAT stamp;
47
static NAT maxlits;
48
49
static BOOL subs_InternIdc(CLAUSE, int, CLAUSE);
50
static BOOL subs_InternIdcEq(CLAUSE, int, CLAUSE);
51
static BOOL subs_InternIdcEqExcept(CLAUSE, int, CLAUSE, int);
52
static BOOL subs_InternIdcRes(CLAUSE, int, int, int);
53
54
/* The following functions are currently unused */
55
BOOL subs_IdcTestlits(CLAUSE, CLAUSE, LITPTR*);
56
BOOL subs_Testlits(CLAUSE, CLAUSE);
57
58
59
void subs_Init(void)
60
{
61
int i;
62
63
stamp = 0;
64
maxlits = 100;
65
multvec_i = memory_Malloc(sizeof(NAT)*maxlits);
66
multvec_j = memory_Malloc(sizeof(NAT)*maxlits);
67
for (i = 0; i < maxlits; i++)
68
multvec_i[i] = multvec_j[i] = 0;
69
}
70
71
void subs_Free(void)
72
{
73
memory_Free(multvec_i, sizeof(NAT)*maxlits);
74
memory_Free(multvec_j, sizeof(NAT)*maxlits);
75
}
76
77
void subs_ExtendLitVector()
78
{
79
int i;
80
81
memory_Free(multvec_i, sizeof(NAT)*maxlits);
82
memory_Free(multvec_j, sizeof(NAT)*maxlits);
83
maxlits = maxlits * 10;
84
stamp = 0;
85
multvec_i = memory_Malloc(sizeof(NAT)*maxlits);
86
multvec_j = memory_Malloc(sizeof(NAT)*maxlits);
87
for (i = 0; i < maxlits; i++)
88
multvec_i[i] = multvec_j[i] = 0;
89
}
90
91
92
static BOOL subs_TestlitsEq(CLAUSE c1, CLAUSE c2)
93
/**********************************************************
94
INPUT: Two clauses c1 and c2.
95
RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise.
96
CAUTION: None.
97
***********************************************************/
98
{
99
TERM t1,t2;
100
int i,j,n,k;
101
BOOL found;
102
103
n = clause_Length(c1);
104
k = clause_Length(c2);
105
106
for (i = 0; i < n; i++){
107
j = 0;
108
found = FALSE;
109
t1 = clause_GetLiteralTerm(c1,i);
110
111
do {
112
t2 = clause_GetLiteralTerm(c2,j);
113
cont_StartBinding();
114
if (unify_Match(cont_LeftContext(), t1, t2))
115
found = TRUE;
116
else{
117
if (symbol_Equal(term_TopSymbol(t1),term_TopSymbol(t2)) &&
118
fol_IsEquality(fol_Atom(t1)) &&
119
fol_IsEquality(fol_Atom(t2)) &&
120
(clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c1,i)) ||
121
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,j)))) {
122
cont_BackTrackAndStart();
123
if (unify_Match(cont_LeftContext(),
124
term_FirstArgument(fol_Atom(t1)),
125
term_SecondArgument(fol_Atom(t2))) &&
126
unify_Match(cont_LeftContext(),
127
term_SecondArgument(fol_Atom(t1)),
128
term_FirstArgument(fol_Atom(t2))))
129
found = TRUE;
130
else
131
j++;
132
}
133
else
134
j++;
135
}
136
cont_BackTrack();
137
138
} while (!found && j < k);
139
140
if (!found)
141
return FALSE;
142
}
143
144
return TRUE;
145
}
146
147
148
static BOOL subs_STMultiIntern(int i, CLAUSE c1, CLAUSE c2)
149
/**********************************************************
150
INPUT: Integers i,j and two clauses c1 and c2
151
i and j stand for the i-th and the j-th literal
152
in the clause c1 respectively c2.
153
RETURNS: FALSE if c1 does not multisubsume c2 and TRUE otherwise.
154
CAUTION: None.
155
***********************************************************/
156
{
157
int n,j;
158
TERM lit1,lit2;
159
160
j = 0;
161
n = clause_Length(c2);
162
lit1 = clause_GetLiteralTerm(c1,i);
163
164
while (j < n) {
165
if (multvec_j[j] != stamp) {
166
lit2 = clause_GetLiteralTerm(c2,j);
167
cont_StartBinding();
168
if (unify_Match(cont_LeftContext(),lit1,lit2)) {
169
if (i == (clause_Length(c1)-1)) {
170
cont_BackTrack();
171
return TRUE;
172
}
173
multvec_j[j] = stamp;
174
if (subs_STMultiIntern(i+1, c1, c2)) {
175
cont_BackTrack();
176
return TRUE;
177
}
178
multvec_j[j] = 0;
179
}
180
cont_BackTrack();
181
if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
182
fol_IsEquality(fol_Atom(lit1)) &&
183
fol_IsEquality(fol_Atom(lit2)) &&
184
(clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c1,i)) ||
185
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,j)))) {
186
cont_StartBinding();
187
if (unify_Match(cont_LeftContext(),
188
term_FirstArgument(fol_Atom(lit1)),
189
term_SecondArgument(fol_Atom(lit2))) &&
190
unify_Match(cont_LeftContext(),
191
term_SecondArgument(fol_Atom(lit1)),
192
term_FirstArgument(fol_Atom(lit2)))) {
193
if (i == (clause_Length(c1)-1)) {
194
cont_BackTrack();
195
return TRUE;
196
}
197
multvec_j[j] = stamp;
198
if (subs_STMultiIntern(i+1, c1, c2)) {
199
cont_BackTrack();
200
return TRUE;
201
}
202
multvec_j[j] = 0;
203
}
204
cont_BackTrack();
205
}
206
}
207
j++;
208
}
209
return FALSE;
210
}
211
212
213
BOOL subs_STMulti(CLAUSE c1, CLAUSE c2)
214
{
215
BOOL Result;
216
int n;
217
218
n = clause_Length(c1);
219
220
/*printf("\n St-Multi: %d -> %d",clause_Number(c1),clause_Number(c2));*/
221
222
if (n > clause_Length(c2) ||
223
(n > 1 && !subs_TestlitsEq(c1,c2))) {
224
/*fputs(" Testlits failure ", stdout);*/
225
return(FALSE);
226
}
227
228
229
if (clause_Length(c1) > maxlits || clause_Length(c2) > maxlits) {
230
subs_ExtendLitVector();
231
stamp++;
232
}
233
else
234
if (++stamp == NAT_MAX) {
235
int i;
236
stamp = 1;
237
for (i = 0; i < maxlits; i++)
238
multvec_i[i] = multvec_j[i] = 0;
239
}
240
/*unify_SaveState();*/
241
Result = subs_STMultiIntern(0,c1,c2);
242
/*unify_CheckState();*/
243
return Result;
244
}
245
246
247
static BOOL subs_TestlitsEqExcept(CLAUSE C1, CLAUSE C2)
248
{
249
TERM t1,t2;
250
int i,j,n,k;
251
BOOL found;
252
253
n = clause_Length(C1);
254
k = clause_Length(C2);
255
256
i = 0;
257
while (multvec_i[i] == stamp && i < n)
258
i++;
259
260
while (i < n) {
261
j = 0;
262
found = FALSE;
263
t1 = clause_GetLiteralTerm(C1,i);
264
265
do {
266
if (multvec_j[j] == stamp)
267
j++;
268
else {
269
t2 = clause_GetLiteralTerm(C2,j);
270
cont_StartBinding();
271
if (unify_MatchBindings(cont_LeftContext(), t1, t2))
272
found = TRUE;
273
else {
274
if (symbol_Equal(term_TopSymbol(t1),term_TopSymbol(t2)) &&
275
fol_IsEquality(fol_Atom(t1)) &&
276
fol_IsEquality(fol_Atom(t2)) &&
277
(clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,i)) ||
278
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) {
279
cont_BackTrackAndStart();
280
if (unify_MatchBindings(cont_LeftContext(),
281
term_FirstArgument(fol_Atom(t1)),
282
term_SecondArgument(fol_Atom(t2))) &&
283
unify_MatchBindings(cont_LeftContext(),
284
term_SecondArgument(fol_Atom(t1)),
285
term_FirstArgument(fol_Atom(t2))))
286
found = TRUE;
287
else
288
j++;
289
}
290
else
291
j++;
292
}
293
cont_BackTrack();
294
} /* else */
295
} while (!found && (j < k));
296
297
if (!found)
298
return FALSE;
299
do
300
i++;
301
while (multvec_i[i] == stamp && i < n);
302
} /* while i < n */
303
304
305
return TRUE;
306
}
307
308
309
static BOOL subs_STMultiExceptIntern(CLAUSE C1, CLAUSE C2)
310
{
311
int n, i, j, k;
312
NAT occs, occsaux;
313
TERM lit1,lit2;
314
315
i = -1;
316
k = 0;
317
occs = 0;
318
j = 0;
319
n = clause_Length(C2);
320
321
while (k < clause_Length(C1)) {
322
/* Select Literal with maximal number of variable occurrences. */
323
if (multvec_i[k] != stamp) {
324
if (i < 0) {
325
i = k;
326
occs = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,i));
327
} else
328
if ((occsaux = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,k)))
329
> occs) {
330
i = k;
331
occs = occsaux;
332
}
333
}
334
k++;
335
}
336
337
if (i < 0)
338
return TRUE;
339
340
lit1 = clause_GetLiteralTerm(C1, i);
341
multvec_i[i] = stamp;
342
343
while (j < n) {
344
if (multvec_j[j] != stamp) {
345
lit2 = clause_GetLiteralTerm(C2, j);
346
cont_StartBinding();
347
if (unify_MatchBindings(cont_LeftContext(), lit1, lit2)) {
348
multvec_j[j] = stamp;
349
if (subs_STMultiExceptIntern(C1, C2)) {
350
cont_BackTrack();
351
return TRUE;
352
}
353
multvec_j[j] = 0;
354
}
355
cont_BackTrack();
356
if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
357
fol_IsEquality(fol_Atom(lit1)) &&
358
fol_IsEquality(fol_Atom(lit2)) &&
359
(clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,i)) ||
360
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) {
361
cont_StartBinding();
362
if (unify_MatchBindings(cont_LeftContext(),
363
term_FirstArgument(fol_Atom(lit1)),
364
term_SecondArgument(fol_Atom(lit2))) &&
365
unify_MatchBindings(cont_LeftContext(),
366
term_SecondArgument(fol_Atom(lit1)),
367
term_FirstArgument(fol_Atom(lit2)))) {
368
multvec_j[j] = stamp;
369
if (subs_STMultiExceptIntern(C1, C2)) {
370
cont_BackTrack();
371
return TRUE;
372
}
373
multvec_j[j] = 0;
374
}
375
cont_BackTrack();
376
}
377
}
378
j++;
379
}
380
multvec_i[i] = 0;
381
return FALSE;
382
}
383
384
385
BOOL subs_STMultiExcept(CLAUSE C1, CLAUSE C2, int ExceptI, int ExceptJ)
386
/**********************************************************
387
INPUT: Two clauses and for each clause a literal that is
388
already bound to each other. If the literal value is negative,
389
a general subsumption test is performed.
390
RETURNS: TRUE if the first clause subsumes the second one.
391
CAUTION: The weight of the clauses must be up to date!
392
***********************************************************/
393
{
394
BOOL Result;
395
int n;
396
397
n = clause_Length(C1);
398
399
if (n > clause_Length(C2) ||
400
(clause_Weight(C1)-clause_LiteralWeight(clause_GetLiteral(C1,ExceptI))) >
401
(clause_Weight(C2)-clause_LiteralWeight(clause_GetLiteral(C2,ExceptJ))))
402
return FALSE;
403
404
if (clause_Length(C1) > maxlits || clause_Length(C2) > maxlits) {
405
subs_ExtendLitVector();
406
stamp++;
407
}
408
else
409
if (++stamp == NAT_MAX) {
410
int i;
411
stamp = 1;
412
for (i = 0; i < maxlits; i++)
413
multvec_i[i] = multvec_j[i] = 0;
414
}
415
multvec_i[ExceptI] = stamp;
416
multvec_j[ExceptJ] = stamp;
417
418
if (n > 1 && !subs_TestlitsEqExcept(C1, C2))
419
return FALSE;
420
421
/*unify_SaveState();*/
422
Result = subs_STMultiExceptIntern(C1, C2);
423
/*unify_CheckState();*/
424
return Result;
425
}
426
427
428
static BOOL subs_PartnerTest(CLAUSE C1, int c1l, int c1r, CLAUSE C2, int c2l, int c2r)
429
/**********************************************************
430
INPUT: Two clauses and for each clause a starting left index
431
and an exclusive right index.
432
RETURNS: TRUE if every literal inside the bounds of the first clause
433
can be matched against a literal inside the bounds of the
434
second clause.
435
CAUTION: None.
436
***********************************************************/
437
{
438
TERM t1,t2;
439
int j;
440
BOOL found;
441
442
if (c1l == c1r)
443
return TRUE;
444
445
while (multvec_i[c1l] == stamp && c1l < c1r)
446
c1l++;
447
448
if (c1l < c1r) {
449
if (c2l == c2r)
450
return FALSE;
451
else
452
do {
453
j = c2l;
454
found = FALSE;
455
t1 = clause_GetLiteralTerm(C1,c1l);
456
457
do {
458
if (multvec_j[j] == stamp)
459
j++;
460
else {
461
t2 = clause_GetLiteralTerm(C2,j);
462
cont_StartBinding();
463
if (unify_MatchBindings(cont_LeftContext(), t1, t2))
464
found = TRUE;
465
else {
466
if (symbol_Equal(term_TopSymbol(t1),term_TopSymbol(t2)) &&
467
fol_IsEquality(fol_Atom(t1)) &&
468
fol_IsEquality(fol_Atom(t2)) &&
469
(clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,c1l)) ||
470
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) {
471
cont_BackTrackAndStart();
472
if (unify_MatchBindings(cont_LeftContext(),
473
term_FirstArgument(fol_Atom(t1)),
474
term_SecondArgument(fol_Atom(t2))) &&
475
unify_MatchBindings(cont_LeftContext(),
476
term_SecondArgument(fol_Atom(t1)),
477
term_FirstArgument(fol_Atom(t2))))
478
found = TRUE;
479
else
480
j++;
481
}
482
else
483
j++;
484
}
485
cont_BackTrack();
486
} /* else */
487
} while (!found && (j < c2r));
488
489
if (!found)
490
return FALSE;
491
do
492
c1l++;
493
while (multvec_i[c1l] == stamp && c1l < c1r);
494
} while (c1l < c1r);
495
}
496
return TRUE;
497
}
498
499
500
static BOOL subs_SubsumesInternBasic(CLAUSE C1, int c1fa, int c1fs, int c1l,
501
CLAUSE C2, int c2fa, int c2fs, int c2l)
502
{
503
int i, j, n, k;
504
NAT occs, occsaux;
505
TERM lit1,lit2;
506
507
i = -1;
508
k = clause_FirstLitIndex();
509
occs = 0;
510
511
while (k < c1l) { /* Select literal with maximal variable occurrences. */
512
if (multvec_i[k] != stamp) {
513
if (i < 0) {
514
i = k;
515
occs = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,i));
516
} else
517
if ((occsaux = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,k)))
518
> occs) {
519
i = k;
520
occs = occsaux;
521
}
522
}
523
k++;
524
}
525
526
if (i < 0)
527
return TRUE;
528
529
lit1 = clause_GetLiteralTerm(C1, i);
530
multvec_i[i] = stamp;
531
532
if (i < c1fa) { /* Only consider relevant partner literals */
533
j = clause_FirstLitIndex();
534
n = c2fa;
535
}
536
else if (i < c1fs) {
537
j = c2fa;
538
n = c2fs;
539
}
540
else {
541
j = c2fs;
542
n = c2l;
543
}
544
545
while (j < n) {
546
if (multvec_j[j] != stamp) {
547
lit2 = clause_GetLiteralTerm(C2, j);
548
cont_StartBinding();
549
if (unify_MatchBindings(cont_LeftContext(), lit1, lit2)) {
550
multvec_j[j] = stamp;
551
if (subs_SubsumesInternBasic(C1,c1fa,c1fs,c1l,C2,c2fa,c2fs,c2l)) {
552
cont_BackTrack();
553
return TRUE;
554
}
555
multvec_j[j] = 0;
556
}
557
cont_BackTrack();
558
if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
559
fol_IsEquality(fol_Atom(lit1)) &&
560
fol_IsEquality(fol_Atom(lit2)) &&
561
(clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,i)) ||
562
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) {
563
cont_StartBinding();
564
if (unify_MatchBindings(cont_LeftContext(),
565
term_FirstArgument(fol_Atom(lit1)),
566
term_SecondArgument(fol_Atom(lit2))) &&
567
unify_MatchBindings(cont_LeftContext(),
568
term_SecondArgument(fol_Atom(lit1)),
569
term_FirstArgument(fol_Atom(lit2)))) {
570
multvec_j[j] = stamp;
571
if (subs_SubsumesInternBasic(C1,c1fa,c1fs,c1l,C2,c2fa,c2fs,c2l)) {
572
cont_BackTrack();
573
return TRUE;
574
}
575
multvec_j[j] = 0;
576
}
577
cont_BackTrack();
578
}
579
}
580
j++;
581
}
582
multvec_i[i] = 0;
583
return FALSE;
584
}
585
586
587
BOOL subs_SubsumesBasic(CLAUSE C1, CLAUSE C2, int ExceptI, int ExceptJ)
588
/**********************************************************
589
INPUT: Two clauses and for each clause a literal that are
590
already bound to each other. If the literal value is negative,
591
a general subsumption test is performed.
592
RETURNS: TRUE if the first clause subsumes the second one with respect
593
to basic restrictions on the sort literals.
594
CAUTION: The weight of the clauses must be up to date!
595
***********************************************************/
596
{
597
BOOL Result;
598
int c1fa,c1fs,c1l,c2fa,c2fs,c2l,lw1,lw2;
599
600
c1fa = clause_FirstAntecedentLitIndex(C1);
601
c1fs = clause_FirstSuccedentLitIndex(C1);
602
c1l = clause_Length(C1);
603
c2fa = clause_FirstAntecedentLitIndex(C2);
604
c2fs = clause_FirstSuccedentLitIndex(C2);
605
c2l = clause_Length(C2);
606
607
lw1 = (ExceptI >= clause_FirstLitIndex() ?
608
clause_LiteralWeight(clause_GetLiteral(C1,ExceptI)) : 0);
609
lw2 = (ExceptJ >= clause_FirstLitIndex() ?
610
clause_LiteralWeight(clause_GetLiteral(C2,ExceptJ)) : 0);
611
612
if (c1l > c2l || /* Multiset restriction */
613
(clause_Weight(C1)-lw1) > (clause_Weight(C2)-lw2)) {
614
return FALSE;
615
}
616
617
if (c1l > maxlits || c2l > maxlits) {
618
subs_ExtendLitVector();
619
stamp++;
620
}
621
else
622
if (++stamp == NAT_MAX) {
623
int i;
624
stamp = 1;
625
for (i = 0; i < maxlits; i++)
626
multvec_i[i] = multvec_j[i] = 0;
627
}
628
629
if (ExceptI >= clause_FirstLitIndex())
630
multvec_i[ExceptI] = stamp;
631
if (ExceptJ >= clause_FirstLitIndex())
632
multvec_j[ExceptJ] = stamp;
633
634
if (c1l > 1 &&
635
(!subs_PartnerTest(C1,clause_FirstConstraintLitIndex(C1),c1fa,
636
C2,clause_FirstConstraintLitIndex(C2),c2fa) ||
637
!subs_PartnerTest(C1,c1fa,c1fs,C2,c2fa,c2fs) ||
638
!subs_PartnerTest(C1,c1fs,c1l,C2,c2fs,c2l)))
639
return FALSE;
640
641
#ifdef CHECK
642
cont_SaveState();
643
#endif
644
645
Result = subs_SubsumesInternBasic(C1,c1fa,c1fs,c1l,C2,c2fa,c2fs,c2l);
646
647
#ifdef CHECK
648
cont_CheckState();
649
#endif
650
651
return Result;
652
}
653
654
655
static BOOL subs_SubsumesInternWithSignature(int i, CLAUSE c1, CLAUSE c2, BOOL Variants, LIST* Bindings)
656
/**********************************************************
657
INPUT:
658
RETURNS:
659
CAUTION:
660
***********************************************************/
661
{
662
int n,j;
663
TERM lit1,lit2;
664
LIST NewBindings,Scan;
665
666
j = 0;
667
n = clause_Length(c2);
668
lit1 = clause_GetLiteralTerm(c1,i);
669
NewBindings = list_Nil();
670
671
while (j < n) {
672
if (multvec_j[j] != stamp) {
673
lit2 = clause_GetLiteralTerm(c2,j);
674
cont_StartBinding();
675
if (fol_SignatureMatch(lit1,lit2,&NewBindings,Variants)) {
676
if (i == (clause_Length(c1)-1)) {
677
*Bindings = list_Nconc(NewBindings,*Bindings);
678
return TRUE;
679
}
680
multvec_j[j] = stamp;
681
if (subs_SubsumesInternWithSignature(i+1, c1, c2,Variants,&NewBindings)) {
682
*Bindings = list_Nconc(NewBindings,*Bindings);
683
return TRUE;
684
}
685
multvec_j[j] = 0;
686
}
687
for (Scan=NewBindings;!list_Empty(Scan);Scan=list_Cdr(Scan)) { /* Backtrack bindings */
688
if (symbol_IsVariable((SYMBOL)list_Car(Scan)))
689
term_ClearBinding((SYMBOL)list_Car(Scan));
690
else
691
symbol_ContextClearValue((SYMBOL)list_Car(Scan));
692
}
693
list_Delete(NewBindings);
694
NewBindings = list_Nil();
695
if (symbol_Equal(term_TopSymbol(fol_Atom(lit1)),term_TopSymbol(fol_Atom(lit2))) &&
696
fol_IsEquality(fol_Atom(lit1))) {
697
if (fol_SignatureMatch(term_FirstArgument(fol_Atom(lit1)),
698
term_SecondArgument(fol_Atom(lit2)), &NewBindings, Variants) &&
699
fol_SignatureMatch(term_SecondArgument(fol_Atom(lit1)),
700
term_FirstArgument(fol_Atom(lit2)), &NewBindings, Variants)) {
701
if (i == (clause_Length(c1)-1)) {
702
*Bindings = list_Nconc(NewBindings,*Bindings);
703
return TRUE;
704
}
705
multvec_j[j] = stamp;
706
if (subs_SubsumesInternWithSignature(i+1, c1, c2,Variants,&NewBindings)) {
707
*Bindings = list_Nconc(NewBindings,*Bindings);
708
return TRUE;
709
}
710
multvec_j[j] = 0;
711
}
712
for (Scan=NewBindings;!list_Empty(Scan);Scan=list_Cdr(Scan)) { /* Backtrack bindings */
713
if (symbol_IsVariable((SYMBOL)list_Car(Scan)))
714
term_ClearBinding((SYMBOL)list_Car(Scan));
715
else
716
symbol_ContextClearValue((SYMBOL)list_Car(Scan));
717
}
718
list_Delete(NewBindings);
719
NewBindings = list_Nil();
720
}
721
}
722
j++;
723
}
724
return FALSE;
725
}
726
727
BOOL subs_SubsumesWithSignature(CLAUSE C1, CLAUSE C2, BOOL Variants, LIST *Bindings)
728
/**********************************************************
729
INPUT: Two clauses .
730
RETURNS: TRUE if the first clause subsumes the second one where
731
we allow signature symbols to be matched as well.
732
If <Variants> is TRUE variables must be mapped to variables.
733
Returns the signature symbols that were bound.
734
EFFECT: Symbol context bindings are established.
735
***********************************************************/
736
{
737
BOOL Result;
738
739
if (clause_Length(C1) > clause_Length(C2) ||
740
clause_NumOfSuccLits(C1) > clause_NumOfSuccLits(C2) ||
741
(clause_NumOfAnteLits(C1) + clause_NumOfConsLits(C1)) >
742
(clause_NumOfAnteLits(C2) + clause_NumOfConsLits(C2))) { /* Multiset restriction */
743
return FALSE;
744
}
745
746
747
if (clause_Length(C1) > maxlits || clause_Length(C2) > maxlits) {
748
subs_ExtendLitVector();
749
stamp++;
750
}
751
else
752
if (++stamp == NAT_MAX) {
753
int i;
754
stamp = 1;
755
for (i = 0; i < maxlits; i++)
756
multvec_i[i] = multvec_j[i] = 0;
757
}
758
759
term_NewMark();
760
Result = subs_SubsumesInternWithSignature(clause_FirstLitIndex(),C1,C2,Variants, Bindings);
761
*Bindings = list_DeleteElementIf(*Bindings, (BOOL (*)(POINTER)) symbol_IsVariable);
762
return Result;
763
}
764
765
static BOOL subs_SubsumesIntern(CLAUSE C1, int c1fs, int c1l, CLAUSE C2, int c2fs, int c2l)
766
{
767
int i, j, n, k;
768
NAT occs, occsaux;
769
TERM lit1,lit2;
770
771
i = -1;
772
k = clause_FirstLitIndex();
773
occs = 0;
774
775
while (k < c1l) { /* Select literal with maximal variable occurrences. */
776
if (multvec_i[k] != stamp) {
777
if (i < 0) {
778
i = k;
779
occs = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,i));
780
} else
781
if ((occsaux = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,k)))
782
> occs) {
783
i = k;
784
occs = occsaux;
785
}
786
}
787
k++;
788
}
789
790
if (i < 0)
791
return TRUE;
792
793
lit1 = clause_GetLiteralTerm(C1, i);
794
multvec_i[i] = stamp;
795
796
if (i < c1fs) { /* Only consider relevant partner literals */
797
j = clause_FirstLitIndex();
798
n = c2fs;
799
}
800
else {
801
j = c2fs;
802
n = c2l;
803
}
804
805
while (j < n) {
806
if (multvec_j[j] != stamp) {
807
lit2 = clause_GetLiteralTerm(C2, j);
808
cont_StartBinding();
809
if (unify_MatchBindings(cont_LeftContext(), lit1, lit2)) {
810
multvec_j[j] = stamp;
811
if (subs_SubsumesIntern(C1,c1fs,c1l,C2,c2fs,c2l)) {
812
cont_BackTrack();
813
return TRUE;
814
}
815
multvec_j[j] = 0;
816
}
817
cont_BackTrack();
818
if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
819
fol_IsEquality(fol_Atom(lit1)) &&
820
fol_IsEquality(fol_Atom(lit2)) &&
821
(clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,i)) ||
822
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) {
823
cont_StartBinding();
824
if (unify_MatchBindings(cont_LeftContext(),
825
term_FirstArgument(fol_Atom(lit1)),
826
term_SecondArgument(fol_Atom(lit2))) &&
827
unify_MatchBindings(cont_LeftContext(),
828
term_SecondArgument(fol_Atom(lit1)),
829
term_FirstArgument(fol_Atom(lit2)))) {
830
multvec_j[j] = stamp;
831
if (subs_SubsumesIntern(C1,c1fs,c1l,C2,c2fs,c2l)) {
832
cont_BackTrack();
833
return TRUE;
834
}
835
multvec_j[j] = 0;
836
}
837
cont_BackTrack();
838
}
839
}
840
j++;
841
}
842
multvec_i[i] = 0;
843
return FALSE;
844
}
845
846
847
BOOL subs_Subsumes(CLAUSE C1, CLAUSE C2, int ExceptI, int ExceptJ)
848
/**********************************************************
849
INPUT: Two clauses and for each clause a literal that is
850
already bound to each other. If the literal value is negative,
851
a general subsumption test is performed.
852
RETURNS: TRUE if the first clause subsumes the second one.
853
CAUTION: The weight of the clauses must be up to date!
854
***********************************************************/
855
{
856
BOOL Result;
857
int c1fs, c1l, c2fs, c2l, lw1, lw2;
858
859
c1fs = clause_FirstSuccedentLitIndex(C1);
860
c1l = clause_Length(C1);
861
c2fs = clause_FirstSuccedentLitIndex(C2);
862
c2l = clause_Length(C2);
863
864
lw1 = (ExceptI >= clause_FirstLitIndex() ?
865
clause_LiteralWeight(clause_GetLiteral(C1,ExceptI)) : 0);
866
lw2 = (ExceptJ >= clause_FirstLitIndex() ?
867
clause_LiteralWeight(clause_GetLiteral(C2,ExceptJ)) : 0);
868
869
if (c1l > c2l || /* Multiset restriction */
870
(clause_Weight(C1) - lw1) > (clause_Weight(C2) - lw2))
871
return FALSE;
872
873
874
if (c1l > maxlits || c2l > maxlits) {
875
subs_ExtendLitVector();
876
stamp++;
877
}
878
else
879
if (++stamp == NAT_MAX) {
880
int i;
881
stamp = 1;
882
for (i = 0; i < maxlits; i++)
883
multvec_i[i] = multvec_j[i] = 0;
884
}
885
886
if (ExceptI >= clause_FirstLitIndex())
887
multvec_i[ExceptI] = stamp;
888
if (ExceptJ >= clause_FirstLitIndex())
889
multvec_j[ExceptJ] = stamp;
890
891
if (c1l > 1 &&
892
(!subs_PartnerTest(C1,clause_FirstConstraintLitIndex(C1),c1fs,
893
C2,clause_FirstConstraintLitIndex(C2),c2fs) ||
894
!subs_PartnerTest(C1,c1fs,c1l,C2,c2fs,c2l)))
895
return FALSE;
896
897
#ifdef CHECK
898
cont_SaveState();
899
#endif
900
901
Result = subs_SubsumesIntern(C1,c1fs,c1l,C2,c2fs,c2l);
902
903
#ifdef CHECK
904
cont_CheckState();
905
#endif
906
907
return Result;
908
}
909
910
911
912
913
BOOL subs_ST(int i, int j, CLAUSE c1, CLAUSE c2)
914
/**********************************************************
915
INPUT: Integers i,j and two clauses c1 and c2.
916
i and j stand for the i-th and the j-th literal
917
in the clause c1 respectively c2.
918
RETURNS: FALSE if c1 does not subsume c2 and TRUE otherwise.
919
CAUTION: None.
920
***********************************************************/
921
{
922
cont_StartBinding();
923
924
while ((j < clause_Length(c2)) &&
925
!(unify_Match(cont_LeftContext(),
926
clause_GetLiteralTerm(c1,i),
927
clause_GetLiteralTerm(c2,j)))){
928
j++;
929
cont_BackTrackAndStart();
930
}
931
932
if (j >= clause_Length(c2)) {
933
cont_BackTrack();
934
return FALSE;
935
}
936
937
if ((i == (clause_Length(c1)-1)) || subs_ST(i+1, 0, c1, c2))
938
return TRUE;
939
else
940
cont_BackTrack();
941
942
if (++j == clause_Length(c2))
943
return FALSE;
944
945
return subs_ST(i, j, c1, c2);
946
}
947
948
949
BOOL subs_Testlits(CLAUSE c1, CLAUSE c2)
950
/**********************************************************
951
INPUT: Two clauses c1 and c2.
952
RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise.
953
CAUTION: None.
954
***********************************************************/
955
{
956
TERM t1;
957
int i,j;
958
BOOL found;
959
960
for (i = 0; i < clause_Length(c1); i++){
961
j = 0;
962
found = FALSE;
963
t1 = clause_GetLiteralTerm(c1,i);
964
965
do {
966
cont_StartBinding();
967
if (!(found = unify_Match(cont_LeftContext(), t1, clause_GetLiteralTerm(c2,j))))
968
j++;
969
cont_BackTrack();
970
971
} while (!found && (j < clause_Length(c2)));
972
973
if (!found)
974
return FALSE;
975
}
976
977
return TRUE;
978
}
979
980
981
static LIST subs_GetVariables(TERM t)
982
/**********************************************************
983
INPUT: A term.
984
RETURNS: The list of non bound variables of the term.
985
CAUTION: None.
986
***********************************************************/
987
{
988
LIST scan,insert,symbols,end;
989
990
symbols = term_VariableSymbols(t);
991
insert = symbols;
992
end = list_Nil();
993
994
for (scan = symbols; !list_Empty(scan); scan = list_Cdr(scan)) {
995
if (!cont_VarIsBound(cont_LeftContext(), (SYMBOL)list_Car(scan))) {
996
end = insert;
997
list_Rplaca(insert, list_Car(scan));
998
insert = list_Cdr(insert);
999
}
1000
}
1001
1002
if (!list_Empty(insert)) {
1003
list_Delete(insert);
1004
if (list_Empty(end))
1005
symbols = list_Nil();
1006
else
1007
list_Rplacd(end,list_Nil());
1008
}
1009
1010
return(symbols);
1011
}
1012
1013
1014
static BOOL subs_SubsumptionPossible(CLAUSE c1, CLAUSE c2)
1015
/**********************************************************
1016
INPUT: Two clauses c1 and c2.
1017
RETURNS: TRUE if every literal in c1 can independently be
1018
matched to a literal in c2.
1019
CAUTION: None.
1020
***********************************************************/
1021
{
1022
int i,j;
1023
1024
for (i = 0; i < clause_Length(c1); i++) {
1025
for (j = 0; j < clause_Length(c2); j++) {
1026
cont_StartBinding();
1027
if (unify_Match(cont_LeftContext(),
1028
clause_GetLiteralTerm(c1,i),
1029
clause_GetLiteralTerm(c2,j)))
1030
j = clause_Length(c2) + 1;
1031
cont_BackTrack();
1032
}
1033
if (j == clause_Length(c2))
1034
return FALSE;
1035
}
1036
1037
return TRUE;
1038
}
1039
1040
1041
BOOL subs_IdcTestlits(CLAUSE c1, CLAUSE c2, LITPTR* litptr)
1042
/**********************************************************
1043
INPUT: Two clauses c1, c2 and a pointer to a litptr structure.
1044
RETURNS: FALSE if c1 can not independently be matched
1045
to c2 and TRUE otherwise.
1046
CAUTION: A structure is build and litptr points to that structure.
1047
***********************************************************/
1048
{
1049
LIST TermIndexlist,VarSymbList,TermSymbList;
1050
int i;
1051
1052
if (subs_SubsumptionPossible(c1,c2)) {
1053
1054
TermIndexlist = list_Nil();
1055
VarSymbList = list_Nil();
1056
TermSymbList = list_Nil();
1057
1058
for (i = 0; i < clause_Length(c1); i++) {
1059
VarSymbList = subs_GetVariables(clause_GetLiteralTerm(c1,i));
1060
1061
if (VarSymbList != list_Nil()){
1062
TermIndexlist = list_Cons((POINTER)i, TermIndexlist);
1063
TermSymbList = list_Cons(VarSymbList,TermSymbList);
1064
}
1065
}
1066
1067
*litptr = litptr_Create(TermIndexlist,TermSymbList);
1068
1069
list_Delete(TermSymbList);
1070
list_Delete(TermIndexlist);
1071
1072
return TRUE;
1073
}
1074
return FALSE;
1075
}
1076
1077
1078
static BOOL subs_SubsumptionVecPossible(CLAUSE c1, int vec, CLAUSE c2)
1079
/**********************************************************
1080
INPUT: Two clauses c1 and c2 and a vector pointer.
1081
RETURNS: TRUE if all literals in c1 which indexes stand
1082
in the vector with bottom pointer vec can
1083
independently be matched to a literal in c2.
1084
CAUTION: None.
1085
***********************************************************/
1086
{
1087
int i,j;
1088
1089
for (i = vec; i < vec_ActMax(); i++) {
1090
for (j = 0; j < clause_Length(c2); j++) {
1091
cont_StartBinding();
1092
if (unify_Match(cont_LeftContext(),
1093
clause_GetLiteralTerm(c1, (int) vec_GetNth(i)),
1094
clause_GetLiteralTerm(c2,j)))
1095
j = clause_Length(c2) + 1;
1096
cont_BackTrack();
1097
}
1098
if (j == clause_Length(c2))
1099
return FALSE;
1100
}
1101
1102
return TRUE;
1103
}
1104
1105
1106
static BOOL subs_SubsumptionVecPossibleEq(CLAUSE c1, int vec, CLAUSE c2)
1107
/**********************************************************
1108
INPUT: Two clauses c1 and c2 and a vector pointer.
1109
RETURNS: TRUE if all literals in c1 which indexes stand
1110
in the vector with bottom pointer vec can
1111
independently be matched to a literal in c2.
1112
CAUTION: None.
1113
***********************************************************/
1114
{
1115
int i,j,n;
1116
TERM lit1,lit2;
1117
1118
n = clause_Length(c2);
1119
for (i = vec; i < vec_ActMax(); i++) {
1120
lit1 = clause_GetLiteralTerm(c1, (int) vec_GetNth(i));
1121
for (j=0;j<n;j++) {
1122
lit2 = clause_GetLiteralTerm(c2,j);
1123
cont_StartBinding();
1124
if (unify_Match(cont_LeftContext(),lit1,lit2)) {
1125
j = n + 1;
1126
cont_BackTrack();
1127
}
1128
else {
1129
cont_BackTrack();
1130
if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
1131
fol_IsEquality(fol_Atom(lit1)) &&
1132
fol_IsEquality(fol_Atom(lit2)) &&
1133
(clause_LiteralIsNotOrientedEquality(
1134
clause_GetLiteral(c1, (int)vec_GetNth(i))) ||
1135
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,j)))) {
1136
cont_StartBinding();
1137
if (unify_Match(cont_LeftContext(),
1138
term_FirstArgument(fol_Atom(lit1)),
1139
term_SecondArgument(fol_Atom(lit2))) &&
1140
unify_Match(cont_LeftContext(),
1141
term_SecondArgument(fol_Atom(lit1)),
1142
term_FirstArgument(fol_Atom(lit2))))
1143
j = n+1;
1144
cont_BackTrack();
1145
}
1146
}
1147
}
1148
if (j==n)
1149
return FALSE;
1150
}
1151
1152
return TRUE;
1153
}
1154
1155
1156
static BOOL subs_IdcVecTestlits(CLAUSE c1, int vec, CLAUSE c2, LITPTR* litptr)
1157
/**********************************************************
1158
INPUT: Two clauses c1, c2, a pointer to a literal structure and
1159
a vector pointer.
1160
RETURNS: FALSE if the literals of c1 which are designated by
1161
the elements of vec do not subsume c2 and TRUE otherwise.
1162
CAUTION: A structure is build and litptr points to that structure.
1163
***********************************************************/
1164
{
1165
LIST TermIndexlist,VarSymbList,TermSymbList;
1166
int i;
1167
1168
if (subs_SubsumptionVecPossible(c1,vec,c2)) {
1169
1170
TermIndexlist = list_Nil();
1171
VarSymbList = list_Nil();
1172
TermSymbList = list_Nil();
1173
1174
for (i = vec; i < vec_ActMax(); i++) {
1175
VarSymbList =
1176
subs_GetVariables(clause_GetLiteralTerm(c1, (int) vec_GetNth(i)));
1177
1178
if (VarSymbList != list_Nil()){
1179
TermIndexlist = list_Cons(vec_GetNth(i), TermIndexlist);
1180
TermSymbList = list_Cons(VarSymbList,TermSymbList);
1181
}
1182
}
1183
1184
*litptr = litptr_Create(TermIndexlist,TermSymbList);
1185
1186
list_Delete(TermSymbList);
1187
list_Delete(TermIndexlist);
1188
1189
return TRUE;
1190
}
1191
return FALSE;
1192
}
1193
1194
1195
static BOOL subs_IdcVecTestlitsEq(CLAUSE c1, int vec, CLAUSE c2,
1196
LITPTR* litptr)
1197
/**********************************************************
1198
INPUT: Two clauses c1, c2, a pointer to a literal structure and
1199
a vector pointer.
1200
RETURNS: FALSE if the literals of c1 which are designated by
1201
the elements of vec do not subsume c2 and TRUE otherwise.
1202
CAUTION: A structure is build and litptr points to that structure.
1203
***********************************************************/
1204
{
1205
LIST TermIndexlist,VarSymbList,TermSymbList;
1206
int i;
1207
1208
if (subs_SubsumptionVecPossibleEq(c1,vec,c2)) {
1209
1210
TermIndexlist = list_Nil();
1211
VarSymbList = list_Nil();
1212
TermSymbList = list_Nil();
1213
1214
for (i = vec; i < vec_ActMax(); i++){
1215
VarSymbList =
1216
subs_GetVariables(clause_GetLiteralTerm(c1, (int) vec_GetNth(i)));
1217
1218
if (VarSymbList != list_Nil()){
1219
TermIndexlist = list_Cons(vec_GetNth(i), TermIndexlist);
1220
TermSymbList = list_Cons(VarSymbList,TermSymbList);
1221
}
1222
}
1223
1224
*litptr = litptr_Create(TermIndexlist,TermSymbList);
1225
1226
list_Delete(TermSymbList);
1227
list_Delete(TermIndexlist);
1228
1229
return TRUE;
1230
}
1231
return FALSE;
1232
}
1233
1234
1235
static void subs_CompVec(LITPTR litptr)
1236
/**********************************************************
1237
INPUT: A LITPTR pointer.
1238
RETURNS: None.
1239
CAUTION: Indexes are pushed on the vector. These indexes build
1240
a component with respect to the structure litptr and to the
1241
actual bindings.
1242
***********************************************************/
1243
{
1244
LIST complist, end, scan;
1245
int lit,n,i,j;
1246
1247
n = litptr_Length(litptr);
1248
complist = list_Nil();
1249
1250
1251
if (n > 0){
1252
for (j = 0; j < n; j++) {
1253
if (!literal_GetUsed(litptr_Literal(litptr,j))) {
1254
complist = list_Cons((POINTER)j,complist);
1255
vec_Push((POINTER)literal_GetLitIndex(litptr_Literal(litptr,j)));
1256
literal_PutUsed(litptr_Literal(litptr,j), TRUE);
1257
j = n + 1;
1258
}
1259
}
1260
1261
if (j != n) {
1262
end = complist;
1263
for (scan = complist; !list_Empty(scan); scan = list_Cdr(scan)) {
1264
lit = (int)list_Car(scan);
1265
for (i = 0; i < n; i++) {
1266
if (!literal_GetUsed(litptr_Literal(litptr,i)) &&
1267
list_HasIntersection(literal_GetLitVarList(litptr_Literal(litptr,lit)),
1268
literal_GetLitVarList(litptr_Literal(litptr,i)))) {
1269
list_Rplacd(end,list_List((POINTER)i));
1270
end = list_Cdr(end);
1271
vec_Push((POINTER)literal_GetLitIndex(litptr_Literal(litptr,i)));
1272
literal_PutUsed(litptr_Literal(litptr,i), TRUE);
1273
}
1274
}
1275
}
1276
list_Delete(complist);
1277
}
1278
}
1279
}
1280
1281
1282
static BOOL subs_StVec(int i, int j, CLAUSE c1, CLAUSE c2)
1283
/**********************************************************
1284
INPUT: Integers i,j and two clauses c1 and c2.
1285
i is a pointer to vector and represents a
1286
literal in clause c1 and j stand for the j-th
1287
literal in the clause c2.
1288
RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise.
1289
CAUTION: None.
1290
***********************************************************/
1291
{
1292
int a;
1293
1294
if (j >= clause_Length(c2))
1295
return FALSE;
1296
1297
a = j;
1298
1299
cont_StartBinding();
1300
1301
while ((a < clause_Length(c2)) &&
1302
!(unify_Match(cont_LeftContext(),
1303
clause_GetLiteralTerm(c1, (int) vec_GetNth(i)),
1304
clause_GetLiteralTerm(c2,a)))){
1305
a++;
1306
cont_BackTrackAndStart();
1307
}
1308
1309
if (a >= clause_Length(c2)) {
1310
cont_BackTrack();
1311
return FALSE;
1312
}
1313
1314
if ((i == (vec_ActMax()-1)) || subs_StVec(i+1, 0, c1, c2))
1315
return TRUE;
1316
else
1317
cont_BackTrack();
1318
1319
return subs_StVec(i, a+1, c1, c2);
1320
}
1321
1322
1323
static int subs_SearchTop(CLAUSE c1, int vec, CLAUSE c2)
1324
/**********************************************************
1325
INPUT: Two clauses c1, c2, a vector pointer vec.
1326
RETURNS: The index of that literal in c1 which has the least positive
1327
matching tests with the literals in c2.
1328
CAUTION: None.
1329
***********************************************************/
1330
{
1331
int found_index, i, j, zaehler;
1332
1333
found_index = (int)vec_GetNth(vec);
1334
1335
for (i = vec; i < vec_ActMax(); i++) {
1336
zaehler = 0;
1337
j = 0;
1338
while (j < clause_Length(c2) && zaehler < 2) {
1339
cont_StartBinding();
1340
if (unify_Match(cont_LeftContext(),
1341
clause_GetLiteralTerm(c1, (int) vec_GetNth(i)),
1342
clause_GetLiteralTerm(c2,j))) {
1343
zaehler++;
1344
}
1345
cont_BackTrack();
1346
j++;
1347
}
1348
1349
if (zaehler == 0 || zaehler == 1) {
1350
found_index = (int)vec_GetNth(i);
1351
return found_index;
1352
}
1353
}
1354
return found_index;
1355
}
1356
1357
1358
static BOOL subs_TcVec(CLAUSE c1, int vec, CLAUSE c2)
1359
/**********************************************************
1360
INPUT: Two clauses c1, c2, a vector pointer vec.
1361
RETURNS: FALSE if the literals of c1 which are designated by
1362
the elements of vec do not subsume c2 and TRUE otherwise.
1363
CAUTION: None.
1364
***********************************************************/
1365
{
1366
int a,top_index;
1367
a = 0;
1368
1369
top_index = subs_SearchTop(c1,vec,c2);
1370
1371
do {
1372
cont_StartBinding();
1373
while ((a < clause_Length(c2)) &&
1374
!(unify_Match(cont_LeftContext(),
1375
clause_GetLiteralTerm(c1,top_index),
1376
clause_GetLiteralTerm(c2,a)))) {
1377
a++;
1378
cont_BackTrackAndStart();
1379
}
1380
1381
if (a >= clause_Length(c2)){
1382
cont_BackTrack();
1383
return FALSE;
1384
}
1385
1386
if ((vec - vec_ActMax()) == 1)
1387
return TRUE;
1388
1389
if (subs_InternIdc(c1, vec, c2))
1390
return TRUE;
1391
else {
1392
cont_BackTrack(); /* Dies ist der 'Hurra' Fall.*/
1393
a++;
1394
}
1395
1396
} while (a < clause_Length(c2));
1397
1398
return FALSE;
1399
}
1400
1401
static BOOL subs_TcVecEq(CLAUSE c1, int vec, CLAUSE c2)
1402
/**********************************************************
1403
INPUT: Two clauses c1, c2, a vector pointer vec.
1404
RETURNS: FALSE if the literals of c1 which are designated by
1405
the elements of vec do not subsume c2 and TRUE otherwise.
1406
CAUTION: None.
1407
***********************************************************/
1408
{
1409
int a,top_index;
1410
BOOL search;
1411
TERM lit1,lit2;
1412
1413
a = 0;
1414
top_index = subs_SearchTop(c1,vec,c2);
1415
lit1 = clause_GetLiteralTerm(c1,top_index);
1416
1417
do {
1418
search = TRUE;
1419
1420
while (a < clause_Length(c2) && search) {
1421
lit2 = clause_GetLiteralTerm(c2,a);
1422
cont_StartBinding();
1423
if (unify_Match(cont_LeftContext(),lit1,lit2))
1424
search = FALSE;
1425
else {
1426
if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
1427
fol_IsEquality(fol_Atom(lit1)) &&
1428
fol_IsEquality(fol_Atom(lit2)) &&
1429
(clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c1,top_index)) ||
1430
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,a)))) {
1431
cont_BackTrackAndStart();
1432
if (unify_Match(cont_LeftContext(),
1433
term_FirstArgument(fol_Atom(lit1)),
1434
term_SecondArgument(fol_Atom(lit2))) &&
1435
unify_Match(cont_LeftContext(),
1436
term_SecondArgument(fol_Atom(lit1)),
1437
term_FirstArgument(fol_Atom(lit2))))
1438
search = FALSE;
1439
}
1440
if (search) {
1441
a++;
1442
cont_BackTrack();
1443
}
1444
}
1445
}
1446
1447
if (a >= clause_Length(c2)) {
1448
cont_BackTrack();
1449
return FALSE;
1450
}
1451
1452
if ((vec_ActMax() - vec) == 1)
1453
return TRUE;
1454
1455
if (subs_InternIdcEq(c1, vec, c2))
1456
return TRUE;
1457
else {
1458
cont_BackTrack();
1459
a++;
1460
}
1461
1462
} while (a < clause_Length(c2));
1463
1464
return FALSE;
1465
}
1466
1467
1468
static BOOL subs_InternIdc(CLAUSE c1, int vec, CLAUSE c2)
1469
/**********************************************************
1470
INPUT: Two clauses c1, c2, a vector pointer vec.
1471
RETURNS: FALSE if the literals of c1 which are designed by
1472
the elements of vec do not subsume c2 and TRUE otherwise.
1473
CAUTION:
1474
***********************************************************/
1475
{
1476
int locvec;
1477
LITPTR litptr;
1478
1479
1480
if (!subs_IdcVecTestlits(c1,vec,c2,&litptr))
1481
return FALSE;
1482
1483
locvec = vec_ActMax();
1484
1485
do {
1486
subs_CompVec(litptr);
1487
if (!vec_IsMax(locvec)) {
1488
if (!subs_TcVec(c1,locvec,c2)) {
1489
vec_SetMax(locvec);
1490
litptr_Delete(litptr);
1491
return FALSE;
1492
}
1493
else
1494
vec_SetMax(locvec);
1495
}
1496
} while (!litptr_AllUsed(litptr));
1497
1498
litptr_Delete(litptr);
1499
1500
return TRUE;
1501
}
1502
1503
1504
static BOOL subs_InternIdcEq(CLAUSE c1, int vec, CLAUSE c2)
1505
/**********************************************************
1506
INPUT: Two clauses c1, c2, a vector pointer vec.
1507
RETURNS: FALSE if the literals of c1 which are designed by
1508
the elements of vec do not subsume c2 and TRUE otherwise.
1509
CAUTION:
1510
***********************************************************/
1511
{
1512
int locvec;
1513
LITPTR litptr;
1514
1515
1516
if (!subs_IdcVecTestlitsEq(c1,vec,c2,&litptr))
1517
return FALSE;
1518
1519
locvec = vec_ActMax();
1520
1521
do {
1522
subs_CompVec(litptr);
1523
if (!vec_IsMax(locvec)) {
1524
if (!subs_TcVecEq(c1,locvec,c2)) {
1525
vec_SetMax(locvec);
1526
litptr_Delete(litptr);
1527
return FALSE;
1528
}
1529
else
1530
vec_SetMax(locvec);
1531
}
1532
1533
} while (!litptr_AllUsed(litptr));
1534
1535
litptr_Delete(litptr);
1536
1537
return TRUE;
1538
}
1539
1540
1541
BOOL subs_Idc(CLAUSE c1, CLAUSE c2)
1542
/**********************************************************
1543
INPUT: Two clauses c1, c2.
1544
RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise.
1545
CAUTION:
1546
***********************************************************/
1547
{
1548
int i,vec;
1549
BOOL Result;
1550
1551
vec = vec_ActMax();
1552
1553
for (i = 0; i < clause_Length(c1); i++)
1554
vec_Push((POINTER) i);
1555
1556
Result = subs_InternIdc(c1,vec,c2);
1557
1558
vec_SetMax(vec);
1559
1560
cont_Reset();
1561
1562
return Result;
1563
}
1564
1565
1566
BOOL subs_IdcEq(CLAUSE c1, CLAUSE c2)
1567
/**********************************************************
1568
INPUT: Two clauses c1, c2.
1569
RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise.
1570
CAUTION:
1571
***********************************************************/
1572
{
1573
int i,vec;
1574
BOOL Result;
1575
1576
/*fputs("\n Idc on: ", stdout); clause_Print(c1);
1577
putchar('\t'); clause_Print(c2); */
1578
vec = vec_ActMax();
1579
1580
for (i = 0; i < clause_Length(c1); i++)
1581
vec_Push((POINTER) i);
1582
1583
Result = subs_InternIdcEq(c1,vec,c2);
1584
1585
vec_SetMax(vec);
1586
1587
cont_Reset();
1588
1589
/*printf(" Result: %s ",(Result ? "TRUE" : "FALSE"));*/
1590
1591
return Result;
1592
}
1593
1594
1595
BOOL subs_IdcEqMatch(CLAUSE c1, CLAUSE c2, SUBST subst)
1596
/**********************************************************
1597
INPUT: Two clauses c1, c2.
1598
RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise.
1599
CAUTION:
1600
***********************************************************/
1601
{
1602
int i,vec;
1603
BOOL Result;
1604
1605
/* fputs("\n Idc on: ", stdout); clause_Print(c1);
1606
putchar('\t'); clause_Print(c2); DBG */
1607
vec = vec_ActMax();
1608
1609
for (i = 0; i < clause_Length(c1); i++)
1610
vec_Push((POINTER) i);
1611
1612
i = 0; /* Doesn't matter, there is a general cont_Reset below */
1613
unify_EstablishMatcher(cont_LeftContext(), subst);
1614
1615
Result = subs_InternIdcEq(c1,vec,c2);
1616
1617
vec_SetMax(vec);
1618
1619
cont_Reset();
1620
1621
/*fputs("\nsubs_Idc end: ",stdout); clause_Print(c1); clause_Print(c2); DBG */
1622
1623
return Result;
1624
}
1625
1626
1627
static BOOL subs_SubsumptionVecPossibleRes(CLAUSE c1, int vec,
1628
int beg, int end)
1629
/**********************************************************
1630
INPUT: Two clauses c1 and c2 and three vector pointer
1631
vec,beg and end.
1632
RETURNS: TRUE if all literals in c1 which indexes stand
1633
in the vector with bottom pointer vec can
1634
independently be matched to a literal in c2
1635
which indexes stand in the vector between the
1636
pointers beg and end (exclusive).
1637
CAUTION: None.
1638
***********************************************************/
1639
{
1640
int j,i;
1641
1642
for (i = vec; i < vec_ActMax(); i++) {
1643
for (j = beg; j < end; j++){
1644
cont_StartBinding();
1645
if (unify_Match(cont_LeftContext(),
1646
clause_GetLiteralTerm(c1, (int) vec_GetNth(i)),
1647
clause_GetLiteralTerm(c1, (int) vec_GetNth(j))))
1648
j = end+1;
1649
cont_BackTrack();
1650
}
1651
if (j == end)
1652
return FALSE;
1653
}
1654
return TRUE;
1655
}
1656
1657
1658
static BOOL subs_IdcVecTestlitsRes(CLAUSE c1, int vec,
1659
int beg, int end, LITPTR* litptr)
1660
/**********************************************************
1661
INPUT: A clause c1, a pointer to a literal structure and
1662
three vector pointer vec, beg and end.
1663
RETURNS: FALSE if the literals of c1 which are designated by
1664
the elements of vec can not be matched independently
1665
to literal in c2 which are designated by the elements
1666
of the vector between the pointers beg and end (exclusive).
1667
CAUTION: A structure is build and litptr points to that structure.
1668
***********************************************************/
1669
{
1670
LIST TermIndexlist,VarSymbList,TermSymbList;
1671
int i;
1672
1673
if (subs_SubsumptionVecPossibleRes(c1,vec,beg,end)) {
1674
1675
TermIndexlist = list_Nil();
1676
VarSymbList = list_Nil();
1677
TermSymbList = list_Nil();
1678
1679
for (i = vec; i < vec_ActMax(); i++) {
1680
VarSymbList =
1681
subs_GetVariables(clause_GetLiteralTerm(c1, (int) vec_GetNth(i)));
1682
1683
if (VarSymbList != list_Nil()) {
1684
TermIndexlist = list_Cons(vec_GetNth(i), TermIndexlist);
1685
TermSymbList = list_Cons(VarSymbList,TermSymbList);
1686
}
1687
}
1688
1689
*litptr = litptr_Create(TermIndexlist,TermSymbList);
1690
1691
list_Delete(TermSymbList);
1692
list_Delete(TermIndexlist);
1693
1694
return TRUE;
1695
}
1696
return FALSE;
1697
}
1698
1699
1700
static int subs_SearchTopRes(CLAUSE c1, int vec, int beg, int end)
1701
/**********************************************************
1702
INPUT: A clause c1, three vector pointers vec, beg and end.
1703
RETURNS: The index of that literal in c1 which has the least positive
1704
matching tests with the literals in c2 with respect to
1705
vector and the vector pointers beg and end.
1706
CAUTION: None.
1707
***********************************************************/
1708
{
1709
int found_index,i,j,zaehler;
1710
1711
found_index = (int) vec_GetNth(vec);
1712
1713
for (i = vec; i < vec_ActMax(); i++) {
1714
zaehler = 0;
1715
j = beg;
1716
while ((j < end) && (zaehler < 2)) {
1717
cont_StartBinding();
1718
if (unify_Match(cont_LeftContext(),
1719
clause_GetLiteralTerm(c1, (int) vec_GetNth(i)),
1720
clause_GetLiteralTerm(c1, (int) vec_GetNth(j)))) {
1721
zaehler++;
1722
}
1723
cont_BackTrack();
1724
j++;
1725
}
1726
1727
if (zaehler == 0 || zaehler == 1) {
1728
found_index = (int)vec_GetNth(i);
1729
return found_index;
1730
}
1731
}
1732
return found_index;
1733
}
1734
1735
1736
static BOOL subs_TcVecRes(CLAUSE c1, int vec, int beg, int end)
1737
/**********************************************************
1738
INPUT: A clause c1, three vector pointers vec,beg and end.
1739
RETURNS: FALSE if the literals of c1 which are designated by
1740
the elements of vec do not subsume c2 with
1741
respect to the vector and the vector pointers
1742
beg and end and TRUE otherwise.
1743
CAUTION: None.
1744
***********************************************************/
1745
{
1746
int a,top_index;
1747
1748
a = beg;
1749
1750
top_index = subs_SearchTopRes(c1,vec,beg,end);
1751
1752
do {
1753
cont_StartBinding();
1754
while ((a < end) &&
1755
!unify_Match(cont_LeftContext(),
1756
clause_GetLiteralTerm(c1,top_index),
1757
clause_GetLiteralTerm(c1,(int)vec_GetNth(a)))) {
1758
a++;
1759
cont_BackTrackAndStart();
1760
}
1761
1762
if (a >= end){
1763
cont_BackTrack();
1764
return FALSE;
1765
}
1766
1767
if ((vec - vec_ActMax()) == 1)
1768
return TRUE;
1769
1770
if (subs_InternIdcRes(c1, vec, beg, end))
1771
return TRUE;
1772
else {
1773
cont_BackTrack();
1774
a++;
1775
}
1776
1777
} while (a < end);
1778
1779
return FALSE;
1780
}
1781
1782
1783
static BOOL subs_InternIdcRes(CLAUSE c1, int vec, int beg, int end)
1784
/**********************************************************
1785
INPUT: A clause c1 and three vector pointers vec,beg and end.
1786
RETURNS: FALSE if the literals of c1 which are designated by
1787
the elements of vec do not subsume c2 with respect
1788
to vector and the vector pointers beg and end
1789
and TRUE otherwise.
1790
CAUTION: None.
1791
***********************************************************/
1792
{
1793
int locvec;
1794
LITPTR litptr;
1795
1796
1797
if (!subs_IdcVecTestlitsRes(c1,vec,beg,end,&litptr))
1798
return FALSE;
1799
1800
locvec = vec_ActMax();
1801
1802
do {
1803
subs_CompVec(litptr);
1804
if (!vec_IsMax(locvec)) {
1805
if (!subs_TcVecRes(c1,locvec,beg,end)) {
1806
vec_SetMax(locvec);
1807
litptr_Delete(litptr);
1808
return FALSE;
1809
}
1810
else
1811
vec_SetMax(locvec);
1812
}
1813
} while (!litptr_AllUsed(litptr));
1814
1815
litptr_Delete(litptr);
1816
1817
return TRUE;
1818
}
1819
1820
1821
BOOL subs_IdcRes(CLAUSE c1, int beg, int end)
1822
/**********************************************************
1823
INPUT: A clause c1 and two vector pointers beg and end.
1824
RETURNS: FALSE if c1 do not subsume c2 with respect to
1825
vector and the vector pointers beg and end
1826
and TRUE otherwise.
1827
CAUTION:
1828
***********************************************************/
1829
{
1830
int i,vec;
1831
BOOL Result;
1832
1833
vec = vec_ActMax();
1834
1835
for (i = 0; i < clause_Length(c1); i++)
1836
vec_Push((POINTER) i);
1837
1838
Result = subs_InternIdcRes(c1, vec, beg, end);
1839
1840
vec_SetMax(vec);
1841
1842
cont_Reset();
1843
1844
return Result;
1845
}
1846
1847
1848
static BOOL subs_TcVecEqExcept(CLAUSE c1, int vec, CLAUSE c2, int i2)
1849
/**********************************************************
1850
INPUT: Two clauses c1, c2, a vector pointer vec.
1851
RETURNS: FALSE if the literals of c1 which are designated by
1852
the elements of vec do not subsume c2 and TRUE otherwise.
1853
CAUTION: None.
1854
***********************************************************/
1855
{
1856
int a,top_index;
1857
BOOL search;
1858
TERM lit1,lit2;
1859
1860
a = 0;
1861
top_index = subs_SearchTop(c1,vec,c2);
1862
lit1 = clause_GetLiteralTerm(c1,top_index);
1863
1864
do {
1865
search = TRUE;
1866
1867
while (a < clause_Length(c2) && search) {
1868
if (a != i2) {
1869
lit2 = clause_GetLiteralTerm(c2,a);
1870
cont_StartBinding();
1871
if (unify_Match(cont_LeftContext(),lit1,lit2))
1872
search = FALSE;
1873
else {
1874
if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
1875
fol_IsEquality(fol_Atom(lit1)) &&
1876
fol_IsEquality(fol_Atom(lit2)) &&
1877
(clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c1,top_index)) ||
1878
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,a)))) {
1879
cont_BackTrackAndStart();
1880
if (unify_Match(cont_LeftContext(),
1881
term_FirstArgument(fol_Atom(lit1)),
1882
term_SecondArgument(fol_Atom(lit2))) &&
1883
unify_Match(cont_LeftContext(),
1884
term_SecondArgument(fol_Atom(lit1)),
1885
term_FirstArgument(fol_Atom(lit2))))
1886
search = FALSE;
1887
}
1888
if (search) {
1889
a++;
1890
cont_BackTrack();
1891
}
1892
}
1893
}
1894
else
1895
a++;
1896
}
1897
1898
if (a>=clause_Length(c2)) {
1899
cont_BackTrack();
1900
return FALSE;
1901
}
1902
1903
if ((vec_ActMax() - vec) == 1)
1904
return TRUE;
1905
1906
if (subs_InternIdcEqExcept(c1, vec, c2, i2))
1907
return TRUE;
1908
else {
1909
cont_BackTrack();
1910
a++;
1911
}
1912
1913
} while (a < clause_Length(c2));
1914
1915
return FALSE;
1916
}
1917
1918
1919
static BOOL subs_SubsumptionVecPossibleEqExcept(CLAUSE c1, int vec,
1920
CLAUSE c2, int i2)
1921
/**********************************************************
1922
INPUT: Two clauses c1 and c2 and a vector pointer
1923
and an accept literal index for c2.
1924
RETURNS: TRUE if all literals in c1 which indexes stand
1925
in the vector with bottom pointer vec can
1926
independently be matched to a literal in c2.
1927
CAUTION: None.
1928
***********************************************************/
1929
{
1930
int i,j,n;
1931
TERM lit1,lit2;
1932
1933
n = clause_Length(c2);
1934
for (i = vec; i < vec_ActMax(); i++) {
1935
lit1 = clause_GetLiteralTerm(c1, (int) vec_GetNth(i));
1936
for (j = 0; j < n; j++) {
1937
if (j != i2) {
1938
lit2 = clause_GetLiteralTerm(c2,j);
1939
cont_StartBinding();
1940
if (unify_Match(cont_LeftContext(),lit1,lit2))
1941
j = n + 1;
1942
else {
1943
if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
1944
fol_IsEquality(fol_Atom(lit1)) &&
1945
fol_IsEquality(fol_Atom(lit2)) &&
1946
(clause_LiteralIsNotOrientedEquality(
1947
clause_GetLiteral(c1,(int)vec_GetNth(i))) ||
1948
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,j)))) {
1949
cont_BackTrackAndStart();
1950
if (unify_Match(cont_LeftContext(),
1951
term_FirstArgument(fol_Atom(lit1)),
1952
term_SecondArgument(fol_Atom(lit2))) &&
1953
unify_Match(cont_LeftContext(),
1954
term_SecondArgument(fol_Atom(lit1)),
1955
term_FirstArgument(fol_Atom(lit2))))
1956
j = n+1;
1957
}
1958
}
1959
cont_BackTrack();
1960
}
1961
}
1962
if (j==n)
1963
return FALSE;
1964
}
1965
1966
return TRUE;
1967
}
1968
1969
1970
static BOOL subs_IdcVecTestlitsEqExcept(CLAUSE c1, int vec,
1971
CLAUSE c2, int i2, LITPTR* litptr)
1972
/**********************************************************
1973
INPUT: Two clauses c1, c2, a pointer to a literal structure and
1974
a vector pointer and a literal index i2 in c2
1975
RETURNS: FALSE if the literals of c1 which are designated by
1976
the elements of vec do not subsume c2 and TRUE otherwise.
1977
CAUTION: A structure is build and litptr points to that structure.
1978
***********************************************************/
1979
{
1980
LIST TermIndexlist,VarSymbList,TermSymbList;
1981
int i;
1982
1983
if (subs_SubsumptionVecPossibleEqExcept(c1,vec,c2,i2)) {
1984
1985
TermIndexlist = list_Nil();
1986
VarSymbList = list_Nil();
1987
TermSymbList = list_Nil();
1988
1989
for (i = vec; i < vec_ActMax(); i++) {
1990
VarSymbList =
1991
subs_GetVariables(clause_GetLiteralTerm(c1, (int) vec_GetNth(i)));
1992
1993
if (VarSymbList != list_Nil()){
1994
TermIndexlist = list_Cons(vec_GetNth(i), TermIndexlist);
1995
TermSymbList = list_Cons(VarSymbList,TermSymbList);
1996
}
1997
}
1998
1999
*litptr = litptr_Create(TermIndexlist,TermSymbList);
2000
2001
list_Delete(TermSymbList);
2002
list_Delete(TermIndexlist);
2003
2004
return TRUE;
2005
}
2006
return FALSE;
2007
}
2008
2009
2010
static BOOL subs_InternIdcEqExcept(CLAUSE c1, int vec, CLAUSE c2, int i2)
2011
/**********************************************************
2012
INPUT: Two clauses c1, c2, a vector pointer vec and a literal
2013
i2 in c2 which must not be considered
2014
RETURNS: FALSE if the literals of c1 which are designed by
2015
the elements of vec do not subsume c2/i2 and TRUE otherwise.
2016
CAUTION:
2017
***********************************************************/
2018
{
2019
int locvec;
2020
LITPTR litptr;
2021
2022
2023
if (!subs_IdcVecTestlitsEqExcept(c1,vec,c2,i2,&litptr))
2024
return FALSE;
2025
2026
locvec = vec_ActMax();
2027
2028
do {
2029
subs_CompVec(litptr);
2030
if (!vec_IsMax(locvec)) {
2031
if (!subs_TcVecEqExcept(c1,locvec,c2,i2)) {
2032
vec_SetMax(locvec);
2033
litptr_Delete(litptr);
2034
return FALSE;
2035
}
2036
else
2037
vec_SetMax(locvec);
2038
}
2039
} while (!litptr_AllUsed(litptr));
2040
2041
litptr_Delete(litptr);
2042
2043
return TRUE;
2044
}
2045
2046
2047
BOOL subs_IdcEqMatchExcept(CLAUSE c1, int i1, CLAUSE c2, int i2,
2048
SUBST subst)
2049
/**********************************************************
2050
INPUT: Two clauses c1, c2 with the indices of two literals
2051
which need not to be considered and a matcher
2052
RETURNS: TRUE if (<c1>/<i1>)<subst> subsumes (<c2>/<i2>)<subst>
2053
CAUTION:
2054
***********************************************************/
2055
{
2056
int i,vec;
2057
BOOL Result;
2058
2059
/*fputs("\n IdcEQExcept on: \n\t", stdout);
2060
subst_Print(subst); fputs("\n\t", stdout);
2061
clause_Print(c1); printf(" \t\t%d \n\t",i1);
2062
clause_Print(c2); printf(" \t\t%d \n\t",i2);*/
2063
2064
if (clause_Length(c1) == 1)
2065
Result = TRUE;
2066
else {
2067
vec = vec_ActMax();
2068
2069
for (i = 0; i < clause_Length(c1); i++)
2070
if (i != i1)
2071
vec_Push((POINTER) i);
2072
2073
i = 0; /* Doesn't matter, there is a general cont_Reset below */
2074
unify_EstablishMatcher(cont_LeftContext(), subst);
2075
2076
Result = subs_InternIdcEqExcept(c1,vec,c2,i2);
2077
2078
/* printf("Result : %d",Result); */
2079
2080
vec_SetMax(vec);
2081
2082
cont_Reset();
2083
}
2084
2085
return Result;
2086
}
Loggerhead is a web-based interface for Breezy
Version: 2.0.1