From 516716e1464e2582d4675be50efc70f734da8993 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 4 Oct 2021 16:53:14 +0200
Subject: [PATCH] Rework pyrat printer once again.
---
config/drivers/pyrat.drv | 2 +-
src/language.mli | 2 +-
src/printer/pyrat.ml | 11 ++++++++---
tests/simple.t | 15 ++++++++++++++-
4 files changed, 24 insertions(+), 6 deletions(-)
diff --git a/config/drivers/pyrat.drv b/config/drivers/pyrat.drv
index ddf120e7..77dff7e0 100644
--- a/config/drivers/pyrat.drv
+++ b/config/drivers/pyrat.drv
@@ -1,6 +1,6 @@
(* Why3 drivers for PyRAT *)
-prelude "(* this is the prelude for PyRAT *)"
+prelude "(* This is the prelude for PyRAT *)"
(* additional regexp for detection of answers, needed for alt-ergo <= 0.99 *)
valid "^Inconsistent assumption$"
diff --git a/src/language.mli b/src/language.mli
index f1812f1d..71482631 100644
--- a/src/language.mli
+++ b/src/language.mli
@@ -12,7 +12,7 @@ type nnet = {
}
val lookup_loaded_nnets : Why3.Term.lsymbol -> nnet option
-(** @return the filename of an nnets Why3 representation. *)
+(** @return the filename of a nnet Why3 representation. *)
val register_nnet_support : unit -> unit
(** Register nnet parser. *)
diff --git a/src/printer/pyrat.ml b/src/printer/pyrat.ml
index e0471186..a852b9cd 100644
--- a/src/printer/pyrat.ml
+++ b/src/printer/pyrat.ml
@@ -29,7 +29,7 @@ let rec print_term info fmt t =
| Tbinop ((Timplies | Tiff), _, _)
| Tnot _ | Ttrue | Tfalse | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _
| Teps _ ->
- Printer.unsupportedTerm t "Pyrat"
+ Printer.unsupportedTerm t "Not supported by PyRAT"
| Tbinop (Tand, _, _) -> assert false (* Should appear only at top-level. *)
| Tconst c -> Constant.(print number_format unsupported_escape) fmt c
| Tapp (ls, l) -> (
@@ -42,7 +42,7 @@ let rec print_term info fmt t =
| Tbinop (Tor, t1, t2) ->
Fmt.pf fmt "%a or %a" (print_term info) t1 (print_term info) t2
-let print_top_level_term info fmt t =
+let rec print_top_level_term info fmt t =
let open Why3 in
(* Don't print things we don't know. *)
let t_is_known =
@@ -55,7 +55,12 @@ let print_top_level_term info fmt t =
| Tquant _ -> ()
| Tbinop (Tand, t1, t2) ->
if t_is_known t1 && t_is_known t2
- then Fmt.pf fmt "%a@.%a" (print_term info) t1 (print_term info) t2
+ then
+ Fmt.pf fmt "%a%a"
+ (print_top_level_term info)
+ t1
+ (print_top_level_term info)
+ t2
| _ -> if t_is_known t then Fmt.pf fmt "%a@." (print_term info) t
let print_decl info fmt d =
diff --git a/tests/simple.t b/tests/simple.t
index f01724c9..18ca8bf1 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -39,6 +39,11 @@ Test verify
> (0.0:t) .< x1 .< (0.5:t) ->
> let (y1,_,_,_,_) = nnet_apply x1 x2 x3 x4 x5 in
> (0.0:t) .< y1 .< (0.5:t)
+ >
+ > goal H: forall x1 x2 x3 x4 x5.
+ > (0.0:t) .< x1 .< (0.5:t) /\ (0.5:t) .< x2 .< (1.0:t) ->
+ > let (y1,y2,_,_,_) = nnet_apply x1 x2 x3 x4 x5 in
+ > ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
> end
> EOF
<autodetect>0 prover(s) added
@@ -54,8 +59,16 @@ Test verify
<autodetect>Found prover Marabou version 1.0.+, OK.
<autodetect>Found prover PyRAT version 1.0, OK.
<autodetect>3 prover(s) added
- (* this is the prelude for PyRAT *)
+ (* This is the prelude for PyRAT *)
0.0 < x0
x0 < 0.5
0.0 < y0
y0 < 0.5
+ (* This is the prelude for PyRAT *)
+ 0.0 < x0
+ x0 < 0.5
+ 0.5 < x1
+ x1 < 1.0
+ 0.0 < y0 or 0.5 < y0
+ 0.0 < y1
+ y1 < 0.5
--
GitLab