From 636f80fbf009e22c3c8bec6be2c5f39f5229b764 Mon Sep 17 00:00:00 2001
From: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Date: Fri, 26 Jul 2019 23:57:01 -0700
Subject: [PATCH 1/2] do not perform rounding when printing models (#158)

---
 src/engine/DnCManager.cpp | 4 ++--
 src/engine/Marabou.cpp    | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/engine/DnCManager.cpp b/src/engine/DnCManager.cpp
index 39176eae0..3d841d8a6 100644
--- 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
index 646e4c877..48f6b5bff 100644
--- 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 )

From 58719915b0972af251f6da4d4886b6a007623cbc Mon Sep 17 00:00:00 2001
From: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Date: Tue, 30 Jul 2019 13:42:08 -0700
Subject: [PATCH 2/2] Property parser scalar check (#159)

* Rename parsing function (and some todos)

*  property-input: make sure the right side of an equation is a scalar

* made extractScalar static

* update header file

* do not allow equality constraints on output variables

* Revert "do not allow equality constraints on output variables"

This reverts commit 80453519c355af242e9bdeb8e3df79ba74029c91.

* removed unnecessary todo

* minor
---
 src/input_parsers/PropertyParser.cpp | 28 +++++++++++++++++++++-------
 src/input_parsers/PropertyParser.h   |  3 +--
 2 files changed, 22 insertions(+), 9 deletions(-)

diff --git a/src/input_parsers/PropertyParser.cpp b/src/input_parsers/PropertyParser.cpp
index 22ff99593..23f34b181 100644
--- 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
index 9dfc9400e..038745a50 100644
--- 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__