potassco / clasp

⚙️ A conflict-driven nogood learning answer set solver
https://potassco.org/clasp/
MIT License
116 stars 16 forks source link

Yielding models using the SolveHandle produces different results in synchronous and asynchronous mode. #65

Closed rkaminsk closed 3 years ago

rkaminsk commented 3 years ago

Would it be possible to make the two programs below produce the same output? I am asking because this is one of those hard to document discrepancies. I believe we had a discussion once that it would be difficult in the synchronous mode to yield models before passing them to the solve event handler. It would fine to first trigger the model callback in the asynchronous mode.

>>> from clingo.control import Control
>>> 
>>> ctl = Control()
>>> ctl.add('base', [], 'a.')
>>> ctl.ground([('base', [])])
>>> 
>>> def cb(prefix):
...     return lambda m: print('{}: {}'.format(prefix, m))
... 
>>> print('synchronous yielding')
synchronous yielding
>>> with ctl.solve(on_model=cb('on_model'), yield_=True, async_=False) as hnd:
...     for m in hnd:
...         cb('on_yield')(m)
...     _ = hnd.get()
... 
on_model: a
on_yield: a
>>> print('asynchronous yielding')
asynchronous yielding
>>> with ctl.solve(on_model=cb('on_model'), yield_=True, async_=True) as hnd:
...     for m in hnd:
...         cb('on_yield')(m)
...     _ = hnd.get()
... 
on_yield: a
on_model: a
BenKaufmann commented 3 years ago

From clasp's perspective there are two event handlers. There is the global event handler stored in the SharedContext (this one is set and used by the clasp app to print all kind of progress and it also seems to be used by clingo) as well as an (optional) model handler that can be passed to ClaspFacade::solve(). This second event handler is always called before a yield. For the synchronous mode, the order is:

For the asynchronous mode, the order is:

Anyhow, while clingo could switch to using the model handler, I agree that this inconsistency feels wrong and is at least annoying.

The major problem with yielding first before calling event handlers is that the user might break the yield loop early so that event handlers are not called at all. This would break certain statistics and/or output and might also be otherwise unexpected.

So, if you are fine with consistently having 1) model handler, 2) global handler, 3) yield, I'll implement it this way.

rkaminsk commented 3 years ago

So, if you are fine with consistently having 1) model handler, 2) global handler, 3) yield, I'll implement it this way.

We stumbled upon this because we once added an interface to extend a model with additional symbols. Now, we need a well-defined place to do this. The above solution seems good to me because:

Let's go for yielding at the end and thanks for looking at this!

BenKaufmann commented 3 years ago

Should be fixed in dev.

rkaminsk commented 3 years ago

Seems to work. Thanks.