instantiator.hh

#pragma once
 
#include <clingo/ground/profile.hh>
 
#include <clingo/core/logger.hh>
#include <clingo/core/output.hh>
#include <clingo/core/symbol.hh>
 
#include <clingo/util/sync.hh>
 
#include <memory>
#include <utility>
#include <vector>
 
namespace CppClingo::Ground {
 
 
class Instantiator;
 
class InstantiationContext {
  public:
    InstantiationContext(Logger &log, SymbolStore &store, OutputStm &out) : log_{&log}, store_{&store}, out_{&out} {}
    [[nodiscard]] auto log() const -> Logger & { return *log_; }
    [[nodiscard]] auto store() const -> SymbolStore & { return *store_; }
    [[nodiscard]] auto out() const -> OutputStm & { return *out_; }
 
  private:
    Logger *log_;
    SymbolStore *store_;
    OutputStm *out_;
};
 
class EvalContext : public InstantiationContext {
  public:
    EvalContext(Logger &log, SymbolStore &store, OutputStm &out, Assignment &ass)
        : InstantiationContext{log, store, out}, ass_{&ass} {}
    [[nodiscard]] auto ass() const -> Assignment & { return *ass_; }
 
  private:
    Assignment *ass_;
};
 
enum class MatcherType : uint8_t {
    new_atoms, 
    old_atoms, 
    all_atoms  
};
 
inline auto operator<<(std::ostream &out, MatcherType type) -> std::ostream & {
    switch (type) {
        case MatcherType::all_atoms: {
            out << "a";
            break;
        }
        case MatcherType::old_atoms: {
            out << "o";
            break;
        }
        case MatcherType::new_atoms: {
            out << "n";
            break;
        }
    }
    return out;
}
 
class Matcher {
  public:
    virtual ~Matcher() = default;
    void init(InstantiationContext const &ctx, size_t gen) { do_init(ctx, gen); }
    void match(EvalContext const &ctx) { do_match(ctx); }
    [[nodiscard]] auto next(EvalContext const &ctx) -> bool { return do_next(ctx); }
    void print(std::ostream &out) const { do_print(out); }
    [[nodiscard]] auto type() const -> MatcherType { return do_type(); }
 
  private:
    virtual void do_init(InstantiationContext const &ctx, size_t gen) = 0;
    virtual void do_match(EvalContext const &ctx) = 0;
    [[nodiscard]] virtual auto do_next(EvalContext const &ctx) -> bool = 0;
    virtual void do_print(std::ostream &out) const = 0;
    [[nodiscard]] virtual auto do_type() const -> MatcherType { return MatcherType::all_atoms; }
};
using UMatcher = std::unique_ptr<Matcher>;
using UMatcherVec = std::vector<UMatcher>;
 
class Queue;
 
class InstanceCallback {
  public:
    virtual ~InstanceCallback() = default;
    void init(size_t gen) { do_init(gen); }
    [[nodiscard]] auto report(EvalContext const &ctx) -> bool { return do_report(ctx); }
    void propagate(SymbolStore &store, OutputStm &out, Queue &queue) { do_propagate(store, out, queue); }
    [[nodiscard]] auto priority() const -> size_t { return do_priority(); }
    void print_head(std::ostream &out) const { do_print_head(out); }
    [[nodiscard]] auto is_important(size_t index) const -> bool { return do_is_important(index); }
    [[nodiscard]] auto profile_node() const -> ProfileNodeInternal * { return do_profile_node(); }
 
  private:
    virtual void do_init(size_t gen) = 0;
    [[nodiscard]] virtual auto do_report(EvalContext const &ctx) -> bool = 0;
    virtual void do_propagate(SymbolStore &store, OutputStm &out, Queue &queue) = 0;
    [[nodiscard]] virtual auto do_priority() const -> size_t = 0;
    virtual void do_print_head(std::ostream &out) const = 0;
    [[nodiscard]] virtual auto do_is_important([[maybe_unused]] size_t index) const -> bool { return true; }
    [[nodiscard]] virtual auto do_profile_node() const -> ProfileNodeInternal * = 0;
};
 
class Instantiator {
  public:
    using DependVec = std::vector<size_t>;
    Instantiator(InstanceCallback &icb, size_t vars, size_t n) : icb_{&icb}, stats_{profile_node_(icb)}, ass_{vars} {
        matchers_.reserve(n + 1);
    }
    void init(InstantiationContext const &ctx, size_t gen);
    void add(UMatcher matcher, DependVec depends);
    void finalize(DependVec depends);
    [[nodiscard]] auto enqueue() -> bool;
    [[nodiscard]] auto instantiate(Logger &log, SymbolStore &store, OutputStm &out, Util::StopFlag *stop)
        -> GroundResult;
    void propagate(SymbolStore &store, OutputStm &out, Queue &queue);
    void print(std::ostream &out) const;
    [[nodiscard]] auto priority() const { return icb_->priority(); }
 
    friend auto operator<<(std::ostream &out, Instantiator const &inst) -> std::ostream & {
        inst.print(out);
        return out;
    }
 
  private:
    static auto profile_node_(InstanceCallback const &icb) -> ProfileStats * {
        auto *node = icb.profile_node();
        return node != nullptr ? &node->add_child(std::make_unique<ProfileData>()).step_ : nullptr;
    }
    class BackjumpMatcher {
      public:
        BackjumpMatcher(UMatcher matcher, DependVec depend)
            : matcher_{std::move(matcher)}, depend_{std::move(depend)} {}
        void init(InstantiationContext const &ctx, size_t gen);
        void match(EvalContext const &ctx);
        auto next(EvalContext const &ctx) -> bool;
        auto first(EvalContext const &ctx) -> bool;
        void print(std::ostream &out, size_t index) const;
        [[nodiscard]] auto depend() const -> DependVec const &;
        [[nodiscard]] auto backjumpable() const -> bool;
        void block();
 
      private:
        UMatcher matcher_;
        std::vector<size_t> depend_;
        bool backjumpable_ = true;
    };
    InstanceCallback *icb_;
    ProfileStats *stats_;
    Assignment ass_;
    std::vector<BackjumpMatcher> matchers_;
    bool enqueued_ = false;
};
 
using InstantiatorVec = std::vector<Instantiator>;
 
class Queue {
  public:
    Queue(Util::StopFlag *stop = nullptr) : stop_{stop} {}
    void insert(Instantiator inst, std::optional<size_t> index);
    void propagate(size_t index);
    [[nodiscard]] auto process(Logger &log, SymbolStore &store, OutputStm &out) -> GroundResult;
    auto release() -> std::vector<Instantiator> { return std::move(insts_); }
 
  private:
    void enter_(size_t i);
 
    std::vector<Instantiator> insts_;
    std::vector<std::vector<size_t>> update_;
    std::vector<std::vector<Instantiator *>> queues_;
    size_t size_ = 0;
    size_t max_prio_ = 0;
    Util::StopFlag *stop_;
};
 
 
} // namespace CppClingo::Ground