From 1dac6d30cbb369724a40083bc6723e5b1b407f22 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 9 Dec 2021 15:01:18 +0100
Subject: [PATCH] [SAVer] Driver and config ready
---
README.md | 12 +++++++++++-
config/caisar-detection-data.conf | 12 ++++++------
tests/autodetect.t | 4 ++++
tests/bin/saver | 13 +++++++++++++
tests/dune | 1 +
tests/marabou.t | 4 +++-
tests/simple.t | 9 +++++++--
tests/simple_onnx.t | 4 +++-
8 files changed, 48 insertions(+), 11 deletions(-)
create mode 100644 tests/bin/saver
diff --git a/README.md b/README.md
index c88daa77..4205bbd9 100644
--- a/README.md
+++ b/README.md
@@ -2,4 +2,14 @@
## How to add a solver
Make sure the solver is added to your systems for tests.
-1. Create a `new_solver.drv` in `config/drivers`
+1. Create a `new_solver.drv` in `config/drivers/`.
+A driver is a serie of whyml modules describing the theories
+the solver will use during its call by why3.
+
+1. Add a new field inside of `config/caisar-detection-data.conf`.
+Here, you only need to define the name of the solver's
+executable as well as the supported versions for CAISAR.
+
+Now, the solver will be recognized by CAISAR. However, in
+order to exploit it, you should write a printer of its
+output in `src/printers/`. TODO
diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index 1dfea43b..3e256ed4 100644
--- a/config/caisar-detection-data.conf
+++ b/config/caisar-detection-data.conf
@@ -31,11 +31,11 @@ driver = "caisar_drivers/pyrat.drv"
use_at_auto_level = 1
[ATP saver]
-name = "SAVER"
+name = "SAVer"
exec = "saver"
-version_switch = "--version"
-version_regexp = "PyRAT \\([0-9.]+\\)"
-version_ok = "1.1"
-command = "%e --model_path %{nnet-onnx} --property_path %f"
-driver = "caisar_drivers/pyrat.drv"
+version_switch = "2>&1 | grep Usage"
+version_regexp = "\\(\\)"
+version_ok = ""
+command = "%e %{svm} %{data}"
+driver = "caisar_drivers/saver.drv"
use_at_auto_level = 1
diff --git a/tests/autodetect.t b/tests/autodetect.t
index 5bc8e94f..fb0fec24 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -15,9 +15,13 @@ Test autodetect
$ bin/Marabou --version
1.0.+
+ $ bin/saver --version
+ 1.0
+
$ PATH=$(pwd)/bin:$PATH
$ caisar config -d
[caisar] Alt-Ergo 2.4.0
Marabou 1.0.+
PyRAT 1.1
+ SAVER 1.0
diff --git a/tests/bin/saver b/tests/bin/saver
new file mode 100644
index 00000000..0f7abafe
--- /dev/null
+++ b/tests/bin/saver
@@ -0,0 +1,13 @@
+#!/bin/sh
+
+
+case $1 in
+ --version)
+ echo "1.0"
+ ;;
+ *)
+ echo "NN: $1"
+ echo "Goal:"
+ cat $2
+ echo "Unknown"
+esac
diff --git a/tests/dune b/tests/dune
index d62110c4..b1122382 100644
--- a/tests/dune
+++ b/tests/dune
@@ -5,4 +5,5 @@
TestNetworkONNX.onnx
bin/pyrat.py
bin/Marabou
+ bin/saver
))
diff --git a/tests/marabou.t b/tests/marabou.t
index 2d7b6bf3..60fc43d7 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -38,11 +38,13 @@ Test verify
<autodetect>Generating strategies:
<autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
<autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
+ <autodetect>Run: (saver --version) > $TMPFILE 2>&1
<autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Found prover Alt-Ergo version 2.4.0, OK.
<autodetect>Found prover Marabou version 1.0.+, OK.
<autodetect>Found prover PyRAT version 1.1, OK.
- <autodetect>3 prover(s) added
+ <autodetect>Found prover SAVER version 1.0, OK.
+ <autodetect>4 prover(s) added
Goal G: Unknown
()
Goal H: Unknown
diff --git a/tests/simple.t b/tests/simple.t
index a49bc1f2..55490627 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -4,7 +4,7 @@ Test verify
> echo "2.4.0"
> EOF
- $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou
+ $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou bin/saver
$ bin/alt-ergo
2.4.0
@@ -15,6 +15,9 @@ Test verify
$ bin/Marabou --version
1.0.+
+ $ bin/saver --version
+ 1.0
+
$ PATH=$(pwd)/bin:$PATH
$ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9_./]*/$TMPFILE/'
@@ -38,11 +41,13 @@ Test verify
<autodetect>Generating strategies:
<autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
<autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
+ <autodetect>Run: (saver --version) > $TMPFILE 2>&1
<autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Found prover Alt-Ergo version 2.4.0, OK.
<autodetect>Found prover Marabou version 1.0.+, OK.
<autodetect>Found prover PyRAT version 1.1, OK.
- <autodetect>3 prover(s) added
+ <autodetect>Found prover SAVER version 1.0, OK.
+ <autodetect>4 prover(s) added
Goal G: Unknown
()
Goal H: Unknown
diff --git a/tests/simple_onnx.t b/tests/simple_onnx.t
index 75095488..419eb106 100644
--- a/tests/simple_onnx.t
+++ b/tests/simple_onnx.t
@@ -33,10 +33,12 @@ Test verify
<autodetect>Generating strategies:
<autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
<autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
+ <autodetect>Run: (saver --version) > $TMPFILE 2>&1
<autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Found prover Alt-Ergo version 2.4.0, OK.
<autodetect>Found prover Marabou version 1.0.+, OK.
<autodetect>Found prover PyRAT version 1.1, OK.
- <autodetect>3 prover(s) added
+ <autodetect>Found prover SAVER version 1.0, OK.
+ <autodetect>4 prover(s) added
Goal G: Unknown
()
--
GitLab