theory.hh

#pragma once
 
#include <clingo/input/literal.hh>
#include <clingo/input/term.hh>
 
#include <utility>
 
namespace CppClingo::Input {
 
 
class TheoryTermSymbol;
class TheoryTermVariable;
class TheoryTermTuple;
class TheoryTermFunction;
class TheoryTermUnparsed;
class UnparsedElement;
 
using TheoryTerm =
    std::variant<TheoryTermSymbol, TheoryTermVariable, TheoryTermTuple, TheoryTermFunction, TheoryTermUnparsed>;
using TheoryTermArray = Util::immutable_array<TheoryTerm>;
 
class TheoryTermSymbol : public Expression<TheoryTermSymbol> {
  public:
    static constexpr auto attributes() {
        return std::tuple{a_loc = &TheoryTermSymbol::loc_, a_value = &TheoryTermSymbol::value};
    }
 
    explicit TheoryTermSymbol(Location loc, Symbol value) : loc_{std::move(loc)}, value_{value} {}
 
    [[nodiscard]] auto loc() const -> Location const & { return loc_; }
    [[nodiscard]] auto value() const -> Symbol const & { return *value_; }
 
  private:
    Location loc_;
    SharedSymbol value_;
};
 
class TheoryTermVariable : public Expression<TheoryTermVariable> {
  public:
    static constexpr auto attributes() {
        return std::tuple{a_loc = &TheoryTermVariable::loc_, a_name = &TheoryTermVariable::name,
                          a_anonymous = &TheoryTermVariable::anonymous_};
    }
 
    explicit TheoryTermVariable(Location loc, String name, bool is_anonymous = false)
        : loc_{std::move(loc)}, name_{name}, anonymous_{is_anonymous} {}
 
    [[nodiscard]] auto loc() const -> Location const & { return loc_; }
    [[nodiscard]] auto name() const -> String const & { return *name_; }
    [[nodiscard]] auto anonymous() const -> bool { return anonymous_; }
 
  private:
    Location loc_;
    SharedString name_;
    bool anonymous_;
};
 
class TheoryTermTuple : public RecursiveExpression<TheoryTermTuple> {
  public:
    static constexpr auto attributes() {
        return std::tuple{a_loc = &TheoryTermTuple::loc_, a_type = &TheoryTermTuple::type_,
                          a_elems = &TheoryTermTuple::elems_};
    }
 
    explicit TheoryTermTuple(Location loc, TheoryTermTupleType type, TheoryTermArray elems);
 
    [[nodiscard]] auto loc() const -> Location const & { return loc_; }
    [[nodiscard]] auto type() const -> TheoryTermTupleType { return type_; }
    [[nodiscard]] auto elems() const -> TheoryTermArray const & { return elems_; }
 
  private:
    Location loc_;
    TheoryTermTupleType type_;
    TheoryTermArray elems_;
};
 
class TheoryTermFunction : public RecursiveExpression<TheoryTermFunction> {
  public:
    static constexpr auto attributes() {
        return std::tuple{a_loc = &TheoryTermFunction::loc_, a_name = &TheoryTermFunction::name,
                          a_args = &TheoryTermFunction::args_};
    }
 
    explicit TheoryTermFunction(Location loc, String name);
    explicit TheoryTermFunction(Location loc, String name, TheoryTermArray args);
 
    [[nodiscard]] auto loc() const -> Location const & { return loc_; }
    [[nodiscard]] auto name() const -> String const & { return *name_; }
    [[nodiscard]] auto args() const -> TheoryTermArray const & { return args_; }
 
  private:
    Location loc_;
    SharedString name_;
    TheoryTermArray args_;
};
 
using UnparsedElementArray = Util::immutable_array<UnparsedElement>;
 
class TheoryTermUnparsed : public RecursiveExpression<TheoryTermUnparsed> {
  public:
    static constexpr auto attributes() {
        return std::tuple{a_loc = &TheoryTermUnparsed::loc_, a_elems = &TheoryTermUnparsed::elems_};
    }
 
    explicit TheoryTermUnparsed(Location loc, UnparsedElementArray elems);
 
    [[nodiscard]] auto loc() const -> Location const & { return loc_; }
    [[nodiscard]] auto elems() const -> UnparsedElementArray const & { return elems_; }
 
  private:
    Location loc_;
    UnparsedElementArray elems_;
};
 
class UnparsedElement : public Expression<UnparsedElement> {
  public:
    static constexpr auto attributes() {
        return std::tuple{a_ops = &UnparsedElement::ops, a_term = &UnparsedElement::term_};
    }
 
    UnparsedElement(StringSpan ops, TheoryTerm term) : ops_{ops.begin(), ops.end()}, term_{std::move(term)} {}
    UnparsedElement(SharedStringArray ops, TheoryTerm term) : ops_{std::move(ops)}, term_{std::move(term)} {}
 
    [[nodiscard]] auto ops() const -> StringSpan { return as_string_span(ops_); }
    [[nodiscard]] auto term() const -> TheoryTerm const & { return term_; }
 
  private:
    SharedStringArray ops_;
    TheoryTerm term_;
};
 
class TheoryRGuard : public Expression<TheoryRGuard> {
  public:
    static constexpr auto attributes() { return std::tuple{a_op = &TheoryRGuard::op, a_term = &TheoryRGuard::term_}; }
 
    explicit TheoryRGuard(String op, TheoryTerm term) : op_{op}, term_{std::move(term)} {}
 
    [[nodiscard]] auto op() const -> String const & { return *op_; }
    [[nodiscard]] auto term() const -> TheoryTerm const & { return term_; }
 
  private:
    SharedString op_;
    TheoryTerm term_;
};
 
class TheoryElement : public Expression<TheoryElement> {
  public:
    static constexpr auto attributes() {
        return std::tuple{a_loc = &TheoryElement::loc_, a_tuple = &TheoryElement::tuple_,
                          a_cond = &TheoryElement::cond_};
    }
 
    explicit TheoryElement(Location loc, TheoryTermArray tuple, LitArray cond)
        : loc_{std::move(loc)}, tuple_{std::move(tuple)}, cond_{std::move(cond)} {}
 
    [[nodiscard]] auto loc() const -> Location const & { return loc_; }
    [[nodiscard]] auto tuple() const -> TheoryTermArray const & { return tuple_; }
    [[nodiscard]] auto cond() const -> LitArray const & { return cond_; }
 
  private:
    Location loc_;
    TheoryTermArray tuple_;
    LitArray cond_;
};
using TheoryElementArray = Util::immutable_array<TheoryElement>;
 
template <bool HasSign>
class TheoryAtom : public std::conditional_t<HasSign, Signed, Unsigned>, public Expression<TheoryAtom<HasSign>> {
  public:
    using Base = std::conditional_t<HasSign, Signed, Unsigned>;
 
    static constexpr auto attributes() {
        if constexpr (HasSign) {
            return std::tuple{a_loc = &TheoryAtom::loc_, a_sign = &Signed::sign, a_name = &TheoryAtom::name_,
                              a_elems = &TheoryAtom::elems_, a_rhs = &TheoryAtom::rhs_};
        } else {
            return std::tuple{a_loc = &TheoryAtom::loc_, a_name = &TheoryAtom::name_, a_elems = &TheoryAtom::elems_,
                              a_rhs = &TheoryAtom::rhs_};
        }
    }
 
    explicit TheoryAtom(Location loc, Term name, TheoryElementArray elems, std::optional<TheoryRGuard> rhs)
        : loc_{std::move(loc)}, name_{std::move(name)}, elems_{std::move(elems)}, rhs_{std::move(rhs)} {
        static_assert(!HasSign);
    }
 
    explicit TheoryAtom(Location loc, Sign sign, Term name, TheoryElementArray elems, std::optional<TheoryRGuard> rhs)
        : Signed{sign}, loc_{std::move(loc)}, name_{std::move(name)}, elems_{std::move(elems)}, rhs_{std::move(rhs)} {
        static_assert(HasSign);
    }
 
    [[nodiscard]] auto loc() const -> Location const & { return loc_; }
    [[nodiscard]] auto name() const -> Term const & { return name_; }
    [[nodiscard]] auto elems() const -> TheoryElementArray const & { return elems_; }
    [[nodiscard]] auto rhs() const -> std::optional<TheoryRGuard> const & { return rhs_; }
 
  private:
    Location loc_;
    Term name_;
    TheoryElementArray elems_;
    std::optional<TheoryRGuard> rhs_;
};
 
using HdLitTheoryAtom = TheoryAtom<false>;
 
using BdLitTheoryAtom = TheoryAtom<true>;
 
 
// TheoryTermTuple
 
inline TheoryTermTuple::TheoryTermTuple(Location loc, TheoryTermTupleType type, TheoryTermArray elems)
    : loc_{std::move(loc)}, type_(type), elems_{std::move(elems)} {
}
 
inline auto operator==(TheoryTermTuple const &a, TheoryTermTuple const &b) -> bool {
    return a.equal(b);
}
 
inline auto operator<=>(TheoryTermTuple const &a, TheoryTermTuple const &b) -> std::strong_ordering {
    return a.compare(b);
}
 
// TheoryTermFunction
 
inline TheoryTermFunction::TheoryTermFunction(Location loc, String name, TheoryTermArray args)
    : loc_{std::move(loc)}, name_(name), args_{std::move(args)} {
}
 
inline TheoryTermFunction::TheoryTermFunction(Location loc, String name)
    : TheoryTermFunction{std::move(loc), name, {}} {
}
 
inline auto operator==(TheoryTermFunction const &a, TheoryTermFunction const &b) -> bool {
    return a.equal(b);
}
 
inline auto operator<=>(TheoryTermFunction const &a, TheoryTermFunction const &b) -> std::strong_ordering {
    return a.compare(b);
}
 
// TheoryTermUnparsed
 
inline TheoryTermUnparsed::TheoryTermUnparsed(Location loc, UnparsedElementArray elems)
    : loc_{std::move(loc)}, elems_{std::move(elems)} {
}
 
inline auto operator==(TheoryTermUnparsed const &a, TheoryTermUnparsed const &b) -> bool {
    return a.equal(b);
}
 
inline auto operator<=>(TheoryTermUnparsed const &a, TheoryTermUnparsed const &b) -> std::strong_ordering {
    return a.compare(b);
}
 
} // namespace CppClingo::Input