From 284a2ae165e265ee46cb687001a49b1fae0a12fc Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sat, 15 Aug 2020 02:20:05 -0700 Subject: [PATCH] [sledge] Add: Formula.map_terms and use it to remove Context.Subst.substf Reviewed By: jvillard Differential Revision: D22571130 fbshipit-source-id: 91c9ee6ca --- sledge/src/fol.ml | 71 +++++++++++++++++++++++++++++++------------ sledge/src/fol.mli | 3 +- sledge/src/sh.ml | 2 +- sledge/src/sh_test.ml | 6 ++-- 4 files changed, 57 insertions(+), 25 deletions(-) diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 74afb01ea..98c019411 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -615,7 +615,7 @@ let fold_vars ~init e ~f = | `Fml p -> fold_vars_f ~f ~init p | #cnd as c -> fold_vars_c ~f ~init c -(** map_vars *) +(** map *) let map1 f e cons x = let x' = f x in @@ -636,6 +636,29 @@ let mapN f e cons xs = let xs' = Array.map_endo ~f xs in if xs' == xs then e else cons xs' +(** map_trms *) + +let rec map_trms_f ~f b = + match b with + | Tt | Ff -> b + | Eq (x, y) -> map2 f b _Eq x y + | Dq (x, y) -> map2 f b _Dq x y + | Eq0 x -> map1 f b _Eq0 x + | Dq0 x -> map1 f b _Dq0 x + | Gt0 x -> map1 f b _Gt0 x + | Ge0 x -> map1 f b _Ge0 x + | Lt0 x -> map1 f b _Lt0 x + | Le0 x -> map1 f b _Le0 x + | And (x, y) -> map2 (map_trms_f ~f) b _And x y + | Or (x, y) -> map2 (map_trms_f ~f) b _Or x y + | Iff (x, y) -> map2 (map_trms_f ~f) b _Iff x y + | Xor (x, y) -> map2 (map_trms_f ~f) b _Xor x y + | Cond {cnd; pos; neg} -> map3 (map_trms_f ~f) b _Cond cnd pos neg + | UPosLit (p, x) -> map1 f b (_UPosLit p) x + | UNegLit (p, x) -> map1 f b (_UNegLit p) x + +(** map_vars *) + let rec map_vars_t ~f e = match e with | Var _ as v -> (f (Var.of_ v) : var :> trm) @@ -654,24 +677,7 @@ let rec map_vars_t ~f e = | Project {ary; idx; tup} -> map1 (map_vars_t ~f) e (_Project ary idx) tup | Apply (g, x) -> map1 (map_vars_t ~f) e (_Apply g) x -let rec map_vars_f ~f e = - match e with - | Tt | Ff -> e - | Eq (x, y) -> map2 (map_vars_t ~f) e _Eq x y - | Dq (x, y) -> map2 (map_vars_t ~f) e _Dq x y - | Eq0 x -> map1 (map_vars_t ~f) e _Eq0 x - | Dq0 x -> map1 (map_vars_t ~f) e _Dq0 x - | Gt0 x -> map1 (map_vars_t ~f) e _Gt0 x - | Ge0 x -> map1 (map_vars_t ~f) e _Ge0 x - | Lt0 x -> map1 (map_vars_t ~f) e _Lt0 x - | Le0 x -> map1 (map_vars_t ~f) e _Le0 x - | And (x, y) -> map2 (map_vars_f ~f) e _And x y - | Or (x, y) -> map2 (map_vars_f ~f) e _Or x y - | Iff (x, y) -> map2 (map_vars_f ~f) e _Iff x y - | Xor (x, y) -> map2 (map_vars_f ~f) e _Xor x y - | Cond {cnd; pos; neg} -> map3 (map_vars_f ~f) e _Cond cnd pos neg - | UPosLit (p, x) -> map1 (map_vars_t ~f) e (_UPosLit p) x - | UNegLit (p, x) -> map1 (map_vars_t ~f) e (_UNegLit p) x +let map_vars_f ~f = map_trms_f ~f:(map_vars_t ~f) let rec map_vars_c ~f c = match c with @@ -1031,6 +1037,32 @@ module Formula = struct let map_vars = map_vars_f + let rec map_terms ~f b = + let lift_map1 : (exp -> exp) -> t -> (trm -> t) -> trm -> t = + fun f b cons x -> map1 f b (ap1f cons) (`Trm x) + in + let lift_map2 : + (exp -> exp) -> t -> (trm -> trm -> t) -> trm -> trm -> t = + fun f b cons x y -> map2 f b (ap2f cons) (`Trm x) (`Trm y) + in + match b with + | Tt | Ff -> b + | Eq (x, y) -> lift_map2 f b _Eq x y + | Dq (x, y) -> lift_map2 f b _Dq x y + | Eq0 x -> lift_map1 f b _Eq0 x + | Dq0 x -> lift_map1 f b _Dq0 x + | Gt0 x -> lift_map1 f b _Gt0 x + | Ge0 x -> lift_map1 f b _Ge0 x + | Lt0 x -> lift_map1 f b _Lt0 x + | Le0 x -> lift_map1 f b _Le0 x + | And (x, y) -> map2 (map_terms ~f) b _And x y + | Or (x, y) -> map2 (map_terms ~f) b _Or x y + | Iff (x, y) -> map2 (map_terms ~f) b _Iff x y + | Xor (x, y) -> map2 (map_terms ~f) b _Xor x y + | Cond {cnd; pos; neg} -> map3 (map_terms ~f) b _Cond cnd pos neg + | UPosLit (p, x) -> lift_map1 f b (_UPosLit p) x + | UNegLit (p, x) -> lift_map1 f b (_UNegLit p) x + let fold_map_vars ~init e ~f = let s = ref init in let f x = @@ -1392,7 +1424,6 @@ module Context = struct f ~key:(of_ses key) ~data:(of_ses data) ) let subst s = ses_map (Ses.Equality.Subst.subst s) - let substf s = f_ses_map (Ses.Equality.Subst.subst s) let partition_valid vs s = let t, ks, u = Ses.Equality.Subst.partition_valid (vs_to_ses vs) s in diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli index 4e9cb4d17..bc94ceb33 100644 --- a/sledge/src/fol.mli +++ b/sledge/src/fol.mli @@ -174,6 +174,7 @@ and Formula : sig (** Transform *) + val map_terms : f:(Term.t -> Term.t) -> t -> t val map_vars : f:(Var.t -> Var.t) -> t -> t val fold_map_vars : @@ -254,8 +255,6 @@ module Context : sig val subst : t -> Term.t -> Term.t (** Apply a substitution recursively to subterms. *) - val substf : t -> Formula.t -> Formula.t - val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t (** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks and ν are maximal where ∃ks. ν is universally valid, xs ⊇ ks diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 58a8d0e17..b86120d7e 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -638,7 +638,7 @@ let rec norm_ s q = ; let q = map q ~f_sjn:(norm_ s) ~f_ctx:Fn.id ~f_trm:(Context.Subst.subst s) - ~f_fml:(Context.Subst.substf s) + ~f_fml:(Formula.map_terms ~f:(Context.Subst.subst s)) in let xs, ctx = Context.apply_subst (Var.Set.union q.us q.xs) s q.ctx in exists_fresh xs {q with ctx} diff --git a/sledge/src/sh_test.ml b/sledge/src/sh_test.ml index 282b80447..0ce3818e2 100644 --- a/sledge/src/sh_test.ml +++ b/sledge/src/sh_test.ml @@ -146,7 +146,7 @@ let%test_module _ = {| ∃ %x_6 . %x_6 = %x_6^ ∧ (-1 + %y_7) = %y_7^ ∧ emp - (%y_7^ = (-1 + %y_7)) ∧ emp + ((%y_7^ = (-1 + %y_7)) ∧ tt) ∧ emp (-1 + %y_7) = %y_7^ ∧ emp |}] @@ -175,7 +175,9 @@ let%test_module _ = ∨ (∃ %b_2 . (⟨8,%a_1⟩ = (⟨4,%c_3⟩^⟨4,%b_2⟩)) ∧ emp) ) - tt ∧ emp * ( ( tt ∧ emp) ∨ ( (%x_6 ≠ 0) ∧ emp) ) + ((tt ∧ (tt ∧ tt)) ∧ tt) + ∧ emp + * ( ( tt ∧ emp) ∨ ( (%x_6 ≠ 0) ∧ emp) ) ( ( emp) ∨ ( (%x_6 ≠ 0) ∧ emp) ) |}] end )