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
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
|
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * RENAMING * */
/* * * */
/* * $Module: REN * */
/* * * */
/* * Copyright (C) 1996, 1997, 1998, 2000, 2001 * */
/* * MPI fuer Informatik * */
/* * * */
/* * This program is free software; you can redistribute * */
/* * it and/or modify it under the terms of the GNU * */
/* * General Public License as published by the Free * */
/* * Software Foundation; either version 2 of the License, * */
/* * or (at your option) any later version. * */
/* * * */
/* * 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 GNU General Public * */
/* * License for more details. * */
/* * * */
/* * You should have received a copy of the GNU General * */
/* * Public License along with this program; if not, write * */
/* * to the Free Software Foundation, Inc., 59 Temple * */
/* * Place, Suite 330, Boston, MA 02111-1307 USA * */
/* * * */
/* * * */
/* $Revision: 21527 $ * */
/* $State$ * */
/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $ * */
/* $Author: duraid $ * */
/* * * */
/* * Contact: * */
/* * Christoph Weidenbach * */
/* * MPI fuer Informatik * */
/* * Stuhlsatzenhausweg 85 * */
/* * 66123 Saarbruecken * */
/* * Email: weidenb@mpi-sb.mpg.de * */
/* * Germany * */
/* * * */
/* ********************************************************** */
/**************************************************************/
/* $RCSfile$ */
#ifndef _SPASS_RENAMING_
#define _SPASS_RENAMING_
/**************************************************************/
/* Includes */
/**************************************************************/
#include "misc.h"
#include "foldfg.h"
#include "unify.h"
#include "vector.h"
/**************************************************************/
/* Data Structures and Constants */
/**************************************************************/
typedef struct {
TERM hit;
LIST matches;
BOOL general;
int polarity;
} *RENAMING, RENAMING_NODE;
/* <hit> is the formula that has a positive benefit */
/* <matches> are further matches of <hit> in the overall formula */
/* <general> is TRUE iff the <hit> formula must not be replaced but */
/* is a generalzation of the matches formulae that are to */
/* be replaced */
/* <polarity> is the most general polarity of <hit> and all <matches> */
/**************************************************************/
/* Functions */
/**************************************************************/
static __inline__ int ren_OverallPolarity(RENAMING ren)
{
return ren->polarity;
}
static __inline__ TERM ren_Hit(RENAMING ren)
{
return ren->hit;
}
static __inline__ LIST ren_Matches(RENAMING ren)
{
return ren->matches;
}
static __inline__ BOOL ren_General(RENAMING ren)
{
return ren->general;
}
static __inline__ void ren_SetMatches(RENAMING ren, LIST matches)
{
ren->matches = matches;
}
static __inline__ void ren_SetHit(RENAMING ren, TERM hit)
{
ren->hit = hit;
}
static __inline__ void ren_SetOverallPolarity(RENAMING ren, int polarity)
{
ren->polarity = polarity;
}
static __inline__ void ren_SetGeneral(RENAMING ren, BOOL general)
{
ren->general = general;
}
static __inline__ RENAMING ren_Create(TERM hit, LIST matches, int polarity)
/**************************************************************
INPUT: A formula, a list of further matching formulae
and the overall polarity of the <hit> and the further <matches>.
RETURNS: A new renaming object, which is initialized.
General is set to false.
MEMORY: Allocates memory for the RENAMING.
***************************************************************/
{
RENAMING Result;
Result = (RENAMING)memory_Malloc(sizeof(RENAMING_NODE));
Result->hit = hit;
Result->matches = matches;
Result->polarity = polarity;
Result->general = FALSE;
return Result;
}
static __inline__ void ren_Delete(RENAMING ren)
/**************************************************************
INPUT: A renaming.
RETURNS: void.
MEMORY: Frees memory for the RENAMING and the matches list.
Formulae are not deleted.
***************************************************************/
{
list_Delete(ren->matches);
memory_Free(ren,sizeof(RENAMING_NODE));
}
/**************************************************************/
/* Function Prototypes */
/**************************************************************/
void ren_Init(void);
TERM ren_Rename(TERM, PRECEDENCE, LIST*,BOOL, BOOL);
void ren_PrettyPrint(RENAMING);
#endif
|
