solver.hh

#pragma once
 
#include <clingo/control/grounder.hh>
 
#include <clingo/output/backend.hh>
 
#include <clasp/clasp_facade.h>
#include <clasp/cli/clasp_options.h>
 
namespace CppClingo::Control {
 
 
class Solver;
 
class Script : public Ground::ScriptCallback {
  public:
    void main(Solver &slv) { do_main(slv); }
    void exec(std::string_view code) { do_exec(code); }
 
  private:
    virtual void do_exec(std::string_view code) = 0;
    virtual void do_main(Solver &slv) = 0;
};
using UScript = std::unique_ptr<Script>;
 
class Scripts : public Ground::ScriptCallback, public Ground::ScriptExec {
  public:
    void register_script(std::string_view name, UScript script);
    void main(Solver &slv);
 
  private:
    void do_exec(Location const &loc, Logger &log, std::string_view name, std::string_view code) override;
    auto do_callable(std::string_view name, size_t args) -> bool override;
    void do_call(Location const &loc, std::string_view name, SymbolSpan args, SymbolVec &out) override;
 
    std::vector<std::pair<std::string, UScript>> scripts_;
};
 
enum class IStop : uint8_t {
    none,   
    sat,    
    unsat,  
    unknown 
};
 
enum class AppMode : uint8_t {
    parse,   
    rewrite, 
    ground,  
    solve    
};
 
struct SolverOptions {
    AppMode mode = AppMode::solve;
    size_t imin = 0;
    std::optional<size_t> imax = std::nullopt;
    IStop istop = IStop::sat;
    bool single_shot = false;
    bool profile = false;
};
 
enum class SymbolSelectFlags : uint8_t {
    none = 0,   
    shown = 1,  
    atoms = 2,  
    terms = 4,  
    theory = 8, 
    all = 15,   
};
CLINGO_ENABLE_BITSET_ENUM(SymbolSelectFlags);
 
enum class ModelType : uint8_t {
    model = 0,                
    brave_consequences = 1,   
    cautious_consequences = 2 
};
 
enum class ConsequenceType : uint8_t {
    false_ = 0, 
    true_ = 1,  
    unknown = 2 
};
 
class TermBaseMap {
  public:
    using Map = Util::ordered_map<SharedSymbol, prg_id_t>;
 
    template <class F> auto add(Symbol sym, F &&fun) -> prg_id_t {
        auto [it, ins] = map_.emplace(sym, 0);
        if (ins) {
            it.value() = std::invoke(std::forward<F>(fun));
        }
        return it.value();
    }
 
    void add(Symbol sym, prg_id_t id) {
        if (!map_.emplace(sym, id).second) {
            throw std::runtime_error("collision of term ids");
        }
    }
 
    [[nodiscard]] auto term_id(size_t i) const -> prg_id_t {
        if (i < size()) {
            return map_.nth(i).value();
        }
        throw std::range_error{"index out of range"};
    }
 
    [[nodiscard]] auto symbol(size_t i) const -> Symbol {
        if (i < size()) {
            return *map_.nth(i).key();
        }
        throw std::range_error{"index out of range"};
    }
 
    [[nodiscard]] auto index(Symbol sym) const -> size_t { return map_.find(sym) - map_.begin(); }
 
    [[nodiscard]] auto size() const -> size_t { return map_.size(); }
 
    [[nodiscard]] auto begin() const -> Map::const_iterator { return map_.cbegin(); }
 
    [[nodiscard]] auto end() const -> Map::const_iterator { return map_.cend(); }
 
  private:
    Util::ordered_map<SharedSymbol, prg_id_t> map_;
};
 
class BaseView {
  public:
    virtual ~BaseView() = default;
    [[nodiscard]] auto bases() const -> Ground::Bases const & { return do_bases(); }
    [[nodiscard]] auto term_base() const -> TermBaseMap const & { return do_term_base(); }
    [[nodiscard]] auto clasp_program() const -> Clasp::Asp::LogicProgram const & { return do_clasp_program(); }
    [[nodiscard]] auto clasp_theory() const -> Potassco::TheoryData const & { return clasp_program().theoryData(); }
 
  private:
    [[nodiscard]] virtual auto do_bases() const -> Ground::Bases const & = 0;
    [[nodiscard]] virtual auto do_term_base() const -> TermBaseMap const & = 0;
    [[nodiscard]] virtual auto do_clasp_program() const -> Clasp::Asp::LogicProgram const & = 0;
};
 
class SolveControl : public BaseView {
  public:
    void add_clause(PrgLitSpan lits) { do_add_clause(lits); }
 
  private:
    virtual void do_add_clause(PrgLitSpan lits) = 0;
};
 
class Model {
  public:
    virtual ~Model() = default;
 
    void symbols(SymbolSelectFlags type, SymbolVec &res) const { do_symbols(type, res); }
    [[nodiscard]] auto number() const -> uint64_t { return do_number(); }
    [[nodiscard]] auto type() const -> ModelType { return do_type(); }
    [[nodiscard]] auto contains(Symbol sym) const -> bool { return do_contains(sym); }
    [[nodiscard]] auto is_true(prg_lit_t lit) const -> bool { return do_is_true(lit); }
    [[nodiscard]] auto is_consequence(prg_lit_t lit) const -> ConsequenceType { return do_is_consequence(lit); }
    [[nodiscard]] auto costs() const -> std::span<prg_sum_t const> { return do_costs(); }
    [[nodiscard]] auto priorities() const -> std::span<prg_weight_t const> { return do_priorities(); }
    [[nodiscard]] auto optimality_proven() const -> bool { return do_optimality_proven(); }
    [[nodiscard]] auto thread_id() const -> prg_id_t { return do_thread_id(); }
    [[nodiscard]] auto context() -> SolveControl & { return do_control(); }
 
    virtual void extend(SymbolSpan symbols) { do_extend(symbols); }
 
  private:
    virtual void do_symbols(SymbolSelectFlags type, SymbolVec &res) const = 0;
    [[nodiscard]] virtual auto do_number() const -> uint64_t = 0;
    [[nodiscard]] virtual auto do_type() const -> ModelType = 0;
    [[nodiscard]] virtual auto do_contains(Symbol sym) const -> bool = 0;
    virtual void do_extend(SymbolSpan symbols) = 0;
    [[nodiscard]] virtual auto do_is_true(prg_lit_t lit) const -> bool = 0;
    [[nodiscard]] virtual auto do_is_consequence(prg_lit_t lit) const -> ConsequenceType = 0;
    [[nodiscard]] virtual auto do_costs() const -> std::span<prg_sum_t const> = 0;
    [[nodiscard]] virtual auto do_priorities() const -> std::span<prg_weight_t const> = 0;
    [[nodiscard]] virtual auto do_optimality_proven() const -> bool = 0;
    [[nodiscard]] virtual auto do_thread_id() const -> prg_id_t = 0;
    [[nodiscard]] virtual auto do_control() -> SolveControl & = 0;
};
using UModel = std::unique_ptr<Model>;
 
enum class SolveResult : uint8_t {
    empty = 0,         
    satisfiable = 1,   
    unsatisfiable = 2, 
    exhausted = 4,     
    interrupted = 8,   
};
CLINGO_ENABLE_BITSET_ENUM(SolveResult);
 
class SolveHandle {
  public:
    virtual ~SolveHandle() = default;
 
    auto get() -> SolveResult { return do_get(); }
    void cancel() { do_cancel(); }
    void resume() { do_resume(); }
    auto model() -> Model const * { return do_model(); }
    auto last() -> Model const * { return do_last(); }
    auto core() -> PrgLitSpan { return do_core(); }
    auto wait(double timeout) -> bool { return do_wait(timeout); }
 
  private:
    virtual auto do_get() -> SolveResult = 0;
    virtual void do_cancel() = 0;
    virtual void do_resume() = 0;
    virtual auto do_model() -> Model const * = 0;
    virtual auto do_last() -> Model const * = 0;
    virtual auto do_core() -> PrgLitSpan = 0;
    virtual auto do_wait(double timeout) -> bool = 0;
};
using USolveHandle = std::unique_ptr<SolveHandle>;
 
class EventHandler {
  public:
    virtual ~EventHandler() = default;
 
    auto on_model(Model &mdl) -> bool { return do_on_model(mdl); }
    void on_stats(Potassco::AbstractStatistics &stats) { do_on_stats(stats); }
    void on_unsat(Clasp::SumView bound) { do_on_unsat(bound); }
    void on_core(Potassco::LitSpan core) { do_on_core(core); }
    void on_finish(SolveResult result) { do_on_finish(result); }
 
  private:
    virtual auto do_on_model([[maybe_unused]] Model &mdl) -> bool { return true; }
    virtual void do_on_stats([[maybe_unused]] Potassco::AbstractStatistics &stats) {}
    virtual void do_on_unsat([[maybe_unused]] Clasp::SumView bound) {}
    virtual void do_on_core([[maybe_unused]] Potassco::LitSpan core) {}
    virtual void do_on_finish([[maybe_unused]] SolveResult result) {}
};
using UEventHandler = std::unique_ptr<EventHandler>;
 
enum class SolveMode : uint8_t {
    none = 0,  
    async = 1, 
    yield = 2, 
};
CLINGO_ENABLE_BITSET_ENUM(SolveMode);
 
class BackendHandle {
  public:
    [[nodiscard]] auto program() -> Clasp::Asp::LogicProgram & { return do_program(); }
    [[nodiscard]] auto theory() -> Output::TheoryData & { return do_theory(); }
    [[nodiscard]] auto store() -> SymbolStore & { return do_store(); }
    [[nodiscard]] auto add_atom(Symbol atom) -> prg_lit_t { return do_add_atom(atom); }
    void close() { do_close(); }
    virtual ~BackendHandle() = default;
 
  private:
    virtual auto do_program() -> Clasp::Asp::LogicProgram & = 0;
    virtual auto do_theory() -> Output::TheoryData & = 0;
    virtual auto do_store() -> SymbolStore & = 0;
    virtual auto do_add_atom(Symbol atom) -> prg_lit_t = 0;
    virtual void do_close() = 0;
};
using UBackendHandle = std::unique_ptr<BackendHandle>;
 
class Propagator : public Potassco::AbstractPropagator, public Potassco::AbstractHeuristic {
  public:
    [[nodiscard]] virtual auto hasHeuristic() const -> bool = 0;
};
using UPropagator = std::unique_ptr<Propagator>;
 
class CallbackLock {
  public:
    void lock() {
        if (mut_) {
            mut_->lock();
        }
    }
    void unlock() {
        if (mut_) {
            mut_->unlock();
        }
    }
    void enable(bool state) {
        if (!state) {
            mut_.reset();
        } else if (!mut_) {
            mut_.emplace();
            mut_->lock();
        }
    }
 
  private:
    std::optional<std::mutex> mut_;
};
 
template <class M> class unlock_guard {
  public:
    explicit unlock_guard(M &mut) : mut_{&mut} { mut_->unlock(); }
    unlock_guard(const unlock_guard &) = delete;
    ~unlock_guard() { mut_->lock(); }
    auto operator=(const unlock_guard &) -> unlock_guard & = delete;
 
  private:
    M *mut_;
};
 
class SymbolTable {
  public:
    void init(CppClingo::Control::BaseView &view, std::ostream &out);
    void begin_step();
    void end_step();
    auto out() -> std::ostream & { return *out_; }
 
  private:
    struct State {
        State() = default;
        size_t atom : 1 = 0;
        size_t term : 1 = 0;
        size_t index : (8 * sizeof(size_t)) - 2 = 0;
    };
 
    auto output(CppClingo::Symbol const &sym) -> State &;
 
    CppClingo::Control::BaseView *view_ = nullptr;
    std::ostream *out_ = nullptr;
    size_t ids_ = 0;
    std::vector<size_t> buf_;
    CppClingo::Util::unordered_map<CppClingo::SharedSymbol, State> done_;
};
using USymbolTable = std::unique_ptr<SymbolTable>;
 
class Solver : public BaseView {
  public:
    Solver(Clasp::ClaspFacade &clasp, Clasp::Cli::ClaspCliConfig &config, Logger &log, SymbolStore &store,
           Scripts &scripts, Input::RewriteOptions ropts, SolverOptions sopts, FILE *out = stdout);
 
    void main(std::span<std::string_view const> const &files);
    void main();
 
    void join(Input::UnprocessedProgram const &prg);
    void parse(std::string_view str);
    void parse(std::span<std::string_view const> const &files);
    void parse_with(std::function<void(ProgramBackend *, TheoryBackend *)> cb);
 
    void add_const(String name, Symbol value);
    [[nodiscard]] auto const_map() -> Input::ConstMap const &;
    void ground(ProgramParamVec const &params, Ground::ScriptCallback *ctx);
    auto solve(UEventHandler handler = {}, PrgLitSpan assumptions = {}, SolveMode mode = SolveMode::none)
        -> USolveHandle;
 
    void output_unprocessed_program(std::ostream &out);
 
    void output_program(std::ostream &out);
 
    auto map_model(Clasp::Model const &mdl) -> Model &;
 
    [[nodiscard]] auto buf() -> Util::OutputBuffer & { return buf_; };
 
    [[nodiscard]] auto backend() -> UBackendHandle;
 
    [[nodiscard]] auto clasp_facade() -> Clasp::ClaspFacade & { return *clasp_; }
 
    [[nodiscard]] auto clasp_facade() const -> Clasp::ClaspFacade const & { return *clasp_; }
 
    [[nodiscard]] auto clasp_config() -> Clasp::Cli::ClaspCliConfig & {
        return clasp_config_ != nullptr ? *clasp_config_ : throw std::runtime_error("not in solving mode");
    }
 
    [[nodiscard]] auto clasp_stats() -> Potassco::AbstractStatistics const & {
        auto const *stats = clasp_->getStats();
        return stats != nullptr ? *stats : throw std::runtime_error("not in solving mode");
    }
 
    void register_propagator(UPropagator propagator);
 
    auto get_lock() -> CallbackLock & { return lock_; }
 
    void block_main(bool block) { block_main_ = block; }
 
    [[nodiscard]] auto get_mode() const -> AppMode { return opts_.mode; }
 
    auto user_data() -> void *& { return data_; }
 
    void interrupt() noexcept;
 
    [[nodiscard]] auto get_parts() -> std::optional<Input::StmParts> const & { return grd_.get_parts(); }
 
    void set_parts(std::optional<Input::StmParts> parts) { grd_.set_parts(std::move(parts)); }
    void set_parts(Input::ProgramParamVec parts) {
        auto pos = Position{*grd_.store().string("<cmd>"), 1, 1};
        auto loc = Location{pos, pos};
        grd_.set_parts(std::make_optional<Input::StmParts>(loc, Input::Precedence::override_, std::move(parts)));
    }
 
    void show(Input::SharedSig const &sig) { grd_.show(sig); }
 
    auto sym_tab() -> SymbolTable & {
        if (!sym_tab_) {
            sym_tab_ = std::make_unique<SymbolTable>();
        }
        return *sym_tab_;
    }
 
  private:
    class ProgramBackendAdapter;
 
    enum class State : uint8_t {
        initial,  //< initial step
        grounded, //< step has been grounded
        prepared, //< step is prepared for solving
        solved,   //< step has been solved
    };
 
    auto make_output_(SymbolStore &store, AppMode mode) -> UOutputStm;
 
    void prepare_();
 
    void simplify_();
 
    void enable_updates_();
 
    [[nodiscard]] auto do_bases() const -> Ground::Bases const & override { return grd_.base(); }
 
    [[nodiscard]] auto do_term_base() const -> TermBaseMap const & override { return terms_; }
 
    [[nodiscard]] auto do_clasp_program() const -> Clasp::Asp::LogicProgram const & override {
        return clasp_->asp() != nullptr ? *clasp_->asp() : throw std::runtime_error("not in solving mode");
    }
 
    void incmode_();
 
    CallbackLock lock_;
    std::vector<UPropagator> propagators_;
    TermBaseMap terms_;
    Clasp::ClaspFacade *clasp_;
    Clasp::Cli::ClaspCliConfig *clasp_config_;
    Util::OutputBuffer buf_;
    UProgramBackend backend_;
    std::unique_ptr<Output::TheoryData> theory_;
    UOutputStm out_;
    UModel mdl_;
    USymbolTable sym_tab_;
    Grounder grd_;
    Scripts *scripts_;
    State state_ = State::initial;
    SolverOptions opts_;
    BuiltinIncludes includes_ = BuiltinIncludes::empty;
    void *data_ = nullptr;
    bool block_main_ = false;
};
 
 
} // namespace CppClingo::Control