Skip to content
Snippets Groups Projects
Commit 72d1ad66 authored by François Bobot's avatar François Bobot Committed by Michele Alberti
Browse files

[Tests] Use floating point

parent 95052cb1
No related branches found
No related tags found
No related merge requests found
......@@ -25,13 +25,12 @@ Test verify
> theory T
> use TestNetwork.AsTuple
> use ieee_float.Float64
> use real.RealInfix
> use caisar.NNet
>
> goal G: forall x1 x2 x3 x4 x5.
> 0.0 <. t'real x1 <. 0.1 ->
> (0.0:t) .< x1 .< (0.5:t) ->
> let (y1,_,_,_,_) = nnet_apply x1 x2 x3 x4 x5 in
> 0.0 <. t'real y1 <. 0.1
> (0.0:t) .< y1 .< (0.5:t)
> end
> EOF
<autodetect>0 prover(s) added
......@@ -1169,12 +1168,12 @@ Test verify
function x5 [@introduced] : t19
axiom H [@introduced] : (0.0 < tqtreal x1)
axiom H [@introduced] : lt 0.0 x1
axiom H1 [@introduced] : (tqtreal x1 < 0.1)
axiom H1 [@introduced] : lt x1 0.5
goal G : match nnet_apply x1 x2 x3 x4 x5 with
| Tuple5 y1 _ _ _ _ -> (0.0 < tqtreal y1) /\ (tqtreal y1 < 0.1)
| Tuple5 y1 _ _ _ _ -> lt 0.0 y1 /\ lt y1 0.5
end
end
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment