[sledge] Use (negated) register ids instead of 0 for program vars

Summary:
Variable ids are currently unique non-negative integers, and register
ids are unique positive integers, so using register ids negated as
variable ids yields a situation where all variable ids are unique.

Reviewed By: jvillard

Differential Revision: D26250544

fbshipit-source-id: 9e47e9776

sledge/src/fol/trm.ml

@@ -121,16 +121,16 @@ end = struct
     if x == y then 0
     else
       match (x, y) with
-      | Var {id= 0; name= s}, Var {id= 0; name= t} -> String.compare s t
-      | Var {id= i; name= _}, Var {id= j; name= _} -> Int.compare i j
+      | Var {id= i; name= s}, Var {id= j; name= t} ->
+          if i < 0 && j < 0 then String.compare s t else Int.compare i j
       | _ -> compare x y
 
   let equal x y =
     x == y
     ||
     match (x, y) with
-    | Var {id= 0; name= s}, Var {id= 0; name= t} -> String.equal s t
-    | Var {id= i; name= _}, Var {id= j; name= _} -> Int.equal i j
+    | Var {id= i; name= s}, Var {id= j; name= t} ->
+        if i < 0 && j < 0 then String.equal s t else Int.equal i j
     | _ -> equal x y
 
   (* nul-terminated string value represented by a concatenation *)

sledge/src/fol/var0.ml

@@ -17,15 +17,13 @@ module Make (T : REPR) = struct
     let ppx strength ppf v =
       let id = id v in
       let name = name v in
-      let pp_id ppf id = if id <> 0 then Format.fprintf ppf "_%d" id in
-      match strength v with
-      | None ->
-          if id = 0 then Trace.pp_styled `Bold "%%%s" ppf name
-          else Format.fprintf ppf "%%%s%a" name pp_id id
-      | Some `Universal -> Trace.pp_styled `Bold "%%%s%a" ppf name pp_id id
-      | Some `Existential ->
-          Trace.pp_styled `Cyan "%%%s%a" ppf name pp_id id
-      | Some `Anonymous -> Trace.pp_styled `Cyan "_" ppf
+      if id < 0 then Trace.pp_styled `Bold "%%%s!%i" ppf name (-id)
+      else
+        match strength v with
+        | None -> Format.fprintf ppf "%%%s_%i" name id
+        | Some `Universal -> Trace.pp_styled `Bold "%%%s_%i" ppf name id
+        | Some `Existential -> Trace.pp_styled `Cyan "%%%s_%i" ppf name id
+        | Some `Anonymous -> Trace.pp_styled `Cyan "_" ppf
 
     let pp = ppx (fun _ -> None)
   end
@@ -51,11 +49,16 @@ module Make (T : REPR) = struct
   end
 
   let fresh name ~wrt =
-    let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in
+    let max =
+      match Set.max_elt wrt with None -> 0 | Some m -> max 0 (id m)
+    in
     let x' = make ~id:(max + 1) ~name in
     (x', Set.add x' wrt)
 
-  let program ~name = make ~id:0 ~name
+  let program ~name ~id =
+    assert (id > 0) ;
+    make ~id:(-id) ~name
+
   let identified ~name ~id = make ~id ~name
 
   (** Variable renaming substitutions *)

sledge/src/fol/var_intf.ml

@@ -39,7 +39,7 @@ module type VAR = sig
 
   val id : t -> int
   val name : t -> string
-  val program : name:string -> t
+  val program : name:string -> id:int -> t
   val fresh : string -> wrt:Set.t -> t * Set.t
 
   val identified : name:string -> id:int -> t

sledge/src/llair/exp.ml

@@ -295,6 +295,7 @@ module Reg = struct
     let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
     match x with Reg _ -> invariant x | _ -> assert false
 
+  let id = function Reg x -> x.id | r -> violates invariant r
   let name = function Reg x -> x.name | r -> violates invariant r
   let typ = function Reg x -> x.typ | r -> violates invariant r
 

sledge/src/llair/exp.mli

@@ -113,6 +113,7 @@ module Reg : sig
 
   val of_exp : exp -> t option
   val mk : Typ.t -> int -> string -> t
+  val id : t -> int
   val name : t -> string
   val typ : t -> Typ.t
 end

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)
+let reg r = Var.program ~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; typ= _} -> T.var (Var.program ~name)
+  | Reg {name; id; typ= _} -> T.var (Var.program ~name ~id)
   | Global {name; typ= _} | Function {name; typ= _} -> uconst name
   | Label {parent; name} ->
       uap0 (Funsym.uninterp ("label_" ^ parent ^ "_" ^ name))