Skip to content

Commit

Permalink
Fix #54: Acquire problem vars on clingo init.
Browse files Browse the repository at this point in the history
* A clingo propagator might add watches over newly added problem
  variables during initialization. So ensure that all problem
  variables are known to the solver before calling
  ClingoPropagatorInit::init().
  • Loading branch information
BenKaufmann committed Feb 7, 2020
1 parent 627dd86 commit 202dc98
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 0 deletions.
1 change: 1 addition & 0 deletions src/clingo.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -187,6 +187,7 @@ void ClingoPropagator::destroy(Solver* s, bool detach) {
bool ClingoPropagator::init(Solver& s) {
POTASSCO_REQUIRE(s.decisionLevel() == 0 && prop_ <= trail_.size(), "Invalid init");
Control ctrl(*this, s, state_init);
s.acquireProblemVars();
init_ = call_->init(init_, ctrl);
front_ = call_->checkMode() == ClingoPropagatorCheck_t::Fixpoint ? -1 : INT32_MAX;
return true;
Expand Down
8 changes: 8 additions & 0 deletions tests/facade_test.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2008,6 +2008,14 @@ TEST_CASE("Clingo propagator init", "[facade][propagator]") {
REQUIRE(s0.hasWatch(posLit(4), pp));
REQUIRE(!s0.hasWatch(posLit(3), pp));
}
SECTION("init acquires all problem vars") {
Var v = ctx.addVar(Var_t::Atom);
init.addWatch(posLit(v));
init.applyConfig(s0);
ctx.endInit();
PostPropagator* pp = s0.getPost(PostPropagator::priority_class_general);
REQUIRE(s0.hasWatch(posLit(v), pp));
}
SECTION("ignore duplicate watches from init") {
init.addWatch(posLit(1));
init.addWatch(posLit(1));
Expand Down

0 comments on commit 202dc98

Please sign in to comment.