prop-src/T11.cc

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //  This file is generated automatically using Prop (version 2.3.4),
   3 //  last updated on Apr 3, 1997.
   4 //  The original source file is "T11.pcc".
   5 ///////////////////////////////////////////////////////////////////////////////
   6
   7 #define PROP_REWRITING_USED
   8 #define PROP_GARBAGE_COLLECTION_USED
   9 #define PROP_QUARK_USED
  10 #include <propdefs.h>
  11 #line 7 "T11.pcc"
  12 ///////////////////////////////////////////////////////////////////////////////
  13 //
  14 // Forward class definition for Wff
  15 //
  16 ///////////////////////////////////////////////////////////////////////////////
  17 #ifndef datatype_Wff_defined
  18 #define datatype_Wff_defined
  19    class a_Wff;
  20    typedef a_Wff * Wff;
  21 #endif
  22
  23 #  define T (Wff)0
  24 #  define F (Wff)1
  25
  26 ///////////////////////////////////////////////////////////////////////////////
  27 //
  28 // Base class for datatype Wff
  29 //
  30 ///////////////////////////////////////////////////////////////////////////////
  31 class a_Wff : public GCObject {
  32 public:
  33    enum Tag_Wff {
  34       tag_VAR = 0, tag_NOT = 1, tag_AND = 2,
  35       tag_OR = 3
  36    };
  37
  38 public:
  39    const Tag_Wff tag__; // variant tag
  40 protected:
  41    inline a_Wff(Tag_Wff t__) : tag__(t__) {
  42 #line 9 "T11.pcc"
  43   cerr << "this";
  44 #line 9 "T11.pcc"
  45 }
  46 public:
  47    inline virtual ~a_Wff()
  48    {
  49
  50 #line 14 "T11.pcc"
  51      cerr << "~wff";
  52 #line 14 "T11.pcc"
  53    }
  54    ////////////////////////////////////////////////////////////////////////////
  55    //
  56    // Method for garbage collection tracing
  57    //
  58    ////////////////////////////////////////////////////////////////////////////
  59 protected:
  60    virtual void trace(GC *);
  61 public:
  62 };
  63 inline int boxed(const a_Wff * x) { return (unsigned long)x >= 2; }
  64 inline int untag(const a_Wff * x) { return boxed(x) ? x->tag__ + 2 : (int)x; }
  65 ///////////////////////////////////////////////////////////////////////////////
  66 //
  67 // Class for datatype constructor Wff::VAR
  68 //
  69 ///////////////////////////////////////////////////////////////////////////////
  70 class Wff_VAR : public a_Wff {
  71 public:
  72 #line 3 "T11.pcc"
  73    Quark VAR;
  74    inline Wff_VAR (Quark x_VAR)
  75     : a_Wff(tag_VAR), VAR(x_VAR)
  76    {
  77
  78 #line 10 "T11.pcc"
  79      cerr << "var";
  80 #line 10 "T11.pcc"
  81    }
  82    inline ~Wff_VAR()
  83    {
  84
  85 #line 15 "T11.pcc"
  86      cerr << "~var";
  87 #line 15 "T11.pcc"
  88    }
  89    ////////////////////////////////////////////////////////////////////////////
  90    //
  91    // Method for garbage collection tracing
  92    //
  93    ////////////////////////////////////////////////////////////////////////////
  94 protected:
  95    virtual void trace(GC *);
  96 public:
  97 };
  98
  99 ///////////////////////////////////////////////////////////////////////////////
 100 //
 101 // Class for datatype constructor Wff::NOT
 102 //
 103 ///////////////////////////////////////////////////////////////////////////////
 104 class Wff_NOT : public a_Wff {
 105 public:
 106 #line 4 "T11.pcc"
 107    Wff NOT;
 108    inline Wff_NOT (Wff x_NOT)
 109     : a_Wff(tag_NOT), NOT(x_NOT)
 110    {
 111
 112 #line 11 "T11.pcc"
 113      cerr << "not";
 114 #line 11 "T11.pcc"
 115    }
 116    inline ~Wff_NOT()
 117    {
 118
 119 #line 16 "T11.pcc"
 120      cerr << "~not";
 121 #line 16 "T11.pcc"
 122    }
 123    ////////////////////////////////////////////////////////////////////////////
 124    //
 125    // Method for garbage collection tracing
 126    //
 127    ////////////////////////////////////////////////////////////////////////////
 128 protected:
 129    virtual void trace(GC *);
 130 public:
 131 };
 132
 133 ///////////////////////////////////////////////////////////////////////////////
 134 //
 135 // Class for datatype constructor Wff::AND
 136 //
 137 ///////////////////////////////////////////////////////////////////////////////
 138 class Wff_AND : public a_Wff {
 139 public:
 140 #line 5 "T11.pcc"
 141    Wff _1; Wff _2;
 142    inline Wff_AND (Wff x_1, Wff x_2)
 143     : a_Wff(tag_AND), _1(x_1), _2(x_2)
 144    {
 145
 146 #line 12 "T11.pcc"
 147      cerr << "and";
 148 #line 12 "T11.pcc"
 149    }
 150    inline ~Wff_AND()
 151    {
 152
 153 #line 17 "T11.pcc"
 154      cerr << "~and";
 155 #line 17 "T11.pcc"
 156    }
 157    ////////////////////////////////////////////////////////////////////////////
 158    //
 159    // Method for garbage collection tracing
 160    //
 161    ////////////////////////////////////////////////////////////////////////////
 162 protected:
 163    virtual void trace(GC *);
 164 public:
 165 };
 166
 167 ///////////////////////////////////////////////////////////////////////////////
 168 //
 169 // Class for datatype constructor Wff::OR
 170 //
 171 ///////////////////////////////////////////////////////////////////////////////
 172 class Wff_OR : public a_Wff {
 173 public:
 174 #line 6 "T11.pcc"
 175    Wff _1; Wff _2;
 176    inline Wff_OR (Wff x_1, Wff x_2)
 177     : a_Wff(tag_OR), _1(x_1), _2(x_2)
 178    {
 179
 180 #line 13 "T11.pcc"
 181      cerr << "or";
 182 #line 13 "T11.pcc"
 183    }
 184    inline ~Wff_OR()
 185    {
 186
 187 #line 18 "T11.pcc"
 188      cerr << "~or";
 189 #line 18 "T11.pcc"
 190    }
 191    ////////////////////////////////////////////////////////////////////////////
 192    //
 193    // Method for garbage collection tracing
 194    //
 195    ////////////////////////////////////////////////////////////////////////////
 196 protected:
 197    virtual void trace(GC *);
 198 public:
 199 };
 200
 201 ///////////////////////////////////////////////////////////////////////////////
 202 //
 203 // Datatype constructor functions for Wff
 204 //
 205 ///////////////////////////////////////////////////////////////////////////////
 206 inline a_Wff * VAR (Quark x_VAR)
 207 {
 208    return new Wff_VAR (x_VAR);
 209 }
 210 inline a_Wff * NOT (Wff x_NOT)
 211 {
 212    return new Wff_NOT (x_NOT);
 213 }
 214 inline a_Wff * AND (Wff x_1, Wff x_2)
 215 {
 216    return new Wff_AND (x_1, x_2);
 217 }
 218 inline a_Wff * OR (Wff x_1, Wff x_2)
 219 {
 220    return new Wff_OR (x_1, x_2);
 221 }
 222 ///////////////////////////////////////////////////////////////////////////////
 223 //
 224 // Downcasting functions for Wff
 225 //
 226 ///////////////////////////////////////////////////////////////////////////////
 227 inline Wff_VAR * _VAR(const a_Wff * _x_) { return (Wff_VAR *)_x_; }
 228 inline Wff_NOT * _NOT(const a_Wff * _x_) { return (Wff_NOT *)_x_; }
 229 inline Wff_AND * _AND(const a_Wff * _x_) { return (Wff_AND *)_x_; }
 230 inline Wff_OR * _OR(const a_Wff * _x_) { return (Wff_OR *)_x_; }
 231
 232 #line 7 "T11.pcc"
 233 #line 7 "T11.pcc"
 234
 235
 236 #line 9 "T11.pcc"
 237 #line 18 "T11.pcc"
 238
 239
 240 #line 21 "T11.pcc"
 241 #line 21 "T11.pcc"
 242 ///////////////////////////////////////////////////////////////////////////////
 243 //
 244 // Interface specification of datatype Wff
 245 //
 246 ///////////////////////////////////////////////////////////////////////////////
 247 #line 21 "T11.pcc"
 248
 249
 250 ///////////////////////////////////////////////////////////////////////////////
 251 //
 252 // Instantiation of datatype Wff
 253 //
 254 ///////////////////////////////////////////////////////////////////////////////
 255 #line 21 "T11.pcc"
 256 void a_Wff::trace(GC * gc__)
 257 {
 258 }
 259
 260 void Wff_VAR::trace(GC * gc__)
 261 {
 262    // call to method a_Wff::trace() has been optimized out
 263    // omitted Quark
 264 }
 265
 266 void Wff_NOT::trace(GC * gc__)
 267 {
 268    // call to method a_Wff::trace() has been optimized out
 269    this->NOT = (Wff )gc__->trace(this->NOT); // Wff
 270 }
 271
 272 void Wff_AND::trace(GC * gc__)
 273 {
 274    // call to method a_Wff::trace() has been optimized out
 275    this->_1 = (Wff )gc__->trace(this->_1); // Wff
 276    this->_2 = (Wff )gc__->trace(this->_2); // Wff
 277 }
 278
 279 void Wff_OR::trace(GC * gc__)
 280 {
 281    // call to method a_Wff::trace() has been optimized out
 282    this->_1 = (Wff )gc__->trace(this->_1); // Wff
 283    this->_2 = (Wff )gc__->trace(this->_2); // Wff
 284 }
 285
 286
 287
 288 #line 21 "T11.pcc"
 289 #line 21 "T11.pcc"
 290
 291
 292 Wff dnf (Wff wff)
 293 {
 294
 295 #line 25 "T11.pcc"
 296 #line 44 "T11.pcc"
 297    extern void  _T_1_1co_X1_rewrite(Wff & );
 298    _T_1_1co_X1_rewrite(wff);
 299 #line 44 "T11.pcc"
 300 #line 44 "T11.pcc"
 301
 302    return wff;
 303 }
 304 #line 47 "T11.pcc"
 305 class _T_1_1co_X1 : public BURS {
 306 private:
 307    _T_1_1co_X1(const _T_1_1co_X1&);               // no copy constructor
 308    void operator = (const _T_1_1co_X1&); // no assignment
 309 public:
 310    struct _T_1_1co_X1_StateRec * stack__, * stack_top__;
 311 public:
 312    void labeler(const char *, int&, int);
 313    void labeler(Quark, int&, int);
 314           void  labeler(Wff & redex, int&, int);
 315    inline virtual void  operator () (Wff & redex) { int s; labeler(redex,s,0); }
 316 private:
 317    public:
 318       inline _T_1_1co_X1() {}
 319 };
 320 void  _T_1_1co_X1_rewrite(Wff &  _x_)
 321 {  _T_1_1co_X1 _r_;
 322    _r_(_x_);
 323 }
 324
 325 ///////////////////////////////////////////////////////////////////////////////
 326 //
 327 // This macro can be redefined by the user for debugging
 328 //
 329 ///////////////////////////////////////////////////////////////////////////////
 330 #ifndef DEBUG__T_1_1co_X1
 331 #define DEBUG__T_1_1co_X1(repl,redex,file,line,rule) repl
 332 #else
 333 static const char * _T_1_1co_X1_file_name = "T11.pcc";
 334 #endif
 335
 336 static const TreeTables::ShortState _T_1_1co_X1_theta_3[5] = {
 337    3, 6, 13, 24, 28
 338 };
 339
 340
 341 static const TreeTables::ShortState _T_1_1co_X1_theta_4[5][4] = {
 342    { 4, 7, 14, 29 },
 343    { 9, 8, 16, 33 },
 344    { 17, 18, 15, 32 },
 345    { 25, 27, 26, 31 },
 346    { 34, 36, 35, 30 }
 347 };
 348
 349
 350 static const TreeTables::ShortState _T_1_1co_X1_theta_5[4][3] = {
 351    { 5, 10, 19 },
 352    { 12, 11, 21 },
 353    { 22, 23, 20 },
 354    { 37, 39, 38 }
 355 };
 356
 357
 358 static const TreeTables::ShortState _T_1_1co_X1_mu_3_0[40] = {
 359    0, 1, 2, 3, 0, 4, 3, 0, 0, 0, 4, 4, 4, 3, 0, 0,
 360    0, 0, 0, 4, 4, 4, 4, 4, 3, 0, 0, 0, 3, 0, 0, 0,
 361    0, 0, 0, 0, 0, 4, 4, 4
 362 };
 363
 364
 365 static const TreeTables::ShortState _T_1_1co_X1_mu_4_0[40] = {
 366    0, 1, 2, 0, 3, 4, 0, 3, 3, 3, 4, 4, 4, 0, 3, 3,
 367    3, 3, 3, 4, 4, 4, 4, 4, 0, 3, 3, 3, 0, 3, 3, 3,
 368    3, 3, 3, 3, 3, 4, 4, 4
 369 };
 370
 371
 372 static const TreeTables::ShortState _T_1_1co_X1_mu_4_1[40] = {
 373    0, 1, 2, 0, 0, 3, 0, 0, 0, 0, 3, 3, 3, 0, 0, 0,
 374    0, 0, 0, 3, 3, 3, 3, 3, 0, 0, 0, 0, 0, 0, 0, 0,
 375    0, 0, 0, 0, 0, 3, 3, 3
 376 };
 377
 378
 379 static const TreeTables::ShortState _T_1_1co_X1_mu_5_0[40] = {
 380    0, 1, 2, 0, 0, 3, 0, 0, 0, 0, 3, 3, 3, 0, 0, 0,
 381    0, 0, 0, 3, 3, 3, 3, 3, 0, 0, 0, 0, 0, 0, 0, 0,
 382    0, 0, 0, 0, 0, 3, 3, 3
 383 };
 384
 385
 386 static const TreeTables::ShortState _T_1_1co_X1_mu_5_1[40] = {
 387    0, 1, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
 388    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
 389    0, 0, 0, 0, 0, 0, 0, 0
 390 };
 391
 392
 393 inline void  _T_1_1co_X1::labeler(char const * redex,int& s__,int)
 394 {
 395    {
 396 s__ = 0;
 397    }
 398 }
 399
 400 inline void  _T_1_1co_X1::labeler(Quark redex,int& s__,int)
 401 {
 402    {
 403 s__ = 0;
 404    }
 405 }
 406
 407 void  _T_1_1co_X1::labeler (Wff & redex, int& s__, int r__)
 408 {
 409 replacement__:
 410    if (boxed(redex)) {
 411       switch(redex->tag__) {
 412          case a_Wff::tag_VAR: {
 413             int s0__;
 414             labeler(_VAR(redex)->VAR, s0__, r__);
 415             s__ = 0;} break;
 416          case a_Wff::tag_NOT: {
 417             int s0__;
 418             labeler(_NOT(redex)->NOT, s0__, r__);
 419             s__ = _T_1_1co_X1_theta_3[_T_1_1co_X1_mu_3_0[s0__]]; } break;
 420          case a_Wff::tag_AND: {
 421             int s0__;
 422             int s1__;
 423             labeler(_AND(redex)->_1, s0__, r__);
 424             labeler(_AND(redex)->_2, s1__, r__);
 425             s__ = _T_1_1co_X1_theta_4[_T_1_1co_X1_mu_4_0[s0__]][_T_1_1co_X1_mu_4_1[s1__]]; } break;
 426          default: {
 427             int s0__;
 428             int s1__;
 429             labeler(_OR(redex)->_1, s0__, r__);
 430             labeler(_OR(redex)->_2, s1__, r__);
 431             s__ = _T_1_1co_X1_theta_5[_T_1_1co_X1_mu_5_0[s0__]][_T_1_1co_X1_mu_5_1[s1__]]; } break;
 432       }
 433    } else {
 434       if (((int)redex)) {s__ = 2;
 435       } else {s__ = 1;
 436       }
 437    }
 438    switch (s__) {
 439       case 25: {
 440 #line 43 "T11.pcc"
 441          { redex = DEBUG__T_1_1co_X1(AND(_AND(_AND(redex)->_1)->_1,AND(_AND(_AND(redex)->_1)->_2,_AND(redex)->_2)),redex,_T_1_1co_X1_file_name,43,"AND (AND (X, Y), Z): ...");
 442            r__ = 1; goto replacement__; }
 443 #line 44 "T11.pcc"
 444 } break;
 445       case 37: {
 446 #line 42 "T11.pcc"
 447          { redex = DEBUG__T_1_1co_X1(OR(_OR(_OR(redex)->_1)->_1,OR(_OR(_OR(redex)->_1)->_2,_OR(redex)->_2)),redex,_T_1_1co_X1_file_name,42,"OR (OR (X, Y), Z): ...");
 448            r__ = 1; goto replacement__; }
 449 #line 43 "T11.pcc"
 450 } break;
 451       case 31:
 452       case 29: {
 453 #line 41 "T11.pcc"
 454          { redex = DEBUG__T_1_1co_X1(OR(AND(_AND(redex)->_1,_OR(_AND(redex)->_2)->_1),AND(_AND(redex)->_1,_OR(_AND(redex)->_2)->_2)),redex,_T_1_1co_X1_file_name,41,"AND (X, OR (Y, Z)): ...");
 455            r__ = 1; goto replacement__; }
 456 #line 42 "T11.pcc"
 457 } break;
 458       case 34:
 459       case 30: {
 460 #line 40 "T11.pcc"
 461          { redex = DEBUG__T_1_1co_X1(OR(AND(_OR(_AND(redex)->_1)->_1,_AND(redex)->_2),AND(_OR(_AND(redex)->_1)->_2,_AND(redex)->_2)),redex,_T_1_1co_X1_file_name,40,"AND (OR (X, Y), Z): ...");
 462            r__ = 1; goto replacement__; }
 463 #line 41 "T11.pcc"
 464 } break;
 465       case 28: {
 466 #line 38 "T11.pcc"
 467          { redex = DEBUG__T_1_1co_X1(AND(NOT(_OR(_NOT(redex)->NOT)->_1),NOT(_OR(_NOT(redex)->NOT)->_2)),redex,_T_1_1co_X1_file_name,38,"NOT OR (X, Y): ...");
 468            r__ = 1; goto replacement__; }
 469 #line 40 "T11.pcc"
 470 } break;
 471       case 35:
 472       case 26:
 473       case 14: {
 474 #line 36 "T11.pcc"
 475          { redex = DEBUG__T_1_1co_X1(F,redex,_T_1_1co_X1_file_name,36,"AND (_, F): ...");
 476            r__ = 1; goto replacement__; }
 477 #line 38 "T11.pcc"
 478 } break;
 479       case 32:
 480       case 17:
 481       case 15: {
 482 #line 35 "T11.pcc"
 483          { redex = DEBUG__T_1_1co_X1(F,redex,_T_1_1co_X1_file_name,35,"AND (F, _): ...");
 484            r__ = 1; goto replacement__; }
 485 #line 36 "T11.pcc"
 486 } break;
 487       case 36:
 488       case 27:
 489       case 18:
 490       case 7: {
 491 #line 34 "T11.pcc"
 492          { redex = DEBUG__T_1_1co_X1(_AND(redex)->_1,redex,_T_1_1co_X1_file_name,34,"AND (X, T): ...");
 493            r__ = 1; goto replacement__; }
 494 #line 35 "T11.pcc"
 495 } break;
 496       case 33:
 497       case 16:
 498       case 9:
 499       case 8: {
 500 #line 33 "T11.pcc"
 501          { redex = DEBUG__T_1_1co_X1(_AND(redex)->_2,redex,_T_1_1co_X1_file_name,33,"AND (T, X): ...");
 502            r__ = 1; goto replacement__; }
 503 #line 34 "T11.pcc"
 504 } break;
 505       case 38:
 506       case 19: {
 507 #line 32 "T11.pcc"
 508          { redex = DEBUG__T_1_1co_X1(_OR(redex)->_1,redex,_T_1_1co_X1_file_name,32,"OR (X, F): ...");
 509            r__ = 1; goto replacement__; }
 510 #line 33 "T11.pcc"
 511 } break;
 512       case 22:
 513       case 20: {
 514 #line 31 "T11.pcc"
 515          { redex = DEBUG__T_1_1co_X1(_OR(redex)->_2,redex,_T_1_1co_X1_file_name,31,"OR (F, X): ...");
 516            r__ = 1; goto replacement__; }
 517 #line 32 "T11.pcc"
 518 } break;
 519       case 39:
 520       case 23:
 521       case 10: {
 522 #line 30 "T11.pcc"
 523          { redex = DEBUG__T_1_1co_X1(T,redex,_T_1_1co_X1_file_name,30,"OR (_, T): ...");
 524            r__ = 1; goto replacement__; }
 525 #line 31 "T11.pcc"
 526 } break;
 527       case 21:
 528       case 12:
 529       case 11: {
 530 #line 29 "T11.pcc"
 531          { redex = DEBUG__T_1_1co_X1(T,redex,_T_1_1co_X1_file_name,29,"OR (T, _): ...");
 532            r__ = 1; goto replacement__; }
 533 #line 30 "T11.pcc"
 534 } break;
 535       case 24: {
 536 #line 28 "T11.pcc"
 537          { redex = DEBUG__T_1_1co_X1(_NOT(_NOT(redex)->NOT)->NOT,redex,_T_1_1co_X1_file_name,28,"NOT NOT X: ...");
 538            r__ = 1; goto replacement__; }
 539 #line 29 "T11.pcc"
 540 } break;
 541       case 13: {
 542 #line 27 "T11.pcc"
 543          { redex = DEBUG__T_1_1co_X1(T,redex,_T_1_1co_X1_file_name,27,"NOT F: ...");
 544            r__ = 1; goto replacement__; }
 545 #line 28 "T11.pcc"
 546 } break;
 547       case 6: {
 548 #line 26 "T11.pcc"
 549          { redex = DEBUG__T_1_1co_X1(F,redex,_T_1_1co_X1_file_name,26,"NOT T: ...");
 550            r__ = 1; goto replacement__; }
 551 #line 27 "T11.pcc"
 552 } break;
 553    }
 554
 555 }
 556
 557 /*
 558 ------------------------------- Statistics -------------------------------
 559 Merge matching rules         = yes
 560 Number of DFA nodes merged   = 0
 561 Number of ifs generated      = 0
 562 Number of switches generated = 0
 563 Number of labels             = 0
 564 Number of gotos              = 0
 565 Adaptive matching            = disabled
 566 Fast string matching         = disabled
 567 Inline downcasts             = disabled
 568 --------------------------------------------------------------------------
 569 */