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 | ./filter_tmpdir.sh
> theory NIER_to_ONNX
> use ieee_float.Float64
> use bool.Bool
> use int.Int
> use interpretation.Vector
> use interpretation.NeuralNetwork
>
> constant nn: nn = read_neural_network "TestNetworkONNX.onnx" 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
[DEBUG]{NIER} Wrote NIER as ONNX in file 'out/TestNetworkONNX.nier.onnx'
Goal G: Unknown ()
Data should be 0.135
$ python3 bin/inspect_onnx.py
Initializer name 12 has data 0.135