diff --git a/src/autodetection.ml b/src/autodetect.ml
similarity index 83%
rename from src/autodetection.ml
rename to src/autodetect.ml
index 329c50f742d47dacfec18c64f7ed83d10cce36fb..4596b104f6b44f2a37fdde6bf7fa2b5525c10547 100644
--- a/src/autodetection.ml
+++ b/src/autodetect.ml
@@ -4,20 +4,19 @@
(* *)
(**************************************************************************)
+open Why3
open Base
-module Sys = Caml.Sys
-let null = if Sys.unix then "/dev/null" else "NUL"
+let null = if Caml.Sys.unix then "/dev/null" else "NUL"
let rec lookup_file dirs filename =
match dirs with
| [] -> raise Caml.Not_found
| dir :: dirs ->
let file = Caml.Filename.concat dir filename in
- if Sys.file_exists file then file else lookup_file dirs filename
+ if Caml.Sys.file_exists file then file else lookup_file dirs filename
-let autodetect ?(debug = false) () =
- let open Why3 in
+let autodetection ?(debug = false) () =
if debug then Debug.set_flag Autodetection.debug;
let caisar_conf =
lookup_file Dirs.Sites.config "caisar-detection-data.conf"
diff --git a/src/autodetection.mli b/src/autodetect.mli
similarity index 88%
rename from src/autodetection.mli
rename to src/autodetect.mli
index 65e97b263dd572afde902ce6a4155c8a877c50a2..e755ada0156a80de1b3e2b1d4cd48bccf3e60f7e 100644
--- a/src/autodetection.mli
+++ b/src/autodetect.mli
@@ -4,7 +4,7 @@
(* *)
(**************************************************************************)
-val autodetect : ?debug:bool -> unit -> Why3.Whyconf.config
+val autodetection : ?debug:bool -> unit -> Why3.Whyconf.config
(** Perform the autodetection of provers.
@param debug activates debug information. *)
diff --git a/src/language.ml b/src/language.ml
index b7171e7a04e20cbf6fa94b353330ae0bbfad9138..bd67d917830d164cf679c11c66130f86a30808f7 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -4,6 +4,7 @@
(* *)
(**************************************************************************)
+open Why3
open Base
(* -- Support for the NNet and ONNX neural network formats. *)
@@ -11,15 +12,14 @@ open Base
type ioshape = {
nb_inputs : int;
nb_outputs : int;
- ty_data : Why3.Ty.ty;
+ ty_data : Ty.ty;
filename : string;
}
-let loaded_nets = Why3.Term.Hls.create 10
-let lookup_loaded_nets = Why3.Term.Hls.find_opt loaded_nets
+let loaded_nets = Term.Hls.create 10
+let lookup_loaded_nets = Term.Hls.find_opt loaded_nets
let register_astuple nb_inputs nb_outputs filename env =
- let open Why3 in
let net = Pmodule.read_module env [ "caisar" ] "IOShape" in
let ioshape_input_type =
Ty.ty_app Theory.(ns_find_ts net.mod_theory.th_export [ "input_type" ]) []
@@ -34,7 +34,7 @@ let register_astuple nb_inputs nb_outputs filename env =
(List.init nb_inputs ~f)
(Ty.ty_tuple (List.init nb_outputs ~f))
in
- Why3.Term.Hls.add loaded_nets ls_net_apply
+ Term.Hls.add loaded_nets ls_net_apply
{ filename; nb_inputs; nb_outputs; ty_data = ioshape_input_type };
let th_uc =
Pmodule.add_pdecl ~vc:false th_uc
@@ -43,25 +43,21 @@ let register_astuple nb_inputs nb_outputs filename env =
Wstdlib.Mstr.singleton "AsTuple" (Pmodule.close_module th_uc)
let nnet_parser env _ filename _ =
- let open Why3 in
let model = Nnet.parse filename in
match model with
| Error s -> Loc.errorm "%s" s
| Ok model -> register_astuple model.n_inputs model.n_outputs filename env
let onnx_parser env _ filename _ =
- let open Why3 in
let model = Onnx.parse filename in
match model with
| Error s -> Loc.errorm "%s" s
| Ok model -> register_astuple model.n_inputs model.n_outputs filename env
let register_nnet_support () =
- Why3.(
- Env.register_format ~desc:"NNet format (ReLU only)" Pmodule.mlw_language
- "NNet" [ "nnet" ] nnet_parser)
+ Env.register_format ~desc:"NNet format (ReLU only)" Pmodule.mlw_language
+ "NNet" [ "nnet" ] nnet_parser
let register_onnx_support () =
- Why3.(
- Env.register_format ~desc:"ONNX format" Pmodule.mlw_language "ONNX"
- [ "onnx" ] onnx_parser)
+ Env.register_format ~desc:"ONNX format" Pmodule.mlw_language "ONNX" [ "onnx" ]
+ onnx_parser
diff --git a/src/language.mli b/src/language.mli
index f1d1fcabeff3011ebe2235a8ebac2dd91fbf3dd4..070aef66e11545814eb2a4924b8e2c648d60054e 100644
--- a/src/language.mli
+++ b/src/language.mli
@@ -4,14 +4,16 @@
(* *)
(**************************************************************************)
+open Why3
+
type ioshape = {
nb_inputs : int;
nb_outputs : int;
- ty_data : Why3.Ty.ty;
+ ty_data : Ty.ty;
filename : string;
}
-val lookup_loaded_nets : Why3.Term.lsymbol -> ioshape option
+val lookup_loaded_nets : Term.lsymbol -> ioshape option
(** @return the filename of a nnet Why3 representation. *)
val register_nnet_support : unit -> unit
diff --git a/src/main.ml b/src/main.ml
index bc097c4ed001ee8cfdf86707ce1dbe6101996d74..32b7d9eec2b163b85976697d4fdfa9ee0b5dde3b 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -55,7 +55,7 @@ let config detect () =
Logs.debug (fun m -> m "Automatic detection.");
let config =
let debug = match Logs.level () with Some Debug -> true | _ -> false in
- Autodetection.autodetect ~debug ()
+ Autodetect.autodetection ~debug ()
in
let open Why3 in
let provers = Whyconf.get_provers config in
diff --git a/src/printers/marabou.ml b/src/printers/marabou.ml
index 72568d3befd211957ccbf1effbc7de9cbe0a999d..b91da57979c6b1b7fa47d4a5ffd3535ab72086f2 100644
--- a/src/printers/marabou.ml
+++ b/src/printers/marabou.ml
@@ -4,32 +4,32 @@
(* *)
(**************************************************************************)
+open Why3
+
type info = {
- le : Why3.Term.lsymbol;
- ge : Why3.Term.lsymbol;
- lt : Why3.Term.lsymbol;
- gt : Why3.Term.lsymbol;
- info_syn : Why3.Printer.syntax_map;
- variables : string Why3.Term.Hls.t;
+ le : Term.lsymbol;
+ ge : Term.lsymbol;
+ lt : Term.lsymbol;
+ gt : Term.lsymbol;
+ info_syn : Printer.syntax_map;
+ variables : string Term.Hls.t;
}
let number_format =
{
- Why3.Number.long_int_support = `Default;
- Why3.Number.negative_int_support = `Default;
- Why3.Number.dec_int_support = `Default;
- Why3.Number.hex_int_support = `Unsupported;
- Why3.Number.oct_int_support = `Unsupported;
- Why3.Number.bin_int_support = `Unsupported;
- Why3.Number.negative_real_support =
- `Custom (fun fmt f -> Fmt.pf fmt "-%t" f);
- Why3.Number.dec_real_support = `Default;
- Why3.Number.hex_real_support = `Unsupported;
- Why3.Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
+ Number.long_int_support = `Default;
+ Number.negative_int_support = `Default;
+ Number.dec_int_support = `Default;
+ Number.hex_int_support = `Unsupported;
+ Number.oct_int_support = `Unsupported;
+ Number.bin_int_support = `Unsupported;
+ Number.negative_real_support = `Custom (fun fmt f -> Fmt.pf fmt "-%t" f);
+ Number.dec_real_support = `Default;
+ Number.hex_real_support = `Unsupported;
+ Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
}
let rec print_term info fmt t =
- let open Why3 in
match t.Term.t_node with
| Tbinop ((Timplies | Tiff | Tor), _, _)
| Tnot _ | Ttrue | Tfalse | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _
@@ -46,7 +46,6 @@ let rec print_term info fmt t =
| _ -> Printer.unsupportedTerm t "Unknown variable(s)"))
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 =
Term.t_s_all
@@ -67,7 +66,6 @@ let rec print_top_level_term info fmt t =
| _ -> if t_is_known t then Fmt.pf fmt "%a@." (print_term info) t
let rec negate_term info t =
- let open Why3 in
match t.Term.t_node with
| Tquant _ -> Printer.unsupportedTerm t "Quantification"
| Tbinop (Tand, _, _) -> Printer.unsupportedTerm t "Conjunction"
@@ -87,7 +85,6 @@ let rec negate_term info t =
| _ -> Printer.unsupportedTerm t "Cannot negate such term"
let print_decl info fmt d =
- let open Why3 in
match d.Decl.d_node with
| Dtype _ -> ()
| Ddata _ -> ()
@@ -100,7 +97,6 @@ let print_decl info fmt d =
print_top_level_term info fmt (negate_term info f)
let rec print_tdecl info fmt task =
- let open Why3 in
match task with
| None -> ()
| Some { Task.task_prev; task_decl; _ } -> (
@@ -121,7 +117,6 @@ let rec print_tdecl info fmt task =
| Decl d -> print_decl info fmt d)
let print_task args ?old:_ fmt task =
- let open Why3 in
let th = Env.read_theory args.Printer.env [ "ieee_float" ] "Float64" in
let le = Theory.ns_find_ls th.th_export [ "le" ] in
let lt = Theory.ns_find_ls th.th_export [ "lt" ] in
@@ -141,5 +136,5 @@ let print_task args ?old:_ fmt task =
print_tdecl info fmt task
let init () =
- Why3.Printer.register_printer ~desc:"Printer for the Marabou prover."
- "marabou" print_task
+ Printer.register_printer ~desc:"Printer for the Marabou prover." "marabou"
+ print_task
diff --git a/src/printers/pyrat.ml b/src/printers/pyrat.ml
index 1014df2aea90361cc006844fae4735dfe6e4df72..67a7f7668e2847cec41737ba6a49389b266801ff 100644
--- a/src/printers/pyrat.ml
+++ b/src/printers/pyrat.ml
@@ -4,28 +4,25 @@
(* *)
(**************************************************************************)
-type info = {
- info_syn : Why3.Printer.syntax_map;
- variables : string Why3.Term.Hls.t;
-}
+open Why3
+
+type info = { info_syn : Printer.syntax_map; variables : string Term.Hls.t }
let number_format =
{
- Why3.Number.long_int_support = `Default;
- Why3.Number.negative_int_support = `Default;
- Why3.Number.dec_int_support = `Default;
- Why3.Number.hex_int_support = `Unsupported;
- Why3.Number.oct_int_support = `Unsupported;
- Why3.Number.bin_int_support = `Unsupported;
- Why3.Number.negative_real_support =
- `Custom (fun fmt f -> Fmt.pf fmt "-%t" f);
- Why3.Number.dec_real_support = `Default;
- Why3.Number.hex_real_support = `Unsupported;
- Why3.Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
+ Number.long_int_support = `Default;
+ Number.negative_int_support = `Default;
+ Number.dec_int_support = `Default;
+ Number.hex_int_support = `Unsupported;
+ Number.oct_int_support = `Unsupported;
+ Number.bin_int_support = `Unsupported;
+ Number.negative_real_support = `Custom (fun fmt f -> Fmt.pf fmt "-%t" f);
+ Number.dec_real_support = `Default;
+ Number.hex_real_support = `Unsupported;
+ Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
}
let rec print_base_term info fmt t =
- let open Why3 in
match t.Term.t_node with
| Tbinop ((Tand | Tor), _, _) -> assert false
| Tbinop ((Timplies | Tiff), _, _)
@@ -42,7 +39,6 @@ let rec print_base_term info fmt t =
| _ -> Printer.unsupportedTerm t "Unknown variable(s)"))
let rec print_term ~sep info fmt t =
- let open Why3 in
(* Don't print things we don't know. *)
let t_is_known =
Term.t_s_all
@@ -66,7 +62,6 @@ let rec print_term ~sep info fmt t =
| _ -> if t_is_known t then Fmt.pf fmt "%a%(%)" (print_base_term info) t sep
let print_decl info fmt d =
- let open Why3 in
match d.Decl.d_node with
| Dtype _ -> ()
| Ddata _ -> ()
@@ -81,7 +76,6 @@ let print_decl info fmt d =
| Dprop (Decl.Pgoal, _, f) -> print_term ~sep:"" info fmt f
let rec print_tdecl info fmt task =
- let open Why3 in
match task with
| None -> ()
| Some { Task.task_prev; task_decl; _ } -> (
@@ -102,7 +96,6 @@ let rec print_tdecl info fmt task =
| Decl d -> print_decl info fmt d)
let print_task args ?old:_ fmt task =
- let open Why3 in
let info =
{
info_syn = Discriminate.get_syntax_map task;
@@ -113,5 +106,5 @@ let print_task args ?old:_ fmt task =
print_tdecl info fmt task
let init () =
- Why3.Printer.register_printer ~desc:"Printer for the PyRAT prover." "pyrat"
+ Printer.register_printer ~desc:"Printer for the PyRAT prover." "pyrat"
print_task
diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml
index 7844e8d9287a1db73ee7deb538bee064ab6d80d8..d6753945a840d2842a6000b3d8a38ff1e121fc0d 100644
--- a/src/transformations/native_nn_prover.ml
+++ b/src/transformations/native_nn_prover.ml
@@ -4,29 +4,29 @@
(* *)
(**************************************************************************)
+open Why3
open Base
let meta_input =
- Why3.Theory.(
+ Theory.(
register_meta "caisar_input"
~desc:"Indicates the input position in the neural network"
[ MTlsymbol; MTint ])
let meta_output =
- Why3.Theory.(
+ Theory.(
register_meta "caisar_output"
~desc:"Indicates the output position in the neural network"
[ MTlsymbol; MTint ])
let meta_nn_filename =
- Why3.Theory.(
+ Theory.(
register_meta_excl "caisar_nnet_or_onnx"
~desc:"Indicates the filename of the network" [ MTstring ])
(* Retrieve the (input) variables appearing, as arguments, after an 'nnet_apply'
symbol. *)
let get_input_variables =
- let open Why3 in
let rec aux acc (term : Term.term) =
match term.t_node with
| Term.Tapp (ls, args) -> (
@@ -48,7 +48,6 @@ let get_input_variables =
(* 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 open Why3 in
let rec aux meta hls (term : Term.term) =
match term.t_node with
| Term.Tapp (ls, _) -> (
@@ -115,9 +114,9 @@ let simplify_goal env input_variables =
None
let native_nn_prover env =
- Why3.(Trans.seq [ Trans.bind get_input_variables (simplify_goal env) ])
+ Trans.seq [ Trans.bind get_input_variables (simplify_goal env) ]
let init () =
- Why3.Trans.register_env_transform
+ Trans.register_env_transform
~desc:"Transformation for provers that support loading neural networks."
"native_nn_prover" native_nn_prover
diff --git a/src/transformations/native_nn_prover.mli b/src/transformations/native_nn_prover.mli
index d8ad4b1276984dd8dce632659dc3b54e55ebe0c0..67dfd65b441ec6065b99f39dcf2b4fd2a24906eb 100644
--- a/src/transformations/native_nn_prover.mli
+++ b/src/transformations/native_nn_prover.mli
@@ -4,14 +4,16 @@
(* *)
(**************************************************************************)
+open Why3
+
val init : unit -> unit
(** Register the transformation. *)
-val meta_input : Why3.Theory.meta
+val meta_input : Theory.meta
(** Indicate the input position. *)
-val meta_output : Why3.Theory.meta
+val meta_output : Theory.meta
(** Indicate the output position. *)
-val meta_nn_filename : Why3.Theory.meta
+val meta_nn_filename : Theory.meta
(** The filename of the nnet or onnx model. *)
diff --git a/src/transformations/vars_on_lhs.ml b/src/transformations/vars_on_lhs.ml
index a1ac31d6c4768e01100a58578e8cb1b5a0f9b601..75cd8eaee5b888745e6ea4f64ce6c0c2b858010b 100644
--- a/src/transformations/vars_on_lhs.ml
+++ b/src/transformations/vars_on_lhs.ml
@@ -4,10 +4,10 @@
(* *)
(**************************************************************************)
+open Why3
open Base
let make_rt env =
- let open Why3 in
let th = Env.read_theory env [ "ieee_float" ] "Float64" in
let t = Theory.ns_find_ts th.th_export [ "t" ] in
let le = Theory.ns_find_ls th.th_export [ "le" ] in
@@ -43,10 +43,10 @@ let make_rt env =
let vars_on_lhs env =
let rt, task = make_rt env in
- Why3.Trans.rewrite rt task
+ Trans.rewrite rt task
let init () =
- Why3.Trans.register_env_transform
+ Trans.register_env_transform
~desc:
"Transformation for provers that need variables on the left-hand-side of \
logic symbols."
diff --git a/src/verification.ml b/src/verification.ml
index 8a6539c13aa7eb2e28958a18821ee5eb7df11705..013344aea432389ab1b6283eef7d6e9ce0e1d270 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -4,6 +4,7 @@
(* *)
(**************************************************************************)
+open Why3
open Base
module Filename = Caml.Filename
@@ -12,8 +13,7 @@ let () =
Language.register_onnx_support ()
let create_env loadpath =
- let config = Autodetection.autodetect ~debug:true () in
- let open Why3 in
+ let config = Autodetect.autodetection ~debug:true () in
let config =
let main = Whyconf.get_main config in
let dft_memlimit = 4000 (* 4 GB *) in
@@ -28,18 +28,15 @@ let create_env loadpath =
(loadpath @ stdlib @ Whyconf.loadpath (Whyconf.get_main config)),
config )
-let nnet_or_onnx = Re.compile (Re.str "%{nnet-onnx}")
+let nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))
let combine_prover_answers answers =
- let open Why3 in
List.fold_left answers ~init:Call_provers.Valid ~f:(fun acc r ->
match (acc, r) with
| Call_provers.Valid, r | r, Call_provers.Valid -> r
| _ -> acc)
-let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver task
- =
- let open Why3 in
+let call_prover ~limit config (prover : Whyconf.config_prover) driver task =
let task_prepared = Driver.prepare_task driver task in
let tasks =
(* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
@@ -70,7 +67,6 @@ let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver task
Call_provers.print_prover_answer answer
let verify ?(debug = false) format loadpath ?memlimit ?timeout ~prover file =
- let open Why3 in
if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
let env, config = create_env loadpath in
let steplimit = None in