1
/**************************************************************/
2
/* ********************************************************** */
4
/* * RECURSIVE PATH ORDERING WITH STATUS * */
6
/* * $Module: RPOS * */
8
/* * Copyright (C) 1997, 1998, 1999, 2000, 2001 * */
9
/* * MPI fuer Informatik * */
11
/* * This program is free software; you can redistribute * */
12
/* * it and/or modify it under the terms of the FreeBSD * */
15
/* * This program is distributed in the hope that it will * */
16
/* * be useful, but WITHOUT ANY WARRANTY; without even * */
17
/* * the implied warranty of MERCHANTABILITY or FITNESS * */
18
/* * FOR A PARTICULAR PURPOSE. See the LICENCE file * */
19
/* * for more details. * */
22
/* $Revision: 1.4 $ * */
24
/* $Date: 2010-02-22 14:09:59 $ * */
25
/* $Author: weidenb $ * */
28
/* * Christoph Weidenbach * */
29
/* * MPI fuer Informatik * */
30
/* * Stuhlsatzenhausweg 85 * */
31
/* * 66123 Saarbruecken * */
32
/* * Email: spass@mpi-inf.mpg.de * */
35
/* ********************************************************** */
36
/**************************************************************/
39
/* $RCSfile: rpos.c,v $ */
43
BOOL rpos_ContEqual(CONTEXT, CONTEXT, TERM, CONTEXT, CONTEXT, TERM);
44
ord_RESULT rpos_ContGreaterEqual(CONTEXT, CONTEXT, TERM, CONTEXT, CONTEXT, TERM, BOOL);
46
/**************************************************************/
48
/**************************************************************/
50
BOOL rpos_Greater(TERM T1, TERM T2, BOOL VarIsConst)
52
return ord_IsGreaterThan(rpos_GreaterEqual(T1, T2, VarIsConst));
55
BOOL rpos_ContGreaterAux(CONTEXT GlobalC1, CONTEXT TermC1, TERM T1,
56
CONTEXT GlobalC2, CONTEXT TermC2, TERM T2,
59
return ord_IsGreaterThan(rpos_ContGreaterEqual(GlobalC1, TermC1, T1,
64
BOOL rpos_ContGreater(CONTEXT GlobalC1, CONTEXT TermC1, TERM T1,
65
CONTEXT GlobalC2, CONTEXT TermC2, TERM T2)
67
return ord_IsGreaterThan(rpos_ContGreaterEqual(GlobalC1, TermC1, T1,
72
BOOL rpos_ContGreaterSkolemSubst(CONTEXT GlobalC1, CONTEXT TermC1, TERM T1,
73
CONTEXT GlobalC2, CONTEXT TermC2, TERM T2)
75
return ord_IsGreaterThan(rpos_ContGreaterEqual(GlobalC1, TermC1, T1,
80
/**************************************************************/
81
/* Top Down Version */
82
/**************************************************************/
84
static LIST rpos_MultisetDifference(TERM T1, TERM T2)
85
/**************************************************************
87
RETURNS: The multiset difference between the arguments
88
of both terms with respect to rpos_Equal.
89
***************************************************************/
93
result = list_Copy(term_ArgumentList(T1));
94
result = list_NMultisetDifference(result, term_ArgumentList(T2),
95
(BOOL (*)(POINTER,POINTER)) rpos_Equal);
100
static ord_RESULT rpos_MulGreaterEqual(TERM T1, TERM T2, BOOL VarIsConst)
101
/**************************************************************
102
INPUT: Two terms with equal top symbols and multiset status.
103
RETURNS: ord_GREATER_THAN if <T1> is greater than <T2>,
104
ord_EQUAL if both terms are equal and
105
ord_UNCOMPARABLE otherwise.
106
CAUTION: If <VarIsConst> is set then variables are interpreted as constants
107
with lowest precedence. They are ranked to each other using
108
their variable index.
109
***************************************************************/
113
l1 = rpos_MultisetDifference(T1, T2);
115
/* If |M| = |N| and M-N = {} then N-M = {} */
116
return ord_Equal(); /* Terms are equal */
121
l2 = rpos_MultisetDifference(T2, T1);
123
for (greater = TRUE; !list_Empty(l2) && greater; l2 = list_Pop(l2)) {
124
for (scan = l1, greater = FALSE; !list_Empty(scan) && !greater; scan = list_Cdr(scan))
125
greater = rpos_Greater(list_Car(scan), list_Car(l2), VarIsConst);
127
list_Delete(l1); /* l2 was freed in the outer for loop */
129
return ord_GreaterThan();
131
return ord_Uncomparable();
135
static ord_RESULT rpos_LexGreaterEqual(TERM T1, TERM T2, BOOL VarIsConst)
136
/**************************************************************
137
INPUT: Two terms with equal top symbols and lexicographic status.
138
RETURNS: ord_GREATER_THAN if <T1> is greater than <T2>,
139
ord_EQUAL if both terms are equal and
140
ord_UNCOMPARABLE otherwise.
141
CAUTION: If <VarIsConst> is set then variables are interpreted as constants
142
with lowest precedence. They are ranked to each other using
143
their variable index.
144
***************************************************************/
147
LIST l1, l2, scan1, scan2;
149
if (symbol_HasProperty(term_TopSymbol(T1), ORDRIGHT)) {
150
l1 = list_Reverse(term_ArgumentList(T1)); /* Create new lists */
151
l2 = list_Reverse(term_ArgumentList(T2));
153
l1 = term_ArgumentList(T1);
154
l2 = term_ArgumentList(T2);
156
/* First ignore equal arguments */
157
result = ord_Equal();
158
for (scan1 = l1, scan2 = l2; !list_Empty(scan1);
159
scan1 = list_Cdr(scan1), scan2 = list_Cdr(scan2)) {
160
result = rpos_GreaterEqual(list_Car(scan1), list_Car(scan2), VarIsConst);
161
if (!ord_IsEqual(result))
165
if (ord_IsEqual(result)) /* All arguments are equal, so the terms */
166
/* empty */; /* are equal with respect to RPOS */
167
else if (ord_IsGreaterThan(result)) {
168
/* Check if T1 > each remaining argument of T2 */
169
for (scan2 = list_Cdr(scan2); !list_Empty(scan2) &&
170
rpos_Greater(T1, list_Car(scan2), VarIsConst);
171
scan2 = list_Cdr(scan2)); /* Empty body */
172
if (list_Empty(scan2))
173
result = ord_GreaterThan();
175
result = ord_Uncomparable();
178
/* Argument of T1 was not >= argument of T2. */
180
/* Try to find an argument of T1 that is >= T2 */
181
for (scan1 = list_Cdr(scan1), result = ord_Uncomparable();
182
!list_Empty(scan1) && !ord_IsGreaterThan(result);
183
scan1 = list_Cdr(scan1)) {
184
if (!ord_IsUncomparable(rpos_GreaterEqual(list_Car(scan1), T2, VarIsConst)))
185
result = ord_GreaterThan();
189
if (symbol_HasProperty(term_TopSymbol(T1), ORDRIGHT)) {
190
list_Delete(l1); /* Delete the lists create above */
197
BOOL rpos_Equal(TERM T1, TERM T2)
198
/**************************************************************
200
RETURNS: TRUE, if <T1> is equal to <T2> and
202
***************************************************************/
206
if (!term_EqualTopSymbols(T1, T2))
208
else if (!term_IsComplex(T1)) /* Equal variable or constant */
211
if (symbol_HasProperty(term_TopSymbol(T1), ORDMUL)) { /* MUL case */
212
l1 = rpos_MultisetDifference(T1, T2);
219
} else { /* LEX case */
220
for (l1 = term_ArgumentList(T1), l2 = term_ArgumentList(T2);
221
!list_Empty(l1) && rpos_Equal(list_Car(l1), list_Car(l2));
222
l1 = list_Cdr(l1), l2 = list_Cdr(l2))
224
return list_Empty(l1); /* All arguments were equal */
230
ord_RESULT rpos_GreaterEqual(TERM T1, TERM T2, BOOL VarIsConst)
231
/**************************************************************
233
RETURNS: ord_GREATER_THAN if <T1> is greater than <T2>
234
ord_EQUAL if both terms are equal
235
ord_UNCOMPARABLE otherwise.
236
CAUTION: The precedence from the order module is used to determine
237
the precedence of symbols!
238
If <VarIsConst> is set then variables are interpreted as constants
239
with lowest precedence. They are ranked to each other using
240
their variable index.
241
***************************************************************/
245
if (term_IsVariable(T1)) {
246
if (term_EqualTopSymbols(T1, T2))
247
return ord_Equal(); /* T2 is the same variable */
248
else if(VarIsConst && term_IsVariable(T2)) {
249
if(term_TopSymbol(T1) > term_TopSymbol(T2))
250
return ord_GreaterThan();
252
return ord_Uncomparable();
255
/* A variable can't be greater than another term */
256
return ord_Uncomparable();
257
} else if (!VarIsConst && term_IsVariable(T2)) { /* T1 isn't a variable */
258
if (term_ContainsSymbol(T1, term_TopSymbol(T2)))
259
return ord_GreaterThan();
261
return ord_Uncomparable();
262
} else if(VarIsConst && term_IsVariable(T2)){
263
return ord_GreaterThan();
264
} else if (term_EqualTopSymbols(T1, T2)) {
265
if (symbol_HasProperty(term_TopSymbol(T1), ORDMUL))
266
return rpos_MulGreaterEqual(T1, T2, VarIsConst);
268
return rpos_LexGreaterEqual(T1, T2, VarIsConst);
270
if (symbol_PrecedenceGreater(ord_PRECEDENCE, term_TopSymbol(T1),
271
term_TopSymbol(T2))) {
272
/* Different top symbols, symbol of T1 > symbol of T2. */
273
/* Try if T1 > each argument of T2. */
274
for (scan = term_ArgumentList(T2); !list_Empty(scan); scan = list_Cdr(scan))
275
if (!rpos_Greater(T1, list_Car(scan), VarIsConst))
276
return ord_Uncomparable();
277
return ord_GreaterThan();
279
/* Try to find an argument of T1 that is >= T2 */
280
for (scan = term_ArgumentList(T1); !list_Empty(scan); scan = list_Cdr(scan))
281
if (!ord_IsUncomparable(rpos_GreaterEqual(list_Car(scan), T2, VarIsConst)))
282
return ord_GreaterThan(); /* Argument of T1 >= T2 */
283
return ord_Uncomparable();
288
ord_RESULT rpos_CompareAux(TERM T1, TERM T2, BOOL VarIsConst)
289
/**************************************************************
290
INPUT: Two terms, a boolean flag indicating if variables
291
of <T1> and <T2> are interpreted as skolem constants
292
RETURNS: The relation between the two terms with respect to the
294
ord_GREATER_THAN if <T1> is greater than <T2>,
295
ord_EQUAL if both terms are equal,
296
ord_SMALLER_THAN if <T2> is greater than <T1> and
297
ord_UNCOMPARABLE otherwise.
298
CAUTION: The precedence from the order module is used to determine
299
the precedence of symbols!
300
If <VarIsConst> is set then variables are interpreted as constants
301
with lowest precedence. They are ranked to each other using
302
their variable index.
303
***************************************************************/
307
result = rpos_GreaterEqual(T1, T2, VarIsConst);
308
if (!ord_IsUncomparable(result))
310
else if (rpos_Greater(T2, T1, VarIsConst))
311
return ord_SmallerThan();
313
return ord_UNCOMPARABLE;
316
ord_RESULT rpos_Compare(TERM T1, TERM T2)
317
/**************************************************************
319
RETURNS: The relation between the two terms with respect to the
321
ord_GREATER_THAN if <T1> is greater than <T2>,
322
ord_EQUAL if both terms are equal,
323
ord_SMALLER_THAN if <T2> is greater than <T1> and
324
ord_UNCOMPARABLE otherwise.
325
CAUTION: The precedence from the order module is used to determine
326
the precedence of symbols!
327
***************************************************************/
329
return rpos_CompareAux(T1, T2, FALSE);
332
ord_RESULT rpos_CompareSkolem(TERM T1, TERM T2)
333
/**************************************************************
335
RETURNS: The relation between the two terms with respect to the
337
ord_GREATER_THAN if <T1> is greater than <T2>,
338
ord_EQUAL if both terms are equal,
339
ord_SMALLER_THAN if <T2> is greater than <T1> and
340
ord_UNCOMPARABLE otherwise.
341
CAUTION: The precedence from the order module is used to determine
342
the precedence of symbols! Variables are threated
344
***************************************************************/
346
return rpos_CompareAux(T1, T2, TRUE);
349
/**************************************************************/
350
/* Term comparison with respect to bindings */
351
/**************************************************************/
353
static LIST rpos_ContMultisetDifference(CONTEXT GlobalC1, CONTEXT TermC1, TERM T1,
354
CONTEXT GlobalC2, CONTEXT TermC2, TERM T2)
355
/**************************************************************
356
INPUT: Four contexts and two terms.
357
RETURNS: The multiset difference between the arguments
358
of both terms with respect to rpos_ContEqual.
359
EFFECT: Variable bindings are considered.
360
ASSUMPTION: All index variables of <T1> and <T2> are bound in
361
<GlobalC1> and <GlobalCt2>, respectively
363
***************************************************************/
365
LIST result, scan1, scan2;
367
/* Don't apply bindings at top level, since that happened */
368
/* in rpos_ContGreaterEqual */
370
/* We can't use list_NMultisetDifference, since that function */
371
/* expects an equality functions for terms that takes two terms */
372
/* as arguments. We also need the two contexts resolve variable */
374
result = list_Copy(term_ArgumentList(T1));
375
for (scan2 = term_ArgumentList(T2); !list_Empty(scan2);
376
scan2 = list_Cdr(scan2)) {
377
/* Delete at most one occurrence of the */
378
/* current element of list2 from list1 */
379
for (scan1 = result; !list_Empty(scan1); scan1 = list_Cdr(scan1)) {
380
if (list_Car(scan1) != NULL &&
381
rpos_ContEqual(GlobalC1, TermC1, list_Car(scan1),
382
GlobalC2, TermC2, list_Car(scan2))) {
383
/* arg of list1 wasn't deleted earlier and terms are equal */
384
list_Rplaca(scan1, NULL); /* Mark argument of T1 as deleted */
389
return list_PointerDeleteElement(result, NULL); /* Delete all marked terms */
393
static ord_RESULT rpos_ContMulGreaterEqual(CONTEXT GlobalC1, CONTEXT TermC1, TERM T1,
394
CONTEXT GlobalC2, CONTEXT TermC2, TERM T2,
396
/**************************************************************
397
INPUT: Two contexts and two terms with equal top symbols
399
RETURNS: ord_GREATER_THAN if <T1> is greater than <T2>,
400
ord_EQUAL if both terms are equal and
401
ord_UNCOMPARABLE otherwise.
402
EFFECT: Variable bindings are considered.
403
ASSUMPTION: All index variables of <T1> and <T2> are bound in
404
<GlobalC1> and <GlobalCt2>, respectively
405
***************************************************************/
409
/* Don't apply bindings at top level, since that happened */
410
/* in rpos_ContGreaterEqual. */
412
l1 = rpos_ContMultisetDifference(GlobalC1, TermC1, T1, GlobalC2, TermC2, T2);
414
/* If |M| = |N| and M-N = {} then N-M = {} */
415
return ord_Equal(); /* Terms are equal */
420
l2 = rpos_ContMultisetDifference(GlobalC2, TermC2, T2, GlobalC1, TermC1, T1);
422
for (greater = TRUE; !list_Empty(l2) && greater; l2 = list_Pop(l2)) {
423
for (scan = l1, greater = FALSE; !list_Empty(scan) && !greater;
424
scan = list_Cdr(scan))
425
greater = rpos_ContGreaterAux(GlobalC1, TermC1, list_Car(scan),
426
GlobalC2, TermC2, list_Car(l2),
429
list_Delete(l1); /* l2 was freed in the outer for loop */
431
return ord_GreaterThan();
433
return ord_Uncomparable();
437
static ord_RESULT rpos_ContLexGreaterEqual(CONTEXT GlobalC1, CONTEXT TermC1, TERM T1,
438
CONTEXT GlobalC2, CONTEXT TermC2, TERM T2,
440
/**************************************************************
441
INPUT: Two contexts and two terms with equal top symbols
442
and lexicographic status and a flag.
443
RETURNS: ord_GREATER_THAN if <T1> is greater than <T2>,
444
ord_EQUAL if both terms are equal and
445
ord_UNCOMPARABLE otherwise.
446
EFFECT: Variable bindings are considered.
447
ASSUMPTION: All index variables of <T1> and <T2> are bound in
448
<GlobalC1> and <GlobalCt2>, respectively
449
CAUTION: If <VarIsConst> is set then variables are interpreted as constants
450
with lowest precedence. They are ranked to each other using
451
their variable index.
452
***************************************************************/
455
LIST l1, l2, scan1, scan2;
457
/* Don't apply bindings at top level, since that happened */
458
/* in rpos_ContGreaterEqual */
460
if (symbol_HasProperty(term_TopSymbol(T1), ORDRIGHT)) {
461
l1 = list_Reverse(term_ArgumentList(T1)); /* Create new lists */
462
l2 = list_Reverse(term_ArgumentList(T2));
464
l1 = term_ArgumentList(T1);
465
l2 = term_ArgumentList(T2);
467
/* First ignore equal arguments */
468
result = ord_Equal();
469
for (scan1 = l1, scan2 = l2; !list_Empty(scan1);
470
scan1 = list_Cdr(scan1), scan2 = list_Cdr(scan2)) {
471
result = rpos_ContGreaterEqual(GlobalC1, TermC1, list_Car(scan1),
472
GlobalC2, TermC2, list_Car(scan2),
474
if (!ord_IsEqual(result))
478
if (ord_IsEqual(result)) /* All arguments are equal, so the terms */
479
/* empty */; /* are equal with respect to RPOS */
480
else if (ord_IsGreaterThan(result)) {
481
/* Check if T1 > each remaining argument of T2 */
482
for (scan2 = list_Cdr(scan2);
483
!list_Empty(scan2) && rpos_ContGreaterAux(GlobalC1, TermC1, T1,
484
GlobalC2, TermC2, list_Car(scan2),
486
scan2 = list_Cdr(scan2)); /* Empty body */
487
if (list_Empty(scan2))
488
result = ord_GreaterThan();
490
result = ord_Uncomparable();
493
/* Argument of T1 was not >= argument of T2. */
494
/* Try to find an argument of T1 that is >= T2 */
495
for (scan1 = list_Cdr(scan1), result = ord_Uncomparable();
496
!list_Empty(scan1) && !ord_IsGreaterThan(result);
497
scan1 = list_Cdr(scan1)) {
498
if (!ord_IsUncomparable(rpos_ContGreaterEqual(GlobalC1, TermC1,list_Car(scan1),
501
result = ord_GreaterThan();
505
if (symbol_HasProperty(term_TopSymbol(T1), ORDRIGHT)) {
506
list_Delete(l1); /* Delete the lists create above */
513
BOOL rpos_ContEqual(CONTEXT GlobalC1, CONTEXT TermC1, TERM T1,
514
CONTEXT GlobalC2, CONTEXT TermC2, TERM T2)
515
/**************************************************************
516
INPUT: Two contexts and two terms.
517
RETURNS: TRUE, if <T1> is equal to <T2> and
519
EFFECT: Variable bindings are considered.
520
ASSUMPTION: All index variables of <T1> and <T2> are bound in
521
<GlobalC1> and <GlobalCt2>, respectively
522
***************************************************************/
526
T1 = cont_Deref(GlobalC1, &TermC1, T1);
527
T2 = cont_Deref(GlobalC2, &TermC2, T2);
529
if (!term_EqualTopSymbols(T1, T2))
531
else if (!term_IsComplex(T1))
534
if (symbol_HasProperty(term_TopSymbol(T1), ORDMUL)) {
535
l1 = rpos_ContMultisetDifference(GlobalC1, TermC1, T1,
536
GlobalC2, TermC2, T2);
543
} else { /* LEX case */
544
for (l1 = term_ArgumentList(T1), l2 = term_ArgumentList(T2);
545
!list_Empty(l1) && rpos_ContEqual(GlobalC1, TermC1,list_Car(l1),
546
GlobalC2, TermC2,list_Car(l2));
547
l1 = list_Cdr(l1), l2 = list_Cdr(l2)); /* empty body */
548
return list_Empty(l1); /* All arguments were equal */
554
ord_RESULT rpos_ContGreaterEqual(CONTEXT GlobalC1, CONTEXT TermC1, TERM T1,
555
CONTEXT GlobalC2, CONTEXT TermC2, TERM T2,
557
/**************************************************************
558
INPUT: Two contexts and two terms.
559
RETURNS: ord_GREATER_THAN if <T1> is greater than <T2>
560
ord_EQUAL if both terms are equal
561
ord_UNCOMPARABLE otherwise.
562
EFFECT: Variable bindings are considered.
563
CAUTION: The precedence from the order module is used to determine
564
the precedence of symbols!
565
If <VarIsConst> is set then variables are interpreted as constants
566
with lowest precedence. They are ranked to each other using
567
their variable index.
568
ASSUMPTION: All index variables of <T1> and <T2> are bound in
569
<GlobalC1> and <GlobalCt2>, respectively
570
***************************************************************/
574
T1 = cont_Deref(GlobalC1, &TermC1, T1);
575
T2 = cont_Deref(GlobalC2, &TermC2, T2);
577
if (term_IsVariable(T1)) {
578
if (term_EqualTopSymbols(T1, T2))
579
return ord_Equal(); /* T2 is the same variable */
581
/* A variable can't be greater than another term */
582
return ord_Uncomparable();
583
} else if (term_IsVariable(T2)) { /* T1 isn't a variable */
584
if (cont_TermContainsSymbol(GlobalC1, TermC1, T1, term_TopSymbol(T2)))
585
return ord_GreaterThan();
587
return ord_Uncomparable();
588
} else if (term_EqualTopSymbols(T1, T2)) {
589
if (symbol_HasProperty(term_TopSymbol(T1), ORDMUL))
590
return rpos_ContMulGreaterEqual(GlobalC1, TermC1, T1,
591
GlobalC2, TermC2, T2, VarIsConst);
593
return rpos_ContLexGreaterEqual(GlobalC1, TermC1, T1,
594
GlobalC2, TermC2, T2, VarIsConst);
596
if (symbol_PrecedenceGreater(ord_PRECEDENCE, term_TopSymbol(T1),
597
term_TopSymbol(T2))) {
598
/* Different top symbols, symbol of T1 > symbol of T2. */
599
/* Try if T1 > each argument of T2. */
600
for (scan = term_ArgumentList(T2); !list_Empty(scan); scan = list_Cdr(scan))
601
if (!rpos_ContGreaterAux(GlobalC1, TermC1, T1,
602
GlobalC2, TermC2, list_Car(scan), VarIsConst))
603
return ord_Uncomparable();
604
return ord_GreaterThan();
606
/* Try to find an argument of T1 that is >= T2 */
607
for (scan = term_ArgumentList(T1); !list_Empty(scan); scan = list_Cdr(scan))
608
if (!ord_IsUncomparable(rpos_ContGreaterEqual(GlobalC1, TermC1,list_Car(scan),
611
return ord_GreaterThan(); /* Argument of T1 >= T2 */
612
return ord_Uncomparable();
617
ord_RESULT rpos_ContCompareAux(CONTEXT C1, TERM T1, CONTEXT C2, TERM T2, BOOL VarIsConst)
618
/**************************************************************
619
INPUT: Two contexts and two terms.
620
RETURNS: The relation between the two terms with respect to the
622
ord_GREATER_THAN if <T1> is greater than <T2>,
623
ord_EQUAL if both terms are equal,
624
ord_SMALLER_THAN if <T2> is greater than <T1> and
625
ord_UNCOMPARABLE otherwise.
626
EFFECT: Variable bindings are considered.
627
If VarIsConst is true variables are interpreted as constants
628
CAUTION: The precedence from the order module is used to determine
629
the precedence of symbols!
630
If <VarIsConst> is set then variables are interpreted as constants
631
with lowest precedence. They are ranked to each other using
632
their variable index.
633
***************************************************************/
636
CONTEXT GlobalC1, GlobalC2;
641
T1 = cont_Deref(GlobalC1, &C1, T1);
642
T2 = cont_Deref(GlobalC2, &C2, T2);
644
result = rpos_ContGreaterEqual(GlobalC1, C1, T1, GlobalC2, C2, T2, VarIsConst);
645
if (!ord_IsUncomparable(result))
647
else if (rpos_ContGreaterAux(GlobalC2, C2, T2, GlobalC1, C1, T1, VarIsConst))
648
return ord_SmallerThan();
650
return ord_UNCOMPARABLE;
653
ord_RESULT rpos_ContCompare(CONTEXT C1, TERM T1, CONTEXT C2, TERM T2)
654
/**************************************************************
655
INPUT: Two contexts, two terms and a flag
656
RETURNS: The relation between the two terms with respect to the
658
ord_GREATER_THAN if <T1> is greater than <T2>,
659
ord_EQUAL if both terms are equal,
660
ord_SMALLER_THAN if <T2> is greater than <T1> and
661
ord_UNCOMPARABLE otherwise.
662
EFFECT: Variable bindings are considered.
663
CAUTION: The precedence from the order module is used to determine
664
the precedence of symbols!
665
***************************************************************/
667
return rpos_ContCompareAux(C1, T1, C2, T2, FALSE);
added
removed
SPASS/rpos.c
