guard_seq.h

Go to the documentation of this file.

#ifndef IREP2_GUARD_SEQ_H_
#define IREP2_GUARD_SEQ_H_
 
#include <cstddef>
#include <immer/vector.hpp>
#include <immer/memory_policy.hpp>
#include <irep2/irep2_expr.h>

class guard_seq
{
  using memory_policy = immer::memory_policy<
    immer::default_heap_policy,
    immer::unsafe_refcount_policy,
    immer::no_lock_policy>;
  using vector_t = immer::vector<expr2tc, memory_policy>;
 
  vector_t v_;
 
  explicit guard_seq(vector_t v) : v_(std::move(v))
  {
  }
 
public:
  guard_seq() = default;
 
  std::size_t size() const
  {
    return v_.size();
  }
  bool empty() const
  {
    return v_.empty();
  }
 
  // Reference-returning into immer storage. The reference is valid only
  // until the next push_back()/clear() replaces the root — callers must not
  // stash an element reference across a guard mutation. (Value-returning was
  // measured at ~2x symex: an expr2tc copy is an atomic refcount bump, and
  // the -=/|=/build_guard_expr/== loops access elements O(N) times per merge,
  // so the per-access copy dominates.) All internal call sites read the
  // reference before any mutation; this is the documented precondition.
  const expr2tc &operator[](std::size_t i) const
  {
    return v_[i];
  }
  const expr2tc &front() const
  {
    return v_.front();
  }
  const expr2tc &back() const
  {
    return v_.back();
  }
 
  void push_back(const expr2tc &e)
  {
    v_ = std::move(v_).push_back(e);
  }

  guard_seq prefix(std::size_t n) const
  {
    return guard_seq(v_.take(n));
  }

  guard_seq suffix(std::size_t n) const
  {
    vector_t r;
    for (std::size_t i = n; i < v_.size(); ++i)
      r = std::move(r).push_back(v_[i]);
    return guard_seq(std::move(r));
  }
 
  void clear()
  {
    v_ = vector_t{};
  }
 
  using const_iterator = vector_t::const_iterator;
  const_iterator begin() const
  {
    return v_.begin();
  }
  const_iterator end() const
  {
    return v_.end();
  }
 
  bool operator==(const guard_seq &o) const
  {
    return v_ == o.v_;
  }
  bool operator!=(const guard_seq &o) const
  {
    return v_ != o.v_;
  }
};
 
#endif /* IREP2_GUARD_SEQ_H_ */