theory_term.hh

#pragma once
 
#include <clingo/ground/instantiator.hh>
#include <clingo/ground/term.hh>
 
namespace CppClingo::Ground {
 
 
class TheoryTerm;
using UTheoryTerm = std::unique_ptr<TheoryTerm>;
using UTheoryTermVec = std::vector<UTheoryTerm>;
 
class TheoryTerm {
  public:
    virtual ~TheoryTerm() = default;
    void vars(VariableSet &vars) const { do_vars(vars); }
    [[nodiscard]] auto copy() const -> UTheoryTerm { return do_copy(); }
    [[nodiscard]] auto hash() const -> size_t { return do_hash(); }
 
    [[nodiscard]] auto vars() const -> VariableSet {
        VariableSet set;
        vars(set);
        return set;
    }
 
    auto output(EvalContext const &ctx, OutputTheory &out) const -> size_t { return do_output(ctx, out); }
 
    friend auto operator==(TheoryTerm const &a, TheoryTerm const &b) -> bool { return a.do_equal_to(b); }
    friend auto operator<=>(TheoryTerm const &a, TheoryTerm const &b) -> std::strong_ordering {
        return a.do_compare_to(b);
    }
    friend auto operator<<(std::ostream &out, TheoryTerm const &term) -> std::ostream & {
        term.do_print(out);
        return out;
    }
 
  private:
    virtual void do_vars(VariableSet &vars) const = 0;
    virtual void do_print(std::ostream &out) const = 0;
    virtual auto do_output(EvalContext const &ctx, OutputTheory &out) const -> size_t = 0;
    [[nodiscard]] virtual auto do_copy() const -> UTheoryTerm = 0;
    [[nodiscard]] virtual auto do_hash() const -> size_t = 0;
    [[nodiscard]] virtual auto do_equal_to(TheoryTerm const &other) const -> bool = 0;
    [[nodiscard]] virtual auto do_compare_to(TheoryTerm const &other) const -> std::strong_ordering = 0;
};
 
class TheoryTermSymbol : public TheoryTerm {
  public:
    TheoryTermSymbol(Symbol sym) : sym_{sym} {}
 
  private:
    void do_vars(VariableSet &vars) const override;
    void do_print(std::ostream &out) const override;
    auto do_output(EvalContext const &ctx, OutputTheory &out) const -> size_t override;
    [[nodiscard]] auto do_copy() const -> UTheoryTerm override;
    [[nodiscard]] auto do_hash() const -> size_t override;
    [[nodiscard]] auto do_equal_to(TheoryTerm const &other) const -> bool override;
    [[nodiscard]] auto do_compare_to(TheoryTerm const &other) const -> std::strong_ordering override;
 
    Symbol sym_;
};
 
class TheoryTermVariable : public TheoryTerm {
  public:
    TheoryTermVariable(size_t var) : var_{var} {}
 
  private:
    void do_vars(VariableSet &vars) const override;
    void do_print(std::ostream &out) const override;
    auto do_output(EvalContext const &ctx, OutputTheory &out) const -> size_t override;
    [[nodiscard]] auto do_copy() const -> UTheoryTerm override;
    [[nodiscard]] auto do_hash() const -> size_t override;
    [[nodiscard]] auto do_equal_to(TheoryTerm const &other) const -> bool override;
    [[nodiscard]] auto do_compare_to(TheoryTerm const &other) const -> std::strong_ordering override;
 
    size_t var_;
};
 
class TheoryTermTuple : public TheoryTerm {
  public:
    TheoryTermTuple(TheoryTermTupleType type, UTheoryTermVec args) : type_{type}, args_{std::move(args)} {}
 
  private:
    void do_vars(VariableSet &vars) const override;
    void do_print(std::ostream &out) const override;
    auto do_output(EvalContext const &ctx, OutputTheory &out) const -> size_t override;
    [[nodiscard]] auto do_copy() const -> UTheoryTerm override;
    [[nodiscard]] auto do_hash() const -> size_t override;
    [[nodiscard]] auto do_equal_to(TheoryTerm const &other) const -> bool override;
    [[nodiscard]] auto do_compare_to(TheoryTerm const &other) const -> std::strong_ordering override;
 
    TheoryTermTupleType type_;
    UTheoryTermVec args_;
};
 
class TheoryTermFunction : public TheoryTerm {
  public:
    TheoryTermFunction(String name, UTheoryTermVec args) : name_{name}, args_{std::move(args)} {}
 
  private:
    void do_vars(VariableSet &vars) const override;
    void do_print(std::ostream &out) const override;
    auto do_output(EvalContext const &ctx, OutputTheory &out) const -> size_t override;
    [[nodiscard]] auto do_copy() const -> UTheoryTerm override;
    [[nodiscard]] auto do_hash() const -> size_t override;
    [[nodiscard]] auto do_equal_to(TheoryTerm const &other) const -> bool override;
    [[nodiscard]] auto do_compare_to(TheoryTerm const &other) const -> std::strong_ordering override;
 
    String name_;
    UTheoryTermVec args_;
};
 
 
} // namespace CppClingo::Ground