propagator

ConstraintHandlerPropagator

Bases: Propagator

Propagator that evaluates constraint_handler variables during solving.

The propagator maintains a mapping from clingo symbols and solver literals to variable objects (see constraint_handler.PropagatorVariables). During propagation/check it evaluates affected variables, checks ensure constraints, and can add nogoods for conflicts or for pruning based on optimization or reasoning mode(brave/cautious).

Attributes:

Name	Type	Description
variable_manager	VariableManager	Manager for all variables and their associations.
evaluations	Evaluations	Collection of evaluated expressions and their results.
evaluatevars	list[EvaluateVariable]	List of EvaluateVariable instances to evaluate.
optimization	OptimizationModeHandler	Controller for objective sums, pruning, and optimal-model enumeration.
shared_values	list[SharedValue]	Collection of shared-value declarations.
environment	ImmutableList[constant]	Evaluation environment built from solver identifier.
check_only		If True, propagate becomes a no-op. Will only evaluate variables in check.
errors	propagator_warning_t	Warnings collected while evaluating variables or reading the input program.
configuration_errors	propagator_warning_t	Collection of configuration-related warnings.
reasoning_mode_handler		Handler for reasoning mode (standard, brave, cautious).
python_model	set[ResultAtom] | None	Stores the python-level model for output.
nogood_queue	list[Iterable[int]]	Queue of nogoods to be added during propagation.
forbidden_warnings	dict[Kind, int]	Mapping from warning kinds to their literals.
ignored_warnings	dict[Kind, tuple[int, bool]]	Mapping from warning kinds to their literal and truth value in the solver.
watches	set[int]	Set of solver literals being watched.

__init__

__init__() -> None

Initialize the propagator.

add_nogood_for_variable

add_nogood_for_variable(ctl: PropagateControl, var: VariableType | OptimizationHandler, extra_literals: Iterable[int] | None = None, conflict: bool = True) -> bool

Add a nogood blocking the current assignment for a variable.

The nogood is constructed from the literals that explain the variable's current value.

It is also possible to include extra literals that should be added to the nogood (e.g. to block only for the current optimization stage).

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo PropagateControl object.	required
var	VariableType | OptimizationHandler	Variable (or optimization handler) to block.	required
extra_literals	Iterable[int] | None	Additional literals to include in the nogood.	None
conflict	bool	Whether to treat the nogood as a conflict.	True

Returns: bool: True if propagation must stop False otherwise Raises: AssertionError: If we expected the nogood to be a conflict but the solver did not detect it

add_nogoods_from_queue

add_nogoods_from_queue(ctl: PropagateControl) -> bool

Add queued nogoods until the queue is empty or clingo refuses one.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo PropagateControl object.	required

Returns:

Name	Type	Description
bool	bool	True if adding a nogood failed (propagation must stop).

add_shared_values

add_shared_values(model: Model) -> None

Add evaluated shared-value atoms to the model.

Parameters:

Name	Type	Description	Default
model	Model	Clingo model to extend.	required

add_watch

add_watch(lit: int) -> None

Add a watch literal to the set of watched literals if check_only is disabled

Parameters:

Name	Type	Description	Default
lit	int	Literal to watch.	required

add_watches_to_ctl

add_watches_to_ctl(ctl: PropagateInit) -> None

Register all watch literals

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo PropagateInit object.	required

check

check(control: PropagateControl) -> None

Perform a full consistency check using the current solver assignment.

This evaluates all variables, checks ensure constraints and forbidden warnings, and applies optimization pruning by adding nogoods when necessary.

Parameters:

Name	Type	Description	Default
control	PropagateControl	Clingo PropagateControl object.	required

check_evaluate

check_evaluate(ctl: PropagateControl) -> None

Evaluate evaluate atoms against the current assignments.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo PropagateControl object.	required

check_shared_values

check_shared_values(ctl: PropagateControl) -> None

Evaluate shared values against the current assignments.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo PropagateControl object.	required

check_total

check_total(control: PropagateControl) -> None

Handle a total assignment.

This evaluates evaluate atoms, updates the python-side model for brave/cautious reasoning, and updates the incumbent objective value.

Parameters:

Name	Type	Description	Default
control	PropagateControl	Clingo PropagateControl object.	required

evaluate_expressions_at_rank

evaluate_expressions_at_rank(ctl: PropagateControl, rank: int, eval_by_rank_expr: dict[int, set[VariableValue]], eval_by_rank: dict[int, set[VariableType]], max_rank: int) -> int

Evaluate expressions at one rank and schedule their eligible owners.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo PropagateControl object.	required
rank	int	The current rank to evaluate.	required
eval_by_rank_expr	dict[int, set[VariableValue]]	Dictionary mapping ranks to sets of expressions to evaluate.	required
eval_by_rank	dict[int, set[VariableType]]	Dictionary mapping ranks to sets of variables to evaluate.	required
max_rank	int	The maximum rank encountered so far.	required

Returns:

Name	Type	Description
int	int	The updated maximum rank.

evaluate_model

evaluate_model(ctl: PropagateControl) -> bool

Update and (if needed) refine the accumulated python model.

In STANDARD mode this only rebuilds the python model and never backtracks. In BRAVE/CAUTIOUS mode, the model is accumulated across models and nogoods may be enqueued to force progress between stages.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo propagation control.	required

Returns:

Name	Type	Description
bool	bool	True if nogoods were added and propagation should stop.

evaluate_optimization_sum

evaluate_optimization_sum(ctl: PropagateControl) -> bool

Evaluate the current objective value and optionally prune.

If the objective is already worse than the incumbent and the relevant parts are fully assigned, a nogood is added to exclude the current partial/total assignment.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo propagation control.	required

Returns:

Name	Type	Description
bool	bool	True if a nogood was added requiring a backtrack.

evaluate_variable

evaluate_variable(ctl: PropagateControl, var: VariableType) -> bool | None

Evaluate one variable against the current assignment.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo PropagateControl object.	required
var	VariableType	Variable to evaluate.	required

Returns:

Type	Description
bool | None	bool | None: - True if the variable's value changed. - False if it did not change. - None if evaluation detected a conflict (nogood added).

evaluate_variables_at_rank

evaluate_variables_at_rank(ctl: PropagateControl, rank: int, eval_by_rank: dict[int, set[VariableType]], eval_by_rank_expr: dict[int, set[VariableValue]], max_rank: int) -> tuple[bool, int]

Evaluate variables at one rank and schedule their dependent expressions.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo PropagateControl object.	required
rank	int	The current rank to evaluate.	required
eval_by_rank	dict[int, set[VariableType]]	Dictionary mapping ranks to sets of variables to evaluate.	required
eval_by_rank_expr	dict[int, set[VariableValue]]	Dictionary mapping ranks to sets of expressions to evaluate.	required
max_rank	int	The maximum rank encountered so far.	required

Returns:

Type	Description
tuple[bool, int]	tuple[bool, int]: - True if a conflict was detected and backtracking is needed, False otherwise. - The updated maximum rank.

evaluated_solver_assignment

evaluated_solver_assignment(ctl: PropagateControl, to_evaluate: set[VariableType], to_evaluate_expressions: set[VariableValue]) -> bool

Evaluate scheduled variables and expressions in dependency-rank order.

As values become available, dependent expressions and their owning variables are scheduled for evaluation.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo PropagateControl object.	required
to_evaluate	set[VariableType]	Variables that may have been affected by recent changes.	required
to_evaluate_expressions	set[VariableValue]	Expressions that may have been affected by recent changes.	required

Returns:

Name	Type	Description
bool	bool	True if propagation should stop (conflict/forbidden warning),
	bool	False otherwise.

get_configuration

get_configuration(ctl: Control) -> None

Read clingo configuration and initialize reasoning and optimization settings.

The mode handlers configure their respective encodings and report incompatible heuristics.

Parameters:

Name	Type	Description	Default
ctl	Control	Clingo control instance.	required

get_forbidden_warnings

get_forbidden_warnings(ctl: PropagateInit) -> None

Load warning_forbid atoms.

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo propagation initializer.	required

get_reasons

get_reasons(var: VariableType | OptimizationHandler, seen: set[VariableType] | None = None) -> set[int]

Compute the set of literals explaining a variable's current value.

This is used when constructing nogoods for conflicts, forbidden warnings, and optimization pruning.

Parameters:

Name	Type	Description	Default
var	VariableType | OptimizationHandler	Variable whose reasons should be collected.	required
seen	set[VariableType] | None	Set of variables already visited to avoid infinite recursion. Defaults to None.	None

Returns: set[int]: Set of signed solver literals.

get_solver_identifier

get_solver_identifier(ctl: PropagateInit) -> None

Initialize the Python evaluation environment using the solver identifier.

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo PropagateInit object.	required

init

init(init: PropagateInit) -> None

Function implementing the init method of a Propagator. See clingo Propagator documentation for more details.

Parameters:

Name	Type	Description	Default
init	PropagateInit	Clingo PropagateInit object	required

on_model

on_model(model: Model) -> None

Extend the clingo model using python-side result atoms.

Parameters:

Name	Type	Description	Default
model	Model	Current clingo model.	required

propagate

propagate(control: PropagateControl, changes: Sequence[int]) -> None

Propagate after a solver assignment change. Checks which variables are affected by the change, evaluates them, and applies optimization pruning if enabled.

Parameters:

Name	Type	Description	Default
control	PropagateControl	Clingo propagation control.	required
changes	Sequence[int]	Sequence of (signed) solver literals that changed.	required

reset_evaluations

reset_evaluations(decision_level: int) -> None

Reset evaluations and dependency counters at or above a decision level.

Parameters:

Name	Type	Description	Default
decision_level	int	Decision level threshold for resetting expressions, variables, and optimization sums.	required

set_parents

set_parents() -> None

Remove engine variables that are not referenced by other managed variables.

Parent links are built only to identify unused engine variables, so no links need to be built when the manager contains none.

undo

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

Undo propagator state on backtracking.

This resets variable evaluations whose decision level is higher or equal to the current backtracking level and clears derived optimization state.

Parameters:

Name	Type	Description	Default
thread_id	int	Clingo thread id (unused).	required
assignment	Assignment	Current assignment after backtracking.	required
changes	Sequence[int]	Literals undone by clingo.	required

update_python_model

update_python_model() -> None

Build the python-side model representation from current variable values.

Populates self.python_model with result atoms (values, sets, multimaps, evaluated atoms) and warning atoms. This is used by on_model to extend the clingo model and by brave/cautious reasoning to accumulate results.