Bug fixes in the preprocessor / relu constraints

regress/main_regress.cpp

@@ -25,6 +25,7 @@
 #include "max_infeasible_1.h"
 #include "max_relu_feasible_1.h"
 #include "relu_feasible_1.h"
+#include "relu_feasible_2.h"
 
 void lps()
 {
@@ -46,6 +47,9 @@ void relus()
     Relu_Feasible_1 rf1;
     rf1.run();
 
+    Relu_Feasible_2 rf2;
+    rf2.run();
+
     Acas_1_1_Fixed_Input acas_1_1_fixed_input;
     acas_1_1_fixed_input.run();
 
@@ -78,8 +82,8 @@ void max_relu()
 int main()
 {
     try
-	{
-		lps();
+    {
+        lps();
 
     	relus();
 

regress/relu_feasible_2.h

@@ -0,0 +1,158 @@
+/*********************                                                        */
+/*! \file Relu_Feasible_2.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Guy Katz
+ ** This file is part of the Marabou project.
+ ** Copyright (c) 2016-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **/
+
+#ifndef __Relu_Feasible_2_h__
+#define __Relu_Feasible_2_h__
+
+#include "Engine.h"
+#include "FloatUtils.h"
+#include "InputQuery.h"
+#include "ReluConstraint.h"
+
+class Relu_Feasible_2
+{
+public:
+    void run()
+    {
+        // The example from the CAV'17 paper, without the aux variables:
+        //   0   <= x0  <= 1
+        //   0   <= x1f
+        //   0   <= x2f
+        //   1/2 <= x3  <= 1
+        //
+        //  x0 - x1b = 0
+        //  x0 + x2b = 0
+        //  x1f + x2f - x3 = 0
+        //
+        //  x2f = Relu(x2b)
+        //  x3f = Relu(x3b)
+        //
+        //   x0: x0
+        //   x1: x1b
+        //   x2: x1f
+        //   x3: x2b
+        //   x4: x2f
+        //   x5: x3
+
+        InputQuery inputQuery;
+        inputQuery.setNumberOfVariables( 6 );
+
+        inputQuery.setLowerBound( 0, 0 );
+        inputQuery.setUpperBound( 0, 1 );
+
+        inputQuery.setLowerBound( 5, 0.5 );
+        inputQuery.setUpperBound( 5, 1 );
+
+        Equation equation1;
+        equation1.addAddend( 1, 0 );
+        equation1.addAddend( -1, 1 );
+        equation1.setScalar( 0 );
+        inputQuery.addEquation( equation1 );
+
+        Equation equation2;
+        equation2.addAddend( 1, 0 );
+        equation2.addAddend( 1, 3 );
+        equation2.setScalar( 0 );
+        inputQuery.addEquation( equation2 );
+
+        Equation equation3;
+        equation3.addAddend( 1, 2 );
+        equation3.addAddend( 1, 4 );
+        equation3.addAddend( -1, 5 );
+        equation3.setScalar( 0 );
+        inputQuery.addEquation( equation3 );
+
+        ReluConstraint *relu1 = new ReluConstraint( 1, 2 );
+        ReluConstraint *relu2 = new ReluConstraint( 3, 4 );
+
+        inputQuery.addPiecewiseLinearConstraint( relu1 );
+        inputQuery.addPiecewiseLinearConstraint( relu2 );
+
+        int outputStream = redirectOutputToFile( "logs/relu_feasible_2.txt" );
+
+        struct timespec start = TimeUtils::sampleMicro();
+
+        Engine engine;
+        if ( !engine.processInputQuery( inputQuery ) )
+        {
+            struct timespec end = TimeUtils::sampleMicro();
+            restoreOutputStream( outputStream );
+            printFailed( "relu_feasible_2", start, end );
+            return;
+        }
+
+        bool result = engine.solve();
+
+        struct timespec end = TimeUtils::sampleMicro();
+
+        restoreOutputStream( outputStream );
+
+        if ( !result )
+        {
+            printFailed( "relu_feasible_2", start, end );
+            return;
+        }
+
+        engine.extractSolution( inputQuery );
+
+        bool correctSolution = true;
+        // Sanity test
+
+        double value_x0 = inputQuery.getSolutionValue( 0 );
+        double value_x1b = inputQuery.getSolutionValue( 1 );
+        double value_x1f = inputQuery.getSolutionValue( 2 );
+        double value_x2b = inputQuery.getSolutionValue( 3 );
+        double value_x2f = inputQuery.getSolutionValue( 4 );
+        double value_x3 = inputQuery.getSolutionValue( 5 );
+
+        if ( !FloatUtils::areEqual( value_x0, value_x1b ) )
+            correctSolution = false;
+
+        if ( !FloatUtils::areEqual( value_x0, -value_x2b ) )
+            correctSolution = false;
+
+        if ( !FloatUtils::areEqual( value_x3, value_x1f + value_x2f ) )
+            correctSolution = false;
+
+        if ( FloatUtils::lt( value_x0, 0 ) || FloatUtils::gt( value_x0, 1 ) ||
+             FloatUtils::lt( value_x1f, 0 ) || FloatUtils::lt( value_x2f, 0 ) ||
+             FloatUtils::lt( value_x3, 0.5 ) || FloatUtils::gt( value_x3, 1 ) )
+        {
+            correctSolution = false;
+        }
+
+        if ( FloatUtils::isPositive( value_x1f ) && !FloatUtils::areEqual( value_x1b, value_x1f ) )
+        {
+            correctSolution = false;
+        }
+
+        if ( FloatUtils::isPositive( value_x2f ) && !FloatUtils::areEqual( value_x2b, value_x2f ) )
+        {
+            correctSolution = false;
+        }
+
+        if ( !correctSolution )
+            printFailed( "relu_feasible_2", start, end );
+        else
+            printPassed( "relu_feasible_2", start, end );
+    }
+};
+
+#endif // __Relu_Feasible_2_h__
+
+//
+// Local Variables:
+// compile-command: "make -C .. "
+// tags-file-name: "../TAGS"
+// c-basic-offset: 4
+// End:
+//

src/basis_factorization/tests/Test_SparseGaussianEliminator.h

@@ -247,7 +247,7 @@ class SparseGaussianEliminatorTestSuite : public CxxTest::TestSuite
                 TS_ASSERT( FloatUtils::areEqual( A[i], result[i] ) );
             }
 
-            double At[9];
+            double At[16];
             transposeMatrix( A, At, 4 );
             computeTransposedMatrixFromFactorization( &lu4, result );
 

src/engine/Engine.cpp

@@ -648,6 +648,8 @@ void Engine::extractSolution( InputQuery &inputQuery )
         {
             if ( _preprocessor.variableIsFixed( i ) )
                 inputQuery.setSolutionValue( i, _preprocessor.getFixedValue( i ) );
+            else if ( _preprocessor.variableIsMerged( i ) )
+                inputQuery.setSolutionValue( i, _tableau->getValue( _preprocessor.getMergedIndex( i ) ) );
             else
                 inputQuery.setSolutionValue( i, _tableau->getValue( _preprocessor.getNewIndex( i ) ) );
         }

src/engine/Preprocessor.cpp

@@ -67,6 +67,12 @@ InputQuery Preprocessor::preprocess( const InputQuery &query, bool attemptVariab
     if ( attemptVariableElimination )
         eliminateVariables();
 
+    DEBUG({
+            // For now, assume merged and fixed variable sets are disjoint
+            for ( const auto &fixed : _fixedVariables )
+                ASSERT( !_mergedVariables.exists( fixed.first ) );
+          });
+
     return _preprocessed;
 }
 
@@ -362,7 +368,6 @@ bool Preprocessor::processIdenticalVariables()
              !FloatUtils::isZero( equation._scalar ) )
             continue;
 
-        // Guy: this should never happen, so adding also an ASSERT
         ASSERT( term1._variable != term2._variable );
         if ( term1._variable == term2._variable )
             continue;
@@ -380,13 +385,14 @@ bool Preprocessor::processIdenticalVariables()
     _preprocessed.removeEquation( equToRemove );
     _preprocessed.mergeIdenticalVariables( v1, v2 );
 
-    double bestLowerBound = FloatUtils::max( _preprocessed.getLowerBound( v1 ), 
+    double bestLowerBound = FloatUtils::max( _preprocessed.getLowerBound( v1 ),
                                              _preprocessed.getLowerBound( v2 ) );
-    double bestUpperBound = FloatUtils::min( _preprocessed.getUpperBound( v1 ), 
+    double bestUpperBound = FloatUtils::min( _preprocessed.getUpperBound( v1 ),
                                              _preprocessed.getUpperBound( v2 ) );
     _preprocessed.setLowerBound( v2, bestLowerBound );
     _preprocessed.setUpperBound( v2, bestUpperBound );
-    _mergedVariables.insert( v1 );
+
+    _mergedVariables[v1] = v2;
     return true;
 }
 
@@ -395,23 +401,22 @@ void Preprocessor::eliminateVariables()
     // First, collect the variables that have become fixed, and their fixed values
 	for ( unsigned i = 0; i < _preprocessed.getNumberOfVariables(); ++i )
 	{
-        if ( FloatUtils::areEqual( _preprocessed.getLowerBound( i ), _preprocessed.getUpperBound( i ) )
-            || _mergedVariables.exists( i ) )
+        if ( FloatUtils::areEqual( _preprocessed.getLowerBound( i ), _preprocessed.getUpperBound( i ) ) )
             _fixedVariables[i] = _preprocessed.getLowerBound( i );
 	}
 
     // If there's nothing to eliminate, we're done
-    if ( _fixedVariables.empty() )
+    if ( _fixedVariables.empty() && _mergedVariables.empty() )
         return;
 
     if ( _statistics )
-        _statistics->ppSetNumEliminatedVars( _fixedVariables.size() );
+        _statistics->ppSetNumEliminatedVars( _fixedVariables.size() + _mergedVariables.size() );
 
     // Compute the new variable indices, after the elimination of fixed variables
  	int offset = 0;
 	for ( unsigned i = 0; i < _preprocessed.getNumberOfVariables(); ++i )
 	{
-        if ( _fixedVariables.exists( i ) )
+        if ( _fixedVariables.exists( i ) || _mergedVariables.exists( i ) )
             ++offset;
         else
             _oldIndexToNewIndex[i] = i - offset;
@@ -424,10 +429,13 @@ void Preprocessor::eliminateVariables()
     while ( equation != equations.end() )
 	{
         // Each equation is of the form sum(addends) = scalar. So, any fixed variable
-        // needs to be subtracted from the scalar.
+        // needs to be subtracted from the scalar. Merged variables should have already
+        // been removed, so we don't care about them
         List<Equation::Addend>::iterator addend = equation->_addends.begin();
         while ( addend != equation->_addends.end() )
         {
+            ASSERT( !_mergedVariables.exists( addend->_variable ) );
+
             if ( _fixedVariables.exists( addend->_variable ) )
             {
                 // Addend has to go...
@@ -496,7 +504,7 @@ void Preprocessor::eliminateVariables()
     // Update the lower/upper bound maps
     for ( unsigned i = 0; i < _preprocessed.getNumberOfVariables(); ++i )
 	{
-        if ( _fixedVariables.exists( i ) )
+        if ( _fixedVariables.exists( i ) || _mergedVariables.exists( i ) )
             continue;
 
         ASSERT( _oldIndexToNewIndex.at( i ) <= i );
@@ -522,6 +530,31 @@ void Preprocessor::eliminateVariables()
 
                 _preprocessed._debuggingSolution.erase( i );
             }
+            else if ( _mergedVariables.exists( i ) )
+            {
+                unsigned oldVar = i;
+                unsigned newVar = _mergedVariables[i];
+
+                if ( !_preprocessed._debuggingSolution.exists( newVar ) )
+                {
+                    _preprocessed._debuggingSolution[newVar] = _preprocessed._debuggingSolution[oldVar];
+                }
+                else
+                {
+                    if ( !FloatUtils::areEqual ( _preprocessed._debuggingSolution[newVar],
+                                                 _preprocessed._debuggingSolution[oldVar] ) )
+                        throw ReluplexError( ReluplexError::DEBUGGING_ERROR,
+                                             Stringf( "Variable %u fixed to %.5lf, "
+                                                      "merged into %u which was fixed to %.5lf",
+                                                      oldVar,
+                                                      _mergedVariables[oldVar],
+                                                      newVar,
+                                                      _mergedVariables[newVar] ).ascii() );
+
+                }
+
+                _preprocessed._debuggingSolution.erase( oldVar );
+            }
             else
             {
                 _preprocessed._debuggingSolution[_oldIndexToNewIndex[i]] =
@@ -534,7 +567,7 @@ void Preprocessor::eliminateVariables()
     }
 
     // Adjust the number of variables in the query
-    _preprocessed.setNumberOfVariables( _preprocessed.getNumberOfVariables() - _fixedVariables.size() );
+    _preprocessed.setNumberOfVariables( _preprocessed.getNumberOfVariables() - _fixedVariables.size() - _mergedVariables.size() );
 }
 
 bool Preprocessor::variableIsFixed( unsigned index ) const
@@ -547,6 +580,16 @@ double Preprocessor::getFixedValue( unsigned index ) const
     return _fixedVariables.at( index );
 }
 
+bool Preprocessor::variableIsMerged( unsigned index ) const
+{
+    return _mergedVariables.exists( index );
+}
+
+unsigned Preprocessor::getMergedIndex( unsigned index ) const
+{
+    return _mergedVariables.at( index );
+}
+
 unsigned Preprocessor::getNewIndex( unsigned oldIndex ) const
 {
     if ( _oldIndexToNewIndex.exists( oldIndex ) )
@@ -574,6 +617,18 @@ void Preprocessor::addPlAuxiliaryEquations()
         _preprocessed.addEquation( equation );
 }
 
+void Preprocessor::dumpAllBounds( const String &message )
+{
+    printf( "\nPP: Dumping all bounds (%s)\n", message.ascii() );
+
+    for ( unsigned i = 0; i < _preprocessed.getNumberOfVariables(); ++i )
+    {
+        printf( "\tx%u: [%5.2lf, %5.2lf]\n", i, _preprocessed.getLowerBound( i ), _preprocessed.getUpperBound( i ) );
+    }
+
+    printf( "\n" );
+}
+
 //
 // Local Variables:
 // compile-command: "make -C ../.. "