term.hh

#pragma once
 
#include <clingo/ground/instantiator.hh>
 
#include <clingo/core/core.hh>
#include <clingo/core/fstring.hh>
#include <clingo/core/location.hh>
#include <clingo/core/logger.hh>
#include <clingo/core/symbol.hh>
 
#include <clingo/util/enum.hh>
#include <clingo/util/ordered_set.hh>
#include <clingo/util/unordered_map.hh>
 
namespace CppClingo::Ground {
 
 
using VariableSet = Util::ordered_set<size_t>;
using VariableVec = VariableSet::values_container_type;
 
enum class RenameMode : uint8_t {
    rename_vars,       
    rename_projection, 
    drop_projection,   
};
 
class Term;
using UTerm = std::unique_ptr<Term>;
using UTermVec = std::vector<UTerm>;
using GuardVec = std::vector<std::pair<Relation, UTerm>>;
 
template <class T>
    requires requires(T x) {
        { x.copy() } -> std::convertible_to<std::unique_ptr<T>>;
    }
auto copy_uvec(std::vector<std::unique_ptr<T>> const &vec) {
    std::vector<std::unique_ptr<T>> res;
    res.reserve(vec.size());
    for (auto const &x : vec) {
        res.emplace_back(x->copy());
    }
    return res;
}
template <class T>
    requires requires(T x) {
        { x.copy() } -> std::convertible_to<std::unique_ptr<T>>;
    }
auto copy_uvec(std::vector<std::vector<std::unique_ptr<T>>> const &vec) {
    std::vector<std::vector<std::unique_ptr<T>>> res;
    res.reserve(vec.size());
    for (auto const &x : vec) {
        res.emplace_back(copy_uvec(x));
    }
    return res;
}
 
class Term {
  public:
    using Key = Symbol;
 
    virtual ~Term() = default;
    [[nodiscard]] auto score(double size, std::vector<bool> const &bound) const -> double {
        return do_score(size, bound);
    }
    [[nodiscard]] auto match(EvalContext const &ctx, Symbol sym) const -> bool { return do_match(ctx, sym); }
    [[nodiscard]] auto eval(EvalContext const &ctx) const -> std::optional<Symbol> { return do_eval(ctx); }
    [[nodiscard]] auto rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const -> UTerm {
        return do_rename(store, mode, name, vars);
    }
    [[nodiscard]] auto rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm { return do_rename(vars); }
    void vars(VariableSet &vars, bool provide = false) const { do_vars(vars, provide); }
    [[nodiscard]] auto copy() const -> UTerm { return do_copy(); }
    [[nodiscard]] auto hash() const -> size_t { return do_hash(); }
 
    [[nodiscard]] auto signature(VariableSet const &bound, VariableSet const &bind) const
        -> std::pair<UTerm, VariableVec> {
        auto names = Util::unordered_map<size_t, size_t>{};
        names.reserve(bind.size() + bound.size());
        auto sig_term = rename(names);
        auto sig_lookup = std::vector<size_t>{};
        sig_lookup.reserve(bound.size());
        for (auto const &var : bound) {
            sig_lookup.emplace_back(names[var]);
        }
        return {std::move(sig_term), std::move(sig_lookup)};
    }
    [[nodiscard]] auto vars() const -> VariableSet {
        VariableSet set;
        vars(set);
        return set;
    }
 
    friend auto operator==(Term const &a, Term const &b) -> bool { return a.do_equal_to(b); }
    friend auto operator<=>(Term const &a, Term const &b) -> std::strong_ordering { return a.do_compare_to(b); }
    friend auto operator<<(std::ostream &out, Term const &term) -> std::ostream & {
        term.do_print(out);
        return out;
    }
 
  private:
    [[nodiscard]] virtual auto do_score(double size, std::vector<bool> const &bound) const -> double = 0;
    [[nodiscard]] virtual auto do_match(EvalContext const &ctx, Symbol sym) const -> bool = 0;
    [[nodiscard]] virtual auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> = 0;
    [[nodiscard]] virtual auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
        -> UTerm = 0;
    [[nodiscard]] virtual auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm = 0;
    virtual void do_vars(VariableSet &vars, bool provide) const = 0;
    virtual void do_print(std::ostream &out) const = 0;
    [[nodiscard]] virtual auto do_copy() const -> UTerm = 0;
    [[nodiscard]] virtual auto do_hash() const -> size_t = 0;
    [[nodiscard]] virtual auto do_equal_to(Term const &other) const -> bool = 0;
    [[nodiscard]] virtual auto do_compare_to(Term const &other) const -> std::strong_ordering = 0;
};
 
class TermProjection : public Term {
  public:
    TermProjection() = default;
 
  private:
    [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
    [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
    [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
    [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
        -> UTerm override;
    [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
    void do_vars(VariableSet &vars, bool provide) const override;
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_copy() const -> UTerm override;
    [[nodiscard]] auto do_hash() const -> size_t override;
    [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
    [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
};
 
class TermSymbol : public Term {
  public:
    TermSymbol(Symbol sym) : sym_{sym} {}
 
    [[nodiscard]] auto symbol() const -> Symbol const & { return *sym_; }
 
  private:
    [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
    [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
    [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
    [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
        -> UTerm override;
    [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
    void do_vars(VariableSet &vars, bool provide) const override;
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_copy() const -> UTerm override;
    [[nodiscard]] auto do_hash() const -> size_t override;
    [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
    [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
 
    SharedSymbol sym_;
};
 
using FormatField = std::variant<SharedString, std::pair<UTerm, FormatSpec>>;
using FormatFieldVec = std::vector<FormatField>;
 
class TermFormatString : public Term {
  public:
    TermFormatString(FormatFieldVec elems) : elems_{std::move(elems)} {}
 
  private:
    [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
    [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
    [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
    [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
        -> UTerm override;
    [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
    void do_vars(VariableSet &vars, bool provide) const override;
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_copy() const -> UTerm override;
    [[nodiscard]] auto do_hash() const -> size_t override;
    [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
    [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
 
    FormatFieldVec elems_;
    mutable Util::OutputBuffer buf_;
    mutable Util::OutputBuffer tmp_;
};
 
class TermVariable : public Term {
  public:
    TermVariable(size_t var) : var_{var} {}
 
  private:
    [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
    [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
    [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
    [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
        -> UTerm override;
    [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
    void do_vars(VariableSet &vars, bool provide) const override;
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_copy() const -> UTerm override;
    [[nodiscard]] auto do_hash() const -> size_t override;
    [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
    [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
 
    size_t var_;
};
 
class TermLinear : public Term {
  public:
    TermLinear(Location loc, Number m, size_t var, Number n)
        : loc_{std::move(loc)}, m_{std::move(m)}, n_{std::move(n)}, var_{var} {}
 
  private:
    [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
    [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
    [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
    [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
        -> UTerm override;
    [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
    void do_vars(VariableSet &vars, bool provide) const override;
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_copy() const -> UTerm override;
    [[nodiscard]] auto do_hash() const -> size_t override;
    [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
    [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
 
    Location loc_;
    Number m_;
    Number n_;
    size_t var_;
    mutable bool logged_ = false;
};
 
enum class UnaryOperator : uint8_t {
    minus = 0,  
    negate = 1, 
    abs = 2,    
};
 
class TermUnary : public Term {
  public:
    TermUnary(UnaryOperator op, Location loc_rhs, UTerm rhs)
        : loc_rhs_{std::move(loc_rhs)}, rhs_{std::move(rhs)}, op_{op} {}
 
  private:
    [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
    [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
    [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
    [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
        -> UTerm override;
    [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
    void do_vars(VariableSet &vars, bool provide) const override;
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_copy() const -> UTerm override;
    [[nodiscard]] auto do_hash() const -> size_t override;
    [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
    [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
 
    Location loc_rhs_;
    UTerm rhs_;
    UnaryOperator op_;
    mutable bool logged_ = false;
};
 
enum class BinaryOperator : uint8_t {
    and_,  
    div,   
    minus, 
    mod,   
    times, 
    or_,   
    plus,  
    pow,   
    xor_,  
};
 
class TermBinary : public Term {
  public:
    TermBinary(Location loc_lhs, UTerm lhs, BinaryOperator op, Location loc_rhs, UTerm rhs)
        : loc_lhs_{std::move(loc_lhs)}, loc_rhs_{std::move(loc_rhs)}, lhs_{std::move(lhs)}, rhs_{std::move(rhs)},
          op_{op} {}
 
  private:
    [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
    [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
    [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
    [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
        -> UTerm override;
    [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
    void do_vars(VariableSet &vars, bool provide) const override;
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_copy() const -> UTerm override;
    [[nodiscard]] auto do_hash() const -> size_t override;
    [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
    [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
 
    Location loc_lhs_;
    Location loc_rhs_;
    UTerm lhs_;
    UTerm rhs_;
    BinaryOperator op_;
    mutable bool logged_ = false;
};
 
class TermTuple : public Term {
  public:
    TermTuple(UTermVec args) : args_{std::move(args)} { eval_.reserve(args_.size()); }
 
  private:
    [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
    [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
    [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
    [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
        -> UTerm override;
    [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
    void do_vars(VariableSet &vars, bool provide) const override;
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_copy() const -> UTerm override;
    [[nodiscard]] auto do_hash() const -> size_t override;
    [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
    [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
 
    UTermVec args_;
    std::vector<Symbol> mutable eval_;
};
 
class TermFunction : public Term {
  public:
    TermFunction(String name, UTermVec args) : name_{name}, args_{std::move(args)} { eval_.reserve(args_.size()); }
 
  private:
    [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
    [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
    [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
    [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
        -> UTerm override;
    [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
    void do_vars(VariableSet &vars, bool provide) const override;
    void do_print(std::ostream &out) const override;
    [[nodiscard]] auto do_copy() const -> UTerm override;
    [[nodiscard]] auto do_hash() const -> size_t override;
    [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
    [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
 
    SharedString name_;
    UTermVec args_;
    std::vector<Symbol> mutable eval_;
};
 
template <class... T>
inline auto expect(EvalContext const &ctx, Location const &loc, bool &logged, T &&...args) -> bool {
    if (!logged && ctx.log().check(MessageCode::info_operation_undefined)) {
        logged = true;
        (CppClingo::Report(ctx.log(), MessageCode::info_operation_undefined, loc).out()
         << ... << std::forward<T>(args));
    }
    return false;
}
 
 
} // namespace CppClingo::Ground