| 75 | } |
| 76 | |
| 77 | void DnCWorker::popOneSubQueryAndSolve( bool restoreTreeStates ) |
| 78 | { |
| 79 | SubQuery *subQuery = NULL; |
| 80 | // Boost queue stores the next element into the passed-in pointer |
| 81 | // and returns true if the pop is successful (aka, the queue is not empty |
| 82 | // in most cases) |
| 83 | if ( _workload->pop( subQuery ) ) |
| 84 | { |
| 85 | String queryId = subQuery->_queryId; |
| 86 | unsigned depth = subQuery->_depth; |
| 87 | auto split = std::move( subQuery->_split ); |
| 88 | std::unique_ptr<SmtState> smtState = nullptr; |
| 89 | if ( restoreTreeStates && subQuery->_smtState ) |
| 90 | smtState = std::move( subQuery->_smtState ); |
| 91 | unsigned timeoutInSeconds = subQuery->_timeoutInSeconds; |
| 92 | |
| 93 | // Reset the engine state |
| 94 | _engine->restoreState( *_initialState ); |
| 95 | _engine->reset(); |
| 96 | |
| 97 | // TODO: each worker is going to keep a map from *CaseSplit to an |
| 98 | // object of class DnCStatistics, which contains some basic |
| 99 | // statistics. The maps are owned by the DnCManager. |
| 100 | |
| 101 | // Apply the split and solve |
| 102 | _engine->applySnCSplit( *split, queryId ); |
| 103 | |
| 104 | bool fullSolveNeeded = true; // denotes whether we need to solve the subquery |
| 105 | if ( restoreTreeStates && smtState ) |
| 106 | fullSolveNeeded = _engine->restoreSmtState( *smtState ); |
| 107 | IEngine::ExitCode result = IEngine::NOT_DONE; |
| 108 | if ( fullSolveNeeded ) |
| 109 | { |
| 110 | _engine->solve( timeoutInSeconds ); |
| 111 | result = _engine->getExitCode(); |
| 112 | } |
| 113 | else |
| 114 | { |
| 115 | // UNSAT is proven when replaying stack-entries |
| 116 | result = IEngine::UNSAT; |
| 117 | } |
| 118 | |
| 119 | if ( _verbosity > 0 ) |
| 120 | printProgress( queryId, result ); |
| 121 | // Switch on the result |
| 122 | if ( result == IEngine::UNSAT ) |
| 123 | { |
| 124 | // If UNSAT, continue to solve |
| 125 | *_numUnsolvedSubQueries -= 1; |
| 126 | if ( _numUnsolvedSubQueries->load() == 0 || _parallelDeepSoI ) |
| 127 | *_shouldQuitSolving = true; |
| 128 | delete subQuery; |
| 129 | } |
| 130 | else if ( result == IEngine::TIMEOUT ) |
| 131 | { |
| 132 | // If TIMEOUT, split the current input region and add the |
| 133 | // new subQueries to the current queue |
| 134 | SubQueries subQueries; |