From fad1a47ae847f91a7635b28e668fafb22436e88a Mon Sep 17 00:00:00 2001 From: liamjdavis Date: Wed, 22 Jan 2025 12:48:05 -0500 Subject: [PATCH] Renamed option from 'babsr-heuristic' to 'babsr' --- src/configuration/OptionParser.cpp | 2 +- src/configuration/Options.cpp | 4 ++-- src/engine/DivideStrategy.h | 2 +- src/engine/Engine.cpp | 2 +- src/engine/SnCDivideStrategy.h | 1 - 5 files changed, 5 insertions(+), 6 deletions(-) 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 };