#include <Tableau.h>

Inheritance diagram for smtrat::lra::Tableau< Settings, T1, T2 >:

Collaboration diagram for smtrat::lra::Tableau< Settings, T1, T2 >:

[legend]

Data Structures
class	Iterator

struct	LearnedBound

Public Member Functions
	Tableau (ModuleInput::iterator _defaultBoundPosition)

	~Tableau ()

void	setSize (size_t _expectedHeight, size_t _expectedWidth, size_t _expectedNumberOfBounds)

size_t	size () const

void	setBlandsRuleStart (size_t _start)

const std::vector< Variable< T1, T2 > * > &	rows () const

const std::vector< Variable< T1, T2 > * > &	columns () const

const carl::FastMap< carl::Variable, Variable< T1, T2 > * > &	originalVars () const

const carl::FastPointerMap< typename Poly::PolyType, Variable< T1, T2 > * > &	slackVars () const

const T1 &	currentDelta () const

const carl::FastMap< FormulaT, std::vector< const Bound< T1, T2 > * > * > &	constraintToBound () const

carl::FastMap< FormulaT, std::vector< const Bound< T1, T2 > * > * > &	rConstraintToBound ()

size_t	numberOfPivotingSteps () const

void	resetNumberOfPivotingSteps ()

carl::FastPointerMap< Variable< T1, T2 >, LearnedBound > &	rLearnedLowerBounds ()

carl::FastPointerMap< Variable< T1, T2 >, LearnedBound > &	rLearnedUpperBounds ()

void	resetTheta ()

std::vector< typename carl::FastPointerMap< Variable< T1, T2 >, LearnedBound >::iterator > &	rNewLearnedBounds ()

bool	entryIsPositive (const TableauEntry< T1, T2 > &_entry) const

bool	entryIsNegative (const TableauEntry< T1, T2 > &_entry) const

auto	defaultBoundPosition () const

bool	isActive (const Variable< T1, T2 > &_var) const

EntryID	newTableauEntry (const T2 &_content)

void	removeEntry (EntryID _entryID)

Variable< T1, T2 > *	getVariable (const Poly &_lhs, T1 &_factor, T1 &_boundValue)

Variable< T1, T2 > *	getObjectiveVariable (const Poly &_lhs)

std::pair< const Bound< T1, T2 > *, bool >	newBound (const FormulaT &_constraint)

void	removeBound (const FormulaT &_constraint)

void	activateBound (const Bound< T1, T2 > *_bound, const FormulaT &_formula)

void	deleteVariable (Variable< T1, T2 > *_variable, bool _optimizationVar=false)

Variable< T1, T2 > *	newNonbasicVariable (const typename Poly::PolyType *_poly, bool _isInteger)

Variable< T1, T2 > *	newBasicVariable (const typename Poly::PolyType *_poly, bool _isInteger)

void	activateBasicVar (Variable< T1, T2 > *_var)
	g More...

void	deactivateBasicVar (Variable< T1, T2 > *_var)

void	storeAssignment ()

void	resetAssignment ()

RationalAssignment	getRationalAssignment () const

void	adaptDelta (const Variable< T1, T2 > &_variable, bool _upperBound, T1 &_minDelta) const

void	compressRows ()

bool	usedBlandsRule ()
	Returns true, if the next pivoting element is selected by blands rule. More...

bool	hasMultilineConflict ()

std::vector< const Bound< T1, T2 > * >	getMultilineConflict ()

std::pair< EntryID, bool >	nextPivotingElement ()

Value< T1 >	violationSum ()
	Method to compute the sum of derivations to the closest bounds. More...

Value< T1 >	dViolationSum (const Variable< T1, T2 > *nVar, const Value< T1 > &update)
	Computes the change in the violation sum when an the update value is added to the assignment of the nonbassi variable nVar. More...

Value< T1 >	get_dVioSum ()
	Used as assertion-function to check the progress of the tableau. More...

std::map< Value< T1 >, Value< T1 > >	compute_dVio (const std::vector< std::pair< Value< T1 >, Variable< T1, T2 > * > > &candidates, const Variable< T1, T2 > &nVar, bool positive)
	Updated Method to computed dVio more efficienlty. More...

std::pair< EntryID, bool >	nextPivotingElementInfeasibilities ()
	Method for next pivoting element according to "Simplex with Sum of Infeasibilities for SMT" by Tim King and Clark Barrett. More...

void	computeLeavingCandidates (const std::size_t i, std::vector< std::pair< Value< T1 >, Variable< T1, T2 > * > > &leaving_candidates)
	Helper method to compute leavind candidates used in nextPivotingElementInfeasibilities. More...

void	updateNonbasicVariable (EntryID _pivotingElement)
	Updates a nonbasic variable by the assignment stored in mpTheta and triggers updates of depending basic variables. More...

void	updateNonbasicVariable (EntryID _pivotingElement, Value< T1 > update)
	Updates a nonbasic variable by the given assignment and triggers updates of depending basic variables. More...

std::pair< EntryID, bool >	hasConflict ()
	Checks if a conflicting pair exists. More...

void	printEntries ()

std::vector< T2 >	getInfeasibilityRow ()
	Method to compute the infeasibility row to the current tableau. More...

void	setInfeasibilityRow ()
	Method to set the initital infeasibility row to avoid recomputation in every round. More...

std::pair< EntryID, bool >	optimizeIndependentNonbasics (const Variable< T1, T2 > &_objective)

std::pair< EntryID, bool >	nextPivotingElementForOptimizing (const Variable< T1, T2 > &_objective)

std::pair< EntryID, bool >	nextZeroPivotingElementForOptimizing (const Variable< T1, T2 > &_objective) const

EntryID	isSuitable (const Variable< T1, T2 > &_basicVar, bool _forIncreasingAssignment) const

EntryID	isSuitableConflictDetection (const Variable< T1, T2 > &_basicVar, bool _forIncreasingAssignment) const
	Checks if the basic variable is pivotable. More...

bool	betterEntry (EntryID _isBetter, EntryID _than) const

std::vector< const Bound< T1, T2 > * >	getConflict (EntryID _rowEntry) const

std::vector< std::vector< const Bound< T1, T2 > * > >	getConflictsFrom (EntryID _rowEntry) const

void	updateBasicAssignments (size_t _column, const Value< T1 > &_change)

Variable< T1, T2 > *	pivot (EntryID _pivotingElement, bool _optimizing=false)

void	update (bool _downwards, EntryID _pivotingElement, std::vector< Iterator > &_pivotingRowLeftSide, std::vector< Iterator > &_pivotingRowRightSide, bool _optimizing=false)
	Updates the tableau according to the new values in the pivoting row containing the given pivoting element. More...

void	addToEntry (const T2 &_toAdd, Iterator &_horiIter, bool _horiIterLeftFromVertIter, Iterator &_vertIter, bool _vertIterBelowHoriIter)
	Adds the given value to the entry being at the position (i,j), where i is the vertical position of the given horizontal iterator and j is the horizontal position of the given vertical iterator. More...

void	rowRefinement (Variable< T1, T2 > *_basicVar)
	Tries to refine the supremum and infimum of the given basic variable. More...

size_t	boundedVariables (const Variable< T1, T2 > &_var, size_t _stopCriterium=0) const

size_t	unboundedVariables (const Variable< T1, T2 > &_var, size_t _stopCriterium=0) const

size_t	checkCorrectness () const

bool	rowCorrect (size_t _rowNumber) const

bool	isConflicting () const

const Poly::PolyType *	gomoryCut (const T2 &_ass, Variable< T1, T2 > *_rowVar)
	Creates a constraint referring to Gomory Cuts, if possible. More...

size_t	getNumberOfEntries (Variable< T1, T2 > *_rowVar)

void	collect_premises (const Variable< T1, T2 > *_rowVar, FormulasT &premises) const
	Collects the premises for branch and bound and stores them in premises. More...

void	printHeap (std::ostream &_out=std::cout, int _maxEntryLength=30, const std::string _init="") const

void	printEntry (EntryID _entry, std::ostream &_out=std::cout, int _maxEntryLength=20) const

void	printVariables (bool _allBounds=true, std::ostream &_out=std::cout, const std::string _init="") const

void	printLearnedBounds (const std::string _init="", std::ostream &_out=std::cout) const

void	printLearnedBound (const Variable< T1, T2 > &_var, const LearnedBound &_learnedBound, const std::string _init="", std::ostream &_out=std::cout) const

void	print (EntryID _pivotingElement=LAST_ENTRY_ID, std::ostream &_out=std::cout, const std::string _init="", bool _friendlyNames=true, bool _withZeroColumns=false) const

Private Attributes
bool	mRowsCompressed

size_t	mWidth

size_t	mPivotingSteps

size_t	mMaxPivotsWithoutBlandsRule

size_t	mVarIDCounter

ModuleInput::iterator	mDefaultBoundPosition

std::stack< EntryID >	mUnusedIDs

carl::IDPool	mVariableIdAllocator
	Id allocator for the variables. More...

std::vector< Variable< T1, T2 > * >	mRows

std::vector< Variable< T1, T2 > * >	mColumns

std::list< std::list< std::pair< Variable< T1, T2 > *, T2 > > >	mNonActiveBasics

std::vector< TableauEntry< T1, T2 > > *	mpEntries

std::vector< Variable< T1, T2 > * >	mConflictingRows

Value< T1 > *	mpTheta

bool	onlyUpdate = false

T1	mCurDelta

carl::FastMap< carl::Variable, Variable< T1, T2 > * >	mOriginalVars

carl::FastPointerMap< typename Poly::PolyType, Variable< T1, T2 > * >	mSlackVars

carl::FastMap< FormulaT, std::vector< const Bound< T1, T2 > * > * >	mConstraintToBound

carl::FastPointerMap< Variable< T1, T2 >, LearnedBound >	mLearnedLowerBounds

carl::FastPointerMap< Variable< T1, T2 >, LearnedBound >	mLearnedUpperBounds

std::vector< typename carl::FastPointerMap< Variable< T1, T2 >, LearnedBound >::iterator >	mNewLearnedBounds

Value< T1 >	mOldVioSum = Value<T1>(-1)

Value< T1 >	mOld_dVioSum = Value<T1>(1)

std::vector< T2 >	mInfeasibilityRow

std::size_t	mFullCandidateSearch = 3

Detailed Description

template<class Settings, typename T1, typename T2>
class smtrat::lra::Tableau< Settings, T1, T2 >

Definition at line 205 of file Tableau.h.

Constructor & Destructor Documentation

◆ Tableau()

template<class Settings , typename T1 , typename T2 >

smtrat::lra::Tableau< Settings, T1, T2 >::Tableau ( ModuleInput::iterator _defaultBoundPosition )

Parameters

_defaultBoundPosition

◆ ~Tableau()

template<class Settings , typename T1 , typename T2 >

smtrat::lra::Tableau< Settings, T1, T2 >::~Tableau ( )

Member Function Documentation

◆ activateBasicVar()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::activateBasicVar ( Variable< T1, T2 > * _var )

g

Parameters

_var

◆ activateBound()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::activateBound	(	const Bound< T1, T2 > *	_bound,
		const FormulaT &	_formula
	)

Parameters

_bound
_formula

◆ adaptDelta()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::adaptDelta	(	const Variable< T1, T2 > &	_variable,
		bool	_upperBound,
		T1 &	_minDelta
	)		const

◆ addToEntry()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::addToEntry	(	const T2 &	_toAdd,
		Iterator &	_horiIter,
		bool	_horiIterLeftFromVertIter,
		Iterator &	_vertIter,
		bool	_vertIterBelowHoriIter
	)

Adds the given value to the entry being at the position (i,j), where i is the vertical position of the given horizontal iterator and j is the horizontal position of the given vertical iterator.

Note, that the entry might not exist, if its current value is 0. Then the horizontal iterator is located horizontally before or after the entry to change and the vertical iterator is located vertically before or after the entry to add.

Parameters

_toAdd	The value to add to the content of the entry specified by the given iterators and their relative position to each other.
_horiIter	The iterator moving horizontally and, hence, giving the vertical position of the entry to add the given value to.
_horiIterLeftFromVertIter	true, if the horizontally moving iterator is left from or equal to the horizontal position of the iterator moving vertically, and, hence, left from or equal to the position of the entry to add the given value to; false, it is right or equal to this position.
_vertIter	The iterator moving vertically and, hence, giving the horizontal position of the entry to add the given value to.
_vertIterBelowHoriIter	true, if the vertically moving iterator is below or exactly at the vertical position of the iterator moving horizontally, and, hence, below or exactly at the position of the entry to add the given value to; false, it is above or equal to this position. @sideeffect If the entry existed (!=0) and is removed because of becoming 0, the iterators are set according to the given relative positioning.

◆ betterEntry()

template<class Settings , typename T1 , typename T2 >

bool smtrat::lra::Tableau< Settings, T1, T2 >::betterEntry	(	EntryID	_isBetter,
		EntryID	_than
	)		const

Parameters

_isBetter
_than

Returns

◆ boundedVariables()

template<class Settings , typename T1 , typename T2 >

size_t smtrat::lra::Tableau< Settings, T1, T2 >::boundedVariables	(	const Variable< T1, T2 > &	_var,
		size_t	_stopCriterium = `0`
	)		const

Parameters

_var
_stopCriterium

Returns

◆ checkCorrectness()

template<class Settings , typename T1 , typename T2 >

size_t smtrat::lra::Tableau< Settings, T1, T2 >::checkCorrectness ( ) const

Returns

◆ collect_premises()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::collect_premises	(	const Variable< T1, T2 > *	_rowVar,
		FormulasT &	premises
	)		const

Collects the premises for branch and bound and stores them in premises.

Parameters

_rowVar
premises

◆ columns()

template<class Settings , typename T1 , typename T2 >

const std::vector<Variable<T1, T2>*>& smtrat::lra::Tableau< Settings, T1, T2 >::columns ( ) const

inline

Returns

Definition at line 465 of file Tableau.h.

◆ compressRows()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::compressRows ( )

◆ compute_dVio()

template<class Settings , typename T1 , typename T2 >

std::map<Value<T1>, Value<T1> > smtrat::lra::Tableau< Settings, T1, T2 >::compute_dVio	(	const std::vector< std::pair< Value< T1 >, Variable< T1, T2 > * > > &	candidates,
		const Variable< T1, T2 > &	nVar,
		bool	positive
	)

Updated Method to computed dVio more efficienlty.

For this the fact is used, that VioSum is piecewise linear (the proof can be found in the SoI paper).

Parameters

candidates	Update candidates, IMPORTANT: Must be sorted with an stabloe sorting algorithm
nVar	The updated nonbasic variable
positive	Whether the positve or negative update values are checked

◆ computeLeavingCandidates()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::computeLeavingCandidates	(	const std::size_t	i,
		std::vector< std::pair< Value< T1 >, Variable< T1, T2 > * > > &	leaving_candidates
	)

Helper method to compute leavind candidates used in nextPivotingElementInfeasibilities.

Computes for every non-basic variable the breaking points. Updates from non-basic vars of 0 are omitted to prevent loops.

Parameters

i	: Index if entering (nonbasic ) variable.
leaving_candidates	: Used as storage object for update candidates.

◆ constraintToBound()

template<class Settings , typename T1 , typename T2 >

const carl::FastMap<FormulaT, std::vector<const Bound<T1, T2>*>*>& smtrat::lra::Tableau< Settings, T1, T2 >::constraintToBound ( ) const

inline

Returns

Definition at line 494 of file Tableau.h.

Here is the caller graph for this function:

◆ currentDelta()

template<class Settings , typename T1 , typename T2 >

const T1& smtrat::lra::Tableau< Settings, T1, T2 >::currentDelta ( ) const

inline

Definition at line 486 of file Tableau.h.

◆ deactivateBasicVar()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::deactivateBasicVar ( Variable< T1, T2 > * _var )

Parameters

_var

◆ defaultBoundPosition()

template<class Settings , typename T1 , typename T2 >

auto smtrat::lra::Tableau< Settings, T1, T2 >::defaultBoundPosition ( ) const

inline

Returns

Definition at line 577 of file Tableau.h.

◆ deleteVariable()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::deleteVariable	(	Variable< T1, T2 > *	_variable,
		bool	_optimizationVar = `false`
	)

Parameters

_variable

◆ dViolationSum()

template<class Settings , typename T1 , typename T2 >

Value<T1> smtrat::lra::Tableau< Settings, T1, T2 >::dViolationSum	(	const Variable< T1, T2 > *	nVar,
		const Value< T1 > &	update
	)

Computes the change in the violation sum when an the update value is added to the assignment of the nonbassi variable nVar.

Parameters

nVar	variable to be updated
update	Update value

◆ entryIsNegative()

template<class Settings , typename T1 , typename T2 >

bool smtrat::lra::Tableau< Settings, T1, T2 >::entryIsNegative ( const TableauEntry< T1, T2 > & _entry ) const

inline

Definition at line 563 of file Tableau.h.

Here is the call graph for this function:

◆ entryIsPositive()

template<class Settings , typename T1 , typename T2 >

bool smtrat::lra::Tableau< Settings, T1, T2 >::entryIsPositive ( const TableauEntry< T1, T2 > & _entry ) const

inline

Definition at line 552 of file Tableau.h.

Here is the call graph for this function:

◆ get_dVioSum()

template<class Settings , typename T1 , typename T2 >

Value<T1> smtrat::lra::Tableau< Settings, T1, T2 >::get_dVioSum ( )

inline

Used as assertion-function to check the progress of the tableau.

Definition at line 715 of file Tableau.h.

◆ getConflict()

template<class Settings , typename T1 , typename T2 >

std::vector< const Bound<T1, T2>* > smtrat::lra::Tableau< Settings, T1, T2 >::getConflict ( EntryID _rowEntry ) const

Parameters

_rowEntry

Returns

◆ getConflictsFrom()

template<class Settings , typename T1 , typename T2 >

std::vector< std::vector< const Bound<T1, T2>* > > smtrat::lra::Tableau< Settings, T1, T2 >::getConflictsFrom ( EntryID _rowEntry ) const

Parameters

_rowEntry

Returns

◆ getInfeasibilityRow()

template<class Settings , typename T1 , typename T2 >

std::vector<T2> smtrat::lra::Tableau< Settings, T1, T2 >::getInfeasibilityRow ( )

Method to compute the infeasibility row to the current tableau.

◆ getMultilineConflict()

template<class Settings , typename T1 , typename T2 >

std::vector< const Bound<T1, T2>* > smtrat::lra::Tableau< Settings, T1, T2 >::getMultilineConflict ( )

Returns: In SUM-Simplex a conflict is possibly created with multiple rows. This function returns the single conflict if possible and otherwise construct the multiline conflict.

◆ getNumberOfEntries()

template<class Settings , typename T1 , typename T2 >

size_t smtrat::lra::Tableau< Settings, T1, T2 >::getNumberOfEntries ( Variable< T1, T2 > * _rowVar )

Parameters

_rowVar

Returns: number of entries in the row belonging to _rowVar

◆ getObjectiveVariable()

template<class Settings , typename T1 , typename T2 >

Variable<T1,T2>* smtrat::lra::Tableau< Settings, T1, T2 >::getObjectiveVariable ( const Poly & _lhs )

◆ getRationalAssignment()

template<class Settings , typename T1 , typename T2 >

RationalAssignment smtrat::lra::Tableau< Settings, T1, T2 >::getRationalAssignment ( ) const

Returns

◆ getVariable()

template<class Settings , typename T1 , typename T2 >

Variable<T1,T2>* smtrat::lra::Tableau< Settings, T1, T2 >::getVariable	(	const Poly &	_lhs,
		T1 &	_factor,
		T1 &	_boundValue
	)

◆ gomoryCut()

template<class Settings , typename T1 , typename T2 >

const Poly::PolyType* smtrat::lra::Tableau< Settings, T1, T2 >::gomoryCut	(	const T2 &	_ass,
		Variable< T1, T2 > *	_rowVar
	)

Creates a constraint referring to Gomory Cuts, if possible.

Parameters

_ass
_rowVar

Returns: NULL, if the cut can´t be constructed; otherwise the valid constraint is returned.

◆ hasConflict()

template<class Settings , typename T1 , typename T2 >

std::pair<EntryID,bool> smtrat::lra::Tableau< Settings, T1, T2 >::hasConflict ( )

Checks if a conflicting pair exists.

In a conflict is found, the cell and false is returned. If not, LAST_ENTRY_ID and true is returned.

◆ hasMultilineConflict()

template<class Settings , typename T1 , typename T2 >

bool smtrat::lra::Tableau< Settings, T1, T2 >::hasMultilineConflict ( )

Returns: In SUM-Simplex a conflict is possibly created with multiple rows. This function returns true iff the multi-conflict settings occured.

◆ isActive()

template<class Settings , typename T1 , typename T2 >

bool smtrat::lra::Tableau< Settings, T1, T2 >::isActive ( const Variable< T1, T2 > & _var ) const

inline

Definition at line 582 of file Tableau.h.

Here is the call graph for this function:

◆ isConflicting()

template<class Settings , typename T1 , typename T2 >

bool smtrat::lra::Tableau< Settings, T1, T2 >::isConflicting ( ) const

◆ isSuitable()

template<class Settings , typename T1 , typename T2 >

EntryID smtrat::lra::Tableau< Settings, T1, T2 >::isSuitable	(	const Variable< T1, T2 > &	_basicVar,
		bool	_forIncreasingAssignment
	)		const

Parameters

_basicVar
_forIncreasingAssignment

Returns

◆ isSuitableConflictDetection()

template<class Settings , typename T1 , typename T2 >

EntryID smtrat::lra::Tableau< Settings, T1, T2 >::isSuitableConflictDetection	(	const Variable< T1, T2 > &	_basicVar,
		bool	_forIncreasingAssignment
	)		const

Checks if the basic variable is pivotable.

Returns LAST_ENTRY_ID as EntryID if a conflict was found. In difference to isSuitable returns this function an EntryID as soon as the EntryID bestEntry is unequal to LAST_ENTRY_ID. The assertions are still checked.

Parameters

_basicVar
_forIncreasingAssignment

Returns

◆ newBasicVariable()

template<class Settings , typename T1 , typename T2 >

Variable<T1, T2>* smtrat::lra::Tableau< Settings, T1, T2 >::newBasicVariable	(	const typename Poly::PolyType *	_poly,
		bool	_isInteger
	)

Parameters

_poly
_originalVars
_isInteger

Returns

◆ newBound()

template<class Settings , typename T1 , typename T2 >

std::pair<const Bound<T1,T2>*, bool> smtrat::lra::Tableau< Settings, T1, T2 >::newBound ( const FormulaT & _constraint )

Parameters

_constraint

Returns

◆ newNonbasicVariable()

template<class Settings , typename T1 , typename T2 >

Variable<T1, T2>* smtrat::lra::Tableau< Settings, T1, T2 >::newNonbasicVariable	(	const typename Poly::PolyType *	_poly,
		bool	_isInteger
	)

Parameters

_poly
_isInteger

Returns

◆ newTableauEntry()

template<class Settings , typename T1 , typename T2 >

EntryID smtrat::lra::Tableau< Settings, T1, T2 >::newTableauEntry ( const T2 & _content )

Parameters

_content

Returns

◆ nextPivotingElement()

template<class Settings , typename T1 , typename T2 >

std::pair<EntryID, bool> smtrat::lra::Tableau< Settings, T1, T2 >::nextPivotingElement ( )

Returns

◆ nextPivotingElementForOptimizing()

template<class Settings , typename T1 , typename T2 >

std::pair<EntryID,bool> smtrat::lra::Tableau< Settings, T1, T2 >::nextPivotingElementForOptimizing ( const Variable< T1, T2 > & _objective )

Returns

◆ nextPivotingElementInfeasibilities()

template<class Settings , typename T1 , typename T2 >

std::pair<EntryID, bool> smtrat::lra::Tableau< Settings, T1, T2 >::nextPivotingElementInfeasibilities ( )

Method for next pivoting element according to "Simplex with Sum of Infeasibilities for SMT" by Tim King and Clark Barrett.

Herefore, one counts the vialation of every bound and searches for elements who minimize the violation sum of the next iteration.

Returns

◆ nextZeroPivotingElementForOptimizing()

template<class Settings , typename T1 , typename T2 >

std::pair<EntryID,bool> smtrat::lra::Tableau< Settings, T1, T2 >::nextZeroPivotingElementForOptimizing ( const Variable< T1, T2 > & _objective ) const

◆ numberOfPivotingSteps()

template<class Settings , typename T1 , typename T2 >

size_t smtrat::lra::Tableau< Settings, T1, T2 >::numberOfPivotingSteps ( ) const

inline

Returns

Definition at line 510 of file Tableau.h.

◆ optimizeIndependentNonbasics()

template<class Settings , typename T1 , typename T2 >

std::pair<EntryID,bool> smtrat::lra::Tableau< Settings, T1, T2 >::optimizeIndependentNonbasics ( const Variable< T1, T2 > & _objective )

Parameters

_objective

Returns

◆ originalVars()

template<class Settings , typename T1 , typename T2 >

const carl::FastMap< carl::Variable, Variable<T1,T2>*>& smtrat::lra::Tableau< Settings, T1, T2 >::originalVars ( ) const

inline

Returns

Definition at line 473 of file Tableau.h.

Here is the caller graph for this function:

◆ pivot()

template<class Settings , typename T1 , typename T2 >

Variable<T1, T2>* smtrat::lra::Tableau< Settings, T1, T2 >::pivot	(	EntryID	_pivotingElement,
		bool	_optimizing = `false`
	)

Parameters

_pivotingElement
updateAssignments

Returns

◆ print()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::print	(	EntryID	_pivotingElement = `LAST_ENTRY_ID`,
		std::ostream &	_out = `std::cout`,
		const std::string	_init = `""`,
		bool	_friendlyNames = `true`,
		bool	_withZeroColumns = `false`
	)		const

Parameters

_pivotingElement
_out
_init
_friendlyNames
_withZeroColumns

◆ printEntries()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::printEntries ( )

inline

Definition at line 761 of file Tableau.h.

◆ printEntry()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::printEntry	(	EntryID	_entry,
		std::ostream &	_out = `std::cout`,
		int	_maxEntryLength = `20`
	)		const

Parameters

_entry
_out
_maxEntryLength

◆ printHeap()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::printHeap	(	std::ostream &	_out = `std::cout`,
		int	_maxEntryLength = `30`,
		const std::string	_init = `""`
	)		const

Parameters

_out
_maxEntryLength
_init

◆ printLearnedBound()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::printLearnedBound	(	const Variable< T1, T2 > &	_var,
		const LearnedBound &	_learnedBound,
		const std::string	_init = `""`,
		std::ostream &	_out = `std::cout`
	)		const

Parameters

_var
_learnedBound
_init
_out

◆ printLearnedBounds()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::printLearnedBounds	(	const std::string	_init = `""`,
		std::ostream &	_out = `std::cout`
	)		const

Parameters

_init
_out

◆ printVariables()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::printVariables	(	bool	_allBounds = `true`,
		std::ostream &	_out = `std::cout`,
		const std::string	_init = `""`
	)		const

Parameters

_allBounds
_out
_init

◆ rConstraintToBound()

template<class Settings , typename T1 , typename T2 >

carl::FastMap<FormulaT, std::vector<const Bound<T1, T2>*>*>& smtrat::lra::Tableau< Settings, T1, T2 >::rConstraintToBound ( )

inline

Returns

Definition at line 502 of file Tableau.h.

◆ removeBound()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::removeBound ( const FormulaT & _constraint )

◆ removeEntry()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::removeEntry ( EntryID _entryID )

Parameters

_entryID

◆ resetAssignment()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::resetAssignment ( )

◆ resetNumberOfPivotingSteps()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::resetNumberOfPivotingSteps ( )

inline

Definition at line 518 of file Tableau.h.

◆ resetTheta()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::resetTheta ( )

inline

Definition at line 539 of file Tableau.h.

◆ rLearnedLowerBounds()

template<class Settings , typename T1 , typename T2 >

carl::FastPointerMap<Variable<T1,T2>, LearnedBound>& smtrat::lra::Tableau< Settings, T1, T2 >::rLearnedLowerBounds ( )

inline

Returns

Definition at line 526 of file Tableau.h.

◆ rLearnedUpperBounds()

template<class Settings , typename T1 , typename T2 >

carl::FastPointerMap<Variable<T1,T2>, LearnedBound>& smtrat::lra::Tableau< Settings, T1, T2 >::rLearnedUpperBounds ( )

inline

Returns

Definition at line 534 of file Tableau.h.

◆ rNewLearnedBounds()

template<class Settings , typename T1 , typename T2 >

std::vector<typename carl::FastPointerMap<Variable<T1,T2>, LearnedBound>::iterator>& smtrat::lra::Tableau< Settings, T1, T2 >::rNewLearnedBounds ( )

inline

Returns

Definition at line 547 of file Tableau.h.

◆ rowCorrect()

template<class Settings , typename T1 , typename T2 >

bool smtrat::lra::Tableau< Settings, T1, T2 >::rowCorrect ( size_t _rowNumber ) const

Parameters

_rowNumber

Returns

◆ rowRefinement()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::rowRefinement ( Variable< T1, T2 > * _basicVar )

Tries to refine the supremum and infimum of the given basic variable.

Parameters

_basicVar The basic variable for which to refine the supremum and infimum.

◆ rows()

template<class Settings , typename T1 , typename T2 >

const std::vector<Variable<T1, T2>*>& smtrat::lra::Tableau< Settings, T1, T2 >::rows ( ) const

inline

Returns

Definition at line 457 of file Tableau.h.

◆ setBlandsRuleStart()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::setBlandsRuleStart ( size_t _start )

inline

Definition at line 449 of file Tableau.h.

◆ setInfeasibilityRow()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::setInfeasibilityRow ( )

Method to set the initital infeasibility row to avoid recomputation in every round.

◆ setSize()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::setSize	(	size_t	_expectedHeight,
		size_t	_expectedWidth,
		size_t	_expectedNumberOfBounds
	)

inline

Parameters

_expectedHeight
_expectedWidth
_expectedNumberOfBounds

Definition at line 431 of file Tableau.h.

◆ size()

template<class Settings , typename T1 , typename T2 >

size_t smtrat::lra::Tableau< Settings, T1, T2 >::size ( ) const

inline

Returns

Definition at line 441 of file Tableau.h.

◆ slackVars()

template<class Settings , typename T1 , typename T2 >

const carl::FastPointerMap<typename Poly::PolyType, Variable<T1,T2>*>& smtrat::lra::Tableau< Settings, T1, T2 >::slackVars ( ) const

inline

Returns

Definition at line 481 of file Tableau.h.

Here is the caller graph for this function:

◆ storeAssignment()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::storeAssignment ( )

◆ unboundedVariables()

template<class Settings , typename T1 , typename T2 >

size_t smtrat::lra::Tableau< Settings, T1, T2 >::unboundedVariables	(	const Variable< T1, T2 > &	_var,
		size_t	_stopCriterium = `0`
	)		const

Parameters

_var
_stopCriterium

Returns

◆ update()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::update	(	bool	_downwards,
		EntryID	_pivotingElement,
		std::vector< Iterator > &	_pivotingRowLeftSide,
		std::vector< Iterator > &	_pivotingRowRightSide,
		bool	_optimizing = `false`
	)

Updates the tableau according to the new values in the pivoting row containing the given pivoting element.

The updating is applied from the pivoting row downwards, if the given flag _downwards is true, and upwards, otherwise.

Parameters

_downwards	The flag indicating whether to update the tableau downwards or upwards starting from the pivoting row.
_pivotingElement	The id of the current pivoting element.
_pivotingRowLeftSide	For every element in the pivoting row, which is positioned left of the pivoting element, this vector contains an iterator. The closer the element is to the pivoting element, the smaller is the iterator's index in the vector.
_pivotingRowRightSide	For every element in the pivoting row, which is positioned right of the pivoting element, this vector contains an iterator. The closer the element is to the pivoting element, the smaller is the iterator's index in the vector.
_updateAssignments	If true, the assignments of all variables will be updated after pivoting.

◆ updateBasicAssignments()

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::updateBasicAssignments	(	size_t	_column,
		const Value< T1 > &	_change
	)

Parameters

_column
_change

◆ updateNonbasicVariable() [1/2]

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::updateNonbasicVariable ( EntryID _pivotingElement )

Updates a nonbasic variable by the assignment stored in mpTheta and triggers updates of depending basic variables.

Parameters

_pivotingElement Element in the row of the nonbasic variable

◆ updateNonbasicVariable() [2/2]

template<class Settings , typename T1 , typename T2 >

void smtrat::lra::Tableau< Settings, T1, T2 >::updateNonbasicVariable	(	EntryID	_pivotingElement,
		Value< T1 >	update
	)

Updates a nonbasic variable by the given assignment and triggers updates of depending basic variables.

Parameters

_pivotingElement	Element in the row of the nonbasic variable
update	Update Value of non-basic var

◆ usedBlandsRule()

template<class Settings , typename T1 , typename T2 >

bool smtrat::lra::Tableau< Settings, T1, T2 >::usedBlandsRule ( )

Returns true, if the next pivoting element is selected by blands rule.

◆ violationSum()

template<class Settings , typename T1 , typename T2 >

Value<T1> smtrat::lra::Tableau< Settings, T1, T2 >::violationSum ( )

Method to compute the sum of derivations to the closest bounds.

Field Documentation

◆ mColumns

template<class Settings , typename T1 , typename T2 >

std::vector<Variable<T1,T2>*> smtrat::lra::Tableau< Settings, T1, T2 >::mColumns

private

Definition at line 259 of file Tableau.h.

◆ mConflictingRows

template<class Settings , typename T1 , typename T2 >

std::vector<Variable<T1,T2>*> smtrat::lra::Tableau< Settings, T1, T2 >::mConflictingRows

private

Definition at line 265 of file Tableau.h.

◆ mConstraintToBound

template<class Settings , typename T1 , typename T2 >

carl::FastMap<FormulaT, std::vector<const Bound<T1, T2>*>*> smtrat::lra::Tableau< Settings, T1, T2 >::mConstraintToBound

private

Definition at line 277 of file Tableau.h.

◆ mCurDelta

template<class Settings , typename T1 , typename T2 >

T1 smtrat::lra::Tableau< Settings, T1, T2 >::mCurDelta

mutableprivate

Definition at line 271 of file Tableau.h.

◆ mDefaultBoundPosition

template<class Settings , typename T1 , typename T2 >

ModuleInput::iterator smtrat::lra::Tableau< Settings, T1, T2 >::mDefaultBoundPosition

private

Definition at line 251 of file Tableau.h.

◆ mFullCandidateSearch

template<class Settings , typename T1 , typename T2 >

std::size_t smtrat::lra::Tableau< Settings, T1, T2 >::mFullCandidateSearch = 3

private

Definition at line 293 of file Tableau.h.

◆ mInfeasibilityRow

template<class Settings , typename T1 , typename T2 >

std::vector<T2> smtrat::lra::Tableau< Settings, T1, T2 >::mInfeasibilityRow

private

Definition at line 290 of file Tableau.h.

◆ mLearnedLowerBounds

template<class Settings , typename T1 , typename T2 >

carl::FastPointerMap<Variable<T1,T2>, LearnedBound> smtrat::lra::Tableau< Settings, T1, T2 >::mLearnedLowerBounds

private

Definition at line 279 of file Tableau.h.

◆ mLearnedUpperBounds

template<class Settings , typename T1 , typename T2 >

carl::FastPointerMap<Variable<T1,T2>, LearnedBound> smtrat::lra::Tableau< Settings, T1, T2 >::mLearnedUpperBounds

private

Definition at line 281 of file Tableau.h.

◆ mMaxPivotsWithoutBlandsRule

template<class Settings , typename T1 , typename T2 >

size_t smtrat::lra::Tableau< Settings, T1, T2 >::mMaxPivotsWithoutBlandsRule

private

Definition at line 247 of file Tableau.h.

◆ mNewLearnedBounds

template<class Settings , typename T1 , typename T2 >

std::vector<typename carl::FastPointerMap<Variable<T1,T2>, LearnedBound>::iterator> smtrat::lra::Tableau< Settings, T1, T2 >::mNewLearnedBounds

private

Definition at line 283 of file Tableau.h.

◆ mNonActiveBasics

template<class Settings , typename T1 , typename T2 >

std::list<std::list<std::pair<Variable<T1,T2>*,T2> > > smtrat::lra::Tableau< Settings, T1, T2 >::mNonActiveBasics

private

Definition at line 261 of file Tableau.h.

◆ mOld_dVioSum

template<class Settings , typename T1 , typename T2 >

Value<T1> smtrat::lra::Tableau< Settings, T1, T2 >::mOld_dVioSum = Value<T1>(1)

private

Definition at line 287 of file Tableau.h.

◆ mOldVioSum

template<class Settings , typename T1 , typename T2 >

Value<T1> smtrat::lra::Tableau< Settings, T1, T2 >::mOldVioSum = Value<T1>(-1)

private

Definition at line 286 of file Tableau.h.

◆ mOriginalVars

template<class Settings , typename T1 , typename T2 >

carl::FastMap<carl::Variable, Variable<T1,T2>*> smtrat::lra::Tableau< Settings, T1, T2 >::mOriginalVars

private

Definition at line 273 of file Tableau.h.

◆ mpEntries

template<class Settings , typename T1 , typename T2 >

std::vector<TableauEntry<T1,T2> >* smtrat::lra::Tableau< Settings, T1, T2 >::mpEntries

private

Definition at line 263 of file Tableau.h.

◆ mPivotingSteps

template<class Settings , typename T1 , typename T2 >

size_t smtrat::lra::Tableau< Settings, T1, T2 >::mPivotingSteps

private

Definition at line 245 of file Tableau.h.

◆ mpTheta

template<class Settings , typename T1 , typename T2 >

Value<T1>* smtrat::lra::Tableau< Settings, T1, T2 >::mpTheta

private

Definition at line 267 of file Tableau.h.

◆ mRows

template<class Settings , typename T1 , typename T2 >

std::vector<Variable<T1,T2>*> smtrat::lra::Tableau< Settings, T1, T2 >::mRows

private

Definition at line 257 of file Tableau.h.

◆ mRowsCompressed

template<class Settings , typename T1 , typename T2 >

bool smtrat::lra::Tableau< Settings, T1, T2 >::mRowsCompressed

private

Definition at line 241 of file Tableau.h.

◆ mSlackVars

template<class Settings , typename T1 , typename T2 >

carl::FastPointerMap<typename Poly::PolyType, Variable<T1,T2>*> smtrat::lra::Tableau< Settings, T1, T2 >::mSlackVars

private

Definition at line 275 of file Tableau.h.

◆ mUnusedIDs

template<class Settings , typename T1 , typename T2 >

std::stack<EntryID> smtrat::lra::Tableau< Settings, T1, T2 >::mUnusedIDs

private

Definition at line 253 of file Tableau.h.

◆ mVariableIdAllocator

template<class Settings , typename T1 , typename T2 >

carl::IDPool smtrat::lra::Tableau< Settings, T1, T2 >::mVariableIdAllocator

private

Id allocator for the variables.

Definition at line 255 of file Tableau.h.

◆ mVarIDCounter

template<class Settings , typename T1 , typename T2 >

size_t smtrat::lra::Tableau< Settings, T1, T2 >::mVarIDCounter

private

Definition at line 249 of file Tableau.h.

◆ mWidth

template<class Settings , typename T1 , typename T2 >

size_t smtrat::lra::Tableau< Settings, T1, T2 >::mWidth

private

Definition at line 243 of file Tableau.h.

◆ onlyUpdate

template<class Settings , typename T1 , typename T2 >

bool smtrat::lra::Tableau< Settings, T1, T2 >::onlyUpdate = false

private

Definition at line 269 of file Tableau.h.

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

smtrat-modules/LRAModule/tableau/Tableau.h

Data Structures

Public Member Functions

Private Attributes

Detailed Description

template<class Settings, typename T1, typename T2> class smtrat::lra::Tableau< Settings, T1, T2 >

Constructor & Destructor Documentation

◆ Tableau()

◆ ~Tableau()

Member Function Documentation

◆ activateBasicVar()

◆ activateBound()

◆ adaptDelta()

◆ addToEntry()

◆ betterEntry()

◆ boundedVariables()

◆ checkCorrectness()

◆ collect_premises()

◆ columns()

◆ compressRows()

◆ compute_dVio()

◆ computeLeavingCandidates()

◆ constraintToBound()

◆ currentDelta()

◆ deactivateBasicVar()

◆ defaultBoundPosition()

◆ deleteVariable()

◆ dViolationSum()

◆ entryIsNegative()

◆ entryIsPositive()

◆ get_dVioSum()

◆ getConflict()

◆ getConflictsFrom()

◆ getInfeasibilityRow()

◆ getMultilineConflict()

◆ getNumberOfEntries()

◆ getObjectiveVariable()

◆ getRationalAssignment()

◆ getVariable()

◆ gomoryCut()

◆ hasConflict()

◆ hasMultilineConflict()

◆ isActive()

◆ isConflicting()

◆ isSuitable()

◆ isSuitableConflictDetection()

◆ newBasicVariable()

◆ newBound()

◆ newNonbasicVariable()

◆ newTableauEntry()

◆ nextPivotingElement()

◆ nextPivotingElementForOptimizing()

◆ nextPivotingElementInfeasibilities()

◆ nextZeroPivotingElementForOptimizing()

◆ numberOfPivotingSteps()

◆ optimizeIndependentNonbasics()

◆ originalVars()

◆ pivot()

◆ print()

◆ printEntries()

◆ printEntry()

◆ printHeap()

◆ printLearnedBound()

◆ printLearnedBounds()

◆ printVariables()

◆ rConstraintToBound()

◆ removeBound()

◆ removeEntry()

◆ resetAssignment()

◆ resetNumberOfPivotingSteps()

◆ resetTheta()

◆ rLearnedLowerBounds()

◆ rLearnedUpperBounds()

◆ rNewLearnedBounds()

◆ rowCorrect()

◆ rowRefinement()

◆ rows()

◆ setBlandsRuleStart()

◆ setInfeasibilityRow()

◆ setSize()

◆ size()

template<class Settings, typename T1, typename T2>
class smtrat::lra::Tableau< Settings, T1, T2 >