statement.hh

#pragma once
 
#include <clingo/ground/literal.hh>
 
#include <clingo/ground/instantiator.hh>
 
#include <clingo/core/core.hh>
 
#include <memory_resource>
 
namespace CppClingo::Ground {
 
 
class Stm : public InstanceCallback {
  public:
    [[nodiscard]] auto body() const -> ULitVec const & { return do_body(); }
    [[nodiscard]] auto important() const -> VariableSet { return do_important(); }
 
    friend auto operator<<(std::ostream &out, Stm const &stm) -> std::ostream & {
        stm.do_print(out);
        return out;
    }
 
  private:
    virtual void do_print(std::ostream &out) const = 0;
    [[nodiscard]] virtual auto do_body() const -> ULitVec const & = 0;
    [[nodiscard]] virtual auto do_important() const -> VariableSet = 0;
};
 
using UStm = std::unique_ptr<Stm>;
using UStmVec = std::vector<UStm>;
 
class Linearizer {
  public:
    Linearizer(std::pmr::monotonic_buffer_resource &mbr) : mbr_{&mbr} {}
    void start(Queue &queue);
    void prepare(InstanceCallback &cb, ULitVec const &body, VariableSet important);
 
  private:
    void build_(ULitVec const &lits);
    auto order_(InstanceCallback &cb, std::vector<MatcherType> const &todo, VariableSet const &important,
                ULitVec const &lits) -> std::pair<Instantiator, std::optional<size_t>>;
 
    Queue *iqueue_ = nullptr;
    std::pmr::monotonic_buffer_resource *mbr_;
    std::vector<size_t> rec_;
    std::vector<std::vector<MatcherType>> todos_;
    std::vector<std::tuple<size_t, size_t, double>> queue_;
    std::vector<std::tuple<size_t, std::vector<size_t>, std::vector<size_t>>> lit_map_;
    std::vector<std::vector<size_t>> var_map_;
};
 
enum class RuleType : uint8_t {
    normal, 
    choice  
};
 
class StmRule : public Stm {
  public:
    StmRule(AtomSimple head, ULitVec body, RuleType type)
        : head_{head ? std::move(std::get<0>(*head)) : nullptr}, base_{head ? &std::get<1>(*head) : nullptr},
          indices_{head ? std::move(std::get<2>(*head)) : std::vector<size_t>{}}, body_{std::move(body)}, type_{type} {
        init_();
    }
 
  private:
    void init_();
 
    // Stm interface
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_body() const -> ULitVec const & override;
    [[nodiscard]] auto do_important() const -> VariableSet override;
 
    // InstanceCallback 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 { return std::numeric_limits<size_t>::max(); }
 
    UTerm head_;
    AtomBase *base_;
    std::vector<size_t> indices_;
    ULitVec body_;
    Symbol atom_ = SymbolStore::sup();
    RuleType type_;
};
 
class StmExternal : public Stm {
  public:
    StmExternal(Ground::UTerm atom, AtomBase &base, std::vector<size_t> indices, ULitVec body,
                std::optional<std::pair<Location, UTerm>> type)
        : type_{std::move(type)}, atom_{std::move(atom)}, base_{&base}, indices_{std::move(indices)},
          body_{std::move(body)} {
        init_();
    }
 
  private:
    void init_();
 
    // Stm interface
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_body() const -> ULitVec const & override;
    [[nodiscard]] auto do_important() const -> VariableSet override;
 
    // InstanceCallback 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 { return std::numeric_limits<size_t>::max(); }
    [[nodiscard]] auto do_is_important([[maybe_unused]] size_t index) const -> bool override { return false; }
 
    std::optional<std::pair<Location, UTerm>> type_;
    UTerm atom_;
    AtomBase *base_;
    std::vector<size_t> indices_;
    ULitVec body_;
    Symbol res_atom_ = SymbolStore::sup();
    ExternalType res_type_ = ExternalType::free;
};
 
class StmWeakConstraint : public Stm {
  public:
    StmWeakConstraint(Location loc_weight, UTerm weight, std::optional<std::pair<Location, UTerm>> prio, UTermVec terms,
                      ULitVec body)
        : loc_weight_{std::move(loc_weight)}, loc_prio_{prio ? std::move(prio->first) : loc_weight_},
          weight_{std::move(weight)}, prio_{prio ? std::move(prio->second) : nullptr}, terms_{std::move(terms)},
          body_{std::move(body)} {
        init_();
    }
 
  private:
    void init_();
    // Stm interface
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_body() const -> ULitVec const & override;
    [[nodiscard]] auto do_important() const -> VariableSet override;
 
    // InstanceCallback 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 { return std::numeric_limits<size_t>::max(); }
 
    Location loc_weight_;
    Location loc_prio_;
    UTerm weight_;
    UTerm prio_;
    UTermVec terms_;
    ULitVec body_;
    Symbol res_weight_;
    std::optional<Symbol> res_prio_;
    SymbolVec res_terms_;
};
 
class StmHeuristic : public Stm {
  public:
    StmHeuristic(UTerm atom, AtomBase &base, ULitVec body, Location loc_weight, UTerm weight,
                 std::optional<std::pair<Location, UTerm>> prio, Location loc_type, UTerm type)
        : loc_weight_{std::move(loc_weight)}, loc_prio_{prio ? std::move(prio->first) : loc_weight_},
          loc_type_{std::move(loc_type)}, atom_{std::move(atom)}, base_{&base}, weight_{std::move(weight)},
          prio_{prio ? std::move(prio->second) : nullptr}, type_{std::move(type)}, body_{std::move(body)} {
        init_();
    }
 
  private:
    void init_();
    // Stm interface
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_body() const -> ULitVec const & override;
    [[nodiscard]] auto do_important() const -> VariableSet override;
 
    // InstanceCallback 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 { return std::numeric_limits<size_t>::max(); }
 
    Location loc_weight_;
    Location loc_prio_;
    Location loc_type_;
    UTerm atom_;
    AtomBase *base_;
    UTerm weight_;
    UTerm prio_;
    UTerm type_;
    ULitVec body_;
    size_t offset_ = 0;
    Symbol res_weight_;
    Symbol res_prio_;
    HeuristicType res_type_ = HeuristicType::level;
};
 
class StmEdge : public Stm {
  public:
    StmEdge(UTerm src, UTerm dst, ULitVec body) : src_{std::move(src)}, dst_{std::move(dst)}, body_{std::move(body)} {
        init_();
    }
 
  private:
    void init_();
    // Stm interface
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_body() const -> ULitVec const & override;
    [[nodiscard]] auto do_important() const -> VariableSet override;
 
    // InstanceCallback 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 { return std::numeric_limits<size_t>::max(); }
 
    UTerm src_;
    UTerm dst_;
    ULitVec body_;
    Symbol res_src_;
    Symbol res_dst_;
};
 
class StmShow : public Stm {
  public:
    StmShow(UTerm term, ULitVec body) : term_{std::move(term)}, body_{std::move(body)} { init_(); }
 
  private:
    void init_();
    // Stm interface
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_body() const -> ULitVec const & override;
    [[nodiscard]] auto do_important() const -> VariableSet override;
 
    // InstanceCallback 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 { return std::numeric_limits<size_t>::max(); }
 
    UTerm term_;
    ULitVec body_;
    Symbol res_term_;
};
 
class StmProject : public Stm {
  public:
    StmProject(UTerm atom, AtomBase &base, ULitVec body)
        : atom_{std::move(atom)}, base_{&base}, body_{std::move(body)} {
        init_();
    }
 
  private:
    void init_();
    // Stm interface
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_body() const -> ULitVec const & override;
    [[nodiscard]] auto do_important() const -> VariableSet override;
 
    // InstanceCallback 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 { return std::numeric_limits<size_t>::max(); }
    [[nodiscard]] auto do_is_important([[maybe_unused]] size_t index) const -> bool override { return false; }
 
    UTerm atom_;
    AtomBase *base_;
    ULitVec body_;
    size_t offset_ = 0;
};
 
 
} // namespace CppClingo::Ground