app/willard/phase2.pcc

   1 #include <AD/pretty/postream.h>
   2 #include "phase2.ph"
   3 #include "list.ph"
   4
   5 ///////////////////////////////////////////////////////////////////////////////
   6 //
   7 //  Constructor and destructor for phase2
   8 //
   9 ///////////////////////////////////////////////////////////////////////////////
  10 Phase2::Phase2() {}
  11 Phase2::~Phase2() {}
  12
  13 ///////////////////////////////////////////////////////////////////////////////
  14 //
  15 //  Method to invoke phase2
  16 //
  17 ///////////////////////////////////////////////////////////////////////////////
  18 Exp Phase2::phase2(Exp e)
  19 {  message("Quantifier elimination phase", e);
  20    (*this)(e);
  21    return collect_subqueries(e);
  22 }
  23
  24 ///////////////////////////////////////////////////////////////////////////////
  25 //
  26 //  Transformation to eliminate existential quantifiers
  27 //  by transforming them into count queries.
  28 //
  29 ///////////////////////////////////////////////////////////////////////////////
  30 rewrite Phase2
  31 {
  32 //
  33 // Locate all existential quantifiers.
  34 //
  35    EXISTS(x,A,p):
  36    {  IdSet S;
  37       free_vars(p,S);
  38
  39       // Transform: exists x : A . p  where x does not occur in p
  40       // into:      #A > 0 and p
  41       if (! S.contains(x)) { rewrite(And(Nonempty(A),p)); }
  42
  43       // Transform: exists x : A . p(x)
  44       // into: #C > 0
  45       //       where C = { x : A | p(x) }
  46       if (S.size() == 1)
  47       {  Id C = gensym("C");
  48          Exp find_query = GENERATOR(#[x],#[A],GUARD(p,ID(x)));
  49          add_subquery(C,find_query);
  50          rewrite(Nonempty(ID(C)));
  51       }
  52
  53       //  Transform: exists x : A . p(x,y)
  54       //  into:   C(y)
  55       //          where C = { [y, #{ [y,x] : x in A | p(x,y)}] : y in B }
  56       if (S.size() == 2)
  57       {  Id C = gensym("C");
  58          Id y = "???";
  59          foreach(i,S) if (S.value(i) != x) y = S.value(i);
  60          Exp B = range_of(y);
  61          Exp count_query =
  62             GENERATOR(#[y],#[B],
  63                TUPLE(#[ID(y),
  64                   Count(
  65                      GENERATOR(#[x],#[A],
  66                         GUARD(p,TUPLE(#[ID(y),ID(x)]))))]));
  67          add_subquery(C,count_query);
  68          rewrite(Gt(APP(C,#[ID(y)]),Zero));
  69       }
  70
  71       // Arity is not zero or one
  72       error("Cannot simplify quantifier",redex);
  73    }
  74
  75 //
  76 // Also simplify all negated relational operator.
  77 //
  78 |  Not(Eq(a,b)):  Ne(a,b)
  79 |  Not(Ne(a,b)):  Eq(a,b)
  80 |  Not(Gt(a,b)):  Le(a,b)
  81 |  Not(Ge(a,b)):  Lt(a,b)
  82 |  Not(Lt(a,b)):  Ge(a,b)
  83 |  Not(Le(a,b)):  Gt(a,b)
  84
  85 //
  86 // Flatten into DNF form
  87 //
  88 |  And(Or(a,b),c):  Or(And(a,c),And(b,c))
  89 |  And(a,Or(b,c)):  Or(And(a,b),And(a,c))
  90 |  Not(And(a,b)):   Or(Not(a),Not(b))
  91 |  Not(Or(a,b)):    And(Not(a),Not(b))
  92 |  Not(Not(a)):     a
  93 |  Or(Or(a,b),c):   Or(a,Or(b,c))
  94
  95 |  GENERATOR(x,A,GENERATOR(y,B,C)): GENERATOR(append(x,y),append(A,B),C)
  96 |  GENERATOR(x,A,GUARD(p as Nonempty(C),E)):
  97       GUARD(p,GENERATOR(x,A,E))
  98 |  GENERATOR(x,A,GUARD(And(p1 as Nonempty(C),p2),E)):
  99       GUARD(p1,GENERATOR(x,A,GUARD(p2,E)))
 100 |  GENERATOR(x,A,GUARD(True,E)): GENERATOR(x,A,E)
 101 |  GENERATOR(#[x],#[A],ID y) | x == y: A
 102 |  GUARD(p1,GUARD(p2,E)): GUARD(And(p1,p2),E)
 103
 104 //
 105 //  Collect subqueries generated
 106 //
 107 postorder:
 108 |  LET(x,A,B) | has_subqueries(): collect_subqueries(redex)
 109 };