Rework pyrat printer.

config/drivers/pyrat.drv

@@ -152,10 +152,10 @@ theory ieee_float.Float64
   syntax function (./)  "(%1 / %2)"
   syntax function (.-_) "(-%1)"
 
-  syntax predicate le "(%1 <= %2)"
-  syntax predicate lt  "(%1 <  %2)"
-  syntax predicate ge "(%1 >= %2)"
-  syntax predicate gt  "(%1 >  %2)"
+  syntax predicate le "%1 <= %2"
+  syntax predicate lt  "%1 <  %2"
+  syntax predicate ge "%1 >= %2"
+  syntax predicate gt  "%1 >  %2"
 
 
 end

src/printer/pyrat.ml

@@ -24,37 +24,39 @@ let number_format =
   }
 
 let rec print_term info fmt t =
-  match t.Why3.Term.t_node with
-  | Tconst c -> Why3.Constant.(print number_format unsupported_escape) fmt c
-  | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _ | Teps _ ->
-    Why3.Printer.unsupportedTerm t "Pyrat"
+  let open Why3 in
+  match t.Term.t_node with
+  | Tbinop ((Timplies | Tiff), _, _)
+  | Tnot _ | Ttrue | Tfalse | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _
+  | Teps _ ->
+    Printer.unsupportedTerm t "Pyrat"
+  | Tbinop (Tand, _, _) -> assert false (* Should appear only at top-level. *)
+  | Tconst c -> Constant.(print number_format unsupported_escape) fmt c
   | Tapp (ls, l) -> (
-    match Why3.Printer.query_syntax info.info_syn ls.ls_name with
-    | Some s -> Why3.Printer.syntax_arguments s (print_term info) fmt l
+    match Printer.query_syntax info.info_syn ls.ls_name with
+    | Some s -> Printer.syntax_arguments s (print_term info) fmt l
     | None -> (
-      match (Why3.Term.Hls.find_opt info.variables ls, l) with
+      match (Term.Hls.find_opt info.variables ls, l) with
       | Some s, [] -> Fmt.string fmt s
-      | _ -> Why3.Printer.unsupportedTerm t "Unknown variables"))
-  | Tbinop ((Timplies | Tiff), _, _) | Tnot _ | Ttrue | Tfalse ->
-    Why3.Printer.unsupportedTerm t "Pyrat: Iff, Implies, not"
-  | Tbinop (Tand, _, _) -> Why3.Printer.unsupportedTerm t "Pyrat: Deep and"
+      | _ -> Printer.unsupportedTerm t "Unknown variable(s)"))
   | Tbinop (Tor, t1, t2) ->
     Fmt.pf fmt "%a or %a" (print_term info) t1 (print_term info) t2
 
-let print_top_term info fmt t =
-  let print_term info fmt t =
-    (** don't print things we don't know *)
-    if Why3.Term.t_s_all (fun _ -> true)
-        (fun ls -> Why3.Ident.Mid.mem ls.ls_name info.info_syn ||
-                   Why3.Term.Hls.mem info.variables ls)
-        t then
-      print_term info fmt t
+let print_top_level_term info fmt t =
+  let open Why3 in
+  (* Don't print things we don't know. *)
+  let t_is_known =
+    Term.t_s_all
+      (fun _ -> true)
+      (fun ls ->
+        Ident.Mid.mem ls.ls_name info.info_syn || Term.Hls.mem info.variables ls)
   in
-  match t.Why3.Term.t_node with
+  match t.Term.t_node with
   | Tquant _ -> ()
   | Tbinop (Tand, t1, t2) ->
-    Fmt.pf fmt "%a@.%a" (print_term info) t1 (print_term info) t2
-  | _ ->  Fmt.pf fmt "%a@." (print_term info) t
+    if t_is_known t1 && t_is_known t2
+    then Fmt.pf fmt "%a@.%a" (print_term info) t1 (print_term info) t2
+  | _ -> if t_is_known t then Fmt.pf fmt "%a@." (print_term info) t
 
 let print_decl info fmt d =
   let open Why3 in
@@ -65,8 +67,8 @@ let print_decl info fmt d =
   | Dlogic _ -> ()
   | Dind _ -> ()
   | Dprop (Decl.Plemma, _, _) -> assert false
-  | Dprop (Decl.Paxiom, _, f) -> print_top_term info fmt f
-  | Dprop (Decl.Pgoal, _, f) -> print_top_term info fmt f
+  | Dprop (Decl.Paxiom, _, f) -> print_top_level_term info fmt f
+  | Dprop (Decl.Pgoal, _, f) -> print_top_level_term info fmt f
 
 let rec print_tdecl info fmt task =
   let open Why3 in
@@ -75,7 +77,6 @@ let rec print_tdecl info fmt task =
   | Some { Task.task_prev; task_decl; _ } -> (
     print_tdecl info fmt task_prev;
     match task_decl.Theory.td_node with
-    | Decl d -> print_decl info fmt d
     | Use _ | Clone _ -> ()
     | Meta (meta, l) when Theory.meta_equal meta Transformations.meta_input -> (
       match l with
@@ -88,7 +89,8 @@ let rec print_tdecl info fmt task =
       | [ MAls ls; MAint i ] ->
         Why3.Term.Hls.add info.variables ls (Fmt.str "y%i" i)
       | _ -> assert false)
-    | Meta (_, _) -> ())
+    | Meta (_, _) -> ()
+    | Decl d -> print_decl info fmt d)
 
 let print_task args ?old:_ fmt task =
   let open Why3 in

src/transformations.ml

@@ -9,17 +9,17 @@ open Base
 let meta_input =
   Why3.Theory.(
     register_meta "caisar_input"
-      ~desc:"Indicates the position of the input in the neural network"
+      ~desc:"Indicates the input position in the neural network"
       [ MTlsymbol; MTint ])
 
 let meta_output =
   Why3.Theory.(
     register_meta "caisar_output"
-      ~desc:"Indicates the position of the output in the neural network"
+      ~desc:"Indicates the output position in the neural network"
       [ MTlsymbol; MTint ])
 
-(* Retrieves the (input) variables appearing, as arguments, after an
-   'nnet_apply' symbol. *)
+(* Retrieve the (input) variables appearing, as arguments, after an 'nnet_apply'
+   symbol. *)
 let get_input_variables =
   let rec aux acc (term : Why3.Term.term) =
     match term.t_node with
@@ -42,7 +42,7 @@ let get_input_variables =
     (fun decl acc -> Why3.Decl.decl_fold aux acc decl)
     Why3.Term.Mls.empty
 
-(* Creates logic symbols for output variables and simplifies the formula. *)
+(* Create logic symbols for output variables and simplify the formula. *)
 (* TODO: [Reduction_engine] is probably an overkill and should be replaced. *)
 let simplify_goal env input_variables =
   let rec aux hls (term : Why3.Term.term) =

src/transformations.mli

@@ -8,7 +8,7 @@ val init : unit -> unit
 (** Register the transformations. *)
 
 val meta_input : Why3.Theory.meta
-(** Indicates the position of the input *)
+(** Indicate the input position. *)
 
 val meta_output : Why3.Theory.meta
-(** Indicates the position of the output *)
+(** Indicate the output position. *)

tests/autodetect.t

 Test autodetect
   $ mkdir bin
 
+  $ cat - > bin/alt-ergo << EOF
+  > #!/bin/sh
+  > echo "2.4.0"
+  > EOF
+
   $ cat - > bin/pyrat.py << EOF
   > #!/bin/sh
   > echo "PyRAT 1.0"
@@ -11,7 +16,10 @@ Test autodetect
   > echo "1.0.+"
   > EOF
 
-  $ chmod u+x bin/pyrat.py bin/Marabou
+  $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou
+
+  $ bin/alt-ergo
+  2.4.0
 
   $ bin/pyrat.py
   PyRAT 1.0

tests/simple.t

 Test verify
   $ mkdir bin
 
+  $ cat - > bin/alt-ergo << EOF
+  > #!/bin/sh
+  > echo "2.4.0"
+  > EOF
+
   $ cat - > bin/pyrat.py << EOF
   > #!/bin/sh
   > echo "PyRAT 1.0"
@@ -11,7 +16,10 @@ Test verify
   > echo "1.0.+"
   > EOF
 
-  $ chmod u+x bin/pyrat.py bin/Marabou
+  $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou
+
+  $ bin/alt-ergo
+  2.4.0
 
   $ bin/pyrat.py
   PyRAT 1.0
@@ -47,76 +55,7 @@ Test verify
   <autodetect>Found prover PyRAT version 1.0, OK.
   <autodetect>3 prover(s) added
   (* this is the prelude for PyRAT *)
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  
-  (0.0 <  x0)
-  (x0 <  0.5)
-  (0.0 <  y0)
-  (y0 <  0.5)
+  0.0 <  x0
+  x0 <  0.5
+  0.0 <  y0
+  y0 <  0.5