diff --git a/src/configuration/OptionParser.cpp b/src/configuration/OptionParser.cpp index 2a116290e..358c11734 100644 --- 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 index 70da66c62..657ddb6b7 100644 --- 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 index 700e71c79..77e260f2a 100644 --- 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 index 4e7c2f71a..311daef54 100644 --- 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 index df3d48d20..bc5f71800 100644 --- 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 };