body_aggregate.hh

#pragma once
 
#include <clingo/ground/literal.hh>
#include <clingo/ground/matcher.hh>
#include <clingo/ground/statement.hh>
 
#include <clingo/util/small_vector.hh>
 
#include <memory_resource>
#include <ostream>
 
namespace CppClingo::Ground {
 
 
enum class AtomBdAggrState : uint8_t {
    unknown = 0, 
    derived = 1, 
    fact = 2,    
};
 
class AtomBdAggr {
  public:
    using Bound = std::variant<std::pair<Number, Number>, std::pair<Symbol, Symbol>>;
 
    AtomBdAggr(AggregateFunction fun) : bound_{init_(fun)} {}
 
    void accumulate(AggregateFunction fun, SymbolSpan tup, bool fact);
 
    auto propagate(GuardVec const &guards, Symbol const *vals) -> std::pair<bool, bool>;
 
    [[nodiscard]] auto derived_idx() const -> size_t;
    void derived_idx(size_t idx);
 
    [[nodiscard]] auto state() const -> AtomBdAggrState;
    void state(AtomBdAggrState state);
 
    auto enqueue() -> bool;
    void dequeue();
 
    void add_elem(size_t idx);
    [[nodiscard]] auto elems() const -> std::span<size_t const>;
    [[nodiscard]] auto todo() -> std::span<size_t const>;
 
    [[nodiscard]] auto uid() const -> std::optional<size_t>;
 
    void uid(size_t uid);
 
  private:
    static auto init_(AggregateFunction fun) -> Bound;
 
    std::vector<size_t> elems_;
    std::variant<std::pair<Number, Number>, std::pair<Symbol, Symbol>> bound_;
    size_t propagated_ = 0;
    size_t derived_idx_ = 0;
    size_t uid_ = invalid_offset;
    AtomBdAggrState state_ = AtomBdAggrState::unknown;
    bool enqueued_ = false;
};
 
class BaseBdAggr : public BaseImpl<Symbol const *, BaseBdAggr> {
  public:
    using BaseImpl::contains;
    using AtomMap = Util::ordered_map<Symbol const *, AtomBdAggr, Util::array_hash, Util::array_equal_to>;
 
    BaseBdAggr(size_t size) : atoms_{0, size, size} {}
 
    auto is_fact(Symbol const *sym) const -> bool;
    void add(AtomMap::iterator it);
 
    [[nodiscard]] auto size() const -> size_t;
 
    auto index(Symbol const *sym) const -> size_t;
    auto nth(size_t i) const -> AtomMap::const_iterator;
    auto nth(size_t i) -> AtomMap::iterator;
 
    [[nodiscard]] auto atoms() -> AtomMap &;
 
  private:
    AtomMap atoms_;
    Util::index_sequence<size_t> derived_;
};
 
// see node in head_aggregate.h
class StmBdAggrElem;
 
class StateBdAggr : public State {
  public:
    class AtomKey;
    class ElementKey {
      private:
        struct priv_tag {};
 
      public:
        ElementKey(priv_tag tag, EvalContext const &ctx, AggregateFunction fun, size_t atom_idx, StmBdAggrElem &elem,
                   bool &res);
        ElementKey(ElementKey const &other) = delete;
        [[nodiscard]] static auto construct(auto &mbr, EvalContext const &ctx, AggregateFunction fun, size_t atom_idx,
                                            StmBdAggrElem &elem) -> bool;
 
        [[nodiscard]] auto span() const -> SymbolSpan;
        [[nodiscard]] auto hash() const -> size_t;
        friend auto operator==(ElementKey const &a, ElementKey const &b) -> bool;
 
      private:
        // Note that these two could be combined to save a little bit of memory.
        size_t n_;
        size_t atom_idx_;
        // NOLINTBEGIN
        CLINGO_IGNORE_ZERO_SIZED_ARRAY_B
        Symbol syms_[0];
        CLINGO_IGNORE_ZERO_SIZED_ARRAY_E
        // NOLINTEND
    };
 
    using AtomMap = BaseBdAggr::AtomMap;
    using ElementMap = Util::ordered_map<ElementKey *, Util::small_vector<size_t>>;
 
    StateBdAggr(std::pmr::monotonic_buffer_resource &mbr, VariableVec global, GuardVec guards, AggregateFunction fun,
                size_t index, bool domain, bool monotone, bool single_pass_elems)
        : base_{global.size()}, global_{std::move(global)}, guards_{std::move(guards)}, mbr_{&mbr}, index_{index},
          fun_{fun}, domain_{domain}, monotone_{monotone}, single_pass_elems_{single_pass_elems} {}
 
    [[nodiscard]] auto global() const -> VariableVec const &;
    [[nodiscard]] auto symbols() -> SymbolVec &;
    [[nodiscard]] auto guards() const -> GuardVec const &;
    [[nodiscard]] auto fun() const -> AggregateFunction;
    [[nodiscard]] auto domain() const -> bool;
    [[nodiscard]] auto monotone() const -> bool;
    [[nodiscard]] auto single_pass_elems() const -> bool;
    [[nodiscard]] auto index() const -> size_t;
 
    auto propagate() -> bool;
 
    auto insert_atom(EvalContext const &ctx) -> std::optional<std::pair<AtomMap::iterator, bool>>;
 
    auto insert_atom(Symbol const *tuple) -> AtomMap::iterator;
 
    void insert_elem(EvalContext const &ctx, AtomMap::iterator it, StmBdAggrElem &elem);
 
    void print(std::ostream &out, bool print_index);
 
    [[nodiscard]] auto base() -> BaseBdAggr &;
 
    void output(Logger &log, SymbolStore &store, OutputStm &out) override;
 
  private:
    void enqueue_(AtomMap::iterator it);
 
    auto atom_index_(AtomMap::iterator it) -> size_t;
 
    BaseBdAggr base_;
    ElementMap tuples_;
    VariableVec global_;
    SymbolVec symbols_;
    GuardVec guards_;
    std::vector<size_t> queue_;
    std::pmr::monotonic_buffer_resource *mbr_;
    AtomKey *atom_key_ = nullptr;
    size_t index_;
    AggregateFunction fun_;
    bool domain_;
    bool monotone_;
    bool single_pass_elems_;
};
 
class MatchBdAggr {
  public:
    using Key = Symbol const *;
 
    MatchBdAggr(StateBdAggr &state) : state_{&state} {
        eval_.reserve(state_->global().size() + state_->guards().size());
    }
 
    [[nodiscard]] auto vars() const -> VariableSet;
 
    [[nodiscard]] auto signature(VariableSet const &bound, [[maybe_unused]] VariableSet const &bind) const
        -> VariableVec;
 
    [[nodiscard]] auto match(EvalContext const &ctx, Symbol const *sym) const -> bool;
 
    [[nodiscard]] auto eval(EvalContext const &ctx) const -> std::optional<Symbol const *>;
 
    friend auto operator<<(std::ostream &out, MatchBdAggr const &m) -> std::ostream &;
 
    [[nodiscard]] auto state() const -> StateBdAggr &;
 
  private:
    std::vector<Symbol> mutable eval_;
    StateBdAggr *state_;
};
 
class LitBdAggr : public Lit, private MatchBdAggr {
  public:
    LitBdAggr(StateBdAggr &state, Sign sign) : MatchBdAggr{state}, sign_{sign} {}
 
  private:
    void do_vars(VariableSet &vars, VarSelectMode mode) const override;
 
    [[nodiscard]] auto do_domain() const -> bool override;
 
    [[nodiscard]] auto do_single_pass() const -> bool override;
 
    [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
                                  std::vector<bool> const &bound)
        -> std::pair<UMatcher, std::optional<size_t>> override;
 
    [[nodiscard]] auto do_score([[maybe_unused]] std::vector<bool> const &bound) const -> double override;
 
    void do_print(std::ostream &out) const override;
 
    auto do_output([[maybe_unused]] EvalContext const &ctx, OutputLit &out) const -> bool override;
 
    [[nodiscard]] auto do_copy() const -> ULit override;
 
    [[nodiscard]] auto do_hash() const -> size_t override;
 
    [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
 
    [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
 
    size_t offset_ = invalid_offset;
    Symbol const *symbol_ = nullptr;
    Sign sign_;
};
 
class StmBdAggrElem : public Stm {
  public:
    StmBdAggrElem(StateBdAggr &state, Location loc_weight, UTermVec tuple, ULitVec body, size_t num_cond,
                  size_t priority)
        : state_{&state}, loc_weight_{std::move(loc_weight)}, tuple_{std::move(tuple)}, body_{std::move(body)},
          num_cond_{num_cond}, priority_{priority} {}
 
    StmBdAggrElem(StmBdAggrElem const &other)
        : state_{other.state_}, loc_weight_{other.loc_weight_}, tuple_{copy_uvec(other.tuple_)},
          body_{copy_uvec(other.body_)}, num_cond_{other.num_cond_}, priority_{other.priority_} {};
    StmBdAggrElem(StmBdAggrElem &&other) noexcept = default;
    auto operator=(StmBdAggrElem const &other) -> StmBdAggrElem & = default;
    auto operator=(StmBdAggrElem &&other) noexcept -> StmBdAggrElem & = default;
 
  private:
    friend class StateBdAggr;
    friend class StateBdAggr::ElementKey;
 
    [[nodiscard]] auto do_body() const -> ULitVec const & override;
    [[nodiscard]] auto do_important() const -> VariableSet override;
    [[nodiscard]] auto do_is_important(size_t index) const -> bool override;
    void do_init([[maybe_unused]] size_t gen) override;
    [[nodiscard]] auto do_report(EvalContext const &ctx) -> bool override;
    void do_propagate(SymbolStore &store, OutputStm &out, Queue &queue) override;
    [[nodiscard]] auto do_priority() const -> size_t override;
    void do_print_head(std::ostream &out) const override;
    void do_print(std::ostream &out) const override;
 
    auto get_cond_(EvalContext const &ctx) -> std::pair<size_t, bool>;
 
    StateBdAggr *state_;
    StateBdAggr::ElementKey *elem_key_ = nullptr;
    Location loc_weight_;
    UTermVec tuple_;
    ULitVec body_;
    size_t num_cond_;
    size_t priority_;
    bool logged_ = false;
};
 
static_assert(std::is_nothrow_move_constructible_v<StmBdAggrElem>);
static_assert(std::is_nothrow_move_assignable_v<StmBdAggrElem>);
static_assert(std::is_copy_assignable_v<StmBdAggrElem>);
 
class LitBdAggrStrat : public Lit {
  public:
    LitBdAggrStrat(StateBdAggr &state, std::vector<StmBdAggrElem> elems, Sign sign)
        : state_{&state}, elems_{std::move(elems)}, sign_{sign} {}
 
  private:
    void do_vars(VariableSet &vars, VarSelectMode mode) const override;
    [[nodiscard]] auto do_domain() const -> bool override;
    [[nodiscard]] auto do_single_pass() const -> bool override;
    [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
                                  std::vector<bool> const &bound)
        -> std::pair<UMatcher, std::optional<size_t>> override;
    [[nodiscard]] auto do_score([[maybe_unused]] std::vector<bool> const &bound) const -> double override;
    void do_print(std::ostream &out) const override;
    auto do_output([[maybe_unused]] EvalContext const &ctx, OutputLit &out) const -> bool override;
    [[nodiscard]] auto do_copy() const -> ULit override;
    [[nodiscard]] auto do_hash() const -> size_t override;
    [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
    [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
 
    StateBdAggr *state_;
    std::vector<StmBdAggrElem> elems_;
    size_t offset_ = invalid_offset;
    Sign sign_;
};
 
 
} // namespace CppClingo::Ground