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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
|
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * INTERFACE FOR ALL ORDERING IMPLEMENTATIONS * */
/* * * */
/* * $Module: ORDER * */
/* * * */
/* * Copyright (C) 1997, 2000, 2001 MPI fuer Informatik * */
/* * * */
/* * This program is free software; you can redistribute * */
/* * it and/or modify it under the terms of the FreeBSD * */
/* * Licence. * */
/* * * */
/* * This program is distributed in the hope that it will * */
/* * be useful, but WITHOUT ANY WARRANTY; without even * */
/* * the implied warranty of MERCHANTABILITY or FITNESS * */
/* * FOR A PARTICULAR PURPOSE. See the LICENCE file * */
/* * for more details. * */
/* * * */
/* * * */
/* $Revision: 1.4 $ * */
/* $State: Exp $ * */
/* $Date: 2010-02-22 14:09:58 $ * */
/* $Author: weidenb $ * */
/* * * */
/* * Contact: * */
/* * Christoph Weidenbach * */
/* * MPI fuer Informatik * */
/* * Stuhlsatzenhausweg 85 * */
/* * 66123 Saarbruecken * */
/* * Email: spass@mpi-inf.mpg.de * */
/* * Germany * */
/* * * */
/* ********************************************************** */
/**************************************************************/
/* $RCSfile: order.h,v $ */
#ifndef _ORDER_
#define _ORDER_
/**************************************************************/
/* Includes */
/**************************************************************/
#include "term.h"
#include "context.h"
#include "flags.h"
#include "symbol.h"
/**************************************************************/
/* TYPES and GLOBAL VARIABLES */
/**************************************************************/
typedef enum { ord_UNCOMPARABLE,
ord_SMALLER_THAN,
ord_EQUAL,
ord_GREATER_THAN } ord_RESULT;
/* This array is used to count variable occurrences in two terms. */
/* It may be used by any available ordering. */
extern NAT ord_VARCOUNT[symbol__MAXSTANDARDVAR][2];
/* A precedence is needed in almost every ordering function. */
/* For performance reasons it is stored in a global variable, */
/* instead of passing it to all those functions, which are */
/* often recursive. Nevertheless this variable must not be */
/* set externally! */
extern PRECEDENCE ord_PRECEDENCE;
/**************************************************************/
/* INLINE FUNCTIONS */
/**************************************************************/
static __inline__ ord_RESULT ord_Uncomparable(void)
{
return ord_UNCOMPARABLE;
}
static __inline__ ord_RESULT ord_Equal(void)
{
return ord_EQUAL;
}
static __inline__ ord_RESULT ord_GreaterThan(void)
{
return ord_GREATER_THAN;
}
static __inline__ ord_RESULT ord_SmallerThan(void)
{
return ord_SMALLER_THAN;
}
static __inline__ BOOL ord_IsGreaterThan(ord_RESULT Res)
{
return ord_GREATER_THAN == Res;
}
static __inline__ BOOL ord_IsNotGreaterThan(ord_RESULT Res)
{
return ord_GREATER_THAN != Res;
}
static __inline__ BOOL ord_IsSmallerThan(ord_RESULT Res)
{
return ord_SMALLER_THAN == Res;
}
static __inline__ BOOL ord_IsNotSmallerThan(ord_RESULT Res)
{
return ord_SMALLER_THAN != Res;
}
static __inline__ BOOL ord_IsEqual(ord_RESULT Res)
{
return ord_EQUAL == Res;
}
static __inline__ BOOL ord_IsUncomparable(ord_RESULT Res)
{
return ord_UNCOMPARABLE == Res;
}
/**************************************************************/
/* FUNCTIONS */
/**************************************************************/
ord_RESULT ord_Not(ord_RESULT);
ord_RESULT ord_CompareAux(TERM, TERM, FLAGSTORE, PRECEDENCE, BOOL);
ord_RESULT ord_Compare(TERM, TERM, FLAGSTORE, PRECEDENCE);
ord_RESULT ord_CompareSkolem(TERM, TERM, FLAGSTORE, PRECEDENCE);
ord_RESULT ord_ContCompare(CONTEXT, TERM, CONTEXT, TERM, FLAGSTORE, PRECEDENCE);
BOOL ord_CompareEqual(TERM, TERM, FLAGSTORE);
BOOL ord_ContGreater(CONTEXT, TERM, CONTEXT, TERM, FLAGSTORE, PRECEDENCE);
ord_RESULT ord_LiteralCompare(TERM,BOOL,TERM,BOOL,BOOL, FLAGSTORE, PRECEDENCE);
void ord_Print(ord_RESULT);
ord_RESULT ord_LiteralCompareAux(TERM, BOOL, TERM, BOOL, BOOL, BOOL, FLAGSTORE, PRECEDENCE);
void ord_CompareCountVars(TERM, int);
BOOL ord_CompareVarsSubset(TERM, TERM);
BOOL ord_ContGreaterSkolemSubst(CONTEXT, TERM, CONTEXT, TERM, FLAGSTORE, PRECEDENCE);
#endif
|
