BoundIterator.h

 
#pragma once
 
#include <cstddef>
#include <iosfwd>
#include <iterator>
#include <optional>
#include <utility>
#include <vector>
 
#include "dlinear/solver/Bound.h"
 
namespace dlinear {
 
class BoundIterator {
 public:
  using vector_type = std::vector<Bound>;
  using internal_iterator = typename vector_type::const_iterator;
  using iterator_category = std::input_iterator_tag;
  using value_type = typename vector_type::value_type;
  using reference = value_type const &;
  using pointer = value_type const *;
  using difference_type = std::ptrdiff_t;
 
  BoundIterator();
  BoundIterator(internal_iterator begin_bounds_it, internal_iterator end_bounds_it);
  explicit BoundIterator(std::pair<internal_iterator, internal_iterator> bounds);
  BoundIterator(internal_iterator begin_bounds_it, internal_iterator end_bounds_it,
                internal_iterator begin_nq_bounds_it, internal_iterator end_nq_bounds_it);
  BoundIterator(std::pair<internal_iterator, internal_iterator> bounds,
                std::pair<internal_iterator, internal_iterator> nq_bounds);
 
  explicit operator bool() const { return bounds_it_ != end_bounds_it_ || nq_bounds_it_ != end_nq_bounds_it_; }
 
  pointer operator->() const { return bounds_it_ != end_bounds_it_ ? &*bounds_it_ : &*nq_bounds_it_; }
  reference operator*() const { return bounds_it_ != end_bounds_it_ ? *bounds_it_ : *nq_bounds_it_; }
 
  BoundIterator &operator++();
  const BoundIterator operator++(int);
 
  BoundIterator &operator--();
  const BoundIterator operator--(int);
 
  value_type operator[](int i) const;
 
  [[nodiscard]] std::pair<internal_iterator, internal_iterator> bounds() const { return {bounds_it_, end_bounds_it_}; }
  [[nodiscard]] std::pair<internal_iterator, internal_iterator> nq_bounds() const {
    return {nq_bounds_it_, end_nq_bounds_it_};
  }
  [[nodiscard]] inline std::size_t bounds_size() const { return std::distance(bounds_it_, end_bounds_it_); }
  [[nodiscard]] inline std::size_t nq_bounds_size() const { return std::distance(nq_bounds_it_, end_nq_bounds_it_); }
  [[nodiscard]] inline bool bounds_empty() const { return bounds_it_ == end_bounds_it_; }
  [[nodiscard]] inline bool nq_bounds_empty() const { return nq_bounds_it_ == end_nq_bounds_it_; }
  [[nodiscard]] inline bool empty() const { return bounds_empty() && nq_bounds_empty(); }
  [[nodiscard]] inline std::size_t size() const { return bounds_size() + nq_bounds_size(); }
 
  [[nodiscard]] internal_iterator begin() const { return bounds_it_; }
  [[nodiscard]] internal_iterator end() const { return end_nq_bounds_it_; }
 
  [[nodiscard]] LiteralSet explanation() const;
  void explanation(LiteralSet &explanation) const;
  [[nodiscard]] std::set<LiteralSet> explanations(const std::optional<Literal> &lit = {}) const;
  void explanations(std::set<LiteralSet> &explanations, const std::optional<Literal> &lit = {}) const;
 
 private:
  static const vector_type default_empty_vector_;  
 
  const internal_iterator begin_bounds_it_;  
  internal_iterator bounds_it_;              
  const internal_iterator end_bounds_it_;    
 
  const internal_iterator begin_nq_bounds_it_;  
  internal_iterator nq_bounds_it_;              
  const internal_iterator end_nq_bounds_it_;    
};
 
std::ostream &operator<<(std::ostream &os, const BoundIterator &violation);
 
}  // namespace dlinear