diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index c12a5e724500815e81dd241439f85fc92e85c7bd..967d8303d5f3af68fb9b52461a2d75654cf81613 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -45,7 +45,7 @@ test:
stage: test
script:
- nix --extra-experimental-features "nix-command flakes" build
- - nix --extra-experimental-features "nix-command flakes" flake check
+ - nix --extra-experimental-features "nix-command flakes" flake check -L
## Manual generation of the documentation
diff --git a/bin/dune b/bin/dune
index 1200cd3a31d2380d536e2639b123dfbe71fb1910..18e0574a8c28cc0c4eb8d697d271739782a0dd7e 100644
--- a/bin/dune
+++ b/bin/dune
@@ -4,4 +4,5 @@
(files
(dummyversion.py as dummyversion.py)
(nnenum.sh as nnenum.sh)
+ (marabou_eval.py as marabou_eval.py)
(abcrown.sh as abcrown.sh)))
diff --git a/bin/marabou_eval.py b/bin/marabou_eval.py
new file mode 100755
index 0000000000000000000000000000000000000000..2683464293326a398d4c8c97a34fc0c0426812f4
--- /dev/null
+++ b/bin/marabou_eval.py
@@ -0,0 +1,113 @@
+#!/usr/bin/env python3
+"""
+Adapted for quick evaluation of Marabou for CAISAR
+
+Top contributors (to current version):
+ - Andrew Wu
+
+This file is part of the Marabou project.
+Copyright (c) 2017-2021 by the authors listed in the file AUTHORS
+in the top-level source directory) and their institutional affiliations.
+All rights reserved. See the file COPYING in the top-level source
+directory for licensing information.
+"""
+
+
+class WrongNetFormat(Exception):
+ def __init__(self, networkPath):
+ self.message = f"Network {networkPath} not in onnx, pb or nnet format!"
+ super().__init__(self.message)
+
+
+import argparse
+from importlib.metadata import version
+import os
+import pathlib
+import shutil
+import subprocess
+import sys
+import tempfile
+
+from maraboupy import Marabou
+from maraboupy import MarabouCore
+
+
+sys.path.insert(0, os.path.join(str(pathlib.Path(__file__).parent.absolute()), "../"))
+
+
+def arguments():
+ parser = argparse.ArgumentParser(
+ description="Thin wrapper around Maraboupy executable"
+ )
+ parser.add_argument(
+ "network",
+ type=str,
+ nargs="?",
+ default=None,
+ help="The network file name, the extension can be only .pb, .nnet, and .onnx",
+ )
+ parser.add_argument(
+ "prop", type=str, nargs="?", default=None, help="The property file name"
+ )
+ parser.add_argument(
+ "-t", "--timeout", type=int, default=10, help="Timeout in seconds"
+ )
+ parser.add_argument(
+ "--temp-dir", type=str, default="/tmp/", help="Temporary directory"
+ )
+ marabou_path = shutil.which("Marabou")
+ parser.add_argument(
+ "--marabou-binary",
+ type=str,
+ default=marabou_path,
+ help="The path to Marabou binary",
+ )
+ parser.add_argument(
+ "--version",
+ action="store_true",
+ help="Output a version string if Maraboupy is present and exit",
+ )
+ parser.set_defaults(version=False)
+
+ return parser
+
+
+def main():
+ args, unknown = arguments().parse_known_args()
+ marabou_binary = args.marabou_binary
+ if not os.access(marabou_binary, os.X_OK):
+ sys.exit('"{}" does not exist or is not executable'.format(marabou_binary))
+ else:
+ if args.version:
+ print(f"Maraboupy version {version('maraboupy')}")
+ else:
+
+ assert args.prop != None
+ networkPath = args.network
+ suffix = networkPath.split(".")[-1]
+ if suffix == "nnet":
+ network = Marabou.read_nnet(networkPath)
+ elif suffix == "pb":
+ network = Marabou.read_tf(networkPath)
+ elif suffix == "onnx":
+ network = Marabou.read_onnx(networkPath)
+ else:
+ raise WrongNetFormat(networkPath)
+ query = network.getInputQuery()
+ MarabouCore.loadProperty(query, args.prop)
+ temp = tempfile.NamedTemporaryFile(dir=args.temp_dir, delete=False)
+ name = temp.name
+ timeout = args.timeout
+ MarabouCore.saveQuery(query, name)
+ print("Running Marabou with the following arguments: ", unknown)
+ subprocess.run(
+ [marabou_binary]
+ + ["--input-query={}".format(name)]
+ + ["--timeout={}".format(timeout)]
+ + unknown
+ )
+ os.remove(name)
+
+
+if __name__ == "__main__":
+ main()
diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index 0355e67901ae35380c4757534e775b0ace248bbe..7eb58a8e784beb4d2620006caa45e6fcc6fb12e2 100644
--- a/config/caisar-detection-data.conf
+++ b/config/caisar-detection-data.conf
@@ -53,6 +53,16 @@ command = "%e %{nnet-onnx} %f --timeout %t --snc --initial-divides=4 --num-onlin
driver = "%{config}/drivers/marabou.drv"
use_at_auto_level = 1
+[ATP maraboupy]
+name = "Maraboupy"
+exec = "marabou_eval.py"
+version_switch = "--version"
+version_regexp = "Maraboupy version \\([0-9.]+\\)"
+version_ok = "2.0.0"
+command = "%e %{nnet-onnx} %f "
+driver = "%{config}/drivers/marabou.drv"
+use_at_auto_level = 1
+
[ATP pyrat]
name = "PyRAT"
exec = "pyrat.py"
diff --git a/tests/autodetect.t b/tests/autodetect.t
index ba5051ce2d5e6b681575f0879917d4cf1aaaeb0b..aa34864e8f786e1b755212f587977d2422c589ea 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -30,11 +30,15 @@ Test autodetect
$ bin/abcrown.sh --version
dummy-version
+ $ bin/marabou_eval.py --version
+ Maraboupy version 2.0.0
+
$ caisar config -d
AIMOS 1.0
Alt-Ergo 2.4.0
CVC5 1.0.2
Marabou 1.0.+
+ Maraboupy 2.0.0
PyRAT 1.1
PyRAT 1.1 (ACAS)
PyRAT 1.1 (ACASd)
diff --git a/tests/bin/marabou_eval.py b/tests/bin/marabou_eval.py
new file mode 100755
index 0000000000000000000000000000000000000000..4ba5fbd8125758a81063b086bcdde7bf2f5c3bac
--- /dev/null
+++ b/tests/bin/marabou_eval.py
@@ -0,0 +1,14 @@
+#!/bin/sh -e
+
+case $1 in
+ --version)
+ echo "Maraboupy version 2.0.0"
+ ;;
+ *)
+ echo "PWD: $(pwd)"
+ echo "NN: $2"
+ test -e $2 || (echo "Cannot find the NN file" && exit 1)
+ echo "Goal:"
+ cat $4
+ echo "Result = Unknown"
+esac