From fe6a0100aa008c3116a18dd0346d996f73707565 Mon Sep 17 00:00:00 2001 From: Guy Katz Date: Wed, 23 May 2018 16:06:07 +0300 Subject: [PATCH] Handle MalformedBasis exceptions when adding a new equation (#50) * a more efficient computation of the explicit basis: 1. Compute from left to write instead of from right to left. This makes multipliciation by eta matrices easier 2. Compute invLP once-and-for-all, when the basis is factorized * pivoting stats * bug fix in store/restore * supprt for a "basis column oracle", which allows the basis factorization classes to query the tableau for constraint matrix columns * cleanup in FT factorization * grab a fresh basis from the oracle instead of condensing th etas * bug fix in test * started separating out the gaussian elimination functionality from the basis factorization classes * error when adding an equation * handle the initial assignment of basic variables as part of Tableau::initializeTableau(0 * make RowBoundTightener remember the tableau, instead of passing the tableau again and again every time * Tableau's addRow() informs objects registered as "resizeWatchers" that the tableau dimensions have changed. Tableau handles the case where the basis factorization fails after a row is added, by choosing a new set of basic variables using gaussian elimination of the constraint matrix * oops * oops --- src/engine/AutoRowBoundTightener.h | 4 +- src/engine/Engine.cpp | 61 ++++---- src/engine/IRowBoundTightener.h | 24 +-- src/engine/ITableau.h | 14 +- src/engine/RowBoundTightener.cpp | 115 ++++++++------- src/engine/RowBoundTightener.h | 40 +++-- src/engine/T/RowBoundTightenerFactory.h | 8 +- src/engine/Tableau.cpp | 139 ++++++++++++++---- src/engine/Tableau.h | 15 +- src/engine/real/RowBoundTightenerFactory.cpp | 4 +- src/engine/tests/MockRowBoundTightener.h | 28 ++-- .../tests/MockRowBoundTightenerFactory.h | 4 +- src/engine/tests/MockTableau.h | 11 +- src/engine/tests/Test_Engine.h | 5 +- src/engine/tests/Test_RowBoundTightener.h | 36 ++--- src/engine/tests/Test_Tableau.h | 79 ++++------ 16 files changed, 354 insertions(+), 233 deletions(-) diff --git a/src/engine/AutoRowBoundTightener.h b/src/engine/AutoRowBoundTightener.h index 100c42b38..3bd26bf08 100644 --- a/src/engine/AutoRowBoundTightener.h +++ b/src/engine/AutoRowBoundTightener.h @@ -19,9 +19,9 @@ class AutoRowBoundTightener { public: - AutoRowBoundTightener() + AutoRowBoundTightener( const ITableau &tableau ) { - _rowBoundTightener = T::createRowBoundTightener(); + _rowBoundTightener = T::createRowBoundTightener( tableau ); } ~AutoRowBoundTightener() diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 05d8d7b5e..c74df43f6 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -25,7 +25,8 @@ #include "TimeUtils.h" Engine::Engine() - : _smtCore( this ) + : _rowBoundTightener( *_tableau ) + , _smtCore( this ) , _numPlConstraintsDisabledByValidSplits( 0 ) , _preprocessingEnabled( false ) , _work( NULL ) @@ -407,7 +408,7 @@ void Engine::performSimplexStep() if ( !fakePivot ) { _tableau->computePivotRow(); - _rowBoundTightener->examinePivotRow( _tableau ); + _rowBoundTightener->examinePivotRow(); } // Perform the actual pivot @@ -562,28 +563,6 @@ bool Engine::processInputQuery( InputQuery &inputQuery, bool preprocess ) ++equationIndex; } - // Placeholder: better constraint matrix analysis as part - // of the preprocessing phase. - - AutoConstraintMatrixAnalyzer analyzer; - analyzer->analyze( _tableau->getA(), _tableau->getM(), _tableau->getN() ); - - if ( analyzer->getRank() != _tableau->getM() ) - { - printf( "Warning!! Contraint matrix rank is %u (out of %u)\n", - analyzer->getRank(), _tableau->getM() ); - } - - List independentColumns = analyzer->getIndependentColumns(); - - unsigned assigned = 0; - for( unsigned basicVar : independentColumns ) - { - _tableau->markAsBasic( basicVar ); - _tableau->assignIndexToBasicVariable( basicVar, assigned ); - assigned++; - } - for ( unsigned i = 0; i < n; ++i ) { _tableau->setLowerBound( i, _preprocessedQuery.getLowerBound( i ) ); @@ -591,8 +570,9 @@ bool Engine::processInputQuery( InputQuery &inputQuery, bool preprocess ) } _tableau->registerToWatchAllVariables( _rowBoundTightener ); + _tableau->registerResizeWatcher( _rowBoundTightener ); - _rowBoundTightener->initialize( _tableau ); + _rowBoundTightener->setDimensions(); _plConstraints = _preprocessedQuery.getPiecewiseLinearConstraints(); for ( const auto &constraint : _plConstraints ) @@ -601,7 +581,20 @@ bool Engine::processInputQuery( InputQuery &inputQuery, bool preprocess ) constraint->setStatistics( &_statistics ); } - _tableau->initializeTableau(); + // Placeholder: better constraint matrix analysis as part + // of the preprocessing phase. + + AutoConstraintMatrixAnalyzer analyzer; + analyzer->analyze( _tableau->getA(), _tableau->getM(), _tableau->getN() ); + + if ( analyzer->getRank() != _tableau->getM() ) + { + printf( "Warning!! Contraint matrix rank is %u (out of %u)\n", + analyzer->getRank(), _tableau->getM() ); + } + List independentColumns = analyzer->getIndependentColumns(); + _tableau->initializeTableau( independentColumns ); + _costFunctionManager->initialize(); _tableau->registerCostFunctionManager( _costFunctionManager ); _activeEntryStrategy->initialize( _tableau ); @@ -711,7 +704,7 @@ void Engine::restoreState( const EngineState &state ) _numPlConstraintsDisabledByValidSplits = state._numPlConstraintsDisabledByValidSplits; // Make sure the data structures are initialized to the correct size - _rowBoundTightener->initialize( _tableau ); + _rowBoundTightener->setDimensions(); adjustWorkMemorySize(); _activeEntryStrategy->resizeHook( _tableau ); _costFunctionManager->initialize(); @@ -755,7 +748,7 @@ void Engine::applySplit( const PiecewiseLinearCaseSplit &split ) adjustWorkMemorySize(); - _rowBoundTightener->initialize( _tableau ); + _rowBoundTightener->resetBounds(); for ( auto &bound : bounds ) { @@ -878,7 +871,7 @@ void Engine::tightenBoundsOnConstraintMatrix() if ( _statistics.getNumMainLoopIterations() % GlobalConfiguration::BOUND_TIGHTING_ON_CONSTRAINT_MATRIX_FREQUENCY == 0 ) { - _rowBoundTightener->examineConstraintMatrix( _tableau, true ); + _rowBoundTightener->examineConstraintMatrix( true ); _statistics.incNumBoundTighteningOnConstraintMatrix(); } @@ -897,15 +890,15 @@ void Engine::explicitBasisBoundTightening() switch ( GlobalConfiguration::EXPLICIT_BASIS_BOUND_TIGHTENING_TYPE ) { case GlobalConfiguration::USE_BASIS_MATRIX: - _rowBoundTightener->examineBasisMatrix( _tableau, saturation ); + _rowBoundTightener->examineBasisMatrix( saturation ); break; case GlobalConfiguration::COMPUTE_INVERTED_BASIS_MATRIX: - _rowBoundTightener->examineInvertedBasisMatrix( _tableau, saturation ); + _rowBoundTightener->examineInvertedBasisMatrix( saturation ); break; case GlobalConfiguration::USE_IMPLICIT_INVERTED_BASIS_MATRIX: - _rowBoundTightener->examineImplicitInvertedBasisMatrix( _tableau, saturation ); + _rowBoundTightener->examineImplicitInvertedBasisMatrix( saturation ); break; } @@ -926,7 +919,7 @@ void Engine::performPrecisionRestoration( PrecisionRestorer::RestoreBasics resto _statistics.addTimeForPrecisionRestoration( TimeUtils::timePassed( start, end ) ); _statistics.incNumPrecisionRestorations(); - _rowBoundTightener->clear( _tableau ); + _rowBoundTightener->clear(); // debug double after = _degradationChecker.computeDegradation( *_tableau ); @@ -946,7 +939,7 @@ void Engine::performPrecisionRestoration( PrecisionRestorer::RestoreBasics resto _statistics.addTimeForPrecisionRestoration( TimeUtils::timePassed( start, end ) ); _statistics.incNumPrecisionRestorations(); - _rowBoundTightener->clear( _tableau ); + _rowBoundTightener->clear(); // debug double afterSecond = _degradationChecker.computeDegradation( *_tableau ); diff --git a/src/engine/IRowBoundTightener.h b/src/engine/IRowBoundTightener.h index a78d2af8b..dd6f1fceb 100644 --- a/src/engine/IRowBoundTightener.h +++ b/src/engine/IRowBoundTightener.h @@ -16,21 +16,25 @@ #include "ITableau.h" #include "Tightening.h" -class IRowBoundTightener : public ITableau::VariableWatcher +class IRowBoundTightener : public ITableau::VariableWatcher, public ITableau::ResizeWatcher { public: virtual ~IRowBoundTightener() {}; /* - Allocate internal work memory according to the tableau size and - initialize tightest lower/upper bounds using the talbeau. + Allocate internal work memory according to the tableau size. */ - virtual void initialize( const ITableau &tableau ) = 0; + virtual void setDimensions() = 0; + + /* + Initialize tightest lower/upper bounds using the talbeau. + */ + virtual void resetBounds() = 0; /* Clear all learned bounds, without reallocating memory. */ - virtual void clear( const ITableau &tableau ) = 0; + virtual void clear() = 0; /* Derive and enqueue new bounds for all varaibles, using the @@ -38,7 +42,7 @@ class IRowBoundTightener : public ITableau::VariableWatcher tableau. Can also do this until saturation, meaning that we continue until no new bounds are learned. */ - virtual void examineBasisMatrix( const ITableau &tableau, bool untilSaturation ) = 0; + virtual void examineBasisMatrix( bool untilSaturation ) = 0; /* Derive and enqueue new bounds for all varaibles, using the @@ -46,7 +50,7 @@ class IRowBoundTightener : public ITableau::VariableWatcher through the tableau. Can also do this until saturation, meaning that we continue until no new bounds are learned. */ - virtual void examineInvertedBasisMatrix( const ITableau &tableau, bool untilSaturation ) = 0; + virtual void examineInvertedBasisMatrix( bool untilSaturation ) = 0; /* Derive and enqueue new bounds for all varaibles, implicitly using the @@ -55,7 +59,7 @@ class IRowBoundTightener : public ITableau::VariableWatcher is performed via FTRANs. Can also do this until saturation, meaning that we continue until no new bounds are learned. */ - virtual void examineImplicitInvertedBasisMatrix( const ITableau &tableau, bool untilSaturation ) = 0; + virtual void examineImplicitInvertedBasisMatrix( bool untilSaturation ) = 0; /* Derive and enqueue new bounds for all varaibles, using the @@ -63,14 +67,14 @@ class IRowBoundTightener : public ITableau::VariableWatcher also do this until saturation, meaning that we continue until no new bounds are learned. */ - virtual void examineConstraintMatrix( const ITableau &tableau, bool untilSaturation ) = 0; + virtual void examineConstraintMatrix( bool untilSaturation ) = 0; /* Derive and enqueue new bounds immedaitely following a pivot operation in the given tableau. The tightening is performed for the entering variable (which is now basic). */ - virtual void examinePivotRow( ITableau &tableau ) = 0; + virtual void examinePivotRow() = 0; /* Get the tightenings entailed by the constraint. diff --git a/src/engine/ITableau.h b/src/engine/ITableau.h index 9dd221878..6fbbc4f48 100644 --- a/src/engine/ITableau.h +++ b/src/engine/ITableau.h @@ -69,10 +69,22 @@ class ITableau virtual void notifyUpperBound( unsigned /* variable */, double /* bound */ ) {} }; + class ResizeWatcher + { + public: + /* + This callback will be invoked when the tableau size changes, + typically when new variables are added. + */ + virtual void notifyDimensionChange( unsigned /* m */, unsigned /* n */ ) {} + }; + virtual void registerToWatchAllVariables( VariableWatcher *watcher ) = 0; virtual void registerToWatchVariable( VariableWatcher *watcher, unsigned variable ) = 0; virtual void unregisterToWatchVariable( VariableWatcher *watcher, unsigned variable ) = 0; + virtual void registerResizeWatcher( ResizeWatcher *watcher ) = 0; + virtual void registerCostFunctionManager( ICostFunctionManager *costFunctionManager ) = 0; virtual ~ITableau() {}; @@ -82,7 +94,7 @@ class ITableau virtual void setRightHandSide( const double *b ) = 0; virtual void setRightHandSide( unsigned index, double value ) = 0; virtual void markAsBasic( unsigned variable ) = 0; - virtual void initializeTableau() = 0; + virtual void initializeTableau( const List &initialBasicVariables ) = 0; virtual double getValue( unsigned variable ) = 0; virtual bool allBoundsValid() const = 0; virtual double getLowerBound( unsigned variable ) const = 0; diff --git a/src/engine/RowBoundTightener.cpp b/src/engine/RowBoundTightener.cpp index 85f6ca35c..bb29edfc1 100644 --- a/src/engine/RowBoundTightener.cpp +++ b/src/engine/RowBoundTightener.cpp @@ -16,8 +16,9 @@ #include "RowBoundTightener.h" #include "Statistics.h" -RowBoundTightener::RowBoundTightener() - : _lowerBounds( NULL ) +RowBoundTightener::RowBoundTightener( const ITableau &tableau ) + : _tableau( tableau ) + , _lowerBounds( NULL ) , _upperBounds( NULL ) , _tightenedLower( NULL ) , _tightenedUpper( NULL ) @@ -30,12 +31,12 @@ RowBoundTightener::RowBoundTightener() { } -void RowBoundTightener::initialize( const ITableau &tableau ) +void RowBoundTightener::setDimensions() { freeMemoryIfNeeded(); - _n = tableau.getN(); - _m = tableau.getM(); + _n = _tableau.getN(); + _m = _tableau.getM(); _lowerBounds = new double[_n]; if ( !_lowerBounds ) @@ -53,14 +54,7 @@ void RowBoundTightener::initialize( const ITableau &tableau ) if ( !_tightenedUpper ) throw ReluplexError( ReluplexError::ALLOCATION_FAILED, "RowBoundTightener::tightenedUpper" ); - std::fill( _tightenedLower, _tightenedLower + _n, false ); - std::fill( _tightenedUpper, _tightenedUpper + _n, false ); - - for ( unsigned i = 0; i < _n; ++i ) - { - _lowerBounds[i] = tableau.getLowerBound( i ); - _upperBounds[i] = tableau.getUpperBound( i ); - } + resetBounds(); if ( GlobalConfiguration::EXPLICIT_BASIS_BOUND_TIGHTENING_TYPE == GlobalConfiguration::COMPUTE_INVERTED_BASIS_MATRIX ) @@ -84,15 +78,27 @@ void RowBoundTightener::initialize( const ITableau &tableau ) _ciSign = new char[_n]; } -void RowBoundTightener::clear( const ITableau &tableau ) +void RowBoundTightener::resetBounds() +{ + std::fill( _tightenedLower, _tightenedLower + _n, false ); + std::fill( _tightenedUpper, _tightenedUpper + _n, false ); + + for ( unsigned i = 0; i < _n; ++i ) + { + _lowerBounds[i] = _tableau.getLowerBound( i ); + _upperBounds[i] = _tableau.getUpperBound( i ); + } +} + +void RowBoundTightener::clear() { std::fill( _tightenedLower, _tightenedLower + _n, false ); std::fill( _tightenedUpper, _tightenedUpper + _n, false ); for ( unsigned i = 0; i < _n; ++i ) { - _lowerBounds[i] = tableau.getLowerBound( i ); - _upperBounds[i] = tableau.getUpperBound( i ); + _lowerBounds[i] = _tableau.getLowerBound( i ); + _upperBounds[i] = _tableau.getUpperBound( i ); } } @@ -160,7 +166,7 @@ void RowBoundTightener::freeMemoryIfNeeded() } } -void RowBoundTightener::examineImplicitInvertedBasisMatrix( const ITableau &tableau, bool untilSaturation ) +void RowBoundTightener::examineImplicitInvertedBasisMatrix( bool untilSaturation ) { /* Roughly (the dimensions don't add up): @@ -169,20 +175,20 @@ void RowBoundTightener::examineImplicitInvertedBasisMatrix( const ITableau &tabl */ // Find z = inv(B) * b, by solving the forward transformation Bz = b - tableau.forwardTransformation( tableau.getRightHandSide(), _z ); + _tableau.forwardTransformation( _tableau.getRightHandSide(), _z ); for ( unsigned i = 0; i < _m; ++i ) { _rows[i]->_scalar = _z[i]; - _rows[i]->_lhs = tableau.basicIndexToVariable( i ); + _rows[i]->_lhs = _tableau.basicIndexToVariable( i ); } // Now, go over the columns of the constraint martrix, perform an FTRAN // for each of them, and populate the rows. for ( unsigned i = 0; i < _n - _m; ++i ) { - unsigned nonBasic = tableau.nonBasicIndexToVariable( i ); - const double *ANColumn = tableau.getAColumn( nonBasic ); - tableau.forwardTransformation( ANColumn, _z ); + unsigned nonBasic = _tableau.nonBasicIndexToVariable( i ); + const double *ANColumn = _tableau.getAColumn( nonBasic ); + _tableau.forwardTransformation( ANColumn, _z ); for ( unsigned j = 0; j < _m; ++j ) { @@ -197,7 +203,7 @@ void RowBoundTightener::examineImplicitInvertedBasisMatrix( const ITableau &tabl unsigned newBoundsLearned; do { - newBoundsLearned = onePassOverInvertedBasisRows( tableau ); + newBoundsLearned = onePassOverInvertedBasisRows(); if ( _statistics && ( newBoundsLearned > 0 ) ) _statistics->incNumTighteningsFromExplicitBasis( newBoundsLearned ); @@ -205,7 +211,7 @@ void RowBoundTightener::examineImplicitInvertedBasisMatrix( const ITableau &tabl while ( untilSaturation && ( newBoundsLearned > 0 ) ); } -void RowBoundTightener::examineInvertedBasisMatrix( const ITableau &tableau, bool untilSaturation ) +void RowBoundTightener::examineInvertedBasisMatrix( bool untilSaturation ) { /* Roughly (the dimensions don't add up): @@ -215,8 +221,8 @@ void RowBoundTightener::examineInvertedBasisMatrix( const ITableau &tableau, boo We compute one row at a time. */ - const double *b = tableau.getRightHandSide(); - const double *invB = tableau.getInverseBasisMatrix(); + const double *b = _tableau.getRightHandSide(); + const double *invB = _tableau.getInverseBasisMatrix(); try { @@ -231,18 +237,18 @@ void RowBoundTightener::examineInvertedBasisMatrix( const ITableau &tableau, boo // Now update the row's coefficients for basic variable i for ( unsigned j = 0; j < _n - _m; ++j ) { - row->_row[j]._var = tableau.nonBasicIndexToVariable( j ); + row->_row[j]._var = _tableau.nonBasicIndexToVariable( j ); // Dot product of the i'th row of inv(B) with the appropriate // column of An - const double *ANColumn = tableau.getAColumn( row->_row[j]._var ); + const double *ANColumn = _tableau.getAColumn( row->_row[j]._var ); row->_row[j]._coefficient = 0; for ( unsigned k = 0; k < _m; ++k ) row->_row[j]._coefficient -= ( invB[i * _m + k] * ANColumn[k] ); } // Store the lhs variable - row->_lhs = tableau.basicIndexToVariable( i ); + row->_lhs = _tableau.basicIndexToVariable( i ); } // We now have all the rows, can use them for tightening. @@ -252,7 +258,7 @@ void RowBoundTightener::examineInvertedBasisMatrix( const ITableau &tableau, boo unsigned newBoundsLearned; do { - newBoundsLearned = onePassOverInvertedBasisRows( tableau ); + newBoundsLearned = onePassOverInvertedBasisRows(); if ( _statistics && ( newBoundsLearned > 0 ) ) _statistics->incNumTighteningsFromExplicitBasis( newBoundsLearned ); @@ -268,17 +274,17 @@ void RowBoundTightener::examineInvertedBasisMatrix( const ITableau &tableau, boo delete[] invB; } -unsigned RowBoundTightener::onePassOverInvertedBasisRows( const ITableau &tableau ) +unsigned RowBoundTightener::onePassOverInvertedBasisRows() { unsigned newBounds = 0; for ( unsigned i = 0; i < _m; ++i ) - newBounds += tightenOnSingleInvertedBasisRow( tableau, *( _rows[i] ) ); + newBounds += tightenOnSingleInvertedBasisRow( *( _rows[i] ) ); return newBounds; } -unsigned RowBoundTightener::tightenOnSingleInvertedBasisRow( const ITableau &tableau, const TableauRow &row ) +unsigned RowBoundTightener::tightenOnSingleInvertedBasisRow( const TableauRow &row ) { /* A row is of the form @@ -287,8 +293,8 @@ unsigned RowBoundTightener::tightenOnSingleInvertedBasisRow( const ITableau &tab We wish to tighten once for y, but also once for every x. */ - unsigned n = tableau.getN(); - unsigned m = tableau.getM(); + unsigned n = _tableau.getN(); + unsigned m = _tableau.getM(); unsigned result = 0; @@ -447,7 +453,7 @@ unsigned RowBoundTightener::tightenOnSingleInvertedBasisRow( const ITableau &tab return result; } -void RowBoundTightener::examineBasisMatrix( const ITableau &tableau, bool untilSaturation ) +void RowBoundTightener::examineBasisMatrix( bool untilSaturation ) { unsigned newBoundsLearned; @@ -457,7 +463,7 @@ void RowBoundTightener::examineBasisMatrix( const ITableau &tableau, bool untilS */ do { - newBoundsLearned = onePassOverBasisMatrix( tableau ); + newBoundsLearned = onePassOverBasisMatrix(); if ( _statistics && ( newBoundsLearned > 0 ) ) _statistics->incNumTighteningsFromExplicitBasis( newBoundsLearned ); @@ -465,12 +471,12 @@ void RowBoundTightener::examineBasisMatrix( const ITableau &tableau, bool untilS while ( untilSaturation && ( newBoundsLearned > 0 ) ); } -unsigned RowBoundTightener::onePassOverBasisMatrix( const ITableau &tableau ) +unsigned RowBoundTightener::onePassOverBasisMatrix() { unsigned newBounds = 0; List basisEquations; - tableau.getBasisEquations( basisEquations ); + _tableau.getBasisEquations( basisEquations ); for ( const auto &equation : basisEquations ) for ( const auto &addend : equation->_addends ) newBounds += tightenOnSingleEquation( *equation, addend ); @@ -552,7 +558,7 @@ unsigned RowBoundTightener::tightenOnSingleEquation( Equation &equation, return result; } -void RowBoundTightener::examineConstraintMatrix( const ITableau &tableau, bool untilSaturation ) +void RowBoundTightener::examineConstraintMatrix( bool untilSaturation ) { unsigned newBoundsLearned; @@ -562,7 +568,7 @@ void RowBoundTightener::examineConstraintMatrix( const ITableau &tableau, bool u */ do { - newBoundsLearned = onePassOverConstraintMatrix( tableau ); + newBoundsLearned = onePassOverConstraintMatrix(); if ( _statistics && ( newBoundsLearned > 0 ) ) _statistics->incNumTighteningsFromConstraintMatrix( newBoundsLearned ); @@ -570,19 +576,19 @@ void RowBoundTightener::examineConstraintMatrix( const ITableau &tableau, bool u while ( untilSaturation && ( newBoundsLearned > 0 ) ); } -unsigned RowBoundTightener::onePassOverConstraintMatrix( const ITableau &tableau ) +unsigned RowBoundTightener::onePassOverConstraintMatrix() { unsigned result = 0; - unsigned m = tableau.getM(); + unsigned m = _tableau.getM(); for ( unsigned i = 0; i < m; ++i ) - result += tightenOnSingleConstraintRow( tableau, i ); + result += tightenOnSingleConstraintRow( i ); return result; } -unsigned RowBoundTightener::tightenOnSingleConstraintRow( const ITableau &tableau, unsigned row ) +unsigned RowBoundTightener::tightenOnSingleConstraintRow( unsigned row ) { /* The cosntraint matrix A satisfies Ax = b. @@ -594,13 +600,13 @@ unsigned RowBoundTightener::tightenOnSingleConstraintRow( const ITableau &tablea sum ci xi - b */ - unsigned n = tableau.getN(); - unsigned m = tableau.getM(); + unsigned n = _tableau.getN(); + unsigned m = _tableau.getM(); unsigned result = 0; - const double *A = tableau.getA(); - const double *b = tableau.getRightHandSide(); + const double *A = _tableau.getA(); + const double *b = _tableau.getRightHandSide(); double ci; @@ -723,13 +729,13 @@ unsigned RowBoundTightener::tightenOnSingleConstraintRow( const ITableau &tablea return result; } -void RowBoundTightener::examinePivotRow( ITableau &tableau ) +void RowBoundTightener::examinePivotRow() { if ( _statistics ) _statistics->incNumRowsExaminedByRowTightener(); - const TableauRow &row = *tableau.getPivotRow(); - unsigned newBoundsLearned = tightenOnSingleInvertedBasisRow( tableau, row ); + const TableauRow &row( *_tableau.getPivotRow() ); + unsigned newBoundsLearned = tightenOnSingleInvertedBasisRow( row ); if ( _statistics && ( newBoundsLearned > 0 ) ) _statistics->incNumTighteningsFromRows( newBoundsLearned ); @@ -776,6 +782,11 @@ void RowBoundTightener::notifyUpperBound( unsigned variable, double bound ) } } +void RowBoundTightener::notifyDimensionChange( unsigned /* m */ , unsigned /* n */ ) +{ + setDimensions(); +} + // // Local Variables: // compile-command: "make -C ../.. " diff --git a/src/engine/RowBoundTightener.h b/src/engine/RowBoundTightener.h index 153c526e0..0c2d5c593 100644 --- a/src/engine/RowBoundTightener.h +++ b/src/engine/RowBoundTightener.h @@ -23,19 +23,23 @@ class RowBoundTightener : public IRowBoundTightener { public: - RowBoundTightener(); + RowBoundTightener( const ITableau &tableau ); ~RowBoundTightener(); /* - Allocate internal work memory according to the tableau size and - initialize tightest lower/upper bounds using the talbeau. + Allocate internal work memory according to the tableau size */ - void initialize( const ITableau &tableau ); + void setDimensions(); + + /* + Initialize tightest lower/upper bounds using the talbeau. + */ + void resetBounds(); /* Clear all learned bounds, without reallocating memory. */ - void clear( const ITableau &tableau ); + void clear(); /* Callbacks from the Tableau, to inform of bounds tightened by, @@ -44,13 +48,18 @@ class RowBoundTightener : public IRowBoundTightener void notifyLowerBound( unsigned variable, double bound ); void notifyUpperBound( unsigned variable, double bound ); + /* + Callback from the Tableau, to inform of a change in dimensions + */ + void notifyDimensionChange( unsigned m, unsigned n ); + /* Derive and enqueue new bounds for all varaibles, using the explicit basis matrix B0 that should be available through the tableau. Can also do this until saturation, meaning that we continue until no new bounds are learned. */ - void examineBasisMatrix( const ITableau &tableau, bool untilSaturation ); + void examineBasisMatrix( bool untilSaturation ); /* Derive and enqueue new bounds for all varaibles, using the @@ -58,7 +67,7 @@ class RowBoundTightener : public IRowBoundTightener through the tableau. Can also do this until saturation, meaning that we continue until no new bounds are learned. */ - void examineInvertedBasisMatrix( const ITableau &tableau, bool untilSaturation ); + void examineInvertedBasisMatrix( bool untilSaturation ); /* Derive and enqueue new bounds for all varaibles, implicitly using the @@ -67,7 +76,7 @@ class RowBoundTightener : public IRowBoundTightener is performed via FTRANs. Can also do this until saturation, meaning that we continue until no new bounds are learned. */ - void examineImplicitInvertedBasisMatrix( const ITableau &tableau, bool untilSaturation ); + void examineImplicitInvertedBasisMatrix( bool untilSaturation ); /* Derive and enqueue new bounds for all varaibles, using the @@ -75,14 +84,14 @@ class RowBoundTightener : public IRowBoundTightener also do this until saturation, meaning that we continue until no new bounds are learned. */ - void examineConstraintMatrix( const ITableau &tableau, bool untilSaturation ); + void examineConstraintMatrix( bool untilSaturation ); /* Derive and enqueue new bounds immedaitely following a pivot operation in the given tableau. The tightening is performed for the entering variable (which is now basic). */ - void examinePivotRow( ITableau &tableau ); + void examinePivotRow(); /* Get the tightenings entailed by the constraint. @@ -95,6 +104,7 @@ class RowBoundTightener : public IRowBoundTightener void setStatistics( Statistics *statistics ); private: + const ITableau &_tableau; unsigned _n; unsigned _m; @@ -132,7 +142,7 @@ class RowBoundTightener : public IRowBoundTightener Do a single pass over the basis matrix and derive any tighter bounds. Return the number of new bounds are learned. */ - unsigned onePassOverBasisMatrix( const ITableau &tableau ); + unsigned onePassOverBasisMatrix(); /* Process the basis row and attempt to derive tighter @@ -146,27 +156,27 @@ class RowBoundTightener : public IRowBoundTightener Do a single pass over the constraint matrix and derive any tighter bounds. Return the number of new bounds learned. */ - unsigned onePassOverConstraintMatrix( const ITableau &tableau ); + unsigned onePassOverConstraintMatrix(); /* Process the tableau row and attempt to derive tighter lower/upper bounds for the specified variable. Return the number of tighter bounds found. */ - unsigned tightenOnSingleConstraintRow( const ITableau &tableau, unsigned row ); + unsigned tightenOnSingleConstraintRow( unsigned row ); /* Do a single pass over the inverted basis rows and derive any tighter bounds. Return the number of new bounds learned. */ - unsigned onePassOverInvertedBasisRows( const ITableau &tableau ); + unsigned onePassOverInvertedBasisRows(); /* Process the inverted basis row and attempt to derive tighter lower/upper bounds for the specified variable. Return the number of tighter bounds found. */ - unsigned tightenOnSingleInvertedBasisRow( const ITableau &tableau, const TableauRow &row ); + unsigned tightenOnSingleInvertedBasisRow( const TableauRow &row ); }; #endif // __RowBoundTightener_h__ diff --git a/src/engine/T/RowBoundTightenerFactory.h b/src/engine/T/RowBoundTightenerFactory.h index 013b03757..00b3c7111 100644 --- a/src/engine/T/RowBoundTightenerFactory.h +++ b/src/engine/T/RowBoundTightenerFactory.h @@ -16,20 +16,20 @@ #include "cxxtest/Mock.h" class IRowBoundTightener; -class ISelector; +class ITableau; namespace T { - IRowBoundTightener *createRowBoundTightener(); + IRowBoundTightener *createRowBoundTightener( const ITableau &tableau ); void discardRowBoundTightener( IRowBoundTightener *rowBoundTightener ); } CXXTEST_SUPPLY( createRowBoundTightener, IRowBoundTightener *, createRowBoundTightener, - (), + ( const ITableau &tableau ), T::createRowBoundTightener, - () ); + ( tableau ) ); CXXTEST_SUPPLY_VOID( discardRowBoundTightener, discardRowBoundTightener, diff --git a/src/engine/Tableau.cpp b/src/engine/Tableau.cpp index 464f0e129..f8cd56ead 100644 --- a/src/engine/Tableau.cpp +++ b/src/engine/Tableau.cpp @@ -11,6 +11,7 @@ **/ #include "BasisFactorizationFactory.h" +#include "ConstraintMatrixAnalyzer.h" #include "Debug.h" #include "EntrySelectionStrategy.h" #include "Equation.h" @@ -244,11 +245,21 @@ void Tableau::assignIndexToBasicVariable( unsigned variable, unsigned index ) _variableToIndex[variable] = index; } -void Tableau::initializeTableau() +void Tableau::initializeTableau( const List &initialBasicVariables ) { - unsigned nonBasicIndex = 0; + _basicVariables.clear(); + + // Assign the basic indices + unsigned basicIndex = 0; + for( unsigned basicVar : initialBasicVariables ) + { + markAsBasic( basicVar ); + assignIndexToBasicVariable( basicVar, basicIndex ); + ++basicIndex; + } - // Assign variable indices + // Assign the non-basic indices + unsigned nonBasicIndex = 0; for ( unsigned i = 0; i < _n; ++i ) { if ( !_basicVariables.exists( i ) ) @@ -1233,46 +1244,114 @@ void Tableau::addEquation( const Equation &equation ) // Invalidate the cost function, so that it is recomputed in the next iteration. _costFunctionManager->invalidateCostFunction(); - // Mark the auxiliary variable as basic, add to indices - _basicVariables.insert( equation._auxVariable ); - _basicIndexToVariable[_m - 1] = equation._auxVariable; - _variableToIndex[equation._auxVariable] = _m - 1; + // All variables except the new one have finite bounds. Use this to compute + // finite bounds for the new variable. + double lb = equation._scalar; + double ub = equation._scalar; + double auxCoefficient; + double coefficient; + unsigned variable; - // Populate the new row of A, compute the assignment for the new basic variable - _b[_m - 1] = equation._scalar; - _basicAssignment[_m - 1] = equation._scalar; - double auxCoefficient = 0.0; for ( const auto &addend : equation._addends ) { - setEntryValue( _m - 1, addend._variable, addend._coefficient ); + coefficient = addend._coefficient; + variable = addend._variable; - if ( addend._variable == equation._auxVariable ) - auxCoefficient = addend._coefficient; + if ( variable == equation._auxVariable ) + { + auxCoefficient = coefficient; + } else - _basicAssignment[_m - 1] -= addend._coefficient * getValue( addend._variable ); + { + if ( FloatUtils::isPositive( coefficient ) ) + { + lb -= coefficient * _upperBounds[variable]; + ub -= coefficient * _lowerBounds[variable]; + } + else + { + lb -= coefficient * _lowerBounds[variable]; + ub -= coefficient * _upperBounds[variable]; + } + } + } + if ( FloatUtils::isPositive( auxCoefficient ) ) + { + setLowerBound( equation._auxVariable, lb / auxCoefficient ); + setUpperBound( equation._auxVariable, ub / auxCoefficient ); + } + else + { + setLowerBound( equation._auxVariable, ub / auxCoefficient ); + setUpperBound( equation._auxVariable, lb / auxCoefficient ); } - ASSERT( !FloatUtils::isZero( auxCoefficient ) ); - _basicAssignment[_m - 1] = _basicAssignment[_m - 1] / auxCoefficient; - ASSERT( FloatUtils::wellFormed( _basicAssignment[_m - 1] ) ); + // Populate the new row of A and b + _b[_m - 1] = equation._scalar; + for ( const auto &addend : equation._addends ) + setEntryValue( _m - 1, addend._variable, addend._coefficient ); - if ( FloatUtils::isZero( _basicAssignment[_m - 1] ) ) - _basicAssignment[_m - 1] = 0.0; + /* + Attempt to make the auxiliary variable the new basic variable. + This usually works. + If it doesn't, compute a new set of basic variables and re-initialize + the tableau (which is more computationally expensive) + */ + _basicIndexToVariable[_m - 1] = equation._auxVariable; + _variableToIndex[equation._auxVariable] = _m - 1; + _basicVariables.insert( equation._auxVariable ); - // Refactorize the basis + // Attempt to refactorize the basis + bool factorizationSuccessful = true; try { _basisFactorization->refactorizeBasis(); } catch ( MalformedBasisException & ) { - log( "addEquation failed - could not refactorize basis" ); - throw ReluplexError( ReluplexError::FAILURE_TO_ADD_NEW_EQUATION ); + factorizationSuccessful = false; + } + + if ( factorizationSuccessful ) + { + _basicAssignment[_m - 1] = equation._scalar; + double auxCoefficient = 0.0; + for ( const auto &addend : equation._addends ) + { + if ( addend._variable == equation._auxVariable ) + auxCoefficient = addend._coefficient; + else + _basicAssignment[_m - 1] -= addend._coefficient * getValue( addend._variable ); + } + + ASSERT( !FloatUtils::isZero( auxCoefficient ) ); + _basicAssignment[_m - 1] = _basicAssignment[_m - 1] / auxCoefficient; + ASSERT( FloatUtils::wellFormed( _basicAssignment[_m - 1] ) ); + + if ( FloatUtils::isZero( _basicAssignment[_m - 1] ) ) + _basicAssignment[_m - 1] = 0.0; + + // Notify about the new variable's assignment and compute its status + notifyVariableValue( _basicIndexToVariable[_m - 1], _basicAssignment[_m - 1] ); + computeBasicStatus( _m - 1 ); + return; } + else + { + ConstraintMatrixAnalyzer analyzer; + analyzer.analyze( _A, _m, _n ); + List independentColumns = analyzer.getIndependentColumns(); - // Notify about the new variable's assignment and compute its status - notifyVariableValue( _basicIndexToVariable[_m - 1], _basicAssignment[_m - 1] ); - computeBasicStatus( _m - 1 ); + try + { + initializeTableau( independentColumns ); + } + catch ( MalformedBasisException & ) + { + log( "addEquation failed - could not refactorize basis" ); + throw ReluplexError( ReluplexError::FAILURE_TO_ADD_NEW_EQUATION ); + } + } } void Tableau::addRow() @@ -1401,6 +1480,9 @@ void Tableau::addRow() _m = newM; _n = newN; _costFunctionManager->initialize(); + + for ( const auto &watcher : _resizeWatchers ) + watcher->notifyDimensionChange( _m, _n ); } void Tableau::registerToWatchVariable( VariableWatcher *watcher, unsigned variable ) @@ -1418,6 +1500,11 @@ void Tableau::registerToWatchAllVariables( VariableWatcher *watcher ) _globalWatchers.append( watcher ); } +void Tableau::registerResizeWatcher( ResizeWatcher *watcher ) +{ + _resizeWatchers.append( watcher ); +} + void Tableau::notifyVariableValue( unsigned variable, double value ) { for ( auto &watcher : _globalWatchers ) diff --git a/src/engine/Tableau.h b/src/engine/Tableau.h index 127651ebf..fc286c67c 100644 --- a/src/engine/Tableau.h +++ b/src/engine/Tableau.h @@ -85,7 +85,7 @@ class Tableau : public ITableau, public IBasisFactorization::BasisColumnOracle to lower bounds and computes the assignment. Assign the initial basic indices according to the equations. */ - void initializeTableau(); + void initializeTableau( const List &initialBasicVariables ); void assignIndexToBasicVariable( unsigned variable, unsigned index ); /* @@ -333,6 +333,11 @@ class Tableau : public ITableau, public IBasisFactorization::BasisColumnOracle void registerToWatchVariable( VariableWatcher *watcher, unsigned variable ); void unregisterToWatchVariable( VariableWatcher *watcher, unsigned variable ); + /* + Register to watch for tableau dimension changes. + */ + void registerResizeWatcher( ResizeWatcher *watcher ); + /* Register the cost function manager. */ @@ -388,10 +393,18 @@ class Tableau : public ITableau, public IBasisFactorization::BasisColumnOracle const double *getColumnOfBasis( unsigned column ) const; private: + /* + Variable watchers + */ typedef List VariableWatchers; Map _variableToWatchers; List _globalWatchers; + /* + Resize watchers + */ + List _resizeWatchers; + /* The dimensions of matrix A */ diff --git a/src/engine/real/RowBoundTightenerFactory.cpp b/src/engine/real/RowBoundTightenerFactory.cpp index d7c1cf04a..5f06ca585 100644 --- a/src/engine/real/RowBoundTightenerFactory.cpp +++ b/src/engine/real/RowBoundTightenerFactory.cpp @@ -14,9 +14,9 @@ namespace T { - IRowBoundTightener *createRowBoundTightener() + IRowBoundTightener *createRowBoundTightener( const ITableau &tableau ) { - return new RowBoundTightener(); + return new RowBoundTightener( tableau ); } void discardRowBoundTightener( IRowBoundTightener *rowBoundTightener ) diff --git a/src/engine/tests/MockRowBoundTightener.h b/src/engine/tests/MockRowBoundTightener.h index 0b524aec3..67065dc11 100644 --- a/src/engine/tests/MockRowBoundTightener.h +++ b/src/engine/tests/MockRowBoundTightener.h @@ -23,7 +23,7 @@ class MockRowBoundTightener : public IRowBoundTightener wasCreated = false; wasDiscarded = false; - initializeWasCalled = false; + setDimensionsWasCalled = false; } ~MockRowBoundTightener() @@ -32,11 +32,13 @@ class MockRowBoundTightener : public IRowBoundTightener bool wasCreated; bool wasDiscarded; + const ITableau *lastTableau; - void mockConstructor() + void mockConstructor( const ITableau &tableau ) { TS_ASSERT( !wasCreated ); wasCreated = true; + lastTableau = &tableau; } void mockDestructor() @@ -46,22 +48,26 @@ class MockRowBoundTightener : public IRowBoundTightener wasDiscarded = true; } - bool initializeWasCalled; - void initialize( const ITableau &/* tableau */ ) + bool setDimensionsWasCalled; + void setDimensions() { - initializeWasCalled = true; + setDimensionsWasCalled = true; } - void clear( const ITableau &/* tableau */ ) {} + void resetBounds() + { + } + + void clear() {} void notifyLowerBound( unsigned /* variable */, double /* bound */ ) {} void notifyUpperBound( unsigned /* variable */, double /* bound */ ) {} - void examineBasisMatrix( const ITableau &/* tableau */, bool /* untilSaturation */ ) {} - void examineInvertedBasisMatrix( const ITableau &/* tableau */, bool /* untilSaturation */ ) {} - void examineConstraintMatrix( const ITableau &/* tableau */, bool /* untilSaturation */ ) {} - void examinePivotRow( ITableau &/* tableau */ ) {} + void examineBasisMatrix( bool /* untilSaturation */ ) {} + void examineInvertedBasisMatrix( bool /* untilSaturation */ ) {} + void examineConstraintMatrix( bool /* untilSaturation */ ) {} + void examinePivotRow() {} void getRowTightenings( List &/* tightenings */ ) const {} void setStatistics( Statistics */* statistics */ ) {} - void examineImplicitInvertedBasisMatrix( const ITableau &/* tableau */, bool /* untilSaturation */ ) {} + void examineImplicitInvertedBasisMatrix( bool /* untilSaturation */ ) {} }; #endif // __MockRowBoundTightener_h__ diff --git a/src/engine/tests/MockRowBoundTightenerFactory.h b/src/engine/tests/MockRowBoundTightenerFactory.h index dc3d5065a..39e6c4b92 100644 --- a/src/engine/tests/MockRowBoundTightenerFactory.h +++ b/src/engine/tests/MockRowBoundTightenerFactory.h @@ -31,9 +31,9 @@ class MockRowBoundTightenerFactory : } } - IRowBoundTightener *createRowBoundTightener() + IRowBoundTightener *createRowBoundTightener( const ITableau &tableau ) { - mockRowBoundTightener.mockConstructor(); + mockRowBoundTightener.mockConstructor( tableau ); return &mockRowBoundTightener; } diff --git a/src/engine/tests/MockTableau.h b/src/engine/tests/MockTableau.h index c0fdfbbac..1915b8d42 100644 --- a/src/engine/tests/MockTableau.h +++ b/src/engine/tests/MockTableau.h @@ -152,10 +152,13 @@ class MockTableau : public ITableau } bool initializeTableauCalled; - void initializeTableau() + void initializeTableau( const List &initialBasicVariables ) { TS_ASSERT( !initializeTableauCalled ); initializeTableauCalled = true; + + for ( const auto &basic : initialBasicVariables ) + lastBasicVariables.insert( basic ); } Map nextValues; @@ -429,6 +432,12 @@ class MockTableau : public ITableau { } + Set lastResizeWatchers; + void registerResizeWatcher( ResizeWatcher *watcher ) + { + lastResizeWatchers.insert( watcher ); + } + ICostFunctionManager *lastCostFunctionManager; void registerCostFunctionManager( ICostFunctionManager *costFunctionManager ) { diff --git a/src/engine/tests/Test_Engine.h b/src/engine/tests/Test_Engine.h index 48a1b9c74..e111cae6e 100644 --- a/src/engine/tests/Test_Engine.h +++ b/src/engine/tests/Test_Engine.h @@ -133,7 +133,10 @@ class EngineTestSuite : public CxxTest::TestSuite TS_ASSERT( tableau->initializeTableauCalled ); TS_ASSERT( costFunctionManager->initializeWasCalled ); - TS_ASSERT( rowTightener->initializeWasCalled ); + TS_ASSERT( rowTightener->setDimensionsWasCalled ); + + TS_ASSERT_EQUALS( tableau->lastResizeWatchers.size(), 1U ); + TS_ASSERT_EQUALS( *( tableau->lastResizeWatchers.begin() ), rowTightener ); TS_ASSERT_EQUALS( tableau->lastCostFunctionManager, costFunctionManager ); diff --git a/src/engine/tests/Test_RowBoundTightener.h b/src/engine/tests/Test_RowBoundTightener.h index b8ebdeb48..570f3aea6 100644 --- a/src/engine/tests/Test_RowBoundTightener.h +++ b/src/engine/tests/Test_RowBoundTightener.h @@ -40,7 +40,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite void test_pivot_row__both_bounds_tightened() { - RowBoundTightener tightener; + RowBoundTightener tightener( *tableau ); tableau->setDimensions( 2, 5 ); @@ -60,7 +60,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite tableau->setLowerBound( 4, -100 ); tableau->setUpperBound( 4, 100 ); - tightener.initialize( *tableau ); + tightener.setDimensions(); TableauRow row( 3 ); // 1 - x0 - x1 + 2x2 @@ -76,7 +76,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite // x0 entering, x4 leaving // x0 = 1 - x1 + 2 x2 - x4 - TS_ASSERT_THROWS_NOTHING( tightener.examinePivotRow( *tableau ) ); + TS_ASSERT_THROWS_NOTHING( tightener.examinePivotRow() ); List tightenings; TS_ASSERT_THROWS_NOTHING( tightener.getRowTightenings( tightenings ) ); @@ -102,7 +102,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite void test_pivot_row__just_upper_tightend() { - RowBoundTightener tightener; + RowBoundTightener tightener( *tableau ); tableau->setDimensions( 2, 5 ); @@ -122,7 +122,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite tableau->setLowerBound( 4, 0 ); tableau->setUpperBound( 4, 0 ); - tightener.initialize( *tableau ); + tightener.setDimensions(); TableauRow row( 3 ); // 1 - x0 - x1 + 2x2 @@ -134,7 +134,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite tableau->nextPivotRow = &row; - TS_ASSERT_THROWS_NOTHING( tightener.examinePivotRow( *tableau ) ); + TS_ASSERT_THROWS_NOTHING( tightener.examinePivotRow() ); List tightenings; TS_ASSERT_THROWS_NOTHING( tightener.getRowTightenings( tightenings ) ); @@ -153,7 +153,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite void test_pivot_row__just_lower_tightend() { - RowBoundTightener tightener; + RowBoundTightener tightener( *tableau ); tableau->setDimensions( 2, 5 ); @@ -168,7 +168,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite tableau->setLowerBound( 4, 0 ); tableau->setUpperBound( 4, 0 ); - tightener.initialize( *tableau ); + tightener.setDimensions(); TableauRow row( 3 ); // 1 - x0 - x1 + 2x2 @@ -180,7 +180,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite tableau->nextPivotRow = &row; - TS_ASSERT_THROWS_NOTHING( tightener.examinePivotRow( *tableau ) ); + TS_ASSERT_THROWS_NOTHING( tightener.examinePivotRow() ); List tightenings; TS_ASSERT_THROWS_NOTHING( tightener.getRowTightenings( tightenings ) ); @@ -198,7 +198,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite void test_pivot_row__nothing_tightened() { - RowBoundTightener tightener; + RowBoundTightener tightener( *tableau ); tableau->setDimensions( 2, 5 ); @@ -213,7 +213,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite tableau->setLowerBound( 4, -100 ); tableau->setUpperBound( 4, 100 ); - tightener.initialize( *tableau ); + tightener.setDimensions(); TableauRow row( 3 ); // 1 - x0 - x1 + 2x2 @@ -225,7 +225,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite tableau->nextPivotRow = &row; - TS_ASSERT_THROWS_NOTHING( tightener.examinePivotRow( *tableau ) ); + TS_ASSERT_THROWS_NOTHING( tightener.examinePivotRow() ); List tightenings; TS_ASSERT_THROWS_NOTHING( tightener.getRowTightenings( tightenings ) ); @@ -235,7 +235,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite void test_examine_constraint_matrix_single_equation() { - RowBoundTightener tightener; + RowBoundTightener tightener( *tableau ); tableau->setDimensions( 1, 5 ); @@ -267,7 +267,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite x1 >= 1.5 */ - tightener.initialize( *tableau ); + tightener.setDimensions(); double A[] = { 1, -2, 0, 1, 2 }; double b[] = { 1 }; @@ -275,7 +275,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite tableau->A = A; tableau->b = b; - TS_ASSERT_THROWS_NOTHING( tightener.examineConstraintMatrix( *tableau, false ) ); + TS_ASSERT_THROWS_NOTHING( tightener.examineConstraintMatrix( false ) ); List tightenings; TS_ASSERT_THROWS_NOTHING( tightener.getRowTightenings( tightenings ) ); @@ -296,7 +296,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite void test_examine_constraint_matrix_multiple_equations() { - RowBoundTightener tightener; + RowBoundTightener tightener( *tableau ); tableau->setDimensions( 2, 5 ); @@ -332,7 +332,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite Equation 2 gives us that x2 <= 2, >= 1 */ - tightener.initialize( *tableau ); + tightener.setDimensions(); double A[] = { 1, 0, -2, -2, @@ -345,7 +345,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite tableau->A = A; tableau->b = b; - TS_ASSERT_THROWS_NOTHING( tightener.examineConstraintMatrix( *tableau, false ) ); + TS_ASSERT_THROWS_NOTHING( tightener.examineConstraintMatrix( false ) ); List tightenings; TS_ASSERT_THROWS_NOTHING( tightener.getRowTightenings( tightenings ) ); diff --git a/src/engine/tests/Test_Tableau.h b/src/engine/tests/Test_Tableau.h index 43f61f149..1cc89c86d 100644 --- a/src/engine/tests/Test_Tableau.h +++ b/src/engine/tests/Test_Tableau.h @@ -162,10 +162,8 @@ class TableauTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( tableau->setLowerBound( 6, 400 ) ); TS_ASSERT_THROWS_NOTHING( tableau->setUpperBound( 6, 402 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 4 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 5 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 6 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau() ); + List basics = { 4, 5, 6 }; + TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau( basics ) ); // All non-basics are set to lower bounds. TS_ASSERT_EQUALS( tableau->getValue( 0 ), 1.0 ); @@ -209,10 +207,6 @@ class TableauTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( tableau->setLowerBound( 6, 400 ) ); TS_ASSERT_THROWS_NOTHING( tableau->setUpperBound( 6, 402 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 4 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 5 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 6 ) ); - MockVariableWatcher watcher1; MockVariableWatcher watcher2; @@ -220,7 +214,8 @@ class TableauTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( tableau->registerToWatchVariable( &watcher1, 5 ) ); TS_ASSERT_THROWS_NOTHING( tableau->registerToWatchVariable( &watcher2, 5 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau() ); + List basics = { 4, 5, 6 }; + TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau( basics ) ); // The basic values get computed, so the watchers should be called @@ -270,10 +265,8 @@ class TableauTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( tableau->setLowerBound( 6, 400 ) ); TS_ASSERT_THROWS_NOTHING( tableau->setUpperBound( 6, 402 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 4 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 5 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 6 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau() ); + List basics = { 4, 5, 6 }; + TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau( basics ) ); TS_ASSERT_EQUALS( tableau->getBasicStatus( 4 ), Tableau::BELOW_LB ); TS_ASSERT_EQUALS( tableau->getBasicStatus( 5 ), Tableau::BETWEEN ); @@ -324,10 +317,8 @@ class TableauTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( tableau->setLowerBound( 6, 400 ) ); TS_ASSERT_THROWS_NOTHING( tableau->setUpperBound( 6, 412 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 4 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 5 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 6 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau() ); + List basics = { 4, 5, 6 }; + TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau( basics ) ); TS_ASSERT_EQUALS( tableau->getBasicStatus( 4 ), Tableau::BETWEEN ); TS_ASSERT_EQUALS( tableau->getBasicStatus( 5 ), Tableau::BELOW_LB ); @@ -378,10 +369,8 @@ class TableauTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( tableau->setLowerBound( 6, 400 ) ); TS_ASSERT_THROWS_NOTHING( tableau->setUpperBound( 6, 402 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 4 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 5 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 6 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau() ); + List basics = { 4, 5, 6 }; + TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau( basics ) ); TS_ASSERT_EQUALS( tableau->getBasicStatus( 4 ), Tableau::BELOW_LB ); TS_ASSERT_EQUALS( tableau->getBasicStatus( 5 ), Tableau::BETWEEN ); @@ -487,10 +476,8 @@ class TableauTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( tableau->setLowerBound( 6, 400 ) ); TS_ASSERT_THROWS_NOTHING( tableau->setUpperBound( 6, 402 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 4 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 5 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 6 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau() ); + List basics = { 4, 5, 6 }; + TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau( basics ) ); TS_ASSERT_THROWS_NOTHING( tableau->computeCostFunction() ); costFunctionManager.nextCostFunction = new double[4]; @@ -547,10 +534,8 @@ class TableauTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( tableau->setLowerBound( 6, 400 ) ); TS_ASSERT_THROWS_NOTHING( tableau->setUpperBound( 6, 402 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 4 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 5 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 6 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau() ); + List basics = { 4, 5, 6 }; + TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau( basics ) ); TS_ASSERT_THROWS_NOTHING( tableau->computeCostFunction() ); costFunctionManager.nextCostFunction = new double[4]; @@ -621,10 +606,8 @@ class TableauTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( tableau->setLowerBound( 6, 400 ) ); TS_ASSERT_THROWS_NOTHING( tableau->setUpperBound( 6, 402 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 4 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 5 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 6 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau() ); + List basics = { 4, 5, 6 }; + TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau( basics ) ); TableauRow row( 4 ); @@ -825,10 +808,8 @@ class TableauTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( tableau->setLowerBound( 6, 400 ) ); TS_ASSERT_THROWS_NOTHING( tableau->setUpperBound( 6, 402 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 4 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 5 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 6 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau() ); + List basics = { 4, 5, 6 }; + TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau( basics ) ); TS_ASSERT_THROWS_NOTHING( tableau->computeAssignment() ); @@ -1028,10 +1009,8 @@ class TableauTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( tableau->setLowerBound( 6, 200 ) ); TS_ASSERT_THROWS_NOTHING( tableau->setUpperBound( 6, 202 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 4 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 5 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 6 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau() ); + List basics = { 4, 5, 6 }; + TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau( basics ) ); TS_ASSERT_THROWS_NOTHING( tableau->computeCostFunction() ); costFunctionManager.nextCostFunction = new double[4]; @@ -1149,10 +1128,8 @@ class TableauTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( tableau->setLowerBound( 6, 400 ) ); TS_ASSERT_THROWS_NOTHING( tableau->setUpperBound( 6, 402 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 4 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 5 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 6 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau() ); + List basics = { 4, 5, 6 }; + TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau( basics ) ); // Do a pivot to shuffle the basis tableau->setEnteringVariableIndex( 2u ); @@ -1304,10 +1281,8 @@ class TableauTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( tableau->setLowerBound( 6, 400 ) ); TS_ASSERT_THROWS_NOTHING( tableau->setUpperBound( 6, 402 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 4 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 5 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 6 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau() ); + List basics = { 4, 5, 6 }; + TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau( basics ) ); for ( unsigned i = 0; i < 4; ++i ) { @@ -1384,10 +1359,8 @@ class TableauTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( tableau->setLowerBound( 6, 400 ) ); TS_ASSERT_THROWS_NOTHING( tableau->setUpperBound( 6, 402 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 4 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 5 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->markAsBasic( 6 ) ); - TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau() ); + List basics = { 4, 5, 6 }; + TS_ASSERT_THROWS_NOTHING( tableau->initializeTableau( basics ) ); TS_ASSERT_THROWS_NOTHING( tableau->computeCostFunction() ); costFunctionManager.nextCostFunction = new double[4];