Symbolic bound tightening over absolute values (#251)

* test

* basic interval artihmetic bound propagation

* another test case

* initialize an SBT within the NLR. Pass topology, weights and biases

* wip

* SBT functionality into NLR

* wip

* bug fix

* cleanup

* cleanup

* wip

* handle eliminated relus

* cleanup: remove symbolic bound tightener

* oops

* additional cleanup

* oops

* first unit test

* unit tests for NLR

* basic support for symbolic bound propagations over ABS constraints

* unit test - evalue abs + relus

* a test for interval bound propagation, for abs constraints

* unit tests, and some consequent corrections, to AbsConstraint SBT

* set lblb to 0 for both Relu and Abs

* always initialize the scalar to 0 by default

* consistency

* oops

Co-authored-by: Guy Katz <guykatz@cs.huji.ac.il>

src/engine/AbsoluteValueConstraint.cpp

@@ -259,8 +259,10 @@ PiecewiseLinearCaseSplit AbsoluteValueConstraint::getValidCaseSplit() const
     return getNegativeSplit();
 }
 
-void AbsoluteValueConstraint::eliminateVariable( unsigned /* variable */, double /* fixedValue */ )
+void AbsoluteValueConstraint::eliminateVariable( unsigned variable, double /* fixedValue */ )
 {
+    ASSERT( variable = _b );
+
     // In an absolute value constraint, if a variable is removed the
     // entire constraint can be discarded
     _haveEliminatedVariables = true;

src/engine/Equation.cpp

@@ -30,12 +30,14 @@ bool Equation::Addend::operator==( const Addend &other ) const
 }
 
 Equation::Equation()
-    : _type( Equation::EQ )
+    : _scalar( 0 )
+    , _type( Equation::EQ )
 {
 }
 
 Equation::Equation( EquationType type )
-    : _type( type )
+    : _scalar( 0 )
+    , _type( type )
 {
 }