working on adding vnnlib support

.gitignore

@@ -13,3 +13,5 @@ __pycache__
 *branch_str.txt
 *.mypy_cache
 .coverage
+examples/acasxu/out.txt
+examples/acasxu/results/*

.travis.yml

@@ -0,0 +1,19 @@
+
+# configuration file for continuous integration testing using travis-ci.org
+
+dist: xenial
+
+language: python
+
+dist:
+ - trusty
+
+services:
+  - docker
+
+script:
+# build Docker container
+- docker build -t nnenum .
+
+# run tests
+- docker run nnenum

Dockerfile

@@ -6,7 +6,7 @@
 # To get a shell after building the image:
 # docker run -ir nnenum_image bash
 
-FROM tensorflow/tensorflow:2.2.0
+FROM python:3.6
 
 COPY ./requirements.txt /work/requirements.txt
 
@@ -22,4 +22,7 @@ ENV OPENBLAS_NUM_THREADS=1
 ENV OMP_NUM_THREADS=1
 
 # copy remaining files to docker
-COPY . /work
+COPY . /work
+
+# cmd, run one of each benchmark
+CMD cd /work && ./run_tests.sh

README.md

@@ -4,14 +4,38 @@
 The tool is written by Stanley Bak ([homepage](http://stanleybak.com), [twitter](https://twitter.com/StanleyBak)).
 
 ### Getting Started
-The `Dockerfile` shows how to install all the dependencies (mostly python packages) and set up the environment. Although the tool loads neural networks directly from ONNX files, the properties and initial sets and verification settings must be defined in python scripts.
+The `Dockerfile` shows how to install all the dependencies (mostly python packages) and set up the environment. The tool loads neural networks directly from ONNX files and properties from vnnlib files.
+For example, try running:
 
-The best way to get started is to look at some of the examples. For example, in the `examples/acasxu` directory you can try to verify property 9 of network 3-3 of the [well-studied ACAS Xu neural network verification benchmarks](https://arxiv.org/abs/1702.01135) by running the command: 
+'python3 -m nnenum.nnenum examples/acasxu/data/ACASXU_run2a_3_3_batch_2000.onnx examples/acasxu/data/prop_9.vnnlib'
 
-```python3 acasxu_single.py 3 3 9```
 
 ### VNN 2020 Neural Network Verification Competition (VNN-COMP) Version
-The nnenum tool performed well in VNN-COMP 2020, being the only tool to verify all the ACAS-Xu benchmarks (each in under 10 seconds), as well as one of the best on the MNIST and CIFAR-10 benchmarks. The version used for the competition as well as model files and scripts to run the compeition benchmarks are in the `vnn2020` branch.
+The nnenum tool performed well in VNN-COMP 2020, being the only tool to verify all the ACAS-Xu benchmarks (each in under 10 seconds). The version used for the competition as well as model files and scripts to run the compeition benchmarks are in the `vnn2020` branch.
 
 ### CAV 2020 Paper Version
 The CAV 2020 paper ["Improved Geometric Path Enumeration for Verifying ReLU Neural Networks"](http://stanleybak.com/papers/bak2020cav.pdf) by S. Bak, H.D Tran, K. Hobbs and T. T. Johnson corresponds to optimizations integrated into the exact analysis mode of nnenum, which also benefits overapproximative analysis. The paper version and repeatability evaluation package instructions are available [here](http://stanleybak.com/papers/bak2020cav_repeatability.zip).
+
+### Citing ###
+The following citations can be used for nnenum:
+
+```
+@inproceedings{bak2021nfm,
+  title={nnenum: Verification of ReLU Neural Networks with Optimized Abstraction Refinement},
+  author={Bak, Stanley},
+  booktitle={NASA Formal Methods Symposium},
+  pages={19--36},
+  year={2021},
+  organization={Springer}
+}
+```
+
+```
+@inproceedings{bak2020cav,
+  title={Improved Geometric Path Enumeration for Verifying ReLU Neural Networks},
+  author={Bak, Stanley and Tran, Hoang-Dung and Hobbs, Kerianne and Johnson, Taylor T.},
+  booktitle={Proceedings of the 32nd International Conference on Computer Aided Verification},
+  year={2020},
+  organization={Springer}
+}
+```

examples/acasxu/README.md

@@ -1,5 +1,5 @@
 These are the well-studied ACAXU benchmarks from "Reluplex: An efficient SMT solver for verifying deep neural networks" by Katz, Guy, et al., CAV 2017.
 
-To run a specific bencmark, such as network 3-3 with property 9, execute 'python3 acasxu_single.py 3 3 9'
+To run a specific bencmark, such as network 3-3 with property 9, execute 'python3 -m nnenum.nnenum data/ACASXU_run2a_3_3_batch_2000.onnx data/prop_9.vnnlib'
 
 To run all the benchmarks, run acasxu_all.py (results summary file is placed in results folder).

examples/acasxu/acasxu_all.py

@@ -4,32 +4,25 @@
 Stanley Bak, 2020
 '''
 
-import os
 import sys
 import time
 from pathlib import Path
+import subprocess
 
 from termcolor import cprint
 
-from nnenum.settings import Settings
-from acasxu_single import verify_acasxu
-
 def main():
     'main entry point'
 
     start = time.time()
 
-    Settings.TIMING_STATS = False
-    Settings.PARALLEL_ROOT_LP = False
-    Settings.SPLIT_IF_IDLE = False
-    Settings.PRINT_OVERAPPROX_OUTPUT = False
-
     full_filename = 'results/full_acasxu.dat'
     hard_filename = 'results/hard_acasxu.dat'
+    timeout = 600.0
 
     if len(sys.argv) > 1:
-        Settings.TIMEOUT = 60 * float(sys.argv[1])
-        print(f"Running measurements with timeout = {Settings.TIMEOUT} secs")
+        timeout = 60.0 * float(sys.argv[1])
+        print(f"Running measurements with timeout = {timeout} secs")
 
     instances = []
 
@@ -69,39 +62,7 @@ def main():
 
                 cprint(f"\nRunning net {a_prev}-{tau} with spec {spec}", "grey", "on_green")
 
-                if spec == "7":
-                    # ego / 10 processes is beter for deep counterexamples in prop 7
-                    Settings.BRANCH_MODE = Settings.BRANCH_EGO
-                    Settings.NUM_PROCESSES = 10
-
-                    # property 7 is nondeterministic due to work sharing among processes... use median of 10 runs
-                    pretimeout = Settings.TIMEOUT
-                    Settings.TIMEOUT = min(5, pretimeout) # smaller timeout to make it go faster
-                    runs = 10
-                    print(f"\nTrying median of {runs} quick runs")
-                    results = []
-
-                    for i in range(runs):
-                        print(f"\nTrial {i+1}/{runs}:")
-                        res_str, secs = verify_acasxu(net_pair, spec)
-                        results.append((secs, res_str))
-
-                    results.sort()
-                    print(f"results: {results}")
-                    secs, res_str = results[runs // 2] # median
-
-                    print(f"Median: {secs}, {res_str}")
-
-                    Settings.TIMEOUT = pretimeout
-
-                    if res_str == "timeout":
-                        # median was timeout; run full
-                        res_str, secs = verify_acasxu(net_pair, spec)
-                else:
-                    Settings.BRANCH_MODE = Settings.BRANCH_OVERAPPROX
-                    Settings.NUM_PROCESSES = len(os.sched_getaffinity(0))
-
-                    res_str, secs = verify_acasxu(net_pair, spec)
+                res_str, secs = verify_acasxu(net_pair, spec, timeout)
 
                 s = f"{a_prev}_{tau}\t{spec}\t{res_str}\t{secs}"
                 f.write(s + "\n")
@@ -116,5 +77,29 @@ def main():
 
     print(f"Completed all measurements in {round(mins, 2)} minutes")
 
+def verify_acasxu(net_pair, spec, timeout):
+    'returns res_str, secs'
+
+    prev, tau = net_pair
+
+    onnx_path = f'./data/ACASXU_run2a_{prev}_{tau}_batch_2000.onnx'
+    spec_path = f'./data/prop_{spec}.vnnlib'
+
+    args = [sys.executable, '-m', 'nnenum.nnenum', onnx_path, spec_path, f'{timeout}', 'out.txt']
+
+    start = time.perf_counter()
+
+    result = subprocess.run(args, check=False)
+
+    if result.returncode == 0:
+        with open('out.txt', 'r') as f:
+            res_str = f.readline()
+    else:
+        res_str = 'error_exit_code_{result.returncode}'
+
+    diff = time.perf_counter() - start
+
+    return res_str, diff
+
 if __name__ == '__main__':
     main()