diff --git a/clasp b/clasp index 3f3db1e3..eb0b28dd 160000 --- a/clasp +++ b/clasp @@ -1 +1 @@ -Subproject commit 3f3db1e3f9a1eda7d2170d5e5a2ade6646a88361 +Subproject commit eb0b28dd618b9762830146428875bbb1c0bee524 diff --git a/libclingo/clingo/clingo_app.hh b/libclingo/clingo/clingo_app.hh index b95bb453..7613489f 100644 --- a/libclingo/clingo/clingo_app.hh +++ b/libclingo/clingo/clingo_app.hh @@ -52,7 +52,7 @@ protected: ProblemType getProblemType() override; void run(Clasp::ClaspFacade& clasp) override; - ClaspOutput* createOutput(ProblemType f) override; + ClaspOutput* createTextOutput(const Clasp::Cli::ClaspAppBase::TextOptions& options) override; void printHelp(const Potassco::ProgramOptions::OptionContext& root) override; void printVersion() override; diff --git a/libclingo/src/clingo_app.cc b/libclingo/src/clingo_app.cc index 1d69785c..535aef5b 100644 --- a/libclingo/src/clingo_app.cc +++ b/libclingo/src/clingo_app.cc @@ -111,80 +111,37 @@ Clasp::ProblemType ClingoApp::getProblemType() { return Clasp::ClaspFacade::detectProblemType(getStream()); } -// TODO: the code below is annoying. There is too much copy and paste. The -// easiest way would be if the textoutput would already provide something to -// customize the output. -namespace { - -class CustomTextOutput : public Clasp::Cli::TextOutput { -public: - CustomTextOutput(std::unique_ptr &ctl, IClingoApp &app, Clasp::uint32 verbosity, Format f, const char* catAtom = 0, char ifs = ' ') - : TextOutput(verbosity, f, catAtom, ifs), ctl_(ctl), app_(app) { } - -protected: - void printModel(const Clasp::OutputTable& out, const Clasp::Model& m, PrintLevel x) override { - if (ctl_) { - if (x == modelQ()) { - comment(1, "%s: %" PRIu64"\n", !m.up ? "Answer" : "Update", m.num); - ClingoModel cm(*ctl_, &m); - std::lock_guardpropLock_)> lock(ctl_->propLock_); - app_.print_model(&cm, [&]() { printValues(out, m); }); - } - if (x == optQ()) { - printMeta(out, m); - } - fflush(stdout); - } - else { Clasp::Cli::TextOutput::printModel(out, m, x); } - } -private: - std::unique_ptr &ctl_; - IClingoApp &app_; -}; - -} // namespace - -ClingoApp::ClaspOutput* ClingoApp::createOutput(ProblemType f) { - if (mode_ == mode_gringo) return 0; - using namespace Clasp; - using namespace Clasp::Cli; - SingleOwnerPtr out; - if (claspAppOpts_.outf == ClaspAppOptions::out_none) { - return 0; +ClingoApp::ClaspOutput* ClingoApp::createTextOutput(const Clasp::Cli::ClaspAppBase::TextOptions &options) { + if (mode_ == mode_gringo) { + return nullptr; } - if (claspAppOpts_.outf != ClaspAppOptions::out_json || claspAppOpts_.onlyPre) { - TextOutput::Format outFormat = TextOutput::format_asp; - if (f == Problem_t::Sat){ outFormat = TextOutput::format_sat09; } - else if (f == Problem_t::Pb) { outFormat = TextOutput::format_pb09; } - else if (f == Problem_t::Asp && claspAppOpts_.outf == ClaspAppOptions::out_comp) { - outFormat = TextOutput::format_aspcomp; - } - if (app_->has_printer()) { - out.reset(new CustomTextOutput(grd, *app_, verbose(), outFormat, claspAppOpts_.outAtom.c_str(), claspAppOpts_.ifs)); - } - else { - out.reset(new TextOutput(verbose(), outFormat, claspAppOpts_.outAtom.c_str(), claspAppOpts_.ifs)); - } - if (claspConfig_.parse.isEnabled(ParserOptions::parse_maxsat) && f == Problem_t::Sat) { - static_cast(out.get())->result[TextOutput::res_sat] = "UNKNOWN"; - } + else if (!app_->has_printer()) { + return Clasp::Cli::ClaspAppBase::createTextOutput(options); } else { - out.reset(new JsonOutput(verbose())); - } - if (claspAppOpts_.quiet[0] != static_cast(UCHAR_MAX)) { - out->setModelQuiet((ClaspOutput::PrintLevel)std::min(uint8(ClaspOutput::print_no), claspAppOpts_.quiet[0])); - } - if (claspAppOpts_.quiet[1] != static_cast(UCHAR_MAX)) { - out->setOptQuiet((ClaspOutput::PrintLevel)std::min(uint8(ClaspOutput::print_no), claspAppOpts_.quiet[1])); - } - if (claspAppOpts_.quiet[2] != static_cast(UCHAR_MAX)) { - out->setCallQuiet((ClaspOutput::PrintLevel)std::min(uint8(ClaspOutput::print_no), claspAppOpts_.quiet[2])); - } - if (claspAppOpts_.hideAux && clasp_.get()) { - clasp_->ctx.output.setFilter('_'); + class CustomTextOutput : public Clasp::Cli::TextOutput { + public: + using BaseType = Clasp::Cli::TextOutput; + CustomTextOutput(std::unique_ptr &ctl, IClingoApp &app, const Clasp::Cli::ClaspAppBase::TextOptions &opts) + : TextOutput(opts.verbosity, opts.format, opts.catAtom, opts.ifs), ctl_(ctl), app_(app) { } + + protected: + void printModelValues(const Clasp::OutputTable &out, const Clasp::Model &m) override { + if (ctl_) { + ClingoModel cm(*ctl_, &m); + std::lock_guardpropLock_)> lock(ctl_->propLock_); + app_.print_model(&cm, [&]() { BaseType::printModelValues(out, m); }); + } + else { + BaseType::printModelValues(out, m); + } + } + private: + std::unique_ptr &ctl_; + IClingoApp &app_; + }; + return new CustomTextOutput(grd, *app_, options); } - return out.release(); } void ClingoApp::printHelp(const Potassco::ProgramOptions::OptionContext& root) {