Extend ground output options wip

[FrancoisLaferriere]

Changes

• Added AbstractProgramAdapter to bridge AbstractProgramBackendImpl and Potassco::AbstractProgram.
• Added AppMode::aspif as a quick way to test the new code path.

Concerns

• I’m not fully convinced this is the best way to pass OutputBuffer into AbstractProgram. I use an internal std::ostringstream which is copied into OutputBufferon every do_end_step() call. I also tried a std::streambuf-based integration but ended up calling OutputBuffer::flush() on every character.

• The placement of begin_step() should be correct, not confident about end_step().

• The adapter currently has to call prg_.outputTerm() and prg_.endStep() directly. I did not find a cleaner way.

[rkaminsk]

After a quick glance, this is starting to look good. I'll take a closer look later and come back to you.

[BenKaufmann]

Maybe consider dropping this comment or elaborate why this information is important.

[rkaminsk]

We should also test this for the aspif parser, then.

[BenKaufmann]

I'm not a huge fan of this template function - the name/signature does not match its implementation.

I would at least a) try to find a better/more obvious name (indicating that the function actually changes internal state) and b) split it into a (mode-independent) parse/apply function and a template. I.e.

// TBD: Find good name
auto parse_format(std::string_view str) -> bool {
        namespace Parse = Potassco::Parse;
        using namespace std::literals;
       ...
}
template <class ModeT> auto parse_format(std::string_view str, ModeT &mode) -> bool {
  if (parse_format(str)) {
    mode = ModeT::solve;
    return true;
  }
  return false;
}

[rkaminsk]

We could use parse_backend_type as name.

[BenKaufmann]

We could use parse_backend_type as name.

I think the "parse" prefix just does not fit here. In other places, parse_* means "transform string to (output) parameter of type T", but here "parse" both applies state and transforms to output.

From a pure implementation perspective, I would do the following:

1. Provide enum entries for enum class AppMode in solver.hh, e.g. via:

POTASSCO_REFLECT_ENUM_ENTRIES(AppMode, 0, 4); // or explicitly via POTASSCO_SET_ENUM_ENTRIES

2. Implement auto init_app_mode(std::string_view str) -> bool in ClingoOptions.

auto init_app_mode(std::string_view str) -> bool {
    namespace Parse = Potassco::Parse;
    using namespace std::literals;
    // Parse to temporaries: we don't want partial state changes
    Control::AppMode mode;
    Control::ReifyFlag reify;
    Control::ModeFormat format;
    if (Parse::ok(Potassco::extract(str, format))) {
        if (format == Control::ModeFormat::reify) {
            while (Parse::matchOpt(str, ',')) {
                ...
        }
    } else if (not Parse::ok(Potassco::stringTo(str, mode))) {
        return false;
    }
    if (str.empty()) { // Success: commit result
        solver_opts_.mode = Control::AppMode::solve;
        solver_opts_.format = format;
        solver_opts_.reify = reify;
       return true;
    }
    return false;
}

3. In clingo_control_new, bind --mode option parser to init_app_mode.

auto parse_mode = [&opts](std::string_view str) { return opts.init_app_mode(str); };

4. In main.cc:initOptions, compose --mode option parser:

auto parse_mode = [this](std::string_view str) {
    if (opts_.init_app_mode(str)) { // "Common" app mode?
        mode_ = static_cast<Mode>(opts_.mode());
        return true;
    }
    if (str == "clasp") { // Special app mode?
        mode_ = Mode::clasp;
        return true;
    }
    return false;
};

Anyhow, to me (the naive user), the semantics of the mode option (and its tight coupling to the internal states) is unclear. For example (ignoring implementation), what's the difference between parse, rewrite, and ground, and why is aspif etc. not some kind of rewrite /grounding?

From a user's perspective, maybe it would be more clear if we'd add a new convert/transform mode with the output format as sub-arguments.

[rkaminsk]

We should probably leave the implementation aside for a moment and discuss what the options from a user's perspective should look like:

Currently, we have --mode={parse,rewrite,ground,solve,clasp}:

• parse: Parses the program and prints it as parsed. Limited use maybe pretty-printing.
• rewrite: Rewrites the parsed program. This applies simplifications and brings rules into a shape ready for grounding. Mostly for debugging purposes.
• ground: This is essentially clingo's previous --text option.
• solve: This is the usual clingo ground and solve mode.
• clasp: This turns clingo into clasp.

Next we want to add aspif/smodels/reify output. Technically, these proceed a bit like the solve mode (solve terminates an aspif/smodels slice with a zero). They don't really fit nicely in the above list.

A separate option --backend={clasp,aspif,smodels,reify} or maybe --output that requires solve mode would also be an option.

What are your thoughts?

[BenKaufmann]

Here is my naive view: we have a mode clasp that turns clingo into clasp and we have a mode ground, which basically turns clingo into a grounder. The mode solve is the actual clingo and shouldn't even be needed in the CLI, so I would actually drop it.
Now, aspif/smodels/reify might internally depend on the "solve" mode, but to me, this is a non-obvious implementation detail since no "solving" is actually happening.

Conceptually, I would think that aspif/smodels/reify belong to the grounder and hence, I would either have --mode=ground[,<output-fmt>[,<options>]] or a separate option --ground-output=aspif,smodels,reify. In the latter case, I would suggest generating an error if --ground-output is used together with an explicit mode != ground.

[rkaminsk]

convert would fit into the existing mode option

But I actually prefer a separate option: --output/--convert/--ground-format whatever. I would also let this option switch the mode behind the scenes as required. To keep things simple we can even make the mode and the new option exclusive.

What about

--mode={parse|rewrite|solve|clasp}
--output={text|aspif|smodels|reify}
--reify-options=<list {sccs,steps}>

?

Option --output can set the internal mode to ground/solve as required. If both are given, we can raise an exception. Then mode becomes an advanced option for debugging and using clasp. Option --output can be used to inspect the text output and use clingo with other solvers.

I won't insist on this solution if you think there is a better one. 😄

[BenKaufmann]

I don't have a strong preference. However, if we go with the separate option, I would prefer a different name for that option. Having both --output and (the poorly named clasp option) --outf might be confusing. Of course, we could also rename the latter.

[rkaminsk]

If everyone is okay with having separate options we can at least go forward with the implementation. Changing names of options later should not be a big deal.

[FrancoisLaferriere]

Let’s settle on a separate option then. What about the reifier options? We could also have a separate option, as Roland suggested, or have them comma-separated, the same way as for --pre in clasp. I tend more toward the second option for consistency with clasp.

[rkaminsk]

I have no strong preference here.

[rkaminsk]

Let's try to find good names next. Afterward, we will still need to test this.

[rkaminsk]

We could use parse_backend_type as name.

[rkaminsk]

We should also test this for the aspif parser, then.

[FrancoisLaferriere]

I used --convert for now, and used comma-separated option for the reifier.

Todo:

• Remove ground from AppMode enum entries. I temporarily kept it to not break the tests, which need update.
• I still need to see what's up with do_fact_lit()

[rkaminsk]

I still need to see what's up with do_fact_lit()

The function exists for backward compatibility with aspif 1.0. It is rather easy to implement:

• introduce a fact_ member that is initially zero
• if fact is zero and a rule is output that is a fact -> set fact_ to the head of the rule
• if do_fact_lit is called
  • generate a rule that is a fact introducing a new atom if fact_ is zero
  • return fact_