diff options
Diffstat (limited to 'omegalib/omega/src/hull_simple.cc')
| -rwxr-xr-x | omegalib/omega/src/hull_simple.cc | 1013 |
1 files changed, 0 insertions, 1013 deletions
diff --git a/omegalib/omega/src/hull_simple.cc b/omegalib/omega/src/hull_simple.cc deleted file mode 100755 index 62dcb26..0000000 --- a/omegalib/omega/src/hull_simple.cc +++ /dev/null @@ -1,1013 +0,0 @@ -/***************************************************************************** - Copyright (C) 2011 Chun Chen - All Rights Reserved. - - Purpose: - Hull approximation including lattice and irregular constraints that - involves wildcards. - - Notes: - - History: - 03/12/11 Created by Chun Chen - *****************************************************************************/ - -#include <assert.h> -#include <omega.h> -#include <basic/BoolSet.h> -#include <vector> -#include <list> -#include <set> -#include <string> -#include <algorithm> - -namespace omega { - -Relation SimpleHull(const Relation &R, bool allow_stride_constraint, - bool allow_irregular_constraint) { - std::vector<Relation> Rs; - Rs.push_back(R); - return SimpleHull(Rs, allow_stride_constraint, allow_irregular_constraint); -} - -Relation SimpleHull(const std::vector<Relation> &Rs, - bool allow_stride_constraint, bool allow_irregular_constraint) { - // check for sanity of parameters - if (Rs.size() == 0) - return Relation::False(0); - int num_dim = -1; - int first_non_null; - for (int i = 0; i < Rs.size(); i++) { - if (Rs[i].is_null()) - continue; - - if (num_dim == -1) { - num_dim = Rs[i].n_inp(); - first_non_null = i; - } - - if (Rs[i].n_inp() != num_dim) - throw std::invalid_argument( - "relations for hull must have same dimension"); - if (Rs[i].n_out() != 0) - throw std::invalid_argument( - "hull calculation must be set relation"); - } - - // convert to a list of relations each with a single conjunct - std::vector<Relation> l_Rs; - for (int i = 0; i < Rs.size(); i++) { - if (Rs[i].is_null()) - continue; - - Relation r = copy(Rs[i]); - - //r.simplify(2, 4); - r.simplify(); - DNF_Iterator c(r.query_DNF()); - int top = l_Rs.size(); - while (c.live()) { - Relation r2 = Relation(r, c.curr()); - - // quick elimination of redundant conjuncts - bool already_included = false; - for (int j = 0; j < top; j++) - if (Must_Be_Subset(copy(r2), copy(l_Rs[j]))) { - already_included = true; - break; - } else if (Must_Be_Subset(copy(l_Rs[j]), copy(r2))) { - l_Rs.erase(l_Rs.begin() + j); - top--; - break; - } - - if (!already_included) - l_Rs.push_back(r2); - c++; - } - } - - // shortcut for simple case - if (l_Rs.size() == 0) { - if (num_dim == -1) - return Relation::False(0); - else { - Relation r = Relation::False(num_dim); - r.copy_names(Rs[first_non_null]); - r.setup_names(); - return r; - } - } else if (l_Rs.size() == 1) { - if (allow_stride_constraint && allow_irregular_constraint) { - l_Rs[0].copy_names(Rs[first_non_null]); - l_Rs[0].setup_names(); - return l_Rs[0]; - } else if (!allow_stride_constraint && !allow_irregular_constraint) { - l_Rs[0] = Approximate(l_Rs[0]); - l_Rs[0].copy_names(Rs[first_non_null]); - l_Rs[0].setup_names(); - return l_Rs[0]; - } - } - - Relation hull = Relation::True(num_dim); - - // lattice union approximation - if (allow_stride_constraint) { - std::vector<std::vector<std::pair<EQ_Handle, BoolSet<> > > > strides( - l_Rs.size()); - for (int i = 0; i < l_Rs.size(); i++) - for (EQ_Iterator e = l_Rs[i].single_conjunct()->EQs(); e; e++) - if ((*e).has_wildcards()) { - int num_wildcard = 0; - BoolSet<> affected(num_dim); - for (Constr_Vars_Iter cvi(*e); cvi; cvi++) { - if (cvi.curr_var()->kind() == Wildcard_Var) - num_wildcard++; - else if (cvi.curr_var()->kind() == Input_Var) - affected.set(cvi.curr_var()->get_position() - 1); - } - if (num_wildcard == 1) - strides[i].push_back(std::make_pair(*e, affected)); - } - - for (int i = 0; i < strides[0].size(); i++) { - coef_t c = - abs( - strides[0][i].first.get_coef( - Constr_Vars_Iter(strides[0][i].first, true).curr_var())); - coef_t old_c = c; - bool is_stride = true; - for (int j = 1; j < l_Rs.size(); j++) { - std::list<coef_t> candidates; - for (int k = 0; k < strides[j].size(); k++) - if (!(strides[0][i].second & strides[j][k].second).empty()) { - coef_t t = gcd(c, - abs( - strides[j][k].first.get_coef( - Constr_Vars_Iter( - strides[j][k].first, - true).curr_var()))); - if (t != 1) { - std::list<coef_t>::iterator p = candidates.begin(); - while (p != candidates.end() && *p > t) - ++p; - if (p == candidates.end() || *p != t) - candidates.insert(p, t); - - t = gcd(t, abs(strides[0][i].first.get_const())); - t = gcd(t, abs(strides[j][k].first.get_const())); - if (t != 1) { - std::list<coef_t>::iterator p = - candidates.begin(); - while (p != candidates.end() && *p > t) - ++p; - if (p == candidates.end() || *p != t) - candidates.insert(p, t); - } - } - } - - bool found_matched_stride = false; - for (std::list<coef_t>::iterator k = candidates.begin(); - k != candidates.end(); k++) { - Relation r = Relation::True(num_dim); - EQ_Handle h = r.and_with_EQ(strides[0][i].first); - h.update_coef(Constr_Vars_Iter(h, true).curr_var(), - -old_c + *k); - r.simplify(); - if (Must_Be_Subset(copy(l_Rs[j]), copy(r))) { - c = *k; - found_matched_stride = true; - break; - } - } - - if (!found_matched_stride) { - is_stride = false; - break; - } - } - - if (is_stride) { - Relation r = Relation::True(num_dim); - EQ_Handle h = r.and_with_EQ(strides[0][i].first); - h.update_coef(Constr_Vars_Iter(h, true).curr_var(), -old_c + c); - r.simplify(); - hull = Intersection(hull, r); - } - } - } - - // consider some special wildcard constraints - if (allow_irregular_constraint) { - std::vector< - std::vector< - std::pair<Variable_ID, std::map<Variable_ID, coef_t> > > > ranges( - l_Rs.size()); - for (int i = 0; i < l_Rs.size(); i++) { - std::vector<std::pair<GEQ_Handle, std::map<Variable_ID, coef_t> > > geqs_ub; - std::vector<std::pair<GEQ_Handle, std::map<Variable_ID, coef_t> > > geqs_lb; - for (GEQ_Iterator e = l_Rs[i].single_conjunct()->GEQs(); e; e++) - if ((*e).has_wildcards()) { - int num_wildcard = 0; - std::map<Variable_ID, coef_t> formula; - int direction; - for (Constr_Vars_Iter cvi(*e); cvi; cvi++) { - Variable_ID v = cvi.curr_var(); - switch (v->kind()) { - case Wildcard_Var: - num_wildcard++; - if (cvi.curr_coef() > 0) - direction = true; - else - direction = false; - break; - case Input_Var: - case Global_Var: - formula[cvi.curr_var()] = cvi.curr_coef(); - break; - default: - assert(false); - } - } - if (num_wildcard == 1) { - if (direction) { - for (std::map<Variable_ID, coef_t>::iterator j = - formula.begin(); j != formula.end(); j++) - j->second = -j->second; - geqs_ub.push_back(std::make_pair(*e, formula)); - } else - geqs_lb.push_back(std::make_pair(*e, formula)); - } - } - for (int j = 0; j < geqs_lb.size(); j++) { - Variable_ID v = - Constr_Vars_Iter(geqs_lb[j].first, true).curr_var(); - for (int k = 0; k < geqs_ub.size(); k++) - if (v == Constr_Vars_Iter(geqs_ub[k].first, true).curr_var() - && geqs_lb[j].second == geqs_ub[k].second) - ranges[i].push_back( - std::make_pair(v, geqs_lb[j].second)); - } - } - - // find compatible wildcard match - // TODO: evaluate to find the best match, also avoid mapping two wildcards - // in a single conjunct to one variable (incorrect) - std::vector<std::vector<int> > all_match; - for (int i = 0; i < ranges[0].size(); i++) { - std::vector<int> match(l_Rs.size(), -1); - match[0] = i; - for (int j = 1; j < l_Rs.size(); j++) { - for (int k = 0; k < ranges[j].size(); k++) - if (ranges[0][i].second == ranges[j][k].second) { - match[j] = k; - break; - } - if (match[j] == -1) - break; - } - if (match[l_Rs.size() - 1] != -1) - all_match.push_back(match); - } - - // map compatible wildcards to input variables - std::vector<Relation> ll_Rs(l_Rs.size()); - for (int i = 0; i < l_Rs.size(); i++) { - Relation r(num_dim + all_match.size()); - F_Exists *f_exists = r.add_and()->add_exists(); - F_And *f_root = f_exists->add_and(); - std::map<Variable_ID, Variable_ID> wc_map; - for (int j = 0; j < all_match.size(); j++) - wc_map[ranges[i][all_match[j][i]].first] = r.set_var(j + 1); - - for (EQ_Iterator e(l_Rs[i].single_conjunct()->EQs()); e; e++) - if (!(*e).has_wildcards()) { - EQ_Handle h = f_root->add_EQ(); - 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() - + all_match.size()), - 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()); - } - - for (GEQ_Iterator e(l_Rs[i].single_conjunct()->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() - + all_match.size()), - 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; - } - case Wildcard_Var: { - std::map<Variable_ID, Variable_ID>::iterator p = - wc_map.find(cvi.curr_var()); - Variable_ID v; - if (p == wc_map.end()) { - v = f_exists->declare(); - wc_map[cvi.curr_var()] = v; - } else - v = p->second; - h.update_coef(v, cvi.curr_coef()); - break; - } - default: - assert(false); - } - h.update_const((*e).get_const()); - } - - r.simplify(); - ll_Rs[i] = r; - } - - // now use SimpleHull on regular bounds only - Relation result = SimpleHull(ll_Rs, false, false); - - // convert imaginary input variables back to wildcards - Relation mapping(num_dim + all_match.size(), num_dim); - F_And *f_root = mapping.add_and(); - for (int i = 0; i < num_dim; i++) { - EQ_Handle h = f_root->add_EQ(); - h.update_coef(mapping.input_var(all_match.size() + i + 1), 1); - h.update_coef(mapping.output_var(i + 1), -1); - } - result = Range(Restrict_Domain(mapping, result)); - - hull = Intersection(hull, result); - hull.simplify(); - hull.copy_names(Rs[first_non_null]); - hull.setup_names(); - return hull; - } - - // check regular bounds - if (l_Rs.size() == 1) { - hull = Intersection(hull, Approximate(copy(l_Rs[0]))); - } else { - for (int i = 0; i < l_Rs.size(); i++) { - l_Rs[i] = Approximate(l_Rs[i]); - l_Rs[i].simplify(2, 4); - } - - // check global variables - // TODO: global variable function_of() is not considered for now - std::map<Global_Var_ID, int> globals; - for (int i = 0; i < l_Rs.size(); i++) - for (Constraint_Iterator e( - l_Rs[i].single_conjunct()->constraints()); e; e++) - for (Constr_Vars_Iter cvi(*e); cvi; cvi++) - if (cvi.curr_var()->kind() == Global_Var) - globals[cvi.curr_var()->get_global_var()] = -1; - - if (globals.size() > 0) { - int count = 1; - for (std::map<Global_Var_ID, int>::iterator i = globals.begin(); - i != globals.end(); i++) - i->second = count++; - - std::vector<Relation> ll_Rs(l_Rs.size()); - for (int i = 0; i < l_Rs.size(); i++) { - Relation r(num_dim + globals.size()); - F_And *f_root = r.add_and(); - for (EQ_Iterator e(l_Rs[i].single_conjunct()->EQs()); e; e++) { - EQ_Handle h = f_root->add_EQ(); - 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() - + globals.size()), - cvi.curr_coef()); - break; - } - case Global_Var: { - h.update_coef( - r.set_var( - globals[cvi.curr_var()->get_global_var()]), - cvi.curr_coef()); - break; - } - default: - assert(false); - } - h.update_const((*e).get_const()); - } - for (GEQ_Iterator e(l_Rs[i].single_conjunct()->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() - + globals.size()), - cvi.curr_coef()); - break; - } - case Global_Var: { - h.update_coef( - r.set_var( - globals[cvi.curr_var()->get_global_var()]), - cvi.curr_coef()); - break; - } - default: - assert(false); - } - h.update_const((*e).get_const()); - } - - ll_Rs[i] = r; - } - - Relation result = SimpleHull(ll_Rs, false, false); - - std::map<int, Global_Var_ID> globals_reverse; - for (std::map<Global_Var_ID, int>::iterator i = globals.begin(); - i != globals.end(); i++) - globals_reverse[i->second] = i->first; - - Relation r(num_dim); - F_And *f_root = r.add_and(); - for (EQ_Iterator e(result.single_conjunct()->EQs()); e; e++) { - EQ_Handle h = f_root->add_EQ(); - for (Constr_Vars_Iter cvi(*e); cvi; cvi++) - switch (cvi.curr_var()->kind()) { - case Input_Var: { - int pos = cvi.curr_var()->get_position(); - if (pos > globals_reverse.size()) - h.update_coef( - r.set_var(pos - globals_reverse.size()), - cvi.curr_coef()); - else { - Global_Var_ID g = globals_reverse[pos]; - h.update_coef(r.get_local(g), cvi.curr_coef()); - } - break; - } - default: - assert(false); - } - h.update_const((*e).get_const()); - } - for (GEQ_Iterator e(result.single_conjunct()->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: { - int pos = cvi.curr_var()->get_position(); - if (pos > globals_reverse.size()) - h.update_coef( - r.set_var(pos - globals_reverse.size()), - cvi.curr_coef()); - else { - Global_Var_ID g = globals_reverse[pos]; - h.update_coef(r.get_local(g), cvi.curr_coef()); - } - break; - } - default: - assert(false); - } - h.update_const((*e).get_const()); - } - - hull = Intersection(hull, r); - hull.simplify(); - hull.copy_names(Rs[first_non_null]); - hull.setup_names(); - return hull; - } else { - std::vector<std::vector<Relation> > projected(num_dim + 1, - std::vector<Relation>(l_Rs.size())); - for (int i = 0; i < l_Rs.size(); i++) { - projected[num_dim][i] = copy(l_Rs[i]); - for (int j = num_dim - 1; j >= 0; j--) { - projected[j][i] = Project(copy(projected[j + 1][i]), - projected[j + 1][i].input_var(j + 1)); - projected[j][i].simplify(2, 4); - } - } - - std::vector<bool> has_lb(num_dim, false); - std::vector<bool> has_ub(num_dim, false); - for (int i = 0; i < num_dim; i++) { - bool skip_lb = false; - bool skip_ub = false; - std::vector<Relation> bound(l_Rs.size()); - for (int j = 0; j < l_Rs.size(); j++) { - bound[j] = Gist(copy(projected[i + 1][j]), - copy(projected[i][j]), 1); - bound[j] = Approximate(bound[j]); - bound[j] = EQs_to_GEQs(bound[j]); - - bool has_lb_not_in_hull = false; - bool has_ub_not_in_hull = false; - for (GEQ_Iterator e = bound[j].single_conjunct()->GEQs(); e; - e++) { - coef_t coef = (*e).get_coef(bound[j].input_var(i + 1)); - if (!skip_lb && coef > 0) { - Relation r = Relation::True(bound[j].n_inp()); - r.and_with_GEQ(*e); - r.simplify(); - - if (j != 0 && l_Rs.size() > 2 - && Must_Be_Subset(copy(hull), copy(r))) - continue; - - bool belong_to_hull = true; - for (int k = 0; k < l_Rs.size(); k++) - if (k != j - && !Must_Be_Subset(copy(l_Rs[k]), - copy(r))) { - belong_to_hull = false; - break; - } - if (belong_to_hull) { - hull.and_with_GEQ(*e); - has_lb[i] = true; - } else - has_lb_not_in_hull = true; - } else if (!skip_ub && coef < 0) { - Relation r = Relation::True(bound[j].n_inp()); - r.and_with_GEQ(*e); - r.simplify(); - - if (j != 0 && l_Rs.size() > 2 - && Must_Be_Subset(copy(hull), copy(r))) - continue; - - bool belong_to_hull = true; - for (int k = 0; k < l_Rs.size(); k++) - if (k != j - && !Must_Be_Subset(copy(l_Rs[k]), - copy(r))) { - belong_to_hull = false; - break; - } - if (belong_to_hull) { - hull.and_with_GEQ(*e); - has_ub[i] = true; - } else - has_ub_not_in_hull = true; - } - } - - if (!has_lb_not_in_hull) - skip_lb = true; - if (!has_ub_not_in_hull) - skip_ub = true; - if (skip_lb && skip_ub) - break; - } - - // no ready lower bound, approximate it - bool got_rect_lb = false; - if (!skip_lb) { - for (int j = 0; j < l_Rs.size(); j++) { - std::set<BoolSet<> > S; - for (GEQ_Iterator e = - bound[j].single_conjunct()->GEQs(); e; e++) { - coef_t coef = (*e).get_coef( - bound[j].input_var(i + 1)); - if (coef > 0) { - BoolSet<> s(i); - for (Constr_Vars_Iter cvi(*e); cvi; cvi++) - if ((*cvi).var->kind() == Input_Var - && (*cvi).var->get_position() - 1 - != i) { - if (((*cvi).coef > 0 - && has_ub[(*cvi).var->get_position() - - 1]) - || ((*cvi).coef < 0 - && has_lb[(*cvi).var->get_position() - - 1])) - s.set( - (*cvi).var->get_position() - - 1); - else { - for (GEQ_Iterator e2 = - bound[j].single_conjunct()->GEQs(); - e2; e2++) - if (e2 != e - && (((*cvi).coef > 0 - && (*e2).get_coef( - (*cvi).var) - < 0) - || ((*cvi).coef - < 0 - && (*e2).get_coef( - (*cvi).var) - > 0))) { - s.set( - (*cvi).var->get_position() - - 1); - break; - } - } - } - - if (s.num_elem() > 0) - S.insert(s); - } - } - - if (S.size() > 0) { - BoolSet<> s(i); - for (std::set<BoolSet<> >::iterator k = S.begin(); - k != S.end(); k++) - s |= *k; - for (int k = 0; k < i; k++) - if (s.get(k)) { - BoolSet<> t(i); - t.set(k); - S.insert(t); - } - - for (std::set<BoolSet<> >::iterator k = S.begin(); - k != S.end(); k++) { - - bool do_again = false; - std::set<int> vars; - int round_trip = 0; - do { - Relation r = copy(projected[i + 1][j]); - - if (!do_again) { - for (int kk = 0; kk < i; kk++) - if ((*k).get(kk)) { - r = Project(r, - r.input_var(kk + 1)); - vars.insert(kk + 1); - } - } else { - for (std::set<int>::iterator vars_it = - vars.begin(); - vars_it != vars.end(); - vars_it++) - if (*vars_it < i + 1) - r = Project(r, - r.input_var(*vars_it)); - } - - r.simplify(2, 4); - Relation r2 = Project(copy(r), - r.input_var(i + 1)); - Relation b = Gist(copy(r), copy(r2), 1); - // Relation c = Project(copy(r),r.input_var(4) ); - - // c.simplify(2,4); - // Relation d = Project(copy(c), r.input_var(i+1)); - // Relation e = Gist(copy(c), copy(d), 1); - - b = Approximate(b); - b = EQs_to_GEQs(b); - - for (GEQ_Iterator e = - b.single_conjunct()->GEQs(); e; - e++) { - coef_t coef = (*e).get_coef( - b.input_var(i + 1)); - if (coef > 0) { - Relation r = Relation::True( - b.n_inp()); - r.and_with_GEQ(*e); - r.simplify(); - - if (Must_Be_Subset(copy(hull), - copy(r))) - continue; - - bool belong_to_hull = true; - for (int k = 0; k < l_Rs.size(); - k++) - if (k != j - && !Must_Be_Subset( - copy(l_Rs[k]), - copy(r))) { - belong_to_hull = false; - break; - } - if (belong_to_hull) { - hull.and_with_GEQ(*e); - got_rect_lb = true; - } - } - } - do_again = false; - if (!got_rect_lb) { - bool found = false; - for (GEQ_Iterator e = - b.single_conjunct()->GEQs(); e; - e++) { - coef_t coef = (*e).get_coef( - b.input_var(i + 1)); - - if (coef > 0) { - for (Constr_Vars_Iter cvi(*e); - cvi; cvi++) - if ((*cvi).var->kind() - == Input_Var - && (*cvi).var->get_position() - - 1 != i) { - - if (((*cvi).coef > 0 - && has_ub[(*cvi).var->get_position() - - 1]) - || ((*cvi).coef - < 0 - && has_lb[(*cvi).var->get_position() - - 1])) { - vars.insert( - (*cvi).var->get_position()); - found = true; - } else { - for (GEQ_Iterator e2 = - b.single_conjunct()->GEQs(); - e2; e2++) - if (e2 != e - && (((*cvi).coef - > 0 - && (*e2).get_coef( - (*cvi).var) - < 0) - || ((*cvi).coef - < 0 - && (*e2).get_coef( - (*cvi).var) - > 0))) { - vars.insert( - (*cvi).var->get_position()); - found = - true; - break; - } - } - - } - - } - if (found) - break; - - } - if (found && (round_trip < i)) - do_again = true; - - } - round_trip++; - } while (do_again); - } - - if (got_rect_lb) - break; - } - } - } - - // no ready upper bound, approximate it - bool got_rect_ub = false; - if (!skip_ub) { - for (int j = 0; j < l_Rs.size(); j++) { - std::set<BoolSet<> > S; - for (GEQ_Iterator e = - bound[j].single_conjunct()->GEQs(); e; e++) { - coef_t coef = (*e).get_coef( - bound[j].input_var(i + 1)); - if (coef < 0) { - BoolSet<> s(i); - for (Constr_Vars_Iter cvi(*e); cvi; cvi++) - if ((*cvi).var->kind() == Input_Var - && (*cvi).var->get_position() - 1 - != i) { - if (((*cvi).coef > 0 - && has_ub[(*cvi).var->get_position() - - 1]) - || ((*cvi).coef < 0 - && has_lb[(*cvi).var->get_position() - - 1])) - s.set( - (*cvi).var->get_position() - - 1); - else { - for (GEQ_Iterator e2 = - bound[j].single_conjunct()->GEQs(); - e2; e2++) - if (e2 != e - && (((*cvi).coef > 0 - && (*e2).get_coef( - (*cvi).var) - < 0) - || ((*cvi).coef - < 0 - && (*e2).get_coef( - (*cvi).var) - > 0))) { - s.set( - (*cvi).var->get_position() - - 1); - break; - } - } - } - - if (s.num_elem() > 0) - S.insert(s); - } - } - - if (S.size() > 0) { - BoolSet<> s(i); - for (std::set<BoolSet<> >::iterator k = S.begin(); - k != S.end(); k++) - s |= *k; - for (int k = 0; k < i; k++) - if (s.get(k)) { - BoolSet<> t(i); - t.set(k); - S.insert(t); - } - - for (std::set<BoolSet<> >::iterator k = S.begin(); - k != S.end(); k++) { - - bool do_again = false; - std::set<int> vars; - int round_trip = 0; - do { - - Relation r = copy(projected[i + 1][j]); - - if (!do_again) { - for (int kk = 0; kk < i; kk++) - if ((*k).get(kk)) { - r = Project(r, - r.input_var(kk + 1)); - vars.insert(kk + 1); - } - } else { - for (std::set<int>::iterator vars_it = - vars.begin(); - vars_it != vars.end(); - vars_it++) - if (*vars_it < i + 1) - r = Project(r, - r.input_var(*vars_it)); - } - - r.simplify(2, 4); - Relation r2 = Project(copy(r), - r.input_var(i + 1)); - // r2.simplify(2,4); - Relation b = Gist(r, r2, 1); - b = Approximate(b); - b = EQs_to_GEQs(b); - - for (GEQ_Iterator e = - b.single_conjunct()->GEQs(); e; - e++) { - coef_t coef = (*e).get_coef( - b.input_var(i + 1)); - if (coef < 0) { - Relation r = Relation::True( - b.n_inp()); - r.and_with_GEQ(*e); - r.simplify(); - - if (Must_Be_Subset(copy(hull), - copy(r))) - continue; - - bool belong_to_hull = true; - for (int k = 0; k < l_Rs.size(); - k++) - if (k != j - && !Must_Be_Subset( - copy(l_Rs[k]), - copy(r))) { - belong_to_hull = false; - break; - } - if (belong_to_hull) { - hull.and_with_GEQ(*e); - got_rect_ub = true; - } - } - } - do_again = false; - if (!got_rect_ub) { - bool found = false; - for (GEQ_Iterator e = - b.single_conjunct()->GEQs(); e; - e++) { - coef_t coef = (*e).get_coef( - b.input_var(i + 1)); - if (coef < 0) { - for (Constr_Vars_Iter cvi(*e); - cvi; cvi++) - if ((*cvi).var->kind() - == Input_Var - && (*cvi).var->get_position() - - 1 != i) { - - if (((*cvi).coef > 0 - && has_ub[(*cvi).var->get_position() - - 1]) - || ((*cvi).coef - < 0 - && has_lb[(*cvi).var->get_position() - - 1])) { - vars.insert( - (*cvi).var->get_position()); - found = true; - } else { - for (GEQ_Iterator e2 = - b.single_conjunct()->GEQs(); - e2; e2++) - if (e2 != e - && (((*cvi).coef - > 0 - && (*e2).get_coef( - (*cvi).var) - < 0) - || ((*cvi).coef - < 0 - && (*e2).get_coef( - (*cvi).var) - > 0))) { - vars.insert( - (*cvi).var->get_position()); - found = - true; - break; - } - } - - } - } - if (found) - break; - } - if (found && (round_trip < i)) - do_again = true; - - } - round_trip++; - } while (do_again); - } - - if (got_rect_ub) - break; - } - } - } - } - } - } - - hull.simplify(); - hull.copy_names(Rs[first_non_null]); - hull.setup_names(); - return hull; -} - -} - |