aggregate.hh

#pragma once
 
#include <clingo/input/literal.hh>
 
#include <optional>
#include <utility>
 
namespace CppClingo::Input {
 
 
using LGuard = std::optional<std::pair<Term, Relation>>;
using RGuard = std::optional<std::pair<Relation, Term>>;
 
inline auto reduct_is_nonmonotone(LGuard const &lhs, AggregateFunction fun, RGuard const &rhs) -> bool {
    if (!lhs.has_value() && !rhs.has_value()) {
        return false;
    }
    if (lhs.has_value() && lhs->second == Relation::not_equal) {
        return true;
    }
    if (rhs.has_value() && rhs->first == Relation::not_equal) {
        return true;
    }
    return fun == AggregateFunction::sum;
}
 
inline auto reduct_is_monotone(LGuard const &lhs, AggregateFunction fun, RGuard const &rhs) -> bool {
    if (fun != AggregateFunction::sum) {
        auto check = [](auto rel, bool less) {
            return less ? (rel == Relation::less || rel == Relation::less_equal)
                        : (rel == Relation::greater || rel == Relation::greater_equal);
        };
        bool less = fun != AggregateFunction::min;
        return (!lhs || check(lhs->second, less)) && (!rhs || check(rhs->first, !less));
    }
    return false;
}
 
class SetAggregateElement : public Expression<SetAggregateElement> {
  public:
    static constexpr auto attributes() {
        return std::tuple{a_loc = &SetAggregateElement::loc_, a_lit = &SetAggregateElement::lit_,
                          a_cond = &SetAggregateElement::cond_};
    }
 
    explicit SetAggregateElement(Location loc, Lit lit, LitArray cond)
        : loc_{std::move(loc)}, lit_{std::move(lit)}, cond_{std::move(cond)} {}
    [[nodiscard]] auto loc() const -> Location const & { return loc_; }
    [[nodiscard]] auto lit() const -> Lit const & { return lit_; }
    [[nodiscard]] auto cond() const -> LitArray const & { return cond_; }
 
  private:
    Location loc_;
    Lit lit_;
    LitArray cond_;
};
 
using SetAggregateElementArray = Util::immutable_array<SetAggregateElement>;
 
template <bool HasSign>
class SetAggregate : public std::conditional_t<HasSign, Signed, Unsigned>, public Expression<SetAggregate<HasSign>> {
  public:
    using Base = std::conditional_t<HasSign, Signed, Unsigned>;
 
    static constexpr auto attributes() {
        if constexpr (HasSign) {
            return std::tuple{a_loc = &SetAggregate::loc_, a_sign = &Signed::sign, a_lhs = &SetAggregate::lhs_,
                              a_elems = &SetAggregate::elems_, a_rhs = &SetAggregate::rhs_};
        } else {
            return std::tuple{a_loc = &SetAggregate::loc_, a_lhs = &SetAggregate::lhs_, a_elems = &SetAggregate::elems_,
                              a_rhs = &SetAggregate::rhs_};
        }
    }
 
    explicit SetAggregate(Location loc, LGuard lhs, SetAggregateElementArray elems, RGuard rhs)
        : loc_{std::move(loc)}, elems_{std::move(elems)}, lhs_(std::move(lhs)), rhs_(std::move(rhs)) {
        static_assert(!HasSign);
    }
 
    explicit SetAggregate(Location loc, Sign sign, LGuard lhs, SetAggregateElementArray elems, RGuard rhs)
        : Signed{sign}, loc_{std::move(loc)}, elems_{std::move(elems)}, lhs_(std::move(lhs)), rhs_(std::move(rhs)) {
        static_assert(HasSign);
    }
 
    [[nodiscard]] auto loc() const -> Location const & { return loc_; }
    [[nodiscard]] auto elems() const -> SetAggregateElementArray const & { return elems_; }
    [[nodiscard]] auto lhs() const -> LGuard const & { return lhs_; }
    [[nodiscard]] auto rhs() const -> RGuard const & { return rhs_; }
 
  private:
    Location loc_;
    SetAggregateElementArray elems_;
    LGuard lhs_;
    RGuard rhs_;
};
 
using HdLitSetAggregate = SetAggregate<false>;
 
using BdLitSetAggregate = SetAggregate<true>;
 
 
} // namespace CppClingo::Input