src/baseparsuif/suifmath/named_lin_ineq.h

   1 /* file "named_lin_ineq.h" */
   2
   3 /*  Copyright (c) 1994 Stanford University
   4
   5     All rights reserved.
   6
   7     This software is provided under the terms described in
   8     the "suif_copyright.h" include file. */
   9
  10 #include <suif_copyright.h>
  11
  12 #pragma interface
  13
  14 #ifndef NAMED_LIN_INEQ_H
  15 #define NAMED_LIN_INEQ_H
  16
  17 enum name_table_entry_kind { nte_none,
  18                              nte_symconst,
  19                              nte_cond,
  20                              nte_loop,
  21                              nte_dim,
  22                              nte_summary,
  23                              nte_aux };
  24
  25 class array_info;
  26 class access_vector;
  27
  28 /**************************************************************************
  29  ***                                                                    ***
  30  *** The name of each column.                                           ***
  31  ***                                                                    ***
  32  **************************************************************************/
  33 class name_table_entry {
  34 friend class name_table;
  35     name_table_entry_kind knd;
  36     union {
  37         var_sym * v;
  38         const char * s;
  39     } vsname;
  40     boolean is_var;
  41
  42 public:
  43     name_table_entry()                          { init(); }
  44     name_table_entry(const immed & im)          { init(im); }
  45     name_table_entry(name_table_entry_kind k,
  46                      const immed & nm)          { init(k, nm); }
  47     ~name_table_entry();
  48
  49     void init()                                 { knd = nte_none;
  50                                                   is_var = FALSE;
  51                                                   vsname.s = NULL;
  52                                               }
  53     void init(const immed &);
  54     void init(name_table_entry_kind k, const immed & nm);
  55     void init(const name_table_entry &);
  56     void operator=(const name_table_entry &nte) { init(nte); };
  57
  58     immed name() const;
  59     const char * string() const;
  60     var_sym * var() const                       { assert(is_var);
  61                                                   return vsname.v;
  62                                               }
  63
  64     void set_name(const immed &);
  65
  66     name_table_entry_kind kind() const         { return knd; }
  67
  68     void mark_sym();
  69     void mark_cond();
  70     void mark_loop();
  71     void mark_dim();
  72     void mark_summary();
  73     void mark_aux();
  74
  75     boolean operator==(const name_table_entry & nte) const;
  76     boolean operator!=(const name_table_entry & nte) const
  77       { return !(*this == nte); }
  78
  79     base_symtab * get_symtab(base_symtab * in = NULL) const;
  80
  81     void print(FILE * fp=stdout) const;
  82 };
  83
  84
  85 /**************************************************************************
  86  ***                                                                    ***
  87  *** A list of names identifying all the column.                        ***
  88  ***                                                                    ***
  89  *** The 0th column is for the constant, thus does not have a name.     ***
  90  *** All the other columns will be named by entries in the table        ***
  91  ***                                                                    ***
  92  **************************************************************************/
  93 class name_table {
  94     name_table_entry * L;
  95     int sz;
  96     int rsz;
  97     void resize(int newsz);
  98 public:
  99     name_table()                                { L = NULL; sz = 1; rsz = 1; }
 100     name_table(const name_table * nt)           { L = NULL; sz = 1; rsz = 1; init(*nt); }
 101     name_table(const name_table & nt)           { L = NULL; sz = 1; rsz = 1; init(nt); }
 102     name_table(int s)                           { L = NULL; sz = 1; rsz = 1; init(s); }
 103     name_table(const immed * v1,        const immed * v2 =NULL,
 104                const immed * v3 =NULL,  const immed * v4 =NULL,
 105                const immed * v5 =NULL,  const immed * v6 =NULL,
 106                const immed * v7 =NULL,  const immed * v8 =NULL,
 107                const immed * v9 =NULL,  const immed * v10=NULL,
 108                const immed * v11=NULL,  const immed * v12=NULL,
 109                const immed * v13=NULL,  const immed * v14=NULL,
 110                const immed * v15=NULL,  const immed * v16=NULL);
 111     ~name_table();
 112     void init(const name_table &);
 113     void init(int s);
 114
 115     name_table &operator=(const name_table &other);
 116
 117     int n() const                               { return sz; }
 118     name_table_entry & operator[](int i)        { assert((i>=1)&&(i<sz));
 119                                                   return L[i-1]; }
 120     const name_table_entry & e(int i) const     { assert((i>=1)&&(i<sz));
 121                                                   return L[i-1]; }
 122
 123     int find(const name_table_entry &) const;
 124     int find(const immed & vs) const;
 125
 126     void remove(int i, int j);
 127     void remove(int i)                          { remove(i, i); }
 128     void remove(const integer_row &rem);
 129     void insert(const name_table_entry & nte, int i);
 130     void insert(const immed & v, int i);
 131
 132     name_table operator&(const name_table &) const;    // merge 2 name tables;
 133     name_table & operator&=(const name_table &);  // merge with other;
 134
 135     // reorders the table so element kind ordering matches historical ordering;
 136     // sets ca so that new[ca[i]] = old[i];
 137     // returns TRUE if table order is changed;
 138     boolean do_reorder_table(integer_row &ca);
 139
 140     // changes ntes occurring in both tables to sync their kinds;
 141     static void change_name_types(name_table & A,
 142                                   name_table & B);
 143
 144     // are tables aligned and ordered?;
 145     static boolean is_aligned(const name_table & A,
 146                               const name_table & B);
 147
 148     // makes a table ret aligning elts of na and nb, reordered;
 149     static name_table * mk_align(const name_table & na, const name_table & nb);
 150
 151     // makes a table ret aligning elts of na and nb, reordered;
 152     // and sets ca and cb;
 153     // so that ret[ca[i]]==na[i] and ret[cb[i]]==nb[i];
 154     static name_table * align_tables(const name_table &na,
 155                                      const name_table &nb,
 156                                      integer_row & ca, integer_row & cb);
 157     // aligns this with nb, reorders, and sets ca and cb so that;
 158     // so that this[ca[i]]==oldthis[i] and this[cb[i]]==nb[i];
 159     void align_with(const name_table &nb,
 160                     integer_row & ca, integer_row & cb);
 161
 162     constraint lio_code_type() const;
 163
 164     base_symtab * get_symtab(base_symtab * in = NULL) const;
 165
 166     void print(FILE * fp=stdout) const;
 167     void print_symtabs(FILE * fp=stdout) const;
 168 };
 169
 170
 171 enum print_exp_type { pet_single, pet_system, pet_system_nl, pet_max, pet_min, pet_expr, pet_expr_nl};
 172
 173 /**************************************************************************
 174  ***                                                                    ***
 175  *** System of linear inequalities with names associated with           ***
 176  *** each column.                                                       ***
 177  ***                                                                    ***
 178  **************************************************************************/
 179 class named_lin_ineq {
 180 friend class named_lin_ineq_list;
 181     int unum;
 182     static int unum_cnt;
 183     name_table nt;
 184     lin_ineq   lq;
 185 public:
 186     named_lin_ineq() : lq(0, 1)                 { init(); }
 187     named_lin_ineq(const named_lin_ineq & c)    { init(); init(c);  }
 188     named_lin_ineq(const named_lin_ineq * c)    { init(); init(*c); }
 189     named_lin_ineq(const immed_list & il)       { init(); init(il); }
 190     named_lin_ineq(int m, int n) : nt(n),lq(m, n) { init(); }
 191     named_lin_ineq(const name_table &n,
 192                    const lin_ineq &l)           { init();
 193                                                   nt.init(n);
 194                                                   lq = l;
 195                                                 }
 196     ~named_lin_ineq();
 197 private:
 198     void init();
 199 public:
 200     void init(const named_lin_ineq & c);
 201     void init(int m, int n);
 202     int init(const immed_list & il, int c=0);
 203     immed_list * cvt_immed_list() const;
 204
 205     int uid() const { return unum; }
 206
 207     name_table & names()                        { return nt; }
 208     lin_ineq   & ineqs()                        { return lq; }
 209
 210     const name_table & const_names() const      { return nt; }
 211     const lin_ineq   & const_ineqs() const      { return lq; }
 212
 213
 214     int n() const                               { assert(nt.n() == lq.n());
 215                                                   return nt.n(); }
 216     int m() const                               { return lq.m(); }
 217
 218     void swap_col(int i, int j);
 219     void add_col(const name_table_entry & nte, int i);
 220     void del_col(int i, int j);
 221     void del_col(int i)                         { del_col(i, i); }
 222     void del_col(const integer_row &);
 223
 224     int find(const immed & v) const          { return const_names().find(v); }
 225
 226     void project();
 227     void project_away(const immed &, int *changed=0);
 228     void project_away(const name_table &, int *changed=0);
 229
 230     named_lin_ineq & operator=(const named_lin_ineq & c);
 231     named_lin_ineq & operator=(const lin_ineq & l);
 232
 233     named_lin_ineq operator&(const named_lin_ineq & c) const;
 234     named_lin_ineq & operator&=(const named_lin_ineq & c);
 235     named_lin_ineq & operator&=(const lin_ineq & l);
 236     // treats 0 as TRUE; returns 0 if c1==c2==0;
 237     // deletes or returns c{1,2} if del{1,2};
 238     static named_lin_ineq * and2(named_lin_ineq * c1,
 239                                  named_lin_ineq * c2,
 240                                  boolean del1=FALSE,
 241                                  boolean del2=FALSE);
 242     boolean operator==(const named_lin_ineq & c2) const;
 243     boolean operator>=(const named_lin_ineq & c2) const;
 244     boolean operator<=(const named_lin_ineq & c2) const
 245         { return (c2 >= (*this)); };
 246     boolean operator~() const;
 247
 248     /* saman compatibility */
 249     boolean operator>>(const named_lin_ineq & c2) const
 250         { return (*this >= c2); };
 251     boolean operator<<(const named_lin_ineq & c2) const
 252       { return (c2 >> (*this)); }
 253     // aligns tables and reorders them;
 254     void operator||(named_lin_ineq & c) { align_with(c); };
 255     /* end saman compatibility */
 256
 257     // a simple substitution method
 258     // This is a cheap alternative to expensive Fourier-Motzkin
 259     // substitution expression given in expr is of the form
 260     //var >= sub_expr and var <= sub_expr or
 261     // sub_expr >= 0
 262     named_lin_ineq * substitute(const immed & var, const named_lin_ineq & expr)
 263             const;
 264     void do_substitute(const immed & var, const named_lin_ineq & expr);
 265
 266     // do all sorts of fm-pairwise projection;
 267     void find_bounds();
 268
 269     void cleanup(); // does simple cleanup;
 270     // returns true for no-soln sys after cleanup();
 271     boolean is_clean_false() const;
 272     void del_zero_cols();
 273
 274     void simplify(); // does somewhat more work to cleanup;
 275
 276     void print(FILE *fp = stdout) const;
 277     void print_exp(print_exp_type tp=pet_single, FILE *fp = stdout) const;
 278
 279     instruction * mk_bounds() const;
 280     instruction * create_expression(const immed & v,
 281                                     boolean is_ub,
 282                                     block_symtab * sym=NULL) const;
 283
 284
 285     // NEED TO LINK LIBDEPENDENCE TO USE THIS FUNCTION
 286     static named_lin_ineq * mk_named_lin_ineq(array_info & ai,
 287                                               immed ind,
 288                                               boolean lb);
 289     // NEED TO LINK LIBDEPENDENCE TO USE THIS FUNCTION
 290     static named_lin_ineq * mk_named_lin_ineq(access_vector & av,
 291                                               immed ind,
 292                                               boolean lb);
 293
 294     // reorders the table so element kind ordering matches historical ordering;
 295     // if ca, then sets ca so that new[*ca[i]] = old[i];
 296     void do_reorder_table(integer_row *ca=0);
 297
 298     // aligns tables and reorders them;
 299     static void align_named_lin_ineqs(named_lin_ineq & A,
 300                                       named_lin_ineq & B);
 301     // aligns tables and reorders them;
 302     void align_with(named_lin_ineq &B);
 303
 304     // aligns this table with nt; does not reorder;
 305     void align(const name_table & nt);
 306
 307     // aligns tables, maximizing congruence of aux variables;
 308     // may alter systems;  returns number of auxes merged;
 309     int merge_auxes(named_lin_ineq &c2);
 310
 311     static boolean is_aligned(const named_lin_ineq & A,
 312                               const named_lin_ineq & B);
 313
 314     static named_lin_ineq * merge_named_lin_ineqs(const named_lin_ineq & A,
 315                                                   const named_lin_ineq & B);
 316 };
 317
 318 typedef named_lin_ineq * p_named_lin_ineq;
 319
 320 // NEED TO LINK LIBDEPENDENCE TO USE THIS FUNCTION
 321 named_lin_ineq * include_for(tree_for * tf,
 322                              named_lin_ineq * c = NULL);
 323
 324 #endif