| 997 | } |
| 998 | |
| 999 | void Engine::invokePreprocessor( const InputQuery &inputQuery, bool preprocess ) |
| 1000 | { |
| 1001 | if ( _verbosity > 0 ) |
| 1002 | printf( "Engine::processInputQuery: Input query (before preprocessing): " |
| 1003 | "%u equations, %u variables\n", |
| 1004 | inputQuery.getEquations().size(), |
| 1005 | inputQuery.getNumberOfVariables() ); |
| 1006 | |
| 1007 | // If processing is enabled, invoke the preprocessor |
| 1008 | _preprocessingEnabled = preprocess; |
| 1009 | if ( _preprocessingEnabled ) |
| 1010 | _preprocessedQuery = _preprocessor.preprocess( |
| 1011 | inputQuery, GlobalConfiguration::PREPROCESSOR_ELIMINATE_VARIABLES ); |
| 1012 | else |
| 1013 | _preprocessedQuery = std::unique_ptr<InputQuery>( new InputQuery( inputQuery ) ); |
| 1014 | |
| 1015 | if ( _verbosity > 0 ) |
| 1016 | printf( "Engine::processInputQuery: Input query (after preprocessing): " |
| 1017 | "%u equations, %u variables\n\n", |
| 1018 | _preprocessedQuery->getEquations().size(), |
| 1019 | _preprocessedQuery->getNumberOfVariables() ); |
| 1020 | |
| 1021 | unsigned infiniteBounds = _preprocessedQuery->countInfiniteBounds(); |
| 1022 | if ( infiniteBounds != 0 ) |
| 1023 | { |
| 1024 | _exitCode = Engine::ERROR; |
| 1025 | throw MarabouError( MarabouError::UNBOUNDED_VARIABLES_NOT_YET_SUPPORTED, |
| 1026 | Stringf( "Error! Have %u infinite bounds", infiniteBounds ).ascii() ); |
| 1027 | } |
| 1028 | } |
| 1029 | |
| 1030 | void Engine::printInputBounds( const InputQuery &inputQuery ) const |
| 1031 | { |
nothing calls this directly
no test coverage detected