Skip to content

Commit

Permalink
Minor
Browse files Browse the repository at this point in the history
  • Loading branch information
@omriisack
omriisack committed Dec 3, 2023
1 parent 758bd6c commit bc5f33a
Show file tree
Hide file tree
Showing 3 changed files with 23 additions and 23 deletions.
16 changes: 8 additions & 8 deletions src/engine/AbsoluteValueConstraint.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -148,7 +148,7 @@ void AbsoluteValueConstraint::notifyLowerBound( unsigned variable, double bound
// If phase is not fixed, both bonds are stored and checker should check the max of the two
if ( proofs && !phaseFixed() )
_boundManager->addLemmaExplanationAndTightenBound( _f, fUpperBound, BoundType::UPPER,
{variable, variable}, BoundType::UPPER, getType() );
{ variable, variable }, BoundType::UPPER, getType() );
else if ( proofs && phaseFixed() )
{
std::shared_ptr<TableauRow> tighteningRow = fUpperBound == getUpperBound( _b ) ? _posTighteningRow : _negTighteningRow;
Expand Down Expand Up @@ -222,7 +222,7 @@ void AbsoluteValueConstraint::notifyUpperBound( unsigned variable, double bound
// If phase is not fixed, both bonds are stored and checker should check the max of the two
if ( proofs && !phaseFixed() )
_boundManager->addLemmaExplanationAndTightenBound( _f, fUpperBound, BoundType::UPPER,
{variable, variable}, BoundType::UPPER, getType() );
{ variable, variable }, BoundType::UPPER, getType() );
else if ( proofs && phaseFixed() )
{
std::shared_ptr<TableauRow> tighteningRow = fUpperBound == bound ? _posTighteningRow : _negTighteningRow;
Expand Down Expand Up @@ -807,7 +807,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
{
setPhaseStatus( ABS_PHASE_POSITIVE );
if ( proofs )
_boundManager->addLemmaExplanationAndTightenBound( _posAux, 0, BoundType::UPPER, {_b},
_boundManager->addLemmaExplanationAndTightenBound( _posAux, 0, BoundType::UPPER, { _b },
BoundType::LOWER, getType() );
return;
}
Expand All @@ -817,7 +817,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
{
setPhaseStatus( ABS_PHASE_NEGATIVE );
if ( proofs )
_boundManager->addLemmaExplanationAndTightenBound( _negAux, 0, BoundType::UPPER, {_b},
_boundManager->addLemmaExplanationAndTightenBound( _negAux, 0, BoundType::UPPER, { _b },
BoundType::UPPER, getType() );
return;
}
Expand All @@ -831,7 +831,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
{
setPhaseStatus( ABS_PHASE_NEGATIVE );
if ( proofs )
_boundManager->addLemmaExplanationAndTightenBound( _negAux, 0, BoundType::UPPER, {_b, _f},
_boundManager->addLemmaExplanationAndTightenBound( _negAux, 0, BoundType::UPPER, { _b, _f },
BoundType::UPPER, getType() );
return;
}
Expand All @@ -842,7 +842,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
{
setPhaseStatus( ABS_PHASE_POSITIVE );
if ( proofs )
_boundManager->addLemmaExplanationAndTightenBound( _posAux, 0, BoundType::UPPER, {_b, _f},
_boundManager->addLemmaExplanationAndTightenBound( _posAux, 0, BoundType::UPPER, { _b, _f },
BoundType::LOWER, getType() );
return;
}
Expand All @@ -861,7 +861,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
{
setPhaseStatus( ABS_PHASE_NEGATIVE );
if ( proofs )
_boundManager->addLemmaExplanationAndTightenBound( _negAux, 0, BoundType::UPPER, {_posAux},
_boundManager->addLemmaExplanationAndTightenBound( _negAux, 0, BoundType::UPPER, { _posAux },
BoundType::LOWER, getType() );
return;
}
Expand All @@ -878,7 +878,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
{
setPhaseStatus( ABS_PHASE_POSITIVE );
if ( proofs )
_boundManager->addLemmaExplanationAndTightenBound( _posAux, 0, BoundType::UPPER, {_negAux},
_boundManager->addLemmaExplanationAndTightenBound( _posAux, 0, BoundType::UPPER, { _negAux },
BoundType::LOWER, getType() );
return;
}
Expand Down
18 changes: 9 additions & 9 deletions src/engine/ReluConstraint.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,7 @@ void ReluConstraint::notifyLowerBound( unsigned variable, double newBound )
{
// If we're in the active phase, aux should be 0
if ( proofs && _auxVarInUse )
_boundManager->addLemmaExplanationAndTightenBound( _aux, 0, BoundType::UPPER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _aux, 0, BoundType::UPPER, { variable },
BoundType::LOWER, getType() );
else if ( !proofs && _auxVarInUse )
_boundManager->tightenUpperBound( _aux, 0 );
Expand All @@ -186,7 +186,7 @@ void ReluConstraint::notifyLowerBound( unsigned variable, double newBound )
else if ( _auxVarInUse && variable == _b && FloatUtils::isZero( bound ) )
{
if ( proofs && _auxVarInUse )
_boundManager->addLemmaExplanationAndTightenBound( _aux, 0, BoundType::UPPER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _aux, 0, BoundType::UPPER, { variable },
BoundType::LOWER, getType() );
else if ( !proofs && _auxVarInUse )
_boundManager->tightenUpperBound( _aux, 0 );
Expand All @@ -197,7 +197,7 @@ void ReluConstraint::notifyLowerBound( unsigned variable, double newBound )
else if ( _auxVarInUse && variable == _aux && bound > 0 )
{
if ( proofs )
_boundManager->addLemmaExplanationAndTightenBound( _f, 0, BoundType::UPPER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _f, 0, BoundType::UPPER, { variable },
BoundType::LOWER, getType() );
else
_boundManager->tightenUpperBound( _f, 0 );
Expand All @@ -215,7 +215,7 @@ void ReluConstraint::notifyLowerBound( unsigned variable, double newBound )
if ( _phaseStatus == RELU_PHASE_INACTIVE )
_boundManager->tightenUpperBound( _aux, -bound, *_tighteningRow );
else if ( _phaseStatus == PHASE_NOT_FIXED )
_boundManager->addLemmaExplanationAndTightenBound( _aux, -bound, BoundType::UPPER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _aux, -bound, BoundType::UPPER, { variable },
BoundType::LOWER, getType() );
}
else
Expand All @@ -227,7 +227,7 @@ void ReluConstraint::notifyLowerBound( unsigned variable, double newBound )
else if ( bound < 0 && variable == _f )
{
if ( proofs )
_boundManager->addLemmaExplanationAndTightenBound( _f, 0, BoundType::LOWER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _f, 0, BoundType::LOWER, { variable },
BoundType::LOWER, getType() );
else
_boundManager->tightenLowerBound( _f, 0 );
Expand Down Expand Up @@ -272,7 +272,7 @@ void ReluConstraint::notifyUpperBound( unsigned variable, double newBound )
else
{
if ( FloatUtils::isZero( bound ) )
_boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::UPPER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::UPPER, { variable },
BoundType::UPPER, getType() );
// Bound cannot be negative if ReLU is inactive
else if ( FloatUtils::isNegative( bound ) )
Expand All @@ -289,7 +289,7 @@ void ReluConstraint::notifyUpperBound( unsigned variable, double newBound )
{
// If b has a non-positive upper bound, f's upper bound is 0
if ( proofs )
_boundManager->addLemmaExplanationAndTightenBound( _f, 0, BoundType::UPPER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _f, 0, BoundType::UPPER, { variable },
BoundType::UPPER, getType() );
else
_boundManager->tightenUpperBound( _f, 0 );
Expand All @@ -308,7 +308,7 @@ void ReluConstraint::notifyUpperBound( unsigned variable, double newBound )
if ( _phaseStatus == RELU_PHASE_ACTIVE )
_boundManager->tightenUpperBound( _f, bound, *_tighteningRow );
else if ( _phaseStatus == PHASE_NOT_FIXED )
_boundManager->addLemmaExplanationAndTightenBound( _f, bound, BoundType::UPPER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _f, bound, BoundType::UPPER, { variable },
BoundType::UPPER, getType() );
}
else
Expand All @@ -324,7 +324,7 @@ void ReluConstraint::notifyUpperBound( unsigned variable, double newBound )
else
{
if ( FloatUtils::isZero( bound ) )
_boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::LOWER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::LOWER, { variable },
BoundType::UPPER, getType() );
// Bound cannot be negative if ReLU is active
else if ( FloatUtils::isNegative( bound ) )
Expand Down
12 changes: 6 additions & 6 deletions src/engine/SignConstraint.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -403,9 +403,9 @@ void SignConstraint::notifyLowerBound( unsigned variable, double bound )
if ( FloatUtils::gt( bound, 1 ) )
throw InfeasibleQueryException();

_boundManager->addLemmaExplanationAndTightenBound( _f, 1, BoundType::LOWER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _f, 1, BoundType::LOWER, { variable },
BoundType::LOWER, getType() );
_boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::LOWER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::LOWER, { variable },
BoundType::LOWER, getType() );
}
else
Expand All @@ -421,7 +421,7 @@ void SignConstraint::notifyLowerBound( unsigned variable, double bound )
if ( _boundManager != nullptr )
{
if ( _boundManager->shouldProduceProofs() )
_boundManager->addLemmaExplanationAndTightenBound( _f, 1, BoundType::LOWER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _f, 1, BoundType::LOWER, { variable },
BoundType::LOWER, getType() );
else
_boundManager->tightenLowerBound( _f, 1 );
Expand Down Expand Up @@ -455,9 +455,9 @@ void SignConstraint::notifyUpperBound( unsigned variable, double bound )
if ( FloatUtils::lt( bound, -1 ) )
throw InfeasibleQueryException();

_boundManager->addLemmaExplanationAndTightenBound( _f, -1, BoundType::UPPER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _f, -1, BoundType::UPPER, { variable },
BoundType::UPPER, getType() );
_boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::UPPER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::UPPER, { variable },
BoundType::UPPER, getType() );
}
else
Expand All @@ -473,7 +473,7 @@ void SignConstraint::notifyUpperBound( unsigned variable, double bound )
if ( _boundManager != nullptr )
{
if ( _boundManager->shouldProduceProofs() )
_boundManager->addLemmaExplanationAndTightenBound( _f, -1, BoundType::UPPER, {variable},
_boundManager->addLemmaExplanationAndTightenBound( _f, -1, BoundType::UPPER, { variable },
BoundType::UPPER, getType() );
else
_boundManager->tightenUpperBound( _f, -1 );
Expand Down

0 comments on commit bc5f33a

Please sign in to comment.