From 324f370384949bca759c5a4e2b90d8fa7162a12f Mon Sep 17 00:00:00 2001
From: Benjamin Kaufmann <kaufmann@cs.uni-potsdam.de>
Date: Fri, 30 Aug 2024 15:01:43 +0200
Subject: [PATCH] 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 e30707d45..6b13fe67e 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<Clasp::Asp::LogicProgram*>(ctl_.clasp_->program()); };
+    Clasp::Asp::LogicProgram const &lp() const { return *static_cast<Clasp::Asp::LogicProgram*>(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 b6743a1b5..af3a4549c 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<Output::OutputBase>(*data_, std::move(outPreds), std::cout, opts.outputFormat, opts.outputOptions);
     }
     out_->keepFacts = opts.keepFacts;
+    preserveFacts_ = opts.outputOptions.preserveFacts;
     aspif_bck_ = gringo_make_unique<ControlBackend>(*this);
     pb_ = gringo_make_unique<Input::NongroundProgramBuilder>(scripts_, prg_, out_->outPreds, defs_, opts.rewriteMinimize);
     parser_ = gringo_make_unique<Input::NonGroundParser>(*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_) {
+            // 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::Asp::LogicProgram&>(*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()));