Extend ground output options wip

lib/c-api/src/control.cc

@@ -44,16 +44,16 @@ extern "C" auto clingo_control_new(clingo_lib_t *lib, clingo_string_t const *arg
         auto ctx = OptionContext{"<libclingo>"};
         opts.init(ctx);
         auto group_basic = OptionGroup{"Basic Options"};
+
+        auto parse_mode = [&opts](std::string_view str) { return opts.init_app_mode(str); };
+
         group_basic.addOptions() //
-            ("mode",
-             storeTo(opts.mode() = CppClingo::Control::AppMode::solve,
-                     values<CppClingo::Control::AppMode>({
-                         {"parse", CppClingo::Control::AppMode::parse},
-                         {"rewrite", CppClingo::Control::AppMode::rewrite},
-                         {"ground", CppClingo::Control::AppMode::ground},
-                         {"solve", CppClingo::Control::AppMode::solve},
-                     })),
-             "Run in {parse|rewrite|ground|solve} mode");
+            ("mode", parse(parse_mode),
+             "Run in the specified mode\n"
+             "      %A: <mode {parse|rewrite|solve}>\n"
+             "        parse   : Stop processing after parsing\n"
+             "        rewrite : Stop processing after rewriting\n"
+             "        solve   : Stop processing after solving");
         ctx.add(group_basic);
         slv_cfg->addOptions(ctx);
         auto pos_parser = [](std::string_view str, std::string &out) {
@@ -75,6 +75,7 @@ extern "C" auto clingo_control_new(clingo_lib_t *lib, clingo_string_t const *arg
         DefaultParseContext pc{ctx};
         parseCommandArray(pc, {cargs.data(), size}, pos_parser);
         ctx.assignDefaults(pc.parsed());
+        opts.validate_options(pc.parsed());
         slv_cfg->finalize(pc.parsed(), Clasp::ProblemType::asp, true);
 
         // setup control

lib/c-api/src/main.cc

@@ -174,31 +174,48 @@ class ClingoApp : public Clasp::Cli::ClaspAppBase {
         BaseType::initOptions(root);
         opts_.init(root);
         auto group_basic = OptionGroup{"Basic Options"};
+
+        auto parse_mode = [this](std::string_view str) {
+            if (opts_.init_app_mode(str)) {
+                mode_ = static_cast<Mode>(opts_.mode());
+                return true;
+            }
+            if (str == "clasp") {
+                mode_ = Mode::clasp;
+                return true;
+            }
+            return false;
+        };
+
         group_basic.addOptions() //
-            ("mode",
-             storeTo(mode_ = Mode::solve, values<Mode>({
-                                              {"parse", Mode::parse},
-                                              {"rewrite", Mode::rewrite},
-                                              {"ground", Mode::ground},
-                                              {"solve", Mode::solve},
-                                              {"clasp", Mode::clasp},
-                                          })),
-             "Run in {parse|rewrite|ground|solve|clasp} mode");
+            ("mode", parse(parse_mode),
+             "Run in the specified mode\n"
+             "      %A: <mode {parse|rewrite|solve|clasp}>\n"
+             "        parse   : Stop processing after parsing\n"
+             "        rewrite : Stop processing after rewriting\n"
+             "        solve   : Stop processing after solving\n"
+             "        clasp   : Invoke clasp on the input");
         root.add(group_basic);
         app_.register_options(root);
     }
 
     void validateOptions(const Potassco::ProgramOptions::OptionContext &root,
                          const Potassco::ProgramOptions::ParsedOptions &parsed) override {
         BaseType::validateOptions(root, parsed);
+        opts_.validate_options(parsed);
+        // --convert may redefine execution mode (e.g., text -> ground)
+        if (parsed.contains("convert")) {
+            mode_ = static_cast<Mode>(opts_.mode());
+        }
         setExitCode(Clasp::Cli::exit_no_run);
         app_.validate_options();
         setExitCode(0);
     }
 
     auto createOutput(Clasp::Cli::OutputSink sink, ProblemType f, Clasp::Cli::ClaspAppOptions::OutputFormat outf)
         -> std::unique_ptr<Clasp::Cli::Output> override {
-        if (mode_ != Mode::solve && mode_ != Mode::clasp) {
+        if ((mode_ != Mode::solve && mode_ != Mode::clasp) ||
+            opts_.backend_type() != CppClingo::Control::BackendType::clasp) {
             return nullptr;
         }
         auto om = mode_ == Mode::clasp ? Clasp::Cli::Output::mode_default : Clasp::Cli::Output::mode_clingo;

lib/c-api/src/opts.hh

@@ -171,6 +171,42 @@ class ClingoOptions {
             }
             return true;
         };
+        auto parse_convert = [this](std::string_view str) {
+            namespace Parse = Potassco::Parse;
+            using namespace std::literals;
+
+            if (auto key = "text"sv; Parse::eqIgnoreCase(str, key, key.size())) {
+                solver_opts_.mode = Control::AppMode::ground;
+                return str.size() == key.size();
+            }
+
+            Control::BackendType backend_type{};
+            Control::ReifyFlags reify_flags{};
+
+            if (!Parse::ok(Potassco::extract(str, backend_type))) {
+                return false;
+            }
+            if (backend_type == Control::BackendType::reify) {
+                while (Parse::matchOpt(str, ',')) {
+                    if (auto key = "sccs"sv; Parse::eqIgnoreCase(str, key, key.size())) {
+                        reify_flags |= Control::ReifyFlags::reify_scc;
+                        str.remove_prefix(key.size());
+                    } else if (key = "steps"sv; Parse::eqIgnoreCase(str, key, key.size())) {
+                        reify_flags |= Control::ReifyFlags::reify_step;
+                        str.remove_prefix(key.size());
+                    } else {
+                        break;
+                    }
+                }
+            }
+            if (str.empty()) {
+                solver_opts_.mode = Control::AppMode::solve;
+                solver_opts_.backend_type = backend_type;
+                solver_opts_.reify_flags = reify_flags;
+                return true;
+            }
+            return false;
+        };
 
         auto group_grounder = OptionGroup{"Grounder Options"};
         group_grounder.addOptions() //
@@ -219,7 +255,16 @@ class ClingoOptions {
       [no-]atom-undefined     : a :- b.
       [no-]file-included      : #include "a.lp". #include "a.lp".
       [no-]operation-undefined: p(1/0).
-      [no-]global-variable    : :- #count { X } = 1, X = 1.)");
+      [no-]global-variable    : :- #count { X } = 1, X = 1.)")                                     //
+            ("convert", parse(parse_convert),
+             "Convert to specified format\n"
+             "      %A: <format {text|aspif|smodels|reify}[,<opts>]>\n"
+             "        text   : Print program in text format (ground)\n"
+             "        aspif  : Print program in ASP intermediate format\n"
+             "        smodels: Print program in smodels format\n"
+             "        reify  : Print program as reified facts with <opts>\n"
+             "          sccs  : Compute and print SCCs\n"
+             "          steps : Add step numbers");
         root.add(group_basic);
     }
 
@@ -237,7 +282,28 @@ class ClingoOptions {
         }
     }
 
+    auto init_app_mode(std::string_view str) -> bool {
+        namespace Parse = Potassco::Parse;
+
+        Control::AppMode mode;
+        if (not Parse::ok(Potassco::extract(str, mode))) {
+            return false;
+        }
+        if (str.empty()) {
+            solver_opts_.mode = mode;
+            return true;
+        }
+        return false;
+    }
+
+    void validate_options(const Potassco::ProgramOptions::ParsedOptions &parsed) {
+        if (parsed.contains("mode") && parsed.contains("convert")) {
+            throw std::invalid_argument("option '--mode' and '--convert' cannot be used together");
+        }
+    }
+
     auto mode() -> Control::AppMode & { return solver_opts_.mode; }
+    auto backend_type() -> Control::BackendType & { return solver_opts_.backend_type; }
 
     auto rewrite_options() -> Input::RewriteOptions const & { return rewrite_opts_; }
     auto solver_options() -> Control::SolverOptions const & { return solver_opts_; }

lib/control/include/clingo/control/solver.hh

@@ -66,11 +66,33 @@ enum class AppMode : uint8_t {
     ground,  //!< Stop processing after grounding.
     solve    //!< Stop processing after solving.
 };
+POTASSCO_SET_ENUM_ENTRIES(AppMode, {parse, "parse"sv}, {rewrite, "rewrite"sv}, {ground, "ground"sv},
+                          {solve, "solve"sv});
+
+//! Enumeration of available output formats when in solving mode.
+enum class BackendType : uint8_t {
+    clasp,   //!< Standard solving mode: use the normal backend (Clasp)
+    aspif,   //!< Print program in ASP intermediate format
+    smodels, //!< Print program in smodels format
+    reify    //!< Print program as reified facts
+};
+POTASSCO_SET_ENUM_ENTRIES(BackendType, {aspif, "aspif"sv}, {smodels, "smodels"sv}, {reify, "reify"sv});
+
+//! Options for reification.
+enum class ReifyFlags : uint8_t {
+    reify_scc = 1U, //!< Compute and print SCCs
+    reify_step = 2U //!< Add step numbers
+};
+POTASSCO_ENABLE_BIT_OPS(ReifyFlags);
 
 //! Options for the solver.
 struct SolverOptions {
     //! Operation mode of the solver.
     AppMode mode = AppMode::solve;
+    //! Output format to use when in solving mode.
+    BackendType backend_type = BackendType::clasp;
+    //! Reification flags.
+    ReifyFlags reify_flags = {};
     //! The minimum number of incremental steps.
     size_t imin = 0;
     //! The maximum number of incremental steps.
@@ -817,8 +839,10 @@ class Solver : public BaseView {
     //! the backend for the clasp output.
     //!
     //! @param mode the configured output mode
+    //! @param backend_type the configured backend type to use when in solving mode
+    //! @param reify_flags the flag defining options for the reification backend
     //! @return the resulting output
-    auto make_output_(SymbolStore &store, AppMode mode) -> UOutputStm;
+    auto make_output_(SymbolStore &store, AppMode mode, BackendType backend_type, ReifyFlags reify_flags) -> UOutputStm;
 
     //! Prepare the solver for grounding.
     void prepare_();
@@ -847,6 +871,7 @@ class Solver : public BaseView {
     Util::OutputBuffer buf_;
     UProgramBackend backend_;
     std::unique_ptr<Output::TheoryData> theory_;
+    std::unique_ptr<Potassco::AbstractProgram> program_;
     UOutputStm out_;
     UModel mdl_;
     USymbolTable sym_tab_;

lib/control/src/solver.cc

@@ -4,7 +4,10 @@
 
 #include <clasp/solver.h>
 
+#include <potassco/aspif.h>
 #include <potassco/aspif_text.h>
+#include <potassco/reify.h>
+#include <potassco/smodels.h>
 #include <potassco/theory_data.h>
 
 #include <future>
@@ -42,6 +45,9 @@ class AbstractProgramBackendImpl : public ProgramBackend, public TheoryBackend {
         return buf_.view();
     }
 
+  protected:
+    auto program() -> Potassco::AbstractProgram & { return *prg_; }
+
   private:
     virtual auto do_term_id(Symbol sym) -> prg_id_t = 0;
 
@@ -252,10 +258,45 @@ class AbstractProgramBackendImpl : public ProgramBackend, public TheoryBackend {
     std::vector<Potassco::WeightLit> wlits_;
 };
 
+class PotasscoBackend : public AbstractProgramBackendImpl {
+  public:
+    PotasscoBackend(Potassco::AbstractProgram &prg, TermBaseMap &terms)
+        : AbstractProgramBackendImpl{prg}, terms_{&terms} {}
+
+  private:
+    auto do_next_lit() -> prg_lit_t override {
+        if (auto lit = new_atom(); std::cmp_less_equal(lit, prg_lit_max)) {
+            return static_cast<prg_lit_t>(lit);
+        }
+        throw std::range_error("number of literals exhausted");
+    }
+
+    auto do_fact_lit() -> std::optional<prg_lit_t> override {
+        return std::nullopt;
+    } // TODO: only called in the aspif parser
+
+    auto do_term_id(Symbol sym) -> prg_id_t override {
+        return terms_->add(sym, [&]() {
+            auto nId = new_show_term();
+            program().outputTerm(nId, as_str(sym));
+            return nId;
+        });
+    }
+
+    void do_term_id(Symbol sym, prg_id_t id) override { terms_->add(sym, id); }
+
+    auto new_atom() -> Potassco::Atom_t { return next_atom_++; }
+    auto new_show_term() -> prg_id_t { return next_show_term_++; }
+
+    Potassco::Atom_t next_atom_{1};
+    prg_id_t next_show_term_{0};
+    TermBaseMap *terms_;
+};
+
 class ProgramBackendImpl : public AbstractProgramBackendImpl {
   public:
-    ProgramBackendImpl(Clasp::Asp::LogicProgram &prg, TermBaseMap &terms)
-        : AbstractProgramBackendImpl{adapter_}, prg_{&prg}, terms_{&terms} {}
+    ProgramBackendImpl(Potassco::AbstractProgram &program, Clasp::Asp::LogicProgram &prg, TermBaseMap &terms)
+        : AbstractProgramBackendImpl{program}, prg_{&prg}, terms_{&terms} {}
 
   private:
     auto do_next_lit() -> prg_lit_t override {
@@ -273,13 +314,12 @@ class ProgramBackendImpl : public AbstractProgramBackendImpl {
     }
 
     auto do_term_id(Symbol sym) -> prg_id_t override {
-        return terms_->add(sym, [&, this]() { return prg_->newShowTerm(as_str(sym)); });
+        return terms_->add(sym, [&]() { return prg_->newShowTerm(as_str(sym)); });
     }
 
     void do_term_id(Symbol sym, prg_id_t id) override { terms_->add(sym, id); }
 
     Clasp::Asp::LogicProgram *prg_;
-    Clasp::Asp::LogicProgramAdapter adapter_{*prg_};
     TermBaseMap *terms_;
 };
 
@@ -1069,23 +1109,51 @@ auto SymbolTable::output(CppClingo::Symbol const &sym) -> State & {
 
 Solver::Solver(Clasp::ClaspFacade &clasp, Clasp::Cli::ClaspCliConfig &clasp_config, Logger &log, SymbolStore &store,
                Scripts &scripts, Input::RewriteOptions ropts, SolverOptions sopts, FILE *out)
-    : clasp_{&clasp}, config_{clasp_config}, buf_{out}, out_{make_output_(store, sopts.mode)},
-      grd_{log, store, ropts, *out_}, scripts_{&scripts}, opts_{std::move(sopts)} {
+    : clasp_{&clasp}, config_{clasp_config}, buf_{out},
+      out_{make_output_(store, sopts.mode, sopts.backend_type, sopts.reify_flags)}, grd_{log, store, ropts, *out_},
+      scripts_{&scripts}, opts_{std::move(sopts)} {
 }
 
-auto Solver::make_output_(SymbolStore &store, AppMode mode) -> UOutputStm {
-    switch (mode) {
-        case AppMode::solve: {
-            auto backend = std::make_unique<ProgramBackendImpl>(*clasp_->asp(), terms_);
-            theory_ = std::make_unique<Output::TheoryData>(store, *backend);
-            backend_ = std::move(backend);
-            return Output::make_backend_output(store, *backend_, *theory_);
+auto Solver::make_output_(SymbolStore &store, AppMode mode, BackendType backend_type, ReifyFlags reify_flags)
+    -> UOutputStm {
+    if (mode != AppMode::solve) {
+        return Output::make_text_output(buf_);
+    }
+
+    switch (backend_type) {
+        case BackendType::clasp: {
+            program_ = std::make_unique<Clasp::Asp::LogicProgramAdapter>(*clasp_->asp());
+            break;
         }
-        default: {
-            return Output::make_text_output(buf_);
+        case BackendType::aspif: {
+            program_ = std::make_unique<Potassco::AspifOutput>(std::cout);
+            break;
+        }
+        case BackendType::smodels: {
+            program_ = std::make_unique<Potassco::SmodelsOutput>(std::cout, true, clasp_->asp()->falseAtom());
+            break;
+        }
+        case BackendType::reify: {
+            Potassco::Reifier::Options reify_opts{};
+            reify_opts.reifyStep = Potassco::test(reify_flags, ReifyFlags::reify_step);
+            reify_opts.calculateSccs = Potassco::test(reify_flags, ReifyFlags::reify_scc);
+            program_ = std::make_unique<Potassco::Reifier>(std::cout, reify_opts);
+            break;
         }
     }
-    Util::unreachable();
+    POTASSCO_ASSERT(program_, "invalid backend type");
+
+    std::unique_ptr<AbstractProgramBackendImpl> backend;
+    if (backend_type == BackendType::clasp) {
+        backend = std::make_unique<ProgramBackendImpl>(*program_, *clasp_->asp(), terms_);
+    } else {
+        backend = std::make_unique<PotasscoBackend>(*program_, terms_);
+    }
+
+    theory_ = std::make_unique<Output::TheoryData>(store, *backend);
+    backend_ = std::move(backend);
+
+    return Output::make_backend_output(store, *backend_, *theory_);
 }
 
 void Solver::interrupt() noexcept {