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) ("reluplex_rotation":string) (0:int) (0:int) (0:int)
  > end
  > EOF
  [caisar] Goal G: Valid