Some fixes in AbsoluteValueConstraint and the preprocessor (#329)

* unserialize an absolute value constraint

* reduce the tolerance of abs and relu constraints

* abs constraint dumping

* preprocessor: declare UNSAT based on bounds from PLCs

* indentation

* higher precision

* review comments

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

Author: guykatzz

src/configuration/GlobalConfiguration.cpp

@@ -67,8 +67,8 @@ 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 double GlobalConfiguration::ABS_CONSTRAINT_COMPARISON_TOLERANCE = 0.001;
+const double GlobalConfiguration::RELU_CONSTRAINT_COMPARISON_TOLERANCE = 0.00001;
+const double GlobalConfiguration::ABS_CONSTRAINT_COMPARISON_TOLERANCE = 0.00001;
 
 const bool GlobalConfiguration::ONLY_AUX_INITIAL_BASIS = false;
 

src/engine/AbsoluteValueConstraint.cpp

@@ -30,6 +30,26 @@ AbsoluteValueConstraint::AbsoluteValueConstraint( unsigned b, unsigned f )
     setPhaseStatus( PhaseStatus::PHASE_NOT_FIXED );
 }
 
+AbsoluteValueConstraint::AbsoluteValueConstraint( const String &serializedAbs )
+    : _haveEliminatedVariables( false )
+{
+    String constraintType = serializedAbs.substring( 0, 13 );
+    ASSERT( constraintType == String( "absoluteValue" ) );
+
+    // Remove the constraint type in serialized form
+    String serializedValues = serializedAbs.substring( 14, serializedAbs.length() - 14 );
+    List<String> values = serializedValues.tokenize( "," );
+
+    ASSERT( values.size() == 2 );
+
+    auto var = values.begin();
+    _f = atoi( var->ascii() );
+    ++var;
+    _b = atoi( var->ascii() );
+
+    setPhaseStatus( PhaseStatus::PHASE_NOT_FIXED );
+}
+
 PiecewiseLinearFunctionType AbsoluteValueConstraint::getType() const
 {
     return PiecewiseLinearFunctionType::ABSOLUTE_VALUE;
@@ -274,6 +294,23 @@ void AbsoluteValueConstraint::eliminateVariable( unsigned variable, double /* fi
     _haveEliminatedVariables = true;
 }
 
+void AbsoluteValueConstraint::dump( String &output ) const
+{
+    output = Stringf( "AbsoluteValueCosntraint: x%u = Abs( x%u ). Active? %s. PhaseStatus = %u (%s).\n",
+                      _f, _b,
+                      _constraintActive ? "Yes" : "No",
+                      _phaseStatus, phaseToString( _phaseStatus ).ascii()
+                      );
+
+    output += Stringf( "b in [%s, %s], ",
+                       _lowerBounds.exists( _b ) ? Stringf( "%lf", _lowerBounds[_b] ).ascii() : "-inf",
+                       _upperBounds.exists( _b ) ? Stringf( "%lf", _upperBounds[_b] ).ascii() : "inf" );
+
+    output += Stringf( "f in [%s, %s]",
+                       _lowerBounds.exists( _f ) ? Stringf( "%lf", _lowerBounds[_f] ).ascii() : "-inf",
+                       _upperBounds.exists( _f ) ? Stringf( "%lf", _upperBounds[_f] ).ascii() : "inf" );
+}
+
 void AbsoluteValueConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex )
 {
     ASSERT( oldIndex == _b || oldIndex == _f );
@@ -429,6 +466,24 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
     }
 }
 
+String AbsoluteValueConstraint::phaseToString( PhaseStatus phase )
+{
+    switch ( phase )
+    {
+    case PHASE_NOT_FIXED:
+        return "PHASE_NOT_FIXED";
+
+    case PHASE_POSITIVE:
+        return "PHASE_POSITIVE";
+
+    case PHASE_NEGATIVE:
+        return "PHASE_NEGATIVE";
+
+    default:
+        return "UNKNOWN";
+    }
+};
+
 void AbsoluteValueConstraint::setPhaseStatus( PhaseStatus phaseStatus )
 {
     _phaseStatus = phaseStatus;

src/engine/AbsoluteValueConstraint.h

@@ -33,6 +33,7 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint
       f = | b |
     */
     AbsoluteValueConstraint( unsigned b, unsigned f );
+    AbsoluteValueConstraint( const String &serializedAbs );
 
     /*
       Get the type of this constraint.
@@ -126,6 +127,11 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint
     */
     void getEntailedTightenings( List<Tightening> &tightenings ) const;
 
+    /*
+      Dump the current state of the constraint.
+    */
+    void dump( String &output ) const;
+
     /*
       For preprocessing: get any auxiliary equations that this
       constraint would like to add to the equation pool. In the ReLU
@@ -163,6 +169,8 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint
     PhaseStatus _phaseStatus;
     void setPhaseStatus( PhaseStatus phaseStatus );
 
+    static String phaseToString( PhaseStatus phase );
+
     /*
       The two case splits.
     */

src/engine/Engine.cpp

@@ -1552,7 +1552,7 @@ bool Engine::applyValidConstraintCaseSplit( PiecewiseLinearConstraint *constrain
         String constraintString;
         constraint->dump( constraintString );
         ENGINE_LOG( Stringf( "A constraint has become valid. Dumping constraint: %s",
-                      constraintString.ascii() ).ascii() );
+                             constraintString.ascii() ).ascii() );
 
         constraint->setActiveConstraint( false );
         PiecewiseLinearCaseSplit validSplit = constraint->getValidCaseSplit();

src/engine/InputQuery.cpp

@@ -321,11 +321,11 @@ void InputQuery::saveQuery( const String &fileName )
 
     // Lower Bounds
     for ( const auto &lb : _lowerBounds )
-        queryFile->write( Stringf( "\n%d,%f", lb.first, lb.second ) );
+        queryFile->write( Stringf( "\n%d,%.10f", lb.first, lb.second ) );
 
     // Upper Bounds
     for ( const auto &ub : _upperBounds )
-        queryFile->write( Stringf( "\n%d,%f", ub.first, ub.second ) );
+        queryFile->write( Stringf( "\n%d,%.10f", ub.first, ub.second ) );
 
     // Equations
     i = 0;
@@ -338,9 +338,9 @@ void InputQuery::saveQuery( const String &fileName )
         queryFile->write( Stringf( "%01d,", e._type ) );
 
         // Equation scalar
-        queryFile->write( Stringf( "%f", e._scalar ) );
+        queryFile->write( Stringf( "%.10f", e._scalar ) );
         for ( const auto &a : e._addends )
-            queryFile->write( Stringf( ",%u,%f", a._variable, a._coefficient ) );
+            queryFile->write( Stringf( ",%u,%.10f", a._variable, a._coefficient ) );
 
         ++i;
     }

src/engine/Marabou.cpp

@@ -72,6 +72,7 @@ void Marabou::prepareInputQuery()
 
         printf( "InputQuery: %s\n", inputQueryFilePath.ascii() );
         _inputQuery = QueryLoader::loadQuery( inputQueryFilePath );
+        _inputQuery.constructNetworkLevelReasoner();
     }
     else
     {
@@ -104,21 +105,10 @@ void Marabou::prepareInputQuery()
             printf( "Property: None\n" );
 
         printf( "\n" );
-
-        /*
-          Step 3: extract options
-        */
-        int splitThreshold = Options::get()->getInt( Options::SPLIT_THRESHOLD );
-        if ( splitThreshold < 0 )
-        {
-            printf( "Invalid constraint violation threshold value %d,"
-                    " using default value %u.\n\n", splitThreshold,
-                    GlobalConfiguration::CONSTRAINT_VIOLATION_THRESHOLD );
-            splitThreshold = GlobalConfiguration::CONSTRAINT_VIOLATION_THRESHOLD;
-        }
-        _engine.setConstraintViolationThreshold( splitThreshold );
     }
 
+    extractSplittingThreshold();
+
     String queryDumpFilePath = Options::get()->getString( Options::QUERY_DUMP_FILE );
     if ( queryDumpFilePath.length() > 0 )
     {
@@ -203,6 +193,19 @@ void Marabou::displayResults( unsigned long long microSecondsElapsed ) const
     }
 }
 
+void Marabou::extractSplittingThreshold()
+{
+    int splitThreshold = Options::get()->getInt( Options::SPLIT_THRESHOLD );
+    if ( splitThreshold < 0 )
+    {
+        printf( "Invalid constraint violation threshold value %d,"
+                " using default value %u.\n\n", splitThreshold,
+                GlobalConfiguration::CONSTRAINT_VIOLATION_THRESHOLD );
+        splitThreshold = GlobalConfiguration::CONSTRAINT_VIOLATION_THRESHOLD;
+    }
+    _engine.setConstraintViolationThreshold( splitThreshold );
+}
+
 //
 // Local Variables:
 // compile-command: "make -C ../.. "

src/engine/Marabou.h

@@ -35,10 +35,11 @@ class Marabou
     InputQuery _inputQuery;
 
     /*
-      Extract the input files: network and property, and use them
-      to generate the input query
+      Extract the options and input files (network and property), and
+      use them to generate the input query
     */
     void prepareInputQuery();
+    void extractSplittingThreshold();
 
     /*
       Invoke the engine to solve the input query

src/engine/Preprocessor.cpp

@@ -439,6 +439,13 @@ bool Preprocessor::processConstraints()
                                        GlobalConfiguration::PREPROCESSOR_ALMOST_FIXED_THRESHOLD ) )
                 _preprocessed.setUpperBound( tightening._variable,
                                              _preprocessed.getLowerBound( tightening._variable ) );
+
+            if ( FloatUtils::gt( _preprocessed.getLowerBound( tightening._variable ),
+                                 _preprocessed.getUpperBound( tightening._variable ),
+                                 GlobalConfiguration::PREPROCESSOR_ALMOST_FIXED_THRESHOLD ) )
+            {
+                throw InfeasibleQueryException();
+            }
 		}
 	}
 

src/engine/tests/Test_AbsoluteValueConstraint.h

@@ -1048,6 +1048,25 @@ class AbsoluteValueConstraintTestSuite : public CxxTest::TestSuite
         for ( const auto &it : a )
             TS_ASSERT( b.exists( it ) );
     }
+
+    void test_serialize_and_unserialize()
+    {
+        unsigned b = 42;
+        unsigned f = 7;
+
+        AbsoluteValueConstraint originalAbs( b, f );
+        originalAbs.notifyLowerBound( b, -10 );
+        originalAbs.notifyUpperBound( f, 5 );
+        originalAbs.notifyUpperBound( f, 5 );
+
+        String originalSerialized = originalAbs.serializeToString();
+        AbsoluteValueConstraint recoveredAbs( originalSerialized );
+
+        TS_ASSERT_EQUALS( originalAbs.serializeToString(),
+                          recoveredAbs.serializeToString() );
+
+        TS_ASSERT_EQUALS( originalSerialized, "absoluteValue,7,42" );
+    }
 };
 
 //

src/query_loader/QueryLoader.cpp

@@ -209,6 +209,10 @@ InputQuery QueryLoader::loadQuery( const String &fileName )
         {
             constraint = new MaxConstraint( serializeConstraint );
         }
+        else if ( coType == "absoluteValue" )
+        {
+            constraint = new AbsoluteValueConstraint( serializeConstraint );
+        }
         else
         {
             throw MarabouError( MarabouError::UNSUPPORTED_PIECEWISE_CONSTRAINT, Stringf( "Unsupported piecewise constraint: %s\n", coType.ascii() ).ascii() );