1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
/*-----------------------------------------------------------------------
File : clb_partial_orderings.h
Author: Stephan Schulz
Contents
Functions and datatypes useful in dealing with partial orderings.
Copyright 1998, 1999 by the author.
This code is released under the GNU General Public Licence and
the GNU Lesser General Public License.
See the file COPYING in the main E directory for details..
Run "eprover -h" for contact information.
Changes
<1> Wed Jun 16 22:37:09 MET DST 1999
New
-----------------------------------------------------------------------*/
#ifndef CLB_PARTIAL_ORDERINGS
#define CLB_PARTIAL_ORDERINGS
#include <clb_defines.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
/* Possible results of partial ordering comparisons */
typedef enum
{
to_unknown = 0,
to_uncomparable = 1,
to_equal = 2,
to_greater = 3,
to_lesser = 4,
to_notgteq, /* For caching partial LPO results */
to_notleeq
}CompareResult;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
extern char* POCompareSymbol[];
/* Translating standard UNIX total Quasi-Ordering comparions into
CompareResult: */
#define Q_TO_PART(res) (((res)<0) ? to_lesser:\
(((res)>0) ? to_greater:to_equal))
static inline CompareResult POInverseRelation(CompareResult
relation);
/*---------------------------------------------------------------------*/
/* Implementations as inline functions */
/*---------------------------------------------------------------------*/
/*-----------------------------------------------------------------------
//
// Function: POInverseRelation()
//
// Given a comparison relation, return the inverse relation.
//
// Global Variables: -
//
// Side Effects : -
//
/----------------------------------------------------------------------*/
static inline CompareResult POInverseRelation(CompareResult
relation)
{
CompareResult res = relation;
switch(relation)
{
case to_equal:
case to_uncomparable:
break;
case to_greater:
res = to_lesser;
break;
case to_lesser:
res = to_greater;
break;
case to_notgteq:
res = to_notleeq;
break;
case to_notleeq:
res = to_notgteq;
break;
default:
assert(false);
break;
}
return res;
}
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
