Renamed option from 'babsr-heuristic' to 'babsr'

NeuralNetworkVerification · Jan 22, 2025 · fad1a47 · fad1a47
1 parent ce03e4f
commit fad1a47
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 6 deletions.
diff --git a/src/configuration/OptionParser.cpp b/src/configuration/OptionParser.cpp
@@ -152,7 +152,7 @@ void OptionParser::initialize()
             &( ( *_stringOptions )[Options::SPLITTING_STRATEGY] ) )
             ->default_value( ( *_stringOptions )[Options::SPLITTING_STRATEGY] ),
         "The branching strategy "
-        "(earliest-relu/pseudo-impact/largest-interval/relu-violation/polarity/babsr-heuristic)."
+        "(earliest-relu/pseudo-impact/largest-interval/relu-violation/polarity/babsr)."
         " pseudo-impact is specific to the DeepSoI (default) procedure and relu-violation is "
         "specific to the Reluplex procedure.\n" )(
         "soi-split-threshold",

diff --git a/src/configuration/Options.cpp b/src/configuration/Options.cpp
@@ -165,8 +165,8 @@ DivideStrategy Options::getDivideStrategy() const
         return DivideStrategy::LargestInterval;
     else if ( strategyString == "pseudo-impact" )
         return DivideStrategy::PseudoImpact;
-    else if ( strategyString == "babsr-heuristic" )
-        return DivideStrategy::BaBsrHeuristic;
+    else if ( strategyString == "babsr" )
+        return DivideStrategy::BaBSR;
     else
         return DivideStrategy::Auto;
 }

diff --git a/src/engine/DivideStrategy.h b/src/engine/DivideStrategy.h
@@ -19,7 +19,7 @@
 enum class DivideStrategy {
     // Relu splitting
     Polarity = 0,    // Pick the ReLU with the polarity closest to 0 among the first K nodes
-    BaBsrHeuristic,  // Pick the ReLU with the highest BaBSR score
+    BaBSR,           // Pick the ReLU with the highest BaBSR score
     EarliestReLU,    // Pick a ReLU that appears in the earliest layer
     ReLUViolation,   // Pick the ReLU that has been violated for the most times
     LargestInterval, // Pick the largest interval every K split steps, use ReLUViolation in other

diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp
@@ -2886,7 +2886,7 @@ PiecewiseLinearConstraint *Engine::pickSplitPLConstraint( DivideStrategy strateg
                 candidatePLConstraint = _smtCore.getConstraintsWithHighestScore();
         }
     }
-    else if ( strategy == DivideStrategy::BaBsrHeuristic )
+    else if ( strategy == DivideStrategy::BaBSR )
         candidatePLConstraint = pickSplitPLConstraintBasedOnBaBsrHeuristic();
     else if ( strategy == DivideStrategy::Polarity )
         candidatePLConstraint = pickSplitPLConstraintBasedOnPolarity();

diff --git a/src/engine/SnCDivideStrategy.h b/src/engine/SnCDivideStrategy.h
@@ -23,7 +23,6 @@ enum class SnCDivideStrategy {
     // Relu splitting
     Polarity, // Pick the ReLU with the polarity closest to 0 among the first K nodes
     EarliestReLU,
-    BaBsrHeuristic, // Pick the ReLU with the highest BaBSR score
 
     Auto
 };