Clingo::PropagateControl Class Reference

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

#include <propagate.hh>

Public Member Functions
	PropagateControl (clingo_propagate_control_t *ctl)
	Constructor from the underlying C representation.
auto	add_literal () const -> SolverLiteral
	Add solver local literal to the solver.
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_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.
auto	propagate () const -> bool
	Propagate consequences of previously added clauses.
void	remove_watch (SolverLiteral lit) const
	Remove a watch for the given solver literal.
auto	assignment () const -> Assignment
	Get the assignment of the current solver.
auto	thread_id () const -> ProgramId
	Get the thread id of the current solver.

Detailed Description

Class to control propagation of 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()

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

inlineexplicit

Constructor from the underlying C representation.

Parameters

ctl	the C representation of the control 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, 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, 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 ( ) const -> SolverLiteral

inline

Add solver local literal to the solver.

Solver local literals are not shared between solvers and are removed at the end of the current solving step.

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.

Parameters

literal

the literal to watch

assignment()

auto Clingo::PropagateControl::assignment ( ) const -> Assignment

inline

Get the assignment of the current solver.

Returns

the assignment of the current solver

has_watch()

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

inline

Check whether the given solver literal is watched.

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 confilct 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

thread_id()

auto Clingo::PropagateControl::thread_id ( ) const -> ProgramId

inline

Get the thread id of the current solver.

Returns

the thread id of the current solver

---

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

• clingo/propagate.hh