From 97a035fd6d8274b26001c9961c6e1976a2a8d9eb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 13 Jul 2021 19:43:12 +0200
Subject: [PATCH] add char sort to .net

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/CMakeLists.txt |  1 +
 src/api/dotnet/CharSort.cs    | 35 +++++++++++++++++++++++++++++++++++
 src/api/dotnet/Context.cs     | 26 +++++++++++++++++++++++---
 3 files changed, 59 insertions(+), 3 deletions(-)
 create mode 100644 src/api/dotnet/CharSort.cs

diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt
index c7ae98762..98d4b9503 100644
--- a/src/api/dotnet/CMakeLists.txt
+++ b/src/api/dotnet/CMakeLists.txt
@@ -55,6 +55,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
     BitVecSort.cs
     BoolExpr.cs
     BoolSort.cs
+    CharSort.cs
     Constructor.cs
     ConstructorList.cs
     Context.cs
diff --git a/src/api/dotnet/CharSort.cs b/src/api/dotnet/CharSort.cs
new file mode 100644
index 000000000..d5410e6c4
--- /dev/null
+++ b/src/api/dotnet/CharSort.cs
@@ -0,0 +1,35 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    CharSort.cs
+
+Abstract:
+
+    Z3 Managed API: Character Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System.Diagnostics;
+using System;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    ///  A Character sort
+    /// </summary>
+    public class CharSort : Sort
+    {
+        #region Internal
+        internal CharSort(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
+        internal CharSort(Context ctx) : base(ctx, Native.Z3_mk_char_sort(ctx.nCtx)) { Debug.Assert(ctx != null); }
+        #endregion
+    }
+}
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index b4afabe0e..e63f86ca0 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -89,7 +89,6 @@ namespace Microsoft.Z3
         /// </remarks>
         public IntSymbol MkSymbol(int i)
         {
-
             return new IntSymbol(this, i);
         }
 
@@ -98,7 +97,6 @@ namespace Microsoft.Z3
         /// </summary>
         public StringSymbol MkSymbol(string name)
         {
-
             return new StringSymbol(this, name);
         }
 
@@ -107,7 +105,6 @@ namespace Microsoft.Z3
         /// </summary>
         internal Symbol[] MkSymbols(string[] names)
         {
-
             if (names == null) return null;
             Symbol[] result = new Symbol[names.Length];
             for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
@@ -120,6 +117,7 @@ namespace Microsoft.Z3
         private IntSort m_intSort = null;
         private RealSort m_realSort = null;
         private SeqSort m_stringSort = null;
+        private CharSort m_charSort = null;
 
         /// <summary>
         /// Retrieves the Boolean sort of the context.
@@ -155,6 +153,18 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Retrieves the String sort of the context.
+        /// </summary>
+        public SeqSort CharSort
+        {
+            get
+            {
+                if (m_charSort == null) m_charSort = new CharSort(this, Native.Z3_mk_char_sort(nCtx)); return m_charSort;
+            }
+        }
+
+
         /// <summary>
         /// Retrieves the String sort of the context.
         /// </summary>
@@ -2385,6 +2395,16 @@ namespace Microsoft.Z3
             return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
         }
 
+        /// <summary>
+        /// Convert a bit-vector expression, represented as an unsigned number, to a string.
+        /// </summary>
+        public SeqExpr UbvToString(Expr e)
+        {
+            Debug.Assert(e != null);
+            Debug.Assert(e is ArithExpr);
+            return new SeqExpr(this, Native.Z3_mk_ubv_to_str(nCtx, e.NativeObject));
+        }
+
         /// <summary>
         /// Convert an integer expression to a string.
         /// </summary>