Propagators

Propagators for Explanation.

DecisionLevel = list[int] module-attribute

DecisionLevelList = list[DecisionLevel] module-attribute

__all__ = ['SolverDecisionPropagator'] module-attribute

SolverDecisionPropagator(signatures: set[tuple[str, int]] | None = None, callback_propagate: Callable[[list[Decision | list[Decision]]], None] | None = None, callback_undo: Callable[[], None] | None = None)

Bases: Propagator

Propagator for showing the Solver Decisions of clingo.

Construct a SolverDecisionPropagator watching decisions for the given signatures with the provided callbacks.

PARAMETER	DESCRIPTION
signatures	The set of fact signatures to match. TYPE: set[tuple[str, int]] | None DEFAULT: None
callback_propagate	The callback to invoke during propagation. TYPE: Callable[[list[Decision | list[Decision]]], None] | None DEFAULT: None
callback_undo	The callback to invoke during undo. TYPE: Callable[[], None] | None DEFAULT: None

get_decisions(assignment: clingo.Assignment) -> tuple[list[int], dict[int, list[int]]] staticmethod

Extract a list of decisions and entailments from a clingo propagator assignment.

init(init: clingo.PropagateInit) -> None

Initialize the Decision Order Propagator.

literal_to_decision(literal: int) -> Decision

Convert a literal integer to a Decision object.

literal_to_decision_sequence(literal_sequence: list[int | list[int]]) -> list[Decision | list[Decision]]

Convert a literal sequence into a decision sequence.

These sequences are made up of their respective types or lists of these types.

propagate(control: clingo.PropagateControl, changes: Sequence[int], use_diff: bool = True) -> None

Propagate method the is called when one the registered literals is propagated by clasp.

Here useful information about the decision progress is recorded to be visualized later.

undo(thread_id: int, assignment: clingo.Assignment, changes: Sequence[int]) -> None

Run when solvers decisions is undone.

constants

Constant definitions for the propagators package.

propagator_solver_decisions

Propagator for the decision order.

Decision(positive: bool, literal: int, symbol: clingo.Symbol | None) dataclass

A solver decision.

__str__() -> str

Return a string representation of the decision.

matches_any(signatures: set[tuple[str, int]], show_internal: bool = True) -> bool

Check if the decisions symbol matches any of the provided signatures.

If the decisions is an internal literal show_internal is returned.

SolverDecisionPropagator(signatures: set[tuple[str, int]] | None = None, callback_propagate: Callable[[list[Decision | list[Decision]]], None] | None = None, callback_undo: Callable[[], None] | None = None)

Bases: Propagator

Propagator for showing the Solver Decisions of clingo.

Construct a SolverDecisionPropagator watching decisions for the given signatures with the provided callbacks.

PARAMETER	DESCRIPTION
signatures	The set of fact signatures to match. TYPE: set[tuple[str, int]] | None DEFAULT: None
callback_propagate	The callback to invoke during propagation. TYPE: Callable[[list[Decision | list[Decision]]], None] | None DEFAULT: None
callback_undo	The callback to invoke during undo. TYPE: Callable[[], None] | None DEFAULT: None

get_decisions(assignment: clingo.Assignment) -> tuple[list[int], dict[int, list[int]]] staticmethod

Extract a list of decisions and entailments from a clingo propagator assignment.

init(init: clingo.PropagateInit) -> None

Initialize the Decision Order Propagator.

literal_to_decision(literal: int) -> Decision

Convert a literal integer to a Decision object.

literal_to_decision_sequence(literal_sequence: list[int | list[int]]) -> list[Decision | list[Decision]]

Convert a literal sequence into a decision sequence.

These sequences are made up of their respective types or lists of these types.

propagate(control: clingo.PropagateControl, changes: Sequence[int], use_diff: bool = True) -> None

Propagate method the is called when one the registered literals is propagated by clasp.

Here useful information about the decision progress is recorded to be visualized later.

undo(thread_id: int, assignment: clingo.Assignment, changes: Sequence[int]) -> None

Run when solvers decisions is undone.