Clingo::PropagateControl Class Reference

Class to control a user-defined propagator. More...

#include <propagate.hh>

Inheritance diagram for Clingo::PropagateControl:

Public Member Functions
	PropagateControl (clingo_propagate_control_t *ctl)
	Constructor from the underlying C representation.
	PropagateControl (clingo_propagate_init_t *init)
	Constructor from the underlying C representation.
auto	add_literal (bool freeze=true) const -> SolverLiteral
	Adds a literal to the problem or the active solver thread.
auto	add_clause (SolverLiteralSpan literals, ClauseFlags flags=ClauseFlags::none) const -> bool
	Add a clause to the solver.
auto	add_clause (SolverLiteralList literals, ClauseFlags flags=ClauseFlags::none) const -> bool
	Add a clause to the solver.
auto	add_weight_constraint (SolverLiteral literal, WeightedLiteralSpan literals, Weight bound, WeightConstraintType type) const -> bool
	Add a weight constraint to the solver.
auto	add_nogood (SolverLiteralSpan literals, ClauseFlags flags=ClauseFlags::none) const -> bool
	Add a nogood to the solver.
void	add_watch (SolverLiteral literal) const
	Add a watch for the given solver literal.
auto	has_watch (SolverLiteral literal) const -> bool
	Check whether the given solver literal is watched in the current context.
void	remove_watch (SolverLiteral lit) const
	Remove a watch for the given solver literal.
auto	propagate () const -> bool
	Propagate consequences of previously added clauses.

Detailed Description

Class to control a user-defined propagator.

This class provides methods for adding clauses, literals, and nogoods, as well as managing watches and performing propagation.

Constructor & Destructor Documentation

PropagateControl() [1/2]

Clingo::PropagateControl::PropagateControl ( clingo_propagate_control_t *  ctl )

inlineexplicit

Constructor from the underlying C representation.

Parameters

ctl	the C representation of the control object

PropagateControl() [2/2]

Clingo::PropagateControl::PropagateControl ( clingo_propagate_init_t *  init )

inlineexplicit

Constructor from the underlying C representation.

Parameters

init	the C representation of the init object

Member Function Documentation

add_clause() [1/2]

auto Clingo::PropagateControl::add_clause ( SolverLiteralList  literals, ClauseFlags  flags = ClauseFlags::none  ) const -> bool

inline

Add a clause to the solver.

If adding the clause results in a conflict or requires backtracking, the function returns false and the calling propagator must not add further clauses from the current callback.

Parameters

literals	the literals of the clause to add
flags	the flags for the clause

Returns

whether the clause was added without conflict

add_clause() [2/2]

auto Clingo::PropagateControl::add_clause ( SolverLiteralSpan  literals, ClauseFlags  flags = ClauseFlags::none  ) const -> bool

inline

Add a clause to the solver.

If adding the clause results in a conflict or requires backtracking, the function returns false and the calling propagator must not add further clauses from the current callback.

Parameters

literals	the literals of the clause to add
flags	the flags for the clause

Returns

whether the clause was added without conflict

add_literal()

auto Clingo::PropagateControl::add_literal ( bool  freeze = true ) const -> SolverLiteral

inline

Adds a literal to the problem or the active solver thread.

Note

If the function is called in the context of a particular solver thread, the literal is solver local: solver local literals are not shared between solvers and are removed at the end of the current solving step.

Parameters

freeze

whether to freeze the literal

Returns

the added literal

add_nogood()

auto Clingo::PropagateControl::add_nogood ( SolverLiteralSpan  literals, ClauseFlags  flags = ClauseFlags::none  ) const -> bool

inline

Add a nogood to the solver.

This is the same as calling add_clause() with the negated literals.

Parameters

literals	the literals of the nogood to add
flags	the flags for the nogood

Returns

whether the nogood was added without conflict

add_watch()

void Clingo::PropagateControl::add_watch ( SolverLiteral  literal ) const

inline

Add a watch for the given solver literal.

Note

If called in the context of initialization, the watch is added to all current and future solving threads. Otherwise, the watch is only added to the active solving thread.

Parameters

literal

the literal to watch

add_weight_constraint()

auto Clingo::PropagateControl::add_weight_constraint ( SolverLiteral  literal, WeightedLiteralSpan  literals, Weight  bound, WeightConstraintType  type  ) const -> bool

inline

Add a weight constraint to the solver.

Parameters

literal	the literal associated with the constraint
literals	the weighted literals of the constraint
bound	the bound of the constraint
type	the type of the weight constraint

Returns

whether the constraint was added without a conflict

has_watch()

auto Clingo::PropagateControl::has_watch ( SolverLiteral  literal ) const -> bool

inline

Check whether the given solver literal is watched in the current context.

Parameters

literal

the literal to check

Returns

whether the literal is watched

propagate()

auto Clingo::PropagateControl::propagate ( ) const -> bool

inline

Propagate consequences of previously added clauses.

If a conflict is detected during propagation, the function returns false and the calling propagator must not add further clauses from the current callback.

Returns

whether propagation succeeded without conflict

remove_watch()

void Clingo::PropagateControl::remove_watch ( SolverLiteral  lit ) const

inline

Remove a watch for the given solver literal.

Parameters

lit	the literal to remove the watch for

---

The documentation for this class was generated from the following file:

• clingo/propagate.hh