← Back to branch summary

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

« back to all changes in this revision

Viewing changes to ladr/just.h.bak

  • 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:
ladr/just.h.bak
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
 
#ifndef TP_JUST_H
20
 
#define TP_JUST_H
21
 
 
22
 
#include "clauseid.h"
23
 
#include "parse.h"
24
 
 
25
 
/* INTRODUCTION
26
 
*/
27
 
 
28
 
/* Public definitions */
29
 
 
30
 
typedef enum {
31
 
  INPUT_JUST,         /* Primary                              */
32
 
  GOAL_JUST,          /* Primary                              */
33
 
  DENY_JUST,          /* Primary    int       (ID)            */
34
 
  CLAUSIFY_JUST,      /* Primary    int       (ID)            */
35
 
  COPY_JUST,          /* Primary    int       (ID)            */
36
 
  BACK_DEMOD_JUST,    /* Primary    int       (ID)            */
37
 
  BACK_UNIT_DEL_JUST, /* Primary    int       (ID)            */
38
 
  NEW_SYMBOL_JUST,    /* Primary    int       (ID)            */
39
 
  EXPAND_DEF_JUST,    /* Primary    Ilist     (ID,def-ID)     */
40
 
  BINARY_RES_JUST,    /* Primary    Ilist                     */
41
 
  HYPER_RES_JUST,     /* Primary    Ilist                     */
42
 
  UR_RES_JUST,        /* Primary    Ilist                     */
43
 
  FACTOR_JUST,        /* Primary    Ilist     (ID,lit1,lit2)  */
44
 
  XXRES_JUST,         /* Primary    Ilist     (ID,lit)        */
45
 
  PARA_JUST,          /* Primary    Parajust                  */
46
 
  PARA_FX_JUST,       /* Primary    Parajust                  */
47
 
  PARA_IX_JUST,       /* Primary    Parajust                  */
48
 
  PARA_FX_IX_JUST,    /* Primary    Parajust                  */
49
 
  INSTANCE_JUST,      /* Primary    Instancejust              */
50
 
  PROPOSITIONAL_JUST, /* Primary    int       (ID)            */
51
 
 
52
 
  DEMOD_JUST,         /* Secondary  I3list                    */
53
 
  UNIT_DEL_JUST,      /* Secondary  Ilist     (lit,ID)        */
54
 
  FLIP_JUST,          /* Secondary  int       (lit)           */
55
 
  XX_JUST,            /* Secondary  int       (lit)           */
56
 
  MERGE_JUST,         /* Secondary  int       (lit)           */
57
 
  EVAL_JUST,          /* Secondary  int       (count)         */
58
 
 
59
 
  IVY_JUST,           /* Primary    Ivyjust                   */
60
 
 
61
 
  UNKNOWN_JUST        /* probably an error                    */
62
 
} Just_type;
63
 
 
64
 
typedef struct parajust * Parajust;
65
 
 
66
 
struct parajust {
67
 
  int from_id;
68
 
  int into_id;
69
 
  Ilist from_pos;
70
 
  Ilist into_pos;
71
 
};
72
 
 
73
 
typedef struct instancejust * Instancejust;
74
 
 
75
 
struct instancejust {
76
 
  int parent_id;
77
 
  Plist pairs;
78
 
};
79
 
 
80
 
typedef struct ivyjust * Ivyjust;
81
 
 
82
 
struct ivyjust {
83
 
  Just_type type;  /* input,resolve,paramod,instantiate,flip,propositional */
84
 
  int parent1;
85
 
  int parent2;
86
 
  Ilist pos1;
87
 
  Ilist pos2;
88
 
  Plist pairs;  /* for instantiate */
89
 
};
90
 
 
91
 
typedef struct just * Just;
92
 
 
93
 
struct just {
94
 
  Just_type type;
95
 
  Just next;
96
 
  union {
97
 
    int id;
98
 
    Ilist lst;
99
 
    Parajust para;
100
 
    I3list demod;
101
 
    Instancejust instance;
102
 
    Ivyjust ivy;
103
 
  } u;
104
 
};
105
 
 
106
 
/* A justification starts with a Primary part and then
107
 
   has a sequence (maybe none) of Secondary parts.
108
 
   Each type has some data, an integer or Ilist (integer
109
 
   list) giving clause IDs, or positions of literals or
110
 
   subterms.
111
 
*/
112
 
 
113
 
/* End of public definitions */
114
 
 
115
 
/* Public function prototypes from just.c */
116
 
 
117
 
Just get_just(void);
118
 
 
119
 
Parajust get_parajust(void);
120
 
 
121
 
Instancejust get_instancejust(void);
122
 
 
123
 
void fprint_just_mem(FILE *fp, BOOL heading);
124
 
 
125
 
void p_just_mem();
126
 
 
127
 
Just ivy_just(Just_type type,
128
 
              int parent1, Ilist pos1,
129
 
              int parent2, Ilist pos2,
130
 
              Plist pairs);
131
 
 
132
 
Just input_just(void);
133
 
 
134
 
Just goal_just(void);
135
 
 
136
 
Just deny_just(Topform tf);
137
 
 
138
 
Just clausify_just(Topform tf);
139
 
 
140
 
Just expand_def_just(Topform tf, Topform def);
141
 
 
142
 
Just copy_just(Topform c);
143
 
 
144
 
Just propositional_just(Topform c);
145
 
 
146
 
Just new_symbol_just(Topform c);
147
 
 
148
 
Just back_demod_just(Topform c);
149
 
 
150
 
Just back_unit_deletion_just(Topform c);
151
 
 
152
 
Just binary_res_just(Topform c1, int n1, Topform c2, int n2);
153
 
 
154
 
Just binary_res_just_by_id(int c1, int n1, int c2, int n2);
155
 
 
156
 
Just factor_just(Topform c, int lit1, int lit2);
157
 
 
158
 
Just xxres_just(Topform c, int lit);
159
 
 
160
 
Just resolve_just(Ilist g, Just_type type);
161
 
 
162
 
Just demod_just(I3list steps);
163
 
 
164
 
Just para_just(Just_type rule,
165
 
               Topform from, Ilist from_vec,
166
 
               Topform into, Ilist into_vec);
167
 
 
168
 
Just instance_just(Topform parent, Plist pairs);
169
 
 
170
 
Just para_just_rev_copy(Just_type rule,
171
 
                        Topform from, Ilist from_vec,
172
 
                        Topform into, Ilist into_vec);
173
 
 
174
 
Just unit_del_just(Topform deleter, int literal_num);
175
 
 
176
 
Just flip_just(int n);
177
 
 
178
 
Just xx_just(int n);
179
 
 
180
 
Just merge_just(int n);
181
 
 
182
 
Just eval_just(int n);
183
 
 
184
 
Just append_just(Just j1, Just j2);
185
 
 
186
 
Just copy_justification(Just j);
187
 
 
188
 
char *jstring(Just j);
189
 
 
190
 
int jmap1(I3list map, int i);
191
 
 
192
 
char *jmap2(I3list map, int i, char *a);
193
 
 
194
 
void sb_append_id(String_buf sb, int id, I3list map);
195
 
 
196
 
void sb_write_ids(String_buf sb, Ilist p, I3list map);
197
 
 
198
 
void sb_write_just(String_buf sb, Just just, I3list map);
199
 
 
200
 
void sb_xml_write_just(String_buf sb, Just just, I3list map);
201
 
 
202
 
void p_just(Just j);
203
 
 
204
 
void zap_just(Just just);
205
 
 
206
 
Ilist get_parents(Just just, BOOL all);
207
 
 
208
 
Topform first_negative_parent(Topform c);
209
 
 
210
 
Plist get_clause_ancestors(Topform c);
211
 
 
212
 
int proof_length(Plist proof);
213
 
 
214
 
void map_just(Just just, I2list map);
215
 
 
216
 
int just_count(Just j);
217
 
 
218
 
void mark_parents_as_used(Topform c);
219
 
 
220
 
int clause_level(Topform c);
221
 
 
222
 
Just term_to_just(Term lst);
223
 
 
224
 
BOOL primary_just_type(Topform c, Just_type t);
225
 
 
226
 
BOOL has_input_just(Topform c);
227
 
 
228
 
BOOL has_copy_just(Topform c);
229
 
 
230
 
BOOL has_copy_flip_just(Topform c);
231
 
 
232
 
void sb_tagged_write_just(String_buf sb, Just just, I3list map);
233
 
 
234
 
#endif  /* conditional compilation of whole file */