[Transformations] identity

Makefile

 all:
-	dune build @install caisar.opam nnet.opam
+	dune build --root=. @install caisar.opam nnet.opam
 
 test:
-	dune runtest
+	dune runtest --root=.
+
+promote:
+	dune promote --root=.

caisar.opam

@@ -19,7 +19,7 @@ depends: [
   "odoc" {with-doc}
 ]
 build: [
-  ["dune" "subst"] {dev}
+  ["dune" "subst" "--root" "."] {dev}
   [
     "dune"
     "build"
@@ -27,7 +27,8 @@ build: [
     name
     "-j"
     jobs
-    "--promote-install-files=false"
+    "--promote-install-files"
+    "false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}

config/drivers/pyrat.drv

@@ -6,7 +6,7 @@ prelude "(* this is the prelude for PyRAT *)"
 valid "^Inconsistent assumption$"
 
 
-printer "alt-ergo"
+printer "why3"
 filename "%f-%t-%g.why"
 
 valid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Valid"
@@ -25,16 +25,11 @@ steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\) steps)" 2
 time "why3cpulimit time : %s s"
 
 transformation "inline_trivial"
+transformation "introduce_premises"
 
 transformation "eliminate_builtin"
-transformation "eliminate_recursion"
-transformation "eliminate_inductive"
-transformation "eliminate_algebraic"
-transformation "eliminate_literal"
-transformation "eliminate_epsilon"
-transformation "eliminate_let_term"
-transformation "split_premise_right"
 transformation "simplify_formula"
+transformation "caisar_native_prover"
 
 theory BuiltIn
   syntax type int   "int"

nnet.opam

@@ -9,7 +9,7 @@ depends: [
   "odoc" {with-doc}
 ]
 build: [
-  ["dune" "subst"] {dev}
+  ["dune" "subst" "--root" "."] {dev}
   [
     "dune"
     "build"
@@ -17,7 +17,8 @@ build: [
     name
     "-j"
     jobs
-    "--promote-install-files=false"
+    "--promote-install-files"
+    "false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}

src/language.ml

@@ -8,6 +8,10 @@ open Base
 
 (* -- Support for the NNet neural network format. *)
 
+let loaded_nnets = Why3.Term.Hls.create 10
+
+let lookup_loaded_nnets = Why3.Term.Hls.find_opt loaded_nnets
+
 let nnet_parser env _ filename _ =
   let open Why3 in
   let header = Nnet.parse filename in
@@ -30,6 +34,7 @@ let nnet_parser env _ filename _ =
         (List.init header.n_inputs ~f)
         (Ty.ty_tuple (List.init header.n_outputs ~f))
     in
+    Why3.Term.Hls.add loaded_nnets ls_nnet_apply filename;
     let th_uc =
       Pmodule.add_pdecl ~vc:false th_uc
         (Pdecl.create_pure_decl (Decl.create_param_decl ls_nnet_apply))

src/language.mli

+val lookup_loaded_nnets : Why3.Term.lsymbol -> string option
+(** Return the filename of an nnets Why3 representation *)
+
+val register_nnet_support : unit -> unit
+(** register nnet parser *)

src/main.ml

@@ -10,6 +10,7 @@ module Format = Caml.Format
 
 let caisar = "caisar"
 
+let () = Transformations.init ()
 (* -- Logs. *)
 
 let pp_header =

src/transformations.ml

+open Base
+
+let get_input_variables =
+  let rec aux acc (term : Why3.Term.term) =
+    match term.t_node with
+    | Why3.Term.Tapp (ls, args) -> (
+      match Language.lookup_loaded_nnets ls with
+      | None -> acc
+      | Some _name ->
+        let add acc = function
+          | { Why3.Term.t_node = Tapp (vs, []); _ } -> Why3.Term.Sls.add vs acc
+          | arg ->
+            invalid_arg
+              (Fmt.str "No direct variable in application: %a"
+                 Why3.Pretty.print_term arg)
+        in
+        List.fold ~init:acc ~f:add args)
+    | _ -> Why3.Term.t_fold aux acc term
+  in
+  Why3.Trans.fold_decl
+    (fun decl acc -> Why3.Decl.decl_fold aux acc decl)
+    Why3.Term.Sls.empty
+
+let simplify_goal _input_variables = Why3.Trans.identity
+
+let caisar_native_prover = Why3.Trans.bind get_input_variables simplify_goal
+
+let init () =
+  Why3.Trans.register_transform
+    ~desc:"Transformation for provers that support loading neural networks."
+    "caisar_native_prover" caisar_native_prover

src/transformations.mli

+val init : unit -> unit
+(** register the transformations *)