clingo.stats

Functions and classes related to solver stats.

Examples

The following example shows how to add custom stats and access the stats:

>>> from clingo.core import Library
>>> from clingo.control import Control
>>>
>>> def on_stats(step, accu):
...     accu.update({"example": [21]})
...     accu.update({"example": [lambda x: (x or 0) + 21]})
...
>>> lib = Library()
>>> ctl = Control(lib, ['--stats'])
>>> ctl.parse_string("{a}.")
>>> ctl.ground()
>>> with ctl.solve(on_stats=on_stats) as hnd:
...     print(hnd.get())
SAT
>>> with ctl.solve(on_stats=on_stats) as hnd:
...     print(hnd.get())
SAT
>>> ctl.stats['user_step']
{ "example": [21.0] }
>>> ctl.stats['user_accu']
{ "example": [42.0] }
>>> ctl.stats['summary']['times']
{ "cpu": 0.000785999999999995,
  "sat": 7.867813110351562e-06,
  "solve": 2.288818359375e-05,
  "total": 0.0007848739624023438,
  "unsat": 0.0 }

Note that the control object is created passing options --stats; without this option only basic stats are reported.

class Stats:

Class representing solver stats.

def nestify(self) -> Any:

Convert the statistics object into a nested structure consisting of sequencens, mappings with string keys, and floats.

def update(self, values: Any) -> None:

Update the statistics with the given values.

Note that values can be inserted and changed but they cannot be deleted nor can their type be changed.

Arguments:

values: A nested structure consisting of sequencens, mappings with string keys, floats, and functions. The latter can be used to update existing values. They receive the previous values as argument and must return an updated value. If there is no previous value, None is passed as argument.

array: StatsArray

Get an array of stats objects.

map: StatsMap

Get a map of stats objects.

type: StatsType

Get the type of the stats object.

value: float

Get/set the value of the stats object.

class StatsArray:

Class representing an array of stats.

This class partially implements the mutable sequence protocol - elements of arrays can be modified but they cannot be deleted. Modifications are implemented via Stats.update.

Most use cases should be implementable just using the update function of the top-level statistics object.

def append(self, value: Any) -> None:

Append the given value to the array.

Arguments:

value: The value to append.

class StatsMap:

Class representing a map of stats.

This class partially implements the mutable mapping protocol - value of keys can be modified but they cannot be deleted. Modifications are implemented via Stats.update.

Most use cases should be implementable just using the update function of the top-level statistics object.

class StatsType:

The type of a stats object.

StatsType(value: int)

Array: ClassVar[StatsType] = StatsType.Array

Indicate an array of stats.

Map: ClassVar[StatsType] = StatsType.Map

Indicate a map of stats.

Value: ClassVar[StatsType] = StatsType.Value

Indicate a value of stats.

name: str

value: int