clingo.control

Module containing the Control class responsible for grounding and solving.

Example

The example shows the most straightforward way to ground and solve a small test program:

>>> from clingo.core import Library
>>> from clingo.control import Control
>>>
>>> lib = Library()
>>> ctl = Control(lib)
>>> ctl.parse_string("1 { a; b }.")
>>> ctl.ground()
>>> print(ctl.solve(on_model=print))
a
SAT
class Control:

A control object for grounding and solving.

Control(lib: clingo.core.Library, options: Sequence[str] = [])

Construct a control object.

Arguments:
  • lib: The library storing symbols and scripts.
  • options: The command line options to initialize the control object.
def discard(self, minimize: bool = False, project: bool = False) -> None:

Discard statements of the selected types.

Arguments:
  • minimize: Discard all minimize and weak constraints (default: False).
  • project: Discard all previously added project statements (default: False).
def ground( self, parts: Optional[Sequence[tuple[str, Sequence[clingo.symbol.Symbol]]]] = None, context: Any = None) -> None:

Ground the given program parts.

Non-ground logic programs must be added before calling this function. Programs can define named sections using #program. directives. These sections can be selectively grounded by specifying their name and binding parameters to symbols.

Arguments:
  • parts: A sequence of tuples, each containing a section name and a sequence of symbols. The name identifies the program section to ground, and the symbols bind its parameters. If None, the implicit base section without arguments is grounded.
  • context: An optional object providing functions that can be called during grounding.
def interrupt(self) -> None:

Interrupt the active solve call.

This function is thread-safe. Prefer using clingo.solve.SolveHandle.cancel if possible.

def join(self, program: clingo.ast.Program) -> None:

Join with the given non-ground logic program.

Arguments:
  • program: A non-ground logic program.
def main(self) -> None:

Ground and solve a logic program based on the current control mode.

This function serves as a high-level entry point for the default ground-and-solve process. It considers the current ControlMode and can dispatch execution to a script's main function if defined.

If solving, the function proceeds as follows:

  1. Each set of program parts in parts is grounded sequentially.
  2. After grounding each set, solving is performed immediately.

Before calling main(), the control object can be prepared by parsing programs, registering propagators, or performing other setup steps.

def observe(self, observer: clingo.backend.Observer, preprocess: bool = True) -> None:

Inspect the ground program of the current step.

Arguments:
  • observer: The program observer to inspect the program. preprocess: Whether the program should be preprocessed first (default: True).
def parse_files(self, files: Sequence[str]) -> None:

Parses the logic programs in the given files

Arguments:
  • files: A list of file paths to parse.
def parse_string(self, program: str) -> None:

Parses a logic program given as a string.

Arguments:
  • program: The logic program as a string.
def register_propagator(self, propagator: clingo.propagate.Propagator) -> None:

Register the given propagator for theory propagation.

See the clingo.propagate module for an example.

Arguments:
  • propagator: The propagator.
def solve( self, assumptions: Sequence[tuple[clingo.symbol.Symbol, bool] | int] = [], on_model: Callable[[clingo.solve.Model], bool | None] | None = None, on_unsat: Callable[[typing.Sequence[int]], None] | None = None, on_stats: Callable[[clingo.stats.Stats, clingo.stats.Stats], None] | None = None, on_finish: Callable[[clingo.solve.SolveResult], None] | None = None) -> clingo.solve.SolveResult:

Solve the current ground program.

This function is semantically equivalent to the following start_solve call:

with self.start_solve(assumptions, on_model, on_unsat, on_stats, on_finish) as hnd:
    return hnd.get()
Arguments:
  • assumptions: A list of assumptions.
  • on_model: Optional callback to intercept models.
  • on_unsat: Optional callback to intercept lower bounds during optimization.
  • on_stats: Optional callback extend statistics.
  • on_finish: Optional callback called once search has finished.
Returns:

A clingo.solve.SolveResult representing the result of the search.

def start_ground( self, parts: Optional[Sequence[tuple[str, Sequence[clingo.symbol.Symbol]]]] = None, context: Any = None, on_finish: Callable[[clingo.ground.GroundResult], None] | None = None) -> clingo.ground.GroundHandle:

Ground the given program parts.

Starts grounding in the background and returns a clingo.ground.GroundHandle to the running grounding. See Control.ground for details on grounding program parts.

Arguments:
  • parts: A sequence of parts to ground.
  • context: An optional object providing functions that can be called during grounding.
  • on_finish: An optional callback called once grounding has finished.
def start_solve( self, assumptions: Sequence[tuple[clingo.symbol.Symbol, bool] | int] = [], on_model: Callable[[clingo.solve.Model], bool | None] | None = None, on_unsat: Callable[[typing.Sequence[int]], None] | None = None, on_stats: Callable[[clingo.stats.Stats, clingo.stats.Stats], None] | None = None, on_finish: Callable[[clingo.solve.SolveResult], None] | None = None, yield_: bool = False, async_: bool = False) -> clingo.solve.SolveHandle:

Solve the current ground program.

This function runs the solver on the current ground program, optionally using assumptions, callbacks, or asynchronous execution. It returns a SolveHandle, allowing interaction with the solving process.

If asynchronous solving (async_) is enabled, the function returns immediately, and solving runs in the background. Otherwise, the function blocks until solving is complete.

Arguments:
  • assumptions: A list of assumptions that constrain this search. Each assumption is either a tuple[clingo.symbol.Symbol, bool] indicating an atom's truth value or a program literal (see clingo.base.Atom.literal). For example, using [(clingo.symbol.Function(lib, "a"), True)] only admits answer sets that contain atom a.
  • on_model: Optional callback that receives a clingo.solve.Model object when a model is found. Returning False from the callback stops solving.
  • on_unsat: Optional callback to intercept lower bounds during optimization.
  • on_stats: Optional callback that receives statistics updates after each step. Two clingo.stats.Stats objects are passed: step-specific and accumulated stats.
  • on_finish: Optional callback called once search has finished. A clingo.solve.SolveResult is passed to the callback.
  • yield_: If True, the returned clingo.solve.SolveHandle is iterable, yielding clingo.solve.Model objects during solving.
  • async_: If True, solving runs asynchronously in a separate thread. Note: Callbacks (on_model, on_stats, etc.) will also be called from a separate thread.
Returns:

A clingo.solve.SolveHandle to control the search.

Notes:

Asynchronous solving requires compiling clingo with thread support. Blocking methods on SolveHandle release the GIL but are not thread-safe.

See Also:

clingo.solve: Contains examples on using this function.

def write_aspif( self, path: str, symbols: bool = False, append: bool = False, preamble: bool | None = None, preprocess: bool = True) -> None:

Write the current logic programs to the given file.

If append is true, a file will be created if none exists yet. If preamble is None, then the aspif preamble is written for newly created files and omitted for existing files.

Arguments:
  • path: The path to write the program to.
  • append: Whether to append to an existing file.
  • preamble: Whether to write the aspif preamble.
  • preprocess: Whether to preprocess the program before writing.
backend: clingo.backend.BackendManager

Get a backend manager to extend the ground program.

base: clingo.base.Base

Get the atom/term bases of the program.

buffer: str

The content of the output buffer.

config: clingo.config.Config

Get the solver config.

const_map: Mapping[str, clingo.symbol.Symbol]

Get the map of constants defined by #const directives.

mode: ControlMode

Get the application mode.

parts: Optional[Sequence[tuple[str, Sequence[clingo.symbol.Symbol]]]]

Get/set the program parts to ground.

profile: list

Get the profiling information as a list of profile nodes.

Each node is a dictionary with keys such as "type", "key", "depth", "nested", "children", etc. Returns a list of top-level profile nodes representing the profiling tree.

The result is directly convertible to JSON using Python's json module.

stats: clingo.stats.StatsView

Get the solver stats.

class ControlMode(enum.IntEnum):

Available control modes.

Ground = <ControlMode.Ground: 2>
Parse = <ControlMode.Parse: 0>
Rewrite = <ControlMode.Rewrite: 1>
Solve = <ControlMode.Solve: 3>