#ifndef _range_hpp_INCLUDED
#define _range_hpp_INCLUDED

namespace CaDiCaL {

struct Clause;

/*----------------------------------------------------------------------*/

// Used for compact and safe iteration over positive ranges of integers,
// particularly for iterating over all variable indices.
//
//   Range vars (max_var);
//   for (auto idx : vars) ...
//
// This iterates over '1, ..., max_var' and is safe for non-negative
// numbers, thus also for 'max_var == 0' or 'max_var == INT_MAX'.
//
// Note that
//
//   for (int idx = 1; idx <= max_var; idx++) ...
//
// leads to an overflow if 'max_var == INT_MAX' and thus depending on what
// the compiler does ('int' overflow is undefined) might lead to any
// behaviour (infinite loop or worse array access way out of bounds).
//
// If we make 'idx' in this last 'for' loop an 'unsigned' then it is safe to
// use this idiom, but we would need to cast 'max_var' explicitly to 'int'
// in order to avoid a warning in the loop condition and actually everywhere
// where 'idx' is compared to a 'signed' expression.  Worse for instance
// 'vals[-idx]' will lead to out of bounds access too.  This is awkward and
// using the range iterator provided here is safer in general.
//
// Another issue is that the dereferencing operator '*' below is required to
// return a reference to the internal index of the iterator.  Thus the 'idx'
// in the auto loop is actually of the same type as the internal state of
// the iterator.  To keep it 'signed' and still avoid overflow issues we
// just have to make sure to use the proper increment (with two implicit
// casts, i.e., from 'int' to 'unsigned', then 'unsigned' addition and the
// result is cast back from 'unsigned' to 'int').
//
// For simplicity we keep a reference to the actual maximum integer, e.g.,
// 'max_var', which makes the idiom 'for (auto idx : vars) ...' possible.
// Further note that the referenced integer has to be non-negative before
// starting to iterate (it can be zero though), otherwise it breaks.

class Range {
  static unsigned inc (unsigned u) { return u + 1u; }
  class iterator {
    int idx;
  public:
    iterator (int i) : idx (i) { }
    void operator++ () { idx = inc (idx); }
    const int & operator* () const { return idx; }
    friend bool operator != (const iterator & a, const iterator & b) {
      return a.idx != b.idx;
    }
  };
  int & n;
public:
  iterator begin () const { return assert (n >= 0), iterator (inc (0)); }
  iterator end ()   const { return assert (n >= 0), iterator (inc (n)); }
  Range (int & m) : n (m) { assert (m >= 0); }
};

// Same, but iterating over literals '-1,1,-2,2,....,-max_var,max_var'.
//
// The only difference to 'Range' is the 'inc' function, but I am too lazy
// to figure out how to properly factor the code into a generic range
// template with 'inc' as only parameter.  This gives at least clean code.

class Sange {
  static unsigned inc (unsigned u) { return ~u + (u >> 31); }
  class iterator {
    int lit;
  public:
    iterator (int i) : lit (i) { }
    void operator++ () { lit = inc (lit); }
    const int & operator* () const { return lit; }
    friend bool operator != (const iterator & a, const iterator & b) {
      return a.lit != b.lit;
    }
  };
  int & n;
public:
  iterator begin () const { return assert (n >= 0), iterator (inc (0)); }
  iterator end ()   const { return assert (n >= 0), iterator (inc (n)); }
  Sange (int & m) : n (m) { assert (m >= 0); }
};

}

#endif