[sledge] Reorganize first-order logic support into separate library

Reviewed By: jvillard

Differential Revision: D24549076

fbshipit-source-id: fcd231ab1

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

sledge/src/fol/arithmetic.ml

@@ -7,7 +7,7 @@
 
 (** Arithmetic terms *)
 
-open Ses.Var_intf
+open Var_intf
 include Arithmetic_intf
 
 module Representation

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

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

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 *)
 

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]
 

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

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
 

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 *)
 

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

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

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 =

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

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

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 *)
 

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
 

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]

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 _ =

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