Method restoreState

src/engine/Engine.cpp:1845–1877

}

void Engine::restoreState( const EngineState &state )
{
    ENGINE_LOG( "Restore state starting" );

    if ( state._tableauStateStorageLevel == TableauStateStorageLevel::STORE_NONE )
        throw MarabouError( MarabouError::RESTORING_ENGINE_FROM_INVALID_STATE );

    ENGINE_LOG( "\tRestoring tableau state" );
    _tableau->restoreState( state._tableauState, state._tableauStateStorageLevel );

    ENGINE_LOG( "\tRestoring constraint states" );
    for ( auto &constraint : _plConstraints )
    {
        if ( !state._plConstraintToState.exists( constraint ) )
            throw MarabouError( MarabouError::MISSING_PL_CONSTRAINT_STATE );

        constraint->restoreState( state._plConstraintToState[constraint] );
    }

    _numPlConstraintsDisabledByValidSplits = state._numPlConstraintsDisabledByValidSplits;

    if ( _lpSolverType == LPSolverType::NATIVE )
    {
        // Make sure the data structures are initialized to the correct size
        _rowBoundTightener->setDimensions();
        adjustWorkMemorySize();
        _activeEntryStrategy->resizeHook( _tableau );
        _costFunctionManager->initialize();
    }

    // Reset the violation counts in the SMT core
    _smtCore.resetSplitConditions();
}

void Engine::setNumPlConstraintsDisabledByValidSplits( unsigned numConstraints )
{