From 87201e15029181ad900f248b7525214894faa4b4 Mon Sep 17 00:00:00 2001 From: Benjamin Kaufmann Date: Fri, 30 Aug 2024 08:01:44 +0200 Subject: [PATCH 1/2] Update clasp. --- clasp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clasp b/clasp index 4fd5c00a..f37d8139 160000 --- a/clasp +++ b/clasp @@ -1 +1 @@ -Subproject commit 4fd5c00ae877b6202254c401a438e322ce584e16 +Subproject commit f37d813980fff4c993ec39bff4a8a07fd8454bfb From 5d5dbf4bd368c4a0844ab18e17d00206edc18d2f Mon Sep 17 00:00:00 2001 From: Benjamin Kaufmann Date: Fri, 30 Aug 2024 15:01:43 +0200 Subject: [PATCH 2/2] Restrict ClingoModel::isConsequence() to relevant atoms. * Only return True/Unknown for atoms that are relevant to the active "projection mode". --- libclingo/clingo/clingocontrol.hh | 33 ++++++++++++++++++++----------- libclingo/src/clingocontrol.cc | 14 +++++++++++++ 2 files changed, 36 insertions(+), 11 deletions(-) diff --git a/libclingo/clingo/clingocontrol.hh b/libclingo/clingo/clingocontrol.hh index e30707d4..6b13fe67 100644 --- a/libclingo/clingo/clingocontrol.hh +++ b/libclingo/clingo/clingocontrol.hh @@ -341,7 +341,7 @@ public: bool initialized_ = false; bool incmode_ = false; bool canClean_ = false; - + bool preserveFacts_ = false; }; // {{{1 declaration of ClingoModel @@ -396,16 +396,21 @@ public: return ctl_.getDomain(); } bool isTrue(Potassco::Lit_t lit) const override { - return model_->isTrue(lp().getLiteral(lit)); + return model_->isTrue(lp().getLiteral(lit)); } ConsequenceType isConsequence(Potassco::Lit_t literal) const override { - if (model_->isDef(lp().getLiteral(literal))) { - return ConsequenceType::True; - } - if (model_->isEst(lp().getLiteral(literal))) { - return ConsequenceType::Unknown; - } - return ConsequenceType::False; + auto lit = lp().getLiteral(literal); + auto res = ConsequenceType::False; + if (model_->isDef(lit)) { + res = ConsequenceType::True; + } + else if (model_->isEst(lit)) { + res = ConsequenceType::Unknown; + } + if (res != ConsequenceType::False && !isProjected(literal)) { + res = ConsequenceType::False; + } + return res; } ModelType type() const override { if (model_->type & Clasp::Model::Brave) { return ModelType::BraveConsequences; } @@ -418,9 +423,15 @@ public: bool optimality_proven() const override { return model_->opt; } ClingoControl &context() { return ctl_; } private: - Clasp::Asp::LogicProgram const &lp() const { return *static_cast(ctl_.clasp_->program()); }; + Clasp::Asp::LogicProgram const &lp() const { return *static_cast(ctl_.clasp_->program()); }; Output::OutputBase const &out() const { return *ctl_.out_; }; - Clasp::SharedContext const &ctx() const { return ctl_.clasp_->ctx; }; + Clasp::SharedContext const &ctx() const { return ctl_.clasp_->ctx; }; + bool isProjected(Potassco::Lit_t literal) const { + if (ctl_.clasp_->ctx.output.projectMode() == Clasp::ProjectMode_t::Explicit) { + return lp().isProjected(literal); + } + return lp().isShown(literal); + } ClingoControl &ctl_; Clasp::Model const *model_; mutable SymVec atms_; diff --git a/libclingo/src/clingocontrol.cc b/libclingo/src/clingocontrol.cc index b6743a1b..5679e4bf 100644 --- a/libclingo/src/clingocontrol.cc +++ b/libclingo/src/clingocontrol.cc @@ -206,6 +206,7 @@ void ClingoControl::parse(const StringVec& files, const ClingoOptions& opts, Cla out_ = gringo_make_unique(*data_, std::move(outPreds), std::cout, opts.outputFormat, opts.outputOptions); } out_->keepFacts = opts.keepFacts; + preserveFacts_ = opts.outputOptions.preserveFacts; aspif_bck_ = gringo_make_unique(*this); pb_ = gringo_make_unique(scripts_, prg_, out_->outPreds, defs_, opts.rewriteMinimize); parser_ = gringo_make_unique(*pb_, *aspif_bck_, incmode_); @@ -524,6 +525,19 @@ void ClingoControl::prepare(Assumptions ass) { } prePrepare(*clasp_); clasp_->prepare(enableEnumAssupmption_ ? Clasp::ClaspFacade::enum_volatile : Clasp::ClaspFacade::enum_static); + if (!preserveFacts_ && clasp_->program()) { + // NB: If facts are not preserved in the output, clasp's "show" state is incomplete wrt to shown facts. + // For now, we explicitly restore the state here. Alternatively, we could adjust Atomtab::output() so + // that it always passes the atom id to the backend, or we could just maintain the set of "shown" atoms + // in ClingoControl. + auto &prg = static_cast(*clasp_->program()); + (void) out_->atoms(clingo_show_type_shown, [&](unsigned uid) { + if (prg.isFact(uid) && !prg.isShown(uid)) { + prg.addOutputState(uid, Clasp::Asp::LogicProgram::OutputState::out_shown); + } + return false; + }); + } preSolve(*clasp_); } out_->reset(data_ || (clasp_ && clasp_->program()));