| 129 | } |
| 130 | |
| 131 | void Checker::fixChildSplitPhase( UnsatCertificateNode *child, |
| 132 | PiecewiseLinearConstraint *childrenSplitConstraint ) |
| 133 | { |
| 134 | if ( childrenSplitConstraint && childrenSplitConstraint->getType() == RELU ) |
| 135 | { |
| 136 | List<Tightening> tightenings = child->getSplit().getBoundTightenings(); |
| 137 | if ( tightenings.front()._type == Tightening::LB || |
| 138 | tightenings.back()._type == Tightening::LB ) |
| 139 | childrenSplitConstraint->setPhaseStatus( RELU_PHASE_ACTIVE ); |
| 140 | else |
| 141 | childrenSplitConstraint->setPhaseStatus( RELU_PHASE_INACTIVE ); |
| 142 | } |
| 143 | else if ( childrenSplitConstraint && childrenSplitConstraint->getType() == SIGN ) |
| 144 | { |
| 145 | List<Tightening> tightenings = child->getSplit().getBoundTightenings(); |
| 146 | if ( tightenings.front()._type == Tightening::LB ) |
| 147 | childrenSplitConstraint->setPhaseStatus( SIGN_PHASE_POSITIVE ); |
| 148 | else |
| 149 | childrenSplitConstraint->setPhaseStatus( SIGN_PHASE_NEGATIVE ); |
| 150 | } |
| 151 | else if ( childrenSplitConstraint && childrenSplitConstraint->getType() == ABSOLUTE_VALUE ) |
| 152 | { |
| 153 | List<Tightening> tightenings = child->getSplit().getBoundTightenings(); |
| 154 | if ( tightenings.front()._type == Tightening::LB ) |
| 155 | childrenSplitConstraint->setPhaseStatus( ABS_PHASE_POSITIVE ); |
| 156 | else |
| 157 | childrenSplitConstraint->setPhaseStatus( ABS_PHASE_NEGATIVE ); |
| 158 | } |
| 159 | else if ( childrenSplitConstraint && childrenSplitConstraint->getType() == MAX ) |
| 160 | { |
| 161 | List<Tightening> tightenings = child->getSplit().getBoundTightenings(); |
| 162 | if ( tightenings.size() == 2 ) |
| 163 | childrenSplitConstraint->setPhaseStatus( MAX_PHASE_ELIMINATED ); |
| 164 | else |
| 165 | { |
| 166 | PhaseStatus phase = ( (MaxConstraint *)childrenSplitConstraint ) |
| 167 | ->variableToPhase( tightenings.back()._variable ); |
| 168 | childrenSplitConstraint->setPhaseStatus( phase ); |
| 169 | } |
| 170 | } |
| 171 | else if ( childrenSplitConstraint && childrenSplitConstraint->getType() == DISJUNCTION ) |
| 172 | ( (DisjunctionConstraint *)childrenSplitConstraint ) |
| 173 | ->removeFeasibleDisjunct( child->getSplit() ); |
| 174 | else if ( childrenSplitConstraint && childrenSplitConstraint->getType() == LEAKY_RELU ) |
| 175 | { |
| 176 | List<Tightening> tightenings = child->getSplit().getBoundTightenings(); |
| 177 | if ( tightenings.front()._type == Tightening::LB && |
| 178 | tightenings.back()._type == Tightening::LB ) |
| 179 | childrenSplitConstraint->setPhaseStatus( RELU_PHASE_ACTIVE ); |
| 180 | else |
| 181 | childrenSplitConstraint->setPhaseStatus( RELU_PHASE_INACTIVE ); |
| 182 | } |
| 183 | } |
| 184 | |
| 185 | bool Checker::checkContradiction( const UnsatCertificateNode *node ) const |
| 186 | { |
nothing calls this directly
no test coverage detected