From ca67dfb80178c71371706d4840320ba7fb8870e8 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 4 Nov 2020 02:07:42 -0800
Subject: [PATCH] [sledge] Reorganize first-order logic support into separate
 library

Reviewed By: jvillard

Differential Revision: D24549076

fbshipit-source-id: fcd231ab1
---
 sledge/dune                                |  8 ++++----
 sledge/src/{ => fol}/arithmetic.ml         |  2 +-
 sledge/src/{ => fol}/arithmetic.mli        |  2 +-
 sledge/src/{ => fol}/arithmetic_intf.ml    |  4 ++--
 sledge/src/{ => fol}/context.ml            |  2 +-
 sledge/src/{ => fol}/context.mli           |  2 +-
 sledge/src/{fol.ml => fol/exp.ml}          |  0
 sledge/src/{fol.mli => fol/exp.mli}        |  4 ++--
 sledge/src/{ => fol}/fml.ml                |  2 +-
 sledge/src/{ => fol}/fml.mli               |  4 ++--
 sledge/src/fol/fol.ml                      | 19 +++++++++++++++++++
 sledge/src/fol/fol.mli                     | 19 +++++++++++++++++++
 sledge/src/{ses => fol}/funsym.ml          |  0
 sledge/src/{ses => fol}/funsym.mli         |  0
 sledge/src/{ses => fol}/predsym.ml         |  0
 sledge/src/{ses => fol}/predsym.mli        |  0
 sledge/src/{ => fol}/propositional.ml      |  2 +-
 sledge/src/{ => fol}/propositional.mli     |  0
 sledge/src/{ => fol}/propositional_intf.ml |  4 ++--
 sledge/src/{ => fol}/trm.ml                |  6 ++----
 sledge/src/{ => fol}/trm.mli               |  6 +++---
 sledge/src/{ => fol}/var.ml                |  0
 sledge/src/{ => fol}/var.mli               |  0
 sledge/src/{ses => fol}/var0.ml            |  0
 sledge/src/{ses => fol}/var0.mli           |  0
 sledge/src/{ses => fol}/var_intf.ml        |  0
 sledge/src/llair_to_Fol.ml                 |  2 --
 sledge/src/solver.mli                      |  2 ++
 sledge/src/test/context_test.ml            |  1 -
 sledge/src/test/term_test.ml               |  1 -
 30 files changed, 63 insertions(+), 29 deletions(-)
 rename sledge/src/{ => fol}/arithmetic.ml (99%)
 rename sledge/src/{ => fol}/arithmetic.mli (95%)
 rename sledge/src/{ => fol}/arithmetic_intf.ml (97%)
 rename sledge/src/{ => fol}/context.ml (99%)
 rename sledge/src/{ => fol}/context.mli (99%)
 rename sledge/src/{fol.ml => fol/exp.ml} (100%)
 rename sledge/src/{fol.mli => fol/exp.mli} (97%)
 rename sledge/src/{ => fol}/fml.ml (98%)
 rename sledge/src/{ => fol}/fml.mli (95%)
 create mode 100644 sledge/src/fol/fol.ml
 create mode 100644 sledge/src/fol/fol.mli
 rename sledge/src/{ses => fol}/funsym.ml (100%)
 rename sledge/src/{ses => fol}/funsym.mli (100%)
 rename sledge/src/{ses => fol}/predsym.ml (100%)
 rename sledge/src/{ses => fol}/predsym.mli (100%)
 rename sledge/src/{ => fol}/propositional.ml (99%)
 rename sledge/src/{ => fol}/propositional.mli (100%)
 rename sledge/src/{ => fol}/propositional_intf.ml (95%)
 rename sledge/src/{ => fol}/trm.ml (99%)
 rename sledge/src/{ => fol}/trm.mli (93%)
 rename sledge/src/{ => fol}/var.ml (100%)
 rename sledge/src/{ => fol}/var.mli (100%)
 rename sledge/src/{ses => fol}/var0.ml (100%)
 rename sledge/src/{ses => fol}/var0.mli (100%)
 rename sledge/src/{ses => fol}/var_intf.ml (100%)

diff --git a/sledge/dune b/sledge/dune
index 3c1341cc5..26fe42609 100644
--- a/sledge/dune
+++ b/sledge/dune
@@ -46,10 +46,10 @@
   (inline_tests)))
 
 (subdir
- src/ses
+ src/fol
  (library
-  (name ses)
-  (public_name sledge.ses)
+  (name fol)
+  (public_name sledge.fol)
   (libraries nonstdlib llair)
   (flags
    (:standard -open NS))
@@ -62,7 +62,7 @@
  (library
   (name sledge)
   (public_name sledge)
-  (libraries mtime mtime.clock.os nonstdlib llair ses)
+  (libraries mtime mtime.clock.os nonstdlib llair fol)
   (flags
    (:standard -open NS))
   (preprocess
diff --git a/sledge/src/arithmetic.ml b/sledge/src/fol/arithmetic.ml
similarity index 99%
rename from sledge/src/arithmetic.ml
rename to sledge/src/fol/arithmetic.ml
index 6fca9c297..963a80985 100644
--- a/sledge/src/arithmetic.ml
+++ b/sledge/src/fol/arithmetic.ml
@@ -7,7 +7,7 @@
 
 (** Arithmetic terms *)
 
-open Ses.Var_intf
+open Var_intf
 include Arithmetic_intf
 
 module Representation
diff --git a/sledge/src/arithmetic.mli b/sledge/src/fol/arithmetic.mli
similarity index 95%
rename from sledge/src/arithmetic.mli
rename to sledge/src/fol/arithmetic.mli
index fdf3d92c1..58edc93e2 100644
--- a/sledge/src/arithmetic.mli
+++ b/sledge/src/fol/arithmetic.mli
@@ -7,7 +7,7 @@
 
 (** Arithmetic terms *)
 
-open Ses.Var_intf
+open Var_intf
 include module type of Arithmetic_intf
 
 module Representation
diff --git a/sledge/src/arithmetic_intf.ml b/sledge/src/fol/arithmetic_intf.ml
similarity index 97%
rename from sledge/src/arithmetic_intf.ml
rename to sledge/src/fol/arithmetic_intf.ml
index e066d12b8..d0592c73c 100644
--- a/sledge/src/arithmetic_intf.ml
+++ b/sledge/src/fol/arithmetic_intf.ml
@@ -12,7 +12,7 @@ module type S = sig
   type trm
   type t [@@deriving compare, equal, sexp]
 
-  val ppx : var Ses.Var_intf.strength -> t pp
+  val ppx : var Var_intf.strength -> t pp
 
   (** Construct and Destruct atomic terms *)
 
@@ -87,7 +87,7 @@ module type INDETERMINATE = sig
   type trm [@@deriving compare, equal, sexp]
   type var
 
-  val ppx : var Ses.Var_intf.strength -> trm pp
+  val ppx : var Var_intf.strength -> trm pp
   val pp : trm pp
   val vars : trm -> var iter
 end
diff --git a/sledge/src/context.ml b/sledge/src/fol/context.ml
similarity index 99%
rename from sledge/src/context.ml
rename to sledge/src/fol/context.ml
index 83bfa2599..33e8db10b 100644
--- a/sledge/src/context.ml
+++ b/sledge/src/fol/context.ml
@@ -7,7 +7,7 @@
 
 (** Equality over uninterpreted functions and linear rational arithmetic *)
 
-open Fol
+open Exp
 
 (** Classification of Terms by Theory *)
 
diff --git a/sledge/src/context.mli b/sledge/src/fol/context.mli
similarity index 99%
rename from sledge/src/context.mli
rename to sledge/src/fol/context.mli
index 2e43b118d..c646a9eb2 100644
--- a/sledge/src/context.mli
+++ b/sledge/src/fol/context.mli
@@ -13,7 +13,7 @@
     the variables with which any generated variables must be chosen fresh,
     and the output set is the variables that have been generated. *)
 
-open Fol
+open Exp
 
 type t [@@deriving sexp]
 
diff --git a/sledge/src/fol.ml b/sledge/src/fol/exp.ml
similarity index 100%
rename from sledge/src/fol.ml
rename to sledge/src/fol/exp.ml
diff --git a/sledge/src/fol.mli b/sledge/src/fol/exp.mli
similarity index 97%
rename from sledge/src/fol.mli
rename to sledge/src/fol/exp.mli
index 120a11e98..9ff78caed 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol/exp.mli
@@ -46,7 +46,7 @@ module rec Term : sig
   val ancestor : int -> t
 
   (* uninterpreted *)
-  val apply : Ses.Funsym.t -> t array -> t
+  val apply : Funsym.t -> t array -> t
 
   (* if-then-else *)
   val ite : cnd:Formula.t -> thn:t -> els:t -> t
@@ -114,7 +114,7 @@ and Formula : sig
   val le : Term.t -> Term.t -> t
 
   (* uninterpreted *)
-  val lit : Ses.Predsym.t -> Term.t array -> t
+  val lit : Predsym.t -> Term.t array -> t
 
   (* connectives *)
   val not_ : t -> t
diff --git a/sledge/src/fml.ml b/sledge/src/fol/fml.ml
similarity index 98%
rename from sledge/src/fml.ml
rename to sledge/src/fol/fml.ml
index 2b49425de..fe84fff36 100644
--- a/sledge/src/fml.ml
+++ b/sledge/src/fol/fml.ml
@@ -65,7 +65,7 @@ let ppx strength fs fml =
     | Iff (x, y) -> pf "(%a@ <=> %a)" pp x pp y
     | Cond {cnd; pos; neg} ->
         pf "@[<hv 1>(%a@ ? %a@ : %a)@]" pp cnd pp pos pp neg
-    | Lit (p, xs) -> pf "%a(%a)" Ses.Predsym.pp p (Array.pp ",@ " pp_t) xs
+    | Lit (p, xs) -> pf "%a(%a)" Predsym.pp p (Array.pp ",@ " pp_t) xs
   in
   pp fs fml
 
diff --git a/sledge/src/fml.mli b/sledge/src/fol/fml.mli
similarity index 95%
rename from sledge/src/fml.mli
rename to sledge/src/fol/fml.mli
index 2099a6bea..d5f85d345 100644
--- a/sledge/src/fml.mli
+++ b/sledge/src/fol/fml.mli
@@ -24,7 +24,7 @@ type t = private
   | Iff of t * t
   | Cond of {cnd: t; pos: t; neg: t}
   (* uninterpreted *)
-  | Lit of Ses.Predsym.t * Trm.t array
+  | Lit of Predsym.t * Trm.t array
 [@@deriving compare, equal, sexp]
 
 module Set : sig
@@ -60,7 +60,7 @@ val iff : t -> t -> t
 val cond : cnd:t -> pos:t -> neg:t -> t
 
 (* uninterpreted *)
-val lit : Ses.Predsym.t -> Trm.t array -> t
+val lit : Predsym.t -> Trm.t array -> t
 
 (** Transform *)
 
diff --git a/sledge/src/fol/fol.ml b/sledge/src/fol/fol.ml
new file mode 100644
index 000000000..0fe7e6263
--- /dev/null
+++ b/sledge/src/fol/fol.ml
@@ -0,0 +1,19 @@
+(*
+ * 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.
+ *)
+
+(** First-Order Logic *)
+
+module Funsym = Funsym
+module Predsym = Predsym
+module Var = Var
+module Term = Exp.Term
+module Formula = Exp.Formula
+module Context = Context
+
+(**/**)
+
+module Trm = Trm
diff --git a/sledge/src/fol/fol.mli b/sledge/src/fol/fol.mli
new file mode 100644
index 000000000..0fe7e6263
--- /dev/null
+++ b/sledge/src/fol/fol.mli
@@ -0,0 +1,19 @@
+(*
+ * 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.
+ *)
+
+(** First-Order Logic *)
+
+module Funsym = Funsym
+module Predsym = Predsym
+module Var = Var
+module Term = Exp.Term
+module Formula = Exp.Formula
+module Context = Context
+
+(**/**)
+
+module Trm = Trm
diff --git a/sledge/src/ses/funsym.ml b/sledge/src/fol/funsym.ml
similarity index 100%
rename from sledge/src/ses/funsym.ml
rename to sledge/src/fol/funsym.ml
diff --git a/sledge/src/ses/funsym.mli b/sledge/src/fol/funsym.mli
similarity index 100%
rename from sledge/src/ses/funsym.mli
rename to sledge/src/fol/funsym.mli
diff --git a/sledge/src/ses/predsym.ml b/sledge/src/fol/predsym.ml
similarity index 100%
rename from sledge/src/ses/predsym.ml
rename to sledge/src/fol/predsym.ml
diff --git a/sledge/src/ses/predsym.mli b/sledge/src/fol/predsym.mli
similarity index 100%
rename from sledge/src/ses/predsym.mli
rename to sledge/src/fol/predsym.mli
diff --git a/sledge/src/propositional.ml b/sledge/src/fol/propositional.ml
similarity index 99%
rename from sledge/src/propositional.ml
rename to sledge/src/fol/propositional.ml
index 48c562035..082ab02d4 100644
--- a/sledge/src/propositional.ml
+++ b/sledge/src/fol/propositional.ml
@@ -35,7 +35,7 @@ module Make (Trm : TERM) = struct
       | Or of {pos: Fmls.t; neg: Fmls.t}
       | Iff of t * t
       | Cond of {cnd: t; pos: t; neg: t}
-      | Lit of Ses.Predsym.t * Trm.t array
+      | Lit of Predsym.t * Trm.t array
     [@@deriving compare, equal, sexp]
 
     let invariant f =
diff --git a/sledge/src/propositional.mli b/sledge/src/fol/propositional.mli
similarity index 100%
rename from sledge/src/propositional.mli
rename to sledge/src/fol/propositional.mli
diff --git a/sledge/src/propositional_intf.ml b/sledge/src/fol/propositional_intf.ml
similarity index 95%
rename from sledge/src/propositional_intf.ml
rename to sledge/src/fol/propositional_intf.ml
index 361f8b73d..4e9d8d9b3 100644
--- a/sledge/src/propositional_intf.ml
+++ b/sledge/src/fol/propositional_intf.ml
@@ -33,7 +33,7 @@ module type FORMULA = sig
     | Iff of t * t
     | Cond of {cnd: t; pos: t; neg: t}
     (* uninterpreted literals *)
-    | Lit of Ses.Predsym.t * trm array
+    | Lit of Predsym.t * trm array
   [@@deriving compare, equal, sexp]
 
   val mk_Tt : unit -> t
@@ -45,7 +45,7 @@ module type FORMULA = sig
   val _Or : pos:set -> neg:set -> t
   val _Iff : t -> t -> t
   val _Cond : t -> t -> t -> t
-  val _Lit : Ses.Predsym.t -> trm array -> t
+  val _Lit : Predsym.t -> trm array -> t
   val and_ : t -> t -> t
   val or_ : t -> t -> t
   val is_negative : t -> bool
diff --git a/sledge/src/trm.ml b/sledge/src/fol/trm.ml
similarity index 99%
rename from sledge/src/trm.ml
rename to sledge/src/fol/trm.ml
index 00405165c..8dcd25697 100644
--- a/sledge/src/trm.ml
+++ b/sledge/src/fol/trm.ml
@@ -7,15 +7,13 @@
 
 (** Terms *)
 
-module Funsym = Ses.Funsym
-
 let pp_boxed fs fmt =
   Format.pp_open_box fs 2 ;
   Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
 
 (** Variable terms, represented as a subtype of general terms *)
 module rec Var : sig
-  include Ses.Var_intf.VAR with type t = private Trm.t
+  include Var_intf.VAR with type t = private Trm.t
 
   val of_ : Trm.t -> t
   val of_trm : Trm.t -> t option
@@ -34,7 +32,7 @@ end = struct
     let name = function Trm.Var v -> v.name | x -> violates invariant x
   end
 
-  include Ses.Var0.Make (T)
+  include Var0.Make (T)
 
   let of_ v = v |> check T.invariant
   let of_trm = function Trm.Var _ as v -> Some v | _ -> None
diff --git a/sledge/src/trm.mli b/sledge/src/fol/trm.mli
similarity index 93%
rename from sledge/src/trm.mli
rename to sledge/src/fol/trm.mli
index a7229fc2d..71a54ec04 100644
--- a/sledge/src/trm.mli
+++ b/sledge/src/fol/trm.mli
@@ -27,13 +27,13 @@ type t = private
   | Record of t array
   | Ancestor of int
   (* uninterpreted *)
-  | Apply of Ses.Funsym.t * t array
+  | Apply of Funsym.t * t array
 [@@deriving compare, equal, sexp]
 
 module Var : sig
   type trm := t
 
-  include Ses.Var_intf.VAR with type t = private trm
+  include Var_intf.VAR with type t = private trm
 
   val of_ : trm -> t
   val of_trm : trm -> t option
@@ -84,7 +84,7 @@ val record : t array -> t
 val ancestor : int -> t
 
 (* uninterpreted *)
-val apply : Ses.Funsym.t -> t array -> t
+val apply : Funsym.t -> t array -> t
 
 (** Transform *)
 
diff --git a/sledge/src/var.ml b/sledge/src/fol/var.ml
similarity index 100%
rename from sledge/src/var.ml
rename to sledge/src/fol/var.ml
diff --git a/sledge/src/var.mli b/sledge/src/fol/var.mli
similarity index 100%
rename from sledge/src/var.mli
rename to sledge/src/fol/var.mli
diff --git a/sledge/src/ses/var0.ml b/sledge/src/fol/var0.ml
similarity index 100%
rename from sledge/src/ses/var0.ml
rename to sledge/src/fol/var0.ml
diff --git a/sledge/src/ses/var0.mli b/sledge/src/fol/var0.mli
similarity index 100%
rename from sledge/src/ses/var0.mli
rename to sledge/src/fol/var0.mli
diff --git a/sledge/src/ses/var_intf.ml b/sledge/src/fol/var_intf.ml
similarity index 100%
rename from sledge/src/ses/var_intf.ml
rename to sledge/src/fol/var_intf.ml
diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml
index 6518400ac..ba91b2f73 100644
--- a/sledge/src/llair_to_Fol.ml
+++ b/sledge/src/llair_to_Fol.ml
@@ -6,8 +6,6 @@
  *)
 
 open Fol
-module Funsym = Ses.Funsym
-module Predsym = Ses.Predsym
 module T = Term
 module F = Formula
 
diff --git a/sledge/src/solver.mli b/sledge/src/solver.mli
index 3a84142aa..ae6ae86ca 100644
--- a/sledge/src/solver.mli
+++ b/sledge/src/solver.mli
@@ -7,6 +7,8 @@
 
 (** Frame Inference Solver over Symbolic Heaps *)
 
+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
     vocabulary of [r] is the vocabulary of [q] union [xs]. A goal is for [r]
diff --git a/sledge/src/test/context_test.ml b/sledge/src/test/context_test.ml
index 5afd36141..109f44aeb 100644
--- a/sledge/src/test/context_test.ml
+++ b/sledge/src/test/context_test.ml
@@ -5,7 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Sledge
 open Fol
 
 let%test_module _ =
diff --git a/sledge/src/test/term_test.ml b/sledge/src/test/term_test.ml
index ea76d9cdb..9dbeebc1c 100644
--- a/sledge/src/test/term_test.ml
+++ b/sledge/src/test/term_test.ml
@@ -5,7 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Sledge
 open Fol
 module T = Term
 module F = Formula