[sledge] Refactor: Expose Context.fold_vars instead of fold_terms

Summary: and define fv in terms of it.

Reviewed By: jvillard

Differential Revision: D22571134

fbshipit-source-id: 03c55281f

sledge/src/fol.ml

@@ -1211,7 +1211,6 @@ module Context = struct
     (vs_of_ses vs', z)
 
   let rename x sub = Ses.Equality.rename x (v_map_ses (Var.Subst.apply sub))
-  let fv x = vs_of_ses (Ses.Equality.fv x)
   let is_true x = Ses.Equality.is_true x
   let is_false x = Ses.Equality.is_false x
   let implies x b = Ses.Equality.implies x (f_to_ses b)
@@ -1221,8 +1220,10 @@ module Context = struct
 
   let normalize x e = ses_map (Ses.Equality.normalize x) e
 
-  let fold_terms ~init x ~f =
+  let fold_vars ~init x ~f =
-    Ses.Equality.fold_terms x ~init ~f:(fun s e -> f s (of_ses e))
+    Ses.Equality.fold_vars x ~init ~f:(fun s v -> f s (v_of_ses v))
+
+  let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
 
   (* Classes *)
 

sledge/src/fol.mli

@@ -204,9 +204,6 @@ module Context : sig
   val rename : t -> Var.Subst.t -> t
   (** Apply a renaming substitution to the relation. *)
 
-  val fv : t -> Var.Set.t
-  (** The variables occurring in the terms of the relation. *)
-
   val is_true : t -> bool
   (** Test if the relation is diagonal. *)
 
@@ -230,7 +227,11 @@ module Context : sig
       relation, where [e'] and its subterms are expressed in terms of the
       relation's canonical representatives of each equivalence class. *)
 
-  val fold_terms : init:'a -> t -> f:('a -> Term.t -> 'a) -> 'a
+  val fold_vars : init:'a -> t -> f:('a -> Var.t -> 'a) -> 'a
+  (** Enumerate the variables occurring in the terms of the context. *)
+
+  val fv : t -> Var.Set.t
+  (** The variables occurring in the terms of the context. *)
 
   (** Solution Substitutions *)
   module Subst : sig

sledge/src/ses/equality.ml

@@ -696,8 +696,6 @@ let fold_terms r ~init ~f =
 let fold_vars r ~init ~f =
   fold_terms r ~init ~f:(fun init -> Term.fold_vars ~f ~init)
 
-let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
-
 (** Existential Witnessing and Elimination *)
 
 let subst_invariant us s0 s =

sledge/src/ses/equality.mli

@@ -47,9 +47,6 @@ val orN : Var.Set.t -> t list -> Var.Set.t * t
 val rename : t -> (Var.t -> Var.t) -> t
 (** Apply a renaming substitution to the relation. *)
 
-val fv : t -> Var.Set.t
-(** The variables occurring in the terms of the relation. *)
-
 val is_true : t -> bool
 (** Test if the relation is diagonal. *)
 
@@ -68,7 +65,7 @@ val normalize : t -> Term.t -> Term.t
     relation, where [e'] and its subterms are expressed in terms of the
     relation's canonical representatives of each equivalence class. *)
 
-val fold_terms : t -> init:'a -> f:('a -> Term.t -> 'a) -> 'a
+val fold_vars : t -> init:'a -> f:('a -> Var.t -> 'a) -> 'a
 
 (** Solution Substitutions *)
 module Subst : sig

sledge/src/ses/equality_test.ml

@@ -53,6 +53,7 @@ let%test_module _ =
     let and_eq a b r = and_eq wrt a b r |> snd
     let and_ r s = and_ wrt r s |> snd
     let or_ r s = or_ wrt r s |> snd
+    let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
 
     (* tests *)
 

sledge/src/sh.ml

@@ -81,8 +81,7 @@ let fold_vars_stem ?ignore_ctx {us= _; xs= _; ctx; pure; heap; djns= _}
   |> fun init ->
   Term.fold_vars ~f ~init (Formula.inject pure)
   |> fun init ->
-  if Option.is_some ignore_ctx then init
+  if Option.is_some ignore_ctx then init else Context.fold_vars ~f ~init ctx
-  else Context.fold_terms ~init ctx ~f:(fun init -> Term.fold_vars ~f ~init)
 
 let fold_vars ?ignore_ctx fold_vars q ~init ~f =
   fold_vars_stem ?ignore_ctx ~init ~f q