Sbt poc

src/common/Map.h

@@ -134,6 +134,11 @@ class Map
         _container.erase( key );
     }
 
+    iterator erase( iterator it )
+    {
+        return _container.erase( it );
+    }
+
     iterator begin()
     {
         return _container.begin();

src/common/Statistics.cpp

@@ -45,6 +45,7 @@ Statistics::Statistics()
     , _currentTableauN( 0 )
     , _numTableauBoundHopping( 0 )
     , _numTightenedBounds( 0 )
+    , _numTighteningsFromSymbolicBoundTightening( 0 )
     , _numRowsExaminedByRowTightener( 0 )
     , _numTighteningsFromRows( 0 )
     , _numBoundTighteningsOnExplicitBasis( 0 )
@@ -60,6 +61,7 @@ Statistics::Statistics()
     , _ppNumConstraintsRemoved( 0 )
     , _ppNumEquationsRemoved( 0 )
     , _totalTimePerformingValidCaseSplitsMicro( 0 )
+    , _totalTimePerformingSymbolicBoundTightening( 0 )
     , _totalTimeHandlingStatisticsMicro( 0 )
     , _totalNumberOfValidCaseSplits( 0 )
     , _totalTimeExplicitBasisBoundTighteningMicro( 0 )
@@ -153,6 +155,11 @@ void Statistics::print()
             , _totalTimeSmtCoreMicro / 1000
             );
 
+    printf( "\t\t[%.2lf%%] Symbolic Bound Tightening: %llu milli\n"
+            , printPercents( _totalTimePerformingSymbolicBoundTightening, _timeMainLoopMicro )
+            , _totalTimePerformingSymbolicBoundTightening / 1000
+            );
+
     unsigned long long total =
         _timeSimplexStepsMicro +
         _timeConstraintFixingStepsMicro +
@@ -163,7 +170,8 @@ void Statistics::print()
         _totalTimePrecisionRestoration +
         _totalTimeConstraintMatrixBoundTighteningMicro +
         _totalTimeApplyingStoredTighteningsMicro +
-        _totalTimeSmtCoreMicro;
+        _totalTimeSmtCoreMicro +
+        _totalTimePerformingSymbolicBoundTightening;
 
     printf( "\t\t[%.2lf%%] Unaccounted for: %llu milli\n"
             , printPercents( _timeMainLoopMicro - total, _timeMainLoopMicro )
@@ -268,6 +276,9 @@ void Statistics::print()
             , _pseNumResetReferenceSpace
             , _pseNumResetReferenceSpace > 0 ?
             (unsigned)((double)_pseNumIterations / _pseNumResetReferenceSpace) : 0 );
+
+    printf( "\t--- SBT ---\n" );
+    printf( "\tNumber of tightened bounds: %llu\n", _numTighteningsFromSymbolicBoundTightening );
 }
 
 double Statistics::printPercents( unsigned long long part, unsigned long long total ) const
@@ -531,6 +542,11 @@ void Statistics::addTimeForValidCaseSplit( unsigned long long time )
     ++_totalNumberOfValidCaseSplits;
 }
 
+void Statistics::addTimeForSymbolicBoundTightening( unsigned long long time )
+{
+    _totalTimePerformingSymbolicBoundTightening += time;
+}
+
 void Statistics::addTimeForStatistics( unsigned long long time )
 {
     _totalTimeHandlingStatisticsMicro += time;
@@ -650,6 +666,11 @@ void Statistics::printStartingIteration( unsigned long long iteration, String me
         printf( "DBG_PRINT: %s\n", message.ascii() );
 }
 
+void Statistics::incNumTighteningsFromSymbolicBoundTightening( unsigned increment )
+{
+    _numTighteningsFromSymbolicBoundTightening += increment;
+}
+
 //
 // Local Variables:
 // compile-command: "make -C ../.. "

src/common/Statistics.h

@@ -52,6 +52,7 @@ class Statistics
     void setNumPlSMTSplits( unsigned numberOfSplits );
     void setCurrentDegradation( double degradation );
     void addTimeForValidCaseSplit( unsigned long long time );
+    void addTimeForSymbolicBoundTightening( unsigned long long time );
     void addTimeForStatistics( unsigned long long time );
     void addTimeForExplicitBasisBoundTightening( unsigned long long time );
     void addTimeForConstraintMatrixBoundTightening( unsigned long long time );
@@ -119,6 +120,7 @@ class Statistics
     void incNumBoundNotificationsPlConstraints();
     void incNumBoundsProposedByPlConstraints();
 
+    void incNumTighteningsFromSymbolicBoundTightening( unsigned increment );
     /*
       Projected Steepest Edge related statistics.
     */
@@ -229,6 +231,9 @@ class Statistics
     // This combines tightenings from all sources: rows, basis, PL constraints, etc.
     unsigned long long _numTightenedBounds;
 
+    // The number of bounds tightened via symbolic bound tightening
+    unsigned long long _numTighteningsFromSymbolicBoundTightening;
+
     // Number of pivot rows examined by the row tightener, and consequent tightenings
     // proposed.
     unsigned long long _numRowsExaminedByRowTightener;
@@ -263,6 +268,8 @@ class Statistics
     // Total amount of time spent performing valid case splits
     unsigned long long _totalTimePerformingValidCaseSplitsMicro;
 
+    unsigned long long _totalTimePerformingSymbolicBoundTightening;
+
     // Total amount of time handling statistics printing
     unsigned long long _totalTimeHandlingStatisticsMicro;
 

src/common/tests/Test_Map.h

@@ -95,6 +95,30 @@ class MapTestSuite : public CxxTest::TestSuite
                                  CommonError::KEY_DOESNT_EXIST_IN_MAP );
     }
 
+    void test_map_erase_using_iterator()
+    {
+        Map<unsigned, unsigned> map;
+
+        map[0] = 10;
+        map[1] = 11;
+        map[2] = 12;
+
+        auto it = map.begin();
+
+        it = map.erase( it );
+
+        TS_ASSERT_EQUALS( map.size(), 2U );
+        TS_ASSERT_EQUALS( it->first, 1U );
+        TS_ASSERT_EQUALS( it->second, 11U );
+
+        ++it;
+
+        it = map.erase( it );
+        TS_ASSERT_EQUALS( it, map.end() );
+
+        TS_ASSERT_EQUALS( map.size(), 1U );
+    }
+
     void test_iterating()
     {
         Map<unsigned, String> map;

src/configuration/GlobalConfiguration.cpp

@@ -40,6 +40,10 @@ const double GlobalConfiguration::COST_FUNCTION_ERROR_THRESHOLD = 0.0000000001;
 
 const bool GlobalConfiguration::USE_HARRIS_RATIO_TEST = true;
 
+const bool GlobalConfiguration::USE_SYMBOLIC_BOUND_TIGHTENING = false;
+const bool GlobalConfiguration::USE_LINEAR_CONCRETIZATION = true;
+const double GlobalConfiguration::SYMBOLIC_TIGHTENING_ROUNDING_CONSTANT = 0.00000005;
+
 const bool GlobalConfiguration::PREPROCESS_INPUT_QUERY = true;
 const bool GlobalConfiguration::PREPROCESSOR_ELIMINATE_VARIABLES = true;
 const bool GlobalConfiguration::PREPROCESSOR_PL_CONSTRAINTS_ADD_AUX_EQUATIONS = true;
@@ -49,7 +53,6 @@ const unsigned GlobalConfiguration::PSE_ITERATIONS_BEFORE_RESET = 1000;
 const double GlobalConfiguration::PSE_GAMMA_ERROR_THRESHOLD = 0.001;
 const double GlobalConfiguration::PSE_GAMMA_UPDATE_TOLERANCE = 0.000000001;
 
-
 const double GlobalConfiguration::RELU_CONSTRAINT_COMPARISON_TOLERANCE = 0.001;
 
 const GlobalConfiguration::ExplicitBasisBoundTighteningType GlobalConfiguration::EXPLICIT_BASIS_BOUND_TIGHTENING_TYPE =
@@ -68,7 +71,8 @@ const bool GlobalConfiguration::DANTZIGS_RULE_LOGGING = false;
 const bool GlobalConfiguration::BASIS_FACTORIZATION_LOGGING = false;
 const bool GlobalConfiguration::PROJECTED_STEEPEST_EDGE_LOGGING = false;
 const bool GlobalConfiguration::GAUSSIAN_ELIMINATION_LOGGING = false;
-const bool GlobalConfiguration::QUERY_LOADER_LOGGING = true;
+const bool GlobalConfiguration::QUERY_LOADER_LOGGING = false;
+const bool GlobalConfiguration::SYMBOLIC_BOUND_TIGHTENER_LOGGING = false;
 
 const bool GlobalConfiguration::USE_SMART_FIX = false;
 const bool GlobalConfiguration::USE_LEAST_FIX = false;

src/configuration/GlobalConfiguration.h

@@ -111,8 +111,9 @@ class GlobalConfiguration
 
     // The tolerance for checking whether f = Relu( b ), to determine a ReLU's statisfaction
     static const double RELU_CONSTRAINT_COMPARISON_TOLERANCE;
+
     /*
-      Bound tightening options
+      Explicit (Reluplex-style) bound tightening options
     */
 
     enum ExplicitBasisBoundTighteningType {
@@ -128,6 +129,24 @@ class GlobalConfiguration
     // When doing explicit bound tightening, should we repeat until saturation?
     static const bool EXPLICIT_BOUND_TIGHTENING_UNTIL_SATURATION;
 
+    /*
+      Symbolic bound tightening options
+    */
+
+    // Whether symbolic bound tightening should be used or not
+    static const bool USE_SYMBOLIC_BOUND_TIGHTENING;
+
+    // If symbolic bound tightening is used, should linear concretization (as
+    // opposed to constant concretization) be used.
+    static const bool USE_LINEAR_CONCRETIZATION;
+
+    // Symbolic tightening rounding constant
+    static const double SYMBOLIC_TIGHTENING_ROUNDING_CONSTANT;
+
+    /*
+      Constraint fixing heuristics
+    */
+
     // When a PL constraint proposes a fix that affects multiple variables, should it first query
     // for any relevant linear connections between the variables?
     static const bool USE_SMART_FIX;
@@ -163,6 +182,7 @@ class GlobalConfiguration
     static const bool PROJECTED_STEEPEST_EDGE_LOGGING;
     static const bool GAUSSIAN_ELIMINATION_LOGGING;
     static const bool QUERY_LOADER_LOGGING;
+    static const bool SYMBOLIC_BOUND_TIGHTENER_LOGGING;
 };
 
 #endif // __GlobalConfiguration_h__