From 72d1ad66476237ff359f5a9b4a15593f256bf0f2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 24 Sep 2021 15:02:50 +0200
Subject: [PATCH] [Tests] Use floating point
---
tests/simple.t | 11 +++++------
1 file changed, 5 insertions(+), 6 deletions(-)
diff --git a/tests/simple.t b/tests/simple.t
index bcda3cab..b608821e 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -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
--
GitLab