/*****************************************************************************
 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>
#include <code_gen/CGdebug.h>

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) { 
          //Relation s = copy(R);
          //s.simplify(2,4);
          //return s;
          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);

        // was Relation cond = pick_one_guard(r);
        Relation cond = pick_one_guard(r,loops[start]->level_);
        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, 
                               std::map<std::string, std::vector<CG_outputRepr *> > unin) {
    CG_DEBUG_PRINT("output_ident( %s )\n", v->name().c_str());
    
    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) { 
        CG_outputRepr *tmp =  assigned_on_the_fly[pos-1].first->clone();
        return tmp;
      }
      else {
        CG_outputRepr *tmp =  ocg->CreateIdent(v->name());
        return tmp;
      }
    }
    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;
        if (unin.find(v->get_global_var()->base_name()) != unin.end()) {
          
          std::vector<CG_outputRepr *> argList_ = unin.find(
            v->get_global_var()->base_name())->second;
          
          for (int l = 0; l < argList_.size(); l++)
            argList.push_back(argList_[l]->clone());
          
        } 
        else {
          for (int i = 1; i <= arity; i++) {
            
            /*
             */
            if (assigned_on_the_fly.size() > (R.n_inp() + i - 1)) {
              if (assigned_on_the_fly[R.n_inp() + i - 1].first != NULL)
                argList.push_back(
                  assigned_on_the_fly[R.n_inp() + i - 1].first->clone());
              else
                argList.push_back(
                  ocg->CreateIdent(
                    const_cast<Relation &>(R).input_var(
                      2 * i)->name()));
            } else
              argList.push_back(
                ocg->CreateIdent(
                  const_cast<Relation &>(R).input_var(
                    2 * i)->name()));
            
            /*if (assigned_on_the_fly[2*i - 1].first == NULL)
              argList.push_back(
              ocg->CreateIdent(
              const_cast<Relation &>(R).input_var(2 * i)->name()));
              else
              argList.push_back(assigned_on_the_fly[2*i - 1].first->clone());
            */
          }
        }
        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,
    std::map<std::string, std::vector<CG_outputRepr *> > unin) {
    
    int numfly =  assigned_on_the_fly.size();
    for (int i=0; i<numfly; i++) {
      std::pair<CG_outputRepr *, int>p = assigned_on_the_fly[i];
      CG_outputRepr *tr = NULL;
      if (p.first != NULL) tr = p.first->clone();
      int val = p.second;
    }

    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, unin);  
        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, unin);
      }
    }
    else { 
      assign_repr = output_substitution_repr(ocg, result.first, v, true, R,
                                             assigned_on_the_fly, unin);
    }
    
    if (assign_repr == NULL) { 
      assign_repr = ocg->CreateInt(0);
    }
    
    //fprintf(stderr, "assigned on the fly  %d\n", numfly );
    //for (int i=0; i<numfly; i++) { 
    //  //fprintf(stderr, "i %d\n", i); 
    //  std::pair<CG_outputRepr *, int>p = assigned_on_the_fly[i];
    //  CG_outputRepr *tr = NULL;
    //  if (p.first != NULL) tr = p.first->clone();
    //  int val = p.second;
    //  //fprintf(stderr, "0x%x   %d\n", tr, val);
    //} 
    
    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,
                                          std::map<std::string, std::vector<CG_outputRepr *> > unin) {
    //fprintf(stderr, "output_substitution_repr(  v = '%s' )\n", v->char_name()); 
    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) {
        //fprintf(stderr, "cvi\n"); 
        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, unin);
        }
        else { 
          //fprintf(stderr, "else t = output_ident()\n"); 
          t = output_ident(ocg, R, cvi.curr_var(), assigned_on_the_fly, unin);
          //if (t== NULL) fprintf(stderr, "t NULL\n"); 
        }
        coef_t coef = cvi.curr_coef();
        //fprintf(stderr, "coef %d\n", coef); 
        
        //fprintf(stderr, "a %d\n", a); 
        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) {
              //fprintf(stderr, "repr = ocg->CreatePlus(repr, t);\n"); 
              repr = ocg->CreatePlus(repr, t);
              //if (repr == NULL) fprintf(stderr, "repr NULL\n"); 
              //else fprintf(stderr, "repr NOT NULL\n"); 
            }
            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));
          }        
        }
      }
    
    //if (repr == NULL) fprintf(stderr, "before inequality, repr == NULL\n"); 
    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)));
    
    //if (repr == NULL) fprintf(stderr, "at end, repr == NULL\n"); 
    //fprintf(stderr, "leaving output_substitution_repr()\n"); 
    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::map<std::string, std::vector<CG_outputRepr *> > unin) {
    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, unin);
        if (repr == NULL) CG_ERROR("IN IF, repr for %s assigned NULL\n", v->char_name());
      }
      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, unin);
          }
          catch (const codegen_error &) {
          }
      }
      
      if (repr == NULL) CG_ERROR("repr NULL\n");
      if (repr != NULL) { 
        subs.push_back(repr);
      }
      else { 
        //Anand:Add additional checks for variables that have been mapped to inspector/global variables
        for (int k = 1; k <= R.n_out(); k++) {
          //Relation mapping1(mapping.n_out(), 1);
          //F_And *f_root = mapping1.add_and();
          //EQ_Handle h = f_root->add_EQ();
          //h.update_coef(mapping1.output_var(1), 1);
          //h.update_coef(mapping1.input_var(i), -1);
          //Relation r = Composition(mapping1, copy(mapping));
          //r.simplify();

          Relation r = copy(R);
          
          Variable_ID v = r.output_var(k);
          CG_outputRepr* inspector = NULL;
          bool has_insp = false;
          Global_Var_ID global_insp;
          
          std::pair<EQ_Handle, int> result = find_simplest_assignment(
            copy(r), v, assigned_on_the_fly);
          CG_outputRepr *repr_ = NULL;
          if (result.second < INT_MAX) {
            /*std::vector<Variable_ID> variables;
            //Anand: commenting this out as well :  05/29/2013
            variables.push_back(r.input_var(2 * k));
            for (Constr_Vars_Iter cvi(result.first); cvi; cvi++) {
            Variable_ID v1 = cvi.curr_var();
            if (v1->kind() == Input_Var)
            variables.push_back(v1);

            }
            */
            repr_ = output_substitution_repr(ocg, result.first, v, true,
                                             copy(r), assigned_on_the_fly, unin);
            
            for (DNF_Iterator di(copy(r).query_DNF()); di; di++)
              for (GEQ_Iterator ci = (*di)->GEQs(); ci; ci++) {
                
                //Anand: temporarily commenting this out as it causes problems 5/28/2013
                /*int j;
                  for (j = 0; j < variables.size(); j++)
                  if ((*ci).get_coef(variables[j]) == 0)
                  break;
                  if (j != variables.size())
                  continue;
                */
                for (Constr_Vars_Iter cvi(*ci); cvi; cvi++) {
                  Variable_ID v1 = cvi.curr_var();
                  if (v1->kind() == Global_Var)
                    if (v1->get_global_var()->arity() > 0) {
                      
                      if (i
                          <= v1->get_global_var()->arity()) {
                        
                        /*  std::pair<EQ_Handle, int> result =
                            find_simplest_assignment(
                            copy(r), v,
                            assigned_on_the_fly);
                            
                            if (result.second < INT_MAX) {
                            CG_outputRepr *repr =
                            output_substitution_repr(
                            ocg,
                            result.first, v,
                            true, copy(r),
                            assigned_on_the_fly);
                            
                            inspector =
                            ocg->CreateArrayRefExpression(
                            ocg->CreateDotExpression(
                            ocg->ObtainInspectorData(
                            v1->get_global_var()->base_name()),
                            ocg->CreateIdent(
                            copy(
                            R).output_var(
                            i)->name())),
                            repr);
                            } else
                        */
                        inspector =
                          /*  ocg->CreateArrayRefExpression(
                              ocg->CreateDotExpression(
                              ocg->ObtainInspectorData(
                              v1->get_global_var()->base_name()),
                              ocg->CreateIdent(
                              copy(
                              R).output_var(
                              i)->name())),
                              repr);*/
                          
                          ocg->CreateArrayRefExpression(
                            
                            ocg->ObtainInspectorData(
                              v1->get_global_var()->base_name(),
                              
                              copy(R).output_var(
                                i)->name()),
                            repr_);
                        //ocg->CreateIdent(
                        //    v->name()));
                        
                      }
                    }
                  
                }
              }
          }
          
          if (inspector != NULL) {
            subs.push_back(inspector);
            break;
          } else if (k == i && repr_ != NULL) {
            subs.push_back(repr_);
            
          }
          
          //std::pair<EQ_Handle, int> result = find_simplest_assignment(r,
          //    v, assigned_on_the_fly, &has_insp);
          
          /*if (has_insp) {
            
            bool found_insp = false;
            //Anand: check if inspector constraint present in equality
            for (Constr_Vars_Iter cvi(result.first); cvi; cvi++) {
            Variable_ID v = cvi.curr_var();
            if (v->kind() == Global_Var)
            if (v->get_global_var()->arity() > 0) {
            global_insp = v->get_global_var();
            found_insp = true;
            }
            
            }
            if (found_insp)
            if (i <= global_insp->arity())
            inspector =
            ocg->CreateArrayRefExpression(
            ocg->CreateDotExpression(
            ocg->ObtainInspectorData(
            global_insp->base_name()),
            ocg->CreateIdent(
            copy(R).output_var(
            i)->name())),
            ocg->CreateIdent(v->name()));
            
            
            }
          */
        } // for int k 
      }
    }
    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,
                                                     bool *found_inspector_global) {
    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) {
              //Anand  --start: Check for Global Variable not being involved in any GEQ
              Conjunct *d =
                const_cast<Relation &>(R).single_conjunct();
              bool found = false;
              for (GEQ_Iterator g(d->GEQs()); g; g++)
                if ((*g).get_coef(v) != 0) {
                  found = true;
                  break;
                }
              if (!found)
                cost += 10;  // function cost
              else {
                cost = INT_MAX;
                eq = *e;
                if (found_inspector_global != NULL)
                  *found_inspector_global = true;
                return std::make_pair(eq, cost);
              } //Anand    --end: Check for Global Variable not being involved in any GEQ
            } 
            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 (found_inspector_global != NULL)
            *found_inspector_global = true;
        }
      }
    
    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;
          if (found_inspector_global != NULL)
            *found_inspector_global = true;
        }
      }
    
    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());
  }
  
  //Anand- adding the following just for debug
  std::vector<std::pair<bool, GEQ_Handle> > find_floor_definition_temp(
    const Relation &R, Variable_ID v,
    std::set<Variable_ID> excluded_floor_vars) {
    Conjunct *c = const_cast<Relation &>(R).single_conjunct();
    std::vector<std::pair<bool, GEQ_Handle> > to_return;
    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;
      
      //Anand: commenting out the following for debug   7/28/2013
      bool interested = true;
      Variable_ID possibly_interfering;
      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) {
          possibly_interfering = *i;
          interested = false;
          break;
        }
      
      //  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 (v == cvi.curr_var()
                && (*e2).get_coef(cvi.curr_var())
                != -cvi.curr_coef()) {
              match = false;
              break;
            }
          if (!match)
            continue;
          for (Constr_Vars_Iter cvi(*e2); cvi; cvi++)
            if (v == cvi.curr_var()
                && (*e).get_coef(cvi.curr_var())
                != -cvi.curr_coef()) {
              match = false;
              break;
            }
          if (match) {
            to_return.push_back(std::make_pair(true, *e));
            if (!interested)
              to_return.push_back(std::make_pair(true, *e2));
            return to_return;
            
          }
        }
    }
    
    to_return.push_back(std::make_pair(false, GEQ_Handle()));
    
    return to_return;
  }

//
// 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,
                              std::map<std::string, std::vector<CG_outputRepr *> > unin) {
    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, unin);
          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()) {
        //fprintf(stderr, "GEQ\n"); 
        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, 
                                          unin);
          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);
        }
        //fprintf(stderr, "result =  ocg->CreateAnd(result, term);\n"); 
        result = ocg->CreateAnd(result, term);
      }
    
    // e.g. 4i=5j+4alpha
    for (EQ_Iterator e = c->EQs(); e; e++)
      if ((*e).has_wildcards()) {
        //fprintf(stderr, "EQ ??\n"); 
        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, unin);
            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()) {
        //fprintf(stderr, "GEQ ??\n"); 
        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, unin);
              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, unin);
              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::map<std::string, std::vector<CG_outputRepr *> > unin,
                                        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);
    
    std::vector<std::pair<bool, GEQ_Handle> > result2;
    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) {
            coef_t coef_ = cvi.curr_coef();
            result2 = find_floor_definition_temp(R, cvi.curr_var(),
                                                 excluded_floor_vars);
            for (Constr_Vars_Iter cvi_(
                   result2[result2.size() - 1].second); cvi_; cvi_++) {
              if (cvi_.curr_var()->kind() != Wildcard_Var
                  && cvi_.curr_var()->kind() != Set_Var) {
                t = output_ident(ocg, R, cvi_.curr_var(),
                                 assigned_on_the_fly, unin);
                coef_t coef2 = cvi_.curr_coef();
                assert(cvi_.curr_coef() == -1 && a == 1);
                repr = ocg->CreateIntegerFloor(t,
                                               ocg->CreateInt(-coef_));
                repr = ocg->CreateTimes(ocg->CreateInt(-coef_),
                                        repr);
                return repr;
                
              }
              
            }
            
          };

          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, 
                                       unin, 
                                       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, unin);
        
        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,
                                         std::map<std::string, std::vector<CG_outputRepr *> > unin) {
    assert(inequality.get_coef(v) < 0);
    CG_outputRepr* zero_;
    
    zero_ = output_inequality_repr(ocg, inequality, v, R, assigned_on_the_fly, 
                                   unin);
    
    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,
                                         std::map<std::string, std::vector<CG_outputRepr *> > unin) {
    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, unin);
      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,unin);
      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, unin);
      }
      
      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();
    fprintf(stderr, "stride eq const %d\n", c); 
    fprintf(stderr, "sign %d\n", sign ); 
    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, unin);
    //fprintf(stderr, "inequality repr %p\n", repr); 
    CG_outputRepr *repr2 = ocg->CreateCopy(repr);
    
    fprintf(stderr, "stride_eq.get_coef(wc) %d\n", stride_eq.get_coef(wc)); 
    fprintf(stderr, "repr + mod( strideBoundRepr - repr, %d )\n", stride_eq.get_coef(wc)); 

    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::map<std::string, std::vector<CG_outputRepr *> > unin) {
    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, unin);
          if (repr == NULL) {
            CG_ERROR("NULL lowerbound, assumed zero\n");
            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, 
                                                        unin);
          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) {
      CG_DEBUG_PRINT("CG_utils.cc output_loop() createInvoke( max )\n");
      lbRepr = ocg->CreateInvoke("max", lbList);
    }
    else { // (lbList.size() == 1)
      lbRepr = lbList[0];
    }

    CG_outputRepr *ubRepr = NULL;
    if (ubList.size() > 1) {
      CG_DEBUG_PRINT("CG_utils.cc output_loop() createInvoke( min )\n");
      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, 
                                            unin);
    //fprintf(stderr,"CG_utils.cc output_loop()  returning CreateInductive()\n"); 
    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) {
    //Anand: commenting the assertion out 8/4/2013
    //assert(R.n_out() == 0 && r.n_out() == 0 && R.n_inp() == r.n_inp());
    bool is_mapping = false;
    if (r.n_out() > 0)
      is_mapping = true;
    
    std::set<Variable_ID> excluded_floor_vars;
    std::set<Variable_ID> excluded_floor_vars2;
    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);
      std::vector<std::pair<bool, GEQ_Handle> > result2;
      
      if (!result.first) {
        
        result2 = find_floor_definition_temp(R, v, excluded_floor_vars2);
        assert(result2.size() >= 1);
        result = result2[0];
      } 
      else
        result2.push_back(result);

      assert(result.first);
      excluded_floor_vars.insert(v);
      excluded_floor_vars2.insert(v);
      
      for (int i = 0; i < result2.size(); i++) {

        GEQ_Handle h1 = f_root->add_GEQ();
        GEQ_Handle h2 = f_root->add_GEQ();
        for (Constr_Vars_Iter cvi(result2[i].second); cvi; cvi++) {
          Variable_ID v2 = cvi.curr_var();
          switch  (v2->kind()) {
          case Input_Var: {
            int pos = v2->get_position();
             if (!is_mapping) {
              h1.update_coef(r.input_var(pos), cvi.curr_coef());
              h2.update_coef(r.input_var(pos), -cvi.curr_coef());
            } 
            else {
              h1.update_coef(r.output_var(pos), cvi.curr_coef());
              h2.update_coef(r.output_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(result2[i].second.get_const());
        h2.update_const(
          -result2[i].second.get_const()
          - result2[i].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) {
    //fprintf(stderr, "pick_one_guard()\n"); 
    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,
                                 std::vector<std::map<std::string, std::vector<CG_outputRepr *> > > unin) {
    //fprintf(stderr, "\n\nleaf_print_repr()\n"); 
    
    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::vector<CG_outputRepr *> sList = output_substitutions(ocg, 
                                                                  mapping, 
                                                                  assigned_on_the_fly,
          unin[*i]);
        
        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,
                                                        unin));

      if (guard_repr == NULL)
        return stmt_list;
      else {
        fprintf(stderr, "CG_utils.cc leaf_print_repr() CreateIf()\n"); 
        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());
      BoolSet<> else_active(active.size());
      BoolSet<> 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());
      
      //Anand: adding support for Replacing substituted variables within
      //Uninterpreted function symbols or global variables with arity > 0 here
      //--begin
      std::vector<std::pair<CG_outputRepr *, int> > aotf = assigned_on_the_fly;

      CG_outputRepr *new_guard_repr = output_guard(ocg, then_cond, aotf, 
                                                   unin[*(active.begin())]);
      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, 
                               unin);


      }
      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,
          unin);

        stmt_list = ocg->StmtListAppend(stmt_list, 
                                        leaf_print_repr(indep_active, 
                                                        guards, 
                                                        NULL, 
                                                        known, 
                                                        new_indent, 
                                                        ocg, 
                                                        remap, 
                                                        xforms, 
                                                        stmts, 
                                                        assigned_on_the_fly,
                                                        unin));

        if (guard_repr == NULL)
          return stmt_list;
        else {
          fprintf(stderr, "CG_utils.cc leaf_print_repr() CreateIf() 2\n"); 
          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,
                                                        unin);
        
        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,
                                                        unin);

        fprintf(stderr, "CG_utils.cc leaf_print_repr() CreateIf() 3\n"); 
        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,
                                                          unin));

        if (guard_repr == NULL)
          return stmt_list;
        else {
          fprintf(stderr, "CG_utils.cc leaf_print_repr() CreateIf() 4\n"); 
          return ocg->CreateIf(indent, guard_repr, stmt_list, NULL);
        }
      }
    }
  }
  
  



  std::string print_to_iegen_string(Relation &R) {
    std::string s = "";
    for (GEQ_Iterator e(R.single_conjunct()->GEQs()); e; e++) {
      if (s != "")
        s += " && ";
      s += (*e).print_to_string();
    }
    
    for (EQ_Iterator e(R.single_conjunct()->EQs()); e; e++) {
      if (s != "")
        s += " && ";
      s += (*e).print_to_string();
    }
    return s;
  }



//
// Check if a set/input var is projected out of a inequality by a global variable with arity > 0
//
  Relation checkAndRestoreIfProjectedByGlobal(const Relation &R1,
                                              const Relation &R2, Variable_ID v) {
    
    Relation to_return(R2.n_set());
    
//1. detect if a variable is not involved in a GEQ.
    for (DNF_Iterator di(copy(R1).query_DNF()); di; di++)
      for (GEQ_Iterator ci = (*di)->GEQs(); ci; ci++)
        if ((*ci).get_coef(v) != 0)
          return copy(R2);
    
    bool found_global_eq = false;
    Global_Var_ID g1;
    EQ_Handle e;
//2. detect if its involved in an eq involving a global with arity >= 1
    for (DNF_Iterator di(copy(R1).query_DNF()); di; di++)
      for (EQ_Iterator ci = (*di)->EQs(); ci; ci++)
        if ((*ci).get_coef(v) != 0)
          for (Constr_Vars_Iter cvi(*ci); cvi; cvi++) {
            v = cvi.curr_var();
            if (v->kind() == Global_Var)
              if (v->get_global_var()->arity() > 0) {
                found_global_eq = true;
                g1 = v->get_global_var();
                e = (*ci);
              }
          }
    
    if (!found_global_eq)
      return copy(R2);
    
//3. check if the global is involved in a geq
    
    bool found_global_lb = false;
    bool found_global_ub = false;
    
    std::vector<GEQ_Handle> ub;
    std::vector<GEQ_Handle> lb;
    for (DNF_Iterator di(copy(R1).query_DNF()); di; di++)
      for (GEQ_Iterator ci = (*di)->GEQs(); ci; ci++)
        for (Constr_Vars_Iter cvi(*ci); cvi; cvi++) {
          Variable_ID v = cvi.curr_var();
          if (v->kind() == Global_Var)
            if (v->get_global_var()->arity() > 0
                && v->get_global_var() == g1) {
              if (cvi.curr_coef() > 0) {
                found_global_lb = true;
                
                lb.push_back(*ci);
              } 
              else if (cvi.curr_coef() < 0) {
                found_global_ub = true;
                
                ub.push_back(*ci);
              }
              
            }
        }
    
    if (!found_global_lb || !found_global_ub)
      return copy(R2);
    
//
    
    F_And *root = to_return.add_and();
    
    for (int i = 0; i < lb.size(); i++) {
      GEQ_Handle lower = root->add_GEQ();
      for (Constr_Vars_Iter cvi(lb[i]); cvi; cvi++) {
        Variable_ID v2 = cvi.curr_var();
        
        if (v2->kind() == Wildcard_Var)
          return copy(R2);
        if (v2->kind() != Global_Var
            || (v2->kind() == Global_Var && v2->get_global_var() != g1)) {
          if (v2->kind() != Global_Var)
            lower.update_coef(v2, cvi.curr_coef());
          else {
            Variable_ID lb1 = to_return.get_local(v2->get_global_var(),
                                                  Input_Tuple);
            lower.update_coef(lb1, cvi.curr_coef());
          }
          
        } 
        else
          lower.update_coef(v, cvi.curr_coef());
      }
      
      lower.update_const(lb[i].get_const());
    }
    
    for (int i = 0; i < ub.size(); i++) {
      GEQ_Handle upper = root->add_GEQ();
      for (Constr_Vars_Iter cvi(ub[i]); cvi; cvi++) {
        Variable_ID v2 = cvi.curr_var();
        
        if (v2->kind() == Wildcard_Var)
          return copy(R2);
        if (v2->kind() != Global_Var
            || (v2->kind() == Global_Var && v2->get_global_var() != g1)) {
          if (v2->kind() != Global_Var)
            upper.update_coef(v2, cvi.curr_coef());
          else {
            Variable_ID ub1 = to_return.get_local(v2->get_global_var(),
                                                  Input_Tuple);
            upper.update_coef(ub1, cvi.curr_coef());
          }
          
        } 
        else
          upper.update_coef(v, cvi.curr_coef());
      }
      
      upper.update_const(ub[i].get_const());
    }
    
//Relation to_return2 = copy(R2);
    
    for (EQ_Iterator g(const_cast<Relation &>(R2).single_conjunct()->EQs()); g;
         g++)
      to_return.and_with_EQ(*g);
    
    for (GEQ_Iterator g(const_cast<Relation &>(R2).single_conjunct()->GEQs());
         g; g++) {
      bool found_glob = false;
      for (Constr_Vars_Iter cvi(*g); cvi; cvi++) {
        Variable_ID v2 = cvi.curr_var();
        if (v2->kind() == Global_Var && v2->get_global_var() == g1) {
          found_glob = true;
          break;
        }
      }
      if (!found_glob)
        to_return.and_with_GEQ(*g);
      
    }
//to_return.and_with_EQ(e);
    
    to_return.copy_names(copy(R2));
    to_return.setup_names();
    to_return.finalize();
    return to_return;
  }
/*Relation addInequalitiesToRelation(const Relation &R,
  std::vector<GEQ_Handle> &inequalities) {
  Relation to_return(R.n_set());
  
  return to_return;
  }
  
*/
  



  
//
// heavy lifting for code output for one level of loop nodes
//
  CG_outputRepr *loop_print_repr(BoolSet<> active,
                                 const std::vector<CG_loop *> &loops, 
                                 int start, 
                                 int end,
                                 const Relation &guard, 
                                 CG_outputRepr *guard_repr,
                                 int indent, 
                                 const std::vector<int> &remap, 
                                 const std::vector<Relation> &xforms,
                                 CG_outputBuilder *ocg, 
                                 const std::vector<CG_outputRepr *> &stmts,
                                 const std::vector<std::pair<CG_outputRepr *, int> > &assigned_on_the_fly,
                                 std::vector<std::map<std::string, std::vector<CG_outputRepr *> > > unin) {

    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,
                                                            unin));
      stmt_list = ocg->StmtListAppend(stmt_list,
                                      loop_print_repr(active,
                                                      loops, 
                                                      i, 
                                                      end, 
                                                      guard, 
                                                      NULL, 
                                                      new_indent, 
                                                      remap, 
                                                      xforms, 
                                                      ocg, 
                                                      stmts, 
                                                      assigned_on_the_fly,
                                                      unin));
      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);
    
    //Anand: adding support for Replacing substituted variables within
    //Uninterpreted function symbols or global variables with arity > 0 here
    //--begin
    std::vector<std::pair<CG_outputRepr *, int> > aotf = assigned_on_the_fly;
    CG_outputRepr *new_guard_repr = output_guard(ocg, then_cond, aotf, unin[*(active.begin())]);

    //fprintf(stderr, "new_guard_repr 0x%x\n", new_guard_repr); 
    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(active, loops, start, end, new_guard, guard_repr,
                             indent,  remap, xforms, ocg, stmts, aotf, unin);
    }
    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(active,
                                                 loops, 
                                                 start, 
                                                 i, 
                                                 new_guard, 
                                                 new_guard_repr, 
                                                 new_indent, 
                                                 remap, 
                                                 xforms, 
                                                 ocg, 
                                                 stmts, 
                                                 aotf,
                                                 unin);
      stmt_list = ocg->StmtListAppend(stmt_list,
                                      loop_print_repr(active,
                                                      loops, 
                                                      j, 
                                                      end, 
                                                      guard, 
                                                      NULL, 
                                                      new_indent, 
                                                      remap, 
                                                      xforms, 
                                                      ocg, 
                                                      stmts, 
                                                      aotf,
                                                      unin));

      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(active,
                                                      loops, 
                                                      start, 
                                                      i, 
                                                      then_new_guard, 
                                                      NULL, 
                                                      new_indent+1, 
                                                      remap, 
                                                      xforms, 
                                                      ocg, 
                                                      stmts, 
                                                      aotf,
                                                      unin);

      Relation else_new_guard = Intersection(copy(guard), copy(else_cond));
      else_new_guard.simplify();
      CG_outputRepr *else_stmt_list = loop_print_repr(active,
                                                      loops, 
                                                      i, 
                                                      j, 
                                                      else_new_guard, 
                                                      NULL, 
                                                      new_indent+1, 
                                                      remap, 
                                                      xforms, 
                                                      ocg, 
                                                      stmts, 
                                                      aotf,
                                                      unin);
      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(active,
                                                      loops, 
                                                      j, 
                                                      end, 
                                                      guard, 
                                                      NULL, 
                                                      new_indent, 
                                                      remap, 
                                                      xforms, 
                                                      ocg, 
                                                      stmts, 
                                                      aotf,
                                                      unin));
      

      if (guard_repr == NULL)
        return stmt_list;
      else {
        return ocg->CreateIf(indent, guard_repr, stmt_list, NULL);
      }
    }
  }
  
}