| 120 | } |
| 121 | |
| 122 | void DeepPolyAnalysis::run() |
| 123 | { |
| 124 | struct timespec deepPolyStart; |
| 125 | (void)deepPolyStart; |
| 126 | struct timespec deepPolyEnd; |
| 127 | (void)deepPolyEnd; |
| 128 | |
| 129 | deepPolyStart = TimeUtils::sampleMicro(); |
| 130 | |
| 131 | const Map<unsigned, Layer *> &layers = _layerOwner->getLayerIndexToLayer(); |
| 132 | for ( const auto &pair : layers ) |
| 133 | { |
| 134 | /* |
| 135 | Go over the layers, one by one. Each time construct and execute |
| 136 | the abstract element. |
| 137 | */ |
| 138 | unsigned index = pair.first; |
| 139 | Layer *layer = pair.second; |
| 140 | |
| 141 | ASSERT( _deepPolyElements.exists( index ) ); |
| 142 | log( Stringf( "Running deeppoly analysis for layer %u...", index ) ); |
| 143 | DeepPolyElement *deepPolyElement = _deepPolyElements[index]; |
| 144 | deepPolyElement->execute( _deepPolyElements ); |
| 145 | |
| 146 | // Extract updated bounds |
| 147 | for ( unsigned j = 0; j < deepPolyElement->getSize(); ++j ) |
| 148 | { |
| 149 | if ( layer->neuronEliminated( j ) ) |
| 150 | continue; |
| 151 | double lb = deepPolyElement->getLowerBound( j ); |
| 152 | if ( layer->getLb( j ) < lb ) |
| 153 | { |
| 154 | log( Stringf( "Neuron %u_%u lower-bound updated from %f to %f", |
| 155 | index, |
| 156 | j, |
| 157 | layer->getLb( j ), |
| 158 | lb ) ); |
| 159 | layer->setLb( j, lb ); |
| 160 | _layerOwner->receiveTighterBound( |
| 161 | Tightening( layer->neuronToVariable( j ), lb, Tightening::LB ) ); |
| 162 | } |
| 163 | double ub = deepPolyElement->getUpperBound( j ); |
| 164 | if ( layer->getUb( j ) > ub ) |
| 165 | { |
| 166 | log( Stringf( "Neuron %u_%u upper-bound updated from %f to %f", |
| 167 | index, |
| 168 | j, |
| 169 | layer->getUb( j ), |
| 170 | ub ) ); |
| 171 | layer->setUb( j, ub ); |
| 172 | _layerOwner->receiveTighterBound( |
| 173 | Tightening( layer->neuronToVariable( j ), ub, Tightening::UB ) ); |
| 174 | } |
| 175 | } |
| 176 | log( Stringf( "Running deeppoly analysis for layer %u - done", index ) ); |
| 177 | } |
| 178 | } |
| 179 |
no test coverage detected