dlinear::BoundIterator Class Reference

BoundIterator class. More...

#include <BoundIterator.h>

Public Member Functions
	BoundIterator ()
	Construct an empty iterator.
	BoundIterator (internal_iterator begin_bounds_it, internal_iterator end_bounds_it)
	Construct an iterator from a pair of iterators, begin_bounds_it and end_bounds_it.
	BoundIterator (std::pair< internal_iterator, internal_iterator > bounds)
	Construct an iterator from a pair of iterators, bounds.
	BoundIterator (internal_iterator begin_bounds_it, internal_iterator end_bounds_it, internal_iterator begin_nq_bounds_it, internal_iterator end_nq_bounds_it)
	Construct an iterator from a pair of iterators to the standard bounds, begin_bounds_it and end_bounds_it, and a pair of iterators to the non-equal bounds, begin_nq_bounds_it and end_nq_bounds_it.
	BoundIterator (std::pair< internal_iterator, internal_iterator > bounds, std::pair< internal_iterator, internal_iterator > nq_bounds)
	Construct an iterator from a pair of iterators to the standard bounds, bounds, and a pair of iterators to the non-equal bounds, nq_bounds.
std::pair< internal_iterator, internal_iterator >	bounds () const
	Return the pair of iterators to the bounds.
std::pair< internal_iterator, internal_iterator >	nq_bounds () const
	Return the pair of iterators to the non-equal bounds.
std::size_t	bounds_size () const
	Number of bounds included between the begin and end iterators.
std::size_t	nq_bounds_size () const
	Number of non-equal bounds included between the begin and end iterators.
bool	bounds_empty () const
	Check if the iterator does not point to any bound.
bool	nq_bounds_empty () const
	Check if the iterator does not point to any non-equal bound.
bool	empty () const
	Check if the iterator does not point to any bound.
std::size_t	size () const
	Number of bounds of any kind included between the begin and end iterators.
internal_iterator	begin () const
	Get read-only access to the begin iterator of the BoundIterator.
internal_iterator	end () const
	Get read-only access to the end iterator of the BoundIterator.
LiteralSet	explanation () const
	Produce and explanation formed by all the theory literals present in the violation.
void	explanation (LiteralSet &explanation) const
	Produce and explanation formed by all the theory literals present in the violation.
std::set< LiteralSet >	explanations (const std::optional< Literal > &lit={}) const
	Produce a set of explanations.
void	explanations (std::set< LiteralSet > &explanations, const std::optional< Literal > &lit={}) const
	Produce a set of explanations.

Private Attributes
const internal_iterator	begin_bounds_it_
	Begin iterator to the first bound.
internal_iterator	bounds_it_
	Iterator to the current bound.
const internal_iterator	end_bounds_it_
	End iterator of the bounds.
const internal_iterator	begin_nq_bounds_it_
	Begin iterator to the first non-equal bound.
internal_iterator	nq_bounds_it_
	Iterator to the current non-equal bound.
const internal_iterator	end_nq_bounds_it_
	End iterator of the non-equal bounds.

Static Private Attributes
static const vector_type	default_empty_vector_ {}
	Default empty vector. Used for default construction.

Detailed Description

BoundIterator class.

It is used to iterate over the bounds of a theory solver without copying each BoundVector::Bound. Can be returned as a result of a bound violation or to iterate over the active bounds. It allows to iterate over the two types of bounds: standard and non-equal as if they were a single container.

std::vector<Bound> bounds, nq_bounds;
bounds.push_back(Bound{0, BoundType::U, ...});
bounds.push_back(Bound{1, BoundType::L, ...});
bounds.push_back(Bound{2, BoundType::B, ...});
nq_bounds.push_back(Bound{3, BoundType::D, ...});
BoundIterator<std::vector<Bound>> it{bounds.begin(), bounds.end(), nq_bounds.begin(), nq_bounds.end()};
for (; it; ++it) {
 std::cout << *it << std::endl;
}
// Output:
// Bound{0, BoundType::U, ...}, Bound{1, BoundType::L, ...}, Bound{2, BoundType::B, ...}, Bound{3, BoundType::D, ...}

Definition at line 43 of file BoundIterator.h.

Constructor & Destructor Documentation

BoundIterator() [1/4]

dlinear::BoundIterator::BoundIterator	(	BoundIterator::internal_iterator	begin_bounds_it,
		BoundIterator::internal_iterator	end_bounds_it )

Construct an iterator from a pair of iterators, begin_bounds_it and end_bounds_it.

Note

Bounds will be normalized, i.e., all ending bounds will be greater or equal to the being bounds.

Parameters

begin_bounds_it	begin iterator to the first bound
end_bounds_it	end iterator of the bounds

Definition at line 58 of file BoundIterator.cpp.

BoundIterator() [2/4]

dlinear::BoundIterator::BoundIterator ( std::pair< internal_iterator, internal_iterator > bounds )

explicit

Construct an iterator from a pair of iterators, bounds.

Note

Bounds will be normalized, i.e., all ending bounds will be greater or equal to the being bounds.

Parameters

bounds

pair of iterators to the bounds, begin and end

Definition at line 70 of file BoundIterator.cpp.

BoundIterator() [3/4]

dlinear::BoundIterator::BoundIterator	(	BoundIterator::internal_iterator	begin_bounds_it,
		BoundIterator::internal_iterator	end_bounds_it,
		BoundIterator::internal_iterator	begin_nq_bounds_it,
		BoundIterator::internal_iterator	end_nq_bounds_it )

Construct an iterator from a pair of iterators to the standard bounds, begin_bounds_it and end_bounds_it, and a pair of iterators to the non-equal bounds, begin_nq_bounds_it and end_nq_bounds_it.

Note

Bounds will be normalized, i.e., all ending bounds will be greater or equal to the being bounds.

Parameters

begin_bounds_it	begin iterator to the first bound
end_bounds_it	end iterator of the bounds
begin_nq_bounds_it	begin iterator to the first non-equal bound
end_nq_bounds_it	end iterator of the non-equal bounds

Definition at line 31 of file BoundIterator.cpp.

BoundIterator() [4/4]

dlinear::BoundIterator::BoundIterator	(	std::pair< internal_iterator, internal_iterator >	bounds,
		std::pair< internal_iterator, internal_iterator >	nq_bounds )

Construct an iterator from a pair of iterators to the standard bounds, bounds, and a pair of iterators to the non-equal bounds, nq_bounds.

Note

Bounds will be normalized, i.e., all ending bounds will be greater or equal to the being bounds.

Parameters

bounds	begin and end iterators to the bounds
nq_bounds	begin and end iterators to the non-equal bounds

Definition at line 46 of file BoundIterator.cpp.

Member Function Documentation

begin()

internal_iterator dlinear::BoundIterator::begin ( ) const

inlinenodiscard

Get read-only access to the begin iterator of the BoundIterator.

Returns

begin iterator of the BoundIterator

Definition at line 153 of file BoundIterator.h.

bounds()

std::pair< internal_iterator, internal_iterator > dlinear::BoundIterator::bounds ( ) const

inlinenodiscard

Return the pair of iterators to the bounds.

Returns

begin and end iterators to the bounds

Definition at line 106 of file BoundIterator.h.

bounds_empty()

bool dlinear::BoundIterator::bounds_empty ( ) const

inlinenodiscard

Check if the iterator does not point to any bound.

Note

Equivalent to bounds_size() == 0

Returns

true if the iterator does not point to any bound

false if the iterator points to at least one bound

Definition at line 130 of file BoundIterator.h.

bounds_size()

std::size_t dlinear::BoundIterator::bounds_size ( ) const

inlinenodiscard

Number of bounds included between the begin and end iterators.

Returns

number of bounds

Definition at line 118 of file BoundIterator.h.

empty()

bool dlinear::BoundIterator::empty ( ) const

inlinenodiscard

Check if the iterator does not point to any bound.

Note

Equivalent to bounds_empty() && nq_bounds_empty()

Returns

true if the iterator does not point to any bound

false if the iterator points to at least one bound

Definition at line 144 of file BoundIterator.h.

end()

internal_iterator dlinear::BoundIterator::end ( ) const

inlinenodiscard

Get read-only access to the end iterator of the BoundIterator.

Returns

end iterator of the BoundIterator

Definition at line 155 of file BoundIterator.h.

explanation() [1/2]

LiteralSet dlinear::BoundIterator::explanation ( ) const

nodiscard

Produce and explanation formed by all the theory literals present in the violation.

It puts in a single set all the explanations and literals of all the bounds.

Returns

explanation

Definition at line 114 of file BoundIterator.cpp.

explanation() [2/2]

void dlinear::BoundIterator::explanation

(

LiteralSet &

explanation

)

const

Produce and explanation formed by all the theory literals present in the violation.

It puts in a single set all the explanations and literals of all the bounds.

Parameters

explanation[out]

set to store the explanation

Returns

explanation

Definition at line 119 of file BoundIterator.cpp.

explanations() [1/2]

std::set< LiteralSet > dlinear::BoundIterator::explanations ( const std::optional< Literal > & lit = {} ) const

nodiscard

Produce a set of explanations.

Each of the explanations is produced from a single bound of the violation, putting together its explanation and literal. If lit is present, it will be added to every explanation.

Parameters

lit	if specified, it is added to all explanations

Returns

set of explanations

Definition at line 131 of file BoundIterator.cpp.

explanations() [2/2]

void dlinear::BoundIterator::explanations	(	std::set< LiteralSet > &	explanations,
		const std::optional< Literal > &	lit = {} ) const

Produce a set of explanations.

Each of the explanations is produced from a single bound of the violation, putting together its explanation and literal. If lit is present, it will be added to every explanation.

Parameters

explanations[out]	set to store the explanations
lit	if specified, it is added to all explanations

Returns

set of explanations

Definition at line 136 of file BoundIterator.cpp.

nq_bounds()

std::pair< internal_iterator, internal_iterator > dlinear::BoundIterator::nq_bounds ( ) const

inlinenodiscard

Return the pair of iterators to the non-equal bounds.

Returns

begin and end iterators to the non-equal bounds

Definition at line 111 of file BoundIterator.h.

nq_bounds_empty()

bool dlinear::BoundIterator::nq_bounds_empty ( ) const

inlinenodiscard

Check if the iterator does not point to any non-equal bound.

Note

Equivalent to nq_bounds_size() == 0

Returns

true if the iterator does not point to any non-equal bound

false if the iterator points to at least one non-equal bound

Definition at line 137 of file BoundIterator.h.

nq_bounds_size()

std::size_t dlinear::BoundIterator::nq_bounds_size ( ) const

inlinenodiscard

Number of non-equal bounds included between the begin and end iterators.

Returns

number of non-equal bounds

Definition at line 123 of file BoundIterator.h.

size()

std::size_t dlinear::BoundIterator::size ( ) const

inlinenodiscard

Number of bounds of any kind included between the begin and end iterators.

Note

Equivalent to bounds_size() + nq_bounds_size()

Returns

number of bounds of any kind

Definition at line 150 of file BoundIterator.h.

---

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

• dlinear/solver/BoundIterator.h
• dlinear/solver/BoundIterator.cpp