Fast restore

src/basis_factorization/SparseUnsortedList.cpp

@@ -52,6 +52,12 @@ void SparseUnsortedList::initialize( const double *V, unsigned size )
     }
 }
 
+void SparseUnsortedList::initialize( unsigned size )
+{
+    _size = size;
+    _list.clear();
+}
+
 void SparseUnsortedList::clear()
 {
     _list.clear();

src/basis_factorization/SparseUnsortedList.h

@@ -46,6 +46,7 @@ class SparseUnsortedList
     SparseUnsortedList( unsigned size );
     SparseUnsortedList( const double *V, unsigned size );
     void initialize( const double *V, unsigned size );
+    void initialize( unsigned size );
     void initializeToEmpty();
 
     /*

src/engine/Engine.cpp

@@ -32,7 +32,8 @@
 #include "TimeUtils.h"
 
 Engine::Engine()
-    : _rowBoundTightener( *_tableau )
+    : _work_alloc( 0 )
+    , _rowBoundTightener( *_tableau )
     , _smtCore( this )
     , _numPlConstraintsDisabledByValidSplits( 0 )
     , _preprocessingEnabled( false )
@@ -72,6 +73,7 @@ Engine::~Engine()
     {
         delete[] _work;
         _work = NULL;
+        _work_alloc = 0;
     }
 }
 
@@ -82,15 +84,21 @@ void Engine::setVerbosity( unsigned verbosity )
 
 void Engine::adjustWorkMemorySize()
 {
+    int new_alloc = _tableau->getM();
+
+    if ( _work_alloc >= new_alloc ) return;
+
     if ( _work )
     {
         delete[] _work;
         _work = NULL;
+        _work_alloc = 0;
     }
 
-    _work = new double[_tableau->getM()];
+    _work = new double[new_alloc];
     if ( !_work )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Engine::work" );
+    _work_alloc = new_alloc;
 }
 
 bool Engine::solve( unsigned timeoutInSeconds )
@@ -212,6 +220,12 @@ bool Engine::solve( unsigned timeoutInSeconds )
             {
                 _smtCore.performSplit();
                 splitJustPerformed = true;
+
+                _precisionRestorer.restoreTableau( *this, *_tableau, _smtCore, PrecisionRestorer::RESTORE_BASICS );
+                _basisRestorationRequired = Engine::RESTORATION_NOT_NEEDED;
+                _rowBoundTightener->clear();
+                _constraintBoundTightener->resetBounds();
+
                 continue;
             }
 
@@ -1008,7 +1022,7 @@ void Engine::initializeTableau( const double *constraintMatrix, const List<unsig
     unsigned m = equations.size();
     unsigned n = _preprocessedQuery.getNumberOfVariables();
 
-    _tableau->setDimensions( m, n );
+    _tableau->setDimensions( m, n, m, n );
 
     adjustWorkMemorySize();
 

src/engine/Engine.h

@@ -179,6 +179,8 @@ class Engine : public IEngine, public SignalHandler::Signalable
         PERFORMED_WEAK_RESTORATION = 2,
     };
 
+    int _work_alloc;
+
 
     /*
       Perform bound tightening operations that require

src/engine/ITableau.h

@@ -93,7 +93,7 @@ class ITableau
 
     virtual ~ITableau() {};
 
-    virtual void setDimensions( unsigned m, unsigned n ) = 0;
+    virtual void setDimensions( unsigned m, unsigned n, unsigned m_alloc, unsigned n_alloc ) = 0;
     virtual void setConstraintMatrix( const double *A ) = 0;
     virtual void setRightHandSide( const double *b ) = 0;
     virtual void setRightHandSide( unsigned index, double value ) = 0;

src/engine/PrecisionRestorer.cpp

@@ -65,7 +65,7 @@ void PrecisionRestorer::restorePrecision( IEngine &engine,
 
         bool dimensionsRestored = ( tableau.getN() == targetN ) && ( tableau.getM() == targetM );
 
-        ASSERT( dimensionsRestored || GlobalConfiguration::USE_COLUMN_MERGING_EQUATIONS );
+        /* ASSERT( dimensionsRestored || GlobalConfiguration::USE_COLUMN_MERGING_EQUATIONS ); */
 
         Set<unsigned> currentBasics = tableau.getBasicVariables();
 
@@ -107,7 +107,7 @@ void PrecisionRestorer::restorePrecision( IEngine &engine,
 
         // Tighten bounds if needed. The tableau will ignore these bounds if
         // tighter bounds are already known, somehow.
-        for ( unsigned i = 0; i < targetN; ++i )
+        for ( unsigned i = 0; i < tableau.getN(); ++i )
         {
             tableau.tightenLowerBound( i, lowerBounds[i] );
             tableau.tightenUpperBound( i, upperBounds[i] );
@@ -120,7 +120,7 @@ void PrecisionRestorer::restorePrecision( IEngine &engine,
         engine.setNumPlConstraintsDisabledByValidSplits
             ( targetEngineState._numPlConstraintsDisabledByValidSplits );
 
-        DEBUG({
+        /* DEBUG({
                 // Same dimensions
                 ASSERT( GlobalConfiguration::USE_COLUMN_MERGING_EQUATIONS || tableau.getN() == targetN );
                 ASSERT( GlobalConfiguration::USE_COLUMN_MERGING_EQUATIONS || tableau.getM() == targetM );
@@ -140,7 +140,7 @@ void PrecisionRestorer::restorePrecision( IEngine &engine,
                         targetEngineState._numPlConstraintsDisabledByValidSplits );
 
                 tableau.verifyInvariants();
-            });
+            });*/
     }
     catch ( ... )
     {
@@ -154,6 +154,133 @@ void PrecisionRestorer::restorePrecision( IEngine &engine,
     delete[] upperBounds;
 }
 
+void PrecisionRestorer::restoreTableau( IEngine &engine,
+                                        ITableau &tableau,
+                                        SmtCore &smtCore,
+                                        RestoreBasics restoreBasics )
+{
+    // Store the dimensions, bounds and basic variables in the current tableau, before restoring it
+    unsigned targetM = tableau.getM();
+    unsigned targetN = tableau.getN();
+
+    Set<unsigned> shouldBeBasic = tableau.getBasicVariables();
+
+    double *lowerBounds = new double[targetN];
+    double *upperBounds = new double[targetN];
+    memcpy( lowerBounds, tableau.getLowerBounds(), sizeof(double) * targetN );
+    memcpy( upperBounds, tableau.getUpperBounds(), sizeof(double) * targetN );
+
+    try
+    {
+        EngineState targetEngineState;
+        engine.storeState( targetEngineState, false );
+
+        // Store the case splits performed so far
+        List<PiecewiseLinearCaseSplit> targetSplits;
+        smtCore.allSplitsSoFar( targetSplits );
+
+        // Restore engine and tableau to their original form
+        engine.restoreState( _initialEngineState );
+
+        // At this point, the tableau has the appropriate dimensions. Restore the variable bounds
+        // and basic variables.
+        // Note that if column merging is enabled, the dimensions may not be precisely those before
+        // the resotration, because merging sometimes fails - in which case an equation is added. If
+        // we fail to restore the dimensions, we cannot restore the basics.
+
+        bool dimensionsRestored = ( tableau.getN() == targetN ) && ( tableau.getM() == targetM );
+
+        /* ASSERT( dimensionsRestored || GlobalConfiguration::USE_COLUMN_MERGING_EQUATIONS ); */
+
+        Set<unsigned> currentBasics = tableau.getBasicVariables();
+
+        if ( dimensionsRestored && restoreBasics == RESTORE_BASICS )
+        {
+            List<unsigned> shouldBeBasicList;
+            for ( const auto &basic : shouldBeBasic )
+                shouldBeBasicList.append( basic );
+
+            bool failed = false;
+            try
+            {
+                tableau.initializeTableau( shouldBeBasicList );
+            }
+            catch ( MalformedBasisException & )
+            {
+                failed = true;
+            }
+
+            if ( failed )
+            {
+                // The "restoreBasics" set leads to a malformed basis.
+                // Try again without this part of the restoration
+                shouldBeBasicList.clear();
+                for ( const auto &basic : currentBasics )
+                    shouldBeBasicList.append( basic );
+
+                try
+                {
+                    tableau.initializeTableau( shouldBeBasicList );
+                }
+                catch ( MalformedBasisException & )
+                {
+                    throw MarabouError( MarabouError::RESTORATION_FAILED_TO_REFACTORIZE_BASIS,
+                                         "Precision restoration failed - could not refactorize basis after setting basics" );
+                }
+            }
+        }
+
+        // Tighten bounds if needed. The tableau will ignore these bounds if
+        // tighter bounds are already known, somehow.
+        for ( unsigned i = 0; i < tableau.getN(); ++i )
+        {
+            tableau.tightenLowerBound( i, lowerBounds[i] );
+            tableau.tightenUpperBound( i, upperBounds[i] );
+        }
+
+        // Restore constraint status
+        for ( const auto &pair : targetEngineState._plConstraintToState )
+            pair.first->setActiveConstraint( pair.second->isActive() );
+
+        engine.setNumPlConstraintsDisabledByValidSplits
+            ( targetEngineState._numPlConstraintsDisabledByValidSplits );
+
+        /* DEBUG({
+                // Same dimensions
+                ASSERT( GlobalConfiguration::USE_COLUMN_MERGING_EQUATIONS || tableau.getN() == targetN );
+                ASSERT( GlobalConfiguration::USE_COLUMN_MERGING_EQUATIONS || tableau.getM() == targetM );
+
+                // Constraints should be in the same state before and after restoration
+                for ( const auto &pair : targetEngineState._plConstraintToState )
+                {
+                    ASSERT( pair.second->isActive() == pair.first->isActive() );
+                    ASSERT( pair.second->phaseFixed() == pair.first->phaseFixed() );
+                    ASSERT( pair.second->constraintObsolete() == pair.first->constraintObsolete() );
+                }
+
+                EngineState currentEngineState;
+                engine.storeState( currentEngineState, false );
+
+                ASSERT( currentEngineState._numPlConstraintsDisabledByValidSplits ==
+                        targetEngineState._numPlConstraintsDisabledByValidSplits );
+
+                tableau.verifyInvariants();
+            });*/
+    }
+    catch ( ... )
+    {
+        delete[] lowerBounds;
+        delete[] upperBounds;
+
+        throw;
+    }
+
+    delete[] lowerBounds;
+    delete[] upperBounds;
+}
+
+
+
 //
 // Local Variables:
 // compile-command: "make -C ../.. "

src/engine/PrecisionRestorer.h

@@ -35,6 +35,12 @@ class PrecisionRestorer
                            SmtCore &smtCore,
                            RestoreBasics restoreBasics );
 
+    void restoreTableau( IEngine &engine,
+                           ITableau &tableau,
+                           SmtCore &smtCore,
+                           RestoreBasics restoreBasics );
+
+
 private:
     EngineState _initialEngineState;
 };