Clingo::PropagateInit Class Reference

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

#include <propagate.hh>

Public Member Functions
	PropagateInit (clingo_propagate_init_t *init)
	Constructor from the underlying C representation.
auto	assignment () const -> Assignment
	Get the assignment of the current solver.
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	add_clause (SolverLiteralSpan literals) const -> bool
	Add a clause to the solver.
auto	add_clause (SolverLiteralList literals) const -> bool
	Add a clause to the solver.
auto	add_literal (bool freeze=true) const -> SolverLiteral
	Add a literal to the solver.
void	add_minimize (SolverLiteral literal, Weight weight, Weight priority) const
	Add a weighted literal to minimize to the solver.
void	add_watch (SolverLiteral literal, std::optional< ProgramId > thread_id=std::nullopt) const
	Add a watch for the given solver literal.
auto	add_weight_constraint (SolverLiteral literal, WeightedLiteralSpan literals, Weight bound, WeightConstraintType type, bool compare_equal) const -> bool
	Add a weight constraint to the solver.
void	freeze_literal (SolverLiteral literal) const
	Freeze the given literal in the solver.
auto	propagate () const -> bool
	Propagate consequences of the underlying problem.
void	remove_watch (SolverLiteral literal, std::optional< ProgramId > thread_id) const
	Remove a watch for the given solver literal.
auto	solver_literal (ProgramLiteral literal) const -> SolverLiteral
	Map a program literal to a solver literal.

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_clause() [1/2]

auto Clingo::PropagateInit::add_clause ( SolverLiteralList  literals ) const -> bool

inline

Add a clause to the solver.

If the clause could not be added to the solver, there is a top-level conflict and the underlying problem is unsatisfiable. The function returns false in this case.

Parameters

literals

the literals of the clause to add

Returns

whether the clause was added without conflict

add_clause() [2/2]

auto Clingo::PropagateInit::add_clause ( SolverLiteralSpan  literals ) const -> bool

inline

Add a clause to the solver.

If the clause could not be added to the solver, there is a top-level conflict and the underlying problem is unsatisfiable. The function returns false in this case.

Parameters

literals

the literals of the clause to add

Returns

whether the clause was added without conflict

add_literal()

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

inline

Add a literal to the solver.

The literal can be frozen to exempt it from being eliminated during preprocessing.

Parameters

freeze

whether to freeze the literal

Returns

the added literal

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

add_watch()

void Clingo::PropagateInit::add_watch ( SolverLiteral  literal, std::optional< ProgramId >  thread_id = std::nullopt  ) const

inline

Add a watch for the given solver literal.

The Clingo::Propagator::propagate() is called whenever the watched literal is assigned a truth value.

Literals can be added to the given thread or all threads if no thread id is given.

Parameters

literal	the literal to watch
thread_id	the id of the thread to add the watch to

add_weight_constraint()

auto Clingo::PropagateInit::add_weight_constraint ( SolverLiteral  literal, WeightedLiteralSpan  literals, Weight  bound, WeightConstraintType  type, bool  compare_equal  ) 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
compare_equal	if true compare equal instead of less than equal

Returns

whether the constraint was added without conflict

assignment()

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

inline

Get the assignment of the current solver.

Returns

the assignment of the current solver

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 not eliminated 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

propagate()

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

inline

Propagate consequences of the underlying problem.

This function can be called to propagte consequences of previously added clauses and weight constraints.

Returns

whether propagation succeeded without conflict

remove_watch()

void Clingo::PropagateInit::remove_watch ( SolverLiteral  literal, std::optional< ProgramId >  thread_id  ) const

inline

Remove a watch for the given solver literal.

If no thread id is given, the watch is removed from all threads.

Parameters

literal	the literal to remove the watch for
thread_id	the id of the thread to remove the watch from

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