← Back to branch summary

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

« back to all changes in this revision

Viewing changes to SPASS/eml.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/eml.h
 
1
/**************************************************************/
 
2
/* ********************************************************** */
 
3
/* *                                                        * */
 
4
/* *              EXTENDED MODAL LOGICS ROUTINES            * */
 
5
/* *                                                        * */
 
6
/* *  $Module:   EML                                        * */ 
 
7
/* *                                                        * */
 
8
/* *                                                        * */
 
9
/* $Revision: 1.3 $                                         * */
 
10
/* $State: Exp $                                            * */
 
11
/* *  This program is free software; you can redistribute   * */
 
12
/* *  it and/or modify it under the terms of the FreeBSD    * */
 
13
/* *  Licence.                                              * */
 
14
/* *                                                        * */
 
15
/* *  This program is distributed in the hope that it will  * */
 
16
/* *  be useful, but WITHOUT ANY WARRANTY; without even     * */
 
17
/* *  the implied warranty of MERCHANTABILITY or FITNESS    * */
 
18
/* *  FOR A PARTICULAR PURPOSE.  See the LICENCE file       * */ 
 
19
/* *  for more details.                                     * */
 
20
/* $Date: 2010-02-22 14:09:58 $                             * */
 
21
/* $Author: weidenb $                                       * */
 
22
/* *                                                        * */
 
23
/* *             Contact:                                   * */
 
24
/* *             Renate Schmidt                             * */
 
25
/* *             School of Computer Science                 * */
 
26
/* *             University of Manchester                   * */
 
27
/* *             Oxford Rd, Manchester M13 9PL, UK          * */
 
28
/* *             Email: Renate.Schmidt@manchester.ac.uk     * */
 
29
/* *                                                        * */
 
30
/* ********************************************************** */
 
31
/**************************************************************/
 
32
 
 
33
 
 
34
/* $RCSfile: eml.h,v $ */
 
35
 
 
36
#ifndef _EMLDFG_
 
37
#define _EMLDFG_
 
38
 
 
39
/**************************************************************/
 
40
/* Includes                                                   */
 
41
/**************************************************************/
 
42
 
 
43
#include "term.h"
 
44
#include "list.h"
 
45
#include "hasharray.h"
 
46
 
 
47
/**************************************************************/
 
48
/* Global Variables and Constants (Only seen by macros)       */
 
49
/**************************************************************/
 
50
 
 
51
extern SYMBOL  eml_APPLYF;
 
52
extern SYMBOL  eml_BOX;
 
53
extern SYMBOL  eml_COMP;
 
54
extern SYMBOL  eml_CONV;
 
55
extern SYMBOL  eml_DIA;
 
56
extern SYMBOL  eml_DIV;
 
57
extern SYMBOL  eml_DOMAIN;
 
58
extern SYMBOL  eml_DOMRESTR;
 
59
extern SYMBOL  eml_ID;
 
60
extern SYMBOL  eml_RANGE;
 
61
extern SYMBOL  eml_RANRESTR;
 
62
extern SYMBOL  eml_SUM;
 
63
extern SYMBOL  eml_TEST;
 
64
 
 
65
typedef enum { eml_PROP,
 
66
               eml_REL,
 
67
               eml_NDE,
 
68
               eml_NARYPROP,
 
69
               eml_NARYNDE,
 
70
               eml_SEMIFNDE, 
 
71
               eml_VARSORT
 
72
} eml_SYMBOLTYPE;
 
73
 
 
74
extern LIST   *eml_PROPINDEXTOFOSYMBOL;
 
75
extern SYMBOL eml_SEMIFNDESYMBOLS[symbol__MAXSIGNATURE];            
 
76
/* Records which nde symbols have been created, for the semi-functional
 
77
 * translation */
 
78
 
 
79
#define eml__MAXMODALDEPTH 100
 
80
 
 
81
extern SYMBOL eml_NARYSYMBOLS[symbol__MAXSIGNATURE][eml__MAXMODALDEPTH];    
 
82
/* Records which symbols of the n-ary signature have been created */
 
83
 
 
84
/**************************************************************/
 
85
/* Access to the first-order symbols.                         */
 
86
/**************************************************************/
 
87
 
 
88
static __inline__ SYMBOL eml_Box(void)
 
89
{
 
90
  return eml_BOX;
 
91
}
 
92
 
 
93
static __inline__ SYMBOL eml_Dia(void)
 
94
{
 
95
  return eml_DIA;
 
96
}
 
97
 
 
98
static __inline__ SYMBOL eml_Domain(void)
 
99
{
 
100
  return eml_DOMAIN;
 
101
}
 
102
 
 
103
static __inline__ SYMBOL eml_Range(void)
 
104
{
 
105
  return eml_RANGE;
 
106
}
 
107
 
 
108
static __inline__ SYMBOL eml_Comp(void)
 
109
{
 
110
  return eml_COMP;
 
111
}
 
112
 
 
113
static __inline__ SYMBOL eml_Sum(void)
 
114
{
 
115
  return eml_SUM;
 
116
}
 
117
 
 
118
static __inline__ SYMBOL eml_Conv(void)
 
119
{
 
120
  return eml_CONV;
 
121
}
 
122
 
 
123
static __inline__ SYMBOL eml_Test(void)
 
124
{
 
125
  return eml_TEST;
 
126
}
 
127
 
 
128
static __inline__ SYMBOL eml_Id(void)
 
129
{
 
130
  return eml_ID;
 
131
}
 
132
 
 
133
static __inline__ SYMBOL eml_Div(void)
 
134
{
 
135
  return eml_DIV;
 
136
}
 
137
 
 
138
static __inline__ SYMBOL eml_DomRestr(void)
 
139
{
 
140
  return eml_DOMRESTR;
 
141
}
 
142
 
 
143
static __inline__ SYMBOL eml_RanRestr(void)
 
144
{
 
145
  return eml_RANRESTR;
 
146
}
 
147
 
 
148
static __inline__ SYMBOL eml_ApplyFunct(void)
 
149
{
 
150
  return eml_APPLYF;
 
151
}
 
152
 
 
153
/**************************************************************/
 
154
/* Symbol identification and access                           */
 
155
/**************************************************************/
 
156
 
 
157
static __inline__ BOOL eml_IsId(TERM S)
 
158
{
 
159
  return symbol_Equal(eml_ID,term_TopSymbol(S));
 
160
}
 
161
 
 
162
static __inline__ BOOL eml_IsDiv(TERM S)
 
163
{
 
164
  return symbol_Equal(eml_DIV,term_TopSymbol(S));
 
165
}
 
166
 
 
167
static __inline__ BOOL eml_IsNotSymbol(SYMBOL S)
 
168
{
 
169
  return symbol_Equal(fol_Not(), S);
 
170
}
 
171
 
 
172
static __inline__ BOOL eml_IsImpliesSymbol(SYMBOL S)
 
173
{
 
174
  return symbol_Equal(fol_Implies(), S);
 
175
}
 
176
 
 
177
static __inline__ BOOL eml_IsImpliedSymbol(SYMBOL S)
 
178
{
 
179
  return symbol_Equal(fol_Implied(), S);
 
180
}
 
181
 
 
182
static __inline__ BOOL eml_IsEquivSymbol(SYMBOL S)
 
183
{
 
184
  return symbol_Equal(fol_Equiv(), S);
 
185
}
 
186
 
 
187
static __inline__ BOOL eml_IsDiaSymbol(SYMBOL S)
 
188
{
 
189
  return (symbol_Equal(eml_DIA,S));
 
190
}
 
191
 
 
192
static __inline__ BOOL eml_IsBoxSymbol(SYMBOL S)
 
193
{
 
194
  return (symbol_Equal(eml_BOX,S));
 
195
}
 
196
 
 
197
static __inline__ BOOL eml_IsModalOpSymbol(SYMBOL S)
 
198
{
 
199
  return (symbol_Equal(eml_BOX,S) || symbol_Equal(eml_DIA,S));
 
200
}
 
201
 
 
202
static __inline__ BOOL eml_IsRelPropSymbol(SYMBOL S)
 
203
{
 
204
  return eml_IsModalOpSymbol(S);
 
205
}
 
206
 
 
207
static __inline__ BOOL eml_IsModalLiteral(TERM T)
 
208
/* unused */
 
209
{
 
210
  return fol_IsLiteral(T) || eml_IsModalOpSymbol(term_TopSymbol(T)) ||
 
211
      (symbol_Equal(term_TopSymbol(T),fol_Not()) && 
 
212
       eml_IsModalOpSymbol(term_TopSymbol(term_FirstArgument(T))));
 
213
}
 
214
 
 
215
 
 
216
static __inline__ BOOL eml_IsPropJunctor(SYMBOL S)
 
217
{
 
218
  return symbol_Equal(S, fol_AND) || 
 
219
      symbol_Equal(S, fol_OR) || 
 
220
      symbol_Equal(S, fol_NOT) || 
 
221
      symbol_Equal(S, fol_IMPLIES) ||
 
222
      symbol_Equal(S, fol_IMPLIED) ||
 
223
      symbol_Equal(S, fol_EQUIV);
 
224
}
 
225
 
 
226
static __inline__ BOOL eml_IsDesignatedPropSymbol(SYMBOL S)
 
227
{
 
228
  return symbol_Equal(S, fol_TRUE) || 
 
229
      symbol_Equal(S, fol_FALSE) || 
 
230
      symbol_Equal(S, eml_ID) || 
 
231
      symbol_Equal(S, eml_DIV);
 
232
}
 
233
 
 
234
static __inline__ BOOL eml_IsNullaryPredicate(SYMBOL S)
 
235
{
 
236
  return symbol_IsPredicate(S) && !eml_IsDesignatedPropSymbol(S) &&
 
237
          (symbol_Arity(S) == 0);
 
238
}
 
239
 
 
240
static __inline__ BOOL eml_IsNaryJunctor(SYMBOL S)
 
241
{
 
242
  return symbol_Equal(S, fol_AND) || 
 
243
      symbol_Equal(S, fol_OR) || 
 
244
      symbol_Equal(S, eml_COMP) || 
 
245
      symbol_Equal(S, eml_SUM);
 
246
}
 
247
 
 
248
static __inline__ BOOL eml_IsRelationalJunctor(SYMBOL S)
 
249
{
 
250
  return eml_IsPropJunctor(S) ||
 
251
      symbol_Equal(S, eml_COMP) || 
 
252
      symbol_Equal(S, eml_CONV) ||
 
253
      symbol_Equal(S, eml_SUM) ||
 
254
      symbol_Equal(S, eml_DOMRESTR) ||
 
255
      symbol_Equal(S, eml_RANRESTR) ||
 
256
      symbol_Equal(S, eml_TEST);
 
257
}
 
258
 
 
259
static __inline__ BOOL eml_IsModalJunctor(SYMBOL S)
 
260
{
 
261
  return eml_IsModalOpSymbol(S) || eml_IsPropJunctor(S);
 
262
}
 
263
 
 
264
static __inline__ BOOL eml_IsPredefinedPred(SYMBOL S)
 
265
{
 
266
  return symbol_Equal(S, eml_DIV) || symbol_Equal(S, eml_ID);
 
267
}
 
268
 
 
269
static __inline__ TERM eml_Atom(TERM Lit)
 
270
{
 
271
  if (term_TopSymbol(Lit) == fol_NOT)
 
272
    return term_FirstArgument(Lit);
 
273
  else
 
274
    return Lit;
 
275
}
 
276
 
 
277
static __inline__ SYMBOL eml_GetDualSymbol(SYMBOL symbol)
 
278
{
 
279
  SYMBOL dual;
 
280
 
 
281
  dual = symbol;
 
282
 
 
283
  if (symbol_Equal(symbol,fol_True()))
 
284
    dual = fol_False();
 
285
  else if (symbol_Equal(symbol,fol_False()))
 
286
    dual = fol_True();
 
287
  else if (symbol_Equal(symbol,fol_Or()))
 
288
    dual = fol_And();
 
289
  else if (symbol_Equal(symbol,fol_And()))
 
290
    dual =  fol_Or();
 
291
  else if (symbol_Equal(symbol,fol_Exist()))
 
292
    dual = fol_All();
 
293
  else if (symbol_Equal(symbol,fol_All()))
 
294
    dual = fol_Exist();
 
295
  else if (symbol_Equal(symbol,eml_Dia()))
 
296
    dual = eml_Box();
 
297
  else if (symbol_Equal(symbol,eml_Box()))
 
298
    dual = eml_Dia();
 
299
  else if (symbol_Equal(symbol,eml_Id()))
 
300
    dual = eml_Div();
 
301
  else if (symbol_Equal(symbol,eml_Div()))
 
302
    dual = eml_Id();
 
303
  else if (symbol_Equal(symbol,eml_Comp()))
 
304
    dual = eml_Sum();
 
305
  else if (symbol_Equal(symbol,eml_Sum()))
 
306
    dual = eml_Comp();
 
307
 
 
308
  return dual;
 
309
}
 
310
 
 
311
/**************************************************************/
 
312
/* Propositional/first order symbol associations              */
 
313
/**************************************************************/
 
314
 
 
315
static __inline__ BOOL eml_VarSortType(eml_SYMBOLTYPE SymbolType)
 
316
{
 
317
  return SymbolType == eml_VARSORT;
 
318
}
 
319
 
 
320
static __inline__ BOOL eml_NaryType(eml_SYMBOLTYPE SymbolType)
 
321
{
 
322
  return SymbolType == eml_NARYPROP || SymbolType == eml_NARYNDE;
 
323
}
 
324
 
 
325
static __inline__ BOOL eml_SemiFuncNdeType(eml_SYMBOLTYPE SymbolType)
 
326
{
 
327
  return SymbolType == eml_SEMIFNDE;
 
328
}
 
329
 
 
330
static __inline__ BOOL eml_RelType(eml_SYMBOLTYPE SymbolType)
 
331
{
 
332
  return SymbolType == eml_REL;
 
333
}
 
334
 
 
335
static __inline__ void eml_SetPropNarySymbolAssocList(SYMBOL PropSymbol, 
 
336
                int Arity, SYMBOL FoSymbol)
 
337
{
 
338
  eml_NARYSYMBOLS[symbol_Index(PropSymbol)][Arity-1] = FoSymbol;
 
339
}
 
340
 
 
341
static __inline__ void eml_SetPropSemiFNdeSymbolAssocList(SYMBOL PropSymbol, 
 
342
                int Arity, SYMBOL FoSymbol)
 
343
{
 
344
  eml_SEMIFNDESYMBOLS[symbol_Index(PropSymbol)] = FoSymbol;
 
345
}
 
346
 
 
347
static __inline__ void eml_SetPropFoSymbolAssocList(SYMBOL PropSymbol, LIST FoSymbols)
 
348
{
 
349
  eml_PROPINDEXTOFOSYMBOL[symbol_Index(PropSymbol)] =  FoSymbols;
 
350
}
 
351
 
 
352
static __inline__ SYMBOL eml_FoQuantAssocWithPropSymbol(SYMBOL PropSymbol)
 
353
{
 
354
  LIST symbolList;
 
355
  symbolList = eml_PROPINDEXTOFOSYMBOL[symbol_Index(PropSymbol)];
 
356
  if (list_Empty(symbolList))
 
357
    return symbol__NULL;
 
358
  else
 
359
    return (SYMBOL) list_First(symbolList);
 
360
}
 
361
 
 
362
static __inline__ SYMBOL eml_FoJunctorAssocWithPropSymbol(SYMBOL PropSymbol)
 
363
{
 
364
  LIST symbolList;
 
365
  symbolList = eml_PROPINDEXTOFOSYMBOL[symbol_Index(PropSymbol)];
 
366
  if (list_Empty(symbolList) || list_Empty(list_Cdr(symbolList)))
 
367
    return symbol__NULL;
 
368
  else
 
369
  return (SYMBOL) list_Second(symbolList);
 
370
}
 
371
 
 
372
/**************************************************************/
 
373
/* Functions                                                  */
 
374
/**************************************************************/
 
375
 
 
376
void eml_Init(PRECEDENCE);
 
377
void eml_Free(void);
 
378
void eml_TranslateToFolMain(LIST*, LIST*, BOOL, FLAGSTORE, PRECEDENCE);
 
379
BOOL eml_FormulaContainsEMLTheorySymbol(TERM);
 
380
 
 
381
#endif