| 162 | } |
| 163 | |
| 164 | void CDSmtCore::decideSplit( PiecewiseLinearConstraint *constraint ) |
| 165 | { |
| 166 | struct timespec start = TimeUtils::sampleMicro(); |
| 167 | |
| 168 | if ( _statistics ) |
| 169 | { |
| 170 | _statistics->incUnsignedAttribute( Statistics::NUM_SPLITS ); |
| 171 | _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); |
| 172 | } |
| 173 | |
| 174 | if ( !constraint->isFeasible() ) |
| 175 | throw MarabouError( MarabouError::DEBUGGING_ERROR ); |
| 176 | ASSERT( constraint->isFeasible() ); |
| 177 | ASSERT( !constraint->isImplication() ); |
| 178 | |
| 179 | PhaseStatus decision = constraint->nextFeasibleCase(); |
| 180 | pushDecision( constraint, decision ); |
| 181 | |
| 182 | if ( _statistics ) |
| 183 | { |
| 184 | unsigned level = _context.getLevel(); |
| 185 | _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, level ); |
| 186 | if ( level > _statistics->getUnsignedAttribute( Statistics::MAX_DECISION_LEVEL ) ) |
| 187 | _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, level ); |
| 188 | |
| 189 | struct timespec end = TimeUtils::sampleMicro(); |
| 190 | _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, |
| 191 | TimeUtils::timePassed( start, end ) ); |
| 192 | } |
| 193 | SMT_LOG( "Performing a ReLU split - DONE" ); |
| 194 | } |
| 195 | |
| 196 | |
| 197 | unsigned CDSmtCore::getDecisionLevel() const |
nothing calls this directly
no test coverage detected