From 50aeffb5a62fc3cd348acaad76a51471dd7f735d Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 23 May 2023 21:38:38 +0200
Subject: [PATCH] [tests] Add abcrown to autodetection test, plus some fixes.
---
tests/autodetect.t | 18 ++++++++++++------
tests/bin/abcrown.sh | 15 +++++++++++++++
tests/bin/nnenum.sh | 2 +-
tests/dune | 1 +
4 files changed, 29 insertions(+), 7 deletions(-)
create mode 100644 tests/bin/abcrown.sh
diff --git a/tests/autodetect.t b/tests/autodetect.t
index 702408e..6c4a2f4 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -4,7 +4,7 @@ Test autodetect
> echo "2.4.0"
> EOF
- $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou bin/saver bin/aimos bin/cvc5 bin/nnenum.sh
+ $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou bin/saver bin/aimos bin/cvc5 bin/nnenum.sh bin/abcrown.sh
$ bin/alt-ergo
2.4.0
@@ -25,19 +25,23 @@ Test autodetect
This is cvc5 version 1.0.2 [git tag 1.0.2 branch HEAD]
$ bin/nnenum.sh --version
- dummy
+ dummy-version
+
+ $ bin/abcrown.sh --version
+ dummy-version
$ PATH=$(pwd)/bin:$PATH
$ caisar config -d -vv 2>&1 | ./filter_tmpdir.sh
[caisar][DEBUG] Execution of command 'config'
[caisar][DEBUG] Automatic detection
+ <autodetect>Run: ($TESTCASE_ROOT/bin/nnenum.sh --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/aimos --version) > $TMPFILE 2>&1
+ <autodetect>Run: ($TESTCASE_ROOT/bin/abcrown.sh --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
- <autodetect>Run: ($TESTCASE_ROOT/bin/nnenum.sh --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/cvc5 --version) > $TMPFILE 2>&1
<autodetect>0 prover(s) added
<autodetect>Generating strategies:
@@ -47,10 +51,11 @@ Test autodetect
<autodetect>Found prover PyRAT version 1.1, OK.
<autodetect>Found prover PyRAT version 1.1 (alternative: VNNLIB)
<autodetect>Found prover PyRAT version 1.1 (alternative: ACAS)
- <autodetect>Found prover nnenum version dummy, OK.
+ <autodetect>Found prover nnenum version dummy-version, OK.
+ <autodetect>Found prover alpha-beta-CROWN version dummy-version, OK.
<autodetect>Found prover SAVer version v1.0, OK.
<autodetect>Found prover AIMOS version 1.0, OK.
- <autodetect>9 prover(s) added
+ <autodetect>10 prover(s) added
[caisar] AIMOS 1.0
Alt-Ergo 2.4.0
CVC5 1.0.2
@@ -59,4 +64,5 @@ Test autodetect
PyRAT 1.1 (ACAS)
PyRAT 1.1 (VNNLIB)
SAVer v1.0
- nnenum dummy
+ alpha-beta-CROWN dummy-version
+ nnenum dummy-version
diff --git a/tests/bin/abcrown.sh b/tests/bin/abcrown.sh
new file mode 100644
index 0000000..036b3d5
--- /dev/null
+++ b/tests/bin/abcrown.sh
@@ -0,0 +1,15 @@
+#!/bin/sh -e
+
+
+case $1 in
+ --version)
+ echo "dummy-version"
+ ;;
+ *)
+ echo "PWD: $(pwd)"
+ echo "NN: $1"
+ test -e $1 || (echo "Cannot find the NN file" && exit 1)
+ echo "Goal:"
+ cat $2
+ echo "Unknown"
+esac
diff --git a/tests/bin/nnenum.sh b/tests/bin/nnenum.sh
index 6b0a76a..036b3d5 100644
--- a/tests/bin/nnenum.sh
+++ b/tests/bin/nnenum.sh
@@ -3,7 +3,7 @@
case $1 in
--version)
- echo "dummy"
+ echo "dummy-version"
;;
*)
echo "PWD: $(pwd)"
diff --git a/tests/dune b/tests/dune
index 2aed42f..09ce2af 100644
--- a/tests/dune
+++ b/tests/dune
@@ -10,6 +10,7 @@
bin/aimos
bin/cvc5
bin/nnenum.sh
+ bin/abcrown.sh
filter_tmpdir.sh
../lib/xgboost/example/california.csv
../lib/xgboost/example/california.json)
--
GitLab