#include <HistoryNode.h>

Collaboration diagram for smtrat::icp::HistoryNode:

[legend]

Public Member Functions
	HistoryNode ()
	Methods. More...

	HistoryNode (const EvalDoubleIntervalMap &_intervals)

	~HistoryNode ()

const EvalDoubleIntervalMap &	intervals () const
	Getters and Setters. More...

EvalDoubleIntervalMap &	rIntervals ()

DoubleInterval &	getInterval (carl::Variable::Arg _variable)

void	setIntervals (const EvalDoubleIntervalMap &_map)

bool	addInterval (carl::Variable::Arg _var, const DoubleInterval &_interval)
	updates or inserts an interval into the actual map More...

bool	hasEmptyInterval () const

std::set< const ContractionCandidate * >	appliedContractions ()

FormulaSetT	appliedConstraints ()

void	appliedConstraints (std::vector< FormulaT > &_result)

std::set< ConstraintT > &	rStateInfeasibleConstraints ()

const std::set< ConstraintT > &	stateInfeasibleConstraints () const

set_icpVariable &	rStateInfeasibleVariables ()

set_icpVariable	stateInfeasibleVariables () const

bool	addInfeasibleConstraint (const ConstraintT &_constraint, bool _addOnlyConstraint=false)

bool	addInfeasibleVariable (const IcpVariable *_variable, bool _addOnlyVariable=false)

void	addContraction (ContractionCandidate *_candidate, const set_icpVariable &_variables)

const std::set< const ContractionCandidate * > &	getCandidates () const

std::map< carl::Variable, std::set< ConstraintT > > &	rReasons ()

const std::map< carl::Variable, std::set< ConstraintT > > &	reasons () const

std::set< ConstraintT > &	reasons (carl::Variable::Arg _variable)

void	addReason (carl::Variable::Arg _variable, const ConstraintT &_reason)

void	addReasons (carl::Variable::Arg _variable, const std::set< ConstraintT > &_reasons)

void	addReasons (carl::Variable::Arg _variable, const FormulasT &_origins)

void	addVariableReason (carl::Variable::Arg _variable, const IcpVariable *_reason)

void	addVariableReasons (carl::Variable::Arg _variable, set_icpVariable _variables)

const std::map< carl::Variable, set_icpVariable > &	variableReasons ()

std::map< carl::Variable, set_icpVariable > &	rVariableReasons ()

set_icpVariable	variableReasons (carl::Variable::Arg _variable)

void	variableHull (carl::Variable::Arg _variable, set_icpVariable &_result) const

void	propagateStateInfeasibleConstraints (HistoryNode *_target) const

void	propagateStateInfeasibleVariables (HistoryNode *_target) const

void	print (std::ostream &_out=std::cout) const

void	printReasons (std::ostream &_out=std::cout) const

void	printVariableReasons (std::ostream &_out=std::cout) const

void	reset ()

Private Member Functions
void	gatherVariables (carl::Variable::Arg _var, set_icpVariable &_result) const
	Functions. More...

Private Attributes
EvalDoubleIntervalMap	mIntervals
	Members. More...

std::map< carl::Variable, std::set< ConstraintT > >	mReasons

std::map< carl::Variable, set_icpVariable >	mVariableReasons

std::set< const ContractionCandidate * >	mAppliedContractions

std::set< ConstraintT >	mStateInfeasibleConstraints

set_icpVariable	mStateInfeasibleVariables

Detailed Description

Definition at line 20 of file HistoryNode.h.

Constructor & Destructor Documentation

◆ HistoryNode() [1/2]

smtrat::icp::HistoryNode::HistoryNode ( )

inline

Methods.

Definition at line 44 of file HistoryNode.h.

◆ HistoryNode() [2/2]

smtrat::icp::HistoryNode::HistoryNode ( const EvalDoubleIntervalMap & _intervals )

inline

Definition at line 53 of file HistoryNode.h.

◆ ~HistoryNode()

smtrat::icp::HistoryNode::~HistoryNode ( )

inline

Definition at line 62 of file HistoryNode.h.

Member Function Documentation

◆ addContraction()

void smtrat::icp::HistoryNode::addContraction	(	ContractionCandidate *	_candidate,
		const set_icpVariable &	_variables
	)

inline

Definition at line 211 of file HistoryNode.h.

Here is the call graph for this function:

◆ addInfeasibleConstraint()

bool smtrat::icp::HistoryNode::addInfeasibleConstraint	(	const ConstraintT &	_constraint,
		bool	_addOnlyConstraint = `false`
	)

inline

Definition at line 180 of file HistoryNode.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addInfeasibleVariable()

bool smtrat::icp::HistoryNode::addInfeasibleVariable	(	const IcpVariable *	_variable,
		bool	_addOnlyVariable = `false`
	)

inline

Definition at line 197 of file HistoryNode.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addInterval()

bool smtrat::icp::HistoryNode::addInterval	(	carl::Variable::Arg	_var,
		const DoubleInterval &	_interval
	)

inline

updates or inserts an interval into the actual map

Parameters

_var
_interval

Returns: true if only an update

Definition at line 106 of file HistoryNode.h.

◆ addReason()

void smtrat::icp::HistoryNode::addReason	(	carl::Variable::Arg	_variable,
		const ConstraintT &	_reason
	)

inline

Definition at line 247 of file HistoryNode.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addReasons() [1/2]

void smtrat::icp::HistoryNode::addReasons	(	carl::Variable::Arg	_variable,
		const FormulasT &	_origins
	)

inline

Definition at line 271 of file HistoryNode.h.

Here is the call graph for this function:

◆ addReasons() [2/2]

void smtrat::icp::HistoryNode::addReasons	(	carl::Variable::Arg	_variable,
		const std::set< ConstraintT > &	_reasons
	)

inline

Definition at line 265 of file HistoryNode.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addVariableReason()

void smtrat::icp::HistoryNode::addVariableReason	(	carl::Variable::Arg	_variable,
		const IcpVariable *	_reason
	)

inline

Definition at line 290 of file HistoryNode.h.

Here is the caller graph for this function:

◆ addVariableReasons()

void smtrat::icp::HistoryNode::addVariableReasons	(	carl::Variable::Arg	_variable,
		set_icpVariable	_variables
	)

inline

Definition at line 295 of file HistoryNode.h.

◆ appliedConstraints() [1/2]

FormulaSetT smtrat::icp::HistoryNode::appliedConstraints ( )

inline

Definition at line 136 of file HistoryNode.h.

◆ appliedConstraints() [2/2]

void smtrat::icp::HistoryNode::appliedConstraints ( std::vector< FormulaT > & _result )

inline

Definition at line 149 of file HistoryNode.h.

◆ appliedContractions()

std::set<const ContractionCandidate*> smtrat::icp::HistoryNode::appliedContractions ( )

inline

Definition at line 131 of file HistoryNode.h.

◆ gatherVariables()

void smtrat::icp::HistoryNode::gatherVariables	(	carl::Variable::Arg	_var,
		set_icpVariable &	_result
	)		const

inlineprivate

Functions.

Definition at line 435 of file HistoryNode.h.

Here is the caller graph for this function:

◆ getCandidates()

const std::set<const ContractionCandidate*>& smtrat::icp::HistoryNode::getCandidates ( ) const

inline

Definition at line 225 of file HistoryNode.h.

◆ getInterval()

DoubleInterval& smtrat::icp::HistoryNode::getInterval ( carl::Variable::Arg _variable )

inline

Definition at line 79 of file HistoryNode.h.

◆ hasEmptyInterval()

bool smtrat::icp::HistoryNode::hasEmptyInterval ( ) const

inline

Definition at line 120 of file HistoryNode.h.

◆ intervals()

const EvalDoubleIntervalMap& smtrat::icp::HistoryNode::intervals ( ) const

inline

Getters and Setters.

Definition at line 69 of file HistoryNode.h.

◆ print()

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

inline

Definition at line 343 of file HistoryNode.h.

◆ printReasons()

void smtrat::icp::HistoryNode::printReasons ( std::ostream & _out = std::cout ) const

inline

Definition at line 389 of file HistoryNode.h.

◆ printVariableReasons()

void smtrat::icp::HistoryNode::printVariableReasons ( std::ostream & _out = std::cout ) const

inline

Definition at line 404 of file HistoryNode.h.

◆ propagateStateInfeasibleConstraints()

void smtrat::icp::HistoryNode::propagateStateInfeasibleConstraints ( HistoryNode * _target ) const

inline

Definition at line 324 of file HistoryNode.h.

Here is the call graph for this function:

◆ propagateStateInfeasibleVariables()

void smtrat::icp::HistoryNode::propagateStateInfeasibleVariables ( HistoryNode * _target ) const

inline

Definition at line 330 of file HistoryNode.h.

Here is the call graph for this function:

◆ reasons() [1/2]

const std::map<carl::Variable, std::set<ConstraintT> >& smtrat::icp::HistoryNode::reasons ( ) const

inline

Definition at line 235 of file HistoryNode.h.

◆ reasons() [2/2]

std::set<ConstraintT>& smtrat::icp::HistoryNode::reasons ( carl::Variable::Arg _variable )

inline

Definition at line 241 of file HistoryNode.h.

◆ reset()

void smtrat::icp::HistoryNode::reset ( )

inline

Definition at line 420 of file HistoryNode.h.

◆ rIntervals()

EvalDoubleIntervalMap& smtrat::icp::HistoryNode::rIntervals ( )

inline

Definition at line 74 of file HistoryNode.h.

◆ rReasons()

std::map<carl::Variable, std::set<ConstraintT> >& smtrat::icp::HistoryNode::rReasons ( )

inline

Definition at line 230 of file HistoryNode.h.

◆ rStateInfeasibleConstraints()

std::set<ConstraintT>& smtrat::icp::HistoryNode::rStateInfeasibleConstraints ( )

inline

Definition at line 160 of file HistoryNode.h.

◆ rStateInfeasibleVariables()

set_icpVariable& smtrat::icp::HistoryNode::rStateInfeasibleVariables ( )

inline

Definition at line 170 of file HistoryNode.h.

◆ rVariableReasons()

std::map<carl::Variable, set_icpVariable>& smtrat::icp::HistoryNode::rVariableReasons ( )

inline

Definition at line 306 of file HistoryNode.h.

◆ setIntervals()

void smtrat::icp::HistoryNode::setIntervals ( const EvalDoubleIntervalMap & _map )

inline

Definition at line 85 of file HistoryNode.h.

◆ stateInfeasibleConstraints()

const std::set<ConstraintT>& smtrat::icp::HistoryNode::stateInfeasibleConstraints ( ) const

inline

Definition at line 165 of file HistoryNode.h.

◆ stateInfeasibleVariables()

set_icpVariable smtrat::icp::HistoryNode::stateInfeasibleVariables ( ) const

inline

Definition at line 175 of file HistoryNode.h.

◆ variableHull()

void smtrat::icp::HistoryNode::variableHull	(	carl::Variable::Arg	_variable,
		set_icpVariable &	_result
	)		const

inline

Definition at line 318 of file HistoryNode.h.

Here is the call graph for this function:

◆ variableReasons() [1/2]

const std::map<carl::Variable, set_icpVariable>& smtrat::icp::HistoryNode::variableReasons ( )

inline

Definition at line 301 of file HistoryNode.h.

◆ variableReasons() [2/2]

set_icpVariable smtrat::icp::HistoryNode::variableReasons ( carl::Variable::Arg _variable )

inline

Definition at line 311 of file HistoryNode.h.

Field Documentation

◆ mAppliedContractions

std::set<const ContractionCandidate*> smtrat::icp::HistoryNode::mAppliedContractions

private

Definition at line 33 of file HistoryNode.h.

◆ mIntervals

EvalDoubleIntervalMap smtrat::icp::HistoryNode::mIntervals

private

Members.

Definition at line 30 of file HistoryNode.h.

◆ mReasons

std::map<carl::Variable, std::set<ConstraintT> > smtrat::icp::HistoryNode::mReasons

private

Definition at line 31 of file HistoryNode.h.

◆ mStateInfeasibleConstraints

std::set<ConstraintT> smtrat::icp::HistoryNode::mStateInfeasibleConstraints

private

Definition at line 34 of file HistoryNode.h.

◆ mStateInfeasibleVariables

set_icpVariable smtrat::icp::HistoryNode::mStateInfeasibleVariables

private

Definition at line 35 of file HistoryNode.h.

◆ mVariableReasons

std::map<carl::Variable, set_icpVariable> smtrat::icp::HistoryNode::mVariableReasons

private

Definition at line 32 of file HistoryNode.h.

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

smtrat-modules/ICPModule/HistoryNode.h

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ HistoryNode() [1/2]

◆ HistoryNode() [2/2]

◆ ~HistoryNode()

Member Function Documentation

◆ addContraction()

◆ addInfeasibleConstraint()

◆ addInfeasibleVariable()

◆ addInterval()

◆ addReason()

◆ addReasons() [1/2]

◆ addReasons() [2/2]

◆ addVariableReason()

◆ addVariableReasons()

◆ appliedConstraints() [1/2]

◆ appliedConstraints() [2/2]

◆ appliedContractions()

◆ gatherVariables()

◆ getCandidates()

◆ getInterval()

◆ hasEmptyInterval()

◆ intervals()

◆ print()

◆ printReasons()

◆ printVariableReasons()

◆ propagateStateInfeasibleConstraints()

◆ propagateStateInfeasibleVariables()

◆ reasons() [1/2]

◆ reasons() [2/2]

◆ reset()

◆ rIntervals()

◆ rReasons()

◆ rStateInfeasibleConstraints()

◆ rStateInfeasibleVariables()

◆ rVariableReasons()

◆ setIntervals()

◆ stateInfeasibleConstraints()

◆ stateInfeasibleVariables()

◆ variableHull()

◆ variableReasons() [1/2]

◆ variableReasons() [2/2]

Field Documentation

◆ mAppliedContractions

◆ mIntervals

◆ mReasons

◆ mStateInfeasibleConstraints

◆ mStateInfeasibleVariables

◆ mVariableReasons