Merge pull request NeuralNetworkVerification#4 from NeuralNetworkVeri…

…fication/master

Merge from master

README.md

@@ -148,6 +148,8 @@ 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)
+
 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, 
@@ -207,7 +209,7 @@ We have three types of tests:
 * regression tests - test end to end functionality thorugh the API, each test is defined by:  
   * network_file - description of the "neural network" supporting nnet and mps formats (using the extension to decdie on the format)  
   * property_file - optional, constraint on the input and output variables  
-  * expected_result - SAT/UNSAT  
+  * expected_result - sat/unsat  
 
 The tests are divided into 5 levels to allow variability in running time, to add a new regression tests: 
   * add the description of the network and property to the _resources_ sub-folder 

maraboupy/Marabou.py

@@ -100,9 +100,9 @@ def solve_query(ipq, filename="", verbose=True, timeout=0, verbosity=2):
         if stats.hasTimedOut():
             print ("TIMEOUT")
         elif len(vals)==0:
-            print("UNSAT")
+            print("unsat")
         else:
-            print("SAT")
+            print("sat")
             for i in range(ipq.getNumInputVariables()):
                 print("input {} = {}".format(i, vals[ipq.inputVariableByIndex(i)]))
             for i in range(ipq.getNumOutputVariables()):

maraboupy/MarabouNetwork.py

@@ -201,9 +201,9 @@ def solve(self, filename="", verbose=True, options=None):
             if stats.hasTimedOut():
                 print("TO")
             elif len(vals)==0:
-                print("UNSAT")
+                print("unsat")
             else:
-                print("SAT")
+                print("sat")
                 for j in range(len(self.inputVars)):
                     for i in range(self.inputVars[j].size):
                         print("input {} = {}".format(i, vals[self.inputVars[j].item(i)]))

maraboupy/MarabouNetworkONNX.py

@@ -342,7 +342,7 @@ def transpose(self, node):
         if inputName in self.varMap:
             self.varMap[nodeName] = np.transpose(self.varMap[node.input[0]], perm)
         elif inputName in self.constantMap:
-            self.constantMap[nodeName] = np.transpose(self.constant[inputName], perm)
+            self.constantMap[nodeName] = np.transpose(self.constantMap[inputName], perm)
 
     def maxpoolEquations(self, node, makeEquations):
         """
@@ -812,4 +812,4 @@ def evaluateWithoutMarabou(self, inputValues):
                 printf("Not sure how to cast input to graph input of type %s" % onnxType)
                 raise NotImplementedError
             input_dict[inputName] = inputValues[i].reshape(self.inputVars[i].shape).astype(inputType)
-        return sess.run([self.outputName],input_dict)[0]
+        return sess.run([self.outputName],input_dict)[0]

maraboupy/examples/Example Notebook.ipynb

@@ -94,7 +94,7 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "SAT\n",
+      "sat\n",
       "input 0 = -0.32842287715105956\n",
       "input 1 = 0.18470882292589386\n",
       "input 2 = -0.015568802288230335\n",
@@ -177,7 +177,7 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "SAT\n",
+      "sat\n",
       "input 0 = -0.32842287715105956\n",
       "input 1 = 0.18470882292589386\n",
       "input 2 = -0.015568802288230335\n",
@@ -245,7 +245,7 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "SAT\n",
+      "sat\n",
       "input 0 = -0.328422874212265\n",
       "input 1 = 0.40932923555374146\n",
       "input 2 = -0.017379289492964745\n",

maraboupy/examples/MarabouCoreExample.py

@@ -88,7 +88,7 @@
 options = createOptions()
 vars1, stats1 = MarabouCore.solve(inputQuery, options, "")
 if len(vars1) > 0:
-    print("SAT")
+    print("sat")
     print(vars1)
 else:
-    print("UNSAT")
+    print("unsat")

regress/regress0/CMakeLists.txt

@@ -1,11 +1,11 @@
-marabou_add_regress_mps_test(0 "lp_feasible_1.mps" "SAT" "" "mps")
-marabou_add_regress_mps_test(0 "lp_infeasible_1.mps" "UNSAT" "" "mps")
+marabou_add_regress_mps_test(0 "lp_feasible_1.mps" "sat" "" "mps")
+marabou_add_regress_mps_test(0 "lp_infeasible_1.mps" "unsat" "" "mps")
 
-marabou_add_acasxu_test(0 "ACASXU_experimental_v2a_1_7.nnet" "3" SAT)
-marabou_add_acasxu_dnc_test(0 "ACASXU_experimental_v2a_1_9.nnet" "4" SAT)
-marabou_add_acasxu_test(0 "ACASXU_experimental_v2a_4_1.nnet" "4" UNSAT)
+marabou_add_acasxu_test(0 "ACASXU_experimental_v2a_1_7.nnet" "3" sat)
+marabou_add_acasxu_dnc_test(0 "ACASXU_experimental_v2a_1_9.nnet" "4" sat)
+marabou_add_acasxu_test(0 "ACASXU_experimental_v2a_4_1.nnet" "4" unsat)
 
-marabou_add_coav_test(0 "reluBenchmark0.067841053009s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(0 "reluBenchmark0.0518190860748s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(0 "reluBenchmark0.536728143692s_SAT.nnet" SAT)
-marabou_add_coav_test(0 "reluBenchmark0.899523973465s_SAT.nnet" SAT)
+marabou_add_coav_test(0 "reluBenchmark0.067841053009s_UNSAT.nnet" unsat)
+marabou_add_coav_test(0 "reluBenchmark0.0518190860748s_UNSAT.nnet" unsat)
+marabou_add_coav_test(0 "reluBenchmark0.536728143692s_SAT.nnet" sat)
+marabou_add_coav_test(0 "reluBenchmark0.899523973465s_SAT.nnet" sat)