output.hh

#pragma once
 
#include <clingo/core/backend.hh>
#include <clingo/core/core.hh>
#include <clingo/core/symbol.hh>
 
#include <clingo/util/small_vector.hh>
 
namespace CppClingo {
 
 
using IndexSpan = std::span<size_t const>;
using IndexVec = std::vector<size_t>;
 
class OutputTheory {
  public:
    enum class AtomType : uint8_t {
        head,      
        body,      
        directive, 
    };
 
    using OptGuard = std::optional<std::pair<String, size_t>>;
    virtual ~OutputTheory() = default;
    auto str(String val) -> size_t { return do_str(val); }
    auto num(Number const &num) -> size_t { return do_num(num); }
    auto fun(String name, IndexSpan args) -> size_t { return do_fun(name, args); }
    auto tup(TheoryTermTupleType type, IndexSpan args) -> size_t { return do_tup(type, args); }
    auto elem(IndexSpan tuple, size_t cond) -> size_t { return do_elem(tuple, cond); }
    void atom(AtomType type, size_t atom_uid, Symbol name, IndexSpan elems, OptGuard guard = std::nullopt) {
        do_atom(type, atom_uid, name, elems, guard);
    }
    auto sym(Symbol sym) -> size_t { return do_sym(sym); }
 
  private:
    virtual auto do_str(String val) -> size_t = 0;
    virtual auto do_num(Number const &val) -> size_t = 0;
    virtual auto do_fun(String name, std::span<size_t const> args) -> size_t = 0;
    virtual auto do_tup(TheoryTermTupleType type, std::span<size_t const> args) -> size_t = 0;
    virtual auto do_sym(Symbol sym) -> size_t = 0;
    virtual auto do_elem(IndexSpan tuple, size_t cond) -> size_t = 0;
    virtual void do_atom(AtomType type, size_t atom_uid, Symbol name, IndexSpan elems, OptGuard guard) = 0;
};
 
class OutputLit {
  public:
    virtual ~OutputLit() = default;
    void lit(Sign sign, Symbol sym, size_t uid) { do_lit(sign, sym, uid); }
    void boolean(bool value) { do_boolean(value); }
    auto cond_lit(std::optional<size_t> uid) -> size_t { return do_cond_lit(uid); }
    auto bd_aggr(Sign sign, std::optional<size_t> uid) -> size_t { return do_bd_aggr(sign, uid); }
    auto bd_theory(Sign sign, std::optional<size_t> uid) -> size_t { return do_bd_theory(sign, uid); }
 
  private:
    virtual void do_lit(Sign sign, Symbol sym, size_t uid) = 0;
    virtual void do_boolean(bool value) = 0;
    virtual auto do_cond_lit(std::optional<size_t> uid) -> size_t = 0;
    virtual auto do_bd_aggr(Sign sign, std::optional<size_t> uid) -> size_t = 0;
    virtual auto do_bd_theory(Sign sign, std::optional<size_t> uid) -> size_t = 0;
};
 
class OutputStm {
  public:
    using BdElem = std::pair<SymbolSpan, IndexSpan>;
    using BdElemSpan = std::span<BdElem const>;
    using HdElem = std::pair<SymbolSpan, std::span<std::tuple<Symbol, size_t, size_t> const>>;
    using HdElemSpan = std::span<HdElem const>;
    using Guard = std::pair<Relation, Symbol>;
    using GuardSpan = std::span<Guard const>;
    using CondLit = std::pair<std::optional<size_t>, size_t>;
    using CondLitSpan = std::span<CondLit const>;
    using DisjElem = std::tuple<Symbol, size_t, IndexSpan>;
    using DisjElemSpan = std::span<DisjElem const>;
 
    virtual ~OutputStm() = default;
 
    auto uid(bool fact = false) -> size_t { return do_uid(fact); }
 
    void fact(Symbol sym, size_t uid) { do_fact(sym, uid); }
 
    void project_atom(size_t p_atom, size_t atom) { do_project_atom(p_atom, atom); }
 
    auto body() -> OutputLit & { return do_body(); }
    void rule(std::optional<std::tuple<Symbol, size_t, bool>> head) { do_rule(head); }
    void external(Symbol atom, size_t uid, ExternalType type) { do_external(atom, uid, type); }
    void project(Symbol atom, size_t uid) { do_project(atom, uid); }
    auto aggr_rule(std::optional<size_t> uid) -> size_t { return do_aggr_rule(uid); }
    auto theory_rule(std::optional<size_t> uid) -> size_t { return do_theory_rule(uid); }
    auto disjunctive_rule(std::optional<size_t> uid) -> size_t { return do_disjunctive_rule(uid); }
    void weak_constraint(Number const &weight, Number const *prio, SymbolSpan terms) {
        do_weak_constraint(weight, prio, terms);
    }
    void heuristic(Symbol atom, size_t uid, Number const &weight, Number const *prio, HeuristicType type) {
        do_heuristic(atom, uid, weight, prio, type);
    }
    void edge(Symbol src, Symbol dst) { do_edge(src, dst); }
 
    void show_atom(Symbol atom, size_t uid) { do_show_atom(atom, uid); }
    void show_term(Symbol term) { do_show_term(term); }
 
    auto cond() -> OutputLit & { return do_cond(); }
    auto cond_id() -> size_t { return do_cond_id(); }
 
    void bd_aggr(size_t uid, AggregateFunction fun, BdElemSpan elems, GuardSpan guards) {
        do_bd_aggr(uid, fun, elems, guards);
    }
    void hd_aggr(size_t uid, AggregateFunction fun, HdElemSpan elems, GuardSpan guards) {
        do_hd_aggr(uid, fun, elems, guards);
    }
    void disjunction(size_t uid, DisjElemSpan elems) { do_disjunction(uid, elems); }
 
    void cond_lit(size_t uid, CondLitSpan elems) { do_cond_lit(uid, elems); }
 
    auto theory() -> OutputTheory & { return do_theory(); }
 
    void flush() { do_flush(); }
    void classical_negation(size_t atom_a, size_t atom_b) { do_classical_negation(atom_a, atom_b); }
    void end_step() { do_end_step(); }
 
    void mark(SymbolCollector &gc) { do_mark(gc); }
 
    void simplify(std::function<TruthValue(prg_lit_t)> const &pred) { do_simplify(pred); }
 
  private:
    virtual auto do_uid(bool fact) -> size_t = 0;
 
    virtual void do_fact(Symbol sym, size_t uid) = 0;
 
    virtual void do_project_atom(size_t p_atom, size_t atom) = 0;
 
    virtual auto do_body() -> OutputLit & = 0;
    virtual void do_rule(std::optional<std::tuple<Symbol, size_t, bool>> head) = 0;
    virtual void do_external(Symbol atom, size_t uid, ExternalType type) = 0;
    virtual void do_project(Symbol atom, size_t uid) = 0;
    virtual auto do_aggr_rule(std::optional<size_t> uid) -> size_t = 0;
    virtual auto do_theory_rule(std::optional<size_t> uid) -> size_t = 0;
    virtual auto do_disjunctive_rule(std::optional<size_t> uid) -> size_t = 0;
    virtual void do_weak_constraint(Number const &weight, Number const *prio, SymbolSpan terms) = 0;
    virtual void do_heuristic(Symbol atom, size_t uid, Number const &weight, Number const *prio,
                              HeuristicType type) = 0;
    virtual void do_edge(Symbol src, Symbol dst) = 0;
 
    virtual void do_show_atom(Symbol atom, size_t uid) = 0;
    virtual void do_show_term(Symbol term) = 0;
 
    virtual auto do_cond() -> OutputLit & = 0;
    virtual auto do_cond_id() -> size_t = 0;
 
    virtual void do_cond_lit(size_t uid, CondLitSpan elems) = 0;
    virtual void do_bd_aggr(size_t uid, AggregateFunction fun, BdElemSpan elems, GuardSpan guards) = 0;
    virtual void do_hd_aggr(size_t uid, AggregateFunction fun, HdElemSpan elems, GuardSpan guards) = 0;
    virtual void do_disjunction(size_t uid, DisjElemSpan elems) = 0;
 
    virtual auto do_theory() -> OutputTheory & = 0;
 
    virtual void do_flush() = 0;
    virtual void do_classical_negation(size_t atom_a, size_t atom_b) = 0;
    virtual void do_end_step() = 0;
 
    virtual void do_mark(SymbolCollector &gc) = 0;
    virtual void do_simplify(std::function<TruthValue(prg_lit_t)> const &pred) = 0;
};
 
using UOutputStm = std::unique_ptr<OutputStm>;
 
 
} // namespace CppClingo