Improve support for writing checkpoints in aspif format (#530)

* add function to register predefined backends
* add support to load multiple slices of aspif

libclingo/clingo.h

@@ -2770,6 +2770,21 @@ typedef struct clingo_part {
 //! ~~~~~~~~~~~~~~~
 typedef bool (*clingo_ground_callback_t) (clingo_location_t const *location, char const *name, clingo_symbol_t const *arguments, size_t arguments_size, void *data, clingo_symbol_callback_t symbol_callback, void *symbol_callback_data);
 
+//! The available backends.
+//!
+//! This is a mix between enum and bit set. Bits 0 and 1 are used to configure
+//! the reify backend.
+enum clingo_backend_type_e {
+    clingo_backend_type_reify = 0,       //!< the reify backend
+    clingo_backend_type_reify_sccs = 1,  //!< whether to reify sccs
+    clingo_backend_type_reify_steps = 2, //!< whether to reify steps individually
+    clingo_backend_type_aspif = 4,       //!< the aspif backend
+    clingo_backend_type_smodels = 5,     //!< the smodels backend
+};
+//! Corresponding type to clingo_backend_type_e.
+typedef unsigned clingo_backend_type_t;
+
+
 //! Control object holding grounding and solving state.
 typedef struct clingo_control clingo_control_t;
 
@@ -2811,6 +2826,20 @@ CLINGO_VISIBILITY_DEFAULT void clingo_control_free(clingo_control_t *control);
 //! - ::clingo_error_runtime if parsing or checking fails
 CLINGO_VISIBILITY_DEFAULT bool clingo_control_load(clingo_control_t *control, char const *file);
 
+//! Load files in aspif format.
+//!
+//! This function should be called on an empty control object.
+//!
+//! If more than one file is given, they are merged into one file. Only the first one should have a preamble.
+//!
+//! @param[in] control the target
+//! @param[in] files the array of files to load
+//! @param[in] size the size of the array
+//! @return whether the call was successful; might set one of the following error codes:
+//! - ::clingo_error_bad_alloc
+//! - ::clingo_error_runtime if parsing or checking fails
+CLINGO_VISIBILITY_DEFAULT bool clingo_control_load_aspif(clingo_control_t *control, char const **files, size_t size);
+
 //! Extend the logic program with the given non-ground logic program in string form.
 //!
 //! This function puts the given program into a block of form: <tt>\#program name(parameters).</tt>
@@ -3100,6 +3129,19 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_control_theory_atoms(clingo_control_t cons
 //! @param[in] data user data passed to the observer functions
 //! @return whether the call was successful
 CLINGO_VISIBILITY_DEFAULT bool clingo_control_register_observer(clingo_control_t *control, clingo_ground_program_observer_t const *observer, bool replace, void *data);
+//! Register a backend with the control object.
+//!
+//! This function is similar to clingo_control_register_observer except that
+//! clingo's internal backends can be selected.
+//!
+//! @param[in] control the target
+//! @param[in] type the kind of backend to register
+//! @param[in] file the file to write the result to
+//! @param[in] replace just pass the grounding to the backend but not the solver
+//! @return whether the call was successful; might set one of the following error codes:
+//! - ::clingo_error_bad_alloc
+//! - ::clingo_error_runtime (for example if the file could not be opened)
+CLINGO_VISIBILITY_DEFAULT bool clingo_control_register_backend(clingo_control_t *control, clingo_backend_type_t type, char const *file, bool replace);
 //! @}
 
 //! @name Program Modification Functions

libclingo/clingo/clingocontrol.hh

@@ -252,6 +252,7 @@ public:
     void ground(Control::GroundVec const &vec, Context *ctx) override;
     void add(std::string const &name, Gringo::StringVec const &params, std::string const &part) override;
     void load(std::string const &filename) override;
+    void load_aspif(Potassco::Span<char const *> files) override;
     bool blocked() override;
     std::string str();
     void assignExternal(Potassco::Atom_t ext, Potassco::Value_t) override;

libclingo/clingo/control.hh

@@ -246,6 +246,7 @@ struct clingo_control {
     virtual void *claspFacade() = 0;
     virtual void add(std::string const &name, Gringo::StringVec const &params, std::string const &part) = 0;
     virtual void load(std::string const &filename) = 0;
+    virtual void load_aspif(Potassco::Span<char const *> files) = 0;
     virtual Gringo::Symbol getConst(std::string const &name) const = 0;
     virtual bool blocked() = 0;
     virtual void assignExternal(Potassco::Atom_t ext, Potassco::Value_t val) = 0;

libclingo/src/clingocontrol.cc

@@ -340,6 +340,19 @@ void ClingoControl::load(std::string const &filename) {
     parser_->pushFile(std::string(filename), logger_);
     parse();
 }
+void ClingoControl::load_aspif(Potassco::Span<char const*> files) {
+    using std::begin;
+    using std::end;
+    for (auto it = end(files), ib = begin(files); it != ib; --it) {
+        parser_->pushFile(std::string{*(it - 1)}, logger_);
+    }
+    if (!parser_->empty()) {
+        parser_->parse_aspif(logger_);
+    }
+    if (logger_.hasError()) {
+        throw std::runtime_error("parsing failed");
+    }
+}
 bool ClingoControl::hasSubKey(unsigned key, char const *name) const {
     unsigned subkey = claspConfig_.getKey(key, name);
     return subkey != Clasp::Cli::ClaspCliConfig::KEY_INVALID;

libclingo/src/control.cc

@@ -2065,6 +2065,11 @@ extern "C" bool clingo_control_load(clingo_control_t *ctl, char const *file) {
     GRINGO_CLINGO_CATCH;
 }
 
+extern "C" bool clingo_control_load_aspif(clingo_control_t *ctl, char const **files, size_t size) {
+    GRINGO_CLINGO_TRY { ctl->load_aspif(Potassco::Span<char const *>{files, size}); }
+    GRINGO_CLINGO_CATCH;
+}
+
 extern "C" bool clingo_control_set_enable_enumeration_assumption(clingo_control_t *ctl, bool value) {
     GRINGO_CLINGO_TRY { ctl->useEnumAssumption(value); }
     GRINGO_CLINGO_CATCH;
@@ -2196,6 +2201,35 @@ extern "C" bool clingo_control_register_observer(clingo_control_t *control, clin
     GRINGO_CLINGO_CATCH;
 }
 
+extern "C" bool clingo_control_register_backend(clingo_control_t *control, clingo_backend_type_t type, char const *file, bool replace) {
+    GRINGO_CLINGO_TRY { 
+        auto out = gringo_make_unique<std::ofstream>(file);
+        if (!out->is_open()) {
+            throw std::runtime_error("file could not be opened");
+        }
+        auto backend = UBackend{};
+        switch (type & 0xFFFFFFFC) {
+            case clingo_backend_type_reify: {
+                backend = Output::make_backend(std::move(out), Output::OutputFormat::REIFY, (type & 1) == 1, (type &2) == 2);
+                break;
+            }
+            case clingo_backend_type_smodels: {
+                backend = Output::make_backend(std::move(out), Output::OutputFormat::SMODELS, false, false);
+                break;
+            }
+            case clingo_backend_type_aspif: {
+                backend = Output::make_backend(std::move(out), Output::OutputFormat::INTERMEDIATE, false, false);
+                break;
+            }
+            default: {
+                throw std::runtime_error("invalid backend type given");
+            }
+        }
+        control->registerObserver(std::move(backend), replace);
+    }
+    GRINGO_CLINGO_CATCH;
+}
+
 extern "C" bool clingo_control_new(char const *const * args, size_t n, clingo_logger_t logger, void *data, unsigned message_limit, clingo_control_t **ctl) {
     GRINGO_CLINGO_TRY {
         static std::mutex mut;

libclingo/src/gringo_app.cc

@@ -163,6 +163,17 @@ struct IncrementalControl : Control, private Output::ASPIFOutBackend {
         parser.pushFile(std::string(filename), logger_);
         parse();
     }
+    void load_aspif(Potassco::Span<char const *> files) override {
+        for (auto it = end(files), ib = begin(files); it != ib; --it) {
+            parser.pushFile(std::string{*(it - 1)}, logger_);
+        }
+        if (!parser.empty()) {
+            parser.parse_aspif(logger_);
+        }
+        if (logger_.hasError()) {
+            throw std::runtime_error("parsing failed");
+        }
+    }
     bool blocked() override { return false; }
     USolveFuture solve(Assumptions ass, clingo_solve_mode_bitset_t, USolveEventHandler cb) override {
         update();

libgringo/gen/src/input/groundtermlexer.hh

@@ -1,4 +1,4 @@
-/* Generated by re2c 3.1 on Sat Jun 22 13:23:28 2024 */
+/* Generated by re2c 3.1 on Tue Dec  3 10:42:26 2024 */
 #line 1 "/home/kaminski/Documents/git/potassco/clingo/libgringo//src/input/groundtermlexer.xh"
 // {{{ MIT License
 

libgringo/gen/src/input/nongroundlexer.hh

@@ -1,4 +1,4 @@
-/* Generated by re2c 3.1 on Sat Jun 22 13:23:27 2024 */
+/* Generated by re2c 3.1 on Tue Dec 10 20:24:59 2024 */
 #line 1 "/home/kaminski/Documents/git/potassco/clingo/libgringo//src/input/nongroundlexer.xch"
 // {{{ MIT License
 
@@ -7715,6 +7715,78 @@ yy514:
 
 }
 
+void NonGroundParser::aspif_asp_(Location &loc) {
+    start(loc);
+    char yych;
+
+#line 7723 "/home/kaminski/Documents/git/potassco/clingo/build/debug/libgringo//src/input/nongroundlexer.hh"
+{
+	YYCTYPE yych;
+	switch (YYGETCONDITION()) {
+		case yycaspif: goto yyc_aspif;
+	}
+/* *********************************** */
+yyc_aspif:
+	if ((YYLIMIT - YYCURSOR) < 4) YYFILL(4);
+	yych = *YYCURSOR;
+	switch (yych) {
+		case '\n': goto yy519;
+		case ' ': goto yy520;
+		case 'a': goto yy521;
+		default: goto yy516;
+	}
+yy516:
+	++YYCURSOR;
+	if (YYLIMIT <= YYCURSOR) YYFILL(1);
+	yych = *YYCURSOR;
+yy517:
+	switch (yych) {
+		case '\n':
+		case ' ': goto yy518;
+		default: goto yy516;
+	}
+yy518:
+#line 338 "/home/kaminski/Documents/git/potassco/clingo/libgringo//src/input/nongroundlexer.xch"
+	{ aspif_error_(loc, format("expected 'asp' but got token ", string()).c_str()); }
+#line 7752 "/home/kaminski/Documents/git/potassco/clingo/build/debug/libgringo//src/input/nongroundlexer.hh"
+yy519:
+	++YYCURSOR;
+#line 336 "/home/kaminski/Documents/git/potassco/clingo/libgringo//src/input/nongroundlexer.xch"
+	{ aspif_error_(loc, format("expected 'asp' but got ", eof() ? "<EOF>" : "<EOL>").c_str()); }
+#line 7757 "/home/kaminski/Documents/git/potassco/clingo/build/debug/libgringo//src/input/nongroundlexer.hh"
+yy520:
+	++YYCURSOR;
+#line 337 "/home/kaminski/Documents/git/potassco/clingo/libgringo//src/input/nongroundlexer.xch"
+	{ aspif_error_(loc, "expected 'asp' but got <SPACE>"); }
+#line 7762 "/home/kaminski/Documents/git/potassco/clingo/build/debug/libgringo//src/input/nongroundlexer.hh"
+yy521:
+	yych = *++YYCURSOR;
+	switch (yych) {
+		case 's': goto yy522;
+		default: goto yy517;
+	}
+yy522:
+	yych = *++YYCURSOR;
+	switch (yych) {
+		case 'p': goto yy523;
+		default: goto yy517;
+	}
+yy523:
+	yych = *++YYCURSOR;
+	switch (yych) {
+		case '\n':
+		case ' ': goto yy524;
+		default: goto yy516;
+	}
+yy524:
+#line 335 "/home/kaminski/Documents/git/potassco/clingo/libgringo//src/input/nongroundlexer.xch"
+	{ return; }
+#line 7785 "/home/kaminski/Documents/git/potassco/clingo/build/debug/libgringo//src/input/nongroundlexer.hh"
+}
+#line 339 "/home/kaminski/Documents/git/potassco/clingo/libgringo//src/input/nongroundlexer.xch"
+
+}
+
 } } // namespace Input Gringo
 
 #undef YYCTYPE

libgringo/gringo/input/nongroundparser.hh

@@ -70,6 +70,7 @@ public:
     int lex(void *pValue, Location &loc);
     bool parseDefine(std::string const &define, Logger &log);
     ParseResult parse(Logger &log);
+    void parse_aspif(Logger &log);
     bool empty() { return LexerState::empty(); }
     void include(String file, Location const &loc, bool inbuilt, Logger &log);
     void theoryLexing(TheoryLexing mode);
@@ -106,6 +107,7 @@ private:
     Condition condition() const;
     String filename() const;
 
+    void aspif_stms_(Location &loc);
     Symbol aspif_symbol_(Location &loc);
     std::vector<Potassco::Id_t> aspif_ids_(Location &loc);
     std::vector<Potassco::Atom_t> aspif_atoms_(Location &loc);
@@ -131,7 +133,7 @@ private:
     void aspif_edge_(Location &loc);
     void aspif_theory_(Location &loc);
     void aspif_comment_(Location &loc);
-
+    void aspif_asp_(Location &loc);
 
     std::set<std::string> filenames_;
     bool &incmode_;

libgringo/gringo/output/output.hh

@@ -228,6 +228,8 @@ private:
     Atom_t fact_id_ = 0;
 };
 
+UBackend make_backend(std::unique_ptr<std::ostream> out, OutputFormat format, bool reify_sccs, bool reify_steps);
+
 } } // namespace Output Gringo
 
 #endif // GRINGO_OUTPUT_OUTPUT_HH

libgringo/src/input/nongroundlexer.xch

@@ -328,6 +328,17 @@ uint32_t NonGroundParser::aspif_unsigned_(Location &loc) {
 
 }
 
+void NonGroundParser::aspif_asp_(Location &loc) {
+    start(loc);
+    char yych;
+    /*!re2c
+    <aspif> "asp"    { return; }
+    <aspif> NL       { aspif_error_(loc, format("expected 'asp' but got ", eof() ? "<EOF>" : "<EOL>").c_str()); }
+    <aspif> WS       { aspif_error_(loc, "expected 'asp' but got <SPACE>"); }
+    <aspif> NOWSNL+  { aspif_error_(loc, format("expected 'asp' but got token ", string()).c_str()); }
+    */
+}
+
 } } // namespace Input Gringo
 
 #undef YYCTYPE

libgringo/src/input/nongroundparser.cc

@@ -266,7 +266,7 @@ String NonGroundParser::filename() const { return LexerState::data().first; }
 
 void NonGroundParser::pushFile(std::string &&file, Logger &log) {
     auto checked = check_file(file);
-    if (!checked.empty() && !filenames_.insert(checked).second) {
+    if (!checked.empty() && !filenames_.emplace(checked).second) {
         report_included("<cmd>", file.c_str(), log);
     }
     else if (checked.empty() || !push(file)) {
@@ -275,7 +275,7 @@ void NonGroundParser::pushFile(std::string &&file, Logger &log) {
 }
 
 void NonGroundParser::pushStream(std::string &&file, std::unique_ptr<std::istream> in, Logger &log) {
-    auto res = filenames_.insert(std::move(file));
+    auto res = filenames_.emplace(std::move(file));
     if (!res.second) {
         report_included("<cmd>", res.first->c_str(), log);
     }
@@ -344,7 +344,7 @@ void NonGroundParser::include(String file, Location const &loc, bool inbuilt, Lo
     }
     else {
         auto paths = check_file(file.c_str(), loc.beginFilename.c_str());
-        if (!paths.first.empty() && !filenames_.insert(paths.first).second) {
+        if (!paths.first.empty() && !filenames_.emplace(paths.first).second) {
             report_included(loc, file.c_str(), log);
         }
         else if (paths.first.empty() || !push(paths.second, true)) {
@@ -531,17 +531,32 @@ std::vector<Potassco::WeightLit_t> NonGroundParser::aspif_wlits_(Location &loc)
     return wlits;
 }
 
-void NonGroundParser::aspif_(Location &loc) {
-    aspif_preamble_(loc);
-    bck_.beginStep();
+void NonGroundParser::parse_aspif(Logger &log) {
+    if (!empty()) {
+        log_ = &log;
+        condition_ = yycaspif;
+        auto loc = Location(filename(), 1, 1, filename(), 1, 1);
+        aspif_asp_(loc);
+        aspif_preamble_(loc);
+        bck_.beginStep();
+        do {
+            aspif_stms_(loc);
+            pop();
+        }
+        while (!empty());
+        bck_.endStep();
+        filenames_.clear();
+        disable_aspif();
+    }
+}
+
+void NonGroundParser::aspif_stms_(Location &loc) {
     for (;;) {
         auto stm_type = aspif_unsigned_(loc);
         switch (stm_type) {
             case 0:  {
                 aspif_nl_(loc);
-                bck_.endStep();
                 start(loc);
-                condition(yycnormal);
                 return;
             }
             case 1:  { aspif_rule_(loc); break; }
@@ -559,6 +574,15 @@ void NonGroundParser::aspif_(Location &loc) {
     }
 }
 
+void NonGroundParser::aspif_(Location &loc) {
+    aspif_preamble_(loc);
+    bck_.beginStep();
+    aspif_stms_(loc);
+    bck_.endStep();
+    condition(yycnormal);
+    return;
+}
+
 void NonGroundParser::aspif_rule_(Location &loc) {
     aspif_ws_(loc);
     auto stm_type = Potassco::Head_t(aspif_unsigned_(loc));