From 5b0df1749ab16b0a7e76ba70417e4a4ba8c81feb Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 4 Oct 2021 14:12:16 +0200
Subject: [PATCH] Rework pyrat printer.
---
config/drivers/pyrat.drv | 8 ++--
src/printer/pyrat.ml | 54 +++++++++++++------------
src/transformations.ml | 10 ++---
src/transformations.mli | 4 +-
tests/autodetect.t | 10 ++++-
tests/simple.t | 87 ++++++----------------------------------
6 files changed, 61 insertions(+), 112 deletions(-)
diff --git a/config/drivers/pyrat.drv b/config/drivers/pyrat.drv
index c47bfc6e..ddf120e7 100644
--- a/config/drivers/pyrat.drv
+++ b/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
diff --git a/src/printer/pyrat.ml b/src/printer/pyrat.ml
index 7f5db7d6..e0471186 100644
--- a/src/printer/pyrat.ml
+++ b/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
diff --git a/src/transformations.ml b/src/transformations.ml
index 99dda35a..5c7fff1d 100644
--- a/src/transformations.ml
+++ b/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) =
diff --git a/src/transformations.mli b/src/transformations.mli
index dc209777..74aa1404 100644
--- a/src/transformations.mli
+++ b/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. *)
diff --git a/tests/autodetect.t b/tests/autodetect.t
index 02dd58bd..99d6c8b8 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -1,6 +1,11 @@
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
diff --git a/tests/simple.t b/tests/simple.t
index f0aab498..f01724c9 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -1,6 +1,11 @@
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
--
GitLab