Rework pyrat printer once again.

config/drivers/pyrat.drv

 (* 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$"

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. *)

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 =

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