| 36 | #include <random> |
| 37 | |
| 38 | Engine::Engine() |
| 39 | : _context() |
| 40 | , _boundManager( _context ) |
| 41 | , _tableau( _boundManager ) |
| 42 | , _preprocessedQuery( nullptr ) |
| 43 | , _rowBoundTightener( *_tableau ) |
| 44 | , _smtCore( this ) |
| 45 | , _numPlConstraintsDisabledByValidSplits( 0 ) |
| 46 | , _preprocessingEnabled( false ) |
| 47 | , _initialStateStored( false ) |
| 48 | , _work( NULL ) |
| 49 | , _basisRestorationRequired( Engine::RESTORATION_NOT_NEEDED ) |
| 50 | , _basisRestorationPerformed( Engine::NO_RESTORATION_PERFORMED ) |
| 51 | , _costFunctionManager( _tableau ) |
| 52 | , _quitRequested( false ) |
| 53 | , _exitCode( Engine::NOT_DONE ) |
| 54 | , _numVisitedStatesAtPreviousRestoration( 0 ) |
| 55 | , _networkLevelReasoner( NULL ) |
| 56 | , _verbosity( Options::get()->getInt( Options::VERBOSITY ) ) |
| 57 | , _lastNumVisitedStates( 0 ) |
| 58 | , _lastIterationWithProgress( 0 ) |
| 59 | , _symbolicBoundTighteningType( Options::get()->getSymbolicBoundTighteningType() ) |
| 60 | , _solveWithMILP( Options::get()->getBool( Options::SOLVE_WITH_MILP ) ) |
| 61 | , _lpSolverType( Options::get()->getLPSolverType() ) |
| 62 | , _gurobi( nullptr ) |
| 63 | , _milpEncoder( nullptr ) |
| 64 | , _soiManager( nullptr ) |
| 65 | , _simulationSize( Options::get()->getInt( Options::NUMBER_OF_SIMULATIONS ) ) |
| 66 | , _isGurobyEnabled( Options::get()->gurobiEnabled() ) |
| 67 | , _performLpTighteningAfterSplit( |
| 68 | Options::get()->getBool( Options::PERFORM_LP_TIGHTENING_AFTER_SPLIT ) ) |
| 69 | , _milpSolverBoundTighteningType( Options::get()->getMILPSolverBoundTighteningType() ) |
| 70 | , _sncMode( false ) |
| 71 | , _queryId( "" ) |
| 72 | , _produceUNSATProofs( Options::get()->getBool( Options::PRODUCE_PROOFS ) ) |
| 73 | , _groundBoundManager( _context ) |
| 74 | , _UNSATCertificate( NULL ) |
| 75 | { |
| 76 | _smtCore.setStatistics( &_statistics ); |
| 77 | _tableau->setStatistics( &_statistics ); |
| 78 | _rowBoundTightener->setStatistics( &_statistics ); |
| 79 | _preprocessor.setStatistics( &_statistics ); |
| 80 | |
| 81 | _activeEntryStrategy = _projectedSteepestEdgeRule; |
| 82 | _activeEntryStrategy->setStatistics( &_statistics ); |
| 83 | _statistics.stampStartingTime(); |
| 84 | setRandomSeed( Options::get()->getInt( Options::SEED ) ); |
| 85 | |
| 86 | _boundManager.registerEngine( this ); |
| 87 | _groundBoundManager.registerEngine( this ); |
| 88 | _statisticsPrintingFrequency = ( _lpSolverType == LPSolverType::NATIVE ) |
| 89 | ? GlobalConfiguration::STATISTICS_PRINTING_FREQUENCY |
| 90 | : GlobalConfiguration::STATISTICS_PRINTING_FREQUENCY_GUROBI; |
| 91 | |
| 92 | _UNSATCertificateCurrentPointer = |
| 93 | _produceUNSATProofs ? new ( true ) |
| 94 | CVC4::context::CDO<UnsatCertificateNode *>( &_context, NULL ) |
| 95 | : NULL; |
nothing calls this directly
no test coverage detected