Clingo::Assignment Class Reference

Represents a (partial) assignment of a particular solver. More...

#include <propagate.hh>

Public Types
using	value_type = SolverLiteral
	The value type, which is a solver literal.
using	size_type = std::size_t
	The size type.
using	difference_type = std::ptrdiff_t
	The difference type.
using	reference = value_type
	The reference type, which simply refers to the value type.
using	pointer = Detail::ArrowProxy< value_type >
	The pointer type, which is a proxy to the value type.
using	iterator = Detail::RandomAccessIterator< Assignment >
	The iterator type, which is a random access iterator over the assignment.

Public Member Functions
	Assignment (clingo_assignment_t const *assignment)
	Construct an assignment from the underlying C representation.
auto	size () const -> size_type
	Get the size of the assignment.
auto	at (size_type size) const -> value_type
	Get the literal at the given index in the assignment.
auto	operator[] (size_type size) const -> value_type
	Get the literal at the given index in the assignment.
auto	decision (ProgramId level) const -> SolverLiteral
	Get the decision literal for the given decision level.
auto	decision_level () const -> ProgramId
	Get the current decision level.
auto	has_conflict () const -> bool
	Check if the assignment is conflicting.
auto	contains (SolverLiteral lit) const -> bool
	Check whether the assignment contains the given literal.
auto	is_false (SolverLiteral lit) const -> bool
	Check if the given literal is false.
auto	is_fixed (SolverLiteral lit) const -> bool
	Check if the truth value of the given literal is fixed.
auto	is_free (SolverLiteral lit) const -> bool
	Check if the truth value of the given literal is free.
auto	is_true (SolverLiteral lit) const -> bool
	Check if the given literal is true.
auto	is_total () const -> bool
	Check whether the assignment is total.
auto	level (SolverLiteral lit) const -> ProgramId
	Get the level on which the given literal was assigned.
auto	value (SolverLiteral lit) const -> std::optional< bool >
	Get the truth value of the given literal.
auto	root_level () const -> ProgramId
	Get the root level of the assignment.
auto	trail () const -> Trail
	Get the trail of the assignment.
auto	begin () const -> iterator
	Get an iterator to the beginning of the assignment.
auto	end () const -> iterator
	Get an iterator to the end of the assignment.

Detailed Description

Represents a (partial) assignment of a particular solver.

An assignment assigns truth values to a set of literals. A literal is assigned to either true or false, or is unassigned. Furthermore, each assigned literal is associated with a decision level. There is exactly one decision literal for each decision level greater than zero. Assignments to all other literals on the same level are consequences implied by the current and possibly previous decisions. Assignments on level zero are immediate consequences of the current program. Decision levels are consecutive numbers starting with zero up to and including the current decision level.

Member Function Documentation

at()

auto Clingo::Assignment::at ( size_type  size ) const -> value_type

inline

Get the literal at the given index in the assignment.

Parameters

size	the index of the literal

Returns

the literal at the index

begin()

auto Clingo::Assignment::begin ( ) const -> iterator

inline

Get an iterator to the beginning of the assignment.

Returns

an iterator to the beginning of the assignment

contains()

auto Clingo::Assignment::contains ( SolverLiteral  lit ) const -> bool

inline

Check whether the assignment contains the given literal.

Returns

whether the assignment contains the literal

decision()

auto Clingo::Assignment::decision ( ProgramId  level ) const -> SolverLiteral

inline

Get the decision literal for the given decision level.

Parameters

level

the decision level to get the decision literal for

Returns

the decision literal for the given level

decision_level()

auto Clingo::Assignment::decision_level ( ) const -> ProgramId

inline

Get the current decision level.

Returns

the current decision level

end()

auto Clingo::Assignment::end ( ) const -> iterator

inline

Get an iterator to the end of the assignment.

Returns

an iterator to the end of the assignment

has_conflict()

auto Clingo::Assignment::has_conflict ( ) const -> bool

inline

Check if the assignment is conflicting.

Returns

whether the assignment is conflicting

is_false()

auto Clingo::Assignment::is_false ( SolverLiteral  lit ) const -> bool

inline

Check if the given literal is false.

Parameters

lit	the literal to check

Returns

whether the literal is false

is_fixed()

auto Clingo::Assignment::is_fixed ( SolverLiteral  lit ) const -> bool

inline

Check if the truth value of the given literal is fixed.

Parameters

lit	the literal to check

Returns

whether the literal has a fixed truth value

is_free()

auto Clingo::Assignment::is_free ( SolverLiteral  lit ) const -> bool

inline

Check if the truth value of the given literal is free.

Parameters

lit	the literal to check

Returns

whether the literal is free

is_total()

auto Clingo::Assignment::is_total ( ) const -> bool

inline

Check whether the assignment is total.

An assignment is total if all literals are assigned a truth value,

Returns

whether the assignment is total

is_true()

auto Clingo::Assignment::is_true ( SolverLiteral  lit ) const -> bool

inline

Check if the given literal is true.

Parameters

lit	the literal to check

Returns

whether the literal is true

level()

auto Clingo::Assignment::level ( SolverLiteral  lit ) const -> ProgramId

inline

Get the level on which the given literal was assigned.

Parameters

lit	the literal to get the level for

Returns

the level on which the literal was assigned

operator[]()

auto Clingo::Assignment::operator[] ( size_type  size ) const -> value_type

inline

Get the literal at the given index in the assignment.

Parameters

size	the index of the literal

Returns

the literal at the index

root_level()

auto Clingo::Assignment::root_level ( ) const -> ProgramId

inline

Get the root level of the assignment.

Decisions levels smaller or equal to the root level are not backtracked during solving.

Returns

the root level of the assignment

size()

auto Clingo::Assignment::size ( ) const -> size_type

inline

Get the size of the assignment.

This is the number af all positive problem literals including unassigned literals.

Returns

the size of the assignment

trail()

auto Clingo::Assignment::trail ( ) const -> Trail

inline

Get the trail of the assignment.

Returns

the trail of the assignment

value()

auto Clingo::Assignment::value ( SolverLiteral  lit ) const -> std::optional<bool>

inline

Get the truth value of the given literal.

The optional returned is empty if the literal is unassigned and, otherwise, contains the truth value of the literal.

Parameters

lit	the literal to get the truth value for

Returns

the truth value of the literal

---

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

• clingo/propagate.hh