Method solveWithMILPEncoding

src/engine/Engine.cpp:2940–2997

}

bool Engine::solveWithMILPEncoding( double timeoutInSeconds )
{
    try
    {
        if ( _lpSolverType == LPSolverType::NATIVE && _tableau->basisMatrixAvailable() )
        {
            explicitBasisBoundTightening();
            applyAllBoundTightenings();
            applyAllValidConstraintCaseSplits();
        }

        while ( applyAllValidConstraintCaseSplits() )
        {
            performSymbolicBoundTightening();
        }
    }
    catch ( const InfeasibleQueryException & )
    {
        _exitCode = Engine::UNSAT;
        return false;
    }

    ENGINE_LOG( "Encoding the input query with Gurobi...\n" );
    _gurobi = std::unique_ptr<GurobiWrapper>( new GurobiWrapper() );
    _tableau->setGurobi( &( *_gurobi ) );
    _milpEncoder = std::unique_ptr<MILPEncoder>( new MILPEncoder( *_tableau ) );
    _milpEncoder->encodeInputQuery( *_gurobi, *_preprocessedQuery );
    ENGINE_LOG( "Query encoded in Gurobi...\n" );

    double timeoutForGurobi = ( timeoutInSeconds == 0 ? FloatUtils::infinity() : timeoutInSeconds );
    ENGINE_LOG( Stringf( "Gurobi timeout set to %f\n", timeoutForGurobi ).ascii() )
    _gurobi->setTimeLimit( timeoutForGurobi );
    if ( !_sncMode )
        _gurobi->setNumberOfThreads( Options::get()->getInt( Options::NUM_WORKERS ) );
    _gurobi->setVerbosity( _verbosity > 0 );
    _gurobi->solve();

    if ( _gurobi->haveFeasibleSolution() )
    {
        if ( allNonlinearConstraintsHold() )
        {
            _exitCode = IEngine::SAT;
            return true;
        }
        else
        {
            _exitCode = IEngine::UNKNOWN;
            return false;
        }
    }
    else if ( _gurobi->infeasible() )
        _exitCode = IEngine::UNSAT;
    else if ( _gurobi->timeout() )
        _exitCode = IEngine::TIMEOUT;
    else
        throw NLRError( NLRError::UNEXPECTED_RETURN_STATUS_FROM_GUROBI );
    return false;
}