condlit.hh

#pragma once
 
#include <clingo/ground/matcher.hh>
#include <clingo/ground/statement.hh>
 
#include <clingo/util/enumerate.hh>
 
namespace CppClingo::Ground {
 
 
enum class LitCondLitType : uint8_t {
    empty = 0,   
    premise = 1, 
    lit = 2,     
};
auto operator<<(std::ostream &out, LitCondLitType type) -> std::ostream &;
 
// NOLINTNEXTLINE(performance-enum-size)
enum class TruthConclusion : uint64_t {
    true_ = 0,   
    false_ = 1,  
    derived = 2, 
    unknown = 3, 
};
 
struct StateCondLitElem {
  public:
    StateCondLitElem(size_t premise, bool premise_is_fact, bool has_conclusion)
        : premise_{premise}, conclusion_truth_{has_conclusion ? TruthConclusion::unknown : TruthConclusion::false_},
          premise_is_fact_{static_cast<uint8_t>(premise_is_fact)} {}
    void set_conclusion(size_t conclusion, bool fact) {
        conclusion_ = conclusion;
        assert(conclusion_truth_ == TruthConclusion::unknown);
        conclusion_truth_ = fact ? TruthConclusion::true_ : TruthConclusion::derived;
    }
    [[nodiscard]] auto is_fact() const -> bool { return conclusion_truth_ == TruthConclusion::true_; }
    [[nodiscard]] auto is_blocked() const -> bool {
        return premise_is_fact_ != 0 &&
               (conclusion_truth_ == TruthConclusion::false_ || conclusion_truth_ == TruthConclusion::unknown);
    }
    [[nodiscard]] auto is_false() const {
        return premise_is_fact_ != 0 && conclusion_truth_ == TruthConclusion::false_;
    }
    [[nodiscard]] auto has_offset() const -> bool { return offset_ > 0; }
    void set_offset(size_t offset) { offset_ = offset + 1; }
    [[nodiscard]] auto offset() const -> size_t { return offset_ - 1; }
 
    [[nodiscard]] auto premise() const -> size_t { return premise_; }
    [[nodiscard]] auto conclusion() const -> std::optional<size_t> {
        return conclusion_ != invalid_offset ? std::make_optional(conclusion_) : std::nullopt;
    }
 
  private:
    size_t conclusion_ = invalid_offset;
    size_t premise_;
    uint64_t offset_ : 61 = 1;
    TruthConclusion conclusion_truth_ : 2;
    uint64_t premise_is_fact_ : 1;
};
 
using MapElemCondLit = Util::ordered_map<Symbol const *, StateCondLitElem, Util::array_hash, Util::array_equal_to>;
 
class StateAtomCondLit {
  public:
    StateAtomCondLit() = default;
    void add_elem(size_t index) { elems_.emplace_back(index); }
    [[nodiscard]] auto enqueue(MapElemCondLit const &elems) -> bool;
    [[nodiscard]] auto propagate(MapElemCondLit const &elems) -> bool;
    [[nodiscard]] auto is_fact(MapElemCondLit const &elems) const -> bool;
    [[nodiscard]] auto is_false() const -> bool { return false_ != 0; }
    [[nodiscard]] auto has_offset() const -> bool { return offset_ > 0; }
    void set_offset(size_t offset) { offset_ = offset + 1; }
    [[nodiscard]] auto offset() const -> size_t { return offset_ - 1; }
 
    [[nodiscard]] auto uid() const -> std::optional<size_t> {
        return uid_ != invalid_offset ? std::make_optional(uid_) : std::nullopt;
    }
    void uid(size_t uid) {
        assert(uid_ == invalid_offset || uid_ == uid);
        uid_ = uid;
    }
    [[nodiscard]] auto elems() const -> std::span<size_t const> { return elems_; }
 
  private:
    std::vector<size_t> elems_;
    uint64_t elems_propagated_ : 61 = 0;
    uint64_t propagated_ : 1 = 0;
    uint64_t enqueued_ : 1 = 0;
    uint64_t false_ : 1 = 0;
    size_t uid_ = invalid_offset;
    size_t offset_ = 0;
};
using MapAtomCondLit = Util::ordered_map<Symbol const *, StateAtomCondLit, Util::array_hash, Util::array_equal_to>;
 
class BaseCondLitEmpty : public BaseImpl<Symbol const *, BaseCondLitEmpty> {
  public:
    BaseCondLitEmpty(MapAtomCondLit &atoms) : atoms_{&atoms} {}
 
    [[nodiscard]] auto index(Key const &key) const -> size_t {
        return std::distance(atoms_->begin(), atoms_->find(key));
    }
    [[nodiscard]] auto size() const -> size_t { return atoms_->size(); }
 
    [[nodiscard]] auto nth(size_t i) const -> MapAtomCondLit::const_iterator { return atoms_->nth(i); }
    [[nodiscard]] auto nth(size_t i) -> MapAtomCondLit::iterator { return atoms_->nth(i); }
 
  private:
    MapAtomCondLit *atoms_;
};
 
class BaseCondLitPremise : public BaseImpl<Symbol const *, BaseCondLitPremise> {
  public:
    using Key = Symbol const *;
 
    BaseCondLitPremise(MapElemCondLit &elems) : elems_{&elems} {}
 
    void add(MapElemCondLit::iterator it) {
        // Note: see note in add_premise
        // assert(it.value().is_blocked());
        it.value().set_offset(base_.size());
        base_.emplace_back(std::distance(elems_->begin(), it));
    }
 
    [[nodiscard]] auto index(Key const &key) const -> size_t {
        if (auto it = elems_->find(key); it != elems_->end() && it->second.has_offset()) {
            return it->second.offset();
        }
        return size();
    }
    [[nodiscard]] auto size() const -> size_t { return base_.size(); }
 
    [[nodiscard]] auto nth(size_t i) const -> MapElemCondLit::const_iterator { return elems_->nth(base_[i]); }
    [[nodiscard]] auto nth(size_t i) -> MapElemCondLit::iterator { return elems_->nth(base_[i]); }
 
  private:
    MapElemCondLit *elems_;
    std::vector<size_t> base_;
};
 
class BaseCondLit : public BaseImpl<Symbol const *, BaseCondLit> {
  public:
    BaseCondLit(MapAtomCondLit &atoms) : atoms_{&atoms} {}
 
    void add(MapAtomCondLit::iterator it) {
        it.value().set_offset(base_.size());
        base_.emplace_back(std::distance(atoms_->begin(), it));
    }
 
    [[nodiscard]] auto index(Key const &key) const -> size_t {
        if (auto it = atoms_->find(key); it != atoms_->end() && it->second.has_offset()) {
            return it->second.offset();
        }
        return size();
    }
    [[nodiscard]] auto size() const -> size_t { return base_.size(); }
 
    [[nodiscard]] auto nth(size_t i) const -> MapAtomCondLit::const_iterator { return atoms_->nth(base_[i]); }
    [[nodiscard]] auto nth(size_t i) -> MapAtomCondLit::iterator { return atoms_->nth(base_[i]); }
 
  private:
    MapAtomCondLit *atoms_;
    std::vector<size_t> base_;
};
 
class StateCondLit : public State {
  public:
    StateCondLit(std::pmr::monotonic_buffer_resource &mbr, VariableVec local, VariableVec global, size_t index,
                 bool has_conclusion, bool sp_premise, bool domain)
        : local_{std::move(local)}, global_{std::move(global)}, mbr_{&mbr},
          atoms_{0, Util::array_hash{global_.size()}, Util::array_equal_to{global_.size()}},
          elems_{0, Util::array_hash{local_.size() + 1}, Util::array_equal_to{local_.size() + 1}}, base_empty_{atoms_},
          base_premise_{elems_}, base_lit_{atoms_}, index_{index}, has_conclusion_{has_conclusion},
          sp_premise_{sp_premise}, domain_{domain} {
        temp_syms_.reserve(std::max(global_.size(), local_.size() + 1));
    }
 
    void vars(VariableSet &res, bool all) const;
 
    [[nodiscard]] auto vars(bool all) const -> VariableSet;
 
    [[nodiscard]] auto vars_global() const -> VariableVec const &;
 
    [[nodiscard]] auto vars_local() const -> VariableVec const &;
 
    [[nodiscard]] auto index() const -> size_t;
 
    auto add_empty(Assignment const &ass) -> std::pair<MapAtomCondLit::iterator, bool>;
 
    auto add_premise(EvalContext const &ctx, ULitVec const &premise) -> bool;
 
    void add_conclusion(Assignment const &ass, MapAtomCondLit::iterator it, size_t conclusion, bool fact);
 
    [[nodiscard]] auto propagate() -> bool;
 
    [[nodiscard]] auto domain() const -> bool;
 
    [[nodiscard]] auto base_empty() -> BaseCondLitEmpty &;
    [[nodiscard]] auto base_premise() -> BaseCondLitPremise &;
    [[nodiscard]] auto base_lit() -> BaseCondLit &;
 
    [[nodiscard]] auto atom_find(Assignment const &ass) -> MapAtomCondLit::iterator;
 
    [[nodiscard]] auto atom_index(Assignment const &ass) -> std::optional<size_t>;
 
    [[nodiscard]] auto atom_index(MapAtomCondLit::const_iterator it) const -> size_t;
 
    [[nodiscard]] auto atom_nth(size_t index) -> MapAtomCondLit::iterator;
 
    [[nodiscard]] auto atom_is_fact(MapAtomCondLit::iterator it) -> bool;
 
    [[nodiscard]] auto elem_find(Assignment const &ass, MapAtomCondLit::iterator it) -> MapElemCondLit::iterator;
 
    [[nodiscard]] auto elem_index(MapElemCondLit::const_iterator it) const -> size_t;
 
    void output(Logger &log, SymbolStore &store, OutputStm &out) override;
 
  private:
    VariableVec local_;
    VariableVec global_;
    std::vector<Symbol> mutable temp_syms_;
    std::pmr::monotonic_buffer_resource *mbr_;
    Symbol *syms_atom_ = nullptr;
    MapAtomCondLit atoms_;
    MapElemCondLit elems_;
    std::vector<size_t> propagate_;
    BaseCondLitEmpty base_empty_;
    BaseCondLitPremise base_premise_;
    BaseCondLit base_lit_;
    size_t index_;
    bool has_conclusion_;
    bool sp_premise_;
    bool domain_;
};
 
class MatchCondLit {
  public:
    using Key = Symbol const *;
 
    MatchCondLit(StateCondLit &state, LitCondLitType type) : state_{&state}, type_{type} {
        eval_.reserve(type_ == LitCondLitType::premise
                          ? std::max(state_->vars_global().size(), state_->vars_local().size() + 1)
                          : state_->vars_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, Symbol const *sym) const -> bool;
 
    [[nodiscard]] auto eval(EvalContext const &ctx) const -> std::optional<Symbol const *>;
 
    friend auto operator<<(std::ostream &out, MatchCondLit const &m) -> std::ostream &;
 
    [[nodiscard]] auto state() const -> StateCondLit &;
    [[nodiscard]] auto type() const -> LitCondLitType;
 
  private:
    [[nodiscard]] static auto match_(Assignment &ass, Symbol const *sym, VariableVec const &vars) -> bool;
 
    std::vector<Symbol> mutable eval_;
    StateCondLit *state_;
    LitCondLitType type_;
};
 
class LitCondLit : public Lit, private MatchCondLit {
  public:
    LitCondLit(LitCondLitType type, StateCondLit &state, size_t index) : MatchCondLit{state, type}, index_{index} {}
 
  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(std::vector<bool> const &bound) const -> double override;
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_output(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 index_;
    size_t offset_ = 0;
};
 
class LitCondLitStrat : public Lit, private InstanceCallback {
  public:
    LitCondLitStrat(StateCondLit &state, ULitVec premise) : state_{&state}, premise_{std::move(premise)} {}
 
  private:
    // lit interface
    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(std::vector<bool> const &bound) const -> double override;
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_output(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;
 
    // cb interface
    void do_init(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;
 
    StateCondLit *state_;
    ULitVec premise_;
};
 
enum class StmCondLitType : uint8_t {
    empty = 0,      
    premise = 1,    
    conclusion = 2, 
};
auto operator<<(std::ostream &out, StmCondLitType type) -> std::ostream &;
 
class StmCondLit : public Stm {
  public:
    StmCondLit(StmCondLitType type, StateCondLit &base, ULitVec body, size_t prio, size_t index)
        : state_{&base}, body_{std::move(body)}, prio_{prio}, index_{index}, type_{type} {}
 
  private:
    // statement interface
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_body() const -> ULitVec const & override;
    [[nodiscard]] auto do_important() const -> VariableSet override;
 
    // solution callback interface
    void do_print_head(std::ostream &out) const override;
    void do_init(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;
 
    StateCondLit *state_;
    ULitVec body_;
    size_t prio_;
    size_t index_;
    StmCondLitType type_;
};
 
 
} // namespace CppClingo::Ground