From ba36a34d422e4df290a24feffbadb2ab58318a54 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 31 Aug 2021 15:55:16 +0200
Subject: [PATCH] Add PyRAT data for autodetection.
---
config/caisar-detection-data.conf | 10 ++++++++++
config/drivers/pyrat.drv | 1 +
tests/autodetect.t | 1 +
tests/simple.t | 10 ++++++----
4 files changed, 18 insertions(+), 4 deletions(-)
create mode 100644 config/drivers/pyrat.drv
diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index 95f48470..fb7c5b65 100644
--- a/config/caisar-detection-data.conf
+++ b/config/caisar-detection-data.conf
@@ -20,3 +20,13 @@ version_ok = "1.0.+"
command = "%e --timeout %t %f"
driver = "drivers/marabou"
use_at_auto_level = 1
+
+[ATP pyrat]
+name = "PyRAT"
+exec = "pyrat.py"
+version_switch = "--version"
+version_regexp = "PyRAT \\([0-9.]+\\)"
+version_ok = "1.0"
+command = "%e --timeout %t %f"
+driver = "drivers/pyrat"
+use_at_auto_level = 1
diff --git a/config/drivers/pyrat.drv b/config/drivers/pyrat.drv
new file mode 100644
index 00000000..0a07e0cf
--- /dev/null
+++ b/config/drivers/pyrat.drv
@@ -0,0 +1 @@
+(* Why3 drivers for PyRAT *)
diff --git a/tests/autodetect.t b/tests/autodetect.t
index b99f1264..13344dc8 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -2,3 +2,4 @@ Test autodetect
$ caisar config -d
[caisar] Alt-Ergo 2.4.0
Marabou 1.0.+
+ PyRAT 1.0
diff --git a/tests/simple.t b/tests/simple.t
index d4a317de..5bd0aa97 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -13,15 +13,17 @@ Test verify
> EOF
<autodetect>0 prover(s) added
<autodetect>Generating strategies:
- <autodetect>Run: (Marabou --version) > /tmp/buildb7d8c3.dune/oute22a8d 2>&1
- <autodetect>Run: (alt-ergo --version) > /tmp/buildb7d8c3.dune/outf61830 2>&1
- <autodetect>Run: (alt-ergo-2.4.0 --version) > /tmp/buildb7d8c3.dune/out36e3db 2>&1
+ <autodetect>Run: (Marabou --version) > /tmp/buildd4bdbe.dune/out113e6d 2>&1
+ <autodetect>Run: (alt-ergo --version) > /tmp/buildd4bdbe.dune/outb7c794 2>&1
+ <autodetect>Run: (alt-ergo-2.4.0 --version) > /tmp/buildd4bdbe.dune/out216d3e 2>&1
<autodetect>command 'alt-ergo-2.4.0 --version' failed. Output:
sh: 1: alt-ergo-2.4.0: not found
+ <autodetect>Run: (pyrat.py --version) > /tmp/buildd4bdbe.dune/outf8b6d4 2>&1
<autodetect>Found prover Alt-Ergo version 2.4.0, OK.
<autodetect>Found prover Marabou version 1.0.+, OK.
- <autodetect>2 prover(s) added
+ <autodetect>Found prover PyRAT version 1.0, OK.
+ <autodetect>3 prover(s) added
(* this is the prelude for Alt-Ergo, version >= 2.4.0 *)
(* this is a prelude for Alt-Ergo integer arithmetic *)
(* this is a prelude for Alt-Ergo real arithmetic *)
--
GitLab