smtrat::cad::preprocessor::AssignmentCollector Class Reference

#include <CADPreprocessor.h>

Collaboration diagram for smtrat::cad::preprocessor::AssignmentCollector:

Public Types
using	CollectionResult = std::variant< bool, ConstraintT >
	Result of an assignment collection. More...

Public Member Functions
	AssignmentCollector (Model &model)
const auto &	reasons () const
auto &	reasons ()
const auto &	constraints () const
auto &	constraints ()
CollectionResult	collect (std::map< ConstraintT, ConstraintT > &constraints)

Private Member Functions
bool	extractValueAssignments (std::map< ConstraintT, ConstraintT > &constraints)
bool	extractParametricAssignments (std::map< ConstraintT, ConstraintT > &constraints)
bool	extractAssignments (std::map< ConstraintT, ConstraintT > &constraints)
CollectionResult	simplify (std::map< ConstraintT, ConstraintT > &constraints)

Private Attributes
Model &	mModel
std::map< carl::Variable, ConstraintT >	mReasons
	Reasons for the assignment of variables. More...
std::map< ConstraintT, carl::Variable >	mConstraints

Detailed Description

Definition at line 52 of file CADPreprocessor.h.

Member Typedef Documentation

CollectionResult

using smtrat::cad::preprocessor::AssignmentCollector::CollectionResult = std::variant<bool,ConstraintT>

Result of an assignment collection.

true: new assignments were found false: no new assignments were found constraint: found direct conflict

Definition at line 58 of file CADPreprocessor.h.

Constructor & Destructor Documentation

AssignmentCollector()

smtrat::cad::preprocessor::AssignmentCollector::AssignmentCollector ( Model &  model )

inline

Definition at line 71 of file CADPreprocessor.h.

Member Function Documentation

collect()

AssignmentCollector::CollectionResult smtrat::cad::preprocessor::AssignmentCollector::collect

(

std::map< ConstraintT, ConstraintT > &

constraints

)

Definition at line 140 of file CADPreprocessor.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

constraints() [1/2]

auto& smtrat::cad::preprocessor::AssignmentCollector::constraints ( )

inline

Definition at line 82 of file CADPreprocessor.h.

constraints() [2/2]

const auto& smtrat::cad::preprocessor::AssignmentCollector::constraints ( ) const

inline

Definition at line 79 of file CADPreprocessor.h.

Here is the caller graph for this function:

extractAssignments()

bool smtrat::cad::preprocessor::AssignmentCollector::extractAssignments ( std::map< ConstraintT, ConstraintT > &  constraints )

private

Definition at line 119 of file CADPreprocessor.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

extractParametricAssignments()

bool smtrat::cad::preprocessor::AssignmentCollector::extractParametricAssignments ( std::map< ConstraintT, ConstraintT > &  constraints )

private

Definition at line 99 of file CADPreprocessor.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

extractValueAssignments()

bool smtrat::cad::preprocessor::AssignmentCollector::extractValueAssignments ( std::map< ConstraintT, ConstraintT > &  constraints )

private

Definition at line 81 of file CADPreprocessor.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

reasons() [1/2]

auto& smtrat::cad::preprocessor::AssignmentCollector::reasons ( )

inline

Definition at line 76 of file CADPreprocessor.h.

reasons() [2/2]

const auto& smtrat::cad::preprocessor::AssignmentCollector::reasons ( ) const

inline

Definition at line 73 of file CADPreprocessor.h.

Here is the caller graph for this function:

simplify()

AssignmentCollector::CollectionResult smtrat::cad::preprocessor::AssignmentCollector::simplify ( std::map< ConstraintT, ConstraintT > &  constraints )

private

Definition at line 124 of file CADPreprocessor.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

Field Documentation

mConstraints

std::map<ConstraintT, carl::Variable> smtrat::cad::preprocessor::AssignmentCollector::mConstraints

private

Definition at line 63 of file CADPreprocessor.h.

mModel

Model& smtrat::cad::preprocessor::AssignmentCollector::mModel

private

Definition at line 60 of file CADPreprocessor.h.

mReasons

std::map<carl::Variable, ConstraintT> smtrat::cad::preprocessor::AssignmentCollector::mReasons

private

Reasons for the assignment of variables.

Definition at line 62 of file CADPreprocessor.h.

---

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

• smtrat-cad/utils/CADPreprocessor.h
• smtrat-cad/utils/CADPreprocessor.cpp