app/willard/phase2.cc

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //  This file is generated automatically using Prop (version 2.3.5),
   3 //  last updated on Jun 18, 1997.
   4 //  The original source file is "phase2.pcc".
   5 ///////////////////////////////////////////////////////////////////////////////
   6
   7 #define PROP_REWRITING_USED
   8 #define PROP_STRCMP_USED
   9 #define PROP_QUARK_USED
  10 #define PROP_TUPLE2_USED
  11 #include <propdefs.h>
  12 #line 1 "phase2.pcc"
  13 #include <AD/pretty/postream.h>
  14 #include "phase2.h"
  15 #include "list.h"
  16
  17 ///////////////////////////////////////////////////////////////////////////////
  18 //
  19 //  Constructor and destructor for phase2
  20 //
  21 ///////////////////////////////////////////////////////////////////////////////
  22 Phase2::Phase2() {}
  23 Phase2::~Phase2() {}
  24
  25 ///////////////////////////////////////////////////////////////////////////////
  26 //
  27 //  Method to invoke phase2
  28 //
  29 ///////////////////////////////////////////////////////////////////////////////
  30 Exp Phase2::phase2(Exp e)
  31 {  message("Quantifier elimination phase", e);
  32    (*this)(e);
  33    return collect_subqueries(e);
  34 }
  35
  36 ///////////////////////////////////////////////////////////////////////////////
  37 //
  38 //  Transformation to eliminate existential quantifiers
  39 //  by transforming them into count queries.
  40 //
  41 ///////////////////////////////////////////////////////////////////////////////
  42 #line 30 "phase2.pcc"
  43 #line 109 "phase2.pcc"
  44 ///////////////////////////////////////////////////////////////////////////////
  45 //
  46 // This macro can be redefined by the user for debugging
  47 //
  48 ///////////////////////////////////////////////////////////////////////////////
  49 #ifndef DEBUG_Phase2
  50 #define DEBUG_Phase2(repl,redex,file,line,rule) repl
  51 #else
  52 static const char * Phase2_file_name = "phase2.pcc";
  53 #endif
  54
  55 static const TreeTables::Offset Phase2_accept_base [ 73 ] = {
  56    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 2,
  57    2, 2, 2, 2, 3, 5, 6, 6, 6, 7, 8, 8, 9, 10, 11, 12,
  58    12, 12, 12, 12, 12, 12, 12, 12, 12, 13, 15, 16, 17, 18, 18, 18,
  59    18, 18, 18, 18, 18, 18, 18, 19, 21, 23, 25, 26, 26, 26, 27, 29,
  60    31, 33, 35, 37, 39, 41, 43, 45, 48
  61 };
  62 static const TreeTables::ShortRule Phase2_accept_vector [ 50 ] = {
  63    -1, 0, -1, 18, -1, 13, -1, 17, -1, 18, -1, 18, -1, 16, -1, 14,
  64    -1, 11, -1, 18, -1, 12, -1, 7, -1, 10, -1, 9, -1, 6, -1, 5,
  65    -1, 4, -1, 3, -1, 2, -1, 1, -1, 15, -1, 8, -1, 7, 8, -1,
  66    8, -1
  67 };
  68 static const TreeTables::ShortState Phase2_theta_1[1][2] = {
  69    { 0, 18 }
  70 };
  71
  72
  73 static const TreeTables::ShortState Phase2_theta_2[11][17] = {
  74    { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
  75    0 },
  76    { 0, 24, 0, 0, 44, 0, 58, 62, 63, 64, 65, 66, 67, 68, 0, 0,
  77    0 },
  78    { 0, 0, 40, 40, 0, 40, 0, 0, 0, 0, 0, 0, 0, 0, 40, 40,
  79    40 },
  80    { 0, 0, 39, 39, 0, 39, 0, 0, 0, 0, 0, 0, 0, 0, 39, 39,
  81    39 },
  82    { 0, 0, 38, 38, 0, 38, 0, 0, 0, 0, 0, 0, 0, 0, 38, 38,
  83    38 },
  84    { 0, 0, 37, 37, 0, 37, 0, 0, 0, 0, 0, 0, 0, 0, 37, 37,
  85    37 },
  86    { 0, 0, 36, 36, 0, 36, 0, 0, 0, 0, 0, 0, 0, 0, 36, 36,
  87    36 },
  88    { 0, 0, 35, 35, 0, 35, 0, 0, 0, 0, 0, 0, 0, 0, 35, 35,
  89    35 },
  90    { 0, 0, 34, 43, 0, 57, 0, 0, 0, 0, 0, 0, 0, 0, 70, 71,
  91    72 },
  92    { 0, 0, 33, 33, 0, 56, 0, 0, 0, 0, 0, 0, 0, 0, 33, 56,
  93    33 },
  94    { 0, 23, 0, 0, 23, 0, 23, 23, 23, 23, 23, 23, 23, 23, 0, 0,
  95    0 }
  96 };
  97
  98
  99 static const TreeTables::ShortState Phase2_theta_4[2] = {
 100    0, 22
 101 };
 102
 103
 104 static const TreeTables::ShortState Phase2_theta_9[5][2] = {
 105    { 15, 20 },
 106    { 27, 28 },
 107    { 29, 30 },
 108    { 54, 55 },
 109    { 54, 55 }
 110 };
 111
 112
 113 static const TreeTables::ShortState Phase2_theta_10[2][2][9] = {
 114    { { 16, 16, 21, 41, 41, 42, 42, 69, 69 },
 115    { 16, 16, 21, 41, 41, 42, 42, 69, 69 } },
 116    { { 16, 16, 21, 41, 41, 42, 42, 69, 69 },
 117    { 16, 25, 21, 41, 41, 42, 42, 69, 69 } }
 118 };
 119
 120
 121 static const TreeTables::ShortState Phase2_theta_13[11][4] = {
 122    { 0, 19, 26, 59 },
 123    { 0, 19, 31, 61 },
 124    { 0, 32, 26, 59 },
 125    { 0, 46, 45, 60 },
 126    { 0, 47, 26, 59 },
 127    { 0, 48, 26, 59 },
 128    { 0, 49, 26, 59 },
 129    { 0, 50, 26, 59 },
 130    { 0, 51, 26, 59 },
 131    { 0, 52, 26, 59 },
 132    { 0, 53, 26, 59 }
 133 };
 134
 135
 136 static const TreeTables::ShortState Phase2_check [ 174 ] = {
 137    0, 2, 0, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 0, 0, 11,
 138    0, 5, 12, 4, 11, 0, 10, 10, 0, 0, 4, 11, 11, 11, 11, 4,
 139    4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 4, 4, 4,
 140    4, 4, 4, 4, 4, 4, 11, 11, 13, 0, 0, 4, 4, 4, 0, 14,
 141    0, 0, 14, 0, 0, 13, 0, 14, 10, 0, 0, 14, 0, 14, 14, 14,
 142    14, 0, 0, 13, 13, 13, 13, 13, 13, 13, 13, 14, 14, 0, 0, 0,
 143    15, 15, 0, 0, 0, 0, 0, 16, 14, 14, 15, 15, 15, 15, 15, 15,
 144    15, 15, 0, 0, 15, 15, 0, 14, 16, 0, 0, 0, 0, 0, 0, 0,
 145    0, 15, 15, 15, 0, 16, 0, 15, 15, 15, 15, 15, 15, 15, 0, 15,
 146    15, 15, 0, 16, 16, 16, 16, 16, 16, 16, 16, 0, 0, 0, 0, 0,
 147    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
 148 };
 149 TreeTables::ShortState Phase2_next [ 174 ] = {
 150    0, 1, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 0, 0, 1,
 151    0, 1, 1, 1, 1, 0, 1, 2, 0, 0, 2, 1, 1, 1, 1, 3,
 152    4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 5, 6, 7,
 153    8, 9, 10, 11, 12, 13, 1, 1, 1, 0, 0, 14, 15, 16, 0, 1,
 154    0, 0, 2, 0, 0, 1, 0, 2, 4, 0, 0, 2, 0, 3, 4, 5,
 155    6, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 0, 0, 0,
 156    1, 2, 0, 0, 0, 0, 0, 1, 7, 8, 3, 4, 5, 6, 7, 8,
 157    9, 10, 0, 0, 4, 2, 0, 2, 2, 0, 0, 0, 0, 0, 0, 0,
 158    0, 3, 4, 2, 0, 2, 0, 2, 2, 2, 2, 2, 2, 2, 0, 4,
 159    4, 4, 0, 3, 2, 2, 2, 2, 2, 2, 2, 0, 0, 0, 0, 0,
 160    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
 161 };
 162 inline void  Phase2::labeler(char const * redex,int& s__,int)
 163 {
 164    {
 165       if (_less_string(redex,">=")) {
 166          if (_less_string(redex,"=")) {
 167             if (_equal_string(redex,"/=")) {s__ = 5;}
 168             else if (_equal_string(redex,"<")) {s__ = 8;}
 169             else if (_equal_string(redex,"<=")) {s__ = 9;}
 170             else {s__ = 0;}
 171          } else {
 172             if (_equal_string(redex,"=")) {s__ = 4;}
 173             else if (_equal_string(redex,">")) {s__ = 6;}
 174             else {s__ = 0;}
 175          }
 176       } else {
 177          if (_less_string(redex,"not")) {
 178             if (_equal_string(redex,">=")) {s__ = 7;}
 179             else if (_equal_string(redex,"and")) {s__ = 10;}
 180             else if (_equal_string(redex,"nonempty")) {s__ = 12;}
 181             else {s__ = 0;}
 182          } else {
 183             if (_equal_string(redex,"not")) {s__ = 3;}
 184             else if (_equal_string(redex,"or")) {s__ = 11;}
 185             else {s__ = 0;}
 186          }
 187       }
 188    }
 189 }
 190
 191 inline void  Phase2::labeler(Quark redex,int& s__,int)
 192 {
 193    {
 194 s__ = 0;
 195    }
 196 }
 197
 198 void  Phase2::labeler (Exp & redex, int& s__, int r__)
 199 {
 200 replacement__:
 201    int cached__;
 202    if (r__ && boxed(redex) && (cached__ = redex->get_rewrite_state()) != BURS::undefined_state)
 203    { s__ = cached__; return; }
 204    switch(redex->tag__) {
 205       case a_Exp::tag_OP: {
 206          int s0__;
 207          int s1__;
 208          labeler(_OP(redex)->_1, s0__, r__);
 209          labeler(_OP(redex)->_2, s1__, r__);
 210          s__ = Phase2_theta_2[Phase2_check[0 + s0__] == 3 ? Phase2_next[0 + s0__] : 0][Phase2_check[0 + s1__] == 4 ? Phase2_next[0 + s1__] : 0]; } break;
 211       case a_Exp::tag_APP: {
 212          int s0__;
 213          int s1__;
 214          labeler(_APP(redex)->_1, s0__, r__);
 215          labeler(_APP(redex)->_2, s1__, r__);
 216          s__ = 0;} break;
 217       case a_Exp::tag_LIT: {
 218          int s0__;
 219          labeler(_LIT(redex)->LIT, s0__, r__);
 220          s__ = Phase2_theta_4[Phase2_check[0 + s0__] == 5 ? Phase2_next[0 + s0__] : 0]; } break;
 221       case a_Exp::tag_ID: {
 222          int s0__;
 223          labeler(_ID(redex)->ID, s0__, r__);
 224          s__ = 13;} break;
 225       case a_Exp::tag_TUPLE: {
 226          int s0__;
 227          labeler(_TUPLE(redex)->TUPLE, s0__, r__);
 228          s__ = 0;} break;
 229       case a_Exp::tag_FORALL: {
 230          int s0__;
 231          int s1__;
 232          int s2__;
 233          labeler(_FORALL(redex)->_1, s0__, r__);
 234          labeler(_FORALL(redex)->_2, s1__, r__);
 235          labeler(_FORALL(redex)->_3, s2__, r__);
 236          s__ = 0;} break;
 237       case a_Exp::tag_EXISTS: {
 238          int s0__;
 239          int s1__;
 240          int s2__;
 241          labeler(_EXISTS(redex)->_1, s0__, r__);
 242          labeler(_EXISTS(redex)->_2, s1__, r__);
 243          labeler(_EXISTS(redex)->_3, s2__, r__);
 244          s__ = 14;} break;
 245       case a_Exp::tag_GUARD: {
 246          int s0__;
 247          int s1__;
 248          labeler(_GUARD(redex)->_1, s0__, r__);
 249          labeler(_GUARD(redex)->_2, s1__, r__);
 250          s__ = Phase2_theta_9[Phase2_check[0 + s0__] == 10 ? Phase2_next[0 + s0__] : 0][Phase2_check[0 + s1__] == 11 ? Phase2_next[0 + s1__] : 0]; } break;
 251       case a_Exp::tag_GENERATOR: {
 252          int s0__;
 253          int s1__;
 254          int s2__;
 255          labeler(_GENERATOR(redex)->_1, s0__, r__);
 256          labeler(_GENERATOR(redex)->_2, s1__, r__);
 257          labeler(_GENERATOR(redex)->_3, s2__, r__);
 258          s__ = Phase2_theta_10[Phase2_check[0 + s0__] == 12 ? Phase2_next[0 + s0__] : 0][Phase2_check[37 + s1__] == 13 ? Phase2_next[37 + s1__] : 0][Phase2_check[50 + s2__] == 14 ? Phase2_next[50 + s2__] : 0]; } break;
 259       default: {
 260          int s0__;
 261          int s1__;
 262          int s2__;
 263          labeler(_LET(redex)->_1, s0__, r__);
 264          labeler(_LET(redex)->_2, s1__, r__);
 265          labeler(_LET(redex)->_3, s2__, r__);
 266          s__ = 0;} break;
 267    }
 268    const TreeTables::ShortRule * o__ = Phase2_accept_vector + Phase2_accept_base[s__];
 269 accept__:
 270    switch (*o__) {
 271       case 18: {
 272 #line 102 "phase2.pcc"
 273          { redex = DEBUG_Phase2(GUARD(And(_GUARD(redex)->_1,_GUARD(_GUARD(redex)->_2)->_1),_GUARD(_GUARD(redex)->_2)->_2),redex,Phase2_file_name,102,"GUARD (p1, GUARD (p2, E)): ...");
 274            r__ = 1; goto replacement__; }
 275 #line 107 "phase2.pcc"
 276 } break;
 277       case 17: if ((_GENERATOR(redex)->_1->_1 == _ID(_GENERATOR(redex)->_3)->ID))
 278       {
 279 #line 101 "phase2.pcc"
 280          { redex = DEBUG_Phase2(_GENERATOR(redex)->_2->_1,redex,Phase2_file_name,101,"GENERATOR (#[x], #[A], ID y) | (redex!GENERATOR.1!#[...].1 == redex!GENERATOR.3!ID): ...");
 281            r__ = 1; goto replacement__; }
 282 #line 102 "phase2.pcc"
 283 }
 284       else { ++o__; goto accept__; } break;
 285       case 16: if ((_BOOL(_LIT(_GUARD(_GENERATOR(redex)->_3)->_1)->LIT)->BOOL == true))
 286       {
 287 #line 100 "phase2.pcc"
 288          { redex = DEBUG_Phase2(GENERATOR(_GENERATOR(redex)->_1,_GENERATOR(redex)->_2,_GUARD(_GENERATOR(redex)->_3)->_2),redex,Phase2_file_name,100,"GENERATOR (x, A, GUARD (LIT BOOL _, E)) | (redex!GENERATOR.3!GUARD.1!LIT!BOOL == true): ...");
 289            r__ = 1; goto replacement__; }
 290 #line 101 "phase2.pcc"
 291 }
 292       else { ++o__; goto accept__; } break;
 293       case 15: {
 294 #line 98 "phase2.pcc"
 295          { redex = DEBUG_Phase2(GUARD(_OP(_GUARD(_GENERATOR(redex)->_3)->_1)->_2->_1,GENERATOR(_GENERATOR(redex)->_1,_GENERATOR(redex)->_2,GUARD(_OP(_GUARD(_GENERATOR(redex)->_3)->_1)->_2->_2->_1,_GUARD(_GENERATOR(redex)->_3)->_2))),redex,Phase2_file_name,98,"GENERATOR (x, A, GUARD (OP (\"and\", #[p1 as OP (\"nonempty\", #[C]), p2]), E)): ...");
 296            r__ = 1; goto replacement__; }
 297 #line 100 "phase2.pcc"
 298 } break;
 299       case 14: {
 300 #line 96 "phase2.pcc"
 301          { redex = DEBUG_Phase2(GUARD(_GUARD(_GENERATOR(redex)->_3)->_1,GENERATOR(_GENERATOR(redex)->_1,_GENERATOR(redex)->_2,_GUARD(_GENERATOR(redex)->_3)->_2)),redex,Phase2_file_name,96,"GENERATOR (x, A, GUARD (p as OP (\"nonempty\", #[C]), E)): ...");
 302            r__ = 1; goto replacement__; }
 303 #line 98 "phase2.pcc"
 304 } break;
 305       case 13: {
 306 #line 95 "phase2.pcc"
 307          { redex = DEBUG_Phase2(GENERATOR(append(_GENERATOR(redex)->_1,_GENERATOR(_GENERATOR(redex)->_3)->_1),append(_GENERATOR(redex)->_2,_GENERATOR(_GENERATOR(redex)->_3)->_2),_GENERATOR(_GENERATOR(redex)->_3)->_3),redex,Phase2_file_name,95,"GENERATOR (x, A, GENERATOR (y, B, C)): ...");
 308            r__ = 1; goto replacement__; }
 309 #line 96 "phase2.pcc"
 310 } break;
 311       case 12: {
 312 #line 93 "phase2.pcc"
 313          { redex = DEBUG_Phase2(Or(_OP(_OP(redex)->_2->_1)->_2->_1,Or(_OP(_OP(redex)->_2->_1)->_2->_2->_1,_OP(redex)->_2->_2->_1)),redex,Phase2_file_name,93,"OP (\"or\", #[OP (\"or\", #[a, b]), c]): ...");
 314            r__ = 1; goto replacement__; }
 315 #line 95 "phase2.pcc"
 316 } break;
 317       case 11: {
 318 #line 92 "phase2.pcc"
 319          { redex = DEBUG_Phase2(_OP(_OP(redex)->_2->_1)->_2->_1,redex,Phase2_file_name,92,"OP (\"not\", #[OP (\"not\", #[a])]): ...");
 320            r__ = 1; goto replacement__; }
 321 #line 93 "phase2.pcc"
 322 } break;
 323       case 10: {
 324 #line 91 "phase2.pcc"
 325          { redex = DEBUG_Phase2(And(Not(_OP(_OP(redex)->_2->_1)->_2->_1),Not(_OP(_OP(redex)->_2->_1)->_2->_2->_1)),redex,Phase2_file_name,91,"OP (\"not\", #[OP (\"or\", #[a, b])]): ...");
 326            r__ = 1; goto replacement__; }
 327 #line 92 "phase2.pcc"
 328 } break;
 329       case 9: {
 330 #line 90 "phase2.pcc"
 331          { redex = DEBUG_Phase2(Or(Not(_OP(_OP(redex)->_2->_1)->_2->_1),Not(_OP(_OP(redex)->_2->_1)->_2->_2->_1)),redex,Phase2_file_name,90,"OP (\"not\", #[OP (\"and\", #[a, b])]): ...");
 332            r__ = 1; goto replacement__; }
 333 #line 91 "phase2.pcc"
 334 } break;
 335       case 8: {
 336 #line 89 "phase2.pcc"
 337          { redex = DEBUG_Phase2(Or(And(_OP(redex)->_2->_1,_OP(_OP(redex)->_2->_2->_1)->_2->_1),And(_OP(redex)->_2->_1,_OP(_OP(redex)->_2->_2->_1)->_2->_2->_1)),redex,Phase2_file_name,89,"OP (\"and\", #[a, OP (\"or\", #[b, c])]): ...");
 338            r__ = 1; goto replacement__; }
 339 #line 90 "phase2.pcc"
 340 } break;
 341       case 7: {
 342 #line 88 "phase2.pcc"
 343          { redex = DEBUG_Phase2(Or(And(_OP(_OP(redex)->_2->_1)->_2->_1,_OP(redex)->_2->_2->_1),And(_OP(_OP(redex)->_2->_1)->_2->_2->_1,_OP(redex)->_2->_2->_1)),redex,Phase2_file_name,88,"OP (\"and\", #[OP (\"or\", #[a, b]), c]): ...");
 344            r__ = 1; goto replacement__; }
 345 #line 89 "phase2.pcc"
 346 } break;
 347       case 6: {
 348 #line 83 "phase2.pcc"
 349          { redex = DEBUG_Phase2(Gt(_OP(_OP(redex)->_2->_1)->_2->_1,_OP(_OP(redex)->_2->_1)->_2->_2->_1),redex,Phase2_file_name,83,"OP (\"not\", #[OP (\"<=\", #[a, b])]): ...");
 350            r__ = 1; goto replacement__; }
 351 #line 88 "phase2.pcc"
 352 } break;
 353       case 5: {
 354 #line 82 "phase2.pcc"
 355          { redex = DEBUG_Phase2(Ge(_OP(_OP(redex)->_2->_1)->_2->_1,_OP(_OP(redex)->_2->_1)->_2->_2->_1),redex,Phase2_file_name,82,"OP (\"not\", #[OP (\"<\", #[a, b])]): ...");
 356            r__ = 1; goto replacement__; }
 357 #line 83 "phase2.pcc"
 358 } break;
 359       case 4: {
 360 #line 81 "phase2.pcc"
 361          { redex = DEBUG_Phase2(Lt(_OP(_OP(redex)->_2->_1)->_2->_1,_OP(_OP(redex)->_2->_1)->_2->_2->_1),redex,Phase2_file_name,81,"OP (\"not\", #[OP (\">=\", #[a, b])]): ...");
 362            r__ = 1; goto replacement__; }
 363 #line 82 "phase2.pcc"
 364 } break;
 365       case 3: {
 366 #line 80 "phase2.pcc"
 367          { redex = DEBUG_Phase2(Le(_OP(_OP(redex)->_2->_1)->_2->_1,_OP(_OP(redex)->_2->_1)->_2->_2->_1),redex,Phase2_file_name,80,"OP (\"not\", #[OP (\">\", #[a, b])]): ...");
 368            r__ = 1; goto replacement__; }
 369 #line 81 "phase2.pcc"
 370 } break;
 371       case 2: {
 372 #line 79 "phase2.pcc"
 373          { redex = DEBUG_Phase2(Eq(_OP(_OP(redex)->_2->_1)->_2->_1,_OP(_OP(redex)->_2->_1)->_2->_2->_1),redex,Phase2_file_name,79,"OP (\"not\", #[OP (\"/=\", #[a, b])]): ...");
 374            r__ = 1; goto replacement__; }
 375 #line 80 "phase2.pcc"
 376 } break;
 377       case 1: {
 378 #line 78 "phase2.pcc"
 379          { redex = DEBUG_Phase2(Ne(_OP(_OP(redex)->_2->_1)->_2->_1,_OP(_OP(redex)->_2->_1)->_2->_2->_1),redex,Phase2_file_name,78,"OP (\"not\", #[OP (\"=\", #[a, b])]): ...");
 380            r__ = 1; goto replacement__; }
 381 #line 79 "phase2.pcc"
 382 } break;
 383       case 0: {
 384 #line 36 "phase2.pcc"
 385        IdSet S;
 386          free_vars(_EXISTS(redex)->_3,S);
 387
 388          // Transform: exists x : A . p  where x does not occur in p
 389          // into:      #A > 0 and p
 390          if (! S.contains(_EXISTS(redex)->_1)) {
 391 #line 41 "phase2.pcc"
 392 #line 41 "phase2.pcc"
 393          { redex = DEBUG_Phase2(And(Nonempty(_EXISTS(redex)->_2),_EXISTS(redex)->_3),redex,Phase2_file_name,35,"EXISTS (x, A, p): ...");
 394            r__ = 1; goto replacement__; }
 395 #line 41 "phase2.pcc"
 396 #line 41 "phase2.pcc"
 397         }
 398
 399                // Transform: exists x : A . p(x)
 400                // into: #C > 0
 401                //       where C = { x : A | p(x) }
 402                if (S.size() == 1)
 403                {  Id C = gensym("C");
 404                  Exp find_query = GENERATOR(
 405 #line 48 "phase2.pcc"
 406 #line 48 "phase2.pcc"
 407          list_1_(_EXISTS(redex)->_1)
 408 #line 48 "phase2.pcc"
 409 #line 48 "phase2.pcc"
 410          ,
 411 #line 48 "phase2.pcc"
 412 #line 48 "phase2.pcc"
 413          list_1_(_EXISTS(redex)->_2)
 414 #line 48 "phase2.pcc"
 415 #line 48 "phase2.pcc"
 416          ,GUARD(_EXISTS(redex)->_3,ID(_EXISTS(redex)->_1)));
 417                  add_subquery(C,find_query);
 418
 419 #line 50 "phase2.pcc"
 420 #line 50 "phase2.pcc"
 421          { redex = DEBUG_Phase2(Nonempty(ID(C)),redex,Phase2_file_name,35,"EXISTS (x, A, p): ...");
 422            r__ = 1; goto replacement__; }
 423 #line 50 "phase2.pcc"
 424 #line 50 "phase2.pcc"
 425
 426          }
 427
 428          //  Transform: exists x : A . p(x,y)
 429          //  into:   C(y)
 430          //          where C = { [y, #{ [y,x] : x in A | p(x,y)}] : y in B }
 431          if (S.size() == 2)
 432          {  Id C = gensym("C");
 433                  Id y = "???";
 434                  foreach(i,S) if (S.value(i) != _EXISTS(redex)->_1) y = S.value(i);
 435                  Exp B = range_of(y);
 436             Exp count_query =
 437                     GENERATOR(
 438 #line 62 "phase2.pcc"
 439 #line 62 "phase2.pcc"
 440          list_1_(y)
 441 #line 62 "phase2.pcc"
 442 #line 62 "phase2.pcc"
 443          ,
 444 #line 62 "phase2.pcc"
 445 #line 62 "phase2.pcc"
 446          list_1_(B)
 447 #line 62 "phase2.pcc"
 448 #line 62 "phase2.pcc"
 449          ,
 450                        TUPLE(
 451 #line 63 "phase2.pcc"
 452 #line 63 "phase2.pcc"
 453          list_1_(ID(y),list_1_(Count(GENERATOR(list_1_(_EXISTS(redex)->_1),list_1_(_EXISTS(redex)->_2),GUARD(_EXISTS(redex)->_3,TUPLE(list_1_(ID(y),list_1_(ID(_EXISTS(redex)->_1)))))))))
 454 #line 66 "phase2.pcc"
 455 #line 66 "phase2.pcc"
 456          ));
 457          add_subquery(C,count_query);
 458
 459 #line 68 "phase2.pcc"
 460 #line 68 "phase2.pcc"
 461          { redex = DEBUG_Phase2(Gt(APP(C,list_1_(ID(y))),Zero),redex,Phase2_file_name,35,"EXISTS (x, A, p): ...");
 462            r__ = 1; goto replacement__; }
 463 #line 68 "phase2.pcc"
 464 #line 68 "phase2.pcc"
 465
 466          }
 467
 468          // Arity is not zero or one
 469          error("Cannot simplify quantifier",redex);
 470
 471 #line 73 "phase2.pcc"
 472 } break;
 473    }
 474    if (boxed(redex)) {
 475       redex->set_rewrite_state(s__);
 476    }
 477    {
 478       switch (redex->tag__) {
 479          case a_Exp::tag_LET: {
 480             if (
 481 #line 108 "phase2.pcc"
 482             has_subqueries()
 483 #line 108 "phase2.pcc"
 484 ) {
 485
 486 #line 108 "phase2.pcc"
 487                { redex = DEBUG_Phase2(collect_subqueries(redex),redex,Phase2_file_name,108,"LET (x, A, B) | has_subqueries(): ...");
 488                  r__ = 1; goto replacement__; }
 489 #line 109 "phase2.pcc"
 490             } else {
 491                }
 492             } break;
 493          default: {} break;
 494       }
 495    }
 496
 497 }
 498
 499 void  Phase2::labeler (Literal & redex, int& s__, int r__)
 500 {
 501 replacement__:
 502    switch(redex->tag__) {
 503       case a_Literal::tag_INT: {
 504          int s0__;
 505          s0__ = 0; // int
 506          s__ = 0;} break;
 507       case a_Literal::tag_STRING: {
 508          int s0__;
 509          labeler(_STRING(redex)->STRING, s0__, r__);
 510          s__ = 0;} break;
 511       default: {
 512          int s0__;
 513          s0__ = 0; // Bool
 514          s__ = 17;} break;
 515    }
 516
 517 }
 518
 519 void  Phase2::labeler (a_List<Exp> *  & redex, int& s__, int r__)
 520 {
 521 replacement__:
 522    if ((redex)) {
 523       int s0__;
 524       int s1__;
 525       labeler(redex->_1, s0__, r__);
 526       labeler(redex->_2, s1__, r__);
 527       s__ = Phase2_theta_13[Phase2_check[73 + s0__] == 15 ? Phase2_next[73 + s0__] : 0][Phase2_check[101 + s1__] == 16 ? Phase2_next[101 + s1__] : 0];
 528    } else {s__ = 2;
 529    }
 530
 531 }
 532
 533 void  Phase2::labeler (a_List<Id> *  & redex, int& s__, int r__)
 534 {
 535 replacement__:
 536    if ((redex)) {
 537       int s0__;
 538       int s1__;
 539       labeler(redex->_1, s0__, r__);
 540       labeler(redex->_2, s1__, r__);
 541       s__ = Phase2_theta_1[0][Phase2_check[0 + s1__] == 2 ? Phase2_next[0 + s1__] : 0];
 542    } else {s__ = 1;
 543    }
 544
 545 }
 546
 547 #line 109 "phase2.pcc"
 548 #line 109 "phase2.pcc"
 549
 550 #line 110 "phase2.pcc"
 551 /*
 552 ------------------------------- Statistics -------------------------------
 553 Merge matching rules         = yes
 554 Number of DFA nodes merged   = 10
 555 Number of ifs generated      = 14
 556 Number of switches generated = 1
 557 Number of labels             = 0
 558 Number of gotos              = 0
 559 Adaptive matching            = disabled
 560 Fast string matching         = disabled
 561 Inline downcasts             = disabled
 562 --------------------------------------------------------------------------
 563 */