sort.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 <map>
#include <memory_resource>
 
namespace CppClingo::Ground {
 
 
class AtomSortAggr {
  public:
    struct ValueState {
        bool fact;       
        bool propagated; 
    };
    using Values = std::map<Symbol, ValueState>;
    using Pairs = std::vector<Symbol>;
    using Elems = Util::small_vector<size_t>;
 
    AtomSortAggr() = default;
 
    void accumulate(Symbol sym, bool fact);
 
    [[nodiscard]] auto is_fact(Symbol sym) const -> bool;
    [[nodiscard]] auto todo_values(SymbolStore &store) -> std::span<Symbol const>;
 
    void add_elem(size_t idx);
    [[nodiscard]] auto elems() const -> std::span<size_t const>;
    [[nodiscard]] auto enqueue() -> bool;
    void dequeue();
    [[nodiscard]] auto todo_elems() -> std::span<size_t const>;
 
  private:
    [[nodiscard]] auto num_values_() const -> size_t;
 
    Elems elems_;
    Values values_;
    Pairs pairs_;
    ptrdiff_t propagated_pairs_ = 0;
    ptrdiff_t propagated_elems_ = 0;
    bool dirty_ = false;
    bool fact_ = true;
    bool enqueued_ = false;
};
 
class BaseSortAggr : public BaseImpl<std::pair<size_t, Symbol>, BaseSortAggr> {
  public:
    using BaseImpl::contains;
    using BaseImpl::Key;
    using AtomMap = Util::ordered_map<Symbol const *, AtomSortAggr, Util::array_hash, Util::array_equal_to>;
    using AtomSet = Util::ordered_map<Key, size_t>;
 
    BaseSortAggr(size_t size, bool domain_elems, bool single_pass_elems)
        : atoms_{0, size, size}, domain_elems_{domain_elems}, single_pass_elems_{single_pass_elems} {}
 
    [[nodiscard]] auto is_fact(Key sym) const -> bool;
    auto add(size_t idx, Symbol val) -> bool;
 
    [[nodiscard]] auto size() const -> size_t;
 
    [[nodiscard]] auto index(Key sym) const -> size_t;
    [[nodiscard]] auto nth(size_t i) const -> AtomSet::const_iterator;
    auto nth(size_t i) -> AtomSet::iterator;
 
    [[nodiscard]] auto atoms() -> AtomMap &;
    [[nodiscard]] auto derived() -> AtomSet &;
 
    [[nodiscard]] auto domain_elems() const -> bool;
    [[nodiscard]] auto single_pass_elems() const -> bool;
 
  private:
    AtomMap atoms_;
    AtomSet derived_;
    bool domain_elems_;
    bool single_pass_elems_;
};
 
class StmSortAggrElem;
 
class StateSortAggr : public State {
  public:
    class AtomKey;
    using ElementKey = std::pair<size_t, Symbol>;
 
    using AtomMap = BaseSortAggr::AtomMap;
    using ElementMap = Util::ordered_map<ElementKey, Util::small_vector<size_t>>;
 
    StateSortAggr(std::pmr::monotonic_buffer_resource &mbr, VariableVec global, UTerm term, size_t index,
                  bool domain_elems, bool single_pass_elems)
        : base_{global.size(), domain_elems, single_pass_elems}, global_{std::move(global)}, term_{std::move(term)},
          mbr_{&mbr}, index_{index} {}
 
    [[nodiscard]] auto global() const -> VariableVec const &;
    [[nodiscard]] auto symbols() -> SymbolVec &;
    [[nodiscard]] auto term() const -> Term const &;
    [[nodiscard]] auto domain_elems() const -> bool;
    [[nodiscard]] auto single_pass_elems() const -> bool;
    [[nodiscard]] auto index() const -> size_t;
 
    auto propagate(SymbolStore &store) -> bool;
 
    auto insert_atom(EvalContext const &ctx) -> std::pair<AtomMap::iterator, bool>;
 
    void insert_elem(EvalContext const &ctx, AtomMap::iterator it, StmSortAggrElem &elem);
 
    auto atom_index(AtomMap::iterator it) -> size_t;
 
    void print(std::ostream &out, bool print_index);
 
    [[nodiscard]] auto base() -> BaseSortAggr &;
 
    void output(Logger &log, SymbolStore &store, OutputStm &out) override;
 
  private:
    void enqueue_(AtomMap::iterator it);
 
    BaseSortAggr base_;
    ElementMap tuples_;
    VariableVec global_;
    SymbolVec symbols_;
    UTerm term_;
    std::vector<size_t> queue_;
    std::pmr::monotonic_buffer_resource *mbr_;
    AtomKey *atom_key_ = nullptr;
    size_t index_;
};
 
class MatchSortAggr {
  public:
    using Key = BaseSortAggr::Key;
 
    MatchSortAggr(StateSortAggr &state) : state_{&state} { eval_.reserve(state_->global().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, Key key) const -> bool;
 
    [[nodiscard]] auto eval(EvalContext const &ctx) const -> std::optional<Key>;
 
    friend auto operator<<(std::ostream &out, MatchSortAggr const &m) -> std::ostream &;
 
    [[nodiscard]] auto state() const -> StateSortAggr &;
 
  private:
    std::vector<Symbol> mutable eval_;
    StateSortAggr *state_;
};
 
class LitSortAggr : public Lit, private MatchSortAggr {
  public:
    LitSortAggr(StateSortAggr &state) : MatchSortAggr{state} {}
 
  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, [[maybe_unused]] double estimate) const
        -> double override;
    [[nodiscard]] auto do_domain_size(EstimateSelector sel) const -> std::optional<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;
};
 
class StmSortAggrElem : public Stm {
  public:
    StmSortAggrElem(StateSortAggr &state, Location loc_weight, UTermVec tuple, ULitVec body, size_t num_cond,
                    size_t priority, ProfileNodeInternal *node)
        : state_{&state}, loc_weight_{std::move(loc_weight)}, tuple_{std::move(tuple)}, body_{std::move(body)},
          node_{node}, num_cond_{num_cond}, priority_{priority} {}
 
    StmSortAggrElem(StmSortAggrElem const &other)
        : state_{other.state_}, loc_weight_{other.loc_weight_}, tuple_{copy_uvec(other.tuple_)},
          body_{copy_uvec(other.body_)}, node_{other.node_}, num_cond_{other.num_cond_}, priority_{other.priority_} {};
    StmSortAggrElem(StmSortAggrElem &&other) noexcept = default;
    auto operator=(StmSortAggrElem const &other) -> StmSortAggrElem & = default;
    auto operator=(StmSortAggrElem &&other) noexcept -> StmSortAggrElem & = default;
 
  private:
    friend class StateSortAggr;
 
    [[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;
    [[nodiscard]] auto do_profile_node() const -> ProfileNodeInternal * override { return node_; }
 
    auto get_cond_(EvalContext const &ctx) -> std::pair<size_t, bool>;
 
    StateSortAggr *state_;
    Location loc_weight_;
    UTermVec tuple_;
    ULitVec body_;
    ProfileNodeInternal *node_;
    size_t num_cond_;
    size_t priority_;
};
 
static_assert(std::is_nothrow_move_constructible_v<StmSortAggrElem>);
static_assert(std::is_nothrow_move_assignable_v<StmSortAggrElem>);
static_assert(std::is_copy_assignable_v<StmSortAggrElem>);
 
class LitSortAggrStrat : public Lit, private MatchSortAggr {
  public:
    LitSortAggrStrat(StateSortAggr &state, std::vector<StmSortAggrElem> elems)
        : MatchSortAggr{state}, elems_{std::move(elems)} {}
 
  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, [[maybe_unused]] double estimate) const
        -> double override;
 
    [[nodiscard]] auto do_domain_size(EstimateSelector sel) const -> std::optional<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;
 
    std::vector<StmSortAggrElem> elems_;
    size_t offset_ = invalid_offset;
};
 
 
} // namespace CppClingo::Ground