From 7e77bad4d2ccef09912d5d319420da762cd627ed Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 9 Jul 2020 07:44:32 -0700
Subject: [PATCH] [sledge] Change: Implement Fol using a solver-independent
 intermediate type

Summary:
In order to allow implementations of the single Fol interface using
multiple backend first-order logic solvers, add explicit definitions
of terms and formulas in the Fol module, and implement Context in
terms of them.

The Fol interface supports freely mixing Terms and Formulas, in
particular there is `Term.ite : cnd:Formula.t -> thn:Term.t ->
els:Term.t -> Term.t` which allows Formulas to appear in Terms. The
Fol implementation performs enough normalization to enable using an
internal representation of terms that is strictly partitioned into
"theory terms" and "formulas", which are stratified below "conditional
terms" and then below "general terms". This partitioning and
stratification enables using backend solvers that do not support
mixing formulas in terms.

Reviewed By: jvillard

Differential Revision: D22170506

fbshipit-source-id: a014ee7d7
---
 infer/src/pulse/Pudge_intf.ml         |   34 +-
 infer/src/pulse/PulseDummySledge.ml   |   24 +-
 infer/src/pulse/PulsePathCondition.ml |   58 +-
 infer/src/pulse/PulseSledge.ml        |  169 ++--
 sledge/src/fol.ml                     | 1292 ++++++++++++++++++++++++-
 sledge/src/fol.mli                    |   39 +-
 sledge/src/ses/term.ml                |    2 +
 sledge/src/ses/term.mli               |    1 +
 sledge/src/sh_test.ml                 |   20 +-
 sledge/src/solver_test.ml             |   12 +-
 10 files changed, 1452 insertions(+), 199 deletions(-)

diff --git a/infer/src/pulse/Pudge_intf.ml b/infer/src/pulse/Pudge_intf.ml
index 60aba4b24..132fa87d4 100644
--- a/infer/src/pulse/Pudge_intf.ml
+++ b/infer/src/pulse/Pudge_intf.ml
@@ -16,39 +16,43 @@ module type S = sig
 
   val true_ : t
 
-  module Term : sig
+  module Var : sig
     type t
 
-    val zero : t
+    val of_absval : AbstractValue.t -> t
 
-    val le : t -> t -> t
+    val to_absval : t -> AbstractValue.t
+    (** use with caution: will crash the program if the given variable wasn't generated from an
+        [AbstractValue.t] using [Var.of_absval] *)
+  end
 
-    val lt : t -> t -> t
+  module Term : sig
+    type t
 
-    val not_ : t -> t
+    val zero : t
 
     val of_intlit : IntLit.t -> t
 
     val of_absval : AbstractValue.t -> t
 
-    val of_unop : Unop.t -> t -> t
+    val of_unop : Unop.t -> t -> t option
 
-    val of_binop : Binop.t -> t -> t -> t
+    val of_binop : Binop.t -> t -> t -> t option
   end
 
-  module Var : sig
+  module Formula : sig
     type t
 
-    val of_absval : AbstractValue.t -> t
+    val eq : Term.t -> Term.t -> t
 
-    val to_absval : t -> AbstractValue.t
-    (** use with caution: will crash the program if the given variable wasn't generated from an
-        [AbstractValue.t] using [Var.of_absval] *)
-  end
+    val lt : Term.t -> Term.t -> t
 
-  val and_eq : Term.t -> Term.t -> t -> t
+    val not_ : t -> t
+
+    val term_binop : Binop.t -> Term.t -> Term.t -> t option
+  end
 
-  val and_term : Term.t -> t -> t
+  val and_formula : Formula.t -> t -> t
 
   val and_ : t -> t -> t
 
diff --git a/infer/src/pulse/PulseDummySledge.ml b/infer/src/pulse/PulseDummySledge.ml
index 2fc206181..a8b2061b4 100644
--- a/infer/src/pulse/PulseDummySledge.ml
+++ b/infer/src/pulse/PulseDummySledge.ml
@@ -21,19 +21,25 @@ module Term = struct
 
   let zero = ()
 
-  let le () () = ()
+  let of_intlit _ = ()
 
-  let lt () () = ()
+  let of_absval _ = ()
 
-  let not_ () = ()
+  let of_unop _ () = None
 
-  let of_intlit _ = ()
+  let of_binop _ () () = None
+end
 
-  let of_absval _ = ()
+module Formula = struct
+  type t = unit
+
+  let eq () () = ()
+
+  let lt () () = ()
 
-  let of_unop _ () = ()
+  let not_ () = ()
 
-  let of_binop _ () () = ()
+  let term_binop _ () () = None
 end
 
 (* same type as {!PulsePathCondition.t} to be nice to summary serialization *)
@@ -46,9 +52,7 @@ let pp fmt {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =
 
 let true_ = {eqs= Lazy.from_val Ses.Equality.true_; non_eqs= Lazy.from_val Ses.Term.true_}
 
-let and_eq () () phi = phi
-
-let and_term () phi = phi
+let and_formula () phi = phi
 
 let and_ phi1 _ = phi1
 
diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml
index 046ce8fa1..644a1b507 100644
--- a/infer/src/pulse/PulsePathCondition.ml
+++ b/infer/src/pulse/PulsePathCondition.ml
@@ -51,7 +51,7 @@ let and_nonnegative v ({satisfiable; bo_itvs; citvs; pudge} as phi) =
     { satisfiable
     ; bo_itvs= BoItvs.add v Itv.ItvPure.nat bo_itvs
     ; citvs= CItvs.add v CItv.zero_inf citvs
-    ; pudge= Pudge.and_term Pudge.Term.(le zero (of_absval v)) pudge }
+    ; pudge= Pudge.(and_formula (Formula.lt Term.zero (Term.of_absval v)) pudge) }
 
 
 let and_positive v ({satisfiable; bo_itvs; citvs; pudge} as phi) =
@@ -60,7 +60,7 @@ let and_positive v ({satisfiable; bo_itvs; citvs; pudge} as phi) =
     { satisfiable
     ; bo_itvs= BoItvs.add v Itv.ItvPure.pos bo_itvs
     ; citvs= CItvs.add v (CItv.ge_to IntLit.one) citvs
-    ; pudge= Pudge.and_term Pudge.Term.(lt zero (of_absval v)) pudge }
+    ; pudge= Pudge.(and_formula (Formula.lt Term.zero (Term.of_absval v)) pudge) }
 
 
 let and_eq_int v i ({satisfiable; bo_itvs; citvs; pudge} as phi) =
@@ -69,7 +69,7 @@ let and_eq_int v i ({satisfiable; bo_itvs; citvs; pudge} as phi) =
     { satisfiable
     ; bo_itvs= BoItvs.add v (Itv.ItvPure.of_int_lit i) bo_itvs
     ; citvs= CItvs.add v (CItv.equal_to i) citvs
-    ; pudge= Pudge.and_eq (Pudge.Term.of_absval v) (Pudge.Term.of_intlit i) pudge }
+    ; pudge= Pudge.(and_formula (Formula.eq (Term.of_absval v) (Term.of_intlit i)) pudge) }
 
 
 let simplify ~keep {satisfiable; bo_itvs; citvs; pudge} =
@@ -182,8 +182,9 @@ let and_pudge_callee subst pudge_caller pudge_callee =
         let subst', v_caller = subst_find_or_new subst v_callee in
         (subst', Pudge.Var.of_absval v_caller) )
   in
-  (* Don't trigger the computation of [path_condition] by asking for satisfiability here. Instead,
-     pudge (un-)satisfiability is computed lazily when we discover issues. *)
+  (* Don't trigger the computation of the underlying Sledge data structure by asking for
+     satisfiability here. Instead, pudge (un-)satisfiability is computed lazily when we discover
+     issues. *)
   (subst, Pudge.and_ pudge_caller pudge_callee_translated)
 
 
@@ -240,16 +241,19 @@ let eval_bo_itv_binop binop_addr bop op_lhs op_rhs bo_itvs =
   BoItvs.add binop_addr bo_itv bo_itvs
 
 
-let eval_path_condition_binop binop_addr binop op_lhs op_rhs pudge =
+let eval_pudge_binop binop_addr binop op_lhs op_rhs pudge =
+  let open Pudge in
   let term_of_op = function
     | LiteralOperand i ->
-        Pudge.Term.of_intlit i
+        Term.of_intlit i
     | AbstractValueOperand v ->
-        Pudge.Term.of_absval v
+        Term.of_absval v
   in
-  Pudge.and_eq (Pudge.Term.of_absval binop_addr)
-    (Pudge.Term.of_binop binop (term_of_op op_lhs) (term_of_op op_rhs))
-    pudge
+  match Term.of_binop binop (term_of_op op_lhs) (term_of_op op_rhs) with
+  | None ->
+      pudge
+  | Some t_binop ->
+      and_formula (Formula.eq (Term.of_absval binop_addr) t_binop) pudge
 
 
 let eval_binop binop_addr binop op_lhs op_rhs ({satisfiable; bo_itvs; citvs; pudge} as phi) =
@@ -258,7 +262,7 @@ let eval_binop binop_addr binop op_lhs op_rhs ({satisfiable; bo_itvs; citvs; pud
     { satisfiable
     ; bo_itvs= eval_bo_itv_binop binop_addr binop op_lhs op_rhs bo_itvs
     ; citvs= eval_citv_binop binop_addr binop op_lhs op_rhs citvs
-    ; pudge= eval_path_condition_binop binop_addr binop op_lhs op_rhs pudge }
+    ; pudge= eval_pudge_binop binop_addr binop op_lhs op_rhs pudge }
 
 
 let eval_citv_unop unop_addr unop operand_addr citvs =
@@ -278,8 +282,13 @@ let eval_bo_itv_unop unop_addr unop operand_addr bo_itvs =
       BoItvs.add unop_addr itv bo_itvs
 
 
-let eval_path_condition_unop unop_addr unop addr pudge =
-  Pudge.and_eq (Pudge.Term.of_absval unop_addr) Pudge.Term.(of_unop unop (of_absval addr)) pudge
+let eval_pudge_unop unop_addr (unop : Unop.t) addr pudge =
+  let open Pudge in
+  match Term.of_unop unop (Term.of_absval addr) with
+  | None ->
+      pudge
+  | Some t_unop ->
+      and_formula (Formula.eq (Term.of_absval unop_addr) t_unop) pudge
 
 
 let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; pudge} as phi) =
@@ -288,7 +297,7 @@ let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; pudge} as phi)
     { satisfiable
     ; bo_itvs= eval_bo_itv_unop unop_addr unop addr bo_itvs
     ; citvs= eval_citv_unop unop_addr unop addr citvs
-    ; pudge= eval_path_condition_unop unop_addr unop addr pudge }
+    ; pudge= eval_pudge_unop unop_addr unop addr pudge }
 
 
 let prune_bo_with_bop ~negated v_opt arith bop arith' phi =
@@ -328,15 +337,18 @@ let bind_satisfiable phi ~f = if phi.satisfiable then f phi else phi
 let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; pudge} as phi) =
   if not satisfiable then phi
   else
-    let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, path_cond_lhs = eval_operand phi lhs_op in
-    let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, path_cond_rhs = eval_operand phi rhs_op in
+    let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, pudge_lhs = eval_operand phi lhs_op in
+    let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, pudge_rhs = eval_operand phi rhs_op in
     let phi =
-      let pudge =
-        let t_positive = Pudge.Term.of_binop bop path_cond_lhs path_cond_rhs in
-        let t = if negated then Pudge.Term.not_ t_positive else t_positive in
-        Pudge.and_term t pudge
-      in
-      {phi with pudge}
+      match Pudge.Formula.term_binop bop pudge_lhs pudge_rhs with
+      | None ->
+          phi
+      | Some f_positive ->
+          let pudge =
+            let f = if negated then Pudge.Formula.not_ f_positive else f_positive in
+            Pudge.and_formula f pudge
+          in
+          {phi with pudge}
     in
     match CItv.abduce_binop_is_true ~negated bop arith_lhs_opt arith_rhs_opt with
     | Unsatisfiable ->
diff --git a/infer/src/pulse/PulseSledge.ml b/infer/src/pulse/PulseSledge.ml
index 009713277..d9a47c529 100644
--- a/infer/src/pulse/PulseSledge.ml
+++ b/infer/src/pulse/PulseSledge.ml
@@ -6,14 +6,13 @@
  *)
 
 open! IStd
-module F = Format
 module L = Logging
 module AbstractValue = PulseAbstractValue
 
 [@@@warning "+9"]
 
 module Var = struct
-  module Var = Ses.Var
+  module Var = Sledge.Fol.Var
 
   let of_absval (v : AbstractValue.t) = Var.identified ~name:"v" ~id:(v :> int)
 
@@ -26,153 +25,133 @@ module Var = struct
 end
 
 module Term = struct
-  module Term = Ses.Term
+  module Term = Sledge.Fol.Term
 
   let of_intlit i = Term.integer (IntLit.to_big_int i)
 
   let of_absval v = Term.var (Var.of_absval v)
 
-  let of_unop (unop : Unop.t) t = match unop with Neg -> Term.neg t | BNot | LNot -> Term.not_ t
+  let of_unop (unop : Unop.t) t = match unop with Neg -> Some (Term.neg t) | BNot | LNot -> None
 
   let of_binop (binop : Binop.t) t1 t2 =
     let open Term in
     match binop with
     | PlusA _ | PlusPI ->
-        add t1 t2
+        Some (add t1 t2)
     | MinusA _ | MinusPI | MinusPP ->
-        sub t1 t2
+        Some (sub t1 t2)
     | Mult _ ->
-        mul t1 t2
-    | Div ->
-        div t1 t2
-    | Mod ->
-        rem t1 t2
-    | Shiftlt ->
-        shl t1 t2
+        Some (mul t1 t2)
+    | Div | Mod | Shiftlt | Shiftrt | Lt | Gt | Le | Ge | Eq | Ne | BAnd | LAnd | BOr | LOr | BXor
+      ->
+        None
+
+
+  include Term
+end
+
+module Formula = struct
+  module Formula = Sledge.Fol.Formula
+
+  let term_binop (binop : Binop.t) t1 t2 =
+    match binop with
+    | BAnd
+    | BOr
+    | BXor
+    | PlusA _
+    | PlusPI
+    | MinusA _
+    | MinusPI
+    | MinusPP
+    | Mult _
+    | Div
+    | Mod
+    | Shiftlt
     | Shiftrt ->
-        lshr t1 t2
+        Term.of_binop binop t1 t2 |> Option.map ~f:(fun t -> Formula.dq t Term.zero)
     | Lt ->
-        lt t1 t2
+        Some (Formula.lt t1 t2)
     | Gt ->
-        lt t2 t1
+        Some (Formula.lt t2 t1)
     | Le ->
-        le t1 t2
+        Some (Formula.le t1 t2)
     | Ge ->
-        le t2 t1
+        Some (Formula.le t2 t1)
     | Eq ->
-        eq t1 t2
+        Some (Formula.eq t1 t2)
     | Ne ->
-        dq t1 t2
-    | BAnd | LAnd ->
-        and_ t1 t2
-    | BOr | LOr ->
-        or_ t1 t2
-    | BXor ->
-        xor t1 t2
+        Some (Formula.dq t1 t2)
+    | LAnd ->
+        Option.both (Formula.project t1) (Formula.project t2)
+        |> Option.map ~f:(fun (f1, f2) -> Formula.and_ f1 f2)
+    | LOr ->
+        Option.both (Formula.project t1) (Formula.project t2)
+        |> Option.map ~f:(fun (f1, f2) -> Formula.or_ f1 f2)
 
 
-  include Term
+  include Formula
 end
 
-module Equality = struct
-  include Ses.Equality
+module Context = struct
+  include Sledge.Fol.Context
 
   let assert_no_new_vars api new_vars =
     if not (Var.Set.is_empty new_vars) then
       L.die InternalError "Huho, %s generated fresh new variables %a" api Var.Set.pp new_vars
 
 
-  let and_eq t1 t2 r =
-    let new_vars, r' = Ses.Equality.and_eq Var.Set.empty t1 t2 r in
-    assert_no_new_vars "Equality.and_eq" new_vars ;
-    r'
-
-
-  let and_term t r =
-    let new_vars, r' = Ses.Equality.and_term Var.Set.empty t r in
-    assert_no_new_vars "Equality.and_term" new_vars ;
+  let and_formula phi r =
+    let new_vars, r' = Sledge.Fol.Context.and_formula Var.Set.empty phi r in
+    assert_no_new_vars "Context.and_formula" new_vars ;
     r'
 
 
   let and_ r1 r2 =
-    let new_vars, r' = Ses.Equality.and_ Var.Set.empty r1 r2 in
-    assert_no_new_vars "Equality.and_" new_vars ;
+    let new_vars, r' = Sledge.Fol.Context.and_ Var.Set.empty r1 r2 in
+    assert_no_new_vars "Context.and_" new_vars ;
     r'
 
 
   let apply_subst subst r =
-    let new_vars, r' = Ses.Equality.apply_subst Var.Set.empty subst r in
-    assert_no_new_vars "Equality.apply_subst" new_vars ;
+    let new_vars, r' = Sledge.Fol.Context.apply_subst Var.Set.empty subst r in
+    assert_no_new_vars "Context.apply_subst" new_vars ;
     r'
 end
 
-(** We distinguish between what the equality relation of sledge can express and the "non-equalities"
-    terms that this relation ignores. We keep the latter around for completeness: we can still
-    substitute known equalities into these and sometimes get contradictions back. *)
-type t = {eqs: Equality.t lazy_t; non_eqs: Term.t lazy_t}
-
-let pp fmt {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =
-  F.fprintf fmt "%a∧%a" Equality.pp eqs Term.pp non_eqs
-
-
-let true_ = {eqs= Lazy.from_val Equality.true_; non_eqs= Lazy.from_val Term.true_}
+type t = Context.t lazy_t
 
-let and_eq t1 t2 phi = {phi with eqs= lazy (Equality.and_eq t1 t2 (Lazy.force phi.eqs))}
+let pp fmt (lazy phi) = Context.pp fmt phi
 
-let and_term (t : Term.t) phi =
-  (* add the term to the relation *)
-  let eqs = lazy (Equality.and_term t (Lazy.force phi.eqs)) in
-  (* [t] normalizes to [true_] so [non_eqs] never changes, do this regardless for now *)
-  let non_eqs = lazy (Term.and_ (Lazy.force phi.non_eqs) (Equality.normalize (Lazy.force eqs) t)) in
-  {eqs; non_eqs}
+let true_ = Lazy.from_val Context.true_
 
+let and_formula f phi = lazy (Context.and_formula f (Lazy.force phi))
 
-let and_ phi1 phi2 =
-  { eqs= lazy (Equality.and_ (Lazy.force phi1.eqs) (Lazy.force phi2.eqs))
-  ; non_eqs= lazy (Term.and_ (Lazy.force phi1.non_eqs) (Lazy.force phi2.non_eqs)) }
+let and_ phi1 phi2 = lazy (Context.and_ (Lazy.force phi1) (Lazy.force phi2))
 
+let is_known_zero t phi = Context.entails_eq (Lazy.force phi) t Term.zero
 
-let is_known_zero t phi = Equality.entails_eq (Lazy.force phi.eqs) t Term.zero
-
-(* NOTE: not normalizing non_eqs here gives imprecise results but is cheaper *)
-let is_unsat {eqs; non_eqs} =
-  (* [Term.is_false] is cheap, forcing [eqs] is expensive, then calling [Equality.normalize] is
-     expensive on top of that *)
-  Term.is_false (Lazy.force non_eqs)
-  || Equality.is_false (Lazy.force eqs)
-  || Term.is_false (Equality.normalize (Lazy.force eqs) (Lazy.force non_eqs))
-
-
-let fv {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =
-  Term.Var.Set.union (Equality.fv eqs) (Term.fv non_eqs)
+let is_unsat phi = Context.is_false (Lazy.force phi)
 
+let fv (lazy phi) = Context.fv phi
 
 let fold_map_variables phi ~init ~f =
-  let term_fold_map t ~init ~f =
-    Term.fold_map_rec_pre t ~init ~f:(fun acc t ->
-        Var.of_term t
-        |> Option.map ~f:(fun v ->
-               let acc', v' = f acc v in
-               (acc', Term.var v') ) )
-  in
-  let acc, eqs' =
-    Equality.classes (Lazy.force phi.eqs)
-    |> Term.Map.fold ~init:(init, Equality.true_) ~f:(fun ~key:t ~data:equal_ts (acc, eqs') ->
-           let acc, t' = term_fold_map ~init:acc ~f t in
-           List.fold equal_ts ~init:(acc, eqs') ~f:(fun (acc, eqs') equal_t ->
-               let acc, t_mapped = term_fold_map ~init:acc ~f equal_t in
-               (acc, Equality.and_eq t' t_mapped eqs') ) )
+  let acc, phi' =
+    Context.classes (Lazy.force phi)
+    |> Term.Map.fold ~init:(init, Context.true_) ~f:(fun ~key:t ~data:equal_ts (acc, phi') ->
+           let acc, t' = Term.fold_map_vars ~init:acc ~f t in
+           List.fold equal_ts ~init:(acc, phi') ~f:(fun (acc, phi') equal_t ->
+               let acc, t_mapped = Term.fold_map_vars ~init:acc ~f equal_t in
+               (acc, Context.and_formula (Formula.eq t' t_mapped) phi') ) )
   in
-  let acc, non_eqs' = term_fold_map ~init:acc ~f (Lazy.force phi.non_eqs) in
-  (acc, {eqs= Lazy.from_val eqs'; non_eqs= Lazy.from_val non_eqs'})
+  (acc, Lazy.from_val phi')
 
 
 let simplify ~keep phi =
   let all_vs = fv phi in
   let keep_vs =
     AbstractValue.Set.fold
-      (fun v keep_vs -> Term.Var.Set.add keep_vs (Var.of_absval v))
-      keep Term.Var.Set.empty
+      (fun v keep_vs -> Var.Set.add keep_vs (Var.of_absval v))
+      keep Var.Set.empty
   in
-  let simpl_subst = Equality.solve_for_vars [keep_vs; all_vs] (Lazy.force phi.eqs) in
-  {phi with eqs= Lazy.from_val (Equality.apply_subst simpl_subst (Lazy.force phi.eqs))}
+  let simpl_subst = Context.solve_for_vars [keep_vs; all_vs] (Lazy.force phi) in
+  Lazy.from_val (Context.apply_subst simpl_subst (Lazy.force phi))
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 578596fd1..69e990db6 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -5,15 +5,280 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-module Var = struct
-  include Ses.Term.Var
+let pp_boxed fs fmt =
+  Format.pp_open_box fs 2 ;
+  Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
+
+(*
+ * Terms
+ *)
+
+(** Terms, denoting functions from structures to values, built from
+    variables and applications of function symbols from various theories. *)
+type trm =
+  | Var of {id: int; name: string}
+  | Z of Z.t
+  | Q of Q.t
+  | Neg of trm
+  | Add of trm * trm
+  | Sub of trm * trm
+  | Mulq of Q.t * trm
+  | Mul of trm * trm
+  | Div of trm * trm
+  | Rem of trm * trm
+  | Splat of trm
+  | Sized of {seq: trm; siz: trm}
+  | Extract of {seq: trm; off: trm; len: trm}
+  | Concat of trm iarray
+  | Select of trm * int
+  | Update of trm * int * trm
+  | Record of trm iarray
+  | RecRecord of int
+  | Label of {parent: string; name: string}
+  | Float of string
+  | BAnd of trm * trm
+  | BOr of trm * trm
+  | BXor of trm * trm
+  | BShl of trm * trm
+  | BLshr of trm * trm
+  | BAshr of trm * trm
+  | Signed of int * trm
+  | Unsigned of int * trm
+  | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t; arg: trm}
+[@@deriving compare, equal, sexp]
+
+let compare_trm x y =
+  if x == y then 0
+  else
+    match (x, y) with
+    | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
+        Int.compare i j
+    | _ -> compare_trm x y
+
+let equal_trm x y =
+  x == y
+  ||
+  match (x, y) with
+  | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
+      Int.equal i j
+  | _ -> equal_trm x y
+
+let _Neg x = Neg x
+let _Add x y = Add (x, y)
+let _Sub x y = Sub (x, y)
+let _Mulq q x = Mulq (q, x)
+let _Mul x y = Mul (x, y)
+let _Div x y = Div (x, y)
+let _Rem x y = Rem (x, y)
+let _Splat x = Splat x
+let _Sized seq siz = Sized {seq; siz}
+let _Extract seq off len = Extract {seq; off; len}
+let _Concat es = Concat es
+let _Select r i = Select (r, i)
+let _Update r i x = Update (r, i, x)
+let _Record es = Record es
+let _RecRecord n = RecRecord n
+let _BAnd x y = BAnd (x, y)
+let _BOr x y = BOr (x, y)
+let _BXor x y = BXor (x, y)
+let _BShl x y = BShl (x, y)
+let _BLshr x y = BLshr (x, y)
+let _BAshr x y = BAshr (x, y)
+let _Signed n x = Signed (n, x)
+let _Unsigned n x = Unsigned (n, x)
+let _Convert src dst arg = Convert {src; dst; arg}
+
+(*
+ * Formulas
+ *)
+
+(** Formulas, denoting sets of structures, built from propositional
+    variables, applications of predicate symbols from various theories, and
+    first-order logic connectives. *)
+type fml =
+  | Tt
+  | Ff
+  | Eq of trm * trm
+  | Dq of trm * trm
+  | Lt of trm * trm
+  | Le of trm * trm
+  | Ord of trm * trm
+  | Uno of trm * trm
+  | Not of fml
+  | And of fml * fml
+  | Or of fml * fml
+  | Iff of fml * fml
+  | Xor of fml * fml
+  | Imp of fml * fml
+  | Cond of {cnd: fml; pos: fml; neg: fml}
+[@@deriving compare, equal, sexp]
+
+let _Eq x y = Eq (x, y)
+let _Dq x y = Dq (x, y)
+let _Lt x y = Lt (x, y)
+let _Le x y = Le (x, y)
+let _Ord x y = Ord (x, y)
+let _Uno x y = Uno (x, y)
+let _Not p = Not p
+let _And p q = And (p, q)
+let _Or p q = Or (p, q)
+let _Iff p q = Iff (p, q)
+let _Xor p q = Xor (p, q)
+let _Imp p q = Imp (p, q)
+let _Cond cnd pos neg = Cond {cnd; pos; neg}
+
+(*
+ * Conditional terms
+ *)
+
+(** Conditional terms, denoting functions from structures to values, taking
+    the form of trees with internal nodes labeled with formulas and leaves
+    labeled with terms. *)
+type cnd = [`Ite of fml * cnd * cnd | `Trm of trm]
+[@@deriving compare, equal, sexp]
+
+(*
+ * Expressions
+ *)
+
+(** Expressions, which are partitioned into terms, conditional terms, and
+    formulas. *)
+type exp = [cnd | `Fml of fml] [@@deriving compare, equal, sexp]
+
+(*
+ * Variables
+ *)
+
+(** Variable terms *)
+module Var : sig
+  type t = private trm [@@deriving compare, equal, sexp]
+  type strength = t -> [`Universal | `Existential | `Anonymous] option
+
+  val ppx : strength -> t pp
+  val pp : t pp
+
+  module Map : Map.S with type key := t
+
+  module Set : sig
+    include NS.Set.S with type elt := t
+
+    val sexp_of_t : t -> Sexp.t
+    val t_of_sexp : Sexp.t -> t
+    val ppx : strength -> t pp
+    val pp : t pp
+    val pp_xs : t pp
+  end
+
+  val of_ : trm -> t
+  val of_exp : exp -> t option
+  val program : name:string -> global:bool -> t
+  val fresh : string -> wrt:Set.t -> t * Set.t
+
+  val identified : name:string -> id:int -> t
+  (** Variable with the given [id]. Variables are compared by [id] alone,
+      [name] is used only for printing. The only way to ensure [identified]
+      variables do not clash with [fresh] variables is to pass the
+      [identified] variables to [fresh] in [wrt]:
+      [Var.fresh name ~wrt:(Var.Set.of_ (Var.identified ~name ~id))]. *)
+
+  val id : t -> int
+  val name : t -> string
+
+  module Subst : sig
+    type var := t
+    type t [@@deriving compare, equal, sexp]
+    type x = {sub: t; dom: Set.t; rng: Set.t}
+
+    val pp : t pp
+    val empty : t
+    val freshen : Set.t -> wrt:Set.t -> x * Set.t
+    val invert : t -> t
+    val restrict : t -> Set.t -> x
+    val is_empty : t -> bool
+    val domain : t -> Set.t
+    val range : t -> Set.t
+    val fold : t -> init:'a -> f:(var -> var -> 'a -> 'a) -> 'a
+    val apply : t -> var -> var
+  end
+end = struct
+  module T = struct
+    type t = trm [@@deriving compare, equal, sexp]
+    type strength = t -> [`Universal | `Existential | `Anonymous] option
+
+    let invariant (x : t) =
+      let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
+      match x with
+      | Var _ -> ()
+      | _ -> fail "non-var: %a" Sexp.pp_hum (sexp_of_trm x) ()
+
+    let ppx strength fs v =
+      let pf fmt = pp_boxed fs fmt in
+      match (v : trm) with
+      | Var {name; id= -1} -> Trace.pp_styled `Bold "%@%s" fs name
+      | Var {name; id= 0} -> Trace.pp_styled `Bold "%%%s" fs name
+      | Var {name; id} -> (
+        match strength v with
+        | None -> pf "%%%s_%d" name id
+        | Some `Universal -> Trace.pp_styled `Bold "%%%s_%d" fs name id
+        | Some `Existential -> Trace.pp_styled `Cyan "%%%s_%d" fs name id
+        | Some `Anonymous -> Trace.pp_styled `Cyan "_" fs )
+      | x -> violates invariant x
+
+    let pp = ppx (fun _ -> None)
+  end
+
+  include T
+
+  module Map = struct
+    include Map.Make (T)
+    include Provide_of_sexp (T)
+  end
+
+  module Set = struct
+    include Set.Make (T)
+    include Provide_of_sexp (T)
+
+    let ppx strength vs = pp (T.ppx strength) vs
+    let pp vs = pp T.pp vs
+
+    let pp_xs fs xs =
+      if not (is_empty xs) then
+        Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs
+  end
+
+  (* access *)
+
+  let id = function Var v -> v.id | x -> violates invariant x
+  let name = function Var v -> v.name | x -> violates invariant x
+
+  (* construct *)
+
+  let of_ = function Var _ as v -> v | _ -> invalid_arg "Var.of_"
+
+  let of_exp = function
+    | `Trm (Var _ as v) -> Some (v |> check invariant)
+    | _ -> None
+
+  let program ~name ~global = Var {name; id= (if global then -1 else 0)}
+
+  let fresh name ~wrt =
+    let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in
+    let x' = Var {name; id= max + 1} in
+    (x', Set.add wrt x')
+
+  let identified ~name ~id = Var {name; id}
+
+  (*
+   * Renamings
+   *)
 
   (** Variable renaming substitutions *)
   module Subst = struct
-    type nonrec t = t Map.t [@@deriving compare, equal, sexp_of]
+    type t = trm Map.t [@@deriving compare, equal, sexp_of]
     type x = {sub: t; dom: Set.t; rng: Set.t}
 
     let t_of_sexp = Map.t_of_sexp t_of_sexp
+    let pp = Map.pp pp pp
 
     let invariant s =
       let@ () = Invariant.invariant [%here] s [%sexp_of: t] in
@@ -26,7 +291,6 @@ module Var = struct
       in
       assert (Set.disjoint domain range)
 
-    let pp = Map.pp pp pp
     let empty = Map.empty
     let is_empty = Map.is_empty
 
@@ -83,42 +347,920 @@ module Var = struct
   end
 end
 
-module Term = struct
-  include (
-    Ses.Term : module type of Ses.Term with module Var := Ses.Term.Var )
+type var = Var.t
 
-  let ite = conditional
-  let rename s e = rename (Var.Subst.apply s) e
-end
+(*
+ * Representation operations
+ *)
+
+(** pp *)
+
+let rec ppx_t strength fs trm =
+  let rec pp fs trm =
+    let pf fmt = pp_boxed fs fmt in
+    match (trm : trm) with
+    | Var _ as v -> Var.ppx strength fs (Var.of_ v)
+    | Z z -> Trace.pp_styled `Magenta "%a" fs Z.pp z
+    | Q q -> Trace.pp_styled `Magenta "%a" fs Q.pp q
+    | Neg x -> pf "(- %a)" pp x
+    | Add (x, y) -> pf "(%a@ + %a)" pp x pp y
+    | Sub (x, y) -> pf "(%a@ - %a)" pp x pp y
+    | Mulq (q, x) -> pf "(%a@ @<2>× %a)" Q.pp q pp x
+    | Mul (x, y) -> pf "(%a@ @<2>× %a)" pp x pp y
+    | Div (x, y) -> pf "(%a@ / %a)" pp x pp y
+    | Rem (x, y) -> pf "(%a@ %% %a)" pp x pp y
+    | Splat x -> pf "%a^" pp x
+    | Sized {seq; siz} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp seq
+    | Extract {seq; off; len} -> pf "%a[%a,%a)" pp seq pp off pp len
+    | Concat xs when IArray.is_empty xs -> pf "@<2>⟨⟩"
+    | Concat xs -> pf "(%a)" (IArray.pp "@,^" pp) xs
+    | Select (rcd, idx) -> pf "%a[%i]" pp rcd idx
+    | Update (rcd, idx, elt) -> pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt
+    | Record xs -> pf "{%a}" (pp_record strength) xs
+    | RecRecord i -> pf "(rec_record %i)" i
+    | Label {name} -> pf "%s" name
+    | Float s -> pf "%s" s
+    | BAnd (x, y) -> pf "(%a@ && %a)" pp x pp y
+    | BOr (x, y) -> pf "(%a@ || %a)" pp x pp y
+    | BXor (x, y) -> pf "(%a@ xor %a)" pp x pp y
+    | BShl (x, y) -> pf "(%a@ shl %a)" pp x pp y
+    | BLshr (x, y) -> pf "(%a@ lshr %a)" pp x pp y
+    | BAshr (x, y) -> pf "(%a@ ashr %a)" pp x pp y
+    | Signed (n, x) -> pf "((s%i)@ %a)" n pp x
+    | Unsigned (n, x) -> pf "((u%i)@ %a)" n pp x
+    | Convert {src; dst; arg} ->
+        pf "((%a)(%a)@ %a)" Llair.Typ.pp dst Llair.Typ.pp src pp arg
+  in
+  pp fs trm
+
+and pp_record strength fs elts =
+  [%Trace.fprintf
+    fs "%a"
+      (fun fs elts ->
+        match
+          String.init (IArray.length elts) ~f:(fun i ->
+              match IArray.get elts i with
+              | Z z -> Char.of_int_exn (Z.to_int z)
+              | _ -> raise (Invalid_argument "not a string") )
+        with
+        | s -> Format.fprintf fs "@[<h>%s@]" (String.escaped s)
+        | exception _ ->
+            Format.fprintf fs "@[<h>%a@]"
+              (IArray.pp ",@ " (ppx_t strength))
+              elts )
+      elts]
+
+let ppx_f strength fs fml =
+  let pp_t = ppx_t strength in
+  let rec pp fs fml =
+    let pf fmt = pp_boxed fs fmt in
+    match (fml : fml) with
+    | Tt -> pf "tt"
+    | Ff -> pf "ff"
+    | Eq (x, y) -> pf "(%a@ = %a)" pp_t x pp_t y
+    | Dq (x, y) -> pf "(%a@ @<2>≠ %a)" pp_t x pp_t y
+    | Lt (x, y) -> pf "(%a@ < %a)" pp_t x pp_t y
+    | Le (x, y) -> pf "(%a@ @<2>≤ %a)" pp_t x pp_t y
+    | Ord (x, y) -> pf "(%a@ ord %a)" pp_t x pp_t y
+    | Uno (x, y) -> pf "(%a@ uno %a)" pp_t x pp_t y
+    | Not x -> pf "¬%a" pp x
+    | And (x, y) -> pf "(%a@ @<2>∧ %a)" pp x pp y
+    | Or (x, y) -> pf "(%a@ @<2>∨ %a)" pp x pp y
+    | Iff (x, y) -> pf "(%a@ <=> %a)" pp x pp y
+    | Xor (x, y) -> pf "(%a@ xor %a)" pp x pp y
+    | Imp (x, y) -> pf "(%a@ => %a)" pp x pp y
+    | Cond {cnd; pos; neg} -> pf "(%a@ ? %a@ : %a)" pp cnd pp pos pp neg
+  in
+  pp fs fml
+
+let pp_f = ppx_f (fun _ -> None)
+
+let ppx_c strength fs ct =
+  let pp_t = ppx_t strength in
+  let pp_f = ppx_f strength in
+  let rec pp fs ct =
+    let pf fmt = pp_boxed fs fmt in
+    match ct with
+    | `Ite (cnd, thn, els) -> pf "(%a@ ? %a@ : %a)" pp_f cnd pp thn pp els
+    | `Trm t -> pp_t fs t
+  in
+  pp fs ct
+
+let ppx strength fs = function
+  | #cnd as c -> ppx_c strength fs c
+  | `Fml f -> ppx_f strength fs f
+
+let pp = ppx (fun _ -> None)
+
+(** fold_vars *)
+
+let rec fold_vars_t e ~init ~f =
+  match (e : trm) with
+  | Var _ as v -> f init (Var.of_ v)
+  | Z _ | Q _ | RecRecord _ | Label _ | Float _ -> init
+  | Neg x
+   |Mulq (_, x)
+   |Splat x
+   |Select (x, _)
+   |Signed (_, x)
+   |Unsigned (_, x)
+   |Convert {src= _; dst= _; arg= x} ->
+      fold_vars_t ~f x ~init
+  | Add (x, y)
+   |Sub (x, y)
+   |Mul (x, y)
+   |Div (x, y)
+   |Rem (x, y)
+   |Sized {seq= x; siz= y}
+   |Update (x, _, y)
+   |BAnd (x, y)
+   |BOr (x, y)
+   |BXor (x, y)
+   |BShl (x, y)
+   |BLshr (x, y)
+   |BAshr (x, y) ->
+      fold_vars_t ~f x ~init:(fold_vars_t ~f y ~init)
+  | Extract {seq= x; off= y; len= z} ->
+      fold_vars_t ~f x
+        ~init:(fold_vars_t ~f y ~init:(fold_vars_t ~f z ~init))
+  | Concat xs | Record xs ->
+      IArray.fold ~f:(fun init -> fold_vars_t ~f ~init) xs ~init
+
+let rec fold_vars_f ~init p ~f =
+  match (p : fml) with
+  | Tt | Ff -> init
+  | Eq (x, y) | Dq (x, y) | Lt (x, y) | Le (x, y) | Ord (x, y) | Uno (x, y)
+    ->
+      fold_vars_t ~f x ~init:(fold_vars_t ~f y ~init)
+  | Not x -> fold_vars_f ~f x ~init
+  | And (x, y) | Or (x, y) | Iff (x, y) | Xor (x, y) | Imp (x, y) ->
+      fold_vars_f ~f x ~init:(fold_vars_f ~f y ~init)
+  | Cond {cnd; pos; neg} ->
+      fold_vars_f ~f cnd
+        ~init:(fold_vars_f ~f pos ~init:(fold_vars_f ~f neg ~init))
+
+let rec fold_vars_c ~init ~f = function
+  | `Ite (cnd, thn, els) ->
+      fold_vars_f ~f cnd
+        ~init:(fold_vars_c ~f thn ~init:(fold_vars_c ~f els ~init))
+  | `Trm t -> fold_vars_t ~f t ~init
+
+let fold_vars ~init e ~f =
+  match e with
+  | `Fml p -> fold_vars_f ~f ~init p
+  | #cnd as c -> fold_vars_c ~f ~init c
+
+(** map_vars *)
+
+let map1 f e cons x =
+  let x' = f x in
+  if x == x' then e else cons x'
+
+let map2 f e cons x y =
+  let x' = f x in
+  let y' = f y in
+  if x == x' && y == y' then e else cons x' y'
+
+let map3 f e cons x y z =
+  let x' = f x in
+  let y' = f y in
+  let z' = f z in
+  if x == x' && y == y' && z == z' then e else cons x' y' z'
+
+let mapN f e cons xs =
+  let xs' = IArray.map_endo ~f xs in
+  if xs' == xs then e else cons xs'
+
+let rec map_vars_t ~f e =
+  match e with
+  | Var _ as v -> (f (Var.of_ v) : var :> trm)
+  | Z _ | Q _ -> e
+  | Neg x -> map1 (map_vars_t ~f) e _Neg x
+  | Add (x, y) -> map2 (map_vars_t ~f) e _Add x y
+  | Sub (x, y) -> map2 (map_vars_t ~f) e _Sub x y
+  | Mulq (q, x) -> map1 (map_vars_t ~f) e (_Mulq q) x
+  | Mul (x, y) -> map2 (map_vars_t ~f) e _Mul x y
+  | Div (x, y) -> map2 (map_vars_t ~f) e _Div x y
+  | Rem (x, y) -> map2 (map_vars_t ~f) e _Rem x y
+  | Splat x -> map1 (map_vars_t ~f) e _Splat x
+  | Sized {seq; siz} -> map2 (map_vars_t ~f) e _Sized seq siz
+  | Extract {seq; off; len} -> map3 (map_vars_t ~f) e _Extract seq off len
+  | Concat xs -> mapN (map_vars_t ~f) e _Concat xs
+  | Select (r, i) -> map1 (map_vars_t ~f) e (fun r -> _Select r i) r
+  | Update (r, i, e) ->
+      map2 (map_vars_t ~f) e (fun r e -> _Update r i e) r e
+  | Record xs -> mapN (map_vars_t ~f) e _Record xs
+  | RecRecord _ | Label _ | Float _ -> e
+  | BAnd (x, y) -> map2 (map_vars_t ~f) e _BAnd x y
+  | BOr (x, y) -> map2 (map_vars_t ~f) e _BOr x y
+  | BXor (x, y) -> map2 (map_vars_t ~f) e _BXor x y
+  | BShl (x, y) -> map2 (map_vars_t ~f) e _BShl x y
+  | BLshr (x, y) -> map2 (map_vars_t ~f) e _BLshr x y
+  | BAshr (x, y) -> map2 (map_vars_t ~f) e _BAshr x y
+  | Signed (n, x) -> map1 (map_vars_t ~f) e (_Signed n) x
+  | Unsigned (n, x) -> map1 (map_vars_t ~f) e (_Unsigned n) x
+  | Convert {src; dst; arg} -> map1 (map_vars_t ~f) e (_Convert src dst) arg
+
+let rec map_vars_f ~f e =
+  match e with
+  | Tt | Ff -> e
+  | Eq (x, y) -> map2 (map_vars_t ~f) e _Eq x y
+  | Dq (x, y) -> map2 (map_vars_t ~f) e _Dq x y
+  | Lt (x, y) -> map2 (map_vars_t ~f) e _Lt x y
+  | Le (x, y) -> map2 (map_vars_t ~f) e _Le x y
+  | Ord (x, y) -> map2 (map_vars_t ~f) e _Ord x y
+  | Uno (x, y) -> map2 (map_vars_t ~f) e _Uno x y
+  | Not x -> map1 (map_vars_f ~f) e _Not x
+  | And (x, y) -> map2 (map_vars_f ~f) e _And x y
+  | Or (x, y) -> map2 (map_vars_f ~f) e _Or x y
+  | Iff (x, y) -> map2 (map_vars_f ~f) e _Iff x y
+  | Xor (x, y) -> map2 (map_vars_f ~f) e _Xor x y
+  | Imp (x, y) -> map2 (map_vars_f ~f) e _Imp x y
+  | Cond {cnd; pos; neg} -> map3 (map_vars_f ~f) e _Cond cnd pos neg
+
+let rec map_vars_c ~f c =
+  match c with
+  | `Ite (cnd, thn, els) ->
+      let cnd' = map_vars_f ~f cnd in
+      let thn' = map_vars_c ~f thn in
+      let els' = map_vars_c ~f els in
+      if cnd' == cnd && thn' == thn && els' == els then c
+      else `Ite (cnd', thn', els')
+  | `Trm t ->
+      let t' = map_vars_t ~f t in
+      if t' == t then c else `Trm t'
+
+let map_vars ~f = function
+  | `Fml p -> `Fml (map_vars_f ~f p)
+  | #cnd as c -> (map_vars_c ~f c :> exp)
+
+(*
+ * Core construction functions
+ *
+ * Support functions for constructing expressions as if terms and formulas
+ * could be freely mixed, instead of being strictly partitioned into terms
+ * and formulas stratified below conditional terms and then expressions.
+ *)
+
+let zero = Z Z.zero
+let one = Z Z.one
+
+(** Map a unary function on terms over the leaves of a conditional term,
+    rebuilding the tree of conditionals with the supplied ite construction
+    function. *)
+let rec map_cnd : (fml -> 'a -> 'a -> 'a) -> (trm -> 'a) -> cnd -> 'a =
+ fun f_ite f_trm -> function
+  | `Trm trm -> f_trm trm
+  | `Ite (cnd, thn, els) ->
+      let thn' = map_cnd f_ite f_trm thn in
+      let els' = map_cnd f_ite f_trm els in
+      f_ite cnd thn' els'
+
+(** Embed a formula into a conditional term (associating true with 1 and
+    false with 0), identity on conditional terms. *)
+let embed_into_cnd : exp -> cnd = function
+  | #cnd as c -> c
+  (* p ==> (p ? 1 : 0) *)
+  | `Fml fml -> `Ite (fml, `Trm one, `Trm zero)
+
+(** Project out a formula that is embedded into a conditional term.
+
+    - [project_out_fml] is left inverse to [embed_into_cnd] in the sense
+      that [project_out_fml (embed_into_cnd (`Fml f)) = Some f]. *)
+let project_out_fml : cnd -> fml option = function
+  (* (p ? 1 : 0) ==> p *)
+  | `Ite (cnd, `Trm one', `Trm zero') when one == one' && zero == zero' ->
+      Some cnd
+  | _ -> None
+
+(** Embed a conditional term into a formula (associating 0 with false and
+    non-0 with true, lifted over the tree mapping conditional terms to
+    conditional formulas), identity on formulas.
+
+    - [embed_into_fml] is left inverse to [embed_into_cnd] in the sense that
+      [embed_into_fml ((embed_into_cnd (`Fml f)) :> exp) = f].
+    - [embed_into_fml] is not right inverse to [embed_into_cnd] since
+      [embed_into_fml] can only preserve one bit of information from its
+      argument. So in general
+      [(embed_into_cnd (`Fml (embed_into_fml x)) :> exp)] is not equivalent
+      to [x].
+    - The weaker condition that
+      [0 ≠ (embed_into_cnd (`Fml (embed_into_fml x)) :> exp)] iff
+      [0 ≠ x] holds. *)
+let embed_into_fml : exp -> fml = function
+  | `Fml fml -> fml
+  | #cnd as c ->
+      (* Some normalization is necessary for [embed_into_fml] to be left
+         inverse to [embed_into_cnd]. Essentially [0 ≠ (p ? 1 : 0)] needs to
+         normalize to [p], by way of [0 ≠ (p ? 1 : 0)] ==> [(p ? 0 ≠ 1 : 0 ≠
+         0)] ==> [(p ? tt : ff)] ==> [p]. *)
+      let dq0 : trm -> fml = function
+        (* 0 ≠ 0 ==> ff *)
+        | Z _ as z when z == zero -> Ff
+        (* 0 ≠ N ==> tt for N≠0 *)
+        | Z _ -> Tt
+        | t -> Dq (zero, t)
+      in
+      let cond : fml -> fml -> fml -> fml =
+       fun cnd pos neg ->
+        match (pos, neg) with
+        (* (p ? tt : ff) ==> p *)
+        | Tt, Ff -> cnd
+        | _ -> Cond {cnd; pos; neg}
+      in
+      map_cnd cond dq0 c
+
+(** Construct a conditional term, or formula if possible precisely. *)
+let ite : fml -> exp -> exp -> exp =
+ fun cnd thn els ->
+  match (thn, els) with
+  | `Fml pos, `Fml neg -> `Fml (Cond {cnd; pos; neg})
+  | _ -> (
+      let c = `Ite (cnd, embed_into_cnd thn, embed_into_cnd els) in
+      match project_out_fml c with Some f -> `Fml f | None -> c )
+
+(** Map a unary function on terms over an expression. *)
+let ap1 : (trm -> exp) -> exp -> exp =
+ fun f x -> map_cnd ite f (embed_into_cnd x)
+
+let ap1t : (trm -> trm) -> exp -> exp = fun f -> ap1 (fun x -> `Trm (f x))
+
+(** Map a binary function on terms over conditional terms. This yields a
+    conditional tree with the structure from the first argument where each
+    leaf has been replaced by a conditional tree with the structure from the
+    second argument where each leaf has been replaced by the application of
+    the argument binary function to the corresponding leaves from the first
+    and second argument. *)
+let map2_cnd :
+    (fml -> 'a -> 'a -> 'a) -> (trm -> trm -> 'a) -> cnd -> cnd -> 'a =
+ fun f_ite f_trm x y ->
+  map_cnd f_ite (fun x' -> map_cnd f_ite (fun y' -> f_trm x' y') y) x
+
+(** Map a binary function on terms over expressions. *)
+let ap2 : (trm -> trm -> exp) -> exp -> exp -> exp =
+ fun f x y -> map2_cnd ite f (embed_into_cnd x) (embed_into_cnd y)
+
+let ap2t : (trm -> trm -> trm) -> exp -> exp -> exp =
+ fun f -> ap2 (fun x y -> `Trm (f x y))
+
+let ap2f : (trm -> trm -> fml) -> exp -> exp -> fml =
+ fun f x y -> map2_cnd _Cond f (embed_into_cnd x) (embed_into_cnd y)
+
+(** Map a ternary function on terms over conditional terms. *)
+let map3_cnd :
+       (fml -> 'a -> 'a -> 'a)
+    -> (trm -> trm -> trm -> 'a)
+    -> cnd
+    -> cnd
+    -> cnd
+    -> 'a =
+ fun f_ite f_trm x y z ->
+  map_cnd f_ite
+    (fun x' ->
+      map_cnd f_ite (fun y' -> map_cnd f_ite (fun z' -> f_trm x' y' z') z) y
+      )
+    x
+
+(** Map a ternary function on terms over expressions. *)
+let ap3 : (trm -> trm -> trm -> exp) -> exp -> exp -> exp -> exp =
+ fun f x y z ->
+  map3_cnd ite f (embed_into_cnd x) (embed_into_cnd y) (embed_into_cnd z)
+
+let ap3t : (trm -> trm -> trm -> trm) -> exp -> exp -> exp -> exp =
+ fun f -> ap3 (fun x y z -> `Trm (f x y z))
+
+(** Reverse-map an nary function on terms over conditional terms. *)
+let rev_mapN_cnd :
+    (fml -> 'a -> 'a -> 'a) -> (trm list -> 'a) -> cnd list -> 'a =
+ fun f_ite f_trms rev_xs ->
+  let rec loop xs' = function
+    | x :: xs -> map_cnd f_ite (fun x' -> loop (x' :: xs') xs) x
+    | [] -> f_trms xs'
+  in
+  loop [] rev_xs
+
+(** Map an nary function on terms over expressions. *)
+let apNt : (trm list -> trm) -> exp array -> exp =
+ fun f xs ->
+  rev_mapN_cnd ite
+    (fun xs -> `Trm (f xs))
+    (Array.fold ~f:(fun xs x -> embed_into_cnd x :: xs) ~init:[] xs)
+
+(*
+ * Formulas: exposed interface
+ *)
 
 module Formula = struct
-  include Term
+  type t = fml [@@deriving compare, equal, sexp]
 
-  let inject b = b
-  let project e = Some e
-  let tt = true_
-  let ff = false_
-  let cond ~cnd ~pos ~neg = conditional ~cnd ~thn:pos ~els:neg
+  let inject f = `Fml f
+  let project = function `Fml f -> Some f | #cnd as c -> project_out_fml c
+  let ppx = ppx_f
+  let pp = pp_f
+
+  (* constants *)
+
+  let tt = Tt
+  let ff = Ff
+
+  (* comparisons *)
+
+  let eq = ap2f _Eq
+  let dq = ap2f _Dq
+  let lt = ap2f _Lt
+  let le = ap2f _Le
+  let ord = ap2f _Ord
+  let uno = ap2f _Uno
+
+  (* connectives *)
+
+  let not_ = _Not
+  let and_ = _And
+  let or_ = _Or
+  let iff = _Iff
+  let xor = _Xor
+  let imp = _Imp
+  let nimp x y = not_ (imp x y)
+  let cond ~cnd ~pos ~neg = _Cond cnd pos neg
+
+  (** Query *)
+
+  let fv e = fold_vars_f e ~f:Var.Set.add ~init:Var.Set.empty
+  let is_true = function Tt -> true | _ -> false
+  let is_false = function Ff -> true | _ -> false
+
+  (** Traverse *)
+
+  let fold_vars = fold_vars_f
+
+  (** Transform *)
+
+  let map_vars = map_vars_f
+
+  let fold_map_vars ~init e ~f =
+    let s = ref init in
+    let f x =
+      let s', x' = f !s x in
+      s := s' ;
+      x'
+    in
+    let e' = map_vars ~f e in
+    (!s, e')
+
+  let rename s e = map_vars ~f:(Var.Subst.apply s) e
+
+  let disjuncts p =
+    let rec disjuncts_ p ds =
+      match p with
+      | Or (a, b) -> disjuncts_ a (disjuncts_ b ds)
+      | Cond {cnd; pos; neg} ->
+          disjuncts_ (And (cnd, pos)) (disjuncts_ (And (Not cnd, neg)) ds)
+      | d -> d :: ds
+    in
+    disjuncts_ p []
+end
+
+(*
+ * Terms: exposed interface
+ *)
+
+module Term = struct
+  (* Exposed terms are represented as expressions, which allow formulas to
+     appear at toplevel, although semantically these are redundant with
+     their [inject]ion into [trm] proper. This redundancy of representation
+     is allowed in order to avoid churning formulas back and forth between
+     [fml] and [cnd] via [inject] and [project] in cases where formulas only
+     transiently pass through term contexts. The construction functions will
+     convert such a formula [p] into [(p ? 1 : 0)] as soon as it is used as
+     a subterm, so this redundancy is only lazily delaying normalization by
+     one step. *)
+  module T = struct
+    type t = exp [@@deriving compare, equal, sexp]
+  end
+
+  include T
+  module Map = Map.Make (T)
+
+  let ppx = ppx
+  let pp = pp
+
+  (* variables *)
+
+  let var v = `Trm (v : var :> trm)
+
+  (* constants *)
+
+  let zero = `Trm zero
+  let one = `Trm one
+
+  let integer z =
+    if Z.equal Z.zero z then zero
+    else if Z.equal Z.one z then one
+    else `Trm (Z z)
+
+  let rational q = `Trm (Q q)
+
+  let float s =
+    match Q.of_float (Float.of_string s) with
+    | q when Q.is_real q -> rational q
+    | _ | (exception Invalid_argument _) -> `Trm (Float s)
+
+  let label ~parent ~name = `Trm (Label {parent; name})
+
+  (* arithmetic *)
+
+  let neg = ap1t _Neg
+  let add = ap2t _Add
+  let sub = ap2t _Sub
+  let mulq q = ap1t (_Mulq q)
+
+  let mul =
+    ap2 (fun x y ->
+        match x with
+        | Z z -> mulq (Q.of_z z) (`Trm y)
+        | Q q -> mulq q (`Trm y)
+        | _ -> (
+          match y with
+          | Z z -> mulq (Q.of_z z) (`Trm x)
+          | Q q -> mulq q (`Trm x)
+          | _ -> ap2t _Mul (`Trm x) (`Trm y) ) )
+
+  let div = ap2t _Div
+  let rem = ap2t _Rem
+
+  (* sequences *)
+
+  let splat = ap1t _Splat
+  let sized ~seq ~siz = ap2t _Sized seq siz
+  let extract ~seq ~off ~len = ap3t _Extract seq off len
+  let concat elts = apNt (fun es -> _Concat (IArray.of_list es)) elts
+
+  (* records *)
+
+  let select ~rcd ~idx = ap1t (fun r -> _Select r idx) rcd
+  let update ~rcd ~idx ~elt = ap2t (fun r e -> _Update r idx e) rcd elt
+  let record elts = apNt (fun es -> _Record (IArray.of_list es)) elts
+  let rec_record i = `Trm (_RecRecord i)
+
+  (* bitwise *)
+
+  let band = ap2t _BAnd
+  let bor = ap2t _BOr
+  let bxor = ap2t _BXor
+  let bshl = ap2t _BShl
+  let blshr = ap2t _BLshr
+  let bashr = ap2t _BAshr
+
+  (* type conversions *)
+
+  let signed bits = function
+    | `Fml _ as fml when bits = 1 -> fml
+    | arg -> ap1t (_Signed bits) arg
+
+  let unsigned bits = function
+    | `Fml _ as fml when bits = 1 -> fml
+    | arg -> ap1t (_Unsigned bits) arg
+
+  let convert src ~to_:dst arg = ap1t (_Convert src dst) arg
+
+  (* if-then-else *)
+
+  let ite ~cnd ~thn ~els = ite cnd thn els
+
+  (** Destruct *)
+
+  let d_int = function `Trm (Z z) -> Some z | _ -> None
+
+  (** Access *)
+
+  let const_of x =
+    let rec const_of t =
+      let add = Option.map2 ~f:Q.add in
+      let neg = Option.map ~f:Q.neg in
+      match t with
+      | Z z -> Some (Q.of_z z)
+      | Q q -> Some q
+      | Add (x, y) -> add (const_of x) (const_of y)
+      | Sub (x, y) -> add (const_of x) (neg (const_of y))
+      | _ -> None
+    in
+    match x with `Trm t -> const_of t | _ -> None
+
+  (** Traverse *)
+
+  let fold_vars = fold_vars
+
+  (** Transform *)
+
+  let map_vars = map_vars
+
+  let fold_map_vars e ~init ~f =
+    let s = ref init in
+    let f x =
+      let s', x' = f !s x in
+      s := s' ;
+      x'
+    in
+    let e' = map_vars ~f e in
+    (!s, e')
+
+  let rename s e = map_vars ~f:(Var.Subst.apply s) e
+
+  (** Query *)
+
+  let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
 end
 
+(*
+ * Convert to Ses
+ *)
+
+let v_to_ses : var -> Ses.Var.t =
+ fun v -> Ses.Var.identified ~id:(Var.id v) ~name:(Var.name v)
+
+let vs_to_ses : Var.Set.t -> Ses.Var.Set.t =
+ fun vs ->
+  Var.Set.fold vs ~init:Ses.Var.Set.empty ~f:(fun vs v ->
+      Ses.Var.Set.add vs (v_to_ses v) )
+
+let rec t_to_ses : trm -> Ses.Term.t = function
+  | Var {name; id} -> Ses.Term.var (Ses.Var.identified ~name ~id)
+  | Z z -> Ses.Term.integer z
+  | Q q -> Ses.Term.rational q
+  | Neg x -> Ses.Term.neg (t_to_ses x)
+  | Add (x, y) -> Ses.Term.add (t_to_ses x) (t_to_ses y)
+  | Sub (x, y) -> Ses.Term.sub (t_to_ses x) (t_to_ses y)
+  | Mulq (q, x) -> Ses.Term.mulq q (t_to_ses x)
+  | Mul (x, y) -> Ses.Term.mul (t_to_ses x) (t_to_ses y)
+  | Div (x, y) -> Ses.Term.div (t_to_ses x) (t_to_ses y)
+  | Rem (x, y) -> Ses.Term.rem (t_to_ses x) (t_to_ses y)
+  | Select (r, i) -> Ses.Term.select ~rcd:(t_to_ses r) ~idx:i
+  | Update (r, i, e) ->
+      Ses.Term.update ~rcd:(t_to_ses r) ~idx:i ~elt:(t_to_ses e)
+  | Record es -> Ses.Term.record (IArray.map ~f:t_to_ses es)
+  | RecRecord i -> Ses.Term.rec_record i
+  | Splat x -> Ses.Term.splat (t_to_ses x)
+  | Sized {seq; siz} ->
+      Ses.Term.sized ~seq:(t_to_ses seq) ~siz:(t_to_ses siz)
+  | Extract {seq; off; len} ->
+      Ses.Term.extract ~seq:(t_to_ses seq) ~off:(t_to_ses off)
+        ~len:(t_to_ses len)
+  | Concat es ->
+      Ses.Term.concat (IArray.to_array (IArray.map ~f:t_to_ses es))
+  | BAnd (x, y) -> Ses.Term.and_ (t_to_ses x) (t_to_ses y)
+  | BOr (x, y) -> Ses.Term.or_ (t_to_ses x) (t_to_ses y)
+  | BXor (x, y) -> Ses.Term.dq (t_to_ses x) (t_to_ses y)
+  | BShl (x, y) -> Ses.Term.shl (t_to_ses x) (t_to_ses y)
+  | BLshr (x, y) -> Ses.Term.lshr (t_to_ses x) (t_to_ses y)
+  | BAshr (x, y) -> Ses.Term.ashr (t_to_ses x) (t_to_ses y)
+  | Label {parent; name} -> Ses.Term.label ~parent ~name
+  | Float s -> Ses.Term.float s
+  | Signed (n, x) -> Ses.Term.signed n (t_to_ses x)
+  | Unsigned (n, x) -> Ses.Term.unsigned n (t_to_ses x)
+  | Convert {src; dst; arg} -> Ses.Term.convert src ~to_:dst (t_to_ses arg)
+
+let rec f_to_ses : fml -> Ses.Term.t = function
+  | Tt -> Ses.Term.true_
+  | Ff -> Ses.Term.false_
+  | Eq (x, y) -> Ses.Term.eq (t_to_ses x) (t_to_ses y)
+  | Dq (x, y) -> Ses.Term.dq (t_to_ses x) (t_to_ses y)
+  | Lt (x, y) -> Ses.Term.lt (t_to_ses x) (t_to_ses y)
+  | Le (x, y) -> Ses.Term.le (t_to_ses x) (t_to_ses y)
+  | Ord (x, y) -> Ses.Term.ord (t_to_ses x) (t_to_ses y)
+  | Uno (x, y) -> Ses.Term.uno (t_to_ses x) (t_to_ses y)
+  | Not p -> Ses.Term.not_ (f_to_ses p)
+  | And (p, q) -> Ses.Term.and_ (f_to_ses p) (f_to_ses q)
+  | Or (p, q) -> Ses.Term.or_ (f_to_ses p) (f_to_ses q)
+  | Iff (p, q) -> Ses.Term.eq (f_to_ses p) (f_to_ses q)
+  | Xor (p, q) -> Ses.Term.dq (f_to_ses p) (f_to_ses q)
+  | Imp (p, q) -> Ses.Term.le (f_to_ses p) (f_to_ses q)
+  | Cond {cnd; pos; neg} ->
+      Ses.Term.conditional ~cnd:(f_to_ses cnd) ~thn:(f_to_ses pos)
+        ~els:(f_to_ses neg)
+
+let rec to_ses : exp -> Ses.Term.t = function
+  | `Ite (cnd, thn, els) ->
+      Ses.Term.conditional ~cnd:(f_to_ses cnd)
+        ~thn:(to_ses (thn :> exp))
+        ~els:(to_ses (els :> exp))
+  | `Trm t -> t_to_ses t
+  | `Fml f -> f_to_ses f
+
+(*
+ * Convert from Ses
+ *)
+
+let v_of_ses : Ses.Var.t -> var =
+ fun v -> Var.identified ~id:(Ses.Var.id v) ~name:(Ses.Var.name v)
+
+let vs_of_ses : Ses.Var.Set.t -> Var.Set.t =
+ fun vs ->
+  Ses.Var.Set.fold vs ~init:Var.Set.empty ~f:(fun vs v ->
+      Var.Set.add vs (v_of_ses v) )
+
+let rec ap_tt f a = f (of_ses a)
+and ap_ttt f a b = f (of_ses a) (of_ses b)
+and ap_ttf f a b = `Fml (f (of_ses a) (of_ses b))
+
+and ap2 mk_f mk_t a b =
+  match (of_ses a, of_ses b) with
+  | `Fml p, `Fml q -> `Fml (mk_f p q)
+  | x, y -> mk_t x y
+
+and ap2_f mk_f mk_t a b = ap2 mk_f (fun x y -> `Fml (mk_t x y)) a b
+
+and apN mk_f mk_t mk_unit es =
+  match
+    Ses.Term.Set.fold ~init:(None, None) es ~f:(fun (fs, ts) e ->
+        match of_ses e with
+        | `Fml f ->
+            (Some (match fs with None -> f | Some g -> mk_f f g), ts)
+        | t -> (fs, Some (match ts with None -> t | Some u -> mk_t t u)) )
+  with
+  | Some f, Some t -> mk_t t (Formula.inject f)
+  | Some f, None -> `Fml f
+  | None, Some t -> t
+  | None, None -> `Fml mk_unit
+
+and of_ses : Ses.Term.t -> exp =
+ fun t ->
+  let open Term in
+  let open Formula in
+  match t with
+  | Var {id; name} -> var (Var.identified ~id ~name)
+  | Integer {data} -> integer data
+  | Rational {data} -> rational data
+  | Float {data} -> float data
+  | Label {parent; name} -> label ~parent ~name
+  | Ap1 (Signed {bits}, e) -> ap_tt (signed bits) e
+  | Ap1 (Unsigned {bits}, e) -> ap_tt (unsigned bits) e
+  | Ap1 (Convert {src; dst}, e) -> ap_tt (convert src ~to_:dst) e
+  | Ap2 (Eq, d, e) -> ap2_f iff eq d e
+  | Ap2 (Dq, d, e) -> ap2_f xor dq d e
+  | Ap2 (Lt, d, e) -> ap2_f (Fn.flip nimp) lt d e
+  | Ap2 (Le, d, e) -> ap2_f imp le d e
+  | Ap2 (Ord, d, e) -> ap_ttf ord d e
+  | Ap2 (Uno, d, e) -> ap_ttf uno d e
+  | Add sum -> (
+    match Ses.Term.Qset.pop_min_elt sum with
+    | None -> zero
+    | Some (e, q, sum) ->
+        let mul e q = mulq q (of_ses e) in
+        Ses.Term.Qset.fold sum ~init:(mul e q) ~f:(fun e q s ->
+            add (mul e q) s ) )
+  | Mul prod -> (
+    match Ses.Term.Qset.pop_min_elt prod with
+    | None -> one
+    | Some (e, q, prod) ->
+        let rec expn e n =
+          if Z.sign n = 0 then one else mul e (expn e (Z.pred n))
+        in
+        let exp e q =
+          let n = Q.num q in
+          if Z.sign n >= 0 then expn (of_ses e) n
+          else div one (expn (of_ses e) (Z.neg n))
+        in
+        Ses.Term.Qset.fold prod ~init:(exp e q) ~f:(fun e q s ->
+            mul (exp e q) s ) )
+  | Ap2 (Div, d, e) -> ap_ttt div d e
+  | Ap2 (Rem, d, e) -> ap_ttt rem d e
+  | And es -> apN and_ band tt es
+  | Or es -> apN or_ bor ff es
+  | Ap2 (Xor, d, e) -> ap2 xor bxor d e
+  | Ap2 (Shl, d, e) -> ap_ttt bshl d e
+  | Ap2 (Lshr, d, e) -> ap_ttt blshr d e
+  | Ap2 (Ashr, d, e) -> ap_ttt bashr d e
+  | Ap3 (Conditional, cnd, thn, els) -> (
+      let cnd = embed_into_fml (of_ses cnd) in
+      match (of_ses thn, of_ses els) with
+      | `Fml pos, `Fml neg -> `Fml (cond ~cnd ~pos ~neg)
+      | thn, els -> ite ~cnd ~thn ~els )
+  | Ap1 (Splat, byt) -> splat (of_ses byt)
+  | Ap3 (Extract, seq, off, len) ->
+      extract ~seq:(of_ses seq) ~off:(of_ses off) ~len:(of_ses len)
+  | Ap2 (Sized, siz, seq) -> sized ~seq:(of_ses seq) ~siz:(of_ses siz)
+  | ApN (Concat, args) ->
+      concat (IArray.to_array (IArray.map ~f:of_ses args))
+  | Ap1 (Select idx, rcd) -> select ~rcd:(of_ses rcd) ~idx
+  | Ap2 (Update idx, rcd, elt) ->
+      update ~rcd:(of_ses rcd) ~idx ~elt:(of_ses elt)
+  | ApN (Record, elts) ->
+      record (IArray.to_array (IArray.map ~f:of_ses elts))
+  | RecRecord i -> rec_record i
+
+let f_of_ses e = embed_into_fml (of_ses e)
+
+let v_map_ses : (var -> var) -> Ses.Var.t -> Ses.Var.t =
+ fun f x ->
+  let v = v_of_ses x in
+  let v' = f v in
+  if v' == v then x else v_to_ses v'
+
+let ses_map : (Ses.Term.t -> Ses.Term.t) -> exp -> exp =
+ fun f x ->
+  let e = to_ses x in
+  let e' = f e in
+  if e' == e then x else of_ses e'
+
+let f_ses_map : (Ses.Term.t -> Ses.Term.t) -> fml -> fml =
+ fun f x ->
+  let e = f_to_ses x in
+  let e' = f e in
+  if e' == e then x else f_of_ses e'
+
+(*
+ * Contexts
+ *)
+
 module Context = struct
-  include Ses.Equality
+  type t = Ses.Equality.t [@@deriving compare, equal, sexp]
+  type classes = exp list Term.Map.t
+
+  let classes_of_ses clss =
+    Ses.Term.Map.fold clss ~init:Term.Map.empty
+      ~f:(fun ~key:rep ~data:cls clss ->
+        let rep' = of_ses rep in
+        let cls' = List.map ~f:of_ses cls in
+        Term.Map.set ~key:rep' ~data:cls' clss )
+
+  let classes_to_ses clss =
+    Term.Map.fold clss ~init:Ses.Term.Map.empty
+      ~f:(fun ~key:rep ~data:cls clss ->
+        let rep' = to_ses rep in
+        let cls' = List.map ~f:to_ses cls in
+        Ses.Term.Map.set ~key:rep' ~data:cls' clss )
+
+  let classes x = classes_of_ses (Ses.Equality.classes x)
+  let diff_classes x y = classes_of_ses (Ses.Equality.diff_classes x y)
+  let pp = Ses.Equality.pp
+  let pp_classes = Ses.Equality.pp_classes
+
+  let ppx_classes x fs clss =
+    Ses.Equality.ppx_classes
+      (fun v -> x (v_of_ses v))
+      fs (classes_to_ses clss)
+
+  let invariant = Ses.Equality.invariant
+  let true_ = Ses.Equality.true_
+
+  let and_formula vs f x =
+    let vs', x' = Ses.Equality.and_term (vs_to_ses vs) (f_to_ses f) x in
+    (vs_of_ses vs', x')
+
+  let and_ vs x y =
+    let vs', z = Ses.Equality.and_ (vs_to_ses vs) x y in
+    (vs_of_ses vs', z)
 
-  let and_formula = and_term
-  let normalizef = normalize
-  let rename x sub = rename x (Var.Subst.apply sub)
+  let orN vs xs =
+    let vs', z = Ses.Equality.orN (vs_to_ses vs) xs in
+    (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 entails_eq x e f = Ses.Equality.entails_eq x (to_ses e) (to_ses f)
+  let class_of x e = List.map ~f:of_ses (Ses.Equality.class_of x (to_ses e))
+  let normalize x e = ses_map (Ses.Equality.normalize x) e
+  let normalizef x e = f_ses_map (Ses.Equality.normalize x) e
+  let difference x e f = Ses.Equality.difference x (to_ses e) (to_ses f)
+
+  let fold_terms ~init x ~f =
+    Ses.Equality.fold_terms x ~init ~f:(fun s e -> f s (of_ses e))
 
   module Subst = struct
-    include Subst
+    type t = Ses.Equality.Subst.t [@@deriving sexp]
+
+    let pp = Ses.Equality.Subst.pp
+    let is_empty = Ses.Equality.Subst.is_empty
+
+    let fold s ~init ~f =
+      Ses.Equality.Subst.fold s ~init ~f:(fun ~key ~data ->
+          f ~key:(of_ses key) ~data:(of_ses data) )
 
-    let substf = subst
+    let subst s = ses_map (Ses.Equality.Subst.subst s)
+    let substf s = f_ses_map (Ses.Equality.Subst.subst s)
+
+    let partition_valid vs s =
+      let t, ks, u = Ses.Equality.Subst.partition_valid (vs_to_ses vs) s in
+      (t, vs_of_ses ks, u)
   end
 
+  let apply_subst vs s x =
+    let vs', x' = Ses.Equality.apply_subst (vs_to_ses vs) s x in
+    (vs_of_ses vs', x')
+
+  let solve_for_vars vss x =
+    Ses.Equality.solve_for_vars (List.map ~f:vs_to_ses vss) x
+
+  let elim vs x = Ses.Equality.elim (vs_to_ses vs) x
+
   (* Replay debugging *)
 
   type call =
-    | Normalize of t * Term.t
-    | And_formula of Var.Set.t * Formula.t * t
+    | Normalize of t * exp
+    | Normalizef of t * fml
+    | And_formula of Var.Set.t * fml * t
     | And_ of Var.Set.t * t * t
     | OrN of Var.Set.t * t list
     | Rename of t * Var.Subst.t
@@ -129,6 +1271,7 @@ module Context = struct
   let replay c =
     match call_of_sexp (Sexp.of_string c) with
     | Normalize (r, e) -> normalize r e |> ignore
+    | Normalizef (r, e) -> normalizef r e |> ignore
     | And_formula (us, e, r) -> and_formula us e r |> ignore
     | And_ (us, r, s) -> and_ us r s |> ignore
     | OrN (us, rs) -> orN us rs |> ignore
@@ -171,6 +1314,11 @@ module Context = struct
   let normalize r e =
     wrap normalize_tmr (fun () -> normalize r e) (fun () -> Normalize (r, e))
 
+  let normalizef r e =
+    wrap normalize_tmr
+      (fun () -> normalizef r e)
+      (fun () -> Normalizef (r, e))
+
   let and_formula us e r =
     wrap and_formula_tmr
       (fun () -> and_formula us e r)
@@ -200,14 +1348,102 @@ end
  *)
 
 module Term_of_Llair = struct
-  let exp = Ses.Term.of_exp
+  let rec uap_ttt : 'a. (exp -> exp -> 'a) -> _ -> _ -> _ -> 'a =
+   fun f typ a b ->
+    let bits = Llair.Typ.bit_size_of typ in
+    f (Term.unsigned bits (exp a)) (Term.unsigned bits (exp b))
+
+  and uap_ttf (f : exp -> exp -> fml) typ a b = `Fml (uap_ttt f typ a b)
+  and ap_tt : 'a. (exp -> 'a) -> _ -> 'a = fun f a -> f (exp a)
+  and ap_ttt : 'a. (exp -> exp -> 'a) -> _ -> _ -> 'a =
+   fun f a b -> f (exp a) (exp b)
+  and ap_ttf (f : exp -> exp -> fml) a b = `Fml (ap_ttt f a b)
+
+  and ap_fff (f : fml -> fml -> fml) a b =
+    `Fml (f (embed_into_fml (exp a)) (embed_into_fml (exp b)))
+
+  and ap_ffff (f : fml -> fml -> fml -> fml) a b c =
+    `Fml
+      (f
+         (embed_into_fml (exp a))
+         (embed_into_fml (exp b))
+         (embed_into_fml (exp c)))
+
+  and exp : Llair.Exp.t -> exp =
+   fun e ->
+    let open Term in
+    let open Formula in
+    match e with
+    | Reg {name; global; typ= _} -> var (Var.program ~name ~global)
+    | Label {parent; name} -> label ~parent ~name
+    | Integer {typ= _; data} -> integer data
+    | Float {data; typ= _} -> float data
+    | Ap1 (Signed {bits}, _, e) -> ap_tt (signed bits) e
+    | Ap1 (Unsigned {bits}, _, e) -> ap_tt (unsigned bits) e
+    | Ap1 (Convert {src}, dst, e) -> ap_tt (convert src ~to_:dst) e
+    | Ap2 (Eq, Integer {bits= 1; _}, d, e) -> ap_fff iff d e
+    | Ap2 (Dq, Integer {bits= 1; _}, d, e) -> ap_fff xor d e
+    | Ap2 ((Gt | Ugt), Integer {bits= 1; _}, d, e) -> ap_fff nimp d e
+    | Ap2 ((Lt | Ult), Integer {bits= 1; _}, d, e) -> ap_fff nimp e d
+    | Ap2 ((Ge | Uge), Integer {bits= 1; _}, d, e) -> ap_fff imp e d
+    | Ap2 ((Le | Ule), Integer {bits= 1; _}, d, e) -> ap_fff imp d e
+    | Ap2 (Eq, _, d, e) -> ap_ttf eq d e
+    | Ap2 (Dq, _, d, e) -> ap_ttf dq d e
+    | Ap2 (Gt, _, d, e) -> ap_ttf lt e d
+    | Ap2 (Lt, _, d, e) -> ap_ttf lt d e
+    | Ap2 (Ge, _, d, e) -> ap_ttf le e d
+    | Ap2 (Le, _, d, e) -> ap_ttf le d e
+    | Ap2 (Ugt, typ, d, e) -> uap_ttf lt typ e d
+    | Ap2 (Ult, typ, d, e) -> uap_ttf lt typ d e
+    | Ap2 (Uge, typ, d, e) -> uap_ttf le typ e d
+    | Ap2 (Ule, typ, d, e) -> uap_ttf le typ d e
+    | Ap2 (Ord, _, d, e) -> ap_ttf ord d e
+    | Ap2 (Uno, _, d, e) -> ap_ttf uno d e
+    | Ap2 (Add, Integer {bits= 1; _}, d, e) -> ap_fff xor d e
+    | Ap2 (Sub, Integer {bits= 1; _}, d, e) -> ap_fff xor d e
+    | Ap2 (Mul, Integer {bits= 1; _}, d, e) -> ap_fff and_ d e
+    | Ap2 (Add, _, d, e) -> ap_ttt add d e
+    | Ap2 (Sub, _, d, e) -> ap_ttt sub d e
+    | Ap2 (Mul, _, d, e) -> ap_ttt mul d e
+    | Ap2 (Div, _, d, e) -> ap_ttt div d e
+    | Ap2 (Rem, _, d, e) -> ap_ttt rem d e
+    | Ap2 (Udiv, typ, d, e) -> uap_ttt div typ d e
+    | Ap2 (Urem, typ, d, e) -> uap_ttt rem typ d e
+    | Ap2 (And, Integer {bits= 1; _}, d, e) -> ap_fff and_ d e
+    | Ap2 (Or, Integer {bits= 1; _}, d, e) -> ap_fff or_ d e
+    | Ap2 (Xor, Integer {bits= 1; _}, d, e) -> ap_fff xor d e
+    | Ap2 (And, _, d, e) -> ap_ttt band d e
+    | Ap2 (Or, _, d, e) -> ap_ttt bor d e
+    | Ap2 (Xor, _, d, e) -> ap_ttt bxor d e
+    | Ap2 (Shl, _, d, e) -> ap_ttt bshl d e
+    | Ap2 (Lshr, _, d, e) -> ap_ttt blshr d e
+    | Ap2 (Ashr, _, d, e) -> ap_ttt bashr d e
+    | Ap3 (Conditional, Integer {bits= 1; _}, cnd, pos, neg) ->
+        ap_ffff _Cond cnd pos neg
+    | Ap3 (Conditional, _, cnd, thn, els) ->
+        ite ~cnd:(embed_into_fml (exp cnd)) ~thn:(exp thn) ~els:(exp els)
+    | Ap1 (Select idx, _, rcd) -> select ~rcd:(exp rcd) ~idx
+    | Ap2 (Update idx, _, rcd, elt) ->
+        update ~rcd:(exp rcd) ~idx ~elt:(exp elt)
+    | ApN (Record, _, elts) ->
+        record (IArray.to_array (IArray.map ~f:exp elts))
+    | RecRecord (i, _) -> rec_record i
+    | Ap1 (Splat, _, byt) -> splat (exp byt)
 end
 
 module Formula_of_Llair = struct
-  let exp = Term_of_Llair.exp
+  let exp e = embed_into_fml (Term_of_Llair.exp e)
 end
 
 module Var_of_Llair = struct
-  let reg = Ses.Var.of_reg
-  let regs = Ses.Var.Set.of_regs
+  let reg r =
+    match
+      Var.of_exp (Term_of_Llair.exp (r : Llair.Reg.t :> Llair.Exp.t))
+    with
+    | Some v -> v
+    | _ -> violates Llair.Reg.invariant r
+
+  let regs =
+    Llair.Reg.Set.fold ~init:Var.Set.empty ~f:(fun s r ->
+        Var.Set.add s (reg r) )
 end
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index 4faa286e2..ba03fa3e5 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -10,6 +10,7 @@ module Var : sig
   type t [@@deriving compare, equal, sexp]
   type strength = t -> [`Universal | `Existential | `Anonymous] option
 
+  val ppx : strength -> t pp
   val pp : t pp
 
   module Map : Map.S with type key := t
@@ -98,17 +99,22 @@ module rec Term : sig
 
   val const_of : t -> Q.t option
 
-  (** Transform *)
+  (** Query *)
 
-  val rename : Var.Subst.t -> t -> t
+  val fv : t -> Var.Set.t
 
   (** Traverse *)
 
-  val fold_vars : t -> init:'a -> f:('a -> Var.t -> 'a) -> 'a
+  val fold_vars : init:'a -> t -> f:('a -> Var.t -> 'a) -> 'a
 
-  (** Query *)
+  (** Transform *)
 
-  val fv : t -> Var.Set.t
+  val map_vars : f:(Var.t -> Var.t) -> t -> t
+
+  val fold_map_vars :
+    t -> init:'a -> f:('a -> Var.t -> 'a * Var.t) -> 'a * t
+
+  val rename : Var.Subst.t -> t -> t
 end
 
 (** Formulas *)
@@ -140,16 +146,25 @@ and Formula : sig
   val or_ : t -> t -> t
   val cond : cnd:t -> pos:t -> neg:t -> t
 
-  (** Transform *)
-
-  val rename : Var.Subst.t -> t -> t
-  val disjuncts : t -> t list
-
   (** Query *)
 
+  val fv : t -> Var.Set.t
   val is_true : t -> bool
   val is_false : t -> bool
-  val fv : t -> Var.Set.t
+
+  (** Traverse *)
+
+  val fold_vars : init:'a -> t -> f:('a -> Var.t -> 'a) -> 'a
+
+  (** Transform *)
+
+  val map_vars : f:(Var.t -> Var.t) -> t -> t
+
+  val fold_map_vars :
+    init:'a -> t -> f:('a -> Var.t -> 'a * Var.t) -> 'a * t
+
+  val rename : Var.Subst.t -> t -> t
+  val disjuncts : t -> t list
 end
 
 (** Inference System *)
@@ -214,7 +229,7 @@ module Context : sig
       implies [a = b+k], or [None] if [a] and [b] are not equal up to an
       integer offset. *)
 
-  val fold_terms : t -> init:'a -> f:('a -> Term.t -> 'a) -> 'a
+  val fold_terms : init:'a -> t -> f:('a -> Term.t -> 'a) -> 'a
 
   (** Solution Substitutions *)
   module Subst : sig
diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml
index f1a013b1b..aacccb999 100644
--- a/sledge/src/ses/term.ml
+++ b/sledge/src/ses/term.ml
@@ -1040,6 +1040,8 @@ module Var = struct
     | Some v -> v
     | _ -> violates Llair.Reg.invariant r
 
+  let program ~name ~global = Var {name; id= (if global then -1 else 0)}
+
   let fresh name ~wrt =
     let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in
     let x' = Var {name; id= max + 1} in
diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli
index 54f6652c3..64cdc7b3d 100644
--- a/sledge/src/ses/term.mli
+++ b/sledge/src/ses/term.mli
@@ -128,6 +128,7 @@ module Var : sig
   val of_ : term -> t
   val of_term : term -> t option
   val of_reg : Llair.Reg.t -> t
+  val program : name:string -> global:bool -> t
   val fresh : string -> wrt:Set.t -> t * Set.t
 
   val identified : name:string -> id:int -> t
diff --git a/sledge/src/sh_test.ml b/sledge/src/sh_test.ml
index 1c8a66eda..c6d71dea3 100644
--- a/sledge/src/sh_test.ml
+++ b/sledge/src/sh_test.ml
@@ -83,9 +83,9 @@ let%test_module _ =
           ( (  0 = %x_6 ∧ emp)
           ∨ (  ( (  1 = _ = %y_7 ∧ emp) ∨ (  2 = _ ∧ emp) ))
           )
-
+    
         ( (∃ %x_6, %x_7 .   2 = %x_7 ∧ (%x_7 = 2) ∧ emp)
-        ∨ (∃ %x_6 .   1 = %x_6 = %y_7 ∧ ((%x_6 = 1) && (%y_7 = 1)) ∧ emp)
+        ∨ (∃ %x_6 .   1 = %x_6 = %y_7 ∧ ((%x_6 = 1) ∧ (%y_7 = 1)) ∧ emp)
         ∨ (  0 = %x_6 ∧ (%x_6 = 0) ∧ emp)
         ) |}]
 
@@ -108,11 +108,11 @@ let%test_module _ =
           ( (  0 = _ ∧ emp)
           ∨ (  ( (  1 = _ = %y_7 ∧ emp) ∨ (  2 = _ ∧ emp) ))
           )
-
+    
         ( (∃ %x_6, %x_8, %x_9 .   2 = %x_9 ∧ (%x_9 = 2) ∧ emp)
         ∨ (∃ %x_6, %x_8 .
              1 = %y_7 = %x_8
-           ∧ ((%y_7 = 1) && (%x_8 = 1))
+           ∧ ((%x_8 = 1) ∧ (%y_7 = 1))
            ∧ emp)
         ∨ (∃ %x_6 .   0 = %x_6 ∧ (%x_6 = 0) ∧ emp)
         ) |}]
@@ -136,7 +136,7 @@ let%test_module _ =
         ( (  0 = _ ∧ emp)
         ∨ (  ( (  1 = _ = %y_7 ∧ emp) ∨ (  2 = _ ∧ emp) ))
         )
-
+    
         ( (  1 = %y_7 ∧ emp) ∨ (  emp) ∨ (  emp) ) |}]
 
     let%expect_test _ =
@@ -148,9 +148,9 @@ let%test_module _ =
       [%expect
         {|
         ∃ %x_6 .   %x_6 = %x_6^ ∧ (%y_7 + -1) = %y_7^ ∧ emp
-
-          (%y_7 + -1) = %y_7^ ∧ (%y_7^ = (%y_7 + -1)) ∧ emp
-
+    
+          (%y_7 + -1) = %y_7^ ∧ (%y_7^ = ((-1 × 1) + (1 × %y_7))) ∧ emp
+    
           (%y_7 + -1) = %y_7^ ∧ emp |}]
 
     let%expect_test _ =
@@ -173,7 +173,7 @@ let%test_module _ =
         {|
         ∃ %a_1, %c_3, %d_4, %e_5 .
           (⟨8,%a_1⟩^⟨8,%d_4⟩) = %e_5
-        ∧ (⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩))
+        ∧ ((⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩)) ∧ tt)
         ∧ emp
         * ( (  (%x_6 ≠ 0) ∧ emp)
           ∨ (∃ %b_2 .
@@ -182,7 +182,7 @@ let%test_module _ =
              ∧ emp)
           )
 
-          -1 ∧ emp * ( (  -1 ∧ emp) ∨ (  (%x_6 ≠ 0) ∧ emp) )
+          tt ∧ emp * ( (  tt ∧ emp) ∨ (  (%x_6 ≠ 0) ∧ emp) )
 
           ( (  emp) ∨ (  (%x_6 ≠ 0) ∧ emp) ) |}]
   end )
diff --git a/sledge/src/solver_test.ml b/sledge/src/solver_test.ml
index 01b8eb039..5c5d63748 100644
--- a/sledge/src/solver_test.ml
+++ b/sledge/src/solver_test.ml
@@ -196,7 +196,7 @@ let%test_module _ =
             %a_2 = %a0_10
           ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ 16 = %m_8 = %n_9
-          ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
+          ∧ ((16 × 1) + (1 × %k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let%expect_test _ =
       infer_frame
@@ -218,7 +218,7 @@ let%test_module _ =
             %a_2 = %a0_10
           ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ 16 = %m_8 = %n_9
-          ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
+          ∧ ((16 × 1) + (1 × %k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let seg_split_symbolically =
       Sh.star
@@ -236,7 +236,7 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(-8 × %n_9 + 16),%a_3⟩
+            %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 - (8 × %n_9)),%a_3⟩
           * ( (  2 = %n_9 ∧ emp)
             ∨ (  0 = %n_9 ∧ emp)
             ∨ (  1 = %n_9 ∧ emp)
@@ -247,7 +247,7 @@ let%test_module _ =
             ( (  %a_1 = %a_2
                ∧ 2 = %n_9
                ∧ 16 = %m_8
-               ∧ (%l_6 + 16) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
+               ∧ ((16 × 1) + (1 × %l_6)) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
             ∨ (  %a_3 = _
                ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
                ∧ 1 = %n_9
@@ -269,8 +269,8 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            (%n_9 ≤ 2)
-          ∧ %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(-8 × %n_9 + 16),%a_3⟩
+            ((%n_9 ≤ 2) ∧ (tt ∧ tt))
+          ∧ %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 - (8 × %n_9)),%a_3⟩
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame: |}]