[interpretation] Copy module reduction_engine from Why3.

src/interpretation.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(*  Copyright (C) 2022                                                    *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  You can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Why3
+open Base
+
+let interpret_task env task =
+  let f = Task.task_goal_fmla task in
+  let engine =
+    Reduction_engine.create
+      {
+        compute_defs = false;
+        compute_builtin = true;
+        compute_def_set = Term.Sls.empty;
+        compute_max_quantifier_domain = 0;
+      }
+      env Ident.Mid.empty
+  in
+  let f = Reduction_engine.normalize ~limit:1000 engine Term.Mvs.empty f in
+  Fmt.pr "%a : %a@." Pretty.print_pr (Task.task_goal task) Pretty.print_term f
+
+let interpret ?debug ?format ~loadpath s =
+  let env, _config, mstr_theory =
+    Verification.open_file ?debug ?format ~loadpath s
+  in
+  Wstdlib.Mstr.iter
+    (fun _ theory ->
+      List.iter (Task.split_theory theory None None) ~f:(fun task ->
+        interpret_task env task))
+    mstr_theory

src/interpretation.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(*  Copyright (C) 2022                                                    *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  You can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Base
+
+val interpret :
+  ?debug:bool ->
+  ?format:string ->
+  loadpath:string list ->
+  Verification.File.t ->
+  unit

src/main.ml

@@ -204,6 +204,10 @@ let verify_json ?memlimit ?timelimit ?outfile json =
       ~f:(record_verification_result jin.id verification_result)
   | _ -> failwith "Unexpected more than one theory from a JSON file"
 
+let interpret format loadpath files =
+  let debug = log_level_is_debug () in
+  List.iter ~f:(Interpretation.interpret ~debug ?format ~loadpath) files
+
 let exec_cmd cmdname cmd =
   Logs.debug (fun m -> m "Execution of command '%s'" cmdname);
   cmd ()
@@ -257,6 +261,20 @@ let timelimit =
   Arg.(
     value & opt (some string) None & info [ "t"; "timelimit" ] ~doc ~docv:"TIME")
 
+  let loadpath =
+    let doc = "Additional loadpath." in
+    Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
+
+  let format =
+    let doc = "File format." in
+    Arg.(value & opt (some string) None & info [ "format" ] ~doc)
+
+  let files =
+    let doc = "File to verify." in
+    let file_or_stdin = Arg.conv' Verification.File.(of_string, pretty) in
+    Arg.(non_empty & pos_all file_or_stdin [] & info [] ~doc ~docv:"FILE")
+
+
 let verify_cmd =
   let cmdname = "verify" in
   let info =
@@ -265,14 +283,6 @@ let verify_cmd =
       ~doc
       ~man:[ `S Manpage.s_description; `P doc ]
   in
-  let loadpath =
-    let doc = "Additional loadpath." in
-    Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
-  in
-  let format =
-    let doc = "File format." in
-    Arg.(value & opt (some string) None & info [ "format" ] ~doc)
-  in
   let prover =
     let all_provers = Prover.list_available () in
     let doc =
@@ -297,11 +307,6 @@ let verify_cmd =
     let doc = "Dataset $(docv) (CSV format only)." in
     Arg.(value & opt (some file) None & info [ "dataset" ] ~doc ~docv:"FILE")
   in
-  let files =
-    let doc = "File to verify." in
-    let file_or_stdin = Arg.conv' Verification.File.(of_string, pretty) in
-    Arg.(non_empty & pos_all file_or_stdin [] & info [] ~doc ~docv:"FILE")
-  in
   let term =
     Term.(
       const
@@ -355,6 +360,24 @@ let verify_json_cmd =
   in
   Cmd.v info term
 
+let interpret_cmd =
+  let cmdname = "interpret" in
+  let doc =
+    "Interpret the goal and print the strategy that will be executed."
+  in
+  let info =
+    Cmd.info cmdname ~sdocs:Manpage.s_common_options ~exits:Cmd.Exit.defaults
+      ~doc
+      ~man:[ `S Manpage.s_description; `P doc ]
+  in
+  let term =
+    Term.(
+      const (fun format loadpath files _ ->
+        exec_cmd cmdname (fun () -> interpret format loadpath files))
+      $ format $ loadpath $ files $ setup_logs)
+  in
+  Cmd.v info term
+
 let default_info =
   let doc =
     "A platform for characterizing the safety and robustness of artificial \
@@ -389,7 +412,7 @@ let () =
 let () =
   try
     Cmd.group ~default:default_cmd default_info
-      [ config_cmd; verify_cmd; verify_json_cmd ]
+      [ config_cmd; verify_cmd; verify_json_cmd; interpret_cmd ]
     |> Cmd.eval ~catch:false |> Caml.exit
   with exn when not (log_level_is_debug ()) ->
     Logs.err (fun m -> m "@[%a@]" Why3.Exn_printer.exn_printer exn)

src/reduction_engine.mli

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2022 --  Inria - CNRS - Paris-Saclay University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+
+(** A reduction engine for Why3 terms *)
+
+(*
+terms are normalized with respect to
+
+1) built-in computation rules
+
+ a) on propositional connectives, e.g.
+
+   f /\ true -> f
+
+ b) on integers, e.g.
+
+   35 + 7 -> 42
+
+ c) on projections of pairs and of other ADTs, e.g
+
+  fst (x,y) -> x
+
+  cdr (Cons x y) -> y
+
+ d) on defined function symbols, e.g.
+
+  function sqr (x:int) = x * x
+
+  sqr 4 -> 4 * 4 -> 16
+
+  sqr x -> x * x
+
+ e) (TODO?) on booleans, e.g.
+
+  True xor False -> True
+
+ f) (TODO?) on reals, e.g.
+
+  1.0 + 2.5 -> 3.5
+
+2) axioms declared as rewrite rules, thanks to the "rewrite" metas, e.g. if
+
+    function dot : t -> t -> t
+    axiom assoc: forall x y z, dot (dot x y) z = dot x (dot y z)
+    meta "rewrite" assoc
+
+  then
+
+  dot (dot a b) (dot c d) -> dot a (dot b (dot c d))
+
+  axioms used as rewrite rules must be either of the form
+
+    forall ... t1 = t2
+
+  or
+
+    forall ... f1 <-> f2
+
+   where the root symbol of t1 (resp. f1) is a non-interpreted function
+   symbol (resp. non-interpreted predicate symbol)
+
+  rewriting is done from left to right
+
+
+*)
+open Why3
+
+type engine
+(** abstract type for reduction engines *)
+
+type params = {
+  compute_defs : bool;
+  compute_builtin : bool;
+  compute_def_set : Term.Sls.t;
+  compute_max_quantifier_domain : int;
+}
+(** Configuration of the engine.
+   . [compute_defs]: if set to true, automatically compute symbols using
+     known definitions. Otherwise, only symbols in [compute_def_set]
+     will be computed.
+   . [compute_builtin]: if set to true, compute builtin functions.
+   . [compute_max_quantifier_domain]: maximum domain size for the reduction of
+     bounded quantifications *)
+
+val create : params -> Env.env -> Decl.decl Ident.Mid.t -> engine
+(** [create env known_map] creates a reduction engine with
+    . builtins theories (int.Int, etc.) extracted from [env]
+    . known declarations from [known_map]
+    . empty set of rewrite rules
+*)
+
+exception NotARewriteRule of string
+
+val add_rule : Term.term -> engine -> engine
+(** [add_rule t e] turns [t] into a new rewrite rule and returns the
+    new engine.
+
+    raise NotARewriteRule if [t] cannot be seen as a rewrite rule
+    according to the general rules given above.
+*)
+
+
+val normalize : ?step_limit:int -> limit:int -> engine -> Term.term Term.Mvs.t -> Term.term -> Term.term
+(** [normalize e sigma t] normalizes the term [t] with respect to the engine
+    [e] with an initial variable environment [sigma].
+
+    parameter [limit] provides a maximum number of steps for execution.
+    When limit is reached, the partially reduced term is returned.
+    parameter [step_limit] provides a maximum number of steps on reductions
+    that would change the term even after reconstruction.
+*)
+
+
+open Term
+
+exception NoMatch of (term * term * term option) option
+(** [NoMatch (t1, t2, t3)] Cannot match [t1] with [t2]. If [t3] exists then [t1]
+    is already matched with [t3]. *)
+
+exception NoMatchpat of (pattern * pattern) option
+
+type substitution = term Mvs.t
+
+val first_order_matching: Svs.t -> term list -> term list -> Ty.ty Ty.Mtv.t * substitution

src/verification.ml

@@ -274,10 +274,25 @@ let call_prover ?dataset ~limit config env prover config_prover driver task =
   let id = Task.task_goal task in
   { id; prover_answer; additional_info }
 
-let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
-  prover ?prover_altern file =
+let open_file ?(debug = false) ?format ~loadpath file =
   if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
   let env, config = create_env ~debug loadpath in
+  let mstr_theory =
+    match file with
+    | File.Stdin ->
+      Env.(read_channel ?format base_language env "stdin" Caml.stdin)
+    | File file ->
+      let mlw_files, _ = Env.(read_file ?format base_language env file) in
+      mlw_files
+    | JSON jin ->
+      let th = JSON.theory_of_input env jin in
+      Wstdlib.Mstr.singleton th.th_name.id_string th
+  in
+  (env, config, mstr_theory)
+
+let verify ?debug ?format ~loadpath ?memlimit ?timelimit ?dataset prover
+  ?prover_altern file =
+  let env, config, mstr_theory = open_file ?debug ?format ~loadpath file in
   let main = Whyconf.get_main config in
   let limit =
     let memlimit = Option.value memlimit ~default:(Whyconf.memlimit main) in
@@ -292,17 +307,6 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
       Call_provers.limit_mem = memlimit;
     }
   in
-  let mstr_theory =
-    match file with
-    | File.Stdin ->
-      Env.(read_channel ?format base_language env "stdin" Caml.stdin)
-    | File file ->
-      let mlw_files, _ = Env.(read_file ?format base_language env file) in
-      mlw_files
-    | JSON jin ->
-      let th = JSON.theory_of_input env jin in
-      Wstdlib.Mstr.singleton th.th_name.id_string th
-  in
   let config_prover =
     let altern =
       let default =

src/verification.mli

@@ -23,7 +23,10 @@
 open Why3
 
 module File : sig
-  type t
+  type t = private
+    | Stdin
+    | File of string
+    | JSON of JSON.input
 
   val of_json_input : JSON.input -> (t, string) result
   val of_string : string -> (t, string) result
@@ -71,3 +74,15 @@ val verify :
     @return
       for each theory, an [answer] for each goal of the theory, respecting the
       order of appearance. *)
+
+val open_file :
+  ?debug:bool ->
+  ?format:string ->
+  loadpath:string list ->
+  File.t ->
+  Env.env * Whyconf.config * Theory.theory Wstdlib.Mstr.t
+(** [open_file ?debug ?format ~loadpath file] just opens the given file.
+
+    @param debug when set, enables debug information.
+    @param format is the [file] format.
+    @param loadpath is the additional loadpath. *)

tests/interpretation.t

+Test verify
+  $ caisar interpret -L . --format whyml - 2>&1 <<EOF | ./filter_tmpdir.sh
+  > theory T
+  >  use int.Int
+  > 
+  >   goal G1: 1+1=2
+  > 
+  >   goal G2: 1+1=3
+  > 
+  > end
+  > EOF
+  G1 : true
+  G2 : false