prop-src/T7.cc

   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 ///////////////////////////////////////////////////////////////////////////////
   6
   7 #define PROP_REWRITING_USED
   8 #define PROP_QUARK_USED
   9 #include <propdefs.h>
  10 #line 7 "T7.pcc"
  11 ///////////////////////////////////////////////////////////////////////////////
  12 //
  13 // Forward class definition for Wff
  14 //
  15 ///////////////////////////////////////////////////////////////////////////////
  16 #ifndef datatype_Wff_defined
  17 #define datatype_Wff_defined
  18    class a_Wff;
  19    typedef a_Wff * Wff;
  20 #endif
  21
  22 #  define T (Wff)0
  23 #  define F (Wff)1
  24
  25 ///////////////////////////////////////////////////////////////////////////////
  26 //
  27 // Base class for datatype Wff
  28 //
  29 ///////////////////////////////////////////////////////////////////////////////
  30 class a_Wff : public TermObj {
  31 public:
  32    enum Tag_Wff {
  33       tag_VAR = 0, tag_NOT = 1, tag_AND = 2,
  34       tag_OR = 3
  35    };
  36
  37 public:
  38    const Tag_Wff tag__; // variant tag
  39 protected:
  40    inline a_Wff(Tag_Wff t__) : tag__(t__) {}
  41 public:
  42 };
  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 ///////////////////////////////////////////////////////////////////////////////
  46 //
  47 // Class for datatype constructor Wff::VAR
  48 //
  49 ///////////////////////////////////////////////////////////////////////////////
  50 class Wff_VAR : public a_Wff {
  51 public:
  52 #line 3 "T7.pcc"
  53    Quark VAR;
  54    inline Wff_VAR (Quark x_VAR)
  55     : a_Wff(tag_VAR), VAR(x_VAR)
  56    {
  57    }
  58 };
  59
  60 ///////////////////////////////////////////////////////////////////////////////
  61 //
  62 // Class for datatype constructor Wff::NOT
  63 //
  64 ///////////////////////////////////////////////////////////////////////////////
  65 class Wff_NOT : public a_Wff {
  66 public:
  67 #line 4 "T7.pcc"
  68    Wff NOT;
  69    inline Wff_NOT (Wff x_NOT)
  70     : a_Wff(tag_NOT), NOT(x_NOT)
  71    {
  72    }
  73 };
  74
  75 ///////////////////////////////////////////////////////////////////////////////
  76 //
  77 // Class for datatype constructor Wff::AND
  78 //
  79 ///////////////////////////////////////////////////////////////////////////////
  80 class Wff_AND : public a_Wff {
  81 public:
  82 #line 5 "T7.pcc"
  83    Wff _1; Wff _2;
  84    inline Wff_AND (Wff x_1, Wff x_2)
  85     : a_Wff(tag_AND), _1(x_1), _2(x_2)
  86    {
  87    }
  88 };
  89
  90 ///////////////////////////////////////////////////////////////////////////////
  91 //
  92 // Class for datatype constructor Wff::OR
  93 //
  94 ///////////////////////////////////////////////////////////////////////////////
  95 class Wff_OR : public a_Wff {
  96 public:
  97 #line 6 "T7.pcc"
  98    Wff _1; Wff _2;
  99    inline Wff_OR (Wff x_1, Wff x_2)
 100     : a_Wff(tag_OR), _1(x_1), _2(x_2)
 101    {
 102    }
 103 };
 104
 105 ///////////////////////////////////////////////////////////////////////////////
 106 //
 107 // Datatype constructor functions for Wff
 108 //
 109 ///////////////////////////////////////////////////////////////////////////////
 110 inline a_Wff * VAR (Quark x_VAR)
 111 {
 112    return new Wff_VAR (x_VAR);
 113 }
 114 inline a_Wff * NOT (Wff x_NOT)
 115 {
 116    return new Wff_NOT (x_NOT);
 117 }
 118 inline a_Wff * AND (Wff x_1, Wff x_2)
 119 {
 120    return new Wff_AND (x_1, x_2);
 121 }
 122 inline a_Wff * OR (Wff x_1, Wff x_2)
 123 {
 124    return new Wff_OR (x_1, x_2);
 125 }
 126 ///////////////////////////////////////////////////////////////////////////////
 127 //
 128 // Downcasting functions for Wff
 129 //
 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_; }
 135
 136 #line 7 "T7.pcc"
 137 #line 7 "T7.pcc"
 138
 139
 140 Wff dnf (Wff wff)
 141 {
 142
 143 #line 11 "T7.pcc"
 144 #line 30 "T7.pcc"
 145    extern void  _T_7co_X1_rewrite(Wff & );
 146    _T_7co_X1_rewrite(wff);
 147 #line 30 "T7.pcc"
 148 #line 30 "T7.pcc"
 149
 150    return wff;
 151 }
 152 #line 33 "T7.pcc"
 153 class _T_7co_X1 : public BURS {
 154 private:
 155    _T_7co_X1(const _T_7co_X1&);               // no copy constructor
 156    void operator = (const _T_7co_X1&); // no assignment
 157 public:
 158    struct _T_7co_X1_StateRec * stack__, * stack_top__;
 159 public:
 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); }
 164 private:
 165    public:
 166       inline _T_7co_X1() {}
 167 };
 168 void  _T_7co_X1_rewrite(Wff &  _x_)
 169 {  _T_7co_X1 _r_;
 170    _r_(_x_);
 171 }
 172
 173 ///////////////////////////////////////////////////////////////////////////////
 174 //
 175 // This macro can be redefined by the user for debugging
 176 //
 177 ///////////////////////////////////////////////////////////////////////////////
 178 #ifndef DEBUG__T_7co_X1
 179 #define DEBUG__T_7co_X1(repl,redex,file,line,rule) repl
 180 #else
 181 static const char * _T_7co_X1_file_name = "T7.pcc";
 182 #endif
 183
 184 static const TreeTables::ShortState _T_7co_X1_theta_3[5] = {
 185    3, 6, 13, 24, 28
 186 };
 187
 188
 189 static const TreeTables::ShortState _T_7co_X1_theta_4[5][4] = {
 190    { 4, 7, 14, 29 },
 191    { 9, 8, 16, 33 },
 192    { 17, 18, 15, 32 },
 193    { 25, 27, 26, 31 },
 194    { 34, 36, 35, 30 }
 195 };
 196
 197
 198 static const TreeTables::ShortState _T_7co_X1_theta_5[4][3] = {
 199    { 5, 10, 19 },
 200    { 12, 11, 21 },
 201    { 22, 23, 20 },
 202    { 37, 39, 38 }
 203 };
 204
 205
 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
 210 };
 211
 212
 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
 217 };
 218
 219
 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
 224 };
 225
 226
 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
 231 };
 232
 233
 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
 238 };
 239
 240
 241 inline void  _T_7co_X1::labeler(char const * redex,int& s__,int)
 242 {
 243    {
 244 s__ = 0;
 245    }
 246 }
 247
 248 inline void  _T_7co_X1::labeler(Quark redex,int& s__,int)
 249 {
 250    {
 251 s__ = 0;
 252    }
 253 }
 254
 255 void  _T_7co_X1::labeler (Wff & redex, int& s__, int r__)
 256 {
 257 replacement__:
 258    int cached__;
 259    if (r__ && boxed(redex) && (cached__ = redex->get_rewrite_state()) != BURS::undefined_state)
 260    { s__ = cached__; return; }
 261    if (boxed(redex)) {
 262       switch(redex->tag__) {
 263          case a_Wff::tag_VAR: {
 264             int s0__;
 265             labeler(_VAR(redex)->VAR, s0__, r__);
 266             s__ = 0;} break;
 267          case a_Wff::tag_NOT: {
 268             int s0__;
 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: {
 272             int s0__;
 273             int s1__;
 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;
 277          default: {
 278             int s0__;
 279             int s1__;
 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;
 283       }
 284    } else {
 285       if (((int)redex)) {s__ = 2;
 286       } else {s__ = 1;
 287       }
 288    }
 289    switch (s__) {
 290       case 25: {
 291 #line 29 "T7.pcc"
 292          Wff  repl__;
 293          Wff  _X3 = _AND(_AND(redex)->_1)->_2;
 294          int _X2 = boxed(_X3) ? _X3->get_rewrite_state() : ((int)_X3 + 0);
 295          switch (_X2) {
 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;
 297             default:
 298             repl__ = AND(_AND(_AND(redex)->_1)->_1,AND(_AND(_AND(redex)->_1)->_2,_AND(redex)->_2)); break;
 299          }
 300          { redex = DEBUG__T_7co_X1(repl__,redex,_T_7co_X1_file_name,29,"AND (AND (X, Y), Z): ...");
 301            r__ = 1; goto replacement__; }
 302 #line 30 "T7.pcc"
 303 } break;
 304       case 37: {
 305 #line 28 "T7.pcc"
 306          Wff  repl__;
 307          Wff  _X5 = _OR(_OR(redex)->_1)->_2;
 308          int _X4 = boxed(_X5) ? _X5->get_rewrite_state() : ((int)_X5 + 0);
 309          switch (_X4) {
 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;
 311             default:
 312             repl__ = OR(_OR(_OR(redex)->_1)->_1,OR(_OR(_OR(redex)->_1)->_2,_OR(redex)->_2)); break;
 313          }
 314          { redex = DEBUG__T_7co_X1(repl__,redex,_T_7co_X1_file_name,28,"OR (OR (X, Y), Z): ...");
 315            r__ = 1; goto replacement__; }
 316 #line 29 "T7.pcc"
 317 } break;
 318       case 31:
 319       case 29: {
 320 #line 27 "T7.pcc"
 321          Wff  repl__;
 322          Wff  _X7 = _AND(redex)->_1;
 323          int _X6 = boxed(_X7) ? _X7->get_rewrite_state() : ((int)_X7 + 0);
 324          switch (_X6) {
 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;
 326             default:
 327             Wff  _X9 = _OR(_AND(redex)->_2)->_2;
 328             int _X8 = boxed(_X9) ? _X9->get_rewrite_state() : ((int)_X9 + 0);
 329             switch (_X8) {
 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;
 331                default:
 332                repl__ = OR(AND(_AND(redex)->_1,_OR(_AND(redex)->_2)->_1),AND(_AND(redex)->_1,_OR(_AND(redex)->_2)->_2)); break;
 333             }
 334          }
 335          { redex = DEBUG__T_7co_X1(repl__,redex,_T_7co_X1_file_name,27,"AND (X, OR (Y, Z)): ...");
 336            r__ = 1; goto replacement__; }
 337 #line 28 "T7.pcc"
 338 } break;
 339       case 34:
 340       case 30: {
 341 #line 26 "T7.pcc"
 342          Wff  repl__;
 343          Wff  _X11 = _OR(_AND(redex)->_1)->_1;
 344          int _X10 = boxed(_X11) ? _X11->get_rewrite_state() : ((int)_X11 + 0);
 345          switch (_X10) {
 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;
 347             default:
 348             Wff  _X13 = _OR(_AND(redex)->_1)->_2;
 349             int _X12 = boxed(_X13) ? _X13->get_rewrite_state() : ((int)_X13 + 0);
 350             switch (_X12) {
 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;
 353                default:
 354                Wff  _X15 = _AND(redex)->_2;
 355                int _X14 = boxed(_X15) ? _X15->get_rewrite_state() : ((int)_X15 + 0);
 356                switch (_X14) {
 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;
 358                   default:
 359                   repl__ = OR(AND(_OR(_AND(redex)->_1)->_1,_AND(redex)->_2),AND(_OR(_AND(redex)->_1)->_2,_AND(redex)->_2)); break;
 360                }
 361             }
 362          }
 363          { redex = DEBUG__T_7co_X1(repl__,redex,_T_7co_X1_file_name,26,"AND (OR (X, Y), Z): ...");
 364            r__ = 1; goto replacement__; }
 365 #line 27 "T7.pcc"
 366 } break;
 367       case 28: {
 368 #line 24 "T7.pcc"
 369          Wff  repl__;
 370          Wff  _X17 = _OR(_NOT(redex)->NOT)->_1;
 371          int _X16 = boxed(_X17) ? _X17->get_rewrite_state() : ((int)_X17 + 0);
 372          switch (_X16) {
 373             case 3: repl__ = AND(_NOT(_OR(_NOT(redex)->NOT)->_1)->NOT,NOT(_OR(_NOT(redex)->NOT)->_2)); break;
 374             default:
 375             Wff  _X19 = _OR(_NOT(redex)->NOT)->_2;
 376             int _X18 = boxed(_X19) ? _X19->get_rewrite_state() : ((int)_X19 + 0);
 377             switch (_X18) {
 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;
 380                default:
 381                repl__ = AND(NOT(_OR(_NOT(redex)->NOT)->_1),NOT(_OR(_NOT(redex)->NOT)->_2)); break;
 382             }
 383          }
 384          { redex = DEBUG__T_7co_X1(repl__,redex,_T_7co_X1_file_name,24,"NOT OR (X, Y): ...");
 385            r__ = 1; goto replacement__; }
 386 #line 26 "T7.pcc"
 387 } break;
 388       case 35:
 389       case 26:
 390       case 14: {
 391 #line 22 "T7.pcc"
 392          { redex = DEBUG__T_7co_X1(F,redex,_T_7co_X1_file_name,22,"AND (_, F): ...");
 393            r__ = 1; goto replacement__; }
 394 #line 24 "T7.pcc"
 395 } break;
 396       case 32:
 397       case 17:
 398       case 15: {
 399 #line 21 "T7.pcc"
 400          { redex = DEBUG__T_7co_X1(F,redex,_T_7co_X1_file_name,21,"AND (F, _): ...");
 401            r__ = 1; goto replacement__; }
 402 #line 22 "T7.pcc"
 403 } break;
 404       case 36:
 405       case 27:
 406       case 18:
 407       case 7: {
 408 #line 20 "T7.pcc"
 409          { redex = DEBUG__T_7co_X1(_AND(redex)->_1,redex,_T_7co_X1_file_name,20,"AND (X, T): ...");
 410            r__ = 1; goto replacement__; }
 411 #line 21 "T7.pcc"
 412 } break;
 413       case 33:
 414       case 16:
 415       case 9:
 416       case 8: {
 417 #line 19 "T7.pcc"
 418          { redex = DEBUG__T_7co_X1(_AND(redex)->_2,redex,_T_7co_X1_file_name,19,"AND (T, X): ...");
 419            r__ = 1; goto replacement__; }
 420 #line 20 "T7.pcc"
 421 } break;
 422       case 38:
 423       case 19: {
 424 #line 18 "T7.pcc"
 425          { redex = DEBUG__T_7co_X1(_OR(redex)->_1,redex,_T_7co_X1_file_name,18,"OR (X, F): ...");
 426            r__ = 1; goto replacement__; }
 427 #line 19 "T7.pcc"
 428 } break;
 429       case 22:
 430       case 20: {
 431 #line 17 "T7.pcc"
 432          { redex = DEBUG__T_7co_X1(_OR(redex)->_2,redex,_T_7co_X1_file_name,17,"OR (F, X): ...");
 433            r__ = 1; goto replacement__; }
 434 #line 18 "T7.pcc"
 435 } break;
 436       case 39:
 437       case 23:
 438       case 10: {
 439 #line 16 "T7.pcc"
 440          { redex = DEBUG__T_7co_X1(T,redex,_T_7co_X1_file_name,16,"OR (_, T): ...");
 441            r__ = 1; goto replacement__; }
 442 #line 17 "T7.pcc"
 443 } break;
 444       case 21:
 445       case 12:
 446       case 11: {
 447 #line 15 "T7.pcc"
 448          { redex = DEBUG__T_7co_X1(T,redex,_T_7co_X1_file_name,15,"OR (T, _): ...");
 449            r__ = 1; goto replacement__; }
 450 #line 16 "T7.pcc"
 451 } break;
 452       case 24: {
 453 #line 14 "T7.pcc"
 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__; }
 456 #line 15 "T7.pcc"
 457 } break;
 458       case 13: {
 459 #line 13 "T7.pcc"
 460          { redex = DEBUG__T_7co_X1(T,redex,_T_7co_X1_file_name,13,"NOT F: ...");
 461            r__ = 1; goto replacement__; }
 462 #line 14 "T7.pcc"
 463 } break;
 464       case 6: {
 465 #line 12 "T7.pcc"
 466          { redex = DEBUG__T_7co_X1(F,redex,_T_7co_X1_file_name,12,"NOT T: ...");
 467            r__ = 1; goto replacement__; }
 468 #line 13 "T7.pcc"
 469 } break;
 470    }
 471    if (boxed(redex)) {
 472       redex->set_rewrite_state(s__);
 473    }
 474
 475 }
 476
 477 /*
 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
 483 Number of labels             = 0
 484 Number of gotos              = 0
 485 Adaptive matching            = disabled
 486 Fast string matching         = disabled
 487 Inline downcasts             = disabled
 488 --------------------------------------------------------------------------
 489 */