SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Private Attributes | Static Private Attributes
smtrat::icp::ContractionCandidate Class Reference

#include <ContractionCandidate.h>

Collaboration diagram for smtrat::icp::ContractionCandidate:
Collaboration graph
[legend]

Public Member Functions

 ContractionCandidate (const ContractionCandidate &_original)=delete
 Constructors: More...
 
 ContractionCandidate ()=delete
 
 ContractionCandidate (carl::Variable _lhs, const Poly _rhs, const ConstraintT &_constraint, carl::Variable _derivationVar, Contractor< carl::SimpleNewton > &_contractor, const FormulaT &_origin, unsigned _id, bool _usePropagation)
 
 ContractionCandidate (carl::Variable _lhs, const Poly _rhs, const ConstraintT &_constraint, carl::Variable _derivationVar, Contractor< carl::SimpleNewton > &_contractor, unsigned _id, bool _usePropagation)
 Constructor only for nonlinear candidates. More...
 
 ~ContractionCandidate ()
 Destructor: More...
 
const Poly & rhs () const
 Functions: More...
 
const ConstraintT & constraint () const
 
Contractor< carl::SimpleNewton > & contractor () const
 
bool contract (EvalDoubleIntervalMap &_intervals, DoubleInterval &_resA, DoubleInterval &_resB)
 
carl::Variable::Arg derivationVar () const
 
const Poly & derivative () const
 
carl::Variable::Arg lhs () const
 
const FormulaSetT & origin () const
 
FormulaSetT & rOrigin ()
 
void addOrigin (const FormulaT &_origin)
 
void removeOrigin (const FormulaT &_origin)
 
bool hasOrigin (const FormulaT &_origin) const
 
void setLinear ()
 
void setNonlinear ()
 
bool is_linear () const
 
unsigned reusagesAfterTargetDiameterReached () const
 
unsigned incrementReusagesAfterTargetDiameterReached ()
 
void resetReusagesAfterTargetDiameterReached ()
 
void addICPVariable (IcpVariable *_icpVar)
 
double calcRWA ()
 
double RWA () const
 
double lastRWA () const
 
void updateLastRWA ()
 
double lastPayoff () const
 
unsigned id () const
 
void setDerivationVar (carl::Variable _var)
 
void setLhs (carl::Variable _lhs)
 
void setPayoff (double _weight)
 
void calcDerivative () throw ()
 
size_t activity ()
 
bool isActive () const
 
bool isDerived () const
 
void resetWeights ()
 
void print (std::ostream &_out=std::cout) const
 
bool operator< (ContractionCandidate const &rhs) const
 
bool operator== (ContractionCandidate const &rhs) const
 

Private Attributes

friend ContractionCandidateManager
 
const Poly mRhs
 Members: More...
 
ConstraintT mConstraint
 
Contractor< carl::SimpleNewton > & mContractor
 
carl::Variable mLhs
 
carl::Variable mDerivationVar
 
Poly mDerivative
 
FormulaSetT mOrigin
 
unsigned mId
 
bool mIsLinear
 
bool mDerived
 
bool mUsePropagation
 
std::set< IcpVariable * > mIcpVariables
 
unsigned mReusagesAfterTargetDiameterReached
 
double mRWA
 
double mLastRWA
 
double mLastPayoff
 

Static Private Attributes

static const size_t mK = 10
 
static constexpr double mAlpha = 0.9
 

Detailed Description

Definition at line 26 of file ContractionCandidate.h.

Constructor & Destructor Documentation

◆ ContractionCandidate() [1/4]

smtrat::icp::ContractionCandidate::ContractionCandidate ( const ContractionCandidate &  _original)
delete

Constructors:

◆ ContractionCandidate() [2/4]

smtrat::icp::ContractionCandidate::ContractionCandidate ( )
delete

◆ ContractionCandidate() [3/4]

smtrat::icp::ContractionCandidate::ContractionCandidate ( carl::Variable  _lhs,
const Poly  _rhs,
const ConstraintT &  _constraint,
carl::Variable  _derivationVar,
Contractor< carl::SimpleNewton > &  _contractor,
const FormulaT &  _origin,
unsigned  _id,
bool  _usePropagation 
)
inline

Definition at line 71 of file ContractionCandidate.h.

◆ ContractionCandidate() [4/4]

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

Constructor only for nonlinear candidates.

Parameters
_constraint
_derivationVar

Definition at line 96 of file ContractionCandidate.h.

◆ ~ContractionCandidate()

smtrat::icp::ContractionCandidate::~ContractionCandidate ( )
inline

Destructor:

Definition at line 118 of file ContractionCandidate.h.

Member Function Documentation

◆ activity()

size_t smtrat::icp::ContractionCandidate::activity ( )
inline

Definition at line 269 of file ContractionCandidate.h.

◆ addICPVariable()

void smtrat::icp::ContractionCandidate::addICPVariable ( IcpVariable *  _icpVar)
inline

Definition at line 209 of file ContractionCandidate.h.

◆ addOrigin()

void smtrat::icp::ContractionCandidate::addOrigin ( const FormulaT &  _origin)

Definition at line 12 of file ContractionCandidate.cpp.

◆ calcDerivative()

void smtrat::icp::ContractionCandidate::calcDerivative ( )
throw (
)
inline

Definition at line 260 of file ContractionCandidate.h.

◆ calcRWA()

double smtrat::icp::ContractionCandidate::calcRWA ( )
inline

Definition at line 214 of file ContractionCandidate.h.

◆ constraint()

const ConstraintT& smtrat::icp::ContractionCandidate::constraint ( ) const
inline

Definition at line 130 of file ContractionCandidate.h.

Here is the caller graph for this function:

◆ contract()

bool smtrat::icp::ContractionCandidate::contract ( EvalDoubleIntervalMap &  _intervals,
DoubleInterval &  _resA,
DoubleInterval &  _resB 
)
inline

Definition at line 140 of file ContractionCandidate.h.

◆ contractor()

Contractor<carl::SimpleNewton>& smtrat::icp::ContractionCandidate::contractor ( ) const
inline

Definition at line 135 of file ContractionCandidate.h.

◆ derivationVar()

carl::Variable::Arg smtrat::icp::ContractionCandidate::derivationVar ( ) const
inline

Definition at line 145 of file ContractionCandidate.h.

Here is the caller graph for this function:

◆ derivative()

const Poly& smtrat::icp::ContractionCandidate::derivative ( ) const
inline

Definition at line 150 of file ContractionCandidate.h.

◆ hasOrigin()

bool smtrat::icp::ContractionCandidate::hasOrigin ( const FormulaT &  _origin) const
inline

Definition at line 174 of file ContractionCandidate.h.

◆ id()

unsigned smtrat::icp::ContractionCandidate::id ( ) const
inline

Definition at line 240 of file ContractionCandidate.h.

Here is the caller graph for this function:

◆ incrementReusagesAfterTargetDiameterReached()

unsigned smtrat::icp::ContractionCandidate::incrementReusagesAfterTargetDiameterReached ( )
inline

Definition at line 199 of file ContractionCandidate.h.

Here is the caller graph for this function:

◆ is_linear()

bool smtrat::icp::ContractionCandidate::is_linear ( ) const
inline

Definition at line 189 of file ContractionCandidate.h.

◆ isActive()

bool smtrat::icp::ContractionCandidate::isActive ( ) const
inline

Definition at line 274 of file ContractionCandidate.h.

◆ isDerived()

bool smtrat::icp::ContractionCandidate::isDerived ( ) const
inline

Definition at line 279 of file ContractionCandidate.h.

◆ lastPayoff()

double smtrat::icp::ContractionCandidate::lastPayoff ( ) const
inline

Definition at line 235 of file ContractionCandidate.h.

◆ lastRWA()

double smtrat::icp::ContractionCandidate::lastRWA ( ) const
inline

Definition at line 225 of file ContractionCandidate.h.

◆ lhs()

carl::Variable::Arg smtrat::icp::ContractionCandidate::lhs ( ) const
inline

Definition at line 155 of file ContractionCandidate.h.

◆ operator<()

bool smtrat::icp::ContractionCandidate::operator< ( ContractionCandidate const &  rhs) const
inline

Definition at line 310 of file ContractionCandidate.h.

Here is the call graph for this function:

◆ operator==()

bool smtrat::icp::ContractionCandidate::operator== ( ContractionCandidate const &  rhs) const
inline

Definition at line 315 of file ContractionCandidate.h.

Here is the call graph for this function:

◆ origin()

const FormulaSetT& smtrat::icp::ContractionCandidate::origin ( ) const
inline

Definition at line 160 of file ContractionCandidate.h.

Here is the caller graph for this function:

◆ print()

void smtrat::icp::ContractionCandidate::print ( std::ostream &  _out = std::cout) const
inline

Definition at line 290 of file ContractionCandidate.h.

Here is the caller graph for this function:

◆ removeOrigin()

void smtrat::icp::ContractionCandidate::removeOrigin ( const FormulaT &  _origin)

Definition at line 23 of file ContractionCandidate.cpp.

◆ resetReusagesAfterTargetDiameterReached()

void smtrat::icp::ContractionCandidate::resetReusagesAfterTargetDiameterReached ( )
inline

Definition at line 204 of file ContractionCandidate.h.

◆ resetWeights()

void smtrat::icp::ContractionCandidate::resetWeights ( )
inline

Definition at line 284 of file ContractionCandidate.h.

◆ reusagesAfterTargetDiameterReached()

unsigned smtrat::icp::ContractionCandidate::reusagesAfterTargetDiameterReached ( ) const
inline

Definition at line 194 of file ContractionCandidate.h.

Here is the caller graph for this function:

◆ rhs()

const Poly& smtrat::icp::ContractionCandidate::rhs ( ) const
inline

Functions:

Definition at line 125 of file ContractionCandidate.h.

Here is the caller graph for this function:

◆ rOrigin()

FormulaSetT& smtrat::icp::ContractionCandidate::rOrigin ( )
inline

Definition at line 165 of file ContractionCandidate.h.

Here is the caller graph for this function:

◆ RWA()

double smtrat::icp::ContractionCandidate::RWA ( ) const
inline

Definition at line 220 of file ContractionCandidate.h.

◆ setDerivationVar()

void smtrat::icp::ContractionCandidate::setDerivationVar ( carl::Variable  _var)
inline

Definition at line 245 of file ContractionCandidate.h.

◆ setLhs()

void smtrat::icp::ContractionCandidate::setLhs ( carl::Variable  _lhs)
inline

Definition at line 250 of file ContractionCandidate.h.

◆ setLinear()

void smtrat::icp::ContractionCandidate::setLinear ( )
inline

Definition at line 179 of file ContractionCandidate.h.

◆ setNonlinear()

void smtrat::icp::ContractionCandidate::setNonlinear ( )
inline

Definition at line 184 of file ContractionCandidate.h.

◆ setPayoff()

void smtrat::icp::ContractionCandidate::setPayoff ( double  _weight)
inline

Definition at line 255 of file ContractionCandidate.h.

◆ updateLastRWA()

void smtrat::icp::ContractionCandidate::updateLastRWA ( )
inline

Definition at line 230 of file ContractionCandidate.h.

Field Documentation

◆ ContractionCandidateManager

friend smtrat::icp::ContractionCandidate::ContractionCandidateManager
private

Definition at line 28 of file ContractionCandidate.h.

◆ mAlpha

constexpr double smtrat::icp::ContractionCandidate::mAlpha = 0.9
staticconstexprprivate

Definition at line 56 of file ContractionCandidate.h.

◆ mConstraint

ConstraintT smtrat::icp::ContractionCandidate::mConstraint
private

Definition at line 36 of file ContractionCandidate.h.

◆ mContractor

Contractor<carl::SimpleNewton>& smtrat::icp::ContractionCandidate::mContractor
private

Definition at line 37 of file ContractionCandidate.h.

◆ mDerivationVar

carl::Variable smtrat::icp::ContractionCandidate::mDerivationVar
private

Definition at line 40 of file ContractionCandidate.h.

◆ mDerivative

Poly smtrat::icp::ContractionCandidate::mDerivative
private

Definition at line 41 of file ContractionCandidate.h.

◆ mDerived

bool smtrat::icp::ContractionCandidate::mDerived
private

Definition at line 45 of file ContractionCandidate.h.

◆ mIcpVariables

std::set<IcpVariable*> smtrat::icp::ContractionCandidate::mIcpVariables
private

Definition at line 47 of file ContractionCandidate.h.

◆ mId

unsigned smtrat::icp::ContractionCandidate::mId
private

Definition at line 43 of file ContractionCandidate.h.

◆ mIsLinear

bool smtrat::icp::ContractionCandidate::mIsLinear
private

Definition at line 44 of file ContractionCandidate.h.

◆ mK

const size_t smtrat::icp::ContractionCandidate::mK = 10
staticprivate

Definition at line 52 of file ContractionCandidate.h.

◆ mLastPayoff

double smtrat::icp::ContractionCandidate::mLastPayoff
private

Definition at line 60 of file ContractionCandidate.h.

◆ mLastRWA

double smtrat::icp::ContractionCandidate::mLastRWA
private

Definition at line 59 of file ContractionCandidate.h.

◆ mLhs

carl::Variable smtrat::icp::ContractionCandidate::mLhs
private

Definition at line 39 of file ContractionCandidate.h.

◆ mOrigin

FormulaSetT smtrat::icp::ContractionCandidate::mOrigin
private

Definition at line 42 of file ContractionCandidate.h.

◆ mReusagesAfterTargetDiameterReached

unsigned smtrat::icp::ContractionCandidate::mReusagesAfterTargetDiameterReached
private

Definition at line 48 of file ContractionCandidate.h.

◆ mRhs

const Poly smtrat::icp::ContractionCandidate::mRhs
private

Members:

Definition at line 35 of file ContractionCandidate.h.

◆ mRWA

double smtrat::icp::ContractionCandidate::mRWA
private

Definition at line 58 of file ContractionCandidate.h.

◆ mUsePropagation

bool smtrat::icp::ContractionCandidate::mUsePropagation
private

Definition at line 46 of file ContractionCandidate.h.

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