| 3717 | } |
| 3718 | |
| 3719 | const Vector<double> Engine::computeContradiction( unsigned infeasibleVar ) const |
| 3720 | { |
| 3721 | ASSERT( _produceUNSATProofs ); |
| 3722 | |
| 3723 | unsigned m = _tableau->getM(); |
| 3724 | SparseUnsortedList upperBoundExplanation( 0 ); |
| 3725 | SparseUnsortedList lowerBoundExplanation( 0 ); |
| 3726 | |
| 3727 | if ( !_boundManager.isExplanationTrivial( infeasibleVar, Tightening::UB ) ) |
| 3728 | upperBoundExplanation = _boundManager.getExplanation( infeasibleVar, Tightening::UB ); |
| 3729 | |
| 3730 | if ( !_boundManager.isExplanationTrivial( infeasibleVar, Tightening::LB ) ) |
| 3731 | lowerBoundExplanation = _boundManager.getExplanation( infeasibleVar, Tightening::LB ); |
| 3732 | |
| 3733 | if ( upperBoundExplanation.empty() && lowerBoundExplanation.empty() ) |
| 3734 | return Vector<double>( 0 ); |
| 3735 | |
| 3736 | Vector<double> contradiction = Vector<double>( m, 0 ); |
| 3737 | |
| 3738 | if ( !upperBoundExplanation.empty() ) |
| 3739 | for ( const auto &entry : upperBoundExplanation ) |
| 3740 | contradiction[entry._index] = entry._value; |
| 3741 | |
| 3742 | if ( !lowerBoundExplanation.empty() ) |
| 3743 | for ( const auto &entry : lowerBoundExplanation ) |
| 3744 | contradiction[entry._index] -= entry._value; |
| 3745 | |
| 3746 | return contradiction; |
| 3747 | } |
| 3748 | |
| 3749 | void Engine::writeContradictionToCertificate( unsigned infeasibleVar ) const |
| 3750 | { |
nothing calls this directly
no test coverage detected