Module clingo.theory_atoms
Functions and classes to work with theory atoms.
Examples
>>> from clingo.control import Control
>>>
>>> ctl = Control()
>>> ctl.add('base', [], """\
... #theory example {
... t { };
... &a/0 : t, head
... }.
... {c}.
... &a { t: c }.
... """)
>>> ctl.ground([('base', [])])
>>> atm = next(ctl.theory_atoms)
>>> print(atm)
&a{t: c}
>>> elm = atm.elements[0]
>>> print(elm)
t: c
Expand source code
'''
Functions and classes to work with theory atoms.
Examples
--------
>>> from clingo.control import Control
>>>
>>> ctl = Control()
>>> ctl.add('base', [], """\\
... #theory example {
... t { };
... &a/0 : t, head
... }.
... {c}.
... &a { t: c }.
... """)
>>> ctl.ground([('base', [])])
>>> atm = next(ctl.theory_atoms)
>>> print(atm)
&a{t: c}
>>> elm = atm.elements[0]
>>> print(elm)
t: c
'''
from typing import List, Optional, Tuple
from functools import total_ordering
from ._internal import _c_call, _c_call2, _lib, _str, _to_str
from .core import OrderedEnum
__all__ = ["TheoryAtom", "TheoryElement", "TheoryTerm", "TheoryTermType"]
class TheoryTermType(OrderedEnum):
"""
Enumeration of theory term types.
"""
Function = _lib.clingo_theory_term_type_function
"""
For a function theory terms.
"""
List = _lib.clingo_theory_term_type_list
"""
For list theory terms.
"""
Number = _lib.clingo_theory_term_type_number
"""
For numeric theory terms.
"""
Set = _lib.clingo_theory_term_type_set
"""
For set theory terms.
"""
Symbol = _lib.clingo_theory_term_type_symbol
"""
For symbolic theory terms (symbol here means the term is a string).
"""
Tuple = _lib.clingo_theory_term_type_tuple
"""
For tuple theory terms.
"""
@total_ordering
class TheoryTerm:
"""
`TheoryTerm` objects represent theory terms.
Theory terms have a readable string representation, implement Python's rich
comparison operators, and can be used as dictionary keys.
"""
def __init__(self, rep, idx):
self._rep = rep
self._idx = idx
def __hash__(self):
return self._idx
def __eq__(self, other):
return self._idx == other._idx
def __lt__(self, other):
return self._idx < other._idx
def __str__(self):
return _str(
_lib.clingo_theory_atoms_term_to_string_size,
_lib.clingo_theory_atoms_term_to_string,
self._rep,
self._idx,
)
def __repr__(self):
return f"TheoryTerm({self._rep!r})"
@property
def arguments(self) -> List["TheoryTerm"]:
"""
The arguments of the term (for functions, tuples, list, and sets).
"""
args, size = _c_call2(
"clingo_id_t*",
"size_t",
_lib.clingo_theory_atoms_term_arguments,
self._rep,
self._idx,
)
return [TheoryTerm(self._rep, args[i]) for i in range(size)]
@property
def name(self) -> str:
"""
The name of the term (for symbols and functions).
"""
return _to_str(
_c_call("char*", _lib.clingo_theory_atoms_term_name, self._rep, self._idx)
)
@property
def number(self) -> int:
"""
The numeric representation of the term (for numbers).
"""
return _c_call(
"int", _lib.clingo_theory_atoms_term_number, self._rep, self._idx
)
@property
def type(self) -> TheoryTermType:
"""
The type of the theory term.
"""
type_ = _c_call(
"clingo_theory_term_type_t",
_lib.clingo_theory_atoms_term_type,
self._rep,
self._idx,
)
return TheoryTermType(type_)
@total_ordering
class TheoryElement:
"""
Class to represent theory elements.
Theory elements have a readable string representation, implement Python's rich
comparison operators, and can be used as dictionary keys.
"""
def __init__(self, rep, idx):
self._rep = rep
self._idx = idx
def __hash__(self):
return self._idx
def __eq__(self, other):
return self._idx == other._idx
def __lt__(self, other):
return self._idx < other._idx
def __str__(self):
return _str(
_lib.clingo_theory_atoms_element_to_string_size,
_lib.clingo_theory_atoms_element_to_string,
self._rep,
self._idx,
)
def __repr__(self):
return f"TheoryElement({self._rep!r})"
@property
def condition(self) -> List[int]:
"""
The condition of the element in form of a list of program literals.
"""
cond, size = _c_call2(
"clingo_literal_t*",
"size_t",
_lib.clingo_theory_atoms_element_condition,
self._rep,
self._idx,
)
return [cond[i] for i in range(size)]
@property
def condition_id(self) -> int:
"""
Each condition has an id, which is a temporary program literal. This id
can be passed to `clingo.propagator.PropagateInit.solver_literal` to
obtain a corresponding solver literal.
"""
return _c_call(
"clingo_literal_t",
_lib.clingo_theory_atoms_element_condition_id,
self._rep,
self._idx,
)
@property
def terms(self) -> List[TheoryTerm]:
"""
The tuple of the element.
"""
terms, size = _c_call2(
"clingo_id_t*",
"size_t",
_lib.clingo_theory_atoms_element_tuple,
self._rep,
self._idx,
)
return [TheoryTerm(self._rep, terms[i]) for i in range(size)]
@total_ordering
class TheoryAtom:
"""
Class to represent theory atoms.
Theory atoms have a readable string representation, implement Python's rich
comparison operators, and can be used as dictionary keys.
"""
def __init__(self, rep, idx):
self._rep = rep
self._idx = idx
def __hash__(self):
return self._idx
def __eq__(self, other):
return self._idx == other._idx
def __lt__(self, other):
return self._idx < other._idx
def __str__(self):
return _str(
_lib.clingo_theory_atoms_atom_to_string_size,
_lib.clingo_theory_atoms_atom_to_string,
self._rep,
self._idx,
)
def __repr__(self):
return f"TheoryAtom({self._rep!r})"
@property
def elements(self) -> List[TheoryElement]:
"""
The elements of the atom.
"""
elems, size = _c_call2(
"clingo_id_t*",
"size_t",
_lib.clingo_theory_atoms_atom_elements,
self._rep,
self._idx,
)
return [TheoryElement(self._rep, elems[i]) for i in range(size)]
@property
def guard(self) -> Optional[Tuple[str, TheoryTerm]]:
"""
The guard of the atom or None if the atom has no guard.
"""
if not _c_call(
"bool", _lib.clingo_theory_atoms_atom_has_guard, self._rep, self._idx
):
return None
conn, term = _c_call2(
"char*",
"clingo_id_t",
_lib.clingo_theory_atoms_atom_guard,
self._rep,
self._idx,
)
return (_to_str(conn), TheoryTerm(self._rep, term))
@property
def literal(self) -> int:
"""
The program literal associated with the atom.
"""
return _c_call(
"clingo_literal_t",
_lib.clingo_theory_atoms_atom_literal,
self._rep,
self._idx,
)
@property
def term(self) -> TheoryTerm:
"""
The term of the atom.
"""
term = _c_call(
"clingo_id_t", _lib.clingo_theory_atoms_atom_term, self._rep, self._idx
)
return TheoryTerm(self._rep, term)
Classes
class TheoryAtom (rep, idx)
-
Class to represent theory atoms.
Theory atoms have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys.
Expand source code
@total_ordering class TheoryAtom: """ Class to represent theory atoms. Theory atoms have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys. """ def __init__(self, rep, idx): self._rep = rep self._idx = idx def __hash__(self): return self._idx def __eq__(self, other): return self._idx == other._idx def __lt__(self, other): return self._idx < other._idx def __str__(self): return _str( _lib.clingo_theory_atoms_atom_to_string_size, _lib.clingo_theory_atoms_atom_to_string, self._rep, self._idx, ) def __repr__(self): return f"TheoryAtom({self._rep!r})" @property def elements(self) -> List[TheoryElement]: """ The elements of the atom. """ elems, size = _c_call2( "clingo_id_t*", "size_t", _lib.clingo_theory_atoms_atom_elements, self._rep, self._idx, ) return [TheoryElement(self._rep, elems[i]) for i in range(size)] @property def guard(self) -> Optional[Tuple[str, TheoryTerm]]: """ The guard of the atom or None if the atom has no guard. """ if not _c_call( "bool", _lib.clingo_theory_atoms_atom_has_guard, self._rep, self._idx ): return None conn, term = _c_call2( "char*", "clingo_id_t", _lib.clingo_theory_atoms_atom_guard, self._rep, self._idx, ) return (_to_str(conn), TheoryTerm(self._rep, term)) @property def literal(self) -> int: """ The program literal associated with the atom. """ return _c_call( "clingo_literal_t", _lib.clingo_theory_atoms_atom_literal, self._rep, self._idx, ) @property def term(self) -> TheoryTerm: """ The term of the atom. """ term = _c_call( "clingo_id_t", _lib.clingo_theory_atoms_atom_term, self._rep, self._idx ) return TheoryTerm(self._rep, term)
Instance variables
var elements : List[TheoryElement]
-
The elements of the atom.
Expand source code
@property def elements(self) -> List[TheoryElement]: """ The elements of the atom. """ elems, size = _c_call2( "clingo_id_t*", "size_t", _lib.clingo_theory_atoms_atom_elements, self._rep, self._idx, ) return [TheoryElement(self._rep, elems[i]) for i in range(size)]
var guard : Optional[Tuple[str, TheoryTerm]]
-
The guard of the atom or None if the atom has no guard.
Expand source code
@property def guard(self) -> Optional[Tuple[str, TheoryTerm]]: """ The guard of the atom or None if the atom has no guard. """ if not _c_call( "bool", _lib.clingo_theory_atoms_atom_has_guard, self._rep, self._idx ): return None conn, term = _c_call2( "char*", "clingo_id_t", _lib.clingo_theory_atoms_atom_guard, self._rep, self._idx, ) return (_to_str(conn), TheoryTerm(self._rep, term))
var literal : int
-
The program literal associated with the atom.
Expand source code
@property def literal(self) -> int: """ The program literal associated with the atom. """ return _c_call( "clingo_literal_t", _lib.clingo_theory_atoms_atom_literal, self._rep, self._idx, )
var term : TheoryTerm
-
The term of the atom.
Expand source code
@property def term(self) -> TheoryTerm: """ The term of the atom. """ term = _c_call( "clingo_id_t", _lib.clingo_theory_atoms_atom_term, self._rep, self._idx ) return TheoryTerm(self._rep, term)
class TheoryElement (rep, idx)
-
Class to represent theory elements.
Theory elements have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys.
Expand source code
@total_ordering class TheoryElement: """ Class to represent theory elements. Theory elements have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys. """ def __init__(self, rep, idx): self._rep = rep self._idx = idx def __hash__(self): return self._idx def __eq__(self, other): return self._idx == other._idx def __lt__(self, other): return self._idx < other._idx def __str__(self): return _str( _lib.clingo_theory_atoms_element_to_string_size, _lib.clingo_theory_atoms_element_to_string, self._rep, self._idx, ) def __repr__(self): return f"TheoryElement({self._rep!r})" @property def condition(self) -> List[int]: """ The condition of the element in form of a list of program literals. """ cond, size = _c_call2( "clingo_literal_t*", "size_t", _lib.clingo_theory_atoms_element_condition, self._rep, self._idx, ) return [cond[i] for i in range(size)] @property def condition_id(self) -> int: """ Each condition has an id, which is a temporary program literal. This id can be passed to `clingo.propagator.PropagateInit.solver_literal` to obtain a corresponding solver literal. """ return _c_call( "clingo_literal_t", _lib.clingo_theory_atoms_element_condition_id, self._rep, self._idx, ) @property def terms(self) -> List[TheoryTerm]: """ The tuple of the element. """ terms, size = _c_call2( "clingo_id_t*", "size_t", _lib.clingo_theory_atoms_element_tuple, self._rep, self._idx, ) return [TheoryTerm(self._rep, terms[i]) for i in range(size)]
Instance variables
var condition : List[int]
-
The condition of the element in form of a list of program literals.
Expand source code
@property def condition(self) -> List[int]: """ The condition of the element in form of a list of program literals. """ cond, size = _c_call2( "clingo_literal_t*", "size_t", _lib.clingo_theory_atoms_element_condition, self._rep, self._idx, ) return [cond[i] for i in range(size)]
var condition_id : int
-
Each condition has an id, which is a temporary program literal. This id can be passed to
PropagateInit.solver_literal()
to obtain a corresponding solver literal.Expand source code
@property def condition_id(self) -> int: """ Each condition has an id, which is a temporary program literal. This id can be passed to `clingo.propagator.PropagateInit.solver_literal` to obtain a corresponding solver literal. """ return _c_call( "clingo_literal_t", _lib.clingo_theory_atoms_element_condition_id, self._rep, self._idx, )
var terms : List[TheoryTerm]
-
The tuple of the element.
Expand source code
@property def terms(self) -> List[TheoryTerm]: """ The tuple of the element. """ terms, size = _c_call2( "clingo_id_t*", "size_t", _lib.clingo_theory_atoms_element_tuple, self._rep, self._idx, ) return [TheoryTerm(self._rep, terms[i]) for i in range(size)]
class TheoryTerm (rep, idx)
-
TheoryTerm
objects represent theory terms.Theory terms have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys.
Expand source code
@total_ordering class TheoryTerm: """ `TheoryTerm` objects represent theory terms. Theory terms have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys. """ def __init__(self, rep, idx): self._rep = rep self._idx = idx def __hash__(self): return self._idx def __eq__(self, other): return self._idx == other._idx def __lt__(self, other): return self._idx < other._idx def __str__(self): return _str( _lib.clingo_theory_atoms_term_to_string_size, _lib.clingo_theory_atoms_term_to_string, self._rep, self._idx, ) def __repr__(self): return f"TheoryTerm({self._rep!r})" @property def arguments(self) -> List["TheoryTerm"]: """ The arguments of the term (for functions, tuples, list, and sets). """ args, size = _c_call2( "clingo_id_t*", "size_t", _lib.clingo_theory_atoms_term_arguments, self._rep, self._idx, ) return [TheoryTerm(self._rep, args[i]) for i in range(size)] @property def name(self) -> str: """ The name of the term (for symbols and functions). """ return _to_str( _c_call("char*", _lib.clingo_theory_atoms_term_name, self._rep, self._idx) ) @property def number(self) -> int: """ The numeric representation of the term (for numbers). """ return _c_call( "int", _lib.clingo_theory_atoms_term_number, self._rep, self._idx ) @property def type(self) -> TheoryTermType: """ The type of the theory term. """ type_ = _c_call( "clingo_theory_term_type_t", _lib.clingo_theory_atoms_term_type, self._rep, self._idx, ) return TheoryTermType(type_)
Instance variables
var arguments : List[TheoryTerm]
-
The arguments of the term (for functions, tuples, list, and sets).
Expand source code
@property def arguments(self) -> List["TheoryTerm"]: """ The arguments of the term (for functions, tuples, list, and sets). """ args, size = _c_call2( "clingo_id_t*", "size_t", _lib.clingo_theory_atoms_term_arguments, self._rep, self._idx, ) return [TheoryTerm(self._rep, args[i]) for i in range(size)]
var name : str
-
The name of the term (for symbols and functions).
Expand source code
@property def name(self) -> str: """ The name of the term (for symbols and functions). """ return _to_str( _c_call("char*", _lib.clingo_theory_atoms_term_name, self._rep, self._idx) )
var number : int
-
The numeric representation of the term (for numbers).
Expand source code
@property def number(self) -> int: """ The numeric representation of the term (for numbers). """ return _c_call( "int", _lib.clingo_theory_atoms_term_number, self._rep, self._idx )
var type : TheoryTermType
-
The type of the theory term.
Expand source code
@property def type(self) -> TheoryTermType: """ The type of the theory term. """ type_ = _c_call( "clingo_theory_term_type_t", _lib.clingo_theory_atoms_term_type, self._rep, self._idx, ) return TheoryTermType(type_)
class TheoryTermType (value, names=None, *, module=None, qualname=None, type=None, start=1)
-
Enumeration of theory term types.
Expand source code
class TheoryTermType(OrderedEnum): """ Enumeration of theory term types. """ Function = _lib.clingo_theory_term_type_function """ For a function theory terms. """ List = _lib.clingo_theory_term_type_list """ For list theory terms. """ Number = _lib.clingo_theory_term_type_number """ For numeric theory terms. """ Set = _lib.clingo_theory_term_type_set """ For set theory terms. """ Symbol = _lib.clingo_theory_term_type_symbol """ For symbolic theory terms (symbol here means the term is a string). """ Tuple = _lib.clingo_theory_term_type_tuple """ For tuple theory terms. """
Ancestors
- OrderedEnum
- enum.Enum
Class variables
var Function
-
For a function theory terms.
var List
-
For list theory terms.
var Number
-
For numeric theory terms.
var Set
-
For set theory terms.
var Symbol
-
For symbolic theory terms (symbol here means the term is a string).
var Tuple
-
For tuple theory terms.