backend.hh

#include <clingo/core/backend.hh>
#include <clingo/core/output.hh>
 
#include <clingo/util/checked_math.hh>
#include <clingo/util/enum.hh>
#include <clingo/util/graph.hh>
#include <clingo/util/interval_set.hh>
#include <clingo/util/ordered_map.hh>
#include <clingo/util/unordered_map.hh>
 
namespace CppClingo::Output {
 
 
class TheoryData {
  public:
    using IdVec = Util::small_vector<prg_id_t, 4>;
    using LitVec = Util::small_vector<prg_lit_t, 4>;
 
    TheoryData(SymbolStore &store, UTheoryBackend backend) : store_{&store}, backend_{std::move(backend)} {}
 
    auto num(prg_weight_t num) -> prg_id_t;
 
    auto str(String str) -> prg_id_t;
 
    auto fun(prg_id_t name, IdVec args) -> prg_id_t;
    auto fun(String name, IdVec args) -> prg_id_t { return fun(str(name), std::move(args)); }
 
    auto fun(String name, PrgIdSpan args) -> prg_id_t { return fun(str(name), IdVec{args.begin(), args.end()}); }
 
    auto tup(TheoryTermTupleType type, IdVec args) -> prg_id_t;
 
    auto tup(TheoryTermTupleType type, PrgIdSpan args) -> prg_id_t {
        return tup(type, IdVec{args.begin(), args.end()});
    }
 
    auto sym(Symbol sym) -> prg_id_t;
 
    auto elem(IdVec tuple, LitVec cond) -> prg_id_t;
 
    auto elem(PrgIdSpan tuple, PrgLitSpan cond) -> prg_id_t {
        return elem(IdVec{tuple.begin(), tuple.end()}, LitVec{cond.begin(), cond.end()});
    }
 
    auto atom(std::function<prg_lit_t()> const &atom, prg_id_t name, IdVec elems,
              std::optional<std::pair<prg_id_t, prg_id_t>> guard) -> prg_lit_t;
 
    auto atom(std::function<prg_lit_t()> const &atom, Symbol name, IdVec elems,
              std::optional<std::pair<String, prg_id_t>> guard) -> prg_lit_t;
 
    auto atom(std::function<prg_lit_t()> const &atom, Symbol name, PrgIdSpan elems,
              std::optional<std::pair<String, prg_id_t>> guard) -> prg_lit_t {
        return this->atom(atom, name, IdVec{elems.begin(), elems.end()}, guard);
    }
 
    void reset() noexcept;
 
  private:
    using StringMap = Util::unordered_map<SharedString, prg_id_t>;
    using NumMap = Util::unordered_map<prg_weight_t, prg_id_t>;
    using FunMap = Util::unordered_map<std::pair<prg_id_t, IdVec>, prg_id_t>;
    using TupMap = Util::unordered_map<std::pair<TheoryTermTupleType, IdVec>, prg_id_t>;
    using ElemMap = Util::unordered_map<std::pair<IdVec, LitVec>, prg_id_t>;
    using AtomMap =
        Util::unordered_map<std::tuple<prg_id_t, IdVec, std::optional<std::pair<prg_id_t, prg_id_t>>>, prg_lit_t>;
 
    template <class M, class V> auto insert_(M &map, V &&val) -> std::pair<typename M::iterator, bool>;
 
    SymbolStore *store_;
    UTheoryBackend backend_;
    Util::OutputBuffer buf_;
    StringMap strings_;
    NumMap nums_;
    FunMap funs_;
    TupMap tups_;
    ElemMap elems_;
    AtomMap atoms_;
    prg_id_t ids_ = 0;
};
 
auto make_backend_output(SymbolStore &store, ProgramBackend &backend, TheoryData &theory) -> UOutputStm;
 
 
} // namespace CppClingo::Output