grounder.hh

#pragma once
 
#include <clingo/control/context.hh>
#include <clingo/control/parse.hh>
 
#include <clingo/input/program.hh>
 
#include <clingo/core/output.hh>
 
namespace CppClingo::Control {
 
 
struct GroundOptions {
    EstimateFunction fun = EstimateFunction::average;
    EstimateSelector sel = EstimateSelector::pred;
};
 
class Grounder {
  public:
    Grounder(Grounder const &) = delete;
    Grounder(Grounder &&) = delete;
    auto operator=(Grounder const &) -> Grounder & = delete;
    auto operator=(Grounder &&) -> Grounder & = delete;
 
    struct Impl;
    Grounder(Logger &log, SymbolStore &store, Input::RewriteOptions const &opts, GroundOptions const &gopts,
             OutputStm &out);
    ~Grounder() noexcept;
    void join(Input::UnprocessedProgram const &prg);
    auto parse(std::string_view str, Ground::ScriptExec *code = nullptr, ProgramBackend *prg = nullptr,
               TheoryBackend *thy = nullptr) -> BuiltinIncludes;
    auto parse(std::span<std::string_view const> const &files, Ground::ScriptExec *code = nullptr,
               ProgramBackend *prg = nullptr, TheoryBackend *thy = nullptr) -> BuiltinIncludes;
    void add_const(String name, Symbol value);
    auto const_map() -> Input::ConstMap const &;
    void mark_unsat();
    [[nodiscard]] auto ground(ProgramParamVec const &params, Ground::ScriptCallback *context = nullptr,
                              Util::StopFlag *stop = nullptr) -> GroundResult;
    void print_summary(bool final);
    void accept(Ground::ProfileNode::Visitor const &visit) const;
 
    void output_unprocessed_program(std::ostream &out);
    void output_program(std::ostream &out);
    void show(Input::SharedSig const &sig);
    void mark_sig(Input::Sig const &sig);
 
    [[nodiscard]] auto get_parts() -> std::optional<Input::StmParts> const &;
    void set_parts(std::optional<Input::StmParts> parts);
    [[nodiscard]] auto base() -> Ground::Bases &;
    [[nodiscard]] auto base() const -> Ground::Bases const &;
    [[nodiscard]] auto store() const -> SymbolStore &;
    [[nodiscard]] auto log() const -> Logger &;
 
  private:
    void prepare_();
 
    std::unique_ptr<Impl> impl_;
};
 
 
} // namespace CppClingo::Control