1 ///////////////////////////////////////////////////////////////////////////////
2 // This file is generated automatically using Prop (version 2.3.4),
3 // last updated on Apr 4, 1997.
4 // The original source file is "T7.pcc".
5 ///////////////////////////////////////////////////////////////////////////////
7 #define PROP_REWRITING_USED
8 #define PROP_QUARK_USED
11 ///////////////////////////////////////////////////////////////////////////////
13 // Forward class definition for Wff
15 ///////////////////////////////////////////////////////////////////////////////
16 #ifndef datatype_Wff_defined
17 #define datatype_Wff_defined
25 ///////////////////////////////////////////////////////////////////////////////
27 // Base class for datatype Wff
29 ///////////////////////////////////////////////////////////////////////////////
30 class a_Wff
: public TermObj
{
33 tag_VAR
= 0, tag_NOT
= 1, tag_AND
= 2,
38 const Tag_Wff tag__
; // variant tag
40 inline a_Wff(Tag_Wff t__
) : tag__(t__
) {}
43 inline int boxed(const a_Wff
* x
) { return (unsigned long)x
>= 2; }
44 inline int untag(const a_Wff
* x
) { return boxed(x
) ? x
->tag__
+ 2 : (int)x
; }
45 ///////////////////////////////////////////////////////////////////////////////
47 // Class for datatype constructor Wff::VAR
49 ///////////////////////////////////////////////////////////////////////////////
50 class Wff_VAR
: public a_Wff
{
54 inline Wff_VAR (Quark x_VAR
)
55 : a_Wff(tag_VAR
), VAR(x_VAR
)
60 ///////////////////////////////////////////////////////////////////////////////
62 // Class for datatype constructor Wff::NOT
64 ///////////////////////////////////////////////////////////////////////////////
65 class Wff_NOT
: public a_Wff
{
69 inline Wff_NOT (Wff x_NOT
)
70 : a_Wff(tag_NOT
), NOT(x_NOT
)
75 ///////////////////////////////////////////////////////////////////////////////
77 // Class for datatype constructor Wff::AND
79 ///////////////////////////////////////////////////////////////////////////////
80 class Wff_AND
: public a_Wff
{
84 inline Wff_AND (Wff x_1
, Wff x_2
)
85 : a_Wff(tag_AND
), _1(x_1
), _2(x_2
)
90 ///////////////////////////////////////////////////////////////////////////////
92 // Class for datatype constructor Wff::OR
94 ///////////////////////////////////////////////////////////////////////////////
95 class Wff_OR
: public a_Wff
{
99 inline Wff_OR (Wff x_1
, Wff x_2
)
100 : a_Wff(tag_OR
), _1(x_1
), _2(x_2
)
105 ///////////////////////////////////////////////////////////////////////////////
107 // Datatype constructor functions for Wff
109 ///////////////////////////////////////////////////////////////////////////////
110 inline a_Wff
* VAR (Quark x_VAR
)
112 return new Wff_VAR (x_VAR
);
114 inline a_Wff
* NOT (Wff x_NOT
)
116 return new Wff_NOT (x_NOT
);
118 inline a_Wff
* AND (Wff x_1
, Wff x_2
)
120 return new Wff_AND (x_1
, x_2
);
122 inline a_Wff
* OR (Wff x_1
, Wff x_2
)
124 return new Wff_OR (x_1
, x_2
);
126 ///////////////////////////////////////////////////////////////////////////////
128 // Downcasting functions for Wff
130 ///////////////////////////////////////////////////////////////////////////////
131 inline Wff_VAR
* _VAR(const a_Wff
* _x_
) { return (Wff_VAR
*)_x_
; }
132 inline Wff_NOT
* _NOT(const a_Wff
* _x_
) { return (Wff_NOT
*)_x_
; }
133 inline Wff_AND
* _AND(const a_Wff
* _x_
) { return (Wff_AND
*)_x_
; }
134 inline Wff_OR
* _OR(const a_Wff
* _x_
) { return (Wff_OR
*)_x_
; }
145 extern void _T_7co_X1_rewrite(Wff
& );
146 _T_7co_X1_rewrite(wff
);
153 class _T_7co_X1
: public BURS
{
155 _T_7co_X1(const _T_7co_X1
&); // no copy constructor
156 void operator = (const _T_7co_X1
&); // no assignment
158 struct _T_7co_X1_StateRec
* stack__
, * stack_top__
;
160 void labeler(const char *, int&, int);
161 void labeler(Quark
, int&, int);
162 void labeler(Wff
& redex
, int&, int);
163 inline virtual void operator () (Wff
& redex
) { int s
; labeler(redex
,s
,0); }
166 inline _T_7co_X1() {}
168 void _T_7co_X1_rewrite(Wff
& _x_
)
173 ///////////////////////////////////////////////////////////////////////////////
175 // This macro can be redefined by the user for debugging
177 ///////////////////////////////////////////////////////////////////////////////
178 #ifndef DEBUG__T_7co_X1
179 #define DEBUG__T_7co_X1(repl,redex,file,line,rule) repl
181 static const char * _T_7co_X1_file_name
= "T7.pcc";
184 static const TreeTables::ShortState _T_7co_X1_theta_3
[5] = {
189 static const TreeTables::ShortState _T_7co_X1_theta_4
[5][4] = {
198 static const TreeTables::ShortState _T_7co_X1_theta_5
[4][3] = {
206 static const TreeTables::ShortState _T_7co_X1_mu_3_0
[40] = {
207 0, 1, 2, 3, 0, 4, 3, 0, 0, 0, 4, 4, 4, 3, 0, 0,
208 0, 0, 0, 4, 4, 4, 4, 4, 3, 0, 0, 0, 3, 0, 0, 0,
209 0, 0, 0, 0, 0, 4, 4, 4
213 static const TreeTables::ShortState _T_7co_X1_mu_4_0
[40] = {
214 0, 1, 2, 0, 3, 4, 0, 3, 3, 3, 4, 4, 4, 0, 3, 3,
215 3, 3, 3, 4, 4, 4, 4, 4, 0, 3, 3, 3, 0, 3, 3, 3,
216 3, 3, 3, 3, 3, 4, 4, 4
220 static const TreeTables::ShortState _T_7co_X1_mu_4_1
[40] = {
221 0, 1, 2, 0, 0, 3, 0, 0, 0, 0, 3, 3, 3, 0, 0, 0,
222 0, 0, 0, 3, 3, 3, 3, 3, 0, 0, 0, 0, 0, 0, 0, 0,
223 0, 0, 0, 0, 0, 3, 3, 3
227 static const TreeTables::ShortState _T_7co_X1_mu_5_0
[40] = {
228 0, 1, 2, 0, 0, 3, 0, 0, 0, 0, 3, 3, 3, 0, 0, 0,
229 0, 0, 0, 3, 3, 3, 3, 3, 0, 0, 0, 0, 0, 0, 0, 0,
230 0, 0, 0, 0, 0, 3, 3, 3
234 static const TreeTables::ShortState _T_7co_X1_mu_5_1
[40] = {
235 0, 1, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
236 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
237 0, 0, 0, 0, 0, 0, 0, 0
241 inline void _T_7co_X1::labeler(char const * redex
,int& s__
,int)
248 inline void _T_7co_X1::labeler(Quark redex
,int& s__
,int)
255 void _T_7co_X1::labeler (Wff
& redex
, int& s__
, int r__
)
259 if (r__
&& boxed(redex
) && (cached__
= redex
->get_rewrite_state()) != BURS::undefined_state
)
260 { s__
= cached__
; return; }
262 switch(redex
->tag__
) {
263 case a_Wff::tag_VAR
: {
265 labeler(_VAR(redex
)->VAR
, s0__
, r__
);
267 case a_Wff::tag_NOT
: {
269 labeler(_NOT(redex
)->NOT
, s0__
, r__
);
270 s__
= _T_7co_X1_theta_3
[_T_7co_X1_mu_3_0
[s0__
]]; } break;
271 case a_Wff::tag_AND
: {
274 labeler(_AND(redex
)->_1
, s0__
, r__
);
275 labeler(_AND(redex
)->_2
, s1__
, r__
);
276 s__
= _T_7co_X1_theta_4
[_T_7co_X1_mu_4_0
[s0__
]][_T_7co_X1_mu_4_1
[s1__
]]; } break;
280 labeler(_OR(redex
)->_1
, s0__
, r__
);
281 labeler(_OR(redex
)->_2
, s1__
, r__
);
282 s__
= _T_7co_X1_theta_5
[_T_7co_X1_mu_5_0
[s0__
]][_T_7co_X1_mu_5_1
[s1__
]]; } break;
285 if (((int)redex
)) {s__
= 2;
293 Wff _X3
= _AND(_AND(redex
)->_1
)->_2
;
294 int _X2
= boxed(_X3
) ? _X3
->get_rewrite_state() : ((int)_X3
+ 0);
296 case 4: repl__
= AND(_AND(_AND(redex
)->_1
)->_1
,AND(_AND(_AND(_AND(redex
)->_1
)->_2
)->_1
,AND(_AND(_AND(_AND(redex
)->_1
)->_2
)->_2
,_AND(redex
)->_2
))); break;
298 repl__
= AND(_AND(_AND(redex
)->_1
)->_1
,AND(_AND(_AND(redex
)->_1
)->_2
,_AND(redex
)->_2
)); break;
300 { redex
= DEBUG__T_7co_X1(repl__
,redex
,_T_7co_X1_file_name
,29,"AND (AND (X, Y), Z): ...");
301 r__
= 1; goto replacement__
; }
307 Wff _X5
= _OR(_OR(redex
)->_1
)->_2
;
308 int _X4
= boxed(_X5
) ? _X5
->get_rewrite_state() : ((int)_X5
+ 0);
310 case 5: repl__
= OR(_OR(_OR(redex
)->_1
)->_1
,OR(_OR(_OR(_OR(redex
)->_1
)->_2
)->_1
,OR(_OR(_OR(_OR(redex
)->_1
)->_2
)->_2
,_OR(redex
)->_2
))); break;
312 repl__
= OR(_OR(_OR(redex
)->_1
)->_1
,OR(_OR(_OR(redex
)->_1
)->_2
,_OR(redex
)->_2
)); break;
314 { redex
= DEBUG__T_7co_X1(repl__
,redex
,_T_7co_X1_file_name
,28,"OR (OR (X, Y), Z): ...");
315 r__
= 1; goto replacement__
; }
322 Wff _X7
= _AND(redex
)->_1
;
323 int _X6
= boxed(_X7
) ? _X7
->get_rewrite_state() : ((int)_X7
+ 0);
325 case 4: repl__
= OR(AND(_AND(_AND(redex
)->_1
)->_1
,AND(_AND(_AND(redex
)->_1
)->_2
,_OR(_AND(redex
)->_2
)->_1
)),AND(_AND(_AND(redex
)->_1
)->_1
,AND(_AND(_AND(redex
)->_1
)->_2
,_OR(_AND(redex
)->_2
)->_2
))); break;
327 Wff _X9
= _OR(_AND(redex
)->_2
)->_2
;
328 int _X8
= boxed(_X9
) ? _X9
->get_rewrite_state() : ((int)_X9
+ 0);
330 case 5: repl__
= OR(AND(_AND(redex
)->_1
,_OR(_AND(redex
)->_2
)->_1
),OR(AND(_AND(redex
)->_1
,_OR(_OR(_AND(redex
)->_2
)->_2
)->_1
),AND(_AND(redex
)->_1
,_OR(_OR(_AND(redex
)->_2
)->_2
)->_2
))); break;
332 repl__
= OR(AND(_AND(redex
)->_1
,_OR(_AND(redex
)->_2
)->_1
),AND(_AND(redex
)->_1
,_OR(_AND(redex
)->_2
)->_2
)); break;
335 { redex
= DEBUG__T_7co_X1(repl__
,redex
,_T_7co_X1_file_name
,27,"AND (X, OR (Y, Z)): ...");
336 r__
= 1; goto replacement__
; }
343 Wff _X11
= _OR(_AND(redex
)->_1
)->_1
;
344 int _X10
= boxed(_X11
) ? _X11
->get_rewrite_state() : ((int)_X11
+ 0);
346 case 4: repl__
= OR(AND(_AND(_OR(_AND(redex
)->_1
)->_1
)->_1
,AND(_AND(_OR(_AND(redex
)->_1
)->_1
)->_2
,_AND(redex
)->_2
)),AND(_OR(_AND(redex
)->_1
)->_2
,_AND(redex
)->_2
)); break;
348 Wff _X13
= _OR(_AND(redex
)->_1
)->_2
;
349 int _X12
= boxed(_X13
) ? _X13
->get_rewrite_state() : ((int)_X13
+ 0);
351 case 5: repl__
= OR(AND(_OR(_AND(redex
)->_1
)->_1
,_AND(redex
)->_2
),OR(AND(_OR(_OR(_AND(redex
)->_1
)->_2
)->_1
,_AND(redex
)->_2
),AND(_OR(_OR(_AND(redex
)->_1
)->_2
)->_2
,_AND(redex
)->_2
))); break;
352 case 4: repl__
= OR(AND(_OR(_AND(redex
)->_1
)->_1
,_AND(redex
)->_2
),AND(_AND(_OR(_AND(redex
)->_1
)->_2
)->_1
,AND(_AND(_OR(_AND(redex
)->_1
)->_2
)->_2
,_AND(redex
)->_2
))); break;
354 Wff _X15
= _AND(redex
)->_2
;
355 int _X14
= boxed(_X15
) ? _X15
->get_rewrite_state() : ((int)_X15
+ 0);
357 case 5: repl__
= OR(AND(_OR(_AND(redex
)->_1
)->_1
,_OR(_AND(redex
)->_2
)->_1
),OR(AND(_OR(_AND(redex
)->_1
)->_1
,_OR(_AND(redex
)->_2
)->_2
),OR(AND(_OR(_AND(redex
)->_1
)->_2
,_OR(_AND(redex
)->_2
)->_1
),AND(_OR(_AND(redex
)->_1
)->_2
,_OR(_AND(redex
)->_2
)->_2
)))); break;
359 repl__
= OR(AND(_OR(_AND(redex
)->_1
)->_1
,_AND(redex
)->_2
),AND(_OR(_AND(redex
)->_1
)->_2
,_AND(redex
)->_2
)); break;
363 { redex
= DEBUG__T_7co_X1(repl__
,redex
,_T_7co_X1_file_name
,26,"AND (OR (X, Y), Z): ...");
364 r__
= 1; goto replacement__
; }
370 Wff _X17
= _OR(_NOT(redex
)->NOT
)->_1
;
371 int _X16
= boxed(_X17
) ? _X17
->get_rewrite_state() : ((int)_X17
+ 0);
373 case 3: repl__
= AND(_NOT(_OR(_NOT(redex
)->NOT
)->_1
)->NOT
,NOT(_OR(_NOT(redex
)->NOT
)->_2
)); break;
375 Wff _X19
= _OR(_NOT(redex
)->NOT
)->_2
;
376 int _X18
= boxed(_X19
) ? _X19
->get_rewrite_state() : ((int)_X19
+ 0);
378 case 5: repl__
= AND(NOT(_OR(_NOT(redex
)->NOT
)->_1
),AND(NOT(_OR(_OR(_NOT(redex
)->NOT
)->_2
)->_1
),NOT(_OR(_OR(_NOT(redex
)->NOT
)->_2
)->_2
))); break;
379 case 3: repl__
= AND(NOT(_OR(_NOT(redex
)->NOT
)->_1
),_NOT(_OR(_NOT(redex
)->NOT
)->_2
)->NOT
); break;
381 repl__
= AND(NOT(_OR(_NOT(redex
)->NOT
)->_1
),NOT(_OR(_NOT(redex
)->NOT
)->_2
)); break;
384 { redex
= DEBUG__T_7co_X1(repl__
,redex
,_T_7co_X1_file_name
,24,"NOT OR (X, Y): ...");
385 r__
= 1; goto replacement__
; }
392 { redex
= DEBUG__T_7co_X1(F
,redex
,_T_7co_X1_file_name
,22,"AND (_, F): ...");
393 r__
= 1; goto replacement__
; }
400 { redex
= DEBUG__T_7co_X1(F
,redex
,_T_7co_X1_file_name
,21,"AND (F, _): ...");
401 r__
= 1; goto replacement__
; }
409 { redex
= DEBUG__T_7co_X1(_AND(redex
)->_1
,redex
,_T_7co_X1_file_name
,20,"AND (X, T): ...");
410 r__
= 1; goto replacement__
; }
418 { redex
= DEBUG__T_7co_X1(_AND(redex
)->_2
,redex
,_T_7co_X1_file_name
,19,"AND (T, X): ...");
419 r__
= 1; goto replacement__
; }
425 { redex
= DEBUG__T_7co_X1(_OR(redex
)->_1
,redex
,_T_7co_X1_file_name
,18,"OR (X, F): ...");
426 r__
= 1; goto replacement__
; }
432 { redex
= DEBUG__T_7co_X1(_OR(redex
)->_2
,redex
,_T_7co_X1_file_name
,17,"OR (F, X): ...");
433 r__
= 1; goto replacement__
; }
440 { redex
= DEBUG__T_7co_X1(T
,redex
,_T_7co_X1_file_name
,16,"OR (_, T): ...");
441 r__
= 1; goto replacement__
; }
448 { redex
= DEBUG__T_7co_X1(T
,redex
,_T_7co_X1_file_name
,15,"OR (T, _): ...");
449 r__
= 1; goto replacement__
; }
454 { redex
= DEBUG__T_7co_X1(_NOT(_NOT(redex
)->NOT
)->NOT
,redex
,_T_7co_X1_file_name
,14,"NOT NOT X: ...");
455 r__
= 1; goto replacement__
; }
460 { redex
= DEBUG__T_7co_X1(T
,redex
,_T_7co_X1_file_name
,13,"NOT F: ...");
461 r__
= 1; goto replacement__
; }
466 { redex
= DEBUG__T_7co_X1(F
,redex
,_T_7co_X1_file_name
,12,"NOT T: ...");
467 r__
= 1; goto replacement__
; }
472 redex
->set_rewrite_state(s__
);
478 ------------------------------- Statistics -------------------------------
479 Merge matching rules = yes
480 Number of DFA nodes merged = 0
481 Number of ifs generated = 0
482 Number of switches generated = 0
485 Adaptive matching = disabled
486 Fast string matching = disabled
487 Inline downcasts = disabled
488 --------------------------------------------------------------------------