Skip to content

Commit

Permalink
Restrict ClingoModel::isConsequence() to relevant atoms.
Browse files Browse the repository at this point in the history
* Only return True/Unknown for atoms that are relevant to the
  active "projection mode".
  • Loading branch information
BenKaufmann committed Aug 30, 2024
1 parent 87201e1 commit 5d5dbf4
Show file tree
Hide file tree
Showing 2 changed files with 36 additions and 11 deletions.
33 changes: 22 additions & 11 deletions libclingo/clingo/clingocontrol.hh
Original file line number Diff line number Diff line change
Expand Up @@ -341,7 +341,7 @@ public:
bool initialized_ = false;
bool incmode_ = false;
bool canClean_ = false;

bool preserveFacts_ = false;
};

// {{{1 declaration of ClingoModel
Expand Down Expand Up @@ -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; }
Expand All @@ -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_;
Expand Down
14 changes: 14 additions & 0 deletions libclingo/src/clingocontrol.cc
Original file line number Diff line number Diff line change
Expand Up @@ -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_);
Expand Down Expand Up @@ -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::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()));
Expand Down

0 comments on commit 5d5dbf4

Please sign in to comment.