Merge branch 'master' into leaky-relu

resources/onnx/vnnlib/test_sub_const.vnnlib

@@ -2,6 +2,6 @@
 (declare-const Y_0 Real)
 
 (assert (>= (- X_0 1) 1))
-(assert (<= X_0 1))
+(assert (<= X_0 3))
 
 (assert (>= Y_0 0))

src/engine/DisjunctionConstraint.cpp

@@ -552,3 +552,65 @@ bool DisjunctionConstraint::addFeasibleDisjunct( const PiecewiseLinearCaseSplit
 void DisjunctionConstraint::addTableauAuxVar( unsigned /* tableauAuxVar */, unsigned /* constraintAuxVar */ )
 {
 }
+
+double DisjunctionConstraint::getMinLowerBound( unsigned int var ) const
+{
+    if ( !participatingVariable( var ) )
+    {
+        return FloatUtils::negativeInfinity();
+    }
+
+    double minLowerBound = FloatUtils::infinity();
+    for ( const auto &disjunct : _disjuncts )
+    {
+        bool foundLowerBound = false;
+        for ( const auto &bound : disjunct.getBoundTightenings() )
+        {
+            if ( bound._variable == var && bound._type == Tightening::LB )
+            {
+                foundLowerBound = true;
+                minLowerBound = FloatUtils::min( minLowerBound, bound._value );
+            }
+        }
+
+        if ( !foundLowerBound )
+        {
+            throw MarabouError( MarabouError::PARTICIPATING_VARIABLE_MISSING_BOUND,
+                                Stringf( "Variable %d missing lower bound in given disjunction constraint %s", var,
+                                         serializeToString().ascii() ).ascii() );
+        }
+    }
+
+    return minLowerBound;
+}
+
+double DisjunctionConstraint::getMaxUpperBound( unsigned int var ) const
+{
+    if ( !participatingVariable( var ) )
+    {
+        return FloatUtils::infinity();
+    }
+
+    double maxUpperBound = FloatUtils::negativeInfinity();
+    for ( const auto &disjunct : _disjuncts )
+    {
+        bool foundUpperBound = false;
+        for ( const auto &bound : disjunct.getBoundTightenings() )
+        {
+            if ( bound._variable == var && bound._type == Tightening::UB )
+            {
+                foundUpperBound = true;
+                maxUpperBound = FloatUtils::max( maxUpperBound, bound._value );
+            }
+        }
+
+        if ( !foundUpperBound )
+        {
+            throw MarabouError( MarabouError::PARTICIPATING_VARIABLE_MISSING_BOUND,
+                                Stringf( "Variable %d missing upper bound in given disjunction constraint %s", var,
+                                         serializeToString().ascii() ).ascii() );
+        }
+    }
+
+    return maxUpperBound;
+}

src/engine/DisjunctionConstraint.h

@@ -189,6 +189,14 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint
     */
     bool addFeasibleDisjunct( const PiecewiseLinearCaseSplit &disjunct );
 
+    /*
+      Get the minimal lower bound and maximal upper bound for the given variable,
+      across all disjuncts. If some disjunct does not contain a bound, an exception
+      will be thrown.
+     */
+    double getMinLowerBound( unsigned int var ) const override;
+    double getMaxUpperBound( unsigned int var ) const override;
+
 private:
     /*
       The disjuncts that form this PL constraint

src/engine/Engine.cpp

@@ -3719,4 +3719,4 @@ void Engine::extractBounds( InputQuery &inputQuery )
             inputQuery.setUpperBound( i, _preprocessedQuery->getUpperBound( i ) );
         }
     }
-}
+}

src/engine/MarabouError.h

@@ -47,11 +47,12 @@ class MarabouError : public Error
         INVALID_WEIGHTED_SUM_INDEX = 22,
         UNSUCCESSFUL_QUEUE_PUSH = 23,
         NETWORK_LEVEL_REASONER_ACTIVATION_NOT_SUPPORTED = 24,
-        NETWORK_LEVEL_REASONER_NOT_AVAILABLE = 24,
-        REQUESTED_NONEXISTENT_CASE_SPLIT = 25,
-        UNABLE_TO_INITIALIZATION_PHASE_PATTERN = 26,
-        BOUNDS_NOT_UP_TO_DATE_IN_LP_SOLVER = 27,
-        INVALID_LEAKY_RELU_SLOPE= 28,
+        NETWORK_LEVEL_REASONER_NOT_AVAILABLE = 25,
+        REQUESTED_NONEXISTENT_CASE_SPLIT = 26,
+        UNABLE_TO_INITIALIZATION_PHASE_PATTERN = 27,
+        BOUNDS_NOT_UP_TO_DATE_IN_LP_SOLVER = 28,
+        PARTICIPATING_VARIABLE_MISSING_BOUND = 29,
+        INVALID_LEAKY_RELU_SLOPE= 30,
 
         // Error codes for Query Loader
         FILE_DOES_NOT_EXIST = 100,

src/engine/PiecewiseLinearConstraint.cpp

@@ -203,6 +203,26 @@ void PiecewiseLinearConstraint::setStatistics( Statistics *statistics )
     _statistics = statistics;
 }
 
+double PiecewiseLinearConstraint::getMinLowerBound( unsigned int var ) const
+{
+    if ( existsLowerBound( var ) )
+    {
+        return getLowerBound( var );
+    }
+
+    return FloatUtils::infinity();
+}
+
+double PiecewiseLinearConstraint::getMaxUpperBound( unsigned int var ) const
+{
+    if ( existsUpperBound( var ) )
+    {
+        return getUpperBound( var );
+    }
+
+    return FloatUtils::negativeInfinity();
+}
+
 //
 // Local Variables:
 // compile-command: "make -C ../.. "

src/engine/PiecewiseLinearConstraint.h

@@ -255,6 +255,12 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher
     virtual void addAuxiliaryEquationsAfterPreprocessing( InputQuery
                                                           &/* inputQuery */ ) {}
 
+    /*
+      Get the minimal lower bound and maximal upper bound for the given variable.
+     */
+    virtual double getMinLowerBound( unsigned int var ) const;
+    virtual double getMaxUpperBound( unsigned int var ) const;
+
     /*
       Whether the constraint can contribute the SoI cost function.
     */

src/engine/Preprocessor.cpp

@@ -78,6 +78,12 @@ std::unique_ptr<InputQuery> Preprocessor::preprocess( const InputQuery &query, b
     */
     transformConstraintsIfNeeded();
 
+    /*
+      Try to find missing lower and upper bounds for input variables from
+      piecewise linear constraints.
+     */
+    getMissingInputBoundsFromConstraints();
+
     /*
       Merge consecutive WS layers
     */
@@ -210,6 +216,43 @@ void Preprocessor::transformConstraintsIfNeeded()
         plConstraint->transformToUseAuxVariables( *_preprocessed );
 }
 
+void Preprocessor::getMissingInputBoundsFromConstraints()
+{
+    const auto &lowerBounds = _preprocessed->getLowerBounds();
+    const auto &upperBounds = _preprocessed->getUpperBounds();
+
+    for ( unsigned int var : _preprocessed->getInputVariables() )
+    {
+        if ( !lowerBounds.exists( var ) )
+        {
+            double minLowerBound = FloatUtils::infinity();
+            for ( const auto &plConstraint : _preprocessed->getPiecewiseLinearConstraints() )
+            {
+                minLowerBound = FloatUtils::min( minLowerBound, plConstraint->getMinLowerBound( var ) );
+            }
+
+            if ( !FloatUtils::areEqual( minLowerBound, FloatUtils::infinity() ) )
+            {
+                _preprocessed->setLowerBound( var, minLowerBound );
+            }
+        }
+
+        if ( !upperBounds.exists( var ) )
+        {
+            double maxUpperBound = FloatUtils::negativeInfinity();
+            for ( const auto &plConstraint : _preprocessed->getPiecewiseLinearConstraints() )
+            {
+                maxUpperBound = FloatUtils::max( maxUpperBound, plConstraint->getMaxUpperBound( var ) );
+            }
+
+            if ( !FloatUtils::areEqual( maxUpperBound, FloatUtils::negativeInfinity() ) )
+            {
+                _preprocessed->setUpperBound( var, maxUpperBound );
+            }
+        }
+    }
+}
+
 void Preprocessor::makeAllEquationsEqualities()
 {
     for ( auto &equation : _preprocessed->getEquations() )

src/engine/Preprocessor.h

@@ -88,6 +88,12 @@ class Preprocessor
     */
     void transformConstraintsIfNeeded();
 
+    /**
+     * Try to find missing lower and upper bounds of input variables from
+     * piecewise linear constraints.
+     */
+    void getMissingInputBoundsFromConstraints();
+
     /*
       Transform all equations of type GE or LE to type EQ.
     */

src/engine/tests/Test_DisjunctionConstraint.h

@@ -621,4 +621,46 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite
         TS_ASSERT_EQUALS( *split++, *cs2);
         TS_ASSERT_EQUALS( *split, *cs3);
     }
+
+    void test_min_lower_bound()
+    {
+        // Disjuncts are:
+        // -1 <= x0 <= 1, x1 = 2
+        // 1 <= x0 <= 5, x1 = x0
+        // 5 <= x0 , x1 = 2x2 + 5
+
+        List<PiecewiseLinearCaseSplit> caseSplits = { *cs1, *cs2, *cs3 };
+
+        // Add lower bound for x0 in first disjunct (otherwise MarabouError will be thrown)
+        caseSplits.front().storeBoundTightening( Tightening( 0, -1, Tightening::LB ) );
+
+        DisjunctionConstraint disj = DisjunctionConstraint( caseSplits );
+
+        double minX0LowerBound = 0;
+        TS_ASSERT_THROWS_NOTHING( minX0LowerBound = disj.getMinLowerBound( 0 ) )
+        TS_ASSERT_EQUALS( minX0LowerBound, -1 )
+
+        TS_ASSERT_THROWS( disj.getMinLowerBound( 1 ), MarabouError )
+    }
+
+    void test_max_upper_bound()
+    {
+        // Disjuncts are:
+        // x0 <= 1, x1 = 2
+        // 1 <= x0 <= 5, x1 = x0
+        // 5 <= x0 <= 3 , x1 = 2x2 + 5
+
+        List<PiecewiseLinearCaseSplit> caseSplits = { *cs1, *cs2, *cs3 };
+
+        // Add upper bound for x0 in last disjunct (otherwise MarabouError will be thrown)
+        caseSplits.back().storeBoundTightening( Tightening( 0, 3, Tightening::UB ) );
+
+        DisjunctionConstraint disj = DisjunctionConstraint( caseSplits );
+
+        double maxX0UpperBound = 0;
+        TS_ASSERT_THROWS_NOTHING( maxX0UpperBound = disj.getMaxUpperBound( 0 ) )
+        TS_ASSERT_EQUALS( maxX0UpperBound, 5 )
+
+        TS_ASSERT_THROWS( disj.getMaxUpperBound( 1 ), MarabouError )
+    }
 };

src/engine/tests/Test_Preprocessor.h

@@ -16,6 +16,7 @@
 
 #include <cxxtest/TestSuite.h>
 
+#include "DisjunctionConstraint.h"
 #include "Engine.h"
 #include "FloatUtils.h"
 #include "InfeasibleQueryException.h"
@@ -935,6 +936,32 @@ class PreprocessorTestSuite : public CxxTest::TestSuite
         }
     }
 
+    void test_preprocessor_with_input_bounds_in_disjunction()
+    {
+        InputQuery ipq;
+        ipq.setNumberOfVariables( 1 );
+        ipq.markInputVariable( 0, 0 );
+
+        PiecewiseLinearCaseSplit cs1;
+        cs1.storeBoundTightening( Tightening( 0, -1, Tightening::LB ) );
+        cs1.storeBoundTightening( Tightening( 0, 3, Tightening::UB ) );
+
+        PiecewiseLinearCaseSplit cs2;
+        cs2.storeBoundTightening( Tightening( 0, -4, Tightening::LB ) );
+        cs2.storeBoundTightening( Tightening( 0, 2, Tightening::UB ) );
+
+        List<PiecewiseLinearCaseSplit> caseSplits = {cs1, cs2};
+        DisjunctionConstraint *disj = new DisjunctionConstraint( caseSplits );
+        ipq.addPiecewiseLinearConstraint( disj );
+
+        InputQuery processed;
+        TS_ASSERT_THROWS_NOTHING( processed = *( Preprocessor().
+            preprocess( ipq ) ) );
+
+        TS_ASSERT_EQUALS( processed.getLowerBound( 0 ), -4 )
+        TS_ASSERT_EQUALS( processed.getUpperBound( 0 ), 3 )
+    }
+
     void test_todo()
     {
         TS_TRACE( "In test_variable_elimination, test something about updated bounds and updated PL constraints" );