← Back to branch summary

~ubuntu-branches/ubuntu/trusty/spass/trusty

« back to all changes in this revision

Viewing changes to SPASS/tptp2dfg.c

  • 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/tptp2dfg.c
 
1
/**************************************************************/
 
2
/* ********************************************************** */
 
3
/* *                                                        * */
 
4
/* *              TPTP2DFG                                  * */
 
5
/* *                                                        * */
 
6
/* ********************************************************** */
 
7
/**************************************************************/
 
8
 
 
9
 
 
10
/**************************************************************/
 
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
/* Includes                                                   */
 
21
/**************************************************************/
 
22
 
 
23
#include "memory.h"
 
24
#include "term.h"
 
25
#include "clause.h"
 
26
#include "foldfg.h"
 
27
#include "symbol.h"
 
28
#include "cmdline.h"
 
29
 
 
30
#include "tptp.h"
 
31
 
 
32
#define TPTP2DFG__VERSION "0.1"
 
33
 
 
34
/*-----------------------------------------------------------------------------*/
 
35
 
 
36
static void tptp_FPrintDFGProblem(FILE*, DFGDESCRIPTION, LIST, LIST, LIST, LIST, LIST, BOOL);
 
37
 
 
38
/*-----------------------------------------------------------------------------*/
 
39
 
 
40
static void tptp_DeleteStrListOfStrPair(POINTER pair) {
 
41
  string_StringFree((char *)list_PairFirst(pair));
 
42
  list_DeleteWithElement(list_PairSecond(pair),(void (*)(POINTER))string_StringFree);  
 
43
  list_PairFree(pair);
 
44
}
 
45
 
 
46
/*-----------------------------------------------------------------------------*/
 
47
 
 
48
int main(int argc, const char* argv[]) {
 
49
 
 
50
  LIST Clauses, Axioms, Conjectures, SortDecls, UserDefinedPrecedence, UserDefinedSelection, ClAxRelation, Includes;
 
51
  PRECEDENCE Precedence;
 
52
  FLAGSTORE  Flags;
 
53
  DFGDESCRIPTION Description;
 
54
  FILE* InFile;
 
55
  FILE* OutFile;
 
56
  BOOL Dummy;
 
57
 
 
58
  /*Set up modules*/
 
59
  
 
60
  memory_Init(memory__UNLIMITED);
 
61
  symbol_Init(TRUE);
 
62
  stack_Init();
 
63
  flag_Init(flag_SPASS);
 
64
  flag_Init(flag_TPTP2DFG);   /* declare include flag */
 
65
  tptp_Init();
 
66
 
 
67
  Flags = flag_CreateStore();
 
68
  flag_InitStoreByDefaults(Flags);
 
69
 
 
70
  Precedence = symbol_CreatePrecedence();
 
71
  term_Init();
 
72
  fol_Init(TRUE, Precedence);
 
73
  clause_Init();
 
74
  cmdlne_Init();
 
75
 
 
76
  if (!cmdlne_Read(argc, argv) ||
 
77
      cmdlne_GetInputFile() == (char*)NULL || 
 
78
      cmdlne_GetOutputFile() == (char*)NULL) {
 
79
    /* print options */
 
80
    fputs("\n\t          tptp2dfg Version ", stdout);
 
81
    fputs(TPTP2DFG__VERSION, stdout);
 
82
    puts("\n\t       Usage: tptp2dfg [-include] <input-file> <output-file>\n");
 
83
 
 
84
    puts("-include makes the parser parse the files in include directive,");
 
85
    puts("\tby default the directives are just translated.");
 
86
    return EXIT_FAILURE;
 
87
  }
 
88
 
 
89
  if (!cmdlne_SetFlags(Flags))
 
90
    return EXIT_FAILURE;
 
91
  
 
92
  /*Set up variables*/
 
93
 
 
94
  Axioms = list_Nil();
 
95
  Conjectures = list_Nil();
 
96
  SortDecls = list_Nil();
 
97
  UserDefinedPrecedence = list_Nil(); 
 
98
  UserDefinedSelection = list_Nil();
 
99
  ClAxRelation = list_Nil();
 
100
  Includes = list_Nil();
 
101
  
 
102
  Description = desc_Create();
 
103
 
 
104
  InFile = tptp_OpenFile(cmdlne_GetInputFile(),NULL);
 
105
  OutFile = misc_OpenFile(cmdlne_GetOutputFile(),"w");
 
106
  tptp_SetParserOutput(OutFile); /*for the header comments*/
 
107
 
 
108
  /*Parse the thing*/
 
109
  if (flag_GetFlagIntValue(Flags, flag_INCLUDE) == flag_INCLUDEON) {
 
110
    Clauses = tptp_TPTPParser(InFile, Flags, Precedence, Description,
 
111
                              &Axioms, &Conjectures, &SortDecls,
 
112
                              &UserDefinedPrecedence, &UserDefinedSelection, &ClAxRelation,
 
113
                              &Dummy);
 
114
  } else {
 
115
    Clauses = tptp_TPTPParserIncludesExplicit(InFile, Flags, Precedence, Description,
 
116
                                              &Axioms, &Conjectures, &SortDecls,
 
117
                                              &UserDefinedPrecedence, &UserDefinedSelection, &ClAxRelation,
 
118
                                              &Includes, &Dummy);
 
119
  }
 
120
 
 
121
  /* Print the thing*/
 
122
  tptp_FPrintDFGProblem(OutFile,Description,Clauses,ClAxRelation,Axioms,Conjectures,Includes,tptp_WasParsingCNF());
 
123
 
 
124
  misc_CloseFile(InFile,cmdlne_GetInputFile());
 
125
  misc_CloseFile(OutFile,cmdlne_GetOutputFile());
 
126
 
 
127
  /* Free the variables */
 
128
  desc_Delete(Description);
 
129
 
 
130
  list_DeleteWithElement(Clauses, (void (*)(POINTER))clause_Delete);
 
131
  list_DeleteWithElement(Axioms, tptp_DeleteLabelTermPair);
 
132
  list_DeleteWithElement(Conjectures, tptp_DeleteLabelTermPair);
 
133
  list_DeleteWithElement(Includes, tptp_DeleteStrListOfStrPair);
 
134
 
 
135
  dfg_DeleteClAxRelation(ClAxRelation);
 
136
 
 
137
#ifdef CHECK
 
138
  if (list_Exist(SortDecls) || list_Exist(UserDefinedPrecedence)
 
139
      || list_Exist(UserDefinedSelection)) {
 
140
    misc_StartUserErrorReport();
 
141
    misc_ErrorReport("SortDecls, UserDefinedPrecedence, and UserDefinedSelection should all be empty!\n");
 
142
    misc_FinishUserErrorReport();
 
143
  }
 
144
#endif
 
145
 
 
146
  /*Free the modules*/
 
147
  tptp_Free();
 
148
  cmdlne_Free();
 
149
  flag_DeleteStore(Flags);
 
150
  symbol_DeletePrecedence(Precedence);
 
151
  fol_Free();
 
152
  symbol_FreeAllSymbols();
 
153
#ifdef CHECK
 
154
  memory_Print();
 
155
#endif
 
156
  
 
157
  return EXIT_SUCCESS;
 
158
}
 
159
 
 
160
static void tptp_FPrintFormulaList(FILE* File, LIST Formulas, const char* Name)
 
161
/**************************************************************
 
162
  INPUT:   A file, a list of formulas, a name.
 
163
  EFFECTS: Print a list formulas in DFG format, with given list name.
 
164
**************************************************************/
 
165
{
 
166
  LIST scan;
 
167
 
 
168
  fputs("list_of_formulae(", File);
 
169
  fputs(Name, File);
 
170
  fputs(").\n", File);
 
171
  for (scan = Formulas; !list_Empty(scan); scan= list_Cdr(scan)) {
 
172
    LIST formula_pair = list_Car(scan);
 
173
  
 
174
    fputs("\tformula(", File);
 
175
    fol_FPrintDFG(File, list_PairSecond(formula_pair));
 
176
    fputs(",", File);
 
177
    fputs((char*)list_PairFirst(formula_pair), File);
 
178
    fputs(").\n", File);
 
179
  }
 
180
  fputs("end_of_list.\n\n", File);
 
181
}
 
182
 
 
183
static void tptp_FPrintClauseWithLabel(FILE* File, CLAUSE Clause, const char* label) {
 
184
  int     n,j;
 
185
  LITERAL Lit;
 
186
  TERM    Atom;
 
187
  LIST    Variables,Iter;
 
188
  
 
189
  n = clause_Length(Clause);
 
190
 
 
191
  fputs("\tclause(", File);
 
192
  Variables = list_Nil();
 
193
 
 
194
  for (j = 0; j < n; j++)
 
195
    Variables =
 
196
      list_NPointerUnion(Variables,
 
197
                         term_VariableSymbols(clause_GetLiteralAtom(Clause,j)));
 
198
 
 
199
  if (!list_Empty(Variables)) {
 
200
    symbol_FPrint(File, fol_All());
 
201
    fputs("([", File);
 
202
    for (Iter = Variables; !list_Empty(Iter); Iter = list_Cdr(Iter)) {
 
203
      symbol_FPrint(File, (SYMBOL) list_Car(Iter));
 
204
      if (!list_Empty(list_Cdr(Iter)))
 
205
        putc(',', File);
 
206
    }
 
207
    fputs("],", File);
 
208
  }
 
209
    
 
210
  symbol_FPrint(File, fol_Or());
 
211
  putc('(', File);  
 
212
 
 
213
  for (j = 0; j < n; j++) {
 
214
    Lit  = clause_GetLiteral(Clause,j);
 
215
    Atom = clause_LiteralSignedAtom(Lit);
 
216
    term_FPrintPrefix(File,Atom);
 
217
    if (j+1 < n)
 
218
      putc(',', File);
 
219
  }
 
220
  if (n==0)
 
221
    symbol_FPrint(File,fol_False());
 
222
 
 
223
  if (!list_Empty(Variables)) {
 
224
    list_Delete(Variables);
 
225
    putc(')', File);
 
226
  }
 
227
  
 
228
  fprintf(File, "),%s", label);
 
229
  
 
230
  fputs(").\n", File);
 
231
}
 
232
 
 
233
static void tptp_FPrintClauseList(FILE* File, LIST Clauses,
 
234
                                  LIST ClAxRelation, BOOL PrintConjectures, const char* Name)
 
235
/**************************************************************
 
236
  INPUT:   A file, a list of clauses, a flag and a name.
 
237
  EFFECTS: Print a list formulas in DFG format, with given list name.
 
238
           Prints the fromula only when
 
239
          ("the formula is a conjecture clause" == PrintConjectures)
 
240
**************************************************************/
 
241
{
 
242
  LIST Scan;
 
243
  
 
244
  fputs("list_of_clauses(", File);
 
245
  fputs(Name, File);
 
246
  fputs(",cnf).\n", File);
 
247
  
 
248
  for (Scan=Clauses; !list_Empty(Scan);Scan=list_Cdr(Scan)) {
 
249
    CLAUSE Clause;
 
250
    LIST ClAx;
 
251
    LIST Labels;
 
252
 
 
253
    Clause = (CLAUSE) list_Car(Scan);
 
254
 
 
255
#ifdef CHECK
 
256
    if (list_Empty(ClAxRelation)) {
 
257
      misc_StartUserErrorReport();
 
258
      misc_ErrorReport("ClAxRelation too short!\n");
 
259
      misc_FinishUserErrorReport();
 
260
    }
 
261
#endif
 
262
 
 
263
    ClAx = (LIST) list_Car(ClAxRelation);
 
264
 
 
265
#ifdef CHECK
 
266
    if ((int)list_Car(ClAx) != clause_Number(Clause)) {
 
267
      misc_StartUserErrorReport();
 
268
      misc_ErrorReport("Incompatible ClAxRelation!\n");
 
269
      misc_FinishUserErrorReport();
 
270
    }
 
271
#endif
 
272
 
 
273
    Labels = list_Cdr(ClAx);
 
274
 
 
275
#ifdef CHECK
 
276
    if (list_Empty(Labels)) {
 
277
      misc_StartUserErrorReport();
 
278
      misc_ErrorReport("Empty ClAxRelation entry!\n");
 
279
      misc_FinishUserErrorReport();
 
280
    }
 
281
#endif
 
282
    
 
283
    if (PrintConjectures == clause_GetFlag(Clause,CONCLAUSE))
 
284
      tptp_FPrintClauseWithLabel(File,Clause,(char*)list_Car(Labels) /*the first and the only one*/);
 
285
 
 
286
    ClAxRelation = list_Cdr(ClAxRelation);
 
287
  }
 
288
  fputs("end_of_list.\n\n", File);
 
289
}
 
290
 
 
291
static void tptp_FPrintInclude(FILE* File, char* filename, LIST selection) 
 
292
/**************************************************************
 
293
  INPUT:   A file, name of file included, list of formule secelection.
 
294
  EFFECTS: Print a line in DFG format denoting the given inclusion.
 
295
**************************************************************/
 
296
{
 
297
  int len;
 
298
        
 
299
  fputs("\tinclude('",File);
 
300
        
 
301
  len = strlen(filename);
 
302
  if ((len >= 2) && (filename[len-1] == 'p') && (filename[len-2] == '.')) { /*changing *.p to *.dfg */
 
303
    filename[len-1] = '\0';
 
304
    fputs(filename,File);
 
305
    fputs("dfg",File);
 
306
    filename[len-1] = 'p';
 
307
  } else if ((len >= 3) && (filename[len-1] == 'x') && (filename[len-2] == 'a') && (filename[len-3] == '.')) { /*changing *.ax to *.ax.dfg */
 
308
    fputs(filename,File);
 
309
    fputs(".dfg",File);
 
310
  } else {
 
311
    fputs(filename,File);
 
312
  }
 
313
 
 
314
  fputs("'",File);
 
315
        
 
316
  if (list_Exist(selection)) {
 
317
    fputs(",[",File);
 
318
    fputs((char*)list_Car(selection),File);
 
319
    selection = list_Cdr(selection);
 
320
                
 
321
    while(list_Exist(selection)) {
 
322
      fputs(",",File);
 
323
      fputs((char*)list_Car(selection),File);
 
324
      selection = list_Cdr(selection);
 
325
    }
 
326
    fputs("]",File);
 
327
  }
 
328
 
 
329
  fputs(").\n",File);
 
330
}
 
331
        
 
332
static __inline__ const char* Null2Empty(char * str) {
 
333
  return str ? str : "";
 
334
}
 
335
 
 
336
static void tptp_FPrintDFGProblem(FILE* File, DFGDESCRIPTION Description,
 
337
                                  LIST Clauses, LIST ClAxRelation,
 
338
                                  LIST Axioms, LIST Conjectures,
 
339
                                  LIST Includes, BOOL IsCnf)
 
340
/**************************************************************
 
341
  INPUT:   A file, some info strings, two lists of formulas, and a boolean flag
 
342
  EFFECTS: Prints a complete DFG file containing these lists.
 
343
**************************************************************/
 
344
{
 
345
  fputs("begin_problem(Unknown).\n\n", File);
 
346
  
 
347
  fputs("list_of_descriptions.\n", File);
 
348
  fprintf(File,"name({*%s*}).\n",Null2Empty(Description->name));
 
349
  fprintf(File,"author({*%s*}).\n",Null2Empty(Description->author));
 
350
  if (Description->version)
 
351
    fprintf(File,"version({*%s*}).\n",Null2Empty(Description->version));
 
352
  if (Description->logic)
 
353
    fprintf(File,"logic({*%s*}).\n",Null2Empty(Description->logic));
 
354
 
 
355
  fprintf(File,"status(%s).\n",desc_StatusString(Description));
 
356
 
 
357
  fprintf(File,"description({*%s*}).\n",Null2Empty(Description->description));
 
358
  if (Description->date)
 
359
    fprintf(File,"date({*%s*}).\n",Null2Empty(Description->date));
 
360
  fputs("end_of_list.\n\n", File);
 
361
  
 
362
  fputs("list_of_symbols.\n", File);
 
363
  symbol_FPrintDFGSignature(File);
 
364
  fputs("end_of_list.\n\n", File);
 
365
 
 
366
  if (!IsCnf) {
 
367
    tptp_FPrintFormulaList(File, Axioms, "axioms");
 
368
    tptp_FPrintFormulaList(File, Conjectures, "conjectures");
 
369
  } else {
 
370
    tptp_FPrintClauseList(File, Clauses, ClAxRelation, FALSE, "axioms");
 
371
    tptp_FPrintClauseList(File, Clauses, ClAxRelation, TRUE, "conjectures");
 
372
  }
 
373
 
 
374
  if (list_Exist(Includes)) {
 
375
    LIST Scan;
 
376
          
 
377
    fputs("list_of_includes.\n", File);
 
378
 
 
379
    for (Scan = Includes; !list_Empty(Scan); Scan = list_Cdr(Scan))     {
 
380
      LIST pair = list_Car(Scan);
 
381
      tptp_FPrintInclude(File,list_PairFirst(pair),list_PairSecond(pair));
 
382
    }
 
383
        
 
384
    fputs("end_of_list.\n\n", File);  
 
385
  }
 
386
     
 
387
  fputs("end_problem.\n", File);
 
388
}