Propagator fails when lookahead is enabled.

[rkaminsk]

The runtime check

POTASSCO_REQUIRE(front_ == INT32_MAX || (dl - level_) == 1, "Propagate must be called on each level");

fires if a propagator is used together with lookahead (solver.6 in the portfolio).

If you need an example, I can provide something but in its current form there is quite some setup required to get it running.

[BenKaufmann]

A (preferably) small example would be highly appreciated.

[rkaminsk]

I'll try to come up with something. So far I can tell that the problem appears when solving incrementally with lookahead enabled. It consistently happens at the beginning of the second solving step. It is either the above runtime error or an assertion:

void Clasp::Lookahead::splice(Clasp::Lookahead::NodeId): Assertion `ul != UINT32_MAX' failed.

[rkaminsk]

Please have a look at the lookahead-bug branch in clingo-dl. The project should build fine on both linux and windows. If you want to avoid installing re2c and bison you can apply the windows.patch.1 after checking out the submodules. The example to reproduce the bug itself is tiny.

[BenKaufmann]

Thanks. Will try to give you some feedback by the end of this week.

[BenKaufmann]

I hopefully found and fixed the problem. Could you please do some further testing?

[rkaminsk]

Thanks. I think that clingo-dl is currently our most sophisticated propagator. But testing with lookahead is a bit difficult because with large instances it slows down solving too much. But maybe @wanko and @MaxOstrowski can try some lookahead options on smaller instances (e.g. --lookahead=atom,100 possible combined with multithreading). Feedback would be appreciated. (Having this bug free is important to run with -t<n> for <n> >= 6 without crashes.)