potassco / clingo

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

Querying from the last model #380

Closed RenatoGeh closed 2 years ago

RenatoGeh commented 2 years ago

Hi,

I'm working with clingo's Python API and am running into a problem that I'm not sure how to solve. I want to do brave or cautious reasoning but only get the last model (i.e. the final result) so I can do some querying on that object (e.g. contains).

The main problem seems to be that I cannot, in any way I'm aware of, retrieve this last model. For instance, given the following program:

from clingo.control import Control
C = Control()
C.add("base", [], "a :- not b. b :- not a.")
C.ground([("base", [])])

I want to be able to get the Model object representing b a for brave reasoning, and the Model object for an "empty model" for cautious reasoning.

The issue is that, because Model objects are only accessible during the time the solver is looking at that particular model, I can't for instance keep a record of the last model seen, since the next time the solver iterates it'll destroy that object and I'll get a segmentation fault. Particularly, this happens even when the Model is the last one. I might've missed something, but I don't remember seeing any way to query whether a model is the last one or a way to only return the last model from the Python API docs.

Interestingly, from the application side I can simply pass --quiet=1 --enum-mode brave 0 to clingo and it'll do exactly what I want.

Am I missing something? Is there a way to do this?

Thanks!

rkaminsk commented 2 years ago

Model objects are not intended to be stored but only provide a view to the current model stored by the solver. You could for example store the symbols in the model and then process them later once you have determined that the stored symbols capture indeed the cautious consequences.

RenatoGeh commented 2 years ago

Model objects are not intended to be stored but only provide a view to the current model stored by the solver. You could for example store the symbols in the model and then process them later once you have determined that the stored symbols capture indeed the cautious consequences.

I see. I guess what I wanted is to have the efficiency of querying from the existing contains method from the API instead of copying all symbols with symbols into Python objects and then having to run things in (slow) Python, but I guess that's the cost of doing things in Python. :) Thanks for the quick reply though!