[sledge] Refactor: Add Fol module to be used for external interface of solver

Reviewed By: ngorogiannis

Differential Revision: D22170509

fbshipit-source-id: f4ed2bfee

sledge/src/domain_sh.ml

@@ -7,7 +7,7 @@
 
 (** Abstract domain *)
 
-open Ses
+open Fol
 
 type t = Sh.t [@@deriving equal, sexp]
 

sledge/src/exec.ml

@@ -7,7 +7,7 @@
 
 (** Symbolic Execution *)
 
-open Ses
+open Fol
 
 [@@@warning "+9"]
 

sledge/src/exec.mli

@@ -7,7 +7,7 @@
 
 (** Symbolic Execution *)
 
-open Ses
+open Fol
 
 val assume : Sh.t -> Term.t -> Sh.t option
 val kill : Sh.t -> Var.t -> Sh.t

sledge/src/fol.ml

@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+module Var = Ses.Var
+module Term = Ses.Term
+module Equality = Ses.Equality

sledge/src/fol.mli

@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+module Var = Ses.Var
+module Term = Ses.Term
+module Equality = Ses.Equality

sledge/src/sh.ml

@@ -7,7 +7,7 @@
 
 (** Symbolic Heap Formulas *)
 
-open Ses
+open Fol
 
 [@@@warning "+9"]
 

sledge/src/sh.mli

@@ -7,7 +7,7 @@
 
 (** Symbolic Heap Formulas *)
 
-open Ses
+open Fol
 
 (** Segment of memory starting at [loc] containing [seq] (a byte-array) of
     size [siz], contained in an enclosing allocation-block starting at [bas]

sledge/src/sh_test.ml

@@ -5,7 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Ses
+open Fol
 
 let%test_module _ =
   ( module struct

sledge/src/solver.ml

@@ -7,7 +7,7 @@
 
 (** Frame Inference Solver over Symbolic Heaps *)
 
-open Ses
+open Fol
 
 module Goal : sig
   (** Excision judgment

sledge/src/solver.mli

@@ -7,7 +7,7 @@
 
 (** Frame Inference Solver over Symbolic Heaps *)
 
-open Ses
+open Fol
 
 val infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option
 (** If [infer_frame p xs q] is [Some r], then [p ⊢ ∃xs. q * r]. The

sledge/src/solver_test.ml

@@ -5,7 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Ses
+open Fol
 
 let%test_module _ =
   ( module struct