formatting

Author: omriisack

src/proofs/AletheProofWriter.cpp

@@ -410,7 +410,6 @@ void AletheProofWriter::writeReluLemma(
     const std::shared_ptr<GroundBoundManager::GroundBoundEntry> &lemmaEntry,
     const ReluConstraint *relu )
 {
-
     ASSERT( lemmaEntry->lemma && lemmaEntry->lemma->getConstraintType() == RELU );
     const std::shared_ptr<PLCLemma> lemma = lemmaEntry->lemma;
 

src/proofs/AletheProofWriter.h

@@ -76,7 +76,8 @@ class AletheProofWriter
 
     void writeTableauAssumptions();
 
-    void writeReluLemma( const std::shared_ptr<GroundBoundManager::GroundBoundEntry> &lemmaEntry, const ReluConstraint *relu );
+    void writeReluLemma( const std::shared_ptr<GroundBoundManager::GroundBoundEntry> &lemmaEntry,
+                         const ReluConstraint *relu );
 
     void insertCurrentBoundsToVec( bool isUpper, Vector<double> &boundsVec );
 

src/proofs/JsonWriter.cpp

@@ -180,11 +180,13 @@ void JsonWriter::writeUnsatCertificateNode( const UnsatCertificateNode *node,
 
         unsigned counter = 0;
         unsigned size = node->getChildren().size();
-        List<UnsatCertificateNode *> childrenInFixedOrder =  List<UnsatCertificateNode *>();
-        const List<Tightening> &backChildTightening = node->getChildren().back()->getSplit().getBoundTightenings();
+        List<UnsatCertificateNode *> childrenInFixedOrder = List<UnsatCertificateNode *>();
+        const List<Tightening> &backChildTightening =
+            node->getChildren().back()->getSplit().getBoundTightenings();
 
         // Insert the inactive phase first
-        if (backChildTightening.back()._type == Tightening::LB || backChildTightening.front()._type == Tightening::LB )
+        if ( backChildTightening.back()._type == Tightening::LB ||
+             backChildTightening.front()._type == Tightening::LB )
         {
             childrenInFixedOrder.append( node->getChildren().front() );
             childrenInFixedOrder.append( node->getChildren().back() );

src/proofs/PlcLemma.h

@@ -34,7 +34,7 @@ class PLCLemma
               const Vector<SparseUnsortedList> &explanation,
               PiecewiseLinearFunctionType constraintType,
               double minTargetBound,
-              unsigned id);
+              unsigned id );
 
     ~PLCLemma();
 

src/proofs/SmtLibWriter.cpp

@@ -255,8 +255,7 @@ void SmtLibWriter::addMaxConstraint( unsigned f,
             for ( unsigned i = 0; i < size - 2; ++i )
                 assertRowLine += String( ")" );
 
-            assertRowLine +=
-                " (= x" + std::to_string( f ) + " x" + std::to_string( element ) + ")";
+            assertRowLine += " (= x" + std::to_string( f ) + " x" + std::to_string( element ) + ")";
 
             instance.append( assertRowLine + "))\n" );
         }

src/proofs/SmtLibWriter.h

@@ -48,8 +48,11 @@ class SmtLibWriter
     /*
       Adds a line representing a ReLU constraint, in SMTLIB format, to the SMTLIB instance
     */
-    static void
-    addReLUConstraint( unsigned b, unsigned f, unsigned aux, const PhaseStatus status, List<String> &instance );
+    static void addReLUConstraint( unsigned b,
+                                   unsigned f,
+                                   unsigned aux,
+                                   const PhaseStatus status,
+                                   List<String> &instance );
 
     /*
       Adds a line representing a sign constraint, in SMTLIB format, to the SMTLIB instance
@@ -125,13 +128,14 @@ class SmtLibWriter
     /*
       Wrapper functions calling all previous functions
     */
-    static List<String> convertToSmtLib( unsigned numOfTableauRows,
-                                   unsigned numOfVariables,
-                                   const Vector<double> &upperBounds,
-                                   const Vector<double> &lowerBounds,
-                                   const SparseMatrix *tableau,
-                                   const List<Equation> &additionalEquations,
-                                   const List<PiecewiseLinearConstraint *> &problemConstraints );
+    static List<String>
+    convertToSmtLib( unsigned numOfTableauRows,
+                     unsigned numOfVariables,
+                     const Vector<double> &upperBounds,
+                     const Vector<double> &lowerBounds,
+                     const SparseMatrix *tableau,
+                     const List<Equation> &additionalEquations,
+                     const List<PiecewiseLinearConstraint *> &problemConstraints );
 
 
     static void writeToSmtLibFile( const String &fileName,

src/proofs/UnsatCertificateNode.h

@@ -35,7 +35,10 @@ enum DelegationStatus : unsigned {
 class UnsatCertificateNode
 {
 public:
-    UnsatCertificateNode( UnsatCertificateNode *parent, PiecewiseLinearCaseSplit split, unsigned splitNum, unsigned id );
+    UnsatCertificateNode( UnsatCertificateNode *parent,
+                          PiecewiseLinearCaseSplit split,
+                          unsigned splitNum,
+                          unsigned id );
     ~UnsatCertificateNode();
 
     /*