← Back to branch summary

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

« back to all changes in this revision

Viewing changes to SPASS/order.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/order.h
 
1
/**************************************************************/
 
2
/* ********************************************************** */
 
3
/* *                                                        * */
 
4
/* *         INTERFACE FOR ALL ORDERING IMPLEMENTATIONS     * */
 
5
/* *                                                        * */
 
6
/* *  $Module:   ORDER                                      * */ 
 
7
/* *                                                        * */
 
8
/* *  Copyright (C) 1997, 2000, 2001 MPI fuer Informatik    * */
 
9
/* *                                                        * */
 
10
/* *  This program is free software; you can redistribute   * */
 
11
/* *  it and/or modify it under the terms of the FreeBSD    * */
 
12
/* *  Licence.                                              * */
 
13
/* *                                                        * */
 
14
/* *  This program is distributed in the hope that it will  * */
 
15
/* *  be useful, but WITHOUT ANY WARRANTY; without even     * */
 
16
/* *  the implied warranty of MERCHANTABILITY or FITNESS    * */
 
17
/* *  FOR A PARTICULAR PURPOSE.  See the LICENCE file       * */
 
18
/* *  for more details.                                     * */
 
19
/* *                                                        * */
 
20
/* *                                                        * */
 
21
/* $Revision: 1.4 $                                         * */
 
22
/* $State: Exp $                                            * */
 
23
/* $Date: 2010-02-22 14:09:58 $                             * */
 
24
/* $Author: weidenb $                                       * */
 
25
/* *                                                        * */
 
26
/* *             Contact:                                   * */
 
27
/* *             Christoph Weidenbach                       * */
 
28
/* *             MPI fuer Informatik                        * */
 
29
/* *             Stuhlsatzenhausweg 85                      * */
 
30
/* *             66123 Saarbruecken                         * */
 
31
/* *             Email: spass@mpi-inf.mpg.de                * */
 
32
/* *             Germany                                    * */
 
33
/* *                                                        * */
 
34
/* ********************************************************** */
 
35
/**************************************************************/
 
36
 
 
37
 
 
38
/* $RCSfile: order.h,v $ */
 
39
 
 
40
#ifndef _ORDER_
 
41
#define _ORDER_
 
42
 
 
43
/**************************************************************/
 
44
/* Includes                                                   */
 
45
/**************************************************************/
 
46
 
 
47
#include "term.h"
 
48
#include "context.h"
 
49
#include "flags.h"
 
50
#include "symbol.h"
 
51
 
 
52
/**************************************************************/
 
53
/* TYPES and GLOBAL VARIABLES                                 */
 
54
/**************************************************************/
 
55
 
 
56
typedef enum { ord_UNCOMPARABLE,
 
57
               ord_SMALLER_THAN,
 
58
               ord_EQUAL,
 
59
               ord_GREATER_THAN } ord_RESULT;
 
60
 
 
61
/* This array is used to count variable occurrences in two terms. */
 
62
/* It may be used by any available ordering.                     */
 
63
extern NAT ord_VARCOUNT[symbol__MAXSTANDARDVAR][2];
 
64
 
 
65
/* A precedence is needed in almost every ordering function. */
 
66
/* For performance reasons it is stored in a global variable, */
 
67
/* instead of passing it to all those functions, which are   */
 
68
/* often recursive. Nevertheless this variable must not be   */
 
69
/* set externally!                                           */
 
70
extern PRECEDENCE ord_PRECEDENCE;
 
71
 
 
72
/**************************************************************/
 
73
/*  INLINE FUNCTIONS                                          */
 
74
/**************************************************************/
 
75
 
 
76
static __inline__ ord_RESULT ord_Uncomparable(void)
 
77
{
 
78
  return ord_UNCOMPARABLE;
 
79
}
 
80
 
 
81
static __inline__ ord_RESULT ord_Equal(void)
 
82
{
 
83
  return ord_EQUAL;
 
84
}
 
85
 
 
86
static __inline__ ord_RESULT ord_GreaterThan(void)
 
87
{
 
88
  return ord_GREATER_THAN;
 
89
}
 
90
 
 
91
static __inline__ ord_RESULT ord_SmallerThan(void)
 
92
{
 
93
  return ord_SMALLER_THAN;
 
94
}
 
95
 
 
96
static __inline__ BOOL ord_IsGreaterThan(ord_RESULT Res)
 
97
{
 
98
  return ord_GREATER_THAN == Res;
 
99
}
 
100
 
 
101
static __inline__ BOOL ord_IsNotGreaterThan(ord_RESULT Res)
 
102
{
 
103
  return ord_GREATER_THAN != Res;
 
104
}
 
105
 
 
106
static __inline__ BOOL ord_IsSmallerThan(ord_RESULT Res)
 
107
{
 
108
  return ord_SMALLER_THAN == Res;
 
109
}
 
110
 
 
111
static __inline__ BOOL ord_IsNotSmallerThan(ord_RESULT Res)
 
112
{
 
113
  return ord_SMALLER_THAN != Res;
 
114
}
 
115
 
 
116
static __inline__ BOOL ord_IsEqual(ord_RESULT Res)
 
117
{
 
118
  return ord_EQUAL == Res;
 
119
}
 
120
 
 
121
static __inline__ BOOL ord_IsUncomparable(ord_RESULT Res)
 
122
{
 
123
  return ord_UNCOMPARABLE == Res;
 
124
}
 
125
 
 
126
 
 
127
 
 
128
/**************************************************************/
 
129
/*  FUNCTIONS                                                 */
 
130
/**************************************************************/
 
131
 
 
132
ord_RESULT ord_Not(ord_RESULT);
 
133
ord_RESULT ord_CompareAux(TERM, TERM, FLAGSTORE, PRECEDENCE, BOOL);
 
134
ord_RESULT ord_Compare(TERM, TERM, FLAGSTORE, PRECEDENCE);
 
135
ord_RESULT ord_CompareSkolem(TERM, TERM, FLAGSTORE, PRECEDENCE);
 
136
ord_RESULT ord_ContCompare(CONTEXT, TERM, CONTEXT, TERM, FLAGSTORE, PRECEDENCE);
 
137
BOOL       ord_CompareEqual(TERM, TERM, FLAGSTORE);
 
138
BOOL       ord_ContGreater(CONTEXT, TERM, CONTEXT, TERM, FLAGSTORE, PRECEDENCE);
 
139
ord_RESULT ord_LiteralCompare(TERM,BOOL,TERM,BOOL,BOOL, FLAGSTORE, PRECEDENCE);
 
140
void       ord_Print(ord_RESULT);
 
141
ord_RESULT ord_LiteralCompareAux(TERM, BOOL, TERM, BOOL, BOOL, BOOL, FLAGSTORE, PRECEDENCE);
 
142
 
 
143
void ord_CompareCountVars(TERM, int);
 
144
BOOL ord_CompareVarsSubset(TERM, TERM);
 
145
BOOL ord_ContGreaterSkolemSubst(CONTEXT, TERM, CONTEXT, TERM, FLAGSTORE, PRECEDENCE);
 
146
 
 
147
#endif