iesolver.hh

#pragma once
 
#include <clingo/input/program.hh>
 
namespace CppClingo::Input {
 
 
struct IETerm {
    friend auto operator<<(std::ostream &out, IETerm const &term) -> std::ostream &;
    friend auto operator==(IETerm const &a, IETerm const &b) -> bool = default;
    friend auto operator<=>(IETerm const &a, IETerm const &b) {
        return std::tie(a.variable, a.coefficient) <=> std::tie(b.variable, b.coefficient);
    }
 
    Number coefficient;
    String variable;
};
using IETermVec = std::vector<IETerm>;
 
void add_term(IETermVec &terms, IETerm term);
auto simplify(IETermVec &terms) -> Number;
 
struct IE {
    friend auto operator<<(std::ostream &out, IE const &ie) -> std::ostream &;
 
    IETermVec terms;
    Number bound;
};
using IEVec = std::vector<IE>;
 
class IEInterval {
  public:
    enum Type : uint8_t { Lower, Upper };
    IEInterval() = default;
    IEInterval(std::optional<Number> lower, std::optional<Number> upper)
        : lower_{std::move(lower)}, upper_{std::move(upper)} {}
 
    [[nodiscard]] auto has_value(Type type) const -> bool;
    [[nodiscard]] auto value(Type type) const -> Number const &;
    void set_value(Type type, Number bound);
    auto refine(Type type, Number const &bound) -> bool;
 
    auto refine(IEInterval const &bound) -> bool;
 
    friend auto operator<<(std::ostream &out, IEInterval const &bound) -> std::ostream &;
    friend auto operator==(IEInterval const &a, IEInterval const &b) -> bool = default;
    friend auto operator!=(IEInterval const &a, IEInterval const &b) -> bool = default;
 
  private:
    std::optional<Number> lower_;
    std::optional<Number> upper_;
};
 
using IEDomain = Util::ordered_map<String, IEInterval>;
 
class IESolver {
  public:
    IESolver(IESolver *parent = nullptr) : parent_{parent} {}
    void add(IE ie);
    [[nodiscard]] auto compute(Logger &log) -> bool;
    [[nodiscard]] auto domain() const -> IEDomain const & { return domain_; }
    [[nodiscard]] auto strengthens(String var) const -> bool;
 
  private:
    auto update_bound_(IETerm const &term, Number slack, size_t num_unbounded) -> bool;
    auto update_slack_(IETerm const &term, Number &slack) -> bool;
 
    IESolver *parent_;
    IEDomain domain_;
    IEVec ies_;
};
 
 
} // namespace CppClingo::Input