SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
smtrat::icp::ContractionCandidateManager Class Reference

#include <ContractionCandidateManager.h>

Collaboration diagram for smtrat::icp::ContractionCandidateManager:

Public Member Functions

 ContractionCandidateManager ()
 Constructors. More...
 
 ~ContractionCandidateManager ()
 
ContractionCandidatecreateCandidate (carl::Variable _lhs, const Poly _rhs, const ConstraintT &_constraint, carl::Variable _derivationVar, Contractor< carl::SimpleNewton > &_contractor, bool _usePropagation)
 Constructor & Functions. More...
 
unsigned getId (const ContractionCandidate *const _candidate) const
 Returns the id of the given contraction candidate. More...
 
ContractionCandidategetCandidate (unsigned _id) const
 Returns the contraction candidate for the given id. More...
 
void closure (const ContractionCandidate *const _candidate, std::set< const ContractionCandidate * > &_candidates) const
 Calculates the closure of a certain candidate according to the variables contained. More...
 
const std::vector< ContractionCandidate * > & candidates ()
 

Private Attributes

unsigned mCurrentId
 Member variables. More...
 
std::vector< ContractionCandidate * > mCandidates
 

Detailed Description

Definition at line 16 of file ContractionCandidateManager.h.

Constructor & Destructor Documentation

◆ ContractionCandidateManager()

smtrat::icp::ContractionCandidateManager::ContractionCandidateManager ( )

Constructors.

Definition at line 7 of file ContractionCandidateManager.cpp.

◆ ~ContractionCandidateManager()

smtrat::icp::ContractionCandidateManager::~ContractionCandidateManager ( )
inline

Definition at line 34 of file ContractionCandidateManager.h.

Member Function Documentation

◆ candidates()

const std::vector<ContractionCandidate*>& smtrat::icp::ContractionCandidateManager::candidates ( )
inline

Definition at line 84 of file ContractionCandidateManager.h.

◆ closure()

void smtrat::icp::ContractionCandidateManager::closure ( const ContractionCandidate *const  _candidate,
std::set< const ContractionCandidate * > &  _candidates 
) const

Calculates the closure of a certain candidate according to the variables contained.

Parameters
_candidate
Returns
the set of candidates in the closure of _candidate

Definition at line 37 of file ContractionCandidateManager.cpp.

Here is the call graph for this function:

◆ createCandidate()

ContractionCandidate * smtrat::icp::ContractionCandidateManager::createCandidate ( carl::Variable  _lhs,
const Poly  _rhs,
const ConstraintT _constraint,
carl::Variable  _derivationVar,
Contractor< carl::SimpleNewton > &  _contractor,
bool  _usePropagation 
)

Constructor & Functions.

Creates a new candidate with an unique id.

Parameters
_lhsThe slack/nonlinear variable which represents the constraint
_constraintThe constraint which is to be replaced
_derivationVarThe variable from which the derivative is created when performing contraction
_originThe pointer to the original formula, needed for assertions and removals of subformulas
Returns
a pointer to the created contraction candidate

Definition at line 12 of file ContractionCandidateManager.cpp.

◆ getCandidate()

ContractionCandidate * smtrat::icp::ContractionCandidateManager::getCandidate ( unsigned  _id) const

Returns the contraction candidate for the given id.

Parameters
_id
Returns
the pointer to the contraction candidate

Definition at line 28 of file ContractionCandidateManager.cpp.

◆ getId()

unsigned smtrat::icp::ContractionCandidateManager::getId ( const ContractionCandidate *const  _candidate) const

Returns the id of the given contraction candidate.

Parameters
_candidate
Returns
id of the candidate

Field Documentation

◆ mCandidates

std::vector<ContractionCandidate*> smtrat::icp::ContractionCandidateManager::mCandidates
private

Definition at line 25 of file ContractionCandidateManager.h.

◆ mCurrentId

unsigned smtrat::icp::ContractionCandidateManager::mCurrentId
private

Member variables.

Definition at line 24 of file ContractionCandidateManager.h.


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