potassco / clingo

🤔 A grounder and solver for logic programs.
https://potassco.org/clingo
MIT License
599 stars 79 forks source link

Potential bug in example on webpage #426

Closed drexlerd closed 1 year ago

drexlerd commented 1 year ago

In the fourth example in this page https://potassco.org/clingo/python-api/current/clingo/solving.html on solving iteratively and asynchronously: according to the documentation the resume() call on the SolveHandle will discard the model. Hence, it should not be called before retrieving the model and therefore, must be placed at the end of the function. Here is what I think is correct. I stumbled upon this because I occasionally got UNSAT in an ASP where I could verify that there is a solution. I was using parallel mode of clingo.

>>> with ctl.solve(yield_=True, async_=True) as hnd:
...     while True:
...         # some computation here
...         _ = hnd.wait()
...         m = hnd.model()
...         if m is None:
...             print(hnd.get())
...             break
...         print(m)
...         hnd.resume()  # moved from beginning to end of function
rkaminsk commented 1 year ago

In the fourth example in this page https://potassco.org/clingo/python-api/current/clingo/solving.html on solving iteratively and asynchronously: according to the documentation the resume() call on the SolveHandle will discard the model. Hence, it should not be called before retrieving the model and therefore, must be placed at the end of the function. Here is what I think is correct. I stumbled upon this because I occasionally got UNSAT in an ASP where I could verify that there is a solution. I was using parallel mode of clingo.

>>> with ctl.solve(yield_=True, async_=True) as hnd:
...     while True:
...         # some computation here
...         _ = hnd.wait()
...         m = hnd.model()
...         if m is None:
...             print(hnd.get())
...             break
...         print(m)
...         hnd.resume()  # moved from beginning to end of function

The intention was that the first call to resume is optional, i.e., the search starts right away. So I would rather say this is a bug in the API. I'll investigate...

rkaminsk commented 1 year ago

I cannot reproduce this issue. I would need an example where this occurs. Either version with resume at the end or beginning should be fine.

drexlerd commented 1 year ago

I did not store the program that I used back then when the error occurred. Also, I noticed a bug in my own software that could also have caused it. I will look more into this at a later time and close the issue for now. Sorry for inconveniences.