From c83a86fa2950f7560f076912939571907afa76ff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 17 Mar 2023 11:42:19 +0100
Subject: [PATCH] [reduction_engine] Customized bounded_quant.
---
src/reduction_engine.ml | 1091 ++++++++++++++++++++------------------
src/reduction_engine.mli | 9 +
2 files changed, 575 insertions(+), 525 deletions(-)
diff --git a/src/reduction_engine.ml b/src/reduction_engine.ml
index aafdb54..0f2c683 100644
--- a/src/reduction_engine.ml
+++ b/src/reduction_engine.ml
@@ -34,8 +34,16 @@ type params = {
compute_max_quantifier_domain : int;
}
+type bounded_quant_result = {
+ new_quant: vsymbol list;
+ substitutions : term list;
+}
+
type 'a builtin = 'a engine -> lsymbol -> value list -> Ty.ty option -> value
+and 'a bounded_quant = 'a engine -> vsymbol -> cond:term ->
+ bounded_quant_result option
+
and 'a engine = {
env : Env.env;
known_map : Decl.decl Ident.Mid.t;
@@ -44,6 +52,7 @@ and 'a engine = {
ls_lt : lsymbol; (* The lsymbol for [int.Int.(<)] *)
user_env : 'a;
builtins : 'a builtin Hls.t;
+ bounded_quant : 'a bounded_quant;
}
let user_env x = x.user_env
@@ -104,11 +113,11 @@ let is_one v =
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)
+ 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 =
@@ -147,22 +156,22 @@ let simpl_minmax _ls v1 v2 _ty =
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 *))
+ 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 *))
+ 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 =
@@ -175,43 +184,43 @@ let real_align ~pow2 ~pow5 r =
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)
+ 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)
+ 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 *))
+ 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
@@ -314,10 +323,10 @@ let simpl_real_pow _ls t1 _t2 _ty =
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)
+ 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 =
@@ -327,7 +336,7 @@ type 'a built_in_theories =
* (string * lsymbol ref option * 'a builtin) list
let built_in_theories : unit -> 'a built_in_theories list =
- fun () ->
+ fun () ->
[
(* ["bool"],"Bool", [], [ "True", None, eval_true ; "False", None,
eval_false ; ] ; *)
@@ -392,14 +401,14 @@ 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)
+ 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)
+ 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 =
@@ -452,7 +461,7 @@ type cont =
type config = {
value_stack : value list;
cont_stack : (cont * term) list;
- (* second term is the original term, for attribute and loc copy *)
+ (* second term is the original term, for attribute and loc copy *)
}
(* This global variable is used to approximate a count of the elementary
@@ -467,22 +476,22 @@ 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))))
+ 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))))
+ 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) :
@@ -491,121 +500,121 @@ let first_order_matching (vars : Svs.t) (largs : term list) (args : term list) :
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 =
+ (* 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
- 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
+ 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
- (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))))
+ 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
@@ -619,10 +628,10 @@ let one_step_reduce engine ls args =
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)
+ try
+ let sigma = first_order_matching vars largs args in
+ (sigma, rhs)
+ with NoMatch _ -> loop rem)
in
loop rules
with Not_found -> raise Irreducible
@@ -632,17 +641,17 @@ let rec matching ((mt, mv) as sigma) t p =
| Pwild -> sigma
| Pvar v -> (mt, Mvs.add v t mv)
| Por (p1, p2) -> (
- try matching sigma t p1 with NoMatch _ -> matching sigma t 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)
+ 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
@@ -659,26 +668,26 @@ 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)
+ 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)
+ && 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
@@ -714,10 +723,10 @@ let bounds ls_lt t1 t2 =
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 =
+ - 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 engine 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,
@@ -725,7 +734,7 @@ let reduce_bounded_quant ls_lt limit t sigma st rem =
:: (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)
@@ -750,48 +759,79 @@ let reduce_bounded_quant ls_lt limit t sigma st rem =
loop rem (BigInt.pred i)
in
{ value_stack = st; cont_stack = loop rem b }
+ | ( Term cond :: st,
+ ( (Kbinop Timplies, _)
+ :: (Kquant ((Tforall as quant), [ vs ], _), t_orig)
+ :: rem ))-> (
+ match engine.bounded_quant engine vs ~cond with
+ | None -> raise Exit
+ | Some res ->
+ let t_empty, binop =
+ match quant with Tforall -> (t_true, Tand) | Texists -> (t_false, Tor)
+ in
+ let rem = match res.new_quant with [] -> rem | _ ->
+ (Kquant ((quant, res.new_quant, [])),t_orig)::rem
+ in
+ let rec loop rem = function
+ | [] -> rem
+ | t_i::l ->
+ let rem =
+ match l with [] -> rem | _ ->
+ (* conjunction *)
+ (Kbinop binop, t_true) :: rem
+ in
+ let rem = (Keval (t, Mvs.add vs t_i sigma), t_true) :: rem in
+ loop rem l
+ in
+ match res.substitutions with
+ | [] ->
+ { value_stack = Term t_empty :: st; cont_stack = rem }
+ | _ ->
+ { value_stack = st; cont_stack = loop rem res.substitutions
+ }
+ )
| _ -> 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)
+ let limit = engine.params.compute_max_quantifier_domain in
+ try reduce_bounded_quant engine 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 ->
+ match v with
+ | Term { t_node = Ttrue } ->
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 *))
+ 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;
@@ -843,26 +883,26 @@ and reduce_match st u ~orig tbl sigma cont =
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)
+ 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 ->
@@ -881,43 +921,43 @@ 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 ->
+ match Ident.Mid.find v.vs_name eng.known_map with
+ | Decl.{ d_node = Dlogic dl } ->
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 }))
+ 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;
@@ -973,15 +1013,15 @@ and reduce_app engine st ls ~orig ty rem_cont =
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)
+ 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)
+ 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
@@ -990,80 +1030,80 @@ and reduce_func_app ~orig _ty rem_st t1 t2 rem_cont =
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
+ let fc, t = Term.t_open_bound tb 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
+ | 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)
| _ -> raise Undetermined
and reduce_app_no_equ engine st ls ~orig ty rem_cont =
@@ -1074,109 +1114,109 @@ and reduce_app_no_equ engine st ls ~orig ty rem_cont =
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)
+ 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
- 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
+ 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
- (* 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
+ (* 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
- iter3 prs tl1
- else iter2 rem2
- in
- iter2 csl
- in
- iter dl
- | _ -> raise Exit
- with Exit -> rewrite ())))
+ iter2 csl
+ in
+ iter dl
+ | _ -> raise Exit
+ with Exit -> rewrite ())))
and reduce_equ ~(* engine *) orig st v1 v2 cont =
(* try *)
@@ -1190,19 +1230,19 @@ and reduce_equ ~(* engine *) orig st v1 v2 cont =
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)
+ 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)
+ 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
@@ -1218,15 +1258,15 @@ and reduce_term_equ ~orig st t1 t2 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)
+ 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
@@ -1303,30 +1343,30 @@ let normalize ?step_limit ~limit engine sigma t0 =
| [ 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
+ 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))
+ 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 create ?(bounded_quant=(fun _ _ ~cond:_ -> None)) 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 =
@@ -1338,6 +1378,7 @@ let create p env km user_env built_in_user =
ls_lt;
builtins = Hls.create 17;
user_env;
+ bounded_quant;
}
in
if p.compute_builtin then get_builtins env built_in_user;
@@ -1362,9 +1403,9 @@ let extract_rule _km t =
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))
+ (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
@@ -1374,19 +1415,19 @@ let extract_rule _km t =
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"))
+ 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"))
+ 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
diff --git a/src/reduction_engine.mli b/src/reduction_engine.mli
index 53407b2..695db72 100644
--- a/src/reduction_engine.mli
+++ b/src/reduction_engine.mli
@@ -99,7 +99,16 @@ type 'a built_in_theories =
* (string * (Ty.tysymbol -> unit)) list
* (string * Why3.Term.lsymbol ref option * 'a builtin) list
+ type bounded_quant_result = {
+ new_quant: Term.vsymbol list;
+ substitutions : Term.term list;
+ }
+
+type 'a bounded_quant = 'a engine -> Term.vsymbol -> cond:Term.term ->
+ bounded_quant_result option
+
val create :
+ ?bounded_quant:'a bounded_quant ->
params ->
Env.env ->
Decl.decl Ident.Mid.t ->
--
GitLab