#include <CADConstraints.h>

Inheritance diagram for smtrat::cad::CADConstraints< BT >:

Collaboration diagram for smtrat::cad::CADConstraints< BT >:

[legend]

Data Structures
struct	ConstraintComparator

Public Types
using	Callback = std::function< void(const UPoly &, std::size_t, bool)>

using	VariableBounds = vb::VariableBounds< ConstraintT >

Public Member Functions
	CADConstraints (const Callback &onAdd, const Callback &onAddEq, const Callback &onRemove)

	CADConstraints (const CADConstraints &)=delete

void	reset (const std::vector< carl::Variable > &vars)

const std::vector< carl::Variable > &	vars () const

std::size_t	size () const

bool	valid (std::size_t id) const

const auto &	indexed () const

const auto &	ordered () const

const auto &	bounds () const

const auto &	unsatByBounds () const

std::size_t	add (const ConstraintT &c)

carl::Bitset	remove (const ConstraintT &c)
	Removes a constraint. More...

const ConstraintT &	operator[] (std::size_t id) const

std::size_t	level (std::size_t id) const

bool	checkForTrivialConflict (std::vector< FormulaSetT > &mis) const

void	exportAsDot (std::ostream &out) const

Protected Types
using	ConstraintMap = std::map< ConstraintT, std::size_t, ConstraintComparator >

using	ConstraintIts = std::vector< typename ConstraintMap::iterator >

Protected Member Functions
template<typename CB , typename... Args>
void	callCallback (const CB &cb, const ConstraintT &c, Args... args) const

Protected Attributes
std::vector< carl::Variable >	mVariables

Callback	mAddCallback

Callback	mAddEqCallback

Callback	mRemoveCallback

ConstraintMap	mActiveConstraintMap

ConstraintMap	mConstraintMap

std::vector< typename ConstraintMap::iterator >	mConstraintIts

std::vector< std::size_t >	mConstraintLevels

carl::IDPool	mIDPool

VariableBounds	mBounds

carl::Bitset	mSatByBounds
	List of constraints that are satisfied by bounds. More...

carl::Bitset	mUnsatByBounds
	List of constraints that are infeasible due to bounds. More...

Friends
template<Backtracking B>
std::ostream &	operator<< (std::ostream &os, const CADConstraints< B > &cc)

Detailed Description

template<Backtracking BT>
class smtrat::cad::CADConstraints< BT >

Definition at line 19 of file CADConstraints.h.

Member Typedef Documentation

◆ Callback

template<Backtracking BT>

using smtrat::cad::CADConstraints< BT >::Callback = std::function<void(const UPoly&, std::size_t, bool)>

Definition at line 21 of file CADConstraints.h.

◆ ConstraintIts

template<Backtracking BT>

using smtrat::cad::CADConstraints< BT >::ConstraintIts = std::vector<typename ConstraintMap::iterator>

protected

Definition at line 38 of file CADConstraints.h.

◆ ConstraintMap

template<Backtracking BT>

using smtrat::cad::CADConstraints< BT >::ConstraintMap = std::map<ConstraintT, std::size_t, ConstraintComparator>

protected

Definition at line 37 of file CADConstraints.h.

◆ VariableBounds

template<Backtracking BT>

using smtrat::cad::CADConstraints< BT >::VariableBounds = vb::VariableBounds<ConstraintT>

Definition at line 22 of file CADConstraints.h.

Constructor & Destructor Documentation

◆ CADConstraints() [1/2]

template<Backtracking BT>

smtrat::cad::CADConstraints< BT >::CADConstraints	(	const Callback &	onAdd,
		const Callback &	onAddEq,
		const Callback &	onRemove
	)

inline

Definition at line 60 of file CADConstraints.h.

◆ CADConstraints() [2/2]

template<Backtracking BT>

smtrat::cad::CADConstraints< BT >::CADConstraints ( const CADConstraints< BT > & )

delete

Member Function Documentation

◆ add()

template<Backtracking BT>

std::size_t smtrat::cad::CADConstraints< BT >::add ( const ConstraintT & c )

inline

Definition at line 94 of file CADConstraints.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ bounds()

template<Backtracking BT>

const auto& smtrat::cad::CADConstraints< BT >::bounds ( ) const

inline

Definition at line 88 of file CADConstraints.h.

Here is the caller graph for this function:

◆ callCallback()

template<Backtracking BT>

template<typename CB , typename... Args>

void smtrat::cad::CADConstraints< BT >::callCallback	(	const CB &	cb,
		const ConstraintT &	c,
		Args...	args
	)		const

inlineprotected

Definition at line 56 of file CADConstraints.h.

Here is the caller graph for this function:

◆ checkForTrivialConflict()

template<Backtracking BT>

bool smtrat::cad::CADConstraints< BT >::checkForTrivialConflict ( std::vector< FormulaSetT > & mis ) const

inline

Definition at line 214 of file CADConstraints.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ exportAsDot()

template<Backtracking BT>

void smtrat::cad::CADConstraints< BT >::exportAsDot ( std::ostream & out ) const

inline

Definition at line 242 of file CADConstraints.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ indexed()

template<Backtracking BT>

const auto& smtrat::cad::CADConstraints< BT >::indexed ( ) const

inline

Definition at line 82 of file CADConstraints.h.

Here is the caller graph for this function:

◆ level()

template<Backtracking BT>

std::size_t smtrat::cad::CADConstraints< BT >::level ( std::size_t id ) const

inline

Definition at line 211 of file CADConstraints.h.

Here is the caller graph for this function:

◆ operator[]()

template<Backtracking BT>

const ConstraintT& smtrat::cad::CADConstraints< BT >::operator[] ( std::size_t id ) const

inline

Definition at line 206 of file CADConstraints.h.

◆ ordered()

template<Backtracking BT>

const auto& smtrat::cad::CADConstraints< BT >::ordered ( ) const

inline

Definition at line 85 of file CADConstraints.h.

Here is the caller graph for this function:

◆ remove()

template<Backtracking BT>

carl::Bitset smtrat::cad::CADConstraints< BT >::remove ( const ConstraintT & c )

inline

Removes a constraint.

Returns the set of constraint ids that have (possibly) been reassigned and should be cleared from the sample evaluations.

Definition at line 158 of file CADConstraints.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ reset()

template<Backtracking BT>

void smtrat::cad::CADConstraints< BT >::reset ( const std::vector< carl::Variable > & vars )

inline

Definition at line 62 of file CADConstraints.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ size()

template<Backtracking BT>

std::size_t smtrat::cad::CADConstraints< BT >::size ( ) const

inline

Definition at line 76 of file CADConstraints.h.

Here is the caller graph for this function:

◆ unsatByBounds()

template<Backtracking BT>

const auto& smtrat::cad::CADConstraints< BT >::unsatByBounds ( ) const

inline

Definition at line 91 of file CADConstraints.h.

◆ valid()

template<Backtracking BT>

bool smtrat::cad::CADConstraints< BT >::valid ( std::size_t id ) const

inline

Definition at line 79 of file CADConstraints.h.

Here is the caller graph for this function:

◆ vars()

template<Backtracking BT>

const std::vector<carl::Variable>& smtrat::cad::CADConstraints< BT >::vars ( ) const

inline

Definition at line 73 of file CADConstraints.h.

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ operator<<

template<Backtracking BT>

template<Backtracking B>

std::ostream& operator<<	(	std::ostream &	os,
		const CADConstraints< B > &	cc
	)

friend

Field Documentation

◆ mActiveConstraintMap

template<Backtracking BT>

ConstraintMap smtrat::cad::CADConstraints< BT >::mActiveConstraintMap

protected

Definition at line 44 of file CADConstraints.h.

◆ mAddCallback

template<Backtracking BT>

Callback smtrat::cad::CADConstraints< BT >::mAddCallback

protected

Definition at line 41 of file CADConstraints.h.

◆ mAddEqCallback

template<Backtracking BT>

Callback smtrat::cad::CADConstraints< BT >::mAddEqCallback

protected

Definition at line 42 of file CADConstraints.h.

◆ mBounds

template<Backtracking BT>

VariableBounds smtrat::cad::CADConstraints< BT >::mBounds

protected

Definition at line 49 of file CADConstraints.h.

◆ mConstraintIts

template<Backtracking BT>

std::vector<typename ConstraintMap::iterator> smtrat::cad::CADConstraints< BT >::mConstraintIts

protected

Definition at line 46 of file CADConstraints.h.

◆ mConstraintLevels

template<Backtracking BT>

std::vector<std::size_t> smtrat::cad::CADConstraints< BT >::mConstraintLevels

protected

Definition at line 47 of file CADConstraints.h.

◆ mConstraintMap

template<Backtracking BT>

ConstraintMap smtrat::cad::CADConstraints< BT >::mConstraintMap

protected

Definition at line 45 of file CADConstraints.h.

◆ mIDPool

template<Backtracking BT>

carl::IDPool smtrat::cad::CADConstraints< BT >::mIDPool

protected

Definition at line 48 of file CADConstraints.h.

◆ mRemoveCallback

template<Backtracking BT>

Callback smtrat::cad::CADConstraints< BT >::mRemoveCallback

protected

Definition at line 43 of file CADConstraints.h.

◆ mSatByBounds

template<Backtracking BT>

carl::Bitset smtrat::cad::CADConstraints< BT >::mSatByBounds

protected

List of constraints that are satisfied by bounds.

Definition at line 51 of file CADConstraints.h.

◆ mUnsatByBounds

template<Backtracking BT>

carl::Bitset smtrat::cad::CADConstraints< BT >::mUnsatByBounds

protected

List of constraints that are infeasible due to bounds.

Definition at line 53 of file CADConstraints.h.

◆ mVariables

template<Backtracking BT>

std::vector<carl::Variable> smtrat::cad::CADConstraints< BT >::mVariables

protected

Definition at line 40 of file CADConstraints.h.

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

smtrat-cad/utils/CADConstraints.h

Data Structures

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Friends

Detailed Description

template<Backtracking BT> class smtrat::cad::CADConstraints< BT >

Member Typedef Documentation

◆ Callback

◆ ConstraintIts

◆ ConstraintMap

◆ VariableBounds

Constructor & Destructor Documentation

◆ CADConstraints() [1/2]

◆ CADConstraints() [2/2]

Member Function Documentation

◆ add()

◆ bounds()

◆ callCallback()

◆ checkForTrivialConflict()

◆ exportAsDot()

◆ indexed()

◆ level()

◆ operator[]()

◆ ordered()

◆ remove()

◆ reset()

◆ size()

◆ unsatByBounds()

◆ valid()

◆ vars()

Friends And Related Function Documentation

◆ operator<<

Field Documentation

◆ mActiveConstraintMap

◆ mAddCallback

◆ mAddEqCallback

◆ mBounds

◆ mConstraintIts

◆ mConstraintLevels

◆ mConstraintMap

◆ mIDPool

◆ mRemoveCallback

◆ mSatByBounds

◆ mUnsatByBounds

◆ mVariables

template<Backtracking BT>
class smtrat::cad::CADConstraints< BT >