[sledge] Simplify Var by combining `program` and `identified` variables

Summary:
The only difference between `program` and `identified` variables is
terminology, technically they are redundant.

Reviewed By: jvillard

Differential Revision: D26451308

fbshipit-source-id: eb4e7be43

sledge/cli/smtlib.ml

@@ -31,7 +31,7 @@ let pop () =
 let reset () = stack := init_stack
 
 let id =
-  let count = ref (-1) in
+  let count = ref 0 in
   fun () ->
     incr count ;
     !count

sledge/src/fol/trm.ml

@@ -167,11 +167,10 @@ module Var = struct
 
     let freshen v ~wrt = fresh (name v) ~wrt
 
-    let program ?(name = "") ~id =
+    let identified ?(name = "") ~id =
       assert (id > 0) ;
       make ~id:(id - Int.max_int) ~name
 
-    let identified ~name ~id = make ~id ~name
     let of_ v = v |> check invariant
     let of_trm = function Var _ as v -> Some v | _ -> None
   end

sledge/src/fol/var_intf.ml

@@ -31,19 +31,11 @@ module type S = sig
 
   val id : t -> int
   val name : t -> string
-
-  val program : ?name:string -> id:int -> t
-  (** Create a program variable with [id] and optional [name]. The [id]
-      uniquely identifies the variable, and must be positive. *)
-
   val fresh : string -> wrt:Set.t -> t * Set.t
 
-  val identified : name:string -> id:int -> t
+  val identified : ?name:string -> id:int -> t
-  (** Variable with the given [id]. Variables are compared by [id] alone,
+  (** Create a variable identified by [id] with optional [name]. The [id]
-      [name] is used only for printing. The only way to ensure [identified]
+      uniquely identifies the variable, and must be positive. *)
-      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))]. *)
 
   (** Variable renaming substitutions *)
   module Subst : Subst.S with type var := t with type set := Set.t

sledge/src/llair_to_Fol.ml

@@ -16,7 +16,7 @@ let lookup_func lookup term =
 
 let uconst name = T.apply (Funsym.uninterp name) [||]
 let global g = uconst (Llair.Global.name g)
-let reg r = Var.program ~name:(Llair.Reg.name r) ~id:(Llair.Reg.id r)
+let reg r = Var.identified ~name:(Llair.Reg.name r) ~id:(Llair.Reg.id r)
 let regs rs = Var.Set.of_iter (Iter.map ~f:reg (Llair.Reg.Set.to_iter rs))
 let uap0 f = T.apply f [||]
 let uap1 f a = T.apply f [|a|]
@@ -66,7 +66,7 @@ and term : Llair.Exp.t -> T.t =
       F.inject
         (F.cond ~cnd:(formula cnd) ~pos:(formula pos) ~neg:(formula neg))
   (* terms *)
-  | Reg {name; id; typ= _} -> T.var (Var.program ~name ~id)
+  | Reg {name; id; typ= _} -> T.var (Var.identified ~name ~id)
   | Global {name; typ= _} | Function {name; typ= _} -> uconst name
   | Label {parent; name} ->
       uap0 (Funsym.uninterp ("label_" ^ parent ^ "_" ^ name))