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):
...     step.update({"example": [21]})
...     accu.update({"example": [lambda x: (x or 0) + 21]})
...
>>> lib = Library()
>>> ctl = Control(lib, ['--stats'])
>>> ctl.parse_string("{a}.")
>>> ctl.ground()
>>> print(ctl.solve(on_stats=on_stats))
SAT
>>> print(ctl.solve(on_stats=on_stats))
SAT
>>> ctl.stats['user_step'].nestify()
{ "example": [21.0] }
>>> ctl.stats['user_accu'].nestify()
{ "example": [42.0] }
>>> ctl.stats['summary']['times'].nestify()
{ "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(StatsView):

Class representing solver stats.

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.

value: float

Get/set the value of the stats object.

Inherited Members
StatsView
nestify
type
class StatsArray(StatsArrayView):

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:

Get an iterator over the values of the map.

class StatsArrayView:

Class representing a read-only array of stats.

This class partially implements the mutable sequence protocol.

class StatsMap(StatsMapView):

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.

def items(self) -> Iterator[tuple[str, Stats]]:

Get an iterator over the items of the map.

def values(self) -> Iterator[Stats]:

Get the value of the stats object.

Inherited Members
StatsMapView
keys
class StatsMapView:

Class representing a read-only map of stats.

This class partially implements the mutable mapping protocol.

def items(self) -> Iterator[tuple[str, StatsView]]:

Get an iterator over the items of the map.

def keys(self) -> Iterator[str]:

Get an iterator over the keys of the map.

def values(self) -> Iterator[StatsView]:

A readable representation to inspect the array.

class StatsType(enum.IntEnum):

The type of a stats object.

Array = <StatsType.Array: 1>
Map = <StatsType.Map: 2>
Value = <StatsType.Value: 0>
class StatsView:

Class representing read-only solver stats.

def nestify(self) -> Any:

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

array: StatsArrayView

Get an array of stats objects.

map: StatsMapView

Get a map of stats objects.

type: StatsType

Get the type of the stats object.

value: float