diff options
Diffstat (limited to 'omega/code_gen/src/output_repr.cc')
| -rw-r--r-- | omega/code_gen/src/output_repr.cc | 1931 |
1 files changed, 1931 insertions, 0 deletions
diff --git a/omega/code_gen/src/output_repr.cc b/omega/code_gen/src/output_repr.cc new file mode 100644 index 0000000..955cc14 --- /dev/null +++ b/omega/code_gen/src/output_repr.cc @@ -0,0 +1,1931 @@ +/***************************************************************************** + Copyright (C) 1994-2000 University of Maryland + Copyright (C) 2008 University of Southern California + Copyright (C) 2009-2010 University of Utah + All Rights Reserved. + + Purpose: + utility functions for outputing CG_outputReprs + + Notes: + + History: + 07/30/10 collect various code outputing into one place, by Chun Chen +*****************************************************************************/ + +#include <omega.h> +#include <code_gen/CG_stringBuilder.h> +#include <code_gen/output_repr.h> +#include <basic/omega_error.h> +#include <math.h> +#include <stack> +#include <typeinfo> + +namespace omega { + +extern Tuple<Tuple<Relation> > projected_nIS; +int var_substitution_threshold = 100; +//protonu. +extern int upperBoundForLevel; +extern int lowerBoundForLevel; +extern bool fillInBounds; +//end--protonu. + +} + + +namespace omega { + +std::pair<EQ_Handle, int> find_simplest_assignment(const Relation &R_, Variable_ID v, const std::vector<CG_outputRepr *> &assigned_on_the_fly); + + +namespace { + + + + +void get_stride(const Constraint_Handle &h, Variable_ID &wc, coef_t &step){ + wc = 0; + for(Constr_Vars_Iter i(h,true); i; i++) { + assert(wc == 0); + wc = (*i).var; + step = ((*i).coef); + } +} + +} + +CG_outputRepr* outputIdent(CG_outputBuilder* ocg, const Relation &R_, Variable_ID v, const std::vector<CG_outputRepr *> &assigned_on_the_fly) { + Relation &R = const_cast<Relation &>(R_); + + switch (v->kind()) { + case Set_Var: { + int pos = v->get_position(); + if (assigned_on_the_fly[pos-1] != NULL) + return assigned_on_the_fly[pos-1]->clone(); + else + return ocg->CreateIdent(v->name()); + break; + } + case Global_Var: { + if (v->get_global_var()->arity() == 0) + return ocg->CreateIdent(v->name()); + else { + /* This should be improved to take into account the possible elimination + of the set variables. */ + int arity = v->get_global_var()->arity(); + //assert(arity <= last_level); + Tuple<CG_outputRepr *> argList; + // Relation R = Relation::True(arity); + + // name_codegen_vars(R); // easy way to make sure the names are correct. + for(int i = 1; i <= arity; i++) + argList.append(ocg->CreateIdent(R.set_var(i)->name())); + CG_outputRepr *call = ocg->CreateInvoke(v->get_global_var()->base_name(), argList); + return call; + } + break; + } + default: + throw std::invalid_argument("wrong variable type"); + } +} + + +//---------------------------------------------------------------------------- +// Translate equality constraints to if-condition and assignment. +// return.first is right-hand-side of assignment, return.second +// is true if assignment is required. +// -- by chun 07/29/2010 +// ---------------------------------------------------------------------------- +std::pair<CG_outputRepr *, bool> outputAssignment(CG_outputBuilder *ocg, const Relation &R_, Variable_ID v, Relation &enforced, CG_outputRepr *&if_repr, const std::vector<CG_outputRepr *> &assigned_on_the_fly) { + Relation &R = const_cast<Relation &>(R_); + + Conjunct *c = R.query_DNF()->single_conjunct(); + + // check whether to generate if-conditions from equality constraints + for (EQ_Iterator ei(c); ei; ei++) + if (!(*ei).has_wildcards() && abs((*ei).get_coef(v)) > 1) { + Relation r(R.n_set()); + F_And *f_super_root = r.add_and(); + F_Exists *fe = f_super_root->add_exists(); + Variable_ID e = fe->declare(); + F_And *f_root = fe->add_and(); + EQ_Handle h = f_root->add_EQ(); + for (Constr_Vars_Iter cvi(*ei); cvi; cvi++) + switch ((*cvi).var->kind()) { + case Input_Var: { + if ((*cvi).var == v) + h.update_coef(e, (*cvi).coef); + else + h.update_coef(r.set_var((*cvi).var->get_position()), (*cvi).coef); + break; + } + case Global_Var: { + Global_Var_ID g = (*cvi).var->get_global_var(); + Variable_ID v2; + if (g->arity() == 0) + v2 = r.get_local(g); + else + v2 = r.get_local(g, (*cvi).var->function_of()); + h.update_coef(v2, (*cvi).coef); + break; + } + default: + assert(0); + } + h.update_const((*ei).get_const()); + + r.copy_names(R); + r.setup_names(); + + // need if-condition to make sure this loop variable has integer value + if (!Gist(r, copy(enforced), 1).is_obvious_tautology()) { + coef_t coef = (*ei).get_coef(v); + coef_t sign = -((coef>0)?1:-1); + coef = abs(coef); + + CG_outputRepr *term = NULL; + for (Constr_Vars_Iter cvi(*ei); cvi; cvi++) + if ((*cvi).var != v) { + CG_outputRepr *varRepr = outputIdent(ocg, R, (*cvi).var, assigned_on_the_fly); + coef_t t = sign*(*cvi).coef; + if (t == 1) + term = ocg->CreatePlus(term, varRepr); + else if (t == -1) + term = ocg->CreateMinus(term, varRepr); + else if (t > 0) + term = ocg->CreatePlus(term, ocg->CreateTimes(ocg->CreateInt(t), varRepr)); + else if (t < 0) + term = ocg->CreateMinus(term, ocg->CreateTimes(ocg->CreateInt(-t), varRepr)); + } + coef_t t = sign*(*ei).get_const(); + if (t > 0) + term = ocg->CreatePlus(term, ocg->CreateInt(t)); + else if (t < 0) + term = ocg->CreateMinus(term, ocg->CreateInt(-t)); + + term = ocg->CreateIntegerMod(term, ocg->CreateInt(coef)); + term = ocg->CreateEQ(term, ocg->CreateInt(0)); + + if_repr = ocg->CreateAnd(if_repr, term); + } + + enforced.and_with_EQ(*ei); + enforced.simplify(); + } + + // find the simplest assignment + std::pair<EQ_Handle, int> a = find_simplest_assignment(R, v, assigned_on_the_fly); + + // now generate assignment + if (a.second < INT_MAX) { + EQ_Handle eq = a.first; + CG_outputRepr *rop_repr = NULL; + + coef_t divider = eq.get_coef(v); + int sign = 1; + if (divider < 0) { + divider = -divider; + sign = -1; + } + + for (Constr_Vars_Iter cvi(eq); cvi; cvi++) + if ((*cvi).var != v) { + CG_outputRepr *var_repr = outputIdent(ocg, R, (*cvi).var, assigned_on_the_fly); + coef_t coef = (*cvi).coef; + if (-sign * coef == -1) + rop_repr = ocg->CreateMinus(rop_repr, var_repr); + else if (-sign * coef < -1) + rop_repr = ocg->CreateMinus(rop_repr, ocg->CreateTimes(ocg->CreateInt(sign * coef), var_repr)); + else if (-sign * coef == 1) + rop_repr = ocg->CreatePlus(rop_repr, var_repr); + else // -sign * coef > 1 + rop_repr = ocg->CreatePlus(rop_repr, ocg->CreateTimes(ocg->CreateInt(-sign * coef), var_repr)); + } + + coef_t c_term = -(eq.get_const() * sign); + + if (c_term > 0) + rop_repr = ocg->CreatePlus(rop_repr, ocg->CreateInt(c_term)); + else if (c_term < 0) + rop_repr = ocg->CreateMinus(rop_repr, ocg->CreateInt(-c_term)); + else if (rop_repr == NULL) + rop_repr = ocg->CreateInt(0); + + if (divider != 1) + rop_repr = ocg->CreateIntegerDivide(rop_repr, ocg->CreateInt(divider)); + + enforced.and_with_EQ(eq); + enforced.simplify(); + + if (a.second > var_substitution_threshold) + return std::make_pair(rop_repr, true); + else + return std::make_pair(rop_repr, false); + } + else + return std::make_pair(static_cast<CG_outputRepr *>(NULL), false); +} + + +//---------------------------------------------------------------------------- +// Don't use Substitutions class since it can't handle integer +// division. Instead, use relation mapping to a single output +// variable to get substitution. -- by chun, 07/19/2007 +//---------------------------------------------------------------------------- +Tuple<CG_outputRepr*> outputSubstitution(CG_outputBuilder* ocg, const Relation &R_, const std::vector<CG_outputRepr *> &assigned_on_the_fly) { + Relation &R = const_cast<Relation &>(R_); + + const int n = R.n_out(); + Tuple<CG_outputRepr*> oReprList; + + // Find substitution for each output variable + for (int i = 1; i <= n; i++) { + Relation mapping(n, 1); + F_And *f_root = mapping.add_and(); + EQ_Handle h = f_root->add_EQ(); + h.update_coef(mapping.output_var(1), 1); + h.update_coef(mapping.input_var(i), -1); + + Relation S = Composition(mapping, copy(R)); + + std::pair<EQ_Handle, int> a = find_simplest_assignment(S, S.output_var(1), assigned_on_the_fly); + + if (a.second < INT_MAX) { + while (a.second > 0) { + EQ_Handle eq = a.first; + std::set<int> candidates; + for (Constr_Vars_Iter cvi(eq); cvi; cvi++) + if ((*cvi).var->kind() == Input_Var) + candidates.insert((*cvi).var->get_position()); + + bool changed = false; + for (std::set<int>::iterator j = candidates.begin(); j != candidates.end(); j++) { + Relation S2 = Project(copy(S), *j, Input_Var); + std::pair<EQ_Handle, int> a2 = find_simplest_assignment(S2, S2.output_var(1), assigned_on_the_fly); + if (a2.second <= a.second) { + S = S2; + a = a2; + changed = true; + break; + } + } + if (!changed) + break; + } + } + + if (a.second < INT_MAX) { + CG_outputRepr *repr = NULL; + EQ_Handle eq = a.first; + Variable_ID v = S.output_var(1); + + for (int j = 1; j <= S.n_inp(); j++) + S.name_input_var(j, R.input_var(j)->name()); + S.setup_names(); + + int d = eq.get_coef(v); + assert(d != 0); + int sign = (d>0)?-1:1; + d = -sign * d; + for (Constr_Vars_Iter cvi(eq); cvi; cvi++) + if ((*cvi).var != v) { + int coef = sign * (*cvi).coef; + CG_outputRepr *op = outputIdent(ocg, S, (*cvi).var, assigned_on_the_fly); + if (coef > 1) + op = ocg->CreateTimes(ocg->CreateInt(coef), op); + else if (coef < -1) + op = ocg->CreateTimes(ocg->CreateInt(-coef), op); + if (coef > 0) + repr = ocg->CreatePlus(repr, op); + else if (coef < 0) + repr = ocg->CreateMinus(repr, op); + } + + int c = sign * eq.get_const(); + if (c > 0) + repr = ocg->CreatePlus(repr, ocg->CreateInt(c)); + else if (c < 0) + repr = ocg->CreateMinus(repr, ocg->CreateInt(-c)); + else if (repr == NULL) + repr = ocg->CreateInt(0); + + if (d != 1) + repr = ocg->CreateIntegerDivide(repr, ocg->CreateInt(d)); + + oReprList.append(repr); + } + else + oReprList.append(NULL); + } + + return oReprList; +} + +namespace { + +Relation create_stride_on_bound(int n, const std::map<Variable_ID, coef_t> &lb, coef_t stride) { + Relation result(n); + F_And *f_root = result.add_and(); + EQ_Handle h = f_root->add_stride(stride); + + for (std::map<Variable_ID, coef_t>::const_iterator i = lb.begin(); i != lb.end(); i++) { + if (i->first == NULL) + h.update_const(i->second); + else { + switch(i->first->kind()) { + case Input_Var: { + int pos = i->first->get_position(); + h.update_coef(result.set_var(pos), i->second); + break; + } + case Global_Var: { + Global_Var_ID g = i->first->get_global_var(); + Variable_ID v; + if (g->arity() == 0) + v = result.get_local(g); + else + v = result.get_local(g, i->first->function_of()); + h.update_coef(v, i->second); + break; + } + default: + assert(0); + } + } + } + + return result; +} + +} + +//---------------------------------------------------------------------------- +// Find the most restrictive common stride constraint for a set of +// relations. -- by chun, 05/20/09 +// ---------------------------------------------------------------------------- +Relation greatest_common_step(const Tuple<Relation> &I, const Tuple<int> &active, int level, const Relation &known) { + assert(I.size() == active.size()); + int n = 0; + + std::vector<Relation> I1, I2; + for (int i = 1; i <= I.size(); i++) + if (active[i]) { + if (n == 0) + n = I[i].n_set(); + + Relation r1; + if (known.is_null()) + r1 = copy(I[i]); + else { + r1 = Intersection(copy(I[i]), copy(known)); + r1.simplify(); + } + I1.push_back(r1); + Relation r2 = Gist(copy(I[i]), copy(known)); + assert(r2.is_upper_bound_satisfiable()); + if (r2.is_obvious_tautology()) + return Relation::True(n); + I2.push_back(r2); + } + + std::vector<bool> is_exact(I2.size(), true); + std::vector<coef_t> step(I2.size(), 0); + std::vector<coef_t> messy_step(I2.size(), 0); + Variable_ID t_col = set_var(level); + std::map<Variable_ID, coef_t> lb; + + // first check all clean strides: t_col = ... (mod step) + for (size_t i = 0; i < I2.size(); i++) { + Conjunct *c = I2[i].query_DNF()->single_conjunct(); + + bool is_degenerated = false; + for (EQ_Iterator e = c->EQs(); e; e++) { + coef_t coef = abs((*e).get_coef(t_col)); + if (coef != 0 && !(*e).has_wildcards()) { + is_degenerated = true; + break; + } + } + if (is_degenerated) + continue; + + for (EQ_Iterator e = c->EQs(); e; e++) { + if ((*e).has_wildcards()) { + coef_t coef = abs((*e).get_coef(t_col)); + if (coef == 0) + continue; + if (coef != 1) { + is_exact[i] = false; + continue; + } + + coef_t this_step = abs(Constr_Vars_Iter(*e, true).curr_coef()); + assert(this_step != 1); + + if (lb.size() != 0) { + Relation test = create_stride_on_bound(n, lb, this_step); + if (Gist(test, copy(I1[i])).is_obvious_tautology()) { + if (step[i] == 0) + step[i] = this_step; + else + step[i] = lcm(step[i], this_step); + } + else + is_exact[i] = false; + } + else { + // try to find a lower bound that hits on stride + Conjunct *c = I2[i].query_DNF()->single_conjunct(); + for (GEQ_Iterator ge = c->GEQs(); ge; ge++) { + if ((*ge).has_wildcards() || (*ge).get_coef(t_col) != 1) + continue; + + std::map<Variable_ID, coef_t> cur_lb; + for (Constr_Vars_Iter cv(*ge); cv; cv++) + cur_lb[cv.curr_var()] = cv.curr_coef(); + cur_lb[NULL] = (*ge).get_const(); + + Relation test = create_stride_on_bound(n, cur_lb, this_step); + if (Gist(test, copy(I1[i])).is_obvious_tautology()) { + if (step[i] == 0) + step[i] = this_step; + else + step[i] = lcm(step[i], this_step); + + lb = cur_lb; + break; + } + } + + // no clean lower bound, thus we use this modular constraint as is + if (lb.size() == 0) { + std::map<Variable_ID, coef_t> cur_lb; + int wild_count = 0; + for (Constr_Vars_Iter cv(*e); cv; cv++) + if (cv.curr_var()->kind() == Wildcard_Var) + wild_count++; + else + cur_lb[cv.curr_var()] = cv.curr_coef(); + cur_lb[NULL] = (*e).get_const(); + + if (wild_count == 1) { + lb = cur_lb; + if (step[i] == 0) + step[i] = this_step; + else + step[i] = lcm(step[i], this_step); + } + } + + if (lb.size() == 0) + is_exact[i] = false; + } + } + } + } + + // aggregate all exact steps + coef_t global_step = 0; + for (size_t i = 0; i < is_exact.size(); i++) + if (is_exact[i]) + global_step = gcd(global_step, step[i]); + if (global_step == 1) + return Relation::True(n); + + // now check all messy strides: a*t_col = ... (mod step) + for (size_t i = 0; i < I2.size(); i++) + if (!is_exact[i]) { + Conjunct *c = I2[i].query_DNF()->single_conjunct(); + for (EQ_Iterator e = c->EQs(); e; e++) { + coef_t coef = abs((*e).get_coef(t_col)); + if (coef == 0 || coef == 1) + continue; + + // make a guess for messy stride condition -- by chun 07/27/2007 + coef_t this_step = abs(Constr_Vars_Iter(*e, true).curr_coef()); + this_step /= gcd(this_step, coef); + this_step = gcd(global_step, this_step); + if (this_step == 1) + continue; + + if (lb.size() != 0) { + Relation test = create_stride_on_bound(n, lb, this_step); + if (Gist(test, copy(I1[i])).is_obvious_tautology()) { + if (step[i] == 0) + step[i] = this_step; + else + step[i] = lcm(step[i], this_step); + } + } + else { + // try to find a lower bound that hits on stride + Conjunct *c = I2[i].query_DNF()->single_conjunct(); + for (GEQ_Iterator ge = c->GEQs(); ge; ge++) { + if ((*ge).has_wildcards() || (*ge).get_coef(t_col) != 1) + continue; + + std::map<Variable_ID, coef_t> cur_lb; + + for (Constr_Vars_Iter cv(*ge); cv; cv++) + cur_lb[cv.curr_var()] = cv.curr_coef(); + + cur_lb[NULL] = (*ge).get_const(); + + Relation test = create_stride_on_bound(n, cur_lb, this_step); + if (Gist(test, copy(I1[i])).is_obvious_tautology()) { + if (step[i] == 0) + step[i] = this_step; + else + step[i] = lcm(step[i], this_step); + + lb = cur_lb; + break; + } + } + } + } + } + + // aggregate all non-exact steps + for (size_t i = 0; i < is_exact.size(); i++) + if (!is_exact[i]) + global_step = gcd(global_step, step[i]); + if (global_step == 1 || global_step == 0) + return Relation::True(n); + + Relation result = create_stride_on_bound(n, lb, global_step); + + // check for statements that haven't been factored into global step + for (size_t i = 0; i < I1.size(); i++) + if (step[i] == 0) { + if (!Gist(copy(result), copy(I1[i])).is_obvious_tautology()) + return Relation::True(n); + } + + return result; +} + + +//----------------------------------------------------------------------------- +// Substitute variables in a statement according to mapping function. +//----------------------------------------------------------------------------- +CG_outputRepr* outputStatement(CG_outputBuilder *ocg, CG_outputRepr *stmt, int indent, const Relation &mapping_, const Relation &known_, const std::vector<CG_outputRepr *> &assigned_on_the_fly) { + Relation mapping = copy(mapping_); + Relation known = copy(known_); + Tuple<std::string> loop_vars; + + for (int i = 1; i <= mapping.n_inp(); i++) + loop_vars.append(mapping.input_var(i)->name()); + + // discard non-existant variables from iteration spaces -- by chun 12/31/2008 + if (known.n_set() > mapping.n_out()) { + Relation r(known.n_set(), mapping.n_out()); + F_And *f_root = r.add_and(); + for (int i = 1; i <= mapping.n_out(); i++) { + EQ_Handle h = f_root->add_EQ(); + h.update_coef(r.input_var(i), 1); + h.update_coef(r.output_var(i), -1); + } + known = Range(Restrict_Domain(r, known)); + known.simplify(); + } + + // remove modular constraints from known to simplify mapping process -- by chun 11/10/2008 + Relation k(known.n_set()); + F_And *f_root = k.add_and(); + Conjunct *c = known.query_DNF()->single_conjunct(); + for (EQ_Iterator e = c->EQs(); e; e++) { + if (!(*e).has_wildcards()) + f_root->add_EQ(*e); + } + k.simplify(); + + // get variable substituion list + Relation Inv_mapping = Restrict_Domain(Inverse(mapping), k); + Tuple<CG_outputRepr*> sList = outputSubstitution(ocg, Inv_mapping, assigned_on_the_fly); + + return ocg->CreatePlaceHolder(indent, stmt, sList, loop_vars); +} + + +// find floor definition for variable such as m-3 <= 4v <= m +bool findFloorInequality(Relation &r, Variable_ID v, GEQ_Handle &h, Variable_ID excluded) { + Conjunct *c = r.single_conjunct(); + + std::set<Variable_ID> var_checked; + std::stack<Variable_ID> var_checking; + var_checking.push(v); + + while (!var_checking.empty()) { + Variable_ID v2 = var_checking.top(); + var_checking.pop(); + + bool is_floor = false; + for (GEQ_Iterator gi(c); gi; gi++) { + if (excluded != NULL && (*gi).get_coef(excluded) != 0) + continue; + + coef_t a = (*gi).get_coef(v2); + if (a < 0) { + for (GEQ_Iterator gi2(c); gi2; gi2++) { + coef_t b = (*gi2).get_coef(v2); + if (b == -a && (*gi).get_const()+(*gi2).get_const() < -a) { + bool match = true; + for (Constr_Vars_Iter cvi(*gi); cvi; cvi++) + if ((*gi2).get_coef((*cvi).var) != -(*cvi).coef) { + match = false; + break; + } + if (!match) + continue; + for (Constr_Vars_Iter cvi(*gi2); cvi; cvi++) + if ((*gi).get_coef((*cvi).var) != -(*cvi).coef) { + match = false; + break; + } + if (match) { + var_checked.insert(v2); + is_floor = true; + if (v == v2) + h = *gi; + + for (Constr_Vars_Iter cvi(*gi); cvi; cvi++) + if (((*cvi).var->kind() == Exists_Var || (*cvi).var->kind() == Wildcard_Var) && + var_checked.find((*cvi).var) == var_checked.end()) + var_checking.push((*cvi).var); + + break; + } + } + } + if (is_floor) + break; + } + } + if (!is_floor) + return false; + } + return true; +} + + + + +//----------------------------------------------------------------------------- +// Output a reqular equality or inequality to conditions. +// e.g. (i=5*j) +//----------------------------------------------------------------------------- +CG_outputRepr* output_as_guard(CG_outputBuilder* ocg, const Relation &guards_in, Constraint_Handle e, bool is_equality, const std::vector<CG_outputRepr *> &assigned_on_the_fly) { + Relation &guards = const_cast<Relation &>(guards_in); + if (e.has_wildcards()) + throw std::invalid_argument("constraint must not have wildcard"); + + Variable_ID v = (*Constr_Vars_Iter(e)).var; + + coef_t saved_coef = ((e).get_coef(v)); + int sign = saved_coef < 0 ? -1 : 1; + + (e).update_coef_during_simplify(v, -saved_coef+sign); + CG_outputRepr* rop = outputEasyBoundAsRepr(ocg, guards, e, v, false, 0, assigned_on_the_fly); + (e).update_coef_during_simplify(v,saved_coef-sign); + + CG_outputRepr* lop = outputIdent(ocg, guards, v, assigned_on_the_fly); + if (abs(saved_coef) != 1) + lop = ocg->CreateTimes(ocg->CreateInt(abs(saved_coef)), lop); + + + if (is_equality) { + return ocg->CreateEQ(lop, rop); + } + else { + if (saved_coef < 0) + return ocg->CreateLE(lop, rop); + else + return ocg->CreateGE(lop, rop); + } +} + + +//----------------------------------------------------------------------------- +// Output stride conditions from equalities. +// e.g. (exists alpha: i = 5*alpha) +//----------------------------------------------------------------------------- +CG_outputRepr *output_EQ_strides(CG_outputBuilder* ocg, const Relation &guards_in, const std::vector<CG_outputRepr *> &assigned_on_the_fly) { + Relation guards = const_cast<Relation &>(guards_in); + Conjunct *c = guards.single_conjunct(); + + CG_outputRepr *eqRepr = NULL; + + for (EQ_Iterator ei(c->EQs()); ei; ei++) { + Variable_ID wc = NULL; + for (Constr_Vars_Iter cvi((*ei), true); cvi; cvi++) { + if (wc != NULL) + throw codegen_error("Can't generate equality condition with multiple wildcards"); + else + wc = (*cvi).var; + } + if (wc == NULL) + continue; + + coef_t step = (*ei).get_coef(wc); + + (*ei).update_coef_during_simplify(wc, 1-step); + CG_outputRepr* lop = outputEasyBoundAsRepr(ocg, guards, (*ei), wc, false, 0, assigned_on_the_fly); + (*ei).update_coef_during_simplify(wc, step-1); + + CG_outputRepr* rop = ocg->CreateInt(abs(step)); + CG_outputRepr* intMod = ocg->CreateIntegerMod(lop, rop); + CG_outputRepr* eqNode = ocg->CreateEQ(intMod, ocg->CreateInt(0)); + + eqRepr = ocg->CreateAnd(eqRepr, eqNode); + } + + return eqRepr; +} + + + +//----------------------------------------------------------------------------- +// Output hole conditions created by inequalities involving wildcards. +// e.g. (exists alpha: 4*alpha <= i <= 5*alpha) +// Collect wildcards +// For each whildcard +// collect lower and upper bounds in which wildcard appears +// For each lower bound +// create constraint with each upper bound +//----------------------------------------------------------------------------- +CG_outputRepr *output_GEQ_strides(CG_outputBuilder* ocg, const Relation &guards_in, const std::vector<CG_outputRepr *> &assigned_on_the_fly) { + Relation guards = const_cast<Relation &>(guards_in); + Conjunct *c = guards.single_conjunct(); + + CG_outputRepr* geqRepr = NULL; + + std::set<Variable_ID> non_orphan_wildcard; + for (GEQ_Iterator gi(c); gi; gi++) { + int num_wild = 0; + Variable_ID first_one; + for (Constr_Vars_Iter cvi(*gi, true); cvi; cvi++) { + num_wild++; + if (num_wild == 1) + first_one = (*cvi).var; + else + non_orphan_wildcard.insert((*cvi).var); + } + if (num_wild > 1) + non_orphan_wildcard.insert(first_one); + } + + for (int i = 1; i <= (*(c->variables())).size(); i++) { + Variable_ID wc = (*(c->variables()))[i]; + if (wc->kind() == Wildcard_Var && non_orphan_wildcard.find(wc) == non_orphan_wildcard.end()) { + Tuple<GEQ_Handle> lower, upper; + for (GEQ_Iterator gi(c); gi; gi++) { + if((*gi).get_coef(wc) > 0) + lower.append(*gi); + else if((*gi).get_coef(wc) < 0) + upper.append(*gi); + } + + // low: c*alpha - x >= 0 + // up: -d*alpha + y >= 0 + for (Tuple_Iterator<GEQ_Handle> low(lower); low; low++) { + for (Tuple_Iterator<GEQ_Handle> up(upper); up; up++) { + coef_t low_coef = (*low).get_coef(wc); + coef_t up_coef = (*up).get_coef(wc); + + (*low).update_coef_during_simplify(wc, 1-low_coef); + CG_outputRepr* lowExpr = outputEasyBoundAsRepr(ocg, guards, *low, wc, false, 0, assigned_on_the_fly); + (*low).update_coef_during_simplify(wc, low_coef-1); + + (*up).update_coef_during_simplify(wc, -1-up_coef); + CG_outputRepr* upExpr = outputEasyBoundAsRepr(ocg, guards, *up, wc, false, 0, assigned_on_the_fly); + (*up).update_coef_during_simplify(wc, up_coef+1); + + CG_outputRepr* intDiv = ocg->CreateIntegerDivide(upExpr, ocg->CreateInt(-up_coef)); + CG_outputRepr* rop = ocg->CreateTimes(ocg->CreateInt(low_coef), intDiv); + CG_outputRepr* geqNode = ocg->CreateLE(lowExpr, rop); + + geqRepr = ocg->CreateAnd(geqRepr, geqNode); + } + } + } + } + + if (non_orphan_wildcard.size() > 0) { + // e.g. c*alpha - x >= 0 (*) + // -d*alpha + y >= 0 (*) + // e1*alpha + f1*beta + g1 >= 0 (**) + // e2*alpha + f2*beta + g2 >= 0 (**) + // ... + // TODO: should generate a testing loop for alpha using its lower and + // upper bounds from (*) constraints and do the same if-condition test + // for beta from each pair of opposite (**) constraints as above, + // and exit the loop when if-condition satisfied. + throw codegen_error("Can't generate multiple wildcard GEQ guards right now"); + } + + return geqRepr; +} + + +//----------------------------------------------------------------------------- +// Translate all constraints in a relation to guard conditions. +//----------------------------------------------------------------------------- +CG_outputRepr *outputGuard(CG_outputBuilder* ocg, const Relation &guards_in, const std::vector<CG_outputRepr *> &assigned_on_the_fly) { + Relation &guards = const_cast<Relation &>(guards_in); + if (guards.is_null() || guards.is_obvious_tautology()) + return NULL; + + CG_outputRepr* nodeRepr = NULL; + + CG_outputRepr *eqStrideRepr = output_EQ_strides(ocg, guards, assigned_on_the_fly); + nodeRepr = ocg->CreateAnd(nodeRepr, eqStrideRepr); + + CG_outputRepr *geqStrideRepr = output_GEQ_strides(ocg, guards, assigned_on_the_fly); + nodeRepr = ocg->CreateAnd(nodeRepr, geqStrideRepr); + + Conjunct *c = guards.single_conjunct(); + for(EQ_Iterator ei(c->EQs()); ei; ei++) + if (!(*ei).has_wildcards()) { + CG_outputRepr *eqRepr = output_as_guard(ocg, guards, (*ei), true, assigned_on_the_fly); + nodeRepr = ocg->CreateAnd(nodeRepr, eqRepr); + } + for(GEQ_Iterator gi(c->GEQs()); gi; gi++) + if (!(*gi).has_wildcards()) { + CG_outputRepr *geqRepr = output_as_guard(ocg, guards, (*gi), false, assigned_on_the_fly); + nodeRepr = ocg->CreateAnd(nodeRepr, geqRepr); + } + + return nodeRepr; +} + + +//----------------------------------------------------------------------------- +// one is 1 for LB +// this function is overloaded should replace the original one +//----------------------------------------------------------------------------- +CG_outputRepr *outputLBasRepr(CG_outputBuilder* ocg, const GEQ_Handle &g, + Relation &bounds, Variable_ID v, + coef_t stride, const EQ_Handle &strideEQ, + Relation known, const std::vector<CG_outputRepr *> &assigned_on_the_fly) { +#if ! defined NDEBUG + coef_t v_coef; + assert((v_coef = g.get_coef(v)) > 0); +#endif + + std::string s; + CG_outputRepr *lbRepr; + if (stride == 1) { + lbRepr = outputEasyBoundAsRepr(ocg, bounds, g, v, false, 1, assigned_on_the_fly); + } + else { + if (!boundHitsStride(g,v,strideEQ,stride,known)) { + bounds.setup_names(); // boundsHitsStride resets variable names + + CG_stringBuilder oscg; + std::string c = GetString(outputEasyBoundAsRepr(&oscg, bounds, strideEQ, v, true, 0, assigned_on_the_fly)); + CG_outputRepr *cRepr = NULL; + if (c != std::string("0")) + cRepr = outputEasyBoundAsRepr(ocg, bounds, strideEQ, v, true, 0, assigned_on_the_fly); + std::string LoverM = GetString(outputEasyBoundAsRepr(&oscg, bounds, g, v, false, 1, assigned_on_the_fly)); + CG_outputRepr *LoverMRepr = NULL; + if (LoverM != std::string("0")) + LoverMRepr = outputEasyBoundAsRepr(ocg, bounds, g, v, false, 1, assigned_on_the_fly); + + if (code_gen_debug > 2) { + fprintf(DebugFile,"::: LoverM is %s\n", LoverM.c_str()); + fprintf(DebugFile,"::: c is %s\n", c.c_str()); + } + + int complexity1 = 0, complexity2 = 0; + for (size_t i = 0; i < c.length(); i++) + if (c[i] == '+' || c[i] == '-' || c[i] == '*' || c[i] == '/') + complexity1++; + else if (c[i] == ',') + complexity1 += 2; + for (size_t i = 0; i < LoverM.length(); i++) + if (LoverM[i] == '+' || LoverM[i] == '-' || LoverM[i] == '*' || LoverM[i] == '/') + complexity2++; + else if (LoverM[i] == ',') + complexity2 += 2; + + if (complexity1 < complexity2) { + CG_outputRepr *idUp = LoverMRepr; + CG_outputRepr *c1Repr = ocg->CreateCopy(cRepr); + idUp = ocg->CreateMinus(idUp, c1Repr); + idUp = ocg->CreatePlus(idUp, ocg->CreateInt(stride-1)); + CG_outputRepr *idLow = ocg->CreateInt(stride); + lbRepr = ocg->CreateTimes(ocg->CreateInt(stride), + ocg->CreateIntegerDivide(idUp, idLow)); + lbRepr = ocg->CreatePlus(lbRepr, cRepr); + } + else { + CG_outputRepr *LoverM1Repr = ocg->CreateCopy(LoverMRepr); + CG_outputRepr *imUp = ocg->CreateMinus(cRepr, LoverM1Repr); + CG_outputRepr *imLow = ocg->CreateInt(stride); + CG_outputRepr *intMod = ocg->CreateIntegerMod(imUp, imLow); + lbRepr = ocg->CreatePlus(LoverMRepr, intMod); + } + } + else { + // boundsHitsStride resets variable names + bounds.setup_names(); + lbRepr = outputEasyBoundAsRepr(ocg, bounds, g, v, false, 0, assigned_on_the_fly); + } + } + + return lbRepr; +} + +//----------------------------------------------------------------------------- +// one is -1 for UB +// this function is overloaded should replace the original one +//----------------------------------------------------------------------------- +CG_outputRepr *outputUBasRepr(CG_outputBuilder* ocg, const GEQ_Handle &g, + Relation & bounds, + Variable_ID v, + coef_t /*stride*/, // currently unused + const EQ_Handle &/*strideEQ*/, //currently unused + const std::vector<CG_outputRepr *> &assigned_on_the_fly) { + assert(g.get_coef(v) < 0); + CG_outputRepr* upRepr = outputEasyBoundAsRepr(ocg, bounds, g, v, false, 0, assigned_on_the_fly); + return upRepr; +} + +//----------------------------------------------------------------------------- +// Print the expression for the variable given as v. Works for both +// GEQ's and EQ's, but produces intDiv (not intMod) when v has a nonunit +// coefficient. So it is OK for loop bounds, but for checking stride +// constraints, you want to make sure the coef of v is 1, and insert the +// intMod yourself. +// +// original name is outputEasyBound +//----------------------------------------------------------------------------- +CG_outputRepr* outputEasyBoundAsRepr(CG_outputBuilder* ocg, Relation &bounds, + const Constraint_Handle &g, Variable_ID v, + bool ignoreWC, + int ceiling, + const std::vector<CG_outputRepr *> &assigned_on_the_fly) { + // assert ignoreWC => g is EQ + // rewrite constraint as foo (== or <= or >=) v, return foo as string + + CG_outputRepr* easyBoundRepr = NULL; + + coef_t v_coef = g.get_coef(v); + int v_sign = v_coef > 0 ? 1 : -1; + v_coef *= v_sign; + assert(v_coef > 0); + // foo is (-constraint)/v_sign/v_coef + + int sign_adj = -v_sign; + + //---------------------------------------------------------------------- + // the following generates +- cf*varName + //---------------------------------------------------------------------- + for(Constr_Vars_Iter c2(g, false); c2; c2++) { + if ((*c2).var != v && (!ignoreWC || (*c2).var->kind()!=Wildcard_Var)) { + + coef_t cf = (*c2).coef*sign_adj; + assert(cf != 0); + + CG_outputRepr *varName; + if ((*c2).var->kind() == Wildcard_Var) { + GEQ_Handle h; + if (!findFloorInequality(bounds, (*c2).var, h, v)) { + if (easyBoundRepr != NULL) { + easyBoundRepr->clear(); + delete easyBoundRepr; + } + return NULL; + } + varName = outputEasyBoundAsRepr(ocg, bounds, h, (*c2).var, false, 0, assigned_on_the_fly); + } + else { + varName = outputIdent(ocg, bounds, (*c2).var, assigned_on_the_fly); + } + CG_outputRepr *cfRepr = NULL; + + if (cf > 1) { + cfRepr = ocg->CreateInt(cf); + CG_outputRepr* rbRepr = ocg->CreateTimes(cfRepr, varName); + easyBoundRepr = ocg->CreatePlus(easyBoundRepr, rbRepr); + } + else if (cf < -1) { + cfRepr = ocg->CreateInt(-cf); + CG_outputRepr* rbRepr = ocg->CreateTimes(cfRepr, varName); + easyBoundRepr = ocg->CreateMinus(easyBoundRepr, rbRepr); + } + else if (cf == 1) { + easyBoundRepr = ocg->CreatePlus(easyBoundRepr, varName); + } + else if (cf == -1) { + easyBoundRepr = ocg->CreateMinus(easyBoundRepr, varName); + } + } + } + + if (g.get_const()) { + coef_t cf = g.get_const()*sign_adj; + assert(cf != 0); + if (cf > 0) { + easyBoundRepr = ocg->CreatePlus(easyBoundRepr, ocg->CreateInt(cf)); + } + else { + easyBoundRepr = ocg->CreateMinus(easyBoundRepr, ocg->CreateInt(-cf)); + } + } + else { + if(easyBoundRepr == NULL) { + easyBoundRepr = ocg->CreateInt(0); + } + } + + if (v_coef > 1) { + assert(ceiling >= 0); + if (ceiling) { + easyBoundRepr= ocg->CreatePlus(easyBoundRepr, ocg->CreateInt(v_coef-1)); + } + easyBoundRepr = ocg->CreateIntegerDivide(easyBoundRepr, ocg->CreateInt(v_coef)); + } + + return easyBoundRepr; +} + + +//---------------------------------------------------------------------------- +// Translate inequality constraints to loop or assignment. +// if return.second is true, return.first is loop structure, +// otherwise it is assignment. +// ---------------------------------------------------------------------------- +std::pair<CG_outputRepr *, bool> outputBounds(CG_outputBuilder* ocg, const Relation &bounds, Variable_ID v, int indent, Relation &enforced, const std::vector<CG_outputRepr *> &assigned_on_the_fly) { + Relation b = copy(bounds); + Conjunct *c = b.query_DNF()->single_conjunct(); + + // Elaborate stride simplification which is complementary to gist function + // since we further target the specific loop variable. -- by chun 08/07/2008 + Relation r1 = Relation::True(b.n_set()), r2 = Relation::True(b.n_set()); + for (EQ_Iterator ei(c); ei; ei++) { + if ((*ei).get_coef(v) != 0 && (*ei).has_wildcards()) { // stride condition found + coef_t sign; + if ((*ei).get_coef(v) > 0) + sign = 1; + else + sign = -1; + + coef_t stride = 0; + for (Constr_Vars_Iter cvi(*ei, true); cvi; cvi++) + if ((*cvi).var->kind() == Wildcard_Var) { + stride = abs((*cvi).coef); + break; + } + + // check if stride hits lower bound + bool found_match = false; + if (abs((*ei).get_coef(v)) != 1) { // expensive matching for non-clean stride condition + coef_t d = stride / gcd(abs((*ei).get_coef(v)), stride); + Relation r3 = Relation::True(b.n_set()); + r3.and_with_EQ(*ei); + + for (GEQ_Iterator gi(c); gi; gi++) { + if ((*gi).get_coef(v) == 1 && !(*gi).has_wildcards()) { + Relation r4(b.n_set()); + F_And *f_root = r4.add_and(); + Stride_Handle h = f_root->add_stride(d); + + for (Constr_Vars_Iter cvi(*gi); cvi; cvi++) + switch ((*cvi).var->kind()) { + case Input_Var: { + int pos = (*cvi).var->get_position(); + h.update_coef(r4.set_var(pos), (*cvi).coef); + break; + } + case Global_Var: { + Global_Var_ID g = (*cvi).var->get_global_var(); + Variable_ID v; + if (g->arity() == 0) + v = r4.get_local(g); + else + v = r4.get_local(g, (*cvi).var->function_of()); + h.update_coef(v, (*cvi).coef); + break; + } + default: + fprintf(DebugFile, "can't deal with the variable type in lower bound\n"); + return std::make_pair(static_cast<CG_outputRepr *>(NULL), false); + } + h.update_const((*gi).get_const()); + + Relation r5 = Gist(copy(r3), Intersection(copy(r4), copy(enforced))); + + // replace original stride condition with striding from this lower bound + if (r5.is_obvious_tautology()) { + r1 = Intersection(r1, r4); + found_match = true; + break; + } + } + } + } + else { + for (GEQ_Iterator gi(c); gi; gi++) { + if ((*gi).get_coef(v) == abs((*ei).get_coef(v)) && !(*gi).has_wildcards()) { // potential matching lower bound found + Relation r(b.n_set()); + Stride_Handle h = r.add_and()->add_stride(stride); + + for (Constr_Vars_Iter cvi(*gi); cvi; cvi++) + switch ((*cvi).var->kind()) { + case Input_Var: { + int pos = (*cvi).var->get_position(); + if ((*cvi).var != v) { + int t1 = int_mod((*cvi).coef, stride); + if (t1 != 0) { + coef_t t2 = enforced.query_variable_mod(enforced.set_var(pos), stride); + if (t2 != posInfinity) + h.update_const(t1*t2); + else + h.update_coef(r.set_var(pos), t1); + } + } + else + h.update_coef(r.set_var(pos), (*cvi).coef); + break; + } + case Global_Var: { + Global_Var_ID g = (*cvi).var->get_global_var(); + Variable_ID v; + if (g->arity() == 0) + v = enforced.get_local(g); + else + v = enforced.get_local(g, (*cvi).var->function_of()); + coef_t t = enforced.query_variable_mod(v, stride); + if (t != posInfinity) + h.update_const(t*(*cvi).coef); + else { + Variable_ID v2; + if (g->arity() == 0) + v2 = r.get_local(g); + else + v2 = r.get_local(g, (*cvi).var->function_of()); + h.update_coef(v2, (*cvi).coef); + } + break; + } + default: + fprintf(DebugFile, "can't deal with the variable type in lower bound\n"); + return std::make_pair(static_cast<CG_outputRepr *>(NULL), false); + } + h.update_const((*gi).get_const()); + + bool t = true; + { + Conjunct *c2 = r.query_DNF()->single_conjunct(); + EQ_Handle h2; + for (EQ_Iterator ei2(c2); ei2; ei2++) { + h2 = *ei2; + break; + } + + int sign; + if (h2.get_coef(v) == (*ei).get_coef(v)) + sign = 1; + else + sign = -1; + + t = int_mod(h2.get_const() - sign * (*ei).get_const(), stride) == 0; + + if (t != false) + for (Constr_Vars_Iter cvi(h2); cvi; cvi++) + if ((*cvi).var->kind() != Wildcard_Var && + int_mod((*cvi).coef - sign * (*ei).get_coef((*cvi).var), stride) != 0) { + t = false; + break; + } + + if (t != false) + for (Constr_Vars_Iter cvi(*ei); cvi; cvi++) + if ((*cvi).var->kind() != Wildcard_Var && + int_mod((*cvi).coef - sign * h2.get_coef((*cvi).var), stride) != 0) { + t = false; + break; + } + + } + + if (t) { + // replace original stride condition with striding from this lower bound + F_And *f_root = r1.and_with_and(); + Stride_Handle h = f_root->add_stride(stride); + for (Constr_Vars_Iter cvi(*gi); cvi; cvi++) + switch ((*cvi).var->kind()) { + case Input_Var: { + h.update_coef(r1.set_var((*cvi).var->get_position()), (*cvi).coef); + break; + } + case Global_Var: { + Global_Var_ID g = (*cvi).var->get_global_var(); + Variable_ID v; + if (g->arity() == 0) + v = r1.get_local(g); + else + v = r1.get_local(g, (*cvi).var->function_of()); + h.update_coef(v, (*cvi).coef); + break; + } + default: + fprintf(DebugFile, "can't deal with the variable type in lower bound\n"); + return std::make_pair(static_cast<CG_outputRepr *>(NULL), false); + } + h.update_const((*gi).get_const()); + + found_match = true; + break; + } + } + } + } + + if (!found_match) + r1.and_with_EQ(*ei); + } + else if ((*ei).get_coef(v) == 0) { + Relation r3 = Relation::True(b.n_set()); + r3.and_with_EQ(*ei); + Relation r4 = Gist(r3, copy(enforced)); + if (!r4.is_obvious_tautology()) + r2.and_with_EQ(*ei); + } + else + r2.and_with_EQ(*ei); + } + + // restore remaining inequalities + { + std::map<Variable_ID, Variable_ID> exists_mapping; + F_Exists *fe = r2.and_with_and()->add_exists(); + F_And *f_root = fe->add_and(); + for (GEQ_Iterator gi(c); gi; gi++) { + GEQ_Handle h = f_root->add_GEQ(); + for (Constr_Vars_Iter cvi(*gi); cvi; cvi++) { + Variable_ID v = cvi.curr_var(); + switch (v->kind()) { + case Input_Var: { + int pos = v->get_position(); + h.update_coef(r2.set_var(pos), cvi.curr_coef()); + break; + } + case Exists_Var: + case Wildcard_Var: { + std::map<Variable_ID, Variable_ID>::iterator p = exists_mapping.find(v); + Variable_ID e; + if (p == exists_mapping.end()) { + e = fe->declare(); + exists_mapping[v] = e; + } + else + e = (*p).second; + h.update_coef(e, cvi.curr_coef()); + break; + } + case Global_Var: { + Global_Var_ID g = v->get_global_var(); + Variable_ID v2; + if (g->arity() == 0) + v2 = r2.get_local(g); + else + v2 = r2.get_local(g, v->function_of()); + h.update_coef(v2, cvi.curr_coef()); + break; + } + default: + assert(0); + } + } + h.update_const((*gi).get_const()); + } + } + + // overwrite original bounds + { + r1.simplify(); + r2.simplify(); + Relation b2 = Intersection(r1, r2); + b2.simplify(); + for (int i = 1; i <= b.n_set(); i++) + b2.name_set_var(i, b.set_var(i)->name()); + b2.setup_names(); + b = b2; + c = b.query_DNF()->single_conjunct(); + } + + + // get loop strides + EQ_Handle strideEQ; + bool foundStride = false; // stride that can be translated to loop + bool foundSimpleStride = false; // stride that starts from const value + coef_t step = 1; + int num_stride = 0; + + for (EQ_Iterator ei(c); ei; ei++) { + if ((*ei).get_coef(v) != 0 && (*ei).has_wildcards()) { + num_stride++; + + if (abs((*ei).get_coef(v)) != 1) + continue; + + bool t = true; + coef_t d = 1; + for (Constr_Vars_Iter cvi(*ei); cvi; cvi++) + if ((*cvi).var->kind() == Wildcard_Var) { + assert(d==1); + d = abs((*cvi).coef); + } + else if ((*cvi).var->kind() == Input_Var) { + if ((*cvi).var != v) + t = false; + } + else + t = false; + + if (d > step) { + step = d; + foundSimpleStride = t; + strideEQ = *ei; + foundStride = true; + } + } + } + + // More than one stride or complex stride found, we should move all + // but strideEQ to body's guard condition. alas, not implemented. + if (!(num_stride == 0 || (num_stride == 1 && foundStride))) + return std::make_pair(static_cast<CG_outputRepr *>(NULL), false); + + // get loop bounds + int lower_bounds = 0, upper_bounds = 0; + Tuple<CG_outputRepr *> lbList; + Tuple<CG_outputRepr *> ubList; + coef_t const_lb = negInfinity, const_ub = posInfinity; + for (GEQ_Iterator g(c); g; g++) { + coef_t coef = (*g).get_coef(v); + if (coef == 0) + continue; + else if (coef > 0) { // lower bound + lower_bounds++; + if ((*g).is_const(v) && !foundStride) { + //no variables but v in constr + coef_t L,m; + L = -((*g).get_const()); + + m = (*g).get_coef(v); + coef_t sb = (int) (ceil(((float) L) /m)); + set_max(const_lb, sb); + } + else if ((*g).is_const(v) && foundSimpleStride) { + // no variables but v in constr + //make LB fit the stride constraint + coef_t L,m,s,c; + L = -((*g).get_const()); + m = (*g).get_coef(v); + s = step; + c = strideEQ.get_const(); + coef_t sb = (s * (int) (ceil( (float) (L - (c * m)) /(s*m))))+ c; + set_max(const_lb, sb); + } + else + lbList.append(outputLBasRepr(ocg, *g, b, v, step, strideEQ, enforced, assigned_on_the_fly)); + } + else { // upper bound + upper_bounds++; + if ((*g).is_const(v)) { + // no variables but v in constraint + set_min(const_ub,-(*g).get_const()/(*g).get_coef(v)); + } + else + ubList.append(outputUBasRepr(ocg, *g, b, v, step, strideEQ, assigned_on_the_fly)); + } + } + + CG_outputRepr *lbRepr = NULL; + CG_outputRepr *ubRepr = NULL; + if (const_lb != negInfinity) + lbList.append(ocg->CreateInt(const_lb)); + if (lbList.size() > 1) + lbRepr = ocg->CreateInvoke("max", lbList); + else if (lbList.size() == 1) + lbRepr = lbList[1]; + + //protonu + if(fillInBounds && lbList.size() == 1 && const_lb != negInfinity) + lowerBoundForLevel = const_lb; + //end-protonu + + if (const_ub != posInfinity) + ubList.append(ocg->CreateInt(const_ub)); + if (ubList.size() > 1) + ubRepr = ocg->CreateInvoke("min", ubList); + else if (ubList.size() == 1) + ubRepr = ubList[1]; + + //protonu + if(fillInBounds && const_ub != posInfinity) + upperBoundForLevel = const_ub; + //end-protonu + + if (upper_bounds == 0 || lower_bounds == 0) { + return std::make_pair(static_cast<CG_outputRepr *>(NULL), false); + } + else { + // bookkeeping catched constraints in new_knwon + F_Exists *fe = enforced.and_with_and()->add_exists(); + F_And *f_root = fe->add_and(); + std::map<Variable_ID, Variable_ID> exists_mapping; + std::stack<std::pair<GEQ_Handle, Variable_ID> > floor_geq_stack; + std::set<Variable_ID> floor_var_set; + + if (foundStride) { + EQ_Handle h = f_root->add_EQ(); + for (Constr_Vars_Iter cvi(strideEQ); cvi; cvi++) + switch ((*cvi).var->kind()) { + case Input_Var: { + int pos = (*cvi).var->get_position(); + h.update_coef(enforced.set_var(pos), (*cvi).coef); + break; + } + case Exists_Var: + case Wildcard_Var: { + std::map<Variable_ID, Variable_ID>::iterator p = exists_mapping.find((*cvi).var); + Variable_ID e; + if (p == exists_mapping.end()) { + e = fe->declare(); + exists_mapping[(*cvi).var] = e; + } + else + e = (*p).second; + h.update_coef(e, (*cvi).coef); + break; + } + case Global_Var: { + Global_Var_ID g = (*cvi).var->get_global_var(); + Variable_ID e; + if (g->arity() == 0) + e = enforced.get_local(g); + else + e = enforced.get_local(g, (*cvi).var->function_of()); + h.update_coef(e, (*cvi).coef); + break; + } + default: + assert(0); + } + h.update_const(strideEQ.get_const()); + } + + for (GEQ_Iterator gi(c); gi; gi++) + if ((*gi).get_coef(v) != 0) { + GEQ_Handle h = f_root->add_GEQ(); + for (Constr_Vars_Iter cvi(*gi); cvi; cvi++) + switch ((*cvi).var->kind()) { + case Input_Var: { + int pos = (*cvi).var->get_position(); + h.update_coef(enforced.set_var(pos), (*cvi).coef); + break; + } + case Exists_Var: + case Wildcard_Var: { + std::map<Variable_ID, Variable_ID>::iterator p = exists_mapping.find((*cvi).var); + Variable_ID e; + if (p == exists_mapping.end()) { + e = fe->declare(); + exists_mapping[(*cvi).var] = e; + } + else + e = (*p).second; + h.update_coef(e, (*cvi).coef); + + if (floor_var_set.find((*cvi).var) == floor_var_set.end()) { + GEQ_Handle h2; + findFloorInequality(b, (*cvi).var, h2, v); + floor_geq_stack.push(std::make_pair(h2, (*cvi).var)); + floor_var_set.insert((*cvi).var); + } + break; + } + case Global_Var: { + Global_Var_ID g = (*cvi).var->get_global_var(); + Variable_ID e; + if (g->arity() == 0) + e = enforced.get_local(g); + else + e = enforced.get_local(g, (*cvi).var->function_of()); + h.update_coef(e, (*cvi).coef); + break; + } + default: + assert(0); + } + h.update_const((*gi).get_const()); + } + + // add floor definition involving variables appeared in bounds + while (!floor_geq_stack.empty()) { + std::pair<GEQ_Handle, Variable_ID> p = floor_geq_stack.top(); + floor_geq_stack.pop(); + + GEQ_Handle h1 = f_root->add_GEQ(); + GEQ_Handle h2 = f_root->add_GEQ(); + for (Constr_Vars_Iter cvi(p.first); cvi; cvi++) { + switch ((*cvi).var->kind()) { + case Input_Var: { + int pos = (*cvi).var->get_position(); + h1.update_coef(enforced.input_var(pos), (*cvi).coef); + h2.update_coef(enforced.input_var(pos), -(*cvi).coef); + break; + } + case Exists_Var: + case Wildcard_Var: { + std::map<Variable_ID, Variable_ID>::iterator p2 = exists_mapping.find((*cvi).var); + Variable_ID e; + if (p2 == exists_mapping.end()) { + e = fe->declare(); + exists_mapping[(*cvi).var] = e; + } + else + e = (*p2).second; + h1.update_coef(e, (*cvi).coef); + h2.update_coef(e, -(*cvi).coef); + + if (floor_var_set.find((*cvi).var) == floor_var_set.end()) { + GEQ_Handle h3; + findFloorInequality(b, (*cvi).var, h3, v); + floor_geq_stack.push(std::make_pair(h3, (*cvi).var)); + floor_var_set.insert((*cvi).var); + } + break; + } + case Global_Var: { + Global_Var_ID g = (*cvi).var->get_global_var(); + Variable_ID e; + if (g->arity() == 0) + e = enforced.get_local(g); + else + e = enforced.get_local(g, (*cvi).var->function_of()); + h1.update_coef(e, (*cvi).coef); + h2.update_coef(e, -(*cvi).coef); + break; + } + default: + assert(0); + } + } + h1.update_const(p.first.get_const()); + h2.update_const(-p.first.get_const()); + h2.update_const(-p.first.get_coef(p.second)-1); + } + enforced.simplify(); + + CG_outputRepr *stRepr = NULL; + if (step != 1) + stRepr = ocg->CreateInt(abs(step)); + CG_outputRepr *indexRepr = outputIdent(ocg, b, v, assigned_on_the_fly); + CG_outputRepr *ctrlRepr = ocg->CreateInductive(indexRepr, lbRepr, ubRepr, stRepr); + + return std::make_pair(ctrlRepr, true); + } +} + + +Relation project_onto_levels(Relation R, int last_level, bool wildcards) { + assert(last_level >= 0 && R.is_set() && last_level <= R.n_set()); + if (last_level == R.n_set()) return R; + + int orig_vars = R.n_set(); + int num_projected = orig_vars - last_level; + R = Extend_Set(R,num_projected + ); // Project out vars numbered > last_level + Mapping m1 = Mapping::Identity(R.n_set()); // now orig_vars+num_proj + + for(int i=last_level+1; i <= orig_vars; i++) { + m1.set_map(Set_Var, i, Exists_Var, i); + m1.set_map(Set_Var, i+num_projected, Set_Var, i); + } + + MapRel1(R, m1, Comb_Id); + R.finalize(); + R.simplify(); + if (!wildcards) + R = Approximate(R,1); + assert(R.is_set()); + return R; +} + + +// Check if the lower bound already enforces the stride by +// (Where m is coef of v in g and L is the bound on m*v): +// Check if m divides L evenly and Check if this l.bound on v implies strideEQ +bool boundHitsStride(const GEQ_Handle &g, Variable_ID v, + const EQ_Handle &strideEQ, + coef_t /*stride*/, // currently unused + Relation known) { +/* m = coef of v in g; + L = bound on v part of g; +*/ + // Check if m divides L evenly + coef_t m = g.get_coef(v); + Relation test(known.n_set()); + F_Exists *e = test.add_exists(); // g is "L >= mv" + Variable_ID alpha = e->declare(); // want: "l = m alpha" + F_And *a = e->add_and(); + EQ_Handle h = a->add_EQ(); + for(Constr_Vars_Iter I(g,false); I; I++) + if((*I).var != v) { + if((*I).var->kind() != Global_Var) + h.update_coef((*I).var, (*I).coef); + else + h.update_coef(test.get_local((*I).var->get_global_var()), (*I).coef); + } + + h.update_const(g.get_const()); + h.update_coef(alpha,m); // set alpha's coef to m + if (!(Gist(test,copy(known)).is_obvious_tautology())) + return false; + // Check if this lower bound on v implies the strideEQ + Relation boundRel = known; // want: "known and l = m v" + boundRel.and_with_EQ(g); // add in l = mv + Relation strideRel(known.n_set()); + strideRel.and_with_EQ(strideEQ); + return Gist(strideRel, boundRel).is_obvious_tautology(); +} + + +// // Return true if there are no variables in g except wildcards & v +bool isSimpleStride(const EQ_Handle &g, Variable_ID v) { + EQ_Handle gg = g; // should not be necessary, but iterators are + // a bit brain-dammaged + bool is_simple=true; + for(Constr_Vars_Iter cvi(gg, false); cvi && is_simple; cvi++) + is_simple = ((*cvi).coef == 0 || (*cvi).var == v + || (*cvi).var->kind() == Wildcard_Var); + return is_simple; +} + + +int countStrides(Conjunct *c, Variable_ID v, EQ_Handle &strideEQ, + bool &simple) { + int strides=0; + for(EQ_Iterator G(c); G; G++) + for(Constr_Vars_Iter I(*G, true); I; I++) + if (((*I).coef != 0) && (*G).get_coef(v) != 0) { + strides++; + simple = isSimpleStride(*G,v); + strideEQ = *G; + break; + } + return strides; +} + +namespace { + +bool hasEQ(Relation r, int level) { + r.simplify(); + Variable_ID v = set_var(level); + Conjunct *s_conj = r.single_conjunct(); + for(EQ_Iterator G(s_conj); G; G++) + if ((*G).get_coef(v)) + return true; + return false; +} + + + +static Relation pickEQ(Relation r, int level) { + r.simplify(); + Variable_ID v = set_var(level); + Conjunct *s_conj = r.single_conjunct(); + for(EQ_Iterator E(s_conj); E; E++) + if ((*E).get_coef(v)) { + Relation test_rel(r.n_set()); + test_rel.and_with_EQ(*E); + return test_rel; + } + assert(0); + return r; +} + +/* pickBound will return an EQ as a GEQ if it finds one */ +Relation pickBound(Relation r, int level, int UB) { + r.simplify(); + Variable_ID v = set_var(level); + Conjunct *s_conj = r.single_conjunct(); + for(GEQ_Iterator G(s_conj); G; G++) { + if ((UB && (*G).get_coef(v) < 0) + || (!UB && (*G).get_coef(v) > 0) ) { + Relation test_rel(r.n_set()); + test_rel.and_with_GEQ(*G); + return test_rel; + } + } + for(EQ_Iterator E(s_conj); E; E++) { + if ((*E).get_coef(v)) { + Relation test_rel(r.n_set()); + test_rel.and_with_GEQ(*E); + if ((UB && (*E).get_coef(v) > 0) + || (!UB && (*E).get_coef(v) < 0) ) + test_rel = Complement(test_rel); + return test_rel; + } + } + assert(0); + return r; +} + +} + +Relation pickOverhead(Relation r, int liftTo) { + r.simplify(); + Conjunct *s_conj = r.single_conjunct(); + for(GEQ_Iterator G(s_conj); G; G++) { + Relation test_rel(r.n_set()); + test_rel.and_with_GEQ(*G); + Variable_ID v; + coef_t pos = -1; + coef_t c= 0; + for(Constr_Vars_Iter cvi(*G, false); cvi; cvi++) + if ((*cvi).coef && (*cvi).var->kind() == Input_Var + && (*cvi).var->get_position() > pos) { + v = (*cvi).var; + pos = (*cvi).var->get_position(); + c = (*cvi).coef; + } +#if 0 + fprintf(DebugFile,"Coef = %d, constraint = %s\n", + c,(const char *)test_rel.print_formula_to_string()); +#endif + return test_rel; + } + for(EQ_Iterator E(s_conj); E; E++) { + assert(liftTo >= 1); + int pos = max((*E).max_tuple_pos(),max_fs_arity(*E)+1); + +/* Pick stride constraints only when the variables with stride are outer + loop variables */ + if ((*E).has_wildcards() && pos < liftTo) { + Relation test_rel(r.n_set()); + test_rel.and_with_EQ(*E); + return test_rel; + } + else if (!(*E).has_wildcards() && pos <= liftTo) { + Relation test_rel(r.n_set()); + test_rel.and_with_EQ(*E); + test_rel.simplify(); + test_rel = EQs_to_GEQs(test_rel,true); + return pickOverhead(test_rel,liftTo); + } + } + if (code_gen_debug>1) { + fprintf(DebugFile,"Could not find overhead:\n"); + r.prefix_print(DebugFile); + } + return Relation::True(r.n_set()); +} + + + +bool hasBound(Relation r, int level, int UB) { + r.simplify(); + Variable_ID v = set_var(level); + Conjunct *s_conj = r.single_conjunct(); + for(GEQ_Iterator G(s_conj); G; G++) { + if (UB && (*G).get_coef(v) < 0) return true; + if (!UB && (*G).get_coef(v) > 0) return true; + } + for(EQ_Iterator E(s_conj); E; E++) { + if ((*E).get_coef(v)) return true; + } + return false; +} + +bool find_any_constraint(int s, int level, Relation &kr, int direction, + Relation &S, bool approx) { + /* If we don't intersect I with restrictions, the combination + of S and restrictions can be unsatisfiable, which means that + the new split node gets pruned away and we still don't have + finite bounds -> infinite recursion. */ + + Relation I = projected_nIS[level][s]; + I = Gist(I,copy(kr)); + if(approx) I = Approximate(I); + if (hasBound(I,level,direction)) { + Relation pickfrom; + if(has_nonstride_EQ(I,level)) + pickfrom = pickEQ(I,level); + else + pickfrom = pickBound(I,level,direction); + S = pickOverhead(pickfrom,level); + if(S.is_obvious_tautology()) S = Relation::Null(); + return !S.is_null(); + } + return false; +} + + +bool has_nonstride_EQ(Relation r, int level) { + r.simplify(); + Variable_ID v = set_var(level); + Conjunct *s_conj = r.single_conjunct(); + for(EQ_Iterator G(s_conj); G; G++) + if ((*G).get_coef(v) && !(*G).has_wildcards()) + return true; + return false; +} + + +Relation minMaxOverhead(Relation r, int level) { + r.finalize(); + r.simplify(); + Conjunct *s_conj = r.single_conjunct(); + GEQ_Handle LBs[50],UBs[50]; + int numLBs = 0; + int numUBs = 0; + Variable_ID v = set_var(level); + for(GEQ_Iterator G(s_conj); G; G++) if ((*G).get_coef(v)) { + GEQ_Handle g = *G; + if (g.get_coef(v) > 0) LBs[numLBs++] = g; + else UBs[numUBs++] = g; + } + if (numLBs <= 1 && numUBs <= 1) { + return Relation::True(r.n_set()); + } + Relation r1(r.n_set()); + Relation r2(r.n_set()); + if (numLBs > 1) { + // remove a max in lower bound + r1.and_with_GEQ(LBs[0]); + r2.and_with_GEQ(LBs[1]); + r1 = project_onto_levels(Difference(r1,r2),level-1,0); + } + else { + // remove a min in upper bound + r1.and_with_GEQ(UBs[0]); + r2.and_with_GEQ(UBs[1]); + r1 = project_onto_levels(Difference(r1,r2),level-1,0); + } +#if 0 + fprintf(DebugFile,"Testing %s\n",(const char *)r1.print_formula_to_string()); + fprintf(DebugFile,"will removed overhead on bounds of t%d: %s\n",level, + (const char *)r.print_formula_to_string()); +#endif + + return pickOverhead(r1, -1); +} + +std::pair<EQ_Handle, int> find_simplest_assignment(const Relation &R_, Variable_ID v, const std::vector<CG_outputRepr *> &assigned_on_the_fly) { + Relation &R = const_cast<Relation &>(R_); + Conjunct *c = R.single_conjunct(); + + int min_cost = INT_MAX; + EQ_Handle eq; + for (EQ_Iterator ei(c->EQs()); ei; ei++) + if (!(*ei).has_wildcards() && (*ei).get_coef(v) != 0) { + int cost = 0; + + if (abs((*ei).get_coef(v)) != 1) + cost += 4; // divide cost + + int num_var = 0; + for (Constr_Vars_Iter cvi(*ei); cvi; cvi++) + if ((*cvi).var != v) { + num_var++; + if ((*cvi).var->kind() == Global_Var && (*cvi).var->get_global_var()->arity() > 0) { + cost += 10; // function cost + } + if (abs((*cvi).coef) != 1) + cost += 2; // multiply cost + if ((*cvi).var->kind() == Input_Var && assigned_on_the_fly[(*cvi).var->get_position()-1] != NULL) { + cost += 5; // substituted variable cost + } + } + if ((*ei).get_const() != 0) + num_var++; + if (num_var > 1) + cost += num_var - 1; // addition cost + + if (cost < min_cost) { + min_cost = cost; + eq = *ei; + } + } + + return std::make_pair(eq, min_cost); +} + +int max_fs_arity(const Constraint_Handle &c) { + int max_arity=0; + for(Constr_Vars_Iter cv(c); cv; cv++) + if((*cv).var->kind() == Global_Var) + max_arity = max(max_arity,(*cv).var->get_global_var()->arity()); + return max_arity; +} + +} |