Avoid "-" in TSTP variable names

sneeuwballen · Nov 14, 2023 · 7ea2a18 · 7ea2a18
1 parent 0c92b3c
commit 7ea2a18
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 5 deletions.
diff --git a/src/core/HVar.ml b/src/core/HVar.ml
@@ -28,8 +28,14 @@ let[@inline] hash a = Hash.int a.id
 let[@inline] max a b = if a.id < b.id then b else a
 let[@inline] min a b = if a.id < b.id then a else b
 
+let[@inline] is_fresh v = id v < 0
+
 let pp out v = Format.fprintf out "X%d" v.id
-let pp_tstp = pp
+let pp_tstp out v =
+  if is_fresh v
+  then Format.fprintf out "XF%d" (- v.id) (* avoid "-" in variable name *)
+  else Format.fprintf out "X%d" v.id
+
 let to_string v = CCFormat.to_string pp v
 let to_string_tstp = to_string
 
@@ -46,5 +52,3 @@ let fresh_cnt ~counter ~ty () =
   let var = make ~ty !counter in 
   incr counter; 
   var
-
-let[@inline] is_fresh v = id v < 0
diff --git a/src/core/Term.ml b/src/core/Term.ml
@@ -1165,7 +1165,7 @@ module TPTP = struct
         Format.fprintf out "(@[<hv2>^[@[%a@]]:@ (@[%a@])@])"
           (Util.pp_list ~sep:"," pp_db) vars pp_rec bod;
         depth := old_d;
-      | Var i -> Format.fprintf out "X%d" (HVar.id i);
+      | Var i -> Format.fprintf out "%a" HVar.pp_tstp i
     and pp_enclosed out t =
       if Type.is_tType (ty t) then (
         let ty = Type.of_term_unsafe (t :> T.t) in

diff --git a/src/core/Type.ml b/src/core/Type.ml
@@ -313,7 +313,7 @@ module TPTP = struct
     | Builtin Int -> CCFormat.string out "$int"
     | Builtin Rat -> CCFormat.string out "$rat"
     | Builtin Real -> CCFormat.string out "$real"
-    | Var v -> Format.fprintf out "X%d" (HVar.id v)
+    | Var v -> Format.fprintf out "%a" HVar.pp_tstp v
     | DB i -> Format.fprintf out "Tb%d" (depth-i-1)
     | App (p, []) -> ID.pp_tstp out p
     | App (p, args) ->