Newer
Older
Test verify
$ . ./setup_env.sh
$ bin/pyrat.py --version
PyRAT 1.1
$ caisar verify --format whyml --prover=PyRAT --ltag=NIER --onnx-out-dir="out" - 2>&1 <<EOF
> theory NIER_to_ONNX
> use ieee_float.Float64
> use types.Vector
> use model.Model
> use model.NN
> constant nn: model nn = read_model "TestNetworkONNX.onnx"
>
> goal G:
> forall i: vector t.
> has_length i 3 ->
> (0.5:t) .<= i[0] .<= (0.5:t) ->
> (0.5:t) .< (nn @@ i)[0] .< (0.5:t)
> end
> EOF

Michele Alberti
committed
[DEBUG]{NIER} Wrote NIER as ONNX in file 'out/onnx_nn.nier.onnx'
Goal G: Unknown ()
Data should be 0.135
$ python3 bin/inspect_onnx.py
Initializer name 12 has data 0.135