Module clingo.backend
Functions and classes to observe or add ground statements.
Examples
The following example shows how to add a fact to a program via the backend and observe the corresponding rule passed to the backend:
>>> from clingo.symbol import Function
>>> from clingo.control import Control
>>>
>>> class Observer:
... def rule(self, choice, head, body):
... print("rule:", choice, head, body)
...
>>> ctl = Control()
>>> ctl.register_observer(Observer())
>>>
>>> sym_a = Function("a")
>>> with ctl.backend() as backend:
... atm_a = backend.add_atom(sym_a)
... backend.add_rule([atm_a])
...
rule: False [1] []
>>> ctl.symbolic_atoms[sym_a].is_fact
True
>>>
>>> print(ctl.solve(on_model=print))
a
SAT
Expand source code
'''
Functions and classes to observe or add ground statements.
Examples
--------
The following example shows how to add a fact to a program via the backend and
observe the corresponding rule passed to the backend:
>>> from clingo.symbol import Function
>>> from clingo.control import Control
>>>
>>> class Observer:
... def rule(self, choice, head, body):
... print("rule:", choice, head, body)
...
>>> ctl = Control()
>>> ctl.register_observer(Observer())
>>>
>>> sym_a = Function("a")
>>> with ctl.backend() as backend:
... atm_a = backend.add_atom(sym_a)
... backend.add_rule([atm_a])
...
rule: False [1] []
>>> ctl.symbolic_atoms[sym_a].is_fact
True
>>>
>>> print(ctl.solve(on_model=print))
a
SAT
'''
from typing import ContextManager, Sequence, Optional, Tuple
from enum import Enum
from abc import ABCMeta
from ._internal import _c_call, _cb_error_handler, _ffi, _handle_error, _lib, _to_str
from .core import TruthValue
from .symbol import Symbol
__all__ = [ 'Backend', 'HeuristicType', 'Observer' ]
class HeuristicType(Enum):
'''
Enumeration of the different heuristic types.
'''
Factor = _lib.clingo_heuristic_type_factor
'''
Heuristic modification to set the decaying factor of an atom.
'''
False_ = _lib.clingo_heuristic_type_false
'''
Heuristic modification to make an atom false.
'''
Init = _lib.clingo_heuristic_type_init
'''
Heuristic modification to set the inital score of an atom.
'''
Level = _lib.clingo_heuristic_type_level
'''
Heuristic modification to set the level of an atom.
'''
Sign = _lib.clingo_heuristic_type_sign
'''
Heuristic modification to set the sign of an atom.
'''
True_ = _lib.clingo_heuristic_type_true
'''
Heuristic modification to make an atom true.
'''
class Observer(metaclass=ABCMeta):
'''
Interface that has to be implemented to inspect rules produced during
grounding.
See Also
--------
clingo.control.Control.register_observer
Notes
-----
Not all functions the `Observer` interface have to be implemented and can
be omitted if not needed.
'''
def init_program(self, incremental: bool) -> None:
'''
Called once in the beginning.
Parameters
----------
incremental
Whether the program is incremental. If the incremental flag is
true, there can be multiple calls to `clingo.control.Control.solve`.
'''
def begin_step(self) -> None:
'''
Marks the beginning of a block of directives passed to the solver.
'''
def rule(self, choice: bool, head: Sequence[int], body: Sequence[int]) -> None:
'''
Observe rules passed to the solver.
Parameters
----------
choice
Determines if the head is a choice or a disjunction.
head
List of program atoms forming the rule head.
body
List of program literals forming the rule body.
'''
def weight_rule(self, choice: bool, head: Sequence[int], lower_bound: int,
body: Sequence[Tuple[int,int]]) -> None:
'''
Observe rules with one weight constraint in the body passed to the
solver.
Parameters
----------
choice
Determines if the head is a choice or a disjunction.
head
List of program atoms forming the head of the rule.
lower_bound
The lower bound of the weight constraint in the rule body.
body
List of weighted literals (pairs of literal and weight) forming the
elements of the weight constraint.
'''
def minimize(self, priority: int, literals: Sequence[Tuple[int,int]]) -> None:
'''
Observe minimize directives (or weak constraints) passed to the
solver.
Parameters
----------
priority
The priority of the directive.
literals
List of weighted literals whose sum to minimize (pairs of literal
and weight).
'''
def project(self, atoms: Sequence[int]) -> None:
'''
Observe projection directives passed to the solver.
Parameters
----------
atoms
The program atoms to project on.
'''
def output_atom(self, symbol: Symbol, atom: int) -> None:
'''
Observe shown atoms passed to the solver. Facts do not have an
associated program atom. The value of the atom is set to zero.
Parameters
----------
symbol
The symbolic representation of the atom.
atom
The associated program atom (`0` for facts).
'''
def output_term(self, symbol: Symbol, condition: Sequence[int]) -> None:
'''
Observe shown terms passed to the solver.
Parameters
----------
symbol
The symbolic representation of the term.
condition
List of program literals forming the condition when to show the
term.
'''
def output_csp(self, symbol: Symbol, value: int,
condition: Sequence[int]) -> None:
'''
Observe shown csp variables passed to the solver.
Parameters
----------
symbol
The symbolic representation of the variable.
value
The integer value of the variable.
condition
List of program literals forming the condition when to show the
variable with its value.
'''
def external(self, atom: int, value: TruthValue) -> None:
'''
Observe external statements passed to the solver.
Parameters
----------
atom
The external atom in form of a program literal.
value
The truth value of the external statement.
'''
def assume(self, literals: Sequence[int]) -> None:
'''
Observe assumption directives passed to the solver.
Parameters
----------
literals
The program literals to assume (positive literals are true and
negative literals false for the next solve call).
'''
def heuristic(self, atom: int, type_: HeuristicType, bias: int,
priority: int, condition: Sequence[int]) -> None:
'''
Observe heuristic directives passed to the solver.
Parameters
----------
atom
The program atom heuristically modified.
type_
The type of the modification.
bias
A signed integer.
priority
An unsigned integer.
condition
List of program literals.
'''
def acyc_edge(self, node_u: int, node_v: int,
condition: Sequence[int]) -> None:
'''
Observe edge directives passed to the solver.
Parameters
----------
node_u
The start vertex of the edge (in form of an integer).
node_v
Тhe end vertex of the edge (in form of an integer).
condition
The list of program literals forming th condition under which to
add the edge.
'''
def theory_term_number(self, term_id: int, number: int) -> None:
'''
Observe numeric theory terms.
Parameters
----------
term_id
The id of the term.
number
The value of the term.
'''
def theory_term_string(self, term_id : int, name : str) -> None:
'''
Observe string theory terms.
Parameters
----------
term_id
The id of the term.
name
The string value of the term.
'''
def theory_term_compound(self, term_id: int, name_id_or_type: int,
arguments: Sequence[int]) -> None:
'''
Observe compound theory terms.
Parameters
----------
term_id
The id of the term.
name_id_or_type
The name id or type of the term where the value `-1` stands for
tuples, `-2` for sets, `-3` for lists, or otherwise for the id of
the name (in form of a string term).
arguments
The arguments of the term in form of a list of term ids.
'''
def theory_element(self, element_id: int, terms: Sequence[int],
condition: Sequence[int]) -> None:
'''
Observe theory elements.
Parameters
----------
element_id
The id of the element.
terms
The term tuple of the element in form of a list of term ids.
condition
The list of program literals forming the condition.
'''
def theory_atom(self, atom_id_or_zero: int, term_id: int,
elements: Sequence[int]) -> None:
'''
Observe theory atoms without guard.
Parameters
----------
atom_id_or_zero
The id of the atom or zero for directives.
term_id
The term associated with the atom.
elements
The elements of the atom in form of a list of element ids.
'''
def theory_atom_with_guard(self, atom_id_or_zero: int, term_id: int,
elements: Sequence[int], operator_id: int,
right_hand_side_id: int) -> None:
'''
Observe theory atoms with guard.
Parameters
----------
atom_id_or_zero
The id of the atom or zero for directives.
term_id : int
The term associated with the atom.
elements
The elements of the atom in form of a list of element ids.
operator_id
The id of the operator (a string term).
right_hand_side_id
The id of the term on the right hand side of the atom.
'''
def end_step(self) -> None:
'''
Marks the end of a block of directives passed to the solver.
This function is called right before solving starts.
'''
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_init_program')
def _pyclingo_observer_init_program(incremental, data):
observer: Observer = _ffi.from_handle(data).data
observer.init_program(incremental)
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_begin_step')
def _pyclingo_observer_begin_step(data):
observer: Observer = _ffi.from_handle(data).data
observer.begin_step()
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_end_step')
def _pyclingo_observer_end_step(data):
observer: Observer = _ffi.from_handle(data).data
observer.end_step()
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_rule')
def _pyclingo_observer_rule(choice, head, head_size, body, body_size, data):
observer: Observer = _ffi.from_handle(data).data
observer.rule(
choice,
[ head[i] for i in range(head_size) ],
[ body[i] for i in range(body_size) ])
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_weight_rule')
def _pyclingo_observer_weight_rule(choice, head, head_size, lower_bound, body, body_size, data):
observer: Observer = _ffi.from_handle(data).data
observer.weight_rule(
choice,
[ head[i] for i in range(head_size) ],
lower_bound,
[ (body[i].literal, body[i].weight) for i in range(body_size) ])
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_minimize')
def _pyclingo_observer_minimize(priority, literals, size, data):
observer: Observer = _ffi.from_handle(data).data
observer.minimize(priority, [ (literals[i].literal, literals[i].weight) for i in range(size) ])
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_project')
def _pyclingo_observer_project(atoms, size, data):
observer: Observer = _ffi.from_handle(data).data
observer.project([ atoms[i] for i in range(size) ])
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_output_atom')
def _pyclingo_observer_output_atom(symbol, atom, data):
observer: Observer = _ffi.from_handle(data).data
observer.output_atom(Symbol(symbol), atom)
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_output_term')
def _pyclingo_observer_output_term(symbol, condition, size, data):
observer: Observer = _ffi.from_handle(data).data
observer.output_term(Symbol(symbol), [ condition[i] for i in range(size) ])
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_output_csp')
def _pyclingo_observer_output_csp(symbol, value, condition, size, data):
observer: Observer = _ffi.from_handle(data).data
observer.output_csp(Symbol(symbol), value, [ condition[i] for i in range(size) ])
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_external')
def _pyclingo_observer_external(atom, type_, data):
observer: Observer = _ffi.from_handle(data).data
observer.external(atom, TruthValue(type_))
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_assume')
def _pyclingo_observer_assume(literals, size, data):
observer: Observer = _ffi.from_handle(data).data
observer.assume([ literals[i] for i in range(size) ])
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_heuristic')
def _pyclingo_observer_heuristic(atom, type_, bias, priority, condition, size, data):
observer: Observer = _ffi.from_handle(data).data
observer.heuristic(atom, HeuristicType(type_), bias, priority, [ condition[i] for i in range(size) ])
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_acyc_edge')
def _pyclingo_observer_acyc_edge(node_u, node_v, condition, size, data):
observer: Observer = _ffi.from_handle(data).data
observer.acyc_edge(node_u, node_v, [ condition[i] for i in range(size) ])
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_theory_term_number')
def _pyclingo_observer_theory_term_number(term_id, number, data):
observer: Observer = _ffi.from_handle(data).data
observer.theory_term_number(term_id, number)
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_theory_term_string')
def _pyclingo_observer_theory_term_string(term_id, name, data):
observer: Observer = _ffi.from_handle(data).data
observer.theory_term_string(term_id, _to_str(name))
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_theory_term_compound')
def _pyclingo_observer_theory_term_compound(term_id, name_id_or_type, arguments, size, data):
observer: Observer = _ffi.from_handle(data).data
observer.theory_term_compound(term_id, name_id_or_type, [ arguments[i] for i in range(size) ])
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_theory_element')
def _pyclingo_observer_theory_element(element_id, terms, terms_size, condition, condition_size, data):
observer: Observer = _ffi.from_handle(data).data
observer.theory_element(
element_id,
[ terms[i] for i in range(terms_size) ],
[ condition[i] for i in range(condition_size) ])
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_theory_atom')
def _pyclingo_observer_theory_atom(atom_id_or_zero, term_id, elements, size, data):
observer: Observer = _ffi.from_handle(data).data
observer.theory_atom(atom_id_or_zero, term_id, [ elements[i] for i in range(size) ])
return True
@_ffi.def_extern(onerror=_cb_error_handler('data'), name='pyclingo_observer_theory_atom_with_guard')
def _pyclingo_observer_theory_atom_with_guard(atom_id_or_zero, term_id, elements, size,
operator_id, right_hand_side_id, data):
observer: Observer = _ffi.from_handle(data).data
observer.theory_atom_with_guard(
atom_id_or_zero, term_id,
[ elements[i] for i in range(size) ],
operator_id, right_hand_side_id)
return True
class Backend(ContextManager['Backend']):
'''
Backend object providing a low level interface to extend a logic program.
This class allows for adding statements in ASPIF format.
See Also
--------
clingo.control.Control.backend
Notes
-----
The `Backend` is a context manager and must be used with Python's `with`
statement.
'''
def __init__(self, rep, error):
self._rep = rep
self._error = error
def __enter__(self):
self._error.clear()
_handle_error(_lib.clingo_backend_begin(self._rep), handler=self._error)
return self
def __exit__(self, exc_type, exc_val, exc_tb):
self._error.clear()
_handle_error(_lib.clingo_backend_end(self._rep), handler=self._error)
return False
def add_acyc_edge(self, node_u: int, node_v: int, condition: Sequence[int]) -> None:
'''
Add an edge directive to the program.
Parameters
----------
node_u
The start node represented as an unsigned integer.
node_v
The end node represented as an unsigned integer.
condition
List of program literals.
'''
_handle_error(_lib.clingo_backend_acyc_edge(self._rep, node_u, node_v, condition, len(condition)))
def add_assume(self, literals: Sequence[int]) -> None:
'''
Add assumptions to the program.
Parameters
----------
literals
The list of literals to assume true.
'''
_handle_error(_lib.clingo_backend_assume(self._rep, literals, len(literals)))
def add_atom(self, symbol: Optional[Symbol]=None) -> int:
'''
Return a fresh program atom or the atom associated with the given symbol.
If the given symbol does not exist in the atom base, it is added first. Such
atoms will be used in subequents calls to ground for instantiation.
Parameters
----------
symbol
The symbol associated with the atom.
Returns
-------
The program atom representing the atom.
'''
# pylint: disable=protected-access
if symbol is None:
p_sym = _ffi.NULL
else:
p_sym = _ffi.new('clingo_symbol_t*', symbol._rep)
self._error.clear()
return _c_call('clingo_atom_t', _lib.clingo_backend_add_atom, self._rep, p_sym, handler=self._error)
def add_external(self, atom : int, value : TruthValue=TruthValue.False_) -> None:
'''
Mark a program atom as external optionally fixing its truth value.
Parameters
----------
atom
The program atom to mark as external.
value
Optional truth value.
Notes
-----
Can also be used to release an external atom using `TruthValue.Release`.
'''
_handle_error(_lib.clingo_backend_external(self._rep, atom, value.value))
def add_heuristic(self, atom: int, type_: HeuristicType, bias: int, priority: int,
condition: Sequence[int]) -> None:
'''
Add a heuristic directive to the program.
Parameters
----------
atom
Program atom to heuristically modify.
type_
The type of modification.
bias
A signed integer.
priority
An unsigned integer.
condition
List of program literals.
'''
_handle_error(_lib.clingo_backend_heuristic(self._rep, atom, type_.value, bias, priority,
condition, len(condition)))
def add_minimize(self, priority: int, literals: Sequence[Tuple[int,int]]) -> None:
'''
Add a minimize constraint to the program.
Parameters
----------
priority
Integer for the priority.
literals
List of pairs of program literals and weights.
'''
_handle_error(_lib.clingo_backend_minimize(self._rep, priority, literals, len(literals)))
def add_project(self, atoms: Sequence[int]) -> None:
'''
Add a project statement to the program.
Parameters
----------
atoms
List of program atoms to project on.
'''
_handle_error(_lib.clingo_backend_project(self._rep, atoms, len(atoms)))
def add_rule(self, head: Sequence[int], body: Sequence[int]=[], choice: bool=False) -> None:
'''
Add a disjuntive or choice rule to the program.
Parameters
----------
head
The program atoms forming the rule head.
body
The program literals forming the rule body.
choice
Whether to add a disjunctive or choice rule.
Notes
-----
Integrity constraints and normal rules can be added by using an empty or
singleton head list, respectively.
'''
# pylint: disable=dangerous-default-value
_handle_error(_lib.clingo_backend_rule(self._rep, choice, head, len(head), body, len(body)))
def add_weight_rule(self, head: Sequence[int], lower: int, body: Sequence[Tuple[int,int]],
choice: bool=False) -> None:
'''
Add a disjuntive or choice rule with one weight constraint with a lower bound
in the body to the program.
Parameters
----------
head
The program atoms forming the rule head.
lower
The lower bound.
body
The pairs of program literals and weights forming the elements of the
weight constraint.
choice
Whether to add a disjunctive or choice rule.
'''
_handle_error(_lib.clingo_backend_weight_rule(self._rep, choice, head, len(head), lower, body, len(body)))Classes
class Backend (rep, error)-
Backend object providing a low level interface to extend a logic program.
This class allows for adding statements in ASPIF format.
See Also
Notes
The
Backendis a context manager and must be used with Python'swithstatement.Expand source code
class Backend(ContextManager['Backend']): ''' Backend object providing a low level interface to extend a logic program. This class allows for adding statements in ASPIF format. See Also -------- clingo.control.Control.backend Notes ----- The `Backend` is a context manager and must be used with Python's `with` statement. ''' def __init__(self, rep, error): self._rep = rep self._error = error def __enter__(self): self._error.clear() _handle_error(_lib.clingo_backend_begin(self._rep), handler=self._error) return self def __exit__(self, exc_type, exc_val, exc_tb): self._error.clear() _handle_error(_lib.clingo_backend_end(self._rep), handler=self._error) return False def add_acyc_edge(self, node_u: int, node_v: int, condition: Sequence[int]) -> None: ''' Add an edge directive to the program. Parameters ---------- node_u The start node represented as an unsigned integer. node_v The end node represented as an unsigned integer. condition List of program literals. ''' _handle_error(_lib.clingo_backend_acyc_edge(self._rep, node_u, node_v, condition, len(condition))) def add_assume(self, literals: Sequence[int]) -> None: ''' Add assumptions to the program. Parameters ---------- literals The list of literals to assume true. ''' _handle_error(_lib.clingo_backend_assume(self._rep, literals, len(literals))) def add_atom(self, symbol: Optional[Symbol]=None) -> int: ''' Return a fresh program atom or the atom associated with the given symbol. If the given symbol does not exist in the atom base, it is added first. Such atoms will be used in subequents calls to ground for instantiation. Parameters ---------- symbol The symbol associated with the atom. Returns ------- The program atom representing the atom. ''' # pylint: disable=protected-access if symbol is None: p_sym = _ffi.NULL else: p_sym = _ffi.new('clingo_symbol_t*', symbol._rep) self._error.clear() return _c_call('clingo_atom_t', _lib.clingo_backend_add_atom, self._rep, p_sym, handler=self._error) def add_external(self, atom : int, value : TruthValue=TruthValue.False_) -> None: ''' Mark a program atom as external optionally fixing its truth value. Parameters ---------- atom The program atom to mark as external. value Optional truth value. Notes ----- Can also be used to release an external atom using `TruthValue.Release`. ''' _handle_error(_lib.clingo_backend_external(self._rep, atom, value.value)) def add_heuristic(self, atom: int, type_: HeuristicType, bias: int, priority: int, condition: Sequence[int]) -> None: ''' Add a heuristic directive to the program. Parameters ---------- atom Program atom to heuristically modify. type_ The type of modification. bias A signed integer. priority An unsigned integer. condition List of program literals. ''' _handle_error(_lib.clingo_backend_heuristic(self._rep, atom, type_.value, bias, priority, condition, len(condition))) def add_minimize(self, priority: int, literals: Sequence[Tuple[int,int]]) -> None: ''' Add a minimize constraint to the program. Parameters ---------- priority Integer for the priority. literals List of pairs of program literals and weights. ''' _handle_error(_lib.clingo_backend_minimize(self._rep, priority, literals, len(literals))) def add_project(self, atoms: Sequence[int]) -> None: ''' Add a project statement to the program. Parameters ---------- atoms List of program atoms to project on. ''' _handle_error(_lib.clingo_backend_project(self._rep, atoms, len(atoms))) def add_rule(self, head: Sequence[int], body: Sequence[int]=[], choice: bool=False) -> None: ''' Add a disjuntive or choice rule to the program. Parameters ---------- head The program atoms forming the rule head. body The program literals forming the rule body. choice Whether to add a disjunctive or choice rule. Notes ----- Integrity constraints and normal rules can be added by using an empty or singleton head list, respectively. ''' # pylint: disable=dangerous-default-value _handle_error(_lib.clingo_backend_rule(self._rep, choice, head, len(head), body, len(body))) def add_weight_rule(self, head: Sequence[int], lower: int, body: Sequence[Tuple[int,int]], choice: bool=False) -> None: ''' Add a disjuntive or choice rule with one weight constraint with a lower bound in the body to the program. Parameters ---------- head The program atoms forming the rule head. lower The lower bound. body The pairs of program literals and weights forming the elements of the weight constraint. choice Whether to add a disjunctive or choice rule. ''' _handle_error(_lib.clingo_backend_weight_rule(self._rep, choice, head, len(head), lower, body, len(body)))Ancestors
- contextlib.AbstractContextManager
- abc.ABC
- typing.Generic
Methods
def add_acyc_edge(self, node_u: int, node_v: int, condition: Sequence[int]) ‑> None-
Add an edge directive to the program.
Parameters
node_u- The start node represented as an unsigned integer.
node_v- The end node represented as an unsigned integer.
condition- List of program literals.
Expand source code
def add_acyc_edge(self, node_u: int, node_v: int, condition: Sequence[int]) -> None: ''' Add an edge directive to the program. Parameters ---------- node_u The start node represented as an unsigned integer. node_v The end node represented as an unsigned integer. condition List of program literals. ''' _handle_error(_lib.clingo_backend_acyc_edge(self._rep, node_u, node_v, condition, len(condition))) def add_assume(self, literals: Sequence[int]) ‑> None-
Add assumptions to the program.
Parameters
literals- The list of literals to assume true.
Expand source code
def add_assume(self, literals: Sequence[int]) -> None: ''' Add assumptions to the program. Parameters ---------- literals The list of literals to assume true. ''' _handle_error(_lib.clingo_backend_assume(self._rep, literals, len(literals))) def add_atom(self, symbol: Optional[Symbol] = None) ‑> int-
Return a fresh program atom or the atom associated with the given symbol.
If the given symbol does not exist in the atom base, it is added first. Such atoms will be used in subequents calls to ground for instantiation.
Parameters
symbol- The symbol associated with the atom.
Returns
The program atom representing the atom.
Expand source code
def add_atom(self, symbol: Optional[Symbol]=None) -> int: ''' Return a fresh program atom or the atom associated with the given symbol. If the given symbol does not exist in the atom base, it is added first. Such atoms will be used in subequents calls to ground for instantiation. Parameters ---------- symbol The symbol associated with the atom. Returns ------- The program atom representing the atom. ''' # pylint: disable=protected-access if symbol is None: p_sym = _ffi.NULL else: p_sym = _ffi.new('clingo_symbol_t*', symbol._rep) self._error.clear() return _c_call('clingo_atom_t', _lib.clingo_backend_add_atom, self._rep, p_sym, handler=self._error) def add_external(self, atom: int, value: TruthValue = TruthValue.False_) ‑> None-
Mark a program atom as external optionally fixing its truth value.
Parameters
atom- The program atom to mark as external.
value- Optional truth value.
Notes
Can also be used to release an external atom using
TruthValue.Release.Expand source code
def add_external(self, atom : int, value : TruthValue=TruthValue.False_) -> None: ''' Mark a program atom as external optionally fixing its truth value. Parameters ---------- atom The program atom to mark as external. value Optional truth value. Notes ----- Can also be used to release an external atom using `TruthValue.Release`. ''' _handle_error(_lib.clingo_backend_external(self._rep, atom, value.value)) def add_heuristic(self, atom: int, type_: HeuristicType, bias: int, priority: int, condition: Sequence[int]) ‑> None-
Add a heuristic directive to the program.
Parameters
atom- Program atom to heuristically modify.
type_- The type of modification.
bias- A signed integer.
priority- An unsigned integer.
condition- List of program literals.
Expand source code
def add_heuristic(self, atom: int, type_: HeuristicType, bias: int, priority: int, condition: Sequence[int]) -> None: ''' Add a heuristic directive to the program. Parameters ---------- atom Program atom to heuristically modify. type_ The type of modification. bias A signed integer. priority An unsigned integer. condition List of program literals. ''' _handle_error(_lib.clingo_backend_heuristic(self._rep, atom, type_.value, bias, priority, condition, len(condition))) def add_minimize(self, priority: int, literals: Sequence[Tuple[int, int]]) ‑> None-
Add a minimize constraint to the program.
Parameters
priority- Integer for the priority.
literals- List of pairs of program literals and weights.
Expand source code
def add_minimize(self, priority: int, literals: Sequence[Tuple[int,int]]) -> None: ''' Add a minimize constraint to the program. Parameters ---------- priority Integer for the priority. literals List of pairs of program literals and weights. ''' _handle_error(_lib.clingo_backend_minimize(self._rep, priority, literals, len(literals))) def add_project(self, atoms: Sequence[int]) ‑> None-
Add a project statement to the program.
Parameters
atoms- List of program atoms to project on.
Expand source code
def add_project(self, atoms: Sequence[int]) -> None: ''' Add a project statement to the program. Parameters ---------- atoms List of program atoms to project on. ''' _handle_error(_lib.clingo_backend_project(self._rep, atoms, len(atoms))) def add_rule(self, head: Sequence[int], body: Sequence[int] = [], choice: bool = False) ‑> None-
Add a disjuntive or choice rule to the program.
Parameters
head- The program atoms forming the rule head.
body- The program literals forming the rule body.
choice- Whether to add a disjunctive or choice rule.
Notes
Integrity constraints and normal rules can be added by using an empty or singleton head list, respectively.
Expand source code
def add_rule(self, head: Sequence[int], body: Sequence[int]=[], choice: bool=False) -> None: ''' Add a disjuntive or choice rule to the program. Parameters ---------- head The program atoms forming the rule head. body The program literals forming the rule body. choice Whether to add a disjunctive or choice rule. Notes ----- Integrity constraints and normal rules can be added by using an empty or singleton head list, respectively. ''' # pylint: disable=dangerous-default-value _handle_error(_lib.clingo_backend_rule(self._rep, choice, head, len(head), body, len(body))) def add_weight_rule(self, head: Sequence[int], lower: int, body: Sequence[Tuple[int, int]], choice: bool = False) ‑> None-
Add a disjuntive or choice rule with one weight constraint with a lower bound in the body to the program.
Parameters
head- The program atoms forming the rule head.
lower- The lower bound.
body- The pairs of program literals and weights forming the elements of the weight constraint.
choice- Whether to add a disjunctive or choice rule.
Expand source code
def add_weight_rule(self, head: Sequence[int], lower: int, body: Sequence[Tuple[int,int]], choice: bool=False) -> None: ''' Add a disjuntive or choice rule with one weight constraint with a lower bound in the body to the program. Parameters ---------- head The program atoms forming the rule head. lower The lower bound. body The pairs of program literals and weights forming the elements of the weight constraint. choice Whether to add a disjunctive or choice rule. ''' _handle_error(_lib.clingo_backend_weight_rule(self._rep, choice, head, len(head), lower, body, len(body)))
class HeuristicType (value, names=None, *, module=None, qualname=None, type=None, start=1)-
Enumeration of the different heuristic types.
Expand source code
class HeuristicType(Enum): ''' Enumeration of the different heuristic types. ''' Factor = _lib.clingo_heuristic_type_factor ''' Heuristic modification to set the decaying factor of an atom. ''' False_ = _lib.clingo_heuristic_type_false ''' Heuristic modification to make an atom false. ''' Init = _lib.clingo_heuristic_type_init ''' Heuristic modification to set the inital score of an atom. ''' Level = _lib.clingo_heuristic_type_level ''' Heuristic modification to set the level of an atom. ''' Sign = _lib.clingo_heuristic_type_sign ''' Heuristic modification to set the sign of an atom. ''' True_ = _lib.clingo_heuristic_type_true ''' Heuristic modification to make an atom true. '''Ancestors
- enum.Enum
Class variables
var Factor-
Heuristic modification to set the decaying factor of an atom.
var False_-
Heuristic modification to make an atom false.
var Init-
Heuristic modification to set the inital score of an atom.
var Level-
Heuristic modification to set the level of an atom.
var Sign-
Heuristic modification to set the sign of an atom.
var True_-
Heuristic modification to make an atom true.
class Observer-
Interface that has to be implemented to inspect rules produced during grounding.
See Also
Notes
Not all functions the
Observerinterface have to be implemented and can be omitted if not needed.Expand source code
class Observer(metaclass=ABCMeta): ''' Interface that has to be implemented to inspect rules produced during grounding. See Also -------- clingo.control.Control.register_observer Notes ----- Not all functions the `Observer` interface have to be implemented and can be omitted if not needed. ''' def init_program(self, incremental: bool) -> None: ''' Called once in the beginning. Parameters ---------- incremental Whether the program is incremental. If the incremental flag is true, there can be multiple calls to `clingo.control.Control.solve`. ''' def begin_step(self) -> None: ''' Marks the beginning of a block of directives passed to the solver. ''' def rule(self, choice: bool, head: Sequence[int], body: Sequence[int]) -> None: ''' Observe rules passed to the solver. Parameters ---------- choice Determines if the head is a choice or a disjunction. head List of program atoms forming the rule head. body List of program literals forming the rule body. ''' def weight_rule(self, choice: bool, head: Sequence[int], lower_bound: int, body: Sequence[Tuple[int,int]]) -> None: ''' Observe rules with one weight constraint in the body passed to the solver. Parameters ---------- choice Determines if the head is a choice or a disjunction. head List of program atoms forming the head of the rule. lower_bound The lower bound of the weight constraint in the rule body. body List of weighted literals (pairs of literal and weight) forming the elements of the weight constraint. ''' def minimize(self, priority: int, literals: Sequence[Tuple[int,int]]) -> None: ''' Observe minimize directives (or weak constraints) passed to the solver. Parameters ---------- priority The priority of the directive. literals List of weighted literals whose sum to minimize (pairs of literal and weight). ''' def project(self, atoms: Sequence[int]) -> None: ''' Observe projection directives passed to the solver. Parameters ---------- atoms The program atoms to project on. ''' def output_atom(self, symbol: Symbol, atom: int) -> None: ''' Observe shown atoms passed to the solver. Facts do not have an associated program atom. The value of the atom is set to zero. Parameters ---------- symbol The symbolic representation of the atom. atom The associated program atom (`0` for facts). ''' def output_term(self, symbol: Symbol, condition: Sequence[int]) -> None: ''' Observe shown terms passed to the solver. Parameters ---------- symbol The symbolic representation of the term. condition List of program literals forming the condition when to show the term. ''' def output_csp(self, symbol: Symbol, value: int, condition: Sequence[int]) -> None: ''' Observe shown csp variables passed to the solver. Parameters ---------- symbol The symbolic representation of the variable. value The integer value of the variable. condition List of program literals forming the condition when to show the variable with its value. ''' def external(self, atom: int, value: TruthValue) -> None: ''' Observe external statements passed to the solver. Parameters ---------- atom The external atom in form of a program literal. value The truth value of the external statement. ''' def assume(self, literals: Sequence[int]) -> None: ''' Observe assumption directives passed to the solver. Parameters ---------- literals The program literals to assume (positive literals are true and negative literals false for the next solve call). ''' def heuristic(self, atom: int, type_: HeuristicType, bias: int, priority: int, condition: Sequence[int]) -> None: ''' Observe heuristic directives passed to the solver. Parameters ---------- atom The program atom heuristically modified. type_ The type of the modification. bias A signed integer. priority An unsigned integer. condition List of program literals. ''' def acyc_edge(self, node_u: int, node_v: int, condition: Sequence[int]) -> None: ''' Observe edge directives passed to the solver. Parameters ---------- node_u The start vertex of the edge (in form of an integer). node_v Тhe end vertex of the edge (in form of an integer). condition The list of program literals forming th condition under which to add the edge. ''' def theory_term_number(self, term_id: int, number: int) -> None: ''' Observe numeric theory terms. Parameters ---------- term_id The id of the term. number The value of the term. ''' def theory_term_string(self, term_id : int, name : str) -> None: ''' Observe string theory terms. Parameters ---------- term_id The id of the term. name The string value of the term. ''' def theory_term_compound(self, term_id: int, name_id_or_type: int, arguments: Sequence[int]) -> None: ''' Observe compound theory terms. Parameters ---------- term_id The id of the term. name_id_or_type The name id or type of the term where the value `-1` stands for tuples, `-2` for sets, `-3` for lists, or otherwise for the id of the name (in form of a string term). arguments The arguments of the term in form of a list of term ids. ''' def theory_element(self, element_id: int, terms: Sequence[int], condition: Sequence[int]) -> None: ''' Observe theory elements. Parameters ---------- element_id The id of the element. terms The term tuple of the element in form of a list of term ids. condition The list of program literals forming the condition. ''' def theory_atom(self, atom_id_or_zero: int, term_id: int, elements: Sequence[int]) -> None: ''' Observe theory atoms without guard. Parameters ---------- atom_id_or_zero The id of the atom or zero for directives. term_id The term associated with the atom. elements The elements of the atom in form of a list of element ids. ''' def theory_atom_with_guard(self, atom_id_or_zero: int, term_id: int, elements: Sequence[int], operator_id: int, right_hand_side_id: int) -> None: ''' Observe theory atoms with guard. Parameters ---------- atom_id_or_zero The id of the atom or zero for directives. term_id : int The term associated with the atom. elements The elements of the atom in form of a list of element ids. operator_id The id of the operator (a string term). right_hand_side_id The id of the term on the right hand side of the atom. ''' def end_step(self) -> None: ''' Marks the end of a block of directives passed to the solver. This function is called right before solving starts. '''Subclasses
Methods
def acyc_edge(self, node_u: int, node_v: int, condition: Sequence[int]) ‑> None-
Observe edge directives passed to the solver.
Parameters
node_u- The start vertex of the edge (in form of an integer).
node_v- Тhe end vertex of the edge (in form of an integer).
condition- The list of program literals forming th condition under which to add the edge.
Expand source code
def acyc_edge(self, node_u: int, node_v: int, condition: Sequence[int]) -> None: ''' Observe edge directives passed to the solver. Parameters ---------- node_u The start vertex of the edge (in form of an integer). node_v Тhe end vertex of the edge (in form of an integer). condition The list of program literals forming th condition under which to add the edge. ''' def assume(self, literals: Sequence[int]) ‑> None-
Observe assumption directives passed to the solver.
Parameters
literals- The program literals to assume (positive literals are true and negative literals false for the next solve call).
Expand source code
def assume(self, literals: Sequence[int]) -> None: ''' Observe assumption directives passed to the solver. Parameters ---------- literals The program literals to assume (positive literals are true and negative literals false for the next solve call). ''' def begin_step(self) ‑> None-
Marks the beginning of a block of directives passed to the solver.
Expand source code
def begin_step(self) -> None: ''' Marks the beginning of a block of directives passed to the solver. ''' def end_step(self) ‑> None-
Marks the end of a block of directives passed to the solver.
This function is called right before solving starts.
Expand source code
def end_step(self) -> None: ''' Marks the end of a block of directives passed to the solver. This function is called right before solving starts. ''' def external(self, atom: int, value: TruthValue) ‑> None-
Observe external statements passed to the solver.
Parameters
atom- The external atom in form of a program literal.
value- The truth value of the external statement.
Expand source code
def external(self, atom: int, value: TruthValue) -> None: ''' Observe external statements passed to the solver. Parameters ---------- atom The external atom in form of a program literal. value The truth value of the external statement. ''' def heuristic(self, atom: int, type_: HeuristicType, bias: int, priority: int, condition: Sequence[int]) ‑> None-
Observe heuristic directives passed to the solver.
Parameters
atom- The program atom heuristically modified.
type_- The type of the modification.
bias- A signed integer.
priority- An unsigned integer.
condition- List of program literals.
Expand source code
def heuristic(self, atom: int, type_: HeuristicType, bias: int, priority: int, condition: Sequence[int]) -> None: ''' Observe heuristic directives passed to the solver. Parameters ---------- atom The program atom heuristically modified. type_ The type of the modification. bias A signed integer. priority An unsigned integer. condition List of program literals. ''' def init_program(self, incremental: bool) ‑> None-
Called once in the beginning.
Parameters
incremental- Whether the program is incremental. If the incremental flag is
true, there can be multiple calls to
Control.solve().
Expand source code
def init_program(self, incremental: bool) -> None: ''' Called once in the beginning. Parameters ---------- incremental Whether the program is incremental. If the incremental flag is true, there can be multiple calls to `clingo.control.Control.solve`. ''' def minimize(self, priority: int, literals: Sequence[Tuple[int, int]]) ‑> None-
Observe minimize directives (or weak constraints) passed to the solver.
Parameters
priority- The priority of the directive.
literals- List of weighted literals whose sum to minimize (pairs of literal and weight).
Expand source code
def minimize(self, priority: int, literals: Sequence[Tuple[int,int]]) -> None: ''' Observe minimize directives (or weak constraints) passed to the solver. Parameters ---------- priority The priority of the directive. literals List of weighted literals whose sum to minimize (pairs of literal and weight). ''' def output_atom(self, symbol: Symbol, atom: int) ‑> None-
Observe shown atoms passed to the solver. Facts do not have an associated program atom. The value of the atom is set to zero.
Parameters
symbol- The symbolic representation of the atom.
atom- The associated program atom (
0for facts).
Expand source code
def output_atom(self, symbol: Symbol, atom: int) -> None: ''' Observe shown atoms passed to the solver. Facts do not have an associated program atom. The value of the atom is set to zero. Parameters ---------- symbol The symbolic representation of the atom. atom The associated program atom (`0` for facts). ''' def output_csp(self, symbol: Symbol, value: int, condition: Sequence[int]) ‑> None-
Observe shown csp variables passed to the solver.
Parameters
symbol- The symbolic representation of the variable.
value- The integer value of the variable.
condition- List of program literals forming the condition when to show the variable with its value.
Expand source code
def output_csp(self, symbol: Symbol, value: int, condition: Sequence[int]) -> None: ''' Observe shown csp variables passed to the solver. Parameters ---------- symbol The symbolic representation of the variable. value The integer value of the variable. condition List of program literals forming the condition when to show the variable with its value. ''' def output_term(self, symbol: Symbol, condition: Sequence[int]) ‑> None-
Observe shown terms passed to the solver.
Parameters
symbol- The symbolic representation of the term.
condition- List of program literals forming the condition when to show the term.
Expand source code
def output_term(self, symbol: Symbol, condition: Sequence[int]) -> None: ''' Observe shown terms passed to the solver. Parameters ---------- symbol The symbolic representation of the term. condition List of program literals forming the condition when to show the term. ''' def project(self, atoms: Sequence[int]) ‑> None-
Observe projection directives passed to the solver.
Parameters
atoms- The program atoms to project on.
Expand source code
def project(self, atoms: Sequence[int]) -> None: ''' Observe projection directives passed to the solver. Parameters ---------- atoms The program atoms to project on. ''' def rule(self, choice: bool, head: Sequence[int], body: Sequence[int]) ‑> None-
Observe rules passed to the solver.
Parameters
choice- Determines if the head is a choice or a disjunction.
head- List of program atoms forming the rule head.
body- List of program literals forming the rule body.
Expand source code
def rule(self, choice: bool, head: Sequence[int], body: Sequence[int]) -> None: ''' Observe rules passed to the solver. Parameters ---------- choice Determines if the head is a choice or a disjunction. head List of program atoms forming the rule head. body List of program literals forming the rule body. ''' def theory_atom(self, atom_id_or_zero: int, term_id: int, elements: Sequence[int]) ‑> None-
Observe theory atoms without guard.
Parameters
atom_id_or_zero- The id of the atom or zero for directives.
term_id- The term associated with the atom.
elements- The elements of the atom in form of a list of element ids.
Expand source code
def theory_atom(self, atom_id_or_zero: int, term_id: int, elements: Sequence[int]) -> None: ''' Observe theory atoms without guard. Parameters ---------- atom_id_or_zero The id of the atom or zero for directives. term_id The term associated with the atom. elements The elements of the atom in form of a list of element ids. ''' def theory_atom_with_guard(self, atom_id_or_zero: int, term_id: int, elements: Sequence[int], operator_id: int, right_hand_side_id: int) ‑> None-
Observe theory atoms with guard.
Parameters
atom_id_or_zero- The id of the atom or zero for directives.
term_id:int- The term associated with the atom.
elements- The elements of the atom in form of a list of element ids.
operator_id- The id of the operator (a string term).
right_hand_side_id- The id of the term on the right hand side of the atom.
Expand source code
def theory_atom_with_guard(self, atom_id_or_zero: int, term_id: int, elements: Sequence[int], operator_id: int, right_hand_side_id: int) -> None: ''' Observe theory atoms with guard. Parameters ---------- atom_id_or_zero The id of the atom or zero for directives. term_id : int The term associated with the atom. elements The elements of the atom in form of a list of element ids. operator_id The id of the operator (a string term). right_hand_side_id The id of the term on the right hand side of the atom. ''' def theory_element(self, element_id: int, terms: Sequence[int], condition: Sequence[int]) ‑> None-
Observe theory elements.
Parameters
element_id- The id of the element.
terms- The term tuple of the element in form of a list of term ids.
condition- The list of program literals forming the condition.
Expand source code
def theory_element(self, element_id: int, terms: Sequence[int], condition: Sequence[int]) -> None: ''' Observe theory elements. Parameters ---------- element_id The id of the element. terms The term tuple of the element in form of a list of term ids. condition The list of program literals forming the condition. ''' def theory_term_compound(self, term_id: int, name_id_or_type: int, arguments: Sequence[int]) ‑> None-
Observe compound theory terms.
Parameters
term_id- The id of the term.
name_id_or_type- The name id or type of the term where the value
-1stands for tuples,-2for sets,-3for lists, or otherwise for the id of the name (in form of a string term). arguments- The arguments of the term in form of a list of term ids.
Expand source code
def theory_term_compound(self, term_id: int, name_id_or_type: int, arguments: Sequence[int]) -> None: ''' Observe compound theory terms. Parameters ---------- term_id The id of the term. name_id_or_type The name id or type of the term where the value `-1` stands for tuples, `-2` for sets, `-3` for lists, or otherwise for the id of the name (in form of a string term). arguments The arguments of the term in form of a list of term ids. ''' def theory_term_number(self, term_id: int, number: int) ‑> None-
Observe numeric theory terms.
Parameters
term_id- The id of the term.
number- The value of the term.
Expand source code
def theory_term_number(self, term_id: int, number: int) -> None: ''' Observe numeric theory terms. Parameters ---------- term_id The id of the term. number The value of the term. ''' def theory_term_string(self, term_id: int, name: str) ‑> None-
Observe string theory terms.
Parameters
term_id- The id of the term.
name- The string value of the term.
Expand source code
def theory_term_string(self, term_id : int, name : str) -> None: ''' Observe string theory terms. Parameters ---------- term_id The id of the term. name The string value of the term. ''' def weight_rule(self, choice: bool, head: Sequence[int], lower_bound: int, body: Sequence[Tuple[int, int]]) ‑> None-
Observe rules with one weight constraint in the body passed to the solver.
Parameters
choice- Determines if the head is a choice or a disjunction.
head- List of program atoms forming the head of the rule.
lower_bound- The lower bound of the weight constraint in the rule body.
body- List of weighted literals (pairs of literal and weight) forming the elements of the weight constraint.
Expand source code
def weight_rule(self, choice: bool, head: Sequence[int], lower_bound: int, body: Sequence[Tuple[int,int]]) -> None: ''' Observe rules with one weight constraint in the body passed to the solver. Parameters ---------- choice Determines if the head is a choice or a disjunction. head List of program atoms forming the head of the rule. lower_bound The lower bound of the weight constraint in the rule body. body List of weighted literals (pairs of literal and weight) forming the elements of the weight constraint. '''