From 0568f2ee2d134a89f334706c0e7a689f70fdfc59 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 9 Jul 2020 07:43:53 -0700
Subject: [PATCH] [sledge] Refactor: Distinguish Fol term and formula types

Reviewed By: ngorogiannis

Differential Revision: D22170516

fbshipit-source-id: e593123ce
---
 sledge/src/domain_sh.ml   |   6 +-
 sledge/src/exec.ml        |  85 ++++++++++++-------------
 sledge/src/exec.mli       |   2 +-
 sledge/src/fol.ml         |  27 ++++++--
 sledge/src/fol.mli        | 128 ++++++++++++++++++++++----------------
 sledge/src/sh.ml          |  65 ++++++++++---------
 sledge/src/sh.mli         |   8 +--
 sledge/src/sh_test.ml     |  12 ++--
 sledge/src/solver.ml      |  59 +++++++++---------
 sledge/src/solver_test.ml |  12 ++--
 10 files changed, 223 insertions(+), 181 deletions(-)

diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index d1f2c8bb7..3ff4c1123 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -38,7 +38,7 @@ let is_false = Sh.is_false
 let dnf = Sh.dnf
 
 let exec_assume q b =
-  Exec.assume q (Term.of_exp b) |> Option.map ~f:simplify
+  Exec.assume q (Formula.of_exp b) |> Option.map ~f:simplify
 
 let exec_kill q r = Exec.kill q (Var.of_reg r) |> simplify
 
@@ -122,7 +122,7 @@ let garbage_collect (q : t) ~wrt =
 let and_eqs sub formals actuals q =
   let and_eq q formal actual =
     let actual' = Term.rename sub actual in
-    Sh.and_ (Term.eq (Term.var formal) actual') q
+    Sh.and_ (Formula.eq (Term.var formal) actual') q
   in
   List.fold2_exn ~f:and_eq formals actuals ~init:q
 
@@ -277,7 +277,7 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
     Var.Set.fold formals ~init:q ~f:(fun q var ->
         let var = Term.var var in
         let renamed_var = Term.rename subst var in
-        Sh.and_ (Term.eq renamed_var var) q )
+        Sh.and_ (Formula.eq renamed_var var) q )
   in
   (* Add back the original formals name *)
   let post = Sh.rename subst post in
diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index f98a95bd0..e6d32a52a 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -87,12 +87,11 @@ let gen_spec us specm =
  * Instruction small axioms
  *)
 
-let null_eq ptr = Sh.pure (Term.eq Term.zero ptr)
+let null_eq ptr = Sh.pure (Formula.eq Term.zero ptr)
 
 let eq_concat (siz, seq) ms =
-  Term.(
-    eq (sized ~siz ~seq)
-      (concat (Array.map ~f:(fun (siz, seq) -> sized ~siz ~seq) ms)))
+  Formula.eq (Term.sized ~siz ~seq)
+    (Term.concat (Array.map ~f:(fun (siz, seq) -> Term.sized ~siz ~seq) ms))
 
 open Fresh.Import
 
@@ -110,7 +109,7 @@ let move_spec reg_exps =
   let+ sub, ms = Fresh.assign ~ws ~rs in
   let post =
     IArray.fold reg_exps ~init:Sh.emp ~f:(fun post (reg, exp) ->
-        Sh.and_ (Term.eq (Term.var reg) (Term.rename sub exp)) post )
+        Sh.and_ (Formula.eq (Term.var reg) (Term.rename sub exp)) post )
   in
   {foot; sub; ms; post}
 
@@ -124,7 +123,7 @@ let load_spec reg ptr len =
   let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
   let post =
     Sh.and_
-      (Term.eq (Term.var reg) (Term.rename sub seg.seq))
+      (Formula.eq (Term.var reg) (Term.rename sub seg.seq))
       (Sh.rename sub foot)
   in
   {foot; sub; ms; post}
@@ -157,7 +156,8 @@ let memcpy_eq_spec dst src len =
   let+ seg = Fresh.seg dst ~len in
   let dst_heap = Sh.seg seg in
   let foot =
-    Sh.and_ (Term.eq dst src) (Sh.and_ (Term.eq len Term.zero) dst_heap)
+    Sh.and_ (Formula.eq dst src)
+      (Sh.and_ (Formula.eq len Term.zero) dst_heap)
   in
   let post = dst_heap in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@@ -187,7 +187,7 @@ let memcpy_specs dst src len =
 let memmov_eq_spec dst src len =
   let+ dst_seg = Fresh.seg dst ~len in
   let dst_heap = Sh.seg dst_seg in
-  let foot = Sh.and_ (Term.eq dst src) dst_heap in
+  let foot = Sh.and_ (Formula.eq dst src) dst_heap in
   let post = dst_heap in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -221,8 +221,8 @@ let memmov_foot dst src len =
   in
   let foot =
     Sh.and_ eq_mem_dst_mid_src
-      (Sh.and_ (Term.lt dst src)
-         (Sh.and_ (Term.lt src (Term.add dst len)) seg))
+      (Sh.and_ (Formula.lt dst src)
+         (Sh.and_ (Formula.lt src (Term.add dst len)) seg))
   in
   (bas, siz, mem_dst, mem_mid, mem_src, foot)
 
@@ -336,7 +336,7 @@ let malloc_spec reg siz =
  * { r=0 ∨ ∃α'. r-[r;sΘ)->⟨sΘ,α'⟩ }
  *)
 let mallocx_spec reg siz =
-  let foot = Sh.pure (Term.dq siz Term.zero) in
+  let foot = Sh.pure (Formula.dq siz Term.zero) in
   let* sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:(Term.fv siz) in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
@@ -381,9 +381,9 @@ let posix_memalign_spec reg ptr siz =
   let enomem = Term.integer (Z.of_int 12) in
   let post =
     Sh.or_
-      (Sh.and_ (Term.eq (Term.var reg) enomem) (Sh.rename sub foot))
+      (Sh.and_ (Formula.eq (Term.var reg) enomem) (Sh.rename sub foot))
       (Sh.and_
-         (Term.eq (Term.var reg) eok)
+         (Formula.eq (Term.var reg) eok)
          (Sh.rename sub (Sh.star (Sh.seg pseg') (Sh.seg qseg))))
   in
   {foot; sub; ms; post}
@@ -410,12 +410,11 @@ let realloc_spec reg ptr siz =
   let+ a2 = Fresh.var "a" in
   let post =
     Sh.or_
-      (Sh.and_ Term.(eq loc zero) (Sh.rename sub foot))
+      (Sh.and_ (Formula.eq loc Term.zero) (Sh.rename sub foot))
       (Sh.and_
-         Term.(
-           conditional ~cnd:(le len siz)
-             ~thn:(eq_concat (siz, a1) [|(len, a0); (sub siz len, a2)|])
-             ~els:(eq_concat (len, a0) [|(siz, a1); (sub len siz, a2)|]))
+         (Formula.conditional ~cnd:(Formula.le len siz)
+            ~thn:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
+            ~els:(eq_concat (len, a0) [|(siz, a1); (Term.sub len siz, a2)|]))
          (Sh.seg rseg))
   in
   {foot; sub; ms; post}
@@ -430,7 +429,7 @@ let rallocx_spec reg ptr siz =
   let* len = Fresh.var "m" in
   let* pseg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in
   let pheap = Sh.seg pseg in
-  let foot = Sh.and_ (Term.dq siz Term.zero) pheap in
+  let foot = Sh.and_ (Formula.dq siz Term.zero) pheap in
   let* sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
@@ -440,12 +439,11 @@ let rallocx_spec reg ptr siz =
   let+ a2 = Fresh.var "a" in
   let post =
     Sh.or_
-      (Sh.and_ Term.(eq loc zero) (Sh.rename sub pheap))
+      (Sh.and_ (Formula.eq loc Term.zero) (Sh.rename sub pheap))
       (Sh.and_
-         Term.(
-           conditional ~cnd:(le len siz)
-             ~thn:(eq_concat (siz, a1) [|(len, a0); (sub siz len, a2)|])
-             ~els:(eq_concat (len, a0) [|(siz, a1); (sub len siz, a2)|]))
+         (Formula.conditional ~cnd:(Formula.le len siz)
+            ~thn:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
+            ~els:(eq_concat (len, a0) [|(siz, a1); (Term.sub len siz, a2)|]))
          (Sh.seg rseg))
   in
   {foot; sub; ms; post}
@@ -458,7 +456,7 @@ let rallocx_spec reg ptr siz =
 let xallocx_spec reg ptr siz ext =
   let* len = Fresh.var "m" in
   let* seg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in
-  let foot = Sh.and_ (Term.dq siz Term.zero) (Sh.seg seg) in
+  let foot = Sh.and_ (Formula.dq siz Term.zero) (Sh.seg seg) in
   let* sub, ms =
     Fresh.assign ~ws:(Var.Set.of_ reg)
       ~rs:Var.Set.(union foot.us (union (Term.fv siz) (Term.fv ext)))
@@ -473,12 +471,12 @@ let xallocx_spec reg ptr siz ext =
   let+ a2 = Fresh.var "a" in
   let post =
     Sh.and_
-      Term.(
-        and_
-          (conditional ~cnd:(le len siz)
-             ~thn:(eq_concat (siz, a1) [|(len, a0); (sub siz len, a2)|])
-             ~els:(eq_concat (len, a0) [|(siz, a1); (sub len siz, a2)|]))
-          (and_ (le siz reg) (le reg (add siz ext))))
+      (Formula.and_
+         (Formula.conditional ~cnd:(Formula.le len siz)
+            ~thn:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
+            ~els:(eq_concat (len, a0) [|(siz, a1); (Term.sub len siz, a2)|]))
+         (Formula.and_ (Formula.le siz reg)
+            (Formula.le reg (Term.add siz ext))))
       (Sh.seg seg')
   in
   {foot; sub; ms; post}
@@ -492,7 +490,7 @@ let sallocx_spec reg ptr =
   let* seg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in
   let foot = Sh.seg seg in
   let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
-  let post = Sh.and_ (Term.eq (Term.var reg) len) (Sh.rename sub foot) in
+  let post = Sh.and_ (Formula.eq (Term.var reg) len) (Sh.rename sub foot) in
   {foot; sub; ms; post}
 
 (* { p-[p;m)->⟨m,α⟩ }
@@ -504,7 +502,7 @@ let malloc_usable_size_spec reg ptr =
   let* seg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in
   let foot = Sh.seg seg in
   let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
-  let post = Sh.and_ (Term.le len (Term.var reg)) (Sh.rename sub foot) in
+  let post = Sh.and_ (Formula.le len (Term.var reg)) (Sh.rename sub foot) in
   {foot; sub; ms; post}
 
 (* { s≠0 }
@@ -512,11 +510,11 @@ let malloc_usable_size_spec reg ptr =
  * { r=0 ∨ r=sΘ }
  *)
 let nallocx_spec reg siz =
-  let foot = Sh.pure (Term.dq siz Term.zero) in
+  let foot = Sh.pure (Formula.dq siz Term.zero) in
   let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
-  let post = Sh.or_ (null_eq loc) (Sh.pure (Term.eq loc siz)) in
+  let post = Sh.or_ (null_eq loc) (Sh.pure (Formula.eq loc siz)) in
   {foot; sub; ms; post}
 
 let size_of_int_mul = Term.mulq (Q.of_int Llair.Typ.(size_of siz))
@@ -530,9 +528,9 @@ let mallctl_read_spec r i w n =
   let* rseg = Fresh.seg r ~siz:iseg.seq in
   let+ a = Fresh.var "a" in
   let foot =
-    Sh.and_
-      Term.(eq w zero)
-      (Sh.and_ Term.(eq n zero) (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
+    Sh.and_ (Formula.eq w Term.zero)
+      (Sh.and_ (Formula.eq n Term.zero)
+         (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
   in
   let rseg' = {rseg with seq= a} in
   let post = Sh.star (Sh.seg rseg') (Sh.seg iseg) in
@@ -552,9 +550,8 @@ let mallctlbymib_read_spec p l r i w n =
   let const = Sh.star (Sh.seg pseg) (Sh.seg iseg) in
   let+ a = Fresh.var "a" in
   let foot =
-    Sh.and_
-      Term.(eq w zero)
-      (Sh.and_ Term.(eq n zero) (Sh.star const (Sh.seg rseg)))
+    Sh.and_ (Formula.eq w Term.zero)
+      (Sh.and_ (Formula.eq n Term.zero) (Sh.star const (Sh.seg rseg)))
   in
   let rseg' = {rseg with seq= a} in
   let post = Sh.star (Sh.seg rseg') const in
@@ -568,7 +565,7 @@ let mallctl_write_spec r i w n =
   let+ seg = Fresh.seg w ~siz:n in
   let post = Sh.seg seg in
   let foot =
-    Sh.and_ (Term.eq r Term.zero) (Sh.and_ (Term.eq i Term.zero) post)
+    Sh.and_ (Formula.eq r Term.zero) (Sh.and_ (Formula.eq i Term.zero) post)
   in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -583,7 +580,7 @@ let mallctlbymib_write_spec p l r i w n =
   let+ wseg = Fresh.seg w ~siz:n in
   let post = Sh.star (Sh.seg pseg) (Sh.seg wseg) in
   let foot =
-    Sh.and_ (Term.eq r Term.zero) (Sh.and_ (Term.eq i Term.zero) post)
+    Sh.and_ (Formula.eq r Term.zero) (Sh.and_ (Formula.eq i Term.zero) post)
   in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -630,7 +627,7 @@ let strlen_spec reg ptr =
   let ret = Term.sub (Term.sub (Term.add b m) p) Term.one in
   let post =
     Sh.and_
-      (Term.eq (Term.var reg) (Term.rename sub ret))
+      (Formula.eq (Term.var reg) (Term.rename sub ret))
       (Sh.rename sub foot)
   in
   {foot; sub; ms; post}
diff --git a/sledge/src/exec.mli b/sledge/src/exec.mli
index 4fef881c4..ff16c9ea5 100644
--- a/sledge/src/exec.mli
+++ b/sledge/src/exec.mli
@@ -9,7 +9,7 @@
 
 open Fol
 
-val assume : Sh.t -> Term.t -> Sh.t option
+val assume : Sh.t -> Formula.t -> Sh.t option
 val kill : Sh.t -> Var.t -> Sh.t
 val move : Sh.t -> (Var.t * Term.t) iarray -> Sh.t
 val load : Sh.t -> reg:Var.t -> ptr:Term.t -> len:Term.t -> Sh.t option
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 57ac50a13..679f90de3 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -10,10 +10,29 @@ module Var = Ses.Term.Var
 module Term = struct
   include Ses.Term
 
-  type term = t
-  type formula = t
-
   let ite = conditional
 end
 
-module Context = Ses.Equality
+module Formula = struct
+  include Ses.Term
+
+  let inject b = b
+  let project e = Some e
+
+  let of_exp e =
+    let b = Term.of_exp e in
+    match project b with Some p -> p | None -> dq Term.zero b
+end
+
+module Context = struct
+  include Ses.Equality
+
+  let and_formula = and_term
+  let normalizef = normalize
+
+  module Subst = struct
+    include Subst
+
+    let substf = subst
+  end
+end
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index b04f5cd9a..1d61add91 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -56,90 +56,110 @@ module Var : sig
 end
 
 (** Terms *)
-module Term : sig
-  type term
-  type formula = term
+module rec Term : sig
+  type t [@@deriving compare, equal, sexp]
 
-  val ppx : Var.strength -> term pp
-  val pp : term pp
+  (* pretty-printing *)
+  val ppx : Var.strength -> t pp
+  val pp : t pp
 
-  module Map : Map.S with type key := term
+  module Map : Map.S with type key := t
 
   (** Construct *)
 
-  (** terms *)
-
   (* variables *)
-  val var : Var.t -> term
+  val var : Var.t -> t
 
   (* constants *)
-  val zero : term
-  val one : term
-  val integer : Z.t -> term
-  val rational : Q.t -> term
+  val zero : t
+  val one : t
+  val integer : Z.t -> t
+  val rational : Q.t -> t
 
   (* arithmetic *)
-  val neg : term -> term
-  val add : term -> term -> term
-  val sub : term -> term -> term
-  val mulq : Q.t -> term -> term
-  val mul : term -> term -> term
+  val neg : t -> t
+  val add : t -> t -> t
+  val sub : t -> t -> t
+  val mulq : Q.t -> t -> t
+  val mul : t -> t -> t
 
   (* sequences *)
-  val splat : term -> term
-  val sized : seq:term -> siz:term -> term
-  val extract : seq:term -> off:term -> len:term -> term
-  val concat : term array -> term
+  val splat : t -> t
+  val sized : seq:t -> siz:t -> t
+  val extract : seq:t -> off:t -> len:t -> t
+  val concat : t array -> t
 
   (* if-then-else *)
-  val ite : cnd:formula -> thn:term -> els:term -> term
-
-  (** formulas *)
-
-  (* constants *)
-  val true_ : formula
-  val false_ : formula
-
-  (* comparisons *)
-  val eq : term -> term -> formula
-  val dq : term -> term -> formula
-  val lt : term -> term -> formula
-  val le : term -> term -> formula
-
-  (* connectives *)
-  val not_ : formula -> formula
-  val and_ : formula -> formula -> formula
-  val or_ : formula -> formula -> formula
-  val conditional : cnd:formula -> thn:formula -> els:formula -> formula
+  val ite : cnd:Formula.t -> thn:t -> els:t -> t
 
   (** Convert *)
 
-  val of_exp : Llair.Exp.t -> term
+  val of_exp : Llair.Exp.t -> t
 
   (** Destruct *)
 
-  val d_int : term -> Z.t option
+  val d_int : t -> Z.t option
 
   (** Access *)
 
-  val const_of : term -> Q.t option
+  val const_of : t -> Q.t option
 
   (** Transform *)
 
-  val disjuncts : term -> term list
-  val rename : Var.Subst.t -> term -> term
+  val rename : Var.Subst.t -> t -> t
 
   (** Traverse *)
 
-  val fold_vars : term -> init:'a -> f:('a -> Var.t -> 'a) -> 'a
+  val fold_vars : t -> init:'a -> f:('a -> Var.t -> 'a) -> 'a
 
   (** Query *)
 
-  val is_true : formula -> bool
-  val is_false : formula -> bool
-  val fv : term -> Var.Set.t
+  val fv : t -> Var.Set.t
+end
+
+(** Formulas *)
+and Formula : sig
+  type t [@@deriving compare, equal, sexp]
+
+  val inject : t -> Term.t
+  val project : Term.t -> t option
+
+  (* pretty-printing *)
+  val ppx : Var.strength -> t pp
+  val pp : t pp
+
+  (** Construct *)
+
+  (* constants *)
+  val true_ : t
+  val false_ : t
+
+  (* comparisons *)
+  val eq : Term.t -> Term.t -> t
+  val dq : Term.t -> Term.t -> t
+  val lt : Term.t -> Term.t -> t
+  val le : Term.t -> Term.t -> t
+
+  (* connectives *)
+  val not_ : t -> t
+  val and_ : t -> t -> t
+  val or_ : t -> t -> t
+  val conditional : cnd:t -> thn:t -> els:t -> t
+
+  (** Convert *)
+
+  val of_exp : Llair.Exp.t -> t
 
-  type t = term [@@deriving compare, equal, sexp]
+  (** Transform *)
+
+  val rename : Var.Subst.t -> t -> t
+  val disjuncts : t -> t list
+
+  (** Query *)
+
+  val is_true : t -> bool
+  val is_false : t -> bool
+  val fv : t -> Var.Set.t
 end
 
 (** Inference System *)
@@ -164,7 +184,7 @@ module Context : sig
   val true_ : t
   (** The diagonal relation, which only equates each term with itself. *)
 
-  val and_term : Var.Set.t -> Term.t -> t -> Var.Set.t * t
+  val and_formula : Var.Set.t -> Formula.t -> t -> Var.Set.t * t
   (** Conjoin a (Boolean) term to a relation. *)
 
   val and_ : Var.Set.t -> t -> t -> Var.Set.t * t
@@ -197,6 +217,8 @@ module Context : sig
       relation, where [e'] and its subterms are expressed in terms of the
       relation's canonical representatives of each equivalence class. *)
 
+  val normalizef : t -> Formula.t -> Formula.t
+
   val difference : t -> Term.t -> Term.t -> Z.t option
   (** The difference as an offset. [difference r a b = Some k] if [r]
       implies [a = b+k], or [None] if [a] and [b] are not equal up to an
@@ -217,6 +239,8 @@ 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 a6178b946..2afc46f4e 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -18,7 +18,7 @@ type starjunction =
   { us: Var.Set.t
   ; xs: Var.Set.t
   ; ctx: Context.t
-  ; pure: Term.t
+  ; pure: Formula.t
   ; heap: seg list
   ; djns: disjunction list }
 [@@deriving compare, equal, sexp]
@@ -33,7 +33,7 @@ let emp =
   { us= Var.Set.empty
   ; xs= Var.Set.empty
   ; ctx= Context.true_
-  ; pure= Term.true_
+  ; pure= Formula.true_
   ; heap= []
   ; djns= [] }
 
@@ -56,9 +56,10 @@ let map_seg ~f h =
   then h
   else {loc; bas; len; siz; seq}
 
-let map ~f_sjn ~f_ctx ~f_trm ({us; xs= _; ctx; pure; heap; djns} as q) =
-  let pure = f_trm pure in
-  if Term.is_false pure then false_ us
+let map ~f_sjn ~f_ctx ~f_trm ~f_fml ({us; xs= _; ctx; pure; heap; djns} as q)
+    =
+  let pure = f_fml pure in
+  if Formula.is_false pure then false_ us
   else
     let ctx = f_ctx ctx in
     let heap = List.map_endo heap ~f:(map_seg ~f:f_trm) in
@@ -78,7 +79,7 @@ let fold_vars_stem ?ignore_ctx {us= _; xs= _; ctx; pure; heap; djns= _}
     ~init ~f =
   List.fold ~init heap ~f:(fun init -> fold_vars_seg ~f ~init)
   |> fun init ->
-  Term.fold_vars ~f ~init pure
+  Term.fold_vars ~f ~init (Formula.inject pure)
   |> fun init ->
   if Option.is_some ignore_ctx then init
   else Context.fold_terms ~init ctx ~f:(fun init -> Term.fold_vars ~f ~init)
@@ -222,12 +223,12 @@ let rec pp_ ?var_strength vs parent_xs parent_ctx fs
   let pure =
     if Option.is_none var_strength then [pure]
     else
-      let pure' = Context.normalize ctx pure in
-      if Term.is_true pure' then [] else [pure']
+      let pure' = Context.normalizef ctx pure in
+      if Formula.is_true pure' then [] else [pure']
   in
   List.pp
     ~pre:(if first then "@[  " else "@ @[@<2>∧ ")
-    "@ @<2>∧ " (Term.ppx x) fs pure ~suf:"@]" ;
+    "@ @<2>∧ " (Formula.ppx x) fs pure ~suf:"@]" ;
   let first = first && List.is_empty pure in
   if List.is_empty heap then
     Format.fprintf fs
@@ -275,11 +276,7 @@ let fv ?ignore_ctx q =
   in
   fv_union Var.Set.empty q
 
-let invariant_pure b =
-  match Term.d_int b with
-  | Some data -> assert (not (Z.is_false data))
-  | _ -> assert true
-
+let invariant_pure p = assert (not (Formula.is_false p))
 let invariant_seg _ = ()
 
 let rec invariant q =
@@ -298,7 +295,7 @@ let rec invariant q =
     ( match djns with
     | [[]] ->
         assert (Context.is_true ctx) ;
-        assert (Term.is_true pure) ;
+        assert (Formula.is_true pure) ;
         assert (List.is_empty heap)
     | _ -> assert (not (Context.is_false ctx)) ) ;
     invariant_pure pure ;
@@ -318,7 +315,7 @@ let rec invariant q =
 let rec apply_subst sub q =
   map q ~f_sjn:(rename sub)
     ~f_ctx:(fun r -> Context.rename r sub)
-    ~f_trm:(Term.rename sub)
+    ~f_trm:(Term.rename sub) ~f_fml:(Formula.rename sub)
   |> check (fun q' ->
          assert (Var.Set.disjoint (fv q') (Var.Subst.domain sub)) )
 
@@ -456,11 +453,11 @@ let star q1 q2 =
   | {djns= [[]]; _}, _ | _, {djns= [[]]; _} ->
       false_ (Var.Set.union q1.us q2.us)
   | {us= _; xs= _; ctx; pure; heap= []; djns= []}, _
-    when Context.is_true ctx && Term.is_true pure ->
+    when Context.is_true ctx && Formula.is_true pure ->
       let us = Var.Set.union q1.us q2.us in
       if us == q2.us then q2 else {q2 with us}
   | _, {us= _; xs= _; ctx; pure; heap= []; djns= []}
-    when Context.is_true ctx && Term.is_true pure ->
+    when Context.is_true ctx && Formula.is_true pure ->
       let us = Var.Set.union q1.us q2.us in
       if us == q1.us then q1 else {q1 with us}
   | _ ->
@@ -479,7 +476,7 @@ let star q1 q2 =
           { us
           ; xs= Var.Set.union xs1 xs2
           ; ctx
-          ; pure= Term.and_ p1 p2
+          ; pure= Formula.and_ p1 p2
           ; heap= List.append h1 h2
           ; djns= List.append d1 d2 } )
   |>
@@ -501,17 +498,17 @@ let or_ q1 q2 =
   | _, {djns= [[]]; _} -> extend_us q2.us q1
   | ( ({djns= []; _} as q)
     , ({us= _; xs; ctx= _; pure; heap= []; djns= [djn]} as d) )
-    when Var.Set.is_empty xs && Term.is_true pure ->
+    when Var.Set.is_empty xs && Formula.is_true pure ->
       {d with us= Var.Set.union q.us d.us; djns= [q :: djn]}
   | ( ({us= _; xs; ctx= _; pure; heap= []; djns= [djn]} as d)
     , ({djns= []; _} as q) )
-    when Var.Set.is_empty xs && Term.is_true pure ->
+    when Var.Set.is_empty xs && Formula.is_true pure ->
       {d with us= Var.Set.union q.us d.us; djns= [q :: djn]}
   | _ ->
       { us= Var.Set.union q1.us q2.us
       ; xs= Var.Set.empty
       ; ctx= Context.true_
-      ; pure= Term.true_
+      ; pure= Formula.true_
       ; heap= []
       ; djns= [[q1; q2]] } )
   |>
@@ -525,14 +522,15 @@ let orN = function
   | [q] -> q
   | q :: qs -> List.fold ~f:or_ ~init:q qs
 
-let pure (e : Term.t) =
-  [%Trace.call fun {pf} -> pf "%a" Term.pp e]
+let pure (p : Formula.t) =
+  [%Trace.call fun {pf} -> pf "%a" Formula.pp p]
   ;
-  List.fold (Term.disjuncts e) ~init:(false_ Var.Set.empty) ~f:(fun q b ->
-      let us = Term.fv b in
-      let xs, ctx = Context.(and_term us b true_) in
+  List.fold (Formula.disjuncts p) ~init:(false_ Var.Set.empty)
+    ~f:(fun q p ->
+      let us = Formula.fv p in
+      let xs, ctx = Context.(and_formula us p true_) in
       if Context.is_false ctx then false_ us
-      else or_ q (exists_fresh xs {emp with us; ctx; pure= b}) )
+      else or_ q (exists_fresh xs {emp with us; ctx; pure= p}) )
   |>
   [%Trace.retn fun {pf} q ->
     pf "%a" pp q ;
@@ -544,7 +542,7 @@ let and_subst subst q =
   [%Trace.call fun {pf} -> pf "%a@ %a" Context.Subst.pp subst pp q]
   ;
   Context.Subst.fold
-    ~f:(fun ~key ~data -> and_ (Term.eq key data))
+    ~f:(fun ~key ~data -> and_ (Formula.eq key data))
     subst ~init:q
   |>
   [%Trace.retn fun {pf} q ->
@@ -555,10 +553,10 @@ let subst sub q =
   [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp q]
   ;
   let dom, eqs =
-    Var.Subst.fold sub ~init:(Var.Set.empty, Term.true_)
+    Var.Subst.fold sub ~init:(Var.Set.empty, Formula.true_)
       ~f:(fun var trm (dom, eqs) ->
         ( Var.Set.add dom var
-        , Term.and_ (Term.eq (Term.var var) (Term.var trm)) eqs ) )
+        , Formula.and_ (Formula.eq (Term.var var) (Term.var trm)) eqs ) )
   in
   exists dom (and_ eqs q)
   |>
@@ -585,13 +583,13 @@ let filter_heap ~f q =
 (** Query *)
 
 let is_emp = function
-  | {us= _; xs= _; ctx= _; pure; heap= []; djns= []} -> Term.is_true pure
+  | {us= _; xs= _; ctx= _; pure; heap= []; djns= []} -> Formula.is_true pure
   | _ -> false
 
 let is_false = function
   | {djns= [[]]; _} -> true
   | {ctx; pure; heap; _} ->
-      Term.is_false (Context.normalize ctx pure)
+      Formula.is_false (Context.normalizef ctx pure)
       || List.exists heap ~f:(fun seg ->
              Context.entails_eq ctx seg.loc Term.zero )
 
@@ -647,6 +645,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)
   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.mli b/sledge/src/sh.mli
index f96e54581..ad5dff26b 100644
--- a/sledge/src/sh.mli
+++ b/sledge/src/sh.mli
@@ -19,7 +19,7 @@ type starjunction = private
   ; xs: Var.Set.t  (** existentially-bound variables *)
   ; ctx: Context.t
         (** first-order logical context induced by rest of formula *)
-  ; pure: Term.t  (** pure boolean constraints *)
+  ; pure: Formula.t  (** pure boolean constraints *)
   ; heap: seg list  (** star-conjunction of segment atomic formulas *)
   ; djns: disjunction list  (** star-conjunction of disjunctions *) }
 
@@ -56,10 +56,10 @@ val or_ : t -> t -> t
 (** Disjoin formulas, extending to a common vocabulary, and avoiding
     capturing existentials. *)
 
-val pure : Term.t -> t
+val pure : Formula.t -> t
 (** Atomic pure boolean constraint formula. *)
 
-val and_ : Term.t -> t -> t
+val and_ : Formula.t -> t -> t
 (** Conjoin a boolean constraint to a formula. *)
 
 val and_ctx : Context.t -> t -> t
@@ -72,7 +72,7 @@ val and_subst : Context.Subst.t -> t -> t
 
 (** Update *)
 
-val with_pure : Term.t -> t -> t
+val with_pure : Formula.t -> t -> t
 (** [with_pure pure q] is [{q with pure}], which assumes that [q.pure] and
     [pure] are defined in the same vocabulary. Note that [ctx] is not
     weakened, so if [pure] and [q.pure] do not induce the same context, then
diff --git a/sledge/src/sh_test.ml b/sledge/src/sh_test.ml
index d421462a2..1c8a66eda 100644
--- a/sledge/src/sh_test.ml
+++ b/sledge/src/sh_test.ml
@@ -24,7 +24,7 @@ let%test_module _ =
     let ( ~$ ) = Var.Set.of_list
     let ( ! ) i = Term.integer (Z.of_int i)
     let ( - ) = Term.sub
-    let ( = ) = Term.eq
+    let ( = ) = Formula.eq
     let f = Term.splat (* any uninterpreted function *)
 
     let wrt = Var.Set.empty
@@ -45,12 +45,12 @@ let%test_module _ =
     let y = Term.var y_
 
     let eq_concat (siz, seq) ms =
-      Term.(
-        eq (sized ~siz ~seq)
-          (concat (Array.map ~f:(fun (siz, seq) -> sized ~siz ~seq) ms)))
+      Formula.eq (Term.sized ~siz ~seq)
+        (Term.concat
+           (Array.map ~f:(fun (siz, seq) -> Term.sized ~siz ~seq) ms))
 
     let of_eqs l =
-      List.fold ~init:emp ~f:(fun q (a, b) -> and_ (Term.eq a b) q) l
+      List.fold ~init:emp ~f:(fun q (a, b) -> and_ (Formula.eq a b) q) l
 
     let%expect_test _ =
       let p = exists ~$[x_] (extend_us ~$[x_] emp) in
@@ -160,7 +160,7 @@ let%test_module _ =
           (star
              (pure (eq_concat (!16, e) [|(!8, a); (!8, d)|]))
              (or_
-                (pure (Term.dq x !0))
+                (pure (Formula.dq x !0))
                 (exists
                    (Var.Set.of_list [b_])
                    (pure (eq_concat (!8, a) [|(!4, c); (!4, b)|])))))
diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml
index 9b6752e8f..6d38ea570 100644
--- a/sledge/src/solver.ml
+++ b/sledge/src/solver.ml
@@ -134,9 +134,8 @@ end
 open Goal
 
 let eq_concat (siz, seq) ms =
-  Term.(
-    eq (sized ~siz ~seq)
-      (concat (Array.map ~f:(fun (siz, seq) -> sized ~siz ~seq) ms)))
+  Formula.eq (Term.sized ~siz ~seq)
+    (Term.concat (Array.map ~f:(fun (siz, seq) -> Term.sized ~siz ~seq) ms))
 
 let fresh_var name vs zs ~wrt =
   let v, wrt = Var.fresh name ~wrt in
@@ -155,7 +154,7 @@ let excise_exists goal =
     let solutions_for_xs =
       let xs =
         Var.Set.diff goal.xs
-          (Sh.fv ~ignore_ctx:() (Sh.with_pure Term.true_ goal.sub))
+          (Sh.fv ~ignore_ctx:() (Sh.with_pure Formula.true_ goal.sub))
       in
       Context.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.ctx
     in
@@ -182,8 +181,8 @@ let excise_exists goal =
 
 let excise_pure ({min; sub} as goal) =
   trace (fun {pf} -> pf "@[<2>excise_pure@ %a@]" pp goal) ;
-  let pure' = Context.normalize min.ctx sub.pure in
-  if Term.is_false pure' then None
+  let pure' = Context.normalizef min.ctx sub.pure in
+  if Formula.is_false pure' then None
   else Some (goal |> with_ ~sub:(Sh.with_pure pure' sub))
 
 (*   [k; o)
@@ -208,8 +207,9 @@ let excise_seg_same ({com; min; sub} as goal) msg ssg =
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
   let sub =
-    Sh.and_ (Term.eq b b')
-      (Sh.and_ (Term.eq m m') (Sh.and_ (Term.eq a a') (Sh.rem_seg ssg sub)))
+    Sh.and_ (Formula.eq b b')
+      (Sh.and_ (Formula.eq m m')
+         (Sh.and_ (Formula.eq a a') (Sh.rem_seg ssg sub)))
   in
   goal |> with_ ~com ~min ~sub
 
@@ -246,9 +246,9 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
          (Sh.rem_seg msg min))
   in
   let sub =
-    Sh.and_ (Term.eq b b')
-      (Sh.and_ (Term.eq m m')
-         (Sh.and_ (Term.eq a0 a') (Sh.rem_seg ssg sub)))
+    Sh.and_ (Formula.eq b b')
+      (Sh.and_ (Formula.eq m m')
+         (Sh.and_ (Formula.eq a0 a') (Sh.rem_seg ssg sub)))
   in
   goal |> with_ ~us ~com ~min ~xs ~sub ~zs
 
@@ -278,8 +278,8 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
   let min = Sh.rem_seg msg min in
   let a1', xs, zs, _ = fresh_var "a1" xs zs ~wrt:(Var.Set.union us xs) in
   let sub =
-    Sh.and_ (Term.eq b b')
-      (Sh.and_ (Term.eq m m')
+    Sh.and_ (Formula.eq b b')
+      (Sh.and_ (Formula.eq m m')
          (Sh.and_
             (eq_concat (n, a') [|(o, a); (n_o, a1')|])
             (Sh.star
@@ -324,9 +324,9 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
          (Sh.rem_seg msg min))
   in
   let sub =
-    Sh.and_ (Term.eq b b')
-      (Sh.and_ (Term.eq m m')
-         (Sh.and_ (Term.eq a1 a') (Sh.rem_seg ssg sub)))
+    Sh.and_ (Formula.eq b b')
+      (Sh.and_ (Formula.eq m m')
+         (Sh.and_ (Formula.eq a1 a') (Sh.rem_seg ssg sub)))
   in
   goal |> with_ ~us ~com ~min ~xs ~sub ~zs
 
@@ -371,9 +371,9 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
             (Sh.rem_seg msg min)))
   in
   let sub =
-    Sh.and_ (Term.eq b b')
-      (Sh.and_ (Term.eq m m')
-         (Sh.and_ (Term.eq a1 a') (Sh.rem_seg ssg sub)))
+    Sh.and_ (Formula.eq b b')
+      (Sh.and_ (Formula.eq m m')
+         (Sh.and_ (Formula.eq a1 a') (Sh.rem_seg ssg sub)))
   in
   goal |> with_ ~us ~com ~min ~xs ~sub ~zs
 
@@ -417,8 +417,8 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
          (Sh.rem_seg msg min))
   in
   let sub =
-    Sh.and_ (Term.eq b b')
-      (Sh.and_ (Term.eq m m')
+    Sh.and_ (Formula.eq b b')
+      (Sh.and_ (Formula.eq m m')
          (Sh.and_
             (eq_concat (n, a') [|(ko_l, a1); (ln_ko, a2')|])
             (Sh.star
@@ -453,8 +453,8 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
   let sub =
-    Sh.and_ (Term.eq b b')
-      (Sh.and_ (Term.eq m m')
+    Sh.and_ (Formula.eq b b')
+      (Sh.and_ (Formula.eq m m')
          (Sh.and_
             (eq_concat (n, a') [|(k_l, a0'); (o, a)|])
             (Sh.star
@@ -493,8 +493,8 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
   let sub =
-    Sh.and_ (Term.eq b b')
-      (Sh.and_ (Term.eq m m')
+    Sh.and_ (Formula.eq b b')
+      (Sh.and_ (Formula.eq m m')
          (Sh.and_
             (eq_concat (n, a') [|(k_l, a0'); (o, a); (ln_ko, a2')|])
             (Sh.star
@@ -544,8 +544,8 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
          (Sh.rem_seg msg min))
   in
   let sub =
-    Sh.and_ (Term.eq b b')
-      (Sh.and_ (Term.eq m m')
+    Sh.and_ (Formula.eq b b')
+      (Sh.and_ (Formula.eq m m')
          (Sh.and_
             (eq_concat (n, a') [|(k_l, a0'); (ln_k, a1)|])
             (Sh.star
@@ -569,8 +569,9 @@ let excise_seg ({sub} as goal) msg ssg =
     Some
       ( goal
       |> with_
-           ~sub:(Sh.and_ (Term.eq b b') (Sh.and_ (Term.eq m m') goal.sub))
-      )
+           ~sub:
+             (Sh.and_ (Formula.eq b b')
+                (Sh.and_ (Formula.eq m m') goal.sub)) )
   else
     match Int.sign (Z.sign k_l) with
     (* k-l < 0 so k < l *)
diff --git a/sledge/src/solver_test.ml b/sledge/src/solver_test.ml
index db520f393..01b8eb039 100644
--- a/sledge/src/solver_test.ml
+++ b/sledge/src/solver_test.ml
@@ -69,7 +69,7 @@ let%test_module _ =
         ) infer_frame:   false |}]
 
     let%expect_test _ =
-      check_frame Sh.emp [n_; m_] (Sh.and_ (Term.eq m n) Sh.emp) ;
+      check_frame Sh.emp [n_; m_] (Sh.and_ (Formula.eq m n) Sh.emp) ;
       [%expect
         {|
         ( infer_frame:   emp \- ∃ %m_8, %n_9 .   %m_8 = %n_9 ∧ emp
@@ -101,7 +101,7 @@ let%test_module _ =
       let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; seq= a} in
       let minued = Sh.star common seg1 in
       let subtrahend =
-        Sh.and_ (Term.eq m n)
+        Sh.and_ (Formula.eq m n)
           (Sh.exists
              (Var.Set.of_list [m_])
              (Sh.extend_us (Var.Set.of_list [m_]) common))
@@ -229,7 +229,7 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.and_
-           Term.(or_ (or_ (eq n !0) (eq n !1)) (eq n !2))
+           Formula.(or_ (or_ (eq n !0) (eq n !1)) (eq n !2))
            seg_split_symbolically)
         [m_; a_]
         (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a}) ;
@@ -263,7 +263,7 @@ let%test_module _ =
     (* Incompleteness: equivalent to above but using ≤ instead of ∨ *)
     let%expect_test _ =
       infer_frame
-        (Sh.and_ (Term.le n !2) seg_split_symbolically)
+        (Sh.and_ (Formula.le n !2) seg_split_symbolically)
         [m_; a_]
         (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a}) ;
       [%expect
@@ -278,7 +278,9 @@ let%test_module _ =
     (* Incompleteness: cannot witness existentials to satisfy non-equality
        pure constraints *)
     let%expect_test _ =
-      let subtrahend = Sh.and_ (Term.eq m a) (Sh.pure (Term.dq m !0)) in
+      let subtrahend =
+        Sh.and_ (Formula.eq m a) (Sh.pure (Formula.dq m !0))
+      in
       let minuend = Sh.extend_us (Var.Set.of_ a_) Sh.emp in
       infer_frame minuend [m_] subtrahend ;
       [%expect