Return true if stack is currently compliant, false otherwise If there is no stored solution, return false --- incompliant.
| 316 | // Return true if stack is currently compliant, false otherwise |
| 317 | // If there is no stored solution, return false --- incompliant. |
| 318 | bool CDSmtCore::checkSkewFromDebuggingSolution() |
| 319 | { |
| 320 | if ( _debuggingSolution.empty() ) |
| 321 | return false; |
| 322 | |
| 323 | String error; |
| 324 | |
| 325 | int decisionLevel = 0; |
| 326 | bool isDecision = false; |
| 327 | // First check that the valid splits implied at the root level are okay |
| 328 | for ( const auto &trailEntry : _trail ) |
| 329 | { |
| 330 | if ( trailEntry._pwlConstraint != _decisions[decisionLevel]._pwlConstraint ) |
| 331 | isDecision = false; |
| 332 | else |
| 333 | { |
| 334 | ASSERT( trailEntry._phase == _decisions[decisionLevel]._phase ); |
| 335 | isDecision = true; |
| 336 | ++decisionLevel; |
| 337 | } |
| 338 | |
| 339 | PiecewiseLinearCaseSplit caseSplit = trailEntry.getPiecewiseLinearCaseSplit(); |
| 340 | if ( decisionLevel == 0 ) |
| 341 | { |
| 342 | if ( !splitAllowsStoredSolution( caseSplit, error ) ) |
| 343 | { |
| 344 | printf( "Error with one of the splits implied at root level:\n\t%s\n", |
| 345 | error.ascii() ); |
| 346 | throw MarabouError( MarabouError::DEBUGGING_ERROR ); |
| 347 | } |
| 348 | } |
| 349 | else |
| 350 | { |
| 351 | // If the active split is non-compliant but there are alternatives, |
| 352 | // i.e. it was a decision, that's fine |
| 353 | if ( isDecision && !splitAllowsStoredSolution( caseSplit, error ) ) |
| 354 | { |
| 355 | // Active split is non-compliant but this is fine, because there |
| 356 | // are alternatives. We're done. |
| 357 | return false; |
| 358 | } |
| 359 | else // Implied split |
| 360 | { |
| 361 | if ( !splitAllowsStoredSolution( caseSplit, error ) ) |
| 362 | { |
| 363 | printf( "Error with one of the splits implied at this stack level:\n\t%s\n", |
| 364 | error.ascii() ); |
| 365 | throw MarabouError( MarabouError::DEBUGGING_ERROR ); |
| 366 | } |
| 367 | } |
| 368 | } |
| 369 | } |
| 370 | |
| 371 | // No problems were detected, the stack is compliant with the stored solution |
| 372 | return true; |
| 373 | } |
| 374 | |
| 375 | bool CDSmtCore::splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, |
nothing calls this directly
no test coverage detected