[aimos] Add test case.

tests/aimos.t

+Test verify
+  $ cat - > test_data.csv << EOF
+  > 4.000000000000000000e+02,4.000000000000000222e-01,-3.139370431367570990e+00,2.333333333333333428e+02,0.000000000000000000e+00
+  > 2.500000000000000000e+02,2.000000000000000111e-01,-3.138814875812015348e+00,2.333333333333333428e+02,0.000000000000000000e+00
+  > 2.500000000000000000e+02,2.222222222222222376e-01,-3.138814875812015348e+00,2.333333333333333428e+02,0.000000000000000000e+00
+  > EOF
+
+  $ chmod u+x bin/aimos
+
+  $ bin/aimos --version
+  AIMOS 1.0
+
+  $ PATH=$(pwd)/bin:$PATH
+
+  $ caisar verify -L . --format whyml --prover=AIMOS --dataset=test_data.csv - 2>&1 <<EOF
+  > theory ACASXU_P5
+  >   use TestNetwork.AsArray
+  >   use ieee_float.Float64
+  >   use caisar.DatasetClassification
+  >   use caisar.DatasetClassificationProps
+  > 
+  >   goal G: meta_robust model dataset (1.0:t)
+  > end
+  > EOF
+  [caisar] Goal G: Valid

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/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/alt-ergo
   2.4.0
@@ -18,6 +18,9 @@ Test autodetect
   $ bin/saver --version
   v1.0
 
+  $ bin/aimos --version
+  AIMOS 1.0
+
   $ bin/cvc5 --version
   This is cvc5 version 1.0.2 [git tag 1.0.2 branch HEAD]
 
@@ -31,6 +34,7 @@ Test autodetect
   [caisar][DEBUG] Automatic detection
   <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/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
@@ -45,8 +49,10 @@ Test autodetect
   <autodetect>Found prover PyRAT version 1.1 (alternative: ACAS)
   <autodetect>Found prover nnenum version dummy, OK.
   <autodetect>Found prover SAVer version v1.0, OK.
-  <autodetect>8 prover(s) added
-  [caisar] Alt-Ergo 2.4.0
+  <autodetect>Found prover AIMOS version 1.0, OK.
+  <autodetect>9 prover(s) added
+  [caisar] AIMOS 1.0
+           Alt-Ergo 2.4.0
            CVC5 1.0.2
            Marabou 1.0.+
            PyRAT 1.1

tests/bin/aimos

+#!/bin/sh
+
+
+case $1 in
+    --version)
+        echo "AIMOS 1.0"
+        ;;
+    *)
+        echo "Goal:"
+        cat $2
+        echo "ACASXU_1_1.nnet, reluplex_rotation, 1.0"
+esac

tests/dune

@@ -7,6 +7,7 @@
   bin/pyrat.py
   bin/Marabou
   bin/saver
+  bin/aimos
   bin/cvc5
   bin/nnenum.sh
   filter_tmpdir.sh)