backend.hh

#pragma once
 
#include <clingo/core/core.hh>
#include <clingo/core/symbol.hh>
 
#include <clingo/util/small_vector.hh>
 
namespace CppClingo {
 
 
using prg_id_t = uint32_t;
using PrgIdSpan = std::span<prg_id_t const>;
using PrgIdVec = std::vector<prg_id_t>;
using prg_sid_t = std::make_signed_t<prg_id_t>;
using prg_lit_t = int32_t;
using prg_atom_t = uint32_t;
using prg_weight_t = int32_t;
using prg_sum_t = int64_t;
using PrgLitSpan = std::span<prg_lit_t const>;
using PrgLitVec = std::vector<prg_lit_t>;
using WeightedPrgLitSpan = std::span<std::pair<prg_lit_t, prg_weight_t> const>;
using WeightedPrgLitVec = std::vector<std::pair<prg_lit_t, prg_weight_t>>;
 
static constexpr auto prg_lit_max = std::numeric_limits<prg_lit_t>::max();
static constexpr auto prg_lit_min = -prg_lit_max;
 
class ProgramBackend {
  public:
    virtual ~ProgramBackend() = default;
 
    void preamble(unsigned major, unsigned minor, unsigned revision, bool incremental) {
        do_preamble(major, minor, revision, incremental);
    }
 
    void end() { do_end(); }
 
    auto next_lit() -> prg_lit_t { return do_next_lit(); }
 
    auto fact_lit() -> std::optional<prg_lit_t> { return do_fact_lit(); }
 
    void bd_aggr(PrgLitSpan head, WeightedPrgLitSpan body, int32_t bound, bool choice) {
        assert(std::ranges::all_of(head, [](auto const &x) { return x > 0; }));
        do_bd_aggr(head, body, bound, choice);
    }
 
    void rule(PrgLitSpan head, PrgLitSpan body, bool choice) {
        assert(std::ranges::all_of(head, [](auto const &x) { return x > 0; }));
        do_rule(head, body, choice);
    }
 
    void show_term(Symbol sym, PrgLitSpan body) { do_show_term(sym, body); }
 
    void show_term(Symbol sym, prg_id_t id) { do_show_term(sym, id); }
 
    void show_term(prg_id_t id, PrgLitSpan body) { do_show_term(id, body); }
 
    void show_atom(Symbol sym, prg_lit_t lit) { do_show_atom(sym, lit); }
 
    void edge(prg_id_t u, prg_id_t v, PrgLitSpan body) { do_edge(u, v, body); }
 
    void heuristic(prg_lit_t atom, int32_t weight, int32_t prio, HeuristicType type, PrgLitSpan body) {
        assert(atom > 0);
        do_heuristic(atom, weight, prio, type, body);
    }
    void external(prg_lit_t atom, ExternalType type) {
        assert(atom > 0);
        do_external(atom, type);
    }
 
    void project(PrgLitSpan atoms) {
        assert(std::ranges::all_of(atoms, [](auto const &x) { return x > 0; }));
        do_project(atoms);
    }
 
    void assume(PrgLitSpan literals) { do_assume(literals); }
 
    void minimize(prg_weight_t priority, WeightedPrgLitSpan body) { do_minimize(priority, body); }
 
  private:
    virtual void do_preamble(unsigned major, unsigned minor, unsigned revision, bool incremental) = 0;
    virtual void do_end() = 0;
    virtual auto do_next_lit() -> prg_lit_t = 0;
    virtual auto do_fact_lit() -> std::optional<prg_lit_t> = 0;
 
    virtual void do_rule(PrgLitSpan head, PrgLitSpan body, bool choice) = 0;
    virtual void do_bd_aggr(PrgLitSpan head, WeightedPrgLitSpan body, int32_t bound, bool choice) = 0;
    virtual void do_show_term(Symbol sym, PrgLitSpan body) = 0;
    virtual void do_show_term(Symbol sym, prg_id_t id) = 0;
    virtual void do_show_term(prg_id_t id, PrgLitSpan body) = 0;
    virtual void do_show_atom(Symbol sym, prg_lit_t lit) = 0;
    virtual void do_edge(prg_id_t u, prg_id_t v, PrgLitSpan body) = 0;
    virtual void do_heuristic(prg_lit_t atom, prg_weight_t weight, prg_weight_t prio, HeuristicType type,
                              PrgLitSpan body) = 0;
    virtual void do_external(prg_lit_t atom, ExternalType type) = 0;
    virtual void do_project(PrgLitSpan atoms) = 0;
    virtual void do_assume(PrgLitSpan literals) = 0;
    virtual void do_minimize(prg_weight_t priority, WeightedPrgLitSpan body) = 0;
};
using UProgramBackend = std::unique_ptr<ProgramBackend>;
 
class TheoryBackend {
  public:
    virtual ~TheoryBackend() = default;
 
    void num(prg_id_t id, prg_weight_t num) { do_num(id, num); }
    void str(prg_id_t id, std::string_view str) { do_str(id, str); }
    void fun(prg_id_t id, prg_id_t name, PrgIdSpan args) { do_fun(id, name, args); }
 
    void tup(prg_id_t id, TheoryTermTupleType type, PrgIdSpan args) { do_tup(id, type, args); }
 
    void elem(prg_id_t id, PrgIdSpan terms, PrgLitSpan cond) { do_elem(id, terms, cond); }
 
    void atom(prg_lit_t atom_or_zero, prg_id_t name, PrgIdSpan elems,
              std::optional<std::pair<prg_id_t, prg_id_t>> guard) {
        assert(atom_or_zero >= 0);
        do_atom(atom_or_zero, name, elems, guard);
    }
 
    void end() { do_end(); }
 
  private:
    virtual void do_num(prg_id_t id, prg_weight_t num) = 0;
    virtual void do_str(prg_id_t id, std::string_view str) = 0;
    virtual void do_fun(prg_id_t id, prg_id_t name, PrgIdSpan args) = 0;
    virtual void do_tup(prg_id_t id, TheoryTermTupleType type, PrgIdSpan args) = 0;
    virtual void do_elem(prg_id_t id, PrgIdSpan terms, PrgLitSpan cond) = 0;
    virtual void do_atom(prg_lit_t atom_or_zero, prg_id_t name, PrgIdSpan elems,
                         std::optional<std::pair<prg_id_t, prg_id_t>> guard) = 0;
    virtual void do_end() = 0;
};
using UTheoryBackend = std::unique_ptr<TheoryBackend>;
 
 
} // namespace CppClingo