From 4b346ef693b07022f4b7b145043d3866a2489e39 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 7 Jul 2020 18:58:42 -0700
Subject: [PATCH] enable binary string access to unsigned numerals over API
 #4568

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/BitVecNum.cs | 10 +++++++++-
 src/api/java/BitVecNum.java | 11 ++++++++++-
 src/api/python/z3/z3.py     |  4 ++++
 3 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/src/api/dotnet/BitVecNum.cs b/src/api/dotnet/BitVecNum.cs
index 5ee2d2ed8..f7c6988b1 100644
--- a/src/api/dotnet/BitVecNum.cs
+++ b/src/api/dotnet/BitVecNum.cs
@@ -100,13 +100,21 @@ namespace Microsoft.Z3
 #endif
 
         /// <summary>
-        /// Returns a string representation of the numeral.
+        /// Returns a decimal string representation of the numeral.
         /// </summary>        
         public override string ToString()
         {
             return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
         }
 
+        /// <summary>
+        /// Returns a binary string representation of the numeral.
+        /// </summary>        
+        public string ToBinaryString()
+        {
+            return Native.Z3_get_numeral_binary_string(Context.nCtx, NativeObject);
+        }
+
         #region Internal
         internal BitVecNum(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
         #endregion
diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java
index d6c176855..e387f86e0 100644
--- a/src/api/java/BitVecNum.java
+++ b/src/api/java/BitVecNum.java
@@ -61,7 +61,7 @@ public class BitVecNum extends BitVecExpr
     }
 
     /**
-     * Returns a string representation of the numeral.
+     * Returns a decimal string representation of the numeral.
      **/
     @Override
     public String toString()
@@ -69,6 +69,15 @@ public class BitVecNum extends BitVecExpr
         return Native.getNumeralString(getContext().nCtx(), getNativeObject());
     }
 
+    /**
+     * Returns a binary string representation of the numeral.
+     **/
+    @Override
+    public String toBinaryString()
+    {
+        return Native.getNumeralBinaryString(getContext().nCtx(), getNativeObject());
+    }
+
     BitVecNum(Context ctx, long obj)
     {
         super(ctx, obj);
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 6ef0e5df6..63a2531fa 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -3711,6 +3711,10 @@ class BitVecNumRef(BitVecRef):
     def as_string(self):
         return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
 
+    def as_binary_string(self):
+        return Z3_get_numeral_binary_string(self.ctx_ref(), self.as_ast())
+    
+
 def is_bv(a):
     """Return `True` if `a` is a Z3 bit-vector expression.