[sledge] Refactor: Move Exp.term to Term.of_exp

Summary: and Reg.var to Var.of_reg

Reviewed By: jvillard

Differential Revision: D21720988

fbshipit-source-id: 8f1ddb1a2

sledge/bin/domain_itv.ml

@@ -173,7 +173,7 @@ let assign reg exp q =
   let lval = apron_var_of_reg reg in
   ( match
       Option.bind
-        ~f:(apron_texpr_of_llair_term (Exp.term exp) q)
+        ~f:(apron_texpr_of_llair_term (Term.of_exp exp) q)
         (apron_typ_of_llair_typ (Reg.typ reg))
     with
   | Some e ->
@@ -196,7 +196,7 @@ let assign reg exp q =
 
 (** block if [e] is known to be false; skip otherwise *)
 let exec_assume q e =
-  match apron_texpr_of_llair_term (Exp.term e) q Texpr1.Int with
+  match apron_texpr_of_llair_term (Term.of_exp e) q Texpr1.Int with
   | Some e ->
       let cond =
         Abstract1.bound_texpr (Lazy.force man) q (Texpr1.of_expr q.env e)

sledge/src/domain_sh.ml

@@ -19,9 +19,9 @@ let simplify q = if !simplify_states then Sh.simplify q else q
 let init globals =
   IArray.fold globals ~init:Sh.emp ~f:(fun q -> function
     | {Global.reg; init= Some (arr, siz)} ->
-        let loc = Term.var (Reg.var reg) in
+        let loc = Term.var (Var.of_reg reg) in
         let len = Term.integer (Z.of_int siz) in
-        let arr = Exp.term arr in
+        let arr = Term.of_exp arr in
         Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr})
     | _ -> q )
 
@@ -34,11 +34,15 @@ let join p q =
 
 let is_false = Sh.is_false
 let dnf = Sh.dnf
-let exec_assume q b = Exec.assume q (Exp.term b) |> Option.map ~f:simplify
+
-let exec_kill q r = Exec.kill q (Reg.var r) |> simplify
+let exec_assume q b =
+  Exec.assume q (Term.of_exp b) |> Option.map ~f:simplify
+
+let exec_kill q r = Exec.kill q (Var.of_reg r) |> simplify
 
 let exec_move q res =
-  Exec.move q (IArray.map res ~f:(fun (r, e) -> (Reg.var r, Exp.term e)))
+  Exec.move q
+    (IArray.map res ~f:(fun (r, e) -> (Var.of_reg r, Term.of_exp e)))
   |> simplify
 
 let exec_inst pre inst =
@@ -46,33 +50,36 @@ let exec_inst pre inst =
   | Move {reg_exps; _} ->
       Some
         (Exec.move pre
-           (IArray.map reg_exps ~f:(fun (r, e) -> (Reg.var r, Exp.term e))))
+           (IArray.map reg_exps ~f:(fun (r, e) ->
+                (Var.of_reg r, Term.of_exp e) )))
   | Load {reg; ptr; len; _} ->
-      Exec.load pre ~reg:(Reg.var reg) ~ptr:(Exp.term ptr)
+      Exec.load pre ~reg:(Var.of_reg reg) ~ptr:(Term.of_exp ptr)
-        ~len:(Exp.term len)
+        ~len:(Term.of_exp len)
   | Store {ptr; exp; len; _} ->
-      Exec.store pre ~ptr:(Exp.term ptr) ~exp:(Exp.term exp)
+      Exec.store pre ~ptr:(Term.of_exp ptr) ~exp:(Term.of_exp exp)
-        ~len:(Exp.term len)
+        ~len:(Term.of_exp len)
   | Memset {dst; byt; len; _} ->
-      Exec.memset pre ~dst:(Exp.term dst) ~byt:(Exp.term byt)
+      Exec.memset pre ~dst:(Term.of_exp dst) ~byt:(Term.of_exp byt)
-        ~len:(Exp.term len)
+        ~len:(Term.of_exp len)
   | Memcpy {dst; src; len; _} ->
-      Exec.memcpy pre ~dst:(Exp.term dst) ~src:(Exp.term src)
+      Exec.memcpy pre ~dst:(Term.of_exp dst) ~src:(Term.of_exp src)
-        ~len:(Exp.term len)
+        ~len:(Term.of_exp len)
   | Memmov {dst; src; len; _} ->
-      Exec.memmov pre ~dst:(Exp.term dst) ~src:(Exp.term src)
+      Exec.memmov pre ~dst:(Term.of_exp dst) ~src:(Term.of_exp src)
-        ~len:(Exp.term len)
+        ~len:(Term.of_exp len)
   | Alloc {reg; num; len; _} ->
-      Exec.alloc pre ~reg:(Reg.var reg) ~num:(Exp.term num)
+      Exec.alloc pre ~reg:(Var.of_reg reg) ~num:(Term.of_exp num)
-        ~len:(Exp.term len)
+        ~len:(Term.of_exp len)
-  | Free {ptr; _} -> Exec.free pre ~ptr:(Exp.term ptr)
+  | Free {ptr; _} -> Exec.free pre ~ptr:(Term.of_exp ptr)
-  | Nondet {reg; _} -> Some (Exec.nondet pre (Option.map ~f:Reg.var reg))
+  | Nondet {reg; _} -> Some (Exec.nondet pre (Option.map ~f:Var.of_reg reg))
   | Abort _ -> Exec.abort pre )
   |> Option.map ~f:simplify
 
 let exec_intrinsic ~skip_throw q r i es =
-  Exec.intrinsic ~skip_throw q (Option.map ~f:Reg.var r) (Reg.var i)
+  Exec.intrinsic ~skip_throw q
-    (List.map ~f:Exp.term es)
+    (Option.map ~f:Var.of_reg r)
+    (Var.of_reg i)
+    (List.map ~f:Term.of_exp es)
   |> Option.map ~f:(Option.map ~f:simplify)
 
 let term_eq_class_has_only_vars_in fvs cong term =
@@ -121,10 +128,12 @@ let and_eqs sub formals actuals q =
 let localize_entry globals actuals formals freturn locals subst pre entry =
   (* Add the formals here to do garbage collection and then get rid of them *)
   let formals_set = Var.Set.of_list formals in
-  let freturn_locals = Reg.Set.vars (Reg.Set.add_option freturn locals) in
+  let freturn_locals =
+    Var.Set.of_regs (Reg.Set.add_option freturn locals)
+  in
   let function_summary_pre =
     garbage_collect entry
-      ~wrt:(Var.Set.union formals_set (Reg.Set.vars globals))
+      ~wrt:(Var.Set.union formals_set (Var.Set.of_regs globals))
   in
   [%Trace.info "function summary pre %a" pp function_summary_pre] ;
   let foot = Sh.exists formals_set function_summary_pre in
@@ -153,10 +162,12 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
       (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Reg.pp)
       (List.rev formals) Reg.Set.pp locals Reg.Set.pp globals pp q]
   ;
-  let actuals = List.map ~f:Exp.term actuals in
+  let actuals = List.map ~f:Term.of_exp actuals in
-  let areturn = Option.map ~f:Reg.var areturn in
+  let areturn = Option.map ~f:Var.of_reg areturn in
-  let formals = List.map ~f:Reg.var formals in
+  let formals = List.map ~f:Var.of_reg formals in
-  let freturn_locals = Reg.Set.vars (Reg.Set.add_option freturn locals) in
+  let freturn_locals =
+    Var.Set.of_regs (Reg.Set.add_option freturn locals)
+  in
   let modifs = Var.Set.of_option areturn in
   (* quantify modifs, their current value will be overwritten and so does
      not need to be saved in the freshening renaming *)
@@ -191,7 +202,7 @@ let post locals _ q =
   [%Trace.call fun {pf} ->
     pf "@[<hv>locals: {@[%a@]}@ q: %a@]" Reg.Set.pp locals Sh.pp q]
   ;
-  Sh.exists (Reg.Set.vars locals) q |> simplify
+  Sh.exists (Var.Set.of_regs locals) q |> simplify
   |>
   [%Trace.retn fun {pf} -> pf "%a" Sh.pp]
 
@@ -207,8 +218,8 @@ let retn formals freturn {areturn; subst; frame} q =
       (Option.pp "@ areturn: %a" Var.pp)
       areturn Var.Subst.pp (Var.Subst.invert subst) pp q pp frame]
   ;
-  let formals = List.map ~f:Reg.var formals in
+  let formals = List.map ~f:Var.of_reg formals in
-  let freturn = Option.map ~f:Reg.var freturn in
+  let freturn = Option.map ~f:Var.of_reg freturn in
   let inv_subst = Var.Subst.invert subst in
   let q, inv_subst =
     match areturn with
@@ -253,8 +264,8 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
     pf "formals %a@ entry: %a@ current: %a" Reg.Set.pp formals pp entry pp
       post]
   ;
-  let locals = Reg.Set.vars locals in
+  let locals = Var.Set.of_regs locals in
-  let formals = Reg.Set.vars formals in
+  let formals = Var.Set.of_regs formals in
   let foot = Sh.exists locals entry in
   let foot, subst = Sh.freshen ~wrt:(Var.Set.union foot.us post.us) foot in
   let restore_formals q =

sledge/src/domain_used_globals.ml

@@ -23,9 +23,7 @@ let is_false _ = false
 let post _ _ state = state
 let retn _ _ from_call post = Reg.Set.union from_call post
 let dnf t = [t]
-
+let add_if_global gs v = if Reg.is_global v then Reg.Set.add gs v else gs
-let add_if_global gs v =
-  if Var.is_global (Reg.var v) then Reg.Set.add gs v else gs
 
 let used_globals ?(init = empty) exp =
   Exp.fold_regs exp ~init ~f:add_if_global

sledge/src/exp.ml

@@ -79,58 +79,6 @@ include T
 module Set = struct include Set.Make (T) include Provide_of_sexp (T) end
 module Map = Map.Make (T)
 
-let unsigned typ = Term.unsigned (Typ.bit_size_of typ)
-
-let rec term = function
-  | Reg {name; global; typ= _} ->
-      Term.var (Var.program ?global:(Option.some_if global ()) name)
-  | Nondet {msg; typ= _} -> Term.nondet msg
-  | Label {parent; name} -> Term.label ~parent ~name
-  | Integer {data; typ= _} -> Term.integer data
-  | Float {data; typ= _} -> Term.float data
-  | Ap1 (Signed {bits}, _, x) -> Term.signed bits (term x)
-  | Ap1 (Unsigned {bits}, _, x) -> Term.unsigned bits (term x)
-  | Ap1 (Convert {src}, dst, exp) -> Term.convert src ~to_:dst (term exp)
-  | Ap2 (Eq, _, x, y) -> Term.eq (term x) (term y)
-  | Ap2 (Dq, _, x, y) -> Term.dq (term x) (term y)
-  | Ap2 (Gt, _, x, y) -> Term.lt (term y) (term x)
-  | Ap2 (Ge, _, x, y) -> Term.le (term y) (term x)
-  | Ap2 (Lt, _, x, y) -> Term.lt (term x) (term y)
-  | Ap2 (Le, _, x, y) -> Term.le (term x) (term y)
-  | Ap2 (Ugt, typ, x, y) ->
-      Term.lt (unsigned typ (term y)) (unsigned typ (term x))
-  | Ap2 (Uge, typ, x, y) ->
-      Term.le (unsigned typ (term y)) (unsigned typ (term x))
-  | Ap2 (Ult, typ, x, y) ->
-      Term.lt (unsigned typ (term x)) (unsigned typ (term y))
-  | Ap2 (Ule, typ, x, y) ->
-      Term.le (unsigned typ (term x)) (unsigned typ (term y))
-  | Ap2 (Ord, _, x, y) -> Term.ord (term x) (term y)
-  | Ap2 (Uno, _, x, y) -> Term.uno (term x) (term y)
-  | Ap2 (Add, _, x, y) -> Term.add (term x) (term y)
-  | Ap2 (Sub, _, x, y) -> Term.sub (term x) (term y)
-  | Ap2 (Mul, _, x, y) -> Term.mul (term x) (term y)
-  | Ap2 (Div, _, x, y) -> Term.div (term x) (term y)
-  | Ap2 (Rem, _, x, y) -> Term.rem (term x) (term y)
-  | Ap2 (Udiv, typ, x, y) ->
-      Term.div (unsigned typ (term x)) (unsigned typ (term y))
-  | Ap2 (Urem, typ, x, y) ->
-      Term.rem (unsigned typ (term x)) (unsigned typ (term y))
-  | Ap2 (And, _, x, y) -> Term.and_ (term x) (term y)
-  | Ap2 (Or, _, x, y) -> Term.or_ (term x) (term y)
-  | Ap2 (Xor, _, x, y) -> Term.xor (term x) (term y)
-  | Ap2 (Shl, _, x, y) -> Term.shl (term x) (term y)
-  | Ap2 (Lshr, _, x, y) -> Term.lshr (term x) (term y)
-  | Ap2 (Ashr, _, x, y) -> Term.ashr (term x) (term y)
-  | Ap3 (Conditional, _, cnd, thn, els) ->
-      Term.conditional ~cnd:(term cnd) ~thn:(term thn) ~els:(term els)
-  | Ap1 (Splat, _, byt) -> Term.splat (term byt)
-  | ApN (Record, _, elts) -> Term.record (IArray.map ~f:term elts)
-  | Ap1 (Select idx, _, rcd) -> Term.select ~rcd:(term rcd) ~idx
-  | Ap2 (Update idx, _, rcd, elt) ->
-      Term.update ~rcd:(term rcd) ~idx ~elt:(term elt)
-  | RecRecord (i, _) -> Term.rec_record i
-
 let pp_op2 fs op =
   let pf fmt = Format.fprintf fs fmt in
   match op with
@@ -167,10 +115,8 @@ let rec pp fs exp =
     Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
   in
   match exp with
-  | Reg {name} -> (
+  | Reg {name; global= true} -> pf "%@%s" name
-    match Var.of_term (term exp) with
+  | Reg {name; global= false} -> pf "%%%s" name
-    | Some v when Var.is_global v -> pf "%@%s" name
-    | _ -> pf "%%%s" name )
   | Nondet {msg} -> pf "nondet \"%s\"" msg
   | Label {name} -> pf "%s" name
   | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null"
@@ -332,18 +278,10 @@ module Reg = struct
 
   let pp = pp
 
-  let var r =
-    match Var.of_term (term r) with
-    | Some v -> v
-    | _ -> violates invariant r
-
   module Set = struct
     include Set
 
     let pp = Set.pp pp_exp
-
-    let vars =
-      Set.fold ~init:Var.Set.empty ~f:(fun s r -> Var.Set.add s (var r))
   end
 
   module Map = Map
@@ -364,7 +302,8 @@ module Reg = struct
     match x with Reg _ -> invariant x | _ -> assert false
 
   let name = function Reg x -> x.name | r -> violates invariant r
-  let typ r = match r with Reg x -> x.typ | _ -> violates invariant r
+  let typ = function Reg x -> x.typ | r -> violates invariant r
+  let is_global = function Reg x -> x.global | r -> violates invariant r
 
   let of_exp = function
     | Reg _ as e -> Some (e |> check invariant)

sledge/src/exp.mli

@@ -102,7 +102,6 @@ module Reg : sig
     val sexp_of_t : t -> Sexp.t
     val t_of_sexp : Sexp.t -> t
     val pp : t pp
-    val vars : t -> Var.Set.t
   end
 
   module Map : Map.S with type key := t
@@ -115,9 +114,9 @@ module Reg : sig
 
   val of_exp : exp -> t option
   val program : ?global:unit -> Typ.t -> string -> t
-  val var : t -> Var.t
   val name : t -> string
   val typ : t -> Typ.t
+  val is_global : t -> bool
 end
 
 (** Construct *)
@@ -191,6 +190,5 @@ val fold_regs : t -> init:'a -> f:('a -> Reg.t -> 'a) -> 'a
 
 (** Query *)
 
-val term : t -> Term.t
 val is_true : t -> bool
 val is_false : t -> bool

sledge/src/exp_test.ml

@@ -14,7 +14,7 @@ let%test_module _ =
     open Exp
 
     let pp e =
-      Format.printf "@\n{desc= %a; term= %a}@." pp e Term.pp (Exp.term e)
+      Format.printf "@\n{desc= %a; term= %a}@." pp e Term.pp (Term.of_exp e)
 
     let ( ! ) i = integer Typ.siz (Z.of_int i)
 

sledge/src/global.ml

@@ -28,6 +28,6 @@ let invariant g =
   let@ () = Invariant.invariant [%here] g [%sexp_of: t] in
   let {reg} = g in
   assert (Typ.is_sized (Reg.typ reg)) ;
-  assert (Var.is_global (Reg.var reg))
+  assert (Reg.is_global reg)
 
 let mk ?init reg loc = {reg; init; loc} |> check invariant

sledge/src/term.ml

@@ -320,116 +320,6 @@ let invariant e =
   | _ -> ()
   [@@warning "-9"]
 
-(** Variables are the terms constructed by [Var] *)
-module Var = struct
-  include T
-
-  let pp = pp
-
-  type strength = t -> [`Universal | `Existential | `Anonymous] option
-
-  module Map = Map
-
-  module Set = struct
-    include Set
-
-    let pp vs = Set.pp pp_t vs
-    let ppx strength vs = Set.pp (ppx strength) vs
-
-    let pp_xs fs xs =
-      if not (is_empty xs) then
-        Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs
-  end
-
-  let invariant x =
-    let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
-    match x with Var _ -> invariant x | _ -> assert false
-
-  let id = function Var v -> v.id | x -> violates invariant x
-  let name = function Var v -> v.name | x -> violates invariant x
-  let is_global = function Var v -> v.id = -1 | x -> violates invariant x
-  let of_ = function Var _ as v -> v | _ -> invalid_arg "Var.of_"
-
-  let of_term = function
-    | Var _ as v -> Some (v |> check invariant)
-    | _ -> None
-
-  let program ?global name =
-    Var {name; id= (if Option.is_some 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}
-
-  (** Variable renaming substitutions *)
-  module Subst = struct
-    type t = T.t Map.t [@@deriving compare, equal, sexp_of]
-
-    let t_of_sexp = Map.t_of_sexp T.t_of_sexp
-
-    let invariant s =
-      let@ () = Invariant.invariant [%here] s [%sexp_of: t] in
-      let domain, range =
-        Map.fold s ~init:(Set.empty, Set.empty)
-          ~f:(fun ~key ~data (domain, range) ->
-            assert (not (Set.mem range data)) ;
-            (Set.add domain key, Set.add range data) )
-      in
-      assert (Set.disjoint domain range)
-
-    let pp = Map.pp pp_t pp_t
-    let empty = Map.empty
-    let is_empty = Map.is_empty
-
-    let freshen vs ~wrt =
-      let xs = Set.inter wrt vs in
-      ( if Set.is_empty xs then empty
-      else
-        let wrt = Set.union wrt vs in
-        Set.fold xs ~init:(empty, wrt) ~f:(fun (sub, wrt) x ->
-            let x', wrt = fresh (name x) ~wrt in
-            let sub = Map.add_exn sub ~key:x ~data:x' in
-            (sub, wrt) )
-        |> fst )
-      |> check invariant
-
-    let fold sub ~init ~f =
-      Map.fold sub ~init ~f:(fun ~key ~data s -> f key data s)
-
-    let invert sub =
-      Map.fold sub ~init:empty ~f:(fun ~key ~data sub' ->
-          Map.add_exn sub' ~key:data ~data:key )
-      |> check invariant
-
-    let restrict sub vs =
-      Map.filter_keys ~f:(Set.mem vs) sub |> check invariant
-
-    let domain sub =
-      Map.fold sub ~init:Set.empty ~f:(fun ~key ~data:_ domain ->
-          Set.add domain key )
-
-    let range sub =
-      Map.fold sub ~init:Set.empty ~f:(fun ~key:_ ~data range ->
-          Set.add range data )
-
-    let apply sub v = Map.find sub v |> Option.value ~default:v
-
-    let apply_set sub vs =
-      Map.fold sub ~init:vs ~f:(fun ~key ~data vs ->
-          let vs' = Set.remove vs key in
-          if vs' == vs then vs
-          else (
-            assert (not (Set.equal vs' vs)) ;
-            Set.add vs' data ) )
-      |> check (fun vs' ->
-             assert (Set.disjoint (domain sub) vs') ;
-             assert (Set.is_subset (range sub) ~of_:vs') )
-  end
-end
-
 (** Construct *)
 
 (* variables *)
@@ -1089,6 +979,169 @@ let eq_concat (siz, arr) ms =
   eq (memory ~siz ~arr)
     (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms))
 
+let rec binary mk x y = mk (of_exp x) (of_exp y)
+
+and ubinary mk typ x y =
+  let unsigned typ = unsigned (Typ.bit_size_of typ) in
+  mk (unsigned typ (of_exp x)) (unsigned typ (of_exp y))
+
+and of_exp e =
+  match (e : Exp.t) with
+  | Reg {name; global; typ= _} -> Var {name; id= (if global then -1 else 0)}
+  | Nondet {msg; typ= _} -> nondet msg
+  | Label {parent; name} -> label ~parent ~name
+  | Integer {data; typ= _} -> integer data
+  | Float {data; typ= _} -> float data
+  | Ap1 (Signed {bits}, _, x) -> signed bits (of_exp x)
+  | Ap1 (Unsigned {bits}, _, x) -> unsigned bits (of_exp x)
+  | Ap1 (Convert {src}, dst, exp) -> convert src ~to_:dst (of_exp exp)
+  | Ap2 (Eq, _, x, y) -> binary eq x y
+  | Ap2 (Dq, _, x, y) -> binary dq x y
+  | Ap2 (Gt, _, x, y) -> binary lt y x
+  | Ap2 (Ge, _, x, y) -> binary le y x
+  | Ap2 (Lt, _, x, y) -> binary lt x y
+  | Ap2 (Le, _, x, y) -> binary le x y
+  | Ap2 (Ugt, typ, x, y) -> ubinary lt typ y x
+  | Ap2 (Uge, typ, x, y) -> ubinary le typ y x
+  | Ap2 (Ult, typ, x, y) -> ubinary lt typ x y
+  | Ap2 (Ule, typ, x, y) -> ubinary le typ x y
+  | Ap2 (Ord, _, x, y) -> binary ord x y
+  | Ap2 (Uno, _, x, y) -> binary uno x y
+  | Ap2 (Add, _, x, y) -> binary add x y
+  | Ap2 (Sub, _, x, y) -> binary sub x y
+  | Ap2 (Mul, _, x, y) -> binary mul x y
+  | Ap2 (Div, _, x, y) -> binary div x y
+  | Ap2 (Rem, _, x, y) -> binary rem x y
+  | Ap2 (Udiv, typ, x, y) -> ubinary div typ x y
+  | Ap2 (Urem, typ, x, y) -> ubinary rem typ x y
+  | Ap2 (And, _, x, y) -> binary and_ x y
+  | Ap2 (Or, _, x, y) -> binary or_ x y
+  | Ap2 (Xor, _, x, y) -> binary xor x y
+  | Ap2 (Shl, _, x, y) -> binary shl x y
+  | Ap2 (Lshr, _, x, y) -> binary lshr x y
+  | Ap2 (Ashr, _, x, y) -> binary ashr x y
+  | Ap3 (Conditional, _, cnd, thn, els) ->
+      conditional ~cnd:(of_exp cnd) ~thn:(of_exp thn) ~els:(of_exp els)
+  | Ap1 (Splat, _, byt) -> splat (of_exp byt)
+  | ApN (Record, _, elts) -> record (IArray.map ~f:of_exp elts)
+  | Ap1 (Select idx, _, rcd) -> select ~rcd:(of_exp rcd) ~idx
+  | Ap2 (Update idx, _, rcd, elt) ->
+      update ~rcd:(of_exp rcd) ~idx ~elt:(of_exp elt)
+  | RecRecord (i, _) -> rec_record i
+
+(** Variables are the terms constructed by [Var] *)
+module Var = struct
+  include T
+
+  let pp = pp
+
+  type strength = t -> [`Universal | `Existential | `Anonymous] option
+
+  let invariant x =
+    let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
+    match x with Var _ -> invariant x | _ -> assert false
+
+  let id = function Var v -> v.id | x -> violates invariant x
+  let name = function Var v -> v.name | x -> violates invariant x
+  let of_ = function Var _ as v -> v | _ -> invalid_arg "Var.of_"
+
+  let of_term = function
+    | Var _ as v -> Some (v |> check invariant)
+    | _ -> None
+
+  let of_reg r =
+    match of_term (of_exp (r : Reg.t :> Exp.t)) with
+    | Some v -> v
+    | _ -> violates Reg.invariant r
+
+  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}
+
+  module Map = Map
+
+  module Set = struct
+    include Set
+
+    let pp vs = Set.pp pp_t vs
+    let ppx strength vs = Set.pp (ppx strength) vs
+
+    let pp_xs fs xs =
+      if not (is_empty xs) then
+        Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs
+
+    let of_regs = Reg.Set.fold ~init:empty ~f:(fun s r -> add s (of_reg r))
+  end
+
+  (** Variable renaming substitutions *)
+  module Subst = struct
+    type t = T.t Map.t [@@deriving compare, equal, sexp_of]
+
+    let t_of_sexp = Map.t_of_sexp T.t_of_sexp
+
+    let invariant s =
+      let@ () = Invariant.invariant [%here] s [%sexp_of: t] in
+      let domain, range =
+        Map.fold s ~init:(Set.empty, Set.empty)
+          ~f:(fun ~key ~data (domain, range) ->
+            assert (not (Set.mem range data)) ;
+            (Set.add domain key, Set.add range data) )
+      in
+      assert (Set.disjoint domain range)
+
+    let pp = Map.pp pp_t pp_t
+    let empty = Map.empty
+    let is_empty = Map.is_empty
+
+    let freshen vs ~wrt =
+      let xs = Set.inter wrt vs in
+      ( if Set.is_empty xs then empty
+      else
+        let wrt = Set.union wrt vs in
+        Set.fold xs ~init:(empty, wrt) ~f:(fun (sub, wrt) x ->
+            let x', wrt = fresh (name x) ~wrt in
+            let sub = Map.add_exn sub ~key:x ~data:x' in
+            (sub, wrt) )
+        |> fst )
+      |> check invariant
+
+    let fold sub ~init ~f =
+      Map.fold sub ~init ~f:(fun ~key ~data s -> f key data s)
+
+    let invert sub =
+      Map.fold sub ~init:empty ~f:(fun ~key ~data sub' ->
+          Map.add_exn sub' ~key:data ~data:key )
+      |> check invariant
+
+    let restrict sub vs =
+      Map.filter_keys ~f:(Set.mem vs) sub |> check invariant
+
+    let domain sub =
+      Map.fold sub ~init:Set.empty ~f:(fun ~key ~data:_ domain ->
+          Set.add domain key )
+
+    let range sub =
+      Map.fold sub ~init:Set.empty ~f:(fun ~key:_ ~data range ->
+          Set.add range data )
+
+    let apply sub v = Map.find sub v |> Option.value ~default:v
+
+    let apply_set sub vs =
+      Map.fold sub ~init:vs ~f:(fun ~key ~data vs ->
+          let vs' = Set.remove vs key in
+          if vs' == vs then vs
+          else (
+            assert (not (Set.equal vs' vs)) ;
+            Set.add vs' data ) )
+      |> check (fun vs' ->
+             assert (Set.disjoint (domain sub) vs') ;
+             assert (Set.is_subset (range sub) ~of_:vs') )
+  end
+end
+
 (** Transform *)
 
 let map e ~f =

sledge/src/term.mli

@@ -118,6 +118,7 @@ module Var : sig
     val ppx : strength -> t pp
     val pp : t pp
     val pp_xs : t pp
+    val of_regs : Reg.Set.t -> t
   end
 
   val pp : t pp
@@ -126,10 +127,9 @@ module Var : sig
 
   val name : t -> string
   val id : t -> int
-  val is_global : t -> bool
   val of_ : term -> t
   val of_term : term -> t option
-  val program : ?global:unit -> string -> t
+  val of_reg : Reg.t -> t
   val fresh : string -> wrt:Set.t -> t * Set.t
 
   val identified : name:string -> id:int -> t
@@ -238,6 +238,9 @@ val select : rcd:t -> idx:int -> t
 val update : rcd:t -> idx:int -> elt:t -> t
 val rec_record : int -> t
 
+(* convert *)
+val of_exp : Exp.t -> t
+
 (** Transform *)
 
 val map : t -> f:(t -> t) -> t

sledge/src/term_test.ml

@@ -40,7 +40,7 @@ let%test_module _ =
 
     let%test "unsigned boolean overflow" =
       is_true
-        (Exp.term
+        (Term.of_exp
            (Exp.uge
               (Exp.integer Typ.bool Z.minus_one)
               (Exp.signed 1 (Exp.integer Typ.siz Z.one) ~to_:Typ.bool)))