From 7ea2a185e21e855f5a30ded6e1b920cf25072eac Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Tue, 14 Nov 2023 21:21:08 +0100
Subject: [PATCH] Avoid "-" in TSTP variable names

---
 src/core/HVar.ml | 10 +++++++---
 src/core/Term.ml |  2 +-
 src/core/Type.ml |  2 +-
 3 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/core/HVar.ml b/src/core/HVar.ml
index 1371c031f..f337568f6 100644
--- 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
index 3e2fc30a3..eed14cf75 100644
--- 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
index 1869e05ba..b25d3a8c5 100644
--- 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) ->