Merge pull request NeuralNetworkVerification#40 from NeuralNetworkVer…

…ification/master

Merge from master

.codecov.yml

@@ -1,5 +1,31 @@
+# Check if this file is valid by running in bash:
+# curl -X POST --data-binary @.codecov.yml https://codecov.io/validate
+
 comment: false
 
 ignore:
   - "**/__init__.py"
   - "maraboupy/test"
+
+coverage:
+  status:
+    # Make sure the total coverage decreased by at most 1%
+    project:
+      default:
+        target: auto
+        threshold: 1%
+        base: auto
+        paths:
+          - "src"
+          - "maraboupy"
+    # Make sure the new added code is at least 80% covered 
+    patch: 
+      default:
+        target: 80%
+        base: auto
+        paths:
+          - "src"
+          - "maraboupy"
+
+
+

.gitignore

@@ -19,6 +19,8 @@ tools/boost_1_68_0
 /tools/boost.unzipped
 /tools/boost_1_68_0.tar.gz
 /tools/pybind11-2.3.0
+/tools/OpenBLAS-0.3.9/
+/tools/OpenBLASv0.3.9.tar.gz
 /cpp_interface_example/example.elf
 /src/input_parsers/mps_example/mps.elf
 

CMakeLists.txt

@@ -205,7 +205,7 @@ if (${ENABLE_OPENBLAS} AND NOT MSVC)
     add_compile_definitions(ENABLE_OPENBLAS)
     #OpenBLAS
     if(NOT EXISTS "${OPENBLAS_DIR}/installed/lib/libopenblas.a")
-        execute_process(COMMAND ${TOOLS_DIR}/get-openBLAS.sh)
+        execute_process(COMMAND ${TOOLS_DIR}/download_openBLAS.sh)
     endif()
 
     add_library(${OPENBLAS_LIB} SHARED IMPORTED)

README.md

@@ -45,12 +45,6 @@ Download
 ------------------------------------------------------------------------------
 The latest version of Marabou is available on [https://github.com/NeuralNetworkVerification/Marabou].
 
-## Static binaries
-
-Pre-compiled binary for Linux is available:
-
-[marabou-1.0-x86_64-linux.zip](https://aisafety.stanford.edu/marabou/marabou-1.0-x86_64-linux.zip)
-
 Build and Dependencies
 ------------------------------------------------------------------------------
 
@@ -134,26 +128,10 @@ written to build/Debug.
 It may be useful to set up a Python virtual environment, see
 [here](https://docs.python.org/3/tutorial/venv.html) for more information.
 
-The python interface was tested only on versions >3.5 and >2.7. The build process preffers python3 but will work if there is only python 2.7 avilable. (To control the default change the DEFAULT_PYTHON_VERSION variable).  
+The python interface was tested only on versions >3.5 and >2.7. The build process prefers python3 but will work if there is only python 2.7 available. (To control the default change the DEFAULT_PYTHON_VERSION variable).  
 The Python interface requires *pybind11* (which is automatically downloaded). 
-To also build the python API on Linux or MacOS, run:
-```
-cd path/to/marabou/repo/folder
-mkdir build 
-cd build
-cmake .. -DBUILD_PYTHON=ON
-cmake --build .
-```
-On Windows, run:
-```
-cd path\to\marabou\repo\folder
-mkdir build 
-cd build
-cmake .. -G"Visual Studio 15 2017 Win64" -DBUILD_PYTHON=ON
-cmake --build . --config Release
-```
-Make sure the detected python ("Found PythonInterp: ....") is a windows python and not cygwin or something like that (if it is cygwin, use -DPYTHON_EXECUTABLE flag to override the default python, or manuialy download the linux pybind and locate it in the tools directory)
-
+By default Marabou builds also the python API, the BUILD_PYTHON variable
+controls that.
 This process will produce the binary file and the shared library for the Python 
 API. The shared library will be in the maraboupy folder for Linux and MacOS. 
 On Windows, the shared library is written to a Release subfolder in maraboupy, 
@@ -171,6 +149,16 @@ JUPYTER_PATH=JUPYTER_PATH:/path/to/marabou/folder
 and Marabou is ready to be used from a Python or a Jupyter script. On Windows, 
 edit your environmental variables so PYTHONPATH includes the marabou folder.
 
+#### Troubleshooting
+
+- On Windows - Make sure the detected python ("Found PythonInterp: ....") is a windows python and not cygwin or something like that (if it is cygwin, use -DPYTHON_EXECUTABLE flag to override the default python, or manuialy download the linux pybind and locate it in the tools directory)
+
+- 32bit Python - By default we install a 64bit Marabou and consequently a 64bit
+  python interface, the maraboupy/build_python_x86.sh file builds a 32bit
+  version.
+
+
+
 Getting Started
 -----------------------------------------------------------------------------
 ### To run Marabou from Command line 

maraboupy/MarabouNetwork.py

@@ -3,7 +3,7 @@
 /*! \file MarabouNetwork.py
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher Lazarus, Shantanu Thakoor, Andrew Wu
+ **   Christopher Lazarus, Shantanu Thakoor, Andrew Wu, Kyle Julian
  ** This file is part of the Marabou project.
  ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -17,6 +17,7 @@
 '''
 
 from maraboupy import MarabouCore
+from maraboupy import MarabouUtils
 import numpy as np
 
 class MarabouNetwork:
@@ -128,6 +129,42 @@ def participatesInPLConstraint(self, x):
         # ReLUs
         return x in self.varsParticipatingInConstraints
 
+    def addEquality(self, vars, coeffs, scalar):
+        """Function to add equality constraint to network
+
+        .. math::
+            \sum_i \text{vars}_i \times \text{coeffs}_i = \text{scalar}
+
+        Args:
+            vars (list of int): Variable numbers
+            coeffs (list of float): Coefficients
+            scalar (float): Right hand side constant of equation
+        """
+        assert len(vars)==len(coeffs)
+        e = MarabouUtils.Equation()
+        for i in range(len(vars)):
+            e.addAddend(coeffs[i], vars[i])
+        e.setScalar(scalar)
+        self.addEquation(e)
+
+    def addInequality(self, vars, coeffs, scalar):
+        """Function to add inequality constraint to network
+
+        .. math::
+            \sum_i \text{vars}_i \times \text{coeffs}_i \le \text{scalar}
+
+        Args:
+            vars (list of int): Variable numbers
+            coeffs (list of float): Coefficients
+            scalar (float): Right hand side constant of inequality
+        """
+        assert len(vars)==len(coeffs)
+        e = MarabouUtils.Equation(MarabouCore.Equation.LE)
+        for i in range(len(vars)):
+            e.addAddend(coeffs[i], vars[i])
+        e.setScalar(scalar)
+        self.addEquation(e)
+
     def getMarabouQuery(self):
         """
         Function to convert network into Marabou Query

maraboupy/MarabouUtils.py

@@ -47,36 +47,3 @@ def addAddend(self, c, x):
         """
         self.addendList += [(c, x)]
 
-def addEquality(network, vars, coeffs, scalar):
-    """
-    Function to conveniently add equality constraint to network
-    \sum_i vars_i*coeffs_i = scalar
-    Arguments:
-        network: (MarabouNetwork) to which to add constraint
-        vars: (list) of variable numbers
-        coeffs: (list) of coefficients
-        scalar: (float) representing RHS of equation
-    """
-    assert len(vars)==len(coeffs)
-    e = Equation()
-    for i in range(len(vars)):
-        e.addAddend(coeffs[i], vars[i])
-    e.setScalar(scalar)
-    network.addEquation(e)
-
-def addInequality(network, vars, coeffs, scalar):
-    """
-    Function to conveniently add inequality constraint to network
-    \sum_i vars_i*coeffs_i <= scalar
-    Arguments:
-        network: (MarabouNetwork) to which to add constraint
-        vars: (list) of variable numbers
-        coeffs: (list) of coefficients
-        scalar: (float) representing RHS of equation
-    """
-    assert len(vars)==len(coeffs)
-    e = Equation(MarabouCore.Equation.LE)
-    for i in range(len(vars)):
-        e.addAddend(coeffs[i], vars[i])
-    e.setScalar(scalar)
-    network.addEquation(e)

maraboupy/test/test_utils.py → maraboupy/test/test_equation.py

@@ -5,7 +5,6 @@
 
 import pytest
 from .. import Marabou
-from .. import MarabouUtils
 import numpy as np
 import os
 
@@ -28,7 +27,7 @@ def test_equality_output():
 
         # Add output equality constraints
         outputValue = np.random.random() * 5 + 3
-        MarabouUtils.addEquality(network, [outputVar], [1.0], outputValue)
+        network.addEquality([outputVar], [1.0], outputValue)
 
         # Call to Marabou solver
         vals, _ = network.solve(options = OPT, verbose = False)
@@ -49,7 +48,7 @@ def test_equality_input():
     inputVars = network.inputVars[0][0]
     weights = np.ones(inputVars.shape)/inputVars.size
     averageInputValue = 5.0
-    MarabouUtils.addEquality(network, inputVars, weights, averageInputValue)
+    network.addEquality(inputVars, weights, averageInputValue)
 
     # Lower bound on second output variable
     outputVars = network.outputVars.flatten()
@@ -75,7 +74,7 @@ def test_inequality_output():
 
         # Output inequality constraint
         outputValue = np.random.random() * 90 + 10
-        MarabouUtils.addInequality(network, outputVars, weights, outputValue)
+        network.addInequality(outputVars, weights, outputValue)
 
         # Call to Marabou solver
         vals, _ = network.solve(options = OPT, verbose = False)
@@ -96,7 +95,7 @@ def test_inequality_input():
     inputVars = network.inputVars[0][0]
     weights = np.ones(inputVars.shape)/inputVars.size
     averageInputValue = -5.0
-    MarabouUtils.addInequality(network, inputVars, weights, averageInputValue)
+    network.addInequality(inputVars, weights, averageInputValue)
 
     # Add lower bound on second output variable
     outputVars = network.outputVars.flatten()

src/configuration/GlobalConfiguration.cpp

@@ -95,6 +95,7 @@ const bool GlobalConfiguration::SMT_CORE_LOGGING = false;
 const bool GlobalConfiguration::DANTZIGS_RULE_LOGGING = false;
 const bool GlobalConfiguration::BASIS_FACTORIZATION_LOGGING = false;
 const bool GlobalConfiguration::PREPROCESSOR_LOGGING = false;
+const bool GlobalConfiguration::INPUT_QUERY_LOGGING = false;
 const bool GlobalConfiguration::PROJECTED_STEEPEST_EDGE_LOGGING = false;
 const bool GlobalConfiguration::GAUSSIAN_ELIMINATION_LOGGING = false;
 const bool GlobalConfiguration::QUERY_LOADER_LOGGING = false;

src/configuration/GlobalConfiguration.h

@@ -232,6 +232,7 @@ class GlobalConfiguration
     static const bool DANTZIGS_RULE_LOGGING;
     static const bool BASIS_FACTORIZATION_LOGGING;
     static const bool PREPROCESSOR_LOGGING;
+    static const bool INPUT_QUERY_LOGGING;
     static const bool PROJECTED_STEEPEST_EDGE_LOGGING;
     static const bool GAUSSIAN_ELIMINATION_LOGGING;
     static const bool QUERY_LOADER_LOGGING;

src/configuration/OptionParser.cpp

@@ -57,6 +57,9 @@ void OptionParser::initialize()
         ( "summary-file",
           boost::program_options::value<std::string>( &((*_stringOptions)[Options::SUMMARY_FILE]) ),
           "Summary file" )
+        ( "query-dump-file",
+          boost::program_options::value<std::string>( &((*_stringOptions)[Options::QUERY_DUMP_FILE]) ),
+          "Query dump file" )
         ( "num-workers",
           boost::program_options::value<int>( &((*_intOptions)[Options::NUM_WORKERS]) ),
           "(DNC) Number of workers" )

src/configuration/Options.cpp

@@ -67,6 +67,7 @@ void Options::initializeDefaultValues()
     _stringOptions[PROPERTY_FILE_PATH] = "";
     _stringOptions[INPUT_QUERY_FILE_PATH] = "";
     _stringOptions[SUMMARY_FILE] = "";
+    _stringOptions[QUERY_DUMP_FILE] = "";
 }
 
 void Options::parseOptions( int argc, char **argv )

src/configuration/Options.h

@@ -67,6 +67,7 @@ class Options
         PROPERTY_FILE_PATH,
         INPUT_QUERY_FILE_PATH,
         SUMMARY_FILE,
+        QUERY_DUMP_FILE,
     };
 
     /*

src/engine/DnCMarabou.cpp

@@ -62,31 +62,32 @@ void DnCMarabou::run()
         }
         printf( "Network: %s\n", networkFilePath.ascii() );
 
+        AcasParser acasParser( networkFilePath );
+        acasParser.generateQuery( _inputQuery );
+        _inputQuery.constructNetworkLevelReasoner();
+
         /*
           Step 2: extract the property in question
         */
         String propertyFilePath = Options::get()->getString( Options::PROPERTY_FILE_PATH );
         if ( propertyFilePath != "" )
         {
-            if ( !File::exists( propertyFilePath ) )
-            {
-                printf( "Error: the specified property file (%s) doesn't exist!\n",
-                        propertyFilePath.ascii() );
-                throw MarabouError( MarabouError::FILE_DOESNT_EXIST,
-                                    propertyFilePath.ascii() );
-            }
             printf( "Property: %s\n", propertyFilePath.ascii() );
+            PropertyParser().parse( propertyFilePath, _inputQuery );
         }
         else
             printf( "Property: None\n" );
-
-        AcasParser acasParser( networkFilePath );
-        acasParser.generateQuery( _inputQuery );
-        if ( propertyFilePath != "" )
-            PropertyParser().parse( propertyFilePath, _inputQuery );
     }
     printf( "\n" );
 
+    String queryDumpFilePath = Options::get()->getString( Options::QUERY_DUMP_FILE );
+    if ( queryDumpFilePath.length() > 0 )
+    {
+        _inputQuery.saveQuery( queryDumpFilePath );
+        printf( "\nInput query successfully dumped to file\n" );
+        exit( 0 );
+    }
+
     /*
       Step 3: initialize the DNC core
     */