use tighten bound in extract bound

wu-haoze · Sep 11, 2024 · 49027b7 · 49027b7
1 parent 93cbbcf
commit 49027b7
Show file tree

Hide file tree

Showing 5 changed files with 53 additions and 10 deletions.
diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp
@@ -3765,30 +3765,30 @@ void Engine::extractBounds( IQuery &inputQuery )
             // Symbolically fixed variables are ignored
             if ( _preprocessor.variableIsUnusedAndSymbolicallyFixed( i ) )
             {
-                inputQuery.setLowerBound( i, FloatUtils::negativeInfinity() );
-                inputQuery.setUpperBound( i, FloatUtils::infinity() );
+                inputQuery.tightenLowerBound( i, FloatUtils::negativeInfinity() );
+                inputQuery.tightenUpperBound( i, FloatUtils::infinity() );
                 continue;
             }
 
             // Fixed variables are easy: return the value they've been fixed to.
             if ( _preprocessor.variableIsFixed( variable ) )
             {
-                inputQuery.setLowerBound( i, _preprocessor.getFixedValue( variable ) );
-                inputQuery.setUpperBound( i, _preprocessor.getFixedValue( variable ) );
+                inputQuery.tightenLowerBound( i, _preprocessor.getFixedValue( variable ) );
+                inputQuery.tightenUpperBound( i, _preprocessor.getFixedValue( variable ) );
                 continue;
             }
 
             // We know which variable to look for, but it may have been assigned
             // a new index, due to variable elimination
             variable = _preprocessor.getNewIndex( variable );
 
-            inputQuery.setLowerBound( i, _preprocessedQuery->getLowerBound( variable ) );
-            inputQuery.setUpperBound( i, _preprocessedQuery->getUpperBound( variable ) );
+            inputQuery.tightenLowerBound( i, _preprocessedQuery->getLowerBound( variable ) );
+            inputQuery.tightenUpperBound( i, _preprocessedQuery->getUpperBound( variable ) );
         }
         else
         {
-            inputQuery.setLowerBound( i, _preprocessedQuery->getLowerBound( i ) );
-            inputQuery.setUpperBound( i, _preprocessedQuery->getUpperBound( i ) );
+            inputQuery.tightenLowerBound( i, _preprocessedQuery->getLowerBound( i ) );
+            inputQuery.tightenUpperBound( i, _preprocessedQuery->getUpperBound( i ) );
         }
     }
 }
diff --git a/src/engine/IQuery.h b/src/engine/IQuery.h
@@ -37,6 +37,8 @@ class IQuery
 
     virtual void setLowerBound( unsigned variable, double bound ) = 0;
     virtual void setUpperBound( unsigned variable, double bound ) = 0;
+    virtual bool tightenLowerBound( unsigned variable, double bound ) = 0;
+    virtual bool tightenUpperBound( unsigned variable, double bound ) = 0;
     virtual double getLowerBound( unsigned variable ) const = 0;
     virtual double getUpperBound( unsigned variable ) const = 0;
 

diff --git a/src/engine/InputQuery.cpp b/src/engine/InputQuery.cpp
@@ -119,7 +119,7 @@ bool InputQuery::tightenLowerBound( unsigned variable, double bound )
     if ( variable >= _numberOfVariables )
     {
         throw MarabouError( MarabouError::VARIABLE_INDEX_OUT_OF_RANGE,
-                            Stringf( "Variable = %u, number of variables = %u (setLowerBound)",
+                            Stringf( "Variable = %u, number of variables = %u (tightenLowerBound)",
                                      variable,
                                      getNumberOfVariables() )
                                 .ascii() );
@@ -138,7 +138,7 @@ bool InputQuery::tightenUpperBound( unsigned variable, double bound )
     if ( variable >= _numberOfVariables )
     {
         throw MarabouError( MarabouError::VARIABLE_INDEX_OUT_OF_RANGE,
-                            Stringf( "Variable = %u, number of variables = %u (setUpperBound)",
+                            Stringf( "Variable = %u, number of variables = %u (tightenUpperBound)",
                                      variable,
                                      getNumberOfVariables() )
                                 .ascii() );

diff --git a/src/engine/Query.cpp b/src/engine/Query.cpp
@@ -81,6 +81,45 @@ void Query::setUpperBound( unsigned variable, double bound )
     _upperBounds[variable] = bound;
 }
 
+bool Query::tightenLowerBound( unsigned variable, double bound )
+{
+    if ( variable >= _numberOfVariables )
+    {
+        throw MarabouError( MarabouError::VARIABLE_INDEX_OUT_OF_RANGE,
+                            Stringf( "Variable = %u, number of variables = %u (tightenLowerBound)",
+                                     variable,
+                                     getNumberOfVariables() )
+                                .ascii() );
+    }
+
+    if ( !_lowerBounds.exists( variable ) || _lowerBounds[variable] < bound )
+    {
+        _lowerBounds[variable] = bound;
+        return true;
+    }
+    return false;
+}
+
+bool Query::tightenUpperBound( unsigned variable, double bound )
+{
+    if ( variable >= _numberOfVariables )
+    {
+        throw MarabouError( MarabouError::VARIABLE_INDEX_OUT_OF_RANGE,
+                            Stringf( "Variable = %u, number of variables = %u (tightenUpperBound)",
+                                     variable,
+                                     getNumberOfVariables() )
+                                .ascii() );
+    }
+
+    if ( !_upperBounds.exists( variable ) || _upperBounds[variable] > bound )
+    {
+        _upperBounds[variable] = bound;
+        return true;
+    }
+    return false;
+}
+
+
 void Query::addEquation( const Equation &equation )
 {
     _equations.append( equation );

diff --git a/src/engine/Query.h b/src/engine/Query.h
@@ -40,6 +40,8 @@ class Query : public IQuery
     void setNumberOfVariables( unsigned numberOfVariables );
     void setLowerBound( unsigned variable, double bound );
     void setUpperBound( unsigned variable, double bound );
+    bool tightenLowerBound( unsigned variable, double bound );
+    bool tightenUpperBound( unsigned variable, double bound );
 
     void addEquation( const Equation &equation );
     unsigned getNumberOfEquations() const;