propagate.hh

#pragma once
 
#include <clingo/base.hh>
#include <clingo/core.hh>
 
#include <clingo/propagate.h>
 
namespace Clingo {
 
 
enum class PropagatorCheckMode : clingo_propagator_check_mode_t {
    none = clingo_propagator_check_mode_none,         
    total = clingo_propagator_check_mode_total,       
    fixpoint = clingo_propagator_check_mode_fixpoint, 
    both = clingo_propagator_check_mode_both,         
};
 
enum class PropagatorUndoMode : clingo_propagator_undo_mode_t {
    default_ = clingo_propagator_undo_mode_default, 
    always = clingo_propagator_undo_mode_always,    
};
 
enum WeightConstraintType : clingo_weight_constraint_type_t {
    implication_left = clingo_weight_constraint_type_implication_left,   
    implication_right = clingo_weight_constraint_type_implication_right, 
    equivalence = clingo_weight_constraint_type_equivalence, 
};
 
enum ClauseFlags : clingo_clause_type_t {
    none = clingo_clause_type_learnt,  
    lock = clingo_clause_type_static,  
    tag = clingo_clause_type_volatile, 
};
CLINGO_ENABLE_BITSET_ENUM(ClauseFlags);
 
class Trail {
  public:
    using value_type = SolverLiteral;
    using size_type = std::size_t;
    using difference_type = std::ptrdiff_t;
    using reference = value_type;
    using pointer = Detail::ArrowProxy<value_type>;
    using iterator = Detail::RandomAccessIterator<Trail>;
 
    explicit Trail(clingo_assignment_t const *assignment) : assignment_{assignment} {}
 
    [[nodiscard]] auto at(size_type index) const -> value_type {
        return Detail::call<clingo_assignment_trail_at>(assignment_, index);
    }
 
    [[nodiscard]] auto operator[](size_type index) const -> value_type { return at(index); }
 
    [[nodiscard]] auto size() const -> size_type { return Detail::call<clingo_assignment_trail_size>(assignment_); }
 
    [[nodiscard]] auto begin() const -> iterator { return iterator{*this, 0}; }
 
    [[nodiscard]] auto end() const -> iterator { return iterator{*this, size()}; }
 
    [[nodiscard]] auto begin(ProgramId level) const -> iterator {
        return iterator{*this, Detail::call<clingo_assignment_trail_begin>(assignment_, level)};
    }
 
    [[nodiscard]] auto end(ProgramId level) const -> iterator {
        return iterator{*this, Detail::call<clingo_assignment_trail_end>(assignment_, level)};
    }
 
    [[nodiscard]] auto level(ProgramId level) const { return std::ranges::subrange{begin(level), end(level)}; }
 
  private:
    clingo_assignment_t const *assignment_;
};
 
class Assignment {
  public:
    using value_type = SolverLiteral;
    using size_type = std::size_t;
    using difference_type = std::ptrdiff_t;
    using reference = value_type;
    using pointer = Detail::ArrowProxy<value_type>;
    using iterator = Detail::RandomAccessIterator<Assignment>;
 
    explicit Assignment(clingo_assignment_t const *assignment) : assignment_(assignment) {}
    [[nodiscard]] auto thread_id() const -> ProgramId { return Detail::call<clingo_assignment_thread_id>(assignment_); }
 
    [[nodiscard]] auto size() const -> size_type { return Detail::call<clingo_assignment_size>(assignment_); }
 
    [[nodiscard]] auto at(size_type size) const -> value_type {
        return Detail::call<clingo_assignment_at>(assignment_, size);
    }
 
    [[nodiscard]] auto operator[](size_type size) const -> value_type { return at(size); }
 
    [[nodiscard]] auto decision(ProgramId level) const -> SolverLiteral {
        return Detail::call<clingo_assignment_decision>(assignment_, level);
    }
 
    [[nodiscard]] auto decision_level() const -> ProgramId {
        return Detail::call<clingo_assignment_decision_level>(assignment_);
    }
 
    [[nodiscard]] auto has_conflict() const -> bool {
        return Detail::call<clingo_assignment_has_conflict>(assignment_);
    }
 
    [[nodiscard]] auto contains(SolverLiteral lit) const -> bool {
        return Detail::call<clingo_assignment_has_literal>(assignment_, lit);
    }
 
    [[nodiscard]] auto is_false(SolverLiteral lit) const -> bool {
        return Detail::call<clingo_assignment_is_false>(assignment_, lit);
    }
 
    [[nodiscard]] auto is_fixed(SolverLiteral lit) const -> bool {
        return Detail::call<clingo_assignment_is_fixed>(assignment_, lit);
    }
 
    [[nodiscard]] auto is_free(SolverLiteral lit) const -> bool {
        return Detail::call<clingo_assignment_truth_value>(assignment_, lit) == clingo_truth_value_free;
    }
 
    [[nodiscard]] auto is_true(SolverLiteral lit) const -> bool {
        return Detail::call<clingo_assignment_is_true>(assignment_, lit);
    }
 
    [[nodiscard]] auto is_total() const -> bool { return Detail::call<clingo_assignment_is_total>(assignment_); }
 
    [[nodiscard]] auto level(SolverLiteral lit) const -> ProgramId {
        return Detail::call<clingo_assignment_level>(assignment_, lit);
    }
 
    [[nodiscard]] auto value(SolverLiteral lit) const -> std::optional<bool> {
        clingo_truth_value_t res = Detail::call<clingo_assignment_truth_value>(assignment_, lit);
        switch (res) {
            case clingo_truth_value_true: {
                return true;
            }
            case clingo_truth_value_false: {
                return false;
            }
            default: {
                return std::nullopt;
            }
        }
    }
 
    [[nodiscard]] auto root_level() const -> ProgramId {
        return Detail::call<clingo_assignment_root_level>(assignment_);
    }
 
    [[nodiscard]] auto trail() const -> Trail { return Trail{assignment_}; }
 
    [[nodiscard]] auto begin() const -> iterator { return iterator{*this, 0}; }
 
    [[nodiscard]] auto end() const -> iterator { return iterator{*this, size()}; }
 
  private:
    clingo_assignment_t const *assignment_;
};
 
class PropagateControl {
  public:
    explicit PropagateControl(clingo_propagate_control_t *ctl) : ctl_{ctl} {}
    explicit PropagateControl(clingo_propagate_init_t *init)
        : PropagateControl(Detail::call<clingo_propagate_init_control>(init)) {}
 
    [[nodiscard]] auto add_literal(bool freeze = true) const -> SolverLiteral {
        return Detail::call<clingo_propagate_control_add_literal>(ctl_, freeze);
    }
 
    [[nodiscard]] auto add_clause(SolverLiteralSpan literals, ClauseFlags flags = ClauseFlags::none) const -> bool {
        return Detail::call<clingo_propagate_control_add_clause>(ctl_, literals.data(), literals.size(),
                                                                 static_cast<clingo_clause_type_t>(flags));
    }
 
    [[nodiscard]] auto add_clause(SolverLiteralList literals, ClauseFlags flags = ClauseFlags::none) const -> bool {
        return add_clause(SolverLiteralSpan{literals}, flags);
    }
 
    [[nodiscard]] auto add_weight_constraint(SolverLiteral literal, WeightedLiteralSpan literals, Weight bound,
                                             WeightConstraintType type) const -> bool {
        return Detail::call<clingo_propagate_control_add_weight_constraint>(ctl_, literal, literals.data(),
                                                                            literals.size(), bound, type);
    }
 
    [[nodiscard]] auto add_nogood(SolverLiteralSpan literals, ClauseFlags flags = ClauseFlags::none) const -> bool {
        return add_clause(Detail::transform(literals, [](auto const &lit) { return -lit; }), flags);
    }
 
    void add_watch(SolverLiteral literal) const {
        Detail::handle_error(clingo_propagate_control_add_watch(ctl_, literal));
    }
 
    [[nodiscard]] auto has_watch(SolverLiteral literal) const -> bool {
        return Detail::call<clingo_propagate_control_has_watch>(ctl_, literal);
    }
 
    void remove_watch(SolverLiteral lit) const {
        Detail::handle_error(clingo_propagate_control_remove_watch(ctl_, lit));
    }
 
    [[nodiscard]] auto propagate() const -> bool { return Detail::call<clingo_propagate_control_propagate>(ctl_); }
 
  private:
    clingo_propagate_control_t *ctl_;
};
 
class PropagateInit : public PropagateControl {
  public:
    explicit PropagateInit(clingo_propagate_init_t *init) : PropagateControl(init), init_{init} {}
 
    [[nodiscard]] auto library() const -> Library {
        return Library{Detail::call<clingo_propagate_init_library>(init_), true};
    }
 
    [[nodiscard]] auto base() const -> Base { return Base{Detail::call<clingo_propagate_init_base>(init_)}; }
 
    [[nodiscard]] auto check_mode() const -> PropagatorCheckMode {
        return static_cast<PropagatorCheckMode>(Detail::call<clingo_propagate_init_get_check_mode>(init_));
    }
 
    void check_mode(PropagatorCheckMode mode) {
        Detail::handle_error(
            clingo_propagate_init_set_check_mode(init_, static_cast<clingo_propagator_check_mode_t>(mode)));
    }
 
    [[nodiscard]] auto number_of_threads() const -> ProgramId {
        return Detail::call<clingo_propagate_init_number_of_threads>(init_);
    }
 
    [[nodiscard]] auto undo_mode() const -> PropagatorUndoMode {
        return static_cast<PropagatorUndoMode>(Detail::call<clingo_propagate_init_get_undo_mode>(init_));
    }
 
    void undo_mode(PropagatorUndoMode mode) const {
        Detail::handle_error(
            clingo_propagate_init_set_undo_mode(init_, static_cast<clingo_propagator_undo_mode_t>(mode)));
    }
 
    [[nodiscard]] auto solver_literal(ProgramLiteral literal) const -> SolverLiteral {
        return Detail::call<clingo_propagate_init_solver_literal>(init_, literal);
    }
 
    void add_minimize(SolverLiteral literal, Weight weight, Weight priority) const {
        Detail::handle_error(clingo_propagate_init_add_minimize(init_, literal, weight, priority));
    }
 
    void freeze_literal(SolverLiteral literal) const {
        Detail::handle_error(clingo_propagate_init_freeze_literal(init_, literal));
    }
 
  private:
    clingo_propagate_init_t *init_;
};
 
class Propagator {
  public:
    Propagator() = default;
    Propagator(Propagator &&other) = delete;
    auto operator=(Propagator &&other) -> Propagator & = delete;
    virtual ~Propagator() = default;
 
    void init(Assignment assignment, PropagateInit init) { do_init(assignment, init); }
    void attach(Assignment assignment, PropagateControl ctl) { do_attach(assignment, ctl); }
 
    void propagate(Assignment assignment, PropagateControl ctl, ProgramLiteralSpan changes) {
        do_propagate(assignment, ctl, changes);
    }
 
    void undo(Assignment assignment, ProgramLiteralSpan changes) { do_undo(assignment, changes); }
 
    void check(Assignment assignment, PropagateControl ctl) { do_check(assignment, ctl); }
 
  private:
    virtual void do_init([[maybe_unused]] Assignment assignment, [[maybe_unused]] PropagateInit init) {}
    virtual void do_attach([[maybe_unused]] Assignment assignment, [[maybe_unused]] PropagateControl ctl) {}
    virtual void do_propagate([[maybe_unused]] Assignment assignment, [[maybe_unused]] PropagateControl ctl,
                              [[maybe_unused]] ProgramLiteralSpan changes) {}
    virtual void do_undo([[maybe_unused]] Assignment assignment, [[maybe_unused]] ProgramLiteralSpan changes) {}
    virtual void do_check([[maybe_unused]] Assignment assignment, [[maybe_unused]] PropagateControl ctl) {}
};
 
class Heuristic : public Propagator {
  public:
    Heuristic() = default;
 
    auto decide(Assignment assignment, SolverLiteral literal) -> SolverLiteral {
        return do_decide(assignment, literal);
    }
 
  private:
    virtual auto do_decide([[maybe_unused]] Assignment assignment, clingo_literal_t literal) -> clingo_literal_t {
        return literal;
    }
};
 
 
namespace Detail {
 
inline static constexpr auto c_propagator = clingo_propagator_t{
    [](clingo_assignment_t const *assignment, clingo_propagate_init_t *init, void *data) -> bool {
        auto &self = *static_cast<Propagator *>(data);
        CLINGO_TRY {
            self.init(Assignment{assignment}, PropagateInit{init});
        }
        CLINGO_CATCH;
    },
    [](clingo_assignment_t const *assignment, clingo_propagate_control_t *control, void *data) {
        auto &self = *static_cast<Propagator *>(data);
        CLINGO_TRY {
            self.attach(Assignment{assignment}, PropagateControl{control});
        }
        CLINGO_CATCH;
    },
    [](clingo_assignment_t const *assignment, clingo_propagate_control_t *control, clingo_literal_t const *changes,
       size_t size, void *data) -> bool {
        auto &self = *static_cast<Propagator *>(data);
        CLINGO_TRY {
            self.propagate(Assignment{assignment}, PropagateControl{control}, SolverLiteralSpan{changes, size});
        }
        CLINGO_CATCH;
    },
    [](clingo_assignment_t const *assignment, clingo_literal_t const *changes, size_t size, void *data) {
        auto &self = *static_cast<Propagator *>(data);
        try {
            self.undo(Assignment{assignment}, SolverLiteralSpan{changes, size});
        } catch (std::exception const &e) {
            printf("panic: %s\n", e.what());
            std::abort();
        }
    },
    [](clingo_assignment_t const *assignment, clingo_propagate_control_t *control, void *data) -> bool {
        auto &self = *static_cast<Propagator *>(data);
        CLINGO_TRY {
            self.check(Assignment{assignment}, PropagateControl{control});
        }
        CLINGO_CATCH;
    },
    nullptr,
    [](void *data) { std::ignore = std::unique_ptr<Propagator>(static_cast<Propagator *>(data)); },
};
 
inline static constexpr auto c_heuristic = clingo_propagator_t{
    c_propagator.init,
    c_propagator.attach,
    c_propagator.propagate,
    c_propagator.undo,
    c_propagator.check,
    [](clingo_assignment_t const *assignment, clingo_literal_t fallback, void *data,
       clingo_literal_t *decision) -> bool {
        auto &self = *static_cast<Propagator *>(data);
        CLINGO_TRY {
            // NOLINTBEGIN
            *decision = static_cast<Heuristic &>(self).decide(Assignment{assignment}, fallback);
            // NOLINTEND
        }
        CLINGO_CATCH;
    },
    c_propagator.free,
};
 
} // namespace Detail
 
} // namespace Clingo