diff --git a/bin/dune b/bin/dune
index 0fe64358fdda03515cf58ec8dfa738cdfc87575b..45f3f6d1325e66f8f6a675268bdd0f51ebf1192d 100644
--- a/bin/dune
+++ b/bin/dune
@@ -3,5 +3,4 @@
(section bin)
(files
(findmodule.py as findmodule.py)
- (nnenum.sh as nnenum.sh))
-)
+ (nnenum.sh as nnenum.sh)))
diff --git a/lib/onnx/dune b/lib/onnx/dune
index 0ced853d1999ef061703a71b0346d21bd8a6cc26..ae47764e9d1ef1fc911e72084072b4ab02690fd4 100644
--- a/lib/onnx/dune
+++ b/lib/onnx/dune
@@ -5,7 +5,10 @@
(synopsis "ONNX parser for CAISAR"))
(rule
- (deps onnx_protoc.proto generate_onnx_interface.sh (package ocaml-protoc-plugin))
+ (deps
+ onnx_protoc.proto
+ generate_onnx_interface.sh
+ (package ocaml-protoc-plugin))
(targets onnx_protoc.ml)
(action
(run ./generate_onnx_interface.sh)))
diff --git a/src/interpretation.ml b/src/interpretation.ml
new file mode 100644
index 0000000000000000000000000000000000000000..eb1cdc00bf9db887ab74764ad998bcd5b912beca
--- /dev/null
+++ b/src/interpretation.ml
@@ -0,0 +1,128 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module CRE = Reduction_engine (* Caisar Reduction Engine *)
+open Why3
+open Base
+
+type dataset = { dataset : string } [@@deriving show]
+type caisar_op = Dataset of dataset [@@deriving show]
+
+type caisar_env = {
+ dataset_ty : Ty.ty;
+ caisar_op_of_ls : caisar_op Term.Hls.t;
+ ls_of_caisar_op : (caisar_op, Term.lsymbol) Hashtbl.t;
+ cwd : string;
+}
+
+let ls_of_caisar_op engine op =
+ let caisar_env = CRE.user_env engine in
+ Hashtbl.find_or_add caisar_env.ls_of_caisar_op op ~default:(fun () ->
+ let id = Ident.id_fresh "caisar_op" in
+ let ty = match op with Dataset _ -> caisar_env.dataset_ty in
+ let ls = Term.create_fsymbol id [] ty in
+ Hashtbl.Poly.add_exn caisar_env.ls_of_caisar_op ~key:op ~data:ls;
+ Term.Hls.add caisar_env.caisar_op_of_ls ls op;
+ ls)
+
+let caisar_op_of_ls engine ls =
+ let caisar_env = CRE.user_env engine in
+ Term.Hls.find caisar_env.caisar_op_of_ls ls
+
+let term_of_caisar_op engine op =
+ Term.t_app_infer (ls_of_caisar_op engine op) []
+
+let caisar_env env cwd =
+ let th = Env.read_theory env [ "caisar" ] "Interpretation" in
+ let ts_dataset = Theory.ns_find_ts th.Theory.th_export [ "dataset" ] in
+ {
+ dataset_ty = Ty.ty_app ts_dataset [];
+ ls_of_caisar_op = Hashtbl.Poly.create ();
+ caisar_op_of_ls = Term.Hls.create 10;
+ cwd;
+ }
+
+let print_caisar_op fmt caisar_env =
+ Pp.print_iter2 Term.Hls.iter Pp.newline Pp.comma Pretty.print_ls pp_caisar_op
+ fmt caisar_env.caisar_op_of_ls
+
+let compute_size_of_dataset ~cwd s =
+ let d = Caml.Filename.concat cwd s in
+ Array.length (Caml.Sys.readdir d)
+
+let builtin_caisar : caisar_env CRE.built_in_theories list =
+ let open_dataset : _ CRE.builtin =
+ fun engine _ l _ ->
+ match l with
+ | [ Term { t_node = Tconst (ConstStr dataset); _ } ] ->
+ Term (term_of_caisar_op engine (Dataset { dataset }))
+ | _ -> invalid_arg "We want a string! ;)"
+ in
+ let size : _ CRE.builtin =
+ fun engine _ l _ ->
+ match l with
+ | [ Term { t_node = Tapp (ls, []); _ } ] -> (
+ match caisar_op_of_ls engine ls with
+ | Dataset { dataset } ->
+ let cwd = (CRE.user_env engine).cwd in
+ Int (BigInt.of_int (compute_size_of_dataset ~cwd dataset)))
+ | _ -> invalid_arg "We want a string! ;)"
+ in
+ [
+ ( [ "caisar" ],
+ "Interpretation",
+ [],
+ [ ("open_dataset", None, open_dataset); ("size", None, size) ] );
+ ]
+
+let interpret_task ~cwd env task =
+ let known_map = Task.task_known task in
+ let caisar_env = caisar_env env cwd in
+ let params =
+ {
+ CRE.compute_defs = true;
+ compute_builtin = true;
+ compute_def_set = Term.Sls.empty;
+ compute_max_quantifier_domain = Int.max_value;
+ }
+ in
+ let engine = CRE.create params env known_map caisar_env builtin_caisar in
+ let f = Task.task_goal_fmla task in
+ let f = CRE.normalize ~limit:1000 engine Term.Mvs.empty f in
+ Fmt.pr "%a : %a@.%a@." Pretty.print_pr (Task.task_goal task) Pretty.print_term
+ f print_caisar_op caisar_env
+
+let interpret ?debug ?format ~loadpath file =
+ let cwd =
+ match file with
+ | Verification.File.Stdin -> Unix.getcwd ()
+ | File s -> Caml.Filename.dirname s
+ | JSON _ -> Unix.getcwd () (*todo *)
+ in
+ let env, _config, mstr_theory =
+ Verification.open_file ?debug ?format ~loadpath file
+ in
+ Wstdlib.Mstr.iter
+ (fun _ theory ->
+ List.iter (Task.split_theory theory None None) ~f:(fun task ->
+ interpret_task ~cwd env task))
+ mstr_theory
diff --git a/src/interpretation.mli b/src/interpretation.mli
new file mode 100644
index 0000000000000000000000000000000000000000..68649f274c7cb2c8bd730daad025bff68d8fb658
--- /dev/null
+++ b/src/interpretation.mli
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(* *)
+(* 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
diff --git a/src/main.ml b/src/main.ml
index 00b42e06141554673f595fd6ec5299bdb182573c..77a4933e0692a1e07c800a77cbf25f74970dd5ff 100644
--- a/src/main.ml
+++ b/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,19 @@ 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 +282,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 +306,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 +359,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 +411,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)
diff --git a/src/reduction_engine.ml b/src/reduction_engine.ml
new file mode 100644
index 0000000000000000000000000000000000000000..cba302c08b0f0147e61d47b1772113209aca8192
--- /dev/null
+++ b/src/reduction_engine.ml
@@ -0,0 +1,1399 @@
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
+
+open Why3
+open Term
+
+[@@@ocaml.warning "-9"]
+
+let debug = Debug.register_info_flag ~desc:"" "Reduction_engine"
+
+(* {2 Values} *)
+
+type value =
+ | Term of term (* invariant: is in normal form *)
+ | Int of BigInt.t
+ | Real of Number.real_value
+
+(** {2 Environment} *)
+
+type rule = Svs.t * term list * term
+
+type params = {
+ compute_defs : bool;
+ compute_builtin : bool;
+ compute_def_set : Term.Sls.t;
+ compute_max_quantifier_domain : int;
+}
+
+type 'a builtin = 'a engine -> lsymbol -> value list -> Ty.ty option -> value
+
+and 'a engine = {
+ env : Env.env;
+ known_map : Decl.decl Ident.Mid.t;
+ rules : rule list Mls.t;
+ params : params;
+ ls_lt : lsymbol; (* The lsymbol for [int.Int.(<)] *)
+ user_env : 'a;
+ builtins : 'a builtin Hls.t;
+}
+
+let user_env x = x.user_env
+
+let v_attr_copy orig v =
+ match v with Int _ -> v | Real _ -> v | Term t -> Term (t_attr_copy orig t)
+
+let term_of_value v =
+ let open Number in
+ match v with
+ | Term t -> t
+ | Int n -> t_int_const n
+ | Real { rv_sig = s; rv_pow2 = pow2; rv_pow5 = pow5 } ->
+ t_real_const ~pow2 ~pow5 s
+
+exception NotNum
+
+let big_int_of_const c =
+ match c with
+ | Constant.ConstInt i -> i.Number.il_int
+ | Constant.ConstReal _ -> assert false
+ | Constant.ConstStr _ -> assert false
+
+let big_int_of_value v =
+ match v with
+ | Int n -> n
+ | Real _ -> assert false
+ | Term { t_node = Tconst c } -> big_int_of_const c
+ | Term _ -> raise NotNum
+
+let real_of_const c =
+ match c with
+ | Constant.ConstReal r -> r.Number.rl_real
+ | Constant.ConstInt _ -> assert false
+ | Constant.ConstStr _ -> assert false
+
+let real_of_value v =
+ match v with
+ | Real r -> r
+ | Int _ -> assert false
+ | Term { t_node = Tconst c } -> real_of_const c
+ | Term _ -> raise NotNum
+
+(* {2 Builtin symbols} *)
+
+(* all builtin functions *)
+
+exception Undetermined
+
+let to_bool b = if b then t_true else t_false
+
+let is_zero v =
+ try BigInt.eq (big_int_of_value v) BigInt.zero with NotNum -> false
+
+let is_one v =
+ try BigInt.eq (big_int_of_value v) BigInt.one with NotNum -> false
+
+let eval_int_op op simpl _ ls l ty =
+ match l with
+ | [ t1; t2 ] -> (
+ try
+ let n1 = big_int_of_value t1 in
+ let n2 = big_int_of_value t2 in
+ Int (op n1 n2)
+ with NotNum | Division_by_zero -> simpl ls t1 t2 ty)
+ | _ -> assert false
+
+let simpl_add _ls t1 t2 _ty =
+ if is_zero t1 then t2 else if is_zero t2 then t1 else raise Undetermined
+
+let simpl_sub _ls t1 t2 _ty = if is_zero t2 then t1 else raise Undetermined
+
+let simpl_mul _ls t1 t2 _ty =
+ if is_zero t1
+ then t1
+ else if is_zero t2
+ then t2
+ else if is_one t1
+ then t2
+ else if is_one t2
+ then t1
+ else raise Undetermined
+
+let simpl_div _ls t1 t2 _ty =
+ if is_zero t2 then raise Undetermined;
+ if is_zero t1 then t1 else if is_one t2 then t1 else raise Undetermined
+
+let simpl_mod _ls t1 t2 _ty =
+ if is_zero t2 then raise Undetermined;
+ if is_zero t1
+ then t1
+ else if is_one t2
+ then Int BigInt.zero
+ else raise Undetermined
+
+let simpl_minmax _ls v1 v2 _ty =
+ match (v1, v2) with
+ | Term t1, Term t2 -> if t_equal t1 t2 then v1 else raise Undetermined
+ | _ -> raise Undetermined
+
+let eval_int_rel op _ _ls l _ty =
+ match l with
+ | [ t1; t2 ] -> (
+ try
+ let n1 = big_int_of_value t1 in
+ let n2 = big_int_of_value t2 in
+ Term (to_bool (op n1 n2))
+ with NotNum | Division_by_zero ->
+ raise Undetermined (* t_app_value ls l ty *))
+ | _ -> assert false
+
+let eval_int_uop op _ _ls l _ty =
+ match l with
+ | [ t1 ] -> (
+ try
+ let n1 = big_int_of_value t1 in
+ Int (op n1)
+ with NotNum | Division_by_zero ->
+ raise Undetermined (* t_app_value ls l ty *))
+ | _ -> assert false
+
+let real_align ~pow2 ~pow5 r =
+ let open Number in
+ let { rv_sig = s; rv_pow2 = p2; rv_pow5 = p5 } = r in
+ let s = BigInt.mul s (BigInt.pow_int_pos_bigint 2 (BigInt.sub p2 pow2)) in
+ let s = BigInt.mul s (BigInt.pow_int_pos_bigint 5 (BigInt.sub p5 pow5)) in
+ s
+
+let eval_real_op op simpl _ ls l ty =
+ match l with
+ | [ t1; t2 ] -> (
+ try
+ let n1 = real_of_value t1 in
+ let n2 = real_of_value t2 in
+ Real (op n1 n2)
+ with NotNum -> simpl ls t1 t2 ty)
+ | _ -> assert false
+
+let eval_real_uop op _ _ls l _ty =
+ match l with
+ | [ t1 ] -> (
+ try
+ let n1 = real_of_value t1 in
+ Real (op n1)
+ with NotNum -> raise Undetermined)
+ | _ -> assert false
+
+let eval_real_rel op _ _ls l _ty =
+ let open Number in
+ match l with
+ | [ t1; t2 ] -> (
+ try
+ let n1 = real_of_value t1 in
+ let n2 = real_of_value t2 in
+ let s1, s2 =
+ let { rv_sig = s1; rv_pow2 = p21; rv_pow5 = p51 } = n1 in
+ let { rv_sig = s2; rv_pow2 = p22; rv_pow5 = p52 } = n2 in
+ if BigInt.sign s1 <> BigInt.sign s2
+ then (s1, s2)
+ else
+ let pow2 = BigInt.min p21 p22 in
+ let pow5 = BigInt.min p51 p52 in
+ let s1 = real_align ~pow2 ~pow5 n1 in
+ let s2 = real_align ~pow2 ~pow5 n2 in
+ (s1, s2)
+ in
+ Term (to_bool (op s1 s2))
+ with NotNum -> raise Undetermined (* t_app_value ls l ty *))
+ | _ -> assert false
+
+let real_0 = Number.real_value BigInt.zero
+let real_1 = Number.real_value BigInt.one
+
+let is_real t r =
+ try Number.compare_real (real_of_value t) r = 0 with NotNum -> false
+
+let real_opp r =
+ let open Number in
+ let { rv_sig = s; rv_pow2 = pow2; rv_pow5 = pow5 } = r in
+ real_value ~pow2 ~pow5 (BigInt.minus s)
+
+let real_add r1 r2 =
+ let open Number in
+ let { rv_sig = s1; rv_pow2 = p21; rv_pow5 = p51 } = r1 in
+ let { rv_sig = s2; rv_pow2 = p22; rv_pow5 = p52 } = r2 in
+ if BigInt.eq s1 BigInt.zero
+ then r2
+ else if BigInt.eq s2 BigInt.zero
+ then r1
+ else
+ let pow2 = BigInt.min p21 p22 in
+ let pow5 = BigInt.min p51 p52 in
+ let s1 = real_align ~pow2 ~pow5 r1 in
+ let s2 = real_align ~pow2 ~pow5 r2 in
+ real_value ~pow2 ~pow5 (BigInt.add s1 s2)
+
+let real_sub r1 r2 =
+ let open Number in
+ let { rv_sig = s1; rv_pow2 = p21; rv_pow5 = p51 } = r1 in
+ let { rv_sig = s2; rv_pow2 = p22; rv_pow5 = p52 } = r2 in
+ if BigInt.eq s2 BigInt.zero
+ then r1
+ else if BigInt.eq s1 BigInt.zero
+ then real_value ~pow2:p22 ~pow5:p52 (BigInt.minus s2)
+ else
+ let pow2 = BigInt.min p21 p22 in
+ let pow5 = BigInt.min p51 p52 in
+ let s1 = real_align ~pow2 ~pow5 r1 in
+ let s2 = real_align ~pow2 ~pow5 r2 in
+ real_value ~pow2 ~pow5 (BigInt.sub s1 s2)
+
+let real_mul r1 r2 =
+ let open Number in
+ let { rv_sig = s1; rv_pow2 = p21; rv_pow5 = p51 } = r1 in
+ let { rv_sig = s2; rv_pow2 = p22; rv_pow5 = p52 } = r2 in
+ let s = BigInt.mul s1 s2 in
+ let pow2 = BigInt.add p21 p22 in
+ let pow5 = BigInt.add p51 p52 in
+ real_value ~pow2 ~pow5 s
+
+let simpl_real_add _ls t1 t2 _ty =
+ if is_real t1 real_0
+ then t2
+ else if is_real t2 real_0
+ then t1
+ else raise Undetermined
+
+let simpl_real_sub _ls t1 t2 _ty =
+ if is_real t2 real_0 then t1 else raise Undetermined
+
+let simpl_real_mul _ls t1 t2 _ty =
+ if is_real t1 real_0
+ then t1
+ else if is_real t2 real_0
+ then t2
+ else if is_real t1 real_1
+ then t2
+ else if is_real t2 real_1
+ then t1
+ else raise Undetermined
+
+let real_pow r1 r2 =
+ let open Number in
+ let { rv_sig = s1; rv_pow2 = p21; rv_pow5 = p51 } = r1 in
+ let { rv_sig = s2; rv_pow2 = p22; rv_pow5 = p52 } = r2 in
+ if BigInt.le s1 BigInt.zero
+ then raise Undetermined
+ else if BigInt.lt p22 BigInt.zero || BigInt.lt p52 BigInt.zero
+ then raise NotNum
+ else
+ let s1 = try BigInt.to_int s1 with Failure _ -> raise NotNum in
+ let s2 = BigInt.mul s2 (BigInt.pow_int_pos_bigint 2 p22) in
+ let s2 = BigInt.mul s2 (BigInt.pow_int_pos_bigint 5 p52) in
+ let s =
+ if s1 = 1
+ then BigInt.one
+ else if BigInt.lt s2 BigInt.zero
+ then raise NotNum
+ else BigInt.pow_int_pos_bigint s1 s2
+ in
+ let pow2 = BigInt.mul p21 s2 in
+ let pow5 = BigInt.mul p51 s2 in
+ Number.real_value ~pow2 ~pow5 s
+
+let simpl_real_pow _ls t1 _t2 _ty =
+ if is_real t1 real_1 then t1 else raise Undetermined
+
+let real_from_int _ _ls l _ty =
+ match l with
+ | [ t ] -> (
+ try
+ let n = big_int_of_value t in
+ Real (Number.real_value n)
+ with NotNum -> raise Undetermined)
+ | _ -> assert false
+
+type 'a built_in_theories =
+ Env.pathname
+ * string
+ * (string * (Ty.tysymbol -> unit)) list
+ * (string * lsymbol ref option * 'a builtin) list
+
+let built_in_theories : unit -> 'a built_in_theories list =
+ fun () ->
+ [
+ (* ["bool"],"Bool", [], [ "True", None, eval_true ; "False", None,
+ eval_false ; ] ; *)
+ ( [ "int" ],
+ "Int",
+ [],
+ [
+ (Ident.op_infix "+", None, eval_int_op BigInt.add simpl_add);
+ (Ident.op_infix "-", None, eval_int_op BigInt.sub simpl_sub);
+ (Ident.op_infix "*", None, eval_int_op BigInt.mul simpl_mul);
+ (Ident.op_prefix "-", None, eval_int_uop BigInt.minus);
+ (Ident.op_infix "<", None, eval_int_rel BigInt.lt);
+ (Ident.op_infix "<=", None, eval_int_rel BigInt.le);
+ (Ident.op_infix ">", None, eval_int_rel BigInt.gt);
+ (Ident.op_infix ">=", None, eval_int_rel BigInt.ge);
+ ] );
+ ( [ "int" ],
+ "MinMax",
+ [],
+ [
+ ("min", None, eval_int_op BigInt.min simpl_minmax);
+ ("max", None, eval_int_op BigInt.max simpl_minmax);
+ ] );
+ ( [ "int" ],
+ "ComputerDivision",
+ [],
+ [
+ ("div", None, eval_int_op BigInt.computer_div simpl_div);
+ ("mod", None, eval_int_op BigInt.computer_mod simpl_mod);
+ ] );
+ ( [ "int" ],
+ "EuclideanDivision",
+ [],
+ [
+ ("div", None, eval_int_op BigInt.euclidean_div simpl_div);
+ ("mod", None, eval_int_op BigInt.euclidean_mod simpl_mod);
+ ] );
+ ( [ "real" ],
+ "Real",
+ [],
+ [
+ (Ident.op_prefix "-", None, eval_real_uop real_opp);
+ (Ident.op_infix "+", None, eval_real_op real_add simpl_real_add);
+ (Ident.op_infix "-", None, eval_real_op real_sub simpl_real_sub);
+ (Ident.op_infix "*", None, eval_real_op real_mul simpl_real_mul);
+ (Ident.op_infix "<", None, eval_real_rel BigInt.lt);
+ (Ident.op_infix "<=", None, eval_real_rel BigInt.le);
+ (Ident.op_infix ">", None, eval_real_rel BigInt.gt);
+ (Ident.op_infix ">=", None, eval_real_rel BigInt.ge);
+ ] );
+ ([ "real" ], "FromInt", [], [ ("from_int", None, real_from_int) ]);
+ ( [ "real" ],
+ "PowerReal",
+ [],
+ [ ("pow", None, eval_real_op real_pow simpl_real_pow) ] );
+ (* ["map"],"Map", ["map", builtin_map_type], [ "const", Some ls_map_const,
+ eval_map_const; "get", Some ls_map_get, eval_map_get; "set", Some
+ ls_map_set, eval_map_set; ] ; *)
+ ]
+
+let add_builtin_th env ((l, n, t, d) : 'a built_in_theories) =
+ let th = Env.read_theory env.env l n in
+ List.iter
+ (fun (id, r) ->
+ let ts = Theory.ns_find_ts th.Theory.th_export [ id ] in
+ r ts)
+ t;
+ List.iter
+ (fun (id, r, f) ->
+ let ls = Theory.ns_find_ls th.Theory.th_export [ id ] in
+ Hls.add env.builtins ls f;
+ match r with None -> () | Some r -> r := ls)
+ d
+
+let get_builtins env built_in_user =
+ Hls.clear env.builtins;
+ List.iter (add_builtin_th env) (built_in_theories ());
+ List.iter (add_builtin_th env) built_in_user
+
+(* {2 the reduction machine} *)
+
+(* OBSOLETE COMMENT
+
+ A configuration is a pair (t,s) where t is a stack of terms and s is a stack
+ of function symbols.
+
+ A configuration ([t1;..;tn],[f1;..;fk]) represents a whole term, its model,
+ as defined recursively by
+
+ model([t],[]) = t
+
+ model(t1::..::tn::t,f::s) = model(f(t1,..,tn)::t,s) where f is of arity n
+
+ A given term can be "exploded" into a configuration by reversing the rules
+ above
+
+ During reduction, the terms in the first stack are kept in normal form
+ (value). The normalization process can be defined as the repeated application
+ of the following rules.
+
+ ([t],[]) --> t // t is in normal form
+
+ if f(t1,..,tn) is not a redex then (t1::..::tn::t,f::s) -->
+ (f(t1,..,tn)::t,s)
+
+ if f(t1,..,tn) is a redex l sigma for a rule l -> r then (t1::..::tn::t,f::s)
+ --> (subst(sigma) @ t,explode(r) @ s) *)
+
+type substitution = term Mvs.t
+
+type cont =
+ | Kapp of lsymbol * Ty.ty option
+ | Kif of term * term * substitution
+ | Klet of vsymbol * term * substitution
+ | Kcase of term_branch list * substitution
+ | Keps of vsymbol
+ | Kquant of quant * vsymbol list * trigger
+ | Kbinop of binop
+ | Knot
+ | Keval of term * substitution
+
+type config = {
+ value_stack : value list;
+ cont_stack : (cont * term) list;
+ (* second term is the original term, for attribute and loc copy *)
+}
+
+(* This global variable is used to approximate a count of the elementary
+ simplifications that are done during normalization. This is used for
+ transformation step. *)
+let rec_step_limit = ref 0
+
+exception NoMatch of (term * term * term option) option
+exception NoMatchpat of (pattern * pattern) option
+
+let rec pattern_renaming (bound_vars, mt) p1 p2 =
+ match (p1.pat_node, p2.pat_node) with
+ | Pwild, Pwild -> (bound_vars, mt)
+ | Pvar v1, Pvar v2 -> (
+ try
+ let mt = Ty.ty_match mt v1.vs_ty v2.vs_ty in
+ let bound_vars = Mvs.add v2 v1 bound_vars in
+ (bound_vars, mt)
+ with Ty.TypeMismatch _ -> raise (NoMatchpat (Some (p1, p2))))
+ | Papp (ls1, tl1), Papp (ls2, tl2) when ls_equal ls1 ls2 ->
+ List.fold_left2 pattern_renaming (bound_vars, mt) tl1 tl2
+ | Por (p1a, p1b), Por (p2a, p2b) ->
+ let bound_vars, mt = pattern_renaming (bound_vars, mt) p1a p2a in
+ pattern_renaming (bound_vars, mt) p1b p2b
+ | Pas (p1, v1), Pas (p2, v2) -> (
+ try
+ let mt = Ty.ty_match mt v1.vs_ty v2.vs_ty in
+ let bound_vars = Mvs.add v2 v1 bound_vars in
+ pattern_renaming (bound_vars, mt) p1 p2
+ with Ty.TypeMismatch _ -> raise (NoMatchpat (Some (p1, p2))))
+ | _ -> raise (NoMatchpat (Some (p1, p2)))
+
+let first_order_matching (vars : Svs.t) (largs : term list) (args : term list) :
+ Ty.ty Ty.Mtv.t * substitution =
+ let rec loop bound_vars ((mt, mv) as sigma) largs args =
+ match (largs, args) with
+ | [], [] -> sigma
+ | t1 :: r1, t2 :: r2 -> (
+ (* Format.eprintf "matching terms %a and %a...@." Pretty.print_term t1
+ Pretty.print_term t2; *)
+ match t1.t_node with
+ | Tvar vs when Svs.mem vs vars -> (
+ try
+ let t = Mvs.find vs mv in
+ if t_equal t t2
+ then loop bound_vars sigma r1 r2
+ else raise (NoMatch (Some (t1, t2, Some t)))
+ with Not_found -> (
+ try
+ let ts = Ty.ty_match mt vs.vs_ty (t_type t2) in
+ let fv2 = t_vars t2 in
+ if Mvs.is_empty (Mvs.set_inter bound_vars fv2)
+ then loop bound_vars (ts, Mvs.add vs t2 mv) r1 r2
+ else raise (NoMatch (Some (t1, t2, None)))
+ with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2, None)))))
+ | Tapp (ls1, args1) -> (
+ match t2.t_node with
+ | Tapp (ls2, args2) when ls_equal ls1 ls2 -> (
+ let mt, mv =
+ loop bound_vars sigma (List.rev_append args1 r1)
+ (List.rev_append args2 r2)
+ in
+ try (Ty.oty_match mt t1.t_ty t2.t_ty, mv)
+ with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2, None))))
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Tquant (q1, bv1) -> (
+ match t2.t_node with
+ | Tquant (q2, bv2) when q1 = q2 ->
+ let vl1, _tl1, term1 = t_open_quant bv1 in
+ let vl2, _tl2, term2 = t_open_quant bv2 in
+ let bound_vars, term1, mt =
+ try
+ List.fold_left2
+ (fun (bound_vars, term1, mt) e1 e2 ->
+ let mt = Ty.ty_match mt e1.vs_ty e2.vs_ty in
+ let bound_vars = Mvs.add e2 e1 bound_vars in
+ (bound_vars, term1, mt))
+ (bound_vars, term1, mt) vl1 vl2
+ with Invalid_argument _ | Ty.TypeMismatch _ ->
+ raise (NoMatch (Some (t1, t2, None)))
+ in
+ loop bound_vars (mt, mv) (term1 :: r1) (term2 :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Tbinop (b1, t1_l, t1_r) -> (
+ match t2.t_node with
+ | Tbinop (b2, t2_l, t2_r) when b1 = b2 ->
+ loop bound_vars (mt, mv) (t1_l :: t1_r :: r1) (t2_l :: t2_r :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Tif (t11, t12, t13) -> (
+ match t2.t_node with
+ | Tif (t21, t22, t23) ->
+ loop bound_vars (mt, mv) (t11 :: t12 :: t13 :: r1)
+ (t21 :: t22 :: t23 :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Tlet (td1, tb1) -> (
+ match t2.t_node with
+ | Tlet (td2, tb2) ->
+ let v1, tl1 = t_open_bound tb1 in
+ let v2, tl2 = t_open_bound tb2 in
+ let mt =
+ try Ty.ty_match mt v1.vs_ty v2.vs_ty
+ with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2, None)))
+ in
+ let bound_vars = Mvs.add v2 v1 bound_vars in
+ loop bound_vars (mt, mv) (td1 :: tl1 :: r1) (td2 :: tl2 :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Tcase (ts1, tbl1) -> (
+ match t2.t_node with
+ | Tcase (ts2, tbl2) -> (
+ try
+ let bound_vars, mt, l1, l2 =
+ List.fold_left2
+ (fun (bound_vars, mt, l1, l2) tb1 tb2 ->
+ let p1, tb1 = t_open_branch tb1 in
+ let p2, tb2 = t_open_branch tb2 in
+ let bound_vars, mt =
+ pattern_renaming (bound_vars, mt) p1 p2
+ in
+ (bound_vars, mt, tb1 :: l1, tb2 :: l2))
+ (bound_vars, mt, ts1 :: r1, ts2 :: r2)
+ tbl1 tbl2
+ in
+ loop bound_vars (mt, mv) l1 l2
+ with Invalid_argument _ -> raise (NoMatch (Some (t1, t2, None))))
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Teps tb1 -> (
+ match t2.t_node with
+ | Teps tb2 ->
+ let v1, td1 = t_open_bound tb1 in
+ let v2, td2 = t_open_bound tb2 in
+ let mt =
+ try Ty.ty_match mt v1.vs_ty v2.vs_ty
+ with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2, None)))
+ in
+ let bound_vars = Mvs.add v2 v1 bound_vars in
+ loop bound_vars (mt, mv) (td1 :: r1) (td2 :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Tnot t1 -> (
+ match t2.t_node with
+ | Tnot t2 -> loop bound_vars sigma (t1 :: r1) (t2 :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Tvar v1 -> (
+ match t2.t_node with
+ | Tvar v2 -> (
+ try
+ if vs_equal v1 (Mvs.find v2 bound_vars)
+ then loop bound_vars sigma r1 r2
+ else raise (NoMatch (Some (t1, t2, None)))
+ with Not_found -> assert false)
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | (Tconst _ | Ttrue | Tfalse) when t_equal t1 t2 ->
+ loop bound_vars sigma r1 r2
+ | Tconst _ | Ttrue | Tfalse -> raise (NoMatch (Some (t1, t2, None))))
+ | _ -> raise (NoMatch None)
+ in
+ loop Mvs.empty (Ty.Mtv.empty, Mvs.empty) largs args
+
+exception Irreducible
+
+let one_step_reduce engine ls args =
+ try
+ let rules = Mls.find ls engine.rules in
+ let rec loop rules =
+ match rules with
+ | [] -> raise Irreducible
+ | (vars, largs, rhs) :: rem -> (
+ try
+ let sigma = first_order_matching vars largs args in
+ (sigma, rhs)
+ with NoMatch _ -> loop rem)
+ in
+ loop rules
+ with Not_found -> raise Irreducible
+
+let rec matching ((mt, mv) as sigma) t p =
+ match p.pat_node with
+ | Pwild -> sigma
+ | Pvar v -> (mt, Mvs.add v t mv)
+ | Por (p1, p2) -> (
+ try matching sigma t p1 with NoMatch _ -> matching sigma t p2)
+ | Pas (p, v) -> matching (mt, Mvs.add v t mv) t p
+ | Papp (ls1, pl) -> (
+ match t.t_node with
+ | Tapp (ls2, tl) ->
+ if ls_equal ls1 ls2
+ then List.fold_left2 matching sigma tl pl
+ else if ls2.ls_constr > 0
+ then raise (NoMatch None)
+ else raise Undetermined
+ | _ -> raise Undetermined)
+
+let rec extract_first n acc l =
+ if n = 0
+ then (acc, l)
+ else
+ match l with
+ | x :: r -> extract_first (n - 1) (x :: acc) r
+ | [] -> assert false
+
+(** If [t1] matches [i1 < vs] or [i1 <= vs] and [t2] matches [vs < i2] or
+ [vs <= i2], then return the bounds [i1(+1), vs, i2(-1)]. The +1/-1 shift the
+ bounds for strict unequalities operators to obtain inclusive bounds. *)
+let bounds ls_lt t1 t2 =
+ let lt order = function
+ (* match [i < vs] or [vs < i], return [i, vs] *)
+ | { t_node = Tapp (ls, [ t1; t2 ]) } when ls_equal ls ls_lt -> (
+ assert (Ty.(ty_equal (t_type t1) ty_int && ty_equal (t_type t2) ty_int));
+ match order t1 t2 with
+ | ( { t_node = Tconst (Constant.ConstInt { Number.il_int = i }) },
+ { t_node = Tvar vs } ) ->
+ (i, vs)
+ | _ -> raise Exit)
+ | _ -> raise Exit
+ in
+ let eq order = function
+ (* match [i = vs] or [vs = i], return [i, vs] *)
+ | { t_node = Tapp (ls, [ t1; t2 ]) }
+ when ls_equal ls Term.ps_equ
+ && Ty.ty_equal (t_type t1) Ty.ty_int
+ && Ty.ty_equal (t_type t2) Ty.ty_int -> (
+ match order t1 t2 with
+ | ( { t_node = Tconst (Constant.ConstInt { Number.il_int = i }) },
+ { t_node = Tvar vs } )
+ when Ty.ty_equal vs.vs_ty Ty.ty_int ->
+ (i, vs)
+ | _ -> raise Exit)
+ | _ -> raise Exit
+ in
+ let le order = function
+ (* match [i <= vs] or [vs <= i], return [i, vs] *)
+ | { t_node = Tbinop (Tor, t1, t2) } ->
+ let i, vs = lt order t1 in
+ let i', vs' = eq order t2 in
+ if not (BigInt.eq i i' && vs_equal vs vs') then raise Exit;
+ (i, vs)
+ | _ -> raise Exit
+ in
+ let bound order shift t =
+ (* match [i op vs] or [vs op i], op is [<] or [<=] *)
+ try le order t
+ with Exit ->
+ let i, vs = lt order t in
+ (shift i, vs)
+ in
+ let i1, vs = bound (fun t1 t2 -> (t1, t2)) BigInt.succ t1 in
+ let i2, vs' = bound (fun t1 t2 -> (t2, t1)) BigInt.pred t2 in
+ if not (vs_equal vs vs') then raise Exit;
+ (i1, vs, i2)
+
+(** [reduce_bounded_quant ls_lt limit t sigma st rem] detects a bounded
+ quantification and reduces it to conjunction:
+
+ forall v. a < v < b. t(v) --> f(a+1) /\ ... /\ f(b-1)
+
+ @param ls_lt lsymbol for [int.Int.(<)]
+ @param limit
+ Reduce if the difference between upper and lower bound is at most
+ [limit].
+
+ TODO:
+
+ - expand to bounded quantifications on range values
+ - compatiblity with reverse direction (forall i. b > i > a -> t)
+ - detect SPARK-style [forall i. if a < i /\ i < b then t else true] *)
+let reduce_bounded_quant ls_lt limit t sigma st rem =
+ match (st, rem) with
+ (* st = a < vs < b :: _; rem = -> :: forall vs :: _ *)
+ | ( Term { t_node = Tbinop (Tand, t1, t2) } :: st,
+ ( (Kbinop Timplies, _)
+ :: (Kquant ((Tforall as quant), [ vs ], _), _)
+ :: rem
+ | (Kbinop Tand, _) :: (Kquant ((Texists as quant), [ vs ], _), _) :: rem
+ ) )
+ when Ty.ty_equal vs.vs_ty Ty.ty_int ->
+ let t_empty, binop =
+ match quant with Tforall -> (t_true, Tand) | Texists -> (t_false, Tor)
+ in
+ let a, vs', b = bounds ls_lt t1 t2 in
+ if not (vs_equal vs vs') then raise Exit;
+ if BigInt.(gt (sub b a) (of_int limit)) then raise Exit;
+ if BigInt.gt a b
+ then (* empty range *)
+ { value_stack = Term t_empty :: st; cont_stack = rem }
+ else
+ let rec loop rem i =
+ if BigInt.lt i a
+ then rem
+ else
+ let t_i = t_const (Constant.int_const i) Ty.ty_int in
+ let rem =
+ (* conjunction for all i > a *)
+ if BigInt.gt i a then (Kbinop binop, t_true) :: rem else rem
+ in
+ let rem = (Keval (t, Mvs.add vs t_i sigma), t_true) :: rem in
+ loop rem (BigInt.pred i)
+ in
+ { value_stack = st; cont_stack = loop rem b }
+ | _ -> raise Exit
+
+let rec reduce engine c =
+ match (c.value_stack, c.cont_stack) with
+ | _, [] -> assert false
+ | st, (Keval (t, sigma), orig) :: rem -> (
+ let limit = engine.params.compute_max_quantifier_domain in
+ try reduce_bounded_quant engine.ls_lt limit t sigma st rem
+ with Exit -> reduce_eval engine st t ~orig sigma rem)
+ | [], (Kif _, _) :: _ -> assert false
+ | v :: st, (Kif (t2, t3, sigma), orig) :: rem -> (
+ match v with
+ | Term { t_node = Ttrue } ->
+ incr rec_step_limit;
+ {
+ value_stack = st;
+ cont_stack = (Keval (t2, sigma), t_attr_copy orig t2) :: rem;
+ }
+ | Term { t_node = Tfalse } ->
+ incr rec_step_limit;
+ {
+ value_stack = st;
+ cont_stack = (Keval (t3, sigma), t_attr_copy orig t3) :: rem;
+ }
+ | Term t1 -> (
+ match (t1.t_node, t2.t_node, t3.t_node) with
+ | ( Tapp (ls, [ b0; { t_node = Tapp (ls1, _) } ]),
+ Tapp (ls2, _),
+ Tapp (ls3, _) )
+ when ls_equal ls ps_equ && ls_equal ls1 fs_bool_true
+ && ls_equal ls2 fs_bool_true && ls_equal ls3 fs_bool_false ->
+ incr rec_step_limit;
+ { value_stack = Term (t_attr_copy orig b0) :: st; cont_stack = rem }
+ | _ ->
+ {
+ value_stack =
+ Term
+ (t_attr_copy orig (t_if t1 (t_subst sigma t2) (t_subst sigma t3)))
+ :: st;
+ cont_stack = rem;
+ })
+ | Int _ | Real _ -> assert false (* would be ill-typed *))
+ | [], (Klet _, _) :: _ -> assert false
+ | t1 :: st, (Klet (v, t2, sigma), orig) :: rem ->
+ incr rec_step_limit;
+ let t1 = term_of_value t1 in
+ {
+ value_stack = st;
+ cont_stack = (Keval (t2, Mvs.add v t1 sigma), t_attr_copy orig t2) :: rem;
+ }
+ | [], (Kcase _, _) :: _ -> assert false
+ | (Int _ | Real _) :: _, (Kcase _, _) :: _ -> assert false
+ | Term t1 :: st, (Kcase (tbl, sigma), orig) :: rem ->
+ reduce_match st t1 ~orig tbl sigma rem
+ | ( ([] | [ _ ] | (Int _ | Real _) :: _ | Term _ :: (Int _ | Real _) :: _),
+ (Kbinop _, _) :: _ ) ->
+ assert false
+ | Term t1 :: Term t2 :: st, (Kbinop op, orig) :: rem ->
+ incr rec_step_limit;
+ {
+ value_stack = Term (t_attr_copy orig (t_binary_simp op t2 t1)) :: st;
+ cont_stack = rem;
+ }
+ | [], (Knot, _) :: _ -> assert false
+ | (Int _ | Real _) :: _, (Knot, _) :: _ -> assert false
+ | Term t :: st, (Knot, orig) :: rem ->
+ incr rec_step_limit;
+ {
+ value_stack = Term (t_attr_copy orig (t_not_simp t)) :: st;
+ cont_stack = rem;
+ }
+ | st, (Kapp (ls, ty), orig) :: rem -> reduce_app engine st ~orig ls ty rem
+ | [], (Keps _, _) :: _ -> assert false
+ | (Int _ | Real _) :: _, (Keps _, _) :: _ -> assert false
+ | Term t :: st, (Keps v, orig) :: rem ->
+ {
+ value_stack = Term (t_attr_copy orig (t_eps_close v t)) :: st;
+ cont_stack = rem;
+ }
+ | [], (Kquant _, _) :: _ -> assert false
+ | (Int _ | Real _) :: _, (Kquant _, _) :: _ -> assert false
+ | Term t :: st, (Kquant (q, vl, tr), orig) :: rem ->
+ {
+ value_stack = Term (t_attr_copy orig (t_quant_close_simp q vl tr t)) :: st;
+ cont_stack = rem;
+ }
+
+and reduce_match st u ~orig tbl sigma cont =
+ let rec iter tbl =
+ match tbl with
+ | [] -> assert false (* pattern matching not exhaustive *)
+ | b :: rem -> (
+ let p, t = t_open_branch b in
+ try
+ let mt', mv' = matching (Ty.Mtv.empty, sigma) u p in
+ (* Format.eprintf "Pattern-matching succeeded:@\nmt' = @["; Ty.Mtv.iter
+ (fun tv ty -> Format.eprintf "%a -> %a," Pretty.print_tv tv
+ Pretty.print_ty ty) mt'; Format.eprintf "@]@\n"; Format.eprintf "mv'
+ = @["; Mvs.iter (fun v t -> Format.eprintf "%a -> %a,"
+ Pretty.print_vs v Pretty.print_term t) mv'; Format.eprintf "@]@.";
+ Format.eprintf "branch before inst: %a@." Pretty.print_term t; *)
+ let mv'', t = t_subst_types mt' mv' t in
+ (* Format.eprintf "branch after types inst: %a@." Pretty.print_term t;
+ Format.eprintf "mv'' = @["; Mvs.iter (fun v t -> Format.eprintf "%a
+ -> %a," Pretty.print_vs v Pretty.print_term t) mv''; Format.eprintf
+ "@]@."; *)
+ incr rec_step_limit;
+ {
+ value_stack = st;
+ cont_stack = (Keval (t, mv''), t_attr_copy orig t) :: cont;
+ }
+ with NoMatch _ -> iter rem)
+ in
+ try iter tbl
+ with Undetermined ->
+ let dmy = t_var (create_vsymbol (Ident.id_fresh "__dmy") (t_type u)) in
+ let tbls =
+ match t_subst sigma (t_case dmy tbl) with
+ | { t_node = Tcase (_, tbls) } -> tbls
+ | _ -> assert false
+ in
+ {
+ value_stack = Term (t_attr_copy orig (t_case u tbls)) :: st;
+ cont_stack = cont;
+ }
+
+and reduce_eval eng st t ~orig sigma rem =
+ let orig = t_attr_copy orig t in
+ match t.t_node with
+ | Tvar v -> (
+ match Ident.Mid.find v.vs_name eng.known_map with
+ | Decl.{ d_node = Dlogic dl } ->
+ incr rec_step_limit;
+ let _, ls_defn =
+ List.find
+ (fun (ls, _) ->
+ String.equal ls.ls_name.Ident.id_string v.vs_name.Ident.id_string)
+ dl
+ in
+ let vs, t = Decl.open_ls_defn ls_defn in
+ let aux vs t =
+ (* Create ε fc. λ vs. fc @ vs = t to make the value from known_map
+ compatible to reduce_func_app *)
+ let ty = Opt.get t.t_ty in
+ let app_ty = Ty.ty_func vs.vs_ty ty in
+ let fc = create_vsymbol (Ident.id_fresh "fc") app_ty in
+ t_eps
+ (t_close_bound fc
+ (t_quant Tforall
+ (t_close_quant [ vs ] []
+ (t_app ps_equ
+ [ t_app fs_func_app [ t_var fc; t_var vs ] (Some ty); t ]
+ None))))
+ in
+ let t = List.fold_right aux vs t in
+ { value_stack = Term t :: st; cont_stack = rem }
+ | _ -> assert false
+ | exception Not_found -> (
+ match Mvs.find v sigma with
+ | t ->
+ incr rec_step_limit;
+ { value_stack = Term (t_attr_copy orig t) :: st; cont_stack = rem }
+ | exception Not_found ->
+ (* this may happen, e.g when computing below a quantified formula *)
+ (* Format.eprintf "Tvar not found: %a@." Pretty.print_vs v; assert
+ false *)
+ { value_stack = Term orig :: st; cont_stack = rem }))
+ | Tif (t1, t2, t3) ->
+ {
+ value_stack = st;
+ cont_stack = (Keval (t1, sigma), t1) :: (Kif (t2, t3, sigma), orig) :: rem;
+ }
+ | Tlet (t1, tb) ->
+ let v, t2 = t_open_bound tb in
+ {
+ value_stack = st;
+ cont_stack = (Keval (t1, sigma), t1) :: (Klet (v, t2, sigma), orig) :: rem;
+ }
+ | Tcase (t1, tbl) ->
+ {
+ value_stack = st;
+ cont_stack = (Keval (t1, sigma), t1) :: (Kcase (tbl, sigma), orig) :: rem;
+ }
+ | Tbinop (op, t1, t2) ->
+ {
+ value_stack = st;
+ cont_stack =
+ (Keval (t1, sigma), t1)
+ :: (Keval (t2, sigma), t2)
+ :: (Kbinop op, orig) :: rem;
+ }
+ | Tnot t1 ->
+ {
+ value_stack = st;
+ cont_stack = (Keval (t1, sigma), t1) :: (Knot, orig) :: rem;
+ }
+ | Teps tb ->
+ let v, t1 = t_open_bound tb in
+ {
+ value_stack = st;
+ cont_stack = (Keval (t1, sigma), t1) :: (Keps v, orig) :: rem;
+ }
+ | Tquant (q, tq) ->
+ let vl, tr, t1 = t_open_quant tq in
+ {
+ value_stack = st;
+ cont_stack = (Keval (t1, sigma), t1) :: (Kquant (q, vl, tr), orig) :: rem;
+ }
+ | Tapp (ls, tl) ->
+ let args = List.rev_map (fun t -> (Keval (t, sigma), t)) tl in
+ {
+ value_stack = st;
+ cont_stack = List.rev_append args ((Kapp (ls, t.t_ty), orig) :: rem);
+ }
+ | Ttrue | Tfalse | Tconst _ ->
+ { value_stack = Term orig :: st; cont_stack = rem }
+
+and reduce_app engine st ls ~orig ty rem_cont =
+ if ls_equal ls ps_equ
+ then
+ match st with
+ | t2 :: t1 :: rem_st -> (
+ try reduce_equ ~orig rem_st t1 t2 rem_cont
+ with Undetermined -> reduce_app_no_equ engine st ls ~orig ty rem_cont)
+ | _ -> assert false
+ else if ls_equal ls fs_func_app
+ then
+ match st with
+ | t2 :: t1 :: rem_st -> (
+ try reduce_func_app ~orig ty rem_st t1 t2 rem_cont
+ with Undetermined -> reduce_app_no_equ engine st ls ~orig ty rem_cont)
+ | _ -> assert false
+ else reduce_app_no_equ engine st ls ~orig ty rem_cont
+
+and reduce_func_app ~orig _ty rem_st t1 t2 rem_cont =
+ (* attempt to decompile t1 under the form (epsilon fc. forall x. fc @ x =
+ body) that is equivalent to \x.body *)
+ match t1 with
+ | Term { t_node = Teps tb } -> (
+ let fc, t = Term.t_open_bound tb in
+ match t.t_node with
+ | Tquant (Tforall, tq) -> (
+ let vl, trig, t = t_open_quant tq in
+ let process lhs body equ elim =
+ let rvl = List.rev vl in
+ let rec remove_var lhs rvh rvt =
+ match lhs.t_node with
+ | Tapp (ls2, [ lhs1; ({ t_node = Tvar v1 } as arg) ])
+ when ls_equal ls2 fs_func_app && vs_equal v1 rvh -> (
+ match (rvt, lhs1) with
+ | rvh :: rvt, _ ->
+ let lhs1, fc2 = remove_var lhs1 rvh rvt in
+ let lhs2 = t_app ls2 [ lhs1; arg ] lhs.t_ty in
+ (t_attr_copy lhs lhs2, fc2)
+ | [], { t_node = Tvar fc1 } when vs_equal fc1 fc ->
+ let fcn = fc.vs_name in
+ let fc2 = Ident.id_derive fcn.Ident.id_string fcn in
+ let fc2 = create_vsymbol fc2 (t_type lhs) in
+ (t_attr_copy lhs (t_var fc2), fc2)
+ | _ -> raise Undetermined)
+ | _ -> raise Undetermined
+ in
+ match rvl with
+ | rvh :: rvt -> (
+ let lhs, fc2 = remove_var lhs rvh rvt in
+ let vh, vl =
+ match vl with [] -> assert false | vh :: vl -> (vh, vl)
+ in
+ let t2 = term_of_value t2 in
+ match vl with
+ | [] -> elim body vh t2
+ | _ ->
+ let eq = equ lhs body in
+ let tq = t_quant Tforall (t_close_quant vl trig eq) in
+ let body = t_attr_copy t (t_eps_close fc2 tq) in
+ {
+ value_stack = rem_st;
+ cont_stack =
+ (Keval (body, Mvs.add vh t2 Mvs.empty), t_attr_copy orig body)
+ :: rem_cont;
+ })
+ | _ -> raise Undetermined
+ in
+ match t.t_node with
+ | Tapp (ls1, [ lhs; body ]) when ls_equal ls1 ps_equ ->
+ let equ lhs body = t_attr_copy t (t_app ps_equ [ lhs; body ] None) in
+ let elim body vh t2 =
+ {
+ value_stack = rem_st;
+ cont_stack =
+ (Keval (body, Mvs.add vh t2 Mvs.empty), t_attr_copy orig body)
+ :: rem_cont;
+ }
+ in
+ process lhs body equ elim
+ | Tbinop (Tiff, ({ t_node = Tapp (ls1, [ lhs; tr ]) } as teq), body)
+ when ls_equal ls1 ps_equ && t_equal tr t_bool_true ->
+ let equ lhs body =
+ let lhs = t_attr_copy teq (t_app ps_equ [ lhs; tr ] None) in
+ t_attr_copy t (t_binary Tiff lhs body)
+ in
+ let elim body vh t2 =
+ let body = t_if body t_bool_true t_bool_false in
+ {
+ value_stack = rem_st;
+ cont_stack =
+ (Keval (body, Mvs.add vh t2 Mvs.empty), t_attr_copy orig body)
+ :: rem_cont;
+ }
+ in
+ process lhs body equ elim
+ | _ -> raise Undetermined)
+ | _ -> raise Undetermined)
+ | _ -> raise Undetermined
+
+and reduce_app_no_equ engine st ls ~orig ty rem_cont =
+ let arity = List.length ls.ls_args in
+ let args, rem_st = extract_first arity [] st in
+ try
+ let f = Hls.find engine.builtins ls in
+ let v = f engine ls args ty in
+ { value_stack = v_attr_copy orig v :: rem_st; cont_stack = rem_cont }
+ with Not_found | Undetermined -> (
+ let args = List.map term_of_value args in
+ match Ident.Mid.find ls.ls_name engine.known_map with
+ | exception Not_found ->
+ Debug.dprintf debug "Reduction engine, ident not found: %s@."
+ ls.ls_name.Ident.id_string;
+ {
+ value_stack = Term (t_attr_copy orig (t_app ls args ty)) :: rem_st;
+ cont_stack = rem_cont;
+ }
+ | d -> (
+ let rewrite () =
+ (* try a rewrite rule *)
+ try
+ (* Format.eprintf "try a rewrite rule on %a@." Pretty.print_ls ls; *)
+ let (mt, mv), rhs = one_step_reduce engine ls args in
+ (* Format.eprintf "rhs = %a@." Pretty.print_term rhs; Format.eprintf
+ "sigma = "; Mvs.iter (fun v t -> Format.eprintf "%a -> %a,"
+ Pretty.print_vs v Pretty.print_term t) (snd sigma); Format.eprintf
+ "@."; Format.eprintf "try a type match: %a and %a@."
+ (Pp.print_option Pretty.print_ty) ty (Pp.print_option
+ Pretty.print_ty) rhs.t_ty; *)
+ (* let type_subst = Ty.oty_match Ty.Mtv.empty rhs.t_ty ty in
+ Format.eprintf "subst of rhs: "; Ty.Mtv.iter (fun tv ty ->
+ Format.eprintf "%a -> %a," Pretty.print_tv tv Pretty.print_ty ty)
+ type_subst; Format.eprintf "@."; let rhs = t_ty_subst type_subst
+ Mvs.empty rhs in let sigma = Mvs.map (t_ty_subst type_subst
+ Mvs.empty) sigma in Format.eprintf "rhs = %a@." Pretty.print_term
+ rhs; Format.eprintf "sigma = "; Mvs.iter (fun v t -> Format.eprintf
+ "%a -> %a," Pretty.print_vs v Pretty.print_term t) sigma;
+ Format.eprintf "@."; *)
+ let mv, rhs = t_subst_types mt mv rhs in
+ incr rec_step_limit;
+ {
+ value_stack = rem_st;
+ cont_stack = (Keval (rhs, mv), orig) :: rem_cont;
+ }
+ with Irreducible ->
+ {
+ value_stack = Term (t_attr_copy orig (t_app ls args ty)) :: rem_st;
+ cont_stack = rem_cont;
+ }
+ in
+ match d.Decl.d_node with
+ | Decl.Dtype _ | Decl.Dprop _ -> assert false
+ | Decl.Dlogic dl ->
+ (* regular definition *)
+ let d = List.assq ls dl in
+ if engine.params.compute_defs
+ || Term.Sls.mem ls engine.params.compute_def_set
+ then
+ let vl, e = Decl.open_ls_defn d in
+ let add (mt, mv) x y =
+ (Ty.ty_match mt x.vs_ty (t_type y), Mvs.add x y mv)
+ in
+ let mt, mv = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vl args in
+ let mt = Ty.oty_match mt e.t_ty ty in
+ let mv, e = t_subst_types mt mv e in
+ {
+ value_stack = rem_st;
+ cont_stack = (Keval (e, mv), orig) :: rem_cont;
+ }
+ else rewrite ()
+ | Decl.Dparam _ | Decl.Dind _ -> rewrite ()
+ | Decl.Ddata dl -> (
+ (* constructor or projection *)
+ try
+ match args with
+ | [ { t_node = Tapp (ls1, tl1) } ] ->
+ (* if ls is a projection and ls1 is a constructor, we should compute
+ that projection *)
+ let rec iter dl =
+ match dl with
+ | [] -> raise Exit
+ | (_, csl) :: rem ->
+ let rec iter2 csl =
+ match csl with
+ | [] -> iter rem
+ | (cs, prs) :: rem2 ->
+ if ls_equal cs ls1
+ then
+ (* we found the right constructor *)
+ let rec iter3 prs tl1 =
+ match (prs, tl1) with
+ | Some pr :: prs, t :: tl1 ->
+ if ls_equal ls pr
+ then
+ (* projection found! *)
+ {
+ value_stack = Term (t_attr_copy orig t) :: rem_st;
+ cont_stack = rem_cont;
+ }
+ else iter3 prs tl1
+ | None :: prs, _ :: tl1 -> iter3 prs tl1
+ | _ -> raise Exit
+ in
+ iter3 prs tl1
+ else iter2 rem2
+ in
+ iter2 csl
+ in
+ iter dl
+ | _ -> raise Exit
+ with Exit -> rewrite ())))
+
+and reduce_equ ~(* engine *) orig st v1 v2 cont =
+ (* try *)
+ match (v1, v2) with
+ | Int n1, Int n2 ->
+ let b = to_bool (BigInt.eq n1 n2) in
+ incr rec_step_limit;
+ { value_stack = Term (t_attr_copy orig b) :: st; cont_stack = cont }
+ | Real r1, Real r2 ->
+ let b = to_bool (Number.compare_real r1 r2 = 0) in
+ incr rec_step_limit;
+ { value_stack = Term (t_attr_copy orig b) :: st; cont_stack = cont }
+ | Int n, Term { t_node = Tconst c } | Term { t_node = Tconst c }, Int n -> (
+ try
+ let n' = big_int_of_const c in
+ let b = to_bool (BigInt.eq n n') in
+ incr rec_step_limit;
+ { value_stack = Term (t_attr_copy orig b) :: st; cont_stack = cont }
+ with NotNum -> raise Undetermined)
+ | Real r, Term { t_node = Tconst c } | Term { t_node = Tconst c }, Real r -> (
+ try
+ let r' = real_of_const c in
+ let b = to_bool (Number.compare_real r r' = 0) in
+ incr rec_step_limit;
+ { value_stack = Term (t_attr_copy orig b) :: st; cont_stack = cont }
+ with NotNum -> raise Undetermined)
+ | Real _, Term _ | Term _, Real _ -> raise Undetermined
+ | Int _, Term _ | Term _, Int _ -> raise Undetermined
+ | Int _, Real _ | Real _, Int _ -> assert false
+ | Term t1, Term t2 -> reduce_term_equ ~orig st t1 t2 cont
+(* with Undetermined -> { value_stack = Term (t_equ (term_of_value v1)
+ (term_of_value v2)) :: st; cont_stack = cont; } *)
+
+and reduce_term_equ ~orig st t1 t2 cont =
+ if t_equal t1 t2
+ then
+ let () = incr rec_step_limit in
+ { value_stack = Term (t_attr_copy orig t_true) :: st; cont_stack = cont }
+ else
+ match (t1.t_node, t2.t_node) with
+ | Tconst c1, Tconst c2 -> (
+ match (c1, c2) with
+ | Constant.ConstInt i1, Constant.ConstInt i2 ->
+ let b = BigInt.eq i1.Number.il_int i2.Number.il_int in
+ incr rec_step_limit;
+ {
+ value_stack = Term (t_attr_copy orig (to_bool b)) :: st;
+ cont_stack = cont;
+ }
+ | _ -> raise Undetermined)
+ | Tapp (ls1, tl1), Tapp (ls2, tl2)
+ when ls1.ls_constr > 0 && ls2.ls_constr > 0 ->
+ if ls_equal ls1 ls2
+ then
+ let rec aux sigma t tyl l1 l2 =
+ match (tyl, l1, l2) with
+ | [], [], [] -> (sigma, t)
+ | ty :: tyl, t1 :: tl1, t2 :: tl2 ->
+ let v1 = create_vsymbol (Ident.id_fresh "") ty in
+ let v2 = create_vsymbol (Ident.id_fresh "") ty in
+ aux
+ (Mvs.add v1 t1 (Mvs.add v2 t2 sigma))
+ (t_and_simp (t_equ (t_var v1) (t_var v2)) t)
+ tyl tl1 tl2
+ | _ -> assert false
+ in
+ let sigma, t = aux Mvs.empty t_true ls1.ls_args tl1 tl2 in
+ let () = incr rec_step_limit in
+ { value_stack = st; cont_stack = (Keval (t, sigma), orig) :: cont }
+ else
+ {
+ value_stack = Term (t_attr_copy orig t_false) :: st;
+ cont_stack = cont;
+ }
+ | ( Tif (b, { t_node = Tapp (ls1, _) }, { t_node = Tapp (ls2, _) }),
+ Tapp (ls3, _) )
+ when ls_equal ls3 fs_bool_true && ls_equal ls1 fs_bool_true
+ && ls_equal ls2 fs_bool_false ->
+ incr rec_step_limit;
+ { value_stack = Term (t_attr_copy orig b) :: st; cont_stack = cont }
+ | _ -> raise Undetermined
+
+let rec reconstruct c =
+ match (c.value_stack, c.cont_stack) with
+ | [ Term t ], [] -> t
+ | _, [] -> assert false
+ | _, (k, orig) :: rem ->
+ let t, st =
+ match (c.value_stack, k) with
+ | st, Keval (t, sigma) -> (t_subst sigma t, st)
+ | [], Kif _ -> assert false
+ | v :: st, Kif (t2, t3, sigma) ->
+ (t_if (term_of_value v) (t_subst sigma t2) (t_subst sigma t3), st)
+ | [], Klet _ -> assert false
+ | t1 :: st, Klet (v, t2, sigma) ->
+ (t_let_close v (term_of_value t1) (t_subst sigma t2), st)
+ | [], Kcase _ -> assert false
+ | v :: st, Kcase (tbl, sigma) ->
+ (t_subst sigma (t_case (term_of_value v) tbl), st)
+ | ([] | [ _ ]), Kbinop _ -> assert false
+ | t1 :: t2 :: st, Kbinop op ->
+ (t_binary_simp op (term_of_value t2) (term_of_value t1), st)
+ | [], Knot -> assert false
+ | t :: st, Knot -> (t_not (term_of_value t), st)
+ | st, Kapp (ls, ty) ->
+ let args, rem_st = extract_first (List.length ls.ls_args) [] st in
+ let args = List.map term_of_value args in
+ (t_app ls args ty, rem_st)
+ | [], Keps _ -> assert false
+ | t :: st, Keps v -> (t_eps_close v (term_of_value t), st)
+ | [], Kquant _ -> assert false
+ | t :: st, Kquant (q, vl, tr) ->
+ (t_quant_close_simp q vl tr (term_of_value t), st)
+ in
+ reconstruct
+ { value_stack = Term (t_attr_copy orig t) :: st; cont_stack = rem }
+
+(** iterated reductions *)
+
+let normalize ?step_limit ~limit engine sigma t0 =
+ rec_step_limit := 0;
+ let rec many_steps c n =
+ match (c.value_stack, c.cont_stack) with
+ | [ Term t ], [] -> t
+ | _, [] -> assert false
+ | _ -> (
+ if n = limit
+ then
+ let t1 = reconstruct c in
+ (* Loc.warning "reduction of term %a takes more than %d steps, aborted at %a.@."
+ * Pretty.print_term t0 limit Pretty.print_term t1; *)
+ t1
+ else
+ match step_limit with
+ | None ->
+ let c = reduce engine c in
+ many_steps c (n + 1)
+ | Some step_limit ->
+ if !rec_step_limit >= step_limit
+ then reconstruct c
+ else
+ let c = reduce engine c in
+ many_steps c (n + 1))
+ in
+ let c = { value_stack = []; cont_stack = [ (Keval (t0, sigma), t0) ] } in
+ many_steps c 0
+
+(* the rewrite engine *)
+
+let create p env km user_env built_in_user =
+ let th = Env.read_theory env [ "int" ] "Int" in
+ let ls_lt = Theory.ns_find_ls th.Theory.th_export [ Ident.op_infix "<" ] in
+ let env =
+ {
+ env;
+ known_map = km;
+ rules = Mls.empty;
+ params = p;
+ ls_lt;
+ builtins = Hls.create 17;
+ user_env;
+ }
+ in
+ if p.compute_builtin then get_builtins env built_in_user;
+ env
+
+exception NotARewriteRule of string
+
+let extract_rule _km t =
+ (* let check_ls ls = try let _ = Hls.find builtins ls in raise
+ (NotARewriteRule "root of lhs of rule must not be a built-in symbol") with
+ Not_found -> let d = Ident.Mid.find ls.ls_name km in match d.Decl.d_node
+ with | Decl.Dtype _ | Decl.Dprop _ -> assert false | Decl.Dlogic _ -> raise
+ (NotARewriteRule "root of lhs of rule must not be defined symbol") |
+ Decl.Ddata _ -> raise (NotARewriteRule "root of lhs of rule must not be a
+ constructor nor a projection") | Decl.Dparam _ | Decl.Dind _ -> () in *)
+ let check_vars acc t1 t2 =
+ (* check that quantified variables all appear in the lefthand side
+ (quantified variables not appearing could be removed and those appearing
+ on right hand side cannot be guessed during rewriting). *)
+ let vars_lhs = t_vars t1 in
+ if Svs.exists (fun vs -> not (Mvs.mem vs vars_lhs)) acc
+ then raise (NotARewriteRule "lhs should contain all variables");
+ (* check the same with type variables *)
+ if not
+ (Ty.Stv.subset
+ (t_ty_freevars Ty.Stv.empty t2)
+ (t_ty_freevars Ty.Stv.empty t2))
+ then raise (NotARewriteRule "lhs should contain all type variables")
+ in
+
+ let rec aux acc t =
+ match t.t_node with
+ | Tquant (Tforall, q) ->
+ let vs, _, t = t_open_quant q in
+ aux (List.fold_left (fun acc v -> Svs.add v acc) acc vs) t
+ | Tbinop (Tiff, t1, t2) -> (
+ match t1.t_node with
+ | Tapp (ls, args) ->
+ (* check_ls ls; *)
+ check_vars acc t1 t2;
+ (acc, ls, args, t2)
+ | _ -> raise (NotARewriteRule "lhs of <-> should be a predicate symbol"))
+ | Tapp (ls, [ t1; t2 ]) when ls == ps_equ -> (
+ match t1.t_node with
+ | Tapp (ls, args) ->
+ (* check_ls ls; *)
+ check_vars acc t1 t2;
+ (acc, ls, args, t2)
+ | _ -> raise (NotARewriteRule "lhs of = should be a function symbol"))
+ | _ ->
+ raise
+ (NotARewriteRule
+ "rule should be of the form forall ... t1 = t2 or f1 <-> f2")
+ in
+ aux Svs.empty t
+
+let add_rule t e =
+ let vars, ls, args, r = extract_rule e.known_map t in
+ let rules = try Mls.find ls e.rules with Not_found -> [] in
+ { e with rules = Mls.add ls ((vars, args, r) :: rules) e.rules }
diff --git a/src/reduction_engine.mli b/src/reduction_engine.mli
new file mode 100644
index 0000000000000000000000000000000000000000..53407b21dc4ffbc5d16c4fe31d0ae29f2c474ded
--- /dev/null
+++ b/src/reduction_engine.mli
@@ -0,0 +1,147 @@
+(********************************************************************)
+(* *)
+(* 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 'a engine
+(** abstract type for reduction engines *)
+
+val user_env : 'a engine -> 'a
+
+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 *)
+
+type value =
+ | Term of Why3.Term.term (* invariant: is in normal form *)
+ | Int of BigInt.t
+ | Real of Number.real_value
+
+type 'a builtin =
+ 'a engine -> Why3.Term.lsymbol -> value list -> Ty.ty option -> value
+
+type 'a built_in_theories =
+ Env.pathname
+ * string
+ * (string * (Ty.tysymbol -> unit)) list
+ * (string * Why3.Term.lsymbol ref option * 'a builtin) list
+
+val create :
+ params ->
+ Env.env ->
+ Decl.decl Ident.Mid.t ->
+ 'a ->
+ 'a built_in_theories list ->
+ 'a 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 -> 'a engine -> 'a 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 ->
+ 'a 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
diff --git a/src/verification.ml b/src/verification.ml
index 8fe43e4d62d58ce27cf604b9f6ebbe4e0c3eda2e..1a7162ed2893184454caec1df7a254b7b7f768a2 100644
--- a/src/verification.ml
+++ b/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 =
diff --git a/src/verification.mli b/src/verification.mli
index 8dc39393c8207ff54c87d58efdc8bafd3acb83c3..0dabf9670ffe682990390fb261ee1926707ae4f4 100644
--- a/src/verification.mli
+++ b/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. *)
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index aeea7093ede433c836821d58fd184d9c7097a2e4..13583bb6717ccf627ea755f124a9239c4f49da89 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -80,3 +80,18 @@ theory NN
function relu (a: t): t = if a .> (0.0:t) then a else (0.0:t)
end
+
+theory Interpretation
+ use bool.Bool
+ use int.Int
+
+ type input
+ type dataset
+
+ function open_dataset string: dataset
+ function size dataset: int
+
+ function get (i:int) (d:dataset) : input
+
+ predicate forall_ (d: dataset) (f: input -> bool) = forall i:int. -1 < i < size d -> f (get i d)
+end
diff --git a/tests/datasets/a/a001.png b/tests/datasets/a/a001.png
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/datasets/a/a002.png b/tests/datasets/a/a002.png
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/dune b/tests/dune
index 26d29551ce04dff1407fd7b9534efbadc0354950..8db19e46cb68c6ba9fc2e8eac42565dbcb5c0514 100644
--- a/tests/dune
+++ b/tests/dune
@@ -10,5 +10,6 @@
bin/aimos
bin/cvc5
bin/nnenum.sh
- filter_tmpdir.sh)
+ filter_tmpdir.sh
+ (glob_files "datasets/a/*"))
(package caisar))
diff --git a/tests/interpretation.t b/tests/interpretation.t
new file mode 100644
index 0000000000000000000000000000000000000000..31dcd1a89e47f5b01d3aa3242820e98199857992
--- /dev/null
+++ b/tests/interpretation.t
@@ -0,0 +1,43 @@
+Test interpret
+ $ caisar interpret -L . --format whyml - 2>&1 <<EOF | ./filter_tmpdir.sh
+ > theory T
+ > use caisar.Interpretation
+ > use int.Int
+ >
+ > goal G1: 1+1=2
+ >
+ > goal G2: 1+1=3
+ >
+ > goal G3: size (open_dataset "datasets/a") = 2
+ >
+ > goal G4:
+ > let dataset = open_dataset "datasets/a" in
+ > size dataset = 2
+ >
+ > predicate robust (i: input)
+ >
+ > goal G5:
+ > let dataset = open_dataset "datasets/a" in
+ > forall_ dataset (fun i -> robust i)
+ >
+ > goal G6:
+ > let dataset = open_dataset "datasets/a" in
+ > forall i:int. i=1+(size dataset) -> i < 4
+ > end
+ > EOF
+ G1 : true
+
+ G2 : false
+
+ G3 : true
+ caisar_op,
+ (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })
+ G4 : true
+ caisar_op1,
+ (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })
+ G5 : robust (get 0 caisar_op2) /\ robust (get 1 caisar_op2)
+ caisar_op2,
+ (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })
+ G6 : forall i:int. i = 3 -> i < 4
+ caisar_op3,
+ (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })