Revert "Backward forward algorithm (#845)"

This reverts commit 90f5271.
NeuralNetworkVerification · Feb 13, 2025 · e0ba0a7 · e0ba0a7
1 parent 90f5271
commit e0ba0a7
Show file tree

Hide file tree

Showing 10 changed files with 1,721 additions and 14,482 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -4,7 +4,6 @@
   - Adding incremental infrastructure which allows pushing and popping constraints to/from the InputQuery.
   - Dropped support for parsing Tensorflow network format. Newest Marabou version that supports Tensorflow is at commit 190555573e4702.
   - Fixed bug in the parsing of `transpose` nodes in command line C++ parser.
-  - Implemented forward-backward abstract interpretation, symbolic bound tightening, interval arithmetic and simulations for all activation functions.
   - Added the BaBSR heuristic as a new branching strategy for ReLU Splitting
 
 ## Version 2.0.0

diff --git a/src/configuration/GlobalConfiguration.cpp b/src/configuration/GlobalConfiguration.cpp
@@ -71,7 +71,6 @@ const unsigned GlobalConfiguration::SIMULATION_RANDOM_SEED = 1;
 const bool GlobalConfiguration::USE_HARRIS_RATIO_TEST = true;
 
 const double GlobalConfiguration::SYMBOLIC_TIGHTENING_ROUNDING_CONSTANT = 0.00000000001;
-const double GlobalConfiguration::LP_TIGHTENING_ROUNDING_CONSTANT = 0.00000001;
 
 const double GlobalConfiguration::SIGMOID_CUTOFF_CONSTANT = 20;
 

diff --git a/src/configuration/GlobalConfiguration.h b/src/configuration/GlobalConfiguration.h
@@ -195,9 +195,8 @@ class GlobalConfiguration
       Symbolic bound tightening options
     */
 
-    // Symbolic tightening, LP rounding constants
+    // Symbolic tightening rounding constant
     static const double SYMBOLIC_TIGHTENING_ROUNDING_CONSTANT;
-    static const double LP_TIGHTENING_ROUNDING_CONSTANT;
 
     static const double SIGMOID_CUTOFF_CONSTANT;
 

diff --git a/src/configuration/OptionParser.cpp b/src/configuration/OptionParser.cpp
@@ -267,7 +267,7 @@ void OptionParser::initialize()
                 &( ( *_stringOptions )[Options::MILP_SOLVER_BOUND_TIGHTENING_TYPE] ) )
                 ->default_value( ( *_stringOptions )[Options::MILP_SOLVER_BOUND_TIGHTENING_TYPE] ),
             "The MILP solver bound tightening type: "
-            "lp/backward-once/backward-converge/lp-inc/milp/milp-inc/iter-prop/none." )
+            "lp/fb-once/fb-converge/lp-inc/milp/milp-inc/iter-prop/none." )
 #endif
         ;
 

diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp
@@ -1579,11 +1579,7 @@ void Engine::performMILPSolverBoundedTightening( Query *inputQuery )
 
         // TODO: Remove this block after getting ready to support sigmoid with MILP Bound
         // Tightening.
-        if ( ( _milpSolverBoundTighteningType == MILPSolverBoundTighteningType::MILP_ENCODING ||
-               _milpSolverBoundTighteningType ==
-                   MILPSolverBoundTighteningType::MILP_ENCODING_INCREMENTAL ||
-               _milpSolverBoundTighteningType ==
-                   MILPSolverBoundTighteningType::ITERATIVE_PROPAGATION ) &&
+        if ( _milpSolverBoundTighteningType != MILPSolverBoundTighteningType::NONE &&
              _preprocessedQuery->getNonlinearConstraints().size() > 0 )
             throw MarabouError( MarabouError::FEATURE_NOT_YET_SUPPORTED,
                                 "Marabou doesn't support sigmoid with MILP Bound Tightening" );