Merge pull request #1 from guykatzz/master

test
NeuralNetworkVerification · Jul 31, 2019 · 6a1696b · 6a1696b
2 parents b1dbe4c + fbdbf74
commit 6a1696b
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 13 deletions.
diff --git a/src/engine/DnCManager.cpp b/src/engine/DnCManager.cpp
@@ -245,7 +245,7 @@ void DnCManager::printResult()
         printf( "Input assignment:\n" );
         for ( unsigned i = 0; i < inputQuery->getNumInputVariables(); ++i )
         {
-            printf( "\tx%u = %8.4lf\n", i, inputQuery->getSolutionValue( inputQuery->inputVariableByIndex( i ) ) );
+            printf( "\tx%u = %lf\n", i, inputQuery->getSolutionValue( inputQuery->inputVariableByIndex( i ) ) );
             inputs[i] = inputQuery->getSolutionValue( inputQuery->inputVariableByIndex( i ) );
         }
 
@@ -255,7 +255,7 @@ void DnCManager::printResult()
         printf( "\n" );
         printf( "Output:\n" );
         for ( unsigned i = 0; i < inputQuery->getNumOutputVariables(); ++i )
-            printf( "\ty%u = %8.4lf\n", i, outputs[i] );
+            printf( "\ty%u = %lf\n", i, outputs[i] );
         printf( "\n" );
         break;
     }

diff --git a/src/engine/Marabou.cpp b/src/engine/Marabou.cpp
@@ -108,12 +108,12 @@ void Marabou::displayResults( unsigned long long microSecondsElapsed ) const
 
         printf( "Input assignment:\n" );
         for ( unsigned i = 0; i < _inputQuery.getNumInputVariables(); ++i )
-            printf( "\tx%u = %8.4lf\n", i, _inputQuery.getSolutionValue( _inputQuery.inputVariableByIndex( i ) ) );
+            printf( "\tx%u = %lf\n", i, _inputQuery.getSolutionValue( _inputQuery.inputVariableByIndex( i ) ) );
 
         printf( "\n" );
         printf( "Output:\n" );
         for ( unsigned i = 0; i < _inputQuery.getNumOutputVariables(); ++i )
-            printf( "\ty%u = %8.4lf\n", i, _inputQuery.getSolutionValue( _inputQuery.outputVariableByIndex( i ) ) );
+            printf( "\ty%u = %lf\n", i, _inputQuery.getSolutionValue( _inputQuery.outputVariableByIndex( i ) ) );
         printf( "\n" );
     }
     else if ( result == Engine::TIMEOUT )

diff --git a/src/input_parsers/PropertyParser.cpp b/src/input_parsers/PropertyParser.cpp
@@ -16,7 +16,20 @@
 #include "Debug.h"
 #include "File.h"
 #include "InputParserError.h"
+#include "MStringf.h"
 #include "PropertyParser.h"
+#include <regex>
+
+static bool isScalar( const String &token )
+{
+    const std::regex floatRegex( "[-+]?[0-9]*\\.?[0-9]+" );
+    return std::regex_match( token.ascii(), floatRegex );
+}
+
+static double extractScalar( const String &token )
+{
+    return atof( token.ascii() );
+}
 
 void PropertyParser::parse( const String &propertyFilePath, InputQuery &inputQuery )
 {
@@ -53,9 +66,15 @@ void PropertyParser::processSingleLine( const String &line, InputQuery &inputQue
         throw InputParserError( InputParserError::UNEXPECTED_INPUT, line.ascii() );
 
     auto it = tokens.rbegin();
+    if ( !isScalar( *it ) )
+    {
+        Stringf message( "Right handside must be scalar in the line: %s", line.ascii() );
+        throw InputParserError( InputParserError::UNEXPECTED_INPUT, message.ascii() );
+    }
+
     double scalar = extractScalar( *it );
     ++it;
-    Equation::EquationType type = extractSign( *it );
+    Equation::EquationType type = extractRelationSymbol( *it );
     ++it;
 
     // Now extract the addends. In the special case where we only have
@@ -171,7 +190,7 @@ void PropertyParser::processSingleLine( const String &line, InputQuery &inputQue
     }
 }
 
-Equation::EquationType PropertyParser::extractSign( const String &token )
+Equation::EquationType PropertyParser::extractRelationSymbol( const String &token )
 {
     if ( token == ">=" )
         return Equation::GE;
@@ -183,11 +202,6 @@ Equation::EquationType PropertyParser::extractSign( const String &token )
     throw InputParserError( InputParserError::UNEXPECTED_INPUT, token.ascii() );
 }
 
-double PropertyParser::extractScalar( const String &token )
-{
-    return atof( token.ascii() );
-}
-
 //
 // Local Variables:
 // compile-command: "make -C ../.. "

diff --git a/src/input_parsers/PropertyParser.h b/src/input_parsers/PropertyParser.h
@@ -33,8 +33,7 @@ class PropertyParser
 
 private:
     void processSingleLine( const String &line, InputQuery &inputQuery );
-    Equation::EquationType extractSign( const String &token );
-    double extractScalar( const String &token );
+    Equation::EquationType extractRelationSymbol( const String &token );
 };
 
 #endif // __PropertyParser_h__