app/willard/paige.ph

   1 #ifndef paige_doyal_h
   2 #define paige_doyal_h
   3
   4 #include <AD/pretty/postream.h>
   5 #include <AD/contain/varstack.h>
   6 #include "willard-ast.ph"
   7 #include "idset.h"
   8 #include "smap.h"
   9
  10 class ostream;
  11
  12 ///////////////////////////////////////////////////////////////////////////////
  13 //
  14 //   This class implements the transformation algorithm as developed by
  15 //   Bob Paige and Deepak Goyal.
  16 //
  17 ///////////////////////////////////////////////////////////////////////////////
  18 class PaigeGoyal
  19 {  PaigeGoyal(const PaigeGoyal&);
  20    void operator = (const PaigeGoyal&);
  21
  22    ////////////////////////////////////////////////////////////////////////////
  23    //
  24    //  Internal data
  25    //
  26    ////////////////////////////////////////////////////////////////////////////
  27 protected:
  28    PrettyOStream    log, errlog; // pretty printing stream for message logging
  29    int              new_name;    // counter for new names
  30    Ids              subquery_names; // set of subqueries currently generated.
  31    Exps             subqueries;  // set of subqueries currently generated.
  32    SMap<Id,Exp>     var_range;   // record the range of each variable
  33    SMap<Id,Id>      parent;      // the query graph:
  34                                  //   mapping from child to parent
  35    SMap<Id,Id>      parent_closure; // the query graph (in closure form):
  36    SMap<.[Id,Id],Exp> edge_queries; // mapping from edge (x,y) to query Q(x,y)
  37    VarStack<Id> quantifier_vars;    // quantifier vars currently in scope
  38 protected:
  39
  40    ////////////////////////////////////////////////////////////////////////////
  41    //
  42    // Internal methods
  43    //
  44    ////////////////////////////////////////////////////////////////////////////
  45
  46    ////////////////////////////////////////////////////////////////////////////
  47    // Common predefined constants
  48    ////////////////////////////////////////////////////////////////////////////
  49    Exp True, False, Zero, One, Two, EmptySet;
  50
  51    ////////////////////////////////////////////////////////////////////////////
  52    // Methods to construct the query graph
  53    ////////////////////////////////////////////////////////////////////////////
  54    void add_edge(Id x, Id y);
  55    Bool has_edge(Id x, Id y) const;
  56    void add_edge_query(Id x, Id y, Exp query);
  57    void compute_transitive_closure();
  58    void print_query_graph();
  59
  60    ////////////////////////////////////////////////////////////////////////////
  61    // Methods to collect free variables in an expression.
  62    ////////////////////////////////////////////////////////////////////////////
  63    void free_vars(Ids,  IdSet&) const;
  64    void free_vars(Exp,  IdSet&) const;
  65    void free_vars(Exps, IdSet&) const;
  66    void remove_vars (IdSet&, Ids) const;
  67    void remove_vars (IdSet&, const IdSet&) const;
  68
  69    ////////////////////////////////////////////////////////////////////////////
  70    // Is x free in e?
  71    ////////////////////////////////////////////////////////////////////////////
  72    Bool is_free(Id x, Exp e) const;
  73    Bool is_free(Ids xs, Exp e) const;
  74
  75    ////////////////////////////////////////////////////////////////////////////
  76    // Methods to generate new names
  77    ////////////////////////////////////////////////////////////////////////////
  78    Id gensym();
  79    Id gensym(Id prefix);
  80
  81    ////////////////////////////////////////////////////////////////////////////
  82    // Methods to generate and collect subqueries
  83    ////////////////////////////////////////////////////////////////////////////
  84    void add_subquery(Id, Exp);
  85    Exp collect_subqueries(Exp);
  86    Bool has_subqueries() const;
  87
  88    ////////////////////////////////////////////////////////////////////////////
  89    // Method to record the range of each variable.
  90    ////////////////////////////////////////////////////////////////////////////
  91    void define_range(Id, Exp);
  92    void define_range(Ids, Exps);
  93    Exp  range_of(Id);
  94
  95    ////////////////////////////////////////////////////////////////////////////
  96    // Methods to push/pop from the quantifier stack
  97    ////////////////////////////////////////////////////////////////////////////
  98    void push_quantifier(Id x);
  99    void push_quantifier(Ids xs);
 100    void pop_quantifier(Id x);
 101    void pop_quantifier(Ids xs);
 102
 103    ////////////////////////////////////////////////////////////////////////////
 104    // Set by subclasses if re-iteration of the transformation process
 105    // is required.
 106    ////////////////////////////////////////////////////////////////////////////
 107    Bool changed;
 108
 109    ////////////////////////////////////////////////////////////////////////////
 110    // Method to create a nested let
 111    ////////////////////////////////////////////////////////////////////////////
 112 public:
 113    static Exp make_let(Ids, Exps, Exp);
 114 public:
 115             PaigeGoyal();
 116    virtual ~PaigeGoyal();
 117
 118    ////////////////////////////////////////////////////////////////////////////
 119    // Main decomposition method
 120    ////////////////////////////////////////////////////////////////////////////
 121    virtual Exp decompose(Exp);
 122
 123    ////////////////////////////////////////////////////////////////////////////
 124    // Method to print messages
 125    ////////////////////////////////////////////////////////////////////////////
 126    void message(const char * mesg, Exp e);
 127    void error(const char * mesg, Exp e);
 128    void set_log  (ostream&);
 129    void set_error(ostream&);
 130 protected:
 131
 132    ////////////////////////////////////////////////////////////////////////////
 133    // The following are the different phases implemented in subclasses.
 134    ////////////////////////////////////////////////////////////////////////////
 135    virtual Exp remove_duplicate_names(Exp) = 0;
 136    virtual Exp construct_query_graph(Exp) = 0; // query graph construction
 137    virtual Exp projection_recognition(Exp) = 0;
 138    virtual Exp phase1(Exp) = 0;  // DNF construction
 139    virtual Exp phase2(Exp) = 0;  // quantifier elimination
 140    virtual Exp phase3(Exp) = 0;  // disjunction removal
 141    virtual Exp phase4(Exp) = 0;  // join decomposition
 142    virtual Exp phase5(Exp) = 0;  // simple count/find query decomposition
 143 };
 144
 145 #endif