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

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_numeral.cpp | 21 +++++++++++++++++++++
 src/api/c++/z3++.h      |  1 +
 src/api/python/z3/z3.py |  8 ++++++++
 src/api/z3_api.h        | 12 +++++++++++-
 4 files changed, 41 insertions(+), 1 deletion(-)

diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp
index c736c92f9..a1397a55f 100644
--- a/src/api/api_numeral.cpp
+++ b/src/api/api_numeral.cpp
@@ -180,6 +180,27 @@ extern "C" {
     }
 
 
+    Z3_string Z3_API Z3_get_numeral_binary_string(Z3_context c, Z3_ast a) {
+        Z3_TRY;
+        // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
+        LOG_Z3_get_numeral_binary_string(c, a);
+        RESET_ERROR_CODE();
+        CHECK_IS_EXPR(a, "");
+        rational r;
+        bool ok = Z3_get_numeral_rational(c, a, r);
+        if (ok && r.is_int() && !r.is_neg()) {
+            std::stringstream strm;
+            r.display_bin(strm, r.get_num_bits());
+            return mk_c(c)->mk_external_string(strm.str().c_str());
+        }
+        else {
+            SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
+            return "";
+        }
+        Z3_CATCH_RETURN("");
+
+    }
+
     Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a) {
         Z3_TRY;
         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index e37398454..b9ee0dd69 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -813,6 +813,7 @@ namespace z3 {
         bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
         bool is_numeral(std::string& s, unsigned precision) const { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; }
         bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
+        bool as_binary(std::string& s) const { return (!is_numeral()) return false; s = Z3_get_numeral_binary_string(ctx(), m_ast); check_error(); return true; }
 
         /**
            \brief Return true if this expression is an application.
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 4ea15895a..6ef0e5df6 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -2792,6 +2792,14 @@ class IntNumRef(ArithRef):
         """
         return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
 
+    def as_binary_string(self):
+        """Return a Z3 integer numeral as a Python binary string.
+        >>> v = IntVal(10)
+        >>> v.as_string()
+        '1010'
+        """
+        return Z3_get_numeral_binary_string(self.ctx_ref(), self.as_ast())
+
 class RatNumRef(ArithRef):
     """Rational values."""
 
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index f8448a81b..259c95716 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -4677,7 +4677,7 @@ extern "C" {
     Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a);
 
     /**
-       \brief Return numeral value, as a string of a numeric constant term
+       \brief Return numeral value, as a decimal string of a numeric constant term
 
        \pre Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST
 
@@ -4685,6 +4685,16 @@ extern "C" {
     */
     Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a);
 
+    /**
+       \brief Return numeral value, as a binary string of a numeric constant term
+
+       \pre Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST
+       \pre a represents a non-negative integer
+
+       def_API('Z3_get_numeral_binary_string', STRING, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_string Z3_API Z3_get_numeral_binary_string(Z3_context c, Z3_ast a);
+
     /**
        \brief Return numeral as a string in decimal notation.
        The result has at most \c precision decimal places.