base.hh

#pragma once
 
#include <clingo/ground/instantiator.hh>
#include <clingo/ground/term.hh>
 
#include <clingo/core/symbol.hh>
 
#include <clingo/util/index_sequence.hh>
#include <clingo/util/ordered_map.hh>
#include <clingo/util/ordered_set.hh>
#include <clingo/util/small_vector.hh>
 
namespace CppClingo::Ground {
 
 
using VariableSet = Util::ordered_set<size_t>;
using VariableVec = VariableSet::values_container_type;
 
// NOLINTNEXTLINE(performance-enum-size)
enum class StateAtom : uint64_t {
    fact = 0,
    derived = 1,
    unknown = 2,
};
 
struct AtomInfo {
    uint64_t id : 62;    
    StateAtom state : 2; 
};
 
static_assert(sizeof(AtomInfo) == sizeof(uint64_t));
 
using SymbolicAtom = std::pair<Symbol, AtomInfo>;
 
enum class AtomUpdate : uint8_t {
    added = 0,     
    changed = 1,   
    unchanged = 2, 
};
 
class GenerationCounts {
  public:
 
    [[nodiscard]] auto begin(MatcherType type) const -> size_t {
        if (type == MatcherType::new_atoms) {
            return old_offset_;
        }
        return 0;
    }
 
    [[nodiscard]] auto end(MatcherType type) const -> size_t {
        if (type == MatcherType::old_atoms) {
            return old_offset_;
        }
        return all_offset_;
    }
 
    [[nodiscard]] auto contains(size_t index, MatcherType type) const -> bool {
        return begin(type) <= index && index < end(type);
    }
 
    [[nodiscard]] auto has_update(size_t size) const -> bool { return all_offset_ < size; }
 
    void update(size_t generation, size_t size) {
        // initialize the domain
        // (all atoms are marked as new)
        if (generation == 0) {
            generation_ = 0;
            old_offset_ = 0;
            all_offset_ = size;
        }
        // the generation has been incremented by one
        // (freshly added atoms are marked new)
        else if (generation_ + 1 == generation) {
            generation_ = generation;
            old_offset_ = all_offset_;
            all_offset_ = size;
            // the generation has been incremented by more than one
            // (all atoms are marked old)
        } else if (generation_ + 1 < generation) {
            generation_ = generation;
            old_offset_ = size;
            all_offset_ = size;
        }
    }
 
  private:
    size_t old_offset_ = 0;
    size_t all_offset_ = 0;
    size_t generation_ = 0;
};
 
class BaseContext {
  public:
    virtual ~BaseContext() = default;
};
 
template <class KeyType, class BaseType> class BaseImpl {
  public:
    using Key = KeyType;
 
    [[nodiscard]] auto begin(MatcherType type) const -> size_t { return counts_.begin(type); }
 
    [[nodiscard]] auto end(MatcherType type) const -> size_t { return counts_.end(type); }
 
    [[nodiscard]] auto contains(Key const &sym, MatcherType type) const -> std::optional<size_t> {
        if (auto idx = base().index(sym); counts_.contains(idx, type)) {
            return idx;
        }
        return std::nullopt;
    }
 
    void update(size_t generation) { counts_.update(generation, base().size()); }
 
    void ensure(size_t generation) { update(generation > 0 ? generation - 1 : 0); }
 
    template <class T> auto context() -> T & {
        if (context_ != nullptr) {
            if (auto res = dynamic_cast<T *>(context_.get()); res != nullptr) {
                return *res;
            }
            throw std::bad_cast();
        }
        context_ = std::make_unique<T>();
        return static_cast<T &>(*context_);
    }
 
    void clear_context() { context_ = nullptr; }
 
    [[nodiscard]] auto has_update() const -> bool { return counts_.has_update(base().size()); }
 
  private:
    friend BaseType;
    BaseImpl() = default;
 
    [[nodiscard]] auto base() -> BaseType & { return *static_cast<BaseType *>(this); }
    [[nodiscard]] auto base() const -> BaseType const & { return *static_cast<BaseType const *>(this); }
 
    GenerationCounts counts_;
    std::unique_ptr<BaseContext> context_;
};
 
class AtomBase : public BaseImpl<Symbol, AtomBase> {
  public:
    using MapAtom = Util::ordered_map<Symbol, AtomInfo>;
 
    [[nodiscard]] auto domain() const {
        for (auto n = derived_.size(); domain_offset_ < n; ++domain_offset_) {
            if (atoms_.nth(derived_[domain_offset_])->second.state != StateAtom::fact) {
                return false;
            }
        }
        return true;
    }
    auto is_fact(Symbol sym) const -> bool {
        auto it = atoms_.find(sym);
        return it != atoms_.end() && it->second.state == StateAtom::fact;
    }
 
    [[nodiscard]] auto find(Symbol const &sym) -> std::optional<MapAtom::iterator> {
        auto it = atoms_.find(sym);
        if (it != atoms_.end() && it->second.state != StateAtom::unknown) {
            return it;
        }
        return std::nullopt;
    }
 
    template <class Gen> auto add(Symbol atom, StateAtom state, Gen &&gen) -> std::pair<MapAtom::iterator, AtomUpdate> {
        auto [it, ins] = atoms_.try_emplace(atom, 0, state);
        if (ins) {
            it.value().id = std::invoke(std::forward<Gen>(gen));
            if (state != StateAtom::unknown) {
                derived_.add(atom_index_(it));
            }
            return {it, AtomUpdate::added};
        }
        auto &prev = it.value();
        if (state < prev.state) {
            if (prev.state == StateAtom::unknown) {
                prev.state = state;
                derived_.add(atom_index_(it));
                return {it, AtomUpdate::added};
            }
            prev.state = state;
            return {it, AtomUpdate::changed};
        }
        return {it, AtomUpdate::unchanged};
    }
 
    [[nodiscard]] auto size() const -> size_t { return derived_.size(); }
    [[nodiscard]] auto num_shown() const -> size_t { return show_offset_; }
 
    auto index(Symbol const &sym) const -> size_t {
        if (auto it = atoms_.find(sym); it != atoms_.end() && it->second.state != StateAtom::unknown) {
            return derived_.find(atom_index_(it));
        }
        return size();
    }
    auto nth(size_t i) const -> MapAtom::const_iterator { return atoms_.nth(derived_[i]); }
    auto nth(size_t i) -> MapAtom::iterator { return atoms_.nth(derived_[i]); }
 
    void mark(SymbolCollector &gc) {
        clear_context();
        for (auto const &[sym, atom] : atoms_) {
            gc.mark(sym);
        }
    }
 
    [[nodiscard]] auto mark_shown() -> size_t { return std::exchange(show_offset_, size()); }
 
    [[nodiscard]] auto mark_negated() -> size_t { return std::exchange(negate_offset_, size()); }
 
    [[nodiscard]] auto mark_projected() -> size_t { return std::exchange(project_offset_, size()); }
 
    template <class Pred> void simplify(Pred const &pred, size_t &rem, size_t &fact) {
        // NOTE: the show offset can be zero for auxiliary domains
        assert(show_offset_ == 0 || show_offset_ == size());
        assert(negate_offset_ == 0 || negate_offset_ == size());
        assert(project_offset_ == 0 || project_offset_ == size());
        auto true_atoms = SymbolVec{};
        erase_if(atoms_, [&](SymbolicAtom const &item) {
            if (item.second.state == StateAtom::unknown) {
                ++rem;
                return true;
            }
            auto tv = pred(item.second.id);
            if (tv == TruthValue::bot) {
                ++rem;
                return true;
            }
            if (tv == TruthValue::top && item.second.state != StateAtom::fact) {
                ++fact;
                true_atoms.emplace_back(item.first);
            }
            return false;
        });
        for (auto const &sym : true_atoms) {
            atoms_.find(sym).value().state = StateAtom::fact;
        }
        derived_.assign(0, atoms_.size());
        assert(derived_.size() == atoms_.size());
        domain_offset_ = 0;
        show_offset_ = show_offset_ > 0 ? size() : 0;
        negate_offset_ = negate_offset_ > 0 ? size() : 0;
        project_offset_ = project_offset_ > 0 ? size() : 0;
    }
 
  private:
    [[nodiscard]] auto atom_index_(MapAtom::const_iterator it) const -> size_t {
        return static_cast<size_t>(std::distance(atoms_.cbegin(), it));
    }
 
    MapAtom atoms_;
    Util::index_sequence<size_t> derived_;
    size_t mutable domain_offset_ = 0;
    size_t show_offset_ = 0;
    size_t negate_offset_ = 0;
    size_t project_offset_ = 0;
};
 
using UAtomBase = std::unique_ptr<AtomBase>;
 
class ProjectState {
  public:
    ProjectState(String name, size_t vars, AtomBase &base, UTerm p_head, UTerm p_body)
        : name_{name}, base_{&base}, p_head_{std::move(p_head)}, p_body_{std::move(p_body)} {
        ass_.resize(vars);
    }
    [[nodiscard]] auto base() const -> AtomBase & { return *base_; }
    [[nodiscard]] auto p_base() -> AtomBase & { return p_base_; }
    [[nodiscard]] auto name() const -> String const & { return *name_; }
    void init(InstantiationContext const &ctx, size_t gen);
 
  private:
    SharedString name_;
    AtomBase *base_;
    AtomBase p_base_;
    UTerm p_head_;
    UTerm p_body_;
    Assignment ass_;
    size_t imported_ = 0;
};
using UProjectState = std::unique_ptr<ProjectState>;
 
using ProjectMap = Util::ordered_map<Ground::UTerm, UProjectState>;
 
using BaseMap = Util::ordered_map<std::tuple<String, size_t, bool>, UAtomBase>;
 
class Bases {
  public:
    [[nodiscard]] auto add_base(std::tuple<String, size_t, bool> sig) -> Ground::AtomBase &;
 
    [[nodiscard]] auto get_base(std::tuple<String, size_t, bool> sig) const -> Ground::AtomBase *;
 
    [[nodiscard]] auto add_project(SymbolStore &store, Ground::UTerm const &term, Ground::AtomBase &base)
        -> std::pair<Ground::UTerm, ProjectState *>;
 
    [[nodiscard]] auto atoms() const -> BaseMap const & { return atoms_; }
    [[nodiscard]] auto projected() const -> ProjectMap const & { return projected_; }
 
    void clear_aux();
 
  private:
    BaseMap atoms_;
    BaseMap aux_;
    ProjectMap projected_;
};
 
class State {
  public:
    virtual ~State() = default;
    virtual void output(Logger &log, SymbolStore &store, OutputStm &out) = 0;
};
using UState = std::unique_ptr<State>;
using UStateVec = std::vector<UState>;
 
 
} // namespace CppClingo::Ground