#include <State.h>

Collaboration diagram for smtrat::vs::State:

[legend]

Public Types
enum	Type { TEST_CANDIDATE_TO_GENERATE , SUBSTITUTION_TO_APPLY , COMBINE_SUBRESULTS }

typedef carl::FastPointerMapB< Substitution, ConditionSetSetSet >	ConflictSets

typedef std::vector< std::pair< ConditionList, bool > >	SubstitutionResult

typedef std::vector< SubstitutionResult >	SubstitutionResults

typedef std::vector< std::pair< unsigned, unsigned > >	SubResultCombination

typedef smtrat::vb::VariableBounds< const Condition * >	VariableBoundsCond

Public Member Functions
	State (carl::IDPool *_conditionIdAllocator, bool _withVariableBounds)
	Constructs an empty state (no conditions yet) being the root (hence neither a substitution) of the state tree which is going to be formed when applying the satisfiability check based on virtual substitution. More...

	State (State const _father, const Substitution &_substitution, carl::IDPool _conditionIdAllocator, bool _withVariableBounds)
	Constructs a state being a child of the given state and containing the given substitution, which maps from the index variable of the given state. More...

	State (const State &)=delete

	~State ()
	Destructor. More...

bool	isRoot () const

bool	cannotBeSolved (bool _lazy) const

bool &	rCannotBeSolved ()

bool &	rCannotBeSolvedLazy ()

bool	markedAsDeleted () const

bool &	rMarkedAsDeleted ()

bool	hasChildrenToInsert () const

bool &	rHasChildrenToInsert ()

carl::Variable::Arg	index () const

size_t	valuation () const

size_t	backendCallValuation () const

size_t	id () const

size_t &	rID ()

std::list< State * > &	rChildren ()

const std::list< State * > &	children () const

State *	pFather () const

const State &	father () const

State &	rFather ()

ConflictSets &	rConflictSets ()

const ConflictSets &	conflictSets () const

bool &	rHasRecentlyAddedConditions ()

bool	hasRecentlyAddedConditions () const

bool &	rInconsistent ()

bool	isInconsistent () const

ConditionList &	rConditions ()

const ConditionList &	conditions () const

Substitution &	rSubstitution ()

const Substitution &	substitution () const

SubstitutionResults &	rSubstitutionResults ()

const SubstitutionResults &	substitutionResults () const

SubResultCombination &	rSubResultCombination ()

const SubResultCombination &	subResultCombination () const

const Substitution *	pSubstitution () const

bool	conditionsSimplified () const

bool	subResultsSimplified () const

bool &	rSubResultsSimplified ()

bool	takeSubResultCombAgain () const

bool &	rTakeSubResultCombAgain ()

bool	tryToRefreshIndex () const

bool	hasSubResultsCombination () const

bool	hasSubstitutionResults () const

bool	unfinished () const

Type	type () const

Type &	rType ()

const Condition *	pOriginalCondition () const

const Condition &	originalCondition () const

const carl::PointerSet< Condition > &	tooHighDegreeConditions () const

carl::PointerSet< Condition > &	rTooHighDegreeConditions ()

const VariableBoundsCond &	variableBounds () const

VariableBoundsCond &	rVariableBounds ()

void	setOriginalCondition (const Condition *_pOCondition)
	Sets the pointer of the original condition of this state to the given pointer to a condition. More...

size_t	currentRangeSize () const

void	resetCurrentRangeSize ()

const smtrat::Rational &	minIntTestCandidate () const

const smtrat::Rational &	maxIntTestCandidate () const

bool	hasInfinityChild () const

void	resetInfinityChild (const State *_state)

void	setInfinityChild (State *_state)

void	resetCannotBeSolvedLazyFlags ()

unsigned	treeDepth () const

bool	substitutionApplicable () const
	Checks if a substitution can be applied. More...

bool	substitutionApplicable (const smtrat::ConstraintT &_constraint) const
	Checks if the substitution of this state can be applied to the given constraint. More...

bool	hasNoninvolvedCondition () const
	Checks whether a condition exists, which was not involved in an elimination step. More...

bool	allTestCandidatesInvalidated (const Condition *_condition) const

bool	hasChildWithID () const
	Checks whether a child exists, which has no ID (!=0). More...

bool	containsState (const State *_state) const

bool	hasOnlyInconsistentChildren () const
	Checks whether a child exists, which is not yet marked as inconsistent. More...

bool	occursInEquation (const carl::Variable &) const
	Checks whether the given variable occurs in a equation. More...

bool	hasFurtherUncheckedTestCandidates () const
	Checks whether there exist more than one test candidate, which has still not been checked. More...

void	variables (carl::Variables &_variables) const
	Finds the variables, which occur in this state. More...

unsigned	numberOfNodes () const
	Determines the number of nodes in the tree with this state as root. More...

State &	root ()

bool	getNextIntTestCandidate (smtrat::Rational &_nextIntTestCandidate, size_t _maxIntRange)

bool	updateIntTestCandidates ()

bool	unfinishedAncestor (State *&_unfinAnt)
	Determines (if it exists) a ancestor node, which is unfinished, that is it has still substitution results to consider. More...

bool	bestCondition (const Condition *&_bestCondition, size_t _numberOfAllVariables, bool _preferEquation)
	Determines the most adequate condition and in it the most adequate variable in the state to generate test candidates for. More...

ConditionList::iterator	constraintExists (const smtrat::ConstraintT &_constraint)
	Checks if the given constraint already exists as condition in the state. More...

void	simplify (ValuationMap &_ranking)
	Cleans up all conditions in this state according to comparison between the corresponding constraints. More...

bool	simplify (ConditionList &_conditionVectorToSimplify, ConditionSetSet &_conflictSet, ValuationMap &_ranking, bool _stateConditions=false)
	Simplifies the given conditions according to comparison between the corresponding constraints. More...

void	setIndex (const carl::Variable &_index)
	Sets the index of this state. More...

void	addConflictSet (const Substitution *_substitution, ConditionSetSet &&_condSetSet)
	Adds a conflict set to the map of substitutions to conflict sets. More...

void	addConflicts (const Substitution *_substitution, ConditionSetSet &&_condSetSet)
	Adds all conflicts to all sets of the conflict set of the given substitution. More...

void	resetConflictSets ()
	Clears the conflict sets. More...

bool	updateOCondsOfSubstitutions (const Substitution &_substitution, std::vector< State * > &_reactivatedStates)
	Updates the original conditions of substitutions having the same test candidate as the given. More...

void	addSubstitutionResults (std::vector< DisjunctionOfConditionConjunctions > &&_disjunctionsOfCondConj)
	Adds the given substitution results to this state. More...

bool	extendSubResultCombination ()
	Extends the currently considered combination of conjunctions in the substitution results. More...

bool	nextSubResultCombination ()
	If the state contains a substitution result, which is a conjunction of disjunctions of conjunctions of conditions, this method sets the current combination to the disjunctions to the next combination. More...

size_t	getNumberOfCurrentSubresultCombination () const

ConditionList	getCurrentSubresultCombination () const
	Gets the current substitution result combination as condition vector. More...

bool	refreshConditions (ValuationMap &_ranking)
	Determines the condition vector corresponding to the current combination of the conjunctions of conditions. More...

void	initConditionFlags ()
	Sets all flags of the conditions to true, if it contains the variable given by the states index. More...

bool	initIndex (const carl::Variables &_allVariables, const smtrat::VariableValuationStrategy &_vvstrat, bool _preferEquation, bool _tryDifferentVarOrder=false, bool _useFixedVariableOrder=false)
	Sets, if it has not already happened, the index of the state to the name of the most adequate variable. More...

void	bestConstraintValuation (const std::vector< std::pair< carl::Variable, std::multiset< double >>> &_varVals)

void	averageConstraintValuation (const std::vector< std::pair< carl::Variable, std::multiset< double >>> &_varVals)

void	worstConstraintValuation (const std::vector< std::pair< carl::Variable, std::multiset< double >>> &_varVals)

void	addCondition (const smtrat::ConstraintT &_constraint, const carl::PointerSet< Condition > &_originalConditions, size_t _valutation, bool _recentlyAdded, ValuationMap &_ranking)
	Adds a constraint to the conditions of this state. More...

bool	checkSubresultCombinations () const
	This is just for debug purpose. More...

int	deleteOrigins (carl::PointerSet< Condition > &_originsToDelete, ValuationMap &_ranking)
	Removes everything in this state originated by the given vector of conditions. More...

void	deleteOriginsFromChildren (carl::PointerSet< Condition > &_originsToDelete, ValuationMap &_ranking)
	Deletes everything originated by the given conditions in the children of this state. More...

void	deleteOriginsFromConflictSets (carl::PointerSet< Condition > &_originsToDelete, bool _originsAreCurrentConditions)
	Deletes everything originated by the given conditions in the conflict sets of this state. More...

void	deleteOriginsFromSubstitutionResults (carl::PointerSet< Condition > &_originsToDelete)
	Deletes everything originated by the given conditions in the substitution results of this state. More...

void	deleteConditions (carl::PointerSet< Condition > &_conditionsToDelete, ValuationMap &_ranking)
	Delete everything originated by the given conditions from the entire subtree with this state as root. More...

std::vector< State * >	addChild (const Substitution &_substitution)
	Adds a state as child to this state with the given substitution. More...

void	updateValuation (bool _lazy)
	Updates the valuation of this state. More...

void	updateBackendCallValuation ()
	Valuates the state's currently considered conditions according to a backend call. More...

void	passConflictToFather (bool _checkConflictForSideCondition, bool _useBackjumping=true, bool _includeInconsistentTestCandidates=false)
	Passes the original conditions of the covering set of the conflicts of this state to its father. More...

bool	hasLocalConflict ()
	Checks whether the currently considered conditions, which have been considered for test candidate construction, form already a conflict. More...

bool	checkTestCandidatesForBounds ()
	Checks whether the test candidate of this state is valid against the variable intervals in the father of this state. More...

std::vector< smtrat::DoubleInterval >	solutionSpace (carl::PointerSet< Condition > &_conflictReason) const
	Determines the solution space of the test candidate of this state regarding to the variable bounds of the father. More...

bool	hasRootsInVariableBounds (const Condition *_condition, bool _useSturmSequence)
	Checks whether there are no zeros for the left-hand side of the constraint of the given condition. More...

void	print (const std::string _initiation="***", std::ostream &_out=std::cout) const
	Prints the conditions, the substitution and the substitution results of this state and all its children. More...

void	printAlone (const std::string="***", std::ostream &_out=std::cout) const
	Prints the conditions, the substitution and the substitution results of this state. More...

void	printConditions (const std::string _initiation="***", std::ostream &_out=std::cout, bool=false) const
	Prints the conditions of this state. More...

void	printSubstitutionResults (const std::string _initiation="***", std::ostream &_out=std::cout) const
	Prints the substitution results of this state. More...

void	printSubstitutionResultCombination (const std::string _initiation="***", std::ostream &_out=std::cout) const
	Prints the combination of substitution results used in this state. More...

void	printSubstitutionResultCombinationAsNumbers (const std::string _initiation="***", std::ostream &_out=std::cout) const
	Prints the combination of substitution results, expressed in numbers, used in this state. More...

void	printConflictSets (const std::string _initiation="***", std::ostream &_out=std::cout) const
	Prints the conflict sets of this state. More...

Static Public Member Functions
static void	removeStatesFromRanking (const State &toRemove, ValuationMap &_ranking)

static size_t	coveringSet (const ConditionSetSetSet &_conflictSets, carl::PointerSet< Condition > &_minCovSet, unsigned _currentTreeDepth)
	Finds a covering set of a vector of sets of sets due to some heuristics. More...

Private Attributes
bool	mConditionsSimplified
	A flag indicating whether the conditions this state considers are simplified. More...

bool	mHasChildrenToInsert
	A flag indicating whether there are states that are children of this state and must be still considered in the further progress of finding a solution. More...

bool	mHasRecentlyAddedConditions
	A flag that indicates whether this state has conditions in its considered list of conditions, which were recently added and, hence, must be propagated further. More...

bool	mInconsistent
	A flag that indicates whether this state is already inconsistent. More...

bool	mMarkedAsDeleted
	A flag indicating whether this state has already marked as deleted, which means that there is no need to consider it in the further progress of finding a solution. More...

bool	mSubResultsSimplified
	A flag indicating whether the substitution results this state are simplified. More...

bool	mTakeSubResultCombAgain
	A flag indicating whether to take the current combination of substitution results once again. More...

bool	mTestCandidateCheckedForBounds
	A flag indicating whether the test candidate contained by this state has already been check for the bounds of the variables. More...

bool	mCannotBeSolved
	A flag indicating whether this state has been progressed until a point where a condition must be involved having a too high degree to tackle with virtual substitution. More...

bool	mCannotBeSolvedLazy

bool	mTryToRefreshIndex
	A flag indicating whether the index (the variable to eliminate in this state) should be reconsidered and maybe changed. More...

size_t	mBackendCallValuation
	A heuristically determined value stating the expected difficulty of this state's considered conditions to be solved by a backend. More...

size_t	mID
	A unique id identifying this state. More...

size_t	mValuation
	A heuristically determined value stating the expected difficulty of this state's considered conditions to be solved by virtual substitution. More...

Type	mType
	The type of this state, which states whether this state has still a substitution to apply or either test candidates shall be generated or a new combination of the substitution results must be found in order to consider it next. More...

carl::Variable	mIndex
	The variable which is going to be eliminated from this state's considered conditions. More...

const Condition *	mpOriginalCondition
	If the test candidate considered by this state stems from a condition for which it is enough to consider it only for test candidate generation for finding the satisfiability of the conditions it occurs in, this member stores that condition. More...

State *	mpFather
	The father state of this state. More...

Substitution *	mpSubstitution
	The substitution this state considers. Note that it is NULL if this state is the root. More...

SubstitutionResults *	mpSubstitutionResults
	The vector storing the substitution results, that is for each application of the substitution in this state to one of its considered conditions a disjunction of conjunctions of constraints. More...

SubResultCombination *	mpSubResultCombination
	The currently considered combination of conjunctions of constraints in the substitution result vector, which form the currently considered conditions of this state (store in mpConditions). More...

ConditionList *	mpConditions
	The currently considered conditions of this state, for which the satisfiability must be checked. More...

ConflictSets *	mpConflictSets
	Stores for each already considered and failed test candidate all conflicts which have been found for it. More...

std::list< State * > *	mpChildren
	The children states of this state. More...

carl::PointerSet< Condition > *	mpTooHighDegreeConditions
	The conditions of this state, which cannot be solved by the virtual substitution. More...

VariableBoundsCond *	mpVariableBounds
	A pointer to an object which manages and stores the bounds on the variables occurring in this state. More...

State *	mpInfinityChild

smtrat::Rational	mMinIntTestCanidate

smtrat::Rational	mMaxIntTestCanidate

size_t	mCurrentIntRange

carl::IDPool *	mpConditionIdAllocator

std::vector< std::pair< carl::Variable, std::multiset< double > > >	mRealVarVals

std::vector< std::pair< carl::Variable, std::multiset< double > > >	mIntVarVals

std::vector< size_t >	mBestVarVals

Detailed Description

Definition at line 64 of file State.h.

Member Typedef Documentation

◆ ConflictSets

typedef carl::FastPointerMapB<Substitution,ConditionSetSetSet> smtrat::vs::State::ConflictSets

Definition at line 70 of file State.h.

◆ SubResultCombination

typedef std::vector<std::pair< unsigned, unsigned> > smtrat::vs::State::SubResultCombination

Definition at line 73 of file State.h.

◆ SubstitutionResult

typedef std::vector<std::pair< ConditionList, bool> > smtrat::vs::State::SubstitutionResult

Definition at line 71 of file State.h.

◆ SubstitutionResults

typedef std::vector<SubstitutionResult> smtrat::vs::State::SubstitutionResults

Definition at line 72 of file State.h.

◆ VariableBoundsCond

typedef smtrat::vb::VariableBounds<const Condition*> smtrat::vs::State::VariableBoundsCond

Definition at line 74 of file State.h.

Member Enumeration Documentation

◆ Type

enum smtrat::vs::State::Type

Enumerator
TEST_CANDIDATE_TO_GENERATE
SUBSTITUTION_TO_APPLY
COMBINE_SUBRESULTS

Definition at line 68 of file State.h.

Constructor & Destructor Documentation

◆ State() [1/3]

smtrat::vs::State::State	(	carl::IDPool *	_conditionIdAllocator,
		bool	_withVariableBounds
	)

Constructs an empty state (no conditions yet) being the root (hence neither a substitution) of the state tree which is going to be formed when applying the satisfiability check based on virtual substitution.

Parameters

_withVariableBounds A flag that indicates whether to use optimizations based on variable bounds.

Definition at line 30 of file State.cpp.

Here is the caller graph for this function:

◆ State() [2/3]

smtrat::vs::State::State	(	State *const	_father,
		const Substitution &	_substitution,
		carl::IDPool *	_conditionIdAllocator,
		bool	_withVariableBounds
	)

Constructs a state being a child of the given state and containing the given substitution, which maps from the index variable of the given state.

Parameters

_father	The father of the state to be constructed.
_substitution	The substitution of the state to be constructed.
_withVariableBounds	A flag that indicates whether to use optimizations based on variable bounds.

Definition at line 70 of file State.cpp.

◆ State() [3/3]

smtrat::vs::State::State ( const State & )

delete

◆ ~State()

smtrat::vs::State::~State ( )

Destructor.

Definition at line 110 of file State.cpp.

Here is the call graph for this function:

Member Function Documentation

◆ addChild()

std::vector< State * > smtrat::vs::State::addChild ( const Substitution & _substitution )

Adds a state as child to this state with the given substitution.

Parameters

_substitution The substitution to generate the state for.

Returns: true, if a state has been added as child to this state; false, otherwise.

Definition at line 1957 of file State.cpp.

Here is the call graph for this function:

◆ addCondition()

void smtrat::vs::State::addCondition	(	const smtrat::ConstraintT &	_constraint,
		const carl::PointerSet< Condition > &	_originalConditions,
		size_t	_valutation,
		bool	_recentlyAdded,
		ValuationMap &	_ranking
	)

Adds a constraint to the conditions of this state.

Parameters

_constraint	The constraint of the condition to add.
_originalConditions	The original conditions of the condition to add.
_valutation	The valuation of the condition to add.
_recentlyAdded	Is the condition a recently added one. @sideeffect The state can obtain a new condition.

Definition at line 1438 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addConflicts()

void smtrat::vs::State::addConflicts	(	const Substitution *	_substitution,
		ConditionSetSet &&	_condSetSet
	)

Adds all conflicts to all sets of the conflict set of the given substitution.

Parameters

_substitution	The corresponding substitution generated the conflict. (NULL in the case a detected conflict without substitution)
_condSetSet	The conflicts to add.

Definition at line 839 of file State.cpp.

◆ addConflictSet()

void smtrat::vs::State::addConflictSet	(	const Substitution *	_substitution,
		ConditionSetSet &&	_condSetSet
	)

Adds a conflict set to the map of substitutions to conflict sets.

Parameters

_substitution	The corresponding substitution generated the conflict. (NULL in the case a detected conflict without substitution)
_condSetSet	The conflicts to add.

Definition at line 818 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addSubstitutionResults()

void smtrat::vs::State::addSubstitutionResults ( std::vector< DisjunctionOfConditionConjunctions > && _disjunctionsOfCondConj )

Adds the given substitution results to this state.

Parameters

_disjunctionsOfCondConj The substitution results given by a vector of disjunctions of conjunctions of conditions.

Definition at line 915 of file State.cpp.

Here is the caller graph for this function:

◆ allTestCandidatesInvalidated()

bool smtrat::vs::State::allTestCandidatesInvalidated ( const Condition * _condition ) const

Parameters

A	condition, which is one of the currently considered constraints to check for satisfiability.

Returns: true, if all test candidates provided by the given condition are no solution of the currently considered conjunction of constraints to check for satisfiability.

Definition at line 230 of file State.cpp.

Here is the call graph for this function:

◆ averageConstraintValuation()

void smtrat::vs::State::averageConstraintValuation ( const std::vector< std::pair< carl::Variable, std::multiset< double >>> & _varVals )

Definition at line 1350 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ backendCallValuation()

size_t smtrat::vs::State::backendCallValuation ( ) const

inline

Returns: The valuation of the state's considered conditions for a possible backend call.

Definition at line 299 of file State.h.

Here is the caller graph for this function:

◆ bestCondition()

bool smtrat::vs::State::bestCondition	(	const Condition *&	_bestCondition,
		size_t	_numberOfAllVariables,
		bool	_preferEquation
	)

Determines the most adequate condition and in it the most adequate variable in the state to generate test candidates for.

Parameters

_bestCondition	The most adequate condition to be the next test candidate provider.
_numberOfAllVariables	The number of all globally known variables.
_preferEquation	A flag that indicates to prefer equations in the heuristics of this method.

Returns: true, if it has a condition and a variable in it to generate test candidates for; false, otherwise.

Definition at line 398 of file State.cpp.

Here is the call graph for this function:

◆ bestConstraintValuation()

void smtrat::vs::State::bestConstraintValuation ( const std::vector< std::pair< carl::Variable, std::multiset< double >>> & _varVals )

Definition at line 1291 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ cannotBeSolved()

bool smtrat::vs::State::cannotBeSolved ( bool _lazy ) const

inline

Returns: A constant reference to the flag indicating whether a condition with too high degree for the virtual substitution method must be considered.

Definition at line 218 of file State.h.

Here is the caller graph for this function:

◆ checkSubresultCombinations()

bool smtrat::vs::State::checkSubresultCombinations ( ) const

This is just for debug purpose.

Returns: true, if no subresult combination is illegal.

Definition at line 1495 of file State.cpp.

Here is the call graph for this function:

◆ checkTestCandidatesForBounds()

bool smtrat::vs::State::checkTestCandidatesForBounds ( )

Checks whether the test candidate of this state is valid against the variable intervals in the father of this state.

Returns: true, if the test candidate of this state is valid against the variable intervals; false, otherwise.

Definition at line 2297 of file State.cpp.

Here is the call graph for this function:

◆ children()

const std::list<State*>& smtrat::vs::State::children ( ) const

inline

Returns: A constant reference to the vector of the children of this state.

Definition at line 331 of file State.h.

Here is the caller graph for this function:

◆ conditions()

const ConditionList& smtrat::vs::State::conditions ( ) const

inline

Returns: A constant reference to the currently considered conditions of this state.

Definition at line 422 of file State.h.

Here is the caller graph for this function:

◆ conditionsSimplified()

bool smtrat::vs::State::conditionsSimplified ( ) const

inline

Returns: true, if the considered conditions of this state are already simplified.

Definition at line 494 of file State.h.

Here is the caller graph for this function:

◆ conflictSets()

const ConflictSets& smtrat::vs::State::conflictSets ( ) const

inline

Returns: A constant reference to the conflict sets of this state.

Definition at line 371 of file State.h.

Here is the caller graph for this function:

◆ constraintExists()

ConditionList::iterator smtrat::vs::State::constraintExists ( const smtrat::ConstraintT & _constraint )

Checks if the given constraint already exists as condition in the state.

Parameters

_constraint The constraint, for which we want to know, if it already exists as condition in the state.

Returns: An iterator to the condition, which involves the constraint or an iterator to the end of the vector of conditions of this state.

Definition at line 435 of file State.cpp.

Here is the call graph for this function:

◆ containsState()

bool smtrat::vs::State::containsState ( const State * _state ) const

Returns: true, if the given state is a node in the state tree starting at this node; false, otherwise.

Definition at line 255 of file State.cpp.

Here is the call graph for this function:

◆ coveringSet()

size_t smtrat::vs::State::coveringSet	(	const ConditionSetSetSet &	_conflictSets,
		carl::PointerSet< Condition > &	_minCovSet,
		unsigned	_currentTreeDepth
	)

static

Finds a covering set of a vector of sets of sets due to some heuristics.

Parameters

_conflictSets	The vector of sets of sets, for which the method finds all minimum covering sets.
_minCovSet	The found mininum covering set.
_currentTreeDepth	The tree depth of the state from which this method is invoked.

Returns: The greatest level, where a condition of the covering set has been created.

Definition at line 2817 of file State.cpp.

Here is the caller graph for this function:

◆ currentRangeSize()

size_t smtrat::vs::State::currentRangeSize ( ) const

inline

Definition at line 654 of file State.h.

◆ deleteConditions()

void smtrat::vs::State::deleteConditions	(	carl::PointerSet< Condition > &	_conditionsToDelete,
		ValuationMap &	_ranking
	)

Delete everything originated by the given conditions from the entire subtree with this state as root.

Parameters

_conditionsToDelete The conditions to delete.

Definition at line 1610 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ deleteOrigins()

int smtrat::vs::State::deleteOrigins	(	carl::PointerSet< Condition > &	_originsToDelete,
		ValuationMap &	_ranking
	)

Removes everything in this state originated by the given vector of conditions.

Parameters

_originsToDelete The conditions for which everything in this state which has been originated by them must be removed.

Returns: 0, if this state got invalid and must be deleted afterwards; -1, if this state got invalid and must be deleted afterwards and made other states unnecessary to consider; 1, otherwise.

Definition at line 1510 of file State.cpp.

Here is the call graph for this function:

◆ deleteOriginsFromChildren()

void smtrat::vs::State::deleteOriginsFromChildren	(	carl::PointerSet< Condition > &	_originsToDelete,
		ValuationMap &	_ranking
	)

Deletes everything originated by the given conditions in the children of this state.

Parameters

_originsToDelete The condition for which to delete everything originated by them.

Definition at line 1682 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ deleteOriginsFromConflictSets()

void smtrat::vs::State::deleteOriginsFromConflictSets	(	carl::PointerSet< Condition > &	_originsToDelete,
		bool	_originsAreCurrentConditions
	)

Deletes everything originated by the given conditions in the conflict sets of this state.

Parameters

_originsToDelete	The condition for which to delete everything originated by them.
_originsAreCurrentConditions	A flag indicating whether the origins to remove stem from conditions of the currently considered condition vector of the father of this state and not, e.g., from somewhere in its substitution results.

Definition at line 1714 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ deleteOriginsFromSubstitutionResults()

void smtrat::vs::State::deleteOriginsFromSubstitutionResults ( carl::PointerSet< Condition > & _originsToDelete )

Deletes everything originated by the given conditions in the substitution results of this state.

Parameters

_originsToDelete The conditions for which to delete everything originated by them.

Definition at line 1846 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ extendSubResultCombination()

bool smtrat::vs::State::extendSubResultCombination ( )

Extends the currently considered combination of conjunctions in the substitution results.

Definition at line 933 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ father()

const State& smtrat::vs::State::father ( ) const

inline

Returns: A constant reference to the father of this state. This method fails if this state is the root.

Definition at line 347 of file State.h.

Here is the caller graph for this function:

◆ getCurrentSubresultCombination()

ConditionList smtrat::vs::State::getCurrentSubresultCombination ( ) const

Gets the current substitution result combination as condition vector.

Returns: The current substitution result combination as condition vector.

Definition at line 1079 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getNextIntTestCandidate()

bool smtrat::vs::State::getNextIntTestCandidate	(	smtrat::Rational &	_nextIntTestCandidate,
		size_t	_maxIntRange
	)

Definition at line 322 of file State.cpp.

Here is the call graph for this function:

◆ getNumberOfCurrentSubresultCombination()

size_t smtrat::vs::State::getNumberOfCurrentSubresultCombination ( ) const

Returns: The number of the current substitution result combination.

Definition at line 1052 of file State.cpp.

Here is the call graph for this function:

◆ hasChildrenToInsert()

bool smtrat::vs::State::hasChildrenToInsert ( ) const

inline

Returns: A constant reference to the flag indicating whether there are states that are children of this state and must be still considered in the further progress of finding a solution.

Definition at line 263 of file State.h.

◆ hasChildWithID()

bool smtrat::vs::State::hasChildWithID ( ) const

Checks whether a child exists, which has no ID (!=0).

Returns: true, if there exists a child with ID (!=0); false, otherwise.

Definition at line 242 of file State.cpp.

Here is the call graph for this function:

◆ hasFurtherUncheckedTestCandidates()

bool smtrat::vs::State::hasFurtherUncheckedTestCandidates ( ) const

Checks whether there exist more than one test candidate, which has still not been checked.

Returns: true, if there exist more than one test candidate, which has still not been checked; false, otherwise.

Definition at line 285 of file State.cpp.

Here is the call graph for this function:

◆ hasInfinityChild()

bool smtrat::vs::State::hasInfinityChild ( ) const

inline

Definition at line 685 of file State.h.

◆ hasLocalConflict()

bool smtrat::vs::State::hasLocalConflict ( )

Checks whether the currently considered conditions, which have been considered for test candidate construction, form already a conflict.

Returns: true, if they form a conflict; false, otherwise.

Definition at line 2201 of file State.cpp.

Here is the call graph for this function:

◆ hasNoninvolvedCondition()

bool smtrat::vs::State::hasNoninvolvedCondition ( ) const

Checks whether a condition exists, which was not involved in an elimination step.

Returns: true, if there exists a condition in the state, which was not already involved in an elimination step; false, otherwise.

Definition at line 217 of file State.cpp.

Here is the call graph for this function:

◆ hasOnlyInconsistentChildren()

bool smtrat::vs::State::hasOnlyInconsistentChildren ( ) const

Checks whether a child exists, which is not yet marked as inconsistent.

Returns: true, if there exists such a child; false, otherwise.

Definition at line 264 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ hasRecentlyAddedConditions()

bool smtrat::vs::State::hasRecentlyAddedConditions ( ) const

inline

Returns: true, if this state has a recently added condition in its considered conditions.

Definition at line 388 of file State.h.

Here is the caller graph for this function:

◆ hasRootsInVariableBounds()

bool smtrat::vs::State::hasRootsInVariableBounds	(	const Condition *	_condition,
		bool	_useSturmSequence
	)

Checks whether there are no zeros for the left-hand side of the constraint of the given condition.

Parameters

_condition	The condition to check.
A	flag that indicates whether to include Sturm's sequences and root counting in this method.

Returns: true, if the constraint of the left-hand side of the given condition has no roots in the variable bounds of this state; false, otherwise.

Definition at line 2423 of file State.cpp.

Here is the call graph for this function:

◆ hasSubResultsCombination()

bool smtrat::vs::State::hasSubResultsCombination ( ) const

inline

Returns: true, if this state has a substitution result combination.

Definition at line 544 of file State.h.

Here is the caller graph for this function:

◆ hasSubstitutionResults()

bool smtrat::vs::State::hasSubstitutionResults ( ) const

inline

Returns: true, if this state has substitution results.

Definition at line 552 of file State.h.

Here is the caller graph for this function:

◆ id()

size_t smtrat::vs::State::id ( ) const

inline

Returns: The id of this state.

Definition at line 307 of file State.h.

Here is the caller graph for this function:

◆ index()

carl::Variable::Arg smtrat::vs::State::index ( ) const

inline

Returns: A constant reference to the variable which is going to be eliminated from this state's considered conditions. Note, if there is no variable decided to be eliminated, this method will fail.

Definition at line 282 of file State.h.

Here is the caller graph for this function:

◆ initConditionFlags()

void smtrat::vs::State::initConditionFlags ( )

Sets all flags of the conditions to true, if it contains the variable given by the states index.

Definition at line 1182 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ initIndex()

bool smtrat::vs::State::initIndex	(	const carl::Variables &	_allVariables,
		const smtrat::VariableValuationStrategy &	_vvstrat,
		bool	_preferEquation,
		bool	_tryDifferentVarOrder = `false`,
		bool	_useFixedVariableOrder = `false`
	)

Sets, if it has not already happened, the index of the state to the name of the most adequate variable.

Which variable is taken depends on heuristics.

Parameters

_allVariables	All globally known variables.
_vvstrat	The strategy according which we choose the variable.
_preferEquation	A flag that indicates to prefer equations in the heuristics of this method.
_tryDifferentVarOrder

Definition at line 1191 of file State.cpp.

Here is the call graph for this function:

◆ isInconsistent()

bool smtrat::vs::State::isInconsistent ( ) const

inline

Returns: true if this state's considered conditions are inconsistent; false, otherwise, which does not necessarily mean that this state is consistent.

Definition at line 406 of file State.h.

Here is the caller graph for this function:

◆ isRoot()

bool smtrat::vs::State::isRoot ( ) const

inline

Returns: The root of the state tree where this state is part from.

Definition at line 209 of file State.h.

Here is the caller graph for this function:

◆ markedAsDeleted()

bool smtrat::vs::State::markedAsDeleted ( ) const

inline

Returns: A constant reference to the flag indicating whether this state is marked as deleted, which means that there is no need to consider it in the further progress of finding a solution.

Definition at line 245 of file State.h.

Here is the caller graph for this function:

◆ maxIntTestCandidate()

const smtrat::Rational& smtrat::vs::State::maxIntTestCandidate ( ) const

inline

Definition at line 680 of file State.h.

Here is the caller graph for this function:

◆ minIntTestCandidate()

const smtrat::Rational& smtrat::vs::State::minIntTestCandidate ( ) const

inline

Definition at line 672 of file State.h.

Here is the caller graph for this function:

◆ nextSubResultCombination()

bool smtrat::vs::State::nextSubResultCombination ( )

If the state contains a substitution result, which is a conjunction of disjunctions of conjunctions of conditions, this method sets the current combination to the disjunctions to the next combination.

Returns: true, if there is a next combination; false, otherwise.

Definition at line 992 of file State.cpp.

Here is the call graph for this function:

◆ numberOfNodes()

unsigned smtrat::vs::State::numberOfNodes ( ) const

Determines the number of nodes in the tree with this state as root.

Returns: The number of nodes in the tree with this state as root.

Definition at line 306 of file State.cpp.

Here is the call graph for this function:

◆ occursInEquation()

bool smtrat::vs::State::occursInEquation ( const carl::Variable & _variable ) const

Checks whether the given variable occurs in a equation.

Returns: true, if the given variable occurs in a equation; false, otherwise.

Definition at line 277 of file State.cpp.

Here is the call graph for this function:

◆ originalCondition()

const Condition& smtrat::vs::State::originalCondition ( ) const

inline

Returns: A reference to the original conditions of this state. Note that if there is no such condition, this method fails. For further information see the description of the corresponding member.

Definition at line 599 of file State.h.

Here is the caller graph for this function:

◆ passConflictToFather()

void smtrat::vs::State::passConflictToFather	(	bool	_checkConflictForSideCondition,
		bool	_useBackjumping = `true`,
		bool	_includeInconsistentTestCandidates = `false`
	)

Passes the original conditions of the covering set of the conflicts of this state to its father.

Parameters

_checkConflictForSideCondition	If this flag is set to false it might save some computations but leads to an over-approximative behavior. Recommendation: set it to true.
_includeInconsistentTestCandidates	If this flag is set to true the conflict analysis takes also the invalid test candidates' conflict sets into account. Recommendation: set it to false.
_useBackjumping	If true, we use the backjumping technique.

Definition at line 2082 of file State.cpp.

Here is the call graph for this function:

◆ pFather()

State* smtrat::vs::State::pFather ( ) const

inline

Returns: A pointer to the father of this state. It is NULL if this state is the root.

Definition at line 339 of file State.h.

Here is the caller graph for this function:

◆ pOriginalCondition()

const Condition* smtrat::vs::State::pOriginalCondition ( ) const

inline

Returns: A pointer to the original condition of this state or NULL, if there is no such condition. For further information see the description of the corresponding member.

Definition at line 590 of file State.h.

Here is the caller graph for this function:

◆ print()

void smtrat::vs::State::print	(	const std::string	_initiation = `"***"`,
		std::ostream &	_out = `std::cout`
	)		const

Prints the conditions, the substitution and the substitution results of this state and all its children.

Parameters

_initiation	A string which is printed in the beginning of every row.
_out	The stream to print on.

Definition at line 2570 of file State.cpp.

Here is the call graph for this function:

◆ printAlone()

void smtrat::vs::State::printAlone	(	const std::string	_initiation = `"***"`,
		std::ostream &	_out = `std::cout`
	)		const

Prints the conditions, the substitution and the substitution results of this state.

Parameters

_initiation	A string which is printed in the beginning of every row.
_out	The stream to print on.

Definition at line 2580 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printConditions()

void smtrat::vs::State::printConditions	(	const std::string	_initiation = `"***"`,
		std::ostream &	_out = `std::cout`,
		bool	_onlyAsConstraints = `false`
	)		const

Prints the conditions of this state.

Parameters

_initiation	A string which is printed in the beginning of every row.
_out	The stream to print on.

Definition at line 2666 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printConflictSets()

void smtrat::vs::State::printConflictSets	(	const std::string	_initiation = `"***"`,
		std::ostream &	_out = `std::cout`
	)		const

Prints the conflict sets of this state.

Parameters

_initiation	A string which is printed in the beginning of every row.
_out	The stream to print on.

Definition at line 2749 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printSubstitutionResultCombination()

void smtrat::vs::State::printSubstitutionResultCombination	(	const std::string	_initiation = `"***"`,
		std::ostream &	_out = `std::cout`
	)		const

Prints the combination of substitution results used in this state.

Parameters

_initiation	A string which is printed in the beginning of every row.
_out	The stream to print on.

Definition at line 2712 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printSubstitutionResultCombinationAsNumbers()

void smtrat::vs::State::printSubstitutionResultCombinationAsNumbers	(	const std::string	_initiation = `"***"`,
		std::ostream &	_out = `std::cout`
	)		const

Prints the combination of substitution results, expressed in numbers, used in this state.

Parameters

_initiation	A string which is printed in the beginning of every row.
_out	The stream to print on.

Definition at line 2735 of file State.cpp.

Here is the call graph for this function:

◆ printSubstitutionResults()

void smtrat::vs::State::printSubstitutionResults	(	const std::string	_initiation = `"***"`,
		std::ostream &	_out = `std::cout`
	)		const

Prints the substitution results of this state.

Parameters

_initiation	A string which is printed in the beginning of every row.
_out	The stream to print on.

Definition at line 2680 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ pSubstitution()

const Substitution* smtrat::vs::State::pSubstitution ( ) const

inline

Returns: A pointer to the substitution of this state, which is NULL, if this state is the root.

Definition at line 486 of file State.h.

Here is the caller graph for this function:

◆ rCannotBeSolved()

bool& smtrat::vs::State::rCannotBeSolved ( )

inline

Returns: A reference to the flag indicating whether a condition with too high degree for the virtual substitution method must be considered.

Definition at line 227 of file State.h.

◆ rCannotBeSolvedLazy()

bool& smtrat::vs::State::rCannotBeSolvedLazy ( )

inline

Returns: A reference to the flag indicating whether a condition with too high degree for the virtual substitution method must be considered.

Definition at line 236 of file State.h.

◆ rChildren()

std::list<State*>& smtrat::vs::State::rChildren ( )

inline

Returns: A reference to the vector of the children of this state.

Definition at line 323 of file State.h.

Here is the caller graph for this function:

◆ rConditions()

ConditionList& smtrat::vs::State::rConditions ( )

inline

Returns: A reference to the currently considered conditions of this state.

Definition at line 414 of file State.h.

Here is the caller graph for this function:

◆ rConflictSets()

ConflictSets& smtrat::vs::State::rConflictSets ( )

inline

Returns: A reference to the conflict sets of this state.

Definition at line 363 of file State.h.

Here is the caller graph for this function:

◆ refreshConditions()

bool smtrat::vs::State::refreshConditions ( ValuationMap & _ranking )

Determines the condition vector corresponding to the current combination of the conjunctions of conditions.

Returns: true, if there has been a change in the currently considered condition vector. false, otherwise.

Definition at line 1096 of file State.cpp.

Here is the call graph for this function:

◆ removeStatesFromRanking()

void smtrat::vs::State::removeStatesFromRanking	(	const State &	toRemove,
		ValuationMap &	_ranking
	)

static

Definition at line 170 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ resetCannotBeSolvedLazyFlags()

void smtrat::vs::State::resetCannotBeSolvedLazyFlags ( )

Definition at line 178 of file State.cpp.

◆ resetConflictSets()

void smtrat::vs::State::resetConflictSets ( )

Clears the conflict sets.

Definition at line 862 of file State.cpp.

◆ resetCurrentRangeSize()

void smtrat::vs::State::resetCurrentRangeSize ( )

inline

Definition at line 662 of file State.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ resetInfinityChild()

void smtrat::vs::State::resetInfinityChild ( const State * _state )

inline

Definition at line 690 of file State.h.

◆ rFather()

State& smtrat::vs::State::rFather ( )

inline

Returns: A reference to the father of this state. This method fails if this state is the root.

Definition at line 355 of file State.h.

Here is the caller graph for this function:

◆ rHasChildrenToInsert()

bool& smtrat::vs::State::rHasChildrenToInsert ( )

inline

Returns: A reference to the flag indicating whether there are states that are children of this state and must be still considered in the further progress of finding a solution.

Definition at line 272 of file State.h.

◆ rHasRecentlyAddedConditions()

bool& smtrat::vs::State::rHasRecentlyAddedConditions ( )

inline

Returns: A reference to the flag indicating that this state has a recently added condition in its considered conditions.

Definition at line 380 of file State.h.

Here is the caller graph for this function:

◆ rID()

size_t& smtrat::vs::State::rID ( )

inline

Returns: A reference to the id of this state.

Definition at line 315 of file State.h.

◆ rInconsistent()

bool& smtrat::vs::State::rInconsistent ( )

inline

Returns: A reference to the flag indicating whether this state's considered conditions are inconsistent. Note that if it is false, it does not necessarily mean that this state is consistent.

Definition at line 397 of file State.h.

Here is the caller graph for this function:

◆ rMarkedAsDeleted()

bool& smtrat::vs::State::rMarkedAsDeleted ( )

inline

Returns: A reference to the flag indicating whether this state is marked as deleted, which means that there is no need to consider it in the further progress of finding a solution.

Definition at line 254 of file State.h.

Here is the caller graph for this function:

◆ root()

State & smtrat::vs::State::root ( )

Returns: The root of the tree, in which this state is located.

Definition at line 314 of file State.cpp.

Here is the call graph for this function:

◆ rSubResultCombination()

SubResultCombination& smtrat::vs::State::rSubResultCombination ( )

inline

Returns: A reference to the current combination of conjunction of constraints within the substitution results of this state. Make sure that a substitution result combination exists when calling this method. (using, e.g., hasSubResultsCombination())

Definition at line 468 of file State.h.

Here is the caller graph for this function:

◆ rSubResultsSimplified()

bool& smtrat::vs::State::rSubResultsSimplified ( )

inline

Returns: A reference to the flag indicating whether the substitution results of this state are already simplified.

Definition at line 510 of file State.h.

Here is the caller graph for this function:

◆ rSubstitution()

Substitution& smtrat::vs::State::rSubstitution ( )

inline

Returns: A reference to the substitution this state considers. Note that this method fails, if this state is the root.

Definition at line 431 of file State.h.

Here is the caller graph for this function:

◆ rSubstitutionResults()

SubstitutionResults& smtrat::vs::State::rSubstitutionResults ( )

inline

Returns: A reference to the substitution results of this state. Make sure that the substitution results exist when calling this method. (using, e.g., hasSubstitutionResults())

Definition at line 449 of file State.h.

Here is the caller graph for this function:

◆ rTakeSubResultCombAgain()

bool& smtrat::vs::State::rTakeSubResultCombAgain ( )

inline

Returns: A reference to the flag indicating whether the current substitution result combination has to be consider once again before considering the next one.

Definition at line 528 of file State.h.

Here is the caller graph for this function:

◆ rTooHighDegreeConditions()

carl::PointerSet<Condition>& smtrat::vs::State::rTooHighDegreeConditions ( )

inline

Returns: A reference to the conditions of those this state currently considers, which have a too high degree to be tackled of the virtual substitution method.

Definition at line 617 of file State.h.

◆ rType()

Type& smtrat::vs::State::rType ( )

inline

Returns: A constant reference to the type of this state: This state has still a substitution to apply or either test candidates shall be generated or a new combination of the substitution results must be found in order to consider it next.

Definition at line 581 of file State.h.

Here is the caller graph for this function:

◆ rVariableBounds()

VariableBoundsCond& smtrat::vs::State::rVariableBounds ( )

inline

Returns: A reference to the object managing and storing the variable's bounds which were extracted from the currently considered conditions of this state.

Definition at line 636 of file State.h.

◆ setIndex()

void smtrat::vs::State::setIndex ( const carl::Variable & _index )

Sets the index of this state.

Parameters

_index The string to which the index should be set.

Definition at line 812 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setInfinityChild()

void smtrat::vs::State::setInfinityChild ( State * _state )

inline

Definition at line 696 of file State.h.

◆ setOriginalCondition()

void smtrat::vs::State::setOriginalCondition ( const Condition * _pOCondition )

inline

Sets the pointer of the original condition of this state to the given pointer to a condition.

Parameters

_pOCondition The pointer to set the original condition to.

Definition at line 646 of file State.h.

◆ simplify() [1/2]

bool smtrat::vs::State::simplify	(	ConditionList &	_conditionVectorToSimplify,
		ConditionSetSet &	_conflictSet,
		ValuationMap &	_ranking,
		bool	_stateConditions = `false`
	)

Simplifies the given conditions according to comparison between the corresponding constraints.

Parameters

_conditionVectorToSimplify	The conditions to simplify. Note, that this method can change these conditions.
_conflictSet	All conflicts this method detects in the given conditions are stored in here.
_stateConditions	A flag indicating whether the conditions to simplify are from the considered condition vector of this state and not, e.g., from somewhere in its substitution results.

Returns: true, if the conditions are not obviously conflicting; false, otherwise.

Definition at line 586 of file State.cpp.

Here is the call graph for this function:

◆ simplify() [2/2]

void smtrat::vs::State::simplify ( ValuationMap & _ranking )

Cleans up all conditions in this state according to comparison between the corresponding constraints.

Definition at line 443 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ solutionSpace()

std::vector< smtrat::DoubleInterval > smtrat::vs::State::solutionSpace ( carl::PointerSet< Condition > & _conflictReason ) const

Determines the solution space of the test candidate of this state regarding to the variable bounds of the father.

The solution space consists of one or two disjoint intervals.

Parameters

_conflictReason If the solution space is empty, the conditions being responsible for this conflict are stored in here.

Returns: The disjoint intervals representing the solution space.

Definition at line 2324 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ subResultCombination()

const SubResultCombination& smtrat::vs::State::subResultCombination ( ) const

inline

Returns: A constant reference to the current combination of conjunction of constraints within the substitution results of this state. Make sure that a substitution result combination exists when calling this method. (using, e.g., hasSubResultsCombination())

Definition at line 478 of file State.h.

Here is the caller graph for this function:

◆ subResultsSimplified()

bool smtrat::vs::State::subResultsSimplified ( ) const

inline

Returns: true, if the substitution results of this state are already simplified.

Definition at line 502 of file State.h.

Here is the caller graph for this function:

◆ substitution()

const Substitution& smtrat::vs::State::substitution ( ) const

inline

Returns: A constant reference to the substitution this state considers. Note that this method fails, if this state is the root.

Definition at line 440 of file State.h.

Here is the caller graph for this function:

◆ substitutionApplicable() [1/2]

bool smtrat::vs::State::substitutionApplicable ( ) const

Checks if a substitution can be applied.

Returns: true, if a substitution can be applied. false, else.

Definition at line 197 of file State.cpp.

Here is the call graph for this function:

◆ substitutionApplicable() [2/2]

bool smtrat::vs::State::substitutionApplicable ( const smtrat::ConstraintT & _constraint ) const

Checks if the substitution of this state can be applied to the given constraint.

Parameters

_constraint The constraint, for which we want to know, if the substitution is applicable.

Returns: true, if the substitution can be applied; false, otherwise.

Definition at line 209 of file State.cpp.

Here is the call graph for this function:

◆ substitutionResults()

const SubstitutionResults& smtrat::vs::State::substitutionResults ( ) const

inline

Returns: A constant reference to the substitution results of this state. Make sure that the substitution results exist when calling this method. (using, e.g., hasSubstitutionResults())

Definition at line 458 of file State.h.

Here is the caller graph for this function:

◆ takeSubResultCombAgain()

bool smtrat::vs::State::takeSubResultCombAgain ( ) const

inline

Returns: true, if the current substitution result combination has to be consider once again before considering the next one.

Definition at line 519 of file State.h.

Here is the caller graph for this function:

◆ tooHighDegreeConditions()

const carl::PointerSet<Condition>& smtrat::vs::State::tooHighDegreeConditions ( ) const

inline

Returns: A constant reference to the conditions of those this state currently considers, which have a too high degree to be tackled of the virtual substitution method.

Definition at line 608 of file State.h.

Here is the caller graph for this function:

◆ treeDepth()

unsigned smtrat::vs::State::treeDepth ( ) const

Returns: The depth of the subtree with this state as root node.

Definition at line 185 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ tryToRefreshIndex()

bool smtrat::vs::State::tryToRefreshIndex ( ) const

inline

Returns: true, if the index variable of this state shall be recalculated.

Definition at line 536 of file State.h.

Here is the caller graph for this function:

◆ type()

Type smtrat::vs::State::type ( ) const

inline

Returns: The type of this state: This state has still a substitution to apply or either test candidates shall be generated or a new combination of the substitution results must be found in order to consider it next.

Definition at line 571 of file State.h.

Here is the caller graph for this function:

◆ unfinished()

bool smtrat::vs::State::unfinished ( ) const

inline

Returns: true, if the currently considered substitution result combination can be extended by taking further substitution results into account.

Definition at line 561 of file State.h.

Here is the caller graph for this function:

◆ unfinishedAncestor()

bool smtrat::vs::State::unfinishedAncestor ( State *& _unfinAnt )

Determines (if it exists) a ancestor node, which is unfinished, that is it has still substitution results to consider.

Parameters

_unfinAnt The unfinished ancestor node.

Returns: true, if it has a unfinished ancestor; false, otherwise.

Definition at line 386 of file State.cpp.

Here is the call graph for this function:

◆ updateBackendCallValuation()

void smtrat::vs::State::updateBackendCallValuation ( )

Valuates the state's currently considered conditions according to a backend call.

Note: The settings are currently optimized for CAD backend calls.

Definition at line 2060 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ updateIntTestCandidates()

bool smtrat::vs::State::updateIntTestCandidates ( )

Definition at line 343 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ updateOCondsOfSubstitutions()

bool smtrat::vs::State::updateOCondsOfSubstitutions	(	const Substitution &	_substitution,
		std::vector< State * > &	_reactivatedStates
	)

Updates the original conditions of substitutions having the same test candidate as the given.

Parameters

_substitution	The substitution containing the test candidate to check for.
_reactivatedStates

Returns: true, if the test candidate of the given substitution was already generated; false, otherwise.

Definition at line 873 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ updateValuation()

void smtrat::vs::State::updateValuation ( bool _lazy )

Updates the valuation of this state.

Definition at line 2023 of file State.cpp.

Here is the call graph for this function:

◆ valuation()

size_t smtrat::vs::State::valuation ( ) const

inline

Returns: The heuristically determined valuation of this state (see for the description of the corresponding member).

Definition at line 291 of file State.h.

Here is the caller graph for this function:

◆ variableBounds()

const VariableBoundsCond& smtrat::vs::State::variableBounds ( ) const

inline

Returns: A constant reference to the object managing and storing the variable's bounds which were extracted from the currently considered conditions of this state.

Definition at line 626 of file State.h.

Here is the caller graph for this function:

◆ variables()

void smtrat::vs::State::variables ( carl::Variables & _variables ) const

Finds the variables, which occur in this state.

Parameters

_variables The variables which occur in this state.

Definition at line 298 of file State.cpp.

Here is the call graph for this function:

◆ worstConstraintValuation()

void smtrat::vs::State::worstConstraintValuation ( const std::vector< std::pair< carl::Variable, std::multiset< double >>> & _varVals )

Definition at line 1379 of file State.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

Field Documentation

◆ mBackendCallValuation

size_t smtrat::vs::State::mBackendCallValuation

private

A heuristically determined value stating the expected difficulty of this state's considered conditions to be solved by a backend.

The higher this value, the easier it should be to solve this state's considered conditions.

Definition at line 116 of file State.h.

◆ mBestVarVals

std::vector<size_t> smtrat::vs::State::mBestVarVals

private

Definition at line 174 of file State.h.

◆ mCannotBeSolved

bool smtrat::vs::State::mCannotBeSolved

private

A flag indicating whether this state has been progressed until a point where a condition must be involved having a too high degree to tackle with virtual substitution.

Note, that this flag is also set to true if heuristics decide that the combinatorial blow up using virtual substitution for the considered list of conditions of this state is too high. If this flag is set to true, it the state is delayed until a point where only such state remain and a backend must be involved.

Definition at line 107 of file State.h.

◆ mCannotBeSolvedLazy

bool smtrat::vs::State::mCannotBeSolvedLazy

private

Definition at line 109 of file State.h.

◆ mConditionsSimplified

bool smtrat::vs::State::mConditionsSimplified

private

A flag indicating whether the conditions this state considers are simplified.

Definition at line 80 of file State.h.

◆ mCurrentIntRange

size_t smtrat::vs::State::mCurrentIntRange

private

Definition at line 166 of file State.h.

◆ mHasChildrenToInsert

bool smtrat::vs::State::mHasChildrenToInsert

private

A flag indicating whether there are states that are children of this state and must be still considered in the further progress of finding a solution.

Definition at line 83 of file State.h.

◆ mHasRecentlyAddedConditions

bool smtrat::vs::State::mHasRecentlyAddedConditions

private

A flag that indicates whether this state has conditions in its considered list of conditions, which were recently added and, hence, must be propagated further.

Definition at line 86 of file State.h.

◆ mID

size_t smtrat::vs::State::mID

private

A unique id identifying this state.

Definition at line 118 of file State.h.

◆ mInconsistent

bool smtrat::vs::State::mInconsistent

private

A flag that indicates whether this state is already inconsistent.

Note that if it is set to false, it does not necessarily mean that this state is consistent.

Definition at line 89 of file State.h.

◆ mIndex

carl::Variable smtrat::vs::State::mIndex

private

The variable which is going to be eliminated from this state's considered conditions.

That means, this variable won't occur in the children of this state.

Definition at line 130 of file State.h.

◆ mIntVarVals

std::vector<std::pair<carl::Variable,std::multiset<double> > > smtrat::vs::State::mIntVarVals

private

Definition at line 172 of file State.h.

◆ mMarkedAsDeleted

bool smtrat::vs::State::mMarkedAsDeleted

private

A flag indicating whether this state has already marked as deleted, which means that there is no need to consider it in the further progress of finding a solution.

Definition at line 92 of file State.h.

◆ mMaxIntTestCanidate

smtrat::Rational smtrat::vs::State::mMaxIntTestCanidate

private

Definition at line 164 of file State.h.

◆ mMinIntTestCanidate

smtrat::Rational smtrat::vs::State::mMinIntTestCanidate

private

Definition at line 162 of file State.h.

◆ mpChildren

std::list< State* >* smtrat::vs::State::mpChildren

private

The children states of this state.

For each test candidate we generate for the conditions this state considers such a child is created.

Definition at line 152 of file State.h.

◆ mpConditionIdAllocator

carl::IDPool* smtrat::vs::State::mpConditionIdAllocator

private

Definition at line 168 of file State.h.

◆ mpConditions

ConditionList* smtrat::vs::State::mpConditions

private

The currently considered conditions of this state, for which the satisfiability must be checked.

Definition at line 147 of file State.h.

◆ mpConflictSets

ConflictSets* smtrat::vs::State::mpConflictSets

private

Stores for each already considered and failed test candidate all conflicts which have been found for it.

Definition at line 149 of file State.h.

◆ mpFather

State* smtrat::vs::State::mpFather

private

The father state of this state.

Definition at line 137 of file State.h.

◆ mpInfinityChild

State* smtrat::vs::State::mpInfinityChild

private

Definition at line 160 of file State.h.

◆ mpOriginalCondition

const Condition* smtrat::vs::State::mpOriginalCondition

private

If the test candidate considered by this state stems from a condition for which it is enough to consider it only for test candidate generation for finding the satisfiability of the conditions it occurs in, this member stores that condition.

It is necessary, as it must be part of the origins (conditions in the father of this state) of any conflict found in this state.

Definition at line 135 of file State.h.

◆ mpSubResultCombination

SubResultCombination* smtrat::vs::State::mpSubResultCombination

private

The currently considered combination of conjunctions of constraints in the substitution result vector, which form the currently considered conditions of this state (store in mpConditions).

Definition at line 145 of file State.h.

◆ mpSubstitution

Substitution* smtrat::vs::State::mpSubstitution

private

The substitution this state considers. Note that it is NULL if this state is the root.

Definition at line 139 of file State.h.

◆ mpSubstitutionResults

SubstitutionResults* smtrat::vs::State::mpSubstitutionResults

private

The vector storing the substitution results, that is for each application of the substitution in this state to one of its considered conditions a disjunction of conjunctions of constraints.

Definition at line 142 of file State.h.

◆ mpTooHighDegreeConditions

carl::PointerSet<Condition>* smtrat::vs::State::mpTooHighDegreeConditions

private

The conditions of this state, which cannot be solved by the virtual substitution.

Definition at line 154 of file State.h.

◆ mpVariableBounds

VariableBoundsCond* smtrat::vs::State::mpVariableBounds

private

A pointer to an object which manages and stores the bounds on the variables occurring in this state.

These bounds are filtered from the conditions this state considers. Note that if we do not use optimizations based on variable bounds.

Definition at line 158 of file State.h.

◆ mRealVarVals

std::vector<std::pair<carl::Variable,std::multiset<double> > > smtrat::vs::State::mRealVarVals

private

Definition at line 170 of file State.h.

◆ mSubResultsSimplified

bool smtrat::vs::State::mSubResultsSimplified

private

A flag indicating whether the substitution results this state are simplified.

Definition at line 94 of file State.h.

◆ mTakeSubResultCombAgain

bool smtrat::vs::State::mTakeSubResultCombAgain

private

A flag indicating whether to take the current combination of substitution results once again.

Definition at line 97 of file State.h.

◆ mTestCandidateCheckedForBounds

bool smtrat::vs::State::mTestCandidateCheckedForBounds

private

A flag indicating whether the test candidate contained by this state has already been check for the bounds of the variables.

Definition at line 100 of file State.h.

◆ mTryToRefreshIndex

bool smtrat::vs::State::mTryToRefreshIndex

private

A flag indicating whether the index (the variable to eliminate in this state) should be reconsidered and maybe changed.

Definition at line 112 of file State.h.

◆ mType

Type smtrat::vs::State::mType

private

The type of this state, which states whether this state has still a substitution to apply or either test candidates shall be generated or a new combination of the substitution results must be found in order to consider it next.

Definition at line 127 of file State.h.

◆ mValuation

size_t smtrat::vs::State::mValuation

private

A heuristically determined value stating the expected difficulty of this state's considered conditions to be solved by virtual substitution.

The higher this value, the easier it should be to solve this state's considered conditions. Furthermore, this value enforces currently a depth first search, as a child has always a higher valuation than its father.

Definition at line 123 of file State.h.

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

smtrat-modules/VSModule/State.h
smtrat-modules/VSModule/State.cpp

Public Types

Public Member Functions

Static Public Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ ConflictSets

◆ SubResultCombination

◆ SubstitutionResult

◆ SubstitutionResults

◆ VariableBoundsCond

Member Enumeration Documentation

◆ Type

Constructor & Destructor Documentation

◆ State() [1/3]

◆ State() [2/3]

◆ State() [3/3]

◆ ~State()

Member Function Documentation

◆ addChild()

◆ addCondition()

◆ addConflicts()

◆ addConflictSet()

◆ addSubstitutionResults()

◆ allTestCandidatesInvalidated()

◆ averageConstraintValuation()

◆ backendCallValuation()

◆ bestCondition()

◆ bestConstraintValuation()

◆ cannotBeSolved()

◆ checkSubresultCombinations()

◆ checkTestCandidatesForBounds()

◆ children()

◆ conditions()

◆ conditionsSimplified()

◆ conflictSets()

◆ constraintExists()

◆ containsState()

◆ coveringSet()

◆ currentRangeSize()

◆ deleteConditions()

◆ deleteOrigins()

◆ deleteOriginsFromChildren()

◆ deleteOriginsFromConflictSets()

◆ deleteOriginsFromSubstitutionResults()

◆ extendSubResultCombination()

◆ father()

◆ getCurrentSubresultCombination()

◆ getNextIntTestCandidate()

◆ getNumberOfCurrentSubresultCombination()

◆ hasChildrenToInsert()

◆ hasChildWithID()

◆ hasFurtherUncheckedTestCandidates()

◆ hasInfinityChild()

◆ hasLocalConflict()

◆ hasNoninvolvedCondition()

◆ hasOnlyInconsistentChildren()

◆ hasRecentlyAddedConditions()

◆ hasRootsInVariableBounds()

◆ hasSubResultsCombination()

◆ hasSubstitutionResults()

◆ id()

◆ index()

◆ initConditionFlags()

◆ initIndex()

◆ isInconsistent()

◆ isRoot()

◆ markedAsDeleted()

◆ maxIntTestCandidate()

◆ minIntTestCandidate()

◆ nextSubResultCombination()

◆ numberOfNodes()

◆ occursInEquation()

◆ originalCondition()

◆ passConflictToFather()

◆ pFather()

◆ pOriginalCondition()

◆ print()

◆ printAlone()

◆ printConditions()