Return true if stack is currently compliant, false otherwise If there is no stored solution, return false --- incompliant.
| 425 | // Return true if stack is currently compliant, false otherwise |
| 426 | // If there is no stored solution, return false --- incompliant. |
| 427 | bool SmtCore::checkSkewFromDebuggingSolution() |
| 428 | { |
| 429 | if ( _debuggingSolution.empty() ) |
| 430 | return false; |
| 431 | |
| 432 | String error; |
| 433 | |
| 434 | // First check that the valid splits implied at the root level are okay |
| 435 | for ( const auto &split : _impliedValidSplitsAtRoot ) |
| 436 | { |
| 437 | if ( !splitAllowsStoredSolution( split, error ) ) |
| 438 | { |
| 439 | printf( "Error with one of the splits implied at root level:\n\t%s\n", error.ascii() ); |
| 440 | throw MarabouError( MarabouError::DEBUGGING_ERROR ); |
| 441 | } |
| 442 | } |
| 443 | |
| 444 | // Now go over the stack from oldest to newest and check that each level is compliant |
| 445 | for ( const auto &stackEntry : _stack ) |
| 446 | { |
| 447 | // If the active split is non-compliant but there are alternatives, that's fine |
| 448 | if ( !splitAllowsStoredSolution( stackEntry->_activeSplit, error ) ) |
| 449 | { |
| 450 | if ( stackEntry->_alternativeSplits.empty() ) |
| 451 | { |
| 452 | printf( "Error! Have a split that is non-compliant with the stored solution, " |
| 453 | "without alternatives:\n\t%s\n", |
| 454 | error.ascii() ); |
| 455 | throw MarabouError( MarabouError::DEBUGGING_ERROR ); |
| 456 | } |
| 457 | |
| 458 | // Active split is non-compliant but this is fine, because there are alternatives. We're |
| 459 | // done. |
| 460 | return false; |
| 461 | } |
| 462 | |
| 463 | // Did we learn any valid splits that are non-compliant? |
| 464 | for ( auto const &split : stackEntry->_impliedValidSplits ) |
| 465 | { |
| 466 | if ( !splitAllowsStoredSolution( split, error ) ) |
| 467 | { |
| 468 | printf( "Error with one of the splits implied at this stack level:\n\t%s\n", |
| 469 | error.ascii() ); |
| 470 | throw MarabouError( MarabouError::DEBUGGING_ERROR ); |
| 471 | } |
| 472 | } |
| 473 | } |
| 474 | |
| 475 | // No problems were detected, the stack is compliant with the stored solution |
| 476 | return true; |
| 477 | } |
| 478 | |
| 479 | bool SmtCore::splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, |
| 480 | String &error ) const |
no test coverage detected