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 mode\n"
+             "      %A: <mode {parse|rewrite|solve}>\n"
+             "        parse   : Print parsed program and exit\n"
+             "        rewrite : Print rewritten program and exit\n"
+             "        solve   : Ground and solve the program (default)");
         ctx.add(group_basic);
         slv_cfg->addOptions(ctx);
         auto pos_parser = [](std::string_view str, std::string &out) {
@@ -74,6 +74,7 @@ extern "C" auto clingo_control_new(clingo_lib_t *lib, clingo_string_t const *arg
         cargs.emplace_back(nullptr);
         DefaultParseContext pc{ctx};
         parseCommandArray(pc, {cargs.data(), size}, pos_parser);
+        opts.validate_options(pc.parsed());
         ctx.assignDefaults(pc.parsed());
         slv_cfg->finalize(pc.parsed(), Clasp::ProblemType::asp, true);
 

lib/c-api/src/main.cc

@@ -174,31 +174,47 @@ 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 mode\n"
+             "      %A: <mode {parse|rewrite|solve|clasp}>\n"
+             "        parse   : Print parsed program and exit\n"
+             "        rewrite : Print rewritten program and exit\n"
+             "        solve   : Ground and solve the program (default)\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

@@ -2,6 +2,7 @@
 
 #include <clingo/control/solver.hh>
 
+#include <potassco/program_opts/errors.h>
 #include <potassco/program_opts/program_options.h>
 #include <potassco/program_opts/typed_value.h>
 
@@ -171,6 +172,42 @@ class ClingoOptions {
             }
             return true;
         };
+        auto parse_convert = [this](std::string_view str) {
+            namespace Parse = Potassco::Parse;
+            using namespace std::literals;
+
+            if (Parse::eqIgnoreCase(str, "text"sv)) {
+                solver_opts_.mode = Control::AppMode::ground;
+                return true;
+            }
+
+            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 +256,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 program, print and exit\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 +283,28 @@ class ClingoOptions {
         }
     }
 
+    auto init_app_mode(std::string_view str) -> bool {
+        namespace Parse = Potassco::Parse;
+
+        Control::AppMode mode{};
+        if (!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 Potassco::ProgramOptions::Error("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,32 @@ 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}, {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 +838,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 +870,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_;