clingo.base

Functions and classes to work with atom and term bases.

Examples

>>> from clingo.core import Library
>>> from clingo.symbol import Function, Number
>>> from clingo.control import Control
>>> lib = Library()
>>> ctl = Control(lib)
>>> ctl.parse_string("""\
... p(1).
... { p(3) }.
... #external p(1..3).
...
... q(X) :- p(X).
... """)
>>> ctl.ground()
>>> bse = ctl.base
>>> len(bse)
2
>>> p = bse[("p", 1)]
>>> Function(lib, "p", [Number(lib, 2)]) in p
True
>>> Function(lib, "p", [Number(lib, 4)]) in p
False
>>> [sig for sig in bse]
[('p', 1, False), ('q', 1, False)]
>>> [(str(x.symbol), bse.is_fact(x.literal), bse.is_external(x.literal))
...  for x in p.values()]
[('p(1)', True, False), ('p(3)', False, False), ('p(2)', False, True)]

class Atom:

A class providing information about symbolic atoms.

literal: int

Get the program literal of the atom.

symbol: clingo.symbol.Symbol

Get the symbol of the atom.

class AtomBase:

An class providing information about symbolic atoms.

Implements Mapping[Symbol, Atom].

def get( self, key: clingo.symbol.Symbol, default: Atom | None = None) -> Atom | None:

Get the value for the given key or the default if absent.

def items(self) -> Iterator[tuple[clingo.symbol.Symbol, Atom]]:

Get an iterator over the items in the map.

def keys(self) -> Iterator[clingo.symbol.Symbol]:

Get an iterator over the keys in the map.

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

Get an iterator over the values in the map.

class Base:

A class providing information about symbolic and theory atoms and shown terms.

Implements Mapping[tuple[str, int, bool], AtomBase] providing additional overloads to directly lookup symbols and short signatures (assuming a positive sign):

__getitem__: Callable[[Symbol], Atom]
__contains__: Callable[[Symbol], bool]
__getitem__: Callable[[tuple[str, int]], AtomBase]
__contains__: Callable[[tuple[str, int]], bool]

def get( self, key: tuple[str, int, bool], default: AtomBase | None = None) -> AtomBase | None:

Get the value for the given key or the default if absent.

def is_current(self, literal: int) -> bool:

Check whether a literal has been introduced in the current step.

Note that all literals introduced before the last solve call are considered from a previous step.

Arguments:

literal: The literal to check.

Returns:

Whether the literal is subject to projection.

def is_external(self, literal: int) -> bool:

Check whether the given program literal corresponds to an external.

Arguments:

literal: The literal to check.

Returns:

Whether the literal is external.

def is_fact(self, literal: int) -> bool:

Check whether the literal is a fact.

Arguments:

literal: The literal to check.

Returns:

Whether the literal is a fact.

def is_projected(self, literal: int) -> bool:

Check whether the literal is part of a #project directive.

Arguments:

literal: The literal to check.

Returns:

Whether the literal is subject to projection.

def is_shown(self, literal: int) -> bool:

Check whether the literal is shown via a #show directive.

Arguments:

literal: The literal to check.

Returns:

Whether the literal is shown.

def items(self) -> Iterator[tuple[tuple[str, int, bool], AtomBase]]:

Get an iterator over the items in the map.

def keys(self) -> Iterator[tuple[str, int, bool]]:

Get an iterator over the keys in the map.

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

Get an iterator over the values in the map.

terms: TermBase

The term base (given by show directives).

theory: TheoryBase

The theory base.

class Term:

A class providing information about terms.

condition: Sequence[Sequence[int]]

Get the condition of the term.

symbol: clingo.symbol.Symbol

Get the symbol of the term.

class TermBase:

A class providing information about shown terms.

The base is established by the show directives occurring in a program.

Implements Mapping[Symbol, Term].

def get( self, key: clingo.symbol.Symbol, default: Term | None = None) -> Term | None:

Get the value for the given key or the default if absent.

def items(self) -> Iterator[tuple[clingo.symbol.Symbol, Term]]:

Get an iterator over the items in the map.

def keys(self) -> Iterator[clingo.symbol.Symbol]:

Get an iterator over the keys in the map.

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

Get an iterator over the values in the map.

class TheoryAtom:

A view to inspect a theory atom.

elements: Sequence[TheoryElement]

Get the elements of a theory atom.

guard: tuple[str, TheoryTerm] | None

Get optional guard of a theory atom.

literal: int

Get the literal of the theory atom (zero for directives).

Get the name of a theory atom.

class TheoryBase:

A class prooviding information about theory atoms.

Implements Sequence[TheoryAtom].

def count(self, value: TheoryAtom) -> int:

Count how often the given value occurs in the sequence.

def index(self, value: TheoryAtom) -> int:

Get the index of the given value in the sequence.

class TheoryElement:

A view to inspect a theory element.

condition: Sequence[int]

Get the condition of a theory element.

condition_id: int

Get the condition id of a theory element.

tuple: Sequence[TheoryTerm]

Get the term tuple of a theory element.

class TheoryTerm:

A view to inspect a theory term.

arguments: Sequence[TheoryTerm]

Get the arguments of a function, tuple, list, or set theory term.

Get the name of a theory symbol or function.

number: int

Get the value of a numeric theory term.

type: TheoryTermType

Get the type of the theory term.

class TheoryTermType:

Enumeration of theory term types.

TheoryTermType(value: int)

Function: ClassVar[TheoryTermType] = TheoryTermType.Function

For function theory terms.

List: ClassVar[TheoryTermType] = TheoryTermType.List

For list theory term.

Number: ClassVar[TheoryTermType] = TheoryTermType.Number

For numeric theory terms.

Set: ClassVar[TheoryTermType] = TheoryTermType.Set

For set theory terms.

Symbol: ClassVar[TheoryTermType] = TheoryTermType.Symbol

For symbolic theory terms (simple strings).

Tuple: ClassVar[TheoryTermType] = TheoryTermType.Tuple

For tuple theory terms.

value: int