Fix formatting in Constraint classes and tests

Author: AleksandarZeljic

src/engine/AbsoluteValueConstraint.cpp

@@ -126,7 +126,7 @@ void AbsoluteValueConstraint::notifyLowerBound( unsigned variable, double bound
 
     if ( _boundManager == nullptr && existsLowerBound( variable ) &&
          !FloatUtils::gt( bound, getLowerBound( variable ) ) )
-      return;
+        return;
 
     setLowerBound( variable, bound );
 
@@ -180,7 +180,7 @@ void AbsoluteValueConstraint::notifyUpperBound( unsigned variable, double bound
          !FloatUtils::lt( bound, getUpperBound( variable ) ) )
         return;
 
-     setUpperBound( variable, bound );
+    setUpperBound( variable, bound );
     // Check whether the phase has become fixed
     fixPhaseIfNeeded();
 
@@ -321,7 +321,7 @@ List<PiecewiseLinearConstraint::Fix> AbsoluteValueConstraint::getPossibleFixes()
     return fixes;
 }
 
-List<PiecewiseLinearConstraint::Fix> AbsoluteValueConstraint::getSmartFixes( ITableau */* tableau */ ) const
+List<PiecewiseLinearConstraint::Fix> AbsoluteValueConstraint::getSmartFixes( ITableau * /* tableau */ ) const
 {
     return getPossibleFixes();
 }
@@ -601,8 +601,7 @@ void AbsoluteValueConstraint::getEntailedTightenings( List<Tightening> &tighteni
     }
 }
 
-void AbsoluteValueConstraint::transformToUseAuxVariables( InputQuery
-                                                                  &inputQuery )
+void AbsoluteValueConstraint::transformToUseAuxVariables( InputQuery &inputQuery )
 {
     /*
       We want to add the two equations
@@ -661,7 +660,7 @@ void AbsoluteValueConstraint::getCostFunctionComponent( LinearExpression &cost,
                                                         PhaseStatus phase ) const
 {
     // If the constraint is not active or is fixed, it contributes nothing
-    if( !isActive() || phaseFixed() )
+    if ( !isActive() || phaseFixed() )
         return;
 
     ASSERT( phase == ABS_PHASE_NEGATIVE || phase == ABS_PHASE_POSITIVE );

src/engine/AbsoluteValueConstraint.h

@@ -23,8 +23,8 @@
  **   * context dependent mode, used during the search.
  **
  ** Invoking initializeCDOs method activates the context dependent mode, and the
- ** AbsoluteValueConstraint object synchronizes its state automatically with the central
- ** Context object.
+ ** AbsoluteValueConstraint object synchronizes its state automatically with the
+ ** central Context object.
  **/
 
 #ifndef __AbsoluteValueConstraint_h__
@@ -34,7 +34,6 @@
 
 class AbsoluteValueConstraint : public PiecewiseLinearConstraint
 {
-
 public:
     /*
       The f variable is the absolute value of the b variable:
@@ -61,8 +60,8 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint
     /*
       Register/unregister the constraint with a talbeau.
      */
-    void registerAsWatcher( ITableau *tableau) override;
-    void unregisterAsWatcher( ITableau *tableau) override;
+    void registerAsWatcher( ITableau *tableau ) override;
+    void unregisterAsWatcher( ITableau *tableau ) override;
 
     /*
       These callbacks are invoked when a watched variable's value
@@ -114,8 +113,8 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint
 
     /*
        Returns a list of all cases - { ABS_POSITIVE, ABS_NEGATIVE }
-       The order of returned cases affects the search, and this method is where related
-       heuristics should be implemented.
+       The order of returned cases affects the search, and this method is where
+       related heuristics should be implemented.
      */
     List<PhaseStatus> getAllCases() const override;
 
@@ -232,4 +231,3 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint
 };
 
 #endif // __AbsoluteValueConstraint_h__
-

src/engine/DisjunctionConstraint.cpp

@@ -49,24 +49,24 @@ DisjunctionConstraint::DisjunctionConstraint( const String &serializedDisjunctio
         ( 5, serializedDisjunction.length() - 5 );
     List<String> values = serializedValues.tokenize( "," );
     auto val = values.begin();
-    unsigned numDisjuncts = atoi(val->ascii());
+    unsigned numDisjuncts = atoi( val->ascii() );
     ++val;
     for ( unsigned i = 0; i < numDisjuncts; ++i )
     {
         PiecewiseLinearCaseSplit split;
-        unsigned numBounds = atoi(val->ascii());
+        unsigned numBounds = atoi( val->ascii() );
         ++val;
         for ( unsigned bi = 0; bi < numBounds; ++bi )
         {
-            Tightening::BoundType type = ( *val == "l") ? Tightening::LB : Tightening::UB;
+            Tightening::BoundType type = ( *val == "l" ) ? Tightening::LB : Tightening::UB;
             ++val;
-            unsigned var = atoi(val->ascii());
+            unsigned var = atoi( val->ascii() );
             ++val;
-            double bd = atof(val->ascii());
+            double bd = atof( val->ascii() );
             ++val;
-            split.storeBoundTightening( Tightening(var, bd, type) );
+            split.storeBoundTightening( Tightening( var, bd, type ) );
         }
-        unsigned numEquations = atoi(val->ascii());
+        unsigned numEquations = atoi( val->ascii() );
 
         ++val;
         for ( unsigned ei = 0; ei < numEquations; ++ei )
@@ -78,29 +78,29 @@ DisjunctionConstraint::DisjunctionConstraint( const String &serializedDisjunctio
                 type = Equation::GE;
             else
             {
-                ASSERT( *val == "e");
+                ASSERT( *val == "e" );
             }
-            Equation eq(type);
+            Equation eq( type );
             ++val;
-            unsigned numAddends = atoi(val->ascii());
+            unsigned numAddends = atoi( val->ascii() );
             ++val;
             for ( unsigned ai = 0; ai < numAddends; ++ai )
             {
-                double coef = atof(val->ascii());
+                double coef = atof( val->ascii() );
                 ++val;
-                unsigned var = atoi(val->ascii());
+                unsigned var = atoi( val->ascii() );
                 ++val;
                 eq.addAddend( coef, var );
             }
-            eq.setScalar(atof(val->ascii()));
+            eq.setScalar( atof( val->ascii() ) );
             ++val;
-            split.addEquation(eq);
+            split.addEquation( eq );
         }
-        disjuncts.append(split);
+        disjuncts.append( split );
     }
     _disjuncts = disjuncts;
 
-    for ( unsigned ind = 0;  ind < disjuncts.size();  ++ind )
+    for ( unsigned ind = 0; ind < disjuncts.size(); ++ind )
         _feasibleDisjuncts.append( ind );
 
     extractParticipatingVariables();
@@ -151,11 +151,11 @@ void DisjunctionConstraint::notifyLowerBound( unsigned variable, double bound )
 
     if ( _boundManager == nullptr && existsLowerBound( variable ) &&
          !FloatUtils::gt( bound, getLowerBound( variable ) ) )
-      return;
+        return;
 
     setLowerBound( variable, bound );
 
-    //TODO: Maintain a mapping from variables to disjuncts and only check relevant
+    // TODO: Maintain a mapping from variables to disjuncts and only check relevant
     // disjuncts for feasibility
     updateFeasibleDisjuncts();
 }
@@ -167,11 +167,11 @@ void DisjunctionConstraint::notifyUpperBound( unsigned variable, double bound )
 
     if ( _boundManager == nullptr && existsUpperBound( variable ) &&
          !FloatUtils::lt( bound, getUpperBound( variable ) ) )
-      return;
+        return;
 
     setUpperBound( variable, bound );
 
-    //TODO: Maintain a mapping from variables to disjuncts and only check relevant
+    // TODO: Maintain a mapping from variables to disjuncts and only check relevant
     // disjuncts for feasibility
     updateFeasibleDisjuncts();
 }
@@ -207,7 +207,7 @@ List<PiecewiseLinearConstraint::Fix> DisjunctionConstraint::getPossibleFixes() c
     return List<PiecewiseLinearConstraint::Fix>();
 }
 
-List<PiecewiseLinearConstraint::Fix> DisjunctionConstraint::getSmartFixes( ITableau */* tableau */ ) const
+List<PiecewiseLinearConstraint::Fix> DisjunctionConstraint::getSmartFixes( ITableau * /* tableau */ ) const
 {
     // Reluplex does not currently work with Gurobi.
     ASSERT( _gurobi == NULL );
@@ -230,29 +230,28 @@ List<PhaseStatus> DisjunctionConstraint::getAllCases() const
 
 PiecewiseLinearCaseSplit DisjunctionConstraint::getCaseSplit( PhaseStatus phase ) const
 {
-  ASSERT ( phase !=  PHASE_NOT_FIXED );
-  return _disjuncts.get( phaseStatusToInd( phase ) );
+    ASSERT( phase != PHASE_NOT_FIXED );
+    return _disjuncts.get( phaseStatusToInd( phase ) );
 }
 
 PhaseStatus DisjunctionConstraint::getPhaseStatus() const
 {
-    ASSERT ( phaseFixed() );
+    ASSERT( phaseFixed() );
     return indToPhaseStatus( *_feasibleDisjuncts.begin() );
 }
 
 PiecewiseLinearCaseSplit DisjunctionConstraint::getImpliedCaseSplit() const
 {
-    ASSERT ( isImplication() );
-    return _disjuncts.get( phaseStatusToInd ( getImpliedCase() ) );
+    ASSERT( isImplication() );
+    return _disjuncts.get( phaseStatusToInd( getImpliedCase() ) );
 }
 
 PiecewiseLinearCaseSplit DisjunctionConstraint::getValidCaseSplit() const
 {
     return getImpliedCaseSplit();
 }
 
-void DisjunctionConstraint::transformToUseAuxVariables( InputQuery
-                                                                &inputQuery )
+void DisjunctionConstraint::transformToUseAuxVariables( InputQuery &inputQuery )
 {
     Vector<PiecewiseLinearCaseSplit> newDisjuncts;
     for ( const auto &disjunct : _disjuncts )
@@ -390,39 +389,39 @@ bool DisjunctionConstraint::constraintObsolete() const
     return false; // A Disjunction is obsolete only when a literal is always true.
 }
 
-void DisjunctionConstraint::getEntailedTightenings( List<Tightening> &/* tightenings */ ) const
+void DisjunctionConstraint::getEntailedTightenings( List<Tightening> & /* tightenings */ ) const
 {
 }
 
 String DisjunctionConstraint::serializeToString() const
 {
     String s = "disj,";
-    s += Stringf("%u,", _disjuncts.size());
+    s += Stringf( "%u,", _disjuncts.size() );
     for ( const auto &disjunct : _disjuncts )
     {
-        s += Stringf("%u,", disjunct.getBoundTightenings().size());
+        s += Stringf( "%u,", disjunct.getBoundTightenings().size() );
         for ( const auto &bound : disjunct.getBoundTightenings() )
         {
             if ( bound._type == Tightening::LB )
-                s += Stringf("l,%u,%f,", bound._variable, bound._value);
+                s += Stringf( "l,%u,%f,", bound._variable, bound._value );
             else if ( bound._type == Tightening::UB )
-                s += Stringf("u,%u,%f,", bound._variable, bound._value);
+                s += Stringf( "u,%u,%f,", bound._variable, bound._value );
         }
-        s += Stringf("%u,", disjunct.getEquations().size());
+        s += Stringf( "%u,", disjunct.getEquations().size() );
         for ( const auto &equation : disjunct.getEquations() )
         {
             if ( equation._type == Equation::LE )
-                s += Stringf("l,");
+                s += Stringf( "l," );
             else if ( equation._type == Equation::GE )
-                s += Stringf("g,");
+                s += Stringf( "g," );
             else
-                s += Stringf("e,");
-            s += Stringf("%u,", equation._addends.size());
+                s += Stringf( "e," );
+            s += Stringf( "%u,", equation._addends.size() );
             for ( const auto &addend : equation._addends )
             {
-                s += Stringf("%f,%u,", addend._coefficient, addend._variable);
+                s += Stringf( "%f,%u,", addend._coefficient, addend._variable );
             }
-            s += Stringf("%f,", equation._scalar );
+            s += Stringf( "%f,", equation._scalar );
         }
     }
     return s;
@@ -495,7 +494,7 @@ void DisjunctionConstraint::updateFeasibleDisjuncts()
 
         for ( unsigned ind = 0; ind < _disjuncts.size(); ++ind )
         {
-          if ( caseSplitIsFeasible( _disjuncts.get( ind ) ) )
+            if ( caseSplitIsFeasible( _disjuncts.get( ind ) ) )
                 _feasibleDisjuncts.append( ind );
         }
     }

src/engine/DisjunctionConstraint.h

@@ -34,13 +34,13 @@
 #ifndef __DisjunctionConstraint_h__
 #define __DisjunctionConstraint_h__
 
-#include "Vector.h"
 #include "PiecewiseLinearConstraint.h"
+#include "Vector.h"
 
 class DisjunctionConstraint : public PiecewiseLinearConstraint
 {
 public:
-    ~DisjunctionConstraint() {};
+    ~DisjunctionConstraint(){};
     DisjunctionConstraint( const List<PiecewiseLinearCaseSplit> &disjuncts );
     DisjunctionConstraint( const Vector<PiecewiseLinearCaseSplit> &disjuncts );
     DisjunctionConstraint( const String &serializedDisjunction );
@@ -154,7 +154,7 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint
 
     virtual bool supportVariableElimination() const override
     {
-      return false;
+        return false;
     }
 
     /*
@@ -209,7 +209,7 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint
       still feasible, given the current variable bounds
     */
     void updateFeasibleDisjuncts();
-    bool caseSplitIsFeasible( const PiecewiseLinearCaseSplit & caseSplit ) const;
+    bool caseSplitIsFeasible( const PiecewiseLinearCaseSplit &caseSplit ) const;
 
     inline PhaseStatus indToPhaseStatus( unsigned ind ) const
     {
@@ -218,7 +218,7 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint
 
     inline unsigned phaseStatusToInd( PhaseStatus phase ) const
     {
-        //ASSERT( phase != PHASE_NOT_FIXED );
+        // ASSERT( phase != PHASE_NOT_FIXED );
         return static_cast<unsigned>( phase ) - 1;
     }
 };

src/engine/MaxConstraint.cpp

@@ -503,7 +503,7 @@ void MaxConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex )
         _auxToElement[auxVar] = newIndex;
 
         if ( _phaseStatus == variableToPhase( oldIndex ) )
-            _phaseStatus = variableToPhase( newIndex ) ;
+            _phaseStatus = variableToPhase( newIndex );
     }
     else
     {
@@ -615,7 +615,7 @@ void MaxConstraint::getCostFunctionComponent( LinearExpression &cost,
                                               PhaseStatus phase ) const
 {
     // If the constraint is not active or is fixed, it contributes nothing
-    if( !isActive() || phaseFixed() )
+    if ( !isActive() || phaseFixed() )
         return;
 
     if ( phase == MAX_PHASE_ELIMINATED )
@@ -669,7 +669,6 @@ String MaxConstraint::serializeToString() const
         // Will be ignored in any case
         output += Stringf( ",%u", 0 );
 
-    //serializeInfeasibleCases( output );
     return output;
 }
 

src/engine/MaxConstraint.h

@@ -46,9 +46,9 @@
 #ifndef __MaxConstraint_h__
 #define __MaxConstraint_h__
 
-#include "PiecewiseLinearConstraint.h"
 #include "LinearExpression.h"
 #include "Map.h"
+#include "PiecewiseLinearConstraint.h"
 
 #define MAX_VARIABLE_TO_PHASE_OFFSET 1