Skip to content

Commit

Permalink
fix incmode for gringo
Browse files Browse the repository at this point in the history
  • Loading branch information
rkaminsk committed Jun 18, 2024
1 parent 041e904 commit 9dab481
Show file tree
Hide file tree
Showing 4 changed files with 17 additions and 8 deletions.
7 changes: 7 additions & 0 deletions libclingo/clingo/clingocontrol.hh
Original file line number Diff line number Diff line change
Expand Up @@ -254,6 +254,13 @@ public:
bool blocked() override;
std::string str();
void assignExternal(Potassco::Atom_t ext, Potassco::Value_t) override;
void assignExternal(Symbol ext, Potassco::Value_t val) override {
update();
auto res = out_->find(ext);
if (res.second != nullptr && res.first != res.second->end() && res.first->hasUid()) {
assignExternal(res.first->uid(), val);
}
}
Symbol getConst(std::string const &name) const override;
bool isConflicting() const noexcept override;
Potassco::AbstractStatistics const *statistics() const override;
Expand Down
1 change: 1 addition & 0 deletions libclingo/clingo/control.hh
Original file line number Diff line number Diff line change
Expand Up @@ -245,6 +245,7 @@ struct clingo_control {
virtual Gringo::Symbol getConst(std::string const &name) const = 0;
virtual bool blocked() = 0;
virtual void assignExternal(Potassco::Atom_t ext, Potassco::Value_t val) = 0;
virtual void assignExternal(Gringo::Symbol ext, Potassco::Value_t val) = 0;
virtual bool isConflicting() const noexcept = 0;
virtual Potassco::AbstractStatistics const *statistics() const = 0;
virtual void useEnumAssumption(bool enable) = 0;
Expand Down
7 changes: 7 additions & 0 deletions libclingo/src/gringo_app.cc
Original file line number Diff line number Diff line change
Expand Up @@ -193,6 +193,13 @@ struct IncrementalControl : Control, private Output::ASPIFOutBackend {
update();
if (auto *b = out.backend()) { b->external(ext, val); }
}
void assignExternal(Symbol ext, Potassco::Value_t val) override {
update();
auto res = out.find(ext);
if (res.second != nullptr && res.first != res.second->end() && res.first->hasUid()) {
assignExternal(res.first->uid(), val);
}
}
SymbolicAtoms const &getDomain() const override { throw std::runtime_error("domain introspection not supported"); }
ConfigProxy &getConf() override { throw std::runtime_error("configuration not supported"); }
void registerPropagator(UProp, bool) override { throw std::runtime_error("theory propagators not supported"); }
Expand Down
10 changes: 2 additions & 8 deletions libclingo/src/incmode.cc
Original file line number Diff line number Diff line change
Expand Up @@ -62,12 +62,6 @@ struct Incmode {
return true;
}

void assign_external_(Symbol sym, Potassco::Value_t val) {
auto &dom = ctl_.getDomain();
auto atm = dom.lookup(sym);
if (!dom.eq(atm, dom.end())) { ctl_.assignExternal(dom.literal(atm), val); }
}

void run() {
ctl_.add("check", {"t"}, "#external query(t).");
imax = get_max();
Expand All @@ -79,14 +73,14 @@ struct Incmode {
parts.reserve(2);
parts.push_back({"check", {Symbol::createNum(step)}});
if (step > 0) {
assign_external_(Symbol::createFun("query", {Symbol::createNum(step - 1)}), Potassco::Value_t::Release);
ctl_.assignExternal(Symbol::createFun("query", {Symbol::createNum(step - 1)}), Potassco::Value_t::Release);
parts.push_back({"step", {Symbol::createNum(step)}});
}
else {
parts.push_back({"base", {}});
}
ctl_.ground(parts, nullptr);
assign_external_(Symbol::createFun("query", {Symbol::createNum(step)}), Potassco::Value_t::True);
ctl_.assignExternal(Symbol::createFun("query", {Symbol::createNum(step)}), Potassco::Value_t::True);
res = ctl_.solve({nullptr, 0}, 0)->get();
step += 1;
}
Expand Down

0 comments on commit 9dab481

Please sign in to comment.