Method solve

src/engine/Engine.cpp:190–456

}

bool Engine::solve( double timeoutInSeconds )
{
    SignalHandler::getInstance()->initialize();
    SignalHandler::getInstance()->registerClient( this );

    // Register the boundManager with all the PL constraints
    for ( auto &plConstraint : _plConstraints )
        plConstraint->registerBoundManager( &_boundManager );
    for ( auto &nlConstraint : _nlConstraints )
        nlConstraint->registerBoundManager( &_boundManager );

    // Before encoding, make sure all valid constraints are applied.
    applyAllValidConstraintCaseSplits();

    if ( _solveWithMILP )
        return solveWithMILPEncoding( timeoutInSeconds );

    updateDirections();
    if ( _lpSolverType == LPSolverType::NATIVE )
        storeInitialEngineState();
    else if ( _lpSolverType == LPSolverType::GUROBI )
    {
        ENGINE_LOG( "Encoding convex relaxation into Gurobi..." );
        _gurobi = std::unique_ptr<GurobiWrapper>( new GurobiWrapper() );
        _tableau->setGurobi( &( *_gurobi ) );
        _milpEncoder = std::unique_ptr<MILPEncoder>( new MILPEncoder( *_tableau ) );
        _milpEncoder->setStatistics( &_statistics );
        _milpEncoder->encodeInputQuery( *_gurobi, *_preprocessedQuery, true );
        ENGINE_LOG( "Encoding convex relaxation into Gurobi - done" );
    }

    mainLoopStatistics();
    if ( _verbosity > 0 )
    {
        printf( "\nEngine::solve: Initial statistics\n" );
        _statistics.print();
        printf( "\n---\n" );
    }

    bool splitJustPerformed = true;
    struct timespec mainLoopStart = TimeUtils::sampleMicro();
    while ( true )
    {
        struct timespec mainLoopEnd = TimeUtils::sampleMicro();
        _statistics.incLongAttribute( Statistics::TIME_MAIN_LOOP_MICRO,
                                      TimeUtils::timePassed( mainLoopStart, mainLoopEnd ) );
        mainLoopStart = mainLoopEnd;

        if ( shouldExitDueToTimeout( timeoutInSeconds ) )
        {
            if ( _verbosity > 0 )
            {
                printf( "\n\nEngine: quitting due to timeout...\n\n" );
                printf( "Final statistics:\n" );
                _statistics.print();
            }

            _exitCode = Engine::TIMEOUT;