clingo.backend

Functions and classes to observe or add ground statements.

Examples

The first example shows how to add a fact to a program:

>>> from clingo.core import Library
>>> from clingo.symbol import Function
>>> from clingo.control import Control
...
>>> lib = Library()
>>> ctl = Control(lib)
>>> sym = Function(lib, "a")
>>> with ctl.backend as bck:
...     atm_a = bck.atom(sym)
...     bck.rule([atm_a])
>>> ctl.base.is_fact(ctl.base[sym].literal)
True
>>> with ctl.solve(on_model=print) as hnd:
...     hnd.get()
a
SAT

The next example shows how to add theory atoms to a program:

>>> from clingo.core import Library
>>> from clingo.symbol import Function
>>> from clingo.control import Control
...
>>> lib = Library()
>>> ctl = Control(lib)
...
>>> with ctl.backend as bck:
...     n = Function(lib, "p")
...     a = bck.theory_string("a")
...     o = bck.theory_number(1)
...     f = bck.theory_function("f", [a, o])
...     e = bck.theory_element([f], [])
...     bck.theory_atom(0, n, [e])
...
>>> print(ctl.base.theory[0])
&p { f(a,1) }
class Backend:

Provides an interface to extend a logic program.

This class offers methods to add various types of rules, set external atoms, specify heuristics, define optimization statements, and extend the underlying theory. It allows for low-level manipulation of logic programs.

See Also:

clingo.control.Control.backend

def assume(self, literals: Sequence[int]) -> None:

Add an assumption directive to the solver.

Specifies literals to be assumed true or false for the next solving call. Positive literals are treated as true, while negative literals are treated as false. These assumptions apply only to the next solve call.

Arguments:
  • literals: Sequence of program literals to assume.
def atom(self, symbol: clingo.symbol.Symbol | None = 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. These atoms will be used in subsequent calls to ground for instantiation.

Arguments:
  • symbol: The symbol associated with the atom.
Returns:

The program atom representing the atom.

def edge(self, node_u: int, node_v: int, condition: Sequence[int]) -> None:

Add an edge directive.

Adds an edge from node_u to node_v to the graph. The edge is subject to the specified condition.

Arguments:
  • node_u: The start node of the edge.
  • node_v: The end node of the edge.
  • condition: Sequence of literals representing the edge condition.
def external(self, atom: int, type: ExternalType) -> None:

Add an external directive.

Declares an atom as external and sets its truth value according to the specified type. External atoms can be used as assumptions or for incremental solving. The special value ExternalType.Release can be used to permanently set an external atom to false.

Arguments:
  • atom: The external atom (must be a positive literal).
  • type: The type determining the truth value of the atom.
def heuristic( self, atom: int, type: HeuristicType, weight: int, priority: int = 0, condition: Sequence[int] = []) -> None:

Add a heuristic directive for an atom.

Adds a heuristic directive for the given atom, influencing the solver's search process. The directive's effect depends on its type, weight, and priority. The condition, if provided, determines when the heuristic should be applied.

Arguments:
  • atom: The atom to which the heuristic applies.
  • type: The type of the heuristic.
  • weight: The weight of the heuristic.
  • priority: The priority of the heuristic (default: 0).
  • condition: Sequence of literals representing the condition (default: []).
def minimize(self, literals: Sequence[tuple[int, int]], priority: int = 0) -> None:

Add a minimize constraint to the program.

Adds a minimize constraint, which instructs the solver to minimize the sum of weights of true literals in the given sequence. Multiple minimize constraints with different priorities can be added, with lower priority values considered more important.

Arguments:
  • literals: Sequence of (literal, weight) tuples to minimize.
  • priority: Priority of the constraint (default: 0).
def project(self, atoms: Sequence[int]) -> None:

Add a projection directive to the program.

Specifies which atoms should be considered in stable models. When projection is used, stable models are treated as equivalent if they agree on the truth values of projected atoms, regardless of other atoms in the model.

Arguments:
  • atoms: Sequence of atoms to project on.
def rule( self, head: Sequence[int], body: Sequence[int] = [], choice: bool = False) -> None:

Add a rule to the program.

Creates a disjunctive or choice rule based on the choice parameter. The head and body are specified as sequences of literals.

Rule types based on head length (when choice is False):

  • Empty head: Integrity constraint
  • Single literal head: Normal rule
  • Multiple literals head: Disjunctive rule
Arguments:
  • head: Sequence of literals in the rule head.
  • body: Sequence of literals in the rule body (default: []).
  • choice: If True, adds a choice rule; otherwise, a disjunctive rule (default: False).
def theory_atom( self, atom: int | None, name: clingo.symbol.Symbol, elements: Sequence[int], guard: tuple[str, int] | None = None) -> int:

Create a theory atom and return its associated program atom.

If the theory atom does not exist yet, the method assigns a program atom based on these rules:

  • If a specific atom value is provided, that value is used.
  • If None is given, a fresh program atom is introduced.
  • For program directives, value zero is used.
Arguments:
  • atom: The program atom to assign, or None to assign a fresh one.
  • name: The name of the theory atom.
  • elements: A sequence of ids representing theory elements.
  • guard: A tuple containing the guard operator and the id of the guard term, or None if there is no guard.
Returns:

The program atom associated with the created theory atom.

def theory_element(self, tuple: Sequence[int], condition: Sequence[int]) -> int:

Create a theory element.

The method creates a theory element consisting of a tuple and a condition, and returns its unique identifier. This id can be used in other theory-related methods to reference this element.

Arguments:
  • tuple: A sequence of ids representing theory terms.
  • condition: A sequence of program literals.
Returns:

The unique id of the created theory element.

def theory_function(self, name: str, arguments: Sequence[int]) -> int:

Create a function theory term.

The method creates a function theory term with the given name and arguments, and returns its unique identifier. This id can be used in other theory-related methods to reference this term.

Arguments:
  • name: The name of the function.
  • arguments: A sequence of ids of theory terms.
Returns:

The unique id of the created function theory term.

def theory_number(self, number: int) -> int:

Create a numeric theory term.

The function creates a numeric theory term with the given value and return its unique identifier. This id can be used in other theory-related methods to reference this term.

Arguments:
  • number: The numeric value of the theory term to create.
Returns:

The unique id of the created theory term.

def theory_sequence( self, type: TheorySequenceType, elements: Sequence[int]) -> int:

Create a sequence theory term.

The method creates a sequence theory term of the specified type, containing the given elements, and returns its unique identifier. This id can be used in other theory-related methods to reference this term.

Arguments:
  • type: The type of the sequence (e.g., tuple, list, set).
  • elements: A sequence of ids representing theory terms.
Returns:

The unique id of the created sequence theory term.

def theory_string(self, string: str) -> int:

Create a string theory term.

The method creates a string theory term with the given value and returns its unique identifier. This id can be used in other theory-related methods to reference this term.

Arguments:
  • string: The string value of the theory term to create.
Returns:

The unique id of the created string theory term.

def theory_symbol(self, symbol: clingo.symbol.Symbol) -> int:

Convert a symbol into a theory term.

The method converts the given symbol into a theory term and returns its unique identifier. This id can be used in other theory-related methods to reference this term.

Arguments:
  • symbol: The symbol to create the theory term from.
Returns:

The unique id of the created theory term.

def weight_rule( self, head: Sequence[int], lower_bound: int, body: Sequence[tuple[int, int]], choice: bool = False) -> None:

Add a weight rule to the program.

Adds a weight rule, where the body is a weight constraint. The head is either a disjunction ro choice (see Backend.rule for more details).

A weight constraint is satisfied if the sum of weights of the true literals meets or exceeds the lower bound.

Arguments:
  • head: Sequence of literals in the rule head.
  • lower_bound: The lower bound of the weight constraint.
  • body: Sequence of (literal, weight) tuples forming the weight constraint.
  • choice: If True, adds a choice rule; otherwise, a disjunctive rule (default: False).
class BackendManager:

A context manager to initialize and finalize a backend.

class ExternalType:

Available external types.

ExternalType(value: int)
False_: ClassVar[ExternalType] = ExternalType.False_

Make an external atom false.

Free: ClassVar[ExternalType] = ExternalType.Free

Make an external atom a choice.

Release: ClassVar[ExternalType] = ExternalType.Release

Release an external atom.

True_: ClassVar[ExternalType] = ExternalType.True_

Make an external atom true.

name: str
value: int
class HeuristicType:

Available heuristic types.

HeuristicType(value: int)
Factor: ClassVar[HeuristicType] = HeuristicType.Factor

The factor modifier.

False_: ClassVar[HeuristicType] = HeuristicType.False_

The false modifier.

Init: ClassVar[HeuristicType] = HeuristicType.Init

The init modifier.

Level: ClassVar[HeuristicType] = HeuristicType.Level

The level modifier.

Sign: ClassVar[HeuristicType] = HeuristicType.Sign

The sign modifier.

True_: ClassVar[HeuristicType] = HeuristicType.True_

The true modifier.

name: str
value: int
class Observer:

ABC to inspect aspif directives.

Not all functions of the interface have to be implemented and can be omitted if not needed.

See Also:

clingo.control.Control.observe

def assume(self, literals: Sequence[int]) -> None:

Called for assumptions in the solver.

See also Backend.assume.

Arguments:
  • literals: Sequence of program literals to assume.
def begin_step(self) -> None:

Called at the beginning of a step.

def edge(self, node_u: int, node_v: int, condition: Sequence[int]) -> None:

Called for edge directives in the program.

See also Backend.edge.

Arguments:
  • node_u: The start node of the edge.
  • node_v: The end node of the edge.
  • condition: Sequence of literals representing the edge condition.
def end_step(self, base: clingo.base.Base) -> None:

Called at the end of a step.

def external(self, atom: int, type: ExternalType) -> None:

Called for external directives in the program.

See also Backend.external.

Arguments:
  • atom: The external atom (must be a positive literal).
  • type: The type determining the truth value of the atom.
def heuristic( self, atom: int, type: HeuristicType, weight: int, priority: int, condition: Sequence[int]) -> None:

Called for heuristic directives in the program.

See also Backend.heuristic.

Arguments:
  • atom: The atom to which the heuristic applies.
  • type: The type of the heuristic.
  • weight: The weight of the heuristic.
  • priority: The priority of the heuristic (default: 0).
  • condition: Sequence of literals representing the condition (default: []).
def init_program(self, incremental: bool) -> None:

The first directive in a program.

The parameter incremental indicates whether the program can consist of more than one step.

Arguments:
  • incremental: Whether the program is incremental.
def minimize(self, literals: Sequence[tuple[int, int]], priority: int) -> None:

Called for minimize constraints in the program.

See also Backend.minimize.

Arguments:
  • literals: Sequence of (literal, weight) tuples to minimize.
  • priority: Priority of the constraint (default: 0).
def project(self, atoms: Sequence[int]) -> None:

Called for projection directives in the program.

See also Backend.project.

Arguments:
  • atoms: Sequence of atoms to project on.
def rule(self, head: Sequence[int], body: Sequence[int], choice: bool) -> None:

Called for rules in the program.

See also Backend.rule.

Arguments:
  • head: Sequence of literals in the rule head.
  • body: Sequence of literals in the rule body (default: []).
  • choice: If True, adds a choice rule; otherwise, a disjunctive rule (default: False).
def weight_rule( self, head: Sequence[int], lower_bound: int, body: Sequence[tuple[int, int]], choice: bool) -> None:

Called for weight rules in the program.

See also Backend.weight_rule.

Arguments:
  • head: Sequence of literals in the rule head.
  • lower_bound: The lower bound of the weight constraint.
  • body: Sequence of (literal, weight) tuples forming the weight constraint.
  • choice: If True, adds a choice rule; otherwise, a disjunctive rule (default: False).
class TheorySequenceType:

Available theory sequence types.

TheorySequenceType(value: int)
List: ClassVar[TheorySequenceType] = TheorySequenceType.List

Sequences enclosed in brackets.

Set: ClassVar[TheorySequenceType] = TheorySequenceType.Set

Sequences enclosed in braces.

Tuple: ClassVar[TheorySequenceType] = TheorySequenceType.Tuple

Sequences enclosed in parentheses.

name: str
value: int