From e4b20015a4ee35f1279af4caa983478fa2ff0d4a Mon Sep 17 00:00:00 2001
From: dhuth <derickhuth@gmail.com>
Date: Mon, 6 Oct 2014 11:56:47 -0600
Subject: Added omega to source
---
omega/code_gen/src/CG_utils.cc | 1735 ++++++++++++++++++++++++++++++++++++++++
1 file changed, 1735 insertions(+)
create mode 100755 omega/code_gen/src/CG_utils.cc
(limited to 'omega/code_gen/src/CG_utils.cc')
diff --git a/omega/code_gen/src/CG_utils.cc b/omega/code_gen/src/CG_utils.cc
new file mode 100755
index 0000000..d3a5f71
--- /dev/null
+++ b/omega/code_gen/src/CG_utils.cc
@@ -0,0 +1,1735 @@
+/*****************************************************************************
+ Copyright (C) 1994-2000 the Omega Project Team
+ Copyright (C) 2005-2011 Chun Chen
+ All Rights Reserved.
+
+ Purpose:
+ Utility functions for processing CG tree.
+
+ Notes:
+
+ History:
+ 07/19/07 when generating output variable substitutions for a mapping
+ relation, map it to each output to get correct equality, -chun
+ 07/29/10 when translating equality to assignment, generate appropriate
+ if-condition when necesssary, -chun
+*****************************************************************************/
+
+#include <typeinfo>
+#include <omega.h>
+#include <code_gen/CG.h>
+#include <code_gen/CG_utils.h>
+#include <code_gen/codegen_error.h>
+#include <math.h>
+#include <stack>
+
+namespace omega {
+
+int checkLoopLevel;
+int stmtForLoopCheck;
+int upperBoundForLevel;
+int lowerBoundForLevel;
+bool fillInBounds;
+
+//trick to static init checkLoopLevel to 0
+class JunkStaticInit{ public: JunkStaticInit(){ checkLoopLevel=0; fillInBounds=false;} };
+static JunkStaticInit junkInitInstance__;
+
+
+
+
+namespace {
+
+Relation find_best_guard(const Relation &R, const BoolSet<> &active, const std::map<int, Relation> &guards) {
+ std::pair<int, int> best_cost = std::make_pair(0, 0);
+ Relation best_cond = Relation::True(R.n_set());
+
+ Relation r = copy(R);
+ int max_iter_count = 2*(r.single_conjunct()->n_EQs()) + r.single_conjunct()->n_GEQs();
+ int iter_count = 0;
+ while (!r.is_obvious_tautology()) {
+ std::pair<int, int> cost = std::make_pair(0, 0);
+ Relation cond = pick_one_guard(r);
+ Relation complement_cond = Complement(copy(cond));
+ complement_cond.simplify();
+ for (BoolSet<>::const_iterator i = active.begin(); i != active.end(); i++) {
+ std::map<int, Relation>::const_iterator j = guards.find(*i);
+ if (j == guards.end())
+ continue;
+ if (Must_Be_Subset(copy(j->second), copy(cond)))
+ cost.first++;
+ else if (Must_Be_Subset(copy(j->second), copy(complement_cond)))
+ cost.second++;
+ }
+ if (cost > best_cost) {
+ best_cost = cost;
+ best_cond = copy(cond);
+ }
+ r = Gist(r, cond, 1);
+
+ if (iter_count > max_iter_count)
+ throw codegen_error("guard condition too complex to handle");
+
+ iter_count++;
+ }
+
+ return best_cond;
+}
+
+
+Relation find_best_guard(const Relation &R, const std::vector<CG_loop *> &loops, int start, int end) {
+ std::pair<int, int> best_cost = std::make_pair(0, 0);
+ Relation best_cond = Relation::True(R.n_set());
+
+ Relation r = copy(R);
+ int max_iter_count = 2*(r.single_conjunct()->n_EQs()) + r.single_conjunct()->n_GEQs();
+ int iter_count = 0;
+ while (!r.is_obvious_tautology()) {
+ std::pair<int, int> cost = std::make_pair(0, 0);
+ Relation cond = pick_one_guard(r);
+ int i = start;
+ for ( ; i < end; i++) {
+ if (Must_Be_Subset(copy(loops[i]->guard_), copy(cond)))
+ cost.first++;
+ else
+ break;
+ }
+ Relation complement_cond = Complement(copy(cond));
+ complement_cond.simplify();
+ for (int j = i; j < end; j++)
+ if (Must_Be_Subset(copy(loops[j]->guard_), copy(complement_cond)))
+ cost.second++;
+ else
+ break;
+
+ if (cost > best_cost) {
+ best_cost = cost;
+ best_cond = copy(cond);
+ }
+ r = Gist(r, cond, 1);
+
+ if (iter_count > max_iter_count)
+ throw codegen_error("guard condition too complex to handle");
+
+ iter_count++;
+ }
+
+ return best_cond;
+}
+
+}
+
+bool bound_must_hit_stride(const GEQ_Handle &inequality, Variable_ID v, const EQ_Handle &stride_eq, Variable_ID wc, const Relation &bounds, const Relation &known) {
+ assert(inequality.get_coef(v) != 0 && abs(stride_eq.get_coef(v)) == 1 && wc->kind() == Wildcard_Var && abs(stride_eq.get_coef(wc)) > 1);
+
+ // if bound expression uses floor operation, bail out for now
+ // TODO: in the future, handle this
+ if (abs(inequality.get_coef(v)) != 1)
+ return false;
+
+ coef_t stride = abs(stride_eq.get_coef(wc));
+
+ Relation r1(known.n_set());
+ F_Exists *f_exists1 = r1.add_and()->add_exists();
+ F_And *f_root1 = f_exists1->add_and();
+ std::map<Variable_ID, Variable_ID> exists_mapping1;
+ EQ_Handle h1 = f_root1->add_EQ();
+ Relation r2(known.n_set());
+ F_Exists *f_exists2 = r2.add_and()->add_exists();
+ F_And *f_root2 = f_exists2->add_and();
+ std::map<Variable_ID, Variable_ID> exists_mapping2;
+ EQ_Handle h2 = f_root2->add_EQ();
+ for (Constr_Vars_Iter cvi(inequality); cvi; cvi++) {
+ Variable_ID v = cvi.curr_var();
+ switch (v->kind()) {
+ case Input_Var:
+ h1.update_coef(r1.input_var(v->get_position()), cvi.curr_coef());
+ h2.update_coef(r2.input_var(v->get_position()), cvi.curr_coef());
+ break;
+ case Global_Var: {
+ Global_Var_ID g = v->get_global_var();
+ Variable_ID v1, v2;
+ if (g->arity() == 0) {
+ v1 = r1.get_local(g);
+ v2 = r2.get_local(g);
+ }
+ else {
+ v1 = r1.get_local(g, v->function_of());
+ v2 = r2.get_local(g, v->function_of());
+ }
+ h1.update_coef(v1, cvi.curr_coef());
+ h2.update_coef(v2, cvi.curr_coef());
+ break;
+ }
+ case Wildcard_Var: {
+ Variable_ID v1 = replicate_floor_definition(bounds, v, r1, f_exists1, f_root1, exists_mapping1);
+ Variable_ID v2 = replicate_floor_definition(bounds, v, r2, f_exists2, f_root2, exists_mapping2);
+ h1.update_coef(v1, cvi.curr_coef());
+ h2.update_coef(v2, cvi.curr_coef());
+ break;
+ }
+ default:
+ assert(false);
+ }
+ }
+ h1.update_const(inequality.get_const());
+ h1.update_coef(f_exists1->declare(), stride);
+ h2.update_const(inequality.get_const());
+ r1.simplify();
+ r2.simplify();
+
+ Relation all_known = Intersection(copy(bounds), copy(known));
+ all_known.simplify();
+
+ if (Gist(r1, copy(all_known), 1).is_obvious_tautology()) {
+ Relation r3(known.n_set());
+ F_Exists *f_exists3 = r3.add_and()->add_exists();
+ F_And *f_root3 = f_exists3->add_and();
+ std::map<Variable_ID, Variable_ID> exists_mapping3;
+ EQ_Handle h3 = f_root3->add_EQ();
+ for (Constr_Vars_Iter cvi(stride_eq); cvi; cvi++) {
+ Variable_ID v= cvi.curr_var();
+ switch (v->kind()) {
+ case Input_Var:
+ h3.update_coef(r3.input_var(v->get_position()), cvi.curr_coef());
+ break;
+ case Global_Var: {
+ Global_Var_ID g = v->get_global_var();
+ Variable_ID v3;
+ if (g->arity() == 0)
+ v3 = r3.get_local(g);
+ else
+ v3 = r3.get_local(g, v->function_of());
+ h3.update_coef(v3, cvi.curr_coef());
+ break;
+ }
+ case Wildcard_Var:
+ if (v == wc)
+ h3.update_coef(f_exists3->declare(), cvi.curr_coef());
+ else {
+ Variable_ID v3 = replicate_floor_definition(bounds, v, r3, f_exists3, f_root3, exists_mapping3);
+ h3.update_coef(v3, cvi.curr_coef());
+ }
+ break;
+ default:
+ assert(false);
+ }
+ }
+ h3.update_const(stride_eq.get_const());
+ r3.simplify();
+
+ if (Gist(r3, Intersection(r2, all_known), 1).is_obvious_tautology())
+ return true;
+ else
+ return false;
+ }
+ else
+ return false;
+}
+
+
+//
+// output variable by its name, however if this variable need to be substituted,
+// return the substitution.
+//
+CG_outputRepr *output_ident(CG_outputBuilder *ocg, const Relation &R, Variable_ID v, const std::vector<std::pair<CG_outputRepr *, int> > &assigned_on_the_fly) {
+ const_cast<Relation &>(R).setup_names(); // hack
+
+ if (v->kind() == Input_Var) {
+ int pos = v->get_position();
+ if (assigned_on_the_fly[pos-1].first != NULL)
+ return assigned_on_the_fly[pos-1].first->clone();
+ else
+ return ocg->CreateIdent(v->name());
+ }
+ else if (v->kind() == 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();
+ std::vector<CG_outputRepr *> argList;
+ for(int i = 1; i <= arity; i++)
+ argList.push_back(ocg->CreateIdent(const_cast<Relation &>(R).input_var(i)->name()));
+ CG_outputRepr *call = ocg->CreateInvoke(v->get_global_var()->base_name(), argList);
+ return call;
+ }
+ }
+ else
+ assert(false);
+}
+
+
+//
+// return pair<if condition, <assignment rhs, assignment cost> >
+//
+std::pair<CG_outputRepr *, std::pair<CG_outputRepr *, int> > output_assignment(CG_outputBuilder *ocg, const Relation &R, int level, const Relation &known, const std::vector<std::pair<CG_outputRepr *, int> > &assigned_on_the_fly) {
+ Variable_ID v = const_cast<Relation &>(R).set_var(level);
+ Conjunct *c = const_cast<Relation &>(R).single_conjunct();
+
+ std::pair<EQ_Handle, int> result = find_simplest_assignment(R, v, assigned_on_the_fly);
+
+ if (result.second == INT_MAX)
+ return std::make_pair(static_cast<CG_outputRepr *>(NULL), std::make_pair(static_cast<CG_outputRepr *>(NULL), INT_MAX));
+
+ CG_outputRepr *if_repr = NULL;
+ CG_outputRepr *assign_repr = NULL;
+ // check whether to generate if-conditions from equality constraints
+ if (abs(result.first.get_coef(v)) != 1) {
+ Relation r(R.n_set());
+ F_Exists *f_exists = r.add_and()->add_exists();
+ F_And *f_root = f_exists->add_and();
+ std::map<Variable_ID, Variable_ID> exists_mapping;
+ exists_mapping[v] = f_exists->declare();
+
+ EQ_Handle h = f_root->add_EQ();
+ for (Constr_Vars_Iter cvi(result.first); cvi; cvi++)
+ switch (cvi.curr_var()->kind()) {
+ case Input_Var: {
+ if (cvi.curr_var() == v)
+ h.update_coef(exists_mapping[v], cvi.curr_coef());
+ else
+ h.update_coef(r.set_var(cvi.curr_var()->get_position()), cvi.curr_coef());
+ break;
+ }
+ case Global_Var: {
+ Global_Var_ID g = cvi.curr_var()->get_global_var();
+ Variable_ID v2;
+ if (g->arity() == 0)
+ v2 = r.get_local(g);
+ else
+ v2 = r.get_local(g, cvi.curr_var()->function_of());
+ h.update_coef(v2, cvi.curr_coef());
+ break;
+ }
+ case Wildcard_Var: {
+ std::map<Variable_ID, Variable_ID>::iterator p = exists_mapping.find(cvi.curr_var());
+ Variable_ID v2;
+ if (p == exists_mapping.end()) {
+ v2 = f_exists->declare();
+ exists_mapping[cvi.curr_var()] = v2;
+ }
+ else
+ v2 = p->second;
+ h.update_coef(v2, cvi.curr_coef());
+ break;
+ }
+ default:
+ assert(0);
+ }
+ h.update_const(result.first.get_const());
+
+ for (EQ_Iterator e(c->EQs()); e; e++)
+ if (!((*e) == result.first)) {
+ EQ_Handle h = f_root->add_EQ();
+ for (Constr_Vars_Iter cvi(*e); cvi; cvi++)
+ switch (cvi.curr_var()->kind()) {
+ case Input_Var: {
+ assert(cvi.curr_var() != v);
+ h.update_coef(r.set_var(cvi.curr_var()->get_position()), cvi.curr_coef());
+ break;
+ }
+ case Global_Var: {
+ Global_Var_ID g = cvi.curr_var()->get_global_var();
+ Variable_ID v2;
+ if (g->arity() == 0)
+ v2 = r.get_local(g);
+ else
+ v2 = r.get_local(g, cvi.curr_var()->function_of());
+ h.update_coef(v2, cvi.curr_coef());
+ break;
+ }
+ case Wildcard_Var: {
+ std::map<Variable_ID, Variable_ID>::iterator p = exists_mapping.find(cvi.curr_var());
+ Variable_ID v2;
+ if (p == exists_mapping.end()) {
+ v2 = f_exists->declare();
+ exists_mapping[cvi.curr_var()] = v2;
+ }
+ else
+ v2 = p->second;
+ h.update_coef(v2, cvi.curr_coef());
+ break;
+ }
+ default:
+ assert(0);
+ }
+ h.update_const((*e).get_const());
+ }
+
+ for (GEQ_Iterator e(c->GEQs()); e; e++) {
+ GEQ_Handle h = f_root->add_GEQ();
+ for (Constr_Vars_Iter cvi(*e); cvi; cvi++)
+ switch (cvi.curr_var()->kind()) {
+ case Input_Var: {
+ h.update_coef(r.set_var(cvi.curr_var()->get_position()), cvi.curr_coef());
+ break;
+ }
+ case Global_Var: {
+ Global_Var_ID g = cvi.curr_var()->get_global_var();
+ Variable_ID v2;
+ if (g->arity() == 0)
+ v2 = r.get_local(g);
+ else
+ v2 = r.get_local(g, cvi.curr_var()->function_of());
+ h.update_coef(v2, cvi.curr_coef());
+ break;
+ }
+ case Wildcard_Var: {
+ std::map<Variable_ID, Variable_ID>::iterator p = exists_mapping.find(cvi.curr_var());
+ Variable_ID v2;
+ if (p == exists_mapping.end()) {
+ v2 = f_exists->declare();
+ exists_mapping[cvi.curr_var()] = v2;
+ }
+ else
+ v2 = p->second;
+ h.update_coef(v2, cvi.curr_coef());
+ break;
+ }
+ default:
+ assert(0);
+ }
+ h.update_const((*e).get_const());
+ }
+
+ r.simplify();
+ if (!Gist(r, copy(known), 1).is_obvious_tautology()) {
+ CG_outputRepr *lhs = output_substitution_repr(ocg, result.first, v, false, R, assigned_on_the_fly);
+ if_repr = ocg->CreateEQ(ocg->CreateIntegerMod(lhs->clone(), ocg->CreateInt(abs(result.first.get_coef(v)))), ocg->CreateInt(0));
+ assign_repr = ocg->CreateDivide(lhs, ocg->CreateInt(abs(result.first.get_coef(v))));
+ }
+ else
+ assign_repr = output_substitution_repr(ocg, result.first, v, true, R, assigned_on_the_fly);
+ }
+ else
+ assign_repr = output_substitution_repr(ocg, result.first, v, true, R, assigned_on_the_fly);
+
+ if (assign_repr == NULL)
+ assign_repr = ocg->CreateInt(0);
+
+ return std::make_pair(if_repr, std::make_pair(assign_repr, result.second));
+}
+
+
+//
+// return NULL if 0
+//
+CG_outputRepr *output_substitution_repr(CG_outputBuilder *ocg, const EQ_Handle &equality, Variable_ID v, bool apply_v_coef, const Relation &R, const std::vector<std::pair<CG_outputRepr *, int> > &assigned_on_the_fly) {
+ const_cast<Relation &>(R).setup_names(); // hack
+
+ coef_t a = equality.get_coef(v);
+ assert(a != 0);
+
+ CG_outputRepr *repr = NULL;
+ for (Constr_Vars_Iter cvi(equality); cvi; cvi++)
+ if (cvi.curr_var() != v) {
+ CG_outputRepr *t;
+ if (cvi.curr_var()->kind() == Wildcard_Var) {
+ std::pair<bool, GEQ_Handle> result = find_floor_definition(R, cvi.curr_var());
+ if (!result.first) {
+ delete repr;
+ throw codegen_error("can't output non floor defined wildcard");
+ }
+ t = output_inequality_repr(ocg, result.second, cvi.curr_var(), R, assigned_on_the_fly);
+ }
+ else
+ t = output_ident(ocg, R, cvi.curr_var(), assigned_on_the_fly);
+ coef_t coef = cvi.curr_coef();
+
+ if (a > 0) {
+ if (coef > 0) {
+ if (coef == 1)
+ repr = ocg->CreateMinus(repr, t);
+ else
+ repr = ocg->CreateMinus(repr, ocg->CreateTimes(ocg->CreateInt(coef), t));
+ }
+ else { // coef < 0
+ if (coef == -1)
+ repr = ocg->CreatePlus(repr, t);
+ else
+ repr = ocg->CreatePlus(repr, ocg->CreateTimes(ocg->CreateInt(-coef), t));
+ }
+ }
+ else {
+ if (coef > 0) {
+ if (coef == 1)
+ repr = ocg->CreatePlus(repr, t);
+ else
+ repr = ocg->CreatePlus(repr, ocg->CreateTimes(ocg->CreateInt(coef), t));
+ }
+ else { // coef < 0
+ if (coef == -1)
+ repr = ocg->CreateMinus(repr, t);
+ else
+ repr = ocg->CreateMinus(repr, ocg->CreateTimes(ocg->CreateInt(-coef), t));
+ }
+ }
+ }
+
+ int c = equality.get_const();
+ if (a > 0) {
+ if (c > 0)
+ repr = ocg->CreateMinus(repr, ocg->CreateInt(c));
+ else if (c < 0)
+ repr = ocg->CreatePlus(repr, ocg->CreateInt(-c));
+ }
+ else {
+ if (c > 0)
+ repr = ocg->CreatePlus(repr, ocg->CreateInt(c));
+ else if (c < 0)
+ repr = ocg->CreateMinus(repr, ocg->CreateInt(-c));
+ }
+
+ if (apply_v_coef && abs(a) != 1)
+ repr = ocg->CreateDivide(repr, ocg->CreateInt(abs(a)));
+
+ return repr;
+}
+
+
+//
+// original Substitutions class from omega can't handle integer
+// division, this is new way.
+//
+std::vector<CG_outputRepr*> output_substitutions(CG_outputBuilder *ocg, const Relation &R, const std::vector<std::pair<CG_outputRepr *, int> > &assigned_on_the_fly) {
+ std::vector<CG_outputRepr *> subs;
+
+ for (int i = 1; i <= R.n_out(); i++) {
+ Relation mapping(R.n_out(), 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 r = Composition(mapping, copy(R));
+ r.simplify();
+
+ Variable_ID v = r.output_var(1);
+ CG_outputRepr *repr = NULL;
+ std::pair<EQ_Handle, int> result = find_simplest_assignment(r, v, assigned_on_the_fly);
+ if (result.second < INT_MAX)
+ repr = output_substitution_repr(ocg, result.first, v, true, r, assigned_on_the_fly);
+ else {
+ std::pair<bool, GEQ_Handle> result = find_floor_definition(R, v);
+ if (result.first)
+ try {
+ repr = output_inequality_repr(ocg, result.second, v, R, assigned_on_the_fly);
+ }
+ catch (const codegen_error &) {
+ }
+ }
+
+ subs.push_back(repr);
+ }
+
+ return subs;
+}
+
+
+//
+// handle floor definition wildcards in equality, the second in returned pair
+// is the cost.
+//
+std::pair<EQ_Handle, int> find_simplest_assignment(const Relation &R, Variable_ID v, const std::vector<std::pair<CG_outputRepr *, int> > &assigned_on_the_fly) {
+ Conjunct *c = const_cast<Relation &>(R).single_conjunct();
+
+ int min_cost = INT_MAX;
+ EQ_Handle eq;
+ for (EQ_Iterator e(c->EQs()); e; e++)
+ if (!(*e).has_wildcards() && (*e).get_coef(v) != 0) {
+ int cost = 0;
+
+ if (abs((*e).get_coef(v)) != 1)
+ cost += 4; // divide cost
+
+ int num_var = 0;
+ for (Constr_Vars_Iter cvi(*e); cvi; cvi++)
+ if (cvi.curr_var() != v) {
+ num_var++;
+ if (abs(cvi.curr_coef()) != 1)
+ cost += 2; // multiply cost
+ if (cvi.curr_var()->kind() == Global_Var && cvi.curr_var()->get_global_var()->arity() > 0)
+ cost += 10; // function cost
+ else if (cvi.curr_var()->kind() == Input_Var &&
+ assigned_on_the_fly.size() >= cvi.curr_var()->get_position() &&
+ assigned_on_the_fly[cvi.curr_var()->get_position()-1].first != NULL)
+ cost += assigned_on_the_fly[cvi.curr_var()->get_position()-1].second; // substitution cost on record
+ }
+ if ((*e).get_const() != 0)
+ num_var++;
+ if (num_var > 1)
+ cost += num_var - 1; // addition cost
+
+ if (cost < min_cost) {
+ min_cost = cost;
+ eq = *e;
+ }
+ }
+
+ if (min_cost < INT_MAX)
+ return std::make_pair(eq, min_cost);
+
+ for (EQ_Iterator e(c->EQs()); e; e++)
+ if ((*e).has_wildcards() && (*e).get_coef(v) != 0) {
+ bool is_assignment = true;
+ for (Constr_Vars_Iter cvi(*e, true); cvi; cvi++) {
+ std::pair<bool, GEQ_Handle> result = find_floor_definition(R, v);
+ if (!result.first) {
+ is_assignment = false;
+ break;
+ }
+ }
+ if (!is_assignment)
+ continue;
+
+ int cost = 0;
+
+ if (abs((*e).get_coef(v)) != 1)
+ cost += 4; // divide cost
+
+ int num_var = 0;
+ for (Constr_Vars_Iter cvi(*e); cvi; cvi++)
+ if (cvi.curr_var() != v) {
+ num_var++;
+ if (abs(cvi.curr_coef()) != 1)
+ cost += 2; // multiply cost
+ if (cvi.curr_var()->kind() == Wildcard_Var)
+ cost += 10; // floor operation cost
+ else if (cvi.curr_var()->kind() == Global_Var && cvi.curr_var()->get_global_var()->arity() > 0)
+ cost += 20; // function cost
+ else if (cvi.curr_var()->kind() == Input_Var &&
+ assigned_on_the_fly.size() >= cvi.curr_var()->get_position() &&
+ assigned_on_the_fly[cvi.curr_var()->get_position()-1].first != NULL)
+ cost += assigned_on_the_fly[cvi.curr_var()->get_position()-1].second; // substitution cost on record
+ }
+ if ((*e).get_const() != 0)
+ num_var++;
+ if (num_var > 1)
+ cost += num_var - 1; // addition cost
+
+ if (cost < min_cost) {
+ min_cost = cost;
+ eq = *e;
+ }
+ }
+
+ return std::make_pair(eq, min_cost);
+}
+
+
+//
+// find floor definition for variable v, e.g. m-c <= 4v <= m, (c is
+// constant and 0 <= c < 4). this translates to v = floor(m, 4) and
+// return 4v<=m in this case. All wildcards in such inequality are
+// also floor defined.
+//
+std::pair<bool, GEQ_Handle> find_floor_definition(const Relation &R, Variable_ID v, std::set<Variable_ID> excluded_floor_vars) {
+ Conjunct *c = const_cast<Relation &>(R).single_conjunct();
+
+ excluded_floor_vars.insert(v);
+ for (GEQ_Iterator e = c->GEQs(); e; e++) {
+ coef_t a = (*e).get_coef(v);
+ if (a >= -1)
+ continue;
+ a = -a;
+
+ bool interested = true;
+ for (std::set<Variable_ID>::const_iterator i = excluded_floor_vars.begin(); i != excluded_floor_vars.end(); i++)
+ if ((*i) != v && (*e).get_coef(*i) != 0) {
+ interested = false;
+ break;
+ }
+ if (!interested)
+ continue;
+
+ // check if any wildcard is floor defined
+ bool has_undefined_wc = false;
+ for (Constr_Vars_Iter cvi(*e, true); cvi; cvi++)
+ if (excluded_floor_vars.find(cvi.curr_var()) == excluded_floor_vars.end()) {
+ std::pair<bool, GEQ_Handle> result = find_floor_definition(R, cvi.curr_var(), excluded_floor_vars);
+ if (!result.first) {
+ has_undefined_wc = true;
+ break;
+ }
+ }
+ if (has_undefined_wc)
+ continue;
+
+ // find the matching upper bound for floor definition
+ for (GEQ_Iterator e2 = c->GEQs(); e2; e2++)
+ if ((*e2).get_coef(v) == a && (*e).get_const() + (*e2).get_const() < a) {
+ bool match = true;
+ for (Constr_Vars_Iter cvi(*e); cvi; cvi++)
+ if ((*e2).get_coef(cvi.curr_var()) != -cvi.curr_coef()) {
+ match = false;
+ break;
+ }
+ if (!match)
+ continue;
+ for (Constr_Vars_Iter cvi(*e2); cvi; cvi++)
+ if ((*e).get_coef(cvi.curr_var()) != -cvi.curr_coef()) {
+ match = false;
+ break;
+ }
+ if (match)
+ return std::make_pair(true, *e);
+ }
+ }
+
+ return std::make_pair(false, GEQ_Handle());
+}
+
+//
+// find the stride involving the specified variable, the stride
+// equality can have other wildcards as long as they are defined as
+// floor variables.
+//
+std::pair<EQ_Handle, Variable_ID> find_simplest_stride(const Relation &R, Variable_ID v) {
+ int best_num_var = INT_MAX;
+ coef_t best_coef;
+ EQ_Handle best_eq;
+ Variable_ID best_stride_wc;
+ for (EQ_Iterator e(const_cast<Relation &>(R).single_conjunct()->EQs()); e; e++)
+ if ((*e).has_wildcards() && (*e).get_coef(v) != 0) {
+ bool is_stride = true;
+ bool found_free = false;
+ int num_var = 0;
+ int num_floor = 0;
+ Variable_ID stride_wc;
+ for (Constr_Vars_Iter cvi(*e); cvi; cvi++) {
+ switch (cvi.curr_var()->kind()) {
+ case Wildcard_Var: {
+ bool is_free = true;
+ for (GEQ_Iterator e2(const_cast<Relation &>(R).single_conjunct()->GEQs()); e2; e2++)
+ if ((*e2).get_coef(cvi.curr_var()) != 0) {
+ is_free = false;
+ break;
+ }
+ if (is_free) {
+ if (found_free)
+ is_stride = false;
+ else {
+ found_free = true;
+ stride_wc = cvi.curr_var();
+ }
+ }
+ else {
+ std::pair<bool, GEQ_Handle> result = find_floor_definition(R, cvi.curr_var());
+ if (result.first)
+ num_floor++;
+ else
+ is_stride = false;
+ }
+ break;
+ }
+ case Input_Var:
+ num_var++;
+ break;
+ default:
+ ;
+ }
+
+ if (!is_stride)
+ break;
+ }
+
+ if (is_stride) {
+ coef_t coef = abs((*e).get_coef(v));
+ if (best_num_var == INT_MAX || coef < best_coef ||
+ (coef == best_coef && num_var < best_num_var)) {
+ best_coef = coef;
+ best_num_var = num_var;
+ best_eq = *e;
+ best_stride_wc = stride_wc;
+ }
+ }
+ }
+
+ if (best_num_var != INT_MAX)
+ return std::make_pair(best_eq, best_stride_wc);
+ else
+ return std::make_pair(EQ_Handle(), static_cast<Variable_ID>(NULL));
+}
+
+//
+// convert relation to if-condition
+//
+CG_outputRepr *output_guard(CG_outputBuilder *ocg, const Relation &R, const std::vector<std::pair<CG_outputRepr *, int> > &assigned_on_the_fly) {
+ assert(R.n_out()==0);
+
+ CG_outputRepr *result = NULL;
+ Conjunct *c = const_cast<Relation &>(R).single_conjunct();
+
+ // e.g. 4i=5*j
+ for (EQ_Iterator e = c->EQs(); e; e++)
+ if (!(*e).has_wildcards()) {
+ CG_outputRepr *lhs = NULL;
+ CG_outputRepr *rhs = NULL;
+ for (Constr_Vars_Iter cvi(*e); cvi; cvi++) {
+ CG_outputRepr *v = output_ident(ocg, R, cvi.curr_var(), assigned_on_the_fly);
+ coef_t coef = cvi.curr_coef();
+ if (coef > 0) {
+ if (coef == 1)
+ lhs = ocg->CreatePlus(lhs, v);
+ else
+ lhs = ocg->CreatePlus(lhs, ocg->CreateTimes(ocg->CreateInt(coef), v));
+ }
+ else { // coef < 0
+ if (coef == -1)
+ rhs = ocg->CreatePlus(rhs, v);
+ else
+ rhs = ocg->CreatePlus(rhs, ocg->CreateTimes(ocg->CreateInt(-coef), v));
+ }
+ }
+ coef_t c = (*e).get_const();
+
+ CG_outputRepr *term;
+ if (lhs == NULL)
+ term = ocg->CreateEQ(rhs, ocg->CreateInt(c));
+ else {
+ if (c > 0)
+ rhs = ocg->CreateMinus(rhs, ocg->CreateInt(c));
+ else if (c < 0)
+ rhs = ocg->CreatePlus(rhs, ocg->CreateInt(-c));
+ else if (rhs == NULL)
+ rhs = ocg->CreateInt(0);
+ term = ocg->CreateEQ(lhs, rhs);
+ }
+ result = ocg->CreateAnd(result, term);
+ }
+
+ // e.g. i>5j
+ for (GEQ_Iterator e = c->GEQs(); e; e++)
+ if (!(*e).has_wildcards()) {
+ CG_outputRepr *lhs = NULL;
+ CG_outputRepr *rhs = NULL;
+ for (Constr_Vars_Iter cvi(*e); cvi; cvi++) {
+ CG_outputRepr *v = output_ident(ocg, R, cvi.curr_var(), assigned_on_the_fly);
+ coef_t coef = cvi.curr_coef();
+ if (coef > 0) {
+ if (coef == 1)
+ lhs = ocg->CreatePlus(lhs, v);
+ else
+ lhs = ocg->CreatePlus(lhs, ocg->CreateTimes(ocg->CreateInt(coef), v));
+ }
+ else { // coef < 0
+ if (coef == -1)
+ rhs = ocg->CreatePlus(rhs, v);
+ else
+ rhs = ocg->CreatePlus(rhs, ocg->CreateTimes(ocg->CreateInt(-coef), v));
+ }
+ }
+ coef_t c = (*e).get_const();
+
+ CG_outputRepr *term;
+ if (lhs == NULL)
+ term = ocg->CreateLE(rhs, ocg->CreateInt(c));
+ else {
+ if (c > 0)
+ rhs = ocg->CreateMinus(rhs, ocg->CreateInt(c));
+ else if (c < 0)
+ rhs = ocg->CreatePlus(rhs, ocg->CreateInt(-c));
+ else if (rhs == NULL)
+ rhs = ocg->CreateInt(0);
+ term = ocg->CreateGE(lhs, rhs);
+ }
+ result = ocg->CreateAnd(result, term);
+ }
+
+ // e.g. 4i=5j+4alpha
+ for (EQ_Iterator e = c->EQs(); e; e++)
+ if ((*e).has_wildcards()) {
+ Variable_ID wc;
+ int num_wildcard = 0;
+ int num_positive = 0;
+ int num_negative = 0;
+ for (Constr_Vars_Iter cvi(*e); cvi; cvi++) {
+ if (cvi.curr_var()->kind() == Wildcard_Var) {
+ num_wildcard++;
+ wc = cvi.curr_var();
+ }
+ else {
+ if (cvi.curr_coef() > 0)
+ num_positive++;
+ else
+ num_negative++;
+ }
+ }
+
+ if (num_wildcard > 1) {
+ delete result;
+ throw codegen_error("Can't generate equality condition with multiple wildcards");
+ }
+ int sign = (num_positive>=num_negative)?1:-1;
+
+ CG_outputRepr *lhs = NULL;
+ for (Constr_Vars_Iter cvi(*e); cvi; cvi++) {
+ if (cvi.curr_var() != wc) {
+ CG_outputRepr *v = output_ident(ocg, R, cvi.curr_var(), assigned_on_the_fly);
+ coef_t coef = cvi.curr_coef();
+ if (sign == 1) {
+ if (coef > 0) {
+ if (coef == 1)
+ lhs = ocg->CreatePlus(lhs, v);
+ else
+ lhs = ocg->CreatePlus(lhs, ocg->CreateTimes(ocg->CreateInt(coef), v));
+ }
+ else { // coef < 0
+ if (coef == -1)
+ lhs = ocg->CreateMinus(lhs, v);
+ else
+ lhs = ocg->CreateMinus(lhs, ocg->CreateTimes(ocg->CreateInt(-coef), v));
+ }
+ }
+ else {
+ if (coef > 0) {
+ if (coef == 1)
+ lhs = ocg->CreateMinus(lhs, v);
+ else
+ lhs = ocg->CreateMinus(lhs, ocg->CreateTimes(ocg->CreateInt(coef), v));
+ }
+ else { // coef < 0
+ if (coef == -1)
+ lhs = ocg->CreatePlus(lhs, v);
+ else
+ lhs = ocg->CreatePlus(lhs, ocg->CreateTimes(ocg->CreateInt(-coef), v));
+ }
+ }
+ }
+ }
+ coef_t c = (*e).get_const();
+ if (sign == 1) {
+ if (c > 0)
+ lhs = ocg->CreatePlus(lhs, ocg->CreateInt(c));
+ else if (c < 0)
+ lhs = ocg->CreateMinus(lhs, ocg->CreateInt(-c));
+ }
+ else {
+ if (c > 0)
+ lhs = ocg->CreateMinus(lhs, ocg->CreateInt(c));
+ else if (c < 0)
+ lhs = ocg->CreatePlus(lhs, ocg->CreateInt(-c));
+ }
+
+ lhs = ocg->CreateIntegerMod(lhs, ocg->CreateInt(abs((*e).get_coef(wc))));
+ CG_outputRepr *term = ocg->CreateEQ(lhs, ocg->CreateInt(0));
+ result = ocg->CreateAnd(result, term);
+ }
+
+ // e.g. 4alpha<=i<=5alpha
+ for (GEQ_Iterator e = c->GEQs(); e; e++)
+ if ((*e).has_wildcards()) {
+ Variable_ID wc;
+ int num_wildcard = 0;
+ for (Constr_Vars_Iter cvi(*e, true); cvi; cvi++)
+ if (num_wildcard == 0) {
+ wc = cvi.curr_var();
+ num_wildcard = 1;
+ }
+ else
+ num_wildcard++;
+
+ if (num_wildcard > 1) {
+ delete result;
+ // 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");
+ }
+
+ coef_t c = (*e).get_coef(wc);
+ int sign = (c>0)?1:-1;
+
+ GEQ_Iterator e2 = e;
+ e2++;
+ for ( ; e2; e2++) {
+ coef_t c2 = (*e2).get_coef(wc);
+ if (c2 == 0)
+ continue;
+ int sign2 = (c2>0)?1:-1;
+ if (sign != -sign2)
+ continue;
+ int num_wildcard2 = 0;
+ for (Constr_Vars_Iter cvi(*e2, true); cvi; cvi++)
+ num_wildcard2++;
+ if (num_wildcard2 > 1)
+ continue;
+
+ GEQ_Handle lb, ub;
+ if (sign == 1) {
+ lb = (*e);
+ ub = (*e2);
+ }
+ else {
+ lb = (*e2);
+ ub = (*e);
+ }
+
+ CG_outputRepr *lhs = NULL;
+ for (Constr_Vars_Iter cvi(lb); cvi; cvi++)
+ if (cvi.curr_var() != wc) {
+ CG_outputRepr *v = output_ident(ocg, R, cvi.curr_var(), assigned_on_the_fly);
+ coef_t coef = cvi.curr_coef();
+ if (coef > 0) {
+ if (coef == 1)
+ lhs = ocg->CreateMinus(lhs, v);
+ else
+ lhs = ocg->CreateMinus(lhs, ocg->CreateTimes(ocg->CreateInt(coef), v));
+ }
+ else { // coef < 0
+ if (coef == -1)
+ lhs = ocg->CreatePlus(lhs, v);
+ else
+ lhs = ocg->CreatePlus(lhs, ocg->CreateTimes(ocg->CreateInt(-coef), v));
+ }
+ }
+ coef_t c = lb.get_const();
+ if (c > 0)
+ lhs = ocg->CreateMinus(lhs, ocg->CreateInt(c));
+ else if (c < 0)
+ lhs = ocg->CreatePlus(lhs, ocg->CreateInt(-c));
+
+ CG_outputRepr *rhs = NULL;
+ for (Constr_Vars_Iter cvi(ub); cvi; cvi++)
+ if (cvi.curr_var() != wc) {
+ CG_outputRepr *v = output_ident(ocg, R, cvi.curr_var(), assigned_on_the_fly);
+ coef_t coef = cvi.curr_coef();
+ if (coef > 0) {
+ if (coef == 1)
+ rhs = ocg->CreatePlus(rhs, v);
+ else
+ rhs = ocg->CreatePlus(rhs, ocg->CreateTimes(ocg->CreateInt(coef), v));
+ }
+ else { // coef < 0
+ if (coef == -1)
+ rhs = ocg->CreateMinus(rhs, v);
+ else
+ rhs = ocg->CreateMinus(rhs, ocg->CreateTimes(ocg->CreateInt(-coef), v));
+ }
+ }
+ c = ub.get_const();
+ if (c > 0)
+ rhs = ocg->CreatePlus(rhs, ocg->CreateInt(c));
+ else if (c < 0)
+ rhs = ocg->CreateMinus(rhs, ocg->CreateInt(-c));
+
+ rhs = ocg->CreateIntegerFloor(rhs, ocg->CreateInt(-ub.get_coef(wc)));
+ rhs = ocg->CreateTimes(ocg->CreateInt(lb.get_coef(wc)), rhs);
+ CG_outputRepr *term = ocg->CreateLE(lhs, rhs);
+ result = ocg->CreateAnd(result, term);
+ }
+ }
+
+ return result;
+}
+
+
+//
+// return NULL if 0
+//
+CG_outputRepr *output_inequality_repr(CG_outputBuilder *ocg, const GEQ_Handle &inequality, Variable_ID v, const Relation &R, const std::vector<std::pair<CG_outputRepr *, int> > &assigned_on_the_fly, std::set<Variable_ID> excluded_floor_vars) {
+ const_cast<Relation &>(R).setup_names(); // hack
+
+ coef_t a = inequality.get_coef(v);
+ assert(a != 0);
+ excluded_floor_vars.insert(v);
+
+ CG_outputRepr *repr = NULL;
+ for (Constr_Vars_Iter cvi(inequality); cvi; cvi++)
+ if (cvi.curr_var() != v) {
+ CG_outputRepr *t;
+ if (cvi.curr_var()->kind() == Wildcard_Var) {
+ std::pair<bool, GEQ_Handle> result = find_floor_definition(R, cvi.curr_var(), excluded_floor_vars);
+ if (!result.first) {
+ delete repr;
+ throw codegen_error("Can't generate bound expression with wildcard not involved in floor definition");
+ }
+ try {
+ t = output_inequality_repr(ocg, result.second, cvi.curr_var(), R, assigned_on_the_fly, excluded_floor_vars);
+ }
+ catch (const std::exception &e) {
+ delete repr;
+ throw e;
+ }
+ }
+ else
+ t = output_ident(ocg, R, cvi.curr_var(), assigned_on_the_fly);
+
+ coef_t coef = cvi.curr_coef();
+ if (a > 0) {
+ if (coef > 0) {
+ if (coef == 1)
+ repr = ocg->CreateMinus(repr, t);
+ else
+ repr = ocg->CreateMinus(repr, ocg->CreateTimes(ocg->CreateInt(coef), t));
+ }
+ else {
+ if (coef == -1)
+ repr = ocg->CreatePlus(repr, t);
+ else
+ repr = ocg->CreatePlus(repr, ocg->CreateTimes(ocg->CreateInt(-coef), t));
+ }
+ }
+ else {
+ if (coef > 0) {
+ if (coef == 1)
+ repr = ocg->CreatePlus(repr, t);
+ else
+ repr = ocg->CreatePlus(repr, ocg->CreateTimes(ocg->CreateInt(coef), t));
+ }
+ else {
+ if (coef == -1)
+ repr = ocg->CreateMinus(repr, t);
+ else
+ repr = ocg->CreateMinus(repr, ocg->CreateTimes(ocg->CreateInt(-coef), t));
+ }
+ }
+ }
+ coef_t c = inequality.get_const();
+ if (c > 0) {
+ if (a > 0)
+ repr = ocg->CreateMinus(repr, ocg->CreateInt(c));
+ else
+ repr = ocg->CreatePlus(repr, ocg->CreateInt(c));
+ }
+ else if (c < 0) {
+ if (a > 0)
+ repr = ocg->CreatePlus(repr, ocg->CreateInt(-c));
+ else
+ repr = ocg->CreateMinus(repr, ocg->CreateInt(-c));
+ }
+
+ if (abs(a) == 1)
+ return repr;
+ else if (a > 0)
+ return ocg->CreateIntegerCeil(repr, ocg->CreateInt(a));
+ else // a < 0
+ return ocg->CreateIntegerFloor(repr, ocg->CreateInt(-a));
+}
+
+
+//
+// nothing special, just an alias
+//
+CG_outputRepr *output_upper_bound_repr(CG_outputBuilder *ocg, const GEQ_Handle &inequality, Variable_ID v, const Relation &R, const std::vector<std::pair<CG_outputRepr *, int> > &assigned_on_the_fly) {
+ assert(inequality.get_coef(v) < 0);
+ CG_outputRepr* zero_;
+
+ zero_ = output_inequality_repr(ocg, inequality, v, R, assigned_on_the_fly);
+
+ if(!zero_)
+ zero_ = ocg->CreateInt(0);
+
+ return zero_;
+
+}
+
+
+//
+// output lower bound with respect to lattice
+//
+CG_outputRepr *output_lower_bound_repr(CG_outputBuilder *ocg, const GEQ_Handle &inequality, Variable_ID v, const EQ_Handle &stride_eq, Variable_ID wc, const Relation &R, const Relation &known, const std::vector<std::pair<CG_outputRepr *, int> > &assigned_on_the_fly) {
+ assert(inequality.get_coef(v) > 0);
+ CG_outputRepr* zero_;
+ if (wc == NULL || bound_must_hit_stride(inequality, v, stride_eq, wc, R, known)){
+ zero_ = output_inequality_repr(ocg, inequality, v, R, assigned_on_the_fly);
+ if(!zero_)
+ zero_ = ocg->CreateInt(0);
+
+ return zero_;
+ }
+ CG_outputRepr *strideBoundRepr = NULL;
+ int sign = (stride_eq.get_coef(v)>0)?1:-1;
+ for (Constr_Vars_Iter cvi(stride_eq); cvi; cvi++) {
+ Variable_ID v2 = cvi.curr_var();
+ if (v2 == v || v2 == wc)
+ continue;
+
+ CG_outputRepr *v_repr;
+ if (v2->kind() == Input_Var || v2->kind() == Global_Var)
+ v_repr = output_ident(ocg, R, v2, assigned_on_the_fly);
+ else if (v2->kind() == Wildcard_Var) {
+ std::pair<bool, GEQ_Handle> result = find_floor_definition(R, v2);
+ assert(result.first);
+ v_repr = output_inequality_repr(ocg, result.second, v2, R, assigned_on_the_fly);
+ }
+
+ coef_t coef = cvi.curr_coef();
+ if (sign < 0) {
+ if (coef > 0) {
+ if (coef == 1)
+ strideBoundRepr = ocg->CreatePlus(strideBoundRepr, v_repr);
+ else
+ strideBoundRepr = ocg->CreatePlus(strideBoundRepr, ocg->CreateTimes(ocg->CreateInt(coef), v_repr));
+ }
+ else { // coef < 0
+ if (coef == -1)
+ strideBoundRepr = ocg->CreateMinus(strideBoundRepr, v_repr);
+ else
+ strideBoundRepr = ocg->CreateMinus(strideBoundRepr, ocg->CreateTimes(ocg->CreateInt(-coef), v_repr));
+ }
+ }
+ else {
+ if (coef > 0) {
+ if (coef == 1)
+ strideBoundRepr = ocg->CreateMinus(strideBoundRepr, v_repr);
+ else
+ strideBoundRepr = ocg->CreateMinus(strideBoundRepr, ocg->CreateTimes(ocg->CreateInt(coef), v_repr));
+ }
+ else { // coef < 0
+ if (coef == -1)
+ strideBoundRepr = ocg->CreatePlus(strideBoundRepr, v_repr);
+ else
+ strideBoundRepr = ocg->CreatePlus(strideBoundRepr, ocg->CreateTimes(ocg->CreateInt(-coef), v_repr));
+ }
+ }
+ }
+ coef_t c = stride_eq.get_const();
+ if (c > 0) {
+ if (sign < 0)
+ strideBoundRepr = ocg->CreatePlus(strideBoundRepr, ocg->CreateInt(c));
+ else
+ strideBoundRepr = ocg->CreateMinus(strideBoundRepr, ocg->CreateInt(c));
+ }
+ else if (c < 0) {
+ if (sign < 0)
+ strideBoundRepr = ocg->CreateMinus(strideBoundRepr, ocg->CreateInt(-c));
+ else
+ strideBoundRepr = ocg->CreatePlus(strideBoundRepr, ocg->CreateInt(-c));
+ }
+
+ CG_outputRepr *repr = output_inequality_repr(ocg, inequality, v, R, assigned_on_the_fly);
+ CG_outputRepr *repr2 = ocg->CreateCopy(repr);
+ repr = ocg->CreatePlus(repr2, ocg->CreateIntegerMod(ocg->CreateMinus(strideBoundRepr, repr), ocg->CreateInt(abs(stride_eq.get_coef(wc)))));
+
+ return repr;
+}
+
+
+//
+// return loop control structure only
+//
+CG_outputRepr *output_loop(CG_outputBuilder *ocg, const Relation &R, int level, const Relation &known, const std::vector<std::pair<CG_outputRepr *, int> > &assigned_on_the_fly) {
+ std::pair<EQ_Handle, Variable_ID> result = find_simplest_stride(R, const_cast<Relation &>(R).set_var(level));
+ if (result.second != NULL)
+ assert(abs(result.first.get_coef(const_cast<Relation &>(R).set_var(level))) == 1);
+
+ std::vector<CG_outputRepr *> lbList, ubList;
+ try {
+
+ coef_t const_lb = negInfinity, const_ub = posInfinity;
+
+ for (GEQ_Iterator e(const_cast<Relation &>(R).single_conjunct()->GEQs()); e; e++) {
+ coef_t coef = (*e).get_coef(const_cast<Relation &>(R).set_var(level));
+
+ if (coef > 0) {
+ CG_outputRepr *repr = output_lower_bound_repr(ocg, *e, const_cast<Relation &>(R).set_var(level), result.first, result.second, R, known, assigned_on_the_fly);
+ if (repr == NULL)
+ repr = ocg->CreateInt(0);
+ lbList.push_back(repr);
+
+ if ((*e).is_const(const_cast<Relation &>(R).set_var(level))){
+ if(!result.second) {
+
+ //no variables but v in constr
+ coef_t L,m;
+ L = -((*e).get_const());
+
+ m = (*e).get_coef(const_cast<Relation &>(R).set_var(level));
+ coef_t sb = (int) (ceil(((float) L) /m));
+ set_max(const_lb, sb);
+ }
+ else{
+
+ coef_t L,m,s,c;
+ L = -((*e).get_const());
+ m = (*e).get_coef(const_cast<Relation &>(R).set_var(level));
+ s = abs(result.first.get_coef(result.second));
+ c = result.first.get_const();
+ coef_t sb = (s * (int) (ceil( (float) (L - (c * m)) /(s*m))))+ c;
+ set_max(const_lb, sb);
+
+ }
+ }
+
+ }
+ else if (coef < 0) {
+ CG_outputRepr *repr = output_upper_bound_repr(ocg, *e, const_cast<Relation &>(R).set_var(level), R, assigned_on_the_fly);
+ if (repr == NULL)
+ repr = ocg->CreateInt(0);
+ ubList.push_back(repr);
+
+ if ((*e).is_const(const_cast<Relation &>(R).set_var(level))) {
+ // no variables but v in constraint
+ set_min(const_ub,-(*e).get_const()/(*e).get_coef(const_cast<Relation &>(R).set_var(level)));
+ }
+
+ }
+ }
+
+ if(fillInBounds && lbList.size() == 1 && const_lb != negInfinity)
+ lowerBoundForLevel = const_lb;
+
+ if(fillInBounds && const_ub != posInfinity)
+ upperBoundForLevel = const_ub;
+ if (lbList.size() == 0)
+ throw codegen_error("missing lower bound at loop level " + to_string(level));
+ if (ubList.size() == 0)
+ throw codegen_error("missing upper bound at loop level " + to_string(level));
+ }
+ catch (const std::exception &e) {
+ for (int i = 0; i < lbList.size(); i++)
+ delete lbList[i];
+ for (int i = 0; i < ubList.size(); i++)
+ delete ubList[i];
+ throw e;
+ }
+
+ CG_outputRepr *lbRepr = NULL;
+ if (lbList.size() > 1)
+ lbRepr = ocg->CreateInvoke("max", lbList);
+ else // (lbList.size() == 1)
+ lbRepr = lbList[0];
+
+ CG_outputRepr *ubRepr = NULL;
+ if (ubList.size() > 1)
+ ubRepr = ocg->CreateInvoke("min", ubList);
+ else // (ubList.size() == 1)
+ ubRepr = ubList[0];
+
+ CG_outputRepr *stRepr;
+ if (result.second == NULL)
+ stRepr = ocg->CreateInt(1);
+ else
+ stRepr = ocg->CreateInt(abs(result.first.get_coef(result.second)));
+ CG_outputRepr *indexRepr = output_ident(ocg, R, const_cast<Relation &>(R).set_var(level), assigned_on_the_fly);
+ return ocg->CreateInductive(indexRepr, lbRepr, ubRepr, stRepr);
+}
+
+
+//
+// parameter f_root is inside f_exists, not the other way around.
+// return replicated variable in new relation, with all cascaded floor definitions
+// using wildcards defined in the same way as in the original relation.
+//
+Variable_ID replicate_floor_definition(const Relation &R, const Variable_ID floor_var,
+ Relation &r, F_Exists *f_exists, F_And *f_root,
+ std::map<Variable_ID, Variable_ID> &exists_mapping) {
+ assert(R.n_out() == 0 && r.n_out() == 0 && R.n_inp() == r.n_inp());
+
+ std::set<Variable_ID> excluded_floor_vars;
+ std::stack<Variable_ID> to_fill;
+ to_fill.push(floor_var);
+
+ while (!to_fill.empty()) {
+ Variable_ID v = to_fill.top();
+ to_fill.pop();
+ if (excluded_floor_vars.find(v) != excluded_floor_vars.end())
+ continue;
+
+ std::pair<bool, GEQ_Handle> result = find_floor_definition(R, v, excluded_floor_vars);
+ assert(result.first);
+ excluded_floor_vars.insert(v);
+
+ GEQ_Handle h1 = f_root->add_GEQ();
+ GEQ_Handle h2 = f_root->add_GEQ();
+ for (Constr_Vars_Iter cvi(result.second); cvi; cvi++) {
+ Variable_ID v2 = cvi.curr_var();
+ switch (v2->kind()) {
+ case Input_Var: {
+ int pos = v2->get_position();
+ h1.update_coef(r.input_var(pos), cvi.curr_coef());
+ h2.update_coef(r.input_var(pos), -cvi.curr_coef());
+ break;
+ }
+ case Wildcard_Var: {
+ std::map<Variable_ID, Variable_ID>::iterator p = exists_mapping.find(v2);
+ Variable_ID v3;
+ if (p == exists_mapping.end()) {
+ v3 = f_exists->declare();
+ exists_mapping[v2] = v3;
+ }
+ else
+ v3 = p->second;
+ h1.update_coef(v3, cvi.curr_coef());
+ h2.update_coef(v3, -cvi.curr_coef());
+ if (v2 != v)
+ to_fill.push(v2);
+ break;
+ }
+ case Global_Var: {
+ Global_Var_ID g = v2->get_global_var();
+ Variable_ID v3;
+ if (g->arity() == 0)
+ v3 = r.get_local(g);
+ else
+ v3 = r.get_local(g, v2->function_of());
+ h1.update_coef(v3, cvi.curr_coef());
+ h2.update_coef(v3, -cvi.curr_coef());
+ break;
+ }
+ default:
+ assert(false);
+ }
+ }
+ h1.update_const(result.second.get_const());
+ h2.update_const(-result.second.get_const()-result.second.get_coef(v)-1);
+ }
+
+ if (floor_var->kind() == Input_Var)
+ return r.input_var(floor_var->get_position());
+ else if (floor_var->kind() == Wildcard_Var)
+ return exists_mapping[floor_var];
+ else
+ assert(false);
+}
+
+
+//
+// pick one guard condition from relation. it can involve multiple
+// constraints when involving wildcards, as long as its complement
+// is a single conjunct.
+//
+Relation pick_one_guard(const Relation &R, int level) {
+ assert(R.n_out()==0);
+
+ Relation r = Relation::True(R.n_set());
+
+ for (GEQ_Iterator e(const_cast<Relation &>(R).single_conjunct()->GEQs()); e; e++)
+ if (!(*e).has_wildcards()) {
+ r.and_with_GEQ(*e);
+ r.simplify();
+ r.copy_names(R);
+ r.setup_names();
+ return r;
+ }
+
+ for (EQ_Iterator e(const_cast<Relation &>(R).single_conjunct()->EQs()); e; e++)
+ if (!(*e).has_wildcards()) {
+ r.and_with_GEQ(*e);
+ r.simplify();
+ r.copy_names(R);
+ r.setup_names();
+ return r;
+ }
+
+ for (EQ_Iterator e(const_cast<Relation &>(R).single_conjunct()->EQs()); e; e++)
+ if ((*e).has_wildcards()) {
+ int num_wildcard = 0;
+ int max_level = 0;
+ for (Constr_Vars_Iter cvi(*e); cvi; cvi++)
+ switch (cvi.curr_var()->kind()) {
+ case Wildcard_Var:
+ num_wildcard++;
+ break;
+ case Input_Var:
+ if (cvi.curr_var()->get_position() > max_level)
+ max_level = cvi.curr_var()->get_position();
+ break;
+ default:
+ ;
+ }
+
+ if (num_wildcard == 1 && max_level != level-1) {
+ r.and_with_EQ(*e);
+ r.simplify();
+ r.copy_names(R);
+ r.setup_names();
+ return r;
+ }
+ }
+
+ for (GEQ_Iterator e(const_cast<Relation &>(R).single_conjunct()->GEQs()); e; e++)
+ if ((*e).has_wildcards()) {
+ int num_wildcard = 0;
+ int max_level = 0;
+ bool direction;
+ Variable_ID wc;
+ for (Constr_Vars_Iter cvi(*e); cvi; cvi++)
+ switch (cvi.curr_var()->kind()) {
+ case Wildcard_Var:
+ num_wildcard++;
+ wc = cvi.curr_var();
+ direction = cvi.curr_coef()>0?true:false;
+ break;
+ case Input_Var:
+ if (cvi.curr_var()->get_position() > max_level)
+ max_level = cvi.curr_var()->get_position();
+ break;
+ default:
+ ;
+ }
+
+ if (num_wildcard == 1 && max_level != level-1) {
+ // find the pairing inequality
+ GEQ_Iterator e2 = e;
+ e2++;
+ for ( ; e2; e2++) {
+ int num_wildcard2 = 0;
+ int max_level2 = 0;
+ bool direction2;
+ Variable_ID wc2;
+ for (Constr_Vars_Iter cvi(*e2); cvi; cvi++)
+ switch (cvi.curr_var()->kind()) {
+ case Wildcard_Var:
+ num_wildcard2++;
+ wc2 = cvi.curr_var();
+ direction2 = cvi.curr_coef()>0?true:false;
+ break;
+ case Input_Var:
+ if (cvi.curr_var()->get_position() > max_level2)
+ max_level2 = cvi.curr_var()->get_position();
+ break;
+ default:
+ ;
+ }
+
+ if (num_wildcard2 == 1 && max_level2 != level-1 && wc2 == wc && direction2 == not direction) {
+ F_Exists *f_exists = r.and_with_and()->add_exists();
+ Variable_ID wc3 = f_exists->declare();
+ F_And *f_root = f_exists->add_and();
+ GEQ_Handle h = f_root->add_GEQ();
+ for (Constr_Vars_Iter cvi(*e); cvi; cvi++) {
+ switch (cvi.curr_var()->kind()) {
+ case Wildcard_Var:
+ h.update_coef(wc3, cvi.curr_coef());
+ break;
+ case Input_Var:
+ h.update_coef(r.input_var(cvi.curr_var()->get_position()), cvi.curr_coef());
+ break;
+ case Global_Var: {
+ Global_Var_ID g = cvi.curr_var()->get_global_var();
+ Variable_ID v;
+ if (g->arity() == 0)
+ v = r.get_local(g);
+ else
+ v = r.get_local(g, cvi.curr_var()->function_of());
+ h.update_coef(v, cvi.curr_coef());
+ break;
+ }
+ default:
+ assert(false);
+ }
+ }
+ h.update_const((*e).get_const());
+
+ h = f_root->add_GEQ();
+ for (Constr_Vars_Iter cvi(*e2); cvi; cvi++) {
+ switch (cvi.curr_var()->kind()) {
+ case Wildcard_Var:
+ h.update_coef(wc3, cvi.curr_coef());
+ break;
+ case Input_Var:
+ h.update_coef(r.input_var(cvi.curr_var()->get_position()), cvi.curr_coef());
+ break;
+ case Global_Var: {
+ Global_Var_ID g = cvi.curr_var()->get_global_var();
+ Variable_ID v;
+ if (g->arity() == 0)
+ v = r.get_local(g);
+ else
+ v = r.get_local(g, cvi.curr_var()->function_of());
+ h.update_coef(v, cvi.curr_coef());
+ break;
+ }
+ default:
+ assert(false);
+ }
+ }
+ h.update_const((*e2).get_const());
+
+ r.simplify();
+ r.copy_names(R);
+ r.setup_names();
+ return r;
+ }
+ }
+ }
+ }
+}
+
+
+//
+// heavy lifting for code output for one leaf node
+//
+CG_outputRepr *leaf_print_repr(BoolSet<> active, const std::map<int, Relation> &guards,
+ CG_outputRepr *guard_repr, const Relation &known,
+ int indent, CG_outputBuilder *ocg, const std::vector<int> &remap,
+ const std::vector<Relation> &xforms, const std::vector<CG_outputRepr *> &stmts,
+ const std::vector<std::pair<CG_outputRepr *, int> > &assigned_on_the_fly) {
+ if (active.num_elem() == 0)
+ return NULL;
+
+ CG_outputRepr *stmt_list = NULL;
+ for (BoolSet<>::iterator i = active.begin(); i != active.end(); i++) {
+ std::map<int, Relation>::const_iterator j = guards.find(*i);
+ if (j == guards.end() || Must_Be_Subset(copy(known), copy(j->second))) {
+ Relation mapping = Inverse(copy((xforms[remap[*i]])));
+ mapping.simplify();
+ mapping.setup_names();
+ std::vector<std::string> loop_vars;
+ for (int k = 1; k <= mapping.n_out(); k++) {
+ loop_vars.push_back(mapping.output_var(k)->name());
+// std::cout << "CG_Utils:: " << k << ", " << mapping.output_var(k)->name().c_str() << "\n";
+ }
+ std::vector<CG_outputRepr *> sList = output_substitutions(ocg, mapping, assigned_on_the_fly);
+ stmt_list = ocg->StmtListAppend(stmt_list, ocg->CreateSubstitutedStmt((guard_repr==NULL)?indent:indent+1, stmts[remap[*i]]->clone(), loop_vars, sList));
+ active.unset(*i);
+ }
+ }
+
+ if (stmt_list != NULL) {
+ if (active.num_elem() != 0)
+ stmt_list = ocg->StmtListAppend(stmt_list, leaf_print_repr(active, guards, NULL, known, (guard_repr==NULL)?indent:indent+1, ocg, remap, xforms, stmts, assigned_on_the_fly));
+ if (guard_repr == NULL)
+ return stmt_list;
+ else
+ return ocg->CreateIf(indent, guard_repr, stmt_list, NULL);
+ }
+ else {
+ Relation then_cond = find_best_guard(const_cast<std::map<int, Relation> &>(guards)[*(active.begin())], active, guards);
+ assert(!then_cond.is_obvious_tautology());
+ Relation new_then_known = Intersection(copy(known), copy(then_cond));
+ new_then_known.simplify();
+ Relation else_cond = Complement(copy(then_cond));
+ else_cond.simplify();
+ Relation new_else_known = Intersection(copy(known), copy(else_cond));
+ new_else_known.simplify();
+
+ BoolSet<> then_active(active.size()), else_active(active.size()), indep_active(active.size());
+ std::map<int, Relation> then_guards, else_guards;
+ for (BoolSet<>::iterator i = active.begin(); i != active.end(); i++) {
+ Relation &r = const_cast<std::map<int, Relation> &>(guards)[*i];
+ if (Must_Be_Subset(copy(r), copy(then_cond))) {
+ Relation r2 = Gist(copy(r), copy(then_cond), 1);
+ if (!r2.is_obvious_tautology())
+ then_guards[*i] = r2;
+ then_active.set(*i);
+ }
+ else if (Must_Be_Subset(copy(r), copy(else_cond))) {
+ Relation r2 = Gist(copy(r), copy(else_cond), 1);
+ if (!r2.is_obvious_tautology())
+ else_guards[*i] = r2;
+ else_active.set(*i);
+ }
+ else
+ indep_active.set(*i);
+ }
+ assert(!then_active.empty());
+
+ CG_outputRepr *new_guard_repr = output_guard(ocg, then_cond, assigned_on_the_fly);
+ if (else_active.empty() && indep_active.empty()) {
+ guard_repr = ocg->CreateAnd(guard_repr, new_guard_repr);
+ return leaf_print_repr(then_active, then_guards, guard_repr, new_then_known, indent, ocg, remap, xforms, stmts, assigned_on_the_fly);
+ }
+ else if (else_active.empty() && !indep_active.empty()) {
+ int new_indent = (guard_repr==NULL)?indent:indent+1;
+ stmt_list = leaf_print_repr(then_active, then_guards, new_guard_repr, new_then_known, new_indent, ocg, remap, xforms, stmts, assigned_on_the_fly);
+ stmt_list = ocg->StmtListAppend(stmt_list, leaf_print_repr(indep_active, guards, NULL, known, new_indent, ocg, remap, xforms, stmts, assigned_on_the_fly));
+ if (guard_repr == NULL)
+ return stmt_list;
+ else
+ return ocg->CreateIf(indent, guard_repr, stmt_list, NULL);
+ }
+ else { // (!else_active.empty())
+ int new_indent = (guard_repr==NULL)?indent:indent+1;
+ CG_outputRepr *then_stmt_list = leaf_print_repr(then_active, then_guards, NULL, new_then_known, new_indent+1, ocg, remap, xforms, stmts, assigned_on_the_fly);
+ CG_outputRepr *else_stmt_list = leaf_print_repr(else_active, else_guards, NULL, new_else_known, new_indent+1, ocg, remap, xforms, stmts, assigned_on_the_fly);
+ stmt_list = ocg->CreateIf(new_indent, new_guard_repr, then_stmt_list, else_stmt_list);
+ if (!indep_active.empty())
+ stmt_list = ocg->StmtListAppend(stmt_list, leaf_print_repr(indep_active, guards, NULL, known, new_indent, ocg, remap, xforms, stmts, assigned_on_the_fly));
+ if (guard_repr == NULL)
+ return stmt_list;
+ else
+ return ocg->CreateIf(indent, guard_repr, stmt_list, NULL);
+ }
+ }
+}
+
+
+//
+// heavy lifting for code output for one level of loop nodes
+//
+CG_outputRepr *loop_print_repr(const std::vector<CG_loop *> &loops, int start, int end,
+ const Relation &guard, CG_outputRepr *guard_repr,
+ int indent, CG_outputBuilder *ocg, const std::vector<CG_outputRepr *> &stmts,
+ const std::vector<std::pair<CG_outputRepr *, int> > &assigned_on_the_fly) {
+ if (start >= end)
+ return NULL;
+
+ Relation R = Gist(copy(loops[start]->guard_), copy(guard), 1);
+ if (Must_Be_Subset(Intersection(copy(loops[start]->known_), copy(guard)), copy(R))) {
+ int new_indent = (guard_repr==NULL)?indent:indent+1;
+ int i = start+1;
+ for ( ; i < end; i++)
+ if (!Gist(copy(loops[i]->guard_), copy(guard), 1).is_obvious_tautology())
+ break;
+ CG_outputRepr *stmt_list = NULL;
+ for (int j = start; j < i; j++)
+ stmt_list = ocg->StmtListAppend(stmt_list, loops[j]->printRepr(false, new_indent, ocg, stmts, assigned_on_the_fly));
+ stmt_list = ocg->StmtListAppend(stmt_list, loop_print_repr(loops, i, end, guard, NULL, new_indent, ocg, stmts, assigned_on_the_fly));
+ if (guard_repr == NULL)
+ return stmt_list;
+ else
+ return ocg->CreateIf(indent, guard_repr, stmt_list, NULL);
+ }
+
+ Relation then_cond = find_best_guard(R, loops, start, end);
+ assert(!then_cond.is_obvious_tautology());
+ Relation else_cond = Complement(copy(then_cond));
+ else_cond.simplify();
+
+ std::vector<CG_loop *> then_loops, else_loops, indep_loops;
+ int i = start;
+ for ( ; i < end; i++)
+ if (!Must_Be_Subset(copy(loops[i]->guard_), copy(then_cond)))
+ break;
+ int j = i;
+ for ( ; j < end; j++)
+ if (!Must_Be_Subset(copy(loops[j]->guard_), copy(else_cond)))
+ break;
+ assert(i>start);
+
+ CG_outputRepr *new_guard_repr = output_guard(ocg, then_cond, assigned_on_the_fly);
+ if (j == i && end == j) {
+ guard_repr = ocg->CreateAnd(guard_repr, new_guard_repr);
+ Relation new_guard = Intersection(copy(guard), copy(then_cond));
+ new_guard.simplify();
+ return loop_print_repr(loops, start, end, new_guard, guard_repr, indent, ocg, stmts, assigned_on_the_fly);
+ }
+ else if (j == i && end > j) {
+ int new_indent = (guard_repr==NULL)?indent:indent+1;
+ Relation new_guard = Intersection(copy(guard), copy(then_cond));
+ new_guard.simplify();
+ CG_outputRepr *stmt_list = loop_print_repr(loops, start, i, new_guard, new_guard_repr, new_indent, ocg, stmts, assigned_on_the_fly);
+ stmt_list = ocg->StmtListAppend(stmt_list, loop_print_repr(loops, j, end, guard, NULL, new_indent, ocg, stmts, assigned_on_the_fly));
+ if (guard_repr == NULL)
+ return stmt_list;
+ else
+ return ocg->CreateIf(indent, guard_repr, stmt_list, NULL);
+ }
+ else { // (j > i)
+ int new_indent = (guard_repr==NULL)?indent:indent+1;
+ Relation then_new_guard = Intersection(copy(guard), copy(then_cond));
+ then_new_guard.simplify();
+ CG_outputRepr *then_stmt_list = loop_print_repr(loops, start, i, then_new_guard, NULL, new_indent+1, ocg, stmts, assigned_on_the_fly);
+ Relation else_new_guard = Intersection(copy(guard), copy(else_cond));
+ else_new_guard.simplify();
+ CG_outputRepr *else_stmt_list = loop_print_repr(loops, i, j, else_new_guard, NULL, new_indent+1, ocg, stmts, assigned_on_the_fly);
+ CG_outputRepr *stmt_list = ocg->CreateIf(new_indent, new_guard_repr, then_stmt_list, else_stmt_list);
+ stmt_list = ocg->StmtListAppend(stmt_list, loop_print_repr(loops, j, end, guard, NULL, new_indent, ocg, stmts, assigned_on_the_fly));
+ if (guard_repr == NULL)
+ return stmt_list;
+ else
+ return ocg->CreateIf(indent, guard_repr, stmt_list, NULL);
+ }
+}
+
+}
--
cgit v1.2.3-70-g09d2