← Back to branch summary

~ubuntu-branches/ubuntu/saucy/ladr/saucy

« back to all changes in this revision

Viewing changes to provers.src/tptp_to_ladr.c.save

  • Committer: Package Import Robot
  • Author(s): Frank Lichtenheld
  • Date: 2013-05-25 11:43:32 UTC
  • mfrom: (5.1.5 sid)
  • Revision ID: package-import@ubuntu.com-20130525114332-lkzco1dti2hwrf7v
Tags: 0.0.200911a-2
* QA upload.
* Upload to unstable.
* Change maintainer to QA group.

Show diffs side-by-side

added added

removed removed

Lines of Context:
provers.src/tptp_to_ladr.c.save
1
 
/*  Copyright (C) 2006, 2007 William McCune
2
 
 
3
 
    This file is part of the LADR Deduction Library.
4
 
 
5
 
    The LADR Deduction Library is free software; you can redistribute it
6
 
    and/or modify it under the terms of the GNU General Public License,
7
 
    version 2.
8
 
 
9
 
    The LADR Deduction Library is distributed in the hope that it will be
10
 
    useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
11
 
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12
 
    GNU General Public License for more details.
13
 
 
14
 
    You should have received a copy of the GNU General Public License
15
 
    along with the LADR Deduction Library; if not, write to the Free Software
16
 
    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
17
 
*/
18
 
 
19
 
#include "../ladr/top_input.h"
20
 
 
21
 
#define PROGRAM_NAME    "tptp_to_ladr"
22
 
#include "../VERSION_DATE.h"
23
 
 
24
 
/*************
25
 
 *
26
 
 *   read_tptp_input()
27
 
 *
28
 
 *************/
29
 
 
30
 
static
31
 
void read_tptp_input(FILE *fin, FILE *fout, FILE *ferr,
32
 
                     Plist *assumps, Plist *goals)
33
 
{
34
 
  Term t = read_term(fin, fout);
35
 
 
36
 
  while (t != NULL) {
37
 
 
38
 
    if (is_term(t, "include", 1) || is_term(t, "include", 2)) {
39
 
      char *fname = new_str_copy(sn_to_str(SYMNUM(ARG(t,0))));
40
 
      char *fname2 = fname;
41
 
      FILE *fin2;
42
 
 
43
 
      if (*fname2 == '\'' || *fname2 == '"') {
44
 
        fname2[strlen(fname2)-1] = '\0';
45
 
        fname2++;
46
 
      }
47
 
      fin2 = fopen(fname2, "r");
48
 
      if (fin2 == NULL) {
49
 
        char s[100];
50
 
        sprintf(s, "read_tptp_input, file %s not found", fname2);
51
 
        fatal_error(s);
52
 
      }
53
 
      fprintf(fout, "\n%% Including file %s\n\n", fname2);
54
 
      read_tptp_input(fin2, fout, ferr, assumps, goals);
55
 
      free(fname);
56
 
    }
57
 
    else if (is_term(t, "cnf", 3) || is_term(t, "cnf", 4) ||
58
 
             is_term(t, "fof", 3) || is_term(t, "fof", 4) ||
59
 
             is_term(t, "input_clause", 3)) {
60
 
      Formula form = tptp_input_to_ladr_formula(t);
61
 
      if (is_term(ARG(t,1), "conjecture", 0))
62
 
        *goals = plist_append(*goals, form);
63
 
      else
64
 
        *assumps = plist_append(*assumps, form);
65
 
    }
66
 
    else {
67
 
      p_term(t);
68
 
      fatal_error("read_tptp_input: unknown term");
69
 
    }
70
 
    zap_term(t);
71
 
    t = read_term(fin, fout);
72
 
  }
73
 
}  /* read_tptp_input */
74
 
 
75
 
int main(int argc, char **argv)
76
 
{
77
 
  Plist assumps = NULL;
78
 
  Plist goals = NULL;
79
 
  int i;
80
 
 
81
 
  init_standard_ladr();
82
 
  i = register_attribute("label",  STRING_ATTRIBUTE);
83
 
 
84
 
  clear_parse_type_for_all_symbols();
85
 
  declare_tptp_parse_types();
86
 
  set_quote_char('\'');  /* TPTP uses single quotes for strings. */
87
 
 
88
 
  read_tptp_input(stdin, stdout, stderr, &assumps, &goals);
89
 
 
90
 
  clear_parse_type_for_all_symbols();
91
 
  declare_standard_parse_types();  /* defaults for LADR */
92
 
 
93
 
  printf("set(prolog_style_variables).\n");
94
 
  fwrite_formula_list(stdout, assumps, "assumptions");
95
 
  fwrite_formula_list(stdout, goals, "goals");
96
 
 
97
 
  exit(0);
98
 
}  /* main */
99