#include "clang/Analysis/Analyses/Interval.h"
#include "clang/AST/Stmt.h"
#include "clang/Analysis/CFG.h"
#include "clang/Analysis/AnalysisContext.h"
#include "clang/AST/StmtVisitor.h"

#include "clang/Analysis/Analyses/IntervalSolver/Log.hpp"
#include "clang/Analysis/Analyses/IntervalSolver/Complete.hpp"
#include "clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp"
#include "clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp"

#include "MCFSimplex.h"
  
#include "llvm/ADT/PostOrderIterator.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/Support/Process.h"
  
#include <deque>
#include <algorithm>
#include <vector>
#include <map>
#include <set>

using namespace clang;

std::string negate_string(const std::string& str) {
  if (str[0] == '-')
    return str.substr(1);
  return '-' + str;
}

#include <sstream>
template<typename T>
std::string toString(const T& obj) {
  std::stringstream stream;
  stream << obj;
  return stream.str();
}

#include <ostream>
template<typename K,typename V>
std::ostream& operator<<(std::ostream& cout, const std::pair<K,V>& v) {
  cout << "(" << v.first << ", " << v.second << ")";
  return cout;
}
template<typename V>
std::ostream& operator<<(std::ostream& cout, const std::pair<Variable<Complete<int64_t> >*, V>& v) {
  cout << "(" << v.first->name() << ", " << v.second << ")";
  return cout;
}

template<typename V>
std::ostream& operator<<(std::ostream& cout, const std::vector<V>& v) {
  cout << "[";
  for(typename std::vector<V>::const_iterator it = v.begin(), ei = v.end();
      it != ei;
      ++it) {
    if (it != v.begin())
      cout << ", ";
    cout << *it;
  }
  cout << "]";
  return cout;
}

template<typename K,typename V>
std::ostream& operator<<(std::ostream& cout, const std::map<K,V>& v) {
  cout << "{";
  for (typename std::map<K,V>::const_iterator it = v.begin(), ei = v.end();
       it != ei;
       ++it) {
    if (it != v.begin())
      cout << ", ";
    cout << it->first << ": " << it->second;
  }
  cout << "}";
  return cout;  
}

// Two pieces of state:
//  -> condition protecting a node
//  -> node's expression itself
// We can then combine these in a straightforward way to
// get out equation system, whereupon we can solve for what
// we want to know. Then we can have program invariants!
//
// Hooray!

typedef Complete<int64_t> ZBar;
template<>
ZBar infinity() {
  return ZBar(1, true);
}
//typedef std::map<std::string, ZBar> Vector;

struct Vector : public std::map<std::string, ZBar> {
  Vector(const ZBar& val=0)
    : _val(val) { }
  ZBar operator[](const std::string& key) const {
    if (this->find(key) != this->end())
      return this->find(key)->second;
    return _val;
  }
  ZBar& operator[](const std::string& key) {
    if (this->find(key) != this->end())
      return this->find(key)->second;
    std::pair<iterator,bool> p = this->insert(std::pair<const std::string, ZBar>(key, _val));
    return p.first->second;
  }
  ZBar _val;
};

Vector negate_vector(const Vector& v) {
  Vector result;
  for (Vector::const_iterator it = v.begin(),
         ei = v.end();
       it != ei;
       ++it) {
    result[negate_string(it->first)] = it->second;
  }
  return result;
}

typedef std::pair<Vector, ZBar> Result; // a "slice" of an equation

Result negate_result(const Result& r) {
  return Result(negate_vector(r.first), -r.second);
}

//typedef std::map<std::string, Result> LinearEquation; // one `Result` per variable
struct LinearEquation : public std::map<std::string, Result> {
  Result operator[](const std::string& key) const {
    if (this->find(key) != this->end())
      return this->find(key)->second;
    Result r;
    r.first[key] = 1;
    r.second = 0;
    return r;
  }
  Result& operator[](const std::string& key) {
    if (this->find(key) != this->end())
      return this->find(key)->second;
    Result r;
    r.first[key] = 1;
    r.second = 0;
    std::pair<iterator,bool> p = this->insert(std::pair<const std::string, Result>(key, r));
    return p.first->second;
  }
};

typedef Vector Condition;

typedef EquationSystem<ZBar> EqnSys;
typedef Expression<ZBar> EqnExpr;
typedef Variable<ZBar> EqnVar;


struct LinearOperator : public Operator<Vector> {
  LinearOperator(const LinearEquation* result)
    : _values(result) {}

  Vector eval(const std::vector<Vector>& vector) const {
    assert(vector.size() == 1);
    const Vector& v = vector[0];
    Vector result = v;
    for (LinearEquation::const_iterator it = _values->begin(),
           ei = _values->end();
         it != ei;
         ++it) {
      ZBar subresult = 0;
      for (Vector::const_iterator jt = it->second.first.begin(),
             ej = it->second.first.end();
           jt != ej;
           ++jt) {
        subresult += jt->second * v[jt->first];
      }
      subresult += it->second.second;
      result[it->first] = subresult;
    }
    return result;
  }

  void print(std::ostream& cout) const {
    cout << "linear[" << *_values << "]";
  }

  const LinearEquation* _values;
};



template<class F, class M>
void transform_values(const F& f, M& map) {
  for (typename M::iterator it = map.begin(),
         ei = map.end();
       it != ei;
       ++it) {
    it->second = f(it->second);
  }
}

template<class M, class F> 
M merge_maps_with(const F& f, const M& left, const M& right) {
  M result;
  typename M::const_iterator first1 = left.begin(), last1 = left.end(),
    first2 = right.begin(), last2 = right.end();
  for (; first1 != last1 && first2 != last2;) {
    if (first2->first < first1->first) {
      result[first2->first] = first2->second;
      ++first2;
    } else if (first1->first == first2->first) {
      result[first1->first] = f(first1->second, first2->second);
      ++first1;
      ++first2;
    } else {
      result[first1->first] = first1->second;
      ++first1;
    }
  }
  while (first1 != last1) {
    result[first1->first] = first1->second;
    ++first1;
  }
  while (first2 != last2) {
    result[first2->first] = first2->second;
    ++first2;
  }
  return result;
}

template<class T>
T max(const T& l, const T& r) {
  return (l < r ? l : r);
}
template<class T>
T negate(const T& v) {
  return -v;
}
template<class T>
T addValues(const T& l, const T& r) {
  return l + r;
}

Vector operator-(const Vector& vector) {
  Vector result(-vector._val);
  for (Vector::const_iterator it = vector.begin(),
         ei = vector.end();
       it != ei;
       ++it) {
    result[it->first] = -it->second;
  }
  return result;
}

Vector operator+(const Vector& left, const Vector& right) {
  return merge_maps_with(addValues<ZBar>, left, right);
}

Vector operator-(const Vector& left, const Vector& right) {
  return merge_maps_with(addValues<ZBar>, left, -right);
}

Vector operator*(const Vector& left, const ZBar& right) {
  Vector result;
  for (Vector::const_iterator it = left.begin(),
         ei = left.end();
       it != ei;
       ++it) {
    result[it->first] = (it->second * right);
  }
  return result;
}
Vector operator*(const ZBar& left, const Vector& right) {
  return right * left;
}
bool operator<(const Vector& left, const Vector& right) {
  bool equal = true;
  for (Vector::const_iterator it = left.begin(),
         ei = left.end();
       it != ei;
       ++it) {
    if (it->second < right[it->first]) {
      equal = false;
    } else if (it->second > right[it->first]) {
      return false;
    }
  }
  for (Vector::const_iterator it = right.begin(),
         ei = right.end();
       it != ei;
       ++it) {
    if (left[it->first] < it->second) {
      equal = false;
    } else if (left[it->first] > it->second) {
      return false;
    }
  }
  return equal ? left._val < right._val : true;
}

template<>
Vector infinity<Vector>() {
  return Vector(infinity<ZBar>());
}

std::ostream& operator<<(std::ostream& cout, const Vector& v) {
  cout << "{";
  for (Vector::const_iterator it = v.begin(), ei = v.end();
       it != ei;
       ++it) {
    cout << it->first << ": " << it->second << ", ";
  }
  cout << "_: " << v._val;
  cout << "}";
  return cout;
}






/* Expression functions */

Result fromExpr(const Expr*);

Result fromInteger(const IntegerLiteral* expr) {
  return Result(Vector(0), *expr->getValue().getRawData());
}

Result fromDeclExpr(const DeclRefExpr* expr) {
  Vector val;
  val[expr->getNameInfo().getAsString()] = 1;
  return Result(val, 0);
}

Result fromUnary(const UnaryOperator* op) {
  switch (op->getOpcode()) {
  case UO_PreInc:
    break;
  case UO_PostInc:
    break;
  }
  return Result(Vector(0), 0);
}

Result operator*(const ZBar& l, const Result& r) {
  return Result(l * r.first, l * r.second);
}

Result fromBinary(const BinaryOperator* op) {
  Result left = fromExpr(op->getLHS()->IgnoreParenCasts());
  Result right = fromExpr(op->getRHS()->IgnoreParenCasts());
  
  switch (op->getOpcode()) {
  case BO_Assign:
    return right;
  case BO_Sub:
    right = negate_result(right);
    //transform_values(negate<ZBar>, right.first);
    //right.second *= -1;
  case BO_Add:
    {
      Result result;
      result.first = merge_maps_with(addValues<ZBar>,
                                     left.first, right.first);
      result.second = left.second + right.second;
      return result;
    }
  case BO_Mul:
    {
      if (!left.first.empty() && !right.first.empty()) {
        return Result(Vector(0), 0);
      }
      ZBar scalar = 0;
      Result value;
      if (left.first.empty()) {
        scalar = left.second;
        value = right;
      } else {
        scalar = right.second;
        value = left;
      }
      if (scalar >= 0) {
        return scalar * value;
      } else {
        return -scalar * negate_result(value);
      }
    }
  case BO_LT:
  case BO_LE:
  case BO_GT:
  case BO_GE:
    break;
  } 
  return Result();
}

Result fromExpr(const Expr* stmt) {
  if (!stmt)
    return Result();
  //stmt->dump();
  switch (stmt->getStmtClass()) {
  case Stmt::IntegerLiteralClass:
    return fromInteger(static_cast<const IntegerLiteral*>(stmt));
  case Stmt::DeclRefExprClass:
    return fromDeclExpr(static_cast<const DeclRefExpr*>(stmt));
  case Stmt::UnaryOperatorClass:
    return fromUnary(static_cast<const UnaryOperator*>(stmt));
  case Stmt::BinaryOperatorClass:
    return fromBinary(static_cast<const BinaryOperator*>(stmt));
  }
  const Expr* expr = stmt->IgnoreParenCasts();
  if (stmt != expr)
    return fromExpr(expr);
  llvm::errs() << "we shouldn't get here...\n";
  return Result();
}


/* Comparison stuff */

Condition fromComparison(const BinaryOperator* op, bool negate) {
  Condition cond(infinity<ZBar>());
  if (!op) {
    if (negate)
      return -cond;
    else
      return cond;
  }
  if (op->isRelationalOp()) {
    const Expr* left = op->getLHS()->IgnoreParenCasts();
    const Expr* right = op->getRHS()->IgnoreParenCasts();

    bool flip = false;
    std::string name;
    int64_t value;
    if (left->getStmtClass() == Stmt::DeclRefExprClass) {
      name = static_cast<const DeclRefExpr*>(left)->getNameInfo().getAsString();
    } else if (right->getStmtClass() == Stmt::DeclRefExprClass) {
      name = static_cast<const DeclRefExpr*>(right)->getNameInfo().getAsString();
      flip = true;
    } else {
      return cond;
    }

    if (right->getStmtClass() == Stmt::IntegerLiteralClass) {
      value = *static_cast<const IntegerLiteral*>(right)->getValue().getRawData();
    } else if (left->getStmtClass() == Stmt::IntegerLiteralClass) {
      value = *static_cast<const IntegerLiteral*>(left)->getValue().getRawData();
    } else {
      return cond;
    }

    BinaryOperator::Opcode operation = op->getOpcode();
    if (flip) {
      switch (operation) {
      case BO_LT: operation = BO_GT; break;
      case BO_GT: operation = BO_LT; break;
      case BO_LE: operation = BO_GE; break;
      case BO_GE: operation = BO_LE; break;
      }
    }

    switch (operation) {
    case BO_LT:
      if (negate)
	cond[negate_string(name)] = -value;
      else
	cond[name] = value - 1;
      break;
    case BO_LE:
      if (negate)
	cond[negate_string(name)] = -(value + 1);
      else
	cond[name] = value;
      break;
    case BO_GE:
      if (negate)
	cond[name] = value - 1;
      else
	cond[negate_string(name)] = -value;
      break;
    case BO_GT:
      if (negate)
	cond[name] = value;
      else
	cond['-' + name] = -(value + 1);
      break;
    }
  }
  return cond;
}


struct MinCostFlow : public Operator<ZBar> {
  MinCostFlow(const std::vector<std::pair<EqnVar*, ZBar> >& supplies)
    : solver(0, 0) {
    assert(supplies.size() % 2 == 0);

    if (supplies.size() == 0)
      return;

    MCFClass::FNumber* deficits = new MCFClass::FNumber[supplies.size()];
    MCFClass::Index* starts = new MCFClass::Index[supplies.size()];
    MCFClass::Index* ends = new MCFClass::Index[supplies.size()];

    for (int i = 0, size = supplies.size(); i < size; i += 2) {
      deficits[i] = -supplies[i].second.as<MCFClass::FNumber>();
      deficits[i+1] = -supplies[i+1].second.as<MCFClass::FNumber>();

      starts[i] = i+1;
      ends[i] = i+2;

      starts[i+1] = i+2;
      ends[i+1] = i+1;

      printableSupply.push_back(supplies[i].second);
      printableSupply.push_back(supplies[i+1].second);
    }

    solver.LoadNet(supplies.size(), supplies.size(), // max nodes/arcs
                   supplies.size(), supplies.size(), // current nodes/arcs
                   NULL, NULL, // arcs have inf cap, zero cost (to begin)
                   deficits, // deficits for each node
                   starts, ends); // start/end of each edge

    delete[] deficits;
    delete[] starts;
    delete[] ends;
  }

  ZBar eval(const std::vector<ZBar>& args) const {
    if (args.size() == 0)
      return 0;
    for (int i = 0, size = args.size(); i < size; ++i) {
      //if (args[i] == infinity<ZBar>()) {
      //  if (!solver.IsClosedArc(i))
      //      solver.CloseArc(i);
      //} else {
      //  if (solver.IsClosedArc(i))
      //    solver.OpenArc(i);
      solver.ChgCost(i, args[i].as<MCFClass::CNumber>());
      //}
    }
    std::cerr << "MCF" << this << "<" << printableSupply << ">(" << args << ")" << " = ";
    solver.SolveMCF();
    if (solver.MCFGetStatus() == MCFClass::kUnfeasible){
      std::cerr << -infinity<ZBar>() << std::endl;
      return -infinity<ZBar>();
    } else {
      if (solver.MCFGetFO() == MCFClass::Inf<MCFClass::FONumber>()) {
        std::cerr << infinity<ZBar>() << std::endl;
        return infinity<ZBar>();
      } else if (solver.MCFGetFO() == -MCFClass::Inf<MCFClass::FONumber>()) {
        std::cerr << -infinity<ZBar>() << std::endl;
        return -infinity<ZBar>();        
      } else {
        ZBar result = solver.MCFGetFO();
        std::cerr << result << std::endl;
        return result;
      }
    }
  }

  virtual void print(std::ostream& cout) const {
    cout << "MCF" << this << "<" << printableSupply << ">";
  }
  
  mutable MCFSimplex solver;
  std::vector<ZBar> printableSupply;
};


/* Blocks */

typedef std::map<std::string, unsigned int> Counters;
typedef std::map<std::string, EqnVar*> VarMap;
typedef std::map<const CFGBlock*, std::set<std::string> > BlockVars;

void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) {
  Counters counters;
  std::string block_id = toString(block->getBlockID());
  VarMap vars;

  for (std::set<std::string>::iterator it = block_vars[block].begin(),
	 ei = block_vars[block].end();
       it != ei;
       ++it) {
    vars[*it] = &system.variable(*it + '-' + block_id + "-pre");
  }
  
  for (CFGBlock::const_iterator it = block->begin(),
                                ei = block->end();
       it != ei;
       ++it) {
    const CFGStmt* cfg_stmt = it->getAs<CFGStmt>();
    const Stmt* stmt = cfg_stmt->getStmt();

    std::string name = "";
    Result result;
    if (stmt->getStmtClass() == Stmt::BinaryOperatorClass) {
      const BinaryOperator* binop = static_cast<const BinaryOperator*>(stmt);
      if (binop->isAssignmentOp()) {
        const Expr* left = binop->getLHS()->IgnoreParenCasts();
        const Expr* right = binop->getRHS()->IgnoreParenCasts();
        if (left->getStmtClass() == Stmt::DeclRefExprClass) {
          name = static_cast<const DeclRefExpr*>(left)->getNameInfo().getAsString();
          result = fromExpr(right);
        }
      }
    } else if (stmt->getStmtClass() == Stmt::DeclStmtClass) {
      const DeclStmt* decl_stmt = static_cast<const DeclStmt*>(stmt);
      for (DeclStmt::const_decl_iterator jt = decl_stmt->decl_begin(),
             ej = decl_stmt->decl_end();
           jt != ej;
           ++jt) {
        if ((*jt)->getKind() == Decl::Var) {
          const VarDecl* decl = static_cast<const VarDecl*>(*jt);
          name = decl->getNameAsString();
          result = fromExpr(decl->getInit());
          jt++;
          if (jt != ej) {
            llvm::errs() << "Only the first declaration in a multi-declaration statement is used.\n";
          }
          break; // only take the first one, for now
        }
      }
    }
    if (name == "")
      continue;

    std::string count = toString(counters[name]);
    EqnVar* var = &system.variable(name + '-' + block_id + '[' + count + ']');
    EqnVar* negative_var = &system.variable(negate_string(name) + '-' + block_id + '[' + count + ']');
    counters[name]++;
    for (int negative = 0; negative < 2; ++negative) { // one loop for positive, the other for negative
      if (negative) {
	result = negate_result(result);
      }
      
      EqnExpr* expression;

      if (result.first.size() > 0) {
        // set up the min-cost stuff
        std::vector<EqnExpr*> minCostArgs;
        std::vector<std::pair<EqnVar*, ZBar> > varCosts;
        for (Vector::iterator it = result.first.begin(),
               ei = result.first.end();
             it != ei;
             ++it) {
          if (!vars[it->first])
            vars[it->first] = &system.variable(it->first + '-' + block_id + "-pre");

          EqnVar& var = *vars[it->first];
          EqnVar& negVar = *vars[negate_string(it->first)];

          varCosts.push_back(std::pair<EqnVar*, ZBar>(&var, it->second));
          varCosts.push_back(std::pair<EqnVar*, ZBar>(&negVar, -it->second));

          minCostArgs.push_back(&var);
          minCostArgs.push_back(&negVar);
        }
        EqnExpr* minCostExpr = &system.expression(new MinCostFlow(varCosts), minCostArgs);
        
        // add the constant factor to the min-cost bit
        std::vector<EqnExpr*> additionArgs;
        additionArgs.push_back(&system.constant(result.second));
        additionArgs.push_back(minCostExpr);
        expression = &system.expression(new Addition<ZBar>(), additionArgs);
      } else {
        expression = &system.constant(result.second);
      }

      // max(-inf, expr), so strategy iteration will work
      std::vector<EqnExpr*> maxArgs;
      maxArgs.push_back(&system.constant(-infinity<ZBar>()));
      maxArgs.push_back(expression);
      if (negative)
	system[*negative_var] = &system.maxExpression(maxArgs);
      else
	system[*var] = &system.maxExpression(maxArgs);
    }
    vars[name] = var;
    vars[negate_string(name)] = negative_var;
    block_vars[block].insert(name);
    block_vars[block].insert(negate_string(name));
  }

  // add to our successor entry values
  for (CFGBlock::const_succ_iterator
	 it = block->succ_begin(),
	 ei = block->succ_end();
       it != ei;
       ++it) {
    bool negate_terminator = it != block->succ_begin(); // not the first means `false` branch
    Condition cond = fromComparison(static_cast<const BinaryOperator*>(block->getTerminatorCondition()), negate_terminator);
    for (VarMap::iterator jt = vars.begin(),
	   ej = vars.end();
	 jt != ej;
	 ++jt) {
      block_vars[*it].insert(jt->first);

      ZBar val = cond[jt->first];
      EqnVar* var = &system.variable(jt->first + '-' + toString((*it)->getBlockID()) + "-pre");
      if (system[*var] == NULL) {
	std::vector<EqnExpr*> maxArgs;
	maxArgs.push_back(&system.constant(-infinity<ZBar>()));
	system[*var] = &system.maxExpression(maxArgs);
      }
      
      EqnExpr* expr = NULL;
      if (val == -infinity<ZBar>()) {
	// don't do anything here: min(-inf, x) = -inf  (for all x)
        expr = &system.constant(-infinity<ZBar>());
      } else if (val == infinity<ZBar>()) {
	// no need to have a min here: min(inf, x) = x  (for all x)
	expr = jt->second;
      } else {
	// need a min here
	std::vector<EqnExpr*> minArgs;
	minArgs.push_back(&system.constant(val));
	minArgs.push_back(jt->second);
	expr = &system.expression(new Minimum<ZBar>(), minArgs);
      }

      system[*var]->arguments().push_back(expr);

      /*if (expr) {
	std::set<std::string> ignore;
	for (VarMap::iterator
	       variables = vars.begin(),
	       variables_end = vars.end();
	     variables != variables_end;
	     ++variables) {
	  if (ignore.find(variables->first) != ignore.end())
	    continue;
	  ignore.insert(negate_string(variables->first));

	  std::vector<EqnExpr*> plusArgs;
	  for (int negate = 0; negate < 2; ++negate) {
	    std::string var_name = negate ? negate_string(variables->first) : variables->first;
            if (cond[var_name] == infinity<ZBar>()) {
              // min(x, inf) = x
              plusArgs.push_back(vars[var_name]);
            } else if (cond[var_name] == -infinity<ZBar>()) {
              // min(x, -inf) = -inf
              plusArgs.push_back(&system.constant(-infinity<ZBar>()));
            } else {
              // min(x, y) = ?
              std::vector<EqnExpr*> minArgs;
              minArgs.push_back(vars[var_name]);
              minArgs.push_back(&system.constant(cond[var_name]));
              plusArgs.push_back(&system.expression(new Minimum<ZBar>(), minArgs));
            }
	  }

	  std::vector<EqnExpr*> guard_args;
	  guard_args.push_back(&system.expression(new Addition<ZBar>(), plusArgs)); // value
	  guard_args.push_back(&system.constant(0)); // lower-bound (so value must be >= this)
	  guard_args.push_back(expr); // result
	  expr = &system.expression(new Guard<ZBar>(), guard_args);
	}
	system[*var]->arguments().push_back(expr);
        }*/
    }
  }
}






IntervalAnalysis :: IntervalAnalysis(AnalysisDeclContext &context)
  : context(&context) {
}

IntervalAnalysis :: ~IntervalAnalysis() {
}

void IntervalAnalysis::runOnAllBlocks(const Decl& decl) {
  const CFG *cfg = this->context->getCFG();

  cfg->dump(context->getASTContext().getLangOpts(),
            llvm::sys::Process::StandardErrHasColors());

  EqnSys system; 
  BlockVars block_vars;

  std::vector<EqnExpr*> infArg; 
  infArg.push_back(&system.constant(-infinity<ZBar>())); // left-most argument has to be -infinity
  infArg.push_back(&system.constant(infinity<ZBar>()));
  std::set<std::string>& function_arguments = block_vars[&cfg->getEntry()];
  std::string block_id = toString(cfg->getEntry().getBlockID());
  if (const FunctionDecl* func = dyn_cast<const FunctionDecl>(&decl)) {
    for (unsigned int i = func->getNumParams(); i > 0; i--) {
      std::string name = func->getParamDecl(i-1)->getNameAsString();

      // add the variables to the first block
      function_arguments.insert(name);
      function_arguments.insert(negate_string(name));
      
      // set the vars to infinity (unconstrained)
      system[system.variable(name + '-' + block_id + "-pre")] = &system.maxExpression(infArg);
      system[system.variable(negate_string(name) + '-' + block_id + "-pre")] = &system.maxExpression(infArg);
    }
  }

  std::set<const CFGBlock*> seen;
  std::deque<const CFGBlock*> todo;
  todo.push_back(&cfg->getEntry());

  while (!todo.empty()) {
    const CFGBlock* block = todo.front();
    if (seen.find(todo.front()) != seen.end()) {
      todo.pop_front();
      continue;
    }
    seen.insert(block);
    todo.pop_front();
    runOnBlock(block, system, block_vars);
    for (CFGBlock::const_succ_iterator it = block->succ_begin(),
                                       ei = block->succ_end();
         it != ei;
         it++ ) {
      todo.push_back(*it);
    }
  }

  llvm::errs() << toString(system) << "\n";

  system.indexMaxExpressions();

  Solver<ZBar> solver(system);

  for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
    EqnVar& var = system.variable(size - i - 1);
    llvm::errs() << toString(var.name()) << " = " << toString(solver.solve(var)) << "\n";
  }
}


const void *IntervalAnalysis::getTag() { static int x; return &x; }