Skip to content
Snippets Groups Projects
Commit 99e351a6 authored by Aymeric Varasse's avatar Aymeric Varasse :innocent:
Browse files

[prover] Minor fixes and formatting for runMarabou

parent 7dc9e16b
No related branches found
No related tags found
No related merge requests found
......@@ -4,9 +4,7 @@ Modified by the AISER team, Software Safety and Security Laboratory, CEA-List.
This file is part of CAISAR.
This file is used for integrating Marabou, via its Python interface, in CAISAR.
"""
"""
Top contributors (to current version):
- Andrew Wu
......@@ -17,38 +15,32 @@ 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} has an unrecognized extension."
f"The network must be in .pb, .nnet or .onnx 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 importlib.metadata import version
from maraboupy import Marabou, MarabouCore # type: ignore
from maraboupy import Marabou
from maraboupy import MarabouCore
class WrongNetFormat(Exception):
def __init__(self, networkPath):
self.message = (
f"Network {networkPath} has an unrecognized extension."
f"The network must be in .pb, .nnet or .onnx format."
)
super().__init__(self.message)
sys.path.insert(
0, os.path.join(str(pathlib.Path(__file__).parent.absolute()), "../")
)
sys.path.insert(0, os.path.join(str(pathlib.Path(__file__).parent.absolute()), "../"))
def maraboupy_version(marabou_binary: str):
result = subprocess.run(
[marabou_binary, "--version"], capture_output=True, text=True
)
result = subprocess.run([marabou_binary, "--version"], capture_output=True, text=True)
if result.returncode != 0:
print(f"Error running {marabou_binary} --version")
sys.exit(1)
......@@ -62,9 +54,7 @@ def maraboupy_version(marabou_binary: str):
def arguments():
parser = argparse.ArgumentParser(
description="Thin wrapper around Maraboupy executable"
)
parser = argparse.ArgumentParser(description="Thin wrapper around Maraboupy executable")
parser.add_argument(
"network",
type=str,
......@@ -72,15 +62,9 @@ def arguments():
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"
)
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",
......@@ -103,15 +87,13 @@ def main():
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)
)
sys.exit('"{}" does not exist or is not executable'.format(marabou_binary))
else:
if args.version:
print(f"{maraboupy_version(marabou_binary)}")
else:
assert args.network != None
assert args.prop != None
assert args.network is not None
assert args.prop is not None
networkPath = args.network
suffix = networkPath.split(".")[-1]
......@@ -133,10 +115,7 @@ def main():
print("Running Marabou with the following arguments: ", unknown)
subprocess.run(
[marabou_binary]
+ ["--input-query={}".format(name)]
+ ["--timeout={}".format(timeout)]
+ unknown
[marabou_binary] + ["--input-query={}".format(name)] + ["--timeout={}".format(timeout)] + unknown
)
os.remove(name)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment