Clingo::PropagateInit Class Reference

Object to initialize a user-defined propagator before each solving step. More...

#include <propagate.hh>

Inheritance diagram for Clingo::PropagateInit:

Public Member Functions
	PropagateInit (clingo_propagate_init_t *init)
	Constructor from the underlying C representation.
auto	library () const -> Library
	Get the library object associated with the propagator.
auto	base () const -> Base
	Get the base object associated with the propagator.
auto	check_mode () const -> PropagatorCheckMode
	Get the check mode of the propagator.
void	check_mode (PropagatorCheckMode mode)
	Set the check mode of the propagator.
auto	number_of_threads () const -> ProgramId
	Get the number of threads used in subsequent solving.
auto	undo_mode () const -> PropagatorUndoMode
	Get the undo mode of the propagator.
void	undo_mode (PropagatorUndoMode mode) const
	Set the undo mode of the propagator.
auto	solver_literal (ProgramLiteral literal) const -> SolverLiteral
	Map a program literal to a solver literal.
void	add_minimize (SolverLiteral literal, Weight weight, Weight priority) const
	Add a weighted literal to minimize to the solver.
void	freeze_literal (SolverLiteral literal) const
	Freeze the given literal in the solver.
Public Member Functions inherited from Clingo::PropagateControl
	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

Object to initialize a user-defined propagator before each solving step.

Each symbolic or theory atom is uniquely associated with an aspif atom in form of a positive integer (Clingo::ProgramLiteral). Aspif literals additionally are signed to represent default negation. Furthermore, there are non-zero integer solver literals (SolverLiteral). There is a surjective mapping from program atoms to solver literals.

All methods called during propagation use solver literals, whereas Clingo::Atom::literal() and Clingo::TheoryAtom::literal() return program literals. The function Clingo::PropagateInit::solver_literal() can be used to map program literals or condition ids to solver literals.

Constructor & Destructor Documentation

PropagateInit()

Clingo::PropagateInit::PropagateInit ( clingo_propagate_init_t *  init )

inlineexplicit

Constructor from the underlying C representation.

Parameters

init	the C representation of the initialization object

Member Function Documentation

add_minimize()

void Clingo::PropagateInit::add_minimize ( SolverLiteral  literal, Weight  weight, Weight  priority  ) const

inline

Add a weighted literal to minimize to the solver.

Parameters

literal	the literal to minimize
weight	the weight of the literal
priority	the priority of the literal

base()

auto Clingo::PropagateInit::base ( ) const -> Base

inline

Get the base object associated with the propagator.

Returns

the base object associated with the propagator

check_mode() [1/2]

auto Clingo::PropagateInit::check_mode ( ) const -> PropagatorCheckMode

inline

Get the check mode of the propagator.

Returns

the check mode of the propagator

check_mode() [2/2]

void Clingo::PropagateInit::check_mode ( PropagatorCheckMode  mode )

inline

Set the check mode of the propagator.

Parameters

mode	the new check mode of the propagator

freeze_literal()

void Clingo::PropagateInit::freeze_literal ( SolverLiteral  literal ) const

inline

Freeze the given literal in the solver.

Frozen literals are exempt from elimination during preprocessing.

Parameters

literal

the literal to freeze

library()

auto Clingo::PropagateInit::library ( ) const -> Library

inline

Get the library object associated with the propagator.

Returns

the library object associated with the propagator

number_of_threads()

auto Clingo::PropagateInit::number_of_threads ( ) const -> ProgramId

inline

Get the number of threads used in subsequent solving.

Returns

the number of threads used in subsequent solving

solver_literal()

auto Clingo::PropagateInit::solver_literal ( ProgramLiteral  literal ) const -> SolverLiteral

inline

Map a program literal to a solver literal.

Parameters

literal

the program literal to map

Returns

the corresponding solver literal

undo_mode() [1/2]

auto Clingo::PropagateInit::undo_mode ( ) const -> PropagatorUndoMode

inline

Get the undo mode of the propagator.

Returns

the undo mode of the propagator

undo_mode() [2/2]

void Clingo::PropagateInit::undo_mode ( PropagatorUndoMode  mode ) const

inline

Set the undo mode of the propagator.

Parameters

mode	the new undo mode of the propagator

---

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

• clingo/propagate.hh