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
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
|
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * FIRST ORDER LOGIC SYMBOLS * */
/* * * */
/* * $Module: FOL DFG * */
/* * * */
/* * Copyright (C) 1996, 1997, 1998, 1999, 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 _FOLDFG_
#define _FOLDFG_
/**************************************************************/
/* Includes */
/**************************************************************/
#include "flags.h"
#include "unify.h"
#include "context.h"
#include "term.h"
/**************************************************************/
/* Global Variables and Constants (Only seen by macros) */
/**************************************************************/
extern SYMBOL fol_ALL;
extern SYMBOL fol_EXIST;
extern SYMBOL fol_AND;
extern SYMBOL fol_OR;
extern SYMBOL fol_NOT;
extern SYMBOL fol_IMPLIES;
extern SYMBOL fol_IMPLIED;
extern SYMBOL fol_EQUIV;
extern SYMBOL fol_VARLIST;
extern SYMBOL fol_EQUALITY;
extern SYMBOL fol_TRUE;
extern SYMBOL fol_FALSE;
/**************************************************************/
/* Access to the first-order symbols. */
/**************************************************************/
static __inline__ SYMBOL fol_All(void)
{
return fol_ALL;
}
static __inline__ SYMBOL fol_Exist(void)
{
return fol_EXIST;
}
static __inline__ SYMBOL fol_And(void)
{
return fol_AND;
}
static __inline__ SYMBOL fol_Or(void)
{
return fol_OR;
}
static __inline__ SYMBOL fol_Not(void)
{
return fol_NOT;
}
static __inline__ SYMBOL fol_Implies(void)
{
return fol_IMPLIES;
}
static __inline__ SYMBOL fol_Implied(void)
{
return fol_IMPLIED;
}
static __inline__ SYMBOL fol_Equiv(void)
{
return fol_EQUIV;
}
static __inline__ SYMBOL fol_Varlist(void)
{
return fol_VARLIST;
}
static __inline__ SYMBOL fol_Equality(void)
{
return fol_EQUALITY;
}
static __inline__ SYMBOL fol_True(void)
{
return fol_TRUE;
}
static __inline__ SYMBOL fol_False(void)
{
return fol_FALSE;
}
/**************************************************************/
/* Macros */
/**************************************************************/
static __inline__ BOOL fol_IsQuantifier(SYMBOL S)
{
return symbol_Equal(fol_ALL,S) || symbol_Equal(fol_EXIST,S);
}
static __inline__ BOOL fol_IsTrue(TERM S)
{
return symbol_Equal(fol_TRUE,term_TopSymbol(S));
}
static __inline__ BOOL fol_IsFalse(TERM S)
{
return symbol_Equal(fol_FALSE,term_TopSymbol(S));
}
static __inline__ LIST fol_QuantifierVariables(TERM T)
/* T's top symbol must be a quantifier ! */
{
return term_ArgumentList(term_FirstArgument(T));
}
static __inline__ BOOL fol_IsLiteral(TERM T)
{
return symbol_IsPredicate(term_TopSymbol(T)) ||
(symbol_Equal(term_TopSymbol(T),fol_Not()) &&
symbol_IsPredicate(term_TopSymbol(term_FirstArgument(T))));
}
static __inline__ BOOL fol_IsNegativeLiteral(TERM T)
{
return (symbol_Equal(term_TopSymbol(T),fol_Not()) &&
symbol_IsPredicate(term_TopSymbol(term_FirstArgument(T))));
}
static __inline__ BOOL fol_IsJunctor(SYMBOL S)
{
return fol_IsQuantifier(S) || symbol_Equal(S, fol_AND) ||
symbol_Equal(S, fol_OR) || symbol_Equal(S, fol_NOT) ||
symbol_Equal(S, fol_IMPLIED) || symbol_Equal(S, fol_VARLIST) ||
symbol_Equal(S, fol_IMPLIES) || symbol_Equal(S, fol_EQUIV);
}
static __inline__ BOOL fol_IsPredefinedPred(SYMBOL S)
{
return symbol_Equal(S, fol_EQUALITY) || symbol_Equal(S, fol_TRUE) ||
symbol_Equal(S, fol_FALSE);
}
static __inline__ TERM fol_Atom(TERM Lit)
{
if (term_TopSymbol(Lit) == fol_NOT)
return term_FirstArgument(Lit);
else
return Lit;
}
static __inline__ BOOL fol_IsEquality(TERM Term)
{
return term_TopSymbol(Term) == fol_EQUALITY;
}
static __inline__ BOOL fol_IsAssignment(TERM Term)
{
return (term_TopSymbol(Term) == fol_EQUALITY &&
((term_IsVariable(term_FirstArgument(Term)) &&
!term_ContainsVariable(term_SecondArgument(Term),
term_TopSymbol(term_FirstArgument(Term)))) ||
(term_IsVariable(term_SecondArgument(Term)) &&
!term_ContainsVariable(term_FirstArgument(Term),
term_TopSymbol(term_SecondArgument(Term))))));
}
static __inline__ LIST fol_DeleteFalseTermFromList(LIST List)
/**************************************************************
INPUT: A list of terms.
RETURNS: The list where all terms equal to the 'False' term are removed.
EFFECTS: 'False' is a special predicate from the fol module.
Terms are compared with respect to the term_Equal function.
The terms are deleted, too.
***************************************************************/
{
return list_DeleteElementIfFree(List, (BOOL (*)(POINTER))fol_IsFalse,
(void (*)(POINTER))term_Delete);
}
static __inline__ LIST fol_DeleteTrueTermFromList(LIST List)
/**************************************************************
INPUT: A list of terms.
RETURNS: The list where all terms equal to the 'True' term are removed.
EFFECTS: 'True' is a special predicate from the fol module.
Terms are compared with respect to the term_Equal function.
The terms are deleted, too.
***************************************************************/
{
return list_DeleteElementIfFree(List, (BOOL (*)(POINTER))fol_IsTrue,
(void (*)(POINTER))term_Delete);
}
/**************************************************************/
/* Functions */
/**************************************************************/
void fol_Init(BOOL, PRECEDENCE);
SYMBOL fol_IsStringPredefined(const char*);
TERM fol_CreateQuantifier(SYMBOL, LIST, LIST);
TERM fol_CreateQuantifierAddFather(SYMBOL, LIST, LIST);
LIST fol_GetNonFOLPredicates(void);
TERM fol_ComplementaryTerm(TERM);
LIST fol_GetAssignments(TERM);
void fol_Free(void);
void fol_CheckFatherLinks(TERM);
BOOL fol_FormulaIsClause(TERM);
void fol_FPrintOtterOptions(FILE*, BOOL, FLAG_TDFG2OTTEROPTIONSTYPE);
void fol_FPrintOtter(FILE*, LIST, FLAG_TDFG2OTTEROPTIONSTYPE);
void fol_FPrintDFGSignature(FILE*);
void fol_PrettyPrintDFG(TERM);
void fol_PrintDFG(TERM);
void fol_FPrintDFG(FILE*, TERM);
void fol_FPrintDFGProblem(FILE*, const char*, const char*, const char*, const char*, LIST, LIST);
void fol_PrintPrecedence(PRECEDENCE);
void fol_FPrintPrecedence(FILE*, PRECEDENCE);
LIST fol_Instances(TERM, TERM);
LIST fol_Generalizations(TERM, TERM);
TERM fol_MostGeneralFormula(LIST);
void fol_NormalizeVars(TERM);
void fol_NormalizeVarsStartingAt(TERM, SYMBOL);
LIST fol_FreeVariables(TERM);
LIST fol_BoundVariables(TERM);
BOOL fol_VarOccursFreely(TERM,TERM);
BOOL fol_AssocEquation(TERM, SYMBOL *);
BOOL fol_DistributiveEquation(TERM, SYMBOL*, SYMBOL*);
void fol_ReplaceVariable(TERM, SYMBOL, TERM);
void fol_PrettyPrint(TERM);
LIST fol_GetSubstEquations(TERM);
TERM fol_GetBindingQuantifier(TERM, SYMBOL);
int fol_TermPolarity(TERM, TERM);
BOOL fol_PolarCheck(TERM, TERM);
void fol_PopQuantifier(TERM);
void fol_DeleteQuantifierVariable(TERM,SYMBOL);
void fol_SetTrue(TERM);
void fol_SetFalse(TERM);
void fol_RemoveImplied(TERM);
BOOL fol_PropagateFreeness(TERM);
BOOL fol_PropagateWitness(TERM);
BOOL fol_PropagateTautologies(TERM);
BOOL fol_AlphaEqual(TERM, TERM);
BOOL fol_VarBoundTwice(TERM);
NAT fol_Depth(TERM);
BOOL fol_ApplyContextToTerm(CONTEXT, TERM);
BOOL fol_CheckFormula(TERM);
BOOL fol_SignatureMatchFormula(TERM, TERM, BOOL);
BOOL fol_SignatureMatch(TERM, TERM, LIST*, BOOL);
#endif
|
