diff --git a/sledge/cli/smtlib.ml b/sledge/cli/smtlib.ml index e45a473b2..da13f22af 100644 --- a/sledge/cli/smtlib.ml +++ b/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 diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml index 726287c99..944fd0b31 100644 --- a/sledge/src/fol/trm.ml +++ b/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 diff --git a/sledge/src/fol/var_intf.ml b/sledge/src/fol/var_intf.ml index cd3b8a209..17e7ba1fe 100644 --- a/sledge/src/fol/var_intf.ml +++ b/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 - (** 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 identified : ?name:string -> id:int -> t + (** Create a variable identified by [id] with optional [name]. The [id] + uniquely identifies the variable, and must be positive. *) (** Variable renaming substitutions *) module Subst : Subst.S with type var := t with type set := Set.t diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml index b5e3f84ec..20486ec9c 100644 --- a/sledge/src/llair_to_Fol.ml +++ b/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))