Quoted identifiers

src/lib/structures/symbols.ml

@@ -294,8 +294,25 @@ let string_of_form f = match f with
   | F_Iff -> "<->"
   | F_Xor -> "xor"
 
+let name_to_string =
+  let no_need_to_quote s =
+    String.length s > 0 &&
+    (match s.[0] with | '0'..'9' -> false | _ -> true) &&
+    String.for_all
+      (function
+        | 'a' .. 'z'
+        | 'A' .. 'Z'
+        | '0' .. '9'
+        | '~' | '!' | '@' | '$' | '%' | '^' | '&'
+        | '*' | '_' | '-' | '+' | '=' | '<' | '>'
+        | '.' | '?' | '/' -> true
+        | _ -> false
+      ) s
+  in
+  fun s -> if no_need_to_quote s then s else Format.sprintf "|%s|" s
+
 let to_string ?(show_vars=true) x = match x with
-  | Name (n, _, _) -> Hstring.view n
+  | Name (n, _, _) -> name_to_string @@ Hstring.view n
   | Var v when show_vars -> Format.sprintf "'%s'" (Var.to_string v)
   | Var v -> Var.to_string v
   | Int n -> Z.to_string n

tests/smtlib/testfile-quoted1.dolmen.expected

@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun |fail))| () Int 0)
+)

tests/smtlib/testfile-quoted1.dolmen.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const |fail))| Int)
+(assert (= |fail))| 0))
+(check-sat)
+(get-model)