diff --git a/tests/autodetect.t b/tests/autodetect.t index 702408e7b889e4709ef011732db70c86728eba9d..6c4a2f42f3537c048f43893961845f5d02870233 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 0000000000000000000000000000000000000000..036b3d59bd303e4f681d1d39992fd3c4b37ba2b7 --- /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 6b0a76a8dc230b662040f7751343b412ff848edd..036b3d59bd303e4f681d1d39992fd3c4b37ba2b7 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 2aed42f48c9297aa4e64908c24103d863736b8af..09ce2af3f16be707a650459cb34e4a57dc6ccf71 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)