app/willard/querygraph.pcc

   1 #include <AD/pretty/postream.h>
   2 #include "querygraph.ph"
   3
   4 ///////////////////////////////////////////////////////////////////////////////
   5 //
   6 //  Constructor and destructor for query graph construction
   7 //
   8 ///////////////////////////////////////////////////////////////////////////////
   9 QueryGraphConstruction::QueryGraphConstruction() {}
  10 QueryGraphConstruction::~QueryGraphConstruction() {}
  11
  12 ///////////////////////////////////////////////////////////////////////////////
  13 //
  14 //  Method to invoke the query graph construction phase
  15 //
  16 ///////////////////////////////////////////////////////////////////////////////
  17 Exp QueryGraphConstruction::construct_query_graph(Exp e)
  18 {  message("Constructing the query graph", e);
  19    parent.clear();               // clears the query graph
  20    (*this)(e);                   // construct the graph
  21    compute_transitive_closure(); // compute the transitive closure
  22    print_query_graph();
  23    return e;
  24 }
  25
  26 ///////////////////////////////////////////////////////////////////////////////
  27 //
  28 //  Method to check whether a variable preceeds another in the quantifier
  29 //  ordering.
  30 //
  31 ///////////////////////////////////////////////////////////////////////////////
  32 Bool QueryGraphConstruction::preceeds(Id x, Id y) const
  33 {  for (int i = 0; i < quantifier_vars.size(); i++)
  34    {  if (quantifier_vars[i] == x)
  35       {  for (int j = i+1; j < quantifier_vars.size(); j++)
  36             if (quantifier_vars[j] == y) return true;
  37          return false;
  38       }
  39    }
  40    return false;
  41 }
  42
  43 ///////////////////////////////////////////////////////////////////////////////
  44 //
  45 //  Transformation rules
  46 //
  47 ///////////////////////////////////////////////////////////////////////////////
  48 rewrite QueryGraphConstruction
  49 {
  50
  51 //
  52 //  Push and pop quantifier names.
  53 //
  54 preorder:
  55   FORALL(x,_,_):      { push_quantifier(x); }
  56 | EXISTS(x,_,_):      { push_quantifier(x); }
  57 | GENERATOR(xs,_,_):  { push_quantifier(xs); }
  58
  59 postorder:
  60 | FORALL(x,_,_):      { pop_quantifier(x); }
  61 | EXISTS(x,_,_):      { pop_quantifier(x); }
  62 | GENERATOR(xs,_,_):  { pop_quantifier(xs); }
  63
  64   // Locate all atomic predicates and add edges into the query graph
  65 preorder:
  66 | OP("=" || "/=" || "<" || ">" || "<=" || ">=" || "#",es):
  67   {
  68      // Collect all free variables in this expression.
  69      IdSet S;
  70      free_vars(es,S);
  71
  72      // Now add edges to the query graph.
  73      foreach(i,S)
  74      {  Id x = S.value(i);
  75         foreach(j,S)
  76         {  Id y = S.value(j);
  77            if (x != y && preceeds(x,y)) add_edge(x,y);
  78         }
  79      }
  80   }
  81 };