clingo.ground

Functions and classes related to grounding.

Examples

The example shows how call external functions during grounding:

>>> from clingo.core import Library
>>> from clingo.symbol import Number
>>> from clingo.control import Control
>>>
>>> class Context:
...     def __init__(self, lib):
...       self.lib = lib
...     def inc(self, x):
...         return Number(self.lib, x.number + 1)
...     def seq(self, x, y):
...         return [x, y]
...
>>> lib = Library()
>>> ctl = Control(lib)
>>> ctl.parse_string("""
... p(@inc(10)).
... q(@seq(1,2)).
... """)
>>> ctl.ground(context=Context(lib))
>>> print(ctl.solve(on_model=print))
p(11) q(1) q(2)
SAT

The example below shows how to start grounding in the background and wait for grounding to finish:

>>> from clingo.control import Control
>>> from clingo.core import Library
>>>
>>> lib = Library()
>>> ctl = Control(lib)
>>> ctl.parse_string("{a}.")
>>> with ctl.start_ground() as hnd:
...     w = {True: "finished", False: "running"}
...     print(f"start_ground status: {w[hnd.wait(0)]}")
...     print(f"start_ground result: {hnd.get()!r}")
...     print(f"start_ground status: {w[hnd.wait(0)]}")
...
start_ground status: running
start_ground result: <GroundResult.Ok: 0>
start_ground status: finished
class GroundHandle:

An object to interact with a running search.

It can be used to control solving, like, retrieving models or cancelling a search.

A GroundHandle is a context manager and must be used with Python's with statement.

Blocking functions in this object release the GIL. They are not thread-safe though.

See also: clingo.control.Control.ground

def cancel(self) -> None:

Cancel the running search.

See also: clingo.control.Control.interrupt

def get(self) -> GroundResult:

Get the ground result.

This is always the last function to be called on a handle to ensure that the search is properly terminated. It might be preceded by a call to cancel to stop the search.

def wait(self, timeout: typing.SupportsFloat | None = None) -> bool:

Wait for the ground call to finish or the next result with an optional timeout.

If a timeout is provided, the function blocks for the given duration or until a result is ready. A positive timeout blocks for that amount of time. A negative timeout blocks until a result is available, and a zero timeout allows polling for a result.

Arguments:
  • timeout: The maximum time to block in seconds.
Returns:

Whether the ground call has finished or the next result is ready.

class GroundResult(enum.IntEnum):

Enumeration of ground result types.

Interrupted = <GroundResult.Interrupted: 2>
Ok = <GroundResult.Ok: 0>
Unsatisfiable = <GroundResult.Unsatisfiable: 1>