[SAVer] Driver and config ready

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

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

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

tests/bin/saver

+#!/bin/sh
+
+
+case $1 in
+    --version)
+        echo "1.0"
+        ;;
+    *)
+        echo "NN: $1"
+        echo "Goal:"
+        cat $2
+        echo "Unknown"
+esac

tests/dune

@@ -5,4 +5,5 @@
    TestNetworkONNX.onnx
    bin/pyrat.py
    bin/Marabou
+   bin/saver
 ))

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

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

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
   ()